theory ADT_IF_Refine

lemma step_corresE:
  assumes corres: "step_corres nf srel mode invs_abs invs_conc f_abs f_conc"
  assumes a: "(s, s') \<in> srel"
  assumes e: "(s, mode) \<in> invs_abs"
  assumes b: "(s', mode) \<in> invs_conc"
  assumes c: "(s', e, t') \<in> f_conc"
  assumes d: "\<And>t. \<lbrakk> (s, e, t) \<in> f_abs; (t, t') \<in> srel \<rbrakk> \<Longrightarrow> P"
  shows "P" apply (insert corres a b c e) 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 d) apply simp+ 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_abs f_conc; (s, s') \<in> srel; (s', mode) \<in> invs_conc; (s', e, t') \<in> f_conc; (s, mode) \<in> invs_abs\<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> (nf \<longrightarrow> (\<exists>e' t'. (s', e', t') \<in> f_conc)) \<and> (\<forall>e' t'. (s', e', t') \<in> f_conc \<longrightarrow> (\<exists>t. (s, e', t) \<in> f_abs \<and> (t, t') \<in> srel)); (s, s') \<in> srel; (s', mode) \<in> invs_conc; (s', e, t') \<in> f_conc; (s, mode) \<in> invs_abs\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> srel; (s', mode) \<in> invs_conc; (s', e, t') \<in> f_conc; (s, mode) \<in> invs_abs; nf \<longrightarrow> (\<exists>e' t'. (s', e', t') \<in> f_conc); \<forall>e' t'. (s', e', t') \<in> f_conc \<longrightarrow> (\<exists>t. (s, e', t) \<in> f_abs \<and> (t, t') \<in> srel)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> srel; (s', mode) \<in> invs_conc; (s', e, t') \<in> f_conc; (s, mode) \<in> invs_abs; nf \<longrightarrow> (\<exists>e' t'. (s', e', t') \<in> f_conc); \<forall>t'. (s', e, t') \<in> f_conc \<longrightarrow> (\<exists>t. (s, e, t) \<in> f_abs \<and> (t, t') \<in> srel)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> srel; (s', mode) \<in> invs_conc; (s', e, t') \<in> f_conc; (s, mode) \<in> invs_abs; nf \<longrightarrow> (\<exists>e' t'. (s', e', t') \<in> f_conc); (s', e, t') \<in> f_conc \<longrightarrow> (\<exists>t. (s, e, t) \<in> f_abs \<and> (t, t') \<in> srel)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>(s, s') \<in> srel; (s', mode) \<in> invs_conc; (s', e, t') \<in> f_conc; (s, mode) \<in> invs_abs; nf \<longrightarrow> (\<exists>e' t'. (s', e', t') \<in> f_conc); (s, e, t) \<in> f_abs; (t, t') \<in> srel\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>(s, s') \<in> srel; (s', mode) \<in> invs_conc; (s', e, t') \<in> f_conc; (s, mode) \<in> invs_abs; nf \<longrightarrow> (\<exists>e' t'. (s', e', t') \<in> f_conc); (s, e, t) \<in> f_abs; (t, t') \<in> srel\<rbrakk> \<Longrightarrow> (s, e, ?t25 t) \<in> f_abs
 2. \<And>t. \<lbrakk>(s, s') \<in> srel; (s', mode) \<in> invs_conc; (s', e, t') \<in> f_conc; (s, mode) \<in> invs_abs; nf \<longrightarrow> (\<exists>e' t'. (s', e', t') \<in> f_conc); (s, e, t) \<in> f_abs; (t, t') \<in> srel\<rbrakk> \<Longrightarrow> (?t25 t, t') \<in> srel proof (prove)
goal:
No subgoals!