theory Invariants_AI

lemma cte_wp_tcb_cap_valid:
  "\<lbrakk> cte_wp_at ((=) c) p s; valid_objs s \<rbrakk> \<Longrightarrow> tcb_cap_valid c p s" apply (clarsimp simp: tcb_cap_valid_def obj_at_def
                        pred_tcb_at_def cte_wp_at_cases) apply (erule disjE, (clarsimp simp: is_tcb)+) apply (erule(1) valid_objsE) apply (clarsimp simp: valid_obj_def valid_tcb_def) apply (drule bspec, erule ranI, simp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) c) p s; valid_objs s\<rbrakk> \<Longrightarrow> tcb_cap_valid c p s proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>(\<exists>sz fun. ko = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> fun (snd p) = Some c) \<or> (\<exists>tcb. ko = TCB tcb \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)); valid_objs s; kheap s (fst p) = Some ko; is_tcb ko\<rbrakk> \<Longrightarrow> (\<exists>tcb. ko = TCB tcb \<and> (case tcb_cap_cases (snd p) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst p) (itcb_state (tcb_to_itcb tcb)) c)) \<and> (snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko = TCB tcb \<longrightarrow> valid_ipc_buffer_cap c (tcb_ipc_buffer tcb))) proof (prove)
goal (1 subgoal):
 1. \<And>tcba get set restr. \<lbrakk>valid_objs s; kheap s (fst p) = Some (TCB tcba); c = get tcba; tcb_cap_cases (snd p) = Some (get, set, restr)\<rbrakk> \<Longrightarrow> restr (fst p) (tcb_state tcba) (get tcba) \<and> (snd p = tcb_cnode_index 4 \<longrightarrow> valid_ipc_buffer_cap (get tcba) (tcb_ipc_buffer tcba)) proof (prove)
goal (1 subgoal):
 1. \<And>tcba get set restr. \<lbrakk>kheap s (fst p) = Some (TCB tcba); c = get tcba; tcb_cap_cases (snd p) = Some (get, set, restr); valid_obj (fst p) (TCB tcba) s\<rbrakk> \<Longrightarrow> restr (fst p) (tcb_state tcba) (get tcba) \<and> (snd p = tcb_cnode_index 4 \<longrightarrow> valid_ipc_buffer_cap (get tcba) (tcb_ipc_buffer tcba)) proof (prove)
goal (1 subgoal):
 1. \<And>tcba get set restr. \<lbrakk>kheap s (fst p) = Some (TCB tcba); c = get tcba; tcb_cap_cases (snd p) = Some (get, set, restr); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF tcba \<and> (case ab of (setF, restr) \<Rightarrow> restr (fst p) (tcb_state tcba) (getF tcba)); valid_ipc_buffer_cap (tcb_ipcframe tcba) (tcb_ipc_buffer tcba); valid_tcb_state (tcb_state tcba) s; case tcb_fault tcba of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcba) = word_bits; valid_bound_ntfn (tcb_bound_notification tcba) s; valid_arch_tcb (tcb_arch tcba) s\<rbrakk> \<Longrightarrow> restr (fst p) (tcb_state tcba) (get tcba) \<and> (snd p = tcb_cnode_index 4 \<longrightarrow> valid_ipc_buffer_cap (get tcba) (tcb_ipc_buffer tcba)) proof (prove)
goal (1 subgoal):
 1. \<And>tcba get set restr. \<lbrakk>kheap s (fst p) = Some (TCB tcba); c = get tcba; tcb_cap_cases (snd p) = Some (get, set, restr); valid_ipc_buffer_cap (tcb_ipcframe tcba) (tcb_ipc_buffer tcba); valid_tcb_state (tcb_state tcba) s; case tcb_fault tcba of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcba) = word_bits; valid_bound_ntfn (tcb_bound_notification tcba) s; valid_arch_tcb (tcb_arch tcba) s; s \<turnstile> get tcba \<and> restr (fst p) (tcb_state tcba) (get tcba)\<rbrakk> \<Longrightarrow> snd p = tcb_cnode_index 4 \<longrightarrow> valid_ipc_buffer_cap (get tcba) (tcb_ipc_buffer tcba) proof (prove)
goal:
No subgoals!