theory Deterministic_AI

lemma (in mdb_empty_abs') next_slot_no_parent:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m\<rbrakk>
    \<Longrightarrow> next_slot p (t(slot := [])) n
     = (if p = slot then None
       else if (\<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot)
         then None
       else next_slot p t m)" apply(case_tac "p=slot") apply(simp add: next_slot_def next_not_child_no_parent) apply(rule impI) apply(simp add: next_not_child_termination next_sib_def) apply(case_tac "\<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot") apply(simp add: next_slot_def) apply(intro conjI impI) apply(elim exE conjE) apply(simp split: if_split_asm) apply(drule(1) next_childD) apply(simp) apply(simp add: next_not_child_no_parent) apply(simp only:, simp) apply(simp add: next_slot_def next_child_no_parent next_not_child_no_parent) apply(fastforce split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p = slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m)
 2. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p = slot\<rbrakk> \<Longrightarrow> (\<forall>sl. next_not_child slot t m = Some sl \<longrightarrow> m sl \<noteq> Some slot) \<longrightarrow> next_not_child slot t m = None
 2. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p = slot; \<forall>sl. next_not_child slot t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_not_child slot t m = None
 2. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m)
 2. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<nexists>sl. next_slot p t m = Some sl \<and> m sl = Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<exists>sl. (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some sl \<and> m sl = Some slot\<rbrakk> \<Longrightarrow> (t p \<noteq> [] \<longrightarrow> next_child p (t(slot := [])) = None) \<and> (t p = [] \<longrightarrow> next_not_child p (t(slot := [])) n = None)
 2. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<nexists>sl. next_slot p t m = Some sl \<and> m sl = Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<exists>sl. (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some sl \<and> m sl = Some slot; t p \<noteq> []\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = None
 2. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<exists>sl. (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some sl \<and> m sl = Some slot; t p = []\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = None
 3. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<nexists>sl. next_slot p t m = Some sl \<and> m sl = Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<And>sl. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; t p \<noteq> []; (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some sl; m sl = Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = None
 2. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<exists>sl. (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some sl \<and> m sl = Some slot; t p = []\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = None
 3. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<nexists>sl. next_slot p t m = Some sl \<and> m sl = Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<And>sl. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; t p \<noteq> []; next_child p t = Some sl; m sl = Some slot\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = None
 2. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<exists>sl. (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some sl \<and> m sl = Some slot; t p = []\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = None
 3. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<nexists>sl. next_slot p t m = Some sl \<and> m sl = Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m) proof (prove)
goal (3 subgoals):
 1. \<And>sl. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; t p \<noteq> []; m sl = Some slot; (\<exists>xs. t p = sl # xs) \<and> m sl = Some p\<rbrakk> \<Longrightarrow> next_child p (t(slot := [])) = None
 2. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<exists>sl. (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some sl \<and> m sl = Some slot; t p = []\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = None
 3. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<nexists>sl. next_slot p t m = Some sl \<and> m sl = Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<exists>sl. (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some sl \<and> m sl = Some slot; t p = []\<rbrakk> \<Longrightarrow> next_not_child p (t(slot := [])) n = None
 2. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<nexists>sl. next_slot p t m = Some sl \<and> m sl = Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<nexists>sl. next_slot p t m = Some sl \<and> m sl = Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = (if p = slot then None else if \<exists>sl. next_slot p t m = Some sl \<and> m sl = Some slot then None else next_slot p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<forall>sl. next_slot p t m = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_slot p (t(slot := [])) n = next_slot p t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = None; no_mloop m; finite_depth m; p \<noteq> slot; \<forall>sl. (if t p \<noteq> [] then next_child p t else next_not_child p t m) = Some sl \<longrightarrow> m sl \<noteq> Some slot\<rbrakk> \<Longrightarrow> (\<exists>sl. next_not_child p t m = Some sl \<and> m sl = Some slot) \<longrightarrow> t p = [] \<longrightarrow> None = next_not_child p t m proof (prove)
goal:
No subgoals!