(* Title: ZF/int_arith.ML
Author: Larry Paulson
Simprocs for linear arithmetic.
*)
signature INT_NUMERAL_SIMPROCS =
sig
val cancel_numerals: simproc list
val combine_numerals: simproc
val combine_numerals_prod: simproc
end
structure Int_Numeral_Simprocs: INT_NUMERAL_SIMPROCS =
struct
(* abstract syntax operations *)
fun mk_bit 0 = \<^term>\<open>0\<close>
| mk_bit 1 = \<^term>\<open>succ(0)\<close>
| mk_bit _ = raise TERM ("mk_bit", []);
fun dest_bit \<^term>\<open>0\<close> = 0
| dest_bit \<^term>\<open>succ(0)\<close> = 1
| dest_bit t = raise TERM ("dest_bit", [t]);
fun mk_bin i =
let
fun term_of [] = \<^term>\<open>Pls\<close>
| term_of [~1] = \<^term>\<open>Min\<close>
| term_of (b :: bs) = \<^term>\<open>Bit\<close> $ term_of bs $ mk_bit b;
in term_of (Numeral_Syntax.make_binary i) end;
fun dest_bin tm =
let
fun bin_of \<^term>\<open>Pls\<close> = []
| bin_of \<^term>\<open>Min\<close> = [~1]
| bin_of (\<^term>\<open>Bit\<close> $ bs $ b) = dest_bit b :: bin_of bs
| bin_of _ = raise TERM ("dest_bin", [tm]);
in Numeral_Syntax.dest_binary (bin_of tm) end;
(*Utilities*)
fun mk_numeral i = \<^const>\<open>integ_of\<close> $ mk_bin i;
fun dest_numeral (Const(\<^const_name>\<open>integ_of\<close>, _) $ w) = dest_bin w
| dest_numeral t = raise TERM ("dest_numeral", [t]);
fun find_first_numeral past (t::terms) =
((dest_numeral t, rev past @ terms)
handle TERM _ => find_first_numeral (t::past) terms)
| find_first_numeral past [] = raise TERM("find_first_numeral", []);
val zero = mk_numeral 0;
val mk_plus = FOLogic.mk_binop \<^const_name>\<open>zadd\<close>;
(*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 [] = zero
| long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
(*decompose additions AND subtractions as a sum*)
fun dest_summing (pos, Const (\<^const_name>\<open>zadd\<close>, _) $ t $ u, ts) =
dest_summing (pos, t, dest_summing (pos, u, ts))
| dest_summing (pos, Const (\<^const_name>\<open>zdiff\<close>, _) $ t $ u, ts) =
dest_summing (pos, t, dest_summing (not pos, u, ts))
| dest_summing (pos, t, ts) =
if pos then t::ts else \<^const>\<open>zminus\<close> $ t :: ts;
fun dest_sum t = dest_summing (true, t, []);
val one = mk_numeral 1;
val mk_times = FOLogic.mk_binop \<^const_name>\<open>zmult\<close>;
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 = FOLogic.dest_bin \<^const_name>\<open>zmult\<close> \<^typ>\<open>i\<close>;
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_numeral k, t);
(*Express t as a product of (possibly) a numeral with other sorted terms*)
fun dest_coeff sign (Const (\<^const_name>\<open>zminus\<close>, _) $ t) = dest_coeff (~sign) t
| dest_coeff sign t =
let val ts = sort Term_Ord.term_ord (dest_prod t)
val (n, ts') = find_first_numeral [] ts
handle TERM _ => (1, ts)
in (sign*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 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;
(*Simplify #1*n and n*#1 to n*)
val add_0s = [@{thm zadd_0_intify}, @{thm zadd_0_right_intify}];
val mult_1s = [@{thm zmult_1_intify}, @{thm zmult_1_right_intify},
@{thm zmult_minus1}, @{thm zmult_minus1_right}];
val tc_rules = [@{thm integ_of_type}, @{thm intify_in_int},
@{thm int_of_type}, @{thm zadd_type}, @{thm zdiff_type}, @{thm zmult_type}] @
@{thms bin.intros};
val intifys = [@{thm intify_ident}, @{thm zadd_intify1}, @{thm zadd_intify2},
@{thm zdiff_intify1}, @{thm zdiff_intify2}, @{thm zmult_intify1}, @{thm zmult_intify2},
@{thm zless_intify1}, @{thm zless_intify2}, @{thm zle_intify1}, @{thm zle_intify2}];
(*To perform binary arithmetic*)
val bin_simps = [@{thm add_integ_of_left}] @ @{thms bin_arith_simps} @ @{thms bin_rel_simps};
(*To evaluate binary negations of coefficients*)
val zminus_simps = @{thms NCons_simps} @
[@{thm integ_of_minus} RS @{thm sym},
@{thm bin_minus_1}, @{thm bin_minus_0}, @{thm bin_minus_Pls}, @{thm bin_minus_Min},
@{thm bin_pred_1}, @{thm bin_pred_0}, @{thm bin_pred_Pls}, @{thm bin_pred_Min}];
(*To let us treat subtraction as addition*)
val diff_simps = [@{thm zdiff_def}, @{thm zminus_zadd_distrib}, @{thm zminus_zminus}];
(*push the unary minus down*)
val int_minus_mult_eq_1_to_2 = @{lemma "$- w $* z = w $* $- z" by simp};
(*to extract again any uncancelled minuses*)
val int_minus_from_mult_simps =
[@{thm zminus_zminus}, @{thm zmult_zminus}, @{thm zmult_zminus_right}];
(*combine unary minus with numeric literals, however nested within a product*)
val int_mult_minus_simps =
[@{thm zmult_assoc}, @{thm zmult_zminus} RS @{thm sym}, int_minus_mult_eq_1_to_2];
structure CancelNumeralsCommon =
struct
val mk_sum = (fn _ : typ => 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 []
fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm iff_trans}
val norm_ss1 =
simpset_of (put_simpset ZF_ss \<^context>
addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac})
val norm_ss2 =
simpset_of (put_simpset ZF_ss \<^context>
addsimps bin_simps @ int_mult_minus_simps @ intifys)
val norm_ss3 =
simpset_of (put_simpset ZF_ss \<^context>
addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys)
fun norm_tac ctxt =
ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss3 ctxt))
val numeral_simp_ss =
simpset_of (put_simpset ZF_ss \<^context>
addsimps add_0s @ bin_simps @ tc_rules @ intifys)
fun numeral_simp_tac ctxt =
ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
THEN ALLGOALS (asm_simp_tac ctxt)
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s)
end;
structure EqCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
val mk_bal = FOLogic.mk_eq
val dest_bal = FOLogic.dest_eq
val bal_add1 = @{thm eq_add_iff1} RS @{thm iff_trans}
val bal_add2 = @{thm eq_add_iff2} RS @{thm iff_trans}
);
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
val mk_bal = FOLogic.mk_binrel \<^const_name>\<open>zless\<close>
val dest_bal = FOLogic.dest_bin \<^const_name>\<open>zless\<close> \<^typ>\<open>i\<close>
val bal_add1 = @{thm less_add_iff1} RS @{thm iff_trans}
val bal_add2 = @{thm less_add_iff2} RS @{thm iff_trans}
);
structure LeCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
val mk_bal = FOLogic.mk_binrel \<^const_name>\<open>zle\<close>
val dest_bal = FOLogic.dest_bin \<^const_name>\<open>zle\<close> \<^typ>\<open>i\<close>
val bal_add1 = @{thm le_add_iff1} RS @{thm iff_trans}
val bal_add2 = @{thm le_add_iff2} RS @{thm iff_trans}
);
val cancel_numerals =
[Simplifier.make_simproc \<^context> "inteq_cancel_numerals"
{lhss =
[\<^term>\<open>l $+ m = n\<close>, \<^term>\<open>l = m $+ n\<close>,
\<^term>\<open>l $- m = n\<close>, \<^term>\<open>l = m $- n\<close>,
\<^term>\<open>l $* m = n\<close>, \<^term>\<open>l = m $* n\<close>],
proc = K EqCancelNumerals.proc},
Simplifier.make_simproc \<^context> "intless_cancel_numerals"
{lhss =
[\<^term>\<open>l $+ m $< n\<close>, \<^term>\<open>l $< m $+ n\<close>,
\<^term>\<open>l $- m $< n\<close>, \<^term>\<open>l $< m $- n\<close>,
\<^term>\<open>l $* m $< n\<close>, \<^term>\<open>l $< m $* n\<close>],
proc = K LessCancelNumerals.proc},
Simplifier.make_simproc \<^context> "intle_cancel_numerals"
{lhss =
[\<^term>\<open>l $+ m $\<le> n\<close>, \<^term>\<open>l $\<le> m $+ n\<close>,
\<^term>\<open>l $- m $\<le> n\<close>, \<^term>\<open>l $\<le> m $- n\<close>,
\<^term>\<open>l $* m $\<le> n\<close>, \<^term>\<open>l $\<le> m $* n\<close>],
proc = K LeCancelNumerals.proc}];
(*version without the hyps argument*)
fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg [];
structure CombineNumeralsData =
struct
type coeff = int
val iszero = (fn x => x = 0)
val add = op +
val mk_sum = (fn _ : typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
val dest_sum = dest_sum
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val left_distrib = @{thm left_zadd_zmult_distrib} RS @{thm trans}
val prove_conv = prove_conv_nohyps "int_combine_numerals"
fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm trans}
val norm_ss1 =
simpset_of (put_simpset ZF_ss \<^context>
addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys)
val norm_ss2 =
simpset_of (put_simpset ZF_ss \<^context>
addsimps bin_simps @ int_mult_minus_simps @ intifys)
val norm_ss3 =
simpset_of (put_simpset ZF_ss \<^context>
addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys)
fun norm_tac ctxt =
ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss3 ctxt))
val numeral_simp_ss =
simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ bin_simps @ tc_rules @ intifys)
fun numeral_simp_tac ctxt =
ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s)
end;
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
val combine_numerals =
Simplifier.make_simproc \<^context> "int_combine_numerals"
{lhss = [\<^term>\<open>i $+ j\<close>, \<^term>\<open>i $- j\<close>],
proc = K CombineNumerals.proc};
(** Constant folding for integer multiplication **)
(*The trick is to regard products as sums, e.g. #3 $* x $* #4 as
the "sum" of #3, x, #4; the literals are then multiplied*)
structure CombineNumeralsProdData =
struct
type coeff = int
val iszero = (fn x => x = 0)
val add = op *
val mk_sum = (fn _ : typ => mk_prod)
val dest_sum = dest_prod
fun mk_coeff(k,t) =
if t = one then mk_numeral k
else raise TERM("mk_coeff", [])
fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*)
val left_distrib = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans}
val prove_conv = prove_conv_nohyps "int_combine_numerals_prod"
fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm trans}
val norm_ss1 =
simpset_of (put_simpset ZF_ss \<^context> addsimps mult_1s @ diff_simps @ zminus_simps)
val norm_ss2 =
simpset_of (put_simpset ZF_ss \<^context> addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @
bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys)
fun norm_tac ctxt =
ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
val numeral_simp_ss =
simpset_of (put_simpset ZF_ss \<^context> addsimps bin_simps @ tc_rules @ intifys)
fun numeral_simp_tac ctxt =
ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s);
end;
structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
val combine_numerals_prod =
Simplifier.make_simproc \<^context> "int_combine_numerals_prod"
{lhss = [\<^term>\<open>i $* j\<close>], proc = K CombineNumeralsProd.proc};
end;
val _ =
Theory.setup (Simplifier.map_theory_simpset (fn ctxt =>
ctxt addsimprocs
(Int_Numeral_Simprocs.cancel_numerals @
[Int_Numeral_Simprocs.combine_numerals,
Int_Numeral_Simprocs.combine_numerals_prod])));