173 instance int :: comm_ring_1 |
173 instance int :: comm_ring_1 |
174 proof |
174 proof |
175 fix i j k :: int |
175 fix i j k :: int |
176 show "(i + j) + k = i + (j + k)" |
176 show "(i + j) + k = i + (j + k)" |
177 unfolding add_int_def |
177 unfolding add_int_def |
178 apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} [@{thm int_equivp}] 1 *}) |
178 apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} 1 *}) |
179 done |
179 done |
180 show "i + j = j + i" |
180 show "i + j = j + i" |
181 unfolding add_int_def |
181 unfolding add_int_def |
182 apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *}) |
182 apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} 1 *}) |
183 done |
183 done |
184 show "0 + i = (i::int)" |
184 show "0 + i = (i::int)" |
185 unfolding add_int_def Zero_int_def |
185 unfolding add_int_def Zero_int_def |
186 apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} [@{thm int_equivp}] 1 *}) |
186 apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} 1 *}) |
187 done |
187 done |
188 show "- i + i = 0" |
188 show "- i + i = 0" |
189 unfolding add_int_def minus_int_def Zero_int_def |
189 unfolding add_int_def minus_int_def Zero_int_def |
190 apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} [@{thm int_equivp}] 1 *}) |
190 apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} 1 *}) |
191 done |
191 done |
192 show "i - j = i + - j" |
192 show "i - j = i + - j" |
193 by (simp add: diff_int_def) |
193 by (simp add: diff_int_def) |
194 show "(i * j) * k = i * (j * k)" |
194 show "(i * j) * k = i * (j * k)" |
195 unfolding mult_int_def |
195 unfolding mult_int_def |
196 apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} [@{thm int_equivp}] 1 *}) |
196 apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} 1 *}) |
197 done |
197 done |
198 show "i * j = j * i" |
198 show "i * j = j * i" |
199 unfolding mult_int_def |
199 unfolding mult_int_def |
200 apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} [@{thm int_equivp}] 1 *}) |
200 apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} 1 *}) |
201 done |
201 done |
202 show "1 * i = i" |
202 show "1 * i = i" |
203 unfolding mult_int_def One_int_def |
203 unfolding mult_int_def One_int_def |
204 apply(tactic {* lift_tac @{context} @{thm mult_one_raw} [@{thm int_equivp}] 1 *}) |
204 apply(tactic {* lift_tac @{context} @{thm mult_one_raw} 1 *}) |
205 done |
205 done |
206 show "(i + j) * k = i * k + j * k" |
206 show "(i + j) * k = i * k + j * k" |
207 unfolding mult_int_def add_int_def |
207 unfolding mult_int_def add_int_def |
208 apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} [@{thm int_equivp}] 1 *}) |
208 apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} 1 *}) |
209 done |
209 done |
210 show "0 \<noteq> (1::int)" |
210 show "0 \<noteq> (1::int)" |
211 unfolding Zero_int_def One_int_def |
211 unfolding Zero_int_def One_int_def |
212 apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} [@{thm int_equivp}] 1 *}) |
212 apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} 1 *}) |
213 done |
213 done |
214 qed |
214 qed |
215 |
215 |
216 term of_nat |
216 term of_nat |
217 thm of_nat_def |
217 thm of_nat_def |
244 instance int :: linorder |
244 instance int :: linorder |
245 proof |
245 proof |
246 fix i j k :: int |
246 fix i j k :: int |
247 show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j" |
247 show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j" |
248 unfolding le_int_def |
248 unfolding le_int_def |
249 apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} [@{thm int_equivp}] 1 *}) |
249 apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} 1 *}) |
250 done |
250 done |
251 show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)" |
251 show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)" |
252 by (auto simp add: less_int_def dest: antisym) |
252 by (auto simp add: less_int_def dest: antisym) |
253 show "i \<le> i" |
253 show "i \<le> i" |
254 unfolding le_int_def |
254 unfolding le_int_def |
255 apply(tactic {* lift_tac @{context} @{thm le_refl_raw} [@{thm int_equivp}] 1 *}) |
255 apply(tactic {* lift_tac @{context} @{thm le_refl_raw} 1 *}) |
256 done |
256 done |
257 show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" |
257 show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" |
258 unfolding le_int_def |
258 unfolding le_int_def |
259 apply(tactic {* lift_tac @{context} @{thm le_trans_raw} [@{thm int_equivp}] 1 *}) |
259 apply(tactic {* lift_tac @{context} @{thm le_trans_raw} 1 *}) |
260 done |
260 done |
261 show "i \<le> j \<or> j \<le> i" |
261 show "i \<le> j \<or> j \<le> i" |
262 unfolding le_int_def |
262 unfolding le_int_def |
263 apply(tactic {* lift_tac @{context} @{thm le_cases_raw} [@{thm int_equivp}] 1 *}) |
263 apply(tactic {* lift_tac @{context} @{thm le_cases_raw} 1 *}) |
264 done |
264 done |
265 qed |
265 qed |
266 |
266 |
267 instantiation int :: distrib_lattice |
267 instantiation int :: distrib_lattice |
268 begin |
268 begin |
287 instance int :: pordered_cancel_ab_semigroup_add |
287 instance int :: pordered_cancel_ab_semigroup_add |
288 proof |
288 proof |
289 fix i j k :: int |
289 fix i j k :: int |
290 show "i \<le> j \<Longrightarrow> k + i \<le> k + j" |
290 show "i \<le> j \<Longrightarrow> k + i \<le> k + j" |
291 unfolding le_int_def add_int_def |
291 unfolding le_int_def add_int_def |
292 apply(tactic {* lift_tac @{context} @{thm le_plus_raw} [@{thm int_equivp}] 1 *}) |
292 apply(tactic {* lift_tac @{context} @{thm le_plus_raw} 1 *}) |
293 done |
293 done |
294 qed |
294 qed |
295 |
295 |
296 lemma test: |
296 lemma test: |
297 "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk> |
297 "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk> |
305 instance int :: ordered_idom |
305 instance int :: ordered_idom |
306 proof |
306 proof |
307 fix i j k :: int |
307 fix i j k :: int |
308 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
308 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
309 unfolding mult_int_def le_int_def less_int_def Zero_int_def |
309 unfolding mult_int_def le_int_def less_int_def Zero_int_def |
310 apply(tactic {* lift_tac @{context} @{thm test} [@{thm int_equivp}] 1 *}) |
310 apply(tactic {* lift_tac @{context} @{thm test} 1 *}) |
311 done |
311 done |
312 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
312 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
313 by (simp only: zabs_def) |
313 by (simp only: zabs_def) |
314 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
314 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
315 by (simp only: zsgn_def) |
315 by (simp only: zsgn_def) |