15 [order_less_irrefl, real_numeral_0_eq_0, real_numeral_1_eq_1, |
20 [order_less_irrefl, real_numeral_0_eq_0, real_numeral_1_eq_1, |
16 real_minus_1_eq_m1, |
21 real_minus_1_eq_m1, |
17 add_real_number_of, minus_real_number_of, diff_real_number_of, |
22 add_real_number_of, minus_real_number_of, diff_real_number_of, |
18 mult_real_number_of, eq_real_number_of, less_real_number_of, |
23 mult_real_number_of, eq_real_number_of, less_real_number_of, |
19 le_real_number_of_eq_not_less, real_diff_def, |
24 le_real_number_of_eq_not_less, real_diff_def, |
20 real_minus_add_distrib, real_minus_minus, real_mult_assoc, |
25 minus_add_distrib, minus_minus, mult_assoc, minus_zero, |
21 real_minus_zero, |
26 add_zero_left, add_zero_right, left_minus, right_minus, |
22 real_add_zero_left, real_add_zero_right, |
27 mult_left_zero, mult_right_zero, mult_1, mult_1_right, |
23 real_add_minus, real_add_minus_left, |
28 minus_mult_left RS sym, minus_mult_right RS sym]; |
24 real_mult_0, real_mult_0_right, |
|
25 real_mult_1, real_mult_1_right, |
|
26 real_mult_minus_eq1, real_mult_minus_eq2]; |
|
27 |
29 |
28 val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@ |
30 val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@ |
29 Real_Numeral_Simprocs.cancel_numerals @ |
31 Real_Numeral_Simprocs.cancel_numerals @ |
30 Real_Numeral_Simprocs.eval_numerals; |
32 Real_Numeral_Simprocs.eval_numerals; |
31 |
33 |
32 val mono_ss = simpset() addsimps |
34 val mono_ss = simpset() addsimps |
33 [real_add_le_mono,real_add_less_mono, |
35 [add_mono,add_strict_mono, |
34 real_add_less_le_mono,real_add_le_less_mono]; |
36 real_add_less_le_mono,real_add_le_less_mono]; |
35 |
37 |
36 val add_mono_thms_real = |
38 val add_mono_thms_real = |
37 map (fn s => prove_goal (the_context ()) s |
39 map (fn s => prove_goal (the_context ()) s |
38 (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1])) |
40 (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1])) |
49 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; |
51 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; |
50 |
52 |
51 val real_mult_mono_thms = |
53 val real_mult_mono_thms = |
52 [(rotate_prems 1 real_mult_less_mono2, |
54 [(rotate_prems 1 real_mult_less_mono2, |
53 cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))), |
55 cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))), |
54 (real_mult_le_mono2, |
56 (real_mult_left_mono, |
55 cvar(real_mult_le_mono2, hd(tl(prems_of real_mult_le_mono2))))] |
57 cvar(real_mult_left_mono, hd(tl(prems_of real_mult_left_mono))))] |
56 |
58 |
57 in |
59 in |
58 |
60 |
59 val fast_real_arith_simproc = Simplifier.simproc (Theory.sign_of (the_context ())) |
61 val fast_real_arith_simproc = Simplifier.simproc (Theory.sign_of (the_context ())) |
60 "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"] |
62 "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"] |