theory CSpace1_R

lemma ctes_of_valid:
  "\<lbrakk> cte_wp_at' ((=) cte) p s; valid_objs' s \<rbrakk>
  \<Longrightarrow> s \<turnstile>' cteCap cte" apply (simp add: cte_wp_at'_obj_at') apply (erule disjE) apply (subgoal_tac "ko_at' cte p s") apply (drule (1) ko_at_valid_objs') apply (simp add: projectKOs) apply (simp add: valid_obj'_def valid_cte'_def) apply (simp add: obj_at'_def projectKOs cte_level_bits_def objBits_simps) apply clarsimp apply (drule obj_at_ko_at') apply clarsimp apply (drule (1) ko_at_valid_objs') apply (simp add: projectKOs) apply (simp add: valid_obj'_def valid_tcb'_def) apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' ((=) cte) p s; valid_objs' s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' ((=) cte) p s \<or> (\<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (p - n) s); valid_objs' s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs' s; obj_at' ((=) cte) p s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s
 2. \<lbrakk>valid_objs' s; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (p - n) s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_objs' s; obj_at' ((=) cte) p s; ko_at' cte p s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s
 2. \<lbrakk>valid_objs' s; obj_at' ((=) cte) p s\<rbrakk> \<Longrightarrow> ko_at' cte p s
 3. \<lbrakk>valid_objs' s; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (p - n) s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (4 subgoals):
 1. \<And>ko. \<lbrakk>valid_objs' s; obj_at' ((=) cte) p s; projectKO_opt ko = Some cte\<rbrakk> \<Longrightarrow> injectKO cte = ko
 2. \<lbrakk>valid_objs' s; obj_at' ((=) cte) p s; valid_obj' (injectKO cte) s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s
 3. \<lbrakk>valid_objs' s; obj_at' ((=) cte) p s\<rbrakk> \<Longrightarrow> ko_at' cte p s
 4. \<lbrakk>valid_objs' s; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (p - n) s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_objs' s; obj_at' ((=) cte) p s; valid_obj' (injectKO cte) s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s
 2. \<lbrakk>valid_objs' s; obj_at' ((=) cte) p s\<rbrakk> \<Longrightarrow> ko_at' cte p s
 3. \<lbrakk>valid_objs' s; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (p - n) s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs' s; obj_at' ((=) cte) p s\<rbrakk> \<Longrightarrow> ko_at' cte p s
 2. \<lbrakk>valid_objs' s; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (p - n) s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s; \<exists>n\<in>dom tcb_cte_cases. obj_at' ((=) cte \<circ> fst (the (tcb_cte_cases n))) (p - n) s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>valid_objs' s; obj_at' ((=) cte \<circ> a) (p - n) s; tcb_cte_cases n = Some (a, b)\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>valid_objs' s; tcb_cte_cases n = Some (a, b); \<exists>ko. ko_at' ko (p - n) s \<and> ((=) cte \<circ> a) ko\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<And>n a b ko. \<lbrakk>valid_objs' s; tcb_cte_cases n = Some (a, b); ko_at' ko (p - n) s; cte = a ko\<rbrakk> \<Longrightarrow> valid_cap' (cteCap (a ko)) s proof (prove)
goal (2 subgoals):
 1. \<And>n a b ko koa. \<lbrakk>valid_objs' s; tcb_cte_cases n = Some (a, b); cte = a ko; projectKO_opt koa = Some ko\<rbrakk> \<Longrightarrow> injectKO ko = koa
 2. \<And>n a b ko. \<lbrakk>valid_objs' s; tcb_cte_cases n = Some (a, b); cte = a ko; valid_obj' (injectKO ko) s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap (a ko)) s proof (prove)
goal (1 subgoal):
 1. \<And>n a b ko. \<lbrakk>valid_objs' s; tcb_cte_cases n = Some (a, b); cte = a ko; valid_obj' (injectKO ko) s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap (a ko)) s proof (prove)
goal (1 subgoal):
 1. \<And>n a b ko. \<lbrakk>valid_objs' s; tcb_cte_cases n = Some (a, b); cte = a ko; (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF ko)) s) \<and> valid_tcb_state' (tcbState ko) s \<and> is_aligned (tcbIPCBuffer ko) msg_align_bits \<and> valid_bound_ntfn' (tcbBoundNotification ko) s \<and> tcbDomain ko \<le> maxDomain \<and> tcbPriority ko \<le> maxPriority \<and> tcbMCP ko \<le> maxPriority\<rbrakk> \<Longrightarrow> valid_cap' (cteCap (a ko)) s proof (prove)
goal:
No subgoals!