|
14352
|
1 |
theory HyperArith = HyperBin
|
|
10751
|
2 |
files "hypreal_arith.ML":
|
|
|
3 |
|
|
|
4 |
setup hypreal_arith_setup
|
|
|
5 |
|
|
14329
|
6 |
text{*Used once in NSA*}
|
|
|
7 |
lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y"
|
|
|
8 |
apply arith
|
|
|
9 |
done
|
|
|
10 |
|
|
|
11 |
ML
|
|
|
12 |
{*
|
|
|
13 |
val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus";
|
|
|
14 |
*}
|
|
|
15 |
|
|
14309
|
16 |
subsubsection{*Division By @{term 1} and @{term "-1"}*}
|
|
|
17 |
|
|
|
18 |
lemma hypreal_divide_minus1 [simp]: "x/-1 = -(x::hypreal)"
|
|
|
19 |
by simp
|
|
|
20 |
|
|
|
21 |
lemma hypreal_minus1_divide [simp]: "-1/(x::hypreal) = - (1/x)"
|
|
|
22 |
by (simp add: hypreal_divide_def hypreal_minus_inverse)
|
|
|
23 |
|
|
|
24 |
|
|
|
25 |
(*
|
|
|
26 |
FIXME: we should have this, as for type int, but many proofs would break.
|
|
|
27 |
It replaces x+-y by x-y.
|
|
|
28 |
Addsimps [symmetric hypreal_diff_def]
|
|
|
29 |
*)
|
|
|
30 |
|
|
10751
|
31 |
end
|