more concise characterization of of_nat operation and class semiring_char_0
authorhaftmann
Fri Aug 20 17:46:56 2010 +0200 (2010-08-20)
changeset 38621d6cb7e625d75
parent 38620 b40524b74f77
child 38622 86fc906dcd86
more concise characterization of of_nat operation and class semiring_char_0
src/HOL/Library/Nat_Infinity.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/NSA/StarDef.thy
src/HOL/Nat.thy
src/HOL/RealVector.thy
     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 ..