theory Deterministic_AI

lemma (in mdb_empty_abs') next_sib_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_sib p (t(slot := [])) n
    = (if m p = Some slot then None
      else next_sib p t m)" apply(simp, intro conjI impI) apply(rule next_sib_NoneI) apply(simp add: n_def) apply(case_tac "next_sib p t m") apply(simp) apply(drule next_sib_NoneD) apply(erule disjE) apply(rule next_sib_NoneI) apply(simp add: n_def) apply(elim exE conjE) apply(rule next_sib_NoneI) apply(rule disjI2) apply(fastforce simp: n_def) apply(fastforce dest: next_sibD intro: next_sibI simp: n_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = (if m p = Some slot then None else next_sib p t m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; m p = Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 2. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; m p = Some slot\<rbrakk> \<Longrightarrow> n p = None \<or> n p = Some ?p7 \<and> after_in_list ((t(slot := [])) ?p7) p = None
 2. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = next_sib p t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; next_sib p t m = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = next_sib p t m
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; next_sib p t m = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; m p = None \<or> (\<exists>pa. m p = Some pa \<and> after_in_list (t pa) p = None)\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; m p = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 2. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; \<exists>pa. m p = Some pa \<and> after_in_list (t pa) p = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = next_sib p t m proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; m p = None\<rbrakk> \<Longrightarrow> n p = None \<or> n p = Some ?p21 \<and> after_in_list ((t(slot := [])) ?p21) p = None
 2. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; \<exists>pa. m p = Some pa \<and> after_in_list (t pa) p = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 3. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; \<exists>pa. m p = Some pa \<and> after_in_list (t pa) p = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; m p = Some pa; after_in_list (t pa) p = None\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; m p = Some pa; after_in_list (t pa) p = None\<rbrakk> \<Longrightarrow> n p = None \<or> n p = Some (?p31 pa) \<and> after_in_list ((t(slot := [])) (?p31 pa)) p = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = next_sib p t m proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; m p = Some pa; after_in_list (t pa) p = None\<rbrakk> \<Longrightarrow> n p = Some (?p31 pa) \<and> after_in_list ((t(slot := [])) (?p31 pa)) p = None
 2. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = next_sib p t m proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_list_2 t m; m slot = None; m p \<noteq> Some slot; next_sib p t m = Some a\<rbrakk> \<Longrightarrow> next_sib p (t(slot := [])) n = next_sib p t m proof (prove)
goal:
No subgoals!