1.1 --- a/src/HOL/Nat.thy	Fri Aug 20 17:46:55 2010 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Aug 20 17:46:56 2010 +0200
     1.3 @@ -1227,21 +1227,27 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +lemma comp_funpow:
     1.8 +  fixes f :: "'a \<Rightarrow> 'a"
     1.9 +  shows "comp f ^^ n = comp (f ^^ n)"
    1.10 +  by (induct n) simp_all
    1.11  
    1.12 -subsection {* Embedding of the Naturals into any
    1.13 -  @{text semiring_1}: @{term of_nat} *}
    1.14 +
    1.15 +subsection {* Embedding of the Naturals into any @{text semiring_1}: @{term of_nat} *}
    1.16  
    1.17  context semiring_1
    1.18  begin
    1.19  
    1.20 -primrec
    1.21 -  of_nat :: "nat \<Rightarrow> 'a"
    1.22 -where
    1.23 -  of_nat_0:     "of_nat 0 = 0"
    1.24 -  | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
    1.25 +definition of_nat :: "nat \<Rightarrow> 'a" where
    1.26 +  "of_nat n = (plus 1 ^^ n) 0"
    1.27 +
    1.28 +lemma of_nat_simps [simp]:
    1.29 +  shows of_nat_0: "of_nat 0 = 0"
    1.30 +    and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
    1.31 +  by (simp_all add: of_nat_def)
    1.32  
    1.33  lemma of_nat_1 [simp]: "of_nat 1 = 1"
    1.34 -  unfolding One_nat_def by simp
    1.35 +  by (simp add: of_nat_def)
    1.36  
    1.37  lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
    1.38    by (induct m) (simp_all add: add_ac)
    1.39 @@ -1274,19 +1280,19 @@
    1.40   Includes non-ordered rings like the complex numbers.*}
    1.41  
    1.42  class semiring_char_0 = semiring_1 +
    1.43 -  assumes of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
    1.44 +  assumes inj_of_nat: "inj of_nat"
    1.45  begin
    1.46  
    1.47 +lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
    1.48 +  by (auto intro: inj_of_nat injD)
    1.49 +
    1.50  text{*Special cases where either operand is zero*}
    1.51  
    1.52  lemma of_nat_0_eq_iff [simp, no_atp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
    1.53 -  by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0])
    1.54 +  by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])
    1.55  
    1.56  lemma of_nat_eq_0_iff [simp, no_atp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
    1.57 -  by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0])
    1.58 -
    1.59 -lemma inj_of_nat: "inj of_nat"
    1.60 -  by (simp add: inj_on_def)
    1.61 +  by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
    1.62  
    1.63  end
    1.64  
    1.65 @@ -1315,8 +1321,8 @@
    1.66  
    1.67  text{*Every @{text linordered_semidom} has characteristic zero.*}
    1.68  
    1.69 -subclass semiring_char_0
    1.70 -  proof qed (simp add: eq_iff order_eq_iff)
    1.71 +subclass semiring_char_0 proof
    1.72 +qed (auto intro!: injI simp add: eq_iff)
    1.73  
    1.74  text{*Special cases where either operand is zero*}
    1.75