theory Corres_UL

lemma corres_noop2:
  assumes x: "\<And>s. P s  \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>"
  assumes y: "\<And>s. P' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>"
  assumes z: "nf' \<Longrightarrow> no_fail P f" "nf' \<Longrightarrow> no_fail P' g"
  shows      "corres_underlying sr nf nf' dc P P' f g" apply (clarsimp simp: corres_underlying_def) apply (rule conjI) apply clarsimp apply (rule use_exs_valid) apply (rule exs_hoare_post_imp) prefer 2 apply (rule x) apply assumption apply simp_all apply (subgoal_tac "ba = b") apply simp apply (rule sym) apply (rule use_valid[OF _ y], assumption+) apply simp apply (insert z) apply (clarsimp simp: no_fail_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' dc P P' f g proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (r, t) \<Rightarrow> (t, t') \<in> sr) \<and> (nf' \<longrightarrow> \<not> snd (g b)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (r, t) \<Rightarrow> (t, t') \<in> sr
 2. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (r, t) \<Rightarrow> (t, ba) \<in> sr
 2. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (g b) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b)\<rbrakk> \<Longrightarrow> \<lbrace>?P36 a b aa ba\<rbrace> f \<exists>\<lbrace>\<lambda>a b. (b, ba) \<in> sr\<rbrace>
 2. \<And>a b aa ba. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b)\<rbrakk> \<Longrightarrow> ?P36 a b aa ba a
 3. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (g b) proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba r s. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); ?Q39 a b aa ba r s\<rbrakk> \<Longrightarrow> (s, ba) \<in> sr
 2. \<And>a b aa ba. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b)\<rbrakk> \<Longrightarrow> \<lbrace>?P36 a b aa ba\<rbrace> f \<exists>\<lbrace>?Q39 a b aa ba\<rbrace>
 3. \<And>a b aa ba. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b)\<rbrakk> \<Longrightarrow> ?P36 a b aa ba a
 4. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (g b) proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b)\<rbrakk> \<Longrightarrow> \<lbrace>?P36 a b aa ba\<rbrace> f \<exists>\<lbrace>?Q39 a b aa ba\<rbrace>
 2. \<And>a b aa ba r s. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); ?Q39 a b aa ba r s\<rbrakk> \<Longrightarrow> (s, ba) \<in> sr
 3. \<And>a b aa ba. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b)\<rbrakk> \<Longrightarrow> ?P36 a b aa ba a
 4. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (g b) proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b)\<rbrakk> \<Longrightarrow> P (?s42 a b aa ba)
 2. \<And>a b aa ba r s. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); ?s42 a b aa ba = s\<rbrakk> \<Longrightarrow> (s, ba) \<in> sr
 3. \<And>a b aa ba. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b)\<rbrakk> \<Longrightarrow> ?s42 a b aa ba = a
 4. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (g b) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba r s. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); a = s\<rbrakk> \<Longrightarrow> (s, ba) \<in> sr
 2. \<And>a b aa ba. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b)\<rbrakk> \<Longrightarrow> a = a
 3. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s. \<lbrakk>(s, b) \<in> sr; P s; P' b; nf \<longrightarrow> \<not> snd (f s); (aa, ba) \<in> fst (g b); a = s\<rbrakk> \<Longrightarrow> (s, ba) \<in> sr
 2. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (g b) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba s. \<lbrakk>(s, b) \<in> sr; P s; P' b; nf \<longrightarrow> \<not> snd (f s); (aa, ba) \<in> fst (g b); a = s; ba = b\<rbrakk> \<Longrightarrow> (s, ba) \<in> sr
 2. \<And>a b aa ba s. \<lbrakk>(s, b) \<in> sr; P s; P' b; nf \<longrightarrow> \<not> snd (f s); (aa, ba) \<in> fst (g b); a = s\<rbrakk> \<Longrightarrow> ba = b
 3. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s. \<lbrakk>(s, b) \<in> sr; P s; P' b; nf \<longrightarrow> \<not> snd (f s); (aa, ba) \<in> fst (g b); a = s\<rbrakk> \<Longrightarrow> ba = b
 2. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s. \<lbrakk>(s, b) \<in> sr; P s; P' b; nf \<longrightarrow> \<not> snd (f s); (aa, ba) \<in> fst (g b); a = s\<rbrakk> \<Longrightarrow> b = ba
 2. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (g b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s. \<lbrakk>(s, b) \<in> sr; P s; P' b; nf \<longrightarrow> \<not> snd (f s); (aa, ba) \<in> fst (g b); a = s\<rbrakk> \<Longrightarrow> b = b
 2. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (g b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (g b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); nf' \<Longrightarrow> no_fail P f; nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (g b) proof (prove)
goal:
No subgoals!