|
14309
|
1 |
|
|
10751
|
2 |
theory HyperArith = HyperArith0
|
|
|
3 |
files "hypreal_arith.ML":
|
|
|
4 |
|
|
|
5 |
setup hypreal_arith_setup
|
|
|
6 |
|
|
14309
|
7 |
subsubsection{*Division By @{term 1} and @{term "-1"}*}
|
|
|
8 |
|
|
|
9 |
lemma hypreal_divide_minus1 [simp]: "x/-1 = -(x::hypreal)"
|
|
|
10 |
by simp
|
|
|
11 |
|
|
|
12 |
lemma hypreal_minus1_divide [simp]: "-1/(x::hypreal) = - (1/x)"
|
|
|
13 |
by (simp add: hypreal_divide_def hypreal_minus_inverse)
|
|
|
14 |
|
|
|
15 |
|
|
|
16 |
(*
|
|
|
17 |
FIXME: we should have this, as for type int, but many proofs would break.
|
|
|
18 |
It replaces x+-y by x-y.
|
|
|
19 |
Addsimps [symmetric hypreal_diff_def]
|
|
|
20 |
*)
|
|
|
21 |
|
|
10751
|
22 |
end
|