kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchRetype_IF

lemma dmo_clearMemory_globals_equiv[Retype_IF_assms]:
  "do_machine_op (clearMemory ptr (2 ^ bits)) \<lbrace>globals_equiv s\<rbrace>" apply (simp add: do_machine_op_def clearMemory_def split_def cleanCacheRange_PoU_def) apply wpsimp apply (erule use_valid) by (wpsimp wp: mapM_x_wp' storeWord_globals_equiv mol_globals_equiv
           simp: cleanCacheRange_RAM_def cleanL2Range_def dsb_def
                 cleanCacheRange_PoC_def cleanByVA_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do_machine_op (clearMemory ptr (2 ^ bits)) \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do ms <- gets machine_state;
p <- select_f ((do y <- mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1];
cleanCacheRange_RAM ptr (ptr + 2 ^ bits - 1) (addrFromPPtr ptr)
od) ms);
modify (machine_state_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa b. \<lbrakk>globals_equiv s sa; ((), b) \<in> fst ((do y <- mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1];
cleanCacheRange_RAM ptr (ptr + 2 ^ bits - 1) (addrFromPPtr ptr)
od) (machine_state sa))\<rbrakk> \<Longrightarrow> globals_equiv s (sa\<lparr>machine_state := b\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>sa b. globals_equiv s sa \<Longrightarrow> \<lbrace>?P9 sa b\<rbrace> do y <- mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1];
cleanCacheRange_RAM ptr (ptr + 2 ^ bits - 1) (addrFromPPtr ptr)
od \<lbrace>\<lambda>a b. globals_equiv s (sa\<lparr>machine_state := b\<rparr>)\<rbrace>
 2. \<And>sa b. globals_equiv s sa \<Longrightarrow> ?P9 sa b (machine_state sa)
theory ArchRetype_IF

lemma dmo_freeMemory_globals_equiv[Retype_IF_assms]:
  "do_machine_op (freeMemory ptr bits) \<lbrace>globals_equiv s\<rbrace>" apply (rule hoare_pre) apply (simp add: do_machine_op_def freeMemory_def split_def) apply (wp) apply clarsimp apply (erule use_valid) apply (wp mapM_x_wp' storeWord_globals_equiv mol_globals_equiv) apply (simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s\<rbrace> do_machine_op (freeMemory ptr bits) \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do_machine_op (freeMemory ptr bits) \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<And>sa. globals_equiv s sa \<Longrightarrow> ?Q sa proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do ms <- gets machine_state;
p <- select_f (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] ms);
modify (machine_state_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<And>sa. globals_equiv s sa \<Longrightarrow> ?Q sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. globals_equiv s sa \<Longrightarrow> \<forall>x\<in>fst (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] (machine_state sa)). globals_equiv s (sa\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa b. \<lbrakk>globals_equiv s sa; ((), b) \<in> fst (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] (machine_state sa))\<rbrakk> \<Longrightarrow> globals_equiv s (sa\<lparr>machine_state := b\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>sa b. globals_equiv s sa \<Longrightarrow> \<lbrace>?P11 sa b\<rbrace> mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1] \<lbrace>\<lambda>a b. globals_equiv s (sa\<lparr>machine_state := b\<rparr>)\<rbrace>
 2. \<And>sa b. globals_equiv s sa \<Longrightarrow> ?P11 sa b (machine_state sa) proof (prove)
goal (1 subgoal):
 1. \<And>sa b. globals_equiv s sa \<Longrightarrow> globals_equiv s (sa\<lparr>machine_state := machine_state sa\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma no_irq_freeMemory[Retype_IF_assms]:
  "no_irq (freeMemory ptr sz)" apply (simp add: freeMemory_def) apply (wp no_irq_mapM_x no_irq_storeWord) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (freeMemory ptr sz) proof (prove)
goal (1 subgoal):
 1. no_irq (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1]) proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma equiv_asid_detype[Retype_IF_assms]:
  "equiv_asid asid s s' \<Longrightarrow> equiv_asid asid (detype N s) (detype N s')" by (auto simp: equiv_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_asid asid s s' \<Longrightarrow> equiv_asid asid (detype N s) (detype N s')
theory ArchRetype_IF

lemma detype_globals_equiv:
  "\<lbrace>globals_equiv st and ((\<lambda>s. arm_global_pd (arch_state s) \<notin> S) and (\<lambda>s. idle_thread s \<notin> S))\<rbrace>
   modify (detype S)
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (wp) apply (clarsimp simp: globals_equiv_def detype_def idle_equiv_def tcb_at_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and ((\<lambda>s. arm_global_pd (arch_state s) \<notin> S) and (\<lambda>s. idle_thread s \<notin> S))\<rbrace> modify (detype S) \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (globals_equiv st and ((\<lambda>s. arm_global_pd (arch_state s) \<notin> S) and (\<lambda>s. idle_thread s \<notin> S))) s \<Longrightarrow> globals_equiv st (detype S s) proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma detype_reads_respects_g:
  "reads_respects_g aag l ((\<lambda>s. arm_global_pd (arch_state s) \<notin> S) and (\<lambda>s. idle_thread s \<notin> S))
                    (modify (detype S))" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_g) apply (rule detype_reads_respects) apply (rule doesnt_touch_globalsI[OF detype_globals_equiv]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ((\<lambda>s. arm_global_pd (arch_state s) \<notin> S) and (\<lambda>s. idle_thread s \<notin> S)) (modify (detype S)) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?Q (modify (detype S))
 2. \<And>s. ((\<lambda>s. arm_global_pd (arch_state s) \<notin> S) and (\<lambda>s. idle_thread s \<notin> S)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P3 (modify (detype S))
 2. doesnt_touch_globals ?Q3 (modify (detype S))
 3. \<And>s. ((\<lambda>s. arm_global_pd (arch_state s) \<notin> S) and (\<lambda>s. idle_thread s \<notin> S)) s \<Longrightarrow> (?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q3 (modify (detype S))
 2. \<And>s. ((\<lambda>s. arm_global_pd (arch_state s) \<notin> S) and (\<lambda>s. idle_thread s \<notin> S)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q3) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. arm_global_pd (arch_state s) \<notin> S) and (\<lambda>s. idle_thread s \<notin> S)) s \<Longrightarrow> ((\<lambda>_. True) and ((\<lambda>s. arm_global_pd (arch_state s) \<notin> S) and (\<lambda>s. idle_thread s \<notin> S))) s proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma retype_region_ret_pd_aligned:
  "\<lbrace>K (range_cover ptr sz (obj_bits_api tp us) num_objects)\<rbrace>
   retype_region ptr num_objects us tp dev
   \<lbrace>\<lambda>rv. K (\<forall>ref \<in> set rv. tp = ArchObject PageDirectoryObj \<longrightarrow> is_aligned ref pd_bits)\<rbrace>" apply (rule hoare_strengthen_post) apply (rule hoare_weaken_pre) apply (rule retype_region_aligned_for_init) apply simp apply (clarsimp simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (range_cover ptr sz (obj_bits_api tp us) num_objects)\<rbrace> retype_region ptr num_objects us tp dev \<lbrace>\<lambda>rv. K (\<forall>ref\<in>set rv. tp = ArchObject PageDirectoryObj \<longrightarrow> is_aligned ref pd_bits)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>K (range_cover ptr sz (obj_bits_api tp us) num_objects)\<rbrace> retype_region ptr num_objects us tp dev \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> K (\<forall>ref\<in>set rv. tp = ArchObject PageDirectoryObj \<longrightarrow> is_aligned ref pd_bits) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q3\<rbrace> retype_region ptr num_objects us tp dev \<lbrace>?Q\<rbrace>
 2. \<And>s. K (range_cover ptr sz (obj_bits_api tp us) num_objects) s \<Longrightarrow> ?Q3 s
 3. \<And>rv s. ?Q rv s \<Longrightarrow> K (\<forall>ref\<in>set rv. tp = ArchObject PageDirectoryObj \<longrightarrow> is_aligned ref pd_bits) s proof (prove)
goal (2 subgoals):
 1. \<And>s. K (range_cover ptr sz (obj_bits_api tp us) num_objects) s \<Longrightarrow> range_cover ptr ?sz6 (obj_bits_api tp us) num_objects
 2. \<And>rv s. \<forall>ref\<in>set rv. is_aligned ref (obj_bits_api tp us) \<Longrightarrow> K (\<forall>ref\<in>set rv. tp = ArchObject PageDirectoryObj \<longrightarrow> is_aligned ref pd_bits) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<forall>ref\<in>set rv. is_aligned ref (obj_bits_api tp us) \<Longrightarrow> K (\<forall>ref\<in>set rv. tp = ArchObject PageDirectoryObj \<longrightarrow> is_aligned ref pd_bits) s proof (prove)
goal:
No subgoals!
theory ArchRetype_IF

lemma delete_objects_globals_equiv[wp]:
  "\<lbrace>globals_equiv st and (\<lambda>s. is_aligned p b \<and> 2 \<le> b \<and> b < word_bits \<and>
                              arm_global_pd (arch_state s) \<notin> ptr_range p b \<and>
                              idle_thread s \<notin> ptr_range p b)\<rbrace>
   delete_objects p b
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (simp add: delete_objects_def) apply (wp detype_globals_equiv dmo_freeMemory_globals_equiv) apply (clarsimp simp: ptr_range_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and (\<lambda>s. is_aligned p b \<and> 2 \<le> b \<and> b < word_bits \<and> arm_global_pd (arch_state s) \<notin> ptr_range p b \<and> idle_thread s \<notin> ptr_range p b)\<rbrace> delete_objects p b \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and (\<lambda>s. is_aligned p b \<and> 2 \<le> b \<and> b < word_bits \<and> arm_global_pd (arch_state s) \<notin> ptr_range p b \<and> idle_thread s \<notin> ptr_range p b)\<rbrace> do y <- do_machine_op (freeMemory p b);
modify (detype {p..p + 2 ^ b - 1})
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (globals_equiv st and (\<lambda>s. is_aligned p b \<and> 2 \<le> b \<and> b < word_bits \<and> arm_global_pd (arch_state s) \<notin> ptr_range p b \<and> idle_thread s \<notin> ptr_range p b)) s \<Longrightarrow> globals_equiv st s \<and> arm_global_pd (arch_state s) \<notin> {p..p + 2 ^ b - 1} \<and> idle_thread s \<notin> {p..p + 2 ^ b - 1} proof (prove)
goal:
No subgoals!
theory Arch_IF

lemma do_extended_op_irq_state_of_state[wp]:
  "do_extended_op f \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace>" by (wpsimp wp: dxo_wp_weak)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> do_extended_op f \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
theory Arch_IF

lemma no_irq_underlying_memory_update[simp]:
  "no_irq (modify (underlying_memory_update f))" by (wpsimp simp: no_irq_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (modify (underlying_memory_update f))
theory Arch_IF

lemma detype_irq_state_of_state[simp]:
  "irq_state_of_state (detype S s) = irq_state_of_state s" by (simp add: detype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_irq_state (machine_state (detype S s)) (machine_state s)
theory Arch_IF

lemma gets_applyE:
  "liftE (gets f) >>=E (\<lambda>f. g (f x)) = liftE (gets_apply f x) >>=E g" apply (simp add: liftE_bindE) apply (rule gets_apply) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doE f <- liftE (gets f);
g (f x)
odE = liftE (gets_apply f x) >>=E g proof (prove)
goal (1 subgoal):
 1. do f <- gets f;
g (f x)
od = gets_apply f x >>= g proof (prove)
goal:
No subgoals!
theory Arch_IF

lemma aag_can_read_own_asids:
  "is_subject_asid aag asid \<Longrightarrow> aag_can_read_asid aag asid" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_subject_asid aag asid \<Longrightarrow> aag_can_read_asid aag asid
theory Arch_IF

lemma reads_respects_unobservable_unit_return:
  assumes f:
    "\<And>P Q R S st. \<lbrace>states_equiv_for P Q R S st\<rbrace> f \<lbrace>\<lambda>_. states_equiv_for P Q R S st\<rbrace>"
  assumes g:
    "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>"
  assumes h:
    "\<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>"
  assumes j:
    "\<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> f \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>"
  assumes k:
    "\<And>P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> f \<lbrace>\<lambda>rv s. P (work_units_completed s)\<rbrace>"
  assumes l:
    "\<And>P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_state_of_state s)\<rbrace>"
  shows
    "reads_respects aag l \<top> (f::(unit,det_ext) s_monad)" apply (subgoal_tac "reads_equiv_valid_rv_inv (affects_equiv aag l) aag \<top>\<top> \<top> f") apply (clarsimp simp: equiv_valid_2_def equiv_valid_def2) apply (rule equiv_valid_2_unobservable[OF f f g g h h j j k k l l]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) f proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (\<lambda>_. True) f \<Longrightarrow> reads_respects aag l (\<lambda>_. True) f
 2. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (\<lambda>_. True) f proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (\<lambda>_. True) f proof (prove)
goal:
No subgoals!
theory Arch_IF

lemma dmo_mol_irq_state_of_state[wp]:
  "do_machine_op (machine_op_lift m) \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace>" by (wpsimp wp: dmo_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> do_machine_op (machine_op_lift m) \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
theory Arch_IF

lemma throw_on_false_reads_respects:
  "reads_respects aag l P f
   \<Longrightarrow> reads_respects aag l P (throw_on_false ex f)" unfolding throw_on_false_def fun_app_def unlessE_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l P f \<Longrightarrow> reads_respects aag l P (throw_on_false ex f) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l P f \<Longrightarrow> reads_respects aag l P (doE v <- liftE f;
if v then returnOk () else throwError ex
odE)
theory Arch_IF

lemma dmo_mol_2_reads_respects:
  "reads_respects aag l \<top> (do_machine_op (machine_op_lift mop >>= (\<lambda> y. machine_op_lift mop')))" apply (rule use_spec_ev) apply (rule do_machine_op_spec_reads_respects) by (wpsimp wp: machine_op_lift_ev)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do_machine_op (do y <- machine_op_lift mop;
machine_op_lift mop'
od)) proof (prove)
goal (1 subgoal):
 1. \<And>st. spec_reads_respects st aag l (\<lambda>_. True) (do_machine_op (do y <- machine_op_lift mop;
machine_op_lift mop'
od)) proof (prove)
goal (2 subgoals):
 1. \<And>st. equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) (do y <- machine_op_lift mop;
machine_op_lift mop'
od)
 2. \<And>st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> do y <- machine_op_lift mop;
machine_op_lift mop'
od \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace>
theory Arch_IF

lemma tl_subseteq:
  "set (tl xs) \<subseteq> set xs" by (induct xs, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set (tl xs) \<subseteq> set xs
theory Arch_IF

lemma ev_invisible:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
    "\<lbrakk> labels_are_invisible aag l L; modifies_at_most aag L Q f;
       \<forall>s t. P s \<and> P t \<longrightarrow> (\<forall>(rva, s') \<in> fst (f s). \<forall>(rvb, t') \<in> fst(f t). W rva rvb) \<rbrakk>
       \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l)
                         W (P and Q) (P and Q) f f" by (rule ev2_invisible[OF domains_distinct]; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f; \<forall>s t. P s \<and> P t \<longrightarrow> (\<forall>(rva, s')\<in>fst (f s). \<forall>(rvb, t')\<in>fst (f t). W rva rvb)\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag W (P and Q) f
theory Arch_IF

lemma modify_det:
  "det (modify f)" by (clarsimp simp: det_def modify_def get_def put_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det (modify f)
theory Arch_IF

lemma dummy_kheap_update:
  "st = st\<lparr>kheap := kheap st\<rparr>" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st = st\<lparr>kheap := kheap st\<rparr>
theory Arch_IF

lemma reads_affects_equiv_kheap_eq:
  "\<lbrakk> reads_equiv aag s s'; affects_equiv aag l s s'; aag_can_affect aag l x \<or> aag_can_read aag x \<rbrakk>
     \<Longrightarrow> kheap s x = kheap s' x" by (fastforce elim: affects_equivE reads_equivE equiv_forE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; affects_equiv aag l s s'; aag_can_affect aag l x \<or> aag_can_read aag x\<rbrakk> \<Longrightarrow> kheap s x = kheap s' x
theory Arch_IF

lemma reads_affects_equiv_get_tcb_eq:
  "\<lbrakk> aag_can_read aag t \<or> aag_can_affect aag l t; reads_equiv aag s s'; affects_equiv aag l s s' \<rbrakk>
     \<Longrightarrow> get_tcb t s = get_tcb t s'" by (fastforce simp: get_tcb_def reads_affects_equiv_kheap_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aag_can_read aag t \<or> aag_can_affect aag l t; reads_equiv aag s s'; affects_equiv aag l s s'\<rbrakk> \<Longrightarrow> get_tcb t s = get_tcb t s'
theory Arch_IF

lemma my_bind_rewrite_lemma:
  "(f >>= g) =  (f >>= (\<lambda> r. (g r) >>= (\<lambda> x. return ())))" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f >>= g = do r <- f;
x <- g r;
return ()
od
theory Arch_IF

lemma delete_objects_reads_respects:
  "reads_respects aag l (\<lambda>_. True) (delete_objects p b)" apply (simp add: delete_objects_def) apply (wp detype_reads_respects dmo_freeMemory_reads_respects) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (delete_objects p b) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do y <- do_machine_op (freeMemory p b);
modify (detype {p..p + 2 ^ b - 1})
od) proof (prove)
goal:
No subgoals!
theory Arch_IF

lemma another_hacky_rewrite:
  "do a; (do x \<leftarrow> f; g x od); h; j od = do a; (f >>= g >>= (\<lambda>_. h)); j od" by (simp add: bind_assoc[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do a;
f >>= g;
h;
j
od = do a;
do _ <- f >>= g;
h
od;
j
od
theory Arch_IF

lemma idle_equiv_arch_state_update[simp]: "idle_equiv st (s\<lparr>arch_state := x\<rparr>) = idle_equiv st s" by (simp add: idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. idle_equiv st (s\<lparr>arch_state := x\<rparr>) = idle_equiv st s
theory Arch_IF

lemma case_junk:
  "(case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r) \<longrightarrow> (case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R r) =
   (case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r \<longrightarrow> R r)" by (case_tac rv; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r) \<longrightarrow> (case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R r) = (case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r \<longrightarrow> R r)
theory Arch_IF

lemma hoare_add_postE:
  "\<lbrakk> \<lbrace>Q\<rbrace> f \<lbrace>P\<rbrace>, - ; \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. (P rv s) \<longrightarrow> (R rv s)\<rbrace>, - \<rbrakk>
     \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,-" unfolding validE_R_def validE_def apply (erule hoare_add_post) apply simp apply (erule hoare_post_imp[rotated]) apply (simp add: case_junk) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>Q\<rbrace> f \<lbrace>P\<rbrace>, -; \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> R rv s\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r s\<rbrace>; \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r s \<longrightarrow> R r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R r s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r s \<longrightarrow> R r s\<rbrace>; Q s\<rbrakk> \<Longrightarrow> Q s
 2. \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r s \<longrightarrow> R r s\<rbrace> \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. (case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r s) \<longrightarrow> (case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R r s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r s \<longrightarrow> R r s\<rbrace> \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. (case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r s) \<longrightarrow> (case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R r s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r s \<longrightarrow> R r s \<Longrightarrow> (case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> P r s) \<longrightarrow> (case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R r s) proof (prove)
goal:
No subgoals!