theory Corres_UL

lemma corres_stateAssert_no_fail:
  "\<lbrakk> no_fail P (do v \<leftarrow> g; _ \<leftarrow> stateAssert X []; h v od);
     corres_underlying S False nf' r P Q (do v \<leftarrow> g; h v od) f \<rbrakk> \<Longrightarrow>
   corres_underlying S False nf' r P Q (do v \<leftarrow> g; _ \<leftarrow> stateAssert X []; h v od) f" apply (simp add: corres_underlying_def stateAssert_def get_def assert_def return_def no_fail_def fail_def cong: if_cong) apply (clarsimp simp: split_def Nondet_Monad.bind_def split: if_splits) apply (erule allE, erule (1) impE) apply (drule (1) bspec, clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail P (do v <- g;
_ <- stateAssert X [];
h v
od); corres_underlying S False nf' r P Q (g >>= h) f\<rbrakk> \<Longrightarrow> corres_underlying S False nf' r P Q (do v <- g;
_ <- stateAssert X [];
h v
od) f proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. P s \<longrightarrow> \<not> snd ((do v <- g;
_ <- do s <- \<lambda>s. ({(s, s)}, False);
if X s then \<lambda>s. ({((), s)}, False) else (\<lambda>s. ({}, True))
od;
h v
od) s); \<forall>x\<in>S. case x of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<forall>x\<in>fst (f s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((g >>= h) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> S \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (f s'))\<rbrakk> \<Longrightarrow> \<forall>x\<in>S. case x of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (\<forall>x\<in>fst (f s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((do v <- g;
_ <- do s <- \<lambda>s. ({(s, s)}, False);
if X s then \<lambda>s. ({((), s)}, False) else (\<lambda>s. ({}, True))
od;
h v
od) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> S \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (f s')) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (g s). (X (snd x) \<longrightarrow> \<not> snd (h (fst x) (snd x))) \<and> X (snd x)) \<and> \<not> snd (g s); \<forall>x\<in>S. P (fst x) \<and> Q (snd x) \<longrightarrow> (\<forall>xa\<in>fst (f (snd x)). \<exists>y\<in>fst (g (fst x)). \<exists>x\<in>fst (h (fst y) (snd y)). (snd x, snd xa) \<in> S \<and> r (fst x) (fst xa)) \<and> (nf' \<longrightarrow> \<not> snd (f (snd x))); (a, b) \<in> S; (aa, ba) \<in> fst (f b); P a; Q b\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (g a). \<exists>x\<in>fst (h (fst y) (snd y)). (snd x, ba) \<in> S \<and> r (fst x) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<forall>x\<in>S. P (fst x) \<and> Q (snd x) \<longrightarrow> (\<forall>xa\<in>fst (f (snd x)). \<exists>y\<in>fst (g (fst x)). \<exists>x\<in>fst (h (fst y) (snd y)). (snd x, snd xa) \<in> S \<and> r (fst x) (fst xa)) \<and> (nf' \<longrightarrow> \<not> snd (f (snd x))); (a, b) \<in> S; (aa, ba) \<in> fst (f b); P a; Q b; (\<forall>x\<in>fst (g a). (X (snd x) \<longrightarrow> \<not> snd (h (fst x) (snd x))) \<and> X (snd x)) \<and> \<not> snd (g a)\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (g a). \<exists>x\<in>fst (h (fst y) (snd y)). (snd x, ba) \<in> S \<and> r (fst x) aa proof (prove)
goal:
No subgoals!