theory Deterministic_AI

lemma (in mdb_empty_abs') valid_list_post:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>valid_list_2 t m; m slot = Some slot_p\<rbrakk>
    \<Longrightarrow> valid_list_2 (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n" apply(simp add: valid_list_2_def) apply(intro conjI impI allI) apply(simp) apply(simp add: n_def) apply(fastforce simp: set_list_replace_list n_def) apply(simp add: n_def) apply(simp add: n_def, fastforce) apply(rule distinct_list_replace_list) apply(simp)+ apply(rule ccontr) apply(fastforce dest: int_not_emptyD) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; m slot = Some slot_p\<rbrakk> \<Longrightarrow> valid_list_2 (t(slot_p := list_replace_list (t slot_p) slot (t slot), slot := [])) n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p\<rbrakk> \<Longrightarrow> (\<forall>p. (p = slot_p \<longrightarrow> (slot_p = slot \<longrightarrow> (\<forall>x. n x \<noteq> Some slot)) \<and> (slot_p \<noteq> slot \<longrightarrow> set (list_replace_list (t slot_p) slot (t slot)) = {c. n c = Some slot_p})) \<and> (p \<noteq> slot_p \<longrightarrow> (p = slot \<longrightarrow> (\<forall>x. n x \<noteq> Some slot)) \<and> (p \<noteq> slot \<longrightarrow> {c. m c = Some p} = {c. n c = Some p}))) \<and> (slot_p \<noteq> slot \<longrightarrow> distinct (list_replace_list (t slot_p) slot (t slot))) proof (prove)
goal (5 subgoals):
 1. \<And>p x. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; p = slot_p; slot_p = slot\<rbrakk> \<Longrightarrow> n x \<noteq> Some slot
 2. \<And>p. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; p = slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> set (list_replace_list (t slot_p) slot (t slot)) = {c. n c = Some slot_p}
 3. \<And>p x. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; p \<noteq> slot_p; p = slot\<rbrakk> \<Longrightarrow> n x \<noteq> Some slot
 4. \<And>p. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; p \<noteq> slot_p; p \<noteq> slot\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. n c = Some p}
 5. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (list_replace_list (t slot_p) slot (t slot)) proof (prove)
goal (4 subgoals):
 1. \<And>p. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; p = slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> set (list_replace_list (t slot_p) slot (t slot)) = {c. n c = Some slot_p}
 2. \<And>p x. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; p \<noteq> slot_p; p = slot\<rbrakk> \<Longrightarrow> n x \<noteq> Some slot
 3. \<And>p. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; p \<noteq> slot_p; p \<noteq> slot\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. n c = Some p}
 4. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (list_replace_list (t slot_p) slot (t slot)) proof (prove)
goal (4 subgoals):
 1. \<And>p. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; p = slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> set (list_replace_list (t slot_p) slot (t slot)) = {c. (m c = Some slot \<longrightarrow> c \<noteq> slot) \<and> (m c \<noteq> Some slot \<longrightarrow> c \<noteq> slot \<and> (c \<noteq> slot \<longrightarrow> m c = Some slot_p))}
 2. \<And>p x. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; p \<noteq> slot_p; p = slot\<rbrakk> \<Longrightarrow> n x \<noteq> Some slot
 3. \<And>p. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; p \<noteq> slot_p; p \<noteq> slot\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. n c = Some p}
 4. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (list_replace_list (t slot_p) slot (t slot)) proof (prove)
goal (3 subgoals):
 1. \<And>p x. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; p \<noteq> slot_p; p = slot\<rbrakk> \<Longrightarrow> n x \<noteq> Some slot
 2. \<And>p. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; p \<noteq> slot_p; p \<noteq> slot\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. n c = Some p}
 3. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (list_replace_list (t slot_p) slot (t slot)) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; p \<noteq> slot_p; p \<noteq> slot\<rbrakk> \<Longrightarrow> {c. m c = Some p} = {c. n c = Some p}
 2. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (list_replace_list (t slot_p) slot (t slot)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (list_replace_list (t slot_p) slot (t slot)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (t slot_p)
 2. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> distinct (t slot)
 3. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> set (t slot_p) \<inter> set (t slot) = {}
 4. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> slot \<in> set (t slot_p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> {c. m c = Some slot_p} \<inter> {c. m c = Some slot} = {}
 2. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> slot \<in> set (t slot_p) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot; {c. m c = Some slot_p} \<inter> {c. m c = Some slot} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> slot \<in> set (t slot_p) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m slot = Some slot_p; slot_p \<noteq> slot\<rbrakk> \<Longrightarrow> slot \<in> set (t slot_p) proof (prove)
goal:
No subgoals!