author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 29269  5c25a2012975 
child 30496  7cdcc9dd95cb 
permissions  rwrr 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29039
diff
changeset

1 
(* Title: HOL/Tools/nat_simprocs.ML 
23164  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
3 

4 
Simprocs for nat numerals. 

5 
*) 

6 

7 
structure Nat_Numeral_Simprocs = 

8 
struct 

9 

10 
(*Maps n to #n for n = 0, 1, 2*) 

11 
val numeral_syms = 

23471  12 
[@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym]; 
23164  13 
val numeral_sym_ss = HOL_ss addsimps numeral_syms; 
14 

15 
fun rename_numerals th = 

16 
simplify numeral_sym_ss (Thm.transfer (the_context ()) th); 

17 

18 
(*Utilities*) 

19 

20 
fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n; 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24431
diff
changeset

21 
fun dest_number t = Int.max (0, snd (HOLogic.dest_number t)); 
23164  22 

23 
fun find_first_numeral past (t::terms) = 

24 
((dest_number t, t, rev past @ terms) 

25 
handle TERM _ => find_first_numeral (t::past) terms) 

26 
 find_first_numeral past [] = raise TERM("find_first_numeral", []); 

27 

28 
val zero = mk_number 0; 

29 
val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; 

30 

31 
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) 

32 
fun mk_sum [] = zero 

33 
 mk_sum [t,u] = mk_plus (t, u) 

34 
 mk_sum (t :: ts) = mk_plus (t, mk_sum ts); 

35 

36 
(*this version ALWAYS includes a trailing zero*) 

37 
fun long_mk_sum [] = HOLogic.zero 

38 
 long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); 

39 

40 
val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT; 

41 

42 

43 
(** Other simproc items **) 

44 

45 
val trans_tac = Int_Numeral_Simprocs.trans_tac; 

46 

47 
val bin_simps = 

23471  48 
[@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, 
49 
@{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 

50 
@{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less}, 

51 
@{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 

52 
@{thm less_nat_number_of}, 

53 
@{thm Let_number_of}, @{thm nat_number_of}] @ 

29039  54 
@{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps}; 
23164  55 

56 
fun prep_simproc (name, pats, proc) = 

57 
Simplifier.simproc (the_context ()) name pats proc; 

58 

59 

60 
(*** CancelNumerals simprocs ***) 

61 

62 
val one = mk_number 1; 

63 
val mk_times = HOLogic.mk_binop @{const_name HOL.times}; 

64 

65 
fun mk_prod [] = one 

66 
 mk_prod [t] = t 

67 
 mk_prod (t :: ts) = if t = one then mk_prod ts 

68 
else mk_times (t, mk_prod ts); 

69 

70 
val dest_times = HOLogic.dest_bin @{const_name HOL.times} HOLogic.natT; 

71 

72 
fun dest_prod t = 

73 
let val (t,u) = dest_times t 

74 
in dest_prod t @ dest_prod u end 

75 
handle TERM _ => [t]; 

76 

77 
(*DON'T do the obvious simplifications; that would create special cases*) 

78 
fun mk_coeff (k,t) = mk_times (mk_number k, t); 

79 

80 
(*Express t as a product of (possibly) a numeral with other factors, sorted*) 

81 
fun dest_coeff t = 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29039
diff
changeset

82 
let val ts = sort TermOrd.term_ord (dest_prod t) 
23164  83 
val (n, _, ts') = find_first_numeral [] ts 
84 
handle TERM _ => (1, one, ts) 

85 
in (n, mk_prod ts') end; 

86 

87 
(*Find first coefficientterm THAT MATCHES u*) 

88 
fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 

89 
 find_first_coeff past u (t::terms) = 

90 
let val (n,u') = dest_coeff t 

91 
in if u aconv u' then (n, rev past @ terms) 

92 
else find_first_coeff (t::past) u terms 

93 
end 

94 
handle TERM _ => find_first_coeff (t::past) u terms; 

95 

96 

97 
(*Split up a sum into the list of its constituent terms, on the way removing any 

98 
Sucs and counting them.*) 

99 
fun dest_Suc_sum (Const ("Suc", _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts)) 

100 
 dest_Suc_sum (t, (k,ts)) = 

101 
let val (t1,t2) = dest_plus t 

102 
in dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts))) end 

103 
handle TERM _ => (k, t::ts); 

104 

105 
(*Code for testing whether numerals are already used in the goal*) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25481
diff
changeset

106 
fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true 
23164  107 
 is_numeral _ = false; 
108 

109 
fun prod_has_numeral t = exists is_numeral (dest_prod t); 

110 

111 
(*The Sucs found in the term are converted to a binary numeral. If relaxed is false, 

112 
an exception is raised unless the original expression contains at least one 

113 
numeral in a coefficient position. This prevents nat_combine_numerals from 

114 
introducing numerals to goals.*) 

115 
fun dest_Sucs_sum relaxed t = 

116 
let val (k,ts) = dest_Suc_sum (t,(0,[])) 

117 
in 

118 
if relaxed orelse exists prod_has_numeral ts then 

119 
if k=0 then ts 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24431
diff
changeset

120 
else mk_number k :: ts 
23164  121 
else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t]) 
122 
end; 

123 

124 

125 
(*Simplify 1*n and n*1 to n*) 

23881  126 
val add_0s = map rename_numerals [@{thm add_0}, @{thm add_0_right}]; 
23164  127 
val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}]; 
128 

129 
(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*) 

130 

131 
(*And these help the simproc return False when appropriate, which helps 

132 
the arith prover.*) 

23881  133 
val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc}, 
134 
@{thm Suc_not_Zero}, @{thm le_0_eq}]; 

23164  135 

136 
val simplify_meta_eq = 

137 
Int_Numeral_Simprocs.simplify_meta_eq 

23471  138 
([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm add_0_right}, 
139 
@{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules); 

23164  140 

141 

142 
(*Like HOL_ss but with an ordering that brings numerals to the front 

143 
under ACrewriting.*) 

144 
val num_ss = Int_Numeral_Simprocs.num_ss; 

145 

146 
(*** Applying CancelNumeralsFun ***) 

147 

148 
structure CancelNumeralsCommon = 

149 
struct 

150 
val mk_sum = (fn T:typ => mk_sum) 

151 
val dest_sum = dest_Sucs_sum true 

152 
val mk_coeff = mk_coeff 

153 
val dest_coeff = dest_coeff 

154 
val find_first_coeff = find_first_coeff [] 

155 
val trans_tac = fn _ => trans_tac 

156 

157 
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ 

23881  158 
[@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac} 
159 
val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} 

23164  160 
fun norm_tac ss = 
161 
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) 

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

163 

164 
val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; 

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

166 
val simplify_meta_eq = simplify_meta_eq 

167 
end; 

168 

169 

170 
structure EqCancelNumerals = CancelNumeralsFun 

171 
(open CancelNumeralsCommon 

172 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

173 
val mk_bal = HOLogic.mk_eq 

174 
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT 

23471  175 
val bal_add1 = @{thm nat_eq_add_iff1} RS trans 
176 
val bal_add2 = @{thm nat_eq_add_iff2} RS trans 

23164  177 
); 
178 

179 
structure LessCancelNumerals = CancelNumeralsFun 

180 
(open CancelNumeralsCommon 

181 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

23881  182 
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} 
183 
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT 

23471  184 
val bal_add1 = @{thm nat_less_add_iff1} RS trans 
185 
val bal_add2 = @{thm nat_less_add_iff2} RS trans 

23164  186 
); 
187 

188 
structure LeCancelNumerals = CancelNumeralsFun 

189 
(open CancelNumeralsCommon 

190 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

23881  191 
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} 
192 
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT 

23471  193 
val bal_add1 = @{thm nat_le_add_iff1} RS trans 
194 
val bal_add2 = @{thm nat_le_add_iff2} RS trans 

23164  195 
); 
196 

197 
structure DiffCancelNumerals = CancelNumeralsFun 

198 
(open CancelNumeralsCommon 

199 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

200 
val mk_bal = HOLogic.mk_binop @{const_name HOL.minus} 

201 
val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT 

23471  202 
val bal_add1 = @{thm nat_diff_add_eq1} RS trans 
203 
val bal_add2 = @{thm nat_diff_add_eq2} RS trans 

23164  204 
); 
205 

206 

207 
val cancel_numerals = 

208 
map prep_simproc 

209 
[("nateq_cancel_numerals", 

210 
["(l::nat) + m = n", "(l::nat) = m + n", 

211 
"(l::nat) * m = n", "(l::nat) = m * n", 

212 
"Suc m = n", "m = Suc n"], 

213 
K EqCancelNumerals.proc), 

214 
("natless_cancel_numerals", 

215 
["(l::nat) + m < n", "(l::nat) < m + n", 

216 
"(l::nat) * m < n", "(l::nat) < m * n", 

217 
"Suc m < n", "m < Suc n"], 

218 
K LessCancelNumerals.proc), 

219 
("natle_cancel_numerals", 

220 
["(l::nat) + m <= n", "(l::nat) <= m + n", 

221 
"(l::nat) * m <= n", "(l::nat) <= m * n", 

222 
"Suc m <= n", "m <= Suc n"], 

223 
K LeCancelNumerals.proc), 

224 
("natdiff_cancel_numerals", 

225 
["((l::nat) + m)  n", "(l::nat)  (m + n)", 

226 
"(l::nat) * m  n", "(l::nat)  m * n", 

227 
"Suc m  n", "m  Suc n"], 

228 
K DiffCancelNumerals.proc)]; 

229 

230 

231 
(*** Applying CombineNumeralsFun ***) 

232 

233 
structure CombineNumeralsData = 

234 
struct 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24431
diff
changeset

235 
type coeff = int 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24431
diff
changeset

236 
val iszero = (fn x => x = 0) 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24431
diff
changeset

237 
val add = op + 
23164  238 
val mk_sum = (fn T:typ => long_mk_sum) (*to work for 2*x + 3*x *) 
239 
val dest_sum = dest_Sucs_sum false 

240 
val mk_coeff = mk_coeff 

241 
val dest_coeff = dest_coeff 

23471  242 
val left_distrib = @{thm left_add_mult_distrib} RS trans 
23164  243 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv_nohyps 
244 
val trans_tac = fn _ => trans_tac 

245 

23881  246 
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac} 
247 
val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} 

23164  248 
fun norm_tac ss = 
249 
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) 

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

251 

252 
val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; 

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

254 
val simplify_meta_eq = simplify_meta_eq 

255 
end; 

256 

257 
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); 

258 

259 
val combine_numerals = 

260 
prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc); 

261 

262 

263 
(*** Applying CancelNumeralFactorFun ***) 

264 

265 
structure CancelNumeralFactorCommon = 

266 
struct 

267 
val mk_coeff = mk_coeff 

268 
val dest_coeff = dest_coeff 

269 
val trans_tac = fn _ => trans_tac 

270 

271 
val norm_ss1 = num_ss addsimps 

23881  272 
numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac} 
273 
val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} 

23164  274 
fun norm_tac ss = 
275 
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) 

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

277 

278 
val numeral_simp_ss = HOL_ss addsimps bin_simps 

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

280 
val simplify_meta_eq = simplify_meta_eq 

281 
end 

282 

283 
structure DivCancelNumeralFactor = CancelNumeralFactorFun 

284 
(open CancelNumeralFactorCommon 

285 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

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

287 
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT 

23471  288 
val cancel = @{thm nat_mult_div_cancel1} RS trans 
23164  289 
val neg_exchanges = false 
290 
) 

291 

23969  292 
structure DvdCancelNumeralFactor = CancelNumeralFactorFun 
293 
(open CancelNumeralFactorCommon 

294 
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:
25919
diff
changeset

295 
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
25919
diff
changeset

296 
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT 
23969  297 
val cancel = @{thm nat_mult_dvd_cancel1} RS trans 
298 
val neg_exchanges = false 

299 
) 

300 

23164  301 
structure EqCancelNumeralFactor = CancelNumeralFactorFun 
302 
(open CancelNumeralFactorCommon 

303 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

304 
val mk_bal = HOLogic.mk_eq 

305 
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT 

23471  306 
val cancel = @{thm nat_mult_eq_cancel1} RS trans 
23164  307 
val neg_exchanges = false 
308 
) 

309 

310 
structure LessCancelNumeralFactor = CancelNumeralFactorFun 

311 
(open CancelNumeralFactorCommon 

312 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

23881  313 
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} 
314 
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT 

23471  315 
val cancel = @{thm nat_mult_less_cancel1} RS trans 
23164  316 
val neg_exchanges = true 
317 
) 

318 

319 
structure LeCancelNumeralFactor = CancelNumeralFactorFun 

320 
(open CancelNumeralFactorCommon 

321 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

23881  322 
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} 
323 
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT 

23471  324 
val cancel = @{thm nat_mult_le_cancel1} RS trans 
23164  325 
val neg_exchanges = true 
326 
) 

327 

328 
val cancel_numeral_factors = 

329 
map prep_simproc 

330 
[("nateq_cancel_numeral_factors", 

331 
["(l::nat) * m = n", "(l::nat) = m * n"], 

332 
K EqCancelNumeralFactor.proc), 

333 
("natless_cancel_numeral_factors", 

334 
["(l::nat) * m < n", "(l::nat) < m * n"], 

335 
K LessCancelNumeralFactor.proc), 

336 
("natle_cancel_numeral_factors", 

337 
["(l::nat) * m <= n", "(l::nat) <= m * n"], 

338 
K LeCancelNumeralFactor.proc), 

339 
("natdiv_cancel_numeral_factors", 

340 
["((l::nat) * m) div n", "(l::nat) div (m * n)"], 

23969  341 
K DivCancelNumeralFactor.proc), 
342 
("natdvd_cancel_numeral_factors", 

343 
["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"], 

344 
K DvdCancelNumeralFactor.proc)]; 

23164  345 

346 

347 

348 
(*** Applying ExtractCommonTermFun ***) 

349 

350 
(*this version ALWAYS includes a trailing one*) 

351 
fun long_mk_prod [] = one 

352 
 long_mk_prod (t :: ts) = mk_times (t, mk_prod ts); 

353 

354 
(*Find first term that matches u*) 

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

356 
 find_first_t past u (t::terms) = 

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

358 
else find_first_t (t::past) u terms 

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

360 

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

362 
val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq 

363 
[@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}]; 

364 

365 
fun cancel_simplify_meta_eq cancel_th ss th = 

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

367 

368 
structure CancelFactorCommon = 

369 
struct 

370 
val mk_sum = (fn T:typ => long_mk_prod) 

371 
val dest_sum = dest_prod 

372 
val mk_coeff = mk_coeff 

373 
val dest_coeff = dest_coeff 

374 
val find_first = find_first_t [] 

375 
val trans_tac = fn _ => trans_tac 

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

379 

380 
structure EqCancelFactor = ExtractCommonTermFun 

381 
(open CancelFactorCommon 

382 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

383 
val mk_bal = HOLogic.mk_eq 

384 
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT 

23471  385 
val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_eq_cancel_disj} 
23164  386 
); 
387 

388 
structure LessCancelFactor = ExtractCommonTermFun 

389 
(open CancelFactorCommon 

390 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

23881  391 
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} 
392 
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT 

23471  393 
val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj} 
23164  394 
); 
395 

396 
structure LeCancelFactor = ExtractCommonTermFun 

397 
(open CancelFactorCommon 

398 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

23881  399 
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} 
400 
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT 

23471  401 
val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj} 
23164  402 
); 
403 

404 
structure DivideCancelFactor = ExtractCommonTermFun 

405 
(open CancelFactorCommon 

406 
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv 

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

408 
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT 

23471  409 
val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj} 
23164  410 
); 
411 

23969  412 
structure DvdCancelFactor = ExtractCommonTermFun 
413 
(open CancelFactorCommon 

414 
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:
25919
diff
changeset

415 
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
25919
diff
changeset

416 
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT 
23969  417 
val simplify_meta_eq = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj} 
418 
); 

419 

23164  420 
val cancel_factor = 
421 
map prep_simproc 

422 
[("nat_eq_cancel_factor", 

423 
["(l::nat) * m = n", "(l::nat) = m * n"], 

424 
K EqCancelFactor.proc), 

425 
("nat_less_cancel_factor", 

426 
["(l::nat) * m < n", "(l::nat) < m * n"], 

427 
K LessCancelFactor.proc), 

428 
("nat_le_cancel_factor", 

429 
["(l::nat) * m <= n", "(l::nat) <= m * n"], 

430 
K LeCancelFactor.proc), 

431 
("nat_divide_cancel_factor", 

432 
["((l::nat) * m) div n", "(l::nat) div (m * n)"], 

23969  433 
K DivideCancelFactor.proc), 
434 
("nat_dvd_cancel_factor", 

435 
["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"], 

436 
K DvdCancelFactor.proc)]; 

23164  437 

438 
end; 

439 

440 

441 
Addsimprocs Nat_Numeral_Simprocs.cancel_numerals; 

442 
Addsimprocs [Nat_Numeral_Simprocs.combine_numerals]; 

443 
Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors; 

444 
Addsimprocs Nat_Numeral_Simprocs.cancel_factor; 

445 

446 

447 
(*examples: 

448 
print_depth 22; 

449 
set timing; 

450 
set trace_simp; 

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

452 

453 
(*cancel_numerals*) 

454 
test "l +( 2) + (2) + 2 + (l + 2) + (oo + 2) = (uu::nat)"; 

455 
test "(2*length xs < 2*length xs + j)"; 

456 
test "(2*length xs < length xs * 2 + j)"; 

457 
test "2*u = (u::nat)"; 

458 
test "2*u = Suc (u)"; 

459 
test "(i + j + 12 + (k::nat))  15 = y"; 

460 
test "(i + j + 12 + (k::nat))  5 = y"; 

461 
test "Suc u  2 = y"; 

462 
test "Suc (Suc (Suc u))  2 = y"; 

463 
test "(i + j + 2 + (k::nat))  1 = y"; 

464 
test "(i + j + 1 + (k::nat))  2 = y"; 

465 

466 
test "(2*x + (u*v) + y)  v*3*u = (w::nat)"; 

467 
test "(2*x*u*v + 5 + (u*v)*4 + y)  v*u*4 = (w::nat)"; 

468 
test "(2*x*u*v + (u*v)*4 + y)  v*u = (w::nat)"; 

469 
test "Suc (Suc (2*x*u*v + u*4 + y))  u = w"; 

470 
test "Suc ((u*v)*4)  v*3*u = w"; 

471 
test "Suc (Suc ((u*v)*3))  v*3*u = w"; 

472 

473 
test "(i + j + 12 + (k::nat)) = u + 15 + y"; 

474 
test "(i + j + 32 + (k::nat))  (u + 15 + y) = zz"; 

475 
test "(i + j + 12 + (k::nat)) = u + 5 + y"; 

476 
(*Suc*) 

477 
test "(i + j + 12 + k) = Suc (u + y)"; 

478 
test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)"; 

479 
test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"; 

480 
test "Suc (Suc (Suc (Suc (Suc (u + y)))))  5 = v"; 

481 
test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"; 

482 
test "2*y + 3*z + 2*u = Suc (u)"; 

483 
test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)"; 

484 
test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::nat)"; 

485 
test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)"; 

486 
test "(2*n*m) < (3*(m*n)) + (u::nat)"; 

487 

488 
test "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0  Suc k => k)))))) <= Suc 0)"; 

489 

490 
test "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) <= length l1"; 

491 

492 
test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) <= length (compT P E A ST mxr e))"; 

493 

494 
test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un \<A> e) ST mxr c))))))) <= length (compT P E A ST mxr e))"; 

495 

496 

497 
(*negative numerals: FAIL*) 

498 
test "(i + j + 23 + (k::nat)) < u + 15 + y"; 

499 
test "(i + j + 3 + (k::nat)) < u + 15 + y"; 

500 
test "(i + j + 12 + (k::nat))  15 = y"; 

501 
test "(i + j + 12 + (k::nat))  15 = y"; 

502 
test "(i + j + 12 + (k::nat))  15 = y"; 

503 

504 
(*combine_numerals*) 

505 
test "k + 3*k = (u::nat)"; 

506 
test "Suc (i + 3) = u"; 

507 
test "Suc (i + j + 3 + k) = u"; 

508 
test "k + j + 3*k + j = (u::nat)"; 

509 
test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)"; 

510 
test "(2*n*m) + (3*(m*n)) = (u::nat)"; 

511 
(*negative numerals: FAIL*) 

512 
test "Suc (i + j + 3 + k) = u"; 

513 

514 
(*cancel_numeral_factors*) 

515 
test "9*x = 12 * (y::nat)"; 

516 
test "(9*x) div (12 * (y::nat)) = z"; 

517 
test "9*x < 12 * (y::nat)"; 

518 
test "9*x <= 12 * (y::nat)"; 

519 

520 
(*cancel_factor*) 

521 
test "x*k = k*(y::nat)"; 

522 
test "k = k*(y::nat)"; 

523 
test "a*(b*c) = (b::nat)"; 

524 
test "a*(b*c) = d*(b::nat)*(x*a)"; 

525 

526 
test "x*k < k*(y::nat)"; 

527 
test "k < k*(y::nat)"; 

528 
test "a*(b*c) < (b::nat)"; 

529 
test "a*(b*c) < d*(b::nat)*(x*a)"; 

530 

531 
test "x*k <= k*(y::nat)"; 

532 
test "k <= k*(y::nat)"; 

533 
test "a*(b*c) <= (b::nat)"; 

534 
test "a*(b*c) <= d*(b::nat)*(x*a)"; 

535 

536 
test "(x*k) div (k*(y::nat)) = (uu::nat)"; 

537 
test "(k) div (k*(y::nat)) = (uu::nat)"; 

538 
test "(a*(b*c)) div ((b::nat)) = (uu::nat)"; 

539 
test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)"; 

540 
*) 

541 

542 

543 
(*** Prepare linear arithmetic for nat numerals ***) 

544 

545 
local 

546 

547 
(* reduce contradictory <= to False *) 

24431
02d29baa42ff
tuned linear arith (once again) with ring_distribs
nipkow
parents:
24093
diff
changeset

548 
val add_rules = @{thms ring_distribs} @ 
23471  549 
[@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1}, 
550 
@{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of}, 

551 
@{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less}, 

552 
@{thm le_Suc_number_of}, @{thm le_number_of_Suc}, 

553 
@{thm less_Suc_number_of}, @{thm less_number_of_Suc}, 

554 
@{thm Suc_eq_number_of}, @{thm eq_number_of_Suc}, 

555 
@{thm mult_Suc}, @{thm mult_Suc_right}, 

24431
02d29baa42ff
tuned linear arith (once again) with ring_distribs
nipkow
parents:
24093
diff
changeset

556 
@{thm add_Suc}, @{thm add_Suc_right}, 
23471  557 
@{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of}, 
558 
@{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}]; 

23164  559 

24431
02d29baa42ff
tuned linear arith (once again) with ring_distribs
nipkow
parents:
24093
diff
changeset

560 
(* Products are multiplied out during proof (re)construction via 
02d29baa42ff
tuned linear arith (once again) with ring_distribs
nipkow
parents:
24093
diff
changeset

561 
ring_distribs. Ideally they should remain atomic. But that is 
02d29baa42ff
tuned linear arith (once again) with ring_distribs
nipkow
parents:
24093
diff
changeset

562 
currently not possible because 1 is replaced by Suc 0, and then some 
02d29baa42ff
tuned linear arith (once again) with ring_distribs
nipkow
parents:
24093
diff
changeset

563 
simprocs start to mess around with products like (n+1)*m. The rule 
02d29baa42ff
tuned linear arith (once again) with ring_distribs
nipkow
parents:
24093
diff
changeset

564 
1 == Suc 0 is necessary for early parts of HOL where numerals and 
02d29baa42ff
tuned linear arith (once again) with ring_distribs
nipkow
parents:
24093
diff
changeset

565 
simprocs are not yet available. But then it is difficult to remove 
02d29baa42ff
tuned linear arith (once again) with ring_distribs
nipkow
parents:
24093
diff
changeset

566 
that rule later on, because it may find its way back in when theories 
02d29baa42ff
tuned linear arith (once again) with ring_distribs
nipkow
parents:
24093
diff
changeset

567 
(and thus linarith simpsets) are merged. Otherwise one could turn the 
02d29baa42ff
tuned linear arith (once again) with ring_distribs
nipkow
parents:
24093
diff
changeset

568 
rule around (Suc n = n+1) and see if that helps products being left 
02d29baa42ff
tuned linear arith (once again) with ring_distribs
nipkow
parents:
24093
diff
changeset

569 
alone. *) 
02d29baa42ff
tuned linear arith (once again) with ring_distribs
nipkow
parents:
24093
diff
changeset

570 

23164  571 
val simprocs = Nat_Numeral_Simprocs.combine_numerals 
572 
:: Nat_Numeral_Simprocs.cancel_numerals; 

573 

574 
in 

575 

576 
val nat_simprocs_setup = 

24093  577 
LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => 
23164  578 
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, 
579 
inj_thms = inj_thms, lessD = lessD, neqE = neqE, 

580 
simpset = simpset addsimps add_rules 

581 
addsimprocs simprocs}); 

582 

583 
end; 