theory ArchTcbAcc_AI

lemma pred_tcb_cap_wp_at [TcbAcc_AI_assms]:
  "\<lbrakk>pred_tcb_at proj P t s; valid_objs s;
    ref \<in> dom tcb_cap_cases;
    \<forall>cap. (pred_tcb_at proj P t s \<and> tcb_cap_valid cap (t, ref) s) \<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 (clarsimp simp: tcb_cap_valid_def pred_tcb_at_def obj_at_def) 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+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pred_tcb_at proj P t s; valid_objs s; ref \<in> dom tcb_cap_cases; \<forall>cap. pred_tcb_at proj P t s \<and> tcb_cap_valid cap (t, ref) s \<longrightarrow> Q cap\<rbrakk> \<Longrightarrow> cte_wp_at Q (t, ref) s proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>pred_tcb_at proj P t s; valid_objs s; \<forall>cap. tcb_cap_valid cap (t, ref) s \<longrightarrow> Q cap; tcb_cap_cases ref = Some (a, aa, b); \<forall>tcb. kheap s t = Some (TCB tcb) \<longrightarrow> \<not> Q (a tcb)\<rbrakk> \<Longrightarrow> \<exists>sz fun. kheap s t = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun ref = Some cap \<and> Q cap) proof (prove)
goal (1 subgoal):
 1. \<And>getF setF restr. \<lbrakk>pred_tcb_at proj P t s; valid_objs s; \<forall>cap. tcb_cap_valid cap (t, ref) s \<longrightarrow> Q cap; tcb_cap_cases ref = Some (getF, setF, restr); \<forall>tcb. kheap s t = Some (TCB tcb) \<longrightarrow> \<not> Q (getF tcb)\<rbrakk> \<Longrightarrow> \<exists>sz fun. kheap s t = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun ref = Some cap \<and> Q cap) proof (prove)
goal (1 subgoal):
 1. \<And>getF setF restr tcb. \<lbrakk>valid_objs s; \<forall>cap. (is_tcb (TCB tcb) \<longrightarrow> restr t (tcb_state tcb) cap \<and> (ref = tcb_cnode_index 4 \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) \<longrightarrow> Q cap; tcb_cap_cases ref = Some (getF, setF, restr); \<not> Q (getF tcb); kheap s t = Some (TCB tcb); P (proj (tcb_to_itcb tcb))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>getF setF restr tcb. \<lbrakk>\<forall>cap. (is_tcb (TCB tcb) \<longrightarrow> restr t (tcb_state tcb) cap \<and> (ref = tcb_cnode_index 4 \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) \<longrightarrow> Q cap; tcb_cap_cases ref = Some (getF, setF, restr); \<not> Q (getF tcb); kheap s t = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); valid_obj t (TCB tcb) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>getF setF restr tcb. \<lbrakk>\<forall>cap. (is_tcb (TCB tcb) \<longrightarrow> restr t (tcb_state tcb) cap \<and> (ref = tcb_cnode_index 4 \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) \<longrightarrow> Q cap; tcb_cap_cases ref = Some (getF, setF, restr); \<not> Q (getF tcb); kheap s t = Some (TCB tcb); P (proj (tcb_to_itcb 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>getF setF restr tcb. \<lbrakk>\<forall>cap. (is_tcb (TCB tcb) \<longrightarrow> restr t (tcb_state tcb) cap \<and> (ref = tcb_cnode_index 4 \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) \<longrightarrow> Q cap; tcb_cap_cases ref = Some (getF, setF, restr); \<not> Q (getF tcb); kheap s t = Some (TCB tcb); P (proj (tcb_to_itcb 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>getF setF restr tcb. \<lbrakk>\<forall>cap. (is_tcb (TCB tcb) \<longrightarrow> restr t (tcb_state tcb) cap \<and> (ref = tcb_cnode_index 4 \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) \<longrightarrow> Q cap; tcb_cap_cases ref = Some (getF, setF, restr); \<not> Q (getF tcb); kheap s t = Some (TCB tcb); P (proj (tcb_to_itcb 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!