theory ArchRetype_AC

lemma dmo_freeMemory_invs[Retype_AC_assms]:
  "do_machine_op (freeMemory ptr bits) \<lbrace>invs\<rbrace>" apply (simp add: do_machine_op_def invs_def valid_state_def cur_tcb_def | wp | wpc)+ apply (clarsimp) apply (frule_tac P1="(=) (device_state (machine_state s))"
                in use_valid[OF _ freeMemory_pspace_respects_device_region]) apply simp apply simp apply (rule conjI) apply (erule use_valid[OF _ freeMemory_valid_irq_states], simp) apply (drule freeMemory_vms) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op (freeMemory ptr bits) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_pspace s \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> tcb_at (cur_thread s) s \<Longrightarrow> \<forall>x\<in>fst (freeMemory ptr bits (machine_state s)). \<forall>xa. x = ((), xa) \<longrightarrow> valid_irq_states (s\<lparr>machine_state := xa\<rparr>) \<and> valid_machine_state (s\<lparr>machine_state := xa\<rparr>) \<and> pspace_respects_device_region (s\<lparr>machine_state := xa\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := xa\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>((), x) \<in> fst (freeMemory ptr bits (machine_state s)); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s\<rbrakk> \<Longrightarrow> valid_irq_states (s\<lparr>machine_state := x\<rparr>) \<and> valid_machine_state (s\<lparr>machine_state := x\<rparr>) \<and> pspace_respects_device_region (s\<lparr>machine_state := x\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>((), x) \<in> fst (freeMemory ptr bits (machine_state s)); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s\<rbrakk> \<Longrightarrow> device_state (machine_state s) = device_state (machine_state s)
 2. \<And>s x. \<lbrakk>((), x) \<in> fst (freeMemory ptr bits (machine_state s)); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; device_state (machine_state s) = device_state x\<rbrakk> \<Longrightarrow> valid_irq_states (s\<lparr>machine_state := x\<rparr>) \<and> valid_machine_state (s\<lparr>machine_state := x\<rparr>) \<and> pspace_respects_device_region (s\<lparr>machine_state := x\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>((), x) \<in> fst (freeMemory ptr bits (machine_state s)); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; device_state (machine_state s) = device_state x\<rbrakk> \<Longrightarrow> valid_irq_states (s\<lparr>machine_state := x\<rparr>) \<and> valid_machine_state (s\<lparr>machine_state := x\<rparr>) \<and> pspace_respects_device_region (s\<lparr>machine_state := x\<rparr>) \<and> cap_refs_respects_device_region (s\<lparr>machine_state := x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>((), x) \<in> fst (freeMemory ptr bits (machine_state s)); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; device_state (machine_state s) = device_state x\<rbrakk> \<Longrightarrow> valid_irq_states (s\<lparr>machine_state := x\<rparr>) \<and> valid_machine_state (s\<lparr>machine_state := x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>((), x) \<in> fst (freeMemory ptr bits (machine_state s)); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; device_state (machine_state s) = device_state x\<rbrakk> \<Longrightarrow> valid_irq_states (s\<lparr>machine_state := x\<rparr>)
 2. \<And>s x. \<lbrakk>((), x) \<in> fst (freeMemory ptr bits (machine_state s)); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; device_state (machine_state s) = device_state x\<rbrakk> \<Longrightarrow> valid_machine_state (s\<lparr>machine_state := x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>((), x) \<in> fst (freeMemory ptr bits (machine_state s)); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; device_state (machine_state s) = device_state x\<rbrakk> \<Longrightarrow> valid_machine_state (s\<lparr>machine_state := x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>((), x) \<in> fst (freeMemory ptr bits (machine_state s)); valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; device_state (machine_state s) = device_state x; \<forall>x\<in>fst (freeMemory (?ptr89 s x) (?bits89 s x) (machine_state s)). valid_machine_state (s\<lparr>machine_state := snd x\<rparr>)\<rbrakk> \<Longrightarrow> valid_machine_state (s\<lparr>machine_state := x\<rparr>) proof (prove)
goal:
No subgoals!