21 |
21 |
22 lemma hrabs_add_less: |
22 lemma hrabs_add_less: |
23 "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)" |
23 "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)" |
24 by (simp add: abs_if split: split_if_asm) |
24 by (simp add: abs_if split: split_if_asm) |
25 |
25 |
26 text{*used once in NSA*} |
|
27 lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r" |
26 lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r" |
28 by (blast intro!: order_le_less_trans abs_ge_zero) |
27 by (blast intro!: order_le_less_trans abs_ge_zero) |
29 |
28 |
30 lemma hrabs_disj: "abs x = (x::hypreal) | abs x = -x" |
29 lemma hrabs_disj: "abs x = (x::hypreal) | abs x = -x" |
31 by (simp add: abs_if) |
30 by (simp add: abs_if) |
32 |
31 |
33 (* Needed in Geom.ML *) |
|
34 lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y" |
32 lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y" |
35 by (simp add: abs_if split add: split_if_asm) |
33 by (simp add: abs_if split add: split_if_asm) |
36 |
34 |
37 lemma hypreal_of_real_hrabs: |
35 lemma hypreal_of_real_hrabs: |
38 "abs (hypreal_of_real r) = hypreal_of_real (abs r)" |
36 "abs (hypreal_of_real r) = hypreal_of_real (abs r)" |
39 by (rule star_of_abs [symmetric]) |
37 by (rule star_of_abs [symmetric]) |
40 |
38 |
41 |
39 |
42 subsection{*Embedding the Naturals into the Hyperreals*} |
40 subsection{*Embedding the Naturals into the Hyperreals*} |
43 |
41 |
44 constdefs |
42 definition |
45 hypreal_of_nat :: "nat => hypreal" |
43 hypreal_of_nat :: "nat => hypreal" |
46 "hypreal_of_nat m == of_nat m" |
44 "hypreal_of_nat m = of_nat m" |
47 |
45 |
48 lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}" |
46 lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}" |
49 by (force simp add: hypreal_of_nat_def Nats_def) |
47 by (force simp add: hypreal_of_nat_def Nats_def) |
50 |
48 |
51 lemma hypreal_of_nat_add [simp]: |
49 lemma hypreal_of_nat_add [simp]: |
109 FIXME: we should declare this, as for type int, but many proofs would break. |
107 FIXME: we should declare this, as for type int, but many proofs would break. |
110 It replaces x+-y by x-y. |
108 It replaces x+-y by x-y. |
111 Addsimps [symmetric hypreal_diff_def] |
109 Addsimps [symmetric hypreal_diff_def] |
112 *) |
110 *) |
113 |
111 |
114 ML |
|
115 {* |
|
116 val hypreal_of_nat_def = thm"hypreal_of_nat_def"; |
|
117 |
|
118 val hrabs_add_less = thm "hrabs_add_less"; |
|
119 val hrabs_disj = thm "hrabs_disj"; |
|
120 val hrabs_add_lemma_disj = thm "hrabs_add_lemma_disj"; |
|
121 val hypreal_of_real_hrabs = thm "hypreal_of_real_hrabs"; |
|
122 val hypreal_of_nat_add = thm "hypreal_of_nat_add"; |
|
123 val hypreal_of_nat_mult = thm "hypreal_of_nat_mult"; |
|
124 val hypreal_of_nat_less_iff = thm "hypreal_of_nat_less_iff"; |
|
125 val hypreal_of_nat_Suc = thm "hypreal_of_nat_Suc"; |
|
126 val hypreal_of_nat_number_of = thm "hypreal_of_nat_number_of"; |
|
127 val hypreal_of_nat_zero = thm "hypreal_of_nat_zero"; |
|
128 val hypreal_of_nat_one = thm "hypreal_of_nat_one"; |
|
129 val hypreal_of_nat_le_iff = thm"hypreal_of_nat_le_iff"; |
|
130 val hypreal_of_nat_ge_zero = thm"hypreal_of_nat_ge_zero"; |
|
131 val hypreal_of_nat = thm"hypreal_of_nat"; |
|
132 *} |
|
133 |
|
134 end |
112 end |