theory Invariants_AI

lemma cte_wp_at_valid_objs_valid_cap:
  "\<lbrakk> cte_wp_at P p s; valid_objs s \<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> valid_cap cap s" apply (clarsimp simp: cte_wp_at_cases valid_objs_def) apply (erule disjE) apply clarsimp apply (drule bspec, erule domI) apply (clarsimp simp: valid_obj_def valid_cs_def) apply (drule bspec, erule ranI) apply fastforce apply clarsimp apply (drule bspec, erule domI) apply (clarsimp simp: valid_obj_def valid_tcb_def) apply (fastforce simp: ran_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P p s; valid_objs s\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<exists>sz fun. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd p) = Some cap \<and> P cap)) \<or> (\<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> P (get tcb))); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; \<exists>sz fun. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun (snd p) = Some cap \<and> P cap)\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap
 2. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> P (get tcb))\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap proof (prove)
goal (2 subgoals):
 1. \<And>sz fun cap. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; kheap s (fst p) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd p) = Some cap; P cap\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap
 2. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> P (get tcb))\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap proof (prove)
goal (2 subgoals):
 1. \<And>sz fun cap. \<lbrakk>kheap s (fst p) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd p) = Some cap; P cap; \<exists>obj. kheap s (fst p) = Some obj \<and> valid_obj (fst p) obj s\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap
 2. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> P (get tcb))\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap proof (prove)
goal (2 subgoals):
 1. \<And>sz fun cap. \<lbrakk>kheap s (fst p) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd p) = Some cap; P cap; \<forall>cap\<in>ran fun. s \<turnstile> cap; valid_cs_size sz fun\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap
 2. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> P (get tcb))\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap proof (prove)
goal (2 subgoals):
 1. \<And>sz fun cap. \<lbrakk>kheap s (fst p) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd p) = Some cap; P cap; valid_cs_size sz fun; s \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap
 2. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> P (get tcb))\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> P (get tcb))\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; kheap s (fst p) = Some (TCB tcb); P (get tcb); tcb_cap_cases (snd p) = Some (get, set, restr)\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>kheap s (fst p) = Some (TCB tcb); P (get tcb); tcb_cap_cases (snd p) = Some (get, set, restr); \<exists>obj. kheap s (fst p) = Some obj \<and> valid_obj (fst p) obj s\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> s \<turnstile> cap proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>kheap s (fst p) = Some (TCB tcb); P (get tcb); 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 tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr (fst p) (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> \<exists>cap. P cap \<and> s \<turnstile> cap proof (prove)
goal:
No subgoals!