theory ADT_IF

lemma fw_sim_serial:
  assumes refines: "LI B A R (I_b \<times> I_a)"
  assumes B_I_b: "B \<Turnstile> I_b'"
  assumes A_I_as: "I \<subseteq> I_a"
  assumes B_I_bs': "I_b' \<subseteq> I_b"
  assumes constrained_B: "\<And>s. s \<in> I_b' \<Longrightarrow> \<exists>s'. s' \<in> I \<and> (s,s') \<in> R"
  shows "serial_system B I_b'" apply unfold_locales apply (rule B_I_b) apply (insert refines) apply (clarsimp simp: LI_def) apply (drule_tac x=a in spec) apply (frule_tac s=s' in constrained_B) apply clarsimp apply (frule_tac a=a in serial) apply (clarsimp simp: rel_semi_def) apply (cut_tac B_I_bs' A_I_as) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. serial_system B I_b' proof (prove)
goal (2 subgoals):
 1. B \<Turnstile> I_b'
 2. \<And>s' a. s' \<in> I_b' \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step B a proof (prove)
goal (1 subgoal):
 1. \<And>s' a. s' \<in> I_b' \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step B a proof (prove)
goal (1 subgoal):
 1. \<And>s' a. \<lbrakk>s' \<in> I_b'; LI B A R (I_b \<times> I_a)\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step B a proof (prove)
goal (1 subgoal):
 1. \<And>s' a. \<lbrakk>s' \<in> I_b'; \<forall>s. Init A s \<subseteq> R `` Init B s; \<forall>j. R \<inter> I_b \<times> I_a ;;; data_type.Step A j \<subseteq> data_type.Step B j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I_b \<and> s' \<in> I_a \<longrightarrow> Fin A s' = Fin B s\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step B a proof (prove)
goal (1 subgoal):
 1. \<And>s' a. \<lbrakk>s' \<in> I_b'; \<forall>s. Init A s \<subseteq> R `` Init B s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I_b \<and> s' \<in> I_a \<longrightarrow> Fin A s' = Fin B s; R \<inter> I_b \<times> I_a ;;; data_type.Step A a \<subseteq> data_type.Step B a ;;; R\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step B a proof (prove)
goal (1 subgoal):
 1. \<And>s' a. \<lbrakk>s' \<in> I_b'; \<forall>s. Init A s \<subseteq> R `` Init B s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I_b \<and> s' \<in> I_a \<longrightarrow> Fin A s' = Fin B s; R \<inter> I_b \<times> I_a ;;; data_type.Step A a \<subseteq> data_type.Step B a ;;; R; \<exists>s'a. s'a \<in> I \<and> (s', s'a) \<in> R\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step B a proof (prove)
goal (1 subgoal):
 1. \<And>s' a s'a. \<lbrakk>s' \<in> I_b'; \<forall>s. Init A s \<subseteq> R `` Init B s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I_b \<and> s' \<in> I_a \<longrightarrow> Fin A s' = Fin B s; R \<inter> I_b \<times> I_a ;;; data_type.Step A a \<subseteq> data_type.Step B a ;;; R; s'a \<in> I; (s', s'a) \<in> R\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step B a proof (prove)
goal (1 subgoal):
 1. \<And>s' a s'a. \<lbrakk>s' \<in> I_b'; \<forall>s. Init A s \<subseteq> R `` Init B s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I_b \<and> s' \<in> I_a \<longrightarrow> Fin A s' = Fin B s; R \<inter> I_b \<times> I_a ;;; data_type.Step A a \<subseteq> data_type.Step B a ;;; R; s'a \<in> I; (s', s'a) \<in> R; \<exists>t. (s'a, t) \<in> data_type.Step A a\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step B a proof (prove)
goal (1 subgoal):
 1. \<And>s' a s'a t. \<lbrakk>s' \<in> I_b'; \<forall>s. Init A s \<subseteq> R `` Init B s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I_b \<and> s' \<in> I_a \<longrightarrow> Fin A s' = Fin B s; (R \<inter> I_b \<times> I_a) O data_type.Step A a \<subseteq> data_type.Step B a O R; s'a \<in> I; (s', s'a) \<in> R; (s'a, t) \<in> data_type.Step A a\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step B a proof (prove)
goal (1 subgoal):
 1. \<And>s' a s'a t. \<lbrakk>s' \<in> I_b'; \<forall>s. Init A s \<subseteq> R `` Init B s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I_b \<and> s' \<in> I_a \<longrightarrow> Fin A s' = Fin B s; (R \<inter> I_b \<times> I_a) O data_type.Step A a \<subseteq> data_type.Step B a O R; s'a \<in> I; (s', s'a) \<in> R; (s'a, t) \<in> data_type.Step A a; I_b' \<subseteq> I_b; I \<subseteq> I_a\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step B a proof (prove)
goal:
No subgoals!