theory ListLibLemmas

lemma after_can_split_distinct:
  "distinct list \<Longrightarrow> after_in_list list x = Some y \<Longrightarrow> \<exists>!ys. \<exists>!xs. list = xs @ (x # y # ys)" apply (frule after_can_split) apply (elim exE) apply (rule ex1I) apply (rule ex1I) apply assumption apply simp apply (elim ex1E) apply (thin_tac "\<forall>x. P x" for P) apply (frule_tac yb="y#ysa" in distinct_inj_middle,assumption+) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct list; after_in_list list x = Some y\<rbrakk> \<Longrightarrow> \<exists>!ys. \<exists>!xs. list = xs @ x # y # ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct list; after_in_list list x = Some y; \<exists>ys xs. list = xs @ x # y # ys\<rbrakk> \<Longrightarrow> \<exists>!ys. \<exists>!xs. list = xs @ x # y # ys proof (prove)
goal (1 subgoal):
 1. \<And>ys xs. \<lbrakk>distinct list; after_in_list list x = Some y; list = xs @ x # y # ys\<rbrakk> \<Longrightarrow> \<exists>!ys. \<exists>!xs. list = xs @ x # y # ys proof (prove)
goal (2 subgoals):
 1. \<And>ys xs. \<lbrakk>distinct list; after_in_list list x = Some y; list = xs @ x # y # ys\<rbrakk> \<Longrightarrow> \<exists>!xsa. list = xsa @ x # y # ?a4 ys xs
 2. \<And>ys xs ysa. \<lbrakk>distinct list; after_in_list list x = Some y; list = xs @ x # y # ys; \<exists>!xs. list = xs @ x # y # ysa\<rbrakk> \<Longrightarrow> ysa = ?a4 ys xs proof (prove)
goal (3 subgoals):
 1. \<And>ys xs. \<lbrakk>distinct list; after_in_list list x = Some y; list = xs @ x # y # ys\<rbrakk> \<Longrightarrow> list = ?a7 ys xs @ x # y # ?a4 ys xs
 2. \<And>ys xs xsa. \<lbrakk>distinct list; after_in_list list x = Some y; list = xs @ x # y # ys; list = xsa @ x # y # ?a4 ys xs\<rbrakk> \<Longrightarrow> xsa = ?a7 ys xs
 3. \<And>ys xs ysa. \<lbrakk>distinct list; after_in_list list x = Some y; list = xs @ x # y # ys; \<exists>!xs. list = xs @ x # y # ysa\<rbrakk> \<Longrightarrow> ysa = ?a4 ys xs proof (prove)
goal (2 subgoals):
 1. \<And>ys xs xsa. \<lbrakk>distinct list; after_in_list list x = Some y; list = xs @ x # y # ys; list = xsa @ x # y # ys\<rbrakk> \<Longrightarrow> xsa = xs
 2. \<And>ys xs ysa. \<lbrakk>distinct list; after_in_list list x = Some y; list = xs @ x # y # ys; \<exists>!xs. list = xs @ x # y # ysa\<rbrakk> \<Longrightarrow> ysa = ys proof (prove)
goal (1 subgoal):
 1. \<And>ys xs ysa. \<lbrakk>distinct list; after_in_list list x = Some y; list = xs @ x # y # ys; \<exists>!xs. list = xs @ x # y # ysa\<rbrakk> \<Longrightarrow> ysa = ys proof (prove)
goal (1 subgoal):
 1. \<And>ys xs ysa xsa. \<lbrakk>distinct list; after_in_list list x = Some y; list = xs @ x # y # ys; list = xsa @ x # y # ysa; \<forall>ya. list = ya @ x # y # ysa \<longrightarrow> ya = xsa\<rbrakk> \<Longrightarrow> ysa = ys proof (prove)
goal (1 subgoal):
 1. \<And>ys xs ysa xsa. \<lbrakk>distinct list; after_in_list list x = Some y; list = xs @ x # y # ys; list = xsa @ x # y # ysa\<rbrakk> \<Longrightarrow> ysa = ys proof (prove)
goal (1 subgoal):
 1. \<And>ys xs ysa xsa. \<lbrakk>distinct list; after_in_list list x = Some y; list = xs @ x # y # ys; list = xsa @ x # y # ysa; xs = xsa \<and> y # ys = y # ysa\<rbrakk> \<Longrightarrow> ysa = ys proof (prove)
goal:
No subgoals!