--- 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 -
--- 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"