theory Deterministic_AI

lemma (in mdb_empty_abs') next_child:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>valid_list_2 t m; m slot = Some slot_p\<rbrakk>
    \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := []))
     = (if p = slot then None
       else if next_child p t = Some slot then
         if t slot = [] then
           if t p = [slot] then None
           else if hd (t p) = slot then after_in_list (t p) slot
           else Some (hd (t p))
         else next_child slot t
       else next_child p t)" apply(case_tac "p=slot") apply(fastforce intro: next_child_NoneI dest: next_child_NoneD) apply(case_tac "next_child p t = Some slot") apply(simp split del: if_split) apply(drule(1) next_childD) apply(elim exE conjE) apply(case_tac "t slot") apply(simp) apply(intro conjI impI) apply(rule next_child_NoneI) apply(simp) apply(case_tac xs, simp, simp) apply(rule next_childI) apply(simp) apply(simp) apply(fastforce simp: next_child_def intro: next_childI next_child_NoneI) apply(simp) apply(case_tac "next_child p t") apply(simp) apply(drule next_child_NoneD) apply(rule next_child_NoneI) apply(fastforce) apply(simp) apply(fastforce intro: next_childI dest: next_childD simp: next_child_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p = slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t = Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t = Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; (\<exists>xs. t p = slot # xs) \<and> m slot = Some p\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m slot = Some p; t p = slot # xs\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (3 subgoals):
 1. \<And>xs. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m slot = Some p; t p = slot # xs; t slot = []\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t)
 2. \<And>xs a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m slot = Some p; t p = slot # xs; t slot = a # list\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (3 subgoals):
 1. \<And>xs. \<lbrakk>valid_list_2 t m; p = slot_p; slot_p \<noteq> slot; m slot = Some slot_p; t slot_p = slot # xs; t slot = []\<rbrakk> \<Longrightarrow> (xs = [] \<longrightarrow> next_child slot_p (t(slot_p := [], slot := [])) = None) \<and> (xs \<noteq> [] \<longrightarrow> next_child slot_p (t(slot_p := xs, slot := [])) = after_in_list (slot # xs) slot)
 2. \<And>xs a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m slot = Some p; t p = slot # xs; t slot = a # list\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (4 subgoals):
 1. \<And>xs. \<lbrakk>valid_list_2 t m; p = slot_p; slot_p \<noteq> slot; m slot = Some slot_p; t slot_p = slot # xs; t slot = []; xs = []\<rbrakk> \<Longrightarrow> next_child slot_p (t(slot_p := [], slot := [])) = None
 2. \<And>xs. \<lbrakk>valid_list_2 t m; p = slot_p; slot_p \<noteq> slot; m slot = Some slot_p; t slot_p = slot # xs; t slot = []; xs \<noteq> []\<rbrakk> \<Longrightarrow> next_child slot_p (t(slot_p := xs, slot := [])) = after_in_list (slot # xs) slot
 3. \<And>xs a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m slot = Some p; t p = slot # xs; t slot = a # list\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (4 subgoals):
 1. \<And>xs. \<lbrakk>valid_list_2 t m; p = slot_p; slot_p \<noteq> slot; m slot = Some slot_p; t slot_p = slot # xs; t slot = []; xs = []\<rbrakk> \<Longrightarrow> (t(slot_p := [], slot := [])) slot_p = []
 2. \<And>xs. \<lbrakk>valid_list_2 t m; p = slot_p; slot_p \<noteq> slot; m slot = Some slot_p; t slot_p = slot # xs; t slot = []; xs \<noteq> []\<rbrakk> \<Longrightarrow> next_child slot_p (t(slot_p := xs, slot := [])) = after_in_list (slot # xs) slot
 3. \<And>xs a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m slot = Some p; t p = slot # xs; t slot = a # list\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t)
 4. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (3 subgoals):
 1. \<And>xs. \<lbrakk>valid_list_2 t m; p = slot_p; slot_p \<noteq> slot; m slot = Some slot_p; t slot_p = slot # xs; t slot = []; xs \<noteq> []\<rbrakk> \<Longrightarrow> next_child slot_p (t(slot_p := xs, slot := [])) = after_in_list (slot # xs) slot
 2. \<And>xs a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m slot = Some p; t p = slot # xs; t slot = a # list\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (3 subgoals):
 1. \<And>xs a list. \<lbrakk>valid_list_2 t m; p = slot_p; slot_p \<noteq> slot; m slot = Some slot_p; t slot_p = slot # a # list; t slot = []; xs = a # list\<rbrakk> \<Longrightarrow> next_child slot_p (t(slot_p := a # list, slot := [])) = Some a
 2. \<And>xs a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m slot = Some p; t p = slot # xs; t slot = a # list\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (3 subgoals):
 1. \<And>xs a list. \<lbrakk>valid_list_2 t m; p = slot_p; slot_p \<noteq> slot; m slot = Some slot_p; t slot_p = slot # a # list; t slot = []; xs = a # list\<rbrakk> \<Longrightarrow> (t(slot_p := a # list, slot := [])) slot_p = a # ?xs33 xs a list
 2. \<And>xs a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m slot = Some p; t p = slot # xs; t slot = a # list\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t)
 3. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (2 subgoals):
 1. \<And>xs a list. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; m slot = Some p; t p = slot # xs; t slot = a # list\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t)
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (2 subgoals):
 1. \<And>xs a list. \<lbrakk>valid_list_2 t m; p = slot_p; slot_p \<noteq> slot; m slot = Some slot_p; t slot_p = slot # xs; t slot = a # list\<rbrakk> \<Longrightarrow> next_child slot_p (t(slot_p := a # list @ xs, slot := [])) = next_child slot t
 2. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = (if p = slot then None else if next_child p t = Some slot then if t slot = [] then if t p = [slot] then None else if hd (t p) = slot then after_in_list (t p) slot else Some (hd (t p)) else next_child slot t else next_child p t) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = next_child p t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot; next_child p t = None\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = next_child p t
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot; next_child p t = Some a\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = next_child p t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t = None\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot; next_child p t = Some a\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = next_child p t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t p = []\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot; next_child p t = Some a\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = next_child p t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; t p = []\<rbrakk> \<Longrightarrow> (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) p = []
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot; next_child p t = Some a\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = next_child p t proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; next_child p t \<noteq> Some slot; next_child p t = Some a\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = next_child p t proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = Some slot_p; p \<noteq> slot; a \<noteq> slot; next_child p t = Some a\<rbrakk> \<Longrightarrow> next_child p (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) = Some a proof (prove)
goal:
No subgoals!