theory Deterministic_AI

lemma valid_list_post_dest_parent:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "m src = None \<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 (fastforce simp: valid_list_2_def replace_distinct list_replace_set)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = None; m dest = Some dest_p\<rbrakk> \<Longrightarrow> valid_list_2 t' n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = None; 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 = None; m dest = Some dest_p; valid_list_2 t m\<rbrakk> \<Longrightarrow> (dest_p = dest \<longrightarrow> dest \<noteq> src \<longrightarrow> valid_list_2 (t(dest := t src, src := list_replace (t dest) dest src)) ((\<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 := None))) \<and> (dest_p \<noteq> dest \<longrightarrow> (dest_p = src \<longrightarrow> (src = dest \<longrightarrow> valid_list_2 t (m(dest := None))) \<and> (src \<noteq> dest \<longrightarrow> valid_list_2 (t(src := t dest, dest := list_replace (t src) dest src)) ((\<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 := None)))) \<and> (dest_p \<noteq> src \<longrightarrow> (src = dest \<longrightarrow> valid_list_2 t (m(dest := None))) \<and> (src \<noteq> dest \<longrightarrow> valid_list_2 (t(src := t dest, dest := t src, dest_p := list_replace (t dest_p) dest src)) ((\<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 := None))))) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m src = None; m dest = Some dest_p; valid_list_2 t m; dest_p = dest; dest \<noteq> src\<rbrakk> \<Longrightarrow> valid_list_2 (t(dest := t src, src := list_replace (t dest) dest src)) ((\<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 := None))
 2. \<lbrakk>m src = None; m dest = Some dest_p; valid_list_2 t m; dest_p \<noteq> dest; dest_p = src; src = dest\<rbrakk> \<Longrightarrow> valid_list_2 t (m(dest := None))
 3. \<lbrakk>m src = None; m dest = Some dest_p; valid_list_2 t m; dest_p \<noteq> dest; dest_p = src; src \<noteq> dest\<rbrakk> \<Longrightarrow> valid_list_2 (t(src := t dest, dest := list_replace (t src) dest src)) ((\<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 := None))
 4. \<lbrakk>m src = None; m dest = Some dest_p; valid_list_2 t m; dest_p \<noteq> dest; dest_p \<noteq> src; src = dest\<rbrakk> \<Longrightarrow> valid_list_2 t (m(dest := None))
 5. \<lbrakk>m src = None; m dest = Some dest_p; valid_list_2 t m; dest_p \<noteq> dest; dest_p \<noteq> src; src \<noteq> dest\<rbrakk> \<Longrightarrow> valid_list_2 (t(src := t dest, dest := t src, dest_p := list_replace (t dest_p) dest src)) ((\<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 := None)) proof (prove)
goal:
No subgoals!