author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 30031  bd786c37af84 
child 30242  aea5d7fa7ef5 
permissions  rwrr 
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 

29038  22 
val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}]; 
23164  23 

24 
local 

25 
open Int_Numeral_Simprocs 

26 
in 

27 

28 
structure CancelNumeralFactorCommon = 

29 
struct 

30 
val mk_coeff = mk_coeff 

31 
val dest_coeff = dest_coeff 1 

32 
val trans_tac = fn _ => trans_tac 

33 

34 
val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s 

35 
val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps 

23881  36 
val norm_ss3 = HOL_ss addsimps @{thms mult_ac} 
23164  37 
fun norm_tac ss = 
38 
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) 

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

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

41 

42 
val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps 

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

44 
val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq 

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

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25481
diff
changeset

46 
@{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}]; 
23164  47 
end 
48 

49 
(*Version for integer division*) 

50 
structure IntDivCancelNumeralFactor = CancelNumeralFactorFun 

51 
(open CancelNumeralFactorCommon 

52 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

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

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

23401  55 
val cancel = @{thm zdiv_zmult_zmult1} RS trans 
23164  56 
val neg_exchanges = false 
57 
) 

58 

59 
(*Version for fields*) 

60 
structure DivideCancelNumeralFactor = CancelNumeralFactorFun 

61 
(open CancelNumeralFactorCommon 

62 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

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

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

23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23401
diff
changeset

65 
val cancel = @{thm mult_divide_mult_cancel_left} RS trans 
23164  66 
val neg_exchanges = false 
67 
) 

68 

69 
structure EqCancelNumeralFactor = CancelNumeralFactorFun 

70 
(open CancelNumeralFactorCommon 

71 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

72 
val mk_bal = HOLogic.mk_eq 

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

74 
val cancel = @{thm mult_cancel_left} RS trans 

75 
val neg_exchanges = false 

76 
) 

77 

78 
structure LessCancelNumeralFactor = CancelNumeralFactorFun 

79 
(open CancelNumeralFactorCommon 

80 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

23881  81 
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} 
82 
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT 

23164  83 
val cancel = @{thm mult_less_cancel_left} RS trans 
84 
val neg_exchanges = true 

85 
) 

86 

87 
structure LeCancelNumeralFactor = CancelNumeralFactorFun 

88 
(open CancelNumeralFactorCommon 

89 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

23881  90 
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} 
91 
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT 

23164  92 
val cancel = @{thm mult_le_cancel_left} RS trans 
93 
val neg_exchanges = true 

94 
) 

95 

96 
val cancel_numeral_factors = 

97 
map Int_Numeral_Base_Simprocs.prep_simproc 

98 
[("ring_eq_cancel_numeral_factor", 

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

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

101 
K EqCancelNumeralFactor.proc), 

102 
("ring_less_cancel_numeral_factor", 

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

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

105 
K LessCancelNumeralFactor.proc), 

106 
("ring_le_cancel_numeral_factor", 

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

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

109 
K LeCancelNumeralFactor.proc), 

110 
("int_div_cancel_numeral_factors", 

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

112 
K IntDivCancelNumeralFactor.proc), 

113 
("divide_cancel_numeral_factor", 

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

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

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

117 
K DivideCancelNumeralFactor.proc)]; 

118 

119 
(* referenced by rat_arith.ML *) 

120 
val field_cancel_numeral_factors = 

121 
map Int_Numeral_Base_Simprocs.prep_simproc 

122 
[("field_eq_cancel_numeral_factor", 

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

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

125 
K EqCancelNumeralFactor.proc), 

126 
("field_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 
end; 

133 

134 
Addsimprocs cancel_numeral_factors; 

135 

136 
(*examples: 

137 
print_depth 22; 

138 
set timing; 

139 
set trace_simp; 

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

141 

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

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

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

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

146 

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

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

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

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

151 

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

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

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

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

156 

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

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

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

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

161 

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

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

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

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

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

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

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

169 
*) 

170 

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

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

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

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

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

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

177 

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

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

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

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

182 

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

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

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

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

187 

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

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

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

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

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

193 

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

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

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

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

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

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

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

201 
*) 

202 

203 

204 
(** Declarations for ExtractCommonTerm **) 

205 

206 
local 

207 
open Int_Numeral_Simprocs 

208 
in 

209 

210 
(*Find first term that matches u*) 

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

212 
 find_first_t past u (t::terms) = 

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

214 
else find_first_t (t::past) u terms 

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

216 

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

218 
val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq 

30031  219 
[@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}]; 
23164  220 

221 
fun cancel_simplify_meta_eq cancel_th ss th = 

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

223 

224 
structure CancelFactorCommon = 

225 
struct 

226 
val mk_sum = long_mk_prod 

227 
val dest_sum = dest_prod 

228 
val mk_coeff = mk_coeff 

229 
val dest_coeff = dest_coeff 

230 
val find_first = find_first_t [] 

231 
val trans_tac = fn _ => trans_tac 

23881  232 
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} 
23164  233 
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) 
234 
end; 

235 

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

237 
structure EqCancelFactor = ExtractCommonTermFun 

238 
(open CancelFactorCommon 

239 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

240 
val mk_bal = HOLogic.mk_eq 

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

242 
val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_cancel_left} 

243 
); 

244 

23401  245 
(*zdiv_zmult_zmult1_if is for integer division (div).*) 
23164  246 
structure IntDivCancelFactor = ExtractCommonTermFun 
247 
(open CancelFactorCommon 

248 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

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

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

23401  251 
val simplify_meta_eq = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if} 
23164  252 
); 
253 

24395  254 
structure IntModCancelFactor = ExtractCommonTermFun 
255 
(open CancelFactorCommon 

256 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

257 
val mk_bal = HOLogic.mk_binop @{const_name Divides.mod} 

258 
val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT 

259 
val simplify_meta_eq = cancel_simplify_meta_eq @{thm zmod_zmult_zmult1} 

260 
); 

261 

23969  262 
structure IntDvdCancelFactor = ExtractCommonTermFun 
263 
(open CancelFactorCommon 

264 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
26086
diff
changeset

265 
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} 
29981
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29038
diff
changeset

266 
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29038
diff
changeset

267 
val simplify_meta_eq = cancel_simplify_meta_eq @{thm dvd_mult_cancel_left} 
23969  268 
); 
269 

23164  270 
(*Version for all fields, including unordered ones (type complex).*) 
271 
structure DivideCancelFactor = ExtractCommonTermFun 

272 
(open CancelFactorCommon 

273 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

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

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

23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23401
diff
changeset

276 
val simplify_meta_eq = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if} 
23164  277 
); 
278 

279 
val cancel_factors = 

280 
map Int_Numeral_Base_Simprocs.prep_simproc 

281 
[("ring_eq_cancel_factor", 

23400
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23398
diff
changeset

282 
["(l::'a::{idom}) * m = n", 
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23398
diff
changeset

283 
"(l::'a::{idom}) = m * n"], 
23164  284 
K EqCancelFactor.proc), 
285 
("int_div_cancel_factor", 

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

287 
K IntDivCancelFactor.proc), 

24395  288 
("int_mod_cancel_factor", 
289 
["((l::int) * m) mod n", "(l::int) mod (m * n)"], 

290 
K IntModCancelFactor.proc), 

29981
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29038
diff
changeset

291 
("dvd_cancel_factor", 
7d0ed261b712
generalize int_dvd_cancel_factor simproc to idom class
huffman
parents:
29038
diff
changeset

292 
["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"], 
23969  293 
K IntDvdCancelFactor.proc), 
23164  294 
("divide_cancel_factor", 
23400
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23398
diff
changeset

295 
["((l::'a::{division_by_zero,field}) * m) / n", 
a64b39e5809b
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents:
23398
diff
changeset

296 
"(l::'a::{division_by_zero,field}) / (m * n)"], 
23164  297 
K DivideCancelFactor.proc)]; 
298 

299 
end; 

300 

301 
Addsimprocs cancel_factors; 

302 

303 

304 
(*examples: 

305 
print_depth 22; 

306 
set timing; 

307 
set trace_simp; 

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

309 

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

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

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

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

314 

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

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

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

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

319 
*) 

320 

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

322 
print_depth 22; 

323 
set timing; 

324 
set trace_simp; 

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

326 

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

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

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

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

331 

332 

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

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

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

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

337 

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

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

340 
*) 