theory Corres_UL

lemma corres_symb_exec_l_Ex:
  assumes x: "\<And>rv. corres_underlying sr nf nf' r (Q rv) P' (g rv) h"
  shows      "corres_underlying sr nf nf' r (\<lambda>s. \<exists>rv. Q rv s \<and> (rv, s) \<in> fst (f s)) P'
                       (do rv \<leftarrow> f; g rv od) h" apply (clarsimp simp add: corres_underlying_def) apply (cut_tac rv=rv in x) apply (clarsimp simp add: corres_underlying_def) apply (drule(1) bspec, clarsimp) apply (case_tac nf) apply (clarsimp simp: bind_def') apply blast apply clarsimp apply (drule(1) bspec, clarsimp) apply (clarsimp simp: bind_def | erule rev_bexI)+ done

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