src/HOL/Integ/int_factor_simprocs.ML
changeset 14390 55fe71faadda
parent 14387 e96d5c42c4b0
child 14426 de890c247b38
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Mon Feb 16 15:24:03 2004 +0100
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Feb 17 10:41:59 2004 +0100
     1.3 @@ -3,12 +3,25 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   2000  University of Cambridge
     1.6  
     1.7 -Factor cancellation simprocs for the integers.
     1.8 +Factor cancellation simprocs for the integers (and for fields).
     1.9  
    1.10  This file can't be combined with int_arith1 because it requires IntDiv.thy.
    1.11  *)
    1.12  
    1.13 -(** Factor cancellation theorems for "int" **)
    1.14 +
    1.15 +(*To quote from Provers/Arith/cancel_numeral_factor.ML:
    1.16 +
    1.17 +Cancels common coefficients in balanced expressions:
    1.18 +
    1.19 +     u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'
    1.20 +
    1.21 +where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
    1.22 +and d = gcd(m,m') and n=m/d and n'=m'/d.
    1.23 +*)
    1.24 +
    1.25 +val rel_number_of = [eq_number_of_eq, less_number_of_eq_neg, le_number_of_eq];
    1.26 +
    1.27 +(** Factor cancellation theorems for integer division (div, not /) **)
    1.28  
    1.29  Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
    1.30  by (stac zdiv_zmult_zmult1 1);
    1.31 @@ -31,13 +44,18 @@
    1.32    val dest_coeff        = dest_coeff 1
    1.33    val trans_tac         = trans_tac
    1.34    val norm_tac =
    1.35 -     ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@mult_1s))
    1.36 +     ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps @ mult_1s))
    1.37       THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_minus_simps))
    1.38       THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
    1.39 -  val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    1.40 -  val simplify_meta_eq  = simplify_meta_eq mult_1s
    1.41 +  val numeral_simp_tac  =
    1.42 +         ALLGOALS (simp_tac (HOL_ss addsimps rel_number_of@bin_simps))
    1.43 +  val simplify_meta_eq  = 
    1.44 +	Int_Numeral_Simprocs.simplify_meta_eq
    1.45 +	     [add_0, add_0_right,
    1.46 +	      mult_zero_left, mult_zero_right, mult_1, mult_1_right];
    1.47    end
    1.48  
    1.49 +(*Version for integer division*)
    1.50  structure DivCancelNumeralFactor = CancelNumeralFactorFun
    1.51   (open CancelNumeralFactorCommon
    1.52    val prove_conv = Bin_Simprocs.prove_conv
    1.53 @@ -47,20 +65,41 @@
    1.54    val neg_exchanges = false
    1.55  )
    1.56  
    1.57 +(*Version for fields*)
    1.58 +structure FieldDivCancelNumeralFactor = CancelNumeralFactorFun
    1.59 + (open CancelNumeralFactorCommon
    1.60 +  val prove_conv = Bin_Simprocs.prove_conv
    1.61 +  val mk_bal   = HOLogic.mk_binop "HOL.divide"
    1.62 +  val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
    1.63 +  val cancel = mult_divide_cancel_left RS trans
    1.64 +  val neg_exchanges = false
    1.65 +)
    1.66 +
    1.67 +(*Version for ordered rings: mult_cancel_left requires an ordering*)
    1.68  structure EqCancelNumeralFactor = CancelNumeralFactorFun
    1.69   (open CancelNumeralFactorCommon
    1.70    val prove_conv = Bin_Simprocs.prove_conv
    1.71    val mk_bal   = HOLogic.mk_eq
    1.72 -  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    1.73 +  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    1.74    val cancel = mult_cancel_left RS trans
    1.75    val neg_exchanges = false
    1.76  )
    1.77  
    1.78 +(*Version for (unordered) fields*)
    1.79 +structure FieldEqCancelNumeralFactor = CancelNumeralFactorFun
    1.80 + (open CancelNumeralFactorCommon
    1.81 +  val prove_conv = Bin_Simprocs.prove_conv
    1.82 +  val mk_bal   = HOLogic.mk_eq
    1.83 +  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    1.84 +  val cancel = field_mult_cancel_left RS trans
    1.85 +  val neg_exchanges = false
    1.86 +)
    1.87 +
    1.88  structure LessCancelNumeralFactor = CancelNumeralFactorFun
    1.89   (open CancelNumeralFactorCommon
    1.90    val prove_conv = Bin_Simprocs.prove_conv
    1.91    val mk_bal   = HOLogic.mk_binrel "op <"
    1.92 -  val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
    1.93 +  val dest_bal = HOLogic.dest_bin "op <" Term.dummyT
    1.94    val cancel = mult_less_cancel_left RS trans
    1.95    val neg_exchanges = true
    1.96  )
    1.97 @@ -69,26 +108,46 @@
    1.98   (open CancelNumeralFactorCommon
    1.99    val prove_conv = Bin_Simprocs.prove_conv
   1.100    val mk_bal   = HOLogic.mk_binrel "op <="
   1.101 -  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
   1.102 +  val dest_bal = HOLogic.dest_bin "op <=" Term.dummyT
   1.103    val cancel = mult_le_cancel_left RS trans
   1.104    val neg_exchanges = true
   1.105  )
   1.106  
   1.107 -val int_cancel_numeral_factors =
   1.108 +val ring_cancel_numeral_factors =
   1.109    map Bin_Simprocs.prep_simproc
   1.110 -   [("inteq_cancel_numeral_factors", ["(l::int) * m = n", "(l::int) = m * n"],
   1.111 +   [("ring_eq_cancel_numeral_factor",
   1.112 +     ["(l::'a::{ordered_ring,number_ring}) * m = n",
   1.113 +      "(l::'a::{ordered_ring,number_ring}) = m * n"],
   1.114       EqCancelNumeralFactor.proc),
   1.115 -    ("intless_cancel_numeral_factors", ["(l::int) * m < n", "(l::int) < m * n"],
   1.116 +    ("ring_less_cancel_numeral_factor",
   1.117 +     ["(l::'a::{ordered_ring,number_ring}) * m < n",
   1.118 +      "(l::'a::{ordered_ring,number_ring}) < m * n"],
   1.119       LessCancelNumeralFactor.proc),
   1.120 -    ("intle_cancel_numeral_factors", ["(l::int) * m <= n", "(l::int) <= m * n"],
   1.121 +    ("ring_le_cancel_numeral_factor",
   1.122 +     ["(l::'a::{ordered_ring,number_ring}) * m <= n",
   1.123 +      "(l::'a::{ordered_ring,number_ring}) <= m * n"],
   1.124       LeCancelNumeralFactor.proc),
   1.125 -    ("intdiv_cancel_numeral_factors", ["((l::int) * m) div n", "(l::int) div (m * n)"],
   1.126 +    ("int_div_cancel_numeral_factors",
   1.127 +     ["((l::int) * m) div n", "(l::int) div (m * n)"],
   1.128       DivCancelNumeralFactor.proc)];
   1.129  
   1.130 +
   1.131 +val field_cancel_numeral_factors =
   1.132 +  map Bin_Simprocs.prep_simproc
   1.133 +   [("field_eq_cancel_numeral_factor",
   1.134 +     ["(l::'a::{field,number_ring}) * m = n",
   1.135 +      "(l::'a::{field,number_ring}) = m * n"],
   1.136 +     FieldEqCancelNumeralFactor.proc),
   1.137 +    ("field_cancel_numeral_factor",
   1.138 +     ["((l::'a::{field,number_ring}) * m) / n",
   1.139 +      "(l::'a::{field,number_ring}) / (m * n)",
   1.140 +      "((number_of v)::'a::{field,number_ring}) / (number_of w)"],
   1.141 +     FieldDivCancelNumeralFactor.proc)]
   1.142 +
   1.143  end;
   1.144  
   1.145 -Addsimprocs int_cancel_numeral_factors;
   1.146 -
   1.147 +Addsimprocs ring_cancel_numeral_factors;
   1.148 +Addsimprocs field_cancel_numeral_factors;
   1.149  
   1.150  (*examples:
   1.151  print_depth 22;
   1.152 @@ -125,6 +184,38 @@
   1.153  test "-x <= -23 * (y::int)";
   1.154  *)
   1.155  
   1.156 +(*And the same examples for fields such as rat or real:
   1.157 +test "0 <= (y::rat) * -2";
   1.158 +test "9*x = 12 * (y::rat)";
   1.159 +test "(9*x) / (12 * (y::rat)) = z";
   1.160 +test "9*x < 12 * (y::rat)";
   1.161 +test "9*x <= 12 * (y::rat)";
   1.162 +
   1.163 +test "-99*x = 132 * (y::rat)";
   1.164 +test "(-99*x) / (132 * (y::rat)) = z";
   1.165 +test "-99*x < 132 * (y::rat)";
   1.166 +test "-99*x <= 132 * (y::rat)";
   1.167 +
   1.168 +test "999*x = -396 * (y::rat)";
   1.169 +test "(999*x) / (-396 * (y::rat)) = z";
   1.170 +test "999*x < -396 * (y::rat)";
   1.171 +test "999*x <= -396 * (y::rat)";
   1.172 +
   1.173 +test  "(- ((2::rat) * x) <= 2 * y)";
   1.174 +test "-99*x = -81 * (y::rat)";
   1.175 +test "(-99*x) / (-81 * (y::rat)) = z";
   1.176 +test "-99*x <= -81 * (y::rat)";
   1.177 +test "-99*x < -81 * (y::rat)";
   1.178 +
   1.179 +test "-2 * x = -1 * (y::rat)";
   1.180 +test "-2 * x = -(y::rat)";
   1.181 +test "(-2 * x) / (-1 * (y::rat)) = z";
   1.182 +test "-2 * x < -(y::rat)";
   1.183 +test "-2 * x <= -1 * (y::rat)";
   1.184 +test "-x < -23 * (y::rat)";
   1.185 +test "-x <= -23 * (y::rat)";
   1.186 +*)
   1.187 +
   1.188  
   1.189  (** Declarations for ExtractCommonTerm **)
   1.190  
   1.191 @@ -178,13 +269,42 @@
   1.192  
   1.193  val int_cancel_factor =
   1.194    map Bin_Simprocs.prep_simproc
   1.195 -   [("int_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"], EqCancelFactor.proc),
   1.196 -    ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m * n)"],
   1.197 +   [("ring_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"], 
   1.198 +    EqCancelFactor.proc),
   1.199 +    ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m*n)"],
   1.200       DivideCancelFactor.proc)];
   1.201  
   1.202 +(** Versions for all fields, including unordered ones (type complex).*)
   1.203 +
   1.204 +structure FieldEqCancelFactor = ExtractCommonTermFun
   1.205 + (open CancelFactorCommon
   1.206 +  val prove_conv = Bin_Simprocs.prove_conv
   1.207 +  val mk_bal   = HOLogic.mk_eq
   1.208 +  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   1.209 +  val simplify_meta_eq  = cancel_simplify_meta_eq field_mult_cancel_left
   1.210 +);
   1.211 +
   1.212 +structure FieldDivideCancelFactor = ExtractCommonTermFun
   1.213 + (open CancelFactorCommon
   1.214 +  val prove_conv = Bin_Simprocs.prove_conv
   1.215 +  val mk_bal   = HOLogic.mk_binop "HOL.divide"
   1.216 +  val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
   1.217 +  val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
   1.218 +);
   1.219 +
   1.220 +val field_cancel_factor =
   1.221 +  map Bin_Simprocs.prep_simproc
   1.222 +   [("field_eq_cancel_factor",
   1.223 +     ["(l::'a::field) * m = n", "(l::'a::field) = m * n"], 
   1.224 +     FieldEqCancelFactor.proc),
   1.225 +    ("field_divide_cancel_factor",
   1.226 +     ["((l::'a::field) * m) / n", "(l::'a::field) / (m * n)"],
   1.227 +     FieldDivideCancelFactor.proc)];
   1.228 +
   1.229  end;
   1.230  
   1.231  Addsimprocs int_cancel_factor;
   1.232 +Addsimprocs field_cancel_factor;
   1.233  
   1.234  
   1.235  (*examples:
   1.236 @@ -204,3 +324,23 @@
   1.237  test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
   1.238  *)
   1.239  
   1.240 +(*And the same examples for fields such as rat or real:
   1.241 +print_depth 22;
   1.242 +set timing;
   1.243 +set trace_simp;
   1.244 +fun test s = (Goal s; by (Asm_simp_tac 1));
   1.245 +
   1.246 +test "x*k = k*(y::rat)";
   1.247 +test "k = k*(y::rat)";
   1.248 +test "a*(b*c) = (b::rat)";
   1.249 +test "a*(b*c) = d*(b::rat)*(x*a)";
   1.250 +
   1.251 +
   1.252 +test "(x*k) / (k*(y::rat)) = (uu::rat)";
   1.253 +test "(k) / (k*(y::rat)) = (uu::rat)";
   1.254 +test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
   1.255 +test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
   1.256 +
   1.257 +(*FIXME: what do we do about this?*)
   1.258 +test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
   1.259 +*)