src/HOL/Tools/nat_numeral_simprocs.ML
changeset 45463 9a588a835c1e
parent 45462 aba629d6cee5
child 45668 0ea1c705eebb
equal deleted inserted replaced
45462:aba629d6cee5 45463:9a588a835c1e
     8   val combine_numerals: simpset -> cterm -> thm option
     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 eq_cancel_numeral_factor: simpset -> cterm -> thm option
       
    14   val less_cancel_numeral_factor: simpset -> cterm -> thm option
       
    15   val le_cancel_numeral_factor: simpset -> cterm -> thm option
       
    16   val div_cancel_numeral_factor: simpset -> cterm -> thm option
       
    17   val dvd_cancel_numeral_factor: simpset -> cterm -> thm option
    13   val eq_cancel_factor: simpset -> cterm -> thm option
    18   val eq_cancel_factor: simpset -> cterm -> thm option
    14   val less_cancel_factor: simpset -> cterm -> thm option
    19   val less_cancel_factor: simpset -> cterm -> thm option
    15   val le_cancel_factor: simpset -> cterm -> thm option
    20   val le_cancel_factor: simpset -> cterm -> thm option
    16   val divide_cancel_factor: simpset -> cterm -> thm option
    21   val div_cancel_factor: simpset -> cterm -> thm option
    17   val dvd_cancel_factor: simpset -> cterm -> thm option
    22   val dvd_cancel_factor: simpset -> cterm -> thm option
    18   val cancel_numeral_factors: simproc list
       
    19 end;
    23 end;
    20 
    24 
    21 structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS =
    25 structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS =
    22 struct
    26 struct
    23 
    27 
   298   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   302   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   299   val cancel = @{thm nat_mult_le_cancel1} RS trans
   303   val cancel = @{thm nat_mult_le_cancel1} RS trans
   300   val neg_exchanges = true
   304   val neg_exchanges = true
   301 )
   305 )
   302 
   306 
   303 val cancel_numeral_factors =
   307 fun eq_cancel_numeral_factor ss ct = EqCancelNumeralFactor.proc ss (term_of ct)
   304   map (Numeral_Simprocs.prep_simproc @{theory})
   308 fun less_cancel_numeral_factor ss ct = LessCancelNumeralFactor.proc ss (term_of ct)
   305    [("nateq_cancel_numeral_factors",
   309 fun le_cancel_numeral_factor ss ct = LeCancelNumeralFactor.proc ss (term_of ct)
   306      ["(l::nat) * m = n", "(l::nat) = m * n"],
   310 fun div_cancel_numeral_factor ss ct = DivCancelNumeralFactor.proc ss (term_of ct)
   307      K EqCancelNumeralFactor.proc),
   311 fun dvd_cancel_numeral_factor ss ct = DvdCancelNumeralFactor.proc ss (term_of ct)
   308     ("natless_cancel_numeral_factors",
       
   309      ["(l::nat) * m < n", "(l::nat) < m * n"],
       
   310      K LessCancelNumeralFactor.proc),
       
   311     ("natle_cancel_numeral_factors",
       
   312      ["(l::nat) * m <= n", "(l::nat) <= m * n"],
       
   313      K LeCancelNumeralFactor.proc),
       
   314     ("natdiv_cancel_numeral_factors",
       
   315      ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
       
   316      K DivCancelNumeralFactor.proc),
       
   317     ("natdvd_cancel_numeral_factors",
       
   318      ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
       
   319      K DvdCancelNumeralFactor.proc)];
       
   320 
       
   321 
   312 
   322 
   313 
   323 (*** Applying ExtractCommonTermFun ***)
   314 (*** Applying ExtractCommonTermFun ***)
   324 
   315 
   325 (*this version ALWAYS includes a trailing one*)
   316 (*this version ALWAYS includes a trailing one*)
   390 );
   381 );
   391 
   382 
   392 fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct)
   383 fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct)
   393 fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct)
   384 fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct)
   394 fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct)
   385 fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct)
   395 fun divide_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct)
   386 fun div_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct)
   396 fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct)
   387 fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct)
   397 
   388 
   398 end;
   389 end;
   399 
       
   400 
       
   401 Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
       
   402 
       
   403 
       
   404 (*examples:
       
   405 print_depth 22;
       
   406 set timing;
       
   407 set simp_trace;
       
   408 fun test s = (Goal s; by (Simp_tac 1));
       
   409 
       
   410 (*cancel_numeral_factors*)
       
   411 test "9*x = 12 * (y::nat)";
       
   412 test "(9*x) div (12 * (y::nat)) = z";
       
   413 test "9*x < 12 * (y::nat)";
       
   414 test "9*x <= 12 * (y::nat)";
       
   415 
       
   416 *)