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 +*)
```