equal
deleted
inserted
replaced
131 lemma injI: |
131 lemma injI: |
132 assumes "\<And>x y. f x = f y \<Longrightarrow> x = y" |
132 assumes "\<And>x y. f x = f y \<Longrightarrow> x = y" |
133 shows "inj f" |
133 shows "inj f" |
134 using assms unfolding inj_on_def by auto |
134 using assms unfolding inj_on_def by auto |
135 |
135 |
136 text{*For Proofs in @{text "Tools/datatype_rep_proofs"}*} |
136 text{*For Proofs in @{text "Tools/datatype_package/datatype_rep_proofs"}*} |
137 lemma datatype_injI: |
137 lemma datatype_injI: |
138 "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)" |
138 "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)" |
139 by (simp add: inj_on_def) |
139 by (simp add: inj_on_def) |
140 |
140 |
141 theorem range_ex1_eq: "inj f \<Longrightarrow> b : range f = (EX! x. b = f x)" |
141 theorem range_ex1_eq: "inj f \<Longrightarrow> b : range f = (EX! x. b = f x)" |