equal
deleted
inserted
replaced
58 lemma Abs_inj_on: "inj_on Abs A" |
58 lemma Abs_inj_on: "inj_on Abs A" |
59 unfolding inj_on_def |
59 unfolding inj_on_def |
60 by (auto dest: Abs_inject [THEN iffD1]) |
60 by (auto dest: Abs_inject [THEN iffD1]) |
61 |
61 |
62 lemma image: "Abs ` A = UNIV" |
62 lemma image: "Abs ` A = UNIV" |
63 by (auto intro!: image_eqI) |
63 by (fact Abs_image) |
64 |
64 |
65 lemmas td_thm = type_definition_axioms |
65 lemmas td_thm = type_definition_axioms |
66 |
66 |
67 lemma fns1: "Rep \<circ> fa = fr \<circ> Rep \<or> fa \<circ> Abs = Abs \<circ> fr \<Longrightarrow> Abs \<circ> fr \<circ> Rep = fa" |
67 lemma fns1: "Rep \<circ> fa = fr \<circ> Rep \<or> fa \<circ> Abs = Abs \<circ> fr \<Longrightarrow> Abs \<circ> fr \<circ> Rep = fa" |
68 by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc) |
68 by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc) |