theory Deterministic_AI

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = None\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = (if p = slot then None else next_child p t) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; p = slot\<rbrakk> \<Longrightarrow> next_child slot (t(slot := [])) = None
 2. \<lbrakk>valid_list_2 t m; m slot = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = next_child p t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; p = slot\<rbrakk> \<Longrightarrow> (t(slot := [])) slot = []
 2. \<lbrakk>valid_list_2 t m; m slot = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = next_child p t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = None; p \<noteq> slot\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = next_child p t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; p \<noteq> slot; next_child p t = None\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = next_child p t
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; p \<noteq> slot; next_child p t = Some a\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = next_child p t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; p \<noteq> slot; next_child p t = None\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; p \<noteq> slot; next_child p t = Some a\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = next_child p t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; p \<noteq> slot; t p = []\<rbrakk> \<Longrightarrow> (t(slot := [])) p = []
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; p \<noteq> slot; next_child p t = Some a\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = next_child p t proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; p \<noteq> slot; next_child p t = Some a\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = next_child p t proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; p \<noteq> slot; next_child p t = Some a\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = Some a proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; p \<noteq> slot; (\<exists>xs. t p = a # xs) \<and> m a = Some p\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = Some a proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>valid_list_2 t m; m slot = None; p \<noteq> slot; m a = Some p; t p = a # xs\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = Some a proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>valid_list_2 t m; m slot = None; p \<noteq> slot; m a = Some p; t p = a # xs\<rbrakk> \<Longrightarrow> (t(slot := [])) p = a # ?xs19 a xs proof (prove)
goal:
No subgoals!