src/HOL/Library/Permutation.thy
changeset 25287 094dab519ff5
parent 25277 95128fcdd7e8
child 25379 12bcf37252b1
equal deleted inserted replaced
25286:35e954ff67f8 25287:094dab519ff5
   177    apply simp_all
   177    apply simp_all
   178  apply fastsimp
   178  apply fastsimp
   179 apply (metis perm_set_eq)
   179 apply (metis perm_set_eq)
   180 done
   180 done
   181 
   181 
       
   182 lemma eq_set_perm_remdups: "set xs = set ys ==> remdups xs <~~> remdups ys"
       
   183 apply(induct xs arbitrary: ys rule:length_induct)
       
   184 apply (case_tac "remdups xs", simp, simp)
       
   185 apply(subgoal_tac "a : set (remdups ys)")
       
   186  prefer 2 apply (metis set.simps(2) insert_iff set_remdups)
       
   187 apply(drule split_list) apply(elim exE conjE)
       
   188 apply(drule_tac x=list in spec) apply(erule impE) prefer 2
       
   189  apply(drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
       
   190   apply simp
       
   191   apply(subgoal_tac "a#list <~~> a#ysa@zs")
       
   192    apply (metis Cons_eq_appendI perm_append_Cons trans)
       
   193   apply (metis Cons Cons_eq_appendI distinct.simps(2) distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
       
   194  apply(subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
       
   195   apply(fastsimp simp add: insert_ident)
       
   196  apply (metis distinct_remdups set_remdups)
       
   197 apply (metis Nat.le_less_trans Suc_length_conv le_def length_remdups_leq less_Suc_eq)
       
   198 done
       
   199 
       
   200 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
       
   201 by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
       
   202 
   182 end
   203 end