theory Deterministic_AI

lemma next_sib_inj:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>next_sib a t m = Some y; next_sib b t m = Some y; valid_list_2 t m\<rbrakk>
    \<Longrightarrow> a = b" apply(drule next_sibD)+ apply(simp add: valid_list_2_def) apply(elim exE conjE) apply(frule_tac a=a in after_in_list_in_list) apply(frule_tac a=b in after_in_list_in_list) apply(rule_tac list="t pa" and x=y in after_in_list_inj) apply(simp) apply(simp) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib a t m = Some y; next_sib b t m = Some y; valid_list_2 t m\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; \<exists>p. m a = Some p \<and> after_in_list (t p) a = Some y; \<exists>p. m b = Some p \<and> after_in_list (t p) b = Some y\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); \<exists>p. m a = Some p \<and> after_in_list (t p) a = Some y; \<exists>p. m b = Some p \<and> after_in_list (t p) b = Some y\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<And>p pa. \<lbrakk>\<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p); m a = Some p; after_in_list (t p) a = Some y; m b = Some pa; after_in_list (t pa) b = Some y\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<And>p pa. \<lbrakk>\<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p); m a = Some p; after_in_list (t p) a = Some y; m b = Some pa; after_in_list (t pa) b = Some y; y \<in> set (t p)\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<And>p pa. \<lbrakk>\<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p); m a = Some p; after_in_list (t p) a = Some y; m b = Some pa; after_in_list (t pa) b = Some y; y \<in> set (t p); y \<in> set (t pa)\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (3 subgoals):
 1. \<And>p pa. \<lbrakk>\<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p); m a = Some p; after_in_list (t p) a = Some y; m b = Some pa; after_in_list (t pa) b = Some y; y \<in> set (t p); y \<in> set (t pa)\<rbrakk> \<Longrightarrow> distinct (t pa)
 2. \<And>p pa. \<lbrakk>\<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p); m a = Some p; after_in_list (t p) a = Some y; m b = Some pa; after_in_list (t pa) b = Some y; y \<in> set (t p); y \<in> set (t pa)\<rbrakk> \<Longrightarrow> after_in_list (t pa) a = Some y
 3. \<And>p pa. \<lbrakk>\<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p); m a = Some p; after_in_list (t p) a = Some y; m b = Some pa; after_in_list (t pa) b = Some y; y \<in> set (t p); y \<in> set (t pa)\<rbrakk> \<Longrightarrow> after_in_list (t pa) b = Some y proof (prove)
goal (2 subgoals):
 1. \<And>p pa. \<lbrakk>\<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p); m a = Some p; after_in_list (t p) a = Some y; m b = Some pa; after_in_list (t pa) b = Some y; y \<in> set (t p); y \<in> set (t pa)\<rbrakk> \<Longrightarrow> after_in_list (t pa) a = Some y
 2. \<And>p pa. \<lbrakk>\<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p); m a = Some p; after_in_list (t p) a = Some y; m b = Some pa; after_in_list (t pa) b = Some y; y \<in> set (t p); y \<in> set (t pa)\<rbrakk> \<Longrightarrow> after_in_list (t pa) b = Some y proof (prove)
goal (1 subgoal):
 1. \<And>p pa. \<lbrakk>\<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p); m a = Some p; after_in_list (t p) a = Some y; m b = Some pa; after_in_list (t pa) b = Some y; y \<in> set (t p); y \<in> set (t pa)\<rbrakk> \<Longrightarrow> after_in_list (t pa) b = Some y proof (prove)
goal:
No subgoals!