author | huffman |
Fri, 21 Oct 2011 08:42:11 +0200 | |
changeset 45224 | b1d5b3820d82 |
child 45270 | d5b5c9259afd |
permissions | -rw-r--r-- |
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
1 |
(* Title: HOL/ex/Simproc_Tests.thy |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
2 |
Author: Brian Huffman |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
3 |
*) |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
4 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
5 |
header {* Testing of arithmetic simprocs *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
6 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
7 |
theory Simproc_Tests |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
8 |
imports Rat |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
9 |
begin |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
10 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
11 |
text {* |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
12 |
This theory tests the various simprocs defined in |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
13 |
@{file "~~/src/HOL/Numeral_Simprocs.thy"}. Many of the tests |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
14 |
are derived from commented-out code originally found in |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
15 |
@{file "~~/src/HOL/Tools/numeral_simprocs.ML"}. |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
16 |
*} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
17 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
18 |
subsection {* ML bindings *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
19 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
20 |
ML {* |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
21 |
val semiring_assoc_fold = Numeral_Simprocs.assoc_fold_simproc |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
22 |
val int_combine_numerals = Numeral_Simprocs.combine_numerals |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
23 |
val field_combine_numerals = Numeral_Simprocs.field_combine_numerals |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
24 |
val [inteq_cancel_numerals, intless_cancel_numerals, intle_cancel_numerals] |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
25 |
= Numeral_Simprocs.cancel_numerals |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
26 |
val [ring_eq_cancel_factor, linordered_ring_le_cancel_factor, |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
27 |
linordered_ring_less_cancel_factor, int_div_cancel_factor, |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
28 |
int_mod_cancel_factor, dvd_cancel_factor, divide_cancel_factor] |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
29 |
= Numeral_Simprocs.cancel_factors |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
30 |
val [ring_eq_cancel_numeral_factor, ring_less_cancel_numeral_factor, |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
31 |
ring_le_cancel_numeral_factor, int_div_cancel_numeral_factors, |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
32 |
divide_cancel_numeral_factor] |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
33 |
= Numeral_Simprocs.cancel_numeral_factors |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
34 |
val field_combine_numerals = Numeral_Simprocs.field_combine_numerals |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
35 |
val [field_eq_cancel_numeral_factor, field_cancel_numeral_factor] |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
36 |
= Numeral_Simprocs.field_cancel_numeral_factors |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
37 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
38 |
fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1) |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
39 |
*} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
40 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
41 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
42 |
subsection {* @{text int_combine_numerals} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
43 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
44 |
lemma assumes "10 + (2 * l + oo) = uu" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
45 |
shows "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
46 |
by (tactic {* test [int_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
47 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
48 |
lemma assumes "-3 + (i + (j + k)) = y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
49 |
shows "(i + j + 12 + (k::int)) - 15 = y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
50 |
by (tactic {* test [int_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
51 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
52 |
lemma assumes "7 + (i + (j + k)) = y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
53 |
shows "(i + j + 12 + (k::int)) - 5 = y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
54 |
by (tactic {* test [int_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
55 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
56 |
lemma assumes "-4 * (u * v) + (2 * x + y) = w" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
57 |
shows "(2*x - (u*v) + y) - v*3*u = (w::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
58 |
by (tactic {* test [int_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
59 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
60 |
lemma assumes "Numeral0 * (u*v) + (2 * x * u * v + y) = w" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
61 |
shows "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
62 |
by (tactic {* test [int_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
63 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
64 |
lemma assumes "3 * (u * v) + (2 * x * u * v + y) = w" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
65 |
shows "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
66 |
by (tactic {* test [int_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
67 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
68 |
lemma assumes "-3 * (u * v) + (- (x * u * v) + - y) = w" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
69 |
shows "u*v - (x*u*v + (u*v)*4 + y) = (w::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
70 |
by (tactic {* test [int_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
71 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
72 |
lemma assumes "Numeral0 * b + (a + - c) = d" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
73 |
shows "a + -(b+c) + b = (d::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
74 |
apply (simp only: minus_add_distrib) |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
75 |
by (tactic {* test [int_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
76 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
77 |
lemma assumes "-2 * b + (a + - c) = d" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
78 |
shows "a + -(b+c) - b = (d::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
79 |
apply (simp only: minus_add_distrib) |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
80 |
by (tactic {* test [int_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
81 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
82 |
lemma assumes "-7 + (i + (j + (k + (- u + - y)))) = zz" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
83 |
shows "(i + j + -2 + (k::int)) - (u + 5 + y) = zz" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
84 |
by (tactic {* test [int_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
85 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
86 |
lemma assumes "-27 + (i + (j + k)) = y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
87 |
shows "(i + j + -12 + (k::int)) - 15 = y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
88 |
by (tactic {* test [int_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
89 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
90 |
lemma assumes "27 + (i + (j + k)) = y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
91 |
shows "(i + j + 12 + (k::int)) - -15 = y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
92 |
by (tactic {* test [int_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
93 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
94 |
lemma assumes "3 + (i + (j + k)) = y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
95 |
shows "(i + j + -12 + (k::int)) - -15 = y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
96 |
by (tactic {* test [int_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
97 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
98 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
99 |
subsection {* @{text inteq_cancel_numerals} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
100 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
101 |
lemma assumes "u = Numeral0" shows "2*u = (u::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
102 |
by (tactic {* test [inteq_cancel_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
103 |
(* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *) |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
104 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
105 |
lemma assumes "i + (j + k) = 3 + (u + y)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
106 |
shows "(i + j + 12 + (k::int)) = u + 15 + y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
107 |
by (tactic {* test [inteq_cancel_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
108 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
109 |
lemma assumes "7 + (j + (i + k)) = y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
110 |
shows "(i + j*2 + 12 + (k::int)) = j + 5 + y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
111 |
by (tactic {* test [inteq_cancel_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
112 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
113 |
lemma assumes "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
114 |
shows "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
115 |
by (tactic {* test [int_combine_numerals, inteq_cancel_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
116 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
117 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
118 |
subsection {* @{text intless_cancel_numerals} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
119 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
120 |
lemma assumes "y < 2 * b" shows "y - b < (b::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
121 |
by (tactic {* test [intless_cancel_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
122 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
123 |
lemma assumes "c + y < 4 * b" shows "y - (3*b + c) < (b::int) - 2*c" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
124 |
by (tactic {* test [intless_cancel_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
125 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
126 |
lemma assumes "i + (j + k) < 8 + (u + y)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
127 |
shows "(i + j + -3 + (k::int)) < u + 5 + y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
128 |
by (tactic {* test [intless_cancel_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
129 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
130 |
lemma assumes "9 + (i + (j + k)) < u + y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
131 |
shows "(i + j + 3 + (k::int)) < u + -6 + y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
132 |
by (tactic {* test [intless_cancel_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
133 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
134 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
135 |
subsection {* @{text ring_eq_cancel_numeral_factor} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
136 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
137 |
lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
138 |
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
139 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
140 |
lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
141 |
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
142 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
143 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
144 |
subsection {* @{text int_div_cancel_numeral_factors} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
145 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
146 |
lemma assumes "(3*x) div (4*y) = z" shows "(9*x) div (12*y) = (z::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
147 |
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
148 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
149 |
lemma assumes "(-3*x) div (4*y) = z" shows "(-99*x) div (132*y) = (z::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
150 |
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
151 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
152 |
lemma assumes "(111*x) div (-44*y) = z" shows "(999*x) div (-396*y) = (z::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
153 |
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
154 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
155 |
lemma assumes "(11*x) div (9*y) = z" shows "(-99*x) div (-81*y) = (z::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
156 |
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
157 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
158 |
lemma assumes "(2*x) div (Numeral1*y) = z" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
159 |
shows "(-2 * x) div (-1 * (y::int)) = z" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
160 |
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
161 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
162 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
163 |
subsection {* @{text ring_less_cancel_numeral_factor} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
164 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
165 |
lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
166 |
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
167 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
168 |
lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
169 |
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
170 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
171 |
lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
172 |
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
173 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
174 |
lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
175 |
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
176 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
177 |
lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
178 |
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
179 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
180 |
lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
181 |
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
182 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
183 |
lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
184 |
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
185 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
186 |
lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
187 |
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
188 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
189 |
lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
190 |
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
191 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
192 |
lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
193 |
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
194 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
195 |
lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
196 |
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
197 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
198 |
lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
199 |
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
200 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
201 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
202 |
subsection {* @{text ring_le_cancel_numeral_factor} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
203 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
204 |
lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
205 |
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
206 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
207 |
lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
208 |
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
209 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
210 |
lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
211 |
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
212 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
213 |
lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
214 |
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
215 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
216 |
lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
217 |
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
218 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
219 |
lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
220 |
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
221 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
222 |
lemma assumes "Numeral1*y \<le> Numeral0" shows "0 \<le> (y::rat) * -2" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
223 |
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
224 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
225 |
lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
226 |
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
227 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
228 |
lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
229 |
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
230 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
231 |
lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
232 |
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
233 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
234 |
lemma assumes "-1*x \<le> Numeral1*y" shows "- ((2::rat) * x) \<le> 2*y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
235 |
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
236 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
237 |
lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
238 |
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
239 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
240 |
lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
241 |
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
242 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
243 |
lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
244 |
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
245 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
246 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
247 |
subsection {* @{text ring_eq_cancel_numeral_factor} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
248 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
249 |
lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
250 |
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
251 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
252 |
lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
253 |
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
254 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
255 |
lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
256 |
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
257 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
258 |
lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
259 |
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
260 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
261 |
lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
262 |
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
263 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
264 |
lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
265 |
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
266 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
267 |
lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
268 |
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
269 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
270 |
lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
271 |
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
272 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
273 |
lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
274 |
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
275 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
276 |
lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
277 |
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
278 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
279 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
280 |
subsection {* @{text field_cancel_numeral_factor} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
281 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
282 |
lemma assumes "(3*x) / (4*y) = z" shows "(9*x) / (12 * (y::rat)) = z" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
283 |
by (tactic {* test [field_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
284 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
285 |
lemma assumes "(-3*x) / (4*y) = z" shows "(-99*x) / (132 * (y::rat)) = z" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
286 |
by (tactic {* test [field_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
287 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
288 |
lemma assumes "(111*x) / (-44*y) = z" shows "(999*x) / (-396 * (y::rat)) = z" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
289 |
by (tactic {* test [field_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
290 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
291 |
lemma assumes "(11*x) / (9*y) = z" shows "(-99*x) / (-81 * (y::rat)) = z" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
292 |
by (tactic {* test [field_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
293 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
294 |
lemma assumes "(2*x) / (Numeral1*y) = z" shows "(-2 * x) / (-1 * (y::rat)) = z" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
295 |
by (tactic {* test [field_cancel_numeral_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
296 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
297 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
298 |
subsection {* @{text ring_eq_cancel_factor} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
299 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
300 |
lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
301 |
by (tactic {* test [ring_eq_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
302 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
303 |
lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
304 |
by (tactic {* test [ring_eq_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
305 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
306 |
lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
307 |
by (tactic {* test [ring_eq_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
308 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
309 |
lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::int)*(x*a)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
310 |
by (tactic {* test [ring_eq_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
311 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
312 |
lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
313 |
by (tactic {* test [ring_eq_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
314 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
315 |
lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
316 |
by (tactic {* test [ring_eq_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
317 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
318 |
lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
319 |
by (tactic {* test [ring_eq_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
320 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
321 |
lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::rat)*(x*a)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
322 |
by (tactic {* test [ring_eq_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
323 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
324 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
325 |
subsection {* @{text int_div_cancel_factor} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
326 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
327 |
lemma assumes "(if k = 0 then 0 else x div y) = uu" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
328 |
shows "(x*k) div (k*(y::int)) = (uu::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
329 |
by (tactic {* test [int_div_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
330 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
331 |
lemma assumes "(if k = 0 then 0 else 1 div y) = uu" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
332 |
shows "(k) div (k*(y::int)) = (uu::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
333 |
by (tactic {* test [int_div_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
334 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
335 |
lemma assumes "(if b = 0 then 0 else a * c) = uu" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
336 |
shows "(a*(b*c)) div ((b::int)) = (uu::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
337 |
by (tactic {* test [int_div_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
338 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
339 |
lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
340 |
shows "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
341 |
by (tactic {* test [int_div_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
342 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
343 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
344 |
subsection {* @{text divide_cancel_factor} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
345 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
346 |
lemma assumes "(if k = 0 then 0 else x / y) = uu" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
347 |
shows "(x*k) / (k*(y::rat)) = (uu::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
348 |
by (tactic {* test [divide_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
349 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
350 |
lemma assumes "(if k = 0 then 0 else 1 / y) = uu" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
351 |
shows "(k) / (k*(y::rat)) = (uu::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
352 |
by (tactic {* test [divide_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
353 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
354 |
lemma assumes "(if b = 0 then 0 else a * c / 1) = uu" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
355 |
shows "(a*(b*c)) / ((b::rat)) = (uu::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
356 |
by (tactic {* test [divide_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
357 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
358 |
lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
359 |
shows "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
360 |
by (tactic {* test [divide_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
361 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
362 |
lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
363 |
oops -- "FIXME: need simproc to cover this case" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
364 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
365 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
366 |
subsection {* @{text linordered_ring_less_cancel_factor} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
367 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
368 |
lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < y*z" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
369 |
by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
370 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
371 |
lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < z*y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
372 |
by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
373 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
374 |
lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < y*z" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
375 |
by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
376 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
377 |
lemma "(0::rat) < z \<Longrightarrow> z*x < z*y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
378 |
apply (tactic {* test [linordered_ring_less_cancel_factor] *})? |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
379 |
oops -- "FIXME: test fails" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
380 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
381 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
382 |
subsection {* @{text linordered_ring_le_cancel_factor} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
383 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
384 |
lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> x*z \<le> y*z" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
385 |
by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
386 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
387 |
lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> z*x \<le> z*y" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
388 |
apply (tactic {* test [linordered_ring_le_cancel_factor] *})? |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
389 |
oops -- "FIXME: test fails" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
390 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
391 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
392 |
subsection {* @{text field_combine_numerals} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
393 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
394 |
lemma assumes "5 / 6 * x = uu" shows "(x::rat) / 2 + x / 3 = uu" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
395 |
by (tactic {* test [field_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
396 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
397 |
lemma assumes "6 / 9 * x + y = uu" shows "(x::rat) / 3 + y + x / 3 = uu" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
398 |
by (tactic {* test [field_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
399 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
400 |
lemma assumes "9 / 9 * x = uu" shows "2 * (x::rat) / 3 + x / 3 = uu" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
401 |
by (tactic {* test [field_combine_numerals] *}) fact |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
402 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
403 |
lemma "2/3 * (x::rat) + x / 3 = uu" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
404 |
apply (tactic {* test [field_combine_numerals] *})? |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
405 |
oops -- "FIXME: test fails" |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
406 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
407 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
408 |
subsection {* @{text field_eq_cancel_numeral_factor} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
409 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
410 |
text {* TODO: tests for @{text field_eq_cancel_numeral_factor} simproc *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
411 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
412 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
413 |
subsection {* @{text field_cancel_numeral_factor} *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
414 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
415 |
text {* TODO: tests for @{text field_cancel_numeral_factor} simproc *} |
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
416 |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset
|
417 |
end |