theory Deterministic_AI

lemma next_not_child_pinduct2':
  "\<lbrakk>next_not_child_dom (p, t, m);
  \<And>a slot. \<lbrakk>next_sib a t m = None; m a = Some slot; P a\<rbrakk> \<Longrightarrow> P slot;
  next_not_child p t m = Some n; P p;
  \<forall>a slot. next_sib a t m = Some slot \<longrightarrow> P slot\<rbrakk>
    \<Longrightarrow> P n" apply(induct rule: next_not_child.pinduct) apply(simp split: if_split_asm del: split_paired_All) apply(case_tac "m slot") apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_not_child_dom (p, t, m); \<And>a slot. \<lbrakk>next_sib a t m = None; m a = Some slot; P a\<rbrakk> \<Longrightarrow> P slot; next_not_child p t m = Some n; P p; \<forall>a slot. next_sib a t m = Some slot \<longrightarrow> P slot\<rbrakk> \<Longrightarrow> P n proof (prove)
goal (1 subgoal):
 1. \<And>slot t m. \<lbrakk>next_not_child_dom (slot, t, m); \<And>x2. \<lbrakk>next_sib slot t m = None; m slot = Some x2; \<And>a slot. \<lbrakk>next_sib a t m = None; m a = Some slot; P a\<rbrakk> \<Longrightarrow> P slot; next_not_child x2 t m = Some n; P x2; \<forall>a slot. next_sib a t m = Some slot \<longrightarrow> P slot\<rbrakk> \<Longrightarrow> P n; \<And>a slot. \<lbrakk>next_sib a t m = None; m a = Some slot; P a\<rbrakk> \<Longrightarrow> P slot; next_not_child slot t m = Some n; P slot; \<forall>a slot. next_sib a t m = Some slot \<longrightarrow> P slot\<rbrakk> \<Longrightarrow> P n proof (prove)
goal (1 subgoal):
 1. \<And>slot t m. \<lbrakk>P slot; \<forall>a slot. next_sib a t m = Some slot \<longrightarrow> P slot; next_not_child_dom (slot, t, m); \<And>x2. \<lbrakk>m slot = Some x2; next_not_child x2 t m = Some n\<rbrakk> \<Longrightarrow> P n; \<And>a slot. \<lbrakk>next_sib a t m = None; m a = Some slot; P a\<rbrakk> \<Longrightarrow> P slot; next_sib slot t m = None; (case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m) = Some n\<rbrakk> \<Longrightarrow> P n proof (prove)
goal (2 subgoals):
 1. \<And>slot t m. \<lbrakk>P slot; \<forall>a slot. next_sib a t m = Some slot \<longrightarrow> P slot; next_not_child_dom (slot, t, m); \<And>x2. \<lbrakk>m slot = Some x2; next_not_child x2 t m = Some n\<rbrakk> \<Longrightarrow> P n; \<And>a slot. \<lbrakk>next_sib a t m = None; m a = Some slot; P a\<rbrakk> \<Longrightarrow> P slot; next_sib slot t m = None; (case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m) = Some n; m slot = None\<rbrakk> \<Longrightarrow> P n
 2. \<And>slot t m a. \<lbrakk>P slot; \<forall>a slot. next_sib a t m = Some slot \<longrightarrow> P slot; next_not_child_dom (slot, t, m); \<And>x2. \<lbrakk>m slot = Some x2; next_not_child x2 t m = Some n\<rbrakk> \<Longrightarrow> P n; \<And>a slot. \<lbrakk>next_sib a t m = None; m a = Some slot; P a\<rbrakk> \<Longrightarrow> P slot; next_sib slot t m = None; (case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m) = Some n; m slot = Some a\<rbrakk> \<Longrightarrow> P n proof (prove)
goal (1 subgoal):
 1. \<And>slot t m a. \<lbrakk>P slot; \<forall>a slot. next_sib a t m = Some slot \<longrightarrow> P slot; next_not_child_dom (slot, t, m); \<And>x2. \<lbrakk>m slot = Some x2; next_not_child x2 t m = Some n\<rbrakk> \<Longrightarrow> P n; \<And>a slot. \<lbrakk>next_sib a t m = None; m a = Some slot; P a\<rbrakk> \<Longrightarrow> P slot; next_sib slot t m = None; (case m slot of None \<Rightarrow> None | Some p \<Rightarrow> next_not_child p t m) = Some n; m slot = Some a\<rbrakk> \<Longrightarrow> P n proof (prove)
goal:
No subgoals!