theory Deterministic_AI

lemma next_not_child_no_parent:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  notes nnext = next_not_child.psimps[OF next_not_child_termination[OF findepth]]
  notes nnext' = next_not_child.psimps[OF next_not_child_termination[OF finite_depth]]
  notes nnext'' = nnext'[simplified m'_def m''_def]
  shows
  "valid_list_2 t m \<Longrightarrow> m src = None
    \<Longrightarrow> next_not_child p (t(src := [], dest := t src)) m'
      = (if p = src then None
         else if p = dest then next_not_child src t m
         else if next_not_child p t m = Some src then Some dest
         else next_not_child p t m)" apply (induct p rule: next_not_child_pinduct[where t=t and m=m, OF _ findepth]) apply (case_tac "m slot") apply (subst next_not_child_root[OF findepth],assumption)+ apply (subst next_not_child_root[OF finite_depth]) apply ((simp add: m'_def m''_def)+)[2] apply (case_tac "next_sib slot t m") apply (drule_tac x="a" in meta_spec) apply (simp add: m'_def m''_def next_sib_def nnext nnext'' cong: if_weak_cong split: if_split_asm) apply (simp split del: if_split) apply (simp add: m'_def m''_def next_sib_def nnext nnext'' cong: if_weak_cong split: if_split_asm | intro impI conjI)+ apply (simp add: valid_list_2_def | drule after_in_list_in_list | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child p (t(src := [], dest := t src)) m' = (if p = src then None else if p = dest then next_not_child src t m else if next_not_child p t m = Some src then Some dest else next_not_child p t m) proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child a (t(src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child slot (t(src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m) proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child a (t(src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); valid_list_2 t m; m src = None; m slot = None\<rbrakk> \<Longrightarrow> next_not_child slot (t(src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m)
 2. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child a (t(src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); valid_list_2 t m; m src = None; m slot = Some a\<rbrakk> \<Longrightarrow> next_not_child slot (t(src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m) proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child a (t(src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); valid_list_2 t m; m src = None; m slot = None\<rbrakk> \<Longrightarrow> next_not_child slot (t(src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then None else if None = Some src then Some dest else None)
 2. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child a (t(src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); valid_list_2 t m; m src = None; m slot = Some a\<rbrakk> \<Longrightarrow> next_not_child slot (t(src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m) proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child a (t(src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); valid_list_2 t m; m src = None; m slot = None\<rbrakk> \<Longrightarrow> m' slot = None
 2. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child a (t(src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); valid_list_2 t m; m src = None; m slot = None\<rbrakk> \<Longrightarrow> None = (if slot = src then None else if slot = dest then None else if None = Some src then Some dest else None)
 3. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child a (t(src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); valid_list_2 t m; m src = None; m slot = Some a\<rbrakk> \<Longrightarrow> next_not_child slot (t(src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m) proof (prove)
goal (1 subgoal):
 1. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child a (t(src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); valid_list_2 t m; m src = None; m slot = Some a\<rbrakk> \<Longrightarrow> next_not_child slot (t(src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m) proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child a (t(src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); valid_list_2 t m; m src = None; m slot = Some a; next_sib slot t m = None\<rbrakk> \<Longrightarrow> next_not_child slot (t(src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m)
 2. \<And>slot a aa. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child a (t(src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); valid_list_2 t m; m src = None; m slot = Some a; next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child slot (t(src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m) proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>valid_list_2 t m; m src = None; m slot = Some a; next_sib slot t m = None; \<lbrakk>next_sib slot t m = None; m slot = Some a; valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child a (t(src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m)\<rbrakk> \<Longrightarrow> next_not_child slot (t(src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m)
 2. \<And>slot a aa. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child a (t(src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); valid_list_2 t m; m src = None; m slot = Some a; next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child slot (t(src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m) proof (prove)
goal (1 subgoal):
 1. \<And>slot a aa. \<lbrakk>\<And>a. \<lbrakk>next_sib slot t m = None; m slot = Some a; valid_list_2 t m; m src = None\<rbrakk> \<Longrightarrow> next_not_child a (t(src := [], dest := t src)) m' = (if a = src then None else if a = dest then next_not_child src t m else if next_not_child a t m = Some src then Some dest else next_not_child a t m); valid_list_2 t m; m src = None; m slot = Some a; next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child slot (t(src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m) proof (prove)
goal (1 subgoal):
 1. \<And>slot a aa. \<lbrakk>valid_list_2 t m; m src = None; m slot = Some a; next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child slot (t(src := [], dest := t src)) m' = (if slot = src then None else if slot = dest then next_not_child src t m else if next_not_child slot t m = Some src then Some dest else next_not_child slot t m) proof (prove)
goal (3 subgoals):
 1. \<And>slot a aa. \<lbrakk>valid_list_2 t m; m src = None; m slot = Some src; after_in_list (t src) slot = Some src; slot \<noteq> dest; a = src; aa = src; slot \<noteq> src\<rbrakk> \<Longrightarrow> False
 2. \<And>slot a aa. \<lbrakk>valid_list_2 t m; m src = None; m slot = Some a; after_in_list (t a) slot = Some aa; a \<noteq> dest; slot \<noteq> dest; a = src; \<exists>y. after_in_list (t src) slot = Some y; aa \<noteq> src; slot \<noteq> src\<rbrakk> \<Longrightarrow> after_in_list (t src) slot = Some aa
 3. \<And>slot a aa. \<lbrakk>valid_list_2 t m; m src = None; m slot = Some a; after_in_list (t a) slot = Some aa; a \<noteq> dest; slot \<noteq> dest; a \<noteq> src; aa = src\<rbrakk> \<Longrightarrow> slot = src proof (prove)
goal:
No subgoals!