1.1 --- a/src/HOL/Library/Nat_Infinity.thy Fri Aug 20 17:46:55 2010 +0200
1.2 +++ b/src/HOL/Library/Nat_Infinity.thy Fri Aug 20 17:46:56 2010 +0200
1.3 @@ -227,8 +227,10 @@
1.4 apply (simp add: plus_1_iSuc iSuc_Fin)
1.5 done
1.6
1.7 -instance inat :: semiring_char_0
1.8 - by default (simp add: of_nat_eq_Fin)
1.9 +instance inat :: semiring_char_0 proof
1.10 + have "inj Fin" by (rule injI) simp
1.11 + then show "inj (\<lambda>n. of_nat n :: inat)" by (simp add: of_nat_eq_Fin)
1.12 +qed
1.13
1.14
1.15 subsection {* Ordering *}
2.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 20 17:46:55 2010 +0200
2.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 20 17:46:56 2010 +0200
2.3 @@ -346,15 +346,15 @@
2.4 lemma one_index[simp]:
2.5 "(1 :: 'a::one ^'n)$i = 1" by vector
2.6
2.7 -instance cart :: (semiring_char_0,finite) semiring_char_0
2.8 -proof (intro_classes)
2.9 - fix m n ::nat
2.10 - show "(of_nat m :: 'a^'b) = of_nat n \<longleftrightarrow> m = n"
2.11 - by (simp add: Cart_eq of_nat_index)
2.12 +instance cart :: (semiring_char_0, finite) semiring_char_0
2.13 +proof
2.14 + fix m n :: nat
2.15 + show "inj (of_nat :: nat \<Rightarrow> 'a ^ 'b)"
2.16 + by (auto intro!: injI simp add: Cart_eq of_nat_index)
2.17 qed
2.18
2.19 -instance cart :: (comm_ring_1,finite) comm_ring_1 by intro_classes
2.20 -instance cart :: (ring_char_0,finite) ring_char_0 by intro_classes
2.21 +instance cart :: (comm_ring_1,finite) comm_ring_1 ..
2.22 +instance cart :: (ring_char_0,finite) ring_char_0 ..
2.23
2.24 instance cart :: (real_vector,finite) real_vector ..
2.25
3.1 --- a/src/HOL/NSA/StarDef.thy Fri Aug 20 17:46:55 2010 +0200
3.2 +++ b/src/HOL/NSA/StarDef.thy Fri Aug 20 17:46:56 2010 +0200
3.3 @@ -1000,8 +1000,11 @@
3.4 lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
3.5 by transfer (rule refl)
3.6
3.7 -instance star :: (semiring_char_0) semiring_char_0
3.8 -by intro_classes (simp only: star_of_nat_def star_of_eq of_nat_eq_iff)
3.9 +instance star :: (semiring_char_0) semiring_char_0 proof
3.10 + have "inj (star_of :: 'a \<Rightarrow> 'a star)" by (rule injI) simp
3.11 + then have "inj (star_of \<circ> of_nat :: nat \<Rightarrow> 'a star)" using inj_of_nat by (rule inj_comp)
3.12 + then show "inj (of_nat :: nat \<Rightarrow> 'a star)" by (simp add: comp_def)
3.13 +qed
3.14
3.15 instance star :: (ring_char_0) ring_char_0 ..
3.16
4.1 --- a/src/HOL/Nat.thy Fri Aug 20 17:46:55 2010 +0200
4.2 +++ b/src/HOL/Nat.thy Fri Aug 20 17:46:56 2010 +0200
4.3 @@ -1227,21 +1227,27 @@
4.4 finally show ?thesis .
4.5 qed
4.6
4.7 +lemma comp_funpow:
4.8 + fixes f :: "'a \<Rightarrow> 'a"
4.9 + shows "comp f ^^ n = comp (f ^^ n)"
4.10 + by (induct n) simp_all
4.11
4.12 -subsection {* Embedding of the Naturals into any
4.13 - @{text semiring_1}: @{term of_nat} *}
4.14 +
4.15 +subsection {* Embedding of the Naturals into any @{text semiring_1}: @{term of_nat} *}
4.16
4.17 context semiring_1
4.18 begin
4.19
4.20 -primrec
4.21 - of_nat :: "nat \<Rightarrow> 'a"
4.22 -where
4.23 - of_nat_0: "of_nat 0 = 0"
4.24 - | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
4.25 +definition of_nat :: "nat \<Rightarrow> 'a" where
4.26 + "of_nat n = (plus 1 ^^ n) 0"
4.27 +
4.28 +lemma of_nat_simps [simp]:
4.29 + shows of_nat_0: "of_nat 0 = 0"
4.30 + and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
4.31 + by (simp_all add: of_nat_def)
4.32
4.33 lemma of_nat_1 [simp]: "of_nat 1 = 1"
4.34 - unfolding One_nat_def by simp
4.35 + by (simp add: of_nat_def)
4.36
4.37 lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
4.38 by (induct m) (simp_all add: add_ac)
4.39 @@ -1274,19 +1280,19 @@
4.40 Includes non-ordered rings like the complex numbers.*}
4.41
4.42 class semiring_char_0 = semiring_1 +
4.43 - assumes of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
4.44 + assumes inj_of_nat: "inj of_nat"
4.45 begin
4.46
4.47 +lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
4.48 + by (auto intro: inj_of_nat injD)
4.49 +
4.50 text{*Special cases where either operand is zero*}
4.51
4.52 lemma of_nat_0_eq_iff [simp, no_atp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
4.53 - by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0])
4.54 + by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])
4.55
4.56 lemma of_nat_eq_0_iff [simp, no_atp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
4.57 - by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0])
4.58 -
4.59 -lemma inj_of_nat: "inj of_nat"
4.60 - by (simp add: inj_on_def)
4.61 + by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
4.62
4.63 end
4.64
4.65 @@ -1315,8 +1321,8 @@
4.66
4.67 text{*Every @{text linordered_semidom} has characteristic zero.*}
4.68
4.69 -subclass semiring_char_0
4.70 - proof qed (simp add: eq_iff order_eq_iff)
4.71 +subclass semiring_char_0 proof
4.72 +qed (auto intro!: injI simp add: eq_iff)
4.73
4.74 text{*Special cases where either operand is zero*}
4.75
5.1 --- a/src/HOL/RealVector.thy Fri Aug 20 17:46:55 2010 +0200
5.2 +++ b/src/HOL/RealVector.thy Fri Aug 20 17:46:56 2010 +0200
5.3 @@ -270,6 +270,10 @@
5.4 lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
5.5 by (simp add: of_real_def)
5.6
5.7 +lemma inj_of_real:
5.8 + "inj of_real"
5.9 + by (auto intro: injI)
5.10 +
5.11 lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]
5.12
5.13 lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)"
5.14 @@ -291,13 +295,11 @@
5.15 by (simp add: number_of_eq)
5.16
5.17 text{*Every real algebra has characteristic zero*}
5.18 +
5.19 instance real_algebra_1 < ring_char_0
5.20 proof
5.21 - fix m n :: nat
5.22 - have "(of_real (of_nat m) = (of_real (of_nat n)::'a)) = (m = n)"
5.23 - by (simp only: of_real_eq_iff of_nat_eq_iff)
5.24 - thus "(of_nat m = (of_nat n::'a)) = (m = n)"
5.25 - by (simp only: of_real_of_nat_eq)
5.26 + from inj_of_real inj_of_nat have "inj (of_real \<circ> of_nat)" by (rule inj_comp)
5.27 + then show "inj (of_nat :: nat \<Rightarrow> 'a)" by (simp add: comp_def)
5.28 qed
5.29
5.30 instance real_field < field_char_0 ..