# HG changeset patch
# User haftmann
# Date 1184874457 -7200
# Node ID 3736cdf9398bcdea9b1bd28820ba26a9720b8da4
# Parent  7921b81baf96d5b90a23efd1c107b15d4fbcd597
moved set Nats to Nat.thy

diff -r 7921b81baf96 -r 3736cdf9398b src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Thu Jul 19 21:47:36 2007 +0200
+++ b/src/HOL/IntDef.thy	Thu Jul 19 21:47:37 2007 +0200
@@ -426,56 +426,12 @@
 by (simp add: linorder_not_less neg_def)
 
 
-subsection{*The Set of Natural Numbers*}
+subsection{*Embedding of the Integers into any @{text ring_1}: @{term of_int}*}
 
 constdefs
-  Nats  :: "'a::semiring_1 set"
-  "Nats == range of_nat"
-
-notation (xsymbols)
-  Nats  ("\<nat>")
-
-lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
-by (simp add: Nats_def)
-
-lemma Nats_0 [simp]: "0 \<in> Nats"
-apply (simp add: Nats_def)
-apply (rule range_eqI)
-apply (rule of_nat_0 [symmetric])
-done
-
-lemma Nats_1 [simp]: "1 \<in> Nats"
-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"
-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"
-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)"
-proof
-  fix n
-  show "of_nat n = id n"  by (induct n, simp_all)
-qed (* belongs in Nat.thy *)
-
-
-subsection{*Embedding of the Integers into any @{text ring_1}:
-@{term of_int}*}
-
-constdefs
-   of_int :: "int => 'a::ring_1"
-   "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
-
+  of_int :: "int => 'a::ring_1"
+  "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
+lemmas [code func del] = of_int_def
 
 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
 proof -
diff -r 7921b81baf96 -r 3736cdf9398b src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Jul 19 21:47:36 2007 +0200
+++ b/src/HOL/Nat.thy	Thu Jul 19 21:47:37 2007 +0200
@@ -1370,6 +1370,48 @@
   by (simp del: of_nat_add
     add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
 
+
+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)
+
+lemma Nats_0 [simp]: "0 \<in> Nats"
+apply (simp add: Nats_def)
+apply (rule range_eqI)
+apply (rule of_nat_0 [symmetric])
+done
+
+lemma Nats_1 [simp]: "1 \<in> Nats"
+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"
+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"
+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)
+
+
 instance nat :: distrib_lattice
   "inf \<equiv> min"
   "sup \<equiv> max"