theory ArchRetype_AI

lemma copy_global_mappings_invs:
  "\<lbrace>invs and (\<lambda>s. pd \<notin> global_refs s)
         and K (is_aligned pd pd_bits)\<rbrace>
     copy_global_mappings pd \<lbrace>\<lambda>rv. invs\<rbrace>" apply (fold all_invs_but_equal_kernel_mappings_restricted_eq) apply (wp copy_global_invs_mappings_restricted) apply (clarsimp simp: equal_kernel_mappings_def obj_at_def
                        restrict_map_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. pd \<notin> global_refs s) and K (is_aligned pd pd_bits)\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap 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. pd \<notin> global_refs s) and K (is_aligned pd pd_bits)\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>rv. (\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap 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 (1 subgoal):
 1. \<And>s. ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap 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. pd \<notin> global_refs s) and K (is_aligned pd pd_bits)) s \<Longrightarrow> ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- {pd})\<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. {pd} \<inter> global_refs s = {}) and K (is_aligned pd pd_bits)) s proof (prove)
goal:
No subgoals!