--- a/src/HOL/Fun.thy Fri Nov 26 20:52:21 2010 +0100
+++ b/src/HOL/Fun.thy Fri Nov 26 21:09:36 2010 +0100
@@ -155,11 +155,6 @@
shows "inj f"
using assms unfolding inj_on_def by auto
-text{*For Proofs in @{text "Tools/Datatype/datatype_rep_proofs"}*}
-lemma datatype_injI:
- "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"
-by (simp add: inj_on_def)
-
theorem range_ex1_eq: "inj f \<Longrightarrow> b : range f = (EX! x. b = f x)"
by (unfold inj_on_def, blast)
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 26 20:52:21 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 26 21:09:36 2010 +0100
@@ -19,7 +19,7 @@
lemma injective_scaleR:
assumes "(c :: real) ~= 0"
shows "inj (%(x :: 'n::euclidean_space). scaleR c x)"
-by (metis assms datatype_injI injI real_vector.scale_cancel_left)
+ by (metis assms injI real_vector.scale_cancel_left)
lemma linear_add_cmul:
fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Nov 26 20:52:21 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Fri Nov 26 21:09:36 2010 +0100
@@ -54,6 +54,8 @@
val Suml_inject = @{thm Suml_inject};
val Sumr_inject = @{thm Sumr_inject};
+val datatype_injI =
+ @{lemma "(!!x. ALL y. f x = f y --> x = y) ==> inj f" by (simp add: inj_on_def)};
(** proof of characteristic theorems **)
@@ -438,8 +440,7 @@
Lim_inject :: inj_thms') @ fun_congs) 1),
atac 1]))])])])]);
- val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
- (split_conj_thm inj_thm);
+ val inj_thms'' = map (fn r => r RS datatype_injI) (split_conj_thm inj_thm);
val elem_thm =
Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))