theory AutoCorres_C

lemma corres_symb_exec_l'':
  assumes corres: "\<And>rv. corres_underlying sr nf nf' r (R rv) (R' rv) (x rv) y"
  assumes no_upd: "\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>"
  assumes result: "\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>"
  assumes nofail: "\<not> nf \<longrightarrow> no_fail P m"
  assumes mtfail: "empty_fail m"
  shows "corres_underlying sr nf nf' r
                           (P and Q) (\<lambda>s'. \<forall>rv s. (s,s') \<in> sr \<and> R rv s \<longrightarrow> R' rv s')
                           (m >>= (\<lambda>rv. x rv)) y" using corres unfolding corres_underlying_def apply (clarsimp; rename_tac s s') apply (subgoal_tac "\<not> snd (m s)") prefer 2 using nofail apply (cases nf; clarsimp simp: no_fail_def elim!: not_snd_bindI1) apply (erule empty_fail_not_snd [OF _ mtfail, THEN exE]; clarsimp; rename_tac rv t) apply (subgoal_tac "t = s") prefer 2 apply (frule use_valid, rule no_upd, simp+) apply clarsimp apply (drule_tac x=rv in spec, drule_tac x=rv in meta_spec, drule (1) bspec, simp) apply (frule use_valid, rule result, assumption) apply (drule mp, rule_tac x=s in exI, simp_all) apply (subgoal_tac "nf \<longrightarrow> \<not> snd (x rv s)") prefer 2 apply (cases nf; clarsimp simp: no_fail_def elim!: not_snd_bindI2) apply (clarsimp; rename_tac fv' t') apply (drule (1) bspec; clarsimp; rename_tac fv t) apply (rule_tac x="(fv,t)" in bexI; clarsimp simp: bind_def) apply (rule bexI[rotated], assumption, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and Q) (\<lambda>s'. \<forall>rv s. (s, s') \<in> sr \<and> R rv s \<longrightarrow> R' rv s') (m >>= x) y proof (prove)
using this:
corres_underlying sr nf nf' r (R ?rv1) (R' ?rv1) (x ?rv1) y

goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and Q) (\<lambda>s'. \<forall>rv s. (s, s') \<in> sr \<and> R rv s \<longrightarrow> R' rv s') (m >>= x) y proof (prove)
using this:
\<forall>(s, s')\<in>sr. R ?rv1 s \<and> R' ?rv1 s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x ?rv1 s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x ?rv1 s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s'))

goal (1 subgoal):
 1. \<forall>(s, s')\<in>sr. (P and Q) s \<and> (\<forall>rv s. (s, s') \<in> sr \<and> R rv s \<longrightarrow> R' rv s') \<longrightarrow> (nf \<longrightarrow> \<not> snd ((m >>= x) s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst ((m >>= x) s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>(s, s')\<in>sr. R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x rv s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s'))\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>\<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>(s, s')\<in>sr. R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x rv s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); \<not> snd (m s)\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s'))
 2. \<And>s s'. \<lbrakk>\<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>(s, s')\<in>sr. R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x rv s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s'))\<rbrakk> \<Longrightarrow> \<not> snd (m s) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>\<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>(s, s')\<in>sr. R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x rv s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s'))\<rbrakk> \<Longrightarrow> \<not> snd (m s)
 2. \<And>s s'. \<lbrakk>\<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>(s, s')\<in>sr. R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x rv s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); \<not> snd (m s)\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')) proof (prove)
using this:
\<not> nf \<longrightarrow> no_fail P m

goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>\<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>(s, s')\<in>sr. R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x rv s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s'))\<rbrakk> \<Longrightarrow> \<not> snd (m s)
 2. \<And>s s'. \<lbrakk>\<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>(s, s')\<in>sr. R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x rv s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); \<not> snd (m s)\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>(s, s')\<in>sr. R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x rv s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); \<not> snd (m s)\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')) proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv t. \<lbrakk>(s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (rv, t) \<in> fst (m s)\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')) proof (prove)
goal (2 subgoals):
 1. \<And>s s' rv t. \<lbrakk>(s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (rv, t) \<in> fst (m s); t = s\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s'))
 2. \<And>s s' rv t. \<lbrakk>(s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (rv, t) \<in> fst (m s)\<rbrakk> \<Longrightarrow> t = s proof (prove)
goal (2 subgoals):
 1. \<And>s s' rv t. \<lbrakk>(s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (rv, t) \<in> fst (m s)\<rbrakk> \<Longrightarrow> t = s
 2. \<And>s s' rv t. \<lbrakk>(s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (rv, t) \<in> fst (m s); t = s\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')) proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv t. \<lbrakk>(s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (rv, s) \<in> fst (m s); t = s\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')) proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv. \<lbrakk>(s, s') \<in> sr; P s; Q s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; nf \<longrightarrow> \<not> snd ((m >>= x) s); \<And>rv. \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (rv, s) \<in> fst (m s)\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')) proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv. \<lbrakk>(s, s') \<in> sr; P s; Q s; nf \<longrightarrow> \<not> snd ((m >>= x) s); (rv, s) \<in> fst (m s); (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s'))\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')) proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv. \<lbrakk>(s, s') \<in> sr; P s; Q s; nf \<longrightarrow> \<not> snd ((m >>= x) s); (rv, s) \<in> fst (m s); (\<exists>s. (s, s') \<in> sr \<and> R rv s) \<longrightarrow> R' rv s'; R rv s \<and> R' rv s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); R rv s\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')) proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv. \<lbrakk>(s, s') \<in> sr; P s; Q s; nf \<longrightarrow> \<not> snd ((m >>= x) s); (rv, s) \<in> fst (m s); (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x rv s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); R rv s; R' rv s'\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')) proof (prove)
goal (2 subgoals):
 1. \<And>s s' rv. \<lbrakk>(s, s') \<in> sr; P s; Q s; nf \<longrightarrow> \<not> snd ((m >>= x) s); (rv, s) \<in> fst (m s); (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x rv s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); R rv s; R' rv s'; nf \<longrightarrow> \<not> snd (x rv s)\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s'))
 2. \<And>s s' rv. \<lbrakk>(s, s') \<in> sr; P s; Q s; nf \<longrightarrow> \<not> snd ((m >>= x) s); (rv, s) \<in> fst (m s); (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x rv s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); R rv s; R' rv s'\<rbrakk> \<Longrightarrow> nf \<longrightarrow> \<not> snd (x rv s) proof (prove)
goal (2 subgoals):
 1. \<And>s s' rv. \<lbrakk>(s, s') \<in> sr; P s; Q s; nf \<longrightarrow> \<not> snd ((m >>= x) s); (rv, s) \<in> fst (m s); (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x rv s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); R rv s; R' rv s'\<rbrakk> \<Longrightarrow> nf \<longrightarrow> \<not> snd (x rv s)
 2. \<And>s s' rv. \<lbrakk>(s, s') \<in> sr; P s; Q s; nf \<longrightarrow> \<not> snd ((m >>= x) s); (rv, s) \<in> fst (m s); (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x rv s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); R rv s; R' rv s'; nf \<longrightarrow> \<not> snd (x rv s)\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')) proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv. \<lbrakk>(s, s') \<in> sr; P s; Q s; nf \<longrightarrow> \<not> snd ((m >>= x) s); (rv, s) \<in> fst (m s); (nf \<longrightarrow> \<not> snd (x rv s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (y s'). \<exists>(ra, t)\<in>fst (x rv s). (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); R rv s; R' rv s'; nf \<longrightarrow> \<not> snd (x rv s)\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')) proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv fv' t'. \<lbrakk>(s, s') \<in> sr; P s; Q s; nf \<longrightarrow> \<not> snd ((m >>= x) s); (rv, s) \<in> fst (m s); R rv s; R' rv s'; nf \<longrightarrow> \<not> snd (x rv s); (fv', t') \<in> fst (y s'); \<forall>xa\<in>fst (y s'). case xa of (r', t') \<Rightarrow> \<exists>x\<in>fst (x rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r'; nf' \<longrightarrow> \<not> snd (y s')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra fv' proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv fv' t' fv t. \<lbrakk>(s, s') \<in> sr; P s; Q s; nf \<longrightarrow> \<not> snd ((m >>= x) s); (rv, s) \<in> fst (m s); R rv s; R' rv s'; nf \<longrightarrow> \<not> snd (x rv s); (fv', t') \<in> fst (y s'); nf' \<longrightarrow> \<not> snd (y s'); (fv, t) \<in> fst (x rv s); (t, t') \<in> sr; r fv fv'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((m >>= x) s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra fv' proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv fv' t' fv t. \<lbrakk>(s, s') \<in> sr; P s; Q s; nf \<longrightarrow> (\<forall>xa\<in>fst (m s). \<not> snd (case xa of (xa, xb) \<Rightarrow> x xa xb)) \<and> \<not> snd (m s); (rv, s) \<in> fst (m s); R rv s; R' rv s'; nf \<longrightarrow> \<not> snd (x rv s); (fv', t') \<in> fst (y s'); nf' \<longrightarrow> \<not> snd (y s'); (fv, t) \<in> fst (x rv s); (t, t') \<in> sr; r fv fv'\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (m s). (fv, t) \<in> fst (case xa of (xa, xb) \<Rightarrow> x xa xb) proof (prove)
goal:
No subgoals!