theory Deterministic_AI

lemma valid_list_post_no_parents:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  notes replace_distinct[simplified list_replace_def,simp]
  shows
  "m src = None \<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) apply (intro impI conjI allI) apply fastforce apply fastforce apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = None; 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 = None; 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 = None; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest\<rbrakk> \<Longrightarrow> (\<forall>p. 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> 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> 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 (3 subgoals):
 1. \<And>p. \<lbrakk>m src = None; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; p \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> {c. m c = Some src} \<union> {c. m c = Some dest} = {c. c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> m c \<noteq> Some src \<longrightarrow> m c = Some dest)}
 2. \<And>p. \<lbrakk>m src = None; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> m c \<noteq> Some src \<and> (m c \<noteq> Some src \<longrightarrow> m c = Some p))}
 3. \<lbrakk>m src = None; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest\<rbrakk> \<Longrightarrow> {c. m c = Some src} \<inter> {c. m c = Some dest} = {} proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>m src = None; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest; p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. c \<noteq> src \<and> (c \<noteq> src \<longrightarrow> m c \<noteq> Some src \<and> (m c \<noteq> Some src \<longrightarrow> m c = Some p))}
 2. \<lbrakk>m src = None; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest\<rbrakk> \<Longrightarrow> {c. m c = Some src} \<inter> {c. m c = Some dest} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = None; m dest = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); src \<noteq> dest\<rbrakk> \<Longrightarrow> {c. m c = Some src} \<inter> {c. m c = Some dest} = {} proof (prove)
goal:
No subgoals!