theory ListLibLemmas

lemma distinct_inj_middle: "distinct list \<Longrightarrow> list = (xa @ x # xb) \<Longrightarrow> list = (ya @ x # yb) \<Longrightarrow> xa = ya \<and> xb = yb" apply (induct list arbitrary: xa ya) apply simp apply clarsimp apply (case_tac "xa") apply simp apply (case_tac "ya") apply simp apply clarsimp apply clarsimp apply (case_tac "ya") apply (simp (no_asm_simp)) apply simp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct list; list = xa @ x # xb; list = ya @ x # yb\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb proof (prove)
goal (2 subgoals):
 1. \<And>xa ya. \<lbrakk>distinct []; [] = xa @ x # xb; [] = ya @ x # yb\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb
 2. \<And>a list xa ya. \<lbrakk>\<And>xa ya. \<lbrakk>distinct list; list = xa @ x # xb; list = ya @ x # yb\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; distinct (a # list); a # list = xa @ x # xb; a # list = ya @ x # yb\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb proof (prove)
goal (1 subgoal):
 1. \<And>a list xa ya. \<lbrakk>\<And>xa ya. \<lbrakk>distinct list; list = xa @ x # xb; list = ya @ x # yb\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; distinct (a # list); a # list = xa @ x # xb; a # list = ya @ x # yb\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb proof (prove)
goal (1 subgoal):
 1. \<And>a list xa ya. \<lbrakk>\<And>xa ya. \<lbrakk>distinct xa \<and> x \<notin> set xa \<and> set xa \<inter> set xb = {}; ya @ x # yb = xa @ x # xb; list = xa @ x # xb\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; ya @ x # yb = xa @ x # xb; a # list = xa @ x # xb; distinct xa; x \<notin> set xb; distinct xb; x \<notin> set xa; set xa \<inter> set xb = {}\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb proof (prove)
goal (2 subgoals):
 1. \<And>a list xa ya. \<lbrakk>\<And>xa ya. \<lbrakk>distinct xa \<and> x \<notin> set xa \<and> set xa \<inter> set xb = {}; ya @ x # yb = xa @ x # xb; list = xa @ x # xb\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; ya @ x # yb = xa @ x # xb; a # list = xa @ x # xb; distinct xa; x \<notin> set xb; distinct xb; x \<notin> set xa; set xa \<inter> set xb = {}; xa = []\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb
 2. \<And>a list xa ya aa lista. \<lbrakk>\<And>xa ya. \<lbrakk>distinct xa \<and> x \<notin> set xa \<and> set xa \<inter> set xb = {}; ya @ x # yb = xa @ x # xb; list = xa @ x # xb\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; ya @ x # yb = xa @ x # xb; a # list = xa @ x # xb; distinct xa; x \<notin> set xb; distinct xb; x \<notin> set xa; set xa \<inter> set xb = {}; xa = aa # lista\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb proof (prove)
goal (2 subgoals):
 1. \<And>a xa ya. \<lbrakk>ya @ x # yb = x # xb; a = x; x \<notin> set xb; distinct xb; xa = []\<rbrakk> \<Longrightarrow> [] = ya \<and> xb = yb
 2. \<And>a list xa ya aa lista. \<lbrakk>\<And>xa ya. \<lbrakk>distinct xa \<and> x \<notin> set xa \<and> set xa \<inter> set xb = {}; ya @ x # yb = xa @ x # xb; list = xa @ x # xb\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; ya @ x # yb = xa @ x # xb; a # list = xa @ x # xb; distinct xa; x \<notin> set xb; distinct xb; x \<notin> set xa; set xa \<inter> set xb = {}; xa = aa # lista\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb proof (prove)
goal (3 subgoals):
 1. \<And>a xa ya. \<lbrakk>ya @ x # yb = x # xb; a = x; x \<notin> set xb; distinct xb; xa = []; ya = []\<rbrakk> \<Longrightarrow> [] = ya \<and> xb = yb
 2. \<And>a xa ya aa list. \<lbrakk>ya @ x # yb = x # xb; a = x; x \<notin> set xb; distinct xb; xa = []; ya = aa # list\<rbrakk> \<Longrightarrow> [] = ya \<and> xb = yb
 3. \<And>a list xa ya aa lista. \<lbrakk>\<And>xa ya. \<lbrakk>distinct xa \<and> x \<notin> set xa \<and> set xa \<inter> set xb = {}; ya @ x # yb = xa @ x # xb; list = xa @ x # xb\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; ya @ x # yb = xa @ x # xb; a # list = xa @ x # xb; distinct xa; x \<notin> set xb; distinct xb; x \<notin> set xa; set xa \<inter> set xb = {}; xa = aa # lista\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb proof (prove)
goal (2 subgoals):
 1. \<And>a xa ya aa list. \<lbrakk>ya @ x # yb = x # xb; a = x; x \<notin> set xb; distinct xb; xa = []; ya = aa # list\<rbrakk> \<Longrightarrow> [] = ya \<and> xb = yb
 2. \<And>a list xa ya aa lista. \<lbrakk>\<And>xa ya. \<lbrakk>distinct xa \<and> x \<notin> set xa \<and> set xa \<inter> set xb = {}; ya @ x # yb = xa @ x # xb; list = xa @ x # xb\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; ya @ x # yb = xa @ x # xb; a # list = xa @ x # xb; distinct xa; x \<notin> set xb; distinct xb; x \<notin> set xa; set xa \<inter> set xb = {}; xa = aa # lista\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb proof (prove)
goal (1 subgoal):
 1. \<And>a list xa ya aa lista. \<lbrakk>\<And>xa ya. \<lbrakk>distinct xa \<and> x \<notin> set xa \<and> set xa \<inter> set xb = {}; ya @ x # yb = xa @ x # xb; list = xa @ x # xb\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; ya @ x # yb = xa @ x # xb; a # list = xa @ x # xb; distinct xa; x \<notin> set xb; distinct xb; x \<notin> set xa; set xa \<inter> set xb = {}; xa = aa # lista\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb proof (prove)
goal (1 subgoal):
 1. \<And>a ya lista. \<lbrakk>\<And>xa ya. \<lbrakk>distinct xa \<and> x \<notin> set xa \<and> set xa \<inter> set xb = {}; ya @ x # yb = xa @ x # xb; lista = xa\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; ya @ x # yb = a # lista @ x # xb; x \<notin> set xb; distinct xb; a \<notin> set lista; distinct lista; x \<noteq> a; x \<notin> set lista; a \<notin> set xb; set lista \<inter> set xb = {}\<rbrakk> \<Longrightarrow> a # lista = ya \<and> xb = yb proof (prove)
goal (2 subgoals):
 1. \<And>a ya lista. \<lbrakk>\<And>xa ya. \<lbrakk>distinct xa \<and> x \<notin> set xa \<and> set xa \<inter> set xb = {}; ya @ x # yb = xa @ x # xb; lista = xa\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; ya @ x # yb = a # lista @ x # xb; x \<notin> set xb; distinct xb; a \<notin> set lista; distinct lista; x \<noteq> a; x \<notin> set lista; a \<notin> set xb; set lista \<inter> set xb = {}; ya = []\<rbrakk> \<Longrightarrow> a # lista = ya \<and> xb = yb
 2. \<And>a ya lista aa list. \<lbrakk>\<And>xa ya. \<lbrakk>distinct xa \<and> x \<notin> set xa \<and> set xa \<inter> set xb = {}; ya @ x # yb = xa @ x # xb; lista = xa\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; ya @ x # yb = a # lista @ x # xb; x \<notin> set xb; distinct xb; a \<notin> set lista; distinct lista; x \<noteq> a; x \<notin> set lista; a \<notin> set xb; set lista \<inter> set xb = {}; ya = aa # list\<rbrakk> \<Longrightarrow> a # lista = ya \<and> xb = yb proof (prove)
goal (2 subgoals):
 1. \<And>a ya lista. \<lbrakk>\<And>xa ya. \<lbrakk>distinct xa \<and> x \<notin> set xa \<and> set xa \<inter> set xb = {}; ya @ x # yb = xa @ x # xb; lista = xa\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; ya @ x # yb = a # lista @ x # xb; x \<notin> set xb; distinct xb; a \<notin> set lista; distinct lista; x \<noteq> a; x \<notin> set lista; a \<notin> set xb; set lista \<inter> set xb = {}; ya = []\<rbrakk> \<Longrightarrow> False
 2. \<And>a ya lista aa list. \<lbrakk>\<And>xa ya. \<lbrakk>distinct xa \<and> x \<notin> set xa \<and> set xa \<inter> set xb = {}; ya @ x # yb = xa @ x # xb; lista = xa\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; ya @ x # yb = a # lista @ x # xb; x \<notin> set xb; distinct xb; a \<notin> set lista; distinct lista; x \<noteq> a; x \<notin> set lista; a \<notin> set xb; set lista \<inter> set xb = {}; ya = aa # list\<rbrakk> \<Longrightarrow> a # lista = ya \<and> xb = yb proof (prove)
goal (1 subgoal):
 1. \<And>a ya lista aa list. \<lbrakk>\<And>xa ya. \<lbrakk>distinct xa \<and> x \<notin> set xa \<and> set xa \<inter> set xb = {}; ya @ x # yb = xa @ x # xb; lista = xa\<rbrakk> \<Longrightarrow> xa = ya \<and> xb = yb; ya @ x # yb = a # lista @ x # xb; x \<notin> set xb; distinct xb; a \<notin> set lista; distinct lista; x \<noteq> a; x \<notin> set lista; a \<notin> set xb; set lista \<inter> set xb = {}; ya = aa # list\<rbrakk> \<Longrightarrow> a # lista = ya \<and> xb = yb proof (prove)
goal:
No subgoals!