theory Detype_R

lemma getPDE_setCTE_commute:
  "monad_commute
     (pde_at' ptr and pspace_distinct' and cte_wp_at' (\<lambda>_. True) src)
     (setCTE src cte)
     (getObject ptr :: KernelStateData_H.kernel_state \<Rightarrow>
                       (pde \<times> KernelStateData_H.kernel_state) set \<times> bool)" apply (rule commute_name_pre_state) apply (clarsimp simp:typ_at'_def ko_wp_at'_def) apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply clarsimp apply (rename_tac pde) apply (subgoal_tac "ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s") prefer 2 apply (clarsimp simp:ko_wp_at'_def) apply (rule monad_commute_guard_imp) apply (rule commute_commute) apply (rule commute_rewrite[OF getPDE_det,where R = \<top>]) apply assumption apply (wp setCTE_pde_at') apply (simp add:monad_commute_def bind_def) apply (auto simp:ko_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (pde_at' ptr and pspace_distinct' and cte_wp_at' (\<lambda>_. True) src) (setCTE src cte) (getObject ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s. (pde_at' ptr and pspace_distinct' and cte_wp_at' (\<lambda>_. True) src) s \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (getObject ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); koTypeOf ko = ArchT PDET; ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (getObject ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s ko x8. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch x8); is_aligned ptr (objBitsKO (KOArch x8)); archTypeOf x8 = PDET; ps_clear ptr (objBitsKO (KOArch x8)) s; ko = KOArch x8\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (getObject ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch arch_kernel_object); is_aligned ptr (objBitsKO (KOArch arch_kernel_object)); archTypeOf arch_kernel_object = PDET; ps_clear ptr (objBitsKO (KOArch arch_kernel_object)) s; ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (getObject ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object x3. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE x3)); is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s; ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (getObject ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s x3. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE x3)); is_aligned ptr (objBitsKO (KOArch (KOPDE x3))); ps_clear ptr (objBitsKO (KOArch (KOPDE x3))) s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (getObject ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (getObject ptr) proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (getObject ptr)
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (getObject ptr) proof (prove)
goal (1 subgoal):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (setCTE src cte) (getObject ptr) proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (?P13 s pde) (setCTE src cte) (getObject ptr)
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> ?P13 s pde sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (?P13 s pde) (getObject ptr) (setCTE src cte)
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> ?P13 s pde sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde sa. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; ?Q18 s pde sa\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE (?pde19 s pde sa)))) ptr sa
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P18 s pde\<rbrace> setCTE src cte \<lbrace>\<lambda>x. ?Q18 s pde\<rbrace>
 3. \<And>s pde. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (\<lambda>_. True) (\<lambda>sa. ({(?pde19 s pde sa, sa)}, False)) (setCTE src cte)
 4. \<And>s pde sa. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (?P18 s pde and ?Q18 s pde and (\<lambda>_. True)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> \<lbrace>?P18 s pde\<rbrace> setCTE src cte \<lbrace>\<lambda>x sa. ko_wp_at' ((=) (KOArch (KOPDE (?pde19 s pde sa)))) ptr sa\<rbrace>
 2. \<And>s pde. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (\<lambda>_. True) (\<lambda>sa. ({(?pde19 s pde sa, sa)}, False)) (setCTE src cte)
 3. \<And>s pde sa. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (?P18 s pde and (\<lambda>sa. ko_wp_at' ((=) (KOArch (KOPDE (?pde19 s pde sa)))) ptr sa) and (\<lambda>_. True)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s\<rbrakk> \<Longrightarrow> monad_commute (\<lambda>_. True) (\<lambda>sa. ({(?pde25 s pde, sa)}, False)) (setCTE src cte)
 2. \<And>s pde sa. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) ptr and (\<lambda>_. True)) sa proof (prove)
goal (1 subgoal):
 1. \<And>s pde sa. \<lbrakk>pspace_distinct' s; cte_wp_at' (\<lambda>_. True) src s; ksPSpace s ptr = Some (KOArch (KOPDE pde)); is_aligned ptr (objBitsKO (KOArch (KOPDE pde))); ps_clear ptr (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) ptr s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) ptr and (\<lambda>_. True)) sa proof (prove)
goal:
No subgoals!