# HG changeset patch # User haftmann # Date 1282319216 -7200 # Node ID d6cb7e625d7572931fe2a1422a28137d99d78887 # Parent b40524b74f7741ee1f18c42b6949b5c340741c81 more concise characterization of of_nat operation and class semiring_char_0 diff -r b40524b74f77 -r d6cb7e625d75 src/HOL/Library/Nat_Infinity.thy --- 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 (\n. of_nat n :: inat)" by (simp add: of_nat_eq_Fin) +qed subsection {* Ordering *} diff -r b40524b74f77 -r d6cb7e625d75 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- 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 \ 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 \ '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 .. diff -r b40524b74f77 -r d6cb7e625d75 src/HOL/NSA/StarDef.thy --- 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 \ 'a star)" by (rule injI) simp + then have "inj (star_of \ of_nat :: nat \ 'a star)" using inj_of_nat by (rule inj_comp) + then show "inj (of_nat :: nat \ 'a star)" by (simp add: comp_def) +qed instance star :: (ring_char_0) ring_char_0 .. diff -r b40524b74f77 -r d6cb7e625d75 src/HOL/Nat.thy --- 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 \ '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 \ 'a" -where - of_nat_0: "of_nat 0 = 0" - | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m" +definition of_nat :: "nat \ '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 \ m = n" + assumes inj_of_nat: "inj of_nat" begin +lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \ 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 \ 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 \ 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*} diff -r b40524b74f77 -r d6cb7e625d75 src/HOL/RealVector.thy --- 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 \ 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 \ of_nat)" by (rule inj_comp) + then show "inj (of_nat :: nat \ 'a)" by (simp add: comp_def) qed instance real_field < field_char_0 ..