src/HOL/Library/Permutation.thy
changeset 25277 95128fcdd7e8
parent 23755 1c4672d130b1
child 25287 094dab519ff5
     1.1 --- a/src/HOL/Library/Permutation.thy	Sun Nov 04 19:17:13 2007 +0100
     1.2 +++ b/src/HOL/Library/Permutation.thy	Mon Nov 05 08:31:12 2007 +0100
     1.3 @@ -46,9 +46,6 @@
     1.4  lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
     1.5    by (erule perm.induct) auto
     1.6  
     1.7 -lemma perm_mem [rule_format]: "xs <~~> ys ==> x mem xs --> x mem ys"
     1.8 -  by (erule perm.induct) auto
     1.9 -
    1.10  
    1.11  subsection {* Ways of making new permutations *}
    1.12  
    1.13 @@ -172,4 +169,14 @@
    1.14    apply (blast intro: sym)+
    1.15    done
    1.16  
    1.17 +lemma perm_set_eq: "xs <~~> ys ==> set xs = set ys"
    1.18 +by (metis multiset_of_eq_perm multiset_of_eq_setD)
    1.19 +
    1.20 +lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys"
    1.21 +apply(induct rule:perm.induct)
    1.22 +   apply simp_all
    1.23 + apply fastsimp
    1.24 +apply (metis perm_set_eq)
    1.25 +done
    1.26 +
    1.27  end