src/HOL/Library/Permutation.thy
changeset 25277 95128fcdd7e8
parent 23755 1c4672d130b1
child 25287 094dab519ff5
equal deleted inserted replaced
25276:f9237f6f3a8d 25277:95128fcdd7e8
    42 
    42 
    43 lemma perm_empty_imp: "[] <~~> xs ==> xs = []"
    43 lemma perm_empty_imp: "[] <~~> xs ==> xs = []"
    44   by (drule perm_length) auto
    44   by (drule perm_length) auto
    45 
    45 
    46 lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
    46 lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
    47   by (erule perm.induct) auto
       
    48 
       
    49 lemma perm_mem [rule_format]: "xs <~~> ys ==> x mem xs --> x mem ys"
       
    50   by (erule perm.induct) auto
    47   by (erule perm.induct) auto
    51 
    48 
    52 
    49 
    53 subsection {* Ways of making new permutations *}
    50 subsection {* Ways of making new permutations *}
    54 
    51 
   170   apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
   167   apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
   171   apply (insert surj_multiset_of, drule surjD)
   168   apply (insert surj_multiset_of, drule surjD)
   172   apply (blast intro: sym)+
   169   apply (blast intro: sym)+
   173   done
   170   done
   174 
   171 
       
   172 lemma perm_set_eq: "xs <~~> ys ==> set xs = set ys"
       
   173 by (metis multiset_of_eq_perm multiset_of_eq_setD)
       
   174 
       
   175 lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys"
       
   176 apply(induct rule:perm.induct)
       
   177    apply simp_all
       
   178  apply fastsimp
       
   179 apply (metis perm_set_eq)
       
   180 done
       
   181 
   175 end
   182 end