theory Deterministic_AI

lemma last_last_child_empty_desc:
  assumes "last_last_child slot (cdt_list s) = Some child" "valid_mdb s" "valid_list s"
  shows "descendants_of child (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 last_child_None_empty_desc
              split: if_split_asm) 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(simp) using assms apply(simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of child (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> descendants_of child (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> descendants_of child (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> descendants_of child (cdt s) = {}; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> descendants_of child (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> descendants_of child (cdt s) = {}; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> descendants_of child (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> descendants_of child (cdt s) = {}; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y = child\<rbrakk> \<Longrightarrow> descendants_of child (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> descendants_of child (cdt s) = {}; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> descendants_of child (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> descendants_of child (cdt s) = {}; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> descendants_of child (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> descendants_of child (cdt s) = {}; last_last_child x (cdt_list s) = Some child; valid_mdb s; valid_list s; y \<noteq> child\<rbrakk> \<Longrightarrow> descendants_of child (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; descendants_of child (cdt s) = {}\<rbrakk> \<Longrightarrow> descendants_of child (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; descendants_of child (cdt s) = {}\<rbrakk> \<Longrightarrow> descendants_of child (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; descendants_of child (cdt s) = {}\<rbrakk> \<Longrightarrow> descendants_of child (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; descendants_of child (cdt s) = {}\<rbrakk> \<Longrightarrow> descendants_of child (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!