theory Corres_UL

lemma corres_stateAssert_implied2:
  assumes c: "corres_underlying sr nf nf' r P Q f g"
  assumes sr: "\<And>s s'. \<lbrakk>(s, s') \<in> sr; R s; R' s'\<rbrakk> \<Longrightarrow> Q' s'"
  assumes f: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. R\<rbrace>"
  assumes g: "\<lbrace>Q\<rbrace> g \<lbrace>\<lambda>_. R'\<rbrace>"
  shows "corres_underlying sr nf nf' dc P Q f (g >>= (\<lambda>_. stateAssert Q' []))" apply (subst bind_return[symmetric]) apply corres_pre apply (rule corres_split) apply (rule c) apply (clarsimp simp: corres_underlying_def return_def
                            stateAssert_def bind_def get_def assert_def
                            fail_def) apply (drule (2) sr) apply simp apply (rule f) apply (rule g) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' dc P Q f (do _ <- g;
stateAssert Q' []
od) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' dc P Q (f >>= return) (do _ <- g;
stateAssert Q' []
od) proof (prove)
goal (3 subgoals):
 1. corres_underlying sr nf nf' dc ?Q ?Q' (f >>= return) (do _ <- g;
stateAssert Q' []
od)
 2. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (6 subgoals):
 1. corres_underlying sr nf nf' ?r'1 ?P1 ?P'1 f g
 2. \<And>rv uu_. ?r'1 rv uu_ \<Longrightarrow> corres_underlying sr nf nf' dc (?R1 rv) (?R'1 uu_) (return rv) (stateAssert Q' [])
 3. \<lbrace>?Q1\<rbrace> f \<lbrace>?R1\<rbrace>
 4. \<lbrace>?Q'1\<rbrace> g \<lbrace>?R'1\<rbrace>
 5. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (?P1 and ?Q1) s
 6. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (?P'1 and ?Q'1) s' proof (prove)
goal (5 subgoals):
 1. \<And>rv uu_. r rv uu_ \<Longrightarrow> corres_underlying sr nf nf' dc (?R1 rv) (?R'1 uu_) (return rv) (stateAssert Q' [])
 2. \<lbrace>?Q1\<rbrace> f \<lbrace>?R1\<rbrace>
 3. \<lbrace>?Q'1\<rbrace> g \<lbrace>?R'1\<rbrace>
 4. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P and ?Q1) s
 5. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (Q and ?Q'1) s' proof (prove)
goal (5 subgoals):
 1. \<And>rv uu_ a b. \<lbrakk>r rv uu_; (a, b) \<in> sr; \<not> Q' b; ?R1 rv a; ?R'1 uu_ b; nf'\<rbrakk> \<Longrightarrow> False
 2. \<lbrace>?Q1\<rbrace> f \<lbrace>?R1\<rbrace>
 3. \<lbrace>?Q'1\<rbrace> g \<lbrace>?R'1\<rbrace>
 4. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P and ?Q1) s
 5. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (Q and ?Q'1) s' proof (prove)
goal (5 subgoals):
 1. \<And>rv uu_ a b. \<lbrakk>r rv uu_; \<not> Q' b; R a; R' b; nf'; Q' b\<rbrakk> \<Longrightarrow> False
 2. \<lbrace>?Q1\<rbrace> f \<lbrace>\<lambda>rv. R\<rbrace>
 3. \<lbrace>?Q'1\<rbrace> g \<lbrace>\<lambda>_. R'\<rbrace>
 4. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P and ?Q1) s
 5. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (Q and ?Q'1) s' proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q1\<rbrace> f \<lbrace>\<lambda>rv. R\<rbrace>
 2. \<lbrace>?Q'1\<rbrace> g \<lbrace>\<lambda>_. R'\<rbrace>
 3. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P and ?Q1) s
 4. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (Q and ?Q'1) s' proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'1\<rbrace> g \<lbrace>\<lambda>_. R'\<rbrace>
 2. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P and P) s
 3. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (Q and ?Q'1) s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (P and P) s
 2. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (Q and Q) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (Q and Q) s' proof (prove)
goal:
No subgoals!