theory Invariants_AI

lemma cte_wp_valid_cap:
  "\<lbrakk> cte_wp_at ((=) c) p s; valid_objs s \<rbrakk> \<Longrightarrow> s \<turnstile> c" apply (simp add: cte_wp_at_cases) apply (erule disjE) apply clarsimp apply (simp add: valid_objs_def dom_def) apply (erule allE, erule impE, fastforce) apply (fastforce simp: ran_def valid_obj_def valid_cs_def) apply clarsimp apply (simp add: valid_objs_def dom_def) apply (erule allE, erule impE, fastforce) apply (fastforce simp: ran_def valid_obj_def valid_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) c) p s; valid_objs s\<rbrakk> \<Longrightarrow> s \<turnstile> c 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> fun (snd p) = Some c) \<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> c = get tcb)); valid_objs s\<rbrakk> \<Longrightarrow> s \<turnstile> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; \<exists>sz fun. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd p) = Some c\<rbrakk> \<Longrightarrow> s \<turnstile> c
 2. \<lbrakk>valid_objs 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> c = get tcb)\<rbrakk> \<Longrightarrow> s \<turnstile> c proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>valid_objs s; kheap s (fst p) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd p) = Some c\<rbrakk> \<Longrightarrow> s \<turnstile> c
 2. \<lbrakk>valid_objs 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> c = get tcb)\<rbrakk> \<Longrightarrow> s \<turnstile> c proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>\<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<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 c\<rbrakk> \<Longrightarrow> s \<turnstile> c
 2. \<lbrakk>valid_objs 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> c = get tcb)\<rbrakk> \<Longrightarrow> s \<turnstile> c proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>kheap s (fst p) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd p) = Some c; \<exists>obj. kheap s (fst p) = Some obj \<and> valid_obj (fst p) obj s\<rbrakk> \<Longrightarrow> s \<turnstile> c
 2. \<lbrakk>valid_objs 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> c = get tcb)\<rbrakk> \<Longrightarrow> s \<turnstile> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs 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> c = get tcb)\<rbrakk> \<Longrightarrow> s \<turnstile> c proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>valid_objs s; kheap s (fst p) = Some (TCB tcb); c = get tcb; tcb_cap_cases (snd p) = Some (get, set, restr)\<rbrakk> \<Longrightarrow> s \<turnstile> get tcb proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>\<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s (fst p) = Some (TCB tcb); c = get tcb; tcb_cap_cases (snd p) = Some (get, set, restr)\<rbrakk> \<Longrightarrow> s \<turnstile> get tcb proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>kheap s (fst p) = Some (TCB tcb); c = 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> s \<turnstile> get tcb proof (prove)
goal:
No subgoals!