theory Finalise_DR

lemma dcorres_get_cap_symb_exec:
  "\<lbrakk> \<And>cap. dcorres r (P cap) (P' cap) f (g cap) \<rbrakk>
        \<Longrightarrow> dcorres r
          (\<lambda>s. \<forall>cap. opt_cap (transform_cslot_ptr slot) s = Some (transform_cap cap) \<longrightarrow> P cap s)
          (\<lambda>s. fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s)
          f (do cap \<leftarrow> get_cap slot; g cap od)" apply (rule corres_symb_exec_r[OF _ get_cap_sp]) apply (rule stronger_corres_guard_imp, assumption) apply (clarsimp simp: cte_wp_at_caps_of_state caps_of_state_transform_opt_cap) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>cap. dcorres r (P cap) (P' cap) f (g cap)) \<Longrightarrow> dcorres r (\<lambda>s. \<forall>cap. opt_cap (transform_cslot_ptr slot) s = Some (transform_cap cap) \<longrightarrow> P cap s) (\<lambda>s. fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s) f (CSpaceAcc_A.get_cap slot >>= g) proof (prove)
goal (3 subgoals):
 1. \<And>cap. (\<And>cap. dcorres r (P cap) (P' cap) f (g cap)) \<Longrightarrow> dcorres r (\<lambda>s. \<forall>cap. opt_cap (transform_cslot_ptr slot) s = Some (transform_cap cap) \<longrightarrow> P cap s) ((\<lambda>s. fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s) and cte_wp_at (\<lambda>c. c = cap) slot) f (g cap)
 2. \<And>s. \<lbrakk>\<And>cap. dcorres r (P cap) (P' cap) f (g cap); fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>\<And>cap. dcorres r (P cap) (P' cap) f (g cap); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (4 subgoals):
 1. \<And>cap s s'. \<lbrakk>\<And>cap. dcorres r (P cap) (P' cap) f (g cap); \<forall>cap. opt_cap (transform_cslot_ptr slot) s = Some (transform_cap cap) \<longrightarrow> P cap s; ((\<lambda>s. fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s) and cte_wp_at (\<lambda>c. c = cap) slot) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> P cap s
 2. \<And>cap s s'. \<lbrakk>\<And>cap. dcorres r (P cap) (P' cap) f (g cap); \<forall>cap. opt_cap (transform_cslot_ptr slot) s = Some (transform_cap cap) \<longrightarrow> P cap s; ((\<lambda>s. fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s) and cte_wp_at (\<lambda>c. c = cap) slot) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> P' cap s'
 3. \<And>s. \<lbrakk>\<And>cap. dcorres r (P cap) (P' cap) f (g cap); fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>\<And>cap. dcorres r (P cap) (P' cap) f (g cap); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (3 subgoals):
 1. \<And>cap s s'. \<lbrakk>\<And>cap. dcorres r (P cap) (P' cap) f (g cap); \<forall>cap. opt_cap (transform_cslot_ptr slot) s = Some (transform_cap cap) \<longrightarrow> P cap s; ((\<lambda>s. fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s) and cte_wp_at (\<lambda>c. c = cap) slot) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> P' cap s'
 2. \<And>s. \<lbrakk>\<And>cap. dcorres r (P cap) (P' cap) f (g cap); fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>\<And>cap. dcorres r (P cap) (P' cap) f (g cap); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>cap. dcorres r (P cap) (P' cap) f (g cap); fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrakk>\<And>cap. dcorres r (P cap) (P' cap) f (g cap); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s) (CSpaceAcc_A.get_cap slot) proof (prove)
goal:
No subgoals!