theory ADT_IF

lemma enabled:
  "enabled_system A s0" supply image_cong_simp [cong del] supply ex_image_cong_iff [simp del] apply (clarsimp simp: enabled_system_def) apply (induct_tac jsa rule: rev_induct) apply (clarsimp simp: execution_def steps_def) apply (fold steps_def) apply (rule_tac x="Fin A x" in exI) apply (rule imageI) apply (rule Init_Fin) apply (rule set_mp) apply (rule invariant_holds_steps[OF I]) apply (rule s0_I) apply simp apply (clarsimp simp: execution_def steps_def) apply (fold steps_def) apply (subgoal_tac "xb \<in> I") apply (drule_tac a=x in serial) apply clarsimp apply (rule_tac x="Fin A t" in exI) apply (rule imageI) apply (rule ImageI) apply assumption apply assumption apply (rule set_mp) apply (rule invariant_holds_steps[OF I]) prefer 2 apply assumption apply (rule I[simplified invariant_holds_def, THEN conjunct1,rule_format]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. enabled_system A s0 proof (prove)
goal (1 subgoal):
 1. enabled_system A s0 proof (prove)
goal (1 subgoal):
 1. enabled_system A s0 proof (prove)
goal (1 subgoal):
 1. \<And>s js jsa. s \<in> execution A s0 js \<Longrightarrow> \<exists>s'. s' \<in> execution A s jsa proof (prove)
goal (2 subgoals):
 1. \<And>s js jsa. s \<in> execution A s0 js \<Longrightarrow> \<exists>s'. s' \<in> execution A s []
 2. \<And>s js jsa x xs. \<lbrakk>s \<in> execution A s0 js; \<exists>s'. s' \<in> execution A s xs\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> execution A s (xs @ [x]) proof (prove)
goal (2 subgoals):
 1. \<And>js x. x \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js \<Longrightarrow> \<exists>s'. s' \<in> Fin A ` Init A (Fin A x)
 2. \<And>s js jsa x xs. \<lbrakk>s \<in> execution A s0 js; \<exists>s'. s' \<in> execution A s xs\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> execution A s (xs @ [x]) proof (prove)
goal (2 subgoals):
 1. \<And>js x. x \<in> steps (data_type.Step A) (Init A s0) js \<Longrightarrow> \<exists>s'. s' \<in> Fin A ` Init A (Fin A x)
 2. \<And>s js jsa x xs. \<lbrakk>s \<in> execution A s0 js; \<exists>s'. s' \<in> execution A s xs\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> execution A s (xs @ [x]) proof (prove)
goal (2 subgoals):
 1. \<And>js x. x \<in> steps (data_type.Step A) (Init A s0) js \<Longrightarrow> Fin A x \<in> Fin A ` Init A (Fin A x)
 2. \<And>s js jsa x xs. \<lbrakk>s \<in> execution A s0 js; \<exists>s'. s' \<in> execution A s xs\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> execution A s (xs @ [x]) proof (prove)
goal (2 subgoals):
 1. \<And>js x. x \<in> steps (data_type.Step A) (Init A s0) js \<Longrightarrow> x \<in> Init A (Fin A x)
 2. \<And>s js jsa x xs. \<lbrakk>s \<in> execution A s0 js; \<exists>s'. s' \<in> execution A s xs\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> execution A s (xs @ [x]) proof (prove)
goal (2 subgoals):
 1. \<And>js x. x \<in> steps (data_type.Step A) (Init A s0) js \<Longrightarrow> x \<in> I
 2. \<And>s js jsa x xs. \<lbrakk>s \<in> execution A s0 js; \<exists>s'. s' \<in> execution A s xs\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> execution A s (xs @ [x]) proof (prove)
goal (3 subgoals):
 1. \<And>js x. x \<in> steps (data_type.Step A) (Init A s0) js \<Longrightarrow> ?A17 js x \<subseteq> I
 2. \<And>js x. x \<in> steps (data_type.Step A) (Init A s0) js \<Longrightarrow> x \<in> ?A17 js x
 3. \<And>s js jsa x xs. \<lbrakk>s \<in> execution A s0 js; \<exists>s'. s' \<in> execution A s xs\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> execution A s (xs @ [x]) proof (prove)
goal (3 subgoals):
 1. \<And>js x. x \<in> steps (data_type.Step A) (Init A s0) js \<Longrightarrow> ?B20 js x \<subseteq> I
 2. \<And>js x. x \<in> steps (data_type.Step A) (Init A s0) js \<Longrightarrow> x \<in> steps (data_type.Step A) (?B20 js x) (?as20 js x)
 3. \<And>s js jsa x xs. \<lbrakk>s \<in> execution A s0 js; \<exists>s'. s' \<in> execution A s xs\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> execution A s (xs @ [x]) proof (prove)
goal (2 subgoals):
 1. \<And>js x. x \<in> steps (data_type.Step A) (Init A s0) js \<Longrightarrow> x \<in> steps (data_type.Step A) (Init A s0) (?as20 js x)
 2. \<And>s js jsa x xs. \<lbrakk>s \<in> execution A s0 js; \<exists>s'. s' \<in> execution A s xs\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> execution A s (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>s js jsa x xs. \<lbrakk>s \<in> execution A s0 js; \<exists>s'. s' \<in> execution A s xs\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> execution A s (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>js x xs xa xb. \<lbrakk>xa \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A s0) js; xb \<in> foldl (\<lambda>S j. data_type.Step A j `` S) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> Fin A ` data_type.Step A x `` foldl (\<lambda>S j. data_type.Step A j `` S) (Init A (Fin A xa)) xs proof (prove)
goal (1 subgoal):
 1. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> Fin A ` data_type.Step A x `` steps (data_type.Step A) (Init A (Fin A xa)) xs proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; xb \<in> I\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> Fin A ` data_type.Step A x `` steps (data_type.Step A) (Init A (Fin A xa)) xs
 2. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> xb \<in> I proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; \<exists>t. (xb, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> Fin A ` data_type.Step A x `` steps (data_type.Step A) (Init A (Fin A xa)) xs
 2. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> xb \<in> I proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb t. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; (xb, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> Fin A ` data_type.Step A x `` steps (data_type.Step A) (Init A (Fin A xa)) xs
 2. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> xb \<in> I proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb t. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; (xb, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> Fin A t \<in> Fin A ` data_type.Step A x `` steps (data_type.Step A) (Init A (Fin A xa)) xs
 2. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> xb \<in> I proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb t. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; (xb, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> t \<in> data_type.Step A x `` steps (data_type.Step A) (Init A (Fin A xa)) xs
 2. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> xb \<in> I proof (prove)
goal (3 subgoals):
 1. \<And>js x xs xa xb t. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; (xb, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> (?a37 js x xs xa xb t, t) \<in> data_type.Step A x
 2. \<And>js x xs xa xb t. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; (xb, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> ?a37 js x xs xa xb t \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs
 3. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> xb \<in> I proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb t. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; (xb, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs
 2. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> xb \<in> I proof (prove)
goal (1 subgoal):
 1. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> xb \<in> I proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> ?A40 js x xs xa xb \<subseteq> I
 2. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> xb \<in> ?A40 js x xs xa xb proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> ?B43 js x xs xa xb \<subseteq> I
 2. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> xb \<in> steps (data_type.Step A) (?B43 js x xs xa xb) (?as43 js x xs xa xb) proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> xb \<in> steps (data_type.Step A) (?B43 js x xs xa xb) (?as43 js x xs xa xb)
 2. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> ?B43 js x xs xa xb \<subseteq> I proof (prove)
goal (1 subgoal):
 1. \<And>js x xs xa xb. \<lbrakk>xa \<in> steps (data_type.Step A) (Init A s0) js; xb \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs\<rbrakk> \<Longrightarrow> Init A (Fin A xa) \<subseteq> I proof (prove)
goal:
No subgoals!