equal
deleted
inserted
replaced
8 |
8 |
9 theory BinEx imports Main begin |
9 theory BinEx imports Main begin |
10 |
10 |
11 subsection {* Regression Testing for Cancellation Simprocs *} |
11 subsection {* Regression Testing for Cancellation Simprocs *} |
12 |
12 |
13 (*taken from HOL/Integ/int_arith1.ML *) |
|
14 |
|
15 |
|
16 lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)" |
13 lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)" |
17 apply simp oops |
14 apply simp oops |
18 |
15 |
19 lemma "2*u = (u::int)" |
16 lemma "2*u = (u::int)" |
20 apply simp oops |
17 apply simp oops |
281 |
278 |
282 text {* Successor *} |
279 text {* Successor *} |
283 |
280 |
284 lemma "Suc 99999 = 100000" |
281 lemma "Suc 99999 = 100000" |
285 by (simp add: Suc_nat_number_of) |
282 by (simp add: Suc_nat_number_of) |
286 -- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *} |
283 -- {* not a default rewrite since sometimes we want to have @{text "Suc nnn"} *} |
287 |
284 |
288 |
285 |
289 text {* \medskip Addition *} |
286 text {* \medskip Addition *} |
290 |
287 |
291 lemma "(13::nat) + 19 = 32" |
288 lemma "(13::nat) + 19 = 32" |
388 by simp |
385 by simp |
389 |
386 |
390 lemma "x + y - x + z - x - y - z + x < (1::int)" |
387 lemma "x + y - x + z - x - y - z + x < (1::int)" |
391 by simp |
388 by simp |
392 |
389 |
393 |
|
394 text{*The proofs about arithmetic yielding normal forms have been deleted: |
|
395 they are irrelevant with the new treatment of numerals.*} |
|
396 |
|
397 end |
390 end |