1 (* Title: HOL/Real/real_arith.ML |
1 (* Title: HOL/Real/real_arith0.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow, TU Muenchen |
3 Author: Tobias Nipkow, TU Muenchen |
4 Copyright 1999 TU Muenchen |
4 Copyright 1999 TU Muenchen |
5 |
5 |
6 Instantiation of the generic linear arithmetic package for type real. |
6 Instantiation of the generic linear arithmetic package for type real. |
7 *) |
7 *) |
|
8 |
|
9 (** Misc ML bindings **) |
|
10 (*FIXME: move to Integ or earlier*) |
|
11 |
|
12 val left_inverse = thm "left_inverse"; |
|
13 val right_inverse = thm "right_inverse"; |
|
14 val inverse_less_iff_less = thm"Ring_and_Field.inverse_less_iff_less"; |
|
15 val inverse_eq_divide = thm"Ring_and_Field.inverse_eq_divide"; |
|
16 val inverse_minus_eq = thm "inverse_minus_eq"; |
|
17 val inverse_mult_distrib = thm "inverse_mult_distrib"; |
|
18 val inverse_add = thm "inverse_add"; |
|
19 |
|
20 val add_right_mono = thm"Ring_and_Field.add_right_mono"; |
|
21 val times_divide_eq_left = thm "times_divide_eq_left"; |
|
22 val times_divide_eq_right = thm "times_divide_eq_right"; |
|
23 val minus_minus = thm "minus_minus"; |
|
24 val minus_mult_left = thm "minus_mult_left"; |
|
25 val minus_mult_right = thm "minus_mult_right"; |
|
26 |
|
27 val pos_real_less_divide_eq = thm"pos_less_divide_eq"; |
|
28 val pos_real_divide_less_eq = thm"pos_divide_less_eq"; |
|
29 val pos_real_le_divide_eq = thm"pos_le_divide_eq"; |
|
30 val pos_real_divide_le_eq = thm"pos_divide_le_eq"; |
|
31 |
|
32 val mult_less_cancel_left = thm"Ring_and_Field.mult_less_cancel_left"; |
|
33 val mult_le_cancel_left = thm"Ring_and_Field.mult_le_cancel_left"; |
|
34 val mult_less_cancel_right = thm"Ring_and_Field.mult_less_cancel_right"; |
|
35 val mult_le_cancel_right = thm"Ring_and_Field.mult_le_cancel_right"; |
|
36 val mult_cancel_left = thm"Ring_and_Field.mult_cancel_left"; |
|
37 val mult_cancel_right = thm"Ring_and_Field.mult_cancel_right"; |
|
38 |
|
39 val field_mult_cancel_left = thm "field_mult_cancel_left"; |
|
40 val field_mult_cancel_right = thm "field_mult_cancel_right"; |
|
41 |
|
42 val mult_divide_cancel_left = thm"Ring_and_Field.mult_divide_cancel_left"; |
|
43 val mult_divide_cancel_right = thm "Ring_and_Field.mult_divide_cancel_right"; |
|
44 val mult_divide_cancel_eq_if = thm"Ring_and_Field.mult_divide_cancel_eq_if"; |
|
45 |
|
46 |
8 |
47 |
9 local |
48 local |
10 |
49 |
11 (* reduce contradictory <= to False *) |
50 (* reduce contradictory <= to False *) |
12 val add_rules = |
51 val add_rules = |