5508
|
1 |
(* Title: IntDef.ML
|
|
2 |
ID: $Id$
|
|
3 |
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
|
6 |
The integers as equivalence classes over nat*nat.
|
|
7 |
*)
|
|
8 |
|
|
9 |
|
|
10 |
(*** Proving that intrel is an equivalence relation ***)
|
|
11 |
|
|
12 |
val eqa::eqb::prems = goal Arith.thy
|
|
13 |
"[| (x1::nat) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] ==> \
|
|
14 |
\ x1 + y3 = x3 + y1";
|
|
15 |
by (res_inst_tac [("k1","x2")] (add_left_cancel RS iffD1) 1);
|
|
16 |
by (rtac (add_left_commute RS trans) 1);
|
|
17 |
by (stac eqb 1);
|
|
18 |
by (rtac (add_left_commute RS trans) 1);
|
|
19 |
by (stac eqa 1);
|
|
20 |
by (rtac (add_left_commute) 1);
|
|
21 |
qed "integ_trans_lemma";
|
|
22 |
|
|
23 |
(** Natural deduction for intrel **)
|
|
24 |
|
|
25 |
Goalw [intrel_def] "[| x1+y2 = x2+y1|] ==> ((x1,y1),(x2,y2)): intrel";
|
|
26 |
by (Fast_tac 1);
|
|
27 |
qed "intrelI";
|
|
28 |
|
|
29 |
(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
|
|
30 |
Goalw [intrel_def]
|
|
31 |
"p: intrel --> (EX x1 y1 x2 y2. \
|
|
32 |
\ p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)";
|
|
33 |
by (Fast_tac 1);
|
|
34 |
qed "intrelE_lemma";
|
|
35 |
|
|
36 |
val [major,minor] = Goal
|
|
37 |
"[| p: intrel; \
|
|
38 |
\ !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2)); x1+y2 = x2+y1|] ==> Q |] \
|
|
39 |
\ ==> Q";
|
|
40 |
by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
|
|
41 |
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
|
|
42 |
qed "intrelE";
|
|
43 |
|
|
44 |
AddSIs [intrelI];
|
|
45 |
AddSEs [intrelE];
|
|
46 |
|
|
47 |
Goal "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
|
|
48 |
by (Fast_tac 1);
|
|
49 |
qed "intrel_iff";
|
|
50 |
|
|
51 |
Goal "(x,x): intrel";
|
|
52 |
by (stac surjective_pairing 1 THEN rtac (refl RS intrelI) 1);
|
|
53 |
qed "intrel_refl";
|
|
54 |
|
|
55 |
Goalw [equiv_def, refl_def, sym_def, trans_def]
|
|
56 |
"equiv {x::(nat*nat).True} intrel";
|
|
57 |
by (fast_tac (claset() addSIs [intrel_refl]
|
|
58 |
addSEs [sym, integ_trans_lemma]) 1);
|
|
59 |
qed "equiv_intrel";
|
|
60 |
|
|
61 |
val equiv_intrel_iff =
|
|
62 |
[TrueI, TrueI] MRS
|
|
63 |
([CollectI, CollectI] MRS
|
|
64 |
(equiv_intrel RS eq_equiv_class_iff));
|
|
65 |
|
|
66 |
Goalw [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
|
|
67 |
by (Fast_tac 1);
|
|
68 |
qed "intrel_in_integ";
|
|
69 |
|
|
70 |
Goal "inj_on Abs_Integ Integ";
|
|
71 |
by (rtac inj_on_inverseI 1);
|
|
72 |
by (etac Abs_Integ_inverse 1);
|
|
73 |
qed "inj_on_Abs_Integ";
|
|
74 |
|
|
75 |
Addsimps [equiv_intrel_iff, inj_on_Abs_Integ RS inj_on_iff,
|
|
76 |
intrel_iff, intrel_in_integ, Abs_Integ_inverse];
|
|
77 |
|
|
78 |
Goal "inj(Rep_Integ)";
|
|
79 |
by (rtac inj_inverseI 1);
|
|
80 |
by (rtac Rep_Integ_inverse 1);
|
|
81 |
qed "inj_Rep_Integ";
|
|
82 |
|
|
83 |
|
|
84 |
(** znat: the injection from nat to Integ **)
|
|
85 |
|
|
86 |
Goal "inj(znat)";
|
|
87 |
by (rtac injI 1);
|
|
88 |
by (rewtac znat_def);
|
|
89 |
by (dtac (inj_on_Abs_Integ RS inj_onD) 1);
|
|
90 |
by (REPEAT (rtac intrel_in_integ 1));
|
|
91 |
by (dtac eq_equiv_class 1);
|
|
92 |
by (rtac equiv_intrel 1);
|
|
93 |
by (Fast_tac 1);
|
|
94 |
by Safe_tac;
|
|
95 |
by (Asm_full_simp_tac 1);
|
|
96 |
qed "inj_znat";
|
|
97 |
|
|
98 |
|
|
99 |
(**** zminus: unary negation on Integ ****)
|
|
100 |
|
|
101 |
Goalw [congruent_def]
|
|
102 |
"congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)";
|
|
103 |
by Safe_tac;
|
|
104 |
by (asm_simp_tac (simpset() addsimps add_ac) 1);
|
|
105 |
qed "zminus_congruent";
|
|
106 |
|
|
107 |
|
|
108 |
(*Resolve th against the corresponding facts for zminus*)
|
|
109 |
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
|
|
110 |
|
|
111 |
Goalw [zminus_def]
|
|
112 |
"- Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})";
|
|
113 |
by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
|
|
114 |
by (simp_tac (simpset() addsimps
|
|
115 |
[intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1);
|
|
116 |
qed "zminus";
|
|
117 |
|
|
118 |
(*by lcp*)
|
|
119 |
val [prem] = Goal "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
|
|
120 |
by (res_inst_tac [("x1","z")]
|
|
121 |
(rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
|
|
122 |
by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
|
|
123 |
by (res_inst_tac [("p","x")] PairE 1);
|
|
124 |
by (rtac prem 1);
|
|
125 |
by (asm_full_simp_tac (simpset() addsimps [Rep_Integ_inverse]) 1);
|
|
126 |
qed "eq_Abs_Integ";
|
|
127 |
|
|
128 |
Goal "- (- z) = (z::int)";
|
|
129 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
|
|
130 |
by (asm_simp_tac (simpset() addsimps [zminus]) 1);
|
|
131 |
qed "zminus_zminus";
|
|
132 |
Addsimps [zminus_zminus];
|
|
133 |
|
|
134 |
Goal "inj(uminus::int=>int)";
|
|
135 |
by (rtac injI 1);
|
|
136 |
by (dres_inst_tac [("f","uminus")] arg_cong 1);
|
|
137 |
by (Asm_full_simp_tac 1);
|
|
138 |
qed "inj_zminus";
|
|
139 |
|
|
140 |
Goalw [znat_def] "- ($# 0) = $# 0";
|
|
141 |
by (simp_tac (simpset() addsimps [zminus]) 1);
|
|
142 |
qed "zminus_nat0";
|
|
143 |
|
|
144 |
Addsimps [zminus_nat0];
|
|
145 |
|
|
146 |
|
|
147 |
(**** znegative: the test for negative integers ****)
|
|
148 |
|
|
149 |
|
|
150 |
Goalw [znegative_def, znat_def] "~ znegative($# n)";
|
|
151 |
by (Simp_tac 1);
|
|
152 |
by Safe_tac;
|
|
153 |
qed "not_znegative_znat";
|
|
154 |
|
|
155 |
Goalw [znegative_def, znat_def] "znegative(- $# Suc(n))";
|
|
156 |
by (simp_tac (simpset() addsimps [zminus]) 1);
|
|
157 |
qed "znegative_zminus_znat";
|
|
158 |
|
|
159 |
Addsimps [znegative_zminus_znat, not_znegative_znat];
|
|
160 |
|
|
161 |
|
|
162 |
(**** zadd: addition on Integ ****)
|
|
163 |
|
|
164 |
(** Congruence property for addition **)
|
|
165 |
|
|
166 |
Goalw [congruent2_def]
|
|
167 |
"congruent2 intrel (%p1 p2. \
|
|
168 |
\ split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)";
|
|
169 |
(*Proof via congruent2_commuteI seems longer*)
|
|
170 |
by Safe_tac;
|
|
171 |
by (asm_simp_tac (simpset() addsimps [add_assoc]) 1);
|
|
172 |
(*The rest should be trivial, but rearranging terms is hard*)
|
|
173 |
by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1);
|
|
174 |
by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
|
|
175 |
qed "zadd_congruent2";
|
|
176 |
|
|
177 |
(*Resolve th against the corresponding facts for zadd*)
|
|
178 |
val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
|
|
179 |
|
|
180 |
Goalw [zadd_def]
|
|
181 |
"Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \
|
|
182 |
\ Abs_Integ(intrel^^{(x1+x2, y1+y2)})";
|
|
183 |
by (asm_simp_tac
|
|
184 |
(simpset() addsimps [zadd_ize UN_equiv_class2]) 1);
|
|
185 |
qed "zadd";
|
|
186 |
|
|
187 |
Goal "- (z + w) = - z + - (w::int)";
|
|
188 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
|
|
189 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
|
|
190 |
by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
|
|
191 |
qed "zminus_zadd_distrib";
|
|
192 |
Addsimps [zminus_zadd_distrib];
|
|
193 |
|
|
194 |
Goal "(z::int) + w = w + z";
|
|
195 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
|
|
196 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
|
|
197 |
by (asm_simp_tac (simpset() addsimps (add_ac @ [zadd])) 1);
|
|
198 |
qed "zadd_commute";
|
|
199 |
|
|
200 |
Goal "((z1::int) + z2) + z3 = z1 + (z2 + z3)";
|
|
201 |
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
|
|
202 |
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
|
|
203 |
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
|
|
204 |
by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
|
|
205 |
qed "zadd_assoc";
|
|
206 |
|
|
207 |
(*For AC rewriting*)
|
|
208 |
Goal "(x::int)+(y+z)=y+(x+z)";
|
|
209 |
by (rtac (zadd_commute RS trans) 1);
|
|
210 |
by (rtac (zadd_assoc RS trans) 1);
|
|
211 |
by (rtac (zadd_commute RS arg_cong) 1);
|
|
212 |
qed "zadd_left_commute";
|
|
213 |
|
|
214 |
(*Integer addition is an AC operator*)
|
|
215 |
val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute];
|
|
216 |
|
|
217 |
Goalw [znat_def] "($#m) + ($#n) = $# (m + n)";
|
|
218 |
by (simp_tac (simpset() addsimps [zadd]) 1);
|
|
219 |
qed "add_znat";
|
|
220 |
|
|
221 |
Goal "$# (Suc m) = $# 1 + ($# m)";
|
|
222 |
by (simp_tac (simpset() addsimps [add_znat]) 1);
|
|
223 |
qed "znat_Suc";
|
|
224 |
|
|
225 |
Goalw [znat_def] "$# 0 + z = z";
|
|
226 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
|
|
227 |
by (asm_simp_tac (simpset() addsimps [zadd]) 1);
|
|
228 |
qed "zadd_nat0";
|
|
229 |
|
|
230 |
Goal "z + $# 0 = z";
|
|
231 |
by (rtac (zadd_commute RS trans) 1);
|
|
232 |
by (rtac zadd_nat0 1);
|
|
233 |
qed "zadd_nat0_right";
|
|
234 |
|
|
235 |
Goalw [znat_def] "z + (- z) = $# 0";
|
|
236 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
|
|
237 |
by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
|
|
238 |
qed "zadd_zminus_inverse_nat";
|
|
239 |
|
|
240 |
Goal "(- z) + z = $# 0";
|
|
241 |
by (rtac (zadd_commute RS trans) 1);
|
|
242 |
by (rtac zadd_zminus_inverse_nat 1);
|
|
243 |
qed "zadd_zminus_inverse_nat2";
|
|
244 |
|
|
245 |
Addsimps [zadd_nat0, zadd_nat0_right,
|
|
246 |
zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2];
|
|
247 |
|
|
248 |
Goal "z + (- z + w) = (w::int)";
|
|
249 |
by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
|
|
250 |
qed "zadd_zminus_cancel";
|
|
251 |
|
|
252 |
Goal "(-z) + (z + w) = (w::int)";
|
|
253 |
by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
|
|
254 |
qed "zminus_zadd_cancel";
|
|
255 |
|
|
256 |
Addsimps [zadd_zminus_cancel, zminus_zadd_cancel];
|
|
257 |
|
|
258 |
|
|
259 |
(** Lemmas **)
|
|
260 |
|
|
261 |
Goal "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
|
|
262 |
by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
|
|
263 |
qed "zadd_assoc_cong";
|
|
264 |
|
|
265 |
Goal "(z::int) + (v + w) = v + (z + w)";
|
|
266 |
by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
|
|
267 |
qed "zadd_assoc_swap";
|
|
268 |
|
|
269 |
|
|
270 |
(*Need properties of subtraction? Or use $- just as an abbreviation!*)
|
|
271 |
|
|
272 |
(**** zmult: multiplication on Integ ****)
|
|
273 |
|
|
274 |
(** Congruence property for multiplication **)
|
|
275 |
|
|
276 |
Goal "((k::nat) + l) + (m + n) = (k + m) + (n + l)";
|
|
277 |
by (simp_tac (simpset() addsimps add_ac) 1);
|
|
278 |
qed "zmult_congruent_lemma";
|
|
279 |
|
|
280 |
Goal "congruent2 intrel (%p1 p2. \
|
|
281 |
\ split (%x1 y1. split (%x2 y2. \
|
|
282 |
\ intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
|
|
283 |
by (rtac (equiv_intrel RS congruent2_commuteI) 1);
|
|
284 |
by (pair_tac "w" 2);
|
|
285 |
by (rename_tac "z1 z2" 2);
|
|
286 |
by Safe_tac;
|
|
287 |
by (rewtac split_def);
|
|
288 |
by (simp_tac (simpset() addsimps add_ac@mult_ac) 1);
|
|
289 |
by (asm_simp_tac (simpset() delsimps [equiv_intrel_iff]
|
|
290 |
addsimps add_ac@mult_ac) 1);
|
|
291 |
by (rtac (intrelI RS(equiv_intrel RS equiv_class_eq)) 1);
|
|
292 |
by (rtac (zmult_congruent_lemma RS trans) 1);
|
|
293 |
by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
|
|
294 |
by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
|
|
295 |
by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
|
|
296 |
by (asm_simp_tac (simpset() addsimps [add_mult_distrib RS sym]) 1);
|
|
297 |
by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
|
|
298 |
qed "zmult_congruent2";
|
|
299 |
|
|
300 |
(*Resolve th against the corresponding facts for zmult*)
|
|
301 |
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
|
|
302 |
|
|
303 |
Goalw [zmult_def]
|
|
304 |
"Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \
|
|
305 |
\ Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
|
|
306 |
by (simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2]) 1);
|
|
307 |
qed "zmult";
|
|
308 |
|
|
309 |
Goal "(- z) * w = - (z * (w::int))";
|
|
310 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
|
|
311 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
|
|
312 |
by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1);
|
|
313 |
qed "zmult_zminus";
|
|
314 |
|
|
315 |
|
|
316 |
Goal "(- z) * (- w) = (z * (w::int))";
|
|
317 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
|
|
318 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
|
|
319 |
by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1);
|
|
320 |
qed "zmult_zminus_zminus";
|
|
321 |
|
|
322 |
Goal "(z::int) * w = w * z";
|
|
323 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
|
|
324 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
|
|
325 |
by (asm_simp_tac (simpset() addsimps ([zmult] @ add_ac @ mult_ac)) 1);
|
|
326 |
qed "zmult_commute";
|
|
327 |
|
|
328 |
Goal "((z1::int) * z2) * z3 = z1 * (z2 * z3)";
|
|
329 |
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
|
|
330 |
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
|
|
331 |
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
|
|
332 |
by (asm_simp_tac (simpset() addsimps ([add_mult_distrib2,zmult] @
|
|
333 |
add_ac @ mult_ac)) 1);
|
|
334 |
qed "zmult_assoc";
|
|
335 |
|
|
336 |
(*For AC rewriting*)
|
|
337 |
Goal "(z1::int)*(z2*z3) = z2*(z1*z3)";
|
|
338 |
by (rtac (zmult_commute RS trans) 1);
|
|
339 |
by (rtac (zmult_assoc RS trans) 1);
|
|
340 |
by (rtac (zmult_commute RS arg_cong) 1);
|
|
341 |
qed "zmult_left_commute";
|
|
342 |
|
|
343 |
(*Integer multiplication is an AC operator*)
|
|
344 |
val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
|
|
345 |
|
|
346 |
Goal "((z1::int) + z2) * w = (z1 * w) + (z2 * w)";
|
|
347 |
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
|
|
348 |
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
|
|
349 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
|
|
350 |
by (asm_simp_tac
|
|
351 |
(simpset() addsimps ([add_mult_distrib2, zadd, zmult] @
|
|
352 |
add_ac @ mult_ac)) 1);
|
|
353 |
qed "zadd_zmult_distrib";
|
|
354 |
|
|
355 |
val zmult_commute'= read_instantiate [("z","w")] zmult_commute;
|
|
356 |
|
|
357 |
Goal "w * (- z) = - (w * (z::int))";
|
|
358 |
by (simp_tac (simpset() addsimps [zmult_commute', zmult_zminus]) 1);
|
|
359 |
qed "zmult_zminus_right";
|
|
360 |
|
|
361 |
Goal "(w::int) * (z1 + z2) = (w * z1) + (w * z2)";
|
|
362 |
by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1);
|
|
363 |
qed "zadd_zmult_distrib2";
|
|
364 |
|
|
365 |
Goalw [znat_def] "$# 0 * z = $# 0";
|
|
366 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
|
|
367 |
by (asm_simp_tac (simpset() addsimps [zmult]) 1);
|
|
368 |
qed "zmult_nat0";
|
|
369 |
|
|
370 |
Goalw [znat_def] "$# 1 * z = z";
|
|
371 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
|
|
372 |
by (asm_simp_tac (simpset() addsimps [zmult]) 1);
|
|
373 |
qed "zmult_nat1";
|
|
374 |
|
|
375 |
Goal "z * $# 0 = $# 0";
|
|
376 |
by (rtac ([zmult_commute, zmult_nat0] MRS trans) 1);
|
|
377 |
qed "zmult_nat0_right";
|
|
378 |
|
|
379 |
Goal "z * $# 1 = z";
|
|
380 |
by (rtac ([zmult_commute, zmult_nat1] MRS trans) 1);
|
|
381 |
qed "zmult_nat1_right";
|
|
382 |
|
|
383 |
Addsimps [zmult_nat0, zmult_nat0_right, zmult_nat1, zmult_nat1_right];
|
|
384 |
|
|
385 |
|
|
386 |
Goal "(- z = w) = (z = - (w::int))";
|
|
387 |
by Safe_tac;
|
|
388 |
by (rtac (zminus_zminus RS sym) 1);
|
|
389 |
by (rtac zminus_zminus 1);
|
|
390 |
qed "zminus_exchange";
|
|
391 |
|
|
392 |
|
|
393 |
(* Theorems about less and less_equal *)
|
|
394 |
|
|
395 |
(*This lemma allows direct proofs of other <-properties*)
|
|
396 |
Goalw [zless_def, znegative_def, zdiff_def, znat_def]
|
|
397 |
"(w < z) = (EX n. z = w + $#(Suc n))";
|
|
398 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
|
|
399 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
|
|
400 |
by (Clarify_tac 1);
|
|
401 |
by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1);
|
|
402 |
by (safe_tac (claset() addSDs [less_eq_Suc_add]));
|
|
403 |
by (res_inst_tac [("x","k")] exI 1);
|
|
404 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
|
|
405 |
qed "zless_iff_Suc_zadd";
|
|
406 |
|
|
407 |
Goal "z < z + $# (Suc n)";
|
|
408 |
by (auto_tac (claset(),
|
|
409 |
simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc,
|
|
410 |
add_znat]));
|
|
411 |
qed "zless_zadd_Suc";
|
|
412 |
|
|
413 |
Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
|
|
414 |
by (auto_tac (claset(),
|
|
415 |
simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc,
|
|
416 |
add_znat]));
|
|
417 |
qed "zless_trans";
|
|
418 |
|
|
419 |
Goal "!!w::int. z<w ==> ~w<z";
|
|
420 |
by (safe_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1]));
|
|
421 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
|
|
422 |
by Safe_tac;
|
|
423 |
by (asm_full_simp_tac (simpset() addsimps ([znat_def, zadd])) 1);
|
|
424 |
qed "zless_not_sym";
|
|
425 |
|
|
426 |
(* [| n<m; ~P ==> m<n |] ==> P *)
|
|
427 |
bind_thm ("zless_asym", (zless_not_sym RS swap));
|
|
428 |
|
|
429 |
Goal "!!z::int. ~ z<z";
|
|
430 |
by (resolve_tac [zless_asym RS notI] 1);
|
|
431 |
by (REPEAT (assume_tac 1));
|
|
432 |
qed "zless_not_refl";
|
|
433 |
|
|
434 |
(* z<z ==> R *)
|
|
435 |
bind_thm ("zless_irrefl", (zless_not_refl RS notE));
|
|
436 |
AddSEs [zless_irrefl];
|
|
437 |
|
|
438 |
Goal "z<w ==> w ~= (z::int)";
|
|
439 |
by (Blast_tac 1);
|
|
440 |
qed "zless_not_refl2";
|
|
441 |
|
|
442 |
(* s < t ==> s ~= t *)
|
|
443 |
bind_thm ("zless_not_refl3", zless_not_refl2 RS not_sym);
|
|
444 |
|
|
445 |
|
|
446 |
(*"Less than" is a linear ordering*)
|
|
447 |
Goalw [zless_def, znegative_def, zdiff_def]
|
|
448 |
"z<w | z=w | w<(z::int)";
|
|
449 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
|
|
450 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
|
|
451 |
by Safe_tac;
|
|
452 |
by (asm_full_simp_tac
|
|
453 |
(simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
|
|
454 |
by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
|
|
455 |
by (auto_tac (claset(), simpset() addsimps add_ac));
|
|
456 |
qed "zless_linear";
|
|
457 |
|
|
458 |
Goal "!!w::int. (w ~= z) = (w<z | z<w)";
|
|
459 |
by (cut_facts_tac [zless_linear] 1);
|
|
460 |
by (Blast_tac 1);
|
|
461 |
qed "int_neq_iff";
|
|
462 |
|
|
463 |
(*** eliminates ~= in premises ***)
|
|
464 |
bind_thm("int_neqE", int_neq_iff RS iffD1 RS disjE);
|
|
465 |
|
|
466 |
Goal "($# m = $# n) = (m = n)";
|
|
467 |
by (fast_tac (claset() addSEs [inj_znat RS injD]) 1);
|
|
468 |
qed "znat_znat_eq";
|
|
469 |
AddIffs [znat_znat_eq];
|
|
470 |
|
|
471 |
Goal "($#m < $#n) = (m<n)";
|
|
472 |
by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd,
|
|
473 |
add_znat]) 1);
|
|
474 |
qed "zless_eq_less";
|
|
475 |
Addsimps [zless_eq_less];
|
|
476 |
|
|
477 |
|
|
478 |
(*** Properties of <= ***)
|
|
479 |
|
|
480 |
Goalw [zle_def, le_def] "($#m <= $#n) = (m<=n)";
|
|
481 |
by (Simp_tac 1);
|
|
482 |
qed "zle_eq_le";
|
|
483 |
Addsimps [zle_eq_le];
|
|
484 |
|
|
485 |
Goalw [zle_def] "~(w<z) ==> z<=(w::int)";
|
|
486 |
by (assume_tac 1);
|
|
487 |
qed "zleI";
|
|
488 |
|
|
489 |
Goalw [zle_def] "z<=w ==> ~(w<(z::int))";
|
|
490 |
by (assume_tac 1);
|
|
491 |
qed "zleD";
|
|
492 |
|
|
493 |
(* [| z <= w; ~ P ==> w < z |] ==> P *)
|
|
494 |
bind_thm ("zleE", zleD RS swap);
|
|
495 |
|
|
496 |
Goalw [zle_def] "(~w<=z) = (z<(w::int))";
|
|
497 |
by (Simp_tac 1);
|
|
498 |
qed "not_zle_iff_zless";
|
|
499 |
|
|
500 |
Goalw [zle_def] "~ z <= w ==> w<(z::int)";
|
|
501 |
by (Fast_tac 1);
|
|
502 |
qed "not_zleE";
|
|
503 |
|
|
504 |
Goalw [zle_def] "z <= w ==> z < w | z=(w::int)";
|
|
505 |
by (cut_facts_tac [zless_linear] 1);
|
|
506 |
by (blast_tac (claset() addEs [zless_asym]) 1);
|
|
507 |
qed "zle_imp_zless_or_eq";
|
|
508 |
|
|
509 |
Goalw [zle_def] "z<w | z=w ==> z <= (w::int)";
|
|
510 |
by (cut_facts_tac [zless_linear] 1);
|
|
511 |
by (blast_tac (claset() addEs [zless_asym]) 1);
|
|
512 |
qed "zless_or_eq_imp_zle";
|
|
513 |
|
|
514 |
Goal "(x <= (y::int)) = (x < y | x=y)";
|
|
515 |
by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1));
|
|
516 |
qed "zle_eq_zless_or_eq";
|
|
517 |
|
|
518 |
Goal "w <= (w::int)";
|
|
519 |
by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1);
|
|
520 |
qed "zle_refl";
|
|
521 |
|
|
522 |
Goalw [zle_def] "z < w ==> z <= (w::int)";
|
|
523 |
by (blast_tac (claset() addEs [zless_asym]) 1);
|
|
524 |
qed "zless_imp_zle";
|
|
525 |
|
|
526 |
Addsimps [zle_refl, zless_imp_zle];
|
|
527 |
|
|
528 |
(* Axiom 'linorder_linear' of class 'linorder': *)
|
|
529 |
Goal "(z::int) <= w | w <= z";
|
|
530 |
by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1);
|
|
531 |
by (cut_facts_tac [zless_linear] 1);
|
|
532 |
by (Blast_tac 1);
|
|
533 |
qed "zle_linear";
|
|
534 |
|
|
535 |
Goal "[| i <= j; j < k |] ==> i < (k::int)";
|
|
536 |
by (dtac zle_imp_zless_or_eq 1);
|
|
537 |
by (blast_tac (claset() addIs [zless_trans]) 1);
|
|
538 |
qed "zle_zless_trans";
|
|
539 |
|
|
540 |
Goal "[| i < j; j <= k |] ==> i < (k::int)";
|
|
541 |
by (dtac zle_imp_zless_or_eq 1);
|
|
542 |
by (blast_tac (claset() addIs [zless_trans]) 1);
|
|
543 |
qed "zless_zle_trans";
|
|
544 |
|
|
545 |
Goal "[| i <= j; j <= k |] ==> i <= (k::int)";
|
|
546 |
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
|
|
547 |
rtac zless_or_eq_imp_zle,
|
|
548 |
blast_tac (claset() addIs [zless_trans])]);
|
|
549 |
qed "zle_trans";
|
|
550 |
|
|
551 |
Goal "[| z <= w; w <= z |] ==> z = (w::int)";
|
|
552 |
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
|
|
553 |
blast_tac (claset() addEs [zless_asym])]);
|
|
554 |
qed "zle_anti_sym";
|
|
555 |
|
|
556 |
(* Axiom 'order_less_le' of class 'order': *)
|
|
557 |
Goal "(w::int) < z = (w <= z & w ~= z)";
|
|
558 |
by (simp_tac (simpset() addsimps [zle_def, int_neq_iff]) 1);
|
|
559 |
by (blast_tac (claset() addSEs [zless_asym]) 1);
|
|
560 |
qed "int_less_le";
|
|
561 |
|
|
562 |
(* [| w <= z; w ~= z |] ==> w < z *)
|
|
563 |
bind_thm ("zle_neq_implies_zless", [int_less_le, conjI] MRS iffD2);
|
|
564 |
|
|
565 |
|
|
566 |
|
|
567 |
(*** Subtraction laws ***)
|
|
568 |
|
|
569 |
Goal "x + (y - z) = (x + y) - (z::int)";
|
|
570 |
by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1);
|
|
571 |
qed "zadd_zdiff_eq";
|
|
572 |
|
|
573 |
Goal "(x - y) + z = (x + z) - (y::int)";
|
|
574 |
by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1);
|
|
575 |
qed "zdiff_zadd_eq";
|
|
576 |
|
|
577 |
Goal "(x - y) - z = x - (y + (z::int))";
|
|
578 |
by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1);
|
|
579 |
qed "zdiff_zdiff_eq";
|
|
580 |
|
|
581 |
Goal "x - (y - z) = (x + z) - (y::int)";
|
|
582 |
by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1);
|
|
583 |
qed "zdiff_zdiff_eq2";
|
|
584 |
|
|
585 |
Goalw [zless_def, zdiff_def] "(x-y < z) = (x < z + (y::int))";
|
|
586 |
by (simp_tac (simpset() addsimps zadd_ac) 1);
|
|
587 |
qed "zdiff_zless_eq";
|
|
588 |
|
|
589 |
Goalw [zless_def, zdiff_def] "(x < z-y) = (x + (y::int) < z)";
|
|
590 |
by (simp_tac (simpset() addsimps zadd_ac) 1);
|
|
591 |
qed "zless_zdiff_eq";
|
|
592 |
|
|
593 |
Goalw [zle_def] "(x-y <= z) = (x <= z + (y::int))";
|
|
594 |
by (simp_tac (simpset() addsimps [zless_zdiff_eq]) 1);
|
|
595 |
qed "zdiff_zle_eq";
|
|
596 |
|
|
597 |
Goalw [zle_def] "(x <= z-y) = (x + (y::int) <= z)";
|
|
598 |
by (simp_tac (simpset() addsimps [zdiff_zless_eq]) 1);
|
|
599 |
qed "zle_zdiff_eq";
|
|
600 |
|
|
601 |
Goalw [zdiff_def] "(x-y = z) = (x = z + (y::int))";
|
|
602 |
by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
|
|
603 |
qed "zdiff_eq_eq";
|
|
604 |
|
|
605 |
Goalw [zdiff_def] "(x = z-y) = (x + (y::int) = z)";
|
|
606 |
by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
|
|
607 |
qed "eq_zdiff_eq";
|
|
608 |
|
|
609 |
(*This list of rewrites simplifies (in)equalities by bringing subtractions
|
|
610 |
to the top and then moving negative terms to the other side.
|
|
611 |
Use with zadd_ac*)
|
|
612 |
val zcompare_rls =
|
|
613 |
[symmetric zdiff_def,
|
|
614 |
zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2,
|
|
615 |
zdiff_zless_eq, zless_zdiff_eq, zdiff_zle_eq, zle_zdiff_eq,
|
|
616 |
zdiff_eq_eq, eq_zdiff_eq];
|
|
617 |
|
|
618 |
|
|
619 |
(** Cancellation laws **)
|
|
620 |
|
|
621 |
Goal "!!w::int. (z + w' = z + w) = (w' = w)";
|
|
622 |
by Safe_tac;
|
|
623 |
by (dres_inst_tac [("f", "%x. x + -z")] arg_cong 1);
|
|
624 |
by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
|
|
625 |
qed "zadd_left_cancel";
|
|
626 |
|
|
627 |
Addsimps [zadd_left_cancel];
|
|
628 |
|
|
629 |
Goal "!!z::int. (w' + z = w + z) = (w' = w)";
|
|
630 |
by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
|
|
631 |
qed "zadd_right_cancel";
|
|
632 |
|
|
633 |
Addsimps [zadd_right_cancel];
|
|
634 |
|
|
635 |
|
|
636 |
Goal "(w < z + $# 1) = (w<z | w=z)";
|
|
637 |
by (auto_tac (claset(),
|
|
638 |
simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc,
|
|
639 |
add_znat]));
|
|
640 |
by (cut_inst_tac [("m","n")] znat_Suc 1);
|
|
641 |
by (exhaust_tac "n" 1);
|
|
642 |
auto();
|
|
643 |
by (full_simp_tac (simpset() addsimps zadd_ac) 1);
|
|
644 |
by (asm_full_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
|
|
645 |
qed "zless_add_nat1_eq";
|
|
646 |
|
|
647 |
|
|
648 |
Goal "(w + $# 1 <= z) = (w<z)";
|
|
649 |
by (simp_tac (simpset() addsimps [zle_def, zless_add_nat1_eq]) 1);
|
|
650 |
by (auto_tac (claset() addIs [zle_anti_sym] addEs [zless_asym],
|
|
651 |
simpset() addsimps [symmetric zle_def]));
|
|
652 |
qed "add_nat1_zle_eq";
|