theory Corres_UL

lemma corres_symb_exec_r_All:
  assumes nf: "\<And>rv. nf' \<Longrightarrow> no_fail (Q' rv) g"
  assumes x: "\<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv)"
  shows      "corres_underlying sr nf nf' r P (\<lambda>s. (\<forall>p \<in> fst (g s). snd p = s \<and> Q' (fst p) s) \<and> (\<exists>rv. Q' rv s))
                       f (do rv \<leftarrow> g; h rv od)" apply (clarsimp simp add: corres_underlying_def bind_def) apply (rule conjI) apply clarsimp apply (cut_tac rv=aa in x) apply (clarsimp simp add: corres_underlying_def bind_def) apply (drule(1) bspec, clarsimp)+ apply (insert nf) apply (clarsimp simp: no_fail_def) apply (erule (1) my_BallE) apply (cut_tac rv="aa" in x) apply (clarsimp simp add: corres_underlying_def bind_def) apply (drule(1) bspec, clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P (\<lambda>s. (\<forall>p\<in>fst (g s). snd p = s \<and> Q' (fst p) s) \<and> (\<exists>rv. Q' rv s)) f (g >>= h) proof (prove)
goal (1 subgoal):
 1. \<And>a b rv. \<lbrakk>(a, b) \<in> sr; P a; \<forall>p\<in>fst (g b). snd p = b \<and> Q' (fst p) b; Q' rv b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> (\<forall>y\<in>fst (g b). \<forall>x\<in>fst (case y of (x, xa) \<Rightarrow> h x xa). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> (\<forall>x\<in>fst (g b). \<not> snd (case x of (x, xa) \<Rightarrow> h x xa)) \<and> \<not> snd (g b)) proof (prove)
goal (2 subgoals):
 1. \<And>a b rv. \<lbrakk>(a, b) \<in> sr; P a; \<forall>p\<in>fst (g b). snd p = b \<and> Q' (fst p) b; Q' rv b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> \<forall>y\<in>fst (g b). \<forall>x\<in>fst (case y of (x, xa) \<Rightarrow> h x xa). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r'
 2. \<And>a b rv. \<lbrakk>(a, b) \<in> sr; P a; \<forall>p\<in>fst (g b). snd p = b \<and> Q' (fst p) b; Q' rv b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>x\<in>fst (g b). \<not> snd (case x of (x, xa) \<Rightarrow> h x xa)) \<and> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b rv aa ba ab bb. \<lbrakk>(a, b) \<in> sr; P a; \<forall>p\<in>fst (g b). snd p = b \<and> Q' (fst p) b; Q' rv b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); (ab, bb) \<in> fst (h aa ba)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, bb) \<in> sr \<and> r ra ab
 2. \<And>a b rv. \<lbrakk>(a, b) \<in> sr; P a; \<forall>p\<in>fst (g b). snd p = b \<and> Q' (fst p) b; Q' rv b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>x\<in>fst (g b). \<not> snd (case x of (x, xa) \<Rightarrow> h x xa)) \<and> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b rv aa ba ab bb. \<lbrakk>(a, b) \<in> sr; P a; \<forall>p\<in>fst (g b). snd p = b \<and> Q' (fst p) b; Q' rv b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); (ab, bb) \<in> fst (h aa ba); corres_underlying sr nf nf' r P (Q' aa) f (h aa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, bb) \<in> sr \<and> r ra ab
 2. \<And>a b rv. \<lbrakk>(a, b) \<in> sr; P a; \<forall>p\<in>fst (g b). snd p = b \<and> Q' (fst p) b; Q' rv b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>x\<in>fst (g b). \<not> snd (case x of (x, xa) \<Rightarrow> h x xa)) \<and> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b rv aa ba ab bb. \<lbrakk>(a, b) \<in> sr; P a; \<forall>p\<in>fst (g b). snd p = b \<and> Q' (fst p) b; Q' rv b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); (ab, bb) \<in> fst (h aa ba); \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> Q' aa s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (f s)) \<longrightarrow> (\<forall>x\<in>fst (h aa s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (h aa s'))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, bb) \<in> sr \<and> r ra ab
 2. \<And>a b rv. \<lbrakk>(a, b) \<in> sr; P a; \<forall>p\<in>fst (g b). snd p = b \<and> Q' (fst p) b; Q' rv b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>x\<in>fst (g b). \<not> snd (case x of (x, xa) \<Rightarrow> h x xa)) \<and> \<not> snd (g b) proof (prove)
goal (1 subgoal):
 1. \<And>a b rv. \<lbrakk>(a, b) \<in> sr; P a; \<forall>p\<in>fst (g b). snd p = b \<and> Q' (fst p) b; Q' rv b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>x\<in>fst (g b). \<not> snd (case x of (x, xa) \<Rightarrow> h x xa)) \<and> \<not> snd (g b) proof (prove)
goal (1 subgoal):
 1. \<And>a b rv. \<lbrakk>(a, b) \<in> sr; P a; \<forall>p\<in>fst (g b). snd p = b \<and> Q' (fst p) b; Q' rv b; nf \<longrightarrow> \<not> snd (f a); \<And>rv. nf' \<Longrightarrow> no_fail (Q' rv) g\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> (\<forall>x\<in>fst (g b). \<not> snd (case x of (x, xa) \<Rightarrow> h x xa)) \<and> \<not> snd (g b) proof (prove)
goal (1 subgoal):
 1. \<And>a b rv aa ba. \<lbrakk>(a, b) \<in> sr; P a; \<forall>p\<in>fst (g b). snd p = b \<and> Q' (fst p) b; Q' rv b; nf \<longrightarrow> \<not> snd (f a); \<And>rv. \<forall>s. Q' rv s \<longrightarrow> \<not> snd (g s); nf'; (aa, ba) \<in> fst (g b); snd (h aa ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b rv aa ba. \<lbrakk>(a, b) \<in> sr; P a; Q' rv b; nf \<longrightarrow> \<not> snd (f a); \<And>rv. \<forall>s. Q' rv s \<longrightarrow> \<not> snd (g s); nf'; (aa, ba) \<in> fst (g b); snd (h aa ba); snd (aa, ba) = b \<and> Q' (fst (aa, ba)) b\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b rv aa ba. \<lbrakk>(a, b) \<in> sr; P a; Q' rv b; nf \<longrightarrow> \<not> snd (f a); \<And>rv. \<forall>s. Q' rv s \<longrightarrow> \<not> snd (g s); nf'; (aa, ba) \<in> fst (g b); snd (h aa ba); snd (aa, ba) = b \<and> Q' (fst (aa, ba)) b; corres_underlying sr nf nf' r P (Q' aa) f (h aa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b rv aa. \<lbrakk>(a, b) \<in> sr; P a; Q' rv b; nf \<longrightarrow> \<not> snd (f a); \<And>rv. \<forall>s. Q' rv s \<longrightarrow> \<not> snd (g s); nf'; (aa, b) \<in> fst (g b); snd (h aa b); Q' aa b; \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> Q' aa s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (f s)) \<longrightarrow> (\<forall>x\<in>fst (h aa s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> \<not> snd (h aa s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!