kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_IF

lemma dmo_mol_reads_respects:
  "reads_respects aag l \<top> (do_machine_op (machine_op_lift mop))" apply (rule use_spec_ev) apply (rule do_machine_op_spec_reads_respects) apply (rule equiv_valid_guard_imp[OF machine_op_lift_ev]) apply simp apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do_machine_op (machine_op_lift mop)) proof (prove)
goal (1 subgoal):
 1. \<And>st. spec_reads_respects st aag l (\<lambda>_. True) (do_machine_op (machine_op_lift mop)) 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) (machine_op_lift mop)
 2. \<And>st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> machine_op_lift mop \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>st s. True \<Longrightarrow> True
 2. \<And>st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> machine_op_lift mop \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> machine_op_lift mop \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma dmo_bind_ev:
  "equiv_valid_inv I A P (do_machine_op (a >>= b)) =
   equiv_valid_inv I A P (do_machine_op a >>= (\<lambda>rv. do_machine_op (b rv)))" by (fastforce simp: do_machine_op_def gets_def get_def select_f_def modify_def
                      put_def return_def bind_def equiv_valid_def2 equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P (do_machine_op (a >>= b)) = equiv_valid_inv I A P (do rv <- do_machine_op a;
do_machine_op (b rv)
od)
theory Retype_IF

lemma dmo_mapM_x_ev_pre:
  assumes reads_res: "\<And>x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))"
  assumes invariant: "\<And>x. x \<in> set lst \<Longrightarrow> do_machine_op (m x) \<lbrace>I\<rbrace>"
  assumes inv_established: "\<And>s. P s \<Longrightarrow> I s"
  shows "equiv_valid_inv D A P (do_machine_op (mapM_x m lst))" apply (subst mapM_x_mapM) apply (simp add: dmo_bind_ev) apply (rule bind_ev_pre[OF return_ev dmo_mapM_ev_pre]) by (blast intro: reads_res invariant inv_established wp_post_taut)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A P (do_machine_op (mapM_x m lst)) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A P (do_machine_op (do x <- mapM m lst;
return ()
od)) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A P (do rv <- do_machine_op (mapM m lst);
return ()
od) proof (prove)
goal (5 subgoals):
 1. \<And>x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A ?I1 (do_machine_op (m x))
 2. \<And>x. x \<in> set lst \<Longrightarrow> \<lbrace>?I1\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. ?I1\<rbrace>
 3. \<And>s. ?P' s \<Longrightarrow> ?I1 s
 4. \<lbrace>?P''\<rbrace> do_machine_op (mapM m lst) \<lbrace>\<lambda>rv _. True\<rbrace>
 5. \<And>s. P s \<Longrightarrow> ?P' s \<and> ?P'' s
theory Retype_IF

lemma dmo_mapM_ev:
  assumes reads_res: "\<And>x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))"
  assumes invariant: "\<And>x. x \<in> set lst \<Longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>"
  shows "equiv_valid_inv D A I (do_machine_op (mapM m lst))" using assms by (auto intro: dmo_mapM_ev_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A I (do_machine_op (mapM m lst)) proof (prove)
using this:
?x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (m ?x))
?x \<in> set lst \<Longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m ?x) \<lbrace>\<lambda>_. I\<rbrace>

goal (1 subgoal):
 1. equiv_valid_inv D A I (do_machine_op (mapM m lst))
theory Retype_IF

lemma dmo_mapM_x_ev:
  assumes reads_res: "\<And>x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (m x))"
  assumes invariant: "\<And>x. x \<in> set lst \<Longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m x) \<lbrace>\<lambda>_. I\<rbrace>"
  shows "equiv_valid_inv D A I (do_machine_op (mapM_x m lst))" using assms by (auto intro: dmo_mapM_x_ev_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A I (do_machine_op (mapM_x m lst)) proof (prove)
using this:
?x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (do_machine_op (m ?x))
?x \<in> set lst \<Longrightarrow> \<lbrace>I\<rbrace> do_machine_op (m ?x) \<lbrace>\<lambda>_. I\<rbrace>

goal (1 subgoal):
 1. equiv_valid_inv D A I (do_machine_op (mapM_x m lst))
theory Retype_IF

lemma dmo_clearMemory_reads_respects:
  "reads_respects aag l \<top> (do_machine_op (clearMemory ptr bits))" apply (rule use_spec_ev) apply (rule do_machine_op_spec_reads_respects) apply (rule equiv_valid_guard_imp[OF clearMemory_ev], rule TrueI) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do_machine_op (clearMemory ptr bits)) proof (prove)
goal (1 subgoal):
 1. \<And>st. spec_reads_respects st aag l (\<lambda>_. True) (do_machine_op (clearMemory ptr bits)) 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) (clearMemory ptr bits)
 2. \<And>st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> clearMemory ptr bits \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> clearMemory ptr bits \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma dmo_freeMemory_reads_respects:
  "reads_respects aag l \<top> (do_machine_op (freeMemory ptr bits))" apply (rule use_spec_ev) apply (rule do_machine_op_spec_reads_respects) apply (rule equiv_valid_guard_imp[OF freeMemory_ev], rule TrueI) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do_machine_op (freeMemory ptr bits)) proof (prove)
goal (1 subgoal):
 1. \<And>st. spec_reads_respects st aag l (\<lambda>_. True) (do_machine_op (freeMemory ptr bits)) 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) (freeMemory ptr bits)
 2. \<And>st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> freeMemory ptr bits \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> freeMemory ptr bits \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma dmo_clearMemory_reads_respects_g:
  "reads_respects_g aag l \<top> (do_machine_op (clearMemory ptr (2 ^bits)))" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_g) apply (rule dmo_clearMemory_reads_respects) apply (rule doesnt_touch_globalsI[where P = \<top>, simplified, OF dmo_clearMemory_globals_equiv]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_g aag l (\<lambda>_. True) (do_machine_op (clearMemory ptr (2 ^ bits))) proof (prove)
goal (2 subgoals):
 1. reads_respects_g aag l ?Q (do_machine_op (clearMemory ptr (2 ^ bits)))
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P3 (do_machine_op (clearMemory ptr (2 ^ bits)))
 2. doesnt_touch_globals ?Q3 (do_machine_op (clearMemory ptr (2 ^ bits)))
 3. \<And>s. True \<Longrightarrow> (?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q3 (do_machine_op (clearMemory ptr (2 ^ bits)))
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q3) s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma dmo_freeMemory_reads_respects_g:
  "reads_respects_g aag l (\<lambda> s. is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits)
                    (do_machine_op (freeMemory ptr bits))" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_g) apply (rule dmo_freeMemory_reads_respects) apply (rule doesnt_touch_globalsI[where P = \<top>, simplified, OF dmo_freeMemory_globals_equiv]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_g aag l (\<lambda>s. is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits) (do_machine_op (freeMemory ptr bits)) proof (prove)
goal (2 subgoals):
 1. reads_respects_g aag l ?Q (do_machine_op (freeMemory ptr bits))
 2. \<And>s. is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P3 (do_machine_op (freeMemory ptr bits))
 2. doesnt_touch_globals ?Q3 (do_machine_op (freeMemory ptr bits))
 3. \<And>s. is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits \<Longrightarrow> (?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q3 (do_machine_op (freeMemory ptr bits))
 2. \<And>s. is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits \<Longrightarrow> ((\<lambda>_. True) and ?Q3) s proof (prove)
goal (1 subgoal):
 1. \<And>s. is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma globals_equiv_cdt_update[simp]:
  "globals_equiv s (s'\<lparr>cdt := x\<rparr>) = globals_equiv s s'" by (fastforce simp: globals_equiv_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv s (s'\<lparr>cdt := x\<rparr>) = globals_equiv s s'
theory Retype_IF

lemma globals_equiv_is_original_cap_update[simp]:
  "globals_equiv s (s'\<lparr>is_original_cap := x\<rparr>) = globals_equiv s s'" by (fastforce simp: globals_equiv_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv s (s'\<lparr>is_original_cap := x\<rparr>) = globals_equiv s s'
theory Retype_IF

lemma create_cap_globals_equiv:
  "\<lbrace>globals_equiv s and valid_global_objs and valid_arch_state\<rbrace>
   create_cap type bits untyped dev slot
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" apply (simp only: create_cap_def split_def) apply (wp set_cap_globals_equiv set_original_globals_equiv set_cdt_globals_equiv
            set_cdt_valid_global_objs dxo_wp_weak set_original_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_global_objs and valid_arch_state\<rbrace> create_cap type bits untyped dev slot \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_global_objs and valid_arch_state\<rbrace> do dest_p <- gets (\<lambda>s. cdt s (fst slot));
cdt <- gets cdt;
set_cdt (cdt(fst slot \<mapsto> untyped));
do_extended_op (create_cap_ext untyped (fst slot) dest_p);
set_original (fst slot) True;
set_cap (default_cap type (snd slot) bits dev) (fst slot)
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma gets_apply_ev':
  "\<forall>s t. I s t \<and> A s t \<and> P s \<and> P t \<longrightarrow> (f s) x = (f t) x
   \<Longrightarrow> equiv_valid I A A P (gets_apply f x)" by (clarsimp simp: gets_apply_def get_def bind_def return_def equiv_valid_def2 equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s t. I s t \<and> A s t \<and> P s \<and> P t \<longrightarrow> f s x = f t x \<Longrightarrow> equiv_valid_inv I A P (gets_apply f x)
theory Retype_IF

lemma do_machine_op_globals_equiv:
   "(\<And>s sa. \<lbrakk> P sa; globals_equiv s sa \<rbrakk>
              \<Longrightarrow> \<forall>x\<in>fst (f (machine_state sa)). globals_equiv s (sa\<lparr>machine_state := snd x\<rparr>))
    \<Longrightarrow> \<lbrace>globals_equiv s and P\<rbrace>
        do_machine_op f
        \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding do_machine_op_def apply (wp | simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s sa. \<lbrakk>P sa; globals_equiv s sa\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f (machine_state sa)). globals_equiv s (sa\<lparr>machine_state := snd x\<rparr>)) \<Longrightarrow> \<lbrace>globals_equiv s and P\<rbrace> do_machine_op f \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>s sa. \<lbrakk>P sa; globals_equiv s sa\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f (machine_state sa)). globals_equiv s (sa\<lparr>machine_state := snd x\<rparr>)) \<Longrightarrow> \<lbrace>globals_equiv s and P\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (f ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma ptr_range_memE:
  "\<lbrakk> x \<in> ptr_range ptr bits; \<lbrakk> ptr \<le> x; x \<le> ptr + 2 ^ bits - 1 \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" by (clarsimp simp: ptr_range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> ptr_range ptr bits; \<lbrakk>ptr \<le> x; x \<le> ptr + (2::'a) ^ bits - (1::'a)\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Retype_IF

lemma is_aligned_word_size_bits_upto_enum_step_mem:
  fixes ptr :: obj_ref
  shows "\<lbrakk> is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits;
           x \<in> set [ptr, ptr + word_size .e. ptr + 2 ^ bits - 1] \<rbrakk>
           \<Longrightarrow> is_aligned x word_size_bits" apply (clarsimp simp: word_size_size_bits_word[symmetric]) apply (subst (asm) upto_enum_step_shift_red; (fastforce simp: word_bits_def)?) apply clarsimp apply (erule aligned_add_aligned) apply (rule is_alignedI) apply (simp add: mult.commute) apply (simp add: word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; x \<in> set [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1]\<rbrakk> \<Longrightarrow> is_aligned x word_size_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; x \<in> set [ptr , ptr + 2 ^ word_size_bits .e. ptr + 2 ^ bits - 1]\<rbrakk> \<Longrightarrow> is_aligned x word_size_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; x \<in> set (map (\<lambda>x. ptr + word_of_nat x * 2 ^ word_size_bits) [0..<2 ^ (bits - word_size_bits)])\<rbrakk> \<Longrightarrow> is_aligned x word_size_bits proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned ptr bits; word_size_bits \<le> bits; bits < word_bits; xa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xa * 2 ^ word_size_bits\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat xa * 2 ^ word_size_bits) word_size_bits proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>word_size_bits \<le> bits; bits < word_bits; xa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xa * 2 ^ word_size_bits\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat xa * 2 ^ word_size_bits) word_size_bits
 2. \<And>xa. \<lbrakk>word_size_bits \<le> bits; bits < word_bits; xa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xa * 2 ^ word_size_bits\<rbrakk> \<Longrightarrow> word_size_bits \<le> bits proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>word_size_bits \<le> bits; bits < word_bits; xa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xa * 2 ^ word_size_bits\<rbrakk> \<Longrightarrow> word_of_nat xa * 2 ^ word_size_bits = 2 ^ word_size_bits * ?k17 xa
 2. \<And>xa. \<lbrakk>word_size_bits \<le> bits; bits < word_bits; xa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xa * 2 ^ word_size_bits\<rbrakk> \<Longrightarrow> word_size_bits \<le> bits proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>word_size_bits \<le> bits; bits < word_bits; xa < 2 ^ (bits - word_size_bits); x = ptr + word_of_nat xa * 2 ^ word_size_bits\<rbrakk> \<Longrightarrow> word_size_bits \<le> bits proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma do_machine_op_mapM_x:
  assumes ef: "\<And>a. empty_fail (f a)"
  shows "do_machine_op (mapM_x f xs) = mapM_x (\<lambda> x. do_machine_op (f x)) xs" apply (induct xs) apply (simp add: mapM_x_Nil) apply (clarsimp simp: mapM_x_Cons do_machine_op_bind[OF ef empty_fail_mapM_x[OF ef]]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do_machine_op (mapM_x f xs) = mapM_x (\<lambda>x. do_machine_op (f x)) xs proof (prove)
goal (2 subgoals):
 1. do_machine_op (mapM_x f []) = mapM_x (\<lambda>x. do_machine_op (f x)) []
 2. \<And>a xs. do_machine_op (mapM_x f xs) = mapM_x (\<lambda>x. do_machine_op (f x)) xs \<Longrightarrow> do_machine_op (mapM_x f (a # xs)) = mapM_x (\<lambda>x. do_machine_op (f x)) (a # xs) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. do_machine_op (mapM_x f xs) = mapM_x (\<lambda>x. do_machine_op (f x)) xs \<Longrightarrow> do_machine_op (mapM_x f (a # xs)) = mapM_x (\<lambda>x. do_machine_op (f x)) (a # xs) proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma create_cap_reads_respects_g:
  "reads_respects_g aag l
     (K (is_subject aag (fst (fst slot))) and valid_global_objs and valid_arch_state)
     (create_cap type bits untyped dev slot)" apply (rule equiv_valid_guard_imp[OF reads_respects_g]) apply (rule create_cap_reads_respects) apply (wp doesnt_touch_globalsI create_cap_globals_equiv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (K (is_subject aag (fst (fst slot))) and valid_global_objs and valid_arch_state) (create_cap type bits untyped dev slot) proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P1 (create_cap type bits untyped dev slot)
 2. doesnt_touch_globals ?Q1 (create_cap type bits untyped dev slot)
 3. \<And>s. (K (is_subject aag (fst (fst slot))) and valid_global_objs and valid_arch_state) s \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (create_cap type bits untyped dev slot)
 2. \<And>s. (K (is_subject aag (fst (fst slot))) and valid_global_objs and valid_arch_state) s \<Longrightarrow> (K (is_subject aag (fst (fst slot))) and ?Q1) s proof (prove)
goal:
No subgoals!
theory Retype_IF

lemma retype_region_ext_def2:
  "retype_region_ext a b =
   modify (\<lambda>s. ekheap_update (\<lambda>ekh x. if x \<in> set a then default_ext b (cur_domain s) else ekh x) s)" by (simp add: retype_region_ext_def foldr_upd_app_if' gets_def bind_def
                return_def modify_def get_def put_def fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retype_region_ext a b = modify (\<lambda>s. ekheap_update (\<lambda>ekh x. if x \<in> set a then default_ext b (cur_domain s) else ekh x) s)
theory Retype_IF

lemma subset_thing:
  "\<lbrakk> a \<le> b; a \<le> a \<rbrakk> \<Longrightarrow> {a} \<subseteq> {a..b}" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; a \<le> a\<rbrakk> \<Longrightarrow> {a} \<subseteq> {a..b}
theory Retype_IF

lemma updates_not_idle:
  "\<lbrakk> idle_equiv st s; \<forall>a \<in> S. a \<noteq> idle_thread s \<rbrakk>
     \<Longrightarrow> idle_equiv st (s\<lparr>kheap := \<lambda>a. if a \<in> S then y else kheap s a\<rparr>)" by (fastforce simp: idle_equiv_def tcb_at_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idle_equiv st s; \<forall>a\<in>S. a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> idle_equiv st (s\<lparr>kheap := \<lambda>a. if a \<in> S then y else kheap s a\<rparr>)
theory Retype_IF

lemma post_retype_invs_valid_arch_stateI:
  "post_retype_invs ty rv s \<Longrightarrow> valid_arch_state s" by (clarsimp simp: post_retype_invs_def invs_def valid_state_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. post_retype_invs ty rv s \<Longrightarrow> valid_arch_state s
theory Retype_IF

lemma post_retype_invs_pspace_alignedI:
  "post_retype_invs ty rv s \<Longrightarrow> pspace_aligned s" by (clarsimp simp: post_retype_invs_def invs_def valid_state_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. post_retype_invs ty rv s \<Longrightarrow> pspace_aligned s
theory Retype_IF

lemma detype_def2:
   "detype S (s :: det_state) = s\<lparr>kheap := \<lambda>x. if x \<in> S then None else kheap s x,
                                  ekheap := \<lambda>x. if x \<in> S then None else ekheap s x\<rparr>" by (simp add: detype_def detype_ext_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. detype S s = ekheap_update (\<lambda>_ x. if x \<in> S then None else ekheap s x) (s\<lparr>kheap := \<lambda>x. if x \<in> S then None else kheap s x\<rparr>)
theory Retype_IF

lemma cur_thread_detype:
  "cur_thread (detype S s) = cur_thread s" by (auto simp: detype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cur_thread (detype S s) = cur_thread s
theory Retype_IF

lemma cur_domain_detype:
  "cur_domain (detype S s) = cur_domain s" by (auto simp: detype_def detype_ext_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cur_domain (detype S s) = cur_domain s
theory Retype_IF

lemma sched_act_detype:
  "scheduler_action (detype S s) = scheduler_action s" by (auto simp: detype_def detype_ext_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_action (detype S s) = scheduler_action s
theory Retype_IF

lemma wuc_detype:
  "work_units_completed (detype S s) = work_units_completed s" by (auto simp: detype_def detype_ext_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. work_units_completed (detype S s) = work_units_completed s
theory Retype_IF

lemma machine_state_detype:
  "machine_state (detype S s) = machine_state s" by (auto simp: detype_def detype_ext_def)

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