kings-crown/FVELER_Isabelle huggingface dataset:
theory ADT_IF

lemma rtranclp_def2:
  "(R\<^sup>*\<^sup>* s0 s) = (R\<^sup>+\<^sup>+ s0 s \<or> s = s0)" apply safe apply (drule rtranclpD) apply simp apply (erule tranclp_into_rtranclp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R\<^sup>*\<^sup>* s0 s = (R\<^sup>+\<^sup>+ s0 s \<or> s = s0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>R\<^sup>*\<^sup>* s0 s; s \<noteq> s0\<rbrakk> \<Longrightarrow> R\<^sup>+\<^sup>+ s0 s
 2. R\<^sup>+\<^sup>+ s0 s \<Longrightarrow> R\<^sup>*\<^sup>* s0 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s \<noteq> s0; s0 = s \<or> s0 \<noteq> s \<and> R\<^sup>+\<^sup>+ s0 s\<rbrakk> \<Longrightarrow> R\<^sup>+\<^sup>+ s0 s
 2. R\<^sup>+\<^sup>+ s0 s \<Longrightarrow> R\<^sup>*\<^sup>* s0 s proof (prove)
goal (1 subgoal):
 1. R\<^sup>+\<^sup>+ s0 s \<Longrightarrow> R\<^sup>*\<^sup>* s0 s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma rel_terminateE:
  assumes a: "rel_terminate A s0 R I measuref"
  assumes b:
    "\<lbrakk> (\<And>s s' as s'' a. \<lbrakk> s \<in> I; \<exists>s0'\<in> Init A s0. R\<^sup>*\<^sup>* s0' s; (s',as) \<in> sub_big_steps A R s;
                          (s',s'') \<in> Step A a; measuref s s' > 0; measuref s s'' = 0 \<rbrakk>
                          \<Longrightarrow> R s s'');
       (\<And>s s' as s'' a. \<lbrakk> s \<in> I; \<exists>s0'\<in> Init A s0. R\<^sup>*\<^sup>* s0' s;
                          (s',as) \<in> sub_big_steps A R s; (s',s'') \<in> Step A a \<rbrakk>
                          \<Longrightarrow> measuref s s'' < measuref s s') \<rbrakk>
       \<Longrightarrow> C"
 shows "C" using a b by (fastforce simp: rel_terminate_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. C proof (prove)
using this:
rel_terminate A s0 R I measuref
\<lbrakk>\<And>s s' as s'' a. \<lbrakk>s \<in> I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s; (s', as) \<in> sub_big_steps A R s; (s', s'') \<in> Step A a; 0 < measuref s s'; measuref s s'' = 0\<rbrakk> \<Longrightarrow> R s s''; \<And>s s' as s'' a. \<lbrakk>s \<in> I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s; (s', as) \<in> sub_big_steps A R s; (s', s'') \<in> Step A a\<rbrakk> \<Longrightarrow> measuref s s'' < measuref s s'\<rbrakk> \<Longrightarrow> C

goal (1 subgoal):
 1. C
theory ADT_IF

lemma Run_big_steps_tranclp:
  "(s0, s) \<in> Run (big_steps C R exmap) js \<Longrightarrow> R\<^sup>*\<^sup>* s0 s" apply (induct js arbitrary: s rule: rev_induct) apply simp apply (fastforce dest: Run_mid elim: big_steps.cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s0, s) \<in> Run (big_steps C R exmap) js \<Longrightarrow> R\<^sup>*\<^sup>* s0 s proof (prove)
goal (2 subgoals):
 1. \<And>s. (s0, s) \<in> Run (big_steps C R exmap) [] \<Longrightarrow> R\<^sup>*\<^sup>* s0 s
 2. \<And>x xs s. \<lbrakk>\<And>s. (s0, s) \<in> Run (big_steps C R exmap) xs \<Longrightarrow> R\<^sup>*\<^sup>* s0 s; (s0, s) \<in> Run (big_steps C R exmap) (xs @ [x])\<rbrakk> \<Longrightarrow> R\<^sup>*\<^sup>* s0 s proof (prove)
goal (1 subgoal):
 1. \<And>x xs s. \<lbrakk>\<And>s. (s0, s) \<in> Run (big_steps C R exmap) xs \<Longrightarrow> R\<^sup>*\<^sup>* s0 s; (s0, s) \<in> Run (big_steps C R exmap) (xs @ [x])\<rbrakk> \<Longrightarrow> R\<^sup>*\<^sup>* s0 s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma Step_system_reachable:
  "\<lbrakk> Step_system A s0; system.reachable A s0 s \<rbrakk>
     \<Longrightarrow> Step_system A s" apply (subst Step_system_def) apply (rule conjI) apply (fastforce simp: system.reachable_def Step_system.execution_Run intro: exI[where x="[]"]) apply clarsimp apply (frule Step_system_reachable_trans, assumption+) apply (simp add: Step_system.execution_Run) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Step_system A s0; system.reachable A s0 s\<rbrakk> \<Longrightarrow> Step_system A s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Step_system A s0; system.reachable A s0 s\<rbrakk> \<Longrightarrow> system.reachable A s s \<and> (\<forall>sa as. system.reachable A s sa \<longrightarrow> execution A sa as = {s'. (sa, s') \<in> Run (system.Step A) as}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Step_system A s0; system.reachable A s0 s\<rbrakk> \<Longrightarrow> system.reachable A s s
 2. \<lbrakk>Step_system A s0; system.reachable A s0 s\<rbrakk> \<Longrightarrow> \<forall>sa as. system.reachable A s sa \<longrightarrow> execution A sa as = {s'. (sa, s') \<in> Run (system.Step A) as} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Step_system A s0; system.reachable A s0 s\<rbrakk> \<Longrightarrow> \<forall>sa as. system.reachable A s sa \<longrightarrow> execution A sa as = {s'. (sa, s') \<in> Run (system.Step A) as} proof (prove)
goal (1 subgoal):
 1. \<And>sa as. \<lbrakk>Step_system A s0; system.reachable A s0 s; system.reachable A s sa\<rbrakk> \<Longrightarrow> execution A sa as = {s'. (sa, s') \<in> Run (system.Step A) as} proof (prove)
goal (1 subgoal):
 1. \<And>sa as. \<lbrakk>Step_system A s0; system.reachable A s0 s; system.reachable A s sa; system.reachable A s0 sa\<rbrakk> \<Longrightarrow> execution A sa as = {s'. (sa, s') \<in> Run (system.Step A) as} proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma Step_system_execution_Run_s0:
  "Step_system A s0 \<Longrightarrow> execution A s0 as = {s'. (s0,s') \<in> Run (system.Step A) as}" apply (rule Step_system.execution_Run, assumption) apply (erule Step_system.reachable_s0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Step_system A s0 \<Longrightarrow> execution A s0 as = {s'. (s0, s') \<in> Run (system.Step A) as} proof (prove)
goal (1 subgoal):
 1. Step_system A s0 \<Longrightarrow> system.reachable A s0 s0 proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma wf_step_measuref_rel_from:
  "\<lbrakk> rel_terminate A s0 R I measuref; s \<in> I; \<exists>s0'\<in> Init A s0. R\<^sup>*\<^sup>* s0' s \<rbrakk>
     \<Longrightarrow> wf (step_measuref_rel_from A R s)" apply (cut_tac wf_measure[where f="measuref s"]) apply (erule wf_subset) apply (fastforce simp: measure_def inv_image_def step_measuref_rel_from_def rel_terminate_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel_terminate A s0 R I measuref; s \<in> I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s\<rbrakk> \<Longrightarrow> wf (step_measuref_rel_from A R s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel_terminate A s0 R I measuref; s \<in> I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s; wf (measure (measuref s))\<rbrakk> \<Longrightarrow> wf (step_measuref_rel_from A R s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel_terminate A s0 R I measuref; s \<in> I; \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s\<rbrakk> \<Longrightarrow> step_measuref_rel_from A R s \<subseteq> measure (measuref s) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma inv_holdsI:
  "(\<forall>j. Step D j `` I \<subseteq> I) \<Longrightarrow> D [> I" by (simp add: inv_holds_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>j. Step D j `` I \<subseteq> I \<Longrightarrow> D [> I
theory ADT_IF

lemma inv_holds_conjI:
  "\<lbrakk> D [> P; D [> Q \<rbrakk> \<Longrightarrow> D [> P \<inter> Q" by (simp add: inv_holds_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D [> P; D [> Q\<rbrakk> \<Longrightarrow> D [> P \<inter> Q
theory ADT_IF

lemma step_serial:
  assumes nonempty_start: "B \<noteq> {}"
  assumes invariant_start: "B \<subseteq> I"
  shows "steps (Simulation.Step A) B as \<noteq> {}" apply (induct as rule: rev_induct) apply (simp add: steps_def nonempty_start) apply (erule nonemptyE) apply (frule set_mp[OF inv_holds_steps[OF I invariant_start]]) apply (frule_tac a=x in serial) apply (elim exE) apply (rule_tac x=t in notemptyI) apply (fastforce simp: steps_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. steps (data_type.Step A) B as \<noteq> {} proof (prove)
goal (2 subgoals):
 1. steps (data_type.Step A) B [] \<noteq> {}
 2. \<And>x xs. steps (data_type.Step A) B xs \<noteq> {} \<Longrightarrow> steps (data_type.Step A) B (xs @ [x]) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x xs. steps (data_type.Step A) B xs \<noteq> {} \<Longrightarrow> steps (data_type.Step A) B (xs @ [x]) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa. xa \<in> steps (data_type.Step A) B xs \<Longrightarrow> steps (data_type.Step A) B (xs @ [x]) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>xa \<in> steps (data_type.Step A) B xs; xa \<in> I\<rbrakk> \<Longrightarrow> steps (data_type.Step A) B (xs @ [x]) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>xa \<in> steps (data_type.Step A) B xs; xa \<in> I; \<exists>t. (xa, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> steps (data_type.Step A) B (xs @ [x]) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa t. \<lbrakk>xa \<in> steps (data_type.Step A) B xs; xa \<in> I; (xa, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> steps (data_type.Step A) B (xs @ [x]) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa t. \<lbrakk>xa \<in> steps (data_type.Step A) B xs; xa \<in> I; (xa, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> t \<in> steps (data_type.Step A) B (xs @ [x]) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma sub_big_steps_nrefl:
  "(\<And>s. \<not> R s s) \<Longrightarrow> (s,[]) \<in> sub_big_steps A R s" by (blast intro: nil)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<not> R s s) \<Longrightarrow> (s, []) \<in> sub_big_steps A R s
theory ADT_IF

lemma big_steps_enabled:
  assumes ss: "serial_system_weak A I"
  assumes rt: "rel_terminate A s0 R I measuref"
  assumes s_I: "s \<in> I"
  assumes nrefl: "\<And>s. \<not> R s s"
  shows "\<exists>s0'\<in> Init A s0. R\<^sup>*\<^sup>* s0' s \<Longrightarrow> \<exists>x s'. (s, s') \<in> big_steps A R exmap x" apply (frule rel_terminate_terminates[OF ss rt s_I]) apply (drule_tac x="[]" in spec) apply (erule impE[OF _ sub_big_steps_nrefl]) apply (rule nrefl) apply (fastforce intro: cstep) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s \<Longrightarrow> \<exists>x s'. (s, s') \<in> big_steps A R exmap x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s; \<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'')\<rbrakk> \<Longrightarrow> \<exists>x s'. (s, s') \<in> big_steps A R exmap x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s; (?x, []) \<in> sub_big_steps A R s \<longrightarrow> (\<exists>as s' a s''. (s', [] @ as) \<in> sub_big_steps A R s \<and> (s', s'') \<in> Step A a \<and> R s s'')\<rbrakk> \<Longrightarrow> \<exists>x s'. (s, s') \<in> big_steps A R exmap x proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s \<Longrightarrow> \<not> R sa sa
 2. \<lbrakk>\<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s; \<exists>as s' a s''. (s', [] @ as) \<in> sub_big_steps A R s \<and> (s', s'') \<in> Step A a \<and> R s s''\<rbrakk> \<Longrightarrow> \<exists>x s'. (s, s') \<in> big_steps A R exmap x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>s0'\<in>Init A s0. R\<^sup>*\<^sup>* s0' s; \<exists>as s' a s''. (s', [] @ as) \<in> sub_big_steps A R s \<and> (s', s'') \<in> Step A a \<and> R s s''\<rbrakk> \<Longrightarrow> \<exists>x s'. (s, s') \<in> big_steps A R exmap x proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma steps_subset:
  "A \<subseteq> B \<Longrightarrow> steps steps1 A as \<subseteq> steps steps1 B as" apply (simp add: steps_def Image_def) apply (induct as rule: rev_induct) apply simp apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B \<Longrightarrow> steps steps1 A as \<subseteq> steps steps1 B as proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B \<Longrightarrow> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> steps1 j}) A as \<subseteq> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> steps1 j}) B as proof (prove)
goal (2 subgoals):
 1. A \<subseteq> B \<Longrightarrow> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> steps1 j}) A [] \<subseteq> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> steps1 j}) B []
 2. \<And>x xs. \<lbrakk>A \<subseteq> B \<Longrightarrow> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> steps1 j}) A xs \<subseteq> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> steps1 j}) B xs; A \<subseteq> B\<rbrakk> \<Longrightarrow> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> steps1 j}) A (xs @ [x]) \<subseteq> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> steps1 j}) B (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>A \<subseteq> B \<Longrightarrow> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> steps1 j}) A xs \<subseteq> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> steps1 j}) B xs; A \<subseteq> B\<rbrakk> \<Longrightarrow> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> steps1 j}) A (xs @ [x]) \<subseteq> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> steps1 j}) B (xs @ [x]) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma step_serial:
  assumes nonempty_start: "B \<noteq> {}"
  assumes invariant_start: "B \<subseteq> I"
  shows "steps (Simulation.Step A) B as \<noteq> {}" apply (induct as rule: rev_induct) apply (simp add: steps_def nonempty_start) apply (erule nonemptyE) apply (frule set_mp[OF invariant_holds_steps[OF I invariant_start]]) apply (frule_tac a=x in serial) apply (elim exE) apply (rule_tac x=t in notemptyI) apply (fastforce simp: steps_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. steps (data_type.Step A) B as \<noteq> {} proof (prove)
goal (2 subgoals):
 1. steps (data_type.Step A) B [] \<noteq> {}
 2. \<And>x xs. steps (data_type.Step A) B xs \<noteq> {} \<Longrightarrow> steps (data_type.Step A) B (xs @ [x]) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x xs. steps (data_type.Step A) B xs \<noteq> {} \<Longrightarrow> steps (data_type.Step A) B (xs @ [x]) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa. xa \<in> steps (data_type.Step A) B xs \<Longrightarrow> steps (data_type.Step A) B (xs @ [x]) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>xa \<in> steps (data_type.Step A) B xs; xa \<in> I\<rbrakk> \<Longrightarrow> steps (data_type.Step A) B (xs @ [x]) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>xa \<in> steps (data_type.Step A) B xs; xa \<in> I; \<exists>t. (xa, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> steps (data_type.Step A) B (xs @ [x]) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa t. \<lbrakk>xa \<in> steps (data_type.Step A) B xs; xa \<in> I; (xa, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> steps (data_type.Step A) B (xs @ [x]) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa t. \<lbrakk>xa \<in> steps (data_type.Step A) B xs; xa \<in> I; (xa, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> t \<in> steps (data_type.Step A) B (xs @ [x]) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma (in Init_Fin_serial) serial_to_weak:
  "Init_Fin_serial_weak A s0 I" by intro_locales

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Init_Fin_serial_weak A s0 I
theory ADT_IF

lemma big_step_adt_R_tranclp_inv:
  "big_step_adt C R exmap [> inv_from_rel C s0 R" apply (rule inv_holdsI) apply (clarsimp simp: big_step_adt_def inv_from_rel_def Fin_trancl_def) apply (rule_tac x="s0'" in bexI) apply (force elim: big_steps.cases) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. big_step_adt C R exmap [> inv_from_rel C s0 R proof (prove)
goal (1 subgoal):
 1. \<forall>j. Step (big_step_adt C R exmap) j `` inv_from_rel C s0 R \<subseteq> inv_from_rel C s0 R proof (prove)
goal (1 subgoal):
 1. \<And>j x xa s0'. \<lbrakk>(xa, x) \<in> big_steps C R exmap j; s0' \<in> Init C s0; R\<^sup>*\<^sup>* s0' xa\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init C s0. R\<^sup>*\<^sup>* s0' x proof (prove)
goal (2 subgoals):
 1. \<And>j x xa s0'. \<lbrakk>(xa, x) \<in> big_steps C R exmap j; s0' \<in> Init C s0; R\<^sup>*\<^sup>* s0' xa\<rbrakk> \<Longrightarrow> R\<^sup>*\<^sup>* s0' x
 2. \<And>j x xa s0'. \<lbrakk>(xa, x) \<in> big_steps C R exmap j; s0' \<in> Init C s0; R\<^sup>*\<^sup>* s0' xa\<rbrakk> \<Longrightarrow> s0' \<in> Init C s0 proof (prove)
goal (1 subgoal):
 1. \<And>j x xa s0'. \<lbrakk>(xa, x) \<in> big_steps C R exmap j; s0' \<in> Init C s0; R\<^sup>*\<^sup>* s0' xa\<rbrakk> \<Longrightarrow> s0' \<in> Init C s0 proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma  big_steps_I_holds:
  "\<lbrakk> (xa, x) \<in> big_steps A R exmap j; xa \<in> I; A [> I \<rbrakk>
     \<Longrightarrow> x \<in> I" apply (erule big_stepsE) apply (frule sub_big_steps_I_holds, assumption+) apply (simp add: inv_holds_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(xa, x) \<in> big_steps A R exmap j; xa \<in> I; A [> I\<rbrakk> \<Longrightarrow> x \<in> I proof (prove)
goal (1 subgoal):
 1. \<And>s' as a. \<lbrakk>xa \<in> I; A [> I; (s', as) \<in> sub_big_steps A R xa; (s', x) \<in> Step A a; R xa x; j = exmap (as @ [a])\<rbrakk> \<Longrightarrow> x \<in> I proof (prove)
goal (1 subgoal):
 1. \<And>s' as a. \<lbrakk>xa \<in> I; A [> I; (s', as) \<in> sub_big_steps A R xa; (s', x) \<in> Step A a; R xa x; j = exmap (as @ [a]); s' \<in> I\<rbrakk> \<Longrightarrow> x \<in> I proof (prove)
goal (1 subgoal):
 1. \<And>s' as a. \<lbrakk>xa \<in> I; \<forall>j. Step A j `` I \<subseteq> I; (s', as) \<in> sub_big_steps A R xa; (s', x) \<in> Step A a; R xa x; j = exmap (as @ [a]); s' \<in> I\<rbrakk> \<Longrightarrow> x \<in> I proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma big_step_adt_inv_holds:
  "A [> I \<Longrightarrow> big_step_adt A R exmap [> I" apply (simp add: big_step_adt_def inv_holds_def) apply clarsimp apply (rule big_steps_I_holds, assumption+) apply (simp add: inv_holds_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A [> I \<Longrightarrow> big_step_adt A R exmap [> I proof (prove)
goal (1 subgoal):
 1. \<forall>j. Step A j `` I \<subseteq> I \<Longrightarrow> \<forall>j. big_steps A R exmap j `` I \<subseteq> I proof (prove)
goal (1 subgoal):
 1. \<And>j x xa. \<lbrakk>\<forall>j. Step A j `` I \<subseteq> I; (xa, x) \<in> big_steps A R exmap j; xa \<in> I\<rbrakk> \<Longrightarrow> x \<in> I proof (prove)
goal (1 subgoal):
 1. \<And>j x xa. \<lbrakk>\<forall>j. Step A j `` I \<subseteq> I; (xa, x) \<in> big_steps A R exmap j; xa \<in> I\<rbrakk> \<Longrightarrow> A [> I proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma sub_big_steps_Run:
  "(t,evlist) \<in> sub_big_steps A R s \<Longrightarrow> (s, t) \<in> Run (Step A) evlist \<and> \<not> R s t" apply (induct t evlist rule: sub_big_steps.induct) apply simp apply clarsimp apply (rule Run_trans) apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (t, evlist) \<in> sub_big_steps A R s \<Longrightarrow> (s, t) \<in> Run (Step A) evlist \<and> \<not> R s t proof (prove)
goal (2 subgoals):
 1. \<And>evlist t. \<lbrakk>evlist = []; t = s; \<not> R s s\<rbrakk> \<Longrightarrow> (s, t) \<in> Run (Step A) evlist \<and> \<not> R s t
 2. \<And>evlist evlist' e s' t. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps A R s; (s, s') \<in> Run (Step A) evlist' \<and> \<not> R s s'; (s', t) \<in> Step A e; \<not> R s t\<rbrakk> \<Longrightarrow> (s, t) \<in> Run (Step A) evlist \<and> \<not> R s t proof (prove)
goal (1 subgoal):
 1. \<And>evlist evlist' e s' t. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps A R s; (s, s') \<in> Run (Step A) evlist' \<and> \<not> R s s'; (s', t) \<in> Step A e; \<not> R s t\<rbrakk> \<Longrightarrow> (s, t) \<in> Run (Step A) evlist \<and> \<not> R s t proof (prove)
goal (1 subgoal):
 1. \<And>evlist' e s' t. \<lbrakk>(s', evlist') \<in> sub_big_steps A R s; (s', t) \<in> Step A e; \<not> R s t; (s, s') \<in> Run (Step A) evlist'; \<not> R s s'\<rbrakk> \<Longrightarrow> (s, t) \<in> Run (Step A) (evlist' @ [e]) proof (prove)
goal (2 subgoals):
 1. \<And>evlist' e s' t. \<lbrakk>(s', evlist') \<in> sub_big_steps A R s; (s', t) \<in> Step A e; \<not> R s t; (s, s') \<in> Run (Step A) evlist'; \<not> R s s'\<rbrakk> \<Longrightarrow> (s, ?t4 evlist' e s' t) \<in> Run (Step A) evlist'
 2. \<And>evlist' e s' t. \<lbrakk>(s', evlist') \<in> sub_big_steps A R s; (s', t) \<in> Step A e; \<not> R s t; (s, s') \<in> Run (Step A) evlist'; \<not> R s s'\<rbrakk> \<Longrightarrow> (?t4 evlist' e s' t, t) \<in> Run (Step A) [e] proof (prove)
goal (1 subgoal):
 1. \<And>evlist' e s' t. \<lbrakk>(s', evlist') \<in> sub_big_steps A R s; (s', t) \<in> Step A e; \<not> R s t; (s, s') \<in> Run (Step A) evlist'; \<not> R s s'\<rbrakk> \<Longrightarrow> (s', t) \<in> Run (Step A) [e] proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma reachable_i_big_step_adt:
  "reachable_i (big_step_adt C R exmap) s0 s \<Longrightarrow> reachable_i C s0 s" apply (clarsimp simp: reachable_i_def) apply (blast intro: big_step_adt_reachable_i_states) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable_i (big_step_adt C R exmap) s0 s \<Longrightarrow> reachable_i C s0 s proof (prove)
goal (1 subgoal):
 1. \<And>js. (s0, s) \<in> Run (Step (big_step_adt C R exmap)) js \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma reachable_reachable_i:
  "system.reachable A s0 s \<Longrightarrow> \<exists>s0' s'. s0' \<in> Init A s0 \<and> Fin A s' = s \<and> reachable_i A s0' s'" by (force simp: system.reachable_def reachable_i_def execution_def steps_eq_Run)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. system.reachable A s0 s \<Longrightarrow> \<exists>s0' s'. s0' \<in> Init A s0 \<and> Fin A s' = s \<and> reachable_i A s0' s'
theory ADT_IF

lemma reachable_i_reachable:
  "\<lbrakk> reachable_i A s0' s'; s0' \<in> Init A s0; Fin A s' = s \<rbrakk>
     \<Longrightarrow> system.reachable A s0 s" by (force simp: system.reachable_def reachable_i_def execution_def steps_eq_Run)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable_i A s0' s'; s0' \<in> Init A s0; Fin A s' = s\<rbrakk> \<Longrightarrow> system.reachable A s0 s
theory ADT_IF

lemma reachable_big_step_adt:
  "system.reachable (big_step_adt C R exmap) s0 s
   \<Longrightarrow> system.reachable C s0 s" by (force dest: reachable_reachable_i
           intro: reachable_i_reachable reachable_i_big_step_adt
            simp: big_step_adt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. system.reachable (big_step_adt C R exmap) s0 s \<Longrightarrow> system.reachable C s0 s
theory ADT_IF

lemma big_step_adt_Init_inv_Fin_system:
  "Init_inv_Fin_system A s0 \<Longrightarrow> Init_inv_Fin_system (big_step_adt A R exmap) s0" apply (clarsimp simp: Init_inv_Fin_system_def big_step_adt_def) apply (erule_tac x=s in allE) apply (force intro: reachable_big_step_adt simp: big_step_adt_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Init_inv_Fin_system A s0 \<Longrightarrow> Init_inv_Fin_system (big_step_adt A R exmap) s0 proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>x \<in> Init A (Fin A x); s0 = Fin A x; \<forall>s. system.reachable A (Fin A x) s \<longrightarrow> Init A s = {s'. Fin A s' = s}; inj (Fin A); system.reachable \<lparr>Init = Init A, Fin = Fin A, Step = big_steps A R exmap\<rparr> (Fin A x) s\<rbrakk> \<Longrightarrow> Init A s = {s'. Fin A s' = s} proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>x \<in> Init A (Fin A x); s0 = Fin A x; inj (Fin A); system.reachable \<lparr>Init = Init A, Fin = Fin A, Step = big_steps A R exmap\<rparr> (Fin A x) s; system.reachable A (Fin A x) s \<longrightarrow> Init A s = {s'. Fin A s' = s}\<rbrakk> \<Longrightarrow> Init A s = {s'. Fin A s' = s} proof (prove)
goal:
No subgoals!