author wenzelm Fri Nov 26 21:09:36 2010 +0100 (2010-11-26) changeset 40719 acb830207103 parent 40718 4d7211968607 child 40720 b770df486e5c
keep private things private, without comments;
```     1.1 --- a/src/HOL/Fun.thy	Fri Nov 26 20:52:21 2010 +0100
1.2 +++ b/src/HOL/Fun.thy	Fri Nov 26 21:09:36 2010 +0100
1.3 @@ -155,11 +155,6 @@
1.4    shows "inj f"
1.5    using assms unfolding inj_on_def by auto
1.6
1.7 -text{*For Proofs in @{text "Tools/Datatype/datatype_rep_proofs"}*}
1.8 -lemma datatype_injI:
1.9 -    "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"
1.11 -
1.12  theorem range_ex1_eq: "inj f \<Longrightarrow> b : range f = (EX! x. b = f x)"
1.13    by (unfold inj_on_def, blast)
1.14
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 26 20:52:21 2010 +0100
2.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 26 21:09:36 2010 +0100
2.3 @@ -19,7 +19,7 @@
2.4  lemma injective_scaleR:
2.5  assumes "(c :: real) ~= 0"
2.6  shows "inj (%(x :: 'n::euclidean_space). scaleR c x)"
2.7 -by (metis assms datatype_injI injI real_vector.scale_cancel_left)
2.8 +  by (metis assms injI real_vector.scale_cancel_left)
2.9
2.11  fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
```
```     3.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Nov 26 20:52:21 2010 +0100
3.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Nov 26 21:09:36 2010 +0100
3.3 @@ -54,6 +54,8 @@
3.4  val Suml_inject = @{thm Suml_inject};
3.5  val Sumr_inject = @{thm Sumr_inject};
3.6
3.7 +val datatype_injI =
3.8 +  @{lemma "(!!x. ALL y. f x = f y --> x = y) ==> inj f" by (simp add: inj_on_def)};
3.9
3.10
3.11  (** proof of characteristic theorems **)
3.12 @@ -438,8 +440,7 @@
3.13                               Lim_inject :: inj_thms') @ fun_congs) 1),
3.14                           atac 1]))])])])]);
3.15
3.16 -        val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
3.17 -                             (split_conj_thm inj_thm);
3.18 +        val inj_thms'' = map (fn r => r RS datatype_injI) (split_conj_thm inj_thm);
3.19
3.20          val elem_thm =
3.21              Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
```