169 instance int :: comm_ring_1 |
167 instance int :: comm_ring_1 |
170 proof |
168 proof |
171 fix i j k :: int |
169 fix i j k :: int |
172 show "(i + j) + k = i + (j + k)" |
170 show "(i + j) + k = i + (j + k)" |
173 unfolding add_int_def |
171 unfolding add_int_def |
174 apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} 1 *}) |
172 by (lifting plus_assoc_raw) |
175 done |
|
176 show "i + j = j + i" |
173 show "i + j = j + i" |
177 unfolding add_int_def |
174 unfolding add_int_def |
178 apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} 1 *}) |
175 by (lifting plus_sym_raw) |
179 done |
|
180 show "0 + i = (i::int)" |
176 show "0 + i = (i::int)" |
181 unfolding add_int_def Zero_int_def |
177 unfolding add_int_def Zero_int_def |
182 apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} 1 *}) |
178 by (lifting plus_zero_raw) |
183 done |
|
184 show "- i + i = 0" |
179 show "- i + i = 0" |
185 unfolding add_int_def minus_int_def Zero_int_def |
180 unfolding add_int_def minus_int_def Zero_int_def |
186 apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} 1 *}) |
181 by (lifting plus_minus_zero_raw) |
187 done |
|
188 show "i - j = i + - j" |
182 show "i - j = i + - j" |
189 by (simp add: diff_int_def) |
183 by (simp add: diff_int_def) |
190 show "(i * j) * k = i * (j * k)" |
184 show "(i * j) * k = i * (j * k)" |
191 unfolding mult_int_def |
185 unfolding mult_int_def |
192 apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} 1 *}) |
186 by (lifting mult_assoc_raw) |
193 done |
|
194 show "i * j = j * i" |
187 show "i * j = j * i" |
195 unfolding mult_int_def |
188 unfolding mult_int_def |
196 apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} 1 *}) |
189 by (lifting mult_sym_raw) |
197 done |
|
198 show "1 * i = i" |
190 show "1 * i = i" |
199 unfolding mult_int_def One_int_def |
191 unfolding mult_int_def One_int_def |
200 apply(tactic {* lift_tac @{context} @{thm mult_one_raw} 1 *}) |
192 by (lifting mult_one_raw) |
201 done |
|
202 show "(i + j) * k = i * k + j * k" |
193 show "(i + j) * k = i * k + j * k" |
203 unfolding mult_int_def add_int_def |
194 unfolding mult_int_def add_int_def |
204 apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} 1 *}) |
195 by (lifting mult_plus_comm_raw) |
205 done |
|
206 show "0 \<noteq> (1::int)" |
196 show "0 \<noteq> (1::int)" |
207 unfolding Zero_int_def One_int_def |
197 unfolding Zero_int_def One_int_def |
208 apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} 1 *}) |
198 by (lifting one_zero_distinct) |
209 done |
|
210 qed |
199 qed |
211 |
200 |
212 term of_nat |
201 term of_nat |
213 thm of_nat_def |
202 thm of_nat_def |
214 |
203 |
240 instance int :: linorder |
229 instance int :: linorder |
241 proof |
230 proof |
242 fix i j k :: int |
231 fix i j k :: int |
243 show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j" |
232 show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j" |
244 unfolding le_int_def |
233 unfolding le_int_def |
245 apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} 1 *}) |
234 by (lifting le_antisym_raw) |
246 done |
|
247 show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)" |
235 show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)" |
248 by (auto simp add: less_int_def dest: antisym) |
236 by (auto simp add: less_int_def dest: antisym) |
249 show "i \<le> i" |
237 show "i \<le> i" |
250 unfolding le_int_def |
238 unfolding le_int_def |
251 apply(tactic {* lift_tac @{context} @{thm le_refl_raw} 1 *}) |
239 by (lifting le_refl_raw) |
252 done |
|
253 show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" |
240 show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" |
254 unfolding le_int_def |
241 unfolding le_int_def |
255 apply(tactic {* lift_tac @{context} @{thm le_trans_raw} 1 *}) |
242 by (lifting le_trans_raw) |
256 done |
|
257 show "i \<le> j \<or> j \<le> i" |
243 show "i \<le> j \<or> j \<le> i" |
258 unfolding le_int_def |
244 unfolding le_int_def |
259 apply(tactic {* lift_tac @{context} @{thm le_cases_raw} 1 *}) |
245 by (lifting le_cases_raw) |
260 done |
|
261 qed |
246 qed |
262 |
247 |
263 instantiation int :: distrib_lattice |
248 instantiation int :: distrib_lattice |
264 begin |
249 begin |
265 |
250 |
283 instance int :: pordered_cancel_ab_semigroup_add |
268 instance int :: pordered_cancel_ab_semigroup_add |
284 proof |
269 proof |
285 fix i j k :: int |
270 fix i j k :: int |
286 show "i \<le> j \<Longrightarrow> k + i \<le> k + j" |
271 show "i \<le> j \<Longrightarrow> k + i \<le> k + j" |
287 unfolding le_int_def add_int_def |
272 unfolding le_int_def add_int_def |
288 apply(tactic {* lift_tac @{context} @{thm le_plus_raw} 1 *}) |
273 by (lifting le_plus_raw) |
289 done |
|
290 qed |
274 qed |
291 |
275 |
292 lemma test: |
276 lemma test: |
293 "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk> |
277 "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk> |
294 \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> \<not>mult_raw k i \<approx> mult_raw k j" |
278 \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> \<not>mult_raw k i \<approx> mult_raw k j" |
301 instance int :: ordered_idom |
285 instance int :: ordered_idom |
302 proof |
286 proof |
303 fix i j k :: int |
287 fix i j k :: int |
304 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
288 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
305 unfolding mult_int_def le_int_def less_int_def Zero_int_def |
289 unfolding mult_int_def le_int_def less_int_def Zero_int_def |
306 apply(tactic {* lift_tac @{context} @{thm test} 1 *}) |
290 by (lifting test) |
307 done |
|
308 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
291 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
309 by (simp only: zabs_def) |
292 by (simp only: zabs_def) |
310 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
293 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
311 by (simp only: zsgn_def) |
294 by (simp only: zsgn_def) |
312 qed |
295 qed |