theory Nondet_While_Loop_Rules

lemma validNF_whileLoopE:
  assumes pre: "\<And>s. P r s \<Longrightarrow> I r s"
  and inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> ((r', s'), (r, s)) \<in> R \<rbrace>,\<lbrace> E \<rbrace>!"
  and wf: "wf R"
  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
  shows "\<lbrace> P r \<rbrace> whileLoopE C B r \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>!" apply (unfold validE_NF_alt_def whileLoopE_def) apply (rule validNF_whileLoop [where
                I="\<lambda>r s. case r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s" and
                R="{((r', s'), (r, s)). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<union>
                   {((r', s'), (r, s)). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'),(x, s)) \<in> R}"]) apply (simp add: pre) apply (insert inv)[1] apply (fastforce simp: lift_def validNF_def valid_def validE_NF_def throwError_def no_fail_def
                           return_def validE_def
                     split: sum.splits prod.splits) apply (rule wf_Un) apply (rule wf_custom_measure [where f="\<lambda>(r, s). case r of Inl _ \<Rightarrow> 0 | _ \<Rightarrow> 1"]) apply clarsimp apply (insert wf_inv_image [OF wf, where f="\<lambda>(r, s). (projr r, s)"]) apply (drule wf_Int1 [where r'="{((r', s'),(r, s)). (\<exists>x. r = Inr x) \<and> (\<exists>x. r' = Inr x)}"]) apply (erule wf_subset) apply (fastforce simp: inv_image_def split: prod.splits sum.splits) apply fastforce apply (fastforce split: sum.splits intro: post_cond) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoopE C
  B r \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r) \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>! proof (prove)
goal (4 subgoals):
 1. \<And>s. P r s \<Longrightarrow> case Inr r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s
 2. \<And>r s. \<lbrace>\<lambda>s'. (case r of Inl x \<Rightarrow> E x s' | Inr x \<Rightarrow> I x s') \<and> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s') \<and> s' = s\<rbrace> lift B r \<lbrace>\<lambda>r' s'. (case r' of Inl x \<Rightarrow> E x s' | Inr x \<Rightarrow> I x s') \<and> ((r', s'), r, s) \<in> {((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<union> {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R}\<rbrace>!
 3. wf ({((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<union> {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R})
 4. \<And>r s. \<lbrakk>case r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s; \<not> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)\<rbrakk> \<Longrightarrow> case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. \<And>r s. \<lbrace>\<lambda>s'. (case r of Inl x \<Rightarrow> E x s' | Inr x \<Rightarrow> I x s') \<and> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s') \<and> s' = s\<rbrace> lift B r \<lbrace>\<lambda>r' s'. (case r' of Inl x \<Rightarrow> E x s' | Inr x \<Rightarrow> I x s') \<and> ((r', s'), r, s) \<in> {((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<union> {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R}\<rbrace>!
 2. wf ({((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<union> {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R})
 3. \<And>r s. \<lbrakk>case r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s; \<not> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)\<rbrakk> \<Longrightarrow> case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. \<And>r s. (\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>, \<lbrace>E\<rbrace>!) \<Longrightarrow> \<lbrace>\<lambda>s'. (case r of Inl x \<Rightarrow> E x s' | Inr x \<Rightarrow> I x s') \<and> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s') \<and> s' = s\<rbrace> lift B r \<lbrace>\<lambda>r' s'. (case r' of Inl x \<Rightarrow> E x s' | Inr x \<Rightarrow> I x s') \<and> ((r', s'), r, s) \<in> {((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<union> {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R}\<rbrace>!
 2. wf ({((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<union> {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R})
 3. \<And>r s. \<lbrakk>case r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s; \<not> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)\<rbrakk> \<Longrightarrow> case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. wf ({((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<union> {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R})
 2. \<And>r s. \<lbrakk>case r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s; \<not> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)\<rbrakk> \<Longrightarrow> case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s proof (prove)
goal (4 subgoals):
 1. wf {((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x}
 2. wf {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R}
 3. Domain {((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<inter> Range {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R} = {}
 4. \<And>r s. \<lbrakk>case r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s; \<not> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)\<rbrakk> \<Longrightarrow> case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s proof (prove)
goal (4 subgoals):
 1. \<And>a b. (a, b) \<in> {((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<Longrightarrow> (case a of (Inl x, s) \<Rightarrow> 0 | (Inr b, s) \<Rightarrow> 1) < (case b of (Inl x, s) \<Rightarrow> 0 | (Inr b, s) \<Rightarrow> 1)
 2. wf {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R}
 3. Domain {((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<inter> Range {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R} = {}
 4. \<And>r s. \<lbrakk>case r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s; \<not> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)\<rbrakk> \<Longrightarrow> case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. wf {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R}
 2. Domain {((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<inter> Range {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R} = {}
 3. \<And>r s. \<lbrakk>case r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s; \<not> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)\<rbrakk> \<Longrightarrow> case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. wf (inv_image R (\<lambda>(r, s). (projr r, s))) \<Longrightarrow> wf {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R}
 2. wf (inv_image R (\<lambda>(r, s). (projr r, s))) \<Longrightarrow> Domain {((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<inter> Range {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R} = {}
 3. \<And>r s. \<lbrakk>case r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s; \<not> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s); wf (inv_image R (\<lambda>(r, s). (projr r, s)))\<rbrakk> \<Longrightarrow> case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. wf (inv_image R (\<lambda>(r, s). (projr r, s)) \<inter> {((r', s'), r, s). (\<exists>x. r = Inr x) \<and> (\<exists>x. r' = Inr x)}) \<Longrightarrow> wf {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R}
 2. wf (inv_image R (\<lambda>(r, s). (projr r, s))) \<Longrightarrow> Domain {((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<inter> Range {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R} = {}
 3. \<And>r s. \<lbrakk>case r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s; \<not> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s); wf (inv_image R (\<lambda>(r, s). (projr r, s)))\<rbrakk> \<Longrightarrow> case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R} \<subseteq> inv_image R (\<lambda>(r, s). (projr r, s)) \<inter> {((r', s'), r, s). (\<exists>x. r = Inr x) \<and> (\<exists>x. r' = Inr x)}
 2. wf (inv_image R (\<lambda>(r, s). (projr r, s))) \<Longrightarrow> Domain {((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<inter> Range {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R} = {}
 3. \<And>r s. \<lbrakk>case r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s; \<not> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s); wf (inv_image R (\<lambda>(r, s). (projr r, s)))\<rbrakk> \<Longrightarrow> case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. wf (inv_image R (\<lambda>(r, s). (projr r, s))) \<Longrightarrow> Domain {((r', s'), r, s). \<exists>x x'. r' = Inl x' \<and> r = Inr x} \<inter> Range {((r', s'), r, s). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'), x, s) \<in> R} = {}
 2. \<And>r s. \<lbrakk>case r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s; \<not> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s); wf (inv_image R (\<lambda>(r, s). (projr r, s)))\<rbrakk> \<Longrightarrow> case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>case r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s; \<not> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s); wf (inv_image R (\<lambda>(r, s). (projr r, s)))\<rbrakk> \<Longrightarrow> case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s proof (prove)
goal:
No subgoals!