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