23164

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 (and for fields).


7 


8 
This file can't be combined with int_arith1 because it requires IntDiv.thy.


9 
*)


10 


11 


12 
(*To quote from Provers/Arith/cancel_numeral_factor.ML:


13 


14 
Cancels common coefficients in balanced expressions:


15 


16 
u*#m ~~ u'*#m' == #n*u ~~ #n'*u'


17 


18 
where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)


19 
and d = gcd(m,m') and n=m/d and n'=m'/d.


20 
*)


21 


22 
val rel_number_of = [eq_number_of_eq, less_number_of_eq_neg, le_number_of_eq];


23 


24 
(** Factor cancellation theorems for integer division (div, not /) **)


25 


26 
Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";


27 
by (stac @{thm zdiv_zmult_zmult1} 1);


28 
by Auto_tac;


29 
qed "int_mult_div_cancel1";


30 


31 
(*For ExtractCommonTermFun, cancelling common factors*)


32 
Goal "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)";


33 
by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1);


34 
qed "int_mult_div_cancel_disj";


35 


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 = fn _ => trans_tac


46 


47 
val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s


48 
val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps


49 
val norm_ss3 = HOL_ss addsimps mult_ac


50 
fun norm_tac ss =


51 
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))


52 
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))


53 
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))


54 


55 
val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps


56 
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))


57 
val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq


58 
[@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},


59 
@{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right}];


60 
end


61 


62 
(*Version for integer division*)


63 
structure IntDivCancelNumeralFactor = CancelNumeralFactorFun


64 
(open CancelNumeralFactorCommon


65 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv


66 
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}


67 
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT


68 
val cancel = int_mult_div_cancel1 RS trans


69 
val neg_exchanges = false


70 
)


71 


72 
(*Version for fields*)


73 
structure DivideCancelNumeralFactor = CancelNumeralFactorFun


74 
(open CancelNumeralFactorCommon


75 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv


76 
val mk_bal = HOLogic.mk_binop @{const_name HOL.divide}


77 
val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT


78 
val cancel = @{thm mult_divide_cancel_left} RS trans


79 
val neg_exchanges = false


80 
)


81 


82 
structure EqCancelNumeralFactor = CancelNumeralFactorFun


83 
(open CancelNumeralFactorCommon


84 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv


85 
val mk_bal = HOLogic.mk_eq


86 
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT


87 
val cancel = @{thm mult_cancel_left} RS trans


88 
val neg_exchanges = false


89 
)


90 


91 
structure LessCancelNumeralFactor = CancelNumeralFactorFun


92 
(open CancelNumeralFactorCommon


93 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv


94 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less}


95 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT


96 
val cancel = @{thm mult_less_cancel_left} RS trans


97 
val neg_exchanges = true


98 
)


99 


100 
structure LeCancelNumeralFactor = CancelNumeralFactorFun


101 
(open CancelNumeralFactorCommon


102 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv


103 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}


104 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT


105 
val cancel = @{thm mult_le_cancel_left} RS trans


106 
val neg_exchanges = true


107 
)


108 


109 
val cancel_numeral_factors =


110 
map Int_Numeral_Base_Simprocs.prep_simproc


111 
[("ring_eq_cancel_numeral_factor",


112 
["(l::'a::{idom,number_ring}) * m = n",


113 
"(l::'a::{idom,number_ring}) = m * n"],


114 
K EqCancelNumeralFactor.proc),


115 
("ring_less_cancel_numeral_factor",


116 
["(l::'a::{ordered_idom,number_ring}) * m < n",


117 
"(l::'a::{ordered_idom,number_ring}) < m * n"],


118 
K LessCancelNumeralFactor.proc),


119 
("ring_le_cancel_numeral_factor",


120 
["(l::'a::{ordered_idom,number_ring}) * m <= n",


121 
"(l::'a::{ordered_idom,number_ring}) <= m * n"],


122 
K LeCancelNumeralFactor.proc),


123 
("int_div_cancel_numeral_factors",


124 
["((l::int) * m) div n", "(l::int) div (m * n)"],


125 
K IntDivCancelNumeralFactor.proc),


126 
("divide_cancel_numeral_factor",


127 
["((l::'a::{division_by_zero,field,number_ring}) * m) / n",


128 
"(l::'a::{division_by_zero,field,number_ring}) / (m * n)",


129 
"((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],


130 
K DivideCancelNumeralFactor.proc)];


131 


132 
(* referenced by rat_arith.ML *)


133 
val field_cancel_numeral_factors =


134 
map Int_Numeral_Base_Simprocs.prep_simproc


135 
[("field_eq_cancel_numeral_factor",


136 
["(l::'a::{field,number_ring}) * m = n",


137 
"(l::'a::{field,number_ring}) = m * n"],


138 
K EqCancelNumeralFactor.proc),


139 
("field_cancel_numeral_factor",


140 
["((l::'a::{division_by_zero,field,number_ring}) * m) / n",


141 
"(l::'a::{division_by_zero,field,number_ring}) / (m * n)",


142 
"((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],


143 
K DivideCancelNumeralFactor.proc)]


144 


145 
end;


146 


147 
Addsimprocs cancel_numeral_factors;


148 


149 
(*examples:


150 
print_depth 22;


151 
set timing;


152 
set trace_simp;


153 
fun test s = (Goal s; by (Simp_tac 1));


154 


155 
test "9*x = 12 * (y::int)";


156 
test "(9*x) div (12 * (y::int)) = z";


157 
test "9*x < 12 * (y::int)";


158 
test "9*x <= 12 * (y::int)";


159 


160 
test "99*x = 132 * (y::int)";


161 
test "(99*x) div (132 * (y::int)) = z";


162 
test "99*x < 132 * (y::int)";


163 
test "99*x <= 132 * (y::int)";


164 


165 
test "999*x = 396 * (y::int)";


166 
test "(999*x) div (396 * (y::int)) = z";


167 
test "999*x < 396 * (y::int)";


168 
test "999*x <= 396 * (y::int)";


169 


170 
test "99*x = 81 * (y::int)";


171 
test "(99*x) div (81 * (y::int)) = z";


172 
test "99*x <= 81 * (y::int)";


173 
test "99*x < 81 * (y::int)";


174 


175 
test "2 * x = 1 * (y::int)";


176 
test "2 * x = (y::int)";


177 
test "(2 * x) div (1 * (y::int)) = z";


178 
test "2 * x < (y::int)";


179 
test "2 * x <= 1 * (y::int)";


180 
test "x < 23 * (y::int)";


181 
test "x <= 23 * (y::int)";


182 
*)


183 


184 
(*And the same examples for fields such as rat or real:


185 
test "0 <= (y::rat) * 2";


186 
test "9*x = 12 * (y::rat)";


187 
test "(9*x) / (12 * (y::rat)) = z";


188 
test "9*x < 12 * (y::rat)";


189 
test "9*x <= 12 * (y::rat)";


190 


191 
test "99*x = 132 * (y::rat)";


192 
test "(99*x) / (132 * (y::rat)) = z";


193 
test "99*x < 132 * (y::rat)";


194 
test "99*x <= 132 * (y::rat)";


195 


196 
test "999*x = 396 * (y::rat)";


197 
test "(999*x) / (396 * (y::rat)) = z";


198 
test "999*x < 396 * (y::rat)";


199 
test "999*x <= 396 * (y::rat)";


200 


201 
test "( ((2::rat) * x) <= 2 * y)";


202 
test "99*x = 81 * (y::rat)";


203 
test "(99*x) / (81 * (y::rat)) = z";


204 
test "99*x <= 81 * (y::rat)";


205 
test "99*x < 81 * (y::rat)";


206 


207 
test "2 * x = 1 * (y::rat)";


208 
test "2 * x = (y::rat)";


209 
test "(2 * x) / (1 * (y::rat)) = z";


210 
test "2 * x < (y::rat)";


211 
test "2 * x <= 1 * (y::rat)";


212 
test "x < 23 * (y::rat)";


213 
test "x <= 23 * (y::rat)";


214 
*)


215 


216 


217 
(** Declarations for ExtractCommonTerm **)


218 


219 
local


220 
open Int_Numeral_Simprocs


221 
in


222 


223 
(*Find first term that matches u*)


224 
fun find_first_t past u [] = raise TERM ("find_first_t", [])


225 
 find_first_t past u (t::terms) =


226 
if u aconv t then (rev past @ terms)


227 
else find_first_t (t::past) u terms


228 
handle TERM _ => find_first_t (t::past) u terms;


229 


230 
(** Final simplification for the CancelFactor simprocs **)


231 
val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq


232 
[@{thm mult_1_left}, mult_1_right, @{thm zdiv_1}, numeral_1_eq_1];


233 


234 
fun cancel_simplify_meta_eq cancel_th ss th =


235 
simplify_one ss (([th, cancel_th]) MRS trans);


236 


237 
(*At present, long_mk_prod creates Numeral1, so this requires the axclass


238 
number_ring*)


239 
structure CancelFactorCommon =


240 
struct


241 
val mk_sum = long_mk_prod


242 
val dest_sum = dest_prod


243 
val mk_coeff = mk_coeff


244 
val dest_coeff = dest_coeff


245 
val find_first = find_first_t []


246 
val trans_tac = fn _ => trans_tac


247 
val norm_ss = HOL_ss addsimps mult_1s @ mult_ac


248 
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))


249 
end;


250 


251 
(*mult_cancel_left requires a ring with no zero divisors.*)


252 
structure EqCancelFactor = ExtractCommonTermFun


253 
(open CancelFactorCommon


254 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv


255 
val mk_bal = HOLogic.mk_eq


256 
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT


257 
val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_cancel_left}


258 
);


259 


260 
(*int_mult_div_cancel_disj is for integer division (div).*)


261 
structure IntDivCancelFactor = ExtractCommonTermFun


262 
(open CancelFactorCommon


263 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv


264 
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}


265 
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT


266 
val simplify_meta_eq = cancel_simplify_meta_eq int_mult_div_cancel_disj


267 
);


268 


269 
(*Version for all fields, including unordered ones (type complex).*)


270 
structure DivideCancelFactor = ExtractCommonTermFun


271 
(open CancelFactorCommon


272 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv


273 
val mk_bal = HOLogic.mk_binop @{const_name HOL.divide}


274 
val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT


275 
val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_divide_cancel_eq_if}


276 
);


277 


278 
(*The number_ring class is necessary because the simprocs refer to the


279 
binary number 1. FIXME: probably they could use 1 instead.*)


280 
val cancel_factors =


281 
map Int_Numeral_Base_Simprocs.prep_simproc


282 
[("ring_eq_cancel_factor",


283 
["(l::'a::{idom,number_ring}) * m = n",


284 
"(l::'a::{idom,number_ring}) = m * n"],


285 
K EqCancelFactor.proc),


286 
("int_div_cancel_factor",


287 
["((l::int) * m) div n", "(l::int) div (m * n)"],


288 
K IntDivCancelFactor.proc),


289 
("divide_cancel_factor",


290 
["((l::'a::{division_by_zero,field,number_ring}) * m) / n",


291 
"(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],


292 
K DivideCancelFactor.proc)];


293 


294 
end;


295 


296 
Addsimprocs cancel_factors;


297 


298 


299 
(*examples:


300 
print_depth 22;


301 
set timing;


302 
set trace_simp;


303 
fun test s = (Goal s; by (Asm_simp_tac 1));


304 


305 
test "x*k = k*(y::int)";


306 
test "k = k*(y::int)";


307 
test "a*(b*c) = (b::int)";


308 
test "a*(b*c) = d*(b::int)*(x*a)";


309 


310 
test "(x*k) div (k*(y::int)) = (uu::int)";


311 
test "(k) div (k*(y::int)) = (uu::int)";


312 
test "(a*(b*c)) div ((b::int)) = (uu::int)";


313 
test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";


314 
*)


315 


316 
(*And the same examples for fields such as rat or real:


317 
print_depth 22;


318 
set timing;


319 
set trace_simp;


320 
fun test s = (Goal s; by (Asm_simp_tac 1));


321 


322 
test "x*k = k*(y::rat)";


323 
test "k = k*(y::rat)";


324 
test "a*(b*c) = (b::rat)";


325 
test "a*(b*c) = d*(b::rat)*(x*a)";


326 


327 


328 
test "(x*k) / (k*(y::rat)) = (uu::rat)";


329 
test "(k) / (k*(y::rat)) = (uu::rat)";


330 
test "(a*(b*c)) / ((b::rat)) = (uu::rat)";


331 
test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";


332 


333 
(*FIXME: what do we do about this?*)


334 
test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";


335 
*)
