theory Deterministic_AI

lemma last_last_childI:
  notes split_paired_All[simp del] split_paired_Ex[simp del] if_weak_cong[cong]
  assumes "child \<in> last_child_set slot (cdt_list s)"
   "descendants_of child (cdt s) = {}" "valid_mdb s" "valid_list s"
  shows "last_last_child slot (cdt_list s) = Some child" apply(insert assms) apply(induct slot rule: last_child_induct[where s=s]) apply(fastforce simp: last_child_set_def dest: tranclD2) apply(simp) apply(case_tac "y=child") apply(simp add: last_last_child_termination last_child_NoneI) apply(atomize) apply(erule impE) apply(fastforce simp: last_child_set_def dest: tranclD2 rtranclD) apply(simp add: last_last_child_termination split: option.splits) using assms apply(simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. last_last_child slot (cdt_list s) = Some child proof (prove)
goal (1 subgoal):
 1. \<lbrakk>child \<in> last_child_set slot (cdt_list s); descendants_of child (cdt s) = {}; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> last_last_child slot (cdt_list s) = Some child proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>last_child x (cdt_list s) = None; child \<in> last_child_set x (cdt_list s); descendants_of child (cdt s) = {}; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> last_last_child x (cdt_list s) = Some child
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>child \<in> last_child_set y (cdt_list s); descendants_of child (cdt s) = {}; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> last_last_child y (cdt_list s) = Some child; child \<in> last_child_set x (cdt_list s); descendants_of child (cdt s) = {}; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> last_last_child x (cdt_list s) = Some child
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>child \<in> last_child_set y (cdt_list s); descendants_of child (cdt s) = {}; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> last_last_child y (cdt_list s) = Some child; child \<in> last_child_set x (cdt_list s); descendants_of child (cdt s) = {}; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> last_last_child x (cdt_list s) = Some child
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; child \<in> last_child_set y (cdt_list s) \<Longrightarrow> last_last_child y (cdt_list s) = Some child; child \<in> last_child_set x (cdt_list s); descendants_of child (cdt s) = {}; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> last_last_child x (cdt_list s) = Some child
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; child \<in> last_child_set y (cdt_list s) \<Longrightarrow> last_last_child y (cdt_list s) = Some child; child \<in> last_child_set x (cdt_list s); descendants_of child (cdt s) = {}; valid_mdb s; valid_list s; y = child\<rbrakk> \<Longrightarrow> last_last_child x (cdt_list s) = Some child
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; child \<in> last_child_set y (cdt_list s) \<Longrightarrow> last_last_child y (cdt_list s) = Some child; child \<in> last_child_set x (cdt_list s); descendants_of child (cdt s) = {}; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> last_last_child x (cdt_list s) = Some child
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; child \<in> last_child_set y (cdt_list s) \<Longrightarrow> last_last_child y (cdt_list s) = Some child; child \<in> last_child_set x (cdt_list s); descendants_of child (cdt s) = {}; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> last_last_child x (cdt_list s) = Some child
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; child \<in> last_child_set y (cdt_list s) \<longrightarrow> last_last_child y (cdt_list s) = Some child; child \<in> last_child_set x (cdt_list s); descendants_of child (cdt s) = {}; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> last_last_child x (cdt_list s) = Some child
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; child \<in> last_child_set x (cdt_list s); descendants_of child (cdt s) = {}; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> child \<in> last_child_set y (cdt_list s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; child \<in> last_child_set x (cdt_list s); descendants_of child (cdt s) = {}; valid_mdb s; valid_list s; y \<noteq> child; last_last_child y (cdt_list s) = Some child\<rbrakk> \<Longrightarrow> last_last_child x (cdt_list s) = Some child
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; child \<in> last_child_set x (cdt_list s); descendants_of child (cdt s) = {}; valid_mdb s; valid_list s; y \<noteq> child; last_last_child y (cdt_list s) = Some child\<rbrakk> \<Longrightarrow> last_last_child x (cdt_list s) = Some child
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (2 subgoals):
 1. valid_mdb s
 2. valid_list s proof (prove)
using this:
child \<in> last_child_set slot (cdt_list s)
descendants_of child (cdt s) = {}
valid_mdb s
valid_list s

goal (2 subgoals):
 1. valid_mdb s
 2. valid_list s proof (prove)
goal:
No subgoals!