src/HOL/Library/Permutation.thy
changeset 25277 95128fcdd7e8
parent 23755 1c4672d130b1
child 25287 094dab519ff5
--- 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