author | paulson |
Fri, 27 Aug 1999 15:42:10 +0200 | |
changeset 7375 | 2cb340e66d15 |
parent 7127 | 48e235179ffb |
child 7428 | 80838c2af97b |
permissions | -rw-r--r-- |
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] |
|
7375
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
56 |
"equiv UNIV intrel"; |
5508 | 57 |
by (fast_tac (claset() addSIs [intrel_refl] |
7375
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
58 |
addSEs [sym, integ_trans_lemma]) 1); |
5508 | 59 |
qed "equiv_intrel"; |
60 |
||
7375
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
61 |
val equiv_intrel_iff = [equiv_intrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff; |
5508 | 62 |
|
63 |
Goalw [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ"; |
|
64 |
by (Fast_tac 1); |
|
65 |
qed "intrel_in_integ"; |
|
66 |
||
67 |
Goal "inj_on Abs_Integ Integ"; |
|
68 |
by (rtac inj_on_inverseI 1); |
|
69 |
by (etac Abs_Integ_inverse 1); |
|
70 |
qed "inj_on_Abs_Integ"; |
|
71 |
||
72 |
Addsimps [equiv_intrel_iff, inj_on_Abs_Integ RS inj_on_iff, |
|
73 |
intrel_iff, intrel_in_integ, Abs_Integ_inverse]; |
|
74 |
||
75 |
Goal "inj(Rep_Integ)"; |
|
76 |
by (rtac inj_inverseI 1); |
|
77 |
by (rtac Rep_Integ_inverse 1); |
|
78 |
qed "inj_Rep_Integ"; |
|
79 |
||
80 |
||
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5540
diff
changeset
|
81 |
(** int: the injection from "nat" to "int" **) |
5508 | 82 |
|
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5540
diff
changeset
|
83 |
Goal "inj int"; |
5508 | 84 |
by (rtac injI 1); |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5540
diff
changeset
|
85 |
by (rewtac int_def); |
5508 | 86 |
by (dtac (inj_on_Abs_Integ RS inj_onD) 1); |
87 |
by (REPEAT (rtac intrel_in_integ 1)); |
|
88 |
by (dtac eq_equiv_class 1); |
|
89 |
by (rtac equiv_intrel 1); |
|
90 |
by (Fast_tac 1); |
|
91 |
by Safe_tac; |
|
92 |
by (Asm_full_simp_tac 1); |
|
6991 | 93 |
qed "inj_int"; |
5508 | 94 |
|
95 |
||
96 |
(**** zminus: unary negation on Integ ****) |
|
97 |
||
7375
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
98 |
Goalw [congruent_def] "congruent intrel (%(x,y). intrel^^{(y,x)})"; |
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
99 |
by (Clarify_tac 1); |
5508 | 100 |
by (asm_simp_tac (simpset() addsimps add_ac) 1); |
101 |
qed "zminus_congruent"; |
|
102 |
||
103 |
Goalw [zminus_def] |
|
104 |
"- Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})"; |
|
105 |
by (simp_tac (simpset() addsimps |
|
7375
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
106 |
[equiv_intrel RS UN_equiv_class, zminus_congruent]) 1); |
5508 | 107 |
qed "zminus"; |
108 |
||
7375
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
109 |
(*Every integer can be written in the form Abs_Integ(...) *) |
5508 | 110 |
val [prem] = Goal "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P"; |
111 |
by (res_inst_tac [("x1","z")] |
|
112 |
(rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1); |
|
113 |
by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1); |
|
114 |
by (res_inst_tac [("p","x")] PairE 1); |
|
115 |
by (rtac prem 1); |
|
116 |
by (asm_full_simp_tac (simpset() addsimps [Rep_Integ_inverse]) 1); |
|
117 |
qed "eq_Abs_Integ"; |
|
118 |
||
119 |
Goal "- (- z) = (z::int)"; |
|
120 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
|
121 |
by (asm_simp_tac (simpset() addsimps [zminus]) 1); |
|
122 |
qed "zminus_zminus"; |
|
123 |
Addsimps [zminus_zminus]; |
|
124 |
||
5594 | 125 |
Goal "inj(%z::int. -z)"; |
5508 | 126 |
by (rtac injI 1); |
127 |
by (dres_inst_tac [("f","uminus")] arg_cong 1); |
|
128 |
by (Asm_full_simp_tac 1); |
|
129 |
qed "inj_zminus"; |
|
130 |
||
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
131 |
Goalw [int_def] "- (int 0) = int 0"; |
5508 | 132 |
by (simp_tac (simpset() addsimps [zminus]) 1); |
6917 | 133 |
qed "zminus_int0"; |
5508 | 134 |
|
6917 | 135 |
Addsimps [zminus_int0]; |
5508 | 136 |
|
137 |
||
5540 | 138 |
(**** neg: the test for negative integers ****) |
5508 | 139 |
|
140 |
||
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
141 |
Goalw [neg_def, int_def] "~ neg(int n)"; |
5508 | 142 |
by (Simp_tac 1); |
7010
63120b6dca50
more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents:
6991
diff
changeset
|
143 |
qed "not_neg_int"; |
5508 | 144 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
145 |
Goalw [neg_def, int_def] "neg(- (int (Suc n)))"; |
5508 | 146 |
by (simp_tac (simpset() addsimps [zminus]) 1); |
7010
63120b6dca50
more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents:
6991
diff
changeset
|
147 |
qed "neg_zminus_int"; |
5508 | 148 |
|
7010
63120b6dca50
more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents:
6991
diff
changeset
|
149 |
Addsimps [neg_zminus_int, not_neg_int]; |
5508 | 150 |
|
151 |
||
152 |
(**** zadd: addition on Integ ****) |
|
153 |
||
154 |
Goalw [zadd_def] |
|
155 |
"Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \ |
|
156 |
\ Abs_Integ(intrel^^{(x1+x2, y1+y2)})"; |
|
7375
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
157 |
by (asm_simp_tac (simpset() addsimps [UN_UN_split_split_eq]) 1); |
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
158 |
by (stac (equiv_intrel RS UN_equiv_class2) 1); |
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
159 |
(*Congruence property for addition*) |
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
160 |
by (auto_tac (claset(), simpset() addsimps [congruent2_def])); |
5508 | 161 |
qed "zadd"; |
162 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7010
diff
changeset
|
163 |
Goal "- (z + w) = (- z) + (- w::int)"; |
5508 | 164 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
165 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
|
166 |
by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1); |
|
167 |
qed "zminus_zadd_distrib"; |
|
168 |
Addsimps [zminus_zadd_distrib]; |
|
169 |
||
170 |
Goal "(z::int) + w = w + z"; |
|
171 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
|
172 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
|
5540 | 173 |
by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1); |
5508 | 174 |
qed "zadd_commute"; |
175 |
||
176 |
Goal "((z1::int) + z2) + z3 = z1 + (z2 + z3)"; |
|
177 |
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); |
|
178 |
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); |
|
179 |
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); |
|
180 |
by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1); |
|
181 |
qed "zadd_assoc"; |
|
182 |
||
183 |
(*For AC rewriting*) |
|
184 |
Goal "(x::int)+(y+z)=y+(x+z)"; |
|
185 |
by (rtac (zadd_commute RS trans) 1); |
|
186 |
by (rtac (zadd_assoc RS trans) 1); |
|
187 |
by (rtac (zadd_commute RS arg_cong) 1); |
|
188 |
qed "zadd_left_commute"; |
|
189 |
||
190 |
(*Integer addition is an AC operator*) |
|
191 |
val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute]; |
|
192 |
||
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
193 |
Goalw [int_def] "(int m) + (int n) = int (m + n)"; |
5508 | 194 |
by (simp_tac (simpset() addsimps [zadd]) 1); |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
195 |
qed "zadd_int"; |
5508 | 196 |
|
5594 | 197 |
Goal "(int m) + (int n + z) = int (m + n) + z"; |
198 |
by (simp_tac (simpset() addsimps [zadd_int, zadd_assoc RS sym]) 1); |
|
199 |
qed "zadd_int_left"; |
|
200 |
||
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
201 |
Goal "int (Suc m) = int 1 + (int m)"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
202 |
by (simp_tac (simpset() addsimps [zadd_int]) 1); |
6717
70b251dc7055
int_Suc->int_Suc_int_1 avoiding confusion with the more useful Bin.int_Suc
paulson
parents:
6674
diff
changeset
|
203 |
qed "int_Suc_int_1"; |
5508 | 204 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
205 |
Goalw [int_def] "int 0 + z = z"; |
5508 | 206 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
207 |
by (asm_simp_tac (simpset() addsimps [zadd]) 1); |
|
6917 | 208 |
qed "zadd_int0"; |
5508 | 209 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
210 |
Goal "z + int 0 = z"; |
5508 | 211 |
by (rtac (zadd_commute RS trans) 1); |
6917 | 212 |
by (rtac zadd_int0 1); |
213 |
qed "zadd_int0_right"; |
|
5508 | 214 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
215 |
Goalw [int_def] "z + (- z) = int 0"; |
5508 | 216 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
217 |
by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1); |
|
5594 | 218 |
qed "zadd_zminus_inverse"; |
5508 | 219 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
220 |
Goal "(- z) + z = int 0"; |
5508 | 221 |
by (rtac (zadd_commute RS trans) 1); |
5594 | 222 |
by (rtac zadd_zminus_inverse 1); |
223 |
qed "zadd_zminus_inverse2"; |
|
5508 | 224 |
|
6917 | 225 |
Addsimps [zadd_int0, zadd_int0_right, |
5594 | 226 |
zadd_zminus_inverse, zadd_zminus_inverse2]; |
5508 | 227 |
|
228 |
Goal "z + (- z + w) = (w::int)"; |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
229 |
by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); |
5508 | 230 |
qed "zadd_zminus_cancel"; |
231 |
||
232 |
Goal "(-z) + (z + w) = (w::int)"; |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
233 |
by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); |
5508 | 234 |
qed "zminus_zadd_cancel"; |
235 |
||
236 |
Addsimps [zadd_zminus_cancel, zminus_zadd_cancel]; |
|
237 |
||
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
238 |
Goal "int 0 - x = -x"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
239 |
by (simp_tac (simpset() addsimps [zdiff_def]) 1); |
6917 | 240 |
qed "zdiff_int0"; |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
241 |
|
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
242 |
Goal "x - int 0 = x"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
243 |
by (simp_tac (simpset() addsimps [zdiff_def]) 1); |
6917 | 244 |
qed "zdiff_int0_right"; |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
245 |
|
5594 | 246 |
Goal "x - x = int 0"; |
247 |
by (simp_tac (simpset() addsimps [zdiff_def]) 1); |
|
248 |
qed "zdiff_self"; |
|
249 |
||
6917 | 250 |
Addsimps [zdiff_int0, zdiff_int0_right, zdiff_self]; |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
251 |
|
5508 | 252 |
|
253 |
(** Lemmas **) |
|
254 |
||
255 |
Goal "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"; |
|
256 |
by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); |
|
257 |
qed "zadd_assoc_cong"; |
|
258 |
||
259 |
Goal "(z::int) + (v + w) = v + (z + w)"; |
|
260 |
by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1)); |
|
261 |
qed "zadd_assoc_swap"; |
|
262 |
||
263 |
||
264 |
(*Need properties of subtraction? Or use $- just as an abbreviation!*) |
|
265 |
||
266 |
(**** zmult: multiplication on Integ ****) |
|
267 |
||
268 |
Goal "((k::nat) + l) + (m + n) = (k + m) + (n + l)"; |
|
269 |
by (simp_tac (simpset() addsimps add_ac) 1); |
|
270 |
qed "zmult_congruent_lemma"; |
|
271 |
||
7375
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
272 |
(*Congruence property for multiplication*) |
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
273 |
Goal "congruent2 intrel \ |
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
274 |
\ (%p1 p2. (%(x1,y1). (%(x2,y2). \ |
5508 | 275 |
\ intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"; |
276 |
by (rtac (equiv_intrel RS congruent2_commuteI) 1); |
|
277 |
by (pair_tac "w" 2); |
|
278 |
by (rename_tac "z1 z2" 2); |
|
7375
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
279 |
by (ALLGOALS Clarify_tac); |
5508 | 280 |
by (simp_tac (simpset() addsimps add_ac@mult_ac) 1); |
281 |
by (asm_simp_tac (simpset() delsimps [equiv_intrel_iff] |
|
7375
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
282 |
addsimps add_ac@mult_ac) 1); |
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
283 |
by (rtac ([equiv_intrel, intrelI] MRS equiv_class_eq) 1); |
5508 | 284 |
by (rtac (zmult_congruent_lemma RS trans) 1); |
285 |
by (rtac (zmult_congruent_lemma RS trans RS sym) 1); |
|
286 |
by (rtac (zmult_congruent_lemma RS trans RS sym) 1); |
|
287 |
by (rtac (zmult_congruent_lemma RS trans RS sym) 1); |
|
288 |
by (asm_simp_tac (simpset() addsimps [add_mult_distrib RS sym]) 1); |
|
289 |
by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1); |
|
290 |
qed "zmult_congruent2"; |
|
291 |
||
292 |
Goalw [zmult_def] |
|
293 |
"Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \ |
|
294 |
\ Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"; |
|
7375
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
295 |
by (asm_simp_tac |
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
296 |
(simpset() addsimps [UN_UN_split_split_eq, zmult_congruent2, |
2cb340e66d15
tidied, allowing pattern-matching in defs of zadd and zmult
paulson
parents:
7127
diff
changeset
|
297 |
equiv_intrel RS UN_equiv_class2]) 1); |
5508 | 298 |
qed "zmult"; |
299 |
||
300 |
Goal "(- z) * w = - (z * (w::int))"; |
|
301 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
|
302 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
|
5540 | 303 |
by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1); |
5508 | 304 |
qed "zmult_zminus"; |
305 |
||
306 |
Goal "(z::int) * w = w * z"; |
|
307 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
|
308 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
|
5540 | 309 |
by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1); |
5508 | 310 |
qed "zmult_commute"; |
311 |
||
312 |
Goal "((z1::int) * z2) * z3 = z1 * (z2 * z3)"; |
|
313 |
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); |
|
314 |
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); |
|
315 |
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); |
|
5540 | 316 |
by (asm_simp_tac (simpset() addsimps [add_mult_distrib2,zmult] @ |
317 |
add_ac @ mult_ac) 1); |
|
5508 | 318 |
qed "zmult_assoc"; |
319 |
||
320 |
(*For AC rewriting*) |
|
321 |
Goal "(z1::int)*(z2*z3) = z2*(z1*z3)"; |
|
322 |
by (rtac (zmult_commute RS trans) 1); |
|
323 |
by (rtac (zmult_assoc RS trans) 1); |
|
324 |
by (rtac (zmult_commute RS arg_cong) 1); |
|
325 |
qed "zmult_left_commute"; |
|
326 |
||
327 |
(*Integer multiplication is an AC operator*) |
|
328 |
val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute]; |
|
329 |
||
330 |
Goal "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"; |
|
331 |
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); |
|
332 |
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); |
|
333 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
|
334 |
by (asm_simp_tac |
|
5540 | 335 |
(simpset() addsimps [add_mult_distrib2, zadd, zmult] @ |
336 |
add_ac @ mult_ac) 1); |
|
5508 | 337 |
qed "zadd_zmult_distrib"; |
338 |
||
339 |
val zmult_commute'= read_instantiate [("z","w")] zmult_commute; |
|
340 |
||
341 |
Goal "w * (- z) = - (w * (z::int))"; |
|
342 |
by (simp_tac (simpset() addsimps [zmult_commute', zmult_zminus]) 1); |
|
343 |
qed "zmult_zminus_right"; |
|
344 |
||
345 |
Goal "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"; |
|
346 |
by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1); |
|
347 |
qed "zadd_zmult_distrib2"; |
|
348 |
||
6839 | 349 |
Goalw [zdiff_def] "((z1::int) - z2) * w = (z1 * w) - (z2 * w)"; |
350 |
by (stac zadd_zmult_distrib 1); |
|
351 |
by (simp_tac (simpset() addsimps [zmult_zminus]) 1); |
|
352 |
qed "zdiff_zmult_distrib"; |
|
353 |
||
354 |
Goal "(w::int) * (z1 - z2) = (w * z1) - (w * z2)"; |
|
355 |
by (simp_tac (simpset() addsimps [zmult_commute',zdiff_zmult_distrib]) 1); |
|
356 |
qed "zdiff_zmult_distrib2"; |
|
357 |
||
7010
63120b6dca50
more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents:
6991
diff
changeset
|
358 |
Goalw [int_def] "(int m) * (int n) = int (m * n)"; |
63120b6dca50
more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents:
6991
diff
changeset
|
359 |
by (simp_tac (simpset() addsimps [zmult]) 1); |
63120b6dca50
more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents:
6991
diff
changeset
|
360 |
qed "zmult_int"; |
63120b6dca50
more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents:
6991
diff
changeset
|
361 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
362 |
Goalw [int_def] "int 0 * z = int 0"; |
5508 | 363 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
364 |
by (asm_simp_tac (simpset() addsimps [zmult]) 1); |
|
6917 | 365 |
qed "zmult_int0"; |
5508 | 366 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
367 |
Goalw [int_def] "int 1 * z = z"; |
5508 | 368 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
369 |
by (asm_simp_tac (simpset() addsimps [zmult]) 1); |
|
6917 | 370 |
qed "zmult_int1"; |
5508 | 371 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
372 |
Goal "z * int 0 = int 0"; |
6917 | 373 |
by (rtac ([zmult_commute, zmult_int0] MRS trans) 1); |
374 |
qed "zmult_int0_right"; |
|
5508 | 375 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
376 |
Goal "z * int 1 = z"; |
6917 | 377 |
by (rtac ([zmult_commute, zmult_int1] MRS trans) 1); |
378 |
qed "zmult_int1_right"; |
|
5508 | 379 |
|
6917 | 380 |
Addsimps [zmult_int0, zmult_int0_right, zmult_int1, zmult_int1_right]; |
5508 | 381 |
|
382 |
||
383 |
(* Theorems about less and less_equal *) |
|
384 |
||
385 |
(*This lemma allows direct proofs of other <-properties*) |
|
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5540
diff
changeset
|
386 |
Goalw [zless_def, neg_def, zdiff_def, int_def] |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
387 |
"(w < z) = (EX n. z = w + int(Suc n))"; |
5508 | 388 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
389 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
|
390 |
by (Clarify_tac 1); |
|
391 |
by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1); |
|
392 |
by (safe_tac (claset() addSDs [less_eq_Suc_add])); |
|
393 |
by (res_inst_tac [("x","k")] exI 1); |
|
394 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac))); |
|
395 |
qed "zless_iff_Suc_zadd"; |
|
396 |
||
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
397 |
Goal "z < z + int (Suc n)"; |
5508 | 398 |
by (auto_tac (claset(), |
399 |
simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
400 |
zadd_int])); |
5508 | 401 |
qed "zless_zadd_Suc"; |
402 |
||
403 |
Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)"; |
|
404 |
by (auto_tac (claset(), |
|
405 |
simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
406 |
zadd_int])); |
5508 | 407 |
qed "zless_trans"; |
408 |
||
409 |
Goal "!!w::int. z<w ==> ~w<z"; |
|
410 |
by (safe_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1])); |
|
411 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
|
412 |
by Safe_tac; |
|
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5540
diff
changeset
|
413 |
by (asm_full_simp_tac (simpset() addsimps [int_def, zadd]) 1); |
5508 | 414 |
qed "zless_not_sym"; |
415 |
||
416 |
(* [| n<m; ~P ==> m<n |] ==> P *) |
|
5540 | 417 |
bind_thm ("zless_asym", zless_not_sym RS swap); |
5508 | 418 |
|
419 |
Goal "!!z::int. ~ z<z"; |
|
420 |
by (resolve_tac [zless_asym RS notI] 1); |
|
421 |
by (REPEAT (assume_tac 1)); |
|
422 |
qed "zless_not_refl"; |
|
423 |
||
424 |
(* z<z ==> R *) |
|
5594 | 425 |
bind_thm ("zless_irrefl", zless_not_refl RS notE); |
5508 | 426 |
AddSEs [zless_irrefl]; |
427 |
||
428 |
Goal "z<w ==> w ~= (z::int)"; |
|
429 |
by (Blast_tac 1); |
|
430 |
qed "zless_not_refl2"; |
|
431 |
||
432 |
(* s < t ==> s ~= t *) |
|
433 |
bind_thm ("zless_not_refl3", zless_not_refl2 RS not_sym); |
|
434 |
||
435 |
||
436 |
(*"Less than" is a linear ordering*) |
|
5540 | 437 |
Goalw [zless_def, neg_def, zdiff_def] |
5508 | 438 |
"z<w | z=w | w<(z::int)"; |
439 |
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
|
440 |
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
|
441 |
by Safe_tac; |
|
442 |
by (asm_full_simp_tac |
|
443 |
(simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1); |
|
444 |
by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1); |
|
5758
27a2b36efd95
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5594
diff
changeset
|
445 |
by (ALLGOALS (force_tac (claset(), simpset() addsimps add_ac))); |
5508 | 446 |
qed "zless_linear"; |
447 |
||
448 |
Goal "!!w::int. (w ~= z) = (w<z | z<w)"; |
|
449 |
by (cut_facts_tac [zless_linear] 1); |
|
450 |
by (Blast_tac 1); |
|
451 |
qed "int_neq_iff"; |
|
452 |
||
453 |
(*** eliminates ~= in premises ***) |
|
454 |
bind_thm("int_neqE", int_neq_iff RS iffD1 RS disjE); |
|
455 |
||
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
456 |
Goal "(int m = int n) = (m = n)"; |
6991 | 457 |
by (fast_tac (claset() addSEs [inj_int RS injD]) 1); |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5540
diff
changeset
|
458 |
qed "int_int_eq"; |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5540
diff
changeset
|
459 |
AddIffs [int_int_eq]; |
5508 | 460 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
461 |
Goal "(int m < int n) = (m<n)"; |
5508 | 462 |
by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd, |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
463 |
zadd_int]) 1); |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
464 |
qed "zless_int"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
465 |
Addsimps [zless_int]; |
5508 | 466 |
|
467 |
||
468 |
(*** Properties of <= ***) |
|
469 |
||
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
470 |
Goalw [zle_def, le_def] "(int m <= int n) = (m<=n)"; |
5508 | 471 |
by (Simp_tac 1); |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
472 |
qed "zle_int"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
473 |
Addsimps [zle_int]; |
5508 | 474 |
|
475 |
Goalw [zle_def] "z <= w ==> z < w | z=(w::int)"; |
|
476 |
by (cut_facts_tac [zless_linear] 1); |
|
477 |
by (blast_tac (claset() addEs [zless_asym]) 1); |
|
478 |
qed "zle_imp_zless_or_eq"; |
|
479 |
||
480 |
Goalw [zle_def] "z<w | z=w ==> z <= (w::int)"; |
|
481 |
by (cut_facts_tac [zless_linear] 1); |
|
482 |
by (blast_tac (claset() addEs [zless_asym]) 1); |
|
483 |
qed "zless_or_eq_imp_zle"; |
|
484 |
||
485 |
Goal "(x <= (y::int)) = (x < y | x=y)"; |
|
486 |
by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1)); |
|
5540 | 487 |
qed "integ_le_less"; |
5508 | 488 |
|
489 |
Goal "w <= (w::int)"; |
|
5540 | 490 |
by (simp_tac (simpset() addsimps [integ_le_less]) 1); |
5508 | 491 |
qed "zle_refl"; |
492 |
||
493 |
Goalw [zle_def] "z < w ==> z <= (w::int)"; |
|
494 |
by (blast_tac (claset() addEs [zless_asym]) 1); |
|
495 |
qed "zless_imp_zle"; |
|
496 |
||
497 |
(* Axiom 'linorder_linear' of class 'linorder': *) |
|
498 |
Goal "(z::int) <= w | w <= z"; |
|
5540 | 499 |
by (simp_tac (simpset() addsimps [integ_le_less]) 1); |
5508 | 500 |
by (cut_facts_tac [zless_linear] 1); |
501 |
by (Blast_tac 1); |
|
502 |
qed "zle_linear"; |
|
503 |
||
504 |
Goal "[| i <= j; j < k |] ==> i < (k::int)"; |
|
505 |
by (dtac zle_imp_zless_or_eq 1); |
|
506 |
by (blast_tac (claset() addIs [zless_trans]) 1); |
|
507 |
qed "zle_zless_trans"; |
|
508 |
||
509 |
Goal "[| i < j; j <= k |] ==> i < (k::int)"; |
|
510 |
by (dtac zle_imp_zless_or_eq 1); |
|
511 |
by (blast_tac (claset() addIs [zless_trans]) 1); |
|
512 |
qed "zless_zle_trans"; |
|
513 |
||
514 |
Goal "[| i <= j; j <= k |] ==> i <= (k::int)"; |
|
515 |
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, |
|
516 |
rtac zless_or_eq_imp_zle, |
|
517 |
blast_tac (claset() addIs [zless_trans])]); |
|
518 |
qed "zle_trans"; |
|
519 |
||
520 |
Goal "[| z <= w; w <= z |] ==> z = (w::int)"; |
|
521 |
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, |
|
522 |
blast_tac (claset() addEs [zless_asym])]); |
|
523 |
qed "zle_anti_sym"; |
|
524 |
||
525 |
(* Axiom 'order_less_le' of class 'order': *) |
|
526 |
Goal "(w::int) < z = (w <= z & w ~= z)"; |
|
527 |
by (simp_tac (simpset() addsimps [zle_def, int_neq_iff]) 1); |
|
528 |
by (blast_tac (claset() addSEs [zless_asym]) 1); |
|
529 |
qed "int_less_le"; |
|
530 |
||
531 |
(* [| w <= z; w ~= z |] ==> w < z *) |
|
532 |
bind_thm ("zle_neq_implies_zless", [int_less_le, conjI] MRS iffD2); |
|
533 |
||
534 |
||
535 |
||
536 |
(*** Subtraction laws ***) |
|
537 |
||
538 |
Goal "x + (y - z) = (x + y) - (z::int)"; |
|
5540 | 539 |
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1); |
5508 | 540 |
qed "zadd_zdiff_eq"; |
541 |
||
542 |
Goal "(x - y) + z = (x + z) - (y::int)"; |
|
5540 | 543 |
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1); |
5508 | 544 |
qed "zdiff_zadd_eq"; |
545 |
||
546 |
Goal "(x - y) - z = x - (y + (z::int))"; |
|
5540 | 547 |
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1); |
5508 | 548 |
qed "zdiff_zdiff_eq"; |
549 |
||
550 |
Goal "x - (y - z) = (x + z) - (y::int)"; |
|
5540 | 551 |
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1); |
5508 | 552 |
qed "zdiff_zdiff_eq2"; |
553 |
||
554 |
Goalw [zless_def, zdiff_def] "(x-y < z) = (x < z + (y::int))"; |
|
555 |
by (simp_tac (simpset() addsimps zadd_ac) 1); |
|
556 |
qed "zdiff_zless_eq"; |
|
557 |
||
558 |
Goalw [zless_def, zdiff_def] "(x < z-y) = (x + (y::int) < z)"; |
|
559 |
by (simp_tac (simpset() addsimps zadd_ac) 1); |
|
560 |
qed "zless_zdiff_eq"; |
|
561 |
||
562 |
Goalw [zle_def] "(x-y <= z) = (x <= z + (y::int))"; |
|
563 |
by (simp_tac (simpset() addsimps [zless_zdiff_eq]) 1); |
|
564 |
qed "zdiff_zle_eq"; |
|
565 |
||
566 |
Goalw [zle_def] "(x <= z-y) = (x + (y::int) <= z)"; |
|
567 |
by (simp_tac (simpset() addsimps [zdiff_zless_eq]) 1); |
|
568 |
qed "zle_zdiff_eq"; |
|
569 |
||
570 |
Goalw [zdiff_def] "(x-y = z) = (x = z + (y::int))"; |
|
571 |
by (auto_tac (claset(), simpset() addsimps [zadd_assoc])); |
|
572 |
qed "zdiff_eq_eq"; |
|
573 |
||
574 |
Goalw [zdiff_def] "(x = z-y) = (x + (y::int) = z)"; |
|
575 |
by (auto_tac (claset(), simpset() addsimps [zadd_assoc])); |
|
576 |
qed "eq_zdiff_eq"; |
|
577 |
||
578 |
(*This list of rewrites simplifies (in)equalities by bringing subtractions |
|
579 |
to the top and then moving negative terms to the other side. |
|
580 |
Use with zadd_ac*) |
|
581 |
val zcompare_rls = |
|
582 |
[symmetric zdiff_def, |
|
583 |
zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2, |
|
584 |
zdiff_zless_eq, zless_zdiff_eq, zdiff_zle_eq, zle_zdiff_eq, |
|
585 |
zdiff_eq_eq, eq_zdiff_eq]; |
|
586 |
||
587 |
||
588 |
(** Cancellation laws **) |
|
589 |
||
590 |
Goal "!!w::int. (z + w' = z + w) = (w' = w)"; |
|
591 |
by Safe_tac; |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7010
diff
changeset
|
592 |
by (dres_inst_tac [("f", "%x. x + (-z)")] arg_cong 1); |
5508 | 593 |
by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1); |
594 |
qed "zadd_left_cancel"; |
|
595 |
||
596 |
Addsimps [zadd_left_cancel]; |
|
597 |
||
598 |
Goal "!!z::int. (w' + z = w + z) = (w' = w)"; |
|
599 |
by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1); |
|
600 |
qed "zadd_right_cancel"; |
|
601 |
||
602 |
Addsimps [zadd_right_cancel]; |
|
603 |
||
604 |
||
5594 | 605 |
(** For the cancellation simproc. |
606 |
The idea is to cancel like terms on opposite sides by subtraction **) |
|
607 |
||
608 |
Goal "(x::int) - y = x' - y' ==> (x<y) = (x'<y')"; |
|
609 |
by (asm_simp_tac (simpset() addsimps [zless_def]) 1); |
|
610 |
qed "zless_eqI"; |
|
5508 | 611 |
|
5594 | 612 |
Goal "(x::int) - y = x' - y' ==> (y<=x) = (y'<=x')"; |
613 |
by (dtac zless_eqI 1); |
|
614 |
by (asm_simp_tac (simpset() addsimps [zle_def]) 1); |
|
615 |
qed "zle_eqI"; |
|
5508 | 616 |
|
5594 | 617 |
Goal "(x::int) - y = x' - y' ==> (x=y) = (x'=y')"; |
618 |
by Safe_tac; |
|
619 |
by (ALLGOALS |
|
620 |
(asm_full_simp_tac (simpset() addsimps [eq_zdiff_eq, zdiff_eq_eq]))); |
|
621 |
qed "zeq_eqI"; |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
622 |