equal
deleted
inserted
replaced
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 