theory Deterministic_AI

lemma next_sib:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "valid_list_2 t m \<Longrightarrow> m src = Some src_p
    \<Longrightarrow> next_sib 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_sib src t m
         else if next_sib p t m = Some src then Some dest
         else next_sib p t m)" apply (simp add: next_sib_def m'_def m''_def split: if_split) apply (intro impI conjI) apply (intro impI | simp split: option.splits  | drule(1) valid_list_2D[OF _ after_in_list_in_list] | rule after_in_list_list_replace | rule replace_list_preserve_after replace_list_preserve_after' | simp add: valid_list_2_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p\<rbrakk> \<Longrightarrow> next_sib 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_sib src t m else if next_sib p t m = Some src then Some dest else next_sib p t m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p\<rbrakk> \<Longrightarrow> (m p = Some src \<longrightarrow> (src_p = dest \<longrightarrow> (after_in_list (t src) p = Some src \<longrightarrow> (p = dest \<longrightarrow> after_in_list (t src) dest = after_in_list (t dest) src) \<and> (p \<noteq> dest \<longrightarrow> p = src)) \<and> (after_in_list (t src) p \<noteq> Some src \<longrightarrow> p = dest \<longrightarrow> after_in_list (t src) dest = after_in_list (t dest) src)) \<and> (src_p \<noteq> dest \<longrightarrow> (src_p = src \<longrightarrow> (after_in_list (t src) p = Some src \<longrightarrow> (p = dest \<longrightarrow> after_in_list (t src) dest = after_in_list (t src) src) \<and> (p \<noteq> dest \<longrightarrow> p = src)) \<and> (after_in_list (t src) p \<noteq> Some src \<longrightarrow> p = dest \<longrightarrow> after_in_list (t src) dest = after_in_list (t src) src)) \<and> (src_p \<noteq> src \<longrightarrow> (after_in_list (t src) p = Some src \<longrightarrow> (p = dest \<longrightarrow> after_in_list (list_replace (t src_p) src dest) dest = after_in_list (t src_p) src) \<and> (p \<noteq> dest \<longrightarrow> p = src)) \<and> (after_in_list (t src) p \<noteq> Some src \<longrightarrow> p = dest \<longrightarrow> after_in_list (list_replace (t src_p) src dest) dest = after_in_list (t src_p) src)))) \<and> (m p \<noteq> Some src \<longrightarrow> (src_p = dest \<longrightarrow> ((case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) = Some src \<longrightarrow> (p = dest \<longrightarrow> after_in_list (t src) dest = after_in_list (t dest) src) \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (if pa = dest then t src else if pa = src then [] else t pa) p) = Some dest)) \<and> ((case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> after_in_list (t src) dest = after_in_list (t dest) src) \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (if pa = dest then t src else if pa = src then [] else t pa) p) = (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p)))) \<and> (src_p \<noteq> dest \<longrightarrow> (src_p = src \<longrightarrow> ((case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) = Some src \<longrightarrow> (p = dest \<longrightarrow> after_in_list (t src) dest = after_in_list (t src) src) \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (if pa = dest then t src else if pa = src then [] else t pa) p) = Some dest)) \<and> ((case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> after_in_list (t src) dest = after_in_list (t src) src) \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (if pa = dest then t src else if pa = src then [] else t pa) p) = (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p)))) \<and> (src_p \<noteq> src \<longrightarrow> ((case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) = Some src \<longrightarrow> (p = dest \<longrightarrow> after_in_list (list_replace (t src_p) src dest) dest = after_in_list (t src_p) src) \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (if pa = dest then t src else if pa = src then [] else if pa = src_p then list_replace (t src_p) src dest else t pa) p) = Some dest)) \<and> ((case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) \<noteq> Some src \<longrightarrow> (p = dest \<longrightarrow> after_in_list (list_replace (t src_p) src dest) dest = after_in_list (t src_p) src) \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (if pa = dest then t src else if pa = src then [] else if pa = src_p then list_replace (t src_p) src dest else t pa) p) = (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p)))))) proof (prove)
goal (21 subgoals):
 1. \<lbrakk>valid_list_2 t m; m src = Some src_p; m p = Some src; src_p = dest; after_in_list (t src) p = Some src; p = dest\<rbrakk> \<Longrightarrow> after_in_list (t src) dest = after_in_list (t dest) src
 2. \<lbrakk>valid_list_2 t m; m src = Some src_p; m p = Some src; src_p = dest; after_in_list (t src) p = Some src; p \<noteq> dest\<rbrakk> \<Longrightarrow> p = src
 3. \<lbrakk>valid_list_2 t m; m src = Some src_p; m p = Some src; src_p = dest; after_in_list (t src) p \<noteq> Some src; p = dest\<rbrakk> \<Longrightarrow> after_in_list (t src) dest = after_in_list (t dest) src
 4. \<lbrakk>valid_list_2 t m; m src = Some src_p; m p = Some src; src_p \<noteq> dest; src_p = src; after_in_list (t src) p = Some src; p = dest\<rbrakk> \<Longrightarrow> after_in_list (t src) dest = after_in_list (t src) src
 5. \<lbrakk>valid_list_2 t m; m src = Some src_p; m p = Some src; src_p \<noteq> dest; src_p = src; after_in_list (t src) p = Some src; p \<noteq> dest\<rbrakk> \<Longrightarrow> p = src
 6. \<lbrakk>valid_list_2 t m; m src = Some src_p; m p = Some src; src_p \<noteq> dest; src_p = src; after_in_list (t src) p \<noteq> Some src; p = dest\<rbrakk> \<Longrightarrow> after_in_list (t src) dest = after_in_list (t src) src
 7. \<lbrakk>valid_list_2 t m; m src = Some src_p; m p = Some src; src_p \<noteq> dest; src_p \<noteq> src; after_in_list (t src) p = Some src; p = dest\<rbrakk> \<Longrightarrow> after_in_list (list_replace (t src_p) src dest) dest = after_in_list (t src_p) src
 8. \<lbrakk>valid_list_2 t m; m src = Some src_p; m p = Some src; src_p \<noteq> dest; src_p \<noteq> src; after_in_list (t src) p = Some src; p \<noteq> dest\<rbrakk> \<Longrightarrow> p = src
 9. \<lbrakk>valid_list_2 t m; m src = Some src_p; m p = Some src; src_p \<noteq> dest; src_p \<noteq> src; after_in_list (t src) p \<noteq> Some src; p = dest\<rbrakk> \<Longrightarrow> after_in_list (list_replace (t src_p) src dest) dest = after_in_list (t src_p) src
 10. \<lbrakk>valid_list_2 t m; m src = Some src_p; m p \<noteq> Some src; src_p = dest; (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) = Some src; p = dest\<rbrakk> \<Longrightarrow> after_in_list (t src) dest = after_in_list (t dest) src
A total of 21 subgoals... proof (prove)
goal:
No subgoals!