0
|
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);
|