theory ADT_IF_Refine

lemma step_corres_bothE:
  assumes corres: "step_corres nf srel mode invs_abs invs_conc f_abs f_conc"
  assumes preserves: "preserves mode mode' invs_conc 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. (s, e, t) \<in> f_abs
                   \<Longrightarrow> (t, mode') \<in> has_srel_state (lift_fst_rel srel) invs_conc
                   \<Longrightarrow> (t, t') \<in> srel
                   \<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 simp apply clarsimp apply (rule_tac t=t in d,simp+) apply (clarsimp simp: has_srel_state_def lift_fst_rel_def) apply (rule preservesE[OF preserves],assumption+) apply fastforce+ 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. \<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); \<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> (t, mode') \<in> has_srel_state (lift_fst_rel srel) invs_conc
 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> (t, t') \<in> srel 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> \<exists>a. (t, a) \<in> srel \<and> (a, mode') \<in> invs_conc
 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> (t, t') \<in> srel 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; (t', mode') \<in> invs_conc\<rbrakk> \<Longrightarrow> \<exists>a. (t, a) \<in> srel \<and> (a, mode') \<in> invs_conc
 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> (t, t') \<in> srel proof (prove)
goal:
No subgoals!