theory Corres_UL

lemma corres_stateAssert_implied:
  "\<lbrakk> corres_underlying sr nf nf' r P Q f (g ());
     \<And>s s'. \<lbrakk> (s, s') \<in> sr; P s; P' s; Q s' \<rbrakk> \<Longrightarrow> Q' s' \<rbrakk>
   \<Longrightarrow> corres_underlying sr nf nf' r (P and P') Q f (stateAssert Q' [] >>= g)" apply (clarsimp simp: bind_assoc stateAssert_def) apply (rule corres_symb_exec_r [OF _ get_sp]) apply (rule corres_assume_pre) apply (rule corres_assert_assume) apply (erule corres_guard_imp, clarsimp+) apply (wp | rule no_fail_pre)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'\<rbrakk> \<Longrightarrow> Q' s'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (P and P') Q f (stateAssert Q' [] >>= g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'\<rbrakk> \<Longrightarrow> Q' s'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (P and P') Q f (do x <- get;
assert (Q' x) >>= g
od) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'\<rbrakk> \<Longrightarrow> Q' s'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (P and P') (\<lambda>s. s = x \<and> Q s) f (assert (Q' x) >>= g)
 2. \<And>s. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'\<rbrakk> \<Longrightarrow> Q' s'; Q s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'\<rbrakk> \<Longrightarrow> Q' s'; nf'\<rbrakk> \<Longrightarrow> no_fail Q get proof (prove)
goal (3 subgoals):
 1. \<And>x s s'. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'\<rbrakk> \<Longrightarrow> Q' s'; (P and P') s; s' = x \<and> Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (P and P') (\<lambda>s. s = x \<and> Q s) f (assert (Q' x) >>= g)
 2. \<And>s. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'\<rbrakk> \<Longrightarrow> Q' s'; Q s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'\<rbrakk> \<Longrightarrow> Q' s'; nf'\<rbrakk> \<Longrightarrow> no_fail Q get proof (prove)
goal (4 subgoals):
 1. \<And>x s s'. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'\<rbrakk> \<Longrightarrow> Q' s'; (P and P') s; s' = x \<and> Q s'; (s, s') \<in> sr; Q' x\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (P and P') (\<lambda>s. s = x \<and> Q s) f (g ())
 2. \<And>x s s' sa. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'\<rbrakk> \<Longrightarrow> Q' s'; (P and P') s; s' = x \<and> Q s'; (s, s') \<in> sr; sa = x \<and> Q sa\<rbrakk> \<Longrightarrow> Q' x
 3. \<And>s. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'\<rbrakk> \<Longrightarrow> Q' s'; Q s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'\<rbrakk> \<Longrightarrow> Q' s'; nf'\<rbrakk> \<Longrightarrow> no_fail Q get proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'\<rbrakk> \<Longrightarrow> Q' s'; Q s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'\<rbrakk> \<Longrightarrow> Q' s'; nf'\<rbrakk> \<Longrightarrow> no_fail Q get proof (prove)
goal:
No subgoals!