theory Deterministic_AI

lemma valid_list_post_src_no_parent:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  notes replace_distinct[simplified list_replace_def,simp]
  notes list_remove_distinct[simp]
  shows
  "m src = None \<Longrightarrow> m dest = Some dest_p \<Longrightarrow> valid_list_2 (t''(src := [], dest := (t'' src) @ (t'' dest))) m'" apply (insert valid_list neq) apply (simp add: m'_def m''_def t'_def t''_def valid_list_2_def list_replace_def list_remove_removed) apply (intro impI conjI allI) apply fastforce+ 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''(src := [], dest := t'' src @ t'' dest)) m' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = None; m dest = Some dest_p; valid_list_2 t m; src \<noteq> dest\<rbrakk> \<Longrightarrow> valid_list_2 (t''(src := [], dest := t'' src @ t'' dest)) m' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = None; m dest = Some dest_p; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest\<rbrakk> \<Longrightarrow> (src = dest_p \<longrightarrow> (dest = dest_p \<longrightarrow> (\<forall>p. (p = dest_p \<longrightarrow> {c. m c = Some dest_p} - {dest_p} = {c. c \<noteq> dest_p \<and> (c \<noteq> dest_p \<longrightarrow> m c = Some dest_p)}) \<and> (p \<noteq> dest_p \<longrightarrow> {c. m c = Some p} = {c. c \<noteq> dest_p \<and> (c \<noteq> dest_p \<longrightarrow> m c = Some p)})) \<and> {c. m c = Some dest_p} \<subseteq> {dest_p}) \<and> (dest \<noteq> dest_p \<longrightarrow> (\<forall>p. (p = dest_p \<longrightarrow> m dest_p \<noteq> Some dest_p) \<and> (p \<noteq> dest_p \<longrightarrow> (p = dest \<longrightarrow> {c. m c = Some dest_p} - {dest} \<union> {c. m c = Some dest} = {c. (c = dest_p \<longrightarrow> m dest_p = Some dest) \<and> (c \<noteq> dest_p \<longrightarrow> c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c \<noteq> Some dest_p \<longrightarrow> m c = Some dest))}) \<and> (p \<noteq> dest \<longrightarrow> {c. m c = Some p} = {c. (c = dest_p \<longrightarrow> m dest_p = Some p) \<and> (c \<noteq> dest_p \<longrightarrow> c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c \<noteq> Some dest_p \<and> (m c \<noteq> Some dest_p \<longrightarrow> m c = Some p)))}))) \<and> ({c. m c = Some dest_p} - {dest}) \<inter> {c. m c = Some dest} = {})) \<and> (src \<noteq> dest_p \<longrightarrow> (dest = dest_p \<longrightarrow> (\<forall>p. p \<noteq> src \<longrightarrow> (p = dest_p \<longrightarrow> {c. m c = Some src} \<union> ({c. m c = Some dest_p} - {dest_p}) = {c. c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> c \<noteq> dest_p \<and> (c \<noteq> dest_p \<longrightarrow> m c \<noteq> Some src \<longrightarrow> m c = Some dest_p))}) \<and> (p \<noteq> dest_p \<longrightarrow> {c. m c = Some p} = {c. c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> c \<noteq> dest_p \<and> (c \<noteq> dest_p \<longrightarrow> m c \<noteq> Some src \<and> (m c \<noteq> Some src \<longrightarrow> m c = Some p)))})) \<and> {c. m c = Some src} \<inter> ({c. m c = Some dest_p} - {dest_p}) = {}) \<and> (dest \<noteq> dest_p \<longrightarrow> (\<forall>p. (p = dest_p \<longrightarrow> {c. m c = Some dest_p} - {dest} = {c. c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c \<noteq> Some src \<and> (m c \<noteq> Some src \<longrightarrow> m c = Some dest_p)))}) \<and> (p \<noteq> dest_p \<longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> {c. m c = Some src} \<union> {c. m c = Some dest} = {c. c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c \<noteq> Some src \<longrightarrow> m c = Some dest))}) \<and> (p \<noteq> dest \<longrightarrow> {c. m c = Some p} = {c. c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c \<noteq> Some src \<and> (m c \<noteq> Some src \<longrightarrow> m c = Some p)))}))) \<and> {c. m c = Some src} \<inter> {c. m c = Some dest} = {})) proof (prove)
goal (14 subgoals):
 1. \<And>p. \<lbrakk>m src = None; m dest = Some dest_p; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src = dest_p; dest = dest_p; p = dest_p\<rbrakk> \<Longrightarrow> {c. m c = Some dest_p} - {dest_p} = {c. c \<noteq> dest_p \<and> (c \<noteq> dest_p \<longrightarrow> m c = Some dest_p)}
 2. \<And>p. \<lbrakk>m src = None; m dest = Some dest_p; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src = dest_p; dest = dest_p; p \<noteq> dest_p\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. c \<noteq> dest_p \<and> (c \<noteq> dest_p \<longrightarrow> m c = Some p)}
 3. \<lbrakk>m src = None; m dest = Some dest_p; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src = dest_p; dest = dest_p\<rbrakk> \<Longrightarrow> {c. m c = Some dest_p} \<subseteq> {dest_p}
 4. \<And>p. \<lbrakk>m src = None; m dest = Some dest_p; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src = dest_p; dest \<noteq> dest_p; p = dest_p\<rbrakk> \<Longrightarrow> m dest_p \<noteq> Some dest_p
 5. \<And>p. \<lbrakk>m src = None; m dest = Some dest_p; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src = dest_p; dest \<noteq> dest_p; p \<noteq> dest_p; p = dest\<rbrakk> \<Longrightarrow> {c. m c = Some dest_p} - {dest} \<union> {c. m c = Some dest} = {c. (c = dest_p \<longrightarrow> m dest_p = Some dest) \<and> (c \<noteq> dest_p \<longrightarrow> c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c \<noteq> Some dest_p \<longrightarrow> m c = Some dest))}
 6. \<And>p. \<lbrakk>m src = None; m dest = Some dest_p; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src = dest_p; dest \<noteq> dest_p; p \<noteq> dest_p; p \<noteq> dest\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. (c = dest_p \<longrightarrow> m dest_p = Some p) \<and> (c \<noteq> dest_p \<longrightarrow> c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c \<noteq> Some dest_p \<and> (m c \<noteq> Some dest_p \<longrightarrow> m c = Some p)))}
 7. \<lbrakk>m src = None; m dest = Some dest_p; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src = dest_p; dest \<noteq> dest_p\<rbrakk> \<Longrightarrow> ({c. m c = Some dest_p} - {dest}) \<inter> {c. m c = Some dest} = {}
 8. \<And>p. \<lbrakk>m src = None; m dest = Some dest_p; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src \<noteq> dest_p; dest = dest_p; p \<noteq> src; p = dest_p\<rbrakk> \<Longrightarrow> {c. m c = Some src} \<union> ({c. m c = Some dest_p} - {dest_p}) = {c. c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> c \<noteq> dest_p \<and> (c \<noteq> dest_p \<longrightarrow> m c \<noteq> Some src \<longrightarrow> m c = Some dest_p))}
 9. \<And>p. \<lbrakk>m src = None; m dest = Some dest_p; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src \<noteq> dest_p; dest = dest_p; p \<noteq> src; p \<noteq> dest_p\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> c \<noteq> dest_p \<and> (c \<noteq> dest_p \<longrightarrow> m c \<noteq> Some src \<and> (m c \<noteq> Some src \<longrightarrow> m c = Some p)))}
 10. \<lbrakk>m src = None; m dest = Some dest_p; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src \<noteq> dest_p; dest = dest_p\<rbrakk> \<Longrightarrow> {c. m c = Some src} \<inter> ({c. m c = Some dest_p} - {dest_p}) = {}
A total of 14 subgoals... proof (prove)
goal:
No subgoals!