169 instance int :: comm_ring_1 |
169 instance int :: comm_ring_1 |
170 proof |
170 proof |
171 fix i j k :: int |
171 fix i j k :: int |
172 show "(i + j) + k = i + (j + k)" |
172 show "(i + j) + k = i + (j + k)" |
173 unfolding add_int_def |
173 unfolding add_int_def |
174 apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} [@{thm int_equivp}] 1 *}) |
174 apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} 1 *}) |
175 done |
175 done |
176 show "i + j = j + i" |
176 show "i + j = j + i" |
177 unfolding add_int_def |
177 unfolding add_int_def |
178 apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *}) |
178 apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} 1 *}) |
179 done |
179 done |
180 show "0 + i = (i::int)" |
180 show "0 + i = (i::int)" |
181 unfolding add_int_def Zero_int_def |
181 unfolding add_int_def Zero_int_def |
182 apply(tactic {* procedure_tac @{context} @{thm plus_zero_raw} 1 *}) |
182 apply(tactic {* procedure_tac @{context} @{thm plus_zero_raw} 1 *}) |
183 apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) |
183 apply(tactic {* regularize_tac @{context} 1 *}) |
184 apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
184 apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
185 defer |
185 defer |
186 apply(tactic {* clean_tac @{context} 1*}) |
186 apply(tactic {* clean_tac @{context} 1*}) |
187 sorry |
187 sorry |
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 {* procedure_tac @{context} @{thm plus_minus_zero_raw} 1 *}) |
190 apply(tactic {* procedure_tac @{context} @{thm plus_minus_zero_raw} 1 *}) |
191 apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) |
191 apply(tactic {* regularize_tac @{context} 1 *}) |
192 apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
192 apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
193 defer |
193 defer |
194 apply(tactic {* clean_tac @{context} 1*}) |
194 apply(tactic {* clean_tac @{context} 1*}) |
195 sorry |
195 sorry |
196 show "i - j = i + - j" |
196 show "i - j = i + - j" |
197 by (simp add: diff_int_def) |
197 by (simp add: diff_int_def) |
198 show "(i * j) * k = i * (j * k)" |
198 show "(i * j) * k = i * (j * k)" |
199 unfolding mult_int_def |
199 unfolding mult_int_def |
200 apply(tactic {* procedure_tac @{context} @{thm mult_assoc_raw} 1 *}) |
200 apply(tactic {* procedure_tac @{context} @{thm mult_assoc_raw} 1 *}) |
201 apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) |
201 apply(tactic {* regularize_tac @{context} 1 *}) |
202 apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
202 apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
203 defer |
203 defer |
204 apply(tactic {* clean_tac @{context} 1*}) |
204 apply(tactic {* clean_tac @{context} 1*}) |
205 sorry |
205 sorry |
206 show "i * j = j * i" |
206 show "i * j = j * i" |
207 unfolding mult_int_def |
207 unfolding mult_int_def |
208 apply(tactic {* procedure_tac @{context} @{thm mult_sym_raw} 1 *}) |
208 apply(tactic {* procedure_tac @{context} @{thm mult_sym_raw} 1 *}) |
209 apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) |
209 apply(tactic {* regularize_tac @{context} 1 *}) |
210 apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
210 apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
211 defer |
211 defer |
212 apply(tactic {* clean_tac @{context} 1*}) |
212 apply(tactic {* clean_tac @{context} 1*}) |
213 sorry |
213 sorry |
214 show "1 * i = i" |
214 show "1 * i = i" |
215 unfolding mult_int_def One_int_def |
215 unfolding mult_int_def One_int_def |
216 apply(tactic {* procedure_tac @{context} @{thm mult_one_raw} 1 *}) |
216 apply(tactic {* procedure_tac @{context} @{thm mult_one_raw} 1 *}) |
217 apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) |
217 apply(tactic {* regularize_tac @{context} 1 *}) |
218 apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
218 apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
219 defer |
219 defer |
220 apply(tactic {* clean_tac @{context} 1*}) |
220 apply(tactic {* clean_tac @{context} 1*}) |
221 sorry |
221 sorry |
222 show "(i + j) * k = i * k + j * k" |
222 show "(i + j) * k = i * k + j * k" |
223 unfolding mult_int_def add_int_def |
223 unfolding mult_int_def add_int_def |
224 apply(tactic {* procedure_tac @{context} @{thm mult_plus_comm_raw} 1 *}) |
224 apply(tactic {* procedure_tac @{context} @{thm mult_plus_comm_raw} 1 *}) |
225 apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *}) |
225 apply(tactic {* regularize_tac @{context} 1 *}) |
226 apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
226 apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
227 defer |
227 defer |
228 apply(tactic {* clean_tac @{context} 1*}) |
228 apply(tactic {* clean_tac @{context} 1*}) |
229 sorry |
229 sorry |
230 show "0 \<noteq> (1::int)" |
230 show "0 \<noteq> (1::int)" |
267 instance int :: linorder |
267 instance int :: linorder |
268 proof |
268 proof |
269 fix i j k :: int |
269 fix i j k :: int |
270 show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j" |
270 show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j" |
271 unfolding le_int_def |
271 unfolding le_int_def |
272 apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} [@{thm int_equivp}] 1 *}) |
272 apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} 1 *}) |
273 done |
273 done |
274 show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)" |
274 show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)" |
275 by (auto simp add: less_int_def dest: antisym) |
275 by (auto simp add: less_int_def dest: antisym) |
276 show "i \<le> i" |
276 show "i \<le> i" |
277 unfolding le_int_def |
277 unfolding le_int_def |
278 apply(tactic {* lift_tac @{context} @{thm le_refl_raw} [@{thm int_equivp}] 1 *}) |
278 apply(tactic {* lift_tac @{context} @{thm le_refl_raw} 1 *}) |
279 done |
279 done |
280 show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" |
280 show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" |
281 unfolding le_int_def |
281 unfolding le_int_def |
282 apply(tactic {* lift_tac @{context} @{thm le_trans_raw} [@{thm int_equivp}] 1 *}) |
282 apply(tactic {* lift_tac @{context} @{thm le_trans_raw} 1 *}) |
283 done |
283 done |
284 show "i \<le> j \<or> j \<le> i" |
284 show "i \<le> j \<or> j \<le> i" |
285 unfolding le_int_def |
285 unfolding le_int_def |
286 apply(tactic {* lift_tac @{context} @{thm le_cases_raw} [@{thm int_equivp}] 1 *}) |
286 apply(tactic {* lift_tac @{context} @{thm le_cases_raw} 1 *}) |
287 done |
287 done |
288 qed |
288 qed |
289 |
289 |
290 instantiation int :: distrib_lattice |
290 instantiation int :: distrib_lattice |
291 begin |
291 begin |