src/HOL/Tools/nat_numeral_simprocs.ML
changeset 45462 aba629d6cee5
parent 45436 62bc9474d04b
child 45463 9a588a835c1e
equal deleted inserted replaced
45451:74515e8e6046 45462:aba629d6cee5
     3 Simprocs for nat numerals.
     3 Simprocs for nat numerals.
     4 *)
     4 *)
     5 
     5 
     6 signature NAT_NUMERAL_SIMPROCS =
     6 signature NAT_NUMERAL_SIMPROCS =
     7 sig
     7 sig
     8   val combine_numerals: simproc
     8   val combine_numerals: simpset -> cterm -> thm option
     9   val eq_cancel_numerals: simpset -> cterm -> thm option
     9   val eq_cancel_numerals: simpset -> cterm -> thm option
    10   val less_cancel_numerals: simpset -> cterm -> thm option
    10   val less_cancel_numerals: simpset -> cterm -> thm option
    11   val le_cancel_numerals: simpset -> cterm -> thm option
    11   val le_cancel_numerals: simpset -> cterm -> thm option
    12   val diff_cancel_numerals: simpset -> cterm -> thm option
    12   val diff_cancel_numerals: simpset -> cterm -> thm option
    13   val cancel_factors: simproc list
    13   val eq_cancel_factor: simpset -> cterm -> thm option
       
    14   val less_cancel_factor: simpset -> cterm -> thm option
       
    15   val le_cancel_factor: simpset -> cterm -> thm option
       
    16   val divide_cancel_factor: simpset -> cterm -> thm option
       
    17   val dvd_cancel_factor: simpset -> cterm -> thm option
    14   val cancel_numeral_factors: simproc list
    18   val cancel_numeral_factors: simproc list
    15 end;
    19 end;
    16 
    20 
    17 structure Nat_Numeral_Simprocs =
    21 structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS =
    18 struct
    22 struct
    19 
    23 
    20 (*Maps n to #n for n = 0, 1, 2*)
    24 (*Maps n to #n for n = 0, 1, 2*)
    21 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];
    25 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];
    22 val numeral_sym_ss = HOL_ss addsimps numeral_syms;
    26 val numeral_sym_ss = HOL_ss addsimps numeral_syms;
   230   val simplify_meta_eq = simplify_meta_eq
   234   val simplify_meta_eq = simplify_meta_eq
   231 end;
   235 end;
   232 
   236 
   233 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   237 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   234 
   238 
   235 val combine_numerals =
   239 fun combine_numerals ss ct = CombineNumerals.proc ss (term_of ct)
   236   Numeral_Simprocs.prep_simproc @{theory}
       
   237     ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
       
   238 
   240 
   239 
   241 
   240 (*** Applying CancelNumeralFactorFun ***)
   242 (*** Applying CancelNumeralFactorFun ***)
   241 
   243 
   242 structure CancelNumeralFactorCommon =
   244 structure CancelNumeralFactorCommon =
   385   val mk_bal   = HOLogic.mk_binrel @{const_name Rings.dvd}
   387   val mk_bal   = HOLogic.mk_binrel @{const_name Rings.dvd}
   386   val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT
   388   val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT
   387   fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj}
   389   fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj}
   388 );
   390 );
   389 
   391 
   390 val cancel_factor =
   392 fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct)
   391   map (Numeral_Simprocs.prep_simproc @{theory})
   393 fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct)
   392    [("nat_eq_cancel_factor",
   394 fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct)
   393      ["(l::nat) * m = n", "(l::nat) = m * n"],
   395 fun divide_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct)
   394      K EqCancelFactor.proc),
   396 fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct)
   395     ("nat_less_cancel_factor",
   397 
   396      ["(l::nat) * m < n", "(l::nat) < m * n"],
   398 end;
   397      K LessCancelFactor.proc),
   399 
   398     ("nat_le_cancel_factor",
   400 
   399      ["(l::nat) * m <= n", "(l::nat) <= m * n"],
       
   400      K LeCancelFactor.proc),
       
   401     ("nat_divide_cancel_factor",
       
   402      ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
       
   403      K DivideCancelFactor.proc),
       
   404     ("nat_dvd_cancel_factor",
       
   405      ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
       
   406      K DvdCancelFactor.proc)];
       
   407 
       
   408 end;
       
   409 
       
   410 
       
   411 Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
       
   412 Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
   401 Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
   413 Addsimprocs Nat_Numeral_Simprocs.cancel_factor;
       
   414 
   402 
   415 
   403 
   416 (*examples:
   404 (*examples:
   417 print_depth 22;
   405 print_depth 22;
   418 set timing;
   406 set timing;
   419 set simp_trace;
   407 set simp_trace;
   420 fun test s = (Goal s; by (Simp_tac 1));
   408 fun test s = (Goal s; by (Simp_tac 1));
   421 
   409 
   422 (*combine_numerals*)
       
   423 test "k + 3*k = (u::nat)";
       
   424 test "Suc (i + 3) = u";
       
   425 test "Suc (i + j + 3 + k) = u";
       
   426 test "k + j + 3*k + j = (u::nat)";
       
   427 test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
       
   428 test "(2*n*m) + (3*(m*n)) = (u::nat)";
       
   429 (*negative numerals: FAIL*)
       
   430 test "Suc (i + j + -3 + k) = u";
       
   431 
       
   432 (*cancel_numeral_factors*)
   410 (*cancel_numeral_factors*)
   433 test "9*x = 12 * (y::nat)";
   411 test "9*x = 12 * (y::nat)";
   434 test "(9*x) div (12 * (y::nat)) = z";
   412 test "(9*x) div (12 * (y::nat)) = z";
   435 test "9*x < 12 * (y::nat)";
   413 test "9*x < 12 * (y::nat)";
   436 test "9*x <= 12 * (y::nat)";
   414 test "9*x <= 12 * (y::nat)";
   437 
   415 
   438 (*cancel_factor*)
       
   439 test "x*k = k*(y::nat)";
       
   440 test "k = k*(y::nat)";
       
   441 test "a*(b*c) = (b::nat)";
       
   442 test "a*(b*c) = d*(b::nat)*(x*a)";
       
   443 
       
   444 test "x*k < k*(y::nat)";
       
   445 test "k < k*(y::nat)";
       
   446 test "a*(b*c) < (b::nat)";
       
   447 test "a*(b*c) < d*(b::nat)*(x*a)";
       
   448 
       
   449 test "x*k <= k*(y::nat)";
       
   450 test "k <= k*(y::nat)";
       
   451 test "a*(b*c) <= (b::nat)";
       
   452 test "a*(b*c) <= d*(b::nat)*(x*a)";
       
   453 
       
   454 test "(x*k) div (k*(y::nat)) = (uu::nat)";
       
   455 test "(k) div (k*(y::nat)) = (uu::nat)";
       
   456 test "(a*(b*c)) div ((b::nat)) = (uu::nat)";
       
   457 test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)";
       
   458 *)
   416 *)