theory Deterministic_AI

lemma next_not_child_NoneI':
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  assumes f_d: "finite_depth m"
  shows
  "\<lbrakk>\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None;
    next_sib p t m = None; finite_depth m\<rbrakk>
    \<Longrightarrow> next_not_child p t m = None" apply(induct p rule: next_not_child_pinduct[where t=t and m=m]) apply(simp) apply(case_tac "m slot") apply(simp add: next_not_child_termination) apply(atomize) apply(erule_tac x=a in allE) apply(simp) apply(erule impE) apply(intro allI impI) apply(erule_tac x=q in allE) apply(erule impE) apply(simp add: descendants_of_def cdt_parent_defs) apply(rule_tac b=a in trancl_into_trancl) apply(simp) apply(simp) apply(simp) apply(erule impE) apply(erule_tac x=a in allE) apply(erule impE) apply(fastforce simp: descendants_of_def cdt_parent_defs) apply(simp) apply(subst next_not_child.psimps) apply(simp add: next_not_child_termination) apply(simp) using f_d apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>q. p \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib p t m = None; finite_depth m\<rbrakk> \<Longrightarrow> next_not_child p t m = None proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; \<forall>q. a \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib a t m = None; finite_depth m\<rbrakk> \<Longrightarrow> next_not_child a t m = None; \<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>m slot = Some a; \<forall>q. a \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = None; \<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 2. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>m slot = Some a; \<forall>q. a \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = None; \<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 2. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>m slot = Some a; \<forall>q. a \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = None; \<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 3. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>m slot = Some a; \<forall>q. a \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_not_child a t m = None; \<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>\<forall>a. m slot = Some a \<longrightarrow> (\<forall>q. a \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<longrightarrow> next_sib a t m = None \<longrightarrow> next_not_child a t m = None; \<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; m slot = Some a \<longrightarrow> (\<forall>q. a \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<longrightarrow> next_sib a t m = None \<longrightarrow> next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 2. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; (\<forall>q. a \<in> descendants_of q m \<longrightarrow> next_sib q t m = None) \<longrightarrow> next_sib a t m = None \<longrightarrow> next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 2. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a\<rbrakk> \<Longrightarrow> \<forall>q. a \<in> descendants_of q m \<longrightarrow> next_sib q t m = None
 2. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_sib a t m = None \<longrightarrow> next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 3. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot a q. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; a \<in> descendants_of q m\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_sib a t m = None \<longrightarrow> next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 3. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot a q. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a; a \<in> descendants_of q m; slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_sib a t m = None \<longrightarrow> next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 3. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a q. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a; a \<in> descendants_of q m\<rbrakk> \<Longrightarrow> slot \<in> descendants_of q m
 2. \<And>slot a q. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a; a \<in> descendants_of q m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_sib a t m = None \<longrightarrow> next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 4. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a q. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a; (q, a) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (q, slot) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot a q. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a; a \<in> descendants_of q m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_sib a t m = None \<longrightarrow> next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 4. finite_depth m proof (prove)
goal (5 subgoals):
 1. \<And>slot a q. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a; (q, a) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (q, a) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>slot a q. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a; (q, a) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (a, slot) \<in> {(p, c). m c = Some p}
 3. \<And>slot a q. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a; a \<in> descendants_of q m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 4. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_sib a t m = None \<longrightarrow> next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 5. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a q. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a; (q, a) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> (a, slot) \<in> {(p, c). m c = Some p}
 2. \<And>slot a q. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a; a \<in> descendants_of q m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 3. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_sib a t m = None \<longrightarrow> next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 4. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot a q. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a; a \<in> descendants_of q m; next_sib q t m = None\<rbrakk> \<Longrightarrow> next_sib q t m = None
 2. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_sib a t m = None \<longrightarrow> next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 3. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_sib a t m = None \<longrightarrow> next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 2. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a\<rbrakk> \<Longrightarrow> next_sib a t m = None
 2. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 3. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a; slot \<in> descendants_of a m \<longrightarrow> next_sib a t m = None\<rbrakk> \<Longrightarrow> next_sib a t m = None
 2. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 3. finite_depth m proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a\<rbrakk> \<Longrightarrow> slot \<in> descendants_of a m
 2. \<And>slot a. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_sib a t m = None
 3. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 4. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>next_sib slot t m = None; finite_depth m; m slot = Some a; next_sib a t m = None\<rbrakk> \<Longrightarrow> next_sib a t m = None
 2. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 3. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 2. finite_depth m proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_not_child a t m = None\<rbrakk> \<Longrightarrow> next_not_child_dom (slot, t, m)
 2. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_not_child a t m = None\<rbrakk> \<Longrightarrow> (if next_sib slot t m = None then case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m else next_sib slot t m) = None
 3. finite_depth m proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>\<forall>q. slot \<in> descendants_of q m \<longrightarrow> next_sib q t m = None; next_sib slot t m = None; finite_depth m; m slot = Some a; next_not_child a t m = None\<rbrakk> \<Longrightarrow> (if next_sib slot t m = None then case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m else next_sib slot t m) = None
 2. finite_depth m proof (prove)
goal (1 subgoal):
 1. finite_depth m proof (prove)
using this:
finite_depth m

goal (1 subgoal):
 1. finite_depth m proof (prove)
goal:
No subgoals!