# HG changeset patch
# User nipkow
# Date 1194283119 -3600
# Node ID 094dab519ff58a958b3b6ab5c368660306cd7fd3
# Parent  35e954ff67f84bd27e8ea8e7e6605bee869c115f
added lemmas

diff -r 35e954ff67f8 -r 094dab519ff5 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Mon Nov 05 17:48:51 2007 +0100
+++ b/src/HOL/Library/Permutation.thy	Mon Nov 05 18:18:39 2007 +0100
@@ -179,4 +179,25 @@
 apply (metis perm_set_eq)
 done
 
+lemma eq_set_perm_remdups: "set xs = set ys ==> remdups xs <~~> remdups ys"
+apply(induct xs arbitrary: ys rule:length_induct)
+apply (case_tac "remdups xs", simp, simp)
+apply(subgoal_tac "a : set (remdups ys)")
+ prefer 2 apply (metis set.simps(2) insert_iff set_remdups)
+apply(drule split_list) apply(elim exE conjE)
+apply(drule_tac x=list in spec) apply(erule impE) prefer 2
+ apply(drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
+  apply simp
+  apply(subgoal_tac "a#list <~~> a#ysa@zs")
+   apply (metis Cons_eq_appendI perm_append_Cons trans)
+  apply (metis Cons Cons_eq_appendI distinct.simps(2) distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
+ apply(subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
+  apply(fastsimp simp add: insert_ident)
+ apply (metis distinct_remdups set_remdups)
+apply (metis Nat.le_less_trans Suc_length_conv le_def length_remdups_leq less_Suc_eq)
+done
+
+lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
+by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
+
 end
diff -r 35e954ff67f8 -r 094dab519ff5 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Nov 05 17:48:51 2007 +0100
+++ b/src/HOL/List.thy	Mon Nov 05 18:18:39 2007 +0100
@@ -2069,6 +2069,12 @@
 lemma distinct_remdups [iff]: "distinct (remdups xs)"
 by (induct xs) auto
 
+lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"
+by (induct xs, auto)
+
+lemma remdups_id_iff_distinct[simp]: "(remdups xs = xs) = distinct xs"
+by(metis distinct_remdups distinct_remdups_id)
+
 lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
 by (metis distinct_remdups finite_list set_remdups)
 
@@ -2184,6 +2190,12 @@
   qed
 qed
 
+lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"
+apply (induct n == "length ws" arbitrary:ws) apply simp
+apply(case_tac ws) apply simp
+apply (simp split:split_if_asm)
+apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
+done
 
 lemma length_remdups_concat:
  "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
diff -r 35e954ff67f8 -r 094dab519ff5 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Nov 05 17:48:51 2007 +0100
+++ b/src/HOL/Set.thy	Mon Nov 05 18:18:39 2007 +0100
@@ -780,6 +780,8 @@
   show "x \<notin> A - {x}" by blast
 qed
 
+lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"
+by auto
 
 subsubsection {* Singletons, using insert *}