src/HOL/List.thy
changeset 18490 434e34392c40
parent 18451 5ff0244e25e8
child 18622 4524643feecc
     1.1 --- a/src/HOL/List.thy	Thu Dec 22 12:27:10 2005 +0100
     1.2 +++ b/src/HOL/List.thy	Thu Dec 22 13:00:53 2005 +0100
     1.3 @@ -1766,16 +1766,15 @@
     1.4  apply(rule length_remdups_leq)
     1.5  done
     1.6  
     1.7 +
     1.8 +lemma distinct_map:
     1.9 +  "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
    1.10 +by (induct xs) auto
    1.11 +
    1.12 +
    1.13  lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
    1.14  by (induct xs) auto
    1.15  
    1.16 -lemma distinct_map_filterI:
    1.17 - "distinct(map f xs) \<Longrightarrow> distinct(map f (filter P xs))"
    1.18 -apply(induct xs)
    1.19 - apply simp
    1.20 -apply force
    1.21 -done
    1.22 -
    1.23  lemma distinct_upt[simp]: "distinct[i..<j]"
    1.24  by (induct j) auto
    1.25  
    1.26 @@ -1830,6 +1829,10 @@
    1.27  apply (erule_tac x = "Suc j" in allE, simp)
    1.28  done
    1.29  
    1.30 +lemma nth_eq_iff_index_eq:
    1.31 + "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
    1.32 +by(auto simp: distinct_conv_nth)
    1.33 +
    1.34  lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
    1.35    by (induct xs) auto
    1.36  
    1.37 @@ -1851,23 +1854,10 @@
    1.38    qed
    1.39  qed
    1.40  
    1.41 -lemma inj_on_setI: "distinct(map f xs) ==> inj_on f (set xs)"
    1.42 -apply(induct xs)
    1.43 - apply simp
    1.44 -apply fastsimp
    1.45 -done
    1.46 -
    1.47 -lemma inj_on_set_conv:
    1.48 - "distinct xs \<Longrightarrow> inj_on f (set xs) = distinct(map f xs)"
    1.49 -apply(induct xs)
    1.50 - apply simp
    1.51 -apply fastsimp
    1.52 -done
    1.53 -
    1.54 -
    1.55 -lemma nth_eq_iff_index_eq:
    1.56 - "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
    1.57 -by(auto simp: distinct_conv_nth)
    1.58 +
    1.59 +lemma length_remdups_concat:
    1.60 + "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
    1.61 +by(simp add: distinct_card[symmetric])
    1.62  
    1.63  
    1.64  subsubsection {* @{text remove1} *}