theory CNode_IF

lemma update_cdt_reads_respects:
  "reads_respects aag l (K (\<forall>rv rv'.
      equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow>
      equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv'))
     (update_cdt f)" unfolding update_cdt_def apply (rule gen_asm_ev) apply (unfold equiv_valid_def2) apply (rule equiv_valid_rv_bind) apply (rule equiv_valid_rv_guard_imp[OF gets_cdt_revrv]) apply (rule TrueI) apply (rule set_cdt_ev2) apply (simp add: equiv_for_comp[symmetric]) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (\<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv')) (update_cdt f) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (\<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv')) (do t <- gets cdt;
set_cdt (f t)
od) proof (prove)
goal (1 subgoal):
 1. \<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv' \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do t <- gets cdt;
set_cdt (f t)
od) proof (prove)
goal (1 subgoal):
 1. \<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv' \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (\<lambda>_. True) (do t <- gets cdt;
set_cdt (f t)
od) proof (prove)
goal (3 subgoals):
 1. \<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv' \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag ?W2 (\<lambda>_. True) (gets cdt)
 2. \<And>rv rv'. \<lbrakk>\<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv'; ?W2 rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q2 rv) (?Q2 rv') (set_cdt (f rv)) (set_cdt (f rv'))
 3. \<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv' \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets cdt \<lbrace>?Q2\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv'; True\<rbrakk> \<Longrightarrow> True
 2. \<And>rv rv'. \<lbrakk>\<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv'; equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q2 rv) (?Q2 rv') (set_cdt (f rv)) (set_cdt (f rv'))
 3. \<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv' \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets cdt \<lbrace>?Q2\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. \<lbrakk>\<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv'; equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q2 rv) (?Q2 rv') (set_cdt (f rv)) (set_cdt (f rv'))
 2. \<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv' \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets cdt \<lbrace>?Q2\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. \<lbrakk>\<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv'; equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv'\<rbrakk> \<Longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id (f rv) (f rv')
 2. \<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv' \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets cdt \<lbrace>\<lambda>rv _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>rv rv'. equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) id rv rv' \<longrightarrow> equiv_for ((aag_can_read aag or aag_can_affect aag l) \<circ> fst) f rv rv' \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> gets cdt \<lbrace>\<lambda>rv _. True\<rbrace> proof (prove)
goal:
No subgoals!