theory ArchRetype_IF

lemma delete_objects_reads_respects_g:
 "reads_equiv_valid_g_inv (affects_equiv aag l) aag
    (\<lambda>s. arm_global_pd (arch_state s) \<notin> ptr_range p b \<and>
         idle_thread s \<notin> ptr_range p b \<and>
         is_aligned p b \<and> 2 \<le> b \<and> b < word_bits)
    (delete_objects p b)" apply (simp add: delete_objects_def2) apply (rule equiv_valid_guard_imp) apply (wp dmo_freeMemory_reads_respects_g) apply (rule detype_reads_respects_g) apply wp apply (unfold ptr_range_def) 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> ptr_range p b \<and> idle_thread s \<notin> ptr_range p b \<and> is_aligned p b \<and> 2 \<le> b \<and> b < word_bits) (delete_objects p b) 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> ptr_range p b \<and> idle_thread s \<notin> ptr_range p b \<and> is_aligned p b \<and> 2 \<le> b \<and> b < word_bits) (do y <- modify (detype {p..p + 2 ^ b - 1});
do_machine_op (freeMemory p b)
od) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?Q (do y <- modify (detype {p..p + 2 ^ b - 1});
do_machine_op (freeMemory p b)
od)
 2. \<And>s. arm_global_pd (arch_state s) \<notin> ptr_range p b \<and> idle_thread s \<notin> ptr_range p b \<and> is_aligned p b \<and> 2 \<le> b \<and> b < word_bits \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P'4 (modify (detype {p..p + 2 ^ b - 1}))
 2. \<lbrace>?P''4\<rbrace> modify (detype {p..p + 2 ^ b - 1}) \<lbrace>\<lambda>rv s. is_aligned p b \<and> 2 \<le> b \<and> b < word_bits\<rbrace>
 3. \<And>s. arm_global_pd (arch_state s) \<notin> ptr_range p b \<and> idle_thread s \<notin> ptr_range p b \<and> is_aligned p b \<and> 2 \<le> b \<and> b < word_bits \<Longrightarrow> ?P'4 s \<and> ?P''4 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''4\<rbrace> modify (detype {p..p + 2 ^ b - 1}) \<lbrace>\<lambda>rv s. is_aligned p b \<and> 2 \<le> b \<and> b < word_bits\<rbrace>
 2. \<And>s. arm_global_pd (arch_state s) \<notin> ptr_range p b \<and> idle_thread s \<notin> ptr_range p b \<and> is_aligned p b \<and> 2 \<le> b \<and> b < word_bits \<Longrightarrow> ((\<lambda>s. arm_global_pd (arch_state s) \<notin> {p..p + 2 ^ b - 1}) and (\<lambda>s. idle_thread s \<notin> {p..p + 2 ^ b - 1})) s \<and> ?P''4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. arm_global_pd (arch_state s) \<notin> ptr_range p b \<and> idle_thread s \<notin> ptr_range p b \<and> is_aligned p b \<and> 2 \<le> b \<and> b < word_bits \<Longrightarrow> ((\<lambda>s. arm_global_pd (arch_state s) \<notin> {p..p + 2 ^ b - 1}) and (\<lambda>s. idle_thread s \<notin> {p..p + 2 ^ b - 1})) s \<and> is_aligned p b \<and> 2 \<le> b \<and> b < word_bits proof (prove)
goal (1 subgoal):
 1. \<And>s. arm_global_pd (arch_state s) \<notin> {p..p + 2 ^ b - 1} \<and> idle_thread s \<notin> {p..p + 2 ^ b - 1} \<and> is_aligned p b \<and> 2 \<le> b \<and> b < word_bits \<Longrightarrow> ((\<lambda>s. arm_global_pd (arch_state s) \<notin> {p..p + 2 ^ b - 1}) and (\<lambda>s. idle_thread s \<notin> {p..p + 2 ^ b - 1})) s \<and> is_aligned p b \<and> 2 \<le> b \<and> b < word_bits proof (prove)
goal:
No subgoals!