theory ADT_IF_Refine

lemma abs_serial:
  assumes constrained_B:
    "\<And>s. s \<in> invs_abs \<inter> extras_abs \<Longrightarrow> \<exists>s'. s' \<in> invs_conc \<and> (s, s') \<in> lift_fst_rel srel"
  assumes uop_sane:
    "\<And>s e t. (s,e,t) \<in> do_user_op_conc \<Longrightarrow> e \<noteq> Some Interrupt"
  assumes no_fail: "nf"
  shows "serial_system (ADT_abs) (invs_abs \<inter> extras_abs)" apply (rule serial_system.fw_sim_serial) apply (rule conc_serial) apply (rule uop_sane,simp) apply (rule no_fail) apply (rule fw_sim_abs_conc) apply (rule invariant_holds_inter) apply (rule abs.ADT_invs) apply (rule abs.ADT_extras) apply clarsimp apply simp apply (frule constrained_B) apply (clarsimp simp: lift_fst_rel_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. serial_system ADT_abs (invs_abs \<inter> extras_abs) proof (prove)
goal (6 subgoals):
 1. serial_system ?A ?I
 2. LI ADT_abs ?A ?R (?I_b \<times> ?I_a)
 3. ADT_abs \<Turnstile> invs_abs \<inter> extras_abs
 4. ?I \<subseteq> ?I_a
 5. invs_abs \<inter> extras_abs \<subseteq> ?I_b
 6. \<And>s. s \<in> invs_abs \<inter> extras_abs \<Longrightarrow> \<exists>s'. s' \<in> ?I \<and> (s, s') \<in> ?R proof (prove)
goal (7 subgoals):
 1. \<And>s e t. (s, e, t) \<in> do_user_op_conc \<Longrightarrow> e \<noteq> Some Interrupt
 2. nf
 3. LI ADT_abs ADT_conc ?R (?I_b \<times> ?I_a)
 4. ADT_abs \<Turnstile> invs_abs \<inter> extras_abs
 5. {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<subseteq> ?I_a
 6. invs_abs \<inter> extras_abs \<subseteq> ?I_b
 7. \<And>s. s \<in> invs_abs \<inter> extras_abs \<Longrightarrow> \<exists>s'. s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<and> (s, s') \<in> ?R proof (prove)
goal (6 subgoals):
 1. nf
 2. LI ADT_abs ADT_conc ?R (?I_b \<times> ?I_a)
 3. ADT_abs \<Turnstile> invs_abs \<inter> extras_abs
 4. {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<subseteq> ?I_a
 5. invs_abs \<inter> extras_abs \<subseteq> ?I_b
 6. \<And>s. s \<in> invs_abs \<inter> extras_abs \<Longrightarrow> \<exists>s'. s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<and> (s, s') \<in> ?R proof (prove)
goal (5 subgoals):
 1. LI ADT_abs ADT_conc ?R (?I_b \<times> ?I_a)
 2. ADT_abs \<Turnstile> invs_abs \<inter> extras_abs
 3. {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<subseteq> ?I_a
 4. invs_abs \<inter> extras_abs \<subseteq> ?I_b
 5. \<And>s. s \<in> invs_abs \<inter> extras_abs \<Longrightarrow> \<exists>s'. s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<and> (s, s') \<in> ?R proof (prove)
goal (4 subgoals):
 1. ADT_abs \<Turnstile> invs_abs \<inter> extras_abs
 2. {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<subseteq> invs_conc
 3. invs_abs \<inter> extras_abs \<subseteq> invs_abs
 4. \<And>s. s \<in> invs_abs \<inter> extras_abs \<Longrightarrow> \<exists>s'. s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<and> (s, s') \<in> lift_fst_rel srel proof (prove)
goal (5 subgoals):
 1. ADT_abs \<Turnstile> invs_abs
 2. ADT_abs \<Turnstile> extras_abs
 3. {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<subseteq> invs_conc
 4. invs_abs \<inter> extras_abs \<subseteq> invs_abs
 5. \<And>s. s \<in> invs_abs \<inter> extras_abs \<Longrightarrow> \<exists>s'. s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<and> (s, s') \<in> lift_fst_rel srel proof (prove)
goal (4 subgoals):
 1. ADT_abs \<Turnstile> extras_abs
 2. {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<subseteq> invs_conc
 3. invs_abs \<inter> extras_abs \<subseteq> invs_abs
 4. \<And>s. s \<in> invs_abs \<inter> extras_abs \<Longrightarrow> \<exists>s'. s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<and> (s, s') \<in> lift_fst_rel srel proof (prove)
goal (3 subgoals):
 1. {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<subseteq> invs_conc
 2. invs_abs \<inter> extras_abs \<subseteq> invs_abs
 3. \<And>s. s \<in> invs_abs \<inter> extras_abs \<Longrightarrow> \<exists>s'. s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<and> (s, s') \<in> lift_fst_rel srel proof (prove)
goal (2 subgoals):
 1. invs_abs \<inter> extras_abs \<subseteq> invs_abs
 2. \<And>s. s \<in> invs_abs \<inter> extras_abs \<Longrightarrow> \<exists>s'. s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<and> (s, s') \<in> lift_fst_rel srel proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> invs_abs \<inter> extras_abs \<Longrightarrow> \<exists>s'. s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<and> (s, s') \<in> lift_fst_rel srel proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> invs_abs \<inter> extras_abs; \<exists>s'. s' \<in> invs_conc \<and> (s, s') \<in> lift_fst_rel srel\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> {s'. \<exists>s. (s, s') \<in> lift_fst_rel srel \<and> s \<in> invs_abs \<and> s' \<in> invs_conc} \<and> (s, s') \<in> lift_fst_rel srel proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bb. \<lbrakk>((a, b), ba) \<in> invs_abs; ((a, b), ba) \<in> extras_abs; ((aa, bb), ba) \<in> invs_conc; ((a, b), aa, bb) \<in> srel\<rbrakk> \<Longrightarrow> \<exists>aa bb. (\<exists>a b. ((a, b), aa, bb) \<in> srel \<and> ((a, b), ba) \<in> invs_abs \<and> ((aa, bb), ba) \<in> invs_conc) \<and> ((a, b), aa, bb) \<in> srel proof (prove)
goal:
No subgoals!