theory CNode_IF

lemma set_original_reads_respects:
  "reads_respects aag l \<top> (set_original slot v)" unfolding set_original_def apply (unfold equiv_valid_def2) apply (rule_tac Q="\<top>\<top>" in equiv_valid_rv_bind) apply (rule gets_is_original_cap_revrv) apply (rule modify_ev2) apply (clarsimp simp: equiv_for_or or_comp_dist) apply (safe) apply (erule reads_equiv_is_original_cap_update) apply (erule equiv_for_id_update) apply (erule affects_equiv_is_original_cap_update) apply (erule equiv_for_id_update) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (set_original slot v) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do r <- gets is_original_cap;
modify (is_original_cap_update (\<lambda>_. r(slot := v)))
od) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (\<lambda>_. True) (do r <- gets is_original_cap;
modify (is_original_cap_update (\<lambda>_. r(slot := v)))
od) proof (prove)
goal (3 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag ?W (\<lambda>_. True) (gets is_original_cap)
 2. \<And>rv rv'. ?W rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (\<lambda>_. True) (modify (is_original_cap_update (\<lambda>_. rv(slot := v)))) (modify (is_original_cap_update (\<lambda>_. rv'(slot := v))))
 3. \<lbrace>\<lambda>_. True\<rbrace> gets is_original_cap \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (\<lambda>_. True) (modify (is_original_cap_update (\<lambda>_. rv(slot := v)))) (modify (is_original_cap_update (\<lambda>_. rv'(slot := v))))
 2. \<lbrace>\<lambda>_. True\<rbrace> gets is_original_cap \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' s t. \<lbrakk>equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'; reads_equiv aag s t; affects_equiv aag l s t; True; True\<rbrakk> \<Longrightarrow> () = () \<and> reads_equiv aag (s\<lparr>is_original_cap := rv(slot := v)\<rparr>) (t\<lparr>is_original_cap := rv'(slot := v)\<rparr>) \<and> affects_equiv aag l (s\<lparr>is_original_cap := rv(slot := v)\<rparr>) (t\<lparr>is_original_cap := rv'(slot := v)\<rparr>)
 2. \<lbrace>\<lambda>_. True\<rbrace> gets is_original_cap \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; equiv_for (aag_can_read aag \<circ> fst) id rv rv'; equiv_for (aag_can_affect aag l \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> reads_equiv aag (s\<lparr>is_original_cap := rv(slot := v)\<rparr>) (t\<lparr>is_original_cap := rv'(slot := v)\<rparr>) \<and> affects_equiv aag l (s\<lparr>is_original_cap := rv(slot := v)\<rparr>) (t\<lparr>is_original_cap := rv'(slot := v)\<rparr>)
 2. \<lbrace>\<lambda>_. True\<rbrace> gets is_original_cap \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; equiv_for (aag_can_read aag \<circ> fst) id rv rv'; equiv_for (aag_can_affect aag l \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> reads_equiv aag (s\<lparr>is_original_cap := rv(slot := v)\<rparr>) (t\<lparr>is_original_cap := rv'(slot := v)\<rparr>)
 2. \<And>rv rv' s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; equiv_for (aag_can_read aag \<circ> fst) id rv rv'; equiv_for (aag_can_affect aag l \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> affects_equiv aag l (s\<lparr>is_original_cap := rv(slot := v)\<rparr>) (t\<lparr>is_original_cap := rv'(slot := v)\<rparr>)
 3. \<lbrace>\<lambda>_. True\<rbrace> gets is_original_cap \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' s t. \<lbrakk>affects_equiv aag l s t; equiv_for (aag_can_read aag \<circ> fst) id rv rv'; equiv_for (aag_can_affect aag l \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read aag \<circ> fst) id (rv(slot := v)) (rv'(slot := v))
 2. \<And>rv rv' s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; equiv_for (aag_can_read aag \<circ> fst) id rv rv'; equiv_for (aag_can_affect aag l \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> affects_equiv aag l (s\<lparr>is_original_cap := rv(slot := v)\<rparr>) (t\<lparr>is_original_cap := rv'(slot := v)\<rparr>)
 3. \<lbrace>\<lambda>_. True\<rbrace> gets is_original_cap \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' s t. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; equiv_for (aag_can_read aag \<circ> fst) id rv rv'; equiv_for (aag_can_affect aag l \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> affects_equiv aag l (s\<lparr>is_original_cap := rv(slot := v)\<rparr>) (t\<lparr>is_original_cap := rv'(slot := v)\<rparr>)
 2. \<lbrace>\<lambda>_. True\<rbrace> gets is_original_cap \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' s t. \<lbrakk>reads_equiv aag s t; equiv_for (aag_can_read aag \<circ> fst) id rv rv'; equiv_for (aag_can_affect aag l \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for (aag_can_affect aag l \<circ> fst) id (rv(slot := v)) (rv'(slot := v))
 2. \<lbrace>\<lambda>_. True\<rbrace> gets is_original_cap \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> gets is_original_cap \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal:
No subgoals!