theory Deterministic_AI

lemma valid_list_post_src_parent:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "m src = Some src_p \<Longrightarrow> m dest = None \<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 = Some src_p; m dest = None\<rbrakk> \<Longrightarrow> valid_list_2 t' n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some src_p; m dest = None; 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 = None; valid_list_2 t m\<rbrakk> \<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, 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 := None, dest \<mapsto> src))) \<and> (src_p \<noteq> dest \<longrightarrow> (src_p = src \<longrightarrow> valid_list_2 (t(src := t dest, 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 := None, dest \<mapsto> dest))) \<and> (src_p \<noteq> src \<longrightarrow> valid_list_2 (t(src := t dest, dest := t 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 := None, dest \<mapsto> src_p))))) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m src = Some src_p; m dest = None; valid_list_2 t m; src = dest; src_p = dest\<rbrakk> \<Longrightarrow> valid_list_2 t (m(dest \<mapsto> dest))
 2. \<lbrakk>m src = Some src_p; m dest = None; valid_list_2 t m; src = dest; src_p \<noteq> dest\<rbrakk> \<Longrightarrow> valid_list_2 t (m(dest \<mapsto> src_p))
 3. \<lbrakk>m src = Some src_p; m dest = None; valid_list_2 t m; src \<noteq> dest; src_p = dest\<rbrakk> \<Longrightarrow> valid_list_2 (t(dest := t 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 := None, dest \<mapsto> src))
 4. \<lbrakk>m src = Some src_p; m dest = None; valid_list_2 t m; src \<noteq> dest; src_p \<noteq> dest; src_p = src\<rbrakk> \<Longrightarrow> valid_list_2 (t(src := t dest, 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 := None, dest \<mapsto> dest))
 5. \<lbrakk>m src = Some src_p; m dest = None; valid_list_2 t m; src \<noteq> dest; src_p \<noteq> dest; src_p \<noteq> src\<rbrakk> \<Longrightarrow> valid_list_2 (t(src := t dest, dest := t 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 := None, dest \<mapsto> src_p)) proof (prove)
goal:
No subgoals!