theory ArchRetype_AC

lemma copy_global_invs_mappings_restricted':
  "pd \<in> S
   \<Longrightarrow> \<lbrace>all_invs_but_equal_kernel_mappings_restricted S and (\<lambda>s. S \<inter> global_refs s = {})
                                                        and K (is_aligned pd pd_bits)\<rbrace>
       copy_global_mappings pd
       \<lbrace>\<lambda>_. all_invs_but_equal_kernel_mappings_restricted S\<rbrace>" apply (rule hoare_weaken_pre) apply (rule copy_global_invs_mappings_restricted) apply (simp add: insert_absorb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pd \<in> S \<Longrightarrow> \<lbrace>(\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports and (\<lambda>s. S \<inter> global_refs s = {}) and K (is_aligned pd pd_bits)\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>_. (\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports\<rbrace> proof (prove)
goal (2 subgoals):
 1. pd \<in> S \<Longrightarrow> \<lbrace>?Q\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>_. (\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports\<rbrace>
 2. \<And>s. \<lbrakk>pd \<in> S; ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports and (\<lambda>s. S \<inter> global_refs s = {}) and K (is_aligned pd pd_bits)) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pd \<in> S; ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- S)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports and (\<lambda>s. S \<inter> global_refs s = {}) and K (is_aligned pd pd_bits)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- insert pd S)\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports and (\<lambda>s. insert pd S \<inter> global_refs s = {}) and K (is_aligned pd pd_bits)) s proof (prove)
goal:
No subgoals!