theory Detype_R

lemma getCTE_commute:
  assumes cte_at_modify:
   "\<And>Q. \<lbrace>\<lambda>s. P s \<and> cte_wp_at' Q dest s \<rbrace> f \<lbrace>\<lambda>a s. cte_wp_at' Q dest s\<rbrace>"
  shows "monad_commute (P and cte_at' dest) (getCTE dest) f" proof - have getsame: "\<And>x y s. (x,y)\<in> fst (getCTE dest s) \<Longrightarrow> y = s" apply (drule use_valid) prefer 3 apply (simp|wp)+ done show ?thesis apply (simp add:monad_commute_def bind_assoc getCTE_def split_def cte_at'_def) apply (clarsimp simp:bind_def split_def return_def) apply (rule conjI) apply (rule set_eqI) apply (rule iffI) apply clarsimp apply (rule bexI[rotated], assumption) apply (drule_tac Q1 ="(=) cte" in use_valid[OF _ cte_at_modify]) apply (simp add:cte_wp_at'_def) apply (simp add:cte_wp_at'_def) apply clarsimp apply (rule conjI) apply (frule_tac Q1 = "(=) cte" in use_valid[OF _ cte_at_modify]) apply (clarsimp simp:cte_wp_at'_def ko_wp_at'_def) apply (clarsimp simp:cte_wp_at'_def) apply (rule bexI[rotated], assumption) apply (metis fst_eqD getObject_cte_det snd_eqD) apply (cut_tac no_failD[OF no_fail_getCTE[unfolded getCTE_def]]) prefer 2 apply (simp add:cte_wp_at'_def) apply fastforce apply simp apply (rule iffI) apply clarsimp+ apply (cut_tac s = b in no_failD[OF no_fail_getCTE[unfolded getCTE_def]]) prefer 2 apply fastforce apply (drule_tac Q1 = "(=) cte" in use_valid[OF _ cte_at_modify]) apply (simp add:cte_wp_at'_def) apply (simp add:cte_wp_at_ctes_of) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (P and cte_wp_at' (\<lambda>_. True) dest) (getCTE dest) f proof (state)
goal (1 subgoal):
 1. monad_commute (P and cte_wp_at' (\<lambda>_. True) dest) (getCTE dest) f proof (prove)
goal (1 subgoal):
 1. \<And>x y s. (x, y) \<in> fst (getCTE dest s) \<Longrightarrow> y = s proof (prove)
goal (3 subgoals):
 1. \<And>x y s. \<lbrace>?P x y s\<rbrace> getCTE dest \<lbrace>?Q x y s\<rbrace>
 2. \<And>x y s. ?P x y s s
 3. \<And>x y s. ?Q x y s x y \<Longrightarrow> y = s proof (prove)
goal (3 subgoals):
 1. \<And>x y s. ?Q x y s x y \<Longrightarrow> y = s
 2. \<And>x y s. \<lbrace>?P x y s\<rbrace> getCTE dest \<lbrace>?Q x y s\<rbrace>
 3. \<And>x y s. ?P x y s s proof (prove)
goal:
No subgoals! proof (state)
this:
(?x, ?y) \<in> fst (getCTE dest ?s) \<Longrightarrow> ?y = ?s

goal (1 subgoal):
 1. monad_commute (P and cte_wp_at' (\<lambda>_. True) dest) (getCTE dest) f proof (prove)
goal (1 subgoal):
 1. monad_commute (P and cte_wp_at' (\<lambda>_. True) dest) (getCTE dest) f proof (prove)
goal (1 subgoal):
 1. \<forall>s. P s \<and> (\<exists>cte. fst (getObject dest s) = {(cte, s)}) \<longrightarrow> (do x <- getObject dest;
y <- f;
return (x, y)
od) s = (do y <- f;
x <- getObject dest;
return (x, y)
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (f s). {((cte, fst x), snd x)}) = (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (getObject dest (snd x)). {((fst xa, fst x), snd xa)}) \<and> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (f s). {((cte, fst x), snd x)}) = (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (getObject dest (snd x)). {((fst xa, fst x), snd xa)})
 2. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte x. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (x \<in> (\<Union>x\<in>fst (f s). {((cte, fst x), snd x)})) = (x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (getObject dest (snd x)). {((fst xa, fst x), snd xa)}))
 2. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (3 subgoals):
 1. \<And>s cte x. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; x \<in> (\<Union>x\<in>fst (f s). {((cte, fst x), snd x)})\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (getObject dest (snd x)). {((fst xa, fst x), snd xa)})
 2. \<And>s cte x. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (getObject dest (snd x)). {((fst xa, fst x), snd xa)})\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>fst (f s). {((cte, fst x), snd x)})
 3. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (3 subgoals):
 1. \<And>s cte aa bb. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; (aa, bb) \<in> fst (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). \<exists>xa\<in>fst (getObject dest (snd x)). cte = fst xa \<and> aa = fst x \<and> bb = snd xa
 2. \<And>s cte x. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (getObject dest (snd x)). {((fst xa, fst x), snd xa)})\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>fst (f s). {((cte, fst x), snd x)})
 3. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (3 subgoals):
 1. \<And>s cte aa bb. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; (aa, bb) \<in> fst (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (getObject dest (snd (aa, bb))). cte = fst x \<and> aa = fst (aa, bb) \<and> bb = snd x
 2. \<And>s cte x. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (getObject dest (snd x)). {((fst xa, fst x), snd xa)})\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>fst (f s). {((cte, fst x), snd x)})
 3. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (4 subgoals):
 1. \<And>s cte aa bb. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> P s \<and> cte_wp_at' ((=) cte) dest s
 2. \<And>s cte aa bb. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; cte_wp_at' ((=) cte) dest bb\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (getObject dest (snd (aa, bb))). cte = fst x \<and> aa = fst (aa, bb) \<and> bb = snd x
 3. \<And>s cte x. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (getObject dest (snd x)). {((fst xa, fst x), snd xa)})\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>fst (f s). {((cte, fst x), snd x)})
 4. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (3 subgoals):
 1. \<And>s cte aa bb. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; cte_wp_at' ((=) cte) dest bb\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (getObject dest (snd (aa, bb))). cte = fst x \<and> aa = fst (aa, bb) \<and> bb = snd x
 2. \<And>s cte x. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (getObject dest (snd x)). {((fst xa, fst x), snd xa)})\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>fst (f s). {((cte, fst x), snd x)})
 3. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte x. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (getObject dest (snd x)). {((fst xa, fst x), snd xa)})\<rbrakk> \<Longrightarrow> x \<in> (\<Union>x\<in>fst (f s). {((cte, fst x), snd x)})
 2. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte aa bb ab bc. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; (aa, bb) \<in> fst (f s); (ab, bc) \<in> fst (getObject dest bb)\<rbrakk> \<Longrightarrow> ab = cte \<and> (\<exists>x\<in>fst (f s). aa = fst x \<and> bc = snd x)
 2. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (3 subgoals):
 1. \<And>s cte aa bb ab bc. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; (aa, bb) \<in> fst (f s); (ab, bc) \<in> fst (getObject dest bb)\<rbrakk> \<Longrightarrow> ab = cte
 2. \<And>s cte aa bb ab bc. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; (aa, bb) \<in> fst (f s); (ab, bc) \<in> fst (getObject dest bb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). aa = fst x \<and> bc = snd x
 3. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (4 subgoals):
 1. \<And>s cte aa bb ab bc. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; (aa, bb) \<in> fst (f s); (ab, bc) \<in> fst (getObject dest bb)\<rbrakk> \<Longrightarrow> P s \<and> cte_wp_at' ((=) cte) dest s
 2. \<And>s cte aa bb ab bc. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; (aa, bb) \<in> fst (f s); (ab, bc) \<in> fst (getObject dest bb); cte_wp_at' ((=) cte) dest bb\<rbrakk> \<Longrightarrow> ab = cte
 3. \<And>s cte aa bb ab bc. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; (aa, bb) \<in> fst (f s); (ab, bc) \<in> fst (getObject dest bb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). aa = fst x \<and> bc = snd x
 4. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (3 subgoals):
 1. \<And>s cte aa bb ab bc. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; (aa, bb) \<in> fst (f s); (ab, bc) \<in> fst (getObject dest bb); cte_wp_at' ((=) cte) dest bb\<rbrakk> \<Longrightarrow> ab = cte
 2. \<And>s cte aa bb ab bc. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; (aa, bb) \<in> fst (f s); (ab, bc) \<in> fst (getObject dest bb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). aa = fst x \<and> bc = snd x
 3. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte aa bb ab bc. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; (aa, bb) \<in> fst (f s); (ab, bc) \<in> fst (getObject dest bb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). aa = fst x \<and> bc = snd x
 2. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte aa bb ab bc. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; (aa, bb) \<in> fst (f s); (ab, bc) \<in> fst (getObject dest bb)\<rbrakk> \<Longrightarrow> aa = fst (aa, bb) \<and> bc = snd (aa, bb)
 2. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject (?p82 s cte) (?s81 s cte))\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s))
 2. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (?p82 s cte) (?s81 s cte) proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (?p82 s cte) (?s81 s cte)
 2. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject (?p82 s cte) (?s81 s cte))\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}\<rbrakk> \<Longrightarrow> \<exists>ctea. fst (getObject (?p82 s cte) (?s81 s cte)) = {(ctea, ?s81 s cte)}
 2. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject (?p82 s cte) (?s81 s cte))\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject dest s)\<rbrakk> \<Longrightarrow> (snd (f s) \<or> snd (getObject dest s)) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject dest s)\<rbrakk> \<Longrightarrow> snd (f s) = ((\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject dest s); snd (f s)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)
 2. \<And>s cte. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject dest s); (\<exists>x\<in>fst (f s). snd (getObject dest (snd x))) \<or> snd (f s)\<rbrakk> \<Longrightarrow> snd (f s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte a b. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject dest s); (a, b) \<in> fst (f s); snd (getObject dest b)\<rbrakk> \<Longrightarrow> snd (f s) proof (prove)
goal (2 subgoals):
 1. \<And>s cte a b. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject dest s); (a, b) \<in> fst (f s); snd (getObject dest b)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (?p121 s cte a b) b
 2. \<And>s cte a b. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject dest s); (a, b) \<in> fst (f s); snd (getObject dest b); \<not> snd (getObject (?p121 s cte a b) b)\<rbrakk> \<Longrightarrow> snd (f s) proof (prove)
goal (2 subgoals):
 1. \<And>s cte a b. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject dest s); (a, b) \<in> fst (f s); snd (getObject dest b); \<not> snd (getObject (?p121 s cte a b) b)\<rbrakk> \<Longrightarrow> snd (f s)
 2. \<And>s cte a b. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject dest s); (a, b) \<in> fst (f s); snd (getObject dest b)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (?p121 s cte a b) b proof (prove)
goal (1 subgoal):
 1. \<And>s cte a b. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject dest s); (a, b) \<in> fst (f s); snd (getObject dest b)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) dest b proof (prove)
goal (2 subgoals):
 1. \<And>s cte a b. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject dest s); snd (getObject dest b)\<rbrakk> \<Longrightarrow> P s \<and> cte_wp_at' ((=) cte) dest s
 2. \<And>s cte a b. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject dest s); snd (getObject dest b); cte_wp_at' ((=) cte) dest b\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) dest b proof (prove)
goal (1 subgoal):
 1. \<And>s cte a b. \<lbrakk>P s; fst (getObject dest s) = {(cte, s)}; \<not> snd (getObject dest s); snd (getObject dest b); cte_wp_at' ((=) cte) dest b\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) dest b proof (prove)
goal:
No subgoals! proof (state)
this:
monad_commute (P and cte_wp_at' (\<lambda>_. True) dest) (getCTE dest) f

goal:
No subgoals!