src/HOL/Nat.thy
 changeset 38621 d6cb7e625d75 parent 37767 a2b7a20d6ea3 child 39198 f967a16dfcdd
```     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.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
```