theory ADT_IF

lemma rel_terminate_terminates:
  assumes ss: "serial_system_weak A I"
  assumes rt: "rel_terminate A s0 R I measuref"
  assumes si: "s \<in> I"
  assumes sR: "\<exists>s0'\<in> Init A s0. R\<^sup>*\<^sup>* s0' s"
  shows "\<forall>js. (x,js) \<in> sub_big_steps A R s
              \<longrightarrow> (\<exists>as s' a s''. (s',(js@as)) \<in> sub_big_steps A R s \<and>
                                  (s',s'') \<in> Step A a \<and> R s s'')" proof - show ?thesis apply (induct x rule: wf_induct) apply (rule wf_step_measuref_rel_from[OF rt si sR]) apply clarsimp apply (frule sub_big_steps_I_holds[OF ss[THEN serial_system_weak.I] si]) apply (frule_tac serial_system_weak.serial[OF ss]) apply (erule exE, rename_tac s') apply (drule_tac x=s' in spec) apply (erule impE) apply (fastforce simp: step_measuref_rel_from_def) apply (case_tac "R s s'") apply (rule_tac x="[]" in exI) apply (rule_tac x=x in exI) apply fastforce apply (fastforce intro: sub_big_steps.step) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>js. (x, js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s' a s''. (s', js @ as) \<in> sub_big_steps A R s \<and> (s', s'') \<in> Step A a \<and> R s s'') proof (state)
goal (1 subgoal):
 1. \<forall>js. (x, js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s' a s''. (s', js @ as) \<in> sub_big_steps A R s \<and> (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal (1 subgoal):
 1. \<forall>js. (x, js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s' a s''. (s', js @ as) \<in> sub_big_steps A R s \<and> (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal (2 subgoals):
 1. wf ?r
 2. \<And>x. \<forall>y. (y, x) \<in> ?r \<longrightarrow> (\<forall>js. (y, js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s' a s''. (s', js @ as) \<in> sub_big_steps A R s \<and> (s', s'') \<in> Step A a \<and> R s s'')) \<Longrightarrow> \<forall>js. (x, js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s' a s''. (s', js @ as) \<in> sub_big_steps A R s \<and> (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> step_measuref_rel_from A R s \<longrightarrow> (\<forall>js. (y, js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s' a s''. (s', js @ as) \<in> sub_big_steps A R s \<and> (s', s'') \<in> Step A a \<and> R s s'')) \<Longrightarrow> \<forall>js. (x, js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s' a s''. (s', js @ as) \<in> sub_big_steps A R s \<and> (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal (1 subgoal):
 1. \<And>x js. \<lbrakk>\<forall>y. (y, x) \<in> step_measuref_rel_from A R s \<longrightarrow> (\<forall>js. (y, js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s''))); (x, js) \<in> sub_big_steps A R s\<rbrakk> \<Longrightarrow> \<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal (1 subgoal):
 1. \<And>x js. \<lbrakk>\<forall>y. (y, x) \<in> step_measuref_rel_from A R s \<longrightarrow> (\<forall>js. (y, js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s''))); (x, js) \<in> sub_big_steps A R s; x \<in> I\<rbrakk> \<Longrightarrow> \<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal (1 subgoal):
 1. \<And>x js. \<lbrakk>\<forall>y. (y, x) \<in> step_measuref_rel_from A R s \<longrightarrow> (\<forall>js. (y, js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s''))); (x, js) \<in> sub_big_steps A R s; x \<in> I; \<exists>t. (x, t) \<in> Step A (?a9 x js)\<rbrakk> \<Longrightarrow> \<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal (1 subgoal):
 1. \<And>x js s'. \<lbrakk>\<forall>y. (y, x) \<in> step_measuref_rel_from A R s \<longrightarrow> (\<forall>js. (y, js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s''))); (x, js) \<in> sub_big_steps A R s; x \<in> I; (x, s') \<in> Step A (?a9 x js)\<rbrakk> \<Longrightarrow> \<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal (1 subgoal):
 1. \<And>x js s'. \<lbrakk>(x, js) \<in> sub_big_steps A R s; x \<in> I; (x, s') \<in> Step A (?a9 x js); (s', x) \<in> step_measuref_rel_from A R s \<longrightarrow> (\<forall>js. (s', js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'')))\<rbrakk> \<Longrightarrow> \<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>x js s'. \<lbrakk>(x, js) \<in> sub_big_steps A R s; x \<in> I; (x, s') \<in> Step A (?a9 x js)\<rbrakk> \<Longrightarrow> (s', x) \<in> step_measuref_rel_from A R s
 2. \<And>x js s'. \<lbrakk>(x, js) \<in> sub_big_steps A R s; x \<in> I; (x, s') \<in> Step A (?a9 x js); \<forall>js. (s', js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s''))\<rbrakk> \<Longrightarrow> \<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal (1 subgoal):
 1. \<And>x js s'. \<lbrakk>(x, js) \<in> sub_big_steps A R s; x \<in> I; (x, s') \<in> Step A (?a9 x js); \<forall>js. (s', js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s''))\<rbrakk> \<Longrightarrow> \<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>x js s'. \<lbrakk>(x, js) \<in> sub_big_steps A R s; x \<in> I; (x, s') \<in> Step A (?a9 x js); \<forall>js. (s', js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'')); R s s'\<rbrakk> \<Longrightarrow> \<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'')
 2. \<And>x js s'. \<lbrakk>(x, js) \<in> sub_big_steps A R s; x \<in> I; (x, s') \<in> Step A (?a9 x js); \<forall>js. (s', js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'')); \<not> R s s'\<rbrakk> \<Longrightarrow> \<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>x js s'. \<lbrakk>(x, js) \<in> sub_big_steps A R s; x \<in> I; (x, s') \<in> Step A (?a9 x js); \<forall>js. (s', js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'')); R s s'\<rbrakk> \<Longrightarrow> \<exists>s'. (s', js @ []) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'')
 2. \<And>x js s'. \<lbrakk>(x, js) \<in> sub_big_steps A R s; x \<in> I; (x, s') \<in> Step A (?a9 x js); \<forall>js. (s', js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'')); \<not> R s s'\<rbrakk> \<Longrightarrow> \<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>x js s'. \<lbrakk>(x, js) \<in> sub_big_steps A R s; x \<in> I; (x, s') \<in> Step A (?a9 x js); \<forall>js. (s', js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'')); R s s'\<rbrakk> \<Longrightarrow> (x, js @ []) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (x, s'') \<in> Step A a \<and> R s s'')
 2. \<And>x js s'. \<lbrakk>(x, js) \<in> sub_big_steps A R s; x \<in> I; (x, s') \<in> Step A (?a9 x js); \<forall>js. (s', js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'')); \<not> R s s'\<rbrakk> \<Longrightarrow> \<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal (1 subgoal):
 1. \<And>x js s'. \<lbrakk>(x, js) \<in> sub_big_steps A R s; x \<in> I; (x, s') \<in> Step A (?a9 x js); \<forall>js. (s', js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'')); \<not> R s s'\<rbrakk> \<Longrightarrow> \<exists>as s'. (s', js @ as) \<in> sub_big_steps A R s \<and> (\<exists>a s''. (s', s'') \<in> Step A a \<and> R s s'') proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>js. (x, js) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s' a s''. (s', js @ as) \<in> sub_big_steps A R s \<and> (s', s'') \<in> Step A a \<and> R s s'')

goal:
No subgoals!