theory ADT_IF

lemma execution_invs:
  assumes e: "s \<in> execution (ADT_A_if utf) s0 js"
  shows "invs_if s" apply (insert e) apply (induct js arbitrary: s rule: rev_induct) apply (clarsimp simp add: execution_def Fin_ADT_if Init_ADT_if
                             image_def) apply (simp add: execution_def Fin_ADT_if Init_ADT_if steps_def) apply (simp add: execution_def steps_def image_def) apply (erule bexE) apply (unfold Image_def) apply (drule CollectD) apply (erule bexE) apply simp apply (rule invs_if_Step_ADT_A_if) apply (drule_tac meta_spec) apply (fastforce) apply simp apply (clarsimp simp: Fin_ADT_if ADT_A_if_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs_if s proof (prove)
goal (1 subgoal):
 1. s \<in> execution (ADT_A_if utf) s0 js \<Longrightarrow> invs_if s proof (prove)
goal (2 subgoals):
 1. \<And>s. s \<in> execution (ADT_A_if utf) s0 [] \<Longrightarrow> invs_if s
 2. \<And>x xs s. \<lbrakk>\<And>s. s \<in> execution (ADT_A_if utf) s0 xs \<Longrightarrow> invs_if s; s \<in> execution (ADT_A_if utf) s0 (xs @ [x])\<rbrakk> \<Longrightarrow> invs_if s proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. ((a, b), ba) \<in> steps (Step (ADT_A_if utf)) ({s0} \<inter> full_invs_if \<inter> Collect step_restrict) [] \<Longrightarrow> invs_if ((a, b), ba)
 2. \<And>x xs s. \<lbrakk>\<And>s. s \<in> execution (ADT_A_if utf) s0 xs \<Longrightarrow> invs_if s; s \<in> execution (ADT_A_if utf) s0 (xs @ [x])\<rbrakk> \<Longrightarrow> invs_if s proof (prove)
goal (1 subgoal):
 1. \<And>x xs s. \<lbrakk>\<And>s. s \<in> execution (ADT_A_if utf) s0 xs \<Longrightarrow> invs_if s; s \<in> execution (ADT_A_if utf) s0 (xs @ [x])\<rbrakk> \<Longrightarrow> invs_if s proof (prove)
goal (1 subgoal):
 1. \<And>xs s. \<lbrakk>\<And>s. \<exists>x\<in>foldl (\<lambda>S j. Step (ADT_A_if utf) () `` S) (Init (ADT_A_if utf) s0) xs. s = Fin (ADT_A_if utf) x \<Longrightarrow> invs_if s; \<exists>x\<in>Step (ADT_A_if utf) () `` foldl (\<lambda>S j. Step (ADT_A_if utf) () `` S) (Init (ADT_A_if utf) s0) xs. s = Fin (ADT_A_if utf) x\<rbrakk> \<Longrightarrow> invs_if s proof (prove)
goal (1 subgoal):
 1. \<And>xs s x. \<lbrakk>\<And>s. \<exists>x\<in>foldl (\<lambda>S j. Step (ADT_A_if utf) () `` S) (Init (ADT_A_if utf) s0) xs. s = Fin (ADT_A_if utf) x \<Longrightarrow> invs_if s; x \<in> Step (ADT_A_if utf) () `` foldl (\<lambda>S j. Step (ADT_A_if utf) () `` S) (Init (ADT_A_if utf) s0) xs; s = Fin (ADT_A_if utf) x\<rbrakk> \<Longrightarrow> invs_if s proof (prove)
goal (1 subgoal):
 1. \<And>xs s x. \<lbrakk>\<And>s. \<exists>x\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs. s = Fin (ADT_A_if utf) x \<Longrightarrow> invs_if s; x \<in> {y. \<exists>x\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs. (x, y) \<in> Step (ADT_A_if utf) ()}; s = Fin (ADT_A_if utf) x\<rbrakk> \<Longrightarrow> invs_if s proof (prove)
goal (1 subgoal):
 1. \<And>xs s x. \<lbrakk>\<And>s. \<exists>x\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs. s = Fin (ADT_A_if utf) x \<Longrightarrow> invs_if s; s = Fin (ADT_A_if utf) x; \<exists>xa\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs. (xa, x) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> invs_if s proof (prove)
goal (1 subgoal):
 1. \<And>xs s x xa. \<lbrakk>\<And>s. \<exists>x\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs. s = Fin (ADT_A_if utf) x \<Longrightarrow> invs_if s; s = Fin (ADT_A_if utf) x; xa \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs; (xa, x) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> invs_if s proof (prove)
goal (1 subgoal):
 1. \<And>xs s x xa. \<lbrakk>\<And>s. \<exists>x\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs. s = Fin (ADT_A_if utf) x \<Longrightarrow> invs_if s; s = Fin (ADT_A_if utf) x; xa \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs; (xa, x) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> invs_if (Fin (ADT_A_if utf) x) proof (prove)
goal (2 subgoals):
 1. \<And>xs s x xa. \<lbrakk>\<And>s. \<exists>x\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs. s = Fin (ADT_A_if utf) x \<Longrightarrow> invs_if s; s = Fin (ADT_A_if utf) x; xa \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs; (xa, x) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> invs_if (?s14 xs s x xa)
 2. \<And>xs s x xa. \<lbrakk>\<And>s. \<exists>x\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs. s = Fin (ADT_A_if utf) x \<Longrightarrow> invs_if s; s = Fin (ADT_A_if utf) x; xa \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs; (xa, x) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> (?s14 xs s x xa, Fin (ADT_A_if utf) x) \<in> Step (ADT_A_if utf) (?e14 xs s x xa) proof (prove)
goal (2 subgoals):
 1. \<And>xs s x xa. \<lbrakk>s = Fin (ADT_A_if utf) x; xa \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs; (xa, x) \<in> Step (ADT_A_if utf) (); \<exists>xb\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs. ?s17 xs s x xa = Fin (ADT_A_if utf) xb \<Longrightarrow> invs_if (?s17 xs s x xa)\<rbrakk> \<Longrightarrow> invs_if (?s14 xs s x xa)
 2. \<And>xs s x xa. \<lbrakk>\<And>s. \<exists>x\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs. s = Fin (ADT_A_if utf) x \<Longrightarrow> invs_if s; s = Fin (ADT_A_if utf) x; xa \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs; (xa, x) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> (?s14 xs s x xa, Fin (ADT_A_if utf) x) \<in> Step (ADT_A_if utf) (?e14 xs s x xa) proof (prove)
goal (1 subgoal):
 1. \<And>xs s x xa. \<lbrakk>\<And>s. \<exists>x\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs. s = Fin (ADT_A_if utf) x \<Longrightarrow> invs_if s; s = Fin (ADT_A_if utf) x; xa \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs; (xa, x) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> (Fin (ADT_A_if utf) xa, Fin (ADT_A_if utf) x) \<in> Step (ADT_A_if utf) (?e14 xs s x xa) proof (prove)
goal (1 subgoal):
 1. \<And>xs s x xa. \<lbrakk>\<And>s. \<exists>x\<in>foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs. s = Fin (ADT_A_if utf) x \<Longrightarrow> invs_if s; s = Fin (ADT_A_if utf) x; xa \<in> foldl (\<lambda>S j. {y. \<exists>x\<in>S. (x, y) \<in> Step (ADT_A_if utf) ()}) (Init (ADT_A_if utf) s0) xs; (xa, x) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> (Fin (ADT_A_if utf) xa, Fin (ADT_A_if utf) x) \<in> Step (ADT_A_if utf) () proof (prove)
goal:
No subgoals!