theory CSpace1_R

lemma getSlotCap_tcb_corres:
  "corres (\<lambda>t c. cap_relation (tcb_ctable t) c)
          (tcb_at t and valid_objs and pspace_aligned)
          (pspace_distinct' and pspace_aligned')
          (gets_the (get_tcb t))
          (getSlotCap t)"
  (is "corres ?r ?P ?Q ?f ?g") using get_cap_corres [where cslot_ptr = "(t, tcb_cnode_index 0)"] apply (simp add: getSlotCap_def liftM_def[symmetric]) apply (drule corres_guard_imp [where P="?P" and P'="?Q"]) apply (clarsimp simp: cte_at_cases tcb_at_def
                   dest!: get_tcb_SomeD) apply simp apply (subst(asm) corres_cong [OF refl refl gets_the_tcb_get_cap[symmetric] refl refl]) apply simp apply (simp add: o_def cte_map_def tcb_cnode_index_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>t. cap_relation (tcb_ctable t)) (tcb_at t and valid_objs and pspace_aligned) (pspace_distinct' and pspace_aligned') (gets_the (get_tcb t)) (getSlotCap t) proof (prove)
using this:
corres (\<lambda>x y. cap_relation x (cteCap y)) (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 0)) (pspace_aligned' and pspace_distinct') (get_cap (t, tcb_cnode_index 0)) (getCTE (cte_map (t, tcb_cnode_index 0)))

goal (1 subgoal):
 1. corres (\<lambda>t. cap_relation (tcb_ctable t)) (tcb_at t and valid_objs and pspace_aligned) (pspace_distinct' and pspace_aligned') (gets_the (get_tcb t)) (getSlotCap t) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>x y. cap_relation x (cteCap y)) (cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 0)) (pspace_aligned' and pspace_distinct') (get_cap (t, tcb_cnode_index 0)) (getCTE (cte_map (t, tcb_cnode_index 0))) \<Longrightarrow> corres (\<lambda>x. cap_relation (tcb_ctable x) \<circ> cteCap) (tcb_at t and valid_objs and pspace_aligned) (pspace_distinct' and pspace_aligned') (gets_the (get_tcb t)) (getCTE t) proof (prove)
goal (3 subgoals):
 1. \<And>s. (tcb_at t and valid_objs and pspace_aligned) s \<Longrightarrow> cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 0) s
 2. \<And>s. (pspace_distinct' and pspace_aligned') s \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 3. corres (\<lambda>x y. cap_relation x (cteCap y)) (tcb_at t and valid_objs and pspace_aligned) (pspace_distinct' and pspace_aligned') (get_cap (t, tcb_cnode_index 0)) (getCTE (cte_map (t, tcb_cnode_index 0))) \<Longrightarrow> corres (\<lambda>x. cap_relation (tcb_ctable x) \<circ> cteCap) (tcb_at t and valid_objs and pspace_aligned) (pspace_distinct' and pspace_aligned') (gets_the (get_tcb t)) (getCTE t) proof (prove)
goal (2 subgoals):
 1. \<And>s. (pspace_distinct' and pspace_aligned') s \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 2. corres (\<lambda>x y. cap_relation x (cteCap y)) (tcb_at t and valid_objs and pspace_aligned) (pspace_distinct' and pspace_aligned') (get_cap (t, tcb_cnode_index 0)) (getCTE (cte_map (t, tcb_cnode_index 0))) \<Longrightarrow> corres (\<lambda>x. cap_relation (tcb_ctable x) \<circ> cteCap) (tcb_at t and valid_objs and pspace_aligned) (pspace_distinct' and pspace_aligned') (gets_the (get_tcb t)) (getCTE t) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>x y. cap_relation x (cteCap y)) (tcb_at t and valid_objs and pspace_aligned) (pspace_distinct' and pspace_aligned') (get_cap (t, tcb_cnode_index 0)) (getCTE (cte_map (t, tcb_cnode_index 0))) \<Longrightarrow> corres (\<lambda>x. cap_relation (tcb_ctable x) \<circ> cteCap) (tcb_at t and valid_objs and pspace_aligned) (pspace_distinct' and pspace_aligned') (gets_the (get_tcb t)) (getCTE t) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; (tcb_at t and valid_objs and pspace_aligned) s; (pspace_distinct' and pspace_aligned') s'\<rbrakk> \<Longrightarrow> tcb_at t s
 2. corres (\<lambda>x y. cap_relation x (cteCap y)) (tcb_at t and valid_objs and pspace_aligned) (pspace_distinct' and pspace_aligned') (liftM tcb_ctable (gets_the (get_tcb t))) (getCTE (cte_map (t, tcb_cnode_index 0))) \<Longrightarrow> corres (\<lambda>x. cap_relation (tcb_ctable x) \<circ> cteCap) (tcb_at t and valid_objs and pspace_aligned) (pspace_distinct' and pspace_aligned') (gets_the (get_tcb t)) (getCTE t) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>x y. cap_relation x (cteCap y)) (tcb_at t and valid_objs and pspace_aligned) (pspace_distinct' and pspace_aligned') (liftM tcb_ctable (gets_the (get_tcb t))) (getCTE (cte_map (t, tcb_cnode_index 0))) \<Longrightarrow> corres (\<lambda>x. cap_relation (tcb_ctable x) \<circ> cteCap) (tcb_at t and valid_objs and pspace_aligned) (pspace_distinct' and pspace_aligned') (gets_the (get_tcb t)) (getCTE t) proof (prove)
goal:
No subgoals!