|
1 (* Title: ZF/ex/integ.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 For integ.thy. The integers as equivalence classes over nat*nat. |
|
7 |
|
8 Could also prove... |
|
9 "znegative(z) ==> $# zmagnitude(z) = $~ z" |
|
10 "~ znegative(z) ==> $# zmagnitude(z) = z" |
|
11 $< is a linear ordering |
|
12 $+ and $* are monotonic wrt $< |
|
13 *) |
|
14 |
|
15 open Integ; |
|
16 |
|
17 val [add_cong] = mk_congs Arith.thy ["op #+"]; |
|
18 |
|
19 (*** Proving that intrel is an equivalence relation ***) |
|
20 |
|
21 val prems = goal Arith.thy |
|
22 "[| m #+ n = m' #+ n'; m: nat; m': nat |] \ |
|
23 \ ==> m #+ (n #+ k) = m' #+ (n' #+ k)"; |
|
24 by (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym] @ prems)) 1); |
|
25 val add_assoc_cong = result(); |
|
26 |
|
27 val prems = goal Arith.thy |
|
28 "[| m: nat; n: nat |] \ |
|
29 \ ==> m #+ (n #+ k) = n #+ (m #+ k)"; |
|
30 by (REPEAT (resolve_tac ([add_commute RS add_assoc_cong] @ prems) 1)); |
|
31 val add_assoc_swap = result(); |
|
32 |
|
33 val add_kill = (refl RS add_cong); |
|
34 val add_assoc_swap_kill = add_kill RSN (3, add_assoc_swap RS trans); |
|
35 |
|
36 (*By luck, requires no typing premises for y1, y2,y3*) |
|
37 val eqa::eqb::prems = goal Arith.thy |
|
38 "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2; \ |
|
39 \ x1: nat; x2: nat; x3: nat |] ==> x1 #+ y3 = x3 #+ y1"; |
|
40 by (res_inst_tac [("k","x2")] add_left_cancel 1); |
|
41 by (resolve_tac prems 1); |
|
42 by (rtac (add_assoc_swap RS trans) 1 THEN typechk_tac prems); |
|
43 by (rtac (eqb RS ssubst) 1); |
|
44 by (rtac (add_assoc_swap RS trans) 1 THEN typechk_tac prems); |
|
45 by (rtac (eqa RS ssubst) 1); |
|
46 by (rtac (add_assoc_swap) 1 THEN typechk_tac prems); |
|
47 val integ_trans_lemma = result(); |
|
48 |
|
49 (** Natural deduction for intrel **) |
|
50 |
|
51 val prems = goalw Integ.thy [intrel_def] |
|
52 "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \ |
|
53 \ <<x1,y1>,<x2,y2>>: intrel"; |
|
54 by (fast_tac (ZF_cs addIs prems) 1); |
|
55 val intrelI = result(); |
|
56 |
|
57 (*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*) |
|
58 goalw Integ.thy [intrel_def] |
|
59 "p: intrel --> (EX x1 y1 x2 y2. \ |
|
60 \ p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \ |
|
61 \ x1: nat & y1: nat & x2: nat & y2: nat)"; |
|
62 by (fast_tac ZF_cs 1); |
|
63 val intrelE_lemma = result(); |
|
64 |
|
65 val [major,minor] = goal Integ.thy |
|
66 "[| p: intrel; \ |
|
67 \ !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>; x1#+y2 = x2#+y1; \ |
|
68 \ x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \ |
|
69 \ ==> Q"; |
|
70 by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1); |
|
71 by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); |
|
72 val intrelE = result(); |
|
73 |
|
74 val intrel_cs = ZF_cs addSIs [intrelI] addSEs [intrelE]; |
|
75 |
|
76 goal Integ.thy |
|
77 "<<x1,y1>,<x2,y2>>: intrel <-> \ |
|
78 \ x1#+y2 = x2#+y1 & x1: nat & y1: nat & x2: nat & y2: nat"; |
|
79 by (fast_tac intrel_cs 1); |
|
80 val intrel_iff = result(); |
|
81 |
|
82 val prems = goalw Integ.thy [equiv_def] "equiv(nat*nat, intrel)"; |
|
83 by (safe_tac intrel_cs); |
|
84 by (rewtac refl_def); |
|
85 by (fast_tac intrel_cs 1); |
|
86 by (rewtac sym_def); |
|
87 by (fast_tac (intrel_cs addSEs [sym]) 1); |
|
88 by (rewtac trans_def); |
|
89 by (fast_tac (intrel_cs addSEs [integ_trans_lemma]) 1); |
|
90 val equiv_intrel = result(); |
|
91 |
|
92 |
|
93 val integ_congs = mk_congs Integ.thy |
|
94 ["znat", "zminus", "znegative", "zmagnitude", "op $+", "op $-", "op $*"]; |
|
95 |
|
96 val intrel_ss0 = arith_ss addcongs integ_congs; |
|
97 |
|
98 val intrel_ss = |
|
99 intrel_ss0 addrews [equiv_intrel RS eq_equiv_class_iff, intrel_iff]; |
|
100 |
|
101 (*More than twice as fast as simplifying with intrel_ss*) |
|
102 fun INTEG_SIMP_TAC ths = |
|
103 let val ss = intrel_ss0 addrews ths |
|
104 in fn i => |
|
105 EVERY [ASM_SIMP_TAC ss i, |
|
106 rtac (intrelI RS (equiv_intrel RS equiv_class_eq)) i, |
|
107 typechk_tac (ZF_typechecks@nat_typechecks@arith_typechecks), |
|
108 ASM_SIMP_TAC ss i] |
|
109 end; |
|
110 |
|
111 |
|
112 (** znat: the injection from nat to integ **) |
|
113 |
|
114 val prems = goalw Integ.thy [integ_def,quotient_def,znat_def] |
|
115 "m : nat ==> $#m : integ"; |
|
116 by (fast_tac (ZF_cs addSIs (nat_0I::prems)) 1); |
|
117 val znat_type = result(); |
|
118 |
|
119 val [major,nnat] = goalw Integ.thy [znat_def] |
|
120 "[| $#m = $#n; n: nat |] ==> m=n"; |
|
121 by (rtac (make_elim (major RS eq_equiv_class)) 1); |
|
122 by (rtac equiv_intrel 1); |
|
123 by (typechk_tac [nat_0I,nnat,SigmaI]); |
|
124 by (safe_tac (intrel_cs addSEs [box_equals,add_0_right])); |
|
125 val znat_inject = result(); |
|
126 |
|
127 |
|
128 (**** zminus: unary negation on integ ****) |
|
129 |
|
130 goalw Integ.thy [congruent_def] |
|
131 "congruent(intrel, split(%x y. intrel``{<y,x>}))"; |
|
132 by (safe_tac intrel_cs); |
|
133 by (ALLGOALS (ASM_SIMP_TAC intrel_ss)); |
|
134 by (etac (box_equals RS sym) 1); |
|
135 by (REPEAT (ares_tac [add_commute] 1)); |
|
136 val zminus_congruent = result(); |
|
137 |
|
138 (*Resolve th against the corresponding facts for zminus*) |
|
139 val zminus_ize = RSLIST [equiv_intrel, zminus_congruent]; |
|
140 |
|
141 val [prem] = goalw Integ.thy [integ_def,zminus_def] |
|
142 "z : integ ==> $~z : integ"; |
|
143 by (typechk_tac [split_type, SigmaI, prem, zminus_ize UN_equiv_class_type, |
|
144 quotientI]); |
|
145 val zminus_type = result(); |
|
146 |
|
147 val major::prems = goalw Integ.thy [integ_def,zminus_def] |
|
148 "[| $~z = $~w; z: integ; w: integ |] ==> z=w"; |
|
149 by (rtac (major RS zminus_ize UN_equiv_class_inject) 1); |
|
150 by (REPEAT (ares_tac prems 1)); |
|
151 by (REPEAT (etac SigmaE 1)); |
|
152 by (etac rev_mp 1); |
|
153 by (ASM_SIMP_TAC ZF_ss 1); |
|
154 by (fast_tac (intrel_cs addSIs [SigmaI, equiv_intrel] |
|
155 addSEs [box_equals RS sym, add_commute, |
|
156 make_elim eq_equiv_class]) 1); |
|
157 val zminus_inject = result(); |
|
158 |
|
159 val prems = goalw Integ.thy [zminus_def] |
|
160 "[| x: nat; y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}"; |
|
161 by (ASM_SIMP_TAC |
|
162 (ZF_ss addrews (prems@[zminus_ize UN_equiv_class, SigmaI])) 1); |
|
163 val zminus = result(); |
|
164 |
|
165 goalw Integ.thy [integ_def] "!!z. z : integ ==> $~ ($~ z) = z"; |
|
166 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
|
167 by (ASM_SIMP_TAC (ZF_ss addrews [zminus] addcongs integ_congs) 1); |
|
168 val zminus_zminus = result(); |
|
169 |
|
170 goalw Integ.thy [integ_def, znat_def] "$~ ($#0) = $#0"; |
|
171 by (SIMP_TAC (arith_ss addrews [zminus]) 1); |
|
172 val zminus_0 = result(); |
|
173 |
|
174 |
|
175 (**** znegative: the test for negative integers ****) |
|
176 |
|
177 goalw Integ.thy [znegative_def, znat_def] |
|
178 "~ znegative($# n)"; |
|
179 by (safe_tac intrel_cs); |
|
180 by (rtac (add_not_less_self RS notE) 1); |
|
181 by (etac ssubst 3); |
|
182 by (ASM_SIMP_TAC (arith_ss addrews [add_0_right]) 3); |
|
183 by (REPEAT (assume_tac 1)); |
|
184 val not_znegative_znat = result(); |
|
185 |
|
186 val [nnat] = goalw Integ.thy [znegative_def, znat_def] |
|
187 "n: nat ==> znegative($~ $# succ(n))"; |
|
188 by (SIMP_TAC (intrel_ss addrews [zminus,nnat]) 1); |
|
189 by (REPEAT |
|
190 (resolve_tac [refl, exI, conjI, naturals_are_ordinals RS Ord_0_mem_succ, |
|
191 refl RS intrelI RS imageI, consI1, nnat, nat_0I, |
|
192 nat_succI] 1)); |
|
193 val znegative_zminus_znat = result(); |
|
194 |
|
195 |
|
196 (**** zmagnitude: magnitide of an integer, as a natural number ****) |
|
197 |
|
198 goalw Integ.thy [congruent_def] |
|
199 "congruent(intrel, split(%x y. (y#-x) #+ (x#-y)))"; |
|
200 by (safe_tac intrel_cs); |
|
201 by (ALLGOALS (ASM_SIMP_TAC intrel_ss)); |
|
202 by (etac rev_mp 1); |
|
203 by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1); |
|
204 by (REPEAT (assume_tac 1)); |
|
205 by (ASM_SIMP_TAC (arith_ss addrews [add_succ_right,succ_inject_iff]) 3); |
|
206 by (ASM_SIMP_TAC |
|
207 (arith_ss addrews [diff_add_inverse,diff_add_0,add_0_right]) 2); |
|
208 by (ASM_SIMP_TAC (arith_ss addrews [add_0_right]) 1); |
|
209 by (rtac impI 1); |
|
210 by (etac subst 1); |
|
211 by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1); |
|
212 by (REPEAT (assume_tac 1)); |
|
213 by (ASM_SIMP_TAC (arith_ss addrews [diff_add_inverse,diff_add_0]) 1); |
|
214 val zmagnitude_congruent = result(); |
|
215 |
|
216 (*Resolve th against the corresponding facts for zmagnitude*) |
|
217 val zmagnitude_ize = RSLIST [equiv_intrel, zmagnitude_congruent]; |
|
218 |
|
219 val [prem] = goalw Integ.thy [integ_def,zmagnitude_def] |
|
220 "z : integ ==> zmagnitude(z) : nat"; |
|
221 by (typechk_tac [split_type, prem, zmagnitude_ize UN_equiv_class_type, |
|
222 add_type, diff_type]); |
|
223 val zmagnitude_type = result(); |
|
224 |
|
225 val prems = goalw Integ.thy [zmagnitude_def] |
|
226 "[| x: nat; y: nat |] ==> \ |
|
227 \ zmagnitude (intrel``{<x,y>}) = (y #- x) #+ (x #- y)"; |
|
228 by (ASM_SIMP_TAC |
|
229 (ZF_ss addrews (prems@[zmagnitude_ize UN_equiv_class, SigmaI])) 1); |
|
230 val zmagnitude = result(); |
|
231 |
|
232 val [nnat] = goalw Integ.thy [znat_def] |
|
233 "n: nat ==> zmagnitude($# n) = n"; |
|
234 by (SIMP_TAC (intrel_ss addrews [zmagnitude,nnat]) 1); |
|
235 val zmagnitude_znat = result(); |
|
236 |
|
237 val [nnat] = goalw Integ.thy [znat_def] |
|
238 "n: nat ==> zmagnitude($~ $# n) = n"; |
|
239 by (SIMP_TAC (intrel_ss addrews [zmagnitude,zminus,nnat,add_0_right]) 1); |
|
240 val zmagnitude_zminus_znat = result(); |
|
241 |
|
242 |
|
243 (**** zadd: addition on integ ****) |
|
244 |
|
245 (** Congruence property for addition **) |
|
246 |
|
247 goalw Integ.thy [congruent2_def] |
|
248 "congruent2(intrel, %p1 p2. \ |
|
249 \ split(%x1 y1. split(%x2 y2. intrel `` {<x1#+x2, y1#+y2>}, p2), p1))"; |
|
250 (*Proof via congruent2_commuteI seems longer*) |
|
251 by (safe_tac intrel_cs); |
|
252 by (INTEG_SIMP_TAC [add_assoc] 1); |
|
253 (*The rest should be trivial, but rearranging terms is hard*) |
|
254 by (res_inst_tac [("m1","x1a")] (add_assoc_swap RS ssubst) 1); |
|
255 by (res_inst_tac [("m1","x2a")] (add_assoc_swap RS ssubst) 3); |
|
256 by (typechk_tac [add_type]); |
|
257 by (ASM_SIMP_TAC (arith_ss addrews [add_assoc RS sym]) 1); |
|
258 val zadd_congruent2 = result(); |
|
259 |
|
260 (*Resolve th against the corresponding facts for zadd*) |
|
261 val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2]; |
|
262 |
|
263 val prems = goalw Integ.thy [integ_def,zadd_def] |
|
264 "[| z: integ; w: integ |] ==> z $+ w : integ"; |
|
265 by (REPEAT (ares_tac (prems@[zadd_ize UN_equiv_class_type2, |
|
266 split_type, add_type, quotientI, SigmaI]) 1)); |
|
267 val zadd_type = result(); |
|
268 |
|
269 val prems = goalw Integ.thy [zadd_def] |
|
270 "[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \ |
|
271 \ (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) = intrel `` {<x1#+x2, y1#+y2>}"; |
|
272 by (ASM_SIMP_TAC (ZF_ss addrews |
|
273 (prems @ [zadd_ize UN_equiv_class2, SigmaI])) 1); |
|
274 val zadd = result(); |
|
275 |
|
276 goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $+ z = z"; |
|
277 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
|
278 by (ASM_SIMP_TAC (arith_ss addrews [zadd]) 1); |
|
279 val zadd_0 = result(); |
|
280 |
|
281 goalw Integ.thy [integ_def] |
|
282 "!!z w. [| z: integ; w: integ |] ==> $~ (z $+ w) = $~ z $+ $~ w"; |
|
283 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
|
284 by (ASM_SIMP_TAC (arith_ss addrews [zminus,zadd] addcongs integ_congs) 1); |
|
285 val zminus_zadd_distrib = result(); |
|
286 |
|
287 goalw Integ.thy [integ_def] |
|
288 "!!z w. [| z: integ; w: integ |] ==> z $+ w = w $+ z"; |
|
289 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
|
290 by (INTEG_SIMP_TAC [zadd] 1); |
|
291 by (REPEAT (ares_tac [add_commute,add_cong] 1)); |
|
292 val zadd_commute = result(); |
|
293 |
|
294 goalw Integ.thy [integ_def] |
|
295 "!!z1 z2 z3. [| z1: integ; z2: integ; z3: integ |] ==> \ |
|
296 \ (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)"; |
|
297 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
|
298 (*rewriting is much faster without intrel_iff, etc.*) |
|
299 by (ASM_SIMP_TAC (intrel_ss0 addrews [zadd,add_assoc]) 1); |
|
300 val zadd_assoc = result(); |
|
301 |
|
302 val prems = goalw Integ.thy [znat_def] |
|
303 "[| m: nat; n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)"; |
|
304 by (ASM_SIMP_TAC (arith_ss addrews (zadd::prems)) 1); |
|
305 val znat_add = result(); |
|
306 |
|
307 goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> z $+ ($~ z) = $#0"; |
|
308 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
|
309 by (ASM_SIMP_TAC (intrel_ss addrews [zminus,zadd,add_0_right]) 1); |
|
310 by (REPEAT (ares_tac [add_commute] 1)); |
|
311 val zadd_zminus_inverse = result(); |
|
312 |
|
313 val prems = goal Integ.thy |
|
314 "z : integ ==> ($~ z) $+ z = $#0"; |
|
315 by (rtac (zadd_commute RS trans) 1); |
|
316 by (REPEAT (resolve_tac (prems@[zminus_type, zadd_zminus_inverse]) 1)); |
|
317 val zadd_zminus_inverse2 = result(); |
|
318 |
|
319 val prems = goal Integ.thy "z:integ ==> z $+ $#0 = z"; |
|
320 by (rtac (zadd_commute RS trans) 1); |
|
321 by (REPEAT (resolve_tac (prems@[znat_type,nat_0I,zadd_0]) 1)); |
|
322 val zadd_0_right = result(); |
|
323 |
|
324 |
|
325 (*Need properties of $- ??? Or use $- just as an abbreviation? |
|
326 [| m: nat; n: nat; m>=n |] ==> $# (m #- n) = ($#m) $- ($#n) |
|
327 *) |
|
328 |
|
329 (**** zmult: multiplication on integ ****) |
|
330 |
|
331 (** Congruence property for multiplication **) |
|
332 |
|
333 val prems = goalw Integ.thy [znat_def] |
|
334 "[| k: nat; l: nat; m: nat; n: nat |] ==> \ |
|
335 \ (k #+ l) #+ (m #+ n) = (k #+ m) #+ (n #+ l)"; |
|
336 val add_commute' = read_instantiate [("m","l")] add_commute; |
|
337 by (SIMP_TAC (arith_ss addrews ([add_commute',add_assoc]@prems)) 1); |
|
338 val zmult_congruent_lemma = result(); |
|
339 |
|
340 goal Integ.thy |
|
341 "congruent2(intrel, %p1 p2. \ |
|
342 \ split(%x1 y1. split(%x2 y2. \ |
|
343 \ intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))"; |
|
344 by (rtac (equiv_intrel RS congruent2_commuteI) 1); |
|
345 by (safe_tac intrel_cs); |
|
346 by (ALLGOALS (INTEG_SIMP_TAC [])); |
|
347 (*Proof that zmult is congruent in one argument*) |
|
348 by (rtac (zmult_congruent_lemma RS trans) 2); |
|
349 by (rtac (zmult_congruent_lemma RS trans RS sym) 6); |
|
350 by (typechk_tac [mult_type]); |
|
351 by (ASM_SIMP_TAC (arith_ss addrews [add_mult_distrib_left RS sym]) 2); |
|
352 (*Proof that zmult is commutative on representatives*) |
|
353 by (rtac add_cong 1); |
|
354 by (rtac (add_commute RS trans) 2); |
|
355 by (REPEAT (ares_tac [mult_commute,add_type,mult_type,add_cong] 1)); |
|
356 val zmult_congruent2 = result(); |
|
357 |
|
358 (*Resolve th against the corresponding facts for zmult*) |
|
359 val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2]; |
|
360 |
|
361 val prems = goalw Integ.thy [integ_def,zmult_def] |
|
362 "[| z: integ; w: integ |] ==> z $* w : integ"; |
|
363 by (REPEAT (ares_tac (prems@[zmult_ize UN_equiv_class_type2, |
|
364 split_type, add_type, mult_type, |
|
365 quotientI, SigmaI]) 1)); |
|
366 val zmult_type = result(); |
|
367 |
|
368 |
|
369 val prems = goalw Integ.thy [zmult_def] |
|
370 "[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \ |
|
371 \ (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) = \ |
|
372 \ intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"; |
|
373 by (ASM_SIMP_TAC (ZF_ss addrews |
|
374 (prems @ [zmult_ize UN_equiv_class2, SigmaI])) 1); |
|
375 val zmult = result(); |
|
376 |
|
377 goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $* z = $#0"; |
|
378 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
|
379 by (ASM_SIMP_TAC (arith_ss addrews [zmult]) 1); |
|
380 val zmult_0 = result(); |
|
381 |
|
382 goalw Integ.thy [integ_def,znat_def,one_def] |
|
383 "!!z. z : integ ==> $#1 $* z = z"; |
|
384 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
|
385 by (ASM_SIMP_TAC (arith_ss addrews [zmult,add_0_right]) 1); |
|
386 val zmult_1 = result(); |
|
387 |
|
388 goalw Integ.thy [integ_def] |
|
389 "!!z w. [| z: integ; w: integ |] ==> ($~ z) $* w = $~ (z $* w)"; |
|
390 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
|
391 by (INTEG_SIMP_TAC [zminus,zmult] 1); |
|
392 by (REPEAT (ares_tac [mult_type,add_commute,add_cong] 1)); |
|
393 val zmult_zminus = result(); |
|
394 |
|
395 goalw Integ.thy [integ_def] |
|
396 "!!z w. [| z: integ; w: integ |] ==> ($~ z) $* ($~ w) = (z $* w)"; |
|
397 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
|
398 by (INTEG_SIMP_TAC [zminus,zmult] 1); |
|
399 by (REPEAT (ares_tac [mult_type,add_commute,add_cong] 1)); |
|
400 val zmult_zminus_zminus = result(); |
|
401 |
|
402 goalw Integ.thy [integ_def] |
|
403 "!!z w. [| z: integ; w: integ |] ==> z $* w = w $* z"; |
|
404 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
|
405 by (INTEG_SIMP_TAC [zmult] 1); |
|
406 by (res_inst_tac [("m1","xc #* y")] (add_commute RS ssubst) 1); |
|
407 by (REPEAT (ares_tac [mult_type,mult_commute,add_cong] 1)); |
|
408 val zmult_commute = result(); |
|
409 |
|
410 goalw Integ.thy [integ_def] |
|
411 "!!z1 z2 z3. [| z1: integ; z2: integ; z3: integ |] ==> \ |
|
412 \ (z1 $* z2) $* z3 = z1 $* (z2 $* z3)"; |
|
413 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
|
414 by (INTEG_SIMP_TAC [zmult, add_mult_distrib_left, |
|
415 add_mult_distrib, add_assoc, mult_assoc] 1); |
|
416 (*takes 54 seconds due to wasteful type-checking*) |
|
417 by (REPEAT (ares_tac [add_type, mult_type, add_commute, add_kill, |
|
418 add_assoc_swap_kill, add_assoc_swap_kill RS sym] 1)); |
|
419 val zmult_assoc = result(); |
|
420 |
|
421 goalw Integ.thy [integ_def] |
|
422 "!!z1 z2 z3. [| z1: integ; z2: integ; w: integ |] ==> \ |
|
423 \ (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)"; |
|
424 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1)); |
|
425 by (INTEG_SIMP_TAC [zadd, zmult, add_mult_distrib, add_assoc] 1); |
|
426 (*takes 30 seconds due to wasteful type-checking*) |
|
427 by (REPEAT (ares_tac [add_type, mult_type, refl, add_commute, add_kill, |
|
428 add_assoc_swap_kill, add_assoc_swap_kill RS sym] 1)); |
|
429 val zadd_zmult_distrib = result(); |
|
430 |
|
431 val integ_typechecks = |
|
432 [znat_type, zminus_type, zmagnitude_type, zadd_type, zmult_type]; |
|
433 |
|
434 val integ_ss = |
|
435 arith_ss addcongs integ_congs |
|
436 addrews ([zminus_zminus,zmagnitude_znat,zmagnitude_zminus_znat, |
|
437 zadd_0] @ integ_typechecks); |