moved set Nats to Nat.thy
authorhaftmann
Thu Jul 19 21:47:37 2007 +0200 (2007-07-19)
changeset 238523736cdf9398b
parent 23851 7921b81baf96
child 23853 2c69bb1374b8
moved set Nats to Nat.thy
src/HOL/IntDef.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/IntDef.thy	Thu Jul 19 21:47:36 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Thu Jul 19 21:47:37 2007 +0200
     1.3 @@ -426,56 +426,12 @@
     1.4  by (simp add: linorder_not_less neg_def)
     1.5  
     1.6  
     1.7 -subsection{*The Set of Natural Numbers*}
     1.8 +subsection{*Embedding of the Integers into any @{text ring_1}: @{term of_int}*}
     1.9  
    1.10  constdefs
    1.11 -  Nats  :: "'a::semiring_1 set"
    1.12 -  "Nats == range of_nat"
    1.13 -
    1.14 -notation (xsymbols)
    1.15 -  Nats  ("\<nat>")
    1.16 -
    1.17 -lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
    1.18 -by (simp add: Nats_def)
    1.19 -
    1.20 -lemma Nats_0 [simp]: "0 \<in> Nats"
    1.21 -apply (simp add: Nats_def)
    1.22 -apply (rule range_eqI)
    1.23 -apply (rule of_nat_0 [symmetric])
    1.24 -done
    1.25 -
    1.26 -lemma Nats_1 [simp]: "1 \<in> Nats"
    1.27 -apply (simp add: Nats_def)
    1.28 -apply (rule range_eqI)
    1.29 -apply (rule of_nat_1 [symmetric])
    1.30 -done
    1.31 -
    1.32 -lemma Nats_add [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a+b \<in> Nats"
    1.33 -apply (auto simp add: Nats_def)
    1.34 -apply (rule range_eqI)
    1.35 -apply (rule of_nat_add [symmetric])
    1.36 -done
    1.37 -
    1.38 -lemma Nats_mult [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a*b \<in> Nats"
    1.39 -apply (auto simp add: Nats_def)
    1.40 -apply (rule range_eqI)
    1.41 -apply (rule of_nat_mult [symmetric])
    1.42 -done
    1.43 -
    1.44 -lemma of_nat_eq_id [simp]: "of_nat = (id :: nat => nat)"
    1.45 -proof
    1.46 -  fix n
    1.47 -  show "of_nat n = id n"  by (induct n, simp_all)
    1.48 -qed (* belongs in Nat.thy *)
    1.49 -
    1.50 -
    1.51 -subsection{*Embedding of the Integers into any @{text ring_1}:
    1.52 -@{term of_int}*}
    1.53 -
    1.54 -constdefs
    1.55 -   of_int :: "int => 'a::ring_1"
    1.56 -   "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
    1.57 -
    1.58 +  of_int :: "int => 'a::ring_1"
    1.59 +  "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
    1.60 +lemmas [code func del] = of_int_def
    1.61  
    1.62  lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
    1.63  proof -
     2.1 --- a/src/HOL/Nat.thy	Thu Jul 19 21:47:36 2007 +0200
     2.2 +++ b/src/HOL/Nat.thy	Thu Jul 19 21:47:37 2007 +0200
     2.3 @@ -1370,6 +1370,48 @@
     2.4    by (simp del: of_nat_add
     2.5      add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
     2.6  
     2.7 +
     2.8 +subsection {*The Set of Natural Numbers*}
     2.9 +
    2.10 +definition
    2.11 +  Nats  :: "'a::semiring_1 set"
    2.12 +where
    2.13 +  "Nats = range of_nat"
    2.14 +
    2.15 +notation (xsymbols)
    2.16 +  Nats  ("\<nat>")
    2.17 +
    2.18 +lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats"
    2.19 +  by (simp add: Nats_def)
    2.20 +
    2.21 +lemma Nats_0 [simp]: "0 \<in> Nats"
    2.22 +apply (simp add: Nats_def)
    2.23 +apply (rule range_eqI)
    2.24 +apply (rule of_nat_0 [symmetric])
    2.25 +done
    2.26 +
    2.27 +lemma Nats_1 [simp]: "1 \<in> Nats"
    2.28 +apply (simp add: Nats_def)
    2.29 +apply (rule range_eqI)
    2.30 +apply (rule of_nat_1 [symmetric])
    2.31 +done
    2.32 +
    2.33 +lemma Nats_add [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a+b \<in> Nats"
    2.34 +apply (auto simp add: Nats_def)
    2.35 +apply (rule range_eqI)
    2.36 +apply (rule of_nat_add [symmetric])
    2.37 +done
    2.38 +
    2.39 +lemma Nats_mult [simp]: "[|a \<in> Nats; b \<in> Nats|] ==> a*b \<in> Nats"
    2.40 +apply (auto simp add: Nats_def)
    2.41 +apply (rule range_eqI)
    2.42 +apply (rule of_nat_mult [symmetric])
    2.43 +done
    2.44 +
    2.45 +lemma of_nat_eq_id [simp]: "of_nat = (id :: nat => nat)"
    2.46 +  by (auto simp add: expand_fun_eq)
    2.47 +
    2.48 +
    2.49  instance nat :: distrib_lattice
    2.50    "inf \<equiv> min"
    2.51    "sup \<equiv> max"