theory CSpace1_R

lemma corres_stateAssert_assume_stronger:
  "\<lbrakk> corres_underlying sr nf nf' r P Q f (g ());
    \<And>s s'. \<lbrakk> (s, s') \<in> sr; P s; Q s' \<rbrakk> \<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_tac F="P' x" in corres_req) apply clarsimp apply (auto elim: corres_guard_imp)[1] apply wp+ 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; Q s'\<rbrakk> \<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 s'. \<lbrakk>(s, s') \<in> sr; P s; Q s'\<rbrakk> \<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 s'. \<lbrakk>(s, s') \<in> sr; P s; Q s'\<rbrakk> \<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 s'. \<lbrakk>(s, s') \<in> sr; P s; Q s'\<rbrakk> \<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 s'. \<lbrakk>(s, s') \<in> sr; P s; Q s'\<rbrakk> \<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 s'. \<lbrakk>(s, s') \<in> sr; P s; Q s'\<rbrakk> \<Longrightarrow> P' s'; (s, s') \<in> sr; P s; s' = x \<and> Q s'\<rbrakk> \<Longrightarrow> P' x
 2. \<And>x. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; Q s'\<rbrakk> \<Longrightarrow> P' s'; P' x\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P (\<lambda>s. s = x \<and> Q s) f (assert (P' x) >>= g)
 3. \<And>s. \<lbrakk>corres_underlying sr nf nf' r P Q f (g ()); \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; Q s'\<rbrakk> \<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 s'. \<lbrakk>(s, s') \<in> sr; P s; Q s'\<rbrakk> \<Longrightarrow> P' s'; nf'\<rbrakk> \<Longrightarrow> no_fail Q get 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; Q s'\<rbrakk> \<Longrightarrow> P' s'; P' x\<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 s'. \<lbrakk>(s, s') \<in> sr; P s; Q s'\<rbrakk> \<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 s'. \<lbrakk>(s, s') \<in> sr; P s; Q s'\<rbrakk> \<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 s'. \<lbrakk>(s, s') \<in> sr; P s; Q s'\<rbrakk> \<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 s'. \<lbrakk>(s, s') \<in> sr; P s; Q s'\<rbrakk> \<Longrightarrow> P' s'; nf'\<rbrakk> \<Longrightarrow> no_fail Q get proof (prove)
goal:
No subgoals!