haftmann@31068: (* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@23164: 
wenzelm@23164: Simprocs for nat numerals.
wenzelm@23164: *)
wenzelm@23164: 
haftmann@31068: signature NAT_NUMERAL_SIMPROCS =
haftmann@31068: sig
haftmann@31068:   val combine_numerals: simproc
haftmann@31068:   val cancel_numerals: simproc list
haftmann@31068:   val cancel_factors: simproc list
haftmann@31068:   val cancel_numeral_factors: simproc list
haftmann@31068: end;
haftmann@31068: 
wenzelm@23164: structure Nat_Numeral_Simprocs =
wenzelm@23164: struct
wenzelm@23164: 
wenzelm@23164: (*Maps n to #n for n = 0, 1, 2*)
haftmann@30496: 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];
wenzelm@23164: val numeral_sym_ss = HOL_ss addsimps numeral_syms;
wenzelm@23164: 
wenzelm@23164: fun rename_numerals th =
wenzelm@32010:     simplify numeral_sym_ss (Thm.transfer @{theory} th);
wenzelm@23164: 
wenzelm@23164: (*Utilities*)
wenzelm@23164: 
wenzelm@23164: fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n;
wenzelm@24630: fun dest_number t = Int.max (0, snd (HOLogic.dest_number t));
wenzelm@23164: 
wenzelm@23164: fun find_first_numeral past (t::terms) =
wenzelm@23164:         ((dest_number t, t, rev past @ terms)
wenzelm@23164:          handle TERM _ => find_first_numeral (t::past) terms)
wenzelm@23164:   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
wenzelm@23164: 
wenzelm@23164: val zero = mk_number 0;
haftmann@34974: val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
wenzelm@23164: 
wenzelm@23164: (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
wenzelm@23164: fun mk_sum []        = zero
wenzelm@23164:   | mk_sum [t,u]     = mk_plus (t, u)
wenzelm@23164:   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
wenzelm@23164: 
wenzelm@23164: (*this version ALWAYS includes a trailing zero*)
wenzelm@23164: fun long_mk_sum []        = HOLogic.zero
wenzelm@23164:   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
wenzelm@23164: 
haftmann@34974: val dest_plus = HOLogic.dest_bin @{const_name Algebras.plus} HOLogic.natT;
wenzelm@23164: 
wenzelm@23164: 
wenzelm@23164: (** Other simproc items **)
wenzelm@23164: 
wenzelm@23164: val bin_simps =
huffman@23471:      [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym,
huffman@23471:       @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 
huffman@23471:       @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less},
huffman@23471:       @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 
huffman@23471:       @{thm less_nat_number_of}, 
huffman@23471:       @{thm Let_number_of}, @{thm nat_number_of}] @
huffman@29039:      @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
wenzelm@23164: 
wenzelm@23164: 
wenzelm@23164: (*** CancelNumerals simprocs ***)
wenzelm@23164: 
wenzelm@23164: val one = mk_number 1;
haftmann@34974: val mk_times = HOLogic.mk_binop @{const_name Algebras.times};
wenzelm@23164: 
wenzelm@23164: fun mk_prod [] = one
wenzelm@23164:   | mk_prod [t] = t
wenzelm@23164:   | mk_prod (t :: ts) = if t = one then mk_prod ts
wenzelm@23164:                         else mk_times (t, mk_prod ts);
wenzelm@23164: 
haftmann@34974: val dest_times = HOLogic.dest_bin @{const_name Algebras.times} HOLogic.natT;
wenzelm@23164: 
wenzelm@23164: fun dest_prod t =
wenzelm@23164:       let val (t,u) = dest_times t
wenzelm@23164:       in  dest_prod t @ dest_prod u  end
wenzelm@23164:       handle TERM _ => [t];
wenzelm@23164: 
wenzelm@23164: (*DON'T do the obvious simplifications; that would create special cases*)
wenzelm@23164: fun mk_coeff (k,t) = mk_times (mk_number k, t);
wenzelm@23164: 
wenzelm@23164: (*Express t as a product of (possibly) a numeral with other factors, sorted*)
wenzelm@23164: fun dest_coeff t =
wenzelm@29269:     let val ts = sort TermOrd.term_ord (dest_prod t)
wenzelm@23164:         val (n, _, ts') = find_first_numeral [] ts
wenzelm@23164:                           handle TERM _ => (1, one, ts)
wenzelm@23164:     in (n, mk_prod ts') end;
wenzelm@23164: 
wenzelm@23164: (*Find first coefficient-term THAT MATCHES u*)
wenzelm@23164: fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
wenzelm@23164:   | find_first_coeff past u (t::terms) =
wenzelm@23164:         let val (n,u') = dest_coeff t
wenzelm@23164:         in  if u aconv u' then (n, rev past @ terms)
wenzelm@23164:                           else find_first_coeff (t::past) u terms
wenzelm@23164:         end
wenzelm@23164:         handle TERM _ => find_first_coeff (t::past) u terms;
wenzelm@23164: 
wenzelm@23164: 
wenzelm@23164: (*Split up a sum into the list of its constituent terms, on the way removing any
wenzelm@23164:   Sucs and counting them.*)
wenzelm@23164: fun dest_Suc_sum (Const ("Suc", _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
wenzelm@23164:   | dest_Suc_sum (t, (k,ts)) = 
wenzelm@23164:       let val (t1,t2) = dest_plus t
wenzelm@23164:       in  dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts)))  end
wenzelm@23164:       handle TERM _ => (k, t::ts);
wenzelm@23164: 
wenzelm@23164: (*Code for testing whether numerals are already used in the goal*)
haftmann@25919: fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
wenzelm@23164:   | is_numeral _ = false;
wenzelm@23164: 
wenzelm@23164: fun prod_has_numeral t = exists is_numeral (dest_prod t);
wenzelm@23164: 
wenzelm@23164: (*The Sucs found in the term are converted to a binary numeral. If relaxed is false,
wenzelm@23164:   an exception is raised unless the original expression contains at least one
wenzelm@23164:   numeral in a coefficient position.  This prevents nat_combine_numerals from 
wenzelm@23164:   introducing numerals to goals.*)
wenzelm@23164: fun dest_Sucs_sum relaxed t = 
wenzelm@23164:   let val (k,ts) = dest_Suc_sum (t,(0,[]))
wenzelm@23164:   in
wenzelm@23164:      if relaxed orelse exists prod_has_numeral ts then 
wenzelm@23164:        if k=0 then ts
wenzelm@24630:        else mk_number k :: ts
wenzelm@23164:      else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t])
wenzelm@23164:   end;
wenzelm@23164: 
wenzelm@23164: 
wenzelm@23164: (*Simplify 1*n and n*1 to n*)
haftmann@35050: val add_0s  = map rename_numerals [@{thm add_0}, @{thm Nat.add_0_right}];
wenzelm@23164: val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
wenzelm@23164: 
wenzelm@23164: (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
wenzelm@23164: 
wenzelm@23164: (*And these help the simproc return False when appropriate, which helps
wenzelm@23164:   the arith prover.*)
haftmann@23881: val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc},
haftmann@23881:   @{thm Suc_not_Zero}, @{thm le_0_eq}];
wenzelm@23164: 
wenzelm@23164: val simplify_meta_eq =
haftmann@30518:     Arith_Data.simplify_meta_eq
haftmann@35050:         ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm Nat.add_0_right},
huffman@23471:           @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
wenzelm@23164: 
wenzelm@23164: 
wenzelm@23164: (*** Applying CancelNumeralsFun ***)
wenzelm@23164: 
wenzelm@23164: structure CancelNumeralsCommon =
wenzelm@23164:   struct
wenzelm@23164:   val mk_sum            = (fn T:typ => mk_sum)
wenzelm@23164:   val dest_sum          = dest_Sucs_sum true
wenzelm@23164:   val mk_coeff          = mk_coeff
wenzelm@23164:   val dest_coeff        = dest_coeff
wenzelm@23164:   val find_first_coeff  = find_first_coeff []
wenzelm@31368:   fun trans_tac _       = Arith_Data.trans_tac
wenzelm@23164: 
haftmann@31068:   val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
nipkow@31790:     [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
haftmann@31068:   val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
wenzelm@23164:   fun norm_tac ss = 
wenzelm@23164:     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
wenzelm@23164:     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
wenzelm@23164: 
wenzelm@23164:   val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
wenzelm@23164:   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss));
wenzelm@23164:   val simplify_meta_eq  = simplify_meta_eq
wenzelm@23164:   end;
wenzelm@23164: 
wenzelm@23164: 
wenzelm@23164: structure EqCancelNumerals = CancelNumeralsFun
wenzelm@23164:  (open CancelNumeralsCommon
haftmann@30496:   val prove_conv = Arith_Data.prove_conv
wenzelm@23164:   val mk_bal   = HOLogic.mk_eq
wenzelm@23164:   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
huffman@23471:   val bal_add1 = @{thm nat_eq_add_iff1} RS trans
huffman@23471:   val bal_add2 = @{thm nat_eq_add_iff2} RS trans
wenzelm@23164: );
wenzelm@23164: 
wenzelm@23164: structure LessCancelNumerals = CancelNumeralsFun
wenzelm@23164:  (open CancelNumeralsCommon
haftmann@30496:   val prove_conv = Arith_Data.prove_conv
haftmann@34974:   val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
haftmann@34974:   val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
huffman@23471:   val bal_add1 = @{thm nat_less_add_iff1} RS trans
huffman@23471:   val bal_add2 = @{thm nat_less_add_iff2} RS trans
wenzelm@23164: );
wenzelm@23164: 
wenzelm@23164: structure LeCancelNumerals = CancelNumeralsFun
wenzelm@23164:  (open CancelNumeralsCommon
haftmann@30496:   val prove_conv = Arith_Data.prove_conv
haftmann@34974:   val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
haftmann@34974:   val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
huffman@23471:   val bal_add1 = @{thm nat_le_add_iff1} RS trans
huffman@23471:   val bal_add2 = @{thm nat_le_add_iff2} RS trans
wenzelm@23164: );
wenzelm@23164: 
wenzelm@23164: structure DiffCancelNumerals = CancelNumeralsFun
wenzelm@23164:  (open CancelNumeralsCommon
haftmann@30496:   val prove_conv = Arith_Data.prove_conv
haftmann@34974:   val mk_bal   = HOLogic.mk_binop @{const_name Algebras.minus}
haftmann@34974:   val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT
huffman@23471:   val bal_add1 = @{thm nat_diff_add_eq1} RS trans
huffman@23471:   val bal_add2 = @{thm nat_diff_add_eq2} RS trans
wenzelm@23164: );
wenzelm@23164: 
wenzelm@23164: 
wenzelm@23164: val cancel_numerals =
wenzelm@32155:   map (Arith_Data.prep_simproc @{theory})
wenzelm@23164:    [("nateq_cancel_numerals",
wenzelm@23164:      ["(l::nat) + m = n", "(l::nat) = m + n",
wenzelm@23164:       "(l::nat) * m = n", "(l::nat) = m * n",
wenzelm@23164:       "Suc m = n", "m = Suc n"],
wenzelm@23164:      K EqCancelNumerals.proc),
wenzelm@23164:     ("natless_cancel_numerals",
wenzelm@23164:      ["(l::nat) + m < n", "(l::nat) < m + n",
wenzelm@23164:       "(l::nat) * m < n", "(l::nat) < m * n",
wenzelm@23164:       "Suc m < n", "m < Suc n"],
wenzelm@23164:      K LessCancelNumerals.proc),
wenzelm@23164:     ("natle_cancel_numerals",
wenzelm@23164:      ["(l::nat) + m <= n", "(l::nat) <= m + n",
wenzelm@23164:       "(l::nat) * m <= n", "(l::nat) <= m * n",
wenzelm@23164:       "Suc m <= n", "m <= Suc n"],
wenzelm@23164:      K LeCancelNumerals.proc),
wenzelm@23164:     ("natdiff_cancel_numerals",
wenzelm@23164:      ["((l::nat) + m) - n", "(l::nat) - (m + n)",
wenzelm@23164:       "(l::nat) * m - n", "(l::nat) - m * n",
wenzelm@23164:       "Suc m - n", "m - Suc n"],
wenzelm@23164:      K DiffCancelNumerals.proc)];
wenzelm@23164: 
wenzelm@23164: 
wenzelm@23164: (*** Applying CombineNumeralsFun ***)
wenzelm@23164: 
wenzelm@23164: structure CombineNumeralsData =
wenzelm@23164:   struct
wenzelm@24630:   type coeff            = int
wenzelm@24630:   val iszero            = (fn x => x = 0)
wenzelm@24630:   val add               = op +
wenzelm@23164:   val mk_sum            = (fn T:typ => long_mk_sum)  (*to work for 2*x + 3*x *)
wenzelm@23164:   val dest_sum          = dest_Sucs_sum false
wenzelm@23164:   val mk_coeff          = mk_coeff
wenzelm@23164:   val dest_coeff        = dest_coeff
huffman@23471:   val left_distrib      = @{thm left_add_mult_distrib} RS trans
haftmann@30496:   val prove_conv        = Arith_Data.prove_conv_nohyps
wenzelm@31368:   fun trans_tac _       = Arith_Data.trans_tac
wenzelm@23164: 
nipkow@31790:   val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms add_ac}
haftmann@31068:   val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
wenzelm@23164:   fun norm_tac ss =
wenzelm@23164:     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
wenzelm@23164:     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
wenzelm@23164: 
wenzelm@23164:   val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
wenzelm@23164:   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
wenzelm@23164:   val simplify_meta_eq  = simplify_meta_eq
wenzelm@23164:   end;
wenzelm@23164: 
wenzelm@23164: structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
wenzelm@23164: 
wenzelm@23164: val combine_numerals =
wenzelm@32155:   Arith_Data.prep_simproc @{theory}
wenzelm@32155:     ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
wenzelm@23164: 
wenzelm@23164: 
wenzelm@23164: (*** Applying CancelNumeralFactorFun ***)
wenzelm@23164: 
wenzelm@23164: structure CancelNumeralFactorCommon =
wenzelm@23164:   struct
wenzelm@23164:   val mk_coeff          = mk_coeff
wenzelm@23164:   val dest_coeff        = dest_coeff
wenzelm@31368:   fun trans_tac _       = Arith_Data.trans_tac
wenzelm@23164: 
haftmann@31068:   val norm_ss1 = Numeral_Simprocs.num_ss addsimps
nipkow@31790:     numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
haftmann@31068:   val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
wenzelm@23164:   fun norm_tac ss =
wenzelm@23164:     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
wenzelm@23164:     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
wenzelm@23164: 
wenzelm@23164:   val numeral_simp_ss = HOL_ss addsimps bin_simps
wenzelm@23164:   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
wenzelm@23164:   val simplify_meta_eq  = simplify_meta_eq
wenzelm@23164:   end
wenzelm@23164: 
wenzelm@23164: structure DivCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164:  (open CancelNumeralFactorCommon
haftmann@30496:   val prove_conv = Arith_Data.prove_conv
wenzelm@23164:   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
wenzelm@23164:   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
huffman@23471:   val cancel = @{thm nat_mult_div_cancel1} RS trans
wenzelm@23164:   val neg_exchanges = false
wenzelm@23164: )
wenzelm@23164: 
nipkow@23969: structure DvdCancelNumeralFactor = CancelNumeralFactorFun
nipkow@23969:  (open CancelNumeralFactorCommon
haftmann@30496:   val prove_conv = Arith_Data.prove_conv
haftmann@35050:   val mk_bal   = HOLogic.mk_binrel @{const_name Rings.dvd}
haftmann@35050:   val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT
nipkow@23969:   val cancel = @{thm nat_mult_dvd_cancel1} RS trans
nipkow@23969:   val neg_exchanges = false
nipkow@23969: )
nipkow@23969: 
wenzelm@23164: structure EqCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164:  (open CancelNumeralFactorCommon
haftmann@30496:   val prove_conv = Arith_Data.prove_conv
wenzelm@23164:   val mk_bal   = HOLogic.mk_eq
wenzelm@23164:   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
huffman@23471:   val cancel = @{thm nat_mult_eq_cancel1} RS trans
wenzelm@23164:   val neg_exchanges = false
wenzelm@23164: )
wenzelm@23164: 
wenzelm@23164: structure LessCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164:  (open CancelNumeralFactorCommon
haftmann@30496:   val prove_conv = Arith_Data.prove_conv
haftmann@34974:   val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
haftmann@34974:   val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
huffman@23471:   val cancel = @{thm nat_mult_less_cancel1} RS trans
wenzelm@23164:   val neg_exchanges = true
wenzelm@23164: )
wenzelm@23164: 
wenzelm@23164: structure LeCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164:  (open CancelNumeralFactorCommon
haftmann@30496:   val prove_conv = Arith_Data.prove_conv
haftmann@34974:   val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
haftmann@34974:   val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
huffman@23471:   val cancel = @{thm nat_mult_le_cancel1} RS trans
wenzelm@23164:   val neg_exchanges = true
wenzelm@23164: )
wenzelm@23164: 
wenzelm@23164: val cancel_numeral_factors =
wenzelm@32155:   map (Arith_Data.prep_simproc @{theory})
wenzelm@23164:    [("nateq_cancel_numeral_factors",
wenzelm@23164:      ["(l::nat) * m = n", "(l::nat) = m * n"],
wenzelm@23164:      K EqCancelNumeralFactor.proc),
wenzelm@23164:     ("natless_cancel_numeral_factors",
wenzelm@23164:      ["(l::nat) * m < n", "(l::nat) < m * n"],
wenzelm@23164:      K LessCancelNumeralFactor.proc),
wenzelm@23164:     ("natle_cancel_numeral_factors",
wenzelm@23164:      ["(l::nat) * m <= n", "(l::nat) <= m * n"],
wenzelm@23164:      K LeCancelNumeralFactor.proc),
wenzelm@23164:     ("natdiv_cancel_numeral_factors",
wenzelm@23164:      ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
nipkow@23969:      K DivCancelNumeralFactor.proc),
nipkow@23969:     ("natdvd_cancel_numeral_factors",
nipkow@23969:      ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
nipkow@23969:      K DvdCancelNumeralFactor.proc)];
wenzelm@23164: 
wenzelm@23164: 
wenzelm@23164: 
wenzelm@23164: (*** Applying ExtractCommonTermFun ***)
wenzelm@23164: 
wenzelm@23164: (*this version ALWAYS includes a trailing one*)
wenzelm@23164: fun long_mk_prod []        = one
wenzelm@23164:   | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
wenzelm@23164: 
wenzelm@23164: (*Find first term that matches u*)
wenzelm@23164: fun find_first_t past u []         = raise TERM("find_first_t", [])
wenzelm@23164:   | find_first_t past u (t::terms) =
wenzelm@23164:         if u aconv t then (rev past @ terms)
wenzelm@23164:         else find_first_t (t::past) u terms
wenzelm@23164:         handle TERM _ => find_first_t (t::past) u terms;
wenzelm@23164: 
wenzelm@23164: (** Final simplification for the CancelFactor simprocs **)
haftmann@30518: val simplify_one = Arith_Data.simplify_meta_eq  
wenzelm@23164:   [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
wenzelm@23164: 
nipkow@30649: fun cancel_simplify_meta_eq ss cancel_th th =
wenzelm@23164:     simplify_one ss (([th, cancel_th]) MRS trans);
wenzelm@23164: 
wenzelm@23164: structure CancelFactorCommon =
wenzelm@23164:   struct
wenzelm@23164:   val mk_sum            = (fn T:typ => long_mk_prod)
wenzelm@23164:   val dest_sum          = dest_prod
wenzelm@23164:   val mk_coeff          = mk_coeff
wenzelm@23164:   val dest_coeff        = dest_coeff
wenzelm@23164:   val find_first        = find_first_t []
wenzelm@31368:   fun trans_tac _       = Arith_Data.trans_tac
haftmann@23881:   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
wenzelm@23164:   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
nipkow@30649:   val simplify_meta_eq  = cancel_simplify_meta_eq
wenzelm@23164:   end;
wenzelm@23164: 
wenzelm@23164: structure EqCancelFactor = ExtractCommonTermFun
wenzelm@23164:  (open CancelFactorCommon
haftmann@30496:   val prove_conv = Arith_Data.prove_conv
wenzelm@23164:   val mk_bal   = HOLogic.mk_eq
wenzelm@23164:   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
wenzelm@31368:   fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj}
wenzelm@23164: );
wenzelm@23164: 
wenzelm@23164: structure LessCancelFactor = ExtractCommonTermFun
wenzelm@23164:  (open CancelFactorCommon
haftmann@30496:   val prove_conv = Arith_Data.prove_conv
haftmann@34974:   val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
haftmann@34974:   val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
wenzelm@31368:   fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
wenzelm@23164: );
wenzelm@23164: 
wenzelm@23164: structure LeCancelFactor = ExtractCommonTermFun
wenzelm@23164:  (open CancelFactorCommon
haftmann@30496:   val prove_conv = Arith_Data.prove_conv
haftmann@34974:   val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
haftmann@34974:   val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
wenzelm@31368:   fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
wenzelm@23164: );
wenzelm@23164: 
wenzelm@23164: structure DivideCancelFactor = ExtractCommonTermFun
wenzelm@23164:  (open CancelFactorCommon
haftmann@30496:   val prove_conv = Arith_Data.prove_conv
wenzelm@23164:   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
wenzelm@23164:   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
wenzelm@31368:   fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj}
wenzelm@23164: );
wenzelm@23164: 
nipkow@23969: structure DvdCancelFactor = ExtractCommonTermFun
nipkow@23969:  (open CancelFactorCommon
haftmann@30496:   val prove_conv = Arith_Data.prove_conv
haftmann@35050:   val mk_bal   = HOLogic.mk_binrel @{const_name Rings.dvd}
haftmann@35050:   val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT
wenzelm@31368:   fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj}
nipkow@23969: );
nipkow@23969: 
wenzelm@23164: val cancel_factor =
wenzelm@32155:   map (Arith_Data.prep_simproc @{theory})
wenzelm@23164:    [("nat_eq_cancel_factor",
wenzelm@23164:      ["(l::nat) * m = n", "(l::nat) = m * n"],
wenzelm@23164:      K EqCancelFactor.proc),
wenzelm@23164:     ("nat_less_cancel_factor",
wenzelm@23164:      ["(l::nat) * m < n", "(l::nat) < m * n"],
wenzelm@23164:      K LessCancelFactor.proc),
wenzelm@23164:     ("nat_le_cancel_factor",
wenzelm@23164:      ["(l::nat) * m <= n", "(l::nat) <= m * n"],
wenzelm@23164:      K LeCancelFactor.proc),
wenzelm@23164:     ("nat_divide_cancel_factor",
wenzelm@23164:      ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
nipkow@23969:      K DivideCancelFactor.proc),
nipkow@23969:     ("nat_dvd_cancel_factor",
nipkow@23969:      ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
nipkow@23969:      K DvdCancelFactor.proc)];
wenzelm@23164: 
wenzelm@23164: end;
wenzelm@23164: 
wenzelm@23164: 
wenzelm@23164: Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
wenzelm@23164: Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
wenzelm@23164: Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
wenzelm@23164: Addsimprocs Nat_Numeral_Simprocs.cancel_factor;
wenzelm@23164: 
wenzelm@23164: 
wenzelm@23164: (*examples:
wenzelm@23164: print_depth 22;
wenzelm@23164: set timing;
wenzelm@23164: set trace_simp;
wenzelm@23164: fun test s = (Goal s; by (Simp_tac 1));
wenzelm@23164: 
wenzelm@23164: (*cancel_numerals*)
wenzelm@23164: test "l +( 2) + (2) + 2 + (l + 2) + (oo  + 2) = (uu::nat)";
wenzelm@23164: test "(2*length xs < 2*length xs + j)";
wenzelm@23164: test "(2*length xs < length xs * 2 + j)";
wenzelm@23164: test "2*u = (u::nat)";
wenzelm@23164: test "2*u = Suc (u)";
wenzelm@23164: test "(i + j + 12 + (k::nat)) - 15 = y";
wenzelm@23164: test "(i + j + 12 + (k::nat)) - 5 = y";
wenzelm@23164: test "Suc u - 2 = y";
wenzelm@23164: test "Suc (Suc (Suc u)) - 2 = y";
wenzelm@23164: test "(i + j + 2 + (k::nat)) - 1 = y";
wenzelm@23164: test "(i + j + 1 + (k::nat)) - 2 = y";
wenzelm@23164: 
wenzelm@23164: test "(2*x + (u*v) + y) - v*3*u = (w::nat)";
wenzelm@23164: test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)";
wenzelm@23164: test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)";
wenzelm@23164: test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w";
wenzelm@23164: test "Suc ((u*v)*4) - v*3*u = w";
wenzelm@23164: test "Suc (Suc ((u*v)*3)) - v*3*u = w";
wenzelm@23164: 
wenzelm@23164: test "(i + j + 12 + (k::nat)) = u + 15 + y";
wenzelm@23164: test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz";
wenzelm@23164: test "(i + j + 12 + (k::nat)) = u + 5 + y";
wenzelm@23164: (*Suc*)
wenzelm@23164: test "(i + j + 12 + k) = Suc (u + y)";
wenzelm@23164: test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)";
wenzelm@23164: test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
wenzelm@23164: test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v";
wenzelm@23164: test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
wenzelm@23164: test "2*y + 3*z + 2*u = Suc (u)";
wenzelm@23164: test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)";
wenzelm@23164: 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)";
wenzelm@23164: test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)";
wenzelm@23164: test "(2*n*m) < (3*(m*n)) + (u::nat)";
wenzelm@23164: 
wenzelm@23164: test "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) <= Suc 0)";
wenzelm@23164:  
wenzelm@23164: test "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) <= length l1";
wenzelm@23164: 
wenzelm@23164: test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) <= length (compT P E A ST mxr e))";
wenzelm@23164: 
wenzelm@23164: test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un \<A> e) ST mxr c))))))) <= length (compT P E A ST mxr e))";
wenzelm@23164: 
wenzelm@23164: 
wenzelm@23164: (*negative numerals: FAIL*)
wenzelm@23164: test "(i + j + -23 + (k::nat)) < u + 15 + y";
wenzelm@23164: test "(i + j + 3 + (k::nat)) < u + -15 + y";
wenzelm@23164: test "(i + j + -12 + (k::nat)) - 15 = y";
wenzelm@23164: test "(i + j + 12 + (k::nat)) - -15 = y";
wenzelm@23164: test "(i + j + -12 + (k::nat)) - -15 = y";
wenzelm@23164: 
wenzelm@23164: (*combine_numerals*)
wenzelm@23164: test "k + 3*k = (u::nat)";
wenzelm@23164: test "Suc (i + 3) = u";
wenzelm@23164: test "Suc (i + j + 3 + k) = u";
wenzelm@23164: test "k + j + 3*k + j = (u::nat)";
wenzelm@23164: test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
wenzelm@23164: test "(2*n*m) + (3*(m*n)) = (u::nat)";
wenzelm@23164: (*negative numerals: FAIL*)
wenzelm@23164: test "Suc (i + j + -3 + k) = u";
wenzelm@23164: 
wenzelm@23164: (*cancel_numeral_factors*)
wenzelm@23164: test "9*x = 12 * (y::nat)";
wenzelm@23164: test "(9*x) div (12 * (y::nat)) = z";
wenzelm@23164: test "9*x < 12 * (y::nat)";
wenzelm@23164: test "9*x <= 12 * (y::nat)";
wenzelm@23164: 
wenzelm@23164: (*cancel_factor*)
wenzelm@23164: test "x*k = k*(y::nat)";
wenzelm@23164: test "k = k*(y::nat)";
wenzelm@23164: test "a*(b*c) = (b::nat)";
wenzelm@23164: test "a*(b*c) = d*(b::nat)*(x*a)";
wenzelm@23164: 
wenzelm@23164: test "x*k < k*(y::nat)";
wenzelm@23164: test "k < k*(y::nat)";
wenzelm@23164: test "a*(b*c) < (b::nat)";
wenzelm@23164: test "a*(b*c) < d*(b::nat)*(x*a)";
wenzelm@23164: 
wenzelm@23164: test "x*k <= k*(y::nat)";
wenzelm@23164: test "k <= k*(y::nat)";
wenzelm@23164: test "a*(b*c) <= (b::nat)";
wenzelm@23164: test "a*(b*c) <= d*(b::nat)*(x*a)";
wenzelm@23164: 
wenzelm@23164: test "(x*k) div (k*(y::nat)) = (uu::nat)";
wenzelm@23164: test "(k) div (k*(y::nat)) = (uu::nat)";
wenzelm@23164: test "(a*(b*c)) div ((b::nat)) = (uu::nat)";
wenzelm@23164: test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)";
wenzelm@23164: *)