theory Deterministic_AI

lemma valid_list_post:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  notes parency_antisym[where x=src and y = dest,simp]
  notes parent_not_next_child[simp]
  shows "valid_list_2 t' n" proof - from valid_list show ?thesis apply (simp add: t'_def t''_def n_def n'_def cong: option.case_cong) by (simp add: replace_distinct[OF parent_not_next_child]
                     replace_distinct list_replace_set
                     list_swap_both insert_Collect remove_collect
                     swap_distinct
           | intro impI conjI iffI allI
           | (intro impI conjI iffI notI,simp_all)
           | rule Collect_cong
           | simp split: option.splits
           | (rule ccontr,simp,elim impE,rule notI)
           | simp only: valid_list_2_def  )+  (*slow*)
 qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_list_2 t' n proof (state)
goal (1 subgoal):
 1. valid_list_2 t' n proof (chain)
picking this:
valid_list_2 t m proof (prove)
using this:
valid_list_2 t m

goal (1 subgoal):
 1. valid_list_2 t' n proof (prove)
goal (1 subgoal):
 1. valid_list_2 t m \<Longrightarrow> (m dest = Some src \<longrightarrow> (m src = Some dest \<longrightarrow> valid_list_2 (t(dest := t src, src := list_swap (t dest) src dest)) ((\<lambda>n. if m n = Some src then Some dest else if m n = Some dest then Some src else m n)(src \<mapsto> src, dest \<mapsto> src))) \<and> (m src \<noteq> Some dest \<longrightarrow> valid_list_2 (case m src of None \<Rightarrow> t(src := t dest, dest := list_replace (t src) dest src) | Some dest_p \<Rightarrow> if dest = dest_p then t(src := t dest_p, dest_p := list_swap (t src) src dest_p) else t(src := t dest, dest := list_replace (t src) dest src, dest_p := list_replace (if dest_p = src then t dest else t dest_p) src dest)) ((\<lambda>n. if m n = Some src then Some dest else if m n = Some dest then Some src else m n)(src \<mapsto> dest, dest := m src)))) \<and> (m dest \<noteq> Some src \<longrightarrow> (m src = Some dest \<longrightarrow> valid_list_2 (case m dest of None \<Rightarrow> t(dest := t src, src := list_replace (t dest) src dest) | Some src_p \<Rightarrow> if src_p = src then t(dest := t src, src := list_swap (t dest) src dest) else t(dest := t src, src_p := list_replace (if src_p = dest then t src else t src_p) dest src, src := list_replace (t dest) src dest)) ((\<lambda>n. if m n = Some src then Some dest else if m n = Some dest then Some src else m n)(src := m dest, dest \<mapsto> src))) \<and> (m src \<noteq> Some dest \<longrightarrow> valid_list_2 (case m dest of None \<Rightarrow> case m src of None \<Rightarrow> t(src := t dest, dest := t src) | Some dest_p \<Rightarrow> t(src := t dest, dest := t src, dest_p := list_replace (if dest_p = dest then t src else if dest_p = src then t dest else t dest_p) src dest) | Some src_p \<Rightarrow> case m src of None \<Rightarrow> t(src := t dest, dest := t src, src_p := list_replace (if src_p = dest then t src else if src_p = src then t dest else t src_p) dest src) | Some dest_p \<Rightarrow> if src_p = dest_p then t(src := t dest, dest := t src, dest_p := list_swap (if dest_p = dest then t src else if dest_p = src then t dest else t dest_p) src dest) else t(src := t dest, dest := t src, src_p := list_replace (if src_p = dest then t src else if src_p = src then t dest else t src_p) dest src, dest_p := list_replace (if dest_p = dest then t src else if dest_p = src then t dest else t dest_p) src dest)) ((\<lambda>n. if m n = Some src then Some dest else if m n = Some dest then Some src else m n)(src := m dest, dest := m src)))) proof (state)
this:
valid_list_2 t' n

goal:
No subgoals! proof (state)
this:
valid_list_2 t' n

goal:
No subgoals!