theory CSpace1_R

lemma lookupCap_corres:
 "corres (lfr \<oplus> cap_relation)
         (valid_objs and pspace_aligned and tcb_at t)
         (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t)
         (lookup_cap t (to_bl ref)) (lookupCap t ref)" apply (simp add: lookup_cap_def lookupCap_def bindE_assoc
                   lookupCapAndSlot_def liftME_def split_def) apply (rule corres_guard_imp) apply (rule corres_splitEE[OF lookupSlotForThread_corres]) apply (simp add: split_def getSlotCap_def liftM_def[symmetric] o_def) apply (rule get_cap_corres) apply (rule hoare_pre, wp lookup_slot_cte_at_wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (lfr \<oplus> cap_relation) (valid_objs and pspace_aligned and tcb_at t) (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) (lookup_cap t (to_bl ref)) (lookupCap t ref) proof (prove)
goal (1 subgoal):
 1. corres (lfr \<oplus> cap_relation) (valid_objs and pspace_aligned and tcb_at t) (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) (doE p <- lookup_slot_for_thread t (to_bl ref);
liftE (get_cap (fst p))
odE) (doE x <- lookupSlotForThread t ref;
liftE (getSlotCap x)
odE) proof (prove)
goal (3 subgoals):
 1. corres (lfr \<oplus> cap_relation) ?Q ?Q' (doE p <- lookup_slot_for_thread t (to_bl ref);
liftE (get_cap (fst p))
odE) (doE x <- lookupSlotForThread t ref;
liftE (getSlotCap x)
odE)
 2. \<And>s. (valid_objs and pspace_aligned and tcb_at t) s \<Longrightarrow> ?Q s
 3. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>p x. (case p of (cref, bits) \<Rightarrow> \<lambda>cref'. cref' = cte_map cref) x \<Longrightarrow> corres (lfr \<oplus> cap_relation) (?R4 p) (?R'4 x) (liftE (get_cap (fst p))) (liftE (getSlotCap x))
 2. \<lbrace>?Q4\<rbrace> lookup_slot_for_thread t (to_bl ref) \<lbrace>?R4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> lookupSlotForThread t ref \<lbrace>?R'4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. (valid_objs and pspace_aligned and tcb_at t) s \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at t and ?Q4) s
 5. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>p. corres (\<lambda>x xa. cap_relation x (cteCap xa)) (?R4 p) (?R'4 (cte_map (fst p))) (get_cap (fst p)) (getCTE (cte_map (fst p)))
 2. \<lbrace>?Q4\<rbrace> lookup_slot_for_thread t (to_bl ref) \<lbrace>?R4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> lookupSlotForThread t ref \<lbrace>?R'4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. (valid_objs and pspace_aligned and tcb_at t) s \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at t and ?Q4) s
 5. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> lookup_slot_for_thread t (to_bl ref) \<lbrace>\<lambda>p. cte_wp_at (\<lambda>_. True) (fst p)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> lookupSlotForThread t ref \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. (valid_objs and pspace_aligned and tcb_at t) s \<Longrightarrow> (valid_objs and pspace_aligned and tcb_at t and ?Q4) s
 4. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t and ?Q'4) s proof (prove)
goal:
No subgoals!