theory ADT_IF

lemma big_step_adt_reachable_i_states:
  "(s0, s) \<in> Run (Step (big_step_adt C R exmap)) js \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js" apply (induct js arbitrary: s0) apply (rule_tac x="[]" in exI, simp) apply (clarsimp simp: big_step_adt_def) apply (rename_tac s0 sa) apply (erule big_stepsE) apply (drule sub_big_steps_Run) apply (subgoal_tac "(s0,sa) \<in> Run (data_type.Step C) (as@[aa])") apply (blast intro: Run_trans) apply (fastforce intro: Run_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (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 (2 subgoals):
 1. \<And>s0. (s0, s) \<in> Run (Step (big_step_adt C R exmap)) [] \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js
 2. \<And>a js s0. \<lbrakk>\<And>s0. (s0, s) \<in> Run (Step (big_step_adt C R exmap)) js \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js; (s0, s) \<in> Run (Step (big_step_adt C R exmap)) (a # js)\<rbrakk> \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js proof (prove)
goal (1 subgoal):
 1. \<And>a js s0. \<lbrakk>\<And>s0. (s0, s) \<in> Run (Step (big_step_adt C R exmap)) js \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js; (s0, s) \<in> Run (Step (big_step_adt C R exmap)) (a # js)\<rbrakk> \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js proof (prove)
goal (1 subgoal):
 1. \<And>a js x y. \<lbrakk>\<And>s0. (s0, s) \<in> Run (big_steps C R exmap) js \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js; (x, y) \<in> big_steps C R exmap a; (y, s) \<in> Run (big_steps C R exmap) js\<rbrakk> \<Longrightarrow> \<exists>js. (x, s) \<in> Run (Step C) js proof (prove)
goal (1 subgoal):
 1. \<And>a js s0 sa. \<lbrakk>\<And>s0. (s0, s) \<in> Run (big_steps C R exmap) js \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js; (s0, sa) \<in> big_steps C R exmap a; (sa, s) \<in> Run (big_steps C R exmap) js\<rbrakk> \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js proof (prove)
goal (1 subgoal):
 1. \<And>a js s0 sa s' as aa. \<lbrakk>\<And>s0. (s0, s) \<in> Run (big_steps C R exmap) js \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js; (sa, s) \<in> Run (big_steps C R exmap) js; (s', as) \<in> sub_big_steps C R s0; (s', sa) \<in> Step C aa; R s0 sa; a = exmap (as @ [aa])\<rbrakk> \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js proof (prove)
goal (1 subgoal):
 1. \<And>a js s0 sa s' as aa. \<lbrakk>\<And>s0. (s0, s) \<in> Run (big_steps C R exmap) js \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js; (sa, s) \<in> Run (big_steps C R exmap) js; (s', sa) \<in> Step C aa; R s0 sa; a = exmap (as @ [aa]); (s0, s') \<in> Run (Step C) as \<and> \<not> R s0 s'\<rbrakk> \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js proof (prove)
goal (2 subgoals):
 1. \<And>a js s0 sa s' as aa. \<lbrakk>\<And>s0. (s0, s) \<in> Run (big_steps C R exmap) js \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js; (sa, s) \<in> Run (big_steps C R exmap) js; (s', sa) \<in> Step C aa; R s0 sa; a = exmap (as @ [aa]); (s0, s') \<in> Run (Step C) as \<and> \<not> R s0 s'; (s0, sa) \<in> Run (Step C) (as @ [aa])\<rbrakk> \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js
 2. \<And>a js s0 sa s' as aa. \<lbrakk>\<And>s0. (s0, s) \<in> Run (big_steps C R exmap) js \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js; (sa, s) \<in> Run (big_steps C R exmap) js; (s', sa) \<in> Step C aa; R s0 sa; a = exmap (as @ [aa]); (s0, s') \<in> Run (Step C) as \<and> \<not> R s0 s'\<rbrakk> \<Longrightarrow> (s0, sa) \<in> Run (Step C) (as @ [aa]) proof (prove)
goal (1 subgoal):
 1. \<And>a js s0 sa s' as aa. \<lbrakk>\<And>s0. (s0, s) \<in> Run (big_steps C R exmap) js \<Longrightarrow> \<exists>js. (s0, s) \<in> Run (Step C) js; (sa, s) \<in> Run (big_steps C R exmap) js; (s', sa) \<in> Step C aa; R s0 sa; a = exmap (as @ [aa]); (s0, s') \<in> Run (Step C) as \<and> \<not> R s0 s'\<rbrakk> \<Longrightarrow> (s0, sa) \<in> Run (Step C) (as @ [aa]) proof (prove)
goal:
No subgoals!