theory Deterministic_AI

lemma valid_list_post_dest_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 = Some src_p \<Longrightarrow> m dest = None \<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 = Some src_p; m dest = None\<rbrakk> \<Longrightarrow> valid_list_2 (t''(src := [], dest := t'' src @ t'' dest)) m' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some src_p; m dest = None; 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 = Some src_p; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest\<rbrakk> \<Longrightarrow> (src = src_p \<longrightarrow> (dest = src_p \<longrightarrow> (\<forall>p. (p = src_p \<longrightarrow> {c. m c = Some src_p} = {c. c \<noteq> src_p \<and> (c \<noteq> src_p \<longrightarrow> m c = Some src_p)}) \<and> (p \<noteq> src_p \<longrightarrow> {c. m c = Some p} = {c. c \<noteq> src_p \<and> (c \<noteq> src_p \<longrightarrow> m c = Some p)})) \<and> (\<forall>x. m x \<noteq> Some src_p)) \<and> (dest \<noteq> src_p \<longrightarrow> (\<forall>p. p \<noteq> src_p \<longrightarrow> (p = dest \<longrightarrow> (\<lambda>a. dest) ` ({c. m c = Some src_p} \<inter> {src_p}) \<union> {c. m c = Some src_p} \<inter> {x. x \<noteq> src_p} \<union> {c. m c = Some dest} = {c. c \<noteq> dest \<longrightarrow> c \<noteq> src_p \<and> (c \<noteq> src_p \<longrightarrow> m c \<noteq> Some src_p \<longrightarrow> m c = Some dest)}) \<and> (p \<noteq> dest \<longrightarrow> {c. m c = Some p} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> c \<noteq> src_p \<and> (c \<noteq> src_p \<longrightarrow> m c \<noteq> Some src_p \<and> (m c \<noteq> Some src_p \<longrightarrow> m c = Some p)))})) \<and> ((\<lambda>a. dest) ` ({c. m c = Some src_p} \<inter> {src_p}) \<union> {c. m c = Some src_p} \<inter> {x. x \<noteq> src_p}) \<inter> {c. m c = Some dest} = {})) \<and> (src \<noteq> src_p \<longrightarrow> (dest = src_p \<longrightarrow> (\<forall>p. p \<noteq> src \<longrightarrow> (p = src_p \<longrightarrow> insert src_p ({c. m c = Some src} \<union> {c. m c = Some src_p} \<inter> {x. x \<noteq> src}) = {c. c \<noteq> src_p \<longrightarrow> c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> m c \<noteq> Some src \<longrightarrow> m c = Some src_p)}) \<and> (p \<noteq> src_p \<longrightarrow> {c. m c = Some p} = {c. c \<noteq> src_p \<and> (c \<noteq> src_p \<longrightarrow> c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> m c \<noteq> Some src \<and> (m c \<noteq> Some src \<longrightarrow> m c = Some p)))})) \<and> distinct (map (\<lambda>x. if x = src then src_p else x) (t src_p)) \<and> m src_p \<noteq> Some src \<and> {c. m c = Some src} \<inter> ({c. m c = Some src_p} \<inter> {x. x \<noteq> src}) = {}) \<and> (dest \<noteq> src_p \<longrightarrow> (\<forall>p. (p = src_p \<longrightarrow> insert dest ({c. m c = Some src_p} \<inter> {x. x \<noteq> src}) = {c. c \<noteq> dest \<longrightarrow> c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> m c \<noteq> Some src \<and> (m c \<noteq> Some src \<longrightarrow> m c = Some src_p))}) \<and> (p \<noteq> src_p \<longrightarrow> p \<noteq> src \<longrightarrow> (p = dest \<longrightarrow> {c. m c = Some src} \<union> {c. m c = Some dest} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> m c \<noteq> Some src \<longrightarrow> m c = Some dest))}) \<and> (p \<noteq> dest \<longrightarrow> {c. m c = Some p} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> c \<noteq> src \<and> (c \<noteq> src \<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 (15 subgoals):
 1. \<And>p. \<lbrakk>m src = Some src_p; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src = src_p; dest = src_p; p = src_p\<rbrakk> \<Longrightarrow> {c. m c = Some src_p} = {c. c \<noteq> src_p \<and> (c \<noteq> src_p \<longrightarrow> m c = Some src_p)}
 2. \<And>p. \<lbrakk>m src = Some src_p; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src = src_p; dest = src_p; p \<noteq> src_p\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. c \<noteq> src_p \<and> (c \<noteq> src_p \<longrightarrow> m c = Some p)}
 3. \<And>x. \<lbrakk>m src = Some src_p; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src = src_p; dest = src_p\<rbrakk> \<Longrightarrow> m x \<noteq> Some src_p
 4. \<And>p. \<lbrakk>m src = Some src_p; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src = src_p; dest \<noteq> src_p; p \<noteq> src_p; p = dest\<rbrakk> \<Longrightarrow> (\<lambda>a. dest) ` ({c. m c = Some src_p} \<inter> {src_p}) \<union> {c. m c = Some src_p} \<inter> {x. x \<noteq> src_p} \<union> {c. m c = Some dest} = {c. c \<noteq> dest \<longrightarrow> c \<noteq> src_p \<and> (c \<noteq> src_p \<longrightarrow> m c \<noteq> Some src_p \<longrightarrow> m c = Some dest)}
 5. \<And>p. \<lbrakk>m src = Some src_p; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src = src_p; dest \<noteq> src_p; p \<noteq> src_p; p \<noteq> dest\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> c \<noteq> src_p \<and> (c \<noteq> src_p \<longrightarrow> m c \<noteq> Some src_p \<and> (m c \<noteq> Some src_p \<longrightarrow> m c = Some p)))}
 6. \<lbrakk>m src = Some src_p; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src = src_p; dest \<noteq> src_p\<rbrakk> \<Longrightarrow> ((\<lambda>a. dest) ` ({c. m c = Some src_p} \<inter> {src_p}) \<union> {c. m c = Some src_p} \<inter> {x. x \<noteq> src_p}) \<inter> {c. m c = Some dest} = {}
 7. \<And>p. \<lbrakk>m src = Some src_p; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src \<noteq> src_p; dest = src_p; p \<noteq> src; p = src_p\<rbrakk> \<Longrightarrow> insert src_p ({c. m c = Some src} \<union> {c. m c = Some src_p} \<inter> {x. x \<noteq> src}) = {c. c \<noteq> src_p \<longrightarrow> c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> m c \<noteq> Some src \<longrightarrow> m c = Some src_p)}
 8. \<And>p. \<lbrakk>m src = Some src_p; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src \<noteq> src_p; dest = src_p; p \<noteq> src; p \<noteq> src_p\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. c \<noteq> src_p \<and> (c \<noteq> src_p \<longrightarrow> c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> m c \<noteq> Some src \<and> (m c \<noteq> Some src \<longrightarrow> m c = Some p)))}
 9. \<lbrakk>m src = Some src_p; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src \<noteq> src_p; dest = src_p\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. if x = src then src_p else x) (t src_p))
 10. \<lbrakk>m src = Some src_p; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; src \<noteq> src_p; dest = src_p\<rbrakk> \<Longrightarrow> m src_p \<noteq> Some src
A total of 15 subgoals... proof (prove)
goal:
No subgoals!