src/HOL/Integ/int_factor_simprocs.ML
author paulson
Tue Dec 19 15:17:21 2000 +0100 (2000-12-19)
changeset 10703 ba98f00cec4f
parent 10536 8f34ecae1446
child 10713 69c9fc1d11f2
permissions -rw-r--r--
inserting the simproc int_cancel_factor
     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 (*For ExtractCommonTermFun, cancelling common factors*)
    33 Goal "(k*m) div (k*n) = (if k = (#0::int) then #0 else m div n)";
    34 by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1); 
    35 qed "int_mult_div_cancel_disj";
    36 
    37 local
    38   open Int_Numeral_Simprocs
    39 in
    40 
    41 structure CancelNumeralFactorCommon =
    42   struct
    43   val mk_coeff		= mk_coeff
    44   val dest_coeff	= dest_coeff 1
    45   val trans_tac         = trans_tac
    46   val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s))
    47                  THEN ALLGOALS
    48                     (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
    49                                                bin_simps@zmult_ac))
    50   val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    51   val simplify_meta_eq  = simplify_meta_eq mult_1s
    52   end
    53 
    54 structure DivCancelNumeralFactor = CancelNumeralFactorFun
    55  (open CancelNumeralFactorCommon
    56   val prove_conv = prove_conv "intdiv_cancel_numeral_factor"
    57   val mk_bal   = HOLogic.mk_binop "Divides.op div"
    58   val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
    59   val cancel = int_mult_div_cancel1 RS trans
    60   val neg_exchanges = false
    61 )
    62 
    63 structure EqCancelNumeralFactor = CancelNumeralFactorFun
    64  (open CancelNumeralFactorCommon
    65   val prove_conv = prove_conv "inteq_cancel_numeral_factor"
    66   val mk_bal   = HOLogic.mk_eq
    67   val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    68   val cancel = int_mult_eq_cancel1 RS trans
    69   val neg_exchanges = false
    70 )
    71 
    72 structure LessCancelNumeralFactor = CancelNumeralFactorFun
    73  (open CancelNumeralFactorCommon
    74   val prove_conv = prove_conv "intless_cancel_numeral_factor"
    75   val mk_bal   = HOLogic.mk_binrel "op <"
    76   val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
    77   val cancel = int_mult_less_cancel1 RS trans
    78   val neg_exchanges = true
    79 )
    80 
    81 structure LeCancelNumeralFactor = CancelNumeralFactorFun
    82  (open CancelNumeralFactorCommon
    83   val prove_conv = prove_conv "intle_cancel_numeral_factor"
    84   val mk_bal   = HOLogic.mk_binrel "op <="
    85   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
    86   val cancel = int_mult_le_cancel1 RS trans
    87   val neg_exchanges = true
    88 )
    89 
    90 val int_cancel_numeral_factors = 
    91   map prep_simproc
    92    [("inteq_cancel_numeral_factors",
    93      prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
    94      EqCancelNumeralFactor.proc),
    95     ("intless_cancel_numeral_factors", 
    96      prep_pats ["(l::int) * m < n", "(l::int) < m * n"], 
    97      LessCancelNumeralFactor.proc),
    98     ("intle_cancel_numeral_factors", 
    99      prep_pats ["(l::int) * m <= n", "(l::int) <= m * n"], 
   100      LeCancelNumeralFactor.proc),
   101     ("intdiv_cancel_numeral_factors", 
   102      prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
   103      DivCancelNumeralFactor.proc)];
   104 
   105 end;
   106 
   107 Addsimprocs int_cancel_numeral_factors;
   108 
   109 
   110 (*examples:
   111 print_depth 22;
   112 set timing;
   113 set trace_simp;
   114 fun test s = (Goal s; by (Simp_tac 1)); 
   115 
   116 test "#9*x = #12 * (y::int)";
   117 test "(#9*x) div (#12 * (y::int)) = z";
   118 test "#9*x < #12 * (y::int)";
   119 test "#9*x <= #12 * (y::int)";
   120 
   121 test "#-99*x = #132 * (y::int)";
   122 test "(#-99*x) div (#132 * (y::int)) = z";
   123 test "#-99*x < #132 * (y::int)";
   124 test "#-99*x <= #132 * (y::int)";
   125 
   126 test "#999*x = #-396 * (y::int)";
   127 test "(#999*x) div (#-396 * (y::int)) = z";
   128 test "#999*x < #-396 * (y::int)";
   129 test "#999*x <= #-396 * (y::int)";
   130 
   131 test "#-99*x = #-81 * (y::int)";
   132 test "(#-99*x) div (#-81 * (y::int)) = z";
   133 test "#-99*x <= #-81 * (y::int)";
   134 test "#-99*x < #-81 * (y::int)";
   135 
   136 test "#-2 * x = #-1 * (y::int)";
   137 test "#-2 * x = -(y::int)";
   138 test "(#-2 * x) div (#-1 * (y::int)) = z";
   139 test "#-2 * x < -(y::int)";
   140 test "#-2 * x <= #-1 * (y::int)";
   141 test "-x < #-23 * (y::int)";
   142 test "-x <= #-23 * (y::int)";
   143 *)
   144 
   145 
   146 (** Declarations for ExtractCommonTerm **)
   147 
   148 local
   149   open Int_Numeral_Simprocs
   150 in
   151 
   152 
   153 (*this version ALWAYS includes a trailing one*)
   154 fun long_mk_prod []        = one
   155   | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
   156 
   157 (*Find first term that matches u*)
   158 fun find_first past u []         = raise TERM("find_first", []) 
   159   | find_first past u (t::terms) =
   160 	if u aconv t then (rev past @ terms)
   161         else find_first (t::past) u terms
   162 	handle TERM _ => find_first (t::past) u terms;
   163 
   164 (*Final simplification: cancel + and *  *)
   165 fun cancel_simplify_meta_eq cancel_th th = 
   166     Int_Numeral_Simprocs.simplify_meta_eq 
   167         [zmult_1, zmult_1_right] 
   168         (([th, cancel_th]) MRS trans);
   169 
   170 structure CancelFactorCommon =
   171   struct
   172   val mk_sum    	= long_mk_prod
   173   val dest_sum		= dest_prod
   174   val mk_coeff		= mk_coeff
   175   val dest_coeff	= dest_coeff
   176   val find_first	= find_first []
   177   val trans_tac         = trans_tac
   178   val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@zmult_ac))
   179   end;
   180 
   181 structure EqCancelFactor = ExtractCommonTermFun
   182  (open CancelFactorCommon
   183   val prove_conv = prove_conv "int_eq_cancel_factor"
   184   val mk_bal   = HOLogic.mk_eq
   185   val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
   186   val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_eq_cancel1
   187 );
   188 
   189 structure DivideCancelFactor = ExtractCommonTermFun
   190  (open CancelFactorCommon
   191   val prove_conv = prove_conv "int_divide_cancel_factor"
   192   val mk_bal   = HOLogic.mk_binop "Divides.op div"
   193   val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
   194   val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
   195 );
   196 
   197 val int_cancel_factor = 
   198   map prep_simproc
   199    [("int_eq_cancel_factor",
   200      prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
   201      EqCancelFactor.proc),
   202     ("int_divide_cancel_factor", 
   203      prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
   204      DivideCancelFactor.proc)];
   205 
   206 end;
   207 
   208 Addsimprocs int_cancel_factor;
   209 
   210 
   211 (*examples:
   212 print_depth 22;
   213 set timing;
   214 set trace_simp;
   215 fun test s = (Goal s; by (Asm_simp_tac 1)); 
   216 
   217 test "x*k = k*(y::int)";
   218 test "k = k*(y::int)"; 
   219 test "a*(b*c) = (b::int)";
   220 test "a*(b*c) = d*(b::int)*(x*a)";
   221 
   222 test "(x*k) div (k*(y::int)) = (uu::int)";
   223 test "(k) div (k*(y::int)) = (uu::int)"; 
   224 test "(a*(b*c)) div ((b::int)) = (uu::int)";
   225 test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
   226 *)
   227