theory Corres_UL

lemma corres_stronger_no_failI:
  assumes f': "nf' \<Longrightarrow> no_fail (\<lambda>s'. \<exists>s. P s \<and> (s,s') \<in> S \<and> P' s')  f'"
  assumes corres: "\<forall>(s, s') \<in> S. P s \<and> P' s' \<longrightarrow>
                     (\<forall>(r', t') \<in> fst (f' s'). \<exists>(r, t) \<in> fst (f s). (t, t') \<in> S \<and> R r r')"
  shows "corres_underlying S nf nf' R P P' f f'" using assms apply (simp add: corres_underlying_def no_fail_def) apply clarsimp apply (rule conjI) apply clarsimp apply blast apply clarsimp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying S nf nf' R P P' f f' proof (prove)
using this:
nf' \<Longrightarrow> no_fail (\<lambda>s'. \<exists>s. P s \<and> (s, s') \<in> S \<and> P' s') f'
\<forall>(s, s')\<in>S. P s \<and> P' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (f' s'). \<exists>(r, t)\<in>fst (f s). (t, t') \<in> S \<and> R r r')

goal (1 subgoal):
 1. corres_underlying S nf nf' R P P' f f' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nf' \<Longrightarrow> \<forall>s. (\<exists>sa. P sa \<and> (sa, s) \<in> S \<and> P' s) \<longrightarrow> \<not> snd (f' s); \<forall>x\<in>S. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (f' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> S \<and> R r r')\<rbrakk> \<Longrightarrow> \<forall>x\<in>S. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (f s)) \<longrightarrow> (\<forall>x\<in>fst (f' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> S \<and> R r r') \<and> (nf' \<longrightarrow> \<not> snd (f' s')) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>nf' \<Longrightarrow> \<forall>s. (\<exists>sa. P sa \<and> (sa, s) \<in> S \<and> P' s) \<longrightarrow> \<not> snd (f' s); \<forall>x\<in>S. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (f' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> S \<and> R r r'); (a, b) \<in> S; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (f' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (r, t) \<Rightarrow> (t, t') \<in> S \<and> R r r') \<and> (nf' \<longrightarrow> \<not> snd (f' b)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>nf' \<Longrightarrow> \<forall>s. (\<exists>sa. P sa \<and> (sa, s) \<in> S \<and> P' s) \<longrightarrow> \<not> snd (f' s); \<forall>x\<in>S. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (f' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> S \<and> R r r'); (a, b) \<in> S; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (r, t) \<Rightarrow> (t, t') \<in> S \<and> R r r'
 2. \<And>a b. \<lbrakk>nf' \<Longrightarrow> \<forall>s. (\<exists>sa. P sa \<and> (sa, s) \<in> S \<and> P' s) \<longrightarrow> \<not> snd (f' s); \<forall>x\<in>S. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (f' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> S \<and> R r r'); (a, b) \<in> S; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (f' b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>nf' \<Longrightarrow> \<forall>s. (\<exists>sa. P sa \<and> (sa, s) \<in> S \<and> P' s) \<longrightarrow> \<not> snd (f' s); \<forall>x\<in>S. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (f' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> S \<and> R r r'); (a, b) \<in> S; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (f' b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (r, t) \<Rightarrow> (t, ba) \<in> S \<and> R r aa
 2. \<And>a b. \<lbrakk>nf' \<Longrightarrow> \<forall>s. (\<exists>sa. P sa \<and> (sa, s) \<in> S \<and> P' s) \<longrightarrow> \<not> snd (f' s); \<forall>x\<in>S. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (f' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> S \<and> R r r'); (a, b) \<in> S; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (f' b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>nf' \<Longrightarrow> \<forall>s. (\<exists>sa. P sa \<and> (sa, s) \<in> S \<and> P' s) \<longrightarrow> \<not> snd (f' s); \<forall>x\<in>S. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (f' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> S \<and> R r r'); (a, b) \<in> S; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (f' b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>s. (\<exists>sa. P sa \<and> (sa, s) \<in> S \<and> P' s) \<longrightarrow> \<not> snd (f' s); \<forall>x\<in>S. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (f' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> S \<and> R r r'); (a, b) \<in> S; P a; P' b; nf \<longrightarrow> \<not> snd (f a); nf'; snd (f' b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!