theory Deterministic_AI

lemma valid_list_post:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
    "
   valid_list_2 (t'(src := dest # (t' src)))
        (m(dest \<mapsto> src))" apply (insert valid_list dest) apply (simp add: valid_list_2_def t'_def) apply (simp add: list_remove_removed insert_Collect remove_collect) apply (intro impI conjI allI) apply (fastforce simp: list_remove_distinct cong: Collect_cong)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_list_2 (t'(src := dest # t' src)) (m(dest \<mapsto> src)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m dest = Some dest_p\<rbrakk> \<Longrightarrow> valid_list_2 (t'(src := dest # t' src)) (m(dest \<mapsto> src)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m dest = Some dest_p\<rbrakk> \<Longrightarrow> (src = dest_p \<longrightarrow> (\<forall>p. (p = dest_p \<longrightarrow> insert dest (set (list_remove (t dest_p) dest)) = {c. c \<noteq> dest \<longrightarrow> m c = Some dest_p}) \<and> (p \<noteq> dest_p \<longrightarrow> {c. m c = Some p} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)})) \<and> dest \<notin> set (list_remove (t dest_p) dest) \<and> distinct (list_remove (t dest_p) dest)) \<and> (src \<noteq> dest_p \<longrightarrow> (\<forall>p. (p = dest_p \<longrightarrow> set (list_remove (t dest_p) dest) = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c = Some dest_p)}) \<and> (p \<noteq> dest_p \<longrightarrow> (p = src \<longrightarrow> insert dest {c. m c = Some src} = {c. c \<noteq> dest \<longrightarrow> m c = Some src}) \<and> (p \<noteq> src \<longrightarrow> {c. m c = Some p} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}))) \<and> distinct (list_remove (t dest_p) dest)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m dest = Some dest_p\<rbrakk> \<Longrightarrow> (src = dest_p \<longrightarrow> (\<forall>p. p \<noteq> dest_p \<longrightarrow> {c. m c = Some p} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}) \<and> distinct (list_remove (t dest_p) dest)) \<and> (src \<noteq> dest_p \<longrightarrow> (\<forall>p. (p = dest_p \<longrightarrow> {c. m c = Some dest_p \<and> c \<noteq> dest} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c = Some dest_p)}) \<and> (p \<noteq> dest_p \<longrightarrow> p \<noteq> src \<longrightarrow> {c. m c = Some p} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)})) \<and> distinct (list_remove (t dest_p) dest)) proof (prove)
goal (5 subgoals):
 1. \<And>p. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m dest = Some dest_p; src = dest_p; p \<noteq> dest_p\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}
 2. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m dest = Some dest_p; src = dest_p\<rbrakk> \<Longrightarrow> distinct (list_remove (t dest_p) dest)
 3. \<And>p. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m dest = Some dest_p; src \<noteq> dest_p; p = dest_p\<rbrakk> \<Longrightarrow> {c. m c = Some dest_p \<and> c \<noteq> dest} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c = Some dest_p)}
 4. \<And>p. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m dest = Some dest_p; src \<noteq> dest_p; p \<noteq> dest_p; p \<noteq> src\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. c \<noteq> dest \<and> (c \<noteq> dest \<longrightarrow> m c = Some p)}
 5. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m dest = Some dest_p; src \<noteq> dest_p\<rbrakk> \<Longrightarrow> distinct (list_remove (t dest_p) dest) proof (prove)
goal:
No subgoals!