theory Detype_R

lemma setCTE_gets_globalPD_commute:
  "monad_commute
     (cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned')
     (setCTE src cte) (gets (armKSGlobalPD \<circ> ksArchState))" apply (simp add:setCTE_def2) apply (rule monad_commute_guard_imp) apply (rule commute_commute[OF monad_commute_split[where Q = "\<lambda>r. \<top>"]]) apply (clarsimp simp:monad_commute_def gets_def simpler_modify_def bind_def get_def return_def) apply (rule commute_commute[OF locateCTE_commute]) apply (wp locateCTE_cte_no_fail)+ apply clarsimp apply (wp|clarsimp)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') (setCTE src cte) (gets (armKSGlobalPD \<circ> ksArchState)) proof (prove)
goal (1 subgoal):
 1. monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') (do ptr <- locateCTE src;
modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> cte_update cte (the (ps ptr)) src ptr)))
od) (gets (armKSGlobalPD \<circ> ksArchState)) proof (prove)
goal (2 subgoals):
 1. monad_commute ?P (do ptr <- locateCTE src;
modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> cte_update cte (the (ps ptr)) src ptr)))
od) (gets (armKSGlobalPD \<circ> ksArchState))
 2. \<And>s. (cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') s \<Longrightarrow> ?P s proof (prove)
goal (4 subgoals):
 1. \<And>r. monad_commute (\<lambda>_. True) (gets (armKSGlobalPD \<circ> ksArchState)) (modify (ksPSpace_update (\<lambda>ps. ps(r \<mapsto> cte_update cte (the (ps r)) src r))))
 2. monad_commute ?P4 (gets (armKSGlobalPD \<circ> ksArchState)) (locateCTE src)
 3. \<lbrace>?P'4\<rbrace> locateCTE src \<lbrace>\<lambda>r _. True\<rbrace>
 4. \<And>s. (cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') s \<Longrightarrow> (?P4 and ?P'4) s proof (prove)
goal (3 subgoals):
 1. monad_commute ?P4 (gets (armKSGlobalPD \<circ> ksArchState)) (locateCTE src)
 2. \<lbrace>?P'4\<rbrace> locateCTE src \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<And>s. (cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') s \<Longrightarrow> (?P4 and ?P'4) s proof (prove)
goal (8 subgoals):
 1. no_fail ?P0.22 (gets (armKSGlobalPD \<circ> ksArchState))
 2. no_fail ?P1.22 (locateCTE src)
 3. \<lbrace>?P2.22\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>a. pspace_distinct'\<rbrace>
 4. \<lbrace>?P3.22\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>a. pspace_aligned'\<rbrace>
 5. \<And>Q dest. \<lbrace>\<lambda>s. (?P0.22 and ?P1.22 and ?P2.22 and ?P3.22) s \<and> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest s\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>a. ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest\<rbrace>
 6. \<And>dest. \<lbrace>\<lambda>s. (?P0.22 and ?P1.22 and ?P2.22 and ?P3.22) s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 7. \<lbrace>?P'4\<rbrace> locateCTE src \<lbrace>\<lambda>r _. True\<rbrace>
 8. \<And>s. (cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') s \<Longrightarrow> (?P0.22 and ?P1.22 and ?P2.22 and ?P3.22 and ?P4.22 and ?P5.22 and pspace_aligned' and pspace_distinct' and ?P'4) s proof (prove)
goal (4 subgoals):
 1. \<And>Q dest s. ((\<lambda>_. True) and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') s \<and> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest s \<Longrightarrow> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest s
 2. \<And>dest. \<lbrace>\<lambda>s. ((\<lambda>_. True) and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 3. \<lbrace>?P'4\<rbrace> locateCTE src \<lbrace>\<lambda>r _. True\<rbrace>
 4. \<And>s. (cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') s \<Longrightarrow> ((\<lambda>_. True) and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned' and ?P4.22 and ?P5.22 and pspace_aligned' and pspace_distinct' and ?P'4) s proof (prove)
goal (3 subgoals):
 1. \<And>dest. \<lbrace>\<lambda>s. ((\<lambda>_. True) and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') s \<and> cte_wp_at' (\<lambda>_. True) dest s\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) dest\<rbrace>
 2. \<lbrace>?P'4\<rbrace> locateCTE src \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<And>s. (cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned') s \<Longrightarrow> ((\<lambda>_. True) and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned' and ?P4.22 and ?P5.22 and pspace_aligned' and pspace_distinct' and ?P'4) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cte_wp_at' (\<lambda>_. True) src s; pspace_distinct' s; pspace_aligned' s\<rbrakk> \<Longrightarrow> ?P4.22 s \<and> ?P5.22 s proof (prove)
goal:
No subgoals!