new lemmas
authornipkow
Thu Dec 22 13:00:53 2005 +0100 (2005-12-22)
changeset 18490434e34392c40
parent 18489 151e52a4db3f
child 18491 1ce410ff9941
new lemmas
src/HOL/Equiv_Relations.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Equiv_Relations.thy	Thu Dec 22 12:27:10 2005 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Dec 22 13:00:53 2005 +0100
     1.3 @@ -90,6 +90,10 @@
     1.4    "equiv A r ==> x \<in> A ==> y \<in> A ==> (r``{x} = r``{y}) = ((x, y) \<in> r)"
     1.5    by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
     1.6  
     1.7 +lemma eq_equiv_class_iff2:
     1.8 +  "\<lbrakk> equiv A r; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> ({x}//r = {y}//r) = ((x,y) : r)"
     1.9 +by(simp add:quotient_def eq_equiv_class_iff)
    1.10 +
    1.11  
    1.12  subsection {* Quotients *}
    1.13  
     2.1 --- a/src/HOL/List.thy	Thu Dec 22 12:27:10 2005 +0100
     2.2 +++ b/src/HOL/List.thy	Thu Dec 22 13:00:53 2005 +0100
     2.3 @@ -1766,16 +1766,15 @@
     2.4  apply(rule length_remdups_leq)
     2.5  done
     2.6  
     2.7 +
     2.8 +lemma distinct_map:
     2.9 +  "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
    2.10 +by (induct xs) auto
    2.11 +
    2.12 +
    2.13  lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
    2.14  by (induct xs) auto
    2.15  
    2.16 -lemma distinct_map_filterI:
    2.17 - "distinct(map f xs) \<Longrightarrow> distinct(map f (filter P xs))"
    2.18 -apply(induct xs)
    2.19 - apply simp
    2.20 -apply force
    2.21 -done
    2.22 -
    2.23  lemma distinct_upt[simp]: "distinct[i..<j]"
    2.24  by (induct j) auto
    2.25  
    2.26 @@ -1830,6 +1829,10 @@
    2.27  apply (erule_tac x = "Suc j" in allE, simp)
    2.28  done
    2.29  
    2.30 +lemma nth_eq_iff_index_eq:
    2.31 + "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
    2.32 +by(auto simp: distinct_conv_nth)
    2.33 +
    2.34  lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
    2.35    by (induct xs) auto
    2.36  
    2.37 @@ -1851,23 +1854,10 @@
    2.38    qed
    2.39  qed
    2.40  
    2.41 -lemma inj_on_setI: "distinct(map f xs) ==> inj_on f (set xs)"
    2.42 -apply(induct xs)
    2.43 - apply simp
    2.44 -apply fastsimp
    2.45 -done
    2.46 -
    2.47 -lemma inj_on_set_conv:
    2.48 - "distinct xs \<Longrightarrow> inj_on f (set xs) = distinct(map f xs)"
    2.49 -apply(induct xs)
    2.50 - apply simp
    2.51 -apply fastsimp
    2.52 -done
    2.53 -
    2.54 -
    2.55 -lemma nth_eq_iff_index_eq:
    2.56 - "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
    2.57 -by(auto simp: distinct_conv_nth)
    2.58 +
    2.59 +lemma length_remdups_concat:
    2.60 + "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
    2.61 +by(simp add: distinct_card[symmetric])
    2.62  
    2.63  
    2.64  subsubsection {* @{text remove1} *}