theory ADT_IF

lemma inv_holds_steps:
  assumes I: "A [> I"
  assumes start_I: "B \<subseteq> I"
  shows "steps (Simulation.Step A) B as \<subseteq> I" apply clarsimp apply (induct as rule: rev_induct) apply (simp add: steps_def) apply (rule set_mp) apply (rule start_I) apply simp apply (simp add: steps_def) apply (erule ImageE) apply (drule_tac x=xb in meta_spec) apply simp apply (rule set_mp) apply (rule I[simplified inv_holds_def,rule_format]) apply (rule ImageI) apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. steps (Step A) B as \<subseteq> I proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> steps (Step A) B as \<Longrightarrow> x \<in> I proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> steps (Step A) B [] \<Longrightarrow> x \<in> I
 2. \<And>x xs xa. \<lbrakk>\<And>x. x \<in> steps (Step A) B xs \<Longrightarrow> x \<in> I; xa \<in> steps (Step A) B (xs @ [x])\<rbrakk> \<Longrightarrow> xa \<in> I proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> B \<Longrightarrow> x \<in> I
 2. \<And>x xs xa. \<lbrakk>\<And>x. x \<in> steps (Step A) B xs \<Longrightarrow> x \<in> I; xa \<in> steps (Step A) B (xs @ [x])\<rbrakk> \<Longrightarrow> xa \<in> I proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> B \<Longrightarrow> ?A2 x \<subseteq> I
 2. \<And>x. x \<in> B \<Longrightarrow> x \<in> ?A2 x
 3. \<And>x xs xa. \<lbrakk>\<And>x. x \<in> steps (Step A) B xs \<Longrightarrow> x \<in> I; xa \<in> steps (Step A) B (xs @ [x])\<rbrakk> \<Longrightarrow> xa \<in> I proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> B \<Longrightarrow> x \<in> B
 2. \<And>x xs xa. \<lbrakk>\<And>x. x \<in> steps (Step A) B xs \<Longrightarrow> x \<in> I; xa \<in> steps (Step A) B (xs @ [x])\<rbrakk> \<Longrightarrow> xa \<in> I proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>\<And>x. x \<in> steps (Step A) B xs \<Longrightarrow> x \<in> I; xa \<in> steps (Step A) B (xs @ [x])\<rbrakk> \<Longrightarrow> xa \<in> I proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa. \<lbrakk>\<And>x. x \<in> foldl (\<lambda>S j. Step A j `` S) B xs \<Longrightarrow> x \<in> I; xa \<in> Step A x `` foldl (\<lambda>S j. Step A j `` S) B xs\<rbrakk> \<Longrightarrow> xa \<in> I proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa xb. \<lbrakk>\<And>x. x \<in> foldl (\<lambda>S j. Step A j `` S) B xs \<Longrightarrow> x \<in> I; (xb, xa) \<in> Step A x; xb \<in> foldl (\<lambda>S j. Step A j `` S) B xs\<rbrakk> \<Longrightarrow> xa \<in> I proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa xb. \<lbrakk>(xb, xa) \<in> Step A x; xb \<in> foldl (\<lambda>S j. Step A j `` S) B xs; xb \<in> foldl (\<lambda>S j. Step A j `` S) B xs \<Longrightarrow> xb \<in> I\<rbrakk> \<Longrightarrow> xa \<in> I proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa xb. \<lbrakk>(xb, xa) \<in> Step A x; xb \<in> foldl (\<lambda>S j. Step A j `` S) B xs; xb \<in> I\<rbrakk> \<Longrightarrow> xa \<in> I proof (prove)
goal (2 subgoals):
 1. \<And>x xs xa xb. \<lbrakk>(xb, xa) \<in> Step A x; xb \<in> foldl (\<lambda>S j. Step A j `` S) B xs; xb \<in> I\<rbrakk> \<Longrightarrow> ?A9 x xs xa xb \<subseteq> I
 2. \<And>x xs xa xb. \<lbrakk>(xb, xa) \<in> Step A x; xb \<in> foldl (\<lambda>S j. Step A j `` S) B xs; xb \<in> I\<rbrakk> \<Longrightarrow> xa \<in> ?A9 x xs xa xb proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa xb. \<lbrakk>(xb, xa) \<in> Step A x; xb \<in> foldl (\<lambda>S j. Step A j `` S) B xs; xb \<in> I\<rbrakk> \<Longrightarrow> xa \<in> Step A (?j12 x xs xa xb) `` I proof (prove)
goal (2 subgoals):
 1. \<And>x xs xa xb. \<lbrakk>(xb, xa) \<in> Step A x; xb \<in> foldl (\<lambda>S j. Step A j `` S) B xs; xb \<in> I\<rbrakk> \<Longrightarrow> (?a13 x xs xa xb, xa) \<in> Step A (?j12 x xs xa xb)
 2. \<And>x xs xa xb. \<lbrakk>(xb, xa) \<in> Step A x; xb \<in> foldl (\<lambda>S j. Step A j `` S) B xs; xb \<in> I\<rbrakk> \<Longrightarrow> ?a13 x xs xa xb \<in> I proof (prove)
goal (1 subgoal):
 1. \<And>x xs xa xb. \<lbrakk>(xb, xa) \<in> Step A x; xb \<in> foldl (\<lambda>S j. Step A j `` S) B xs; xb \<in> I\<rbrakk> \<Longrightarrow> xb \<in> I proof (prove)
goal:
No subgoals!