kings-crown/FVELER_Isabelle huggingface dataset:
theory Detype_R

lemma deleteObjects_invs_derivatives:
  "\<lbrace>cte_wp_at' (\<lambda>c. cteCap c = UntypedCap d ptr bits idx) p
     and invs' and ct_active' and sch_act_simple
     and (\<lambda>s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s))
     and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace>
     deleteObjects ptr bits
   \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>"
  "\<lbrace>cte_wp_at' (\<lambda>c. cteCap c = UntypedCap d ptr bits idx) p
     and invs' and ct_active' and sch_act_simple
     and (\<lambda>s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s))
     and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace>
     deleteObjects ptr bits
   \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>"
  "\<lbrace>cte_wp_at' (\<lambda>c. cteCap c = UntypedCap d ptr bits idx) p
     and invs' and ct_active' and sch_act_simple
     and (\<lambda>s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s))
     and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace>
     deleteObjects ptr bits
   \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>"
  "\<lbrace>cte_wp_at' (\<lambda>c. cteCap c = UntypedCap d ptr bits idx) p
     and invs' and ct_active' and sch_act_simple
     and (\<lambda>s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s))
     and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace>
     deleteObjects ptr bits
   \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>" by (safe intro!: hoare_strengthen_post [OF deleteObjects_invs'])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> &&& \<lbrace>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>) &&& \<lbrace>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> &&& \<lbrace>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>
theory Detype_R

lemma deleteObjects_nosch:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
   deleteObjects ptr sz
   \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" by (simp add: deleteObjects_def3 | wp hoare_drop_imp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>
theory Detype_R

lemma createObjects'_wp_subst:
  "\<lbrakk>\<lbrace>P\<rbrace>createObjects a b c d\<lbrace>\<lambda>r. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>createObjects' a b c d\<lbrace>\<lambda>r. Q\<rbrace>" apply (clarsimp simp:createObjects_def valid_def return_def bind_def) apply (drule_tac x = s in spec) apply (clarsimp simp:split_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> createObjects a b c d \<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> createObjects' a b c d \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ba. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>y\<in>fst (createObjects' a b c d s). \<forall>x\<in>fst (case y of (y, s) \<Rightarrow> ({(map (\<lambda>n. a + (n << objBitsKO c + d)) [0 .e. word_of_nat b - 1], s)}, False)). case x of (r, x) \<Rightarrow> Q x); P s; ((), ba) \<in> fst (createObjects' a b c d s)\<rbrakk> \<Longrightarrow> Q ba proof (prove)
goal (1 subgoal):
 1. \<And>s ba. \<lbrakk>P s; ((), ba) \<in> fst (createObjects' a b c d s); P s \<longrightarrow> (\<forall>y\<in>fst (createObjects' a b c d s). \<forall>x\<in>fst (case y of (y, s) \<Rightarrow> ({(map (\<lambda>n. a + (n << objBitsKO c + d)) [0 .e. word_of_nat b - 1], s)}, False)). case x of (r, x) \<Rightarrow> Q x)\<rbrakk> \<Longrightarrow> Q ba proof (prove)
goal (1 subgoal):
 1. \<And>s ba. \<lbrakk>P s; ((), ba) \<in> fst (createObjects' a b c d s); \<forall>y\<in>fst (createObjects' a b c d s). Q (snd y)\<rbrakk> \<Longrightarrow> Q ba proof (prove)
goal:
No subgoals!
theory Detype_R

lemma setCTE_pspace_no_overlap':
  "\<lbrace>pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\<rbrace>
   setCTE cte src
   \<lbrace>\<lambda>r. pspace_no_overlap' ptr sz\<rbrace>" apply (rule pspace_no_overlap'_lift; wp setCTE_typ_at') apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\<rbrace> setCTE cte src \<lbrace>\<lambda>r. pspace_no_overlap' ptr sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned' and pspace_distinct') s \<Longrightarrow> pspace_aligned' s \<and> pspace_distinct' s proof (prove)
goal:
No subgoals!
theory Detype_R

lemma pspace_no_overlapD3':
  "\<lbrakk>pspace_no_overlap' ptr sz s;ksPSpace s p = Some obj;is_aligned ptr sz\<rbrakk>
  \<Longrightarrow> obj_range' p obj \<inter> {ptr..ptr + 2 ^ sz - 1} = {}" apply (unfold pspace_no_overlap'_def) apply (drule spec)+ apply (erule(1) impE) apply (simp only:is_aligned_neg_mask_eq obj_range'_def p_assoc_help) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap' ptr sz s; ksPSpace s p = Some obj; is_aligned ptr sz\<rbrakk> \<Longrightarrow> obj_range' p obj \<inter> {ptr..ptr + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr sz = {}; ksPSpace s p = Some obj; is_aligned ptr sz\<rbrakk> \<Longrightarrow> obj_range' p obj \<inter> {ptr..ptr + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some obj; is_aligned ptr sz; ksPSpace s ?x = Some ?ko2 \<longrightarrow> {?x..?x + 2 ^ objBitsKO ?ko2 - 1} \<inter> up_aligned_area ptr sz = {}\<rbrakk> \<Longrightarrow> obj_range' p obj \<inter> {ptr..ptr + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some obj; is_aligned ptr sz; {p..p + 2 ^ objBitsKO obj - 1} \<inter> up_aligned_area ptr sz = {}\<rbrakk> \<Longrightarrow> obj_range' p obj \<inter> {ptr..ptr + 2 ^ sz - 1} = {} proof (prove)
goal:
No subgoals!
theory Detype_R

lemma singleton_locateCTE:
  "a \<in> fst (locateCTE src s) = ({a} = fst (locateCTE src s))" apply (clarsimp simp:locateCTE_def assert_opt_def assert_def
    gets_def get_def bind_def return_def split_def) apply (clarsimp simp:return_def fail_def
    split:if_splits option.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a \<in> fst (locateCTE src s)) = ({a} = fst (locateCTE src s)) proof (prove)
goal (1 subgoal):
 1. (\<exists>x\<in>fst ((case fst (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> fail | Some v \<Rightarrow> \<lambda>s. ({(v, s)}, False)) s). (cte_check (snd (fst x)) src (fst (fst x)) (snd (lookupAround2 src (ksPSpace s))) \<longrightarrow> a = (fst (fst x), snd x)) \<and> (\<not> cte_check (snd (fst x)) src (fst (fst x)) (snd (lookupAround2 src (ksPSpace s))) \<longrightarrow> (\<exists>xa\<in>fst (fail (snd x)). a = (fst (fst x), snd xa)))) = ({a} = (\<Union>x\<in>fst ((case fst (lookupAround2 src (ksPSpace s)) of None \<Rightarrow> fail | Some v \<Rightarrow> \<lambda>s. ({(v, s)}, False)) s). \<Union>xa\<in>fst ((if cte_check (snd (fst x)) src (fst (fst x)) (snd (lookupAround2 src (ksPSpace s))) then return () else fail) (snd x)). {(fst (fst x), snd xa)})) proof (prove)
goal:
No subgoals!
theory Detype_R

lemma locateCTE_inv:
  "\<lbrace>P\<rbrace>locateCTE s\<lbrace>\<lambda>r. P\<rbrace>" apply (simp add:locateCTE_def split_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> locateCTE s \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 s ps));
y <- assert (cte_check (snd p) s (fst p) (snd (lookupAround2 s ps)));
return (fst p)
od \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. P sa \<Longrightarrow> fst (lookupAround2 s (ksPSpace sa)) \<noteq> None \<longrightarrow> cte_check (snd (the (fst (lookupAround2 s (ksPSpace sa))))) s (fst (the (fst (lookupAround2 s (ksPSpace sa))))) (snd (lookupAround2 s (ksPSpace sa))) \<longrightarrow> P sa proof (prove)
goal:
No subgoals!
theory Detype_R

lemma empty_fail_locateCTE:
  "empty_fail (locateCTE src)" by (fastforce simp: locateCTE_def bind_assoc split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (locateCTE src)
theory Detype_R

lemma fail_empty_locateCTE:
  "snd (locateCTE src s) \<Longrightarrow> fst (locateCTE src s) = {}" by (auto simp: assert_def fail_def locateCTE_def bind_assoc return_def split_def gets_def
                 get_def bind_def assert_opt_def image_def
           split:option.splits if_split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (locateCTE src s) \<Longrightarrow> fst (locateCTE src s) = {}
theory Detype_R

lemma arch_toAPIType_simps:
 "ARM_H.toAPIType ty = Some a \<Longrightarrow> ty = APIObjectType a" by (case_tac ty,auto simp:ARM_H.toAPIType_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. toAPIType ty = Some a \<Longrightarrow> ty = APIObjectType a
theory Detype_R

lemma fail_set: "fst (fail s) = {}" by (clarsimp simp: fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (fail s) = {}
theory Detype_R

lemma not_in_new_cap_addrs':
  "\<lbrakk>dest \<in> set (new_cap_addrs (2 ^ us) ptr obj);
    is_aligned ptr (objBitsKO obj + us);
    objBitsKO obj + us < word_bits;
    pspace_no_overlap' ptr (objBitsKO obj + us) s;
    pspace_aligned' s \<rbrakk>
  \<Longrightarrow> ksPSpace s dest = None" apply (rule ccontr) apply clarsimp apply (drule not_in_new_cap_addrs) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dest \<in> set (new_cap_addrs (2 ^ us) ptr obj); is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; pspace_aligned' s\<rbrakk> \<Longrightarrow> ksPSpace s dest = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dest \<in> set (new_cap_addrs (2 ^ us) ptr obj); is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; pspace_aligned' s; ksPSpace s dest \<noteq> None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>dest \<in> set (new_cap_addrs (2 ^ us) ptr obj); is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; pspace_aligned' s; ksPSpace s dest = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>y. \<lbrakk>dest \<in> set (new_cap_addrs (2 ^ us) ptr obj); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; pspace_aligned' s; ksPSpace s dest = Some y\<rbrakk> \<Longrightarrow> objBitsKO obj + us < word_bits
 2. \<And>y. \<lbrakk>dest \<in> set (new_cap_addrs (2 ^ us) ptr obj); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; pspace_aligned' s; ksPSpace s dest = Some y\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (objBitsKO obj + us) (?s3 y)
 3. \<And>y. \<lbrakk>dest \<in> set (new_cap_addrs (2 ^ us) ptr obj); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; pspace_aligned' s; ksPSpace s dest = Some y\<rbrakk> \<Longrightarrow> ksPSpace (?s3 y) (?dest3 y) = Some (?ko3 y)
 4. \<And>y. \<lbrakk>dest \<in> set (new_cap_addrs (2 ^ us) ptr obj); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; pspace_aligned' s; ksPSpace s dest = Some y\<rbrakk> \<Longrightarrow> pspace_aligned' (?s3 y)
 5. \<And>y. \<lbrakk>dest \<in> set (new_cap_addrs (2 ^ us) ptr obj); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; pspace_aligned' s; ksPSpace s dest = Some y; ?dest3 y \<notin> set (new_cap_addrs (2 ^ us) ptr obj)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Detype_R

lemma placeNewObject_cte_wp_at':
  "\<lbrace>K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and>
       objBitsKO (injectKOS val) + us < word_bits) and
    K (ptr \<noteq> src) and cte_wp_at' P src and
    pspace_aligned' and pspace_distinct' and
    pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)\<rbrace>
   placeNewObject ptr val us
   \<lbrace>\<lambda>r s. cte_wp_at' P src s\<rbrace>" apply (clarsimp simp:placeNewObject_def2) apply (wp createObjects_orig_cte_wp_at') apply (auto simp:range_cover_full) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and K (ptr \<noteq> src) and cte_wp_at' P src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>r. cte_wp_at' P src\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>y. is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and (\<lambda>y. ptr \<noteq> src) and cte_wp_at' P src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)\<rbrace> createObjects' ptr (Suc 0) (injectKOS val) us \<lbrace>\<lambda>r. cte_wp_at' P src\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>y. is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> objBitsKO (injectKOS val) + us < word_bits) and (\<lambda>y. ptr \<noteq> src) and cte_wp_at' P src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) s \<Longrightarrow> range_cover ptr ?sz2 (objBitsKO (injectKOS val) + us) (Suc 0) \<and> Suc 0 \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> cte_wp_at' P src s \<and> pspace_no_overlap' ptr ?sz2 s proof (prove)
goal:
No subgoals!
theory Detype_R

lemma no_fail_placeNewObject:
  "no_fail (\<lambda>s. us < word_bits \<and>
                is_aligned ptr (objBitsKO (injectKOS val) + us) \<and>
                pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and>
                pspace_aligned' s)
           (placeNewObject ptr val us)" by (clarsimp simp:no_fail_def simpler_modify_def simpler_placeNewObject_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. us < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS val) + us) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \<and> pspace_aligned' s) (placeNewObject ptr val us)
theory Detype_R

lemma update_ksPSpaceI:
  "kh = kh' \<Longrightarrow> s\<lparr>ksPSpace := kh\<rparr> = s\<lparr>ksPSpace := kh'\<rparr>" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kh = kh' \<Longrightarrow> s\<lparr>ksPSpace := kh\<rparr> = s\<lparr>ksPSpace := kh'\<rparr>
theory Detype_R

lemma cte_update_objBits[simp]:
  "(objBitsKO (cte_update cte b src a)) = objBitsKO b" by (case_tac b,
    (simp add:objBits_simps cte_update_def)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. objBitsKO (cte_update cte b src a) = objBitsKO b
theory Detype_R

lemma doMachineOp_upd_heap_commute:
  "monad_commute \<top> (doMachineOp x) (modify (ksPSpace_update P))" apply (clarsimp simp:doMachineOp_def split_def simpler_modify_def
    gets_def get_def return_def bind_def select_f_def) apply (clarsimp simp:monad_commute_def bind_def return_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (doMachineOp x) (modify (ksPSpace_update P)) proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (\<lambda>s. (\<Union>x\<in>fst (x (ksMachineState s)) \<times> {s}. {(fst (fst x), snd x\<lparr>ksMachineState := snd (fst x)\<rparr>)}, snd (x (ksMachineState s)))) (\<lambda>s. ({((), ksPSpace_update P s)}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union>x\<in>fst (x (ksMachineState s)) \<times> {s}. {((fst (fst x), ()), ksPSpace_update P (snd x\<lparr>ksMachineState := snd (fst x)\<rparr>))}) = (\<Union>x\<in>fst (x (ksMachineState s)) \<times> {ksPSpace_update P s}. {((fst (fst x), ()), snd x\<lparr>ksMachineState := snd (fst x)\<rparr>)}) proof (prove)
goal:
No subgoals!
theory Detype_R

lemma in_dom_eq:
  "m a = Some obj \<Longrightarrow> dom (\<lambda>b. if b = a then Some g else m b) = dom m" by (rule set_eqI,clarsimp simp:dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m a = Some obj \<Longrightarrow> dom (\<lambda>b. if b = a then Some g else m b) = dom m
theory Detype_R

lemma modify_obj_commute:
  "monad_commute (K (ptr\<noteq> ptr'))
     (modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> ko))))
     (modify (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> ko'))))" apply (clarsimp simp:monad_commute_def return_def bind_def simpler_modify_def) apply (case_tac s) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (K (ptr \<noteq> ptr')) (modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> ko)))) (modify (ksPSpace_update (\<lambda>ps. ps(ptr' \<mapsto> ko')))) proof (prove)
goal (1 subgoal):
 1. \<And>s. ptr \<noteq> ptr' \<Longrightarrow> ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> ko')) \<circ> (\<lambda>ps. ps(ptr \<mapsto> ko))) s = ksPSpace_update ((\<lambda>ps. ps(ptr \<mapsto> ko)) \<circ> (\<lambda>ps. ps(ptr' \<mapsto> ko'))) s proof (prove)
goal (1 subgoal):
 1. \<And>s ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState more. \<lbrakk>ptr \<noteq> ptr'; s = \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState, \<dots> = more\<rparr>\<rbrakk> \<Longrightarrow> ksPSpace_update ((\<lambda>ps. ps(ptr' \<mapsto> ko')) \<circ> (\<lambda>ps. ps(ptr \<mapsto> ko))) s = ksPSpace_update ((\<lambda>ps. ps(ptr \<mapsto> ko)) \<circ> (\<lambda>ps. ps(ptr' \<mapsto> ko'))) s proof (prove)
goal:
No subgoals!
theory Detype_R

lemma modify_specify:
  "(\<lambda>s. modify (ksPSpace_update (\<lambda>_. P (ksPSpace s))) s) =
   modify (ksPSpace_update (\<lambda>ps. P ps))" by (auto simp: simpler_modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. modify (ksPSpace_update (\<lambda>_. P (ksPSpace s))) s) = modify (ksPSpace_update P)
theory Detype_R

lemma modify_specify2:
  "(modify (ksPSpace_update (\<lambda>_. P (ksPSpace s))) >>= g) s =
   (modify (ksPSpace_update (\<lambda>ps. P ps)) >>=g) s" apply (clarsimp simp:simpler_modify_def bind_def) apply (rule arg_cong[where f = "\<lambda>x. g ()  x"],simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (modify (ksPSpace_update (\<lambda>_. P (ksPSpace s))) >>= g) s = (modify (ksPSpace_update P) >>= g) s proof (prove)
goal (1 subgoal):
 1. g () (s\<lparr>ksPSpace := P (ksPSpace s)\<rparr>) = g () (ksPSpace_update P s) proof (prove)
goal:
No subgoals!
theory Detype_R

lemma koTypeOf_pde:
  "koTypeOf ko = ArchT PDET \<Longrightarrow> \<exists>pde. ko = KOArch (KOPDE pde)" apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. koTypeOf ko = ArchT PDET \<Longrightarrow> \<exists>pde. ko = KOArch (KOPDE pde) proof (prove)
goal (1 subgoal):
 1. \<And>x8. \<lbrakk>archTypeOf x8 = PDET; ko = KOArch x8\<rbrakk> \<Longrightarrow> \<exists>pde. x8 = KOPDE pde proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_object. \<lbrakk>archTypeOf arch_kernel_object = PDET; ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> \<exists>pde. arch_kernel_object = KOPDE pde proof (prove)
goal:
No subgoals!