# HG changeset patch # User haftmann # Date 1241768887 -7200 # Node ID f591144b0f17d8ee27944bbcb51909fbae8cec9b # Parent fd7ec31f850cce843722f0afeb9bc16a6a8ef91c modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs diff -r fd7ec31f850c -r f591144b0f17 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Fri May 08 08:01:09 2009 +0200 +++ b/src/HOL/Groebner_Basis.thy Fri May 08 09:48:07 2009 +0200 @@ -635,7 +635,7 @@ val comp_conv = (Simplifier.rewrite (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} addsimps ths addsimps simp_thms - addsimprocs field_cancel_numeral_factors + addsimprocs Numeral_Simprocs.field_cancel_numeral_factors addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc] addcongs [@{thm "if_weak_cong"}])) diff -r fd7ec31f850c -r f591144b0f17 src/HOL/Int.thy --- a/src/HOL/Int.thy Fri May 08 08:01:09 2009 +0200 +++ b/src/HOL/Int.thy Fri May 08 09:48:07 2009 +0200 @@ -12,13 +12,13 @@ uses ("Tools/numeral.ML") ("Tools/numeral_syntax.ML") + ("Tools/int_arith.ML") "~~/src/Provers/Arith/assoc_fold.ML" "~~/src/Provers/Arith/cancel_numerals.ML" "~~/src/Provers/Arith/combine_numerals.ML" "~~/src/Provers/Arith/cancel_numeral_factor.ML" "~~/src/Provers/Arith/extract_common_term.ML" - ("Tools/int_factor_simprocs.ML") - ("Tools/int_arith.ML") + ("Tools/numeral_simprocs.ML") begin subsection {* The equivalence relation underlying the integers *} @@ -1518,9 +1518,10 @@ of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult of_int_0 of_int_1 of_int_add of_int_mult +use "Tools/numeral_simprocs.ML" + use "Tools/int_arith.ML" declaration {* K Int_Arith.setup *} -use "Tools/int_factor_simprocs.ML" setup {* ReorientProc.add diff -r fd7ec31f850c -r f591144b0f17 src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Fri May 08 08:01:09 2009 +0200 +++ b/src/HOL/IntDiv.thy Fri May 08 09:48:07 2009 +0200 @@ -252,8 +252,8 @@ val div_name = @{const_name div}; val mod_name = @{const_name mod}; val mk_binop = HOLogic.mk_binop; - val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT; - val dest_sum = Int_Numeral_Simprocs.dest_sum; + val mk_sum = Numeral_Simprocs.mk_sum HOLogic.intT; + val dest_sum = Numeral_Simprocs.dest_sum; val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}]; diff -r fd7ec31f850c -r f591144b0f17 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri May 08 08:01:09 2009 +0200 +++ b/src/HOL/IsaMakefile Fri May 08 09:48:07 2009 +0200 @@ -226,19 +226,19 @@ $(SRC)/Provers/Arith/combine_numerals.ML \ $(SRC)/Provers/Arith/extract_common_term.ML \ $(SRC)/Tools/Metis/metis.ML \ - Tools/int_arith.ML \ - Tools/int_factor_simprocs.ML \ - Tools/nat_simprocs.ML \ Tools/Groebner_Basis/groebner.ML \ Tools/Groebner_Basis/misc.ML \ Tools/Groebner_Basis/normalizer_data.ML \ Tools/Groebner_Basis/normalizer.ML \ Tools/atp_manager.ML \ Tools/atp_wrapper.ML \ + Tools/int_arith.ML \ Tools/list_code.ML \ Tools/meson.ML \ Tools/metis_tools.ML \ + Tools/nat_numeral_simprocs.ML \ Tools/numeral.ML \ + Tools/numeral_simprocs.ML \ Tools/numeral_syntax.ML \ Tools/polyhash.ML \ Tools/Qelim/cooper_data.ML \ diff -r fd7ec31f850c -r f591144b0f17 src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Fri May 08 08:01:09 2009 +0200 +++ b/src/HOL/Nat_Numeral.thy Fri May 08 09:48:07 2009 +0200 @@ -7,7 +7,7 @@ theory Nat_Numeral imports IntDiv -uses ("Tools/nat_simprocs.ML") +uses ("Tools/nat_numeral_simprocs.ML") begin subsection {* Numerals for natural numbers *} @@ -455,29 +455,6 @@ declare dvd_eq_mod_eq_0_number_of [simp] -ML -{* -val nat_number_of_def = thm"nat_number_of_def"; - -val nat_number_of = thm"nat_number_of"; -val nat_numeral_0_eq_0 = thm"nat_numeral_0_eq_0"; -val nat_numeral_1_eq_1 = thm"nat_numeral_1_eq_1"; -val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0"; -val numeral_2_eq_2 = thm"numeral_2_eq_2"; -val nat_div_distrib = thm"nat_div_distrib"; -val nat_mod_distrib = thm"nat_mod_distrib"; -val int_nat_number_of = thm"int_nat_number_of"; -val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1"; -val Suc_nat_number_of_add = thm"Suc_nat_number_of_add"; -val Suc_nat_number_of = thm"Suc_nat_number_of"; -val add_nat_number_of = thm"add_nat_number_of"; -val diff_nat_eq_if = thm"diff_nat_eq_if"; -val diff_nat_number_of = thm"diff_nat_number_of"; -val mult_nat_number_of = thm"mult_nat_number_of"; -val div_nat_number_of = thm"div_nat_number_of"; -val mod_nat_number_of = thm"mod_nat_number_of"; -*} - subsection{*Comparisons*} @@ -737,23 +714,6 @@ power_number_of_odd [of "number_of v", standard] - -ML -{* -val numeral_ss = @{simpset} addsimps @{thms numerals}; - -val nat_bin_arith_setup = - Lin_Arith.map_data - (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => - {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, - inj_thms = inj_thms, - lessD = lessD, neqE = neqE, - simpset = simpset addsimps @{thms neg_simps} @ - [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]}) -*} - -declaration {* K nat_bin_arith_setup *} - (* Enable arith to deal with div/mod k where k is a numeral: *) declare split_div[of _ _ "number_of k", standard, arith_split] declare split_mod[of _ _ "number_of k", standard, arith_split] @@ -912,8 +872,37 @@ subsection {* Simprocs for the Naturals *} -use "Tools/nat_simprocs.ML" -declaration {* K nat_simprocs_setup *} +use "Tools/nat_numeral_simprocs.ML" + +declaration {* +let + +val less_eq_rules = @{thms ring_distribs} @ + [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1}, + @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of}, + @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less}, + @{thm le_Suc_number_of}, @{thm le_number_of_Suc}, + @{thm less_Suc_number_of}, @{thm less_number_of_Suc}, + @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc}, + @{thm mult_Suc}, @{thm mult_Suc_right}, + @{thm add_Suc}, @{thm add_Suc_right}, + @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of}, + @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}]; + +val simprocs = Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals; + +in + +K (Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => + {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, + inj_thms = inj_thms, lessD = lessD, neqE = neqE, + simpset = simpset addsimps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]) + addsimps less_eq_rules + addsimprocs simprocs})) + +end +*} + subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*} diff -r fd7ec31f850c -r f591144b0f17 src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Fri May 08 08:01:09 2009 +0200 +++ b/src/HOL/Tools/int_arith.ML Fri May 08 09:48:07 2009 +0200 @@ -1,420 +1,15 @@ -(* Authors: Larry Paulson and Tobias Nipkow - -Simprocs and decision procedure for numerals and linear arithmetic. -*) - -structure Int_Numeral_Simprocs = -struct - -(** Utilities **) - -fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n; - -fun find_first_numeral past (t::terms) = - ((snd (HOLogic.dest_number t), rev past @ terms) - handle TERM _ => find_first_numeral (t::past) terms) - | find_first_numeral past [] = raise TERM("find_first_numeral", []); - -val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; - -fun mk_minus t = - let val T = Term.fastype_of t - in Const (@{const_name HOL.uminus}, T --> T) $ t end; - -(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) -fun mk_sum T [] = mk_number T 0 - | mk_sum T [t,u] = mk_plus (t, u) - | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); - -(*this version ALWAYS includes a trailing zero*) -fun long_mk_sum T [] = mk_number T 0 - | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); - -val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT; - -(*decompose additions AND subtractions as a sum*) -fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) = - dest_summing (pos, t, dest_summing (pos, u, ts)) - | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) = - dest_summing (pos, t, dest_summing (not pos, u, ts)) - | dest_summing (pos, t, ts) = - if pos then t::ts else mk_minus t :: ts; - -fun dest_sum t = dest_summing (true, t, []); - -val mk_diff = HOLogic.mk_binop @{const_name HOL.minus}; -val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT; - -val mk_times = HOLogic.mk_binop @{const_name HOL.times}; - -fun one_of T = Const(@{const_name HOL.one},T); - -(* build product with trailing 1 rather than Numeral 1 in order to avoid the - unnecessary restriction to type class number_ring - which is not required for cancellation of common factors in divisions. -*) -fun mk_prod T = - let val one = one_of T - fun mk [] = one - | mk [t] = t - | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts) - in mk end; - -(*This version ALWAYS includes a trailing one*) -fun long_mk_prod T [] = one_of T - | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts); - -val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT; - -fun dest_prod t = - let val (t,u) = dest_times t - in dest_prod t @ dest_prod u end - handle TERM _ => [t]; - -(*DON'T do the obvious simplifications; that would create special cases*) -fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t); - -(*Express t as a product of (possibly) a numeral with other sorted terms*) -fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t - | dest_coeff sign t = - let val ts = sort TermOrd.term_ord (dest_prod t) - val (n, ts') = find_first_numeral [] ts - handle TERM _ => (1, ts) - in (sign*n, mk_prod (Term.fastype_of t) ts') end; - -(*Find first coefficient-term THAT MATCHES u*) -fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) - | find_first_coeff past u (t::terms) = - let val (n,u') = dest_coeff 1 t - in if u aconv u' then (n, rev past @ terms) - else find_first_coeff (t::past) u terms - end - handle TERM _ => find_first_coeff (t::past) u terms; - -(*Fractions as pairs of ints. Can't use Rat.rat because the representation - needs to preserve negative values in the denominator.*) -fun mk_frac (p, q) = if q = 0 then raise Div else (p, q); - -(*Don't reduce fractions; sums must be proved by rule add_frac_eq. - Fractions are reduced later by the cancel_numeral_factor simproc.*) -fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2); - -val mk_divide = HOLogic.mk_binop @{const_name HOL.divide}; - -(*Build term (p / q) * t*) -fun mk_fcoeff ((p, q), t) = - let val T = Term.fastype_of t - in mk_times (mk_divide (mk_number T p, mk_number T q), t) end; - -(*Express t as a product of a fraction with other sorted terms*) -fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t - | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) = - let val (p, t') = dest_coeff sign t - val (q, u') = dest_coeff 1 u - in (mk_frac (p, q), mk_divide (t', u')) end - | dest_fcoeff sign t = - let val (p, t') = dest_coeff sign t - val T = Term.fastype_of t - in (mk_frac (p, 1), mk_divide (t', one_of T)) end; - - -(** New term ordering so that AC-rewriting brings numerals to the front **) - -(*Order integers by absolute value and then by sign. The standard integer - ordering is not well-founded.*) -fun num_ord (i,j) = - (case int_ord (abs i, abs j) of - EQUAL => int_ord (Int.sign i, Int.sign j) - | ord => ord); - -(*This resembles TermOrd.term_ord, but it puts binary numerals before other - non-atomic terms.*) -local open Term -in -fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) = - (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord) - | numterm_ord - (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) = - num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w) - | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS - | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER - | numterm_ord (t, u) = - (case int_ord (size_of_term t, size_of_term u) of - EQUAL => - let val (f, ts) = strip_comb t and (g, us) = strip_comb u in - (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord) - end - | ord => ord) -and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) -end; - -fun numtermless tu = (numterm_ord tu = LESS); - -val num_ss = HOL_ss settermless numtermless; - -(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*) -val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym]; - -(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) -val add_0s = @{thms add_0s}; -val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1}; - -(*Simplify inverse Numeral1, a/Numeral1*) -val inverse_1s = [@{thm inverse_numeral_1}]; -val divide_1s = [@{thm divide_numeral_1}]; - -(*To perform binary arithmetic. The "left" rewriting handles patterns - created by the Int_Numeral_Simprocs, such as 3 * (5 * x). *) -val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym, - @{thm add_number_of_left}, @{thm mult_number_of_left}] @ - @{thms arith_simps} @ @{thms rel_simps}; - -(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms - during re-arrangement*) -val non_add_simps = - subtract Thm.eq_thm [@{thm add_number_of_left}, @{thm number_of_add} RS sym] simps; - -(*To evaluate binary negations of coefficients*) -val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym] @ - @{thms minus_bin_simps} @ @{thms pred_bin_simps}; - -(*To let us treat subtraction as addition*) -val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}]; - -(*To let us treat division as multiplication*) -val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}]; - -(*push the unary minus down: - x * y = x * - y *) -val minus_mult_eq_1_to_2 = - [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> standard; - -(*to extract again any uncancelled minuses*) -val minus_from_mult_simps = - [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}]; - -(*combine unary minus with numeric literals, however nested within a product*) -val mult_minus_simps = - [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2]; - -val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ - diff_simps @ minus_simps @ @{thms add_ac} -val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps -val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} +(* Author: Tobias Nipkow -structure CancelNumeralsCommon = - struct - val mk_sum = mk_sum - val dest_sum = dest_sum - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - val find_first_coeff = find_first_coeff [] - val trans_tac = K Arith_Data.trans_tac - - fun norm_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) - - val numeral_simp_ss = HOL_ss addsimps add_0s @ simps - fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s) - end; - - -structure EqCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin "op =" Term.dummyT - val bal_add1 = @{thm eq_add_iff1} RS trans - val bal_add2 = @{thm eq_add_iff2} RS trans -); - -structure LessCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT - val bal_add1 = @{thm less_add_iff1} RS trans - val bal_add2 = @{thm less_add_iff2} RS trans -); - -structure LeCancelNumerals = CancelNumeralsFun - (open CancelNumeralsCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT - val bal_add1 = @{thm le_add_iff1} RS trans - val bal_add2 = @{thm le_add_iff2} RS trans -); - -val cancel_numerals = - map Arith_Data.prep_simproc - [("inteq_cancel_numerals", - ["(l::'a::number_ring) + m = n", - "(l::'a::number_ring) = m + n", - "(l::'a::number_ring) - m = n", - "(l::'a::number_ring) = m - n", - "(l::'a::number_ring) * m = n", - "(l::'a::number_ring) = m * n"], - K EqCancelNumerals.proc), - ("intless_cancel_numerals", - ["(l::'a::{ordered_idom,number_ring}) + m < n", - "(l::'a::{ordered_idom,number_ring}) < m + n", - "(l::'a::{ordered_idom,number_ring}) - m < n", - "(l::'a::{ordered_idom,number_ring}) < m - n", - "(l::'a::{ordered_idom,number_ring}) * m < n", - "(l::'a::{ordered_idom,number_ring}) < m * n"], - K LessCancelNumerals.proc), - ("intle_cancel_numerals", - ["(l::'a::{ordered_idom,number_ring}) + m <= n", - "(l::'a::{ordered_idom,number_ring}) <= m + n", - "(l::'a::{ordered_idom,number_ring}) - m <= n", - "(l::'a::{ordered_idom,number_ring}) <= m - n", - "(l::'a::{ordered_idom,number_ring}) * m <= n", - "(l::'a::{ordered_idom,number_ring}) <= m * n"], - K LeCancelNumerals.proc)]; - - -structure CombineNumeralsData = - struct - type coeff = int - val iszero = (fn x => x = 0) - val add = op + - val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) - val dest_sum = dest_sum - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - val left_distrib = @{thm combine_common_factor} RS trans - val prove_conv = Arith_Data.prove_conv_nohyps - val trans_tac = K Arith_Data.trans_tac - - fun norm_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) - - val numeral_simp_ss = HOL_ss addsimps add_0s @ simps - fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s) - end; - -structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); - -(*Version for fields, where coefficients can be fractions*) -structure FieldCombineNumeralsData = - struct - type coeff = int * int - val iszero = (fn (p, q) => p = 0) - val add = add_frac - val mk_sum = long_mk_sum - val dest_sum = dest_sum - val mk_coeff = mk_fcoeff - val dest_coeff = dest_fcoeff 1 - val left_distrib = @{thm combine_common_factor} RS trans - val prove_conv = Arith_Data.prove_conv_nohyps - val trans_tac = K Arith_Data.trans_tac - - val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps - fun norm_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1a)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) - - val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}] - fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s) - end; - -structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData); - -val combine_numerals = - Arith_Data.prep_simproc - ("int_combine_numerals", - ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], - K CombineNumerals.proc); - -val field_combine_numerals = - Arith_Data.prep_simproc - ("field_combine_numerals", - ["(i::'a::{number_ring,field,division_by_zero}) + j", - "(i::'a::{number_ring,field,division_by_zero}) - j"], - K FieldCombineNumerals.proc); - -(** Constant folding for multiplication in semirings **) - -(*We do not need folding for addition: combine_numerals does the same thing*) - -structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = -struct - val assoc_ss = HOL_ss addsimps @{thms mult_ac} - val eq_reflection = eq_reflection - fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true - | is_numeral _ = false; -end; - -structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); - -val assoc_fold_simproc = - Arith_Data.prep_simproc - ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"], - K Semiring_Times_Assoc.proc); - -end; - -Addsimprocs Int_Numeral_Simprocs.cancel_numerals; -Addsimprocs [Int_Numeral_Simprocs.combine_numerals]; -Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals]; -Addsimprocs [Int_Numeral_Simprocs.assoc_fold_simproc]; - -(*examples: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s, by (Simp_tac 1)); - -test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"; - -test "2*u = (u::int)"; -test "(i + j + 12 + (k::int)) - 15 = y"; -test "(i + j + 12 + (k::int)) - 5 = y"; - -test "y - b < (b::int)"; -test "y - (3*b + c) < (b::int) - 2*c"; - -test "(2*x - (u*v) + y) - v*3*u = (w::int)"; -test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"; -test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"; -test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"; - -test "(i + j + 12 + (k::int)) = u + 15 + y"; -test "(i + j*2 + 12 + (k::int)) = j + 5 + y"; - -test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"; - -test "a + -(b+c) + b = (d::int)"; -test "a + -(b+c) - b = (d::int)"; - -(*negative numerals*) -test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"; -test "(i + j + -3 + (k::int)) < u + 5 + y"; -test "(i + j + 3 + (k::int)) < u + -6 + y"; -test "(i + j + -12 + (k::int)) - 15 = y"; -test "(i + j + 12 + (k::int)) - -15 = y"; -test "(i + j + -12 + (k::int)) - -15 = y"; -*) - -(*** decision procedure for linear arithmetic ***) - -(*---------------------------------------------------------------------------*) -(* Linear arithmetic *) -(*---------------------------------------------------------------------------*) - -(* Instantiation of the generic linear arithmetic package for int. *) -structure Int_Arith = +signature INT_ARITH = +sig + val fast_int_arith_simproc: simproc + val setup: Context.generic -> Context.generic +end + +structure Int_Arith : INT_ARITH = struct (* Update parameters of arithmetic prover *) @@ -491,9 +86,9 @@ val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2] -val int_numeral_base_simprocs = Int_Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc - :: Int_Numeral_Simprocs.combine_numerals - :: Int_Numeral_Simprocs.cancel_numerals; +val numeral_base_simprocs = Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc + :: Numeral_Simprocs.combine_numerals + :: Numeral_Simprocs.cancel_numerals; val setup = Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => @@ -503,7 +98,7 @@ lessD = lessD @ [@{thm zless_imp_add1_zle}], neqE = neqE, simpset = simpset addsimps add_rules - addsimprocs int_numeral_base_simprocs + addsimprocs numeral_base_simprocs addcongs [if_weak_cong]}) #> arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #> arith_discrete @{type_name Int.int} diff -r fd7ec31f850c -r f591144b0f17 src/HOL/Tools/int_factor_simprocs.ML --- a/src/HOL/Tools/int_factor_simprocs.ML Fri May 08 08:01:09 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,391 +0,0 @@ -(* Title: HOL/int_factor_simprocs.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2000 University of Cambridge - -Factor cancellation simprocs for the integers (and for fields). - -This file can't be combined with int_arith1 because it requires IntDiv.thy. -*) - - -(*To quote from Provers/Arith/cancel_numeral_factor.ML: - -Cancels common coefficients in balanced expressions: - - u*#m ~~ u'*#m' == #n*u ~~ #n'*u' - -where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /) -and d = gcd(m,m') and n=m/d and n'=m'/d. -*) - -val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}]; - -local - open Int_Numeral_Simprocs -in - -structure CancelNumeralFactorCommon = - struct - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - val trans_tac = K Arith_Data.trans_tac - - val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s - val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps - val norm_ss3 = HOL_ss addsimps @{thms mult_ac} - fun norm_tac ss = - ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) - THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) - - val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps - fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - val simplify_meta_eq = Arith_Data.simplify_meta_eq - [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left}, - @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}]; - end - -(*Version for semiring_div*) -structure DivCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name Divides.div} - val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT - val cancel = @{thm div_mult_mult1} RS trans - val neg_exchanges = false -) - -(*Version for fields*) -structure DivideCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} - val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT - val cancel = @{thm mult_divide_mult_cancel_left} RS trans - val neg_exchanges = false -) - -structure EqCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin "op =" Term.dummyT - val cancel = @{thm mult_cancel_left} RS trans - val neg_exchanges = false -) - -structure LessCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT - val cancel = @{thm mult_less_cancel_left} RS trans - val neg_exchanges = true -) - -structure LeCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT - val cancel = @{thm mult_le_cancel_left} RS trans - val neg_exchanges = true -) - -val cancel_numeral_factors = - map Arith_Data.prep_simproc - [("ring_eq_cancel_numeral_factor", - ["(l::'a::{idom,number_ring}) * m = n", - "(l::'a::{idom,number_ring}) = m * n"], - K EqCancelNumeralFactor.proc), - ("ring_less_cancel_numeral_factor", - ["(l::'a::{ordered_idom,number_ring}) * m < n", - "(l::'a::{ordered_idom,number_ring}) < m * n"], - K LessCancelNumeralFactor.proc), - ("ring_le_cancel_numeral_factor", - ["(l::'a::{ordered_idom,number_ring}) * m <= n", - "(l::'a::{ordered_idom,number_ring}) <= m * n"], - K LeCancelNumeralFactor.proc), - ("int_div_cancel_numeral_factors", - ["((l::'a::{semiring_div,number_ring}) * m) div n", - "(l::'a::{semiring_div,number_ring}) div (m * n)"], - K DivCancelNumeralFactor.proc), - ("divide_cancel_numeral_factor", - ["((l::'a::{division_by_zero,field,number_ring}) * m) / n", - "(l::'a::{division_by_zero,field,number_ring}) / (m * n)", - "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"], - K DivideCancelNumeralFactor.proc)]; - -(* referenced by rat_arith.ML *) -val field_cancel_numeral_factors = - map Arith_Data.prep_simproc - [("field_eq_cancel_numeral_factor", - ["(l::'a::{field,number_ring}) * m = n", - "(l::'a::{field,number_ring}) = m * n"], - K EqCancelNumeralFactor.proc), - ("field_cancel_numeral_factor", - ["((l::'a::{division_by_zero,field,number_ring}) * m) / n", - "(l::'a::{division_by_zero,field,number_ring}) / (m * n)", - "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"], - K DivideCancelNumeralFactor.proc)] - -end; - -Addsimprocs cancel_numeral_factors; - -(*examples: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s; by (Simp_tac 1)); - -test "9*x = 12 * (y::int)"; -test "(9*x) div (12 * (y::int)) = z"; -test "9*x < 12 * (y::int)"; -test "9*x <= 12 * (y::int)"; - -test "-99*x = 132 * (y::int)"; -test "(-99*x) div (132 * (y::int)) = z"; -test "-99*x < 132 * (y::int)"; -test "-99*x <= 132 * (y::int)"; - -test "999*x = -396 * (y::int)"; -test "(999*x) div (-396 * (y::int)) = z"; -test "999*x < -396 * (y::int)"; -test "999*x <= -396 * (y::int)"; - -test "-99*x = -81 * (y::int)"; -test "(-99*x) div (-81 * (y::int)) = z"; -test "-99*x <= -81 * (y::int)"; -test "-99*x < -81 * (y::int)"; - -test "-2 * x = -1 * (y::int)"; -test "-2 * x = -(y::int)"; -test "(-2 * x) div (-1 * (y::int)) = z"; -test "-2 * x < -(y::int)"; -test "-2 * x <= -1 * (y::int)"; -test "-x < -23 * (y::int)"; -test "-x <= -23 * (y::int)"; -*) - -(*And the same examples for fields such as rat or real: -test "0 <= (y::rat) * -2"; -test "9*x = 12 * (y::rat)"; -test "(9*x) / (12 * (y::rat)) = z"; -test "9*x < 12 * (y::rat)"; -test "9*x <= 12 * (y::rat)"; - -test "-99*x = 132 * (y::rat)"; -test "(-99*x) / (132 * (y::rat)) = z"; -test "-99*x < 132 * (y::rat)"; -test "-99*x <= 132 * (y::rat)"; - -test "999*x = -396 * (y::rat)"; -test "(999*x) / (-396 * (y::rat)) = z"; -test "999*x < -396 * (y::rat)"; -test "999*x <= -396 * (y::rat)"; - -test "(- ((2::rat) * x) <= 2 * y)"; -test "-99*x = -81 * (y::rat)"; -test "(-99*x) / (-81 * (y::rat)) = z"; -test "-99*x <= -81 * (y::rat)"; -test "-99*x < -81 * (y::rat)"; - -test "-2 * x = -1 * (y::rat)"; -test "-2 * x = -(y::rat)"; -test "(-2 * x) / (-1 * (y::rat)) = z"; -test "-2 * x < -(y::rat)"; -test "-2 * x <= -1 * (y::rat)"; -test "-x < -23 * (y::rat)"; -test "-x <= -23 * (y::rat)"; -*) - - -(** Declarations for ExtractCommonTerm **) - -local - open Int_Numeral_Simprocs -in - -(*Find first term that matches u*) -fun find_first_t past u [] = raise TERM ("find_first_t", []) - | find_first_t past u (t::terms) = - if u aconv t then (rev past @ terms) - else find_first_t (t::past) u terms - handle TERM _ => find_first_t (t::past) u terms; - -(** Final simplification for the CancelFactor simprocs **) -val simplify_one = Arith_Data.simplify_meta_eq - [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}]; - -fun cancel_simplify_meta_eq ss cancel_th th = - simplify_one ss (([th, cancel_th]) MRS trans); - -local - val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory HOL} HOLogic.Trueprop) - fun Eq_True_elim Eq = - Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI} -in -fun sign_conv pos_th neg_th ss t = - let val T = fastype_of t; - val zero = Const(@{const_name HOL.zero}, T); - val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT); - val pos = less $ zero $ t and neg = less $ t $ zero - fun prove p = - Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p) - handle THM _ => NONE - in case prove pos of - SOME th => SOME(th RS pos_th) - | NONE => (case prove neg of - SOME th => SOME(th RS neg_th) - | NONE => NONE) - end; -end - -structure CancelFactorCommon = - struct - val mk_sum = long_mk_prod - val dest_sum = dest_prod - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val find_first = find_first_t [] - val trans_tac = K Arith_Data.trans_tac - val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} - fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) - val simplify_meta_eq = cancel_simplify_meta_eq - end; - -(*mult_cancel_left requires a ring with no zero divisors.*) -structure EqCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin "op =" Term.dummyT - val simp_conv = K (K (SOME @{thm mult_cancel_left})) -); - -(*for ordered rings*) -structure LeCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT - val simp_conv = sign_conv - @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg} -); - -(*for ordered rings*) -structure LessCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} - val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT - val simp_conv = sign_conv - @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg} -); - -(*for semirings with division*) -structure DivCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name Divides.div} - val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT - val simp_conv = K (K (SOME @{thm div_mult_mult1_if})) -); - -structure ModCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name Divides.mod} - val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT - val simp_conv = K (K (SOME @{thm mod_mult_mult1})) -); - -(*for idoms*) -structure DvdCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} - val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT - val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left})) -); - -(*Version for all fields, including unordered ones (type complex).*) -structure DivideCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} - val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT - val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if})) -); - -val cancel_factors = - map Arith_Data.prep_simproc - [("ring_eq_cancel_factor", - ["(l::'a::idom) * m = n", - "(l::'a::idom) = m * n"], - K EqCancelFactor.proc), - ("ordered_ring_le_cancel_factor", - ["(l::'a::ordered_ring) * m <= n", - "(l::'a::ordered_ring) <= m * n"], - K LeCancelFactor.proc), - ("ordered_ring_less_cancel_factor", - ["(l::'a::ordered_ring) * m < n", - "(l::'a::ordered_ring) < m * n"], - K LessCancelFactor.proc), - ("int_div_cancel_factor", - ["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"], - K DivCancelFactor.proc), - ("int_mod_cancel_factor", - ["((l::'a::semiring_div) * m) mod n", "(l::'a::semiring_div) mod (m * n)"], - K ModCancelFactor.proc), - ("dvd_cancel_factor", - ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"], - K DvdCancelFactor.proc), - ("divide_cancel_factor", - ["((l::'a::{division_by_zero,field}) * m) / n", - "(l::'a::{division_by_zero,field}) / (m * n)"], - K DivideCancelFactor.proc)]; - -end; - -Addsimprocs cancel_factors; - - -(*examples: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s; by (Asm_simp_tac 1)); - -test "x*k = k*(y::int)"; -test "k = k*(y::int)"; -test "a*(b*c) = (b::int)"; -test "a*(b*c) = d*(b::int)*(x*a)"; - -test "(x*k) div (k*(y::int)) = (uu::int)"; -test "(k) div (k*(y::int)) = (uu::int)"; -test "(a*(b*c)) div ((b::int)) = (uu::int)"; -test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"; -*) - -(*And the same examples for fields such as rat or real: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s; by (Asm_simp_tac 1)); - -test "x*k = k*(y::rat)"; -test "k = k*(y::rat)"; -test "a*(b*c) = (b::rat)"; -test "a*(b*c) = d*(b::rat)*(x*a)"; - - -test "(x*k) / (k*(y::rat)) = (uu::rat)"; -test "(k) / (k*(y::rat)) = (uu::rat)"; -test "(a*(b*c)) / ((b::rat)) = (uu::rat)"; -test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"; - -(*FIXME: what do we do about this?*) -test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"; -*) diff -r fd7ec31f850c -r f591144b0f17 src/HOL/Tools/nat_numeral_simprocs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Fri May 08 09:48:07 2009 +0200 @@ -0,0 +1,538 @@ +(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory + +Simprocs for nat numerals. +*) + +signature NAT_NUMERAL_SIMPROCS = +sig + val combine_numerals: simproc + val cancel_numerals: simproc list + val cancel_factors: simproc list + val cancel_numeral_factors: simproc list +end; + +structure Nat_Numeral_Simprocs = +struct + +(*Maps n to #n for n = 0, 1, 2*) +val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym]; +val numeral_sym_ss = HOL_ss addsimps numeral_syms; + +fun rename_numerals th = + simplify numeral_sym_ss (Thm.transfer (the_context ()) th); + +(*Utilities*) + +fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n; +fun dest_number t = Int.max (0, snd (HOLogic.dest_number t)); + +fun find_first_numeral past (t::terms) = + ((dest_number t, t, rev past @ terms) + handle TERM _ => find_first_numeral (t::past) terms) + | find_first_numeral past [] = raise TERM("find_first_numeral", []); + +val zero = mk_number 0; +val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; + +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) +fun mk_sum [] = zero + | mk_sum [t,u] = mk_plus (t, u) + | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); + +(*this version ALWAYS includes a trailing zero*) +fun long_mk_sum [] = HOLogic.zero + | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); + +val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT; + + +(** Other simproc items **) + +val bin_simps = + [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, + @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, + @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less}, + @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, + @{thm less_nat_number_of}, + @{thm Let_number_of}, @{thm nat_number_of}] @ + @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps}; + + +(*** CancelNumerals simprocs ***) + +val one = mk_number 1; +val mk_times = HOLogic.mk_binop @{const_name HOL.times}; + +fun mk_prod [] = one + | mk_prod [t] = t + | mk_prod (t :: ts) = if t = one then mk_prod ts + else mk_times (t, mk_prod ts); + +val dest_times = HOLogic.dest_bin @{const_name HOL.times} HOLogic.natT; + +fun dest_prod t = + let val (t,u) = dest_times t + in dest_prod t @ dest_prod u end + handle TERM _ => [t]; + +(*DON'T do the obvious simplifications; that would create special cases*) +fun mk_coeff (k,t) = mk_times (mk_number k, t); + +(*Express t as a product of (possibly) a numeral with other factors, sorted*) +fun dest_coeff t = + let val ts = sort TermOrd.term_ord (dest_prod t) + val (n, _, ts') = find_first_numeral [] ts + handle TERM _ => (1, one, ts) + in (n, mk_prod ts') end; + +(*Find first coefficient-term THAT MATCHES u*) +fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) + | find_first_coeff past u (t::terms) = + let val (n,u') = dest_coeff t + in if u aconv u' then (n, rev past @ terms) + else find_first_coeff (t::past) u terms + end + handle TERM _ => find_first_coeff (t::past) u terms; + + +(*Split up a sum into the list of its constituent terms, on the way removing any + Sucs and counting them.*) +fun dest_Suc_sum (Const ("Suc", _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts)) + | dest_Suc_sum (t, (k,ts)) = + let val (t1,t2) = dest_plus t + in dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts))) end + handle TERM _ => (k, t::ts); + +(*Code for testing whether numerals are already used in the goal*) +fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true + | is_numeral _ = false; + +fun prod_has_numeral t = exists is_numeral (dest_prod t); + +(*The Sucs found in the term are converted to a binary numeral. If relaxed is false, + an exception is raised unless the original expression contains at least one + numeral in a coefficient position. This prevents nat_combine_numerals from + introducing numerals to goals.*) +fun dest_Sucs_sum relaxed t = + let val (k,ts) = dest_Suc_sum (t,(0,[])) + in + if relaxed orelse exists prod_has_numeral ts then + if k=0 then ts + else mk_number k :: ts + else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t]) + end; + + +(*Simplify 1*n and n*1 to n*) +val add_0s = map rename_numerals [@{thm add_0}, @{thm add_0_right}]; +val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}]; + +(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*) + +(*And these help the simproc return False when appropriate, which helps + the arith prover.*) +val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc}, + @{thm Suc_not_Zero}, @{thm le_0_eq}]; + +val simplify_meta_eq = + Arith_Data.simplify_meta_eq + ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm add_0_right}, + @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules); + + +(*** Applying CancelNumeralsFun ***) + +structure CancelNumeralsCommon = + struct + val mk_sum = (fn T:typ => mk_sum) + val dest_sum = dest_Sucs_sum true + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val find_first_coeff = find_first_coeff [] + val trans_tac = K Arith_Data.trans_tac + + val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ + [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac} + val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + + val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)); + val simplify_meta_eq = simplify_meta_eq + end; + + +structure EqCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT + val bal_add1 = @{thm nat_eq_add_iff1} RS trans + val bal_add2 = @{thm nat_eq_add_iff2} RS trans +); + +structure LessCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT + val bal_add1 = @{thm nat_less_add_iff1} RS trans + val bal_add2 = @{thm nat_less_add_iff2} RS trans +); + +structure LeCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT + val bal_add1 = @{thm nat_le_add_iff1} RS trans + val bal_add2 = @{thm nat_le_add_iff2} RS trans +); + +structure DiffCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name HOL.minus} + val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT + val bal_add1 = @{thm nat_diff_add_eq1} RS trans + val bal_add2 = @{thm nat_diff_add_eq2} RS trans +); + + +val cancel_numerals = + map Arith_Data.prep_simproc + [("nateq_cancel_numerals", + ["(l::nat) + m = n", "(l::nat) = m + n", + "(l::nat) * m = n", "(l::nat) = m * n", + "Suc m = n", "m = Suc n"], + K EqCancelNumerals.proc), + ("natless_cancel_numerals", + ["(l::nat) + m < n", "(l::nat) < m + n", + "(l::nat) * m < n", "(l::nat) < m * n", + "Suc m < n", "m < Suc n"], + K LessCancelNumerals.proc), + ("natle_cancel_numerals", + ["(l::nat) + m <= n", "(l::nat) <= m + n", + "(l::nat) * m <= n", "(l::nat) <= m * n", + "Suc m <= n", "m <= Suc n"], + K LeCancelNumerals.proc), + ("natdiff_cancel_numerals", + ["((l::nat) + m) - n", "(l::nat) - (m + n)", + "(l::nat) * m - n", "(l::nat) - m * n", + "Suc m - n", "m - Suc n"], + K DiffCancelNumerals.proc)]; + + +(*** Applying CombineNumeralsFun ***) + +structure CombineNumeralsData = + struct + type coeff = int + val iszero = (fn x => x = 0) + val add = op + + val mk_sum = (fn T:typ => long_mk_sum) (*to work for 2*x + 3*x *) + val dest_sum = dest_Sucs_sum false + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val left_distrib = @{thm left_add_mult_distrib} RS trans + val prove_conv = Arith_Data.prove_conv_nohyps + val trans_tac = K Arith_Data.trans_tac + + val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac} + val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + + val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) + val simplify_meta_eq = simplify_meta_eq + end; + +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); + +val combine_numerals = + Arith_Data.prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc); + + +(*** Applying CancelNumeralFactorFun ***) + +structure CancelNumeralFactorCommon = + struct + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val trans_tac = K Arith_Data.trans_tac + + val norm_ss1 = Numeral_Simprocs.num_ss addsimps + numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac} + val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + + val numeral_simp_ss = HOL_ss addsimps bin_simps + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) + val simplify_meta_eq = simplify_meta_eq + end + +structure DivCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name Divides.div} + val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT + val cancel = @{thm nat_mult_div_cancel1} RS trans + val neg_exchanges = false +) + +structure DvdCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} + val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT + val cancel = @{thm nat_mult_dvd_cancel1} RS trans + val neg_exchanges = false +) + +structure EqCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT + val cancel = @{thm nat_mult_eq_cancel1} RS trans + val neg_exchanges = false +) + +structure LessCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT + val cancel = @{thm nat_mult_less_cancel1} RS trans + val neg_exchanges = true +) + +structure LeCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT + val cancel = @{thm nat_mult_le_cancel1} RS trans + val neg_exchanges = true +) + +val cancel_numeral_factors = + map Arith_Data.prep_simproc + [("nateq_cancel_numeral_factors", + ["(l::nat) * m = n", "(l::nat) = m * n"], + K EqCancelNumeralFactor.proc), + ("natless_cancel_numeral_factors", + ["(l::nat) * m < n", "(l::nat) < m * n"], + K LessCancelNumeralFactor.proc), + ("natle_cancel_numeral_factors", + ["(l::nat) * m <= n", "(l::nat) <= m * n"], + K LeCancelNumeralFactor.proc), + ("natdiv_cancel_numeral_factors", + ["((l::nat) * m) div n", "(l::nat) div (m * n)"], + K DivCancelNumeralFactor.proc), + ("natdvd_cancel_numeral_factors", + ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"], + K DvdCancelNumeralFactor.proc)]; + + + +(*** Applying ExtractCommonTermFun ***) + +(*this version ALWAYS includes a trailing one*) +fun long_mk_prod [] = one + | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts); + +(*Find first term that matches u*) +fun find_first_t past u [] = raise TERM("find_first_t", []) + | find_first_t past u (t::terms) = + if u aconv t then (rev past @ terms) + else find_first_t (t::past) u terms + handle TERM _ => find_first_t (t::past) u terms; + +(** Final simplification for the CancelFactor simprocs **) +val simplify_one = Arith_Data.simplify_meta_eq + [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}]; + +fun cancel_simplify_meta_eq ss cancel_th th = + simplify_one ss (([th, cancel_th]) MRS trans); + +structure CancelFactorCommon = + struct + val mk_sum = (fn T:typ => long_mk_prod) + val dest_sum = dest_prod + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val find_first = find_first_t [] + val trans_tac = K Arith_Data.trans_tac + val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} + fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) + val simplify_meta_eq = cancel_simplify_meta_eq + end; + +structure EqCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT + val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj})) +); + +structure LessCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT + val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj})) +); + +structure LeCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT + val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj})) +); + +structure DivideCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name Divides.div} + val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT + val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj})) +); + +structure DvdCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} + val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT + val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj})) +); + +val cancel_factor = + map Arith_Data.prep_simproc + [("nat_eq_cancel_factor", + ["(l::nat) * m = n", "(l::nat) = m * n"], + K EqCancelFactor.proc), + ("nat_less_cancel_factor", + ["(l::nat) * m < n", "(l::nat) < m * n"], + K LessCancelFactor.proc), + ("nat_le_cancel_factor", + ["(l::nat) * m <= n", "(l::nat) <= m * n"], + K LeCancelFactor.proc), + ("nat_divide_cancel_factor", + ["((l::nat) * m) div n", "(l::nat) div (m * n)"], + K DivideCancelFactor.proc), + ("nat_dvd_cancel_factor", + ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"], + K DvdCancelFactor.proc)]; + +end; + + +Addsimprocs Nat_Numeral_Simprocs.cancel_numerals; +Addsimprocs [Nat_Numeral_Simprocs.combine_numerals]; +Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors; +Addsimprocs Nat_Numeral_Simprocs.cancel_factor; + + +(*examples: +print_depth 22; +set timing; +set trace_simp; +fun test s = (Goal s; by (Simp_tac 1)); + +(*cancel_numerals*) +test "l +( 2) + (2) + 2 + (l + 2) + (oo + 2) = (uu::nat)"; +test "(2*length xs < 2*length xs + j)"; +test "(2*length xs < length xs * 2 + j)"; +test "2*u = (u::nat)"; +test "2*u = Suc (u)"; +test "(i + j + 12 + (k::nat)) - 15 = y"; +test "(i + j + 12 + (k::nat)) - 5 = y"; +test "Suc u - 2 = y"; +test "Suc (Suc (Suc u)) - 2 = y"; +test "(i + j + 2 + (k::nat)) - 1 = y"; +test "(i + j + 1 + (k::nat)) - 2 = y"; + +test "(2*x + (u*v) + y) - v*3*u = (w::nat)"; +test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)"; +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)"; +test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w"; +test "Suc ((u*v)*4) - v*3*u = w"; +test "Suc (Suc ((u*v)*3)) - v*3*u = w"; + +test "(i + j + 12 + (k::nat)) = u + 15 + y"; +test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz"; +test "(i + j + 12 + (k::nat)) = u + 5 + y"; +(*Suc*) +test "(i + j + 12 + k) = Suc (u + y)"; +test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)"; +test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"; +test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v"; +test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"; +test "2*y + 3*z + 2*u = Suc (u)"; +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)"; +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::nat)"; +test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)"; +test "(2*n*m) < (3*(m*n)) + (u::nat)"; + +test "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) <= Suc 0)"; + +test "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) <= length l1"; + +test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) <= length (compT P E A ST mxr e))"; + +test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un \ e) ST mxr c))))))) <= length (compT P E A ST mxr e))"; + + +(*negative numerals: FAIL*) +test "(i + j + -23 + (k::nat)) < u + 15 + y"; +test "(i + j + 3 + (k::nat)) < u + -15 + y"; +test "(i + j + -12 + (k::nat)) - 15 = y"; +test "(i + j + 12 + (k::nat)) - -15 = y"; +test "(i + j + -12 + (k::nat)) - -15 = y"; + +(*combine_numerals*) +test "k + 3*k = (u::nat)"; +test "Suc (i + 3) = u"; +test "Suc (i + j + 3 + k) = u"; +test "k + j + 3*k + j = (u::nat)"; +test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)"; +test "(2*n*m) + (3*(m*n)) = (u::nat)"; +(*negative numerals: FAIL*) +test "Suc (i + j + -3 + k) = u"; + +(*cancel_numeral_factors*) +test "9*x = 12 * (y::nat)"; +test "(9*x) div (12 * (y::nat)) = z"; +test "9*x < 12 * (y::nat)"; +test "9*x <= 12 * (y::nat)"; + +(*cancel_factor*) +test "x*k = k*(y::nat)"; +test "k = k*(y::nat)"; +test "a*(b*c) = (b::nat)"; +test "a*(b*c) = d*(b::nat)*(x*a)"; + +test "x*k < k*(y::nat)"; +test "k < k*(y::nat)"; +test "a*(b*c) < (b::nat)"; +test "a*(b*c) < d*(b::nat)*(x*a)"; + +test "x*k <= k*(y::nat)"; +test "k <= k*(y::nat)"; +test "a*(b*c) <= (b::nat)"; +test "a*(b*c) <= d*(b::nat)*(x*a)"; + +test "(x*k) div (k*(y::nat)) = (uu::nat)"; +test "(k) div (k*(y::nat)) = (uu::nat)"; +test "(a*(b*c)) div ((b::nat)) = (uu::nat)"; +test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)"; +*) diff -r fd7ec31f850c -r f591144b0f17 src/HOL/Tools/numeral_simprocs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/numeral_simprocs.ML Fri May 08 09:48:07 2009 +0200 @@ -0,0 +1,786 @@ +(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2000 University of Cambridge + +Simprocs for the integer numerals. +*) + +(*To quote from Provers/Arith/cancel_numeral_factor.ML: + +Cancels common coefficients in balanced expressions: + + u*#m ~~ u'*#m' == #n*u ~~ #n'*u' + +where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /) +and d = gcd(m,m') and n=m/d and n'=m'/d. +*) + +signature NUMERAL_SIMPROCS = +sig + val mk_sum: typ -> term list -> term + val dest_sum: term -> term list + + val assoc_fold_simproc: simproc + val combine_numerals: simproc + val cancel_numerals: simproc list + val cancel_factors: simproc list + val cancel_numeral_factors: simproc list + val field_combine_numerals: simproc + val field_cancel_numeral_factors: simproc list + val num_ss: simpset +end; + +structure Numeral_Simprocs : NUMERAL_SIMPROCS = +struct + +fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n; + +fun find_first_numeral past (t::terms) = + ((snd (HOLogic.dest_number t), rev past @ terms) + handle TERM _ => find_first_numeral (t::past) terms) + | find_first_numeral past [] = raise TERM("find_first_numeral", []); + +val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; + +fun mk_minus t = + let val T = Term.fastype_of t + in Const (@{const_name HOL.uminus}, T --> T) $ t end; + +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) +fun mk_sum T [] = mk_number T 0 + | mk_sum T [t,u] = mk_plus (t, u) + | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); + +(*this version ALWAYS includes a trailing zero*) +fun long_mk_sum T [] = mk_number T 0 + | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); + +val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT; + +(*decompose additions AND subtractions as a sum*) +fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) = + dest_summing (pos, t, dest_summing (pos, u, ts)) + | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) = + dest_summing (pos, t, dest_summing (not pos, u, ts)) + | dest_summing (pos, t, ts) = + if pos then t::ts else mk_minus t :: ts; + +fun dest_sum t = dest_summing (true, t, []); + +val mk_diff = HOLogic.mk_binop @{const_name HOL.minus}; +val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT; + +val mk_times = HOLogic.mk_binop @{const_name HOL.times}; + +fun one_of T = Const(@{const_name HOL.one},T); + +(* build product with trailing 1 rather than Numeral 1 in order to avoid the + unnecessary restriction to type class number_ring + which is not required for cancellation of common factors in divisions. +*) +fun mk_prod T = + let val one = one_of T + fun mk [] = one + | mk [t] = t + | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts) + in mk end; + +(*This version ALWAYS includes a trailing one*) +fun long_mk_prod T [] = one_of T + | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts); + +val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT; + +fun dest_prod t = + let val (t,u) = dest_times t + in dest_prod t @ dest_prod u end + handle TERM _ => [t]; + +(*DON'T do the obvious simplifications; that would create special cases*) +fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t); + +(*Express t as a product of (possibly) a numeral with other sorted terms*) +fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t + | dest_coeff sign t = + let val ts = sort TermOrd.term_ord (dest_prod t) + val (n, ts') = find_first_numeral [] ts + handle TERM _ => (1, ts) + in (sign*n, mk_prod (Term.fastype_of t) ts') end; + +(*Find first coefficient-term THAT MATCHES u*) +fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) + | find_first_coeff past u (t::terms) = + let val (n,u') = dest_coeff 1 t + in if u aconv u' then (n, rev past @ terms) + else find_first_coeff (t::past) u terms + end + handle TERM _ => find_first_coeff (t::past) u terms; + +(*Fractions as pairs of ints. Can't use Rat.rat because the representation + needs to preserve negative values in the denominator.*) +fun mk_frac (p, q) = if q = 0 then raise Div else (p, q); + +(*Don't reduce fractions; sums must be proved by rule add_frac_eq. + Fractions are reduced later by the cancel_numeral_factor simproc.*) +fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2); + +val mk_divide = HOLogic.mk_binop @{const_name HOL.divide}; + +(*Build term (p / q) * t*) +fun mk_fcoeff ((p, q), t) = + let val T = Term.fastype_of t + in mk_times (mk_divide (mk_number T p, mk_number T q), t) end; + +(*Express t as a product of a fraction with other sorted terms*) +fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t + | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) = + let val (p, t') = dest_coeff sign t + val (q, u') = dest_coeff 1 u + in (mk_frac (p, q), mk_divide (t', u')) end + | dest_fcoeff sign t = + let val (p, t') = dest_coeff sign t + val T = Term.fastype_of t + in (mk_frac (p, 1), mk_divide (t', one_of T)) end; + + +(** New term ordering so that AC-rewriting brings numerals to the front **) + +(*Order integers by absolute value and then by sign. The standard integer + ordering is not well-founded.*) +fun num_ord (i,j) = + (case int_ord (abs i, abs j) of + EQUAL => int_ord (Int.sign i, Int.sign j) + | ord => ord); + +(*This resembles TermOrd.term_ord, but it puts binary numerals before other + non-atomic terms.*) +local open Term +in +fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) = + (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord) + | numterm_ord + (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) = + num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w) + | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS + | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER + | numterm_ord (t, u) = + (case int_ord (size_of_term t, size_of_term u) of + EQUAL => + let val (f, ts) = strip_comb t and (g, us) = strip_comb u in + (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord) + end + | ord => ord) +and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) +end; + +fun numtermless tu = (numterm_ord tu = LESS); + +val num_ss = HOL_ss settermless numtermless; + +(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*) +val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym]; + +(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) +val add_0s = @{thms add_0s}; +val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1}; + +(*Simplify inverse Numeral1, a/Numeral1*) +val inverse_1s = [@{thm inverse_numeral_1}]; +val divide_1s = [@{thm divide_numeral_1}]; + +(*To perform binary arithmetic. The "left" rewriting handles patterns + created by the Numeral_Simprocs, such as 3 * (5 * x). *) +val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym, + @{thm add_number_of_left}, @{thm mult_number_of_left}] @ + @{thms arith_simps} @ @{thms rel_simps}; + +(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms + during re-arrangement*) +val non_add_simps = + subtract Thm.eq_thm [@{thm add_number_of_left}, @{thm number_of_add} RS sym] simps; + +(*To evaluate binary negations of coefficients*) +val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym] @ + @{thms minus_bin_simps} @ @{thms pred_bin_simps}; + +(*To let us treat subtraction as addition*) +val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}]; + +(*To let us treat division as multiplication*) +val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}]; + +(*push the unary minus down: - x * y = x * - y *) +val minus_mult_eq_1_to_2 = + [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> standard; + +(*to extract again any uncancelled minuses*) +val minus_from_mult_simps = + [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}]; + +(*combine unary minus with numeric literals, however nested within a product*) +val mult_minus_simps = + [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2]; + +val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ + diff_simps @ minus_simps @ @{thms add_ac} +val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps +val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} + +structure CancelNumeralsCommon = + struct + val mk_sum = mk_sum + val dest_sum = dest_sum + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val find_first_coeff = find_first_coeff [] + val trans_tac = K Arith_Data.trans_tac + + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) + + val numeral_simp_ss = HOL_ss addsimps add_0s @ simps + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) + val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s) + end; + + +structure EqCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" Term.dummyT + val bal_add1 = @{thm eq_add_iff1} RS trans + val bal_add2 = @{thm eq_add_iff2} RS trans +); + +structure LessCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT + val bal_add1 = @{thm less_add_iff1} RS trans + val bal_add2 = @{thm less_add_iff2} RS trans +); + +structure LeCancelNumerals = CancelNumeralsFun + (open CancelNumeralsCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT + val bal_add1 = @{thm le_add_iff1} RS trans + val bal_add2 = @{thm le_add_iff2} RS trans +); + +val cancel_numerals = + map Arith_Data.prep_simproc + [("inteq_cancel_numerals", + ["(l::'a::number_ring) + m = n", + "(l::'a::number_ring) = m + n", + "(l::'a::number_ring) - m = n", + "(l::'a::number_ring) = m - n", + "(l::'a::number_ring) * m = n", + "(l::'a::number_ring) = m * n"], + K EqCancelNumerals.proc), + ("intless_cancel_numerals", + ["(l::'a::{ordered_idom,number_ring}) + m < n", + "(l::'a::{ordered_idom,number_ring}) < m + n", + "(l::'a::{ordered_idom,number_ring}) - m < n", + "(l::'a::{ordered_idom,number_ring}) < m - n", + "(l::'a::{ordered_idom,number_ring}) * m < n", + "(l::'a::{ordered_idom,number_ring}) < m * n"], + K LessCancelNumerals.proc), + ("intle_cancel_numerals", + ["(l::'a::{ordered_idom,number_ring}) + m <= n", + "(l::'a::{ordered_idom,number_ring}) <= m + n", + "(l::'a::{ordered_idom,number_ring}) - m <= n", + "(l::'a::{ordered_idom,number_ring}) <= m - n", + "(l::'a::{ordered_idom,number_ring}) * m <= n", + "(l::'a::{ordered_idom,number_ring}) <= m * n"], + K LeCancelNumerals.proc)]; + +structure CombineNumeralsData = + struct + type coeff = int + val iszero = (fn x => x = 0) + val add = op + + val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) + val dest_sum = dest_sum + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val left_distrib = @{thm combine_common_factor} RS trans + val prove_conv = Arith_Data.prove_conv_nohyps + val trans_tac = K Arith_Data.trans_tac + + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) + + val numeral_simp_ss = HOL_ss addsimps add_0s @ simps + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) + val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s) + end; + +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); + +(*Version for fields, where coefficients can be fractions*) +structure FieldCombineNumeralsData = + struct + type coeff = int * int + val iszero = (fn (p, q) => p = 0) + val add = add_frac + val mk_sum = long_mk_sum + val dest_sum = dest_sum + val mk_coeff = mk_fcoeff + val dest_coeff = dest_fcoeff 1 + val left_distrib = @{thm combine_common_factor} RS trans + val prove_conv = Arith_Data.prove_conv_nohyps + val trans_tac = K Arith_Data.trans_tac + + val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1a)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) + + val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}] + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) + val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s) + end; + +structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData); + +val combine_numerals = + Arith_Data.prep_simproc + ("int_combine_numerals", + ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], + K CombineNumerals.proc); + +val field_combine_numerals = + Arith_Data.prep_simproc + ("field_combine_numerals", + ["(i::'a::{number_ring,field,division_by_zero}) + j", + "(i::'a::{number_ring,field,division_by_zero}) - j"], + K FieldCombineNumerals.proc); + +(** Constant folding for multiplication in semirings **) + +(*We do not need folding for addition: combine_numerals does the same thing*) + +structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = +struct + val assoc_ss = HOL_ss addsimps @{thms mult_ac} + val eq_reflection = eq_reflection + fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true + | is_numeral _ = false; +end; + +structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); + +val assoc_fold_simproc = + Arith_Data.prep_simproc + ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"], + K Semiring_Times_Assoc.proc); + +structure CancelNumeralFactorCommon = + struct + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val trans_tac = K Arith_Data.trans_tac + + val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s + val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps + val norm_ss3 = HOL_ss addsimps @{thms mult_ac} + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) + THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) + + val numeral_simp_ss = HOL_ss addsimps + [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}] @ simps + fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) + val simplify_meta_eq = Arith_Data.simplify_meta_eq + [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left}, + @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}]; + end + +(*Version for semiring_div*) +structure DivCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name Divides.div} + val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT + val cancel = @{thm div_mult_mult1} RS trans + val neg_exchanges = false +) + +(*Version for fields*) +structure DivideCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} + val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT + val cancel = @{thm mult_divide_mult_cancel_left} RS trans + val neg_exchanges = false +) + +structure EqCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" Term.dummyT + val cancel = @{thm mult_cancel_left} RS trans + val neg_exchanges = false +) + +structure LessCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT + val cancel = @{thm mult_less_cancel_left} RS trans + val neg_exchanges = true +) + +structure LeCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT + val cancel = @{thm mult_le_cancel_left} RS trans + val neg_exchanges = true +) + +val cancel_numeral_factors = + map Arith_Data.prep_simproc + [("ring_eq_cancel_numeral_factor", + ["(l::'a::{idom,number_ring}) * m = n", + "(l::'a::{idom,number_ring}) = m * n"], + K EqCancelNumeralFactor.proc), + ("ring_less_cancel_numeral_factor", + ["(l::'a::{ordered_idom,number_ring}) * m < n", + "(l::'a::{ordered_idom,number_ring}) < m * n"], + K LessCancelNumeralFactor.proc), + ("ring_le_cancel_numeral_factor", + ["(l::'a::{ordered_idom,number_ring}) * m <= n", + "(l::'a::{ordered_idom,number_ring}) <= m * n"], + K LeCancelNumeralFactor.proc), + ("int_div_cancel_numeral_factors", + ["((l::'a::{semiring_div,number_ring}) * m) div n", + "(l::'a::{semiring_div,number_ring}) div (m * n)"], + K DivCancelNumeralFactor.proc), + ("divide_cancel_numeral_factor", + ["((l::'a::{division_by_zero,field,number_ring}) * m) / n", + "(l::'a::{division_by_zero,field,number_ring}) / (m * n)", + "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"], + K DivideCancelNumeralFactor.proc)]; + +val field_cancel_numeral_factors = + map Arith_Data.prep_simproc + [("field_eq_cancel_numeral_factor", + ["(l::'a::{field,number_ring}) * m = n", + "(l::'a::{field,number_ring}) = m * n"], + K EqCancelNumeralFactor.proc), + ("field_cancel_numeral_factor", + ["((l::'a::{division_by_zero,field,number_ring}) * m) / n", + "(l::'a::{division_by_zero,field,number_ring}) / (m * n)", + "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"], + K DivideCancelNumeralFactor.proc)] + + +(** Declarations for ExtractCommonTerm **) + +(*Find first term that matches u*) +fun find_first_t past u [] = raise TERM ("find_first_t", []) + | find_first_t past u (t::terms) = + if u aconv t then (rev past @ terms) + else find_first_t (t::past) u terms + handle TERM _ => find_first_t (t::past) u terms; + +(** Final simplification for the CancelFactor simprocs **) +val simplify_one = Arith_Data.simplify_meta_eq + [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}]; + +fun cancel_simplify_meta_eq ss cancel_th th = + simplify_one ss (([th, cancel_th]) MRS trans); + +local + val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory HOL} HOLogic.Trueprop) + fun Eq_True_elim Eq = + Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI} +in +fun sign_conv pos_th neg_th ss t = + let val T = fastype_of t; + val zero = Const(@{const_name HOL.zero}, T); + val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT); + val pos = less $ zero $ t and neg = less $ t $ zero + fun prove p = + Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p) + handle THM _ => NONE + in case prove pos of + SOME th => SOME(th RS pos_th) + | NONE => (case prove neg of + SOME th => SOME(th RS neg_th) + | NONE => NONE) + end; +end + +structure CancelFactorCommon = + struct + val mk_sum = long_mk_prod + val dest_sum = dest_prod + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val find_first = find_first_t [] + val trans_tac = K Arith_Data.trans_tac + val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} + fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) + val simplify_meta_eq = cancel_simplify_meta_eq + end; + +(*mult_cancel_left requires a ring with no zero divisors.*) +structure EqCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" Term.dummyT + val simp_conv = K (K (SOME @{thm mult_cancel_left})) +); + +(*for ordered rings*) +structure LeCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT + val simp_conv = sign_conv + @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg} +); + +(*for ordered rings*) +structure LessCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT + val simp_conv = sign_conv + @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg} +); + +(*for semirings with division*) +structure DivCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name Divides.div} + val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT + val simp_conv = K (K (SOME @{thm div_mult_mult1_if})) +); + +structure ModCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name Divides.mod} + val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT + val simp_conv = K (K (SOME @{thm mod_mult_mult1})) +); + +(*for idoms*) +structure DvdCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} + val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT + val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left})) +); + +(*Version for all fields, including unordered ones (type complex).*) +structure DivideCancelFactor = ExtractCommonTermFun + (open CancelFactorCommon + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} + val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT + val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if})) +); + +val cancel_factors = + map Arith_Data.prep_simproc + [("ring_eq_cancel_factor", + ["(l::'a::idom) * m = n", + "(l::'a::idom) = m * n"], + K EqCancelFactor.proc), + ("ordered_ring_le_cancel_factor", + ["(l::'a::ordered_ring) * m <= n", + "(l::'a::ordered_ring) <= m * n"], + K LeCancelFactor.proc), + ("ordered_ring_less_cancel_factor", + ["(l::'a::ordered_ring) * m < n", + "(l::'a::ordered_ring) < m * n"], + K LessCancelFactor.proc), + ("int_div_cancel_factor", + ["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"], + K DivCancelFactor.proc), + ("int_mod_cancel_factor", + ["((l::'a::semiring_div) * m) mod n", "(l::'a::semiring_div) mod (m * n)"], + K ModCancelFactor.proc), + ("dvd_cancel_factor", + ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"], + K DvdCancelFactor.proc), + ("divide_cancel_factor", + ["((l::'a::{division_by_zero,field}) * m) / n", + "(l::'a::{division_by_zero,field}) / (m * n)"], + K DivideCancelFactor.proc)]; + +end; + +Addsimprocs Numeral_Simprocs.cancel_numerals; +Addsimprocs [Numeral_Simprocs.combine_numerals]; +Addsimprocs [Numeral_Simprocs.field_combine_numerals]; +Addsimprocs [Numeral_Simprocs.assoc_fold_simproc]; + +(*examples: +print_depth 22; +set timing; +set trace_simp; +fun test s = (Goal s, by (Simp_tac 1)); + +test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"; + +test "2*u = (u::int)"; +test "(i + j + 12 + (k::int)) - 15 = y"; +test "(i + j + 12 + (k::int)) - 5 = y"; + +test "y - b < (b::int)"; +test "y - (3*b + c) < (b::int) - 2*c"; + +test "(2*x - (u*v) + y) - v*3*u = (w::int)"; +test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"; +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"; +test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"; + +test "(i + j + 12 + (k::int)) = u + 15 + y"; +test "(i + j*2 + 12 + (k::int)) = j + 5 + y"; + +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"; + +test "a + -(b+c) + b = (d::int)"; +test "a + -(b+c) - b = (d::int)"; + +(*negative numerals*) +test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"; +test "(i + j + -3 + (k::int)) < u + 5 + y"; +test "(i + j + 3 + (k::int)) < u + -6 + y"; +test "(i + j + -12 + (k::int)) - 15 = y"; +test "(i + j + 12 + (k::int)) - -15 = y"; +test "(i + j + -12 + (k::int)) - -15 = y"; +*) + +Addsimprocs Numeral_Simprocs.cancel_numeral_factors; + +(*examples: +print_depth 22; +set timing; +set trace_simp; +fun test s = (Goal s; by (Simp_tac 1)); + +test "9*x = 12 * (y::int)"; +test "(9*x) div (12 * (y::int)) = z"; +test "9*x < 12 * (y::int)"; +test "9*x <= 12 * (y::int)"; + +test "-99*x = 132 * (y::int)"; +test "(-99*x) div (132 * (y::int)) = z"; +test "-99*x < 132 * (y::int)"; +test "-99*x <= 132 * (y::int)"; + +test "999*x = -396 * (y::int)"; +test "(999*x) div (-396 * (y::int)) = z"; +test "999*x < -396 * (y::int)"; +test "999*x <= -396 * (y::int)"; + +test "-99*x = -81 * (y::int)"; +test "(-99*x) div (-81 * (y::int)) = z"; +test "-99*x <= -81 * (y::int)"; +test "-99*x < -81 * (y::int)"; + +test "-2 * x = -1 * (y::int)"; +test "-2 * x = -(y::int)"; +test "(-2 * x) div (-1 * (y::int)) = z"; +test "-2 * x < -(y::int)"; +test "-2 * x <= -1 * (y::int)"; +test "-x < -23 * (y::int)"; +test "-x <= -23 * (y::int)"; +*) + +(*And the same examples for fields such as rat or real: +test "0 <= (y::rat) * -2"; +test "9*x = 12 * (y::rat)"; +test "(9*x) / (12 * (y::rat)) = z"; +test "9*x < 12 * (y::rat)"; +test "9*x <= 12 * (y::rat)"; + +test "-99*x = 132 * (y::rat)"; +test "(-99*x) / (132 * (y::rat)) = z"; +test "-99*x < 132 * (y::rat)"; +test "-99*x <= 132 * (y::rat)"; + +test "999*x = -396 * (y::rat)"; +test "(999*x) / (-396 * (y::rat)) = z"; +test "999*x < -396 * (y::rat)"; +test "999*x <= -396 * (y::rat)"; + +test "(- ((2::rat) * x) <= 2 * y)"; +test "-99*x = -81 * (y::rat)"; +test "(-99*x) / (-81 * (y::rat)) = z"; +test "-99*x <= -81 * (y::rat)"; +test "-99*x < -81 * (y::rat)"; + +test "-2 * x = -1 * (y::rat)"; +test "-2 * x = -(y::rat)"; +test "(-2 * x) / (-1 * (y::rat)) = z"; +test "-2 * x < -(y::rat)"; +test "-2 * x <= -1 * (y::rat)"; +test "-x < -23 * (y::rat)"; +test "-x <= -23 * (y::rat)"; +*) + +Addsimprocs Numeral_Simprocs.cancel_factors; + + +(*examples: +print_depth 22; +set timing; +set trace_simp; +fun test s = (Goal s; by (Asm_simp_tac 1)); + +test "x*k = k*(y::int)"; +test "k = k*(y::int)"; +test "a*(b*c) = (b::int)"; +test "a*(b*c) = d*(b::int)*(x*a)"; + +test "(x*k) div (k*(y::int)) = (uu::int)"; +test "(k) div (k*(y::int)) = (uu::int)"; +test "(a*(b*c)) div ((b::int)) = (uu::int)"; +test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"; +*) + +(*And the same examples for fields such as rat or real: +print_depth 22; +set timing; +set trace_simp; +fun test s = (Goal s; by (Asm_simp_tac 1)); + +test "x*k = k*(y::rat)"; +test "k = k*(y::rat)"; +test "a*(b*c) = (b::rat)"; +test "a*(b*c) = d*(b::rat)*(x*a)"; + + +test "(x*k) / (k*(y::rat)) = (uu::rat)"; +test "(k) / (k*(y::rat)) = (uu::rat)"; +test "(a*(b*c)) / ((b::rat)) = (uu::rat)"; +test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"; + +(*FIXME: what do we do about this?*) +test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"; +*) diff -r fd7ec31f850c -r f591144b0f17 src/HOL/Tools/rat_arith.ML --- a/src/HOL/Tools/rat_arith.ML Fri May 08 08:01:09 2009 +0200 +++ b/src/HOL/Tools/rat_arith.ML Fri May 08 09:48:07 2009 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Real/rat_arith.ML - ID: $Id$ Author: Lawrence C Paulson Copyright 2004 University of Cambridge @@ -10,8 +9,6 @@ local -val simprocs = field_cancel_numeral_factors - val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals}, read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib}, @@ -42,7 +39,7 @@ lessD = lessD, (*Can't change lessD: the rats are dense!*) neqE = neqE, simpset = simpset addsimps simps - addsimprocs simprocs}) #> + addsimprocs Numeral_Simprocs.field_cancel_numeral_factors}) #> arith_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #> arith_inj_const (@{const_name of_int}, @{typ "int => rat"})