theory Deterministic_AI

lemma last_last_child_in_desc:
  assumes "last_last_child slot (cdt_list s) = Some child" "valid_mdb s" "valid_list s"
  shows "child \<in> descendants_of slot (cdt s)" apply(insert assms) apply(induct slot rule: last_child_induct[where s=s]) apply(simp add: last_last_child_termination) apply(case_tac "y=child") apply(simp add: last_last_child_termination) apply(drule last_childD, simp) apply(fastforce dest: child_descendant intro: descendants_trans split: option.splits) apply(simp) apply(atomize, erule impE) apply(subst(asm) last_last_child.psimps) apply(simp add: last_last_child_termination) apply(simp split: option.splits if_split_asm) apply(drule last_childD, simp) apply(fastforce dest: child_descendant descendants_trans) using assms apply(simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. child \<in> descendants_of slot (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>last_last_child slot (cdt_list s) = Some child; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> child \<in> descendants_of slot (cdt s) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>last_child x (cdt_list s) = None; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> child \<in> descendants_of y (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 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>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> child \<in> descendants_of y (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 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; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> child \<in> descendants_of y (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y = child\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> child \<in> descendants_of y (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some child; (case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else last_last_child child (cdt_list s)) = Some child \<Longrightarrow> child \<in> descendants_of child (cdt s); (if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else last_last_child child (cdt_list s)) = Some child; valid_mdb s; valid_list s; y = child\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> child \<in> descendants_of y (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>(case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else last_last_child child (cdt_list s)) = Some child \<Longrightarrow> child \<in> descendants_of child (cdt s); (if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else case last_child child (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else last_last_child child (cdt_list s)) = Some child; valid_mdb s; valid_list s; y = child; cdt s child = Some x \<and> next_sib child (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; \<lbrakk>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> child \<in> descendants_of y (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 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>last_last_child y (cdt_list s) = Some child; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> child \<in> descendants_of y (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 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; last_last_child y (cdt_list s) = Some child \<Longrightarrow> child \<in> descendants_of y (cdt s); last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 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; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> last_last_child y (cdt_list s) = Some child
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y \<noteq> child; child \<in> descendants_of y (cdt s)\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>valid_mdb s; valid_list s; y \<noteq> child; last_child x (cdt_list s) = Some y\<rbrakk> \<Longrightarrow> last_last_child_dom (x, cdt_list s)
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; (case last_child x (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else last_last_child child (cdt_list s)) = Some child; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> last_last_child y (cdt_list s) = Some child
 3. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y \<noteq> child; child \<in> descendants_of y (cdt s)\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 4. valid_mdb s
 5. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; (case last_child x (cdt_list s) of None \<Rightarrow> None | Some child \<Rightarrow> if last_child child (cdt_list s) = None then Some child else last_last_child child (cdt_list s)) = Some child; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> last_last_child y (cdt_list s) = Some child
 2. \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y \<noteq> child; child \<in> descendants_of y (cdt s)\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 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; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y \<noteq> child; child \<in> descendants_of y (cdt s)\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y \<noteq> child; child \<in> descendants_of y (cdt s); cdt s y = Some x \<and> next_sib y (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> child \<in> descendants_of x (cdt s)
 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:
last_last_child slot (cdt_list s) = Some child
valid_mdb s
valid_list s

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