src/HOL/Integ/int_factor_simprocs.ML
author paulson
Wed Nov 29 10:21:43 2000 +0100 (2000-11-29)
changeset 10536 8f34ecae1446
child 10703 ba98f00cec4f
permissions -rw-r--r--
invoking CancelNumeralFactorFun
     1 (*  Title:      HOL/int_factor_simprocs.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   2000  University of Cambridge
     5 
     6 Factor cancellation simprocs for the integers.
     7 
     8 This file can't be combined with int_arith1,2 because it requires IntDiv.thy.
     9 *)
    10 
    11 (** Factor cancellation theorems for "int" **)
    12 
    13 Goal "!!k::int. (k*m <= k*n) = ((#0 < k --> m<=n) & (k < #0 --> n<=m))";
    14 by (stac zmult_zle_cancel1 1);
    15 by Auto_tac;  
    16 qed "int_mult_le_cancel1";
    17 
    18 Goal "!!k::int. (k*m < k*n) = ((#0 < k & m<n) | (k < #0 & n<m))";
    19 by (stac zmult_zless_cancel1 1);
    20 by Auto_tac;  
    21 qed "int_mult_less_cancel1";
    22 
    23 Goal "!!k::int. (k*m = k*n) = (k = #0 | m=n)";
    24 by Auto_tac;  
    25 qed "int_mult_eq_cancel1";
    26 
    27 Goal "!!k::int. k~=#0 ==> (k*m) div (k*n) = (m div n)";
    28 by (stac zdiv_zmult_zmult1 1); 
    29 by Auto_tac;  
    30 qed "int_mult_div_cancel1";
    31 
    32 local
    33   open Int_Numeral_Simprocs
    34 in
    35 
    36 structure CancelNumeralFactorCommon =
    37   struct
    38   val mk_coeff		= mk_coeff
    39   val dest_coeff	= dest_coeff 1
    40   val trans_tac         = trans_tac
    41   val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s))
    42                  THEN ALLGOALS
    43                     (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
    44                                                bin_simps@zmult_ac))
    45   val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    46   val simplify_meta_eq  = simplify_meta_eq mult_1s
    47   end
    48 
    49 structure DivCancelNumeralFactor = CancelNumeralFactorFun
    50  (open CancelNumeralFactorCommon
    51   val prove_conv = prove_conv "intdiv_cancel_numeral_factor"
    52   val mk_bal   = HOLogic.mk_binop "Divides.op div"
    53   val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
    54   val cancel = int_mult_div_cancel1 RS trans
    55   val neg_exchanges = false
    56 )
    57 
    58 structure EqCancelNumeralFactor = CancelNumeralFactorFun
    59  (open CancelNumeralFactorCommon
    60   val prove_conv = prove_conv "inteq_cancel_numeral_factor"
    61   val mk_bal   = HOLogic.mk_eq
    62   val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    63   val cancel = int_mult_eq_cancel1 RS trans
    64   val neg_exchanges = false
    65 )
    66 
    67 structure LessCancelNumeralFactor = CancelNumeralFactorFun
    68  (open CancelNumeralFactorCommon
    69   val prove_conv = prove_conv "intless_cancel_numeral_factor"
    70   val mk_bal   = HOLogic.mk_binrel "op <"
    71   val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
    72   val cancel = int_mult_less_cancel1 RS trans
    73   val neg_exchanges = true
    74 )
    75 
    76 structure LeCancelNumeralFactor = CancelNumeralFactorFun
    77  (open CancelNumeralFactorCommon
    78   val prove_conv = prove_conv "intle_cancel_numeral_factor"
    79   val mk_bal   = HOLogic.mk_binrel "op <="
    80   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
    81   val cancel = int_mult_le_cancel1 RS trans
    82   val neg_exchanges = true
    83 )
    84 
    85 val int_cancel_numeral_factors = 
    86   map prep_simproc
    87    [("inteq_cancel_numeral_factors",
    88      prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
    89      EqCancelNumeralFactor.proc),
    90     ("intless_cancel_numeral_factors", 
    91      prep_pats ["(l::int) * m < n", "(l::int) < m * n"], 
    92      LessCancelNumeralFactor.proc),
    93     ("intle_cancel_numeral_factors", 
    94      prep_pats ["(l::int) * m <= n", "(l::int) <= m * n"], 
    95      LeCancelNumeralFactor.proc),
    96     ("intdiv_cancel_numeral_factors", 
    97      prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
    98      DivCancelNumeralFactor.proc)];
    99 
   100 end;
   101 
   102 Addsimprocs int_cancel_numeral_factors;
   103 
   104 
   105 (*examples:
   106 print_depth 22;
   107 set timing;
   108 set trace_simp;
   109 fun test s = (Goal s; by (Simp_tac 1)); 
   110 
   111 test "#9*x = #12 * (y::int)";
   112 test "(#9*x) div (#12 * (y::int)) = z";
   113 test "#9*x < #12 * (y::int)";
   114 test "#9*x <= #12 * (y::int)";
   115 
   116 test "#-99*x = #132 * (y::int)";
   117 test "(#-99*x) div (#132 * (y::int)) = z";
   118 test "#-99*x < #132 * (y::int)";
   119 test "#-99*x <= #132 * (y::int)";
   120 
   121 test "#999*x = #-396 * (y::int)";
   122 test "(#999*x) div (#-396 * (y::int)) = z";
   123 test "#999*x < #-396 * (y::int)";
   124 test "#999*x <= #-396 * (y::int)";
   125 
   126 test "#-99*x = #-81 * (y::int)";
   127 test "(#-99*x) div (#-81 * (y::int)) = z";
   128 test "#-99*x <= #-81 * (y::int)";
   129 test "#-99*x < #-81 * (y::int)";
   130 
   131 test "#-2 * x = #-1 * (y::int)";
   132 test "#-2 * x = -(y::int)";
   133 test "(#-2 * x) div (#-1 * (y::int)) = z";
   134 test "#-2 * x < -(y::int)";
   135 test "#-2 * x <= #-1 * (y::int)";
   136 test "-x < #-23 * (y::int)";
   137 test "-x <= #-23 * (y::int)";
   138 *)
   139