theory KHeap_AI

lemma tcb_cap_wp_at:
  "\<lbrakk>tcb_at t s; valid_objs s; ref \<in> dom tcb_cap_cases;
    \<forall>cap st getF setF restr.
    tcb_cap_cases ref = Some (getF, setF, restr) \<and> restr t st cap \<longrightarrow> Q cap\<rbrakk> \<Longrightarrow>
   cte_wp_at Q (t, ref) s" apply (clarsimp simp: cte_wp_at_cases tcb_at_def dest!: get_tcb_SomeD) apply (rename_tac getF setF restr) apply (erule(1) valid_objsE) apply (clarsimp simp add: valid_obj_def valid_tcb_def) apply (erule_tac x="(getF, setF, restr)" in ballE) apply (fastforce simp add: ranI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at t s; valid_objs s; ref \<in> dom tcb_cap_cases; \<forall>cap st getF setF restr. tcb_cap_cases ref = Some (getF, setF, restr) \<and> restr t st cap \<longrightarrow> Q cap\<rbrakk> \<Longrightarrow> cte_wp_at Q (t, ref) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb a aa b. \<lbrakk>valid_objs s; \<forall>cap. (\<exists>st. b t st cap) \<longrightarrow> Q cap; kheap s t = Some (TCB tcb); tcb_cap_cases ref = Some (a, aa, b); \<not> Q (a tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb getF setF restr. \<lbrakk>valid_objs s; \<forall>cap. (\<exists>st. restr t st cap) \<longrightarrow> Q cap; kheap s t = Some (TCB tcb); tcb_cap_cases ref = Some (getF, setF, restr); \<not> Q (getF tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb getF setF restr. \<lbrakk>\<forall>cap. (\<exists>st. restr t st cap) \<longrightarrow> Q cap; kheap s t = Some (TCB tcb); tcb_cap_cases ref = Some (getF, setF, restr); \<not> Q (getF tcb); valid_obj t (TCB tcb) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb getF setF restr. \<lbrakk>\<forall>cap. (\<exists>st. restr t st cap) \<longrightarrow> Q cap; kheap s t = Some (TCB tcb); tcb_cap_cases ref = Some (getF, setF, restr); \<not> Q (getF tcb); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr t (tcb_state tcb) (getF tcb)); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>tcb getF setF restr. \<lbrakk>\<forall>cap. (\<exists>st. restr t st cap) \<longrightarrow> Q cap; kheap s t = Some (TCB tcb); tcb_cap_cases ref = Some (getF, setF, restr); \<not> Q (getF tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; case (getF, setF, restr) of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr t (tcb_state tcb) (getF tcb))\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb getF setF restr. \<lbrakk>\<forall>cap. (\<exists>st. restr t st cap) \<longrightarrow> Q cap; kheap s t = Some (TCB tcb); tcb_cap_cases ref = Some (getF, setF, restr); \<not> Q (getF tcb); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; (getF, setF, restr) \<notin> ran tcb_cap_cases\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!