theory TcbAcc_R

lemma get_tcb_cap_corres:
  "tcb_cap_cases ref = Some (getF, v) \<Longrightarrow>
   corres cap_relation (tcb_at t and valid_objs) (tcb_at' t and pspace_aligned' and pspace_distinct')
                       (liftM getF (gets_the (get_tcb t)))
                       (getSlotCap (cte_map (t, ref)))" apply (simp add: getSlotCap_def liftM_def[symmetric]) apply (rule corres_no_failI) apply (rule no_fail_pre, wp) apply (cases v, simp) apply (frule tcb_cases_related) apply (clarsimp simp: cte_at'_obj_at') apply (drule spec[where x=t]) apply (drule bspec, erule domI) apply simp apply clarsimp apply (clarsimp simp: gets_the_def simpler_gets_def
                        bind_def assert_opt_def tcb_at_def
                        return_def
                 dest!: get_tcb_SomeD) apply (drule use_valid [OF _ getCTE_sp[where P="(=) s'" for s'], OF _ refl]) apply (clarsimp simp: get_tcb_def return_def) apply (drule pspace_relation_ctes_ofI[OF state_relation_pspace_relation]) apply (rule cte_wp_at_tcbI[where t="(t, ref)"], fastforce+)[1] apply assumption+ apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cap_cases ref = Some (getF, v) \<Longrightarrow> corres cap_relation (tcb_at t and valid_objs) (tcb_at' t and pspace_aligned' and pspace_distinct') (liftM getF (gets_the (get_tcb t))) (getSlotCap (cte_map (t, ref))) proof (prove)
goal (1 subgoal):
 1. tcb_cap_cases ref = Some (getF, v) \<Longrightarrow> corres ((\<lambda>x. cap_relation x \<circ> cteCap) \<circ> getF) (tcb_at t and valid_objs) (tcb_at' t and pspace_aligned' and pspace_distinct') (gets_the (get_tcb t)) (getCTE (cte_map (t, ref))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_cap_cases ref = Some (getF, v); True\<rbrakk> \<Longrightarrow> no_fail (tcb_at' t and pspace_aligned' and pspace_distinct') (getCTE (cte_map (t, ref)))
 2. tcb_cap_cases ref = Some (getF, v) \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (tcb_at t and valid_objs) s \<and> (tcb_at' t and pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map (t, ref)) s'). \<exists>(r, t)\<in>fst (gets_the (get_tcb t) s). (t, t') \<in> state_relation \<and> ((\<lambda>x. cap_relation x \<circ> cteCap) \<circ> getF) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>tcb_cap_cases ref = Some (getF, v); True; (tcb_at' t and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (t, ref)) s
 2. tcb_cap_cases ref = Some (getF, v) \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (tcb_at t and valid_objs) s \<and> (tcb_at' t and pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map (t, ref)) s'). \<exists>(r, t)\<in>fst (gets_the (get_tcb t) s). (t, t') \<in> state_relation \<and> ((\<lambda>x. cap_relation x \<circ> cteCap) \<circ> getF) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>tcb_cap_cases ref = Some (getF, a, b); tcb_at' t s \<and> pspace_aligned' s \<and> pspace_distinct' s; v = (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (t, ref)) s
 2. tcb_cap_cases ref = Some (getF, v) \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (tcb_at t and valid_objs) s \<and> (tcb_at' t and pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map (t, ref)) s'). \<exists>(r, t)\<in>fst (gets_the (get_tcb t) s). (t, t') \<in> state_relation \<and> ((\<lambda>x. cap_relation x \<circ> cteCap) \<circ> getF) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>tcb_cap_cases ref = Some (getF, a, b); tcb_at' t s \<and> pspace_aligned' s \<and> pspace_distinct' s; v = (a, b); \<exists>getF' setF'. (\<forall>x. tcb_cte_cases (cte_map (x, ref) - x) = Some (getF', setF')) \<and> (\<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF tcb) (cteCap (getF' tcb')))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (t, ref)) s
 2. tcb_cap_cases ref = Some (getF, v) \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (tcb_at t and valid_objs) s \<and> (tcb_at' t and pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map (t, ref)) s'). \<exists>(r, t)\<in>fst (gets_the (get_tcb t) s). (t, t') \<in> state_relation \<and> ((\<lambda>x. cap_relation x \<circ> cteCap) \<circ> getF) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s a b getF' setF'. \<lbrakk>tcb_cap_cases ref = Some (getF, a, b); v = (a, b); tcb_at' t s; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF tcb) (cteCap (getF' tcb')); \<forall>x. tcb_cte_cases (cte_map (x, ref) - x) = Some (getF', setF'); pspace_aligned' s; pspace_distinct' s; \<forall>n\<in>dom tcb_cte_cases. \<not> tcb_at' (cte_map (t, ref) - n) s\<rbrakk> \<Longrightarrow> real_cte_at' (cte_map (t, ref)) s
 2. tcb_cap_cases ref = Some (getF, v) \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (tcb_at t and valid_objs) s \<and> (tcb_at' t and pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map (t, ref)) s'). \<exists>(r, t)\<in>fst (gets_the (get_tcb t) s). (t, t') \<in> state_relation \<and> ((\<lambda>x. cap_relation x \<circ> cteCap) \<circ> getF) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s a b getF' setF'. \<lbrakk>tcb_cap_cases ref = Some (getF, a, b); v = (a, b); tcb_at' t s; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF tcb) (cteCap (getF' tcb')); pspace_aligned' s; pspace_distinct' s; \<forall>n\<in>dom tcb_cte_cases. \<not> tcb_at' (cte_map (t, ref) - n) s; tcb_cte_cases (cte_map (t, ref) - t) = Some (getF', setF')\<rbrakk> \<Longrightarrow> real_cte_at' (cte_map (t, ref)) s
 2. tcb_cap_cases ref = Some (getF, v) \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (tcb_at t and valid_objs) s \<and> (tcb_at' t and pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map (t, ref)) s'). \<exists>(r, t)\<in>fst (gets_the (get_tcb t) s). (t, t') \<in> state_relation \<and> ((\<lambda>x. cap_relation x \<circ> cteCap) \<circ> getF) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s a b getF' setF'. \<lbrakk>tcb_cap_cases ref = Some (getF, a, b); v = (a, b); tcb_at' t s; \<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF tcb) (cteCap (getF' tcb')); pspace_aligned' s; pspace_distinct' s; tcb_cte_cases (cte_map (t, ref) - t) = Some (getF', setF'); \<not> tcb_at' (cte_map (t, ref) - (cte_map (t, ref) - t)) s\<rbrakk> \<Longrightarrow> real_cte_at' (cte_map (t, ref)) s
 2. tcb_cap_cases ref = Some (getF, v) \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (tcb_at t and valid_objs) s \<and> (tcb_at' t and pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map (t, ref)) s'). \<exists>(r, t)\<in>fst (gets_the (get_tcb t) s). (t, t') \<in> state_relation \<and> ((\<lambda>x. cap_relation x \<circ> cteCap) \<circ> getF) r r') proof (prove)
goal (1 subgoal):
 1. tcb_cap_cases ref = Some (getF, v) \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (tcb_at t and valid_objs) s \<and> (tcb_at' t and pspace_aligned' and pspace_distinct') s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE (cte_map (t, ref)) s'). \<exists>(r, t)\<in>fst (gets_the (get_tcb t) s). (t, t') \<in> state_relation \<and> ((\<lambda>x. cap_relation x \<circ> cteCap) \<circ> getF) r r') proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>tcb_cap_cases ref = Some (getF, v); (a, b) \<in> state_relation; (aa, ba) \<in> fst (getCTE (cte_map (t, ref)) b); tcb_at t a; valid_objs a; tcb_at' t b; pspace_aligned' b; pspace_distinct' b\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (gets_the (get_tcb t) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> state_relation \<and> cap_relation (getF r) (cteCap aa) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba tcb. \<lbrakk>tcb_cap_cases ref = Some (getF, v); (a, b) \<in> state_relation; (aa, ba) \<in> fst (getCTE (cte_map (t, ref)) b); valid_objs a; tcb_at' t b; pspace_aligned' b; pspace_distinct' b; kheap a t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((case get_tcb t a of None \<Rightarrow> fail | Some v \<Rightarrow> \<lambda>s. ({(v, s)}, False)) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> state_relation \<and> cap_relation (getF r) (cteCap aa) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba tcb. \<lbrakk>tcb_cap_cases ref = Some (getF, v); (a, b) \<in> state_relation; valid_objs a; tcb_at' t b; pspace_aligned' b; pspace_distinct' b; kheap a t = Some (TCB tcb); (cte_wp_at' (\<lambda>c. c = aa) (cte_map (t, ref)) and (=) b) ba\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((case get_tcb t a of None \<Rightarrow> fail | Some v \<Rightarrow> \<lambda>s. ({(v, s)}, False)) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> state_relation \<and> cap_relation (getF r) (cteCap aa) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa tcb. \<lbrakk>tcb_cap_cases ref = Some (getF, v); (a, b) \<in> state_relation; valid_objs a; tcb_at' t b; pspace_aligned' b; pspace_distinct' b; kheap a t = Some (TCB tcb); cte_wp_at' (\<lambda>c. c = aa) (cte_map (t, ref)) b\<rbrakk> \<Longrightarrow> cap_relation (getF tcb) (cteCap aa) proof (prove)
goal (4 subgoals):
 1. \<And>a b aa tcb. \<lbrakk>tcb_cap_cases ref = Some (getF, v); valid_objs a; tcb_at' t b; pspace_aligned' b; pspace_distinct' b; kheap a t = Some (TCB tcb); cte_wp_at' (\<lambda>c. c = aa) (cte_map (t, ref)) b\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?c37 a b aa tcb)) (?slot37 a b aa tcb) a
 2. \<And>a b aa tcb. \<lbrakk>tcb_cap_cases ref = Some (getF, v); valid_objs a; tcb_at' t b; pspace_aligned' b; pspace_distinct' b; kheap a t = Some (TCB tcb); cte_wp_at' (\<lambda>c. c = aa) (cte_map (t, ref)) b\<rbrakk> \<Longrightarrow> pspace_aligned' b
 3. \<And>a b aa tcb. \<lbrakk>tcb_cap_cases ref = Some (getF, v); valid_objs a; tcb_at' t b; pspace_aligned' b; pspace_distinct' b; kheap a t = Some (TCB tcb); cte_wp_at' (\<lambda>c. c = aa) (cte_map (t, ref)) b\<rbrakk> \<Longrightarrow> pspace_distinct' b
 4. \<And>a b aa tcb. \<lbrakk>tcb_cap_cases ref = Some (getF, v); valid_objs a; tcb_at' t b; pspace_aligned' b; pspace_distinct' b; kheap a t = Some (TCB tcb); cte_wp_at' (\<lambda>c. c = aa) (cte_map (t, ref)) b; \<exists>cte. ctes_of b (cte_map (?slot37 a b aa tcb)) = Some cte \<and> cap_relation (?c37 a b aa tcb) (cteCap cte)\<rbrakk> \<Longrightarrow> cap_relation (getF tcb) (cteCap aa) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa tcb. \<lbrakk>tcb_cap_cases ref = Some (getF, v); valid_objs a; tcb_at' t b; pspace_aligned' b; pspace_distinct' b; kheap a t = Some (TCB tcb); cte_wp_at' (\<lambda>c. c = aa) (cte_map (t, ref)) b\<rbrakk> \<Longrightarrow> pspace_aligned' b
 2. \<And>a b aa tcb. \<lbrakk>tcb_cap_cases ref = Some (getF, v); valid_objs a; tcb_at' t b; pspace_aligned' b; pspace_distinct' b; kheap a t = Some (TCB tcb); cte_wp_at' (\<lambda>c. c = aa) (cte_map (t, ref)) b\<rbrakk> \<Longrightarrow> pspace_distinct' b
 3. \<And>a b aa tcb. \<lbrakk>tcb_cap_cases ref = Some (getF, v); valid_objs a; tcb_at' t b; pspace_aligned' b; pspace_distinct' b; kheap a t = Some (TCB tcb); cte_wp_at' (\<lambda>c. c = aa) (cte_map (t, ref)) b; \<exists>cte. ctes_of b (cte_map (t, ref)) = Some cte \<and> cap_relation (getF tcb) (cteCap cte)\<rbrakk> \<Longrightarrow> cap_relation (getF tcb) (cteCap aa) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa tcb. \<lbrakk>tcb_cap_cases ref = Some (getF, v); valid_objs a; tcb_at' t b; pspace_aligned' b; pspace_distinct' b; kheap a t = Some (TCB tcb); cte_wp_at' (\<lambda>c. c = aa) (cte_map (t, ref)) b; \<exists>cte. ctes_of b (cte_map (t, ref)) = Some cte \<and> cap_relation (getF tcb) (cteCap cte)\<rbrakk> \<Longrightarrow> cap_relation (getF tcb) (cteCap aa) proof (prove)
goal:
No subgoals!