--- a/src/HOL/Library/Nat_Infinity.thy Fri Aug 20 17:46:55 2010 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Fri Aug 20 17:46:56 2010 +0200
@@ -227,8 +227,10 @@
apply (simp add: plus_1_iSuc iSuc_Fin)
done
-instance inat :: semiring_char_0
- by default (simp add: of_nat_eq_Fin)
+instance inat :: semiring_char_0 proof
+ have "inj Fin" by (rule injI) simp
+ then show "inj (\<lambda>n. of_nat n :: inat)" by (simp add: of_nat_eq_Fin)
+qed
subsection {* Ordering *}
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 20 17:46:55 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 20 17:46:56 2010 +0200
@@ -346,15 +346,15 @@
lemma one_index[simp]:
"(1 :: 'a::one ^'n)$i = 1" by vector
-instance cart :: (semiring_char_0,finite) semiring_char_0
-proof (intro_classes)
- fix m n ::nat
- show "(of_nat m :: 'a^'b) = of_nat n \<longleftrightarrow> m = n"
- by (simp add: Cart_eq of_nat_index)
+instance cart :: (semiring_char_0, finite) semiring_char_0
+proof
+ fix m n :: nat
+ show "inj (of_nat :: nat \<Rightarrow> 'a ^ 'b)"
+ by (auto intro!: injI simp add: Cart_eq of_nat_index)
qed
-instance cart :: (comm_ring_1,finite) comm_ring_1 by intro_classes
-instance cart :: (ring_char_0,finite) ring_char_0 by intro_classes
+instance cart :: (comm_ring_1,finite) comm_ring_1 ..
+instance cart :: (ring_char_0,finite) ring_char_0 ..
instance cart :: (real_vector,finite) real_vector ..
--- a/src/HOL/NSA/StarDef.thy Fri Aug 20 17:46:55 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy Fri Aug 20 17:46:56 2010 +0200
@@ -1000,8 +1000,11 @@
lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
by transfer (rule refl)
-instance star :: (semiring_char_0) semiring_char_0
-by intro_classes (simp only: star_of_nat_def star_of_eq of_nat_eq_iff)
+instance star :: (semiring_char_0) semiring_char_0 proof
+ have "inj (star_of :: 'a \<Rightarrow> 'a star)" by (rule injI) simp
+ then have "inj (star_of \<circ> of_nat :: nat \<Rightarrow> 'a star)" using inj_of_nat by (rule inj_comp)
+ then show "inj (of_nat :: nat \<Rightarrow> 'a star)" by (simp add: comp_def)
+qed
instance star :: (ring_char_0) ring_char_0 ..
--- a/src/HOL/Nat.thy Fri Aug 20 17:46:55 2010 +0200
+++ b/src/HOL/Nat.thy Fri Aug 20 17:46:56 2010 +0200
@@ -1227,21 +1227,27 @@
finally show ?thesis .
qed
+lemma comp_funpow:
+ fixes f :: "'a \<Rightarrow> 'a"
+ shows "comp f ^^ n = comp (f ^^ n)"
+ by (induct n) simp_all
-subsection {* Embedding of the Naturals into any
- @{text semiring_1}: @{term of_nat} *}
+
+subsection {* Embedding of the Naturals into any @{text semiring_1}: @{term of_nat} *}
context semiring_1
begin
-primrec
- of_nat :: "nat \<Rightarrow> 'a"
-where
- of_nat_0: "of_nat 0 = 0"
- | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
+definition of_nat :: "nat \<Rightarrow> 'a" where
+ "of_nat n = (plus 1 ^^ n) 0"
+
+lemma of_nat_simps [simp]:
+ shows of_nat_0: "of_nat 0 = 0"
+ and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
+ by (simp_all add: of_nat_def)
lemma of_nat_1 [simp]: "of_nat 1 = 1"
- unfolding One_nat_def by simp
+ by (simp add: of_nat_def)
lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
by (induct m) (simp_all add: add_ac)
@@ -1274,19 +1280,19 @@
Includes non-ordered rings like the complex numbers.*}
class semiring_char_0 = semiring_1 +
- assumes of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
+ assumes inj_of_nat: "inj of_nat"
begin
+lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
+ by (auto intro: inj_of_nat injD)
+
text{*Special cases where either operand is zero*}
lemma of_nat_0_eq_iff [simp, no_atp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
- by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0])
+ by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])
lemma of_nat_eq_0_iff [simp, no_atp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
- by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0])
-
-lemma inj_of_nat: "inj of_nat"
- by (simp add: inj_on_def)
+ by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
end
@@ -1315,8 +1321,8 @@
text{*Every @{text linordered_semidom} has characteristic zero.*}
-subclass semiring_char_0
- proof qed (simp add: eq_iff order_eq_iff)
+subclass semiring_char_0 proof
+qed (auto intro!: injI simp add: eq_iff)
text{*Special cases where either operand is zero*}
--- a/src/HOL/RealVector.thy Fri Aug 20 17:46:55 2010 +0200
+++ b/src/HOL/RealVector.thy Fri Aug 20 17:46:56 2010 +0200
@@ -270,6 +270,10 @@
lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
by (simp add: of_real_def)
+lemma inj_of_real:
+ "inj of_real"
+ by (auto intro: injI)
+
lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]
lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)"
@@ -291,13 +295,11 @@
by (simp add: number_of_eq)
text{*Every real algebra has characteristic zero*}
+
instance real_algebra_1 < ring_char_0
proof
- fix m n :: nat
- have "(of_real (of_nat m) = (of_real (of_nat n)::'a)) = (m = n)"
- by (simp only: of_real_eq_iff of_nat_eq_iff)
- thus "(of_nat m = (of_nat n::'a)) = (m = n)"
- by (simp only: of_real_of_nat_eq)
+ from inj_of_real inj_of_nat have "inj (of_real \<circ> of_nat)" by (rule inj_comp)
+ then show "inj (of_nat :: nat \<Rightarrow> 'a)" by (simp add: comp_def)
qed
instance real_field < field_char_0 ..