src/HOL/IntDef.thy
changeset 23852 3736cdf9398b
parent 23705 315c638d5856
child 23879 4776af8be741
     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 -