489 |
489 |
490 lemma map_injective: |
490 lemma map_injective: |
491 "!!xs. map f xs = map f ys ==> inj f ==> xs = ys" |
491 "!!xs. map f xs = map f ys ==> inj f ==> xs = ys" |
492 by (induct ys) (auto dest!:injD) |
492 by (induct ys) (auto dest!:injD) |
493 |
493 |
|
494 lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)" |
|
495 by(blast dest:map_injective) |
|
496 |
494 lemma inj_mapI: "inj f ==> inj (map f)" |
497 lemma inj_mapI: "inj f ==> inj (map f)" |
495 by (rules dest: map_injective injD intro: inj_onI) |
498 by (rules dest: map_injective injD intro: inj_onI) |
496 |
499 |
497 lemma inj_mapD: "inj (map f) ==> inj f" |
500 lemma inj_mapD: "inj (map f) ==> inj f" |
498 apply (unfold inj_on_def, clarify) |
501 apply (unfold inj_on_def, clarify) |
499 apply (erule_tac x = "[x]" in ballE) |
502 apply (erule_tac x = "[x]" in ballE) |
500 apply (erule_tac x = "[y]" in ballE, simp, blast) |
503 apply (erule_tac x = "[y]" in ballE, simp, blast) |
501 apply blast |
504 apply blast |
502 done |
505 done |
503 |
506 |
504 lemma inj_map: "inj (map f) = inj f" |
507 lemma inj_map[iff]: "inj (map f) = inj f" |
505 by (blast dest: inj_mapD intro: inj_mapI) |
508 by (blast dest: inj_mapD intro: inj_mapI) |
506 |
509 |
507 |
510 |
508 subsection {* @{text rev} *} |
511 subsection {* @{text rev} *} |
509 |
512 |