theory Ipc_AI

lemma st_tcb_at_valid_st:
  "\<lbrakk> invs s ; tcb_at t s ; st_tcb_at ((=) st) t s \<rbrakk> \<Longrightarrow> valid_tcb_state st s" apply (clarsimp simp add: invs_def valid_state_def valid_pspace_def
                  valid_objs_def tcb_at_def get_tcb_def pred_tcb_at_def
                  obj_at_def) apply (drule_tac x=t in bspec) apply (erule domI) apply (simp add: valid_obj_def valid_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; tcb_at t s; st_tcb_at ((=) st) t s\<rbrakk> \<Longrightarrow> valid_tcb_state st s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; is_tcb (TCB tcb); kheap s t = Some (TCB tcb); pspace_aligned s; st = tcb_state tcb; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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_ioports 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; cur_tcb s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state tcb) s proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>is_tcb (TCB tcb); kheap s t = Some (TCB tcb); pspace_aligned s; st = tcb_state tcb; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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_ioports 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; cur_tcb s\<rbrakk> \<Longrightarrow> t \<in> dom (kheap s)
 2. \<And>tcb. \<lbrakk>is_tcb (TCB tcb); kheap s t = Some (TCB tcb); pspace_aligned s; st = tcb_state tcb; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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_ioports 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; cur_tcb s; \<exists>obj. kheap s t = Some obj \<and> valid_obj t obj s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state tcb) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>is_tcb (TCB tcb); kheap s t = Some (TCB tcb); pspace_aligned s; st = tcb_state tcb; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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_ioports 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; cur_tcb s; \<exists>obj. kheap s t = Some obj \<and> valid_obj t obj s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state tcb) s proof (prove)
goal:
No subgoals!