62 |
62 |
63 |
63 |
64 (* rewriting *) |
64 (* rewriting *) |
65 |
65 |
66 fun simp_all_tac rules ss = |
66 fun simp_all_tac rules ss = |
67 ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps rules)); |
67 ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps rules)); |
68 |
68 |
69 val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right]; |
69 val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right]; |
70 val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right]; |
70 val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right]; |
71 |
71 |
72 fun prep_simproc (name, pats, proc) = |
72 fun prep_simproc (name, pats, proc) = |
392 Most of the work is done by the cancel tactics. |
392 Most of the work is done by the cancel tactics. |
393 *) |
393 *) |
394 val add_rules = |
394 val add_rules = |
395 [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq, |
395 [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq, |
396 One_nat_def,isolateSuc, |
396 One_nat_def,isolateSuc, |
397 order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one, |
397 order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one, |
398 zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero]; |
398 zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero]; |
399 |
399 |
400 val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s |
400 val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s |
401 (fn prems => [cut_facts_tac prems 1, |
401 (fn prems => [cut_facts_tac prems 1, |
402 blast_tac (claset() addIs [add_mono]) 1])) |
402 blast_tac (claset() addIs [add_mono]) 1])) |
429 inj_thms = inj_thms, |
429 inj_thms = inj_thms, |
430 lessD = lessD @ [Suc_leI], |
430 lessD = lessD @ [Suc_leI], |
431 neqE = [linorder_neqE_nat, |
431 neqE = [linorder_neqE_nat, |
432 get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")], |
432 get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")], |
433 simpset = HOL_basic_ss addsimps add_rules |
433 simpset = HOL_basic_ss addsimps add_rules |
434 addsimprocs [ab_group_add_cancel.sum_conv, |
434 addsimprocs [ab_group_add_cancel.sum_conv, |
435 ab_group_add_cancel.rel_conv] |
435 ab_group_add_cancel.rel_conv] |
436 (*abel_cancel helps it work in abstract algebraic domains*) |
436 (*abel_cancel helps it work in abstract algebraic domains*) |
437 addsimprocs nat_cancel_sums_add}), |
437 addsimprocs nat_cancel_sums_add}), |
438 ArithTheoryData.init, arith_discrete "nat"]; |
438 ArithTheoryData.init, arith_discrete "nat"]; |
439 |
439 |
536 *) |
536 *) |
537 |
537 |
538 (* theory setup *) |
538 (* theory setup *) |
539 |
539 |
540 val arith_setup = |
540 val arith_setup = |
541 [Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @ |
|
542 init_lin_arith_data @ |
541 init_lin_arith_data @ |
543 [Simplifier.change_simpset_of (op addSolver) |
542 [fn thy => (Simplifier.change_simpset_of thy (fn ss => ss |
544 (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac), |
543 addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc]) |
545 Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc], |
544 addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy), |
546 Method.add_methods |
545 Method.add_methods |
547 [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts, |
546 [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts, |
548 "decide linear arithmethic")], |
547 "decide linear arithmethic")], |
549 Attrib.add_attributes [("arith_split", |
548 Attrib.add_attributes [("arith_split", |
550 (Attrib.no_args arith_split_add, |
549 (Attrib.no_args arith_split_add, |
551 Attrib.no_args Attrib.undef_local_attribute), |
550 Attrib.no_args Attrib.undef_local_attribute), |
552 "declaration of split rules for arithmetic procedure")]]; |
551 "declaration of split rules for arithmetic procedure")]]; |