diff -r b568f8c5d5ca -r e2e1a4b00de3 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Oct 25 16:57:57 2007 +0200
+++ b/src/HOL/Nat.thy	Thu Oct 25 19:27:50 2007 +0200
@@ -1147,8 +1147,8 @@
   using Suc_le_eq less_Suc_eq_le by 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
@@ -1156,8 +1156,102 @@
 definition
   of_nat_def: "of_nat = nat_rec 0 (\<lambda>_. (op +) 1)"
 
+lemma of_nat_simps [simp, code]:
+  shows of_nat_0:   "of_nat 0 = 0"
+    and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
+  unfolding of_nat_def by simp_all
+
+lemma of_nat_1 [simp]: "of_nat 1 = 1"
+  by simp
+
+lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
+  by (induct m) (simp_all add: add_ac)
+
+lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
+  by (induct m) (simp_all add: add_ac left_distrib)
+
 end
 
+context ordered_semidom
+begin
+
+lemma zero_le_imp_of_nat: "0 \<le> of_nat m"
+  apply (induct m, simp_all)
+  apply (erule order_trans)
+  apply (rule ord_le_eq_trans [OF _ add_commute])
+  apply (rule less_add_one [THEN less_imp_le])
+  done
+
+lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n"
+  apply (induct m n rule: diff_induct, simp_all)
+  apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force)
+  done
+
+lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
+  apply (induct m n rule: diff_induct, simp_all)
+  apply (insert zero_le_imp_of_nat)
+  apply (force simp add: not_less [symmetric])
+  done
+
+lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n"
+  by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
+
+text{*Special cases where either operand is zero*}
+
+lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
+  by (rule of_nat_less_iff [of 0, simplified])
+
+lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
+  by (rule of_nat_less_iff [of _ 0, simplified])
+
+lemma of_nat_le_iff [simp]:
+  "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
+  by (simp add: not_less [symmetric] linorder_not_less [symmetric])
+
+text{*Special cases where either operand is zero*}
+
+lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
+  by (rule of_nat_le_iff [of 0, simplified])
+
+lemma of_nat_le_0_iff [simp, noatp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
+  by (rule of_nat_le_iff [of _ 0, simplified])
+
+end
+
+lemma of_nat_id [simp]: "of_nat n = n"
+  by (induct n) auto
+
+lemma of_nat_eq_id [simp]: "of_nat = id"
+  by (auto simp add: expand_fun_eq)
+
+text{*Class for unital semirings with characteristic zero.
+ 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"
+
+text{*Every @{text ordered_semidom} has characteristic zero.*}
+
+subclass (in ordered_semidom) semiring_char_0
+  by unfold_locales (simp add: eq_iff order_eq_iff)
+
+context semiring_char_0
+begin
+
+text{*Special cases where either operand is zero*}
+
+lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
+  by (rule of_nat_eq_iff [of 0, simplified])
+
+lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
+  by (rule of_nat_eq_iff [of _ 0, simplified])
+
+lemma inj_of_nat: "inj of_nat"
+  by (simp add: inj_on_def)
+
+end
+
+
 subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
 
 lemma subst_equals:
@@ -1165,7 +1259,6 @@
   shows "u = s"
   using 2 1 by (rule trans)
 
-
 use "arith_data.ML"
 declaration {* K arith_data_setup *}
 
@@ -1186,6 +1279,18 @@
     -- {* elimination of @{text -} on @{text nat} *}
 by (cases "a<b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
 
+context ring_1
+begin
+
+lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
+  by (simp del: of_nat_add
+    add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
+
+end
+
+lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
+  by (rule of_nat_0_le_iff [THEN abs_of_nonneg])
+
 lemma nat_diff_split_asm:
   "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
     -- {* elimination of @{text -} on @{text nat} in assumptions *}
@@ -1333,141 +1438,52 @@
 Least_Suc}, since there appears to be no need.*}
 
 
-subsection{*Embedding of the Naturals into any
-  @{text semiring_1}: @{term of_nat}*}
+subsection {*The Set of Natural Numbers*}
 
 context semiring_1
 begin
 
-lemma of_nat_simps [simp, code]:
-  shows of_nat_0:   "of_nat 0 = 0"
-    and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
-  unfolding of_nat_def by simp_all
+definition
+  Nats  :: "'a set"
+where
+  "Nats = range of_nat"
 
 end
 
-lemma of_nat_id [simp]: "(of_nat n \<Colon> nat) = n"
-by (induct n) auto
-
-lemma of_nat_1 [simp]: "of_nat 1 = 1"
-by simp
-
-lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
-by (induct m) (simp_all add: add_ac)
-
-lemma of_nat_mult: "of_nat (m*n) = of_nat m * of_nat n"
-by (induct m) (simp_all add: add_ac left_distrib)
-
-lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
-  apply (induct m, simp_all)
-  apply (erule order_trans)
-  apply (rule ord_le_eq_trans [OF _ add_commute])
-  apply (rule less_add_one [THEN order_less_imp_le])
-  done
-
-lemma less_imp_of_nat_less:
-    "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
-  apply (induct m n rule: diff_induct, simp_all)
-  apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force)
-  done
-
-lemma of_nat_less_imp_less:
-    "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
-  apply (induct m n rule: diff_induct, simp_all)
-  apply (insert zero_le_imp_of_nat)
-  apply (force simp add: linorder_not_less [symmetric])
-  done
-
-lemma of_nat_less_iff [simp]:
-  "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
-by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
-
-text{*Special cases where either operand is zero*}
-
-lemma of_nat_0_less_iff [simp]: "((0::'a::ordered_semidom) < of_nat n) = (0 < n)"
-by (rule of_nat_less_iff [of 0, simplified])
-
-lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < (0::'a::ordered_semidom)"
-by (rule of_nat_less_iff [of _ 0, simplified])
-
-lemma of_nat_le_iff [simp]:
-  "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
-by (simp add: linorder_not_less [symmetric])
-
-text{*Special cases where either operand is zero*}
-lemma of_nat_0_le_iff [simp]: "(0::'a::ordered_semidom) \<le> of_nat n"
-by (rule of_nat_le_iff [of 0, simplified])
-lemma of_nat_le_0_iff [simp,noatp]: "(of_nat m \<le> (0::'a::ordered_semidom)) = (m = 0)"
-by (rule of_nat_le_iff [of _ 0, simplified])
-
-text{*Class for unital semirings with characteristic zero.
- 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"
-
-text{*Every @{text ordered_semidom} has characteristic zero.*}
-instance ordered_semidom < semiring_char_0
-by intro_classes (simp add: order_eq_iff)
-
-text{*Special cases where either operand is zero*}
-lemma of_nat_0_eq_iff [simp,noatp]: "((0::'a::semiring_char_0) = of_nat n) = (0 = n)"
-by (rule of_nat_eq_iff [of 0, simplified])
-lemma of_nat_eq_0_iff [simp,noatp]: "(of_nat m = (0::'a::semiring_char_0)) = (m = 0)"
-by (rule of_nat_eq_iff [of _ 0, simplified])
-
-lemma inj_of_nat: "inj (of_nat :: nat \<Rightarrow> 'a::semiring_char_0)"
-by (simp add: inj_on_def)
-
-lemma of_nat_diff:
-  "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
-by (simp del: of_nat_add
-    add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
-
-lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
-by (rule of_nat_0_le_iff [THEN abs_of_nonneg])
-
-
-subsection {*The Set of Natural Numbers*}
-
-definition
-  Nats  :: "'a::semiring_1 set"
-where
-  "Nats = range of_nat"
-
 notation (xsymbols)
   Nats  ("\<nat>")
 
-lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
-by (simp add: Nats_def)
+context semiring_1
+begin
 
-lemma Nats_0 [simp]: "0 \<in> Nats"
+lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>"
+  by (simp add: Nats_def)
+
+lemma Nats_0 [simp]: "0 \<in> \<nat>"
 apply (simp add: Nats_def)
 apply (rule range_eqI)
 apply (rule of_nat_0 [symmetric])
 done
 
-lemma Nats_1 [simp]: "1 \<in> Nats"
+lemma Nats_1 [simp]: "1 \<in> \<nat>"
 apply (simp add: Nats_def)
 apply (rule range_eqI)
 apply (rule of_nat_1 [symmetric])
 done
 
-lemma Nats_add [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a+b \<in> Nats"
+lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>"
 apply (auto simp add: Nats_def)
 apply (rule range_eqI)
 apply (rule of_nat_add [symmetric])
 done
 
-lemma Nats_mult [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a*b \<in> Nats"
+lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>"
 apply (auto simp add: Nats_def)
 apply (rule range_eqI)
 apply (rule of_nat_mult [symmetric])
 done
 
-lemma of_nat_eq_id [simp]: "of_nat = (id :: nat => nat)"
-by (auto simp add: expand_fun_eq)
+end
 
 
 text {* the lattice order on @{typ nat} *}