theory ADT_IF

lemma big_step_adt_Init_Fin_serial_weak:
  assumes single_event: "\<forall>(x::'b) (y::'b). x = y"
  assumes nrefl: "\<And>s. \<not> R s s"
  assumes ifsw: "Init_Fin_serial_weak A s0 I"
  assumes rt: "rel_terminate A s0 R I measuref"
  assumes J_def: "J = inv_from_rel A s0 R \<inter> I"
  shows "Init_Fin_serial_weak (big_step_adt A R (exmap::('a list \<Rightarrow> 'b))) s0 J" using ifsw apply (unfold_locales) apply (simp add: J_def) apply (rule inv_holds_conjI) apply (rule big_step_adt_R_tranclp_inv) apply (rule big_step_adt_inv_holds) apply (simp add: Init_Fin_serial_weak_def serial_system_weak.I) apply (simp add: big_step_adt_def J_def inv_from_rel_def) apply (elim conjE exE) apply (cut_tac s=s' and I=I and exmap=exmap in big_steps_enabled) apply (force simp: Init_Fin_serial_weak_def) apply (rule rt) apply assumption apply (simp add: nrefl) apply simp apply clarsimp apply (cut_tac x=x and xa=a in single_event[rule_format]) apply blast apply (simp add: J_def big_step_adt_def Init_Fin_serial_weak.Init_Fin) apply (simp add: big_step_adt_def Init_Fin_serial_weak.s0_I J_def inv_from_rel_def, force) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Init_Fin_serial_weak (big_step_adt A R exmap) s0 J proof (prove)
using this:
Init_Fin_serial_weak A s0 I

goal (1 subgoal):
 1. Init_Fin_serial_weak (big_step_adt A R exmap) s0 J proof (prove)
goal (4 subgoals):
 1. Init_Fin_serial_weak A s0 I \<Longrightarrow> big_step_adt A R exmap [> J
 2. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> Step (big_step_adt A R exmap) a
 3. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 4. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (4 subgoals):
 1. Init_Fin_serial_weak A s0 I \<Longrightarrow> big_step_adt A R exmap [> inv_from_rel A s0 R \<inter> I
 2. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> Step (big_step_adt A R exmap) a
 3. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 4. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (5 subgoals):
 1. Init_Fin_serial_weak A s0 I \<Longrightarrow> big_step_adt A R exmap [> inv_from_rel A s0 R
 2. Init_Fin_serial_weak A s0 I \<Longrightarrow> big_step_adt A R exmap [> I
 3. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> Step (big_step_adt A R exmap) a
 4. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 5. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (4 subgoals):
 1. Init_Fin_serial_weak A s0 I \<Longrightarrow> big_step_adt A R exmap [> I
 2. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> Step (big_step_adt A R exmap) a
 3. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 4. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (4 subgoals):
 1. Init_Fin_serial_weak A s0 I \<Longrightarrow> A [> I
 2. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> Step (big_step_adt A R exmap) a
 3. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 4. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (3 subgoals):
 1. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> Step (big_step_adt A R exmap) a
 2. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 3. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (3 subgoals):
 1. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; (\<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s') \<and> s' \<in> I\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> big_steps A R exmap a
 2. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 3. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (3 subgoals):
 1. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> big_steps A R exmap a
 2. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 3. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (8 subgoals):
 1. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> serial_system_weak (?A11 s' a) I
 2. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> rel_terminate (?A11 s' a) (?s0.11 s' a) (?R11 s' a) I (?measuref11 s' a)
 3. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> s' \<in> I
 4. \<And>s' a s. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> \<not> ?R11 s' a s s
 5. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init (?A11 s' a) (?s0.11 s' a). (?R11 s' a)\<^sup>*\<^sup>* s0' s'
 6. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I; \<exists>x s'a. (s', s'a) \<in> big_steps (?A11 s' a) (?R11 s' a) exmap x\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> big_steps A R exmap a
 7. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 8. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (7 subgoals):
 1. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> rel_terminate A (?s0.11 s' a) (?R11 s' a) I (?measuref11 s' a)
 2. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> s' \<in> I
 3. \<And>s' a s. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> \<not> ?R11 s' a s s
 4. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init A (?s0.11 s' a). (?R11 s' a)\<^sup>*\<^sup>* s0' s'
 5. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I; \<exists>x s'a. (s', s'a) \<in> big_steps A (?R11 s' a) exmap x\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> big_steps A R exmap a
 6. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 7. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (6 subgoals):
 1. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> s' \<in> I
 2. \<And>s' a s. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> \<not> R s s
 3. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'
 4. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I; \<exists>x s'a. (s', s'a) \<in> big_steps A R exmap x\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> big_steps A R exmap a
 5. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 6. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (5 subgoals):
 1. \<And>s' a s. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> \<not> R s s
 2. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'
 3. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I; \<exists>x s'a. (s', s'a) \<in> big_steps A R exmap x\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> big_steps A R exmap a
 4. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 5. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (4 subgoals):
 1. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'
 2. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I; \<exists>x s'a. (s', s'a) \<in> big_steps A R exmap x\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> big_steps A R exmap a
 3. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 4. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (3 subgoals):
 1. \<And>s' a. \<lbrakk>Init_Fin_serial_weak A s0 I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s'; s' \<in> I; \<exists>x s'a. (s', s'a) \<in> big_steps A R exmap x\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> big_steps A R exmap a
 2. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 3. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (3 subgoals):
 1. \<And>s' a s0' x s'a. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> I; s0' \<in> Init A s0; R\<^sup>*\<^sup>* s0' s'; (s', s'a) \<in> big_steps A R exmap x\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> big_steps A R exmap a
 2. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 3. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (3 subgoals):
 1. \<And>s' a s0' x s'a. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> I; s0' \<in> Init A s0; R\<^sup>*\<^sup>* s0' s'; (s', s'a) \<in> big_steps A R exmap x; x = a\<rbrakk> \<Longrightarrow> \<exists>t. (s', t) \<in> big_steps A R exmap a
 2. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 3. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>Init_Fin_serial_weak A s0 I; s' \<in> J\<rbrakk> \<Longrightarrow> s' \<in> Init (big_step_adt A R exmap) (Fin (big_step_adt A R exmap) s')
 2. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal (1 subgoal):
 1. Init_Fin_serial_weak A s0 I \<Longrightarrow> Init (big_step_adt A R exmap) s0 \<subseteq> J proof (prove)
goal:
No subgoals!