theory ADT_IF_Refine

lemma step_corres_exE:
  assumes step: "step_corres nf srel mode invs_abs invs_conc f f'"
  assumes nf: "nf"
  assumes invsC: "(s',mode) \<in> invs_conc"
  assumes invsA: "(s,mode) \<in> invs_abs"
  assumes srel: "(s,s') \<in> srel"
  assumes ex: "\<And>e t' t. (s',e,t') \<in> f' \<Longrightarrow> (s,e,t) \<in> f \<Longrightarrow> (t,t') \<in> srel \<Longrightarrow> P"
  shows P apply (insert step invsC invsA srel nf) apply (clarsimp simp: step_corres_def) apply (drule_tac x="(s,s')" in bspec,clarsimp+) apply (drule_tac x=e' in spec) apply (drule_tac x=t' in spec) apply clarsimp apply (rule ex) apply assumption+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step_corres nf srel mode invs_abs invs_conc f f'; (s', mode) \<in> invs_conc; (s, mode) \<in> invs_abs; (s, s') \<in> srel; nf\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>srel. case x of (s, s') \<Rightarrow> (s', mode) \<in> invs_conc \<and> (s, mode) \<in> invs_abs \<longrightarrow> (\<exists>e' t'. (s', e', t') \<in> f') \<and> (\<forall>e' t'. (s', e', t') \<in> f' \<longrightarrow> (\<exists>t. (s, e', t) \<in> f \<and> (t, t') \<in> srel)); (s', mode) \<in> invs_conc; (s, mode) \<in> invs_abs; (s, s') \<in> srel; nf\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>e' t'. \<lbrakk>(s', mode) \<in> invs_conc; (s, mode) \<in> invs_abs; (s, s') \<in> srel; nf; \<forall>e' t'. (s', e', t') \<in> f' \<longrightarrow> (\<exists>t. (s, e', t) \<in> f \<and> (t, t') \<in> srel); (s', e', t') \<in> f'\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>e' t'. \<lbrakk>(s', mode) \<in> invs_conc; (s, mode) \<in> invs_abs; (s, s') \<in> srel; nf; (s', e', t') \<in> f'; \<forall>t'. (s', e', t') \<in> f' \<longrightarrow> (\<exists>t. (s, e', t) \<in> f \<and> (t, t') \<in> srel)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>e' t'. \<lbrakk>(s', mode) \<in> invs_conc; (s, mode) \<in> invs_abs; (s, s') \<in> srel; nf; (s', e', t') \<in> f'; (s', e', t') \<in> f' \<longrightarrow> (\<exists>t. (s, e', t) \<in> f \<and> (t, t') \<in> srel)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>e' t' t. \<lbrakk>(s', mode) \<in> invs_conc; (s, mode) \<in> invs_abs; (s, s') \<in> srel; nf; (s', e', t') \<in> f'; (s, e', t) \<in> f; (t, t') \<in> srel\<rbrakk> \<Longrightarrow> P proof (prove)
goal (3 subgoals):
 1. \<And>e' t' t. \<lbrakk>(s', mode) \<in> invs_conc; (s, mode) \<in> invs_abs; (s, s') \<in> srel; nf; (s', e', t') \<in> f'; (s, e', t) \<in> f; (t, t') \<in> srel\<rbrakk> \<Longrightarrow> (s', ?e27 e' t' t, ?t'27 e' t' t) \<in> f'
 2. \<And>e' t' t. \<lbrakk>(s', mode) \<in> invs_conc; (s, mode) \<in> invs_abs; (s, s') \<in> srel; nf; (s', e', t') \<in> f'; (s, e', t) \<in> f; (t, t') \<in> srel\<rbrakk> \<Longrightarrow> (s, ?e27 e' t' t, ?t27 e' t' t) \<in> f
 3. \<And>e' t' t. \<lbrakk>(s', mode) \<in> invs_conc; (s, mode) \<in> invs_abs; (s, s') \<in> srel; nf; (s', e', t') \<in> f'; (s, e', t) \<in> f; (t, t') \<in> srel\<rbrakk> \<Longrightarrow> (?t27 e' t' t, ?t'27 e' t' t) \<in> srel proof (prove)
goal:
No subgoals!