theory Deterministic_AI

lemma valid_list_post_parents:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "m src = Some src_p \<Longrightarrow> m dest = Some dest_p \<Longrightarrow> valid_list_2 t' n" apply (insert valid_list) apply (simp add: t'_def t''_def n_def n'_def) apply (intro impI conjI allI) apply (simp add: valid_list_2_def list_swap_def swap_distinct[simplified list_swap_def] list_replace_def replace_distinct[simplified list_replace_def]| intro impI conjI allI | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some src_p; m dest = Some dest_p\<rbrakk> \<Longrightarrow> valid_list_2 t' n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some src_p; m dest = Some dest_p; valid_list_2 t m\<rbrakk> \<Longrightarrow> valid_list_2 t' n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some src_p; m dest = Some dest_p; valid_list_2 t m\<rbrakk> \<Longrightarrow> (dest_p = src_p \<longrightarrow> (src_p = dest \<longrightarrow> (dest = src \<longrightarrow> valid_list_2 t (m(src \<mapsto> src))) \<and> (dest \<noteq> src \<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> (src_p \<noteq> dest \<longrightarrow> (src_p = src \<longrightarrow> (src = dest \<longrightarrow> valid_list_2 t (m(dest \<mapsto> dest))) \<and> (src \<noteq> dest \<longrightarrow> valid_list_2 (t(src := t dest, dest := list_swap (t src) 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 \<mapsto> dest)))) \<and> (src_p \<noteq> src \<longrightarrow> (src = dest \<longrightarrow> valid_list_2 t (m(dest \<mapsto> src_p))) \<and> (src \<noteq> dest \<longrightarrow> valid_list_2 (t(src := t dest, dest := t src, src_p := list_swap (t src_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> src_p, dest \<mapsto> src_p)))))) \<and> (dest_p \<noteq> src_p \<longrightarrow> (dest_p = dest \<longrightarrow> (dest = src \<longrightarrow> (src_p = src \<longrightarrow> valid_list_2 t (m(src \<mapsto> src))) \<and> (src_p \<noteq> src \<longrightarrow> valid_list_2 t (m(src \<mapsto> src_p)))) \<and> (dest \<noteq> src \<longrightarrow> (src_p = 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> (src_p \<noteq> dest \<longrightarrow> (src_p = src \<longrightarrow> valid_list_2 (t(src := list_replace (t dest) dest src, dest := list_replace (t src) 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> dest))) \<and> (src_p \<noteq> src \<longrightarrow> valid_list_2 (t(dest := t src, src := list_replace (t dest) dest src, src_p := list_replace (t src_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> src, dest \<mapsto> src_p)))))) \<and> (dest_p \<noteq> dest \<longrightarrow> (dest_p = src \<longrightarrow> (src = dest \<longrightarrow> (src_p = dest \<longrightarrow> valid_list_2 t (m(dest \<mapsto> dest))) \<and> (src_p \<noteq> dest \<longrightarrow> valid_list_2 t (m(dest \<mapsto> src_p)))) \<and> (src \<noteq> dest \<longrightarrow> (src_p = dest \<longrightarrow> valid_list_2 (t(dest := list_replace (t src) 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 \<mapsto> dest, dest \<mapsto> src))) \<and> (src_p \<noteq> dest \<longrightarrow> (src_p = src \<longrightarrow> valid_list_2 (t(src := t dest, dest := list_swap (t src) 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 \<mapsto> dest))) \<and> (src_p \<noteq> src \<longrightarrow> valid_list_2 (t(src := t dest, dest := list_replace (t src) dest src, src_p := list_replace (t src_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 \<mapsto> src_p)))))) \<and> (dest_p \<noteq> src \<longrightarrow> (src = dest \<longrightarrow> (src_p = dest \<longrightarrow> valid_list_2 t (m(dest \<mapsto> dest))) \<and> (src_p \<noteq> dest \<longrightarrow> valid_list_2 t (m(dest \<mapsto> src_p)))) \<and> (src \<noteq> dest \<longrightarrow> (src_p = dest \<longrightarrow> valid_list_2 (t(dest := t src, dest_p := list_replace (t dest_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 \<mapsto> dest_p, dest \<mapsto> src))) \<and> (src_p \<noteq> dest \<longrightarrow> (src_p = src \<longrightarrow> valid_list_2 (t(src := t dest, dest_p := list_replace (t dest_p) dest src, dest := list_replace (t src) 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_p, dest \<mapsto> dest))) \<and> (src_p \<noteq> src \<longrightarrow> valid_list_2 (t(src := t dest, dest := t src, dest_p := list_replace (t dest_p) dest src, src_p := list_replace (t src_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_p, dest \<mapsto> src_p)))))))) proof (prove)
goal (21 subgoals):
 1. \<lbrakk>m src = Some src_p; m dest = Some dest_p; valid_list_2 t m; dest_p = src_p; src_p = dest; dest = src\<rbrakk> \<Longrightarrow> valid_list_2 t (m(src \<mapsto> src))
 2. \<lbrakk>m src = Some src_p; m dest = Some dest_p; valid_list_2 t m; dest_p = src_p; src_p = dest; dest \<noteq> src\<rbrakk> \<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))
 3. \<lbrakk>m src = Some src_p; m dest = Some dest_p; valid_list_2 t m; dest_p = src_p; src_p \<noteq> dest; src_p = src; src = dest\<rbrakk> \<Longrightarrow> valid_list_2 t (m(dest \<mapsto> dest))
 4. \<lbrakk>m src = Some src_p; m dest = Some dest_p; valid_list_2 t m; dest_p = src_p; src_p \<noteq> dest; src_p = src; src \<noteq> dest\<rbrakk> \<Longrightarrow> valid_list_2 (t(src := t dest, dest := list_swap (t src) 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 \<mapsto> dest))
 5. \<lbrakk>m src = Some src_p; m dest = Some dest_p; valid_list_2 t m; dest_p = src_p; src_p \<noteq> dest; src_p \<noteq> src; src = dest\<rbrakk> \<Longrightarrow> valid_list_2 t (m(dest \<mapsto> src_p))
 6. \<lbrakk>m src = Some src_p; m dest = Some dest_p; valid_list_2 t m; dest_p = src_p; src_p \<noteq> dest; src_p \<noteq> src; src \<noteq> dest\<rbrakk> \<Longrightarrow> valid_list_2 (t(src := t dest, dest := t src, src_p := list_swap (t src_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> src_p, dest \<mapsto> src_p))
 7. \<lbrakk>m src = Some src_p; m dest = Some dest_p; valid_list_2 t m; dest_p \<noteq> src_p; dest_p = dest; dest = src; src_p = src\<rbrakk> \<Longrightarrow> valid_list_2 t (m(src \<mapsto> src))
 8. \<lbrakk>m src = Some src_p; m dest = Some dest_p; valid_list_2 t m; dest_p \<noteq> src_p; dest_p = dest; dest = src; src_p \<noteq> src\<rbrakk> \<Longrightarrow> valid_list_2 t (m(src \<mapsto> src_p))
 9. \<lbrakk>m src = Some src_p; m dest = Some dest_p; valid_list_2 t m; dest_p \<noteq> src_p; dest_p = dest; dest \<noteq> src; src_p = dest\<rbrakk> \<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))
 10. \<lbrakk>m src = Some src_p; m dest = Some dest_p; valid_list_2 t m; dest_p \<noteq> src_p; dest_p = dest; dest \<noteq> src; src_p \<noteq> dest; src_p = src\<rbrakk> \<Longrightarrow> valid_list_2 (t(src := list_replace (t dest) dest src, dest := list_replace (t src) 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> dest))
A total of 21 subgoals... proof (prove)
goal:
No subgoals!