91 val arith_special = thms"arith_special"; |
91 val arith_special = thms"arith_special"; |
92 |
92 |
93 structure Bin_Simprocs = |
93 structure Bin_Simprocs = |
94 struct |
94 struct |
95 fun prove_conv tacs sg (hyps: thm list) xs (t, u) = |
95 fun prove_conv tacs sg (hyps: thm list) xs (t, u) = |
96 if t aconv u then None |
96 if t aconv u then NONE |
97 else |
97 else |
98 let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) |
98 let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) |
99 in Some (Tactic.prove sg xs [] eq (K (EVERY tacs))) end |
99 in SOME (Tactic.prove sg xs [] eq (K (EVERY tacs))) end |
100 |
100 |
101 fun prove_conv_nohyps tacs sg = prove_conv tacs sg []; |
101 fun prove_conv_nohyps tacs sg = prove_conv tacs sg []; |
102 fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] []; |
102 fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] []; |
103 |
103 |
104 fun prep_simproc (name, pats, proc) = |
104 fun prep_simproc (name, pats, proc) = |
117 |
117 |
118 (*reorientation simplification procedure: reorients (polymorphic) |
118 (*reorientation simplification procedure: reorients (polymorphic) |
119 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*) |
119 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*) |
120 fun reorient_proc sg _ (_ $ t $ u) = |
120 fun reorient_proc sg _ (_ $ t $ u) = |
121 case u of |
121 case u of |
122 Const("0", _) => None |
122 Const("0", _) => NONE |
123 | Const("1", _) => None |
123 | Const("1", _) => NONE |
124 | Const("Numeral.number_of", _) $ _ => None |
124 | Const("Numeral.number_of", _) $ _ => NONE |
125 | _ => Some (case t of |
125 | _ => SOME (case t of |
126 Const("0", _) => meta_zero_reorient |
126 Const("0", _) => meta_zero_reorient |
127 | Const("1", _) => meta_one_reorient |
127 | Const("1", _) => meta_one_reorient |
128 | Const("Numeral.number_of", _) $ _ => meta_number_of_reorient) |
128 | Const("Numeral.number_of", _) $ _ => meta_number_of_reorient) |
129 |
129 |
130 val reorient_simproc = |
130 val reorient_simproc = |
303 (*combine unary minus with numeric literals, however nested within a product*) |
303 (*combine unary minus with numeric literals, however nested within a product*) |
304 val mult_minus_simps = |
304 val mult_minus_simps = |
305 [mult_assoc, minus_mult_left, minus_mult_eq_1_to_2]; |
305 [mult_assoc, minus_mult_left, minus_mult_eq_1_to_2]; |
306 |
306 |
307 (*Apply the given rewrite (if present) just once*) |
307 (*Apply the given rewrite (if present) just once*) |
308 fun trans_tac None = all_tac |
308 fun trans_tac NONE = all_tac |
309 | trans_tac (Some th) = ALLGOALS (rtac (th RS trans)); |
309 | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans)); |
310 |
310 |
311 fun simplify_meta_eq rules = |
311 fun simplify_meta_eq rules = |
312 simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules) |
312 simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules) |
313 o mk_meta_eq; |
313 o mk_meta_eq; |
314 |
314 |
536 "(m::'a::{ordered_idom,number_ring}) = n"] Fast_Arith.lin_arith_prover; |
536 "(m::'a::{ordered_idom,number_ring}) = n"] Fast_Arith.lin_arith_prover; |
537 |
537 |
538 Addsimprocs [fast_int_arith_simproc] |
538 Addsimprocs [fast_int_arith_simproc] |
539 |
539 |
540 |
540 |
541 (* Some test data |
541 (* SOME test data |
542 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"; |
542 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"; |
543 by (fast_arith_tac 1); |
543 by (fast_arith_tac 1); |
544 Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)"; |
544 Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)"; |
545 by (fast_arith_tac 1); |
545 by (fast_arith_tac 1); |
546 Goal "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d"; |
546 Goal "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d"; |