22 *} |
22 *} |
23 |
23 |
24 |
24 |
25 subsection {* @{text int_combine_numerals} *} |
25 subsection {* @{text int_combine_numerals} *} |
26 |
26 |
27 lemma assumes "10 + (2 * l + oo) = uu" |
27 notepad begin |
28 shows "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)" |
28 fix a b c d oo uu i j k l u v w x y z :: "'a::number_ring" |
29 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
29 { |
30 |
30 assume "10 + (2 * l + oo) = uu" |
31 lemma assumes "-3 + (i + (j + k)) = y" |
31 have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu" |
32 shows "(i + j + 12 + (k::int)) - 15 = y" |
32 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
33 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
33 next |
34 |
34 assume "-3 + (i + (j + k)) = y" |
35 lemma assumes "7 + (i + (j + k)) = y" |
35 have "(i + j + 12 + k) - 15 = y" |
36 shows "(i + j + 12 + (k::int)) - 5 = y" |
36 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
37 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
37 next |
38 |
38 assume "7 + (i + (j + k)) = y" |
39 lemma assumes "-4 * (u * v) + (2 * x + y) = w" |
39 have "(i + j + 12 + k) - 5 = y" |
40 shows "(2*x - (u*v) + y) - v*3*u = (w::int)" |
40 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
41 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
41 next |
42 |
42 assume "-4 * (u * v) + (2 * x + y) = w" |
43 lemma assumes "Numeral0 * (u*v) + (2 * x * u * v + y) = w" |
43 have "(2*x - (u*v) + y) - v*3*u = w" |
44 shows "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)" |
44 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
45 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
45 next |
46 |
46 assume "Numeral0 * (u*v) + (2 * x * u * v + y) = w" |
47 lemma assumes "3 * (u * v) + (2 * x * u * v + y) = w" |
47 have "(2*x*u*v + (u*v)*4 + y) - v*u*4 = w" |
48 shows "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)" |
48 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
49 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
49 next |
50 |
50 assume "3 * (u * v) + (2 * x * u * v + y) = w" |
51 lemma assumes "-3 * (u * v) + (- (x * u * v) + - y) = w" |
51 have "(2*x*u*v + (u*v)*4 + y) - v*u = w" |
52 shows "u*v - (x*u*v + (u*v)*4 + y) = (w::int)" |
52 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
53 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
53 next |
54 |
54 assume "-3 * (u * v) + (- (x * u * v) + - y) = w" |
55 lemma assumes "Numeral0 * b + (a + - c) = d" |
55 have "u*v - (x*u*v + (u*v)*4 + y) = w" |
56 shows "a + -(b+c) + b = (d::int)" |
56 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
57 apply (simp only: minus_add_distrib) |
57 next |
58 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
58 assume "Numeral0 * b + (a + - c) = d" |
59 |
59 have "a + -(b+c) + b = d" |
60 lemma assumes "-2 * b + (a + - c) = d" |
60 apply (simp only: minus_add_distrib) |
61 shows "a + -(b+c) - b = (d::int)" |
61 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
62 apply (simp only: minus_add_distrib) |
62 next |
63 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
63 assume "-2 * b + (a + - c) = d" |
64 |
64 have "a + -(b+c) - b = d" |
65 lemma assumes "-7 + (i + (j + (k + (- u + - y)))) = zz" |
65 apply (simp only: minus_add_distrib) |
66 shows "(i + j + -2 + (k::int)) - (u + 5 + y) = zz" |
66 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
67 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
67 next |
68 |
68 assume "-7 + (i + (j + (k + (- u + - y)))) = z" |
69 lemma assumes "-27 + (i + (j + k)) = y" |
69 have "(i + j + -2 + k) - (u + 5 + y) = z" |
70 shows "(i + j + -12 + (k::int)) - 15 = y" |
70 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
71 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
71 next |
72 |
72 assume "-27 + (i + (j + k)) = y" |
73 lemma assumes "27 + (i + (j + k)) = y" |
73 have "(i + j + -12 + k) - 15 = y" |
74 shows "(i + j + 12 + (k::int)) - -15 = y" |
74 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
75 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
75 next |
76 |
76 assume "27 + (i + (j + k)) = y" |
77 lemma assumes "3 + (i + (j + k)) = y" |
77 have "(i + j + 12 + k) - -15 = y" |
78 shows "(i + j + -12 + (k::int)) - -15 = y" |
78 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
79 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
79 next |
80 |
80 assume "3 + (i + (j + k)) = y" |
|
81 have "(i + j + -12 + k) - -15 = y" |
|
82 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact |
|
83 } |
|
84 end |
81 |
85 |
82 subsection {* @{text inteq_cancel_numerals} *} |
86 subsection {* @{text inteq_cancel_numerals} *} |
83 |
87 |
84 lemma assumes "u = Numeral0" shows "2*u = (u::int)" |
88 notepad begin |
85 by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact |
89 fix i j k u vv w y z w' y' z' :: "'a::number_ring" |
|
90 { |
|
91 assume "u = Numeral0" have "2*u = u" |
|
92 by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact |
86 (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *) |
93 (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *) |
87 |
94 next |
88 lemma assumes "i + (j + k) = 3 + (u + y)" |
95 assume "i + (j + k) = 3 + (u + y)" |
89 shows "(i + j + 12 + (k::int)) = u + 15 + y" |
96 have "(i + j + 12 + k) = u + 15 + y" |
90 by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact |
97 by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact |
91 |
98 next |
92 lemma assumes "7 + (j + (i + k)) = y" |
99 assume "7 + (j + (i + k)) = y" |
93 shows "(i + j*2 + 12 + (k::int)) = j + 5 + y" |
100 have "(i + j*2 + 12 + k) = j + 5 + y" |
94 by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact |
101 by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact |
95 |
102 next |
96 lemma assumes "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))" |
103 assume "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))" |
97 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)" |
104 have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv" |
98 by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact |
105 by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact |
99 |
106 } |
|
107 end |
100 |
108 |
101 subsection {* @{text intless_cancel_numerals} *} |
109 subsection {* @{text intless_cancel_numerals} *} |
102 |
110 |
103 lemma assumes "y < 2 * b" shows "y - b < (b::int)" |
111 notepad begin |
104 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact |
112 fix b c i j k u y :: "'a::{linordered_idom,number_ring}" |
105 |
113 { |
106 lemma assumes "c + y < 4 * b" shows "y - (3*b + c) < (b::int) - 2*c" |
114 assume "y < 2 * b" have "y - b < b" |
107 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact |
115 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact |
108 |
116 next |
109 lemma assumes "i + (j + k) < 8 + (u + y)" |
117 assume "c + y < 4 * b" have "y - (3*b + c) < b - 2*c" |
110 shows "(i + j + -3 + (k::int)) < u + 5 + y" |
118 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact |
111 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact |
119 next |
112 |
120 assume "i + (j + k) < 8 + (u + y)" |
113 lemma assumes "9 + (i + (j + k)) < u + y" |
121 have "(i + j + -3 + k) < u + 5 + y" |
114 shows "(i + j + 3 + (k::int)) < u + -6 + y" |
122 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact |
115 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact |
123 next |
116 |
124 assume "9 + (i + (j + k)) < u + y" |
|
125 have "(i + j + 3 + k) < u + -6 + y" |
|
126 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact |
|
127 } |
|
128 end |
117 |
129 |
118 subsection {* @{text ring_eq_cancel_numeral_factor} *} |
130 subsection {* @{text ring_eq_cancel_numeral_factor} *} |
119 |
131 |
120 lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::int)" |
132 notepad begin |
121 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
133 fix x y :: "'a::{idom,ring_char_0,number_ring}" |
122 |
134 { |
123 lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::int)" |
135 assume "3*x = 4*y" have "9*x = 12 * y" |
124 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
136 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
125 |
137 next |
|
138 assume "-3*x = 4*y" have "-99*x = 132 * y" |
|
139 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
140 next |
|
141 assume "111*x = -44*y" have "999*x = -396 * y" |
|
142 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
143 next |
|
144 assume "11*x = 9*y" have "-99*x = -81 * y" |
|
145 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
146 next |
|
147 assume "2*x = Numeral1*y" have "-2 * x = -1 * y" |
|
148 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
149 next |
|
150 assume "2*x = Numeral1*y" have "-2 * x = -y" |
|
151 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
152 } |
|
153 end |
126 |
154 |
127 subsection {* @{text int_div_cancel_numeral_factors} *} |
155 subsection {* @{text int_div_cancel_numeral_factors} *} |
128 |
156 |
129 lemma assumes "(3*x) div (4*y) = z" shows "(9*x) div (12*y) = (z::int)" |
157 notepad begin |
130 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
158 fix x y z :: "'a::{semiring_div,ring_char_0,number_ring}" |
131 |
159 { |
132 lemma assumes "(-3*x) div (4*y) = z" shows "(-99*x) div (132*y) = (z::int)" |
160 assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z" |
133 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
161 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
134 |
162 next |
135 lemma assumes "(111*x) div (-44*y) = z" shows "(999*x) div (-396*y) = (z::int)" |
163 assume "(-3*x) div (4*y) = z" have "(-99*x) div (132*y) = z" |
136 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
164 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
137 |
165 next |
138 lemma assumes "(11*x) div (9*y) = z" shows "(-99*x) div (-81*y) = (z::int)" |
166 assume "(111*x) div (-44*y) = z" have "(999*x) div (-396*y) = z" |
139 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
167 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
140 |
168 next |
141 lemma assumes "(2*x) div (Numeral1*y) = z" |
169 assume "(11*x) div (9*y) = z" have "(-99*x) div (-81*y) = z" |
142 shows "(-2 * x) div (-1 * (y::int)) = z" |
170 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
143 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
171 next |
144 |
172 assume "(2*x) div (Numeral1*y) = z" |
|
173 have "(-2 * x) div (-1 * y) = z" |
|
174 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact |
|
175 } |
|
176 end |
145 |
177 |
146 subsection {* @{text ring_less_cancel_numeral_factor} *} |
178 subsection {* @{text ring_less_cancel_numeral_factor} *} |
147 |
179 |
148 lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::int)" |
180 notepad begin |
149 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
181 fix x y :: "'a::{linordered_idom,number_ring}" |
150 |
182 { |
151 lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::int)" |
183 assume "3*x < 4*y" have "9*x < 12 * y" |
152 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
184 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
153 |
185 next |
154 lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::int)" |
186 assume "-3*x < 4*y" have "-99*x < 132 * y" |
155 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
187 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
156 |
188 next |
157 lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::int)" |
189 assume "111*x < -44*y" have "999*x < -396 * y" |
158 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
190 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
159 |
191 next |
160 lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::int)" |
192 assume "9*y < 11*x" have "-99*x < -81 * y" |
161 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
193 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
162 |
194 next |
163 lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::int)" |
195 assume "Numeral1*y < 2*x" have "-2 * x < -y" |
164 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
196 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
165 |
197 next |
166 lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::rat)" |
198 assume "23*y < Numeral1*x" have "-x < -23 * y" |
167 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
199 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
168 |
200 } |
169 lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::rat)" |
201 end |
170 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
|
171 |
|
172 lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::rat)" |
|
173 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
|
174 |
|
175 lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::rat)" |
|
176 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
|
177 |
|
178 lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::rat)" |
|
179 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
|
180 |
|
181 lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::rat)" |
|
182 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact |
|
183 |
|
184 |
202 |
185 subsection {* @{text ring_le_cancel_numeral_factor} *} |
203 subsection {* @{text ring_le_cancel_numeral_factor} *} |
186 |
204 |
187 lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::int)" |
205 notepad begin |
188 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
206 fix x y :: "'a::{linordered_idom,number_ring}" |
189 |
207 { |
190 lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::int)" |
208 assume "3*x \<le> 4*y" have "9*x \<le> 12 * y" |
191 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
209 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
192 |
210 next |
193 lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::int)" |
211 assume "-3*x \<le> 4*y" have "-99*x \<le> 132 * y" |
194 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
212 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
195 |
213 next |
196 lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::int)" |
214 assume "111*x \<le> -44*y" have "999*x \<le> -396 * y" |
197 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
215 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
198 |
216 next |
199 lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::int)" |
217 assume "9*y \<le> 11*x" have "-99*x \<le> -81 * y" |
200 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
218 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
201 |
219 next |
202 lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::int)" |
220 assume "Numeral1*y \<le> 2*x" have "-2 * x \<le> -1 * y" |
203 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
221 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
204 |
222 next |
205 lemma assumes "Numeral1*y \<le> Numeral0" shows "0 \<le> (y::rat) * -2" |
223 assume "23*y \<le> Numeral1*x" have "-x \<le> -23 * y" |
206 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
224 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
207 |
225 next |
208 lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::rat)" |
226 assume "Numeral1*y \<le> Numeral0" have "0 \<le> y * -2" |
209 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
227 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
210 |
228 next |
211 lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::rat)" |
229 assume "-1*x \<le> Numeral1*y" have "- (2 * x) \<le> 2*y" |
212 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
230 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
213 |
231 } |
214 lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::rat)" |
232 end |
215 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
|
216 |
|
217 lemma assumes "-1*x \<le> Numeral1*y" shows "- ((2::rat) * x) \<le> 2*y" |
|
218 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
|
219 |
|
220 lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::rat)" |
|
221 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
|
222 |
|
223 lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::rat)" |
|
224 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
|
225 |
|
226 lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::rat)" |
|
227 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact |
|
228 |
|
229 |
|
230 subsection {* @{text ring_eq_cancel_numeral_factor} *} |
|
231 |
|
232 lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::int)" |
|
233 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
234 |
|
235 lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::int)" |
|
236 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
237 |
|
238 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::int)" |
|
239 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
240 |
|
241 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::int)" |
|
242 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
243 |
|
244 lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::rat)" |
|
245 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
246 |
|
247 lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::rat)" |
|
248 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
249 |
|
250 lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::rat)" |
|
251 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
252 |
|
253 lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::rat)" |
|
254 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
255 |
|
256 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::rat)" |
|
257 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
258 |
|
259 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::rat)" |
|
260 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact |
|
261 |
|
262 |
233 |
263 subsection {* @{text divide_cancel_numeral_factor} *} |
234 subsection {* @{text divide_cancel_numeral_factor} *} |
264 |
235 |
265 lemma assumes "(3*x) / (4*y) = z" shows "(9*x) / (12 * (y::rat)) = z" |
236 notepad begin |
266 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
237 fix x y z :: "'a::{field_inverse_zero,ring_char_0,number_ring}" |
267 |
238 { |
268 lemma assumes "(-3*x) / (4*y) = z" shows "(-99*x) / (132 * (y::rat)) = z" |
239 assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z" |
269 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
240 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
270 |
241 next |
271 lemma assumes "(111*x) / (-44*y) = z" shows "(999*x) / (-396 * (y::rat)) = z" |
242 assume "(-3*x) / (4*y) = z" have "(-99*x) / (132 * y) = z" |
272 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
243 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
273 |
244 next |
274 lemma assumes "(11*x) / (9*y) = z" shows "(-99*x) / (-81 * (y::rat)) = z" |
245 assume "(111*x) / (-44*y) = z" have "(999*x) / (-396 * y) = z" |
275 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
246 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
276 |
247 next |
277 lemma assumes "(2*x) / (Numeral1*y) = z" shows "(-2 * x) / (-1 * (y::rat)) = z" |
248 assume "(11*x) / (9*y) = z" have "(-99*x) / (-81 * y) = z" |
278 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
249 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
279 |
250 next |
|
251 assume "(2*x) / (Numeral1*y) = z" have "(-2 * x) / (-1 * y) = z" |
|
252 by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact |
|
253 } |
|
254 end |
280 |
255 |
281 subsection {* @{text ring_eq_cancel_factor} *} |
256 subsection {* @{text ring_eq_cancel_factor} *} |
282 |
257 |
283 lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::int)" |
258 notepad begin |
284 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
259 fix a b c d k x y :: "'a::idom" |
285 |
260 { |
286 lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::int)" |
261 assume "k = 0 \<or> x = y" have "x*k = k*y" |
287 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
262 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
288 |
263 next |
289 lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::int)" |
264 assume "k = 0 \<or> 1 = y" have "k = k*y" |
290 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
265 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
291 |
266 next |
292 lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::int)*(x*a)" |
267 assume "b = 0 \<or> a*c = 1" have "a*(b*c) = b" |
293 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
268 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
294 |
269 next |
295 lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::rat)" |
270 assume "a = 0 \<or> b = 0 \<or> c = d*x" have "a*(b*c) = d*b*(x*a)" |
296 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
271 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
297 |
272 next |
298 lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::rat)" |
273 assume "k = 0 \<or> x = y" have "x*k = k*y" |
299 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
274 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
300 |
275 next |
301 lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::rat)" |
276 assume "k = 0 \<or> 1 = y" have "k = k*y" |
302 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
277 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
303 |
278 } |
304 lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::rat)*(x*a)" |
279 end |
305 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact |
|
306 |
|
307 |
280 |
308 subsection {* @{text int_div_cancel_factor} *} |
281 subsection {* @{text int_div_cancel_factor} *} |
309 |
282 |
310 lemma assumes "(if k = 0 then 0 else x div y) = uu" |
283 notepad begin |
311 shows "(x*k) div (k*(y::int)) = (uu::int)" |
284 fix a b c d k uu x y :: "'a::semiring_div" |
312 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact |
285 { |
313 |
286 assume "(if k = 0 then 0 else x div y) = uu" |
314 lemma assumes "(if k = 0 then 0 else 1 div y) = uu" |
287 have "(x*k) div (k*y) = uu" |
315 shows "(k) div (k*(y::int)) = (uu::int)" |
288 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact |
316 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact |
289 next |
317 |
290 assume "(if k = 0 then 0 else 1 div y) = uu" |
318 lemma assumes "(if b = 0 then 0 else a * c) = uu" |
291 have "(k) div (k*y) = uu" |
319 shows "(a*(b*c)) div ((b::int)) = (uu::int)" |
292 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact |
320 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact |
293 next |
321 |
294 assume "(if b = 0 then 0 else a * c) = uu" |
322 lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" |
295 have "(a*(b*c)) div b = uu" |
323 shows "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)" |
296 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact |
324 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact |
297 next |
325 |
298 assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" |
|
299 have "(a*(b*c)) div (d*b*(x*a)) = uu" |
|
300 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact |
|
301 } |
|
302 end |
326 |
303 |
327 subsection {* @{text divide_cancel_factor} *} |
304 subsection {* @{text divide_cancel_factor} *} |
328 |
305 |
329 lemma assumes "(if k = 0 then 0 else x / y) = uu" |
306 notepad begin |
330 shows "(x*k) / (k*(y::rat)) = (uu::rat)" |
307 fix a b c d k uu x y :: "'a::field_inverse_zero" |
331 by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact |
308 { |
332 |
309 assume "(if k = 0 then 0 else x / y) = uu" |
333 lemma assumes "(if k = 0 then 0 else 1 / y) = uu" |
310 have "(x*k) / (k*y) = uu" |
334 shows "(k) / (k*(y::rat)) = (uu::rat)" |
311 by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact |
335 by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact |
312 next |
336 |
313 assume "(if k = 0 then 0 else 1 / y) = uu" |
337 lemma assumes "(if b = 0 then 0 else a * c / 1) = uu" |
314 have "(k) / (k*y) = uu" |
338 shows "(a*(b*c)) / ((b::rat)) = (uu::rat)" |
315 by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact |
339 by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact |
316 next |
340 |
317 assume "(if b = 0 then 0 else a * c / 1) = uu" |
341 lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu" |
318 have "(a*(b*c)) / b = uu" |
342 shows "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)" |
319 by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact |
343 by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact |
320 next |
|
321 assume "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu" |
|
322 have "(a*(b*c)) / (d*b*(x*a)) = uu" |
|
323 by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact |
|
324 } |
|
325 end |
344 |
326 |
345 lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z" |
327 lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z" |
346 oops -- "FIXME: need simproc to cover this case" |
328 oops -- "FIXME: need simproc to cover this case" |
347 |
329 |
348 |
330 |
349 subsection {* @{text linordered_ring_less_cancel_factor} *} |
331 subsection {* @{text linordered_ring_less_cancel_factor} *} |
350 |
332 |
351 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < y*z" |
333 notepad begin |
352 by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact |
334 fix x y z :: "'a::linordered_idom" |
353 |
335 { |
354 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < z*y" |
336 assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < y*z" |
355 by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact |
337 by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact |
356 |
338 next |
357 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < y*z" |
339 assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < z*y" |
358 by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact |
340 by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact |
359 |
341 next |
360 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < z*y" |
342 assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < y*z" |
361 by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact |
343 by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact |
362 |
344 next |
|
345 assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < z*y" |
|
346 by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact |
|
347 } |
|
348 end |
363 |
349 |
364 subsection {* @{text linordered_ring_le_cancel_factor} *} |
350 subsection {* @{text linordered_ring_le_cancel_factor} *} |
365 |
351 |
366 lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> x*z \<le> y*z" |
352 notepad begin |
367 by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact |
353 fix x y z :: "'a::linordered_idom" |
368 |
354 { |
369 lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> z*x \<le> z*y" |
355 assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> x*z \<le> y*z" |
370 by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact |
356 by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact |
371 |
357 next |
|
358 assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> z*x \<le> z*y" |
|
359 by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact |
|
360 } |
|
361 end |
372 |
362 |
373 subsection {* @{text field_combine_numerals} *} |
363 subsection {* @{text field_combine_numerals} *} |
374 |
364 |
375 lemma assumes "5 / 6 * x = uu" shows "(x::rat) / 2 + x / 3 = uu" |
365 notepad begin |
376 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
366 fix x uu :: "'a::{field_inverse_zero,ring_char_0,number_ring}" |
377 |
367 { |
378 lemma assumes "6 / 9 * x + y = uu" shows "(x::rat) / 3 + y + x / 3 = uu" |
368 assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu" |
379 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
369 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
380 |
370 next |
381 lemma assumes "9 / 9 * x = uu" shows "2 * (x::rat) / 3 + x / 3 = uu" |
371 assume "6 / 9 * x + y = uu" have "x / 3 + y + x / 3 = uu" |
382 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
372 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
|
373 next |
|
374 assume "9 / 9 * x = uu" have "2 * x / 3 + x / 3 = uu" |
|
375 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact |
|
376 } |
|
377 end |
383 |
378 |
384 lemma "2/3 * (x::rat) + x / 3 = uu" |
379 lemma "2/3 * (x::rat) + x / 3 = uu" |
385 apply (tactic {* test [@{simproc field_combine_numerals}] *})? |
380 apply (tactic {* test [@{simproc field_combine_numerals}] *})? |
386 oops -- "FIXME: test fails" |
381 oops -- "FIXME: test fails" |
387 |
382 |