theory Detype_R

lemma doMachineOp_storePDE_commute:
  "monad_commute (pde_at' src) (doMachineOp f)
                 (storePDE src (new_pde::ARM_H.pde))" proof - have  eq_fail: "\<And>sa ks. snd (doMachineOp f (sa\<lparr>ksPSpace := ks\<rparr>)) = snd (doMachineOp f sa)" apply (clarsimp simp:doMachineOp_def bind_def return_def gets_def
      get_def simpler_modify_def select_def) apply (intro iffI) apply (elim disjE) apply (clarsimp simp:image_def select_f_def)+ done show ?thesis 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))) src 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 storePDE_det,where R = "\<top>"]) apply assumption apply wp apply (clarsimp simp:monad_commute_def simpler_modify_def return_def bind_def) apply (intro conjI iffI set_eqI) apply (clarsimp simp:doMachineOp_def gets_def bind_def get_def select_f_def return_def) apply (erule bexI[rotated]) apply (clarsimp simp:simpler_modify_def) apply (clarsimp simp:doMachineOp_def gets_def bind_def get_def select_f_def return_def) apply (erule bexI[rotated]) apply (clarsimp simp:simpler_modify_def) apply (simp add:eq_fail image_def) apply (elim disjE) apply clarsimp apply (clarsimp simp:doMachineOp_def gets_def bind_def get_def select_f_def return_def) apply (clarsimp simp:eq_fail) apply auto done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (pde_at' src) (doMachineOp f) (storePDE src new_pde) proof (state)
goal (1 subgoal):
 1. monad_commute (pde_at' src) (doMachineOp f) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>sa ks. snd (doMachineOp f (sa\<lparr>ksPSpace := ks\<rparr>)) = snd (doMachineOp f sa) proof (prove)
goal (1 subgoal):
 1. \<And>sa ks. ((\<exists>x\<in>fst (select_f (f (ksMachineState sa)) (sa\<lparr>ksPSpace := ks\<rparr>)). snd (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) xa)) \<or> snd (select_f (f (ksMachineState sa)) (sa\<lparr>ksPSpace := ks\<rparr>))) = ((\<exists>x\<in>fst (select_f (f (ksMachineState sa)) sa). snd (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) xa)) \<or> snd (select_f (f (ksMachineState sa)) sa)) proof (prove)
goal (2 subgoals):
 1. \<And>sa ks. (\<exists>x\<in>fst (select_f (f (ksMachineState sa)) (sa\<lparr>ksPSpace := ks\<rparr>)). snd (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) xa)) \<or> snd (select_f (f (ksMachineState sa)) (sa\<lparr>ksPSpace := ks\<rparr>)) \<Longrightarrow> (\<exists>x\<in>fst (select_f (f (ksMachineState sa)) sa). snd (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) xa)) \<or> snd (select_f (f (ksMachineState sa)) sa)
 2. \<And>sa ks. (\<exists>x\<in>fst (select_f (f (ksMachineState sa)) sa). snd (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) xa)) \<or> snd (select_f (f (ksMachineState sa)) sa) \<Longrightarrow> (\<exists>x\<in>fst (select_f (f (ksMachineState sa)) (sa\<lparr>ksPSpace := ks\<rparr>)). snd (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) xa)) \<or> snd (select_f (f (ksMachineState sa)) (sa\<lparr>ksPSpace := ks\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>sa ks. \<exists>x\<in>fst (select_f (f (ksMachineState sa)) (sa\<lparr>ksPSpace := ks\<rparr>)). snd (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) xa) \<Longrightarrow> (\<exists>x\<in>fst (select_f (f (ksMachineState sa)) sa). snd (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) xa)) \<or> snd (select_f (f (ksMachineState sa)) sa)
 2. \<And>sa ks. snd (select_f (f (ksMachineState sa)) (sa\<lparr>ksPSpace := ks\<rparr>)) \<Longrightarrow> (\<exists>x\<in>fst (select_f (f (ksMachineState sa)) sa). snd (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) xa)) \<or> snd (select_f (f (ksMachineState sa)) sa)
 3. \<And>sa ks. (\<exists>x\<in>fst (select_f (f (ksMachineState sa)) sa). snd (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) xa)) \<or> snd (select_f (f (ksMachineState sa)) sa) \<Longrightarrow> (\<exists>x\<in>fst (select_f (f (ksMachineState sa)) (sa\<lparr>ksPSpace := ks\<rparr>)). snd (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) xa)) \<or> snd (select_f (f (ksMachineState sa)) (sa\<lparr>ksPSpace := ks\<rparr>)) proof (prove)
goal:
No subgoals! proof (state)
this:
snd (doMachineOp f (?sa\<lparr>ksPSpace := ?ks\<rparr>)) = snd (doMachineOp f ?sa)

goal (1 subgoal):
 1. monad_commute (pde_at' src) (doMachineOp f) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. monad_commute (pde_at' src) (doMachineOp f) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s. pde_at' src s \<Longrightarrow> monad_commute ((=) s) (doMachineOp f) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>ksPSpace s src = Some ko; is_aligned src (objBitsKO ko); koTypeOf ko = ArchT PDET; ps_clear src (objBitsKO ko) s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (doMachineOp f) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s ko x8. \<lbrakk>ksPSpace s src = Some (KOArch x8); is_aligned src (objBitsKO (KOArch x8)); archTypeOf x8 = PDET; ps_clear src (objBitsKO (KOArch x8)) s; ko = KOArch x8\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (doMachineOp f) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object. \<lbrakk>ksPSpace s src = Some (KOArch arch_kernel_object); is_aligned src (objBitsKO (KOArch arch_kernel_object)); archTypeOf arch_kernel_object = PDET; ps_clear src (objBitsKO (KOArch arch_kernel_object)) s; ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (doMachineOp f) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s ko arch_kernel_object x3. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE x3)); is_aligned src (objBitsKO (KOArch (KOPDE x3))); ps_clear src (objBitsKO (KOArch (KOPDE x3))) s; ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (doMachineOp f) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s x3. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE x3)); is_aligned src (objBitsKO (KOArch (KOPDE x3))); ps_clear src (objBitsKO (KOArch (KOPDE x3))) s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (doMachineOp f) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s pde. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (doMachineOp f) (storePDE src new_pde) proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (doMachineOp f) (storePDE src new_pde)
 2. \<And>s pde. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) src s proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE pde))) src s
 2. \<And>s pde. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (doMachineOp f) (storePDE src new_pde) proof (prove)
goal (1 subgoal):
 1. \<And>s pde. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> monad_commute ((=) s) (doMachineOp f) (storePDE src new_pde) proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> monad_commute (?P11 s pde) (doMachineOp f) (storePDE src new_pde)
 2. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> ?P11 s pde sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> monad_commute (?P11 s pde) (storePDE src new_pde) (doMachineOp f)
 2. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> ?P11 s pde sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; ?Q16 s pde sa\<rbrakk> \<Longrightarrow> ko_wp_at' ((=) (KOArch (KOPDE (?pde17 s pde sa)))) src sa
 2. \<And>s pde. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> \<lbrace>?P16 s pde\<rbrace> doMachineOp f \<lbrace>\<lambda>x. ?Q16 s pde\<rbrace>
 3. \<And>s pde. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> monad_commute (\<lambda>_. True) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde)))) s) (doMachineOp f)
 4. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (?P16 s pde and ?Q16 s pde and (\<lambda>_. True)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> \<lbrace>?P16 s pde\<rbrace> doMachineOp f \<lbrace>\<lambda>x sa. ko_wp_at' ((=) (KOArch (KOPDE (?pde17 s pde sa)))) src sa\<rbrace>
 2. \<And>s pde. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> monad_commute (\<lambda>_. True) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde)))) s) (doMachineOp f)
 3. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (?P16 s pde and (\<lambda>sa. ko_wp_at' ((=) (KOArch (KOPDE (?pde17 s pde sa)))) src sa) and (\<lambda>_. True)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> monad_commute (\<lambda>_. True) (\<lambda>s. modify (ksPSpace_update (\<lambda>_. (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde)))) s) (doMachineOp f)
 2. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and (\<lambda>_. True)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s\<rbrakk> \<Longrightarrow> (\<Union>a\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). fst (case a of (y, s) \<Rightarrow> ({(((), y), s)}, False))) = (\<Union>a\<in>fst (doMachineOp f sa). fst (case a of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<and> ((\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))) = ((\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa))
 2. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and (\<lambda>_. True)) sa proof (prove)
goal (5 subgoals):
 1. \<And>s pde sa x. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; x \<in> (\<Union>a\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). fst (case a of (y, s) \<Rightarrow> ({(((), y), s)}, False)))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (doMachineOp f sa). fst (case a of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False)))
 2. \<And>s pde sa x. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; x \<in> (\<Union>a\<in>fst (doMachineOp f sa). fst (case a of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False)))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). fst (case a of (y, s) \<Rightarrow> ({(((), y), s)}, False)))
 3. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)
 4. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))
 5. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and (\<lambda>_. True)) sa proof (prove)
goal (5 subgoals):
 1. \<And>s pde sa ba a bb. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (a, bb) \<in> fst (f (ksMachineState sa)); ((), ba) \<in> fst (modify (ksMachineState_update (\<lambda>_. bb)) (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f (ksMachineState sa)). \<exists>x\<in>fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. (\<Union>a\<in>fst (modify (ksMachineState_update (\<lambda>_. ms')) s). fst (case a of (y, s) \<Rightarrow> ({(r, s)}, False)), (\<exists>x\<in>fst (modify (ksMachineState_update (\<lambda>_. ms')) s). snd (case x of (y, s) \<Rightarrow> ({(r, s)}, False))) \<or> snd (modify (ksMachineState_update (\<lambda>_. ms')) s))) sa). (((), a), ba) \<in> fst (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))
 2. \<And>s pde sa x. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; x \<in> (\<Union>a\<in>fst (doMachineOp f sa). fst (case a of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False)))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). fst (case a of (y, s) \<Rightarrow> ({(((), y), s)}, False)))
 3. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)
 4. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))
 5. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and (\<lambda>_. True)) sa proof (prove)
goal (5 subgoals):
 1. \<And>s pde sa ba a bb. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; ((), ba) \<in> fst (modify (ksMachineState_update (\<lambda>_. bb)) (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((case (a, bb) of (r, ms') \<Rightarrow> \<lambda>s. (\<Union>a\<in>fst (modify (ksMachineState_update (\<lambda>_. ms')) s). fst (case a of (y, s) \<Rightarrow> ({(r, s)}, False)), (\<exists>x\<in>fst (modify (ksMachineState_update (\<lambda>_. ms')) s). snd (case x of (y, s) \<Rightarrow> ({(r, s)}, False))) \<or> snd (modify (ksMachineState_update (\<lambda>_. ms')) s))) sa). (((), a), ba) \<in> fst (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))
 2. \<And>s pde sa x. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; x \<in> (\<Union>a\<in>fst (doMachineOp f sa). fst (case a of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False)))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). fst (case a of (y, s) \<Rightarrow> ({(((), y), s)}, False)))
 3. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)
 4. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))
 5. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and (\<lambda>_. True)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde sa x. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; x \<in> (\<Union>a\<in>fst (doMachineOp f sa). fst (case a of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False)))\<rbrakk> \<Longrightarrow> x \<in> (\<Union>a\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). fst (case a of (y, s) \<Rightarrow> ({(((), y), s)}, False)))
 2. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)
 3. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))
 4. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and (\<lambda>_. True)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde sa a bb bc. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (a, bb) \<in> fst (f (ksMachineState sa)); ((), bc) \<in> fst (modify (ksMachineState_update (\<lambda>_. bb)) sa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f (ksMachineState sa)). \<exists>x\<in>fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. (\<Union>a\<in>fst (modify (ksMachineState_update (\<lambda>_. ms')) s). fst (case a of (y, s) \<Rightarrow> ({(r, s)}, False)), (\<exists>x\<in>fst (modify (ksMachineState_update (\<lambda>_. ms')) s). snd (case x of (y, s) \<Rightarrow> ({(r, s)}, False))) \<or> snd (modify (ksMachineState_update (\<lambda>_. ms')) s))) (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). (((), a), bc\<lparr>ksPSpace := (ksPSpace bc)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>) \<in> fst (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))
 2. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)
 3. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))
 4. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and (\<lambda>_. True)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde sa a bb bc. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; ((), bc) \<in> fst (modify (ksMachineState_update (\<lambda>_. bb)) sa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((case (a, bb) of (r, ms') \<Rightarrow> \<lambda>s. (\<Union>a\<in>fst (modify (ksMachineState_update (\<lambda>_. ms')) s). fst (case a of (y, s) \<Rightarrow> ({(r, s)}, False)), (\<exists>x\<in>fst (modify (ksMachineState_update (\<lambda>_. ms')) s). snd (case x of (y, s) \<Rightarrow> ({(r, s)}, False))) \<or> snd (modify (ksMachineState_update (\<lambda>_. ms')) s))) (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). (((), a), bc\<lparr>ksPSpace := (ksPSpace bc)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>) \<in> fst (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))
 2. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)
 3. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))
 4. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and (\<lambda>_. True)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)
 2. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))
 3. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and (\<lambda>_. True)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f sa)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)
 2. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))
 3. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and (\<lambda>_. True)) sa proof (prove)
goal (4 subgoals):
 1. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; \<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)
 2. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; snd (doMachineOp f sa)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)
 3. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))
 4. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and (\<lambda>_. True)) sa proof (prove)
goal (3 subgoals):
 1. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; snd (doMachineOp f sa)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)
 2. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))
 3. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and (\<lambda>_. True)) sa proof (prove)
goal (2 subgoals):
 1. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; (\<exists>x\<in>fst (doMachineOp f sa). snd (case x of (y, s) \<Rightarrow> ({(((), y), s\<lparr>ksPSpace := (ksPSpace s)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)}, False))) \<or> snd (doMachineOp f sa)\<rbrakk> \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>)). snd (case x of (y, s) \<Rightarrow> ({(((), y), s)}, False))) \<or> snd (doMachineOp f (sa\<lparr>ksPSpace := (ksPSpace sa)(src \<mapsto> KOArch (KOPDE new_pde))\<rparr>))
 2. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and (\<lambda>_. True)) sa proof (prove)
goal (1 subgoal):
 1. \<And>s pde sa. \<lbrakk>ksPSpace s src = Some (KOArch (KOPDE pde)); is_aligned src (objBitsKO (KOArch (KOPDE pde))); ps_clear src (objBitsKO (KOArch (KOPDE pde))) s; ko_wp_at' ((=) (KOArch (KOPDE pde))) src s; s = sa\<rbrakk> \<Longrightarrow> (ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and ko_wp_at' ((=) (KOArch (KOPDE (?pde25 s pde)))) src and (\<lambda>_. True)) sa proof (prove)
goal:
No subgoals! proof (state)
this:
monad_commute (pde_at' src) (doMachineOp f) (storePDE src new_pde)

goal:
No subgoals!