theory Retype_R

lemma mapM_x_modify_futz:
  assumes "\<forall>ptr\<in>set ptrs. ekheap s ptr \<noteq> None"
  shows "mapM_x (ethread_set F) (rev ptrs) s
       = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := Some (F (the (ekh p))))) ptrs)) s" (is "?lhs ptrs s = ?rhs ptrs s") using assms proof(induct ptrs arbitrary: s) case Nil thus ?case by (simp add: mapM_x_Nil return_def simpler_modify_def) next case (Cons ptr ptrs s) have "?rhs (ptr # ptrs) s
      = (do modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs));
            modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))
        od) s" by (simp only: foldr_Cons modify_ekheap_update_comp_futz) simp also have "... = (do ?lhs ptrs;
                      modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))
                    od) s" apply (rule monad_eq_split_tail) apply simp apply (rule Cons.hyps[symmetric]) using Cons.prems apply force done also have "... = ?lhs (ptr # ptrs) s" apply (simp add: mapM_x_append mapM_x_singleton) apply (rule monad_eq_split2[OF refl, where
                 P="\<lambda>s. \<forall>ptr\<in>set (ptr # ptrs). ekheap s ptr \<noteq> None"
             and Q="\<lambda>_ s. ekheap s ptr \<noteq> None"]) apply (simp add: ethread_set_def
                       assert_opt_def get_etcb_def gets_the_def gets_def get_def modify_def put_def set_eobject_def
                       bind_def fail_def return_def split_def
                split: option.splits) apply ((wp mapM_x_wp[OF _ subset_refl] | simp add: ethread_set_def set_eobject_def)+)[1] using Cons.prems apply force done finally show ?case by (rule sym) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x (ethread_set F) (rev ptrs) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) s proof (prove)
using this:
\<forall>ptr\<in>set ptrs. ekheap s ptr \<noteq> None

goal (1 subgoal):
 1. mapM_x (ethread_set F) (rev ptrs) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) s proof (state)
goal (2 subgoals):
 1. \<And>s. \<forall>ptr\<in>set []. ekheap s ptr \<noteq> None \<Longrightarrow> mapM_x (ethread_set F) (rev []) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) [])) s
 2. \<And>a ptrs s. \<lbrakk>\<And>s. \<forall>ptr\<in>set ptrs. ekheap s ptr \<noteq> None \<Longrightarrow> mapM_x (ethread_set F) (rev ptrs) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) s; \<forall>ptr\<in>set (a # ptrs). ekheap s ptr \<noteq> None\<rbrakk> \<Longrightarrow> mapM_x (ethread_set F) (rev (a # ptrs)) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (a # ptrs))) s proof (state)
this:
\<forall>ptr\<in>set []. ekheap s ptr \<noteq> None

goal (2 subgoals):
 1. \<And>s. \<forall>ptr\<in>set []. ekheap s ptr \<noteq> None \<Longrightarrow> mapM_x (ethread_set F) (rev []) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) [])) s
 2. \<And>a ptrs s. \<lbrakk>\<And>s. \<forall>ptr\<in>set ptrs. ekheap s ptr \<noteq> None \<Longrightarrow> mapM_x (ethread_set F) (rev ptrs) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) s; \<forall>ptr\<in>set (a # ptrs). ekheap s ptr \<noteq> None\<rbrakk> \<Longrightarrow> mapM_x (ethread_set F) (rev (a # ptrs)) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (a # ptrs))) s proof (prove)
using this:
\<forall>ptr\<in>set []. ekheap s ptr \<noteq> None

goal (1 subgoal):
 1. mapM_x (ethread_set F) (rev []) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) [])) s proof (state)
this:
mapM_x (ethread_set F) (rev []) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) [])) s

goal (1 subgoal):
 1. \<And>a ptrs s. \<lbrakk>\<And>s. \<forall>ptr\<in>set ptrs. ekheap s ptr \<noteq> None \<Longrightarrow> mapM_x (ethread_set F) (rev ptrs) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) s; \<forall>ptr\<in>set (a # ptrs). ekheap s ptr \<noteq> None\<rbrakk> \<Longrightarrow> mapM_x (ethread_set F) (rev (a # ptrs)) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (a # ptrs))) s proof (state)
goal (1 subgoal):
 1. \<And>a ptrs s. \<lbrakk>\<And>s. \<forall>ptr\<in>set ptrs. ekheap s ptr \<noteq> None \<Longrightarrow> mapM_x (ethread_set F) (rev ptrs) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) s; \<forall>ptr\<in>set (a # ptrs). ekheap s ptr \<noteq> None\<rbrakk> \<Longrightarrow> mapM_x (ethread_set F) (rev (a # ptrs)) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (a # ptrs))) s proof (state)
this:
\<forall>ptr\<in>set ptrs. ekheap ?s ptr \<noteq> None \<Longrightarrow> mapM_x (ethread_set F) (rev ptrs) ?s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) ?s
\<forall>ptr\<in>set (ptr # ptrs). ekheap s ptr \<noteq> None

goal (1 subgoal):
 1. \<And>a ptrs s. \<lbrakk>\<And>s. \<forall>ptr\<in>set ptrs. ekheap s ptr \<noteq> None \<Longrightarrow> mapM_x (ethread_set F) (rev ptrs) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) s; \<forall>ptr\<in>set (a # ptrs). ekheap s ptr \<noteq> None\<rbrakk> \<Longrightarrow> mapM_x (ethread_set F) (rev (a # ptrs)) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (a # ptrs))) s proof (prove)
goal (1 subgoal):
 1. modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (ptr # ptrs))) s = (do modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs));
modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))
od) s proof (state)
this:
modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (ptr # ptrs))) s = (do modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs));
modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))
od) s

goal (1 subgoal):
 1. \<And>a ptrs s. \<lbrakk>\<And>s. \<forall>ptr\<in>set ptrs. ekheap s ptr \<noteq> None \<Longrightarrow> mapM_x (ethread_set F) (rev ptrs) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) s; \<forall>ptr\<in>set (a # ptrs). ekheap s ptr \<noteq> None\<rbrakk> \<Longrightarrow> mapM_x (ethread_set F) (rev (a # ptrs)) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (a # ptrs))) s proof (state)
this:
modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (ptr # ptrs))) s = (do modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs));
modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))
od) s

goal (1 subgoal):
 1. \<And>a ptrs s. \<lbrakk>\<And>s. \<forall>ptr\<in>set ptrs. ekheap s ptr \<noteq> None \<Longrightarrow> mapM_x (ethread_set F) (rev ptrs) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) s; \<forall>ptr\<in>set (a # ptrs). ekheap s ptr \<noteq> None\<rbrakk> \<Longrightarrow> mapM_x (ethread_set F) (rev (a # ptrs)) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (a # ptrs))) s proof (prove)
goal (1 subgoal):
 1. (do modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs));
modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))
od) s = (do mapM_x (ethread_set F) (rev ptrs);
modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))
od) s proof (prove)
goal (2 subgoals):
 1. K_bind (modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))) = K_bind (modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr))))))
 2. modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) s = mapM_x (ethread_set F) (rev ptrs) s proof (prove)
goal (1 subgoal):
 1. modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) s = mapM_x (ethread_set F) (rev ptrs) s proof (prove)
goal (1 subgoal):
 1. \<forall>ptr\<in>set ptrs. ekheap s ptr \<noteq> None proof (prove)
using this:
\<forall>ptr\<in>set (ptr # ptrs). ekheap s ptr \<noteq> None

goal (1 subgoal):
 1. \<forall>ptr\<in>set ptrs. ekheap s ptr \<noteq> None proof (prove)
goal:
No subgoals! proof (state)
this:
(do modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs));
modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))
od) s = (do mapM_x (ethread_set F) (rev ptrs);
modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))
od) s

goal (1 subgoal):
 1. \<And>a ptrs s. \<lbrakk>\<And>s. \<forall>ptr\<in>set ptrs. ekheap s ptr \<noteq> None \<Longrightarrow> mapM_x (ethread_set F) (rev ptrs) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) s; \<forall>ptr\<in>set (a # ptrs). ekheap s ptr \<noteq> None\<rbrakk> \<Longrightarrow> mapM_x (ethread_set F) (rev (a # ptrs)) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (a # ptrs))) s proof (state)
this:
(do modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs));
modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))
od) s = (do mapM_x (ethread_set F) (rev ptrs);
modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))
od) s

goal (1 subgoal):
 1. \<And>a ptrs s. \<lbrakk>\<And>s. \<forall>ptr\<in>set ptrs. ekheap s ptr \<noteq> None \<Longrightarrow> mapM_x (ethread_set F) (rev ptrs) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) s; \<forall>ptr\<in>set (a # ptrs). ekheap s ptr \<noteq> None\<rbrakk> \<Longrightarrow> mapM_x (ethread_set F) (rev (a # ptrs)) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (a # ptrs))) s proof (prove)
goal (1 subgoal):
 1. (do mapM_x (ethread_set F) (rev ptrs);
modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))
od) s = mapM_x (ethread_set F) (rev (ptr # ptrs)) s proof (prove)
goal (1 subgoal):
 1. (do y <- mapM_x (ethread_set F) (rev ptrs);
modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))
od) s = (do x <- mapM_x (ethread_set F) (rev ptrs);
ethread_set F ptr
od) s proof (prove)
goal (3 subgoals):
 1. \<And>r s. ekheap s ptr \<noteq> None \<Longrightarrow> modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr))))) s = ethread_set F ptr s
 2. \<lbrace>\<lambda>s. \<forall>ptr\<in>set (ptr # ptrs). ekheap s ptr \<noteq> None\<rbrace> mapM_x (ethread_set F) (rev ptrs) \<lbrace>\<lambda>r s. ekheap s ptr \<noteq> None\<rbrace>
 3. \<forall>ptr\<in>set (ptr # ptrs). ekheap s ptr \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<forall>ptr\<in>set (ptr # ptrs). ekheap s ptr \<noteq> None\<rbrace> mapM_x (ethread_set F) (rev ptrs) \<lbrace>\<lambda>r s. ekheap s ptr \<noteq> None\<rbrace>
 2. \<forall>ptr\<in>set (ptr # ptrs). ekheap s ptr \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<forall>ptr\<in>set (ptr # ptrs). ekheap s ptr \<noteq> None proof (prove)
using this:
\<forall>ptr\<in>set (ptr # ptrs). ekheap s ptr \<noteq> None

goal (1 subgoal):
 1. \<forall>ptr\<in>set (ptr # ptrs). ekheap s ptr \<noteq> None proof (prove)
goal:
No subgoals! proof (state)
this:
(do mapM_x (ethread_set F) (rev ptrs);
modify (ekheap_update (\<lambda>ekh. ekh(ptr \<mapsto> F (the (ekh ptr)))))
od) s = mapM_x (ethread_set F) (rev (ptr # ptrs)) s

goal (1 subgoal):
 1. \<And>a ptrs s. \<lbrakk>\<And>s. \<forall>ptr\<in>set ptrs. ekheap s ptr \<noteq> None \<Longrightarrow> mapM_x (ethread_set F) (rev ptrs) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) ptrs)) s; \<forall>ptr\<in>set (a # ptrs). ekheap s ptr \<noteq> None\<rbrakk> \<Longrightarrow> mapM_x (ethread_set F) (rev (a # ptrs)) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (a # ptrs))) s proof (chain)
picking this:
modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (ptr # ptrs))) s = mapM_x (ethread_set F) (rev (ptr # ptrs)) s proof (prove)
using this:
modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (ptr # ptrs))) s = mapM_x (ethread_set F) (rev (ptr # ptrs)) s

goal (1 subgoal):
 1. mapM_x (ethread_set F) (rev (ptr # ptrs)) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (ptr # ptrs))) s proof (state)
this:
mapM_x (ethread_set F) (rev (ptr # ptrs)) s = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> F (the (ekh p)))) (ptr # ptrs))) s

goal:
No subgoals!