theory Deterministic_AI

lemma next_not_child:
  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]]
  assumes misc: "valid_list_2 t m" "m src = Some src_p"
  shows
  "next_not_child p (t(src_p := list_replace (t src_p) src dest, 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 (insert misc) apply (insert src_loop_facts[where src_p=src_p],simp split del: if_split) apply (induct p rule: next_not_child_pinduct[where t=t and m=m, OF _ findepth]) apply (case_tac "m slot") apply (rule next_not_child_helper',(simp split del: if_split)+) apply (drule_tac x=a in meta_spec) apply (simp split del: if_split) apply (case_tac "next_sib slot t m") apply (rule next_not_child_helper''',(simp split del: if_split)+) apply (rule next_not_child_helper'',(simp split del: if_split)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_not_child p (t(src_p := list_replace (t src_p) src dest, 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. \<lbrakk>valid_list_2 t m; m src = Some src_p\<rbrakk> \<Longrightarrow> next_not_child p (t(src_p := list_replace (t src_p) src dest, 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. \<lbrakk>valid_list_2 t m; m src = Some src_p; m src_p \<noteq> Some src; src_p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child p (t(src_p := list_replace (t src_p) src dest, 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 = Some src_p; m src_p \<noteq> Some src; src_p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child a (t(src_p := list_replace (t src_p) src dest, 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 = Some src_p; m src_p \<noteq> Some src; src_p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, 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 = Some src_p; m src_p \<noteq> Some src; src_p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child a (t(src_p := list_replace (t src_p) src dest, 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 = Some src_p; m src_p \<noteq> Some src; src_p \<noteq> src; m slot = None\<rbrakk> \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, 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 = Some src_p; m src_p \<noteq> Some src; src_p \<noteq> src\<rbrakk> \<Longrightarrow> next_not_child a (t(src_p := list_replace (t src_p) src dest, 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 = Some src_p; m src_p \<noteq> Some src; src_p \<noteq> src; m slot = Some a\<rbrakk> \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, 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>aa. \<lbrakk>next_sib slot t m = None; a = aa\<rbrakk> \<Longrightarrow> next_not_child aa (t(src_p := list_replace (t src_p) src dest, src := [], dest := t src)) m' = (if aa = src then None else if aa = dest then next_not_child src t m else if next_not_child aa t m = Some src then Some dest else next_not_child aa t m); valid_list_2 t m; m src = Some src_p; m src_p \<noteq> Some src; src_p \<noteq> src; m slot = Some a\<rbrakk> \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, 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>valid_list_2 t m; m src = Some src_p; m src_p \<noteq> Some src; src_p \<noteq> src; m slot = Some a; \<lbrakk>next_sib slot t m = None; a = a\<rbrakk> \<Longrightarrow> next_not_child a (t(src_p := list_replace (t src_p) src dest, 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_p := list_replace (t src_p) src dest, 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>valid_list_2 t m; m src = Some src_p; m src_p \<noteq> Some src; src_p \<noteq> src; m slot = Some a; next_sib slot t m = None \<Longrightarrow> next_not_child a (t(src_p := list_replace (t src_p) src dest, 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_p := list_replace (t src_p) src dest, 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 = Some src_p; m src_p \<noteq> Some src; src_p \<noteq> src; m slot = Some a; next_sib slot t m = None \<Longrightarrow> next_not_child a (t(src_p := list_replace (t src_p) src dest, 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); next_sib slot t m = None\<rbrakk> \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, 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>valid_list_2 t m; m src = Some src_p; m src_p \<noteq> Some src; src_p \<noteq> src; m slot = Some a; next_sib slot t m = None \<Longrightarrow> next_not_child a (t(src_p := list_replace (t src_p) src dest, 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); next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, 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 = Some src_p; m src_p \<noteq> Some src; src_p \<noteq> src; m slot = Some a; next_sib slot t m = Some aa\<rbrakk> \<Longrightarrow> next_not_child slot (t(src_p := list_replace (t src_p) src dest, 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:
No subgoals!