theory Deterministic_AI

lemma last_last_child_NoneD:
  notes split_paired_Ex[simp del] if_weak_cong[cong]
  assumes "last_last_child slot (cdt_list s) = None" "valid_list s" "valid_mdb s"
  shows "descendants_of slot (cdt s) = {}" apply(insert assms) apply(simp add: last_last_child_termination) apply(simp split: if_split_asm option.splits) apply(simp add:last_child_NoneD) apply(erule exE) apply(induct slot rule: last_child_induct[where s=s]) apply(fastforce dest: last_child_NoneD) apply(simp) apply(case_tac "last_child ya (cdt_list s)") apply(simp add: last_last_child_termination) apply(atomize, simp) apply(erule impE) apply(simp add: last_last_child_termination) apply(drule_tac slot=y in last_childD, simp) apply(fastforce dest: child_descendant) using assms apply(simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of slot (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>last_last_child slot (cdt_list s) = None; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> descendants_of slot (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(case last_child slot (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)) = None; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> descendants_of slot (cdt s) = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; last_child slot (cdt_list s) = None\<rbrakk> \<Longrightarrow> descendants_of slot (cdt s) = {}
 2. \<And>x2. \<lbrakk>valid_list s; valid_mdb s; last_child slot (cdt_list s) = Some x2; \<exists>y. last_child x2 (cdt_list s) = Some y; last_last_child x2 (cdt_list s) = None\<rbrakk> \<Longrightarrow> descendants_of slot (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>valid_list s; valid_mdb s; last_child slot (cdt_list s) = Some x2; \<exists>y. last_child x2 (cdt_list s) = Some y; last_last_child x2 (cdt_list s) = None\<rbrakk> \<Longrightarrow> descendants_of slot (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x2 y. \<lbrakk>valid_list s; valid_mdb s; last_child slot (cdt_list s) = Some x2; last_last_child x2 (cdt_list s) = None; last_child x2 (cdt_list s) = Some y\<rbrakk> \<Longrightarrow> descendants_of slot (cdt s) = {} proof (prove)
goal (4 subgoals):
 1. \<And>x x2 y. \<lbrakk>last_child x (cdt_list s) = None; valid_list s; valid_mdb s; last_child x (cdt_list s) = Some x2; last_last_child x2 (cdt_list s) = None; last_child x2 (cdt_list s) = Some y\<rbrakk> \<Longrightarrow> descendants_of x (cdt s) = {}
 2. \<And>x y x2 ya. \<lbrakk>last_child x (cdt_list s) = Some y; \<And>x2 ya. \<lbrakk>valid_list s; valid_mdb s; last_child y (cdt_list s) = Some x2; last_last_child x2 (cdt_list s) = None; last_child x2 (cdt_list s) = Some ya\<rbrakk> \<Longrightarrow> descendants_of y (cdt s) = {}; valid_list s; valid_mdb s; last_child x (cdt_list s) = Some x2; last_last_child x2 (cdt_list s) = None; last_child x2 (cdt_list s) = Some ya\<rbrakk> \<Longrightarrow> descendants_of x (cdt s) = {}
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y x2 ya. \<lbrakk>last_child x (cdt_list s) = Some y; \<And>x2 ya. \<lbrakk>valid_list s; valid_mdb s; last_child y (cdt_list s) = Some x2; last_last_child x2 (cdt_list s) = None; last_child x2 (cdt_list s) = Some ya\<rbrakk> \<Longrightarrow> descendants_of y (cdt s) = {}; valid_list s; valid_mdb s; last_child x (cdt_list s) = Some x2; last_last_child x2 (cdt_list s) = None; last_child x2 (cdt_list s) = Some ya\<rbrakk> \<Longrightarrow> descendants_of x (cdt s) = {}
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y x2 ya. \<lbrakk>x2 = y; \<And>x2 yb. \<lbrakk>ya = x2; last_last_child x2 (cdt_list s) = None; last_child x2 (cdt_list s) = Some yb\<rbrakk> \<Longrightarrow> descendants_of y (cdt s) = {}; valid_list s; valid_mdb s; last_child x (cdt_list s) = Some y; last_last_child y (cdt_list s) = None; last_child y (cdt_list s) = Some ya\<rbrakk> \<Longrightarrow> descendants_of x (cdt s) = {}
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>x y x2 ya. \<lbrakk>x2 = y; \<And>x2 yb. \<lbrakk>ya = x2; last_last_child x2 (cdt_list s) = None; last_child x2 (cdt_list s) = Some yb\<rbrakk> \<Longrightarrow> descendants_of y (cdt s) = {}; valid_list s; valid_mdb s; last_child x (cdt_list s) = Some y; last_last_child y (cdt_list s) = None; last_child y (cdt_list s) = Some ya; last_child ya (cdt_list s) = None\<rbrakk> \<Longrightarrow> descendants_of x (cdt s) = {}
 2. \<And>x y x2 ya a. \<lbrakk>x2 = y; \<And>x2 yb. \<lbrakk>ya = x2; last_last_child x2 (cdt_list s) = None; last_child x2 (cdt_list s) = Some yb\<rbrakk> \<Longrightarrow> descendants_of y (cdt s) = {}; valid_list s; valid_mdb s; last_child x (cdt_list s) = Some y; last_last_child y (cdt_list s) = None; last_child y (cdt_list s) = Some ya; last_child ya (cdt_list s) = Some a\<rbrakk> \<Longrightarrow> descendants_of x (cdt s) = {}
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y x2 ya a. \<lbrakk>x2 = y; \<And>x2 yb. \<lbrakk>ya = x2; last_last_child x2 (cdt_list s) = None; last_child x2 (cdt_list s) = Some yb\<rbrakk> \<Longrightarrow> descendants_of y (cdt s) = {}; valid_list s; valid_mdb s; last_child x (cdt_list s) = Some y; last_last_child y (cdt_list s) = None; last_child y (cdt_list s) = Some ya; last_child ya (cdt_list s) = Some a\<rbrakk> \<Longrightarrow> descendants_of x (cdt s) = {}
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y x2 ya a. \<lbrakk>x2 = y; last_last_child ya (cdt_list s) = None \<longrightarrow> descendants_of y (cdt s) = {}; valid_list s; valid_mdb s; last_child x (cdt_list s) = Some y; last_last_child y (cdt_list s) = None; last_child y (cdt_list s) = Some ya; last_child ya (cdt_list s) = Some a\<rbrakk> \<Longrightarrow> descendants_of x (cdt s) = {}
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (4 subgoals):
 1. \<And>x y x2 ya a. \<lbrakk>x2 = y; valid_list s; valid_mdb s; last_child x (cdt_list s) = Some y; last_last_child y (cdt_list s) = None; last_child y (cdt_list s) = Some ya; last_child ya (cdt_list s) = Some a\<rbrakk> \<Longrightarrow> last_last_child ya (cdt_list s) = None
 2. \<And>x y x2 ya a. \<lbrakk>x2 = y; valid_list s; valid_mdb s; last_child x (cdt_list s) = Some y; last_last_child y (cdt_list s) = None; last_child y (cdt_list s) = Some ya; last_child ya (cdt_list s) = Some a; descendants_of y (cdt s) = {}\<rbrakk> \<Longrightarrow> descendants_of x (cdt s) = {}
 3. valid_mdb s
 4. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y x2 ya a. \<lbrakk>x2 = y; valid_list s; valid_mdb s; last_child x (cdt_list s) = Some y; last_last_child y (cdt_list s) = None; last_child y (cdt_list s) = Some ya; last_child ya (cdt_list s) = Some a; descendants_of y (cdt s) = {}\<rbrakk> \<Longrightarrow> descendants_of x (cdt s) = {}
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>x y x2 ya a. \<lbrakk>x2 = y; valid_list s; valid_mdb s; last_child x (cdt_list s) = Some y; last_last_child y (cdt_list s) = None; last_child ya (cdt_list s) = Some a; descendants_of y (cdt s) = {}; cdt s ya = Some y \<and> next_sib ya (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> 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) = None
valid_list s
valid_mdb s

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