theory ADT_IF

lemma steps_eq_Run:
  "(s' \<in> steps (Step A) (Init A s0) js) =
   (\<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) js)" apply (rule iffI) apply (clarsimp simp: steps_def image_def Image_def) apply (induct js arbitrary: s' rule: rev_induct) apply simp apply (force intro: Run_trans) apply (clarsimp simp: steps_def image_def Image_def) apply (induct js arbitrary: s' rule: rev_induct) apply simp apply clarsimp apply (drule Run_mid, force) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s' \<in> steps (Step A) (Init A s0) js) = (\<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) js) proof (prove)
goal (2 subgoals):
 1. s' \<in> steps (Step A) (Init A s0) js \<Longrightarrow> \<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) js
 2. \<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) js \<Longrightarrow> s' \<in> steps (Step A) (Init A s0) js proof (prove)
goal (2 subgoals):
 1. s' \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step A j}) (Init A s0) js \<Longrightarrow> \<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) js
 2. \<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) js \<Longrightarrow> s' \<in> steps (Step A) (Init A s0) js proof (prove)
goal (3 subgoals):
 1. \<And>s'. s' \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step A j}) (Init A s0) [] \<Longrightarrow> \<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) []
 2. \<And>x xs s'. \<lbrakk>\<And>s'. s' \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step A j}) (Init A s0) xs \<Longrightarrow> \<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) xs; s' \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step A j}) (Init A s0) (xs @ [x])\<rbrakk> \<Longrightarrow> \<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) (xs @ [x])
 3. \<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) js \<Longrightarrow> s' \<in> steps (Step A) (Init A s0) js proof (prove)
goal (2 subgoals):
 1. \<And>x xs s'. \<lbrakk>\<And>s'. s' \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step A j}) (Init A s0) xs \<Longrightarrow> \<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) xs; s' \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step A j}) (Init A s0) (xs @ [x])\<rbrakk> \<Longrightarrow> \<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) (xs @ [x])
 2. \<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) js \<Longrightarrow> s' \<in> steps (Step A) (Init A s0) js proof (prove)
goal (1 subgoal):
 1. \<exists>s0'. s0' \<in> Init A s0 \<and> (s0', s') \<in> Run (Step A) js \<Longrightarrow> s' \<in> steps (Step A) (Init A s0) js proof (prove)
goal (1 subgoal):
 1. \<And>s0'. \<lbrakk>s0' \<in> Init A s0; (s0', s') \<in> Run (Step A) js\<rbrakk> \<Longrightarrow> s' \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step A j}) (Init A s0) js proof (prove)
goal (2 subgoals):
 1. \<And>s0' s'. \<lbrakk>s0' \<in> Init A s0; (s0', s') \<in> Run (Step A) []\<rbrakk> \<Longrightarrow> s' \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step A j}) (Init A s0) []
 2. \<And>x xs s0' s'. \<lbrakk>\<And>s0' s'. \<lbrakk>s0' \<in> Init A s0; (s0', s') \<in> Run (Step A) xs\<rbrakk> \<Longrightarrow> s' \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step A j}) (Init A s0) xs; s0' \<in> Init A s0; (s0', s') \<in> Run (Step A) (xs @ [x])\<rbrakk> \<Longrightarrow> s' \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step A j}) (Init A s0) (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s0' s'. \<lbrakk>\<And>s0' s'. \<lbrakk>s0' \<in> Init A s0; (s0', s') \<in> Run (Step A) xs\<rbrakk> \<Longrightarrow> s' \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step A j}) (Init A s0) xs; s0' \<in> Init A s0; (s0', s') \<in> Run (Step A) (xs @ [x])\<rbrakk> \<Longrightarrow> s' \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step A j}) (Init A s0) (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s0' s'. \<lbrakk>\<And>s0' s'. \<lbrakk>s0' \<in> Init A s0; (s0', s') \<in> Run (Step A) xs\<rbrakk> \<Longrightarrow> s' \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step A j}) (Init A s0) xs; s0' \<in> Init A s0; (s0', s') \<in> Run (Step A) (xs @ [x])\<rbrakk> \<Longrightarrow> \<exists>xa\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step A j}) (Init A s0) xs. (xa, s') \<in> Step A x proof (prove)
goal:
No subgoals!