src/HOL/Integ/int_factor_simprocs.ML
changeset 10536 8f34ecae1446
child 10703 ba98f00cec4f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Wed Nov 29 10:21:43 2000 +0100
     1.3 @@ -0,0 +1,139 @@
     1.4 +(*  Title:      HOL/int_factor_simprocs.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   2000  University of Cambridge
     1.8 +
     1.9 +Factor cancellation simprocs for the integers.
    1.10 +
    1.11 +This file can't be combined with int_arith1,2 because it requires IntDiv.thy.
    1.12 +*)
    1.13 +
    1.14 +(** Factor cancellation theorems for "int" **)
    1.15 +
    1.16 +Goal "!!k::int. (k*m <= k*n) = ((#0 < k --> m<=n) & (k < #0 --> n<=m))";
    1.17 +by (stac zmult_zle_cancel1 1);
    1.18 +by Auto_tac;  
    1.19 +qed "int_mult_le_cancel1";
    1.20 +
    1.21 +Goal "!!k::int. (k*m < k*n) = ((#0 < k & m<n) | (k < #0 & n<m))";
    1.22 +by (stac zmult_zless_cancel1 1);
    1.23 +by Auto_tac;  
    1.24 +qed "int_mult_less_cancel1";
    1.25 +
    1.26 +Goal "!!k::int. (k*m = k*n) = (k = #0 | m=n)";
    1.27 +by Auto_tac;  
    1.28 +qed "int_mult_eq_cancel1";
    1.29 +
    1.30 +Goal "!!k::int. k~=#0 ==> (k*m) div (k*n) = (m div n)";
    1.31 +by (stac zdiv_zmult_zmult1 1); 
    1.32 +by Auto_tac;  
    1.33 +qed "int_mult_div_cancel1";
    1.34 +
    1.35 +local
    1.36 +  open Int_Numeral_Simprocs
    1.37 +in
    1.38 +
    1.39 +structure CancelNumeralFactorCommon =
    1.40 +  struct
    1.41 +  val mk_coeff		= mk_coeff
    1.42 +  val dest_coeff	= dest_coeff 1
    1.43 +  val trans_tac         = trans_tac
    1.44 +  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s))
    1.45 +                 THEN ALLGOALS
    1.46 +                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
    1.47 +                                               bin_simps@zmult_ac))
    1.48 +  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    1.49 +  val simplify_meta_eq  = simplify_meta_eq mult_1s
    1.50 +  end
    1.51 +
    1.52 +structure DivCancelNumeralFactor = CancelNumeralFactorFun
    1.53 + (open CancelNumeralFactorCommon
    1.54 +  val prove_conv = prove_conv "intdiv_cancel_numeral_factor"
    1.55 +  val mk_bal   = HOLogic.mk_binop "Divides.op div"
    1.56 +  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
    1.57 +  val cancel = int_mult_div_cancel1 RS trans
    1.58 +  val neg_exchanges = false
    1.59 +)
    1.60 +
    1.61 +structure EqCancelNumeralFactor = CancelNumeralFactorFun
    1.62 + (open CancelNumeralFactorCommon
    1.63 +  val prove_conv = prove_conv "inteq_cancel_numeral_factor"
    1.64 +  val mk_bal   = HOLogic.mk_eq
    1.65 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    1.66 +  val cancel = int_mult_eq_cancel1 RS trans
    1.67 +  val neg_exchanges = false
    1.68 +)
    1.69 +
    1.70 +structure LessCancelNumeralFactor = CancelNumeralFactorFun
    1.71 + (open CancelNumeralFactorCommon
    1.72 +  val prove_conv = prove_conv "intless_cancel_numeral_factor"
    1.73 +  val mk_bal   = HOLogic.mk_binrel "op <"
    1.74 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
    1.75 +  val cancel = int_mult_less_cancel1 RS trans
    1.76 +  val neg_exchanges = true
    1.77 +)
    1.78 +
    1.79 +structure LeCancelNumeralFactor = CancelNumeralFactorFun
    1.80 + (open CancelNumeralFactorCommon
    1.81 +  val prove_conv = prove_conv "intle_cancel_numeral_factor"
    1.82 +  val mk_bal   = HOLogic.mk_binrel "op <="
    1.83 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
    1.84 +  val cancel = int_mult_le_cancel1 RS trans
    1.85 +  val neg_exchanges = true
    1.86 +)
    1.87 +
    1.88 +val int_cancel_numeral_factors = 
    1.89 +  map prep_simproc
    1.90 +   [("inteq_cancel_numeral_factors",
    1.91 +     prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
    1.92 +     EqCancelNumeralFactor.proc),
    1.93 +    ("intless_cancel_numeral_factors", 
    1.94 +     prep_pats ["(l::int) * m < n", "(l::int) < m * n"], 
    1.95 +     LessCancelNumeralFactor.proc),
    1.96 +    ("intle_cancel_numeral_factors", 
    1.97 +     prep_pats ["(l::int) * m <= n", "(l::int) <= m * n"], 
    1.98 +     LeCancelNumeralFactor.proc),
    1.99 +    ("intdiv_cancel_numeral_factors", 
   1.100 +     prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
   1.101 +     DivCancelNumeralFactor.proc)];
   1.102 +
   1.103 +end;
   1.104 +
   1.105 +Addsimprocs int_cancel_numeral_factors;
   1.106 +
   1.107 +
   1.108 +(*examples:
   1.109 +print_depth 22;
   1.110 +set timing;
   1.111 +set trace_simp;
   1.112 +fun test s = (Goal s; by (Simp_tac 1)); 
   1.113 +
   1.114 +test "#9*x = #12 * (y::int)";
   1.115 +test "(#9*x) div (#12 * (y::int)) = z";
   1.116 +test "#9*x < #12 * (y::int)";
   1.117 +test "#9*x <= #12 * (y::int)";
   1.118 +
   1.119 +test "#-99*x = #132 * (y::int)";
   1.120 +test "(#-99*x) div (#132 * (y::int)) = z";
   1.121 +test "#-99*x < #132 * (y::int)";
   1.122 +test "#-99*x <= #132 * (y::int)";
   1.123 +
   1.124 +test "#999*x = #-396 * (y::int)";
   1.125 +test "(#999*x) div (#-396 * (y::int)) = z";
   1.126 +test "#999*x < #-396 * (y::int)";
   1.127 +test "#999*x <= #-396 * (y::int)";
   1.128 +
   1.129 +test "#-99*x = #-81 * (y::int)";
   1.130 +test "(#-99*x) div (#-81 * (y::int)) = z";
   1.131 +test "#-99*x <= #-81 * (y::int)";
   1.132 +test "#-99*x < #-81 * (y::int)";
   1.133 +
   1.134 +test "#-2 * x = #-1 * (y::int)";
   1.135 +test "#-2 * x = -(y::int)";
   1.136 +test "(#-2 * x) div (#-1 * (y::int)) = z";
   1.137 +test "#-2 * x < -(y::int)";
   1.138 +test "#-2 * x <= #-1 * (y::int)";
   1.139 +test "-x < #-23 * (y::int)";
   1.140 +test "-x <= #-23 * (y::int)";
   1.141 +*)
   1.142 +