theory Arch_DR

lemma set_cap_corres_stronger:
assumes rules: "\<And>s.  P cap' s \<Longrightarrow> cap = transform_cap cap'"  "slot = transform_cslot_ptr slot'"
shows "dcorres dc \<top>
           (\<lambda>s. P cap' s \<and> valid_idle s \<and> fst slot' \<noteq> idle_thread s \<and> valid_etcbs s)
           (KHeap_D.set_cap slot cap)
           (CSpaceAcc_A.set_cap cap' slot')" 
(* corres_req2 *)
   apply (rule corres_req[rotated]) apply (rule corres_req[rotated]) apply (rule stronger_corres_guard_imp, erule(1) set_cap_corres) apply (auto simp add: rules) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. P cap' s \<and> valid_idle s \<and> fst slot' \<noteq> idle_thread s \<and> valid_etcbs s) (KHeap_D.set_cap slot cap) (CSpaceAcc_A.set_cap cap' slot') proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. P cap' s \<and> valid_idle s \<and> fst slot' \<noteq> idle_thread s \<and> valid_etcbs s) (KHeap_D.set_cap slot cap) (CSpaceAcc_A.set_cap cap' slot') proof (prove)
goal (2 subgoals):
 1. ?F \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. P cap' s \<and> valid_idle s \<and> fst slot' \<noteq> idle_thread s \<and> valid_etcbs s) (KHeap_D.set_cap slot cap) (CSpaceAcc_A.set_cap cap' slot')
 2. \<And>s s'. \<lbrakk>(s, s') \<in> {ss'. transform (snd ss') = fst ss'}; True; P cap' s' \<and> valid_idle s' \<and> fst slot' \<noteq> idle_thread s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> ?F proof (prove)
goal (3 subgoals):
 1. \<lbrakk>?F; ?F3\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. P cap' s \<and> valid_idle s \<and> fst slot' \<noteq> idle_thread s \<and> valid_etcbs s) (KHeap_D.set_cap slot cap) (CSpaceAcc_A.set_cap cap' slot')
 2. \<And>s s'. \<lbrakk>?F; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}; True; P cap' s' \<and> valid_idle s' \<and> fst slot' \<noteq> idle_thread s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> ?F3
 3. \<And>s s'. \<lbrakk>(s, s') \<in> {ss'. transform (snd ss') = fst ss'}; True; P cap' s' \<and> valid_idle s' \<and> fst slot' \<noteq> idle_thread s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> ?F proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>cap = transform_cap cap'; slot = transform_cslot_ptr slot'; True; P cap' s' \<and> valid_idle s' \<and> fst slot' \<noteq> idle_thread s' \<and> valid_etcbs s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> True
 2. \<And>s s'. \<lbrakk>cap = transform_cap cap'; slot = transform_cslot_ptr slot'; True; P cap' s' \<and> valid_idle s' \<and> fst slot' \<noteq> idle_thread s' \<and> valid_etcbs s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> valid_idle s' \<and> fst slot' \<noteq> idle_thread s' \<and> valid_etcbs s'
 3. \<And>s s'. \<lbrakk>cap = transform_cap cap'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}; True; P cap' s' \<and> valid_idle s' \<and> fst slot' \<noteq> idle_thread s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> slot = transform_cslot_ptr slot'
 4. \<And>s s'. \<lbrakk>(s, s') \<in> {ss'. transform (snd ss') = fst ss'}; True; P cap' s' \<and> valid_idle s' \<and> fst slot' \<noteq> idle_thread s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> cap = transform_cap cap' proof (prove)
goal:
No subgoals!