# HG changeset patch
# User nipkow
# Date 1194247872 -3600
# Node ID 95128fcdd7e855f529346c457bbf72042ae74d24
# Parent  f9237f6f3a8dc129e06f66b1c3f8b76dd392764a
added lemmas

diff -r f9237f6f3a8d -r 95128fcdd7e8 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Sun Nov 04 19:17:13 2007 +0100
+++ b/src/HOL/Library/Permutation.thy	Mon Nov 05 08:31:12 2007 +0100
@@ -46,9 +46,6 @@
 lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
   by (erule perm.induct) auto
 
-lemma perm_mem [rule_format]: "xs <~~> ys ==> x mem xs --> x mem ys"
-  by (erule perm.induct) auto
-
 
 subsection {* Ways of making new permutations *}
 
@@ -172,4 +169,14 @@
   apply (blast intro: sym)+
   done
 
+lemma perm_set_eq: "xs <~~> ys ==> set xs = set ys"
+by (metis multiset_of_eq_perm multiset_of_eq_setD)
+
+lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys"
+apply(induct rule:perm.induct)
+   apply simp_all
+ apply fastsimp
+apply (metis perm_set_eq)
+done
+
 end
diff -r f9237f6f3a8d -r 95128fcdd7e8 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Nov 04 19:17:13 2007 +0100
+++ b/src/HOL/List.thy	Mon Nov 05 08:31:12 2007 +0100
@@ -2581,6 +2581,9 @@
 
 end
 
+lemma sorted_upt[simp]: "sorted[i..<j]"
+by (induct j) (simp_all add:sorted_append)
+
 
 subsubsection {* @{text sorted_list_of_set} *}