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 (rename_tac jsa, 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 inv_holds_steps[OF I]) apply (rule s0_I) apply simp apply (clarsimp simp: execution_def steps_def) apply (fold steps_def) apply (subgoal_tac "steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {}") apply (erule nonemptyE) apply clarsimp 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 (cut_tac inv_holds_steps[OF I s0_I]) apply (drule (1) subsetD) apply (cut_tac B="{xa}" and as=xs in inv_holds_steps[OF I]) apply simp apply (cut_tac B="{xa}" and as=xs in step_serial) apply simp+ apply (cut_tac A="{xa}" and B="Init A (Fin A xa)" in steps_subset) apply (simp add: Init_Fin) apply force 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; steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {}\<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> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb xc. \<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; xc \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> 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> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb xc. \<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; xc \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; xc \<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> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb xc. \<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; xc \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; \<exists>t. (xc, 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> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb xc 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; xc \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; (xc, 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> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb xc 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; xc \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; (xc, 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> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb xc 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; xc \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; (xc, 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> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} proof (prove)
goal (3 subgoals):
 1. \<And>js x xs xa xb xc 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; xc \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; (xc, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> (?a42 js x xs xa xb xc t, t) \<in> data_type.Step A x
 2. \<And>js x xs xa xb xc 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; xc \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; (xc, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> ?a42 js x xs xa xb xc 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> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>js x xs xa xb xc 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; xc \<in> steps (data_type.Step A) (Init A (Fin A xa)) xs; (xc, t) \<in> data_type.Step A x\<rbrakk> \<Longrightarrow> xc \<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> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} 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> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} 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; steps (data_type.Step A) (Init A s0) (?as46 js x xs xa xb) \<subseteq> I\<rbrakk> \<Longrightarrow> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} 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; xa \<in> I\<rbrakk> \<Longrightarrow> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} 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; xa \<in> I\<rbrakk> \<Longrightarrow> {xa} \<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; xa \<in> I; steps (data_type.Step A) {xa} xs \<subseteq> I\<rbrakk> \<Longrightarrow> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} 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; xa \<in> I; steps (data_type.Step A) {xa} xs \<subseteq> I\<rbrakk> \<Longrightarrow> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} proof (prove)
goal (3 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; xa \<in> I; steps (data_type.Step A) {xa} xs \<subseteq> I\<rbrakk> \<Longrightarrow> {xa} \<noteq> {}
 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; xa \<in> I; steps (data_type.Step A) {xa} xs \<subseteq> I\<rbrakk> \<Longrightarrow> {xa} \<subseteq> I
 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; xa \<in> I; steps (data_type.Step A) {xa} xs \<subseteq> I; steps (data_type.Step A) {xa} xs \<noteq> {}\<rbrakk> \<Longrightarrow> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>js 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; xa \<in> I; steps (data_type.Step A) {xa} xs \<subseteq> I; steps (data_type.Step A) {xa} xs \<noteq> {}\<rbrakk> \<Longrightarrow> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>js 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; xa \<in> I; steps (data_type.Step A) {xa} xs \<subseteq> I; steps (data_type.Step A) {xa} xs \<noteq> {}\<rbrakk> \<Longrightarrow> {xa} \<subseteq> Init A (Fin A xa)
 2. \<And>js 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; xa \<in> I; steps (data_type.Step A) {xa} xs \<subseteq> I; steps (data_type.Step A) {xa} xs \<noteq> {}; steps (?steps1.56 js xs xa xb) {xa} (?as56 js xs xa xb) \<subseteq> steps (?steps1.56 js xs xa xb) (Init A (Fin A xa)) (?as56 js xs xa xb)\<rbrakk> \<Longrightarrow> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>js 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; xa \<in> I; steps (data_type.Step A) {xa} xs \<subseteq> I; steps (data_type.Step A) {xa} xs \<noteq> {}; steps (?steps1.56 js xs xa xb) {xa} (?as56 js xs xa xb) \<subseteq> steps (?steps1.56 js xs xa xb) (Init A (Fin A xa)) (?as56 js xs xa xb)\<rbrakk> \<Longrightarrow> steps (data_type.Step A) (Init A (Fin A xa)) xs \<inter> I \<noteq> {} proof (prove)
goal:
No subgoals!