src/HOL/List.thy
changeset 14339 ec575b7bde7a
parent 14338 a1add2de7601
child 14343 6bc647f472b9
     1.1 --- a/src/HOL/List.thy	Mon Jan 05 22:43:03 2004 +0100
     1.2 +++ b/src/HOL/List.thy	Mon Jan 05 23:10:32 2004 +0100
     1.3 @@ -491,6 +491,9 @@
     1.4   "!!xs. map f xs = map f ys ==> inj f ==> xs = ys"
     1.5  by (induct ys) (auto dest!:injD)
     1.6  
     1.7 +lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
     1.8 +by(blast dest:map_injective)
     1.9 +
    1.10  lemma inj_mapI: "inj f ==> inj (map f)"
    1.11  by (rules dest: map_injective injD intro: inj_onI)
    1.12  
    1.13 @@ -501,7 +504,7 @@
    1.14  apply blast
    1.15  done
    1.16  
    1.17 -lemma inj_map: "inj (map f) = inj f"
    1.18 +lemma inj_map[iff]: "inj (map f) = inj f"
    1.19  by (blast dest: inj_mapD intro: inj_mapI)
    1.20  
    1.21