theory Corres_UL

lemma corres_stateAssert_assume:
  "\<lbrakk> corres_underlying sr nf nf' r P Q f (g ()); \<And>s. Q s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow>
   corres_underlying sr nf nf' r P Q f (stateAssert P' [] >>= g)" apply (clarsimp simp: bind_assoc stateAssert_def) apply (rule corres_symb_exec_r [OF _ get_sp]) apply (rule corres_assert_assume) apply (rule corres_assume_pre) 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. Q s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P Q f (stateAssert P' [] >>= g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s. Q s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P Q f (do x <- get;
assert (P' x) >>= g
od) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s. Q s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P (\<lambda>s. s = x \<and> Q s) f (assert (P' x) >>= g)
 2. \<And>s. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s. Q s \<Longrightarrow> P' 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. Q s \<Longrightarrow> P' s; nf'\<rbrakk> \<Longrightarrow> no_fail Q get proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s. Q s \<Longrightarrow> P' s; P' x\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P (\<lambda>s. s = x \<and> Q s) f (g ())
 2. \<And>x s. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s. Q s \<Longrightarrow> P' s; s = x \<and> Q s\<rbrakk> \<Longrightarrow> P' x
 3. \<And>s. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s. Q s \<Longrightarrow> P' 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. Q s \<Longrightarrow> P' 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. Q s \<Longrightarrow> P' s; P' x; P s; s' = x \<and> Q s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P (\<lambda>s. s = x \<and> Q s) f (g ())
 2. \<And>x s. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s. Q s \<Longrightarrow> P' s; s = x \<and> Q s\<rbrakk> \<Longrightarrow> P' x
 3. \<And>s. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s. Q s \<Longrightarrow> P' 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. Q s \<Longrightarrow> P' 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. Q s \<Longrightarrow> P' 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. Q s \<Longrightarrow> P' s; nf'\<rbrakk> \<Longrightarrow> no_fail Q get proof (prove)
goal:
No subgoals!