7 *) |
7 *) |
8 |
8 |
9 local |
9 local |
10 |
10 |
11 (* reduce contradictory <= to False *) |
11 (* reduce contradictory <= to False *) |
12 val simps = |
12 val add_rules = |
13 [order_less_irrefl, zero_eq_numeral_0, one_eq_numeral_1, |
13 [order_less_irrefl, hypreal_numeral_0_eq_0, hypreal_numeral_1_eq_1, |
14 add_hypreal_number_of, minus_hypreal_number_of, diff_hypreal_number_of, |
14 add_hypreal_number_of, minus_hypreal_number_of, diff_hypreal_number_of, |
15 mult_hypreal_number_of, eq_hypreal_number_of, less_hypreal_number_of, |
15 mult_hypreal_number_of, eq_hypreal_number_of, less_hypreal_number_of, |
16 le_hypreal_number_of_eq_not_less, hypreal_diff_def, |
16 le_hypreal_number_of_eq_not_less, hypreal_diff_def, |
17 hypreal_minus_add_distrib, hypreal_minus_minus, hypreal_mult_assoc]; |
17 hypreal_minus_add_distrib, hypreal_minus_minus, hypreal_mult_assoc, |
18 |
18 hypreal_minus_zero, |
19 val add_rules = |
19 hypreal_add_zero_left, hypreal_add_zero_right, |
20 map rename_numerals |
20 hypreal_add_minus, hypreal_add_minus_left, |
21 [hypreal_add_zero_left, hypreal_add_zero_right, |
21 hypreal_mult_0, hypreal_mult_0_right, |
22 hypreal_add_minus, hypreal_add_minus_left, |
22 hypreal_mult_1, hypreal_mult_1_right, |
23 hypreal_mult_0, hypreal_mult_0_right, |
23 hypreal_mult_minus_1, hypreal_mult_minus_1_right]; |
24 hypreal_mult_1, hypreal_mult_1_right, |
|
25 hypreal_mult_minus_1, hypreal_mult_minus_1_right]; |
|
26 |
24 |
27 val simprocs = [Hyperreal_Times_Assoc.conv, |
25 val simprocs = [Hyperreal_Times_Assoc.conv, |
28 Hyperreal_Numeral_Simprocs.combine_numerals]@ |
26 Hyperreal_Numeral_Simprocs.combine_numerals]@ |
29 Hyperreal_Numeral_Simprocs.cancel_numerals; |
27 Hyperreal_Numeral_Simprocs.cancel_numerals @ |
|
28 Hyperreal_Numeral_Simprocs.eval_numerals; |
30 |
29 |
31 val mono_ss = simpset() addsimps |
30 val mono_ss = simpset() addsimps |
32 [hypreal_add_le_mono,hypreal_add_less_mono, |
31 [hypreal_add_le_mono,hypreal_add_less_mono, |
33 hypreal_add_less_le_mono,hypreal_add_le_less_mono]; |
32 hypreal_add_less_le_mono,hypreal_add_le_less_mono]; |
34 |
33 |
67 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
66 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
68 {add_mono_thms = add_mono_thms @ add_mono_thms_hypreal, |
67 {add_mono_thms = add_mono_thms @ add_mono_thms_hypreal, |
69 mult_mono_thms = mult_mono_thms @ hypreal_mult_mono_thms, |
68 mult_mono_thms = mult_mono_thms @ hypreal_mult_mono_thms, |
70 inj_thms = inj_thms, (*FIXME: add hypreal*) |
69 inj_thms = inj_thms, (*FIXME: add hypreal*) |
71 lessD = lessD, (*We don't change LA_Data_Ref.lessD because the hypreal ordering is dense!*) |
70 lessD = lessD, (*We don't change LA_Data_Ref.lessD because the hypreal ordering is dense!*) |
72 simpset = simpset addsimps (add_rules @ simps) |
71 simpset = simpset addsimps add_rules addsimprocs simprocs}), |
73 addsimprocs simprocs}), |
|
74 arith_discrete ("HyperDef.hypreal",false), |
72 arith_discrete ("HyperDef.hypreal",false), |
75 Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]]; |
73 Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]]; |
76 |
74 |
77 end; |
75 end; |
78 |
76 |