author | paulson |
Sat, 31 Jul 2004 20:54:23 +0200 | |
changeset 15094 | a7d1a3fdc30d |
parent 15013 | 34264f5e4691 |
child 15131 | c69542757a4d |
permissions | -rw-r--r-- |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
1 |
(* Title: HOL/HyperArith.thy |
14369 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1999 University of Cambridge |
|
5 |
*) |
|
6 |
||
7 |
header{*Binary arithmetic and Simplification for the Hyperreals*} |
|
8 |
||
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
9 |
theory HyperArith = HyperDef |
14369 | 10 |
files ("hypreal_arith.ML"): |
11 |
||
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
12 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
13 |
subsection{*Numerals and Arithmetic*} |
14369 | 14 |
|
15 |
instance hypreal :: number .. |
|
16 |
||
15013 | 17 |
defs (overloaded) |
18 |
hypreal_number_of_def: "(number_of w :: hypreal) == of_int (Rep_Bin w)" |
|
19 |
--{*the type constraint is essential!*} |
|
14369 | 20 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
21 |
instance hypreal :: number_ring |
15013 | 22 |
by (intro_classes, simp add: hypreal_number_of_def) |
14369 | 23 |
|
24 |
||
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
25 |
text{*Collapse applications of @{term hypreal_of_real} to @{term number_of}*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
26 |
lemma hypreal_number_of [simp]: "hypreal_of_real (number_of w) = number_of w" |
15013 | 27 |
by (simp add: hypreal_number_of_def real_number_of_def) |
28 |
||
14369 | 29 |
|
30 |
||
31 |
use "hypreal_arith.ML" |
|
10751 | 32 |
|
33 |
setup hypreal_arith_setup |
|
34 |
||
14370 | 35 |
lemma hypreal_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::hypreal) \<le> x + y" |
36 |
by arith |
|
37 |
||
14329 | 38 |
|
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
39 |
subsection{*The Function @{term hypreal_of_real}*} |
14369 | 40 |
|
41 |
lemma number_of_less_hypreal_of_real_iff [simp]: |
|
42 |
"(number_of w < hypreal_of_real z) = (number_of w < z)" |
|
43 |
apply (subst hypreal_of_real_less_iff [symmetric]) |
|
44 |
apply (simp (no_asm)) |
|
45 |
done |
|
46 |
||
47 |
lemma number_of_le_hypreal_of_real_iff [simp]: |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
48 |
"(number_of w \<le> hypreal_of_real z) = (number_of w \<le> z)" |
14369 | 49 |
apply (subst hypreal_of_real_le_iff [symmetric]) |
50 |
apply (simp (no_asm)) |
|
51 |
done |
|
52 |
||
53 |
lemma hypreal_of_real_eq_number_of_iff [simp]: |
|
54 |
"(hypreal_of_real z = number_of w) = (z = number_of w)" |
|
55 |
apply (subst hypreal_of_real_eq_iff [symmetric]) |
|
56 |
apply (simp (no_asm)) |
|
57 |
done |
|
58 |
||
59 |
lemma hypreal_of_real_less_number_of_iff [simp]: |
|
60 |
"(hypreal_of_real z < number_of w) = (z < number_of w)" |
|
61 |
apply (subst hypreal_of_real_less_iff [symmetric]) |
|
62 |
apply (simp (no_asm)) |
|
63 |
done |
|
64 |
||
65 |
lemma hypreal_of_real_le_number_of_iff [simp]: |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
66 |
"(hypreal_of_real z \<le> number_of w) = (z \<le> number_of w)" |
14369 | 67 |
apply (subst hypreal_of_real_le_iff [symmetric]) |
68 |
apply (simp (no_asm)) |
|
69 |
done |
|
70 |
||
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
71 |
subsection{*Absolute Value Function for the Hyperreals*} |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
72 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
73 |
declare abs_mult [simp] |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
74 |
|
15003 | 75 |
lemma hrabs_add_less: |
76 |
"[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)" |
|
77 |
by (simp add: abs_if split: split_if_asm) |
|
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
78 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
79 |
text{*used once in NSA*} |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
80 |
lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r" |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
81 |
by (blast intro!: order_le_less_trans abs_ge_zero) |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
82 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
83 |
lemma hrabs_disj: "abs x = (x::hypreal) | abs x = -x" |
15003 | 84 |
by (simp add: abs_if) |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
85 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
86 |
(* Needed in Geom.ML *) |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
87 |
lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y" |
15003 | 88 |
by (simp add: abs_if split add: split_if_asm) |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
89 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
90 |
lemma hypreal_of_real_hrabs: |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
91 |
"abs (hypreal_of_real r) = hypreal_of_real (abs r)" |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
92 |
apply (unfold hypreal_of_real_def) |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
93 |
apply (auto simp add: hypreal_hrabs) |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
94 |
done |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
95 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
96 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
97 |
subsection{*Embedding the Naturals into the Hyperreals*} |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
98 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
99 |
constdefs |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
100 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
101 |
hypreal_of_nat :: "nat => hypreal" |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
102 |
"hypreal_of_nat m == of_nat m" |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
103 |
|
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
104 |
lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}" |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
105 |
by (force simp add: hypreal_of_nat_def Nats_def) |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
106 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
107 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
108 |
lemma hypreal_of_nat_add [simp]: |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
109 |
"hypreal_of_nat (m + n) = hypreal_of_nat m + hypreal_of_nat n" |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
110 |
by (simp add: hypreal_of_nat_def) |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
111 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
112 |
lemma hypreal_of_nat_mult: "hypreal_of_nat (m * n) = hypreal_of_nat m * hypreal_of_nat n" |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
113 |
by (simp add: hypreal_of_nat_def) |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
114 |
declare hypreal_of_nat_mult [simp] |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
115 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
116 |
lemma hypreal_of_nat_less_iff: |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
117 |
"(n < m) = (hypreal_of_nat n < hypreal_of_nat m)" |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
118 |
apply (simp add: hypreal_of_nat_def) |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
119 |
done |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
120 |
declare hypreal_of_nat_less_iff [symmetric, simp] |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
121 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
122 |
(*------------------------------------------------------------*) |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
123 |
(* naturals embedded in hyperreals *) |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
124 |
(* is a hyperreal c.f. NS extension *) |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
125 |
(*------------------------------------------------------------*) |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
126 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
127 |
lemma hypreal_of_nat_eq: |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
128 |
"hypreal_of_nat (n::nat) = hypreal_of_real (real n)" |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
129 |
apply (induct n) |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
130 |
apply (simp_all add: hypreal_of_nat_def real_of_nat_def) |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
131 |
done |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
132 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
133 |
lemma hypreal_of_nat: |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
134 |
"hypreal_of_nat m = Abs_hypreal(hyprel``{%n. real m})" |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
135 |
apply (induct m) |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
136 |
apply (simp_all add: hypreal_of_nat_def real_of_nat_def hypreal_zero_def |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
137 |
hypreal_one_def hypreal_add) |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
138 |
done |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
139 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
140 |
lemma hypreal_of_nat_Suc: |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
141 |
"hypreal_of_nat (Suc n) = hypreal_of_nat n + (1::hypreal)" |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
142 |
by (simp add: hypreal_of_nat_def) |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
143 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
144 |
(*"neg" is used in rewrite rules for binary comparisons*) |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
145 |
lemma hypreal_of_nat_number_of [simp]: |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
146 |
"hypreal_of_nat (number_of v :: nat) = |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
147 |
(if neg (number_of v :: int) then 0 |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
148 |
else (number_of v :: hypreal))" |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
149 |
by (simp add: hypreal_of_nat_eq) |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
150 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
151 |
lemma hypreal_of_nat_zero [simp]: "hypreal_of_nat 0 = 0" |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
152 |
by (simp add: hypreal_of_nat_def) |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
153 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
154 |
lemma hypreal_of_nat_one [simp]: "hypreal_of_nat 1 = 1" |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
155 |
by (simp add: hypreal_of_nat_def) |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
156 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
157 |
lemma hypreal_of_nat_le_iff [simp]: |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
158 |
"(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)" |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
159 |
by (simp add: hypreal_of_nat_def) |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
160 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
161 |
lemma hypreal_of_nat_ge_zero [simp]: "0 \<le> hypreal_of_nat n" |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14371
diff
changeset
|
162 |
by (simp add: hypreal_of_nat_def) |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
163 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
164 |
|
14309 | 165 |
(* |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
166 |
FIXME: we should declare this, as for type int, but many proofs would break. |
14309 | 167 |
It replaces x+-y by x-y. |
168 |
Addsimps [symmetric hypreal_diff_def] |
|
169 |
*) |
|
170 |
||
14369 | 171 |
ML |
172 |
{* |
|
14370 | 173 |
val hypreal_le_add_order = thm"hypreal_le_add_order"; |
14371
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
174 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
175 |
val hypreal_of_nat_def = thm"hypreal_of_nat_def"; |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
176 |
|
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
177 |
val hrabs_add_less = thm "hrabs_add_less"; |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
178 |
val hrabs_disj = thm "hrabs_disj"; |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
179 |
val hrabs_add_lemma_disj = thm "hrabs_add_lemma_disj"; |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
180 |
val hypreal_of_real_hrabs = thm "hypreal_of_real_hrabs"; |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
181 |
val hypreal_of_nat_add = thm "hypreal_of_nat_add"; |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
182 |
val hypreal_of_nat_mult = thm "hypreal_of_nat_mult"; |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
183 |
val hypreal_of_nat_less_iff = thm "hypreal_of_nat_less_iff"; |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
184 |
val hypreal_of_nat_Suc = thm "hypreal_of_nat_Suc"; |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
185 |
val hypreal_of_nat_number_of = thm "hypreal_of_nat_number_of"; |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
186 |
val hypreal_of_nat_zero = thm "hypreal_of_nat_zero"; |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
187 |
val hypreal_of_nat_one = thm "hypreal_of_nat_one"; |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
188 |
val hypreal_of_nat_le_iff = thm"hypreal_of_nat_le_iff"; |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
189 |
val hypreal_of_nat_ge_zero = thm"hypreal_of_nat_ge_zero"; |
c78c7da09519
Conversion of HyperNat to Isar format and its declaration as a semiring
paulson
parents:
14370
diff
changeset
|
190 |
val hypreal_of_nat = thm"hypreal_of_nat"; |
14369 | 191 |
*} |
192 |
||
10751 | 193 |
end |