theory Arch_IF

lemma equiv_valid_get_assert:
  "equiv_valid_inv I A P f
   \<Longrightarrow> equiv_valid_inv I A P (get >>= (\<lambda> s. assert (g s) >>= (\<lambda> y. f)))" apply (subst equiv_valid_def2) apply (rule_tac W="\<top>\<top>" in equiv_valid_rv_bind) apply (rule equiv_valid_rv_guard_imp) apply (rule equiv_valid_rv_trivial) apply wpsimp+ apply (rule_tac R'="\<top>\<top>" in equiv_valid_2_bind) apply (simp add: equiv_valid_def2) apply (rule assert_ev2) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P f \<Longrightarrow> equiv_valid_inv I A P (do s <- get;
y <- assert (g s);
f
od) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P f \<Longrightarrow> equiv_valid_rv_inv I A (=) P (do s <- get;
y <- assert (g s);
f
od) proof (prove)
goal (3 subgoals):
 1. equiv_valid_inv I A P f \<Longrightarrow> equiv_valid_rv_inv I A (\<lambda>_ _. True) P get
 2. \<And>rv rv'. \<lbrakk>equiv_valid_inv I A P f; True\<rbrakk> \<Longrightarrow> equiv_valid_2 I A A (=) (?Q rv) (?Q rv') (do y <- assert (g rv);
f
od) (do y <- assert (g rv');
f
od)
 3. equiv_valid_inv I A P f \<Longrightarrow> \<lbrace>P\<rbrace> get \<lbrace>?Q\<rbrace> proof (prove)
goal (4 subgoals):
 1. equiv_valid_inv I A P f \<Longrightarrow> equiv_valid_rv_inv I A (\<lambda>_ _. True) ?P2 get
 2. \<And>s. \<lbrakk>equiv_valid_inv I A P f; P s\<rbrakk> \<Longrightarrow> ?P2 s
 3. \<And>rv rv'. \<lbrakk>equiv_valid_inv I A P f; True\<rbrakk> \<Longrightarrow> equiv_valid_2 I A A (=) (?Q rv) (?Q rv') (do y <- assert (g rv);
f
od) (do y <- assert (g rv');
f
od)
 4. equiv_valid_inv I A P f \<Longrightarrow> \<lbrace>P\<rbrace> get \<lbrace>?Q\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>Pa. equiv_valid_inv I A P f \<Longrightarrow> \<lbrace>Pa\<rbrace> get \<lbrace>\<lambda>_. Pa\<rbrace>
 2. \<And>s. \<lbrakk>equiv_valid_inv I A P f; P s\<rbrakk> \<Longrightarrow> True
 3. \<And>rv rv'. \<lbrakk>equiv_valid_inv I A P f; True\<rbrakk> \<Longrightarrow> equiv_valid_2 I A A (=) (?Q rv) (?Q rv') (do y <- assert (g rv);
f
od) (do y <- assert (g rv');
f
od)
 4. equiv_valid_inv I A P f \<Longrightarrow> \<lbrace>P\<rbrace> get \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. equiv_valid_inv I A P f \<Longrightarrow> equiv_valid_2 I A A (=) (?Q rv) (?Q rv') (do y <- assert (g rv);
f
od) (do y <- assert (g rv');
f
od)
 2. equiv_valid_inv I A P f \<Longrightarrow> \<lbrace>P\<rbrace> get \<lbrace>?Q\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>equiv_valid_inv I A P f; True\<rbrakk> \<Longrightarrow> equiv_valid_2 I A A (=) (?Q15 rv rv' rva) (?Q'15 rv rv' rv'a) f f
 2. \<And>rv rv'. equiv_valid_inv I A P f \<Longrightarrow> equiv_valid_2 I A A (\<lambda>_ _. True) (?P'19 rv) (?P'19 rv') (assert (g rv)) (assert (g rv'))
 3. \<And>rv rv'. equiv_valid_inv I A P f \<Longrightarrow> \<lbrace>?S'20 rv\<rbrace> assert (g rv) \<lbrace>?Q15 rv rv'\<rbrace>
 4. \<And>rv rv'. equiv_valid_inv I A P f \<Longrightarrow> \<lbrace>?S'20 rv'\<rbrace> assert (g rv') \<lbrace>?Q'15 rv rv'\<rbrace>
 5. equiv_valid_inv I A P f \<Longrightarrow> \<lbrace>P\<rbrace> get \<lbrace>\<lambda>rv s. ?P'19 rv s \<and> ?S'20 rv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. equiv_valid_inv I A P f \<Longrightarrow> equiv_valid_2 I A A (\<lambda>_ _. True) (?P'19 rv) (?P'19 rv') (assert (g rv)) (assert (g rv'))
 2. \<And>rv rv'. equiv_valid_inv I A P f \<Longrightarrow> \<lbrace>?S'20 rv\<rbrace> assert (g rv) \<lbrace>\<lambda>a. P\<rbrace>
 3. \<And>rv rv'. equiv_valid_inv I A P f \<Longrightarrow> \<lbrace>?S'20 rv'\<rbrace> assert (g rv') \<lbrace>\<lambda>a. P\<rbrace>
 4. equiv_valid_inv I A P f \<Longrightarrow> \<lbrace>P\<rbrace> get \<lbrace>\<lambda>rv s. ?P'19 rv s \<and> ?S'20 rv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. equiv_valid_inv I A P f \<Longrightarrow> True
 2. \<And>rv rv'. equiv_valid_inv I A P f \<Longrightarrow> \<lbrace>?S'20 rv\<rbrace> assert (g rv) \<lbrace>\<lambda>a. P\<rbrace>
 3. \<And>rv rv'. equiv_valid_inv I A P f \<Longrightarrow> \<lbrace>?S'20 rv'\<rbrace> assert (g rv') \<lbrace>\<lambda>a. P\<rbrace>
 4. equiv_valid_inv I A P f \<Longrightarrow> \<lbrace>P\<rbrace> get \<lbrace>\<lambda>rv s. ?P'19 rv s \<and> ?S'20 rv s\<rbrace> proof (prove)
goal:
No subgoals!