theory Corres_UL

lemma corres_underlying_decomposition:
  assumes x: "corres_underlying {(s, s'). P s s'} nf nf' r Pr Pr' f g"
      and y: "\<And>s'. \<lbrace>R s'\<rbrace> f \<lbrace>\<lambda>rv s. Q s s'\<rbrace>"
      and z: "\<And>s. \<lbrace>P s and Q s and K (Pr s) and Pr'\<rbrace> g \<lbrace>\<lambda>rv s'. R s' s\<rbrace>"
  shows      "corres_underlying {(s, s'). P s s' \<and> Q s s'} nf nf' r Pr Pr' f g" using x apply (clarsimp simp: corres_underlying_def) apply (elim allE, drule(1) mp, clarsimp) apply (drule(1) bspec) apply clarsimp apply (rule rev_bexI, assumption) apply simp apply (erule use_valid [OF _ y]) apply (erule use_valid [OF _ z]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying {(s, s'). P s s' \<and> Q s s'} nf nf' r Pr Pr' f g proof (prove)
using this:
corres_underlying {(s, s'). P s s'} nf nf' r Pr Pr' f g

goal (1 subgoal):
 1. corres_underlying {(s, s'). P s s' \<and> Q s s'} nf nf' r Pr Pr' f g proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<forall>a b. P a b \<longrightarrow> Pr a \<and> Pr' b \<longrightarrow> (nf \<longrightarrow> \<not> snd (f a)) \<longrightarrow> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> P t t' \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (g b)); P a b; Q a b; Pr a; Pr' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> P t ba \<and> Q t ba \<and> r ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>P a b; Q a b; Pr a; Pr' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); \<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> P t t' \<and> r ra r'; nf' \<longrightarrow> \<not> snd (g b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> P t ba \<and> Q t ba \<and> r ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>P a b; Q a b; Pr a; Pr' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); nf' \<longrightarrow> \<not> snd (g b); case (aa, ba) of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> P t t' \<and> r ra r'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> P t ba \<and> Q t ba \<and> r ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>P a b; Q a b; Pr a; Pr' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); nf' \<longrightarrow> \<not> snd (g b); (ab, bb) \<in> fst (f a); P bb ba; r ab aa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> P t ba \<and> Q t ba \<and> r ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>P a b; Q a b; Pr a; Pr' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); nf' \<longrightarrow> \<not> snd (g b); (ab, bb) \<in> fst (f a); P bb ba; r ab aa\<rbrakk> \<Longrightarrow> case (ab, bb) of (ra, t) \<Rightarrow> P t ba \<and> Q t ba \<and> r ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>P a b; Q a b; Pr a; Pr' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); nf' \<longrightarrow> \<not> snd (g b); (ab, bb) \<in> fst (f a); P bb ba; r ab aa\<rbrakk> \<Longrightarrow> Q bb ba proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>P a b; Q a b; Pr a; Pr' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); nf' \<longrightarrow> \<not> snd (g b); P bb ba; r ab aa\<rbrakk> \<Longrightarrow> R ba a proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>P a b; Q a b; Pr a; Pr' b; nf \<longrightarrow> \<not> snd (f a); nf' \<longrightarrow> \<not> snd (g b); P bb ba; r ab aa\<rbrakk> \<Longrightarrow> (P a and Q a and K (Pr a) and Pr') b proof (prove)
goal:
No subgoals!