theory Deterministic_AI

lemma next_sib:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  notes parency_antisym[where x=src and y = dest,simp]
  notes next_sib_antisym[where x=src and y = dest,simp]
  notes distinct_after_in_list_not_self[OF t_distinct,simp]
  notes rdefs = t'_def t''_def n_def n'_def
  notes parent_not_next_child[simp]
  shows
  "next_sib p t' n
    = (if p = src then
        (if next_sib dest t m = Some src then Some dest
         else next_sib dest t m)
      else if p = dest then
        (if next_sib src t m = Some dest then Some src
         else next_sib src t m)
      else if next_sib p t m = Some src then Some dest
      else if next_sib p t m = Some dest then Some src
      else next_sib p t m)" apply simp apply (intro impI conjI allI,simp_all) by ((intro impI conjI allI
   | drule next_sib_NoneD next_sibD'
   | simp add: next_sib_def rdefs split: option.splits
   | simp add: after_in_list_append_notin_hd replace_list_preserve_after replace_list_preserve_after'
               list_swap_preservation_t replace_distinct swap_distinct
   | rule after_in_list_list_replace
   | drule optionD after_in_listD'
   | elim exE conjE disjE | force )+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_sib p t' n = (if p = src then if next_sib dest t m = Some src then Some dest else next_sib dest t m else if p = dest then if next_sib src t m = Some dest then Some src else next_sib src t m else if next_sib p t m = Some src then Some dest else if next_sib p t m = Some dest then Some src else next_sib p t m) proof (prove)
goal (1 subgoal):
 1. (next_sib dest t m = Some src \<longrightarrow> (next_sib p t m = Some dest \<longrightarrow> (next_sib src t m = Some dest \<longrightarrow> (p = dest \<longrightarrow> next_sib dest t' n = Some src) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_sib src t' n = Some src) \<and> (p \<noteq> src \<longrightarrow> next_sib p t' n = Some src))) \<and> (next_sib src t m \<noteq> Some dest \<longrightarrow> (p = dest \<longrightarrow> next_sib dest t' n = next_sib src t m) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_sib src t' n = Some dest) \<and> (p \<noteq> src \<longrightarrow> next_sib p t' n = Some src)))) \<and> (next_sib p t m \<noteq> Some dest \<longrightarrow> (next_sib p t m = Some src \<longrightarrow> (next_sib src t m = Some dest \<longrightarrow> (p = dest \<longrightarrow> next_sib dest t' n = Some src) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_sib src t' n = Some src) \<and> (p \<noteq> src \<longrightarrow> next_sib p t' n = Some dest))) \<and> (next_sib src t m \<noteq> Some dest \<longrightarrow> (p = dest \<longrightarrow> next_sib dest t' n = next_sib src t m) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_sib src t' n = Some dest) \<and> (p \<noteq> src \<longrightarrow> next_sib p t' n = Some dest)))) \<and> (next_sib p t m \<noteq> Some src \<longrightarrow> (next_sib src t m = Some dest \<longrightarrow> (p = dest \<longrightarrow> next_sib dest t' n = Some src) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_sib src t' n = Some src) \<and> (p \<noteq> src \<longrightarrow> next_sib p t' n = next_sib p t m))) \<and> (next_sib src t m \<noteq> Some dest \<longrightarrow> (p = dest \<longrightarrow> next_sib dest t' n = next_sib src t m) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_sib src t' n = Some dest) \<and> (p \<noteq> src \<longrightarrow> next_sib p t' n = next_sib p t m)))))) \<and> (next_sib dest t m \<noteq> Some src \<longrightarrow> (next_sib p t m = Some dest \<longrightarrow> (next_sib src t m = Some dest \<longrightarrow> (p = dest \<longrightarrow> next_sib dest t' n = Some src) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_sib src t' n = next_sib dest t m) \<and> (p \<noteq> src \<longrightarrow> next_sib p t' n = Some src))) \<and> (next_sib src t m \<noteq> Some dest \<longrightarrow> (p = dest \<longrightarrow> next_sib dest t' n = next_sib src t m) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_sib src t' n = next_sib dest t m) \<and> (p \<noteq> src \<longrightarrow> next_sib p t' n = Some src)))) \<and> (next_sib p t m \<noteq> Some dest \<longrightarrow> (next_sib p t m = Some src \<longrightarrow> (next_sib src t m = Some dest \<longrightarrow> (p = dest \<longrightarrow> next_sib dest t' n = Some src) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_sib src t' n = next_sib dest t m) \<and> (p \<noteq> src \<longrightarrow> next_sib p t' n = Some dest))) \<and> (next_sib src t m \<noteq> Some dest \<longrightarrow> (p = dest \<longrightarrow> next_sib dest t' n = next_sib src t m) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_sib src t' n = next_sib dest t m) \<and> (p \<noteq> src \<longrightarrow> next_sib p t' n = Some dest)))) \<and> (next_sib p t m \<noteq> Some src \<longrightarrow> (next_sib src t m = Some dest \<longrightarrow> (p = dest \<longrightarrow> next_sib dest t' n = Some src) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_sib src t' n = next_sib dest t m) \<and> (p \<noteq> src \<longrightarrow> next_sib p t' n = next_sib p t m))) \<and> (next_sib src t m \<noteq> Some dest \<longrightarrow> (p = dest \<longrightarrow> next_sib dest t' n = next_sib src t m) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> next_sib src t' n = next_sib dest t m) \<and> (p \<noteq> src \<longrightarrow> next_sib p t' n = next_sib p t m)))))) proof (prove)
goal (19 subgoals):
 1. \<lbrakk>next_sib dest t m = Some src; next_sib p t m = Some dest; next_sib src t m \<noteq> Some dest; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_sib p t' n = Some src
 2. \<lbrakk>next_sib dest t m = Some src; next_sib src t m \<noteq> Some dest; p = dest\<rbrakk> \<Longrightarrow> next_sib dest t' n = next_sib src t m
 3. \<lbrakk>next_sib dest t m = Some src; next_sib src t m = Some src; p = src\<rbrakk> \<Longrightarrow> next_sib src t' n = Some dest
 4. \<lbrakk>next_sib dest t m = Some src; next_sib p t m = Some src; next_sib src t m \<noteq> Some dest; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_sib p t' n = Some dest
 5. \<lbrakk>next_sib dest t m = Some src; next_sib src t m \<noteq> Some src; next_sib src t m \<noteq> Some dest; p = src\<rbrakk> \<Longrightarrow> next_sib src t' n = Some dest
 6. \<lbrakk>next_sib dest t m = Some src; next_sib p t m \<noteq> Some dest; next_sib p t m \<noteq> Some src; next_sib src t m \<noteq> Some dest; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_sib p t' n = next_sib p t m
 7. \<lbrakk>next_sib dest t m = Some dest; next_sib src t m = Some dest; p = dest\<rbrakk> \<Longrightarrow> next_sib dest t' n = Some src
 8. \<lbrakk>next_sib src t m = Some dest; p = src\<rbrakk> \<Longrightarrow> next_sib src t' n = next_sib dest t m
 9. \<lbrakk>next_sib p t m = Some dest; next_sib src t m = Some dest; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> next_sib p t' n = Some src
 10. \<lbrakk>next_sib dest t m = Some dest; next_sib src t m \<noteq> Some dest; p = dest\<rbrakk> \<Longrightarrow> next_sib dest t' n = next_sib src t m
A total of 19 subgoals...