int_arithScript.sml
1Theory int_arith
2Ancestors
3 integer divides arithmetic gcd
4Libs
5 intSyntax simpLib boolSimps BasicProvers
6
7val arith_ss = bool_ss ++ numSimps.old_ARITH_ss
8
9val _ = ParseExtras.temp_loose_equality()
10
11
12Theorem not_less:
13 ~(x:int < y) = y < x + 1
14Proof
15 EQ_TAC THEN REWRITE_TAC [INT_NOT_LT] THEN STRIP_TAC THENL [
16 IMP_RES_TAC INT_LT_ADD1,
17 REWRITE_TAC [INT_LE_LT] THEN Q.ASM_CASES_TAC `y = x` THEN
18 ASM_REWRITE_TAC [] THEN Q.ASM_CASES_TAC `x < y` THENL [
19 IMP_RES_TAC INT_DISCRETE,
20 MP_TAC (Q.SPEC `x` (Q.SPEC `y` INT_LT_TOTAL)) THEN
21 ASM_REWRITE_TAC []
22 ]
23 ]
24QED
25
26Theorem elim_eq:
27 (x:int = y) = (x < y + 1 /\ y < x + 1)
28Proof
29 REWRITE_TAC [GSYM not_less] THEN EQ_TAC THEN STRIP_TAC THENL [
30 ASM_REWRITE_TAC [INT_LT_REFL],
31 MP_TAC (Q.SPECL [`x`,`y`] INT_LT_TOTAL) THEN
32 ASM_REWRITE_TAC []
33 ]
34QED
35
36Theorem less_to_leq_samel:
37 !x y. x < y = x <= y + ~1
38Proof
39 REWRITE_TAC [int_le, not_less, GSYM INT_ADD_ASSOC, INT_ADD_LINV,
40 INT_ADD_RID]
41QED
42Theorem less_to_leq_samer:
43 !x y:int. x < y = x + 1 <= y
44Proof
45 REWRITE_TAC [int_le, not_less, INT_LT_RADD]
46QED
47
48Theorem lt_move_all_right:
49 !x y. x < y = 0 < y + ~x
50Proof
51 REWRITE_TAC [INT_LT_ADDNEG, INT_ADD_LID]
52QED
53Theorem lt_move_all_left:
54 !x y. x < y = x + ~y < 0
55Proof
56 REWRITE_TAC [INT_LT_ADDNEG2, INT_ADD_LID]
57QED
58Theorem lt_move_left_left:
59 !x y z. x < y + z = x + ~y < z
60Proof
61 REPEAT GEN_TAC THEN REWRITE_TAC [INT_LT_ADDNEG2] THEN
62 CONV_TAC (LHS_CONV (RAND_CONV (REWR_CONV INT_ADD_COMM))) THEN REFL_TAC
63QED
64Theorem lt_move_left_right:
65 !x y z. x + y < z = y < z + ~x
66Proof
67 REPEAT GEN_TAC THEN REWRITE_TAC [INT_LT_ADDNEG] THEN
68 CONV_TAC (LHS_CONV (RATOR_CONV (RAND_CONV (REWR_CONV INT_ADD_COMM)))) THEN
69 REFL_TAC
70QED
71
72Theorem le_move_right_left:
73 !x y z. x <= y + z = x + ~z <= y
74Proof
75 REWRITE_TAC [INT_LE_SUB_RADD, GSYM int_sub]
76QED
77
78Theorem le_move_all_right:
79 !x y. x <= y = 0 <= y + ~x
80Proof
81 REWRITE_TAC [GSYM int_sub, INT_LE_SUB_LADD, INT_ADD_LID]
82QED
83
84
85Theorem eq_move_all_right:
86 !x y. (x = y) = (0 = y + ~x)
87Proof
88 REPEAT GEN_TAC THEN EQ_TAC THENL [
89 SIMP_TAC bool_ss [INT_ADD_RINV],
90 SIMP_TAC bool_ss [GSYM int_sub, INT_EQ_SUB_LADD, INT_ADD_LID]
91 ]
92QED
93Theorem eq_move_all_left:
94 !x y. (x = y) = (x + ~y = 0)
95Proof
96 PROVE_TAC [INT_ADD_COMM, eq_move_all_right]
97QED
98Theorem eq_move_left_left:
99 !x y z. (x = y + z) = (x + ~y = z)
100Proof
101 REPEAT GEN_TAC THEN EQ_TAC THENL [
102 DISCH_THEN SUBST1_TAC THEN
103 ONCE_REWRITE_TAC [INT_ADD_COMM] THEN
104 REWRITE_TAC [INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_LID],
105 DISCH_THEN (SUBST1_TAC o SYM) THEN
106 ONCE_REWRITE_TAC [INT_ADD_COMM] THEN
107 REWRITE_TAC [GSYM INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_RID]
108 ]
109QED
110Theorem eq_move_left_right:
111 !x y z. (x + y = z) = (y = z + ~x)
112Proof
113 PROVE_TAC [INT_ADD_COMM, eq_move_left_left]
114QED
115
116Theorem eq_move_right_left:
117 !x y z. (x = y + z) = (x + ~z = y)
118Proof
119 PROVE_TAC [INT_ADD_COMM, eq_move_left_left]
120QED
121
122Theorem lcm_eliminate:
123 !P c. (?x. P (c * x)) = (?x. P x /\ c int_divides x)
124Proof
125 REPEAT GEN_TAC THEN SIMP_TAC bool_ss [INT_DIVIDES] THEN
126 PROVE_TAC [INT_MUL_SYM]
127QED
128
129
130Theorem lt_justify_multiplication:
131 !n x y:int. 0 < n ==> (x < y = n * x < n * y)
132Proof
133 REPEAT STRIP_TAC THEN
134 `n * x < n * y = 0 < n * y - n * x`
135 by PROVE_TAC [INT_LT_ADD_SUB, INT_ADD_LID] THEN
136 POP_ASSUM SUBST_ALL_TAC THEN
137 ASM_REWRITE_TAC [GSYM INT_SUB_LDISTRIB, INT_MUL_SIGN_CASES] THEN
138 `~(n < 0)` by PROVE_TAC [INT_LT_TRANS, INT_LT_REFL] THEN
139 ASM_REWRITE_TAC [INT_ADD_LID, GSYM INT_LT_ADD_SUB]
140QED
141
142Theorem eq_justify_multiplication:
143 !n x y:int. 0 < n ==> ((x = y) = (n * x = n * y))
144Proof
145 PROVE_TAC [INT_EQ_RMUL, INT_LT_REFL, INT_MUL_COMM]
146QED
147
148Theorem justify_divides:
149 !n x y:int. 0 < n ==> (x int_divides y = n * x int_divides n * y)
150Proof
151 PROVE_TAC [INT_DIVIDES_MUL_BOTH, INT_LT_REFL]
152QED
153
154Theorem justify_divides2:
155 !n c x y:int.
156 n * x int_divides n * y + c =
157 n * x int_divides n * y + c /\ n int_divides c
158Proof
159 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THEN
160 ASM_REWRITE_TAC [] THEN POP_ASSUM MP_TAC THEN
161 REWRITE_TAC [INT_DIVIDES] THEN
162 DISCH_THEN (STRIP_THM_THEN
163 (SUBST_ALL_TAC o SYM o
164 REWRITE_RULE [eq_move_left_left,
165 INT_NEG_RMUL])) THEN
166 `m * (n * x) = n * (m * x)` by PROVE_TAC [INT_MUL_COMM, INT_MUL_ASSOC] THEN
167 POP_ASSUM SUBST_ALL_TAC THEN
168 REWRITE_TAC [GSYM INT_LDISTRIB] THEN
169 PROVE_TAC [INT_MUL_COMM]
170QED
171
172Theorem justify_divides3:
173 !n x c. n int_divides n * x + c = n int_divides c
174Proof
175 REPEAT STRIP_TAC THEN MATCH_MP_TAC INT_DIVIDES_LADD THEN
176 MATCH_MP_TAC INT_DIVIDES_LMUL THEN MATCH_ACCEPT_TAC INT_DIVIDES_REFL
177QED
178
179
180Theorem INT_SUB_SUB3:
181 !x y z:int. x - (y - z) = x + z - y
182Proof
183 REWRITE_TAC [int_sub, INT_NEG_ADD, INT_NEGNEG] THEN
184 PROVE_TAC [INT_ADD_COMM, INT_ADD_ASSOC]
185QED
186
187(* |- !a b c:int. a - b + c = a + c - b *)
188Theorem move_sub = (
189 let
190 val thm0 = SYM (SPEC_ALL INT_ADD2_SUB2)
191 val thm1 = Thm.INST [(mk_var("d", int_ty) |-> zero_tm)] thm0
192 val thm2 = REWRITE_RULE [INT_ADD_RID, INT_SUB_RZERO] thm1
193 in
194 GEN_ALL thm2
195 end)
196
197Theorem can_get_small:
198 !x:int y d. 0 < d ==> ?c. 0 < c /\ y - c * d < x
199Proof
200 REPEAT STRIP_TAC THEN
201 Q.EXISTS_TAC `if y < x then 1
202 else if y = x then 1
203 else 2 * (y - x)` THEN
204 SRW_TAC [][] THENL [
205 SRW_TAC [][INT_MUL_SIGN_CASES, INT_SUB_LT] THEN PROVE_TAC [INT_LT_TOTAL],
206 MATCH_MP_TAC INT_LT_TRANS THEN Q.EXISTS_TAC `y` THEN
207 ASM_REWRITE_TAC [INT_LT_SUB_RADD, INT_LT_ADDR],
208 ASM_REWRITE_TAC [INT_LT_SUB_RADD, INT_LT_ADDR],
209 ASM_SIMP_TAC (srw_ss()) [INT_MUL_SIGN_CASES, INT_SUB_LDISTRIB,
210 INT_SUB_RDISTRIB, INT_SUB_LT, INT_SUB_SUB3] THEN
211 `x < y` by PROVE_TAC [INT_LT_TOTAL] THEN
212 ASM_REWRITE_TAC [GSYM move_sub, INT_LT_ADD_SUB] THEN
213 `2 * y * d = y * (2 * d)` by PROVE_TAC [INT_MUL_SYM, INT_MUL_ASSOC] THEN
214 POP_ASSUM SUBST_ALL_TAC THEN
215 `2 * x * d = x * (2 * d)` by PROVE_TAC [INT_MUL_SYM, INT_MUL_ASSOC] THEN
216 POP_ASSUM SUBST_ALL_TAC THEN
217 CONV_TAC
218 (BINOP_CONV (LAND_CONV (REWR_CONV (GSYM INT_MUL_RID)))) THEN
219 REWRITE_TAC [GSYM INT_SUB_LDISTRIB] THEN
220 ONCE_REWRITE_TAC [GSYM INT_LT_NEG] THEN
221 REWRITE_TAC [INT_NEG_RMUL, INT_NEG_SUB] THEN
222 Q.SUBGOAL_THEN `0 < 2 * d - 1`
223 (fn th => PROVE_TAC [th, lt_justify_multiplication, INT_MUL_SYM]) THEN
224 `?n. d = &n` by PROVE_TAC [NUM_POSINT_EXISTS, INT_LE_LT] THEN
225 SRW_TAC [][INT_SUB_LT, INT_LT, INT_MUL] THEN
226 FULL_SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss) []
227 ]
228QED
229
230Theorem can_get_big:
231 !x:int y d. 0 < d ==> ?c. 0 < c /\ x < y + c * d
232Proof
233 REPEAT STRIP_TAC THEN REWRITE_TAC [GSYM INT_LT_SUB_RADD] THEN
234 PROVE_TAC [can_get_small]
235QED
236
237Theorem positive_product_implication:
238 !c d:int. 0 < c /\ 0 < d ==> 0 < c * d
239Proof
240 SRW_TAC [] [INT_MUL_SIGN_CASES]
241QED
242
243Theorem restricted_quantification_simp:
244 !low high x:int.
245 (low < x /\ x <= high) =
246 (low < high /\ ((x = high) \/ (low < x /\ x <= high - 1)))
247Proof
248 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
249 `low < high` by PROVE_TAC [INT_LTE_TRANS] THEN
250 FULL_SIMP_TAC (srw_ss()) [INT_LE_LT] THEN
251 `~(x = high)` by PROVE_TAC [INT_LT_REFL] THEN
252 POP_ASSUM (fn th => REWRITE_TAC [th]) THEN
253 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
254 `high - 1 < x` by PROVE_TAC [INT_LT_TOTAL] THEN
255 `high < x + 1` by PROVE_TAC [INT_LT_SUB_RADD] THEN
256 PROVE_TAC [INT_DISCRETE],
257 SRW_TAC [][],
258 FULL_SIMP_TAC (srw_ss()) [INT_LE_LT] THEN DISJ1_TAC THENL [
259 MATCH_MP_TAC INT_LT_TRANS THEN
260 Q.EXISTS_TAC `high - 1`,
261 ALL_TAC
262 ] THEN
263 SRW_TAC [] [INT_LT_SUB_RADD, INT_LT_ADDR]
264 ]
265QED
266
267Theorem top_and_lessers:
268 !P d:int x0. (!x. P x ==> P(x - d)) /\ P x0 ==>
269 !c. 0 < c ==> P(x0 - c * d)
270Proof
271 REPEAT STRIP_TAC THEN
272 STRIP_ASSUME_TAC (Q.SPEC `c` INT_NUM_CASES) THENL [
273 (* c strictly positive *)
274 FIRST_ASSUM SUBST_ALL_TAC THEN
275 Induct_on `n` THEN REWRITE_TAC [INT_LT,
276 prim_recTheory.LESS_0,
277 numTheory.NOT_SUC, INT,
278 INT_RDISTRIB, INT_MUL_LID] THEN
279 Cases_on `n` THENL [
280 PROVE_TAC [INT_MUL_LZERO, INT_ADD_LID],
281 FULL_SIMP_TAC bool_ss [INT_INJ, prim_recTheory.INV_SUC_EQ,
282 prim_recTheory.LESS_0, INT_LT,
283 numTheory.NOT_SUC] THEN
284 Q.ABBREV_TAC `q = &(SUC n')*d` THEN
285 Q.SUBGOAL_THEN `x0 - (q + d) = x0 - q - d` (fn th => PROVE_TAC [th]) THEN
286 REWRITE_TAC [INT_SUB_CALCULATE, INT_NEG_ADD] THEN
287 CONV_TAC (AC_CONV(INT_ADD_ASSOC, INT_ADD_COMM))
288 ],
289 (* c strictly negative *)
290 FULL_SIMP_TAC bool_ss [INT_NEG_GT0, INT_LT,
291 prim_recTheory.NOT_LESS_0],
292 (* c zero *)
293 PROVE_TAC [INT_LT_REFL]
294 ]
295QED
296
297Theorem bot_and_greaters:
298 !P d:int x0. (!x. P x ==> P (x + d)) /\ P x0 ==>
299 !c. 0 < c ==> P(x0 + c * d)
300Proof
301 REPEAT STRIP_TAC THEN
302 Q.SPECL_THEN [`P`, `~d`, `x0`] MP_TAC top_and_lessers THEN
303 ASM_SIMP_TAC bool_ss [int_sub, INT_NEGNEG, GSYM INT_NEG_RMUL]
304QED
305
306Theorem in_additive_range:
307 !low d x:int.
308 low < x /\ x <= low + d =
309 ?j. (x = low + j) /\ 0 < j /\ j <= d
310Proof
311 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
312 Q.EXISTS_TAC `x - low` THEN
313 FULL_SIMP_TAC bool_ss [INT_LE_SUB_RADD, INT_LT_SUB_LADD,
314 INT_ADD_COMM, INT_ADD_LID, INT_SUB_ADD2],
315 FIRST_X_ASSUM SUBST_ALL_TAC THEN
316 ASM_SIMP_TAC bool_ss [INT_LT_SUB_RADD, INT_LT_ADDR, INT_LE_LADD]
317 ]
318QED
319
320Theorem in_subtractive_range:
321 !high d x:int.
322 high - d <= x /\ x < high =
323 ?j. (x = high - j) /\ 0 < j /\ j <= d
324Proof
325 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
326 Q.EXISTS_TAC `high - x` THEN
327 FULL_SIMP_TAC bool_ss [INT_SUB_SUB2, INT_LT_SUB_LADD,
328 INT_ADD_LID, INT_LE_SUB_RADD,
329 INT_ADD_COMM],
330 FIRST_X_ASSUM SUBST_ALL_TAC THEN
331 ASM_SIMP_TAC bool_ss [INT_LT_SUB_RADD, INT_LT_ADDR] THEN
332 ASM_SIMP_TAC bool_ss [int_sub, INT_LE_LADD, INT_LE_NEG]
333 ]
334QED
335
336Theorem subtract_to_small:
337 !x d:int. 0 < d ==> ?k. 0 < x - k * d /\ x - k * d <= d
338Proof
339 REPEAT STRIP_TAC THEN
340 `~(d = 0)` by PROVE_TAC [INT_LT_REFL] THEN
341 `~(d < 0)` by PROVE_TAC [INT_NOT_LT, INT_LE_LT] THEN
342 `(x = x / d * d + x % d) /\ 0 <= x % d /\ x % d < d`
343 by PROVE_TAC [INT_DIVISION] THEN
344 Q.ABBREV_TAC `q = x / d` THEN POP_ASSUM (K ALL_TAC) THEN
345 Q.ABBREV_TAC `r = x % d` THEN POP_ASSUM (K ALL_TAC) THEN
346 FIRST_X_ASSUM SUBST_ALL_TAC THEN
347 FULL_SIMP_TAC (srw_ss()) [INT_LE_LT] THENL [
348 Q.EXISTS_TAC `q`,
349 Q.EXISTS_TAC `q - 1`
350 ] THEN
351 SRW_TAC [] [INT_LT_SUB_LADD, INT_LE_SUB_RADD, INT_SUB_RDISTRIB,
352 INT_LT_SUB_RADD] THEN
353 PROVE_TAC [INT_ADD_COMM, INT_LT_LADD]
354QED
355
356Theorem add_to_greater:
357 !x d:int. 0 < d ==> ?k. 0 < x + k * d /\ x + k * d <= d
358Proof
359 REPEAT STRIP_TAC THEN
360 Q.SPECL_THEN [`x`, `d`] MP_TAC subtract_to_small THEN
361 ASM_REWRITE_TAC [] THEN STRIP_TAC THEN
362 Q.EXISTS_TAC `~k` THEN
363 ASM_REWRITE_TAC [GSYM INT_NEG_LMUL, GSYM int_sub]
364QED
365
366
367Theorem INT_LT_ADD_NUMERAL:
368 !x:int y. x < x + &(NUMERAL (BIT1 y)) /\
369 x < x + &(NUMERAL (BIT2 y)) /\
370 ~(x < x + ~(&(NUMERAL y)))
371Proof
372 SIMP_TAC bool_ss [INT_LT_ADDR, INT_LT, NUMERAL_DEF, BIT1,BIT2,
373 ADD_CLAUSES, prim_recTheory.LESS_0,
374 INT_NEG_GT0, prim_recTheory.NOT_LESS_0]
375QED
376
377
378Theorem INT_NUM_FORALL:
379 (!n:num. P (&n)) = (!x:int. 0 <= x ==> P x)
380Proof
381 EQ_TAC THEN REPEAT STRIP_TAC THENL [
382 PROVE_TAC [NUM_POSINT_EXISTS],
383 POP_ASSUM MATCH_MP_TAC THEN SIMP_TAC bool_ss [INT_LE, ZERO_LESS_EQ]
384 ]
385QED
386
387Theorem INT_NUM_EXISTS:
388 (?n:num. P(&n)) = (?x:int. 0 <= x /\ P x)
389Proof
390 EQ_TAC THEN REPEAT STRIP_TAC THENL [
391 PROVE_TAC [INT_LE, ZERO_LESS_EQ],
392 PROVE_TAC [NUM_POSINT_EXISTS]
393 ]
394QED
395
396Theorem INT_NUM_UEXISTS:
397 (?!n:num. P (&n)) = (?!x:int. 0 <= x /\ P x)
398Proof
399 EQ_TAC THEN SIMP_TAC bool_ss [EXISTS_UNIQUE_THM] THEN
400 REPEAT STRIP_TAC THENL [
401 PROVE_TAC [INT_LE, ZERO_LESS_EQ],
402 PROVE_TAC [INT_INJ, NUM_POSINT_EXISTS],
403 PROVE_TAC [NUM_POSINT_EXISTS],
404 PROVE_TAC [INT_INJ, ZERO_LESS_EQ, INT_LE]
405 ]
406QED
407
408Theorem INT_NUM_SUB:
409 !n m:num. &(n - m) = if int_of_num n < &m then 0i else &n - &m
410Proof
411 SIMP_TAC (bool_ss ++ COND_elim_ss) [INT_LT, INT_INJ] THEN
412 REPEAT GEN_TAC THEN Q.ASM_CASES_TAC `n < m` THEN
413 ASM_SIMP_TAC bool_ss [SUB_EQ_0, LESS_OR_EQ] THEN
414 PROVE_TAC [INT_SUB, NOT_LESS]
415QED
416
417Theorem INT_NUM_COND:
418 !b n m. int_of_num (if b then n else m) =
419 if b then &n else &m
420Proof
421 SIMP_TAC (bool_ss ++ COND_elim_ss) [] THEN PROVE_TAC []
422QED
423
424Theorem INT_NUM_ODD:
425 !n:num. ODD n = ~(2 int_divides &n)
426Proof
427 SIMP_TAC bool_ss [ODD_EVEN, EVEN_EXISTS, INT_DIVIDES, GSYM INT_INJ,
428 GSYM INT_MUL] THEN GEN_TAC THEN EQ_TAC THEN
429 REPEAT STRIP_TAC THENL [
430 Cases_on `&n = 0` THENL [
431 POP_ASSUM SUBST_ALL_TAC THEN POP_ASSUM MP_TAC THEN
432 FULL_SIMP_TAC (srw_ss()) [INT_MUL],
433 `0 < &n` by PROVE_TAC [INT_LE_LT, INT_POS] THEN
434 `0 < 2i` by SRW_TAC [][] THEN
435 `0 < m` by PROVE_TAC [INT_MUL_SIGN_CASES, INT_LT_ANTISYM] THEN
436 `?k. m = &k` by PROVE_TAC [NUM_POSINT_EXISTS, INT_LE_LT] THEN
437 POP_ASSUM SUBST_ALL_TAC THEN
438 FIRST_X_ASSUM (MP_TAC o ONCE_REWRITE_RULE [INT_MUL_COMM] o
439 Q.SPEC `k`) THEN
440 ASM_REWRITE_TAC []
441 ],
442 FIRST_X_ASSUM (MP_TAC o Q.SPEC `int_of_num m`) THEN
443 ASM_REWRITE_TAC [] THEN MATCH_ACCEPT_TAC INT_MUL_COMM
444 ]
445QED
446
447Theorem INT_NUM_EVEN:
448 !n:num. EVEN n = 2 int_divides &n
449Proof
450 SIMP_TAC bool_ss [EVEN_ODD, INT_NUM_ODD]
451QED
452
453Theorem HO_SUB_ELIM:
454 !(P:int -> bool) a b.
455 P(&(a - b)) =
456 (int_of_num b <= &a /\ P(&a + ~&b)) \/
457 (int_of_num a < &b /\ P 0i)
458Proof
459 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN
460 FULL_SIMP_TAC (bool_ss ++ COND_elim_ss) [INT_NUM_SUB, LEFT_AND_OVER_OR,
461 RIGHT_AND_OVER_OR, INT_NOT_LT,
462 int_sub] THEN
463 PROVE_TAC [INT_LE_LT, INT_LT_TOTAL, INT_LET_TRANS, INT_LT_REFL]
464QED
465
466Theorem CONJ_EQ_ELIM:
467 !P v e. (v = e) /\ P v = (v = e) /\ P e
468Proof
469 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
470 FIRST_X_ASSUM (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC [],
471 ASM_REWRITE_TAC []
472 ]
473QED
474
475Theorem elim_neg_ones:
476 !x. x + ~1 + 1 = x
477Proof
478 REWRITE_TAC [GSYM INT_ADD_ASSOC, INT_ADD_LINV, INT_ADD_RID]
479QED
480
481Theorem elim_minus_ones:
482 !x:int. (x + 1) - 1 = x
483Proof
484 REWRITE_TAC [int_sub, GSYM INT_ADD_ASSOC, INT_ADD_RINV, INT_ADD_RID]
485QED
486
487Theorem INT_NUM_DIVIDES:
488 !n m. &n int_divides &m = divides n m
489Proof
490 SIMP_TAC bool_ss [INT_DIVIDES, dividesTheory.divides_def, EQ_IMP_THM,
491 FORALL_AND_THM, GSYM LEFT_FORALL_IMP_THM] THEN
492 REPEAT STRIP_TAC THENL [
493 STRIP_ASSUME_TAC (Q.SPEC `m'` INT_NUM_CASES) THEN
494 FULL_SIMP_TAC bool_ss [INT_MUL_CALCULATE, INT_INJ, INT_EQ_CALCULATE,
495 MULT_CLAUSES] THENL [
496 PROVE_TAC [],
497 PROVE_TAC [MULT_CLAUSES],
498 PROVE_TAC [MULT_CLAUSES]
499 ],
500 Q.EXISTS_TAC `&q` THEN SIMP_TAC bool_ss [INT_MUL]
501 ]
502QED
503
504Theorem INT_LINEAR_GCD:
505 !n m. ?p:int q. p * &n + q * &m = &(gcd n m)
506Proof
507 REPEAT GEN_TAC THEN
508 Cases_on `n = 0` THENL [
509 POP_ASSUM SUBST1_TAC THEN
510 SIMP_TAC bool_ss [INT_MUL_RZERO, GCD_0L, INT_ADD_LID] THEN
511 PROVE_TAC [INT_MUL_LID],
512 ALL_TAC
513 ] THEN Cases_on `m = 0` THENL [
514 POP_ASSUM SUBST1_TAC THEN
515 SIMP_TAC bool_ss [INT_MUL_RZERO, GCD_0R, INT_ADD_RID] THEN
516 PROVE_TAC [INT_MUL_LID],
517 ALL_TAC
518 ] THEN
519 `?i j. i * n = j * m + gcd m n` by PROVE_TAC [LINEAR_GCD] THEN
520 MAP_EVERY Q.EXISTS_TAC [`&i`, `~&j`] THEN
521 ASM_SIMP_TAC bool_ss [INT_MUL_CALCULATE, GSYM eq_move_left_left,
522 GCD_SYM, INT_ADD]
523QED
524
525Theorem INT_DIVIDES_LRMUL:
526 !p q r. ~(q = 0) ==> ((p * q) int_divides (r * q) = p int_divides r)
527Proof
528 REPEAT GEN_TAC THEN SIMP_TAC bool_ss [INT_DIVIDES] THEN
529 STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
530 `(m * p) * q = r * q` by PROVE_TAC [INT_MUL_ASSOC] THEN
531 PROVE_TAC [INT_EQ_RMUL],
532 PROVE_TAC [INT_MUL_ASSOC]
533 ]
534QED
535
536
537Theorem INT_DIVIDES_RELPRIME_MUL:
538 !p q r.
539 (gcd p q = 1) ==>
540 (&p int_divides &q * r = &p int_divides r)
541Proof
542 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
543 STRIP_ASSUME_TAC (Q.SPEC `r` INT_NUM_CASES) THEN
544 FIRST_X_ASSUM SUBST_ALL_TAC THEN
545 FULL_SIMP_TAC bool_ss [INT_NUM_DIVIDES, INT_MUL_CALCULATE,
546 INT_DIVIDES_NEG] THEN
547 PROVE_TAC [L_EUCLIDES, GCD_SYM],
548 PROVE_TAC [INT_DIVIDES_RMUL]
549 ]
550QED
551
552Theorem INT_MUL_DIV'[local]:
553 !p q k.
554 ~(q = 0) /\ q int_divides p ==> (k * (p / q) = k * p / q)
555Proof
556 REPEAT STRIP_TAC THEN
557 FULL_SIMP_TAC bool_ss [INT_DIVIDES_MOD0] THEN FULL_SIMP_TAC bool_ss [] THEN
558 PROVE_TAC [INT_MUL_DIV]
559QED
560
561Theorem fractions[local]:
562 !p q r.
563 ~(r = 0) /\ r int_divides p /\ r int_divides q ==>
564 (p / r + q / r = (p + q) / r)
565Proof
566 REPEAT STRIP_TAC THEN
567 `?i. p = i * r` by PROVE_TAC [INT_DIVIDES] THEN POP_ASSUM SUBST1_TAC THEN
568 `?j. q = j * r` by PROVE_TAC [INT_DIVIDES] THEN POP_ASSUM SUBST1_TAC THEN
569 `i * r + j * r = (i + j) * r` by REWRITE_TAC [INT_RDISTRIB] THEN
570 POP_ASSUM SUBST1_TAC THEN
571 ASM_SIMP_TAC bool_ss [INT_MUL_DIV, INT_MOD_ID, INT_DIV_ID, INT_MUL_RID]
572QED
573
574Theorem gcdthm2:
575 !m:num a:num x b d p q.
576 (d = gcd a m) /\ (&d = p * &a + q * &m) /\ ~(d = 0) /\
577 ~(m = 0) /\ ~(a = 0) ==>
578 (&m int_divides (&a * x) + b =
579 &d int_divides b /\
580 ?t. x = ~p * (b / &d) + t * (&m / &d))
581Proof
582 REPEAT STRIP_TAC THEN EQ_TAC THENL [
583 STRIP_TAC THEN
584 `&d int_divides &a /\ &d int_divides &m` by
585 PROVE_TAC [INT_NUM_DIVIDES, GCD_IS_GCD, is_gcd_def] THEN
586 `&d int_divides &a * x + b` by PROVE_TAC [INT_DIVIDES_TRANS] THEN
587 `&d int_divides &a * x` by PROVE_TAC [INT_DIVIDES_LMUL] THEN
588 `&d int_divides b` by PROVE_TAC [INT_DIVIDES_LADD] THEN CONJ_TAC THENL [
589 ASM_REWRITE_TAC [],
590 ALL_TAC
591 ] THEN (* existential goal remains *)
592 Cases_on `d = 1` THENL [
593 POP_ASSUM SUBST_ALL_TAC THEN SIMP_TAC bool_ss [INT_DIV_1],
594 `?b'. b = b' * &d` by PROVE_TAC [INT_DIVIDES] THEN
595 POP_ASSUM SUBST_ALL_TAC THEN
596 REPEAT (FIRST_X_ASSUM (MP_TAC o assert (is_eq o concl))) THEN
597 REPEAT (DISCH_THEN (ASSUME_TAC o SYM)) THEN
598 ASM_SIMP_TAC bool_ss [INT_MUL_DIV, INT_MOD_ID, INT_INJ, INT_DIV_ID,
599 INT_MUL_RID] THEN
600 MP_TAC (Q.SPECL [`m`, `a`] FACTOR_OUT_GCD) THEN
601 ASM_REWRITE_TAC [] THEN
602 DISCH_THEN (Q.X_CHOOSE_THEN `m'`
603 (Q.X_CHOOSE_THEN `a'` STRIP_ASSUME_TAC)) THEN
604 `gcd m a = d` by PROVE_TAC [GCD_SYM] THEN
605 POP_ASSUM SUBST_ALL_TAC THEN
606 POP_ASSUM MP_TAC THEN
607 NTAC 2 (POP_ASSUM SUBST_ALL_TAC) THEN
608 FULL_SIMP_TAC bool_ss [MULT_EQ_0] THEN
609 ASM_SIMP_TAC bool_ss [INT_MUL_DIV, GSYM INT_MUL, INT_MOD_ID, INT_INJ,
610 INT_DIV_ID, INT_MUL_RID] THEN
611 FULL_SIMP_TAC bool_ss [GSYM INT_MUL] THEN
612 `&m' int_divides &a' * x + b'` by
613 (`&a' * &d * x = &a' * x * &d` by
614 CONV_TAC(AC_CONV(INT_MUL_ASSOC, INT_MUL_COMM)) THEN
615 POP_ASSUM SUBST_ALL_TAC THEN
616 `&m' * &d int_divides (&a' * x + b') * &d` by
617 ASM_SIMP_TAC bool_ss [INT_RDISTRIB] THEN
618 POP_ASSUM MP_TAC THEN
619 ASM_SIMP_TAC bool_ss [INT_DIVIDES_LRMUL, INT_INJ]) THEN
620 NTAC 2 (POP_ASSUM MP_TAC) THEN POP_ASSUM (K ALL_TAC) THEN
621 REPEAT (Q.PAT_X_ASSUM `y int_divides z` (K ALL_TAC)) THEN
622 Q.PAT_X_ASSUM `T` (K ALL_TAC) THEN
623 REWRITE_TAC [INT_MUL_ASSOC, GSYM INT_RDISTRIB] THEN
624 CONV_TAC (LAND_CONV (RHS_CONV (REWR_CONV (GSYM INT_MUL_LID)))) THEN
625 ASM_SIMP_TAC bool_ss [INT_INJ, INT_EQ_RMUL] THEN
626 REPEAT (DISCH_THEN (ASSUME_TAC o GSYM)) THEN
627 Q.ABBREV_TAC `b = b'` THEN POP_ASSUM (K ALL_TAC) THEN
628 Q.ABBREV_TAC `m = m'` THEN POP_ASSUM (K ALL_TAC) THEN
629 Q.ABBREV_TAC `a = a'` THEN POP_ASSUM (K ALL_TAC) THEN
630 POP_ASSUM (ASSUME_TAC o ONCE_REWRITE_RULE [GCD_SYM])
631 ] THEN
632
633 `b * 1 = b * (p * &a + q * &m)` by (AP_TERM_TAC THEN
634 ASM_REWRITE_TAC []) THEN
635 POP_ASSUM (fn th =>
636 `b = b * (p * &a) + b * (q * &m)` by
637 PROVE_TAC [th, INT_LDISTRIB, INT_MUL_RID]) THEN
638 POP_ASSUM (fn th =>
639 `b + ~(b * (q * &m)) = b * (p * &a)` by
640 (MP_TAC th THEN
641 SIMP_TAC bool_ss [GSYM eq_move_left_left] THEN
642 SIMP_TAC bool_ss [INT_ADD_COMM])) THEN
643 POP_ASSUM (fn th =>
644 `&a * (b * p) = b + ~(b * (q * &m))` by
645 (REWRITE_TAC [th] THEN
646 CONV_TAC (AC_CONV(INT_MUL_ASSOC, INT_MUL_COMM)))) THEN
647 POP_ASSUM (fn th =>
648 `&m int_divides &a * (x + b * p)` by
649 (SIMP_TAC bool_ss [INT_LDISTRIB, th] THEN
650 REWRITE_TAC [INT_ADD_ASSOC] THEN
651 ASM_SIMP_TAC bool_ss [INT_DIVIDES_LADD] THEN
652 SIMP_TAC bool_ss [INT_NEG_LMUL, INT_DIVIDES_RMUL,
653 INT_DIVIDES_REFL])) THEN
654 `&m int_divides x + b*p`
655 by PROVE_TAC [GCD_SYM, INT_DIVIDES_RELPRIME_MUL] THEN
656 `?j. j * &m = x + p * b` by PROVE_TAC [INT_DIVIDES, INT_MUL_COMM] THEN
657 `x = j * &m + ~(p * b)` by PROVE_TAC [eq_move_left_left, INT_ADD_COMM] THEN
658 PROVE_TAC [INT_MUL_CALCULATE, INT_ADD_COMM],
659
660 STRIP_TAC THEN POP_ASSUM SUBST_ALL_TAC THEN
661 REPEAT (FIRST_X_ASSUM (MP_TAC o assert (is_eq o concl))) THEN
662 REPEAT (DISCH_THEN (ASSUME_TAC o SYM)) THEN
663 `&d int_divides &m /\ &d int_divides &a` by
664 PROVE_TAC [INT_NUM_DIVIDES, GCD_IS_GCD, is_gcd_def] THEN
665 REWRITE_TAC [INT_LDISTRIB] THEN
666 `&a * (~p * (b / &d)) = b * (~p * &a / &d)` by
667 (ASM_SIMP_TAC bool_ss [INT_MUL_DIV', INT_DIVIDES_LMUL,
668 INT_DIVIDES_RMUL, INT_INJ] THEN
669 REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC) THEN
670 CONV_TAC (AC_CONV(INT_MUL_ASSOC, INT_MUL_COMM))) THEN
671 POP_ASSUM SUBST1_TAC THEN
672 `&a * (t * (&m / &d)) = &m * (t * &a / &d)` by
673 (ASM_SIMP_TAC bool_ss [INT_MUL_DIV', INT_DIVIDES_LMUL,
674 INT_DIVIDES_RMUL, INT_INJ] THEN
675 REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC) THEN
676 CONV_TAC (AC_CONV(INT_MUL_ASSOC, INT_MUL_COMM))) THEN
677 POP_ASSUM SUBST1_TAC THEN
678 `b * (~p * &a / &d) + &m * (t * &a / &d) + b =
679 &m * (t * &a / &d) + b * (1 + ~p * &a / &d)` by
680 (REWRITE_TAC [INT_LDISTRIB, INT_MUL_RID] THEN
681 CONV_TAC (AC_CONV(INT_ADD_ASSOC, INT_ADD_COMM))) THEN
682 POP_ASSUM SUBST1_TAC THEN
683 SIMP_TAC bool_ss [INT_DIVIDES_LADD, INT_DIVIDES_LMUL,
684 INT_DIVIDES_REFL] THEN
685 Q.SUBGOAL_THEN `1 = &d / &d` SUBST1_TAC THENL [
686 ASM_SIMP_TAC bool_ss [INT_INJ, INT_DIV_ID],
687 ALL_TAC
688 ] THEN
689 ASM_SIMP_TAC bool_ss [fractions, INT_DIVIDES_RMUL, INT_DIVIDES_REFL,
690 INT_INJ] THEN
691 Q.SUBGOAL_THEN `&d + ~p * &a = q * &m` SUBST1_TAC THENL [
692 REWRITE_TAC [INT_MUL_CALCULATE] THEN
693 PROVE_TAC [eq_move_left_left],
694 ALL_TAC
695 ] THEN
696 Q.SUBGOAL_THEN `b * (q * &m / &d) = &m * (q * b / &d)`
697 (fn th => SUBST1_TAC th THEN
698 SIMP_TAC bool_ss [INT_DIVIDES_LMUL, INT_DIVIDES_REFL]) THEN
699 ASM_SIMP_TAC bool_ss [INT_MUL_DIV', INT_DIVIDES_LMUL, INT_DIVIDES_RMUL,
700 INT_INJ] THEN
701 REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN
702 CONV_TAC (AC_CONV(INT_MUL_ASSOC, INT_MUL_COMM))
703 ]
704QED
705
706Theorem gcd1thm:
707 !m n p q. (p * &m + q * &n = 1i) ==> (gcd m n = 1n)
708Proof
709 REPEAT STRIP_TAC THEN
710 Q.SUBGOAL_THEN `&(gcd m n) int_divides (p * &m + q * &n)` ASSUME_TAC
711 THENL [
712 Q.SUBGOAL_THEN `&(gcd m n) int_divides (p * &m)`
713 (REWRITE_TAC o C cons [] o MATCH_MP INT_DIVIDES_LADD) THENL [
714 Q.SPEC_THEN `p` STRIP_ASSUME_TAC INT_NUM_CASES THEN
715 FIRST_X_ASSUM SUBST_ALL_TAC THEN
716 SIMP_TAC bool_ss [INT_NUM_DIVIDES, INT_MUL_CALCULATE,
717 INT_DIVIDES_NEG, INT_MUL_LZERO,
718 ALL_DIVIDES_0] THEN
719 `divides (gcd m n) m` by PROVE_TAC [GCD_IS_GCD, is_gcd_def] THEN
720 PROVE_TAC [DIVIDES_TRANS, DIVIDES_MULT, MULT_COMM],
721
722 Q.SPEC_THEN `q` STRIP_ASSUME_TAC INT_NUM_CASES THEN
723 FIRST_X_ASSUM SUBST_ALL_TAC THEN
724 SIMP_TAC bool_ss [INT_NUM_DIVIDES, INT_MUL_CALCULATE,
725 INT_DIVIDES_NEG, INT_MUL_LZERO,
726 ALL_DIVIDES_0] THEN
727 `divides (gcd m n) n` by PROVE_TAC [GCD_IS_GCD, is_gcd_def] THEN
728 PROVE_TAC [DIVIDES_TRANS, DIVIDES_MULT, MULT_COMM]
729 ],
730
731 FIRST_X_ASSUM SUBST_ALL_TAC THEN
732 FULL_SIMP_TAC bool_ss [INT_DIVIDES_1, INT_EQ_CALCULATE]
733 ]
734QED
735
736Theorem gcd21_thm:
737 !m a x b p q.
738 (p * &a + q * &m = 1i) /\ ~(m = 0) /\ ~(a = 0) ==>
739 (&m int_divides &a * x + b = ?t. x = ~p * b + t * &m)
740Proof
741 REPEAT STRIP_TAC THEN
742 `1 = gcd a m` by PROVE_TAC [gcd1thm] THEN
743 `~(1n = 0)` by ASM_SIMP_TAC arith_ss [] THEN
744 Q.PAT_X_ASSUM `_ = 1i` (ASSUME_TAC o SYM) THEN
745 Q.SPECL_THEN [`m`, `a`, `x`, `b`, `1`, `p`, `q`] MP_TAC gcdthm2 THEN
746 REPEAT (FIRST_X_ASSUM (MP_TAC o SYM)) THEN
747 ASM_SIMP_TAC bool_ss [INT_DIV_1, INT_DIVIDES_1]
748QED
749
750
751Theorem elim_lt_coeffs1:
752 !n m x:int. ~(m = 0) ==> (&n < &m * x = &n / &m < x)
753Proof
754 REPEAT STRIP_TAC THEN
755 ASM_SIMP_TAC bool_ss [INT_DIV] THEN
756 `0 < m` by ASM_SIMP_TAC arith_ss [] THEN
757 POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `n` o MATCH_MP DIVISION) THEN
758 Q.ABBREV_TAC `r = n MOD m` THEN
759 Q.ABBREV_TAC `i = n DIV m` THEN
760 EQ_TAC THEN STRIP_TAC THENL [
761 SPOSE_NOT_THEN (ASSUME_TAC o REWRITE_RULE [INT_NOT_LT]) THEN
762 Q.SUBGOAL_THEN `&m * x <= &m * &i` ASSUME_TAC THENL [
763 ASM_SIMP_TAC arith_ss [INT_LE_CALCULATE, INT_EQ_LMUL, INT_INJ,
764 GSYM lt_justify_multiplication, INT_LT] THEN
765 ASM_SIMP_TAC bool_ss [GSYM INT_LE_CALCULATE],
766 ALL_TAC
767 ] THEN
768 `&n < &i * &m` by PROVE_TAC [INT_LTE_TRANS, INT_MUL_COMM] THEN
769 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC arith_ss [INT_LT, INT_MUL],
770
771 Q.SPEC_THEN `x` STRIP_ASSUME_TAC INT_NUM_CASES THEN
772 FIRST_X_ASSUM SUBST_ALL_TAC THEN
773 FULL_SIMP_TAC arith_ss [INT_LT, INT_INJ, INT_LT_CALCULATE, INT_MUL] THEN
774 `i + 1 <= n'` by ASM_SIMP_TAC arith_ss [] THEN
775 POP_ASSUM (MP_TAC o EQ_MP (Q.SPECL [`i + 1`, `n'`, `PRE m`]
776 MULT_LESS_EQ_SUC)) THEN
777 `~(m = 0)` by ASM_SIMP_TAC arith_ss [] THEN POP_ASSUM MP_TAC THEN
778 SIMP_TAC bool_ss [
779 numLib.ARITH_PROVE ``~(x = 0) ==> (SUC (PRE x) = x)``] THEN
780 Q.SUBGOAL_THEN `i * m = m * i` SUBST1_TAC THENL [
781 CONV_TAC (AC_CONV(MULT_ASSOC, MULT_COMM)),
782 ALL_TAC
783 ] THEN
784 MP_TAC (Q.ASSUME `r:num < m`) THEN
785 SIMP_TAC bool_ss [LEFT_ADD_DISTRIB, MULT_CLAUSES] THEN
786 numLib.ARITH_TAC
787 ]
788QED
789
790Theorem elim_lt_coeffs2:
791 !n m x:int. ~(m = 0) ==>
792 (&m * x < &n = x < if &m int_divides &n then &n / &m
793 else &n / &m + 1)
794Proof
795 REPEAT STRIP_TAC THEN
796 ASM_SIMP_TAC bool_ss [INT_DIV, INT_DIVIDES_MOD0, INT_INJ,
797 INT_MOD] THEN
798 `0 < m` by ASM_SIMP_TAC arith_ss [] THEN
799 POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `n` o MATCH_MP DIVISION) THEN
800 Q.ABBREV_TAC `r = n MOD m` THEN
801 Q.ABBREV_TAC `i = n DIV m` THEN
802 `i * m = m * i` by CONV_TAC (AC_CONV(MULT_ASSOC, MULT_COMM)) THEN
803 POP_ASSUM SUBST_ALL_TAC THEN
804 EQ_TAC THEN COND_CASES_TAC THEN STRIP_TAC THEN
805 REPEAT (FIRST_X_ASSUM SUBST_ALL_TAC) THENL [
806 FULL_SIMP_TAC arith_ss [GSYM INT_MUL] THEN
807 PROVE_TAC [lt_justify_multiplication, INT_LT],
808 FULL_SIMP_TAC arith_ss [GSYM INT_MUL, GSYM INT_ADD] THEN
809 `&m * &i + &r < &m * (&i + 1)` by
810 ASM_SIMP_TAC bool_ss [INT_LDISTRIB, INT_LT_LADD, INT_LT,
811 INT_MUL_RID] THEN
812 `&m * x < &m * (&i + 1)` by PROVE_TAC [INT_LT_TRANS] THEN
813 `0i < &m` by ASM_SIMP_TAC arith_ss [INT_LT] THEN
814 PROVE_TAC [lt_justify_multiplication],
815 REWRITE_TAC [GSYM INT_MUL, GSYM INT_ADD, INT_ADD_RID] THEN
816 PROVE_TAC [lt_justify_multiplication, INT_LT],
817 `x <= &i` by ASM_SIMP_TAC bool_ss [GSYM INT_NOT_LT, not_less] THEN
818 `&m * x <= &m * &i` by
819 (FULL_SIMP_TAC bool_ss [INT_LE_CALCULATE, INT_EQ_LMUL, INT_INJ] THEN
820 ASM_SIMP_TAC arith_ss [INT_LT, GSYM lt_justify_multiplication]) THEN
821 `&m * &i < &(m * i + r)` by
822 ASM_SIMP_TAC arith_ss [INT_LT, INT_MUL] THEN
823 PROVE_TAC [INT_LET_TRANS]
824 ]
825QED
826
827Theorem elim_le_coeffs:
828 !m n x. 0 < m ==> (0 <= m * x + n = 0 <= x + n/m)
829Proof
830 REPEAT STRIP_TAC THEN
831 `~(m = 0) /\ ~(m < 0)` by PROVE_TAC [INT_LT_REFL, INT_LT_ANTISYM] THEN
832 Q.SPEC_THEN `m` MP_TAC INT_DIVISION THEN
833 ASM_SIMP_TAC arith_ss [] THEN
834 DISCH_THEN (Q.SPEC_THEN `n` STRIP_ASSUME_TAC) THEN
835 Q.ABBREV_TAC `q = n / m` THEN POP_ASSUM (K ALL_TAC) THEN
836 Q.ABBREV_TAC `r = n % m` THEN POP_ASSUM (K ALL_TAC) THEN
837 FIRST_X_ASSUM SUBST_ALL_TAC THEN
838 SIMP_TAC arith_ss [INT_ADD_ASSOC, INT_MUL_COMM, GSYM INT_LDISTRIB] THEN
839 EQ_TAC THEN STRIP_TAC THENL [
840 `0 < m * (x + q) + m * 1` by
841 (MATCH_MP_TAC INT_LET_TRANS THEN
842 Q.EXISTS_TAC `m * (x + q) + r` THEN
843 ASM_SIMP_TAC arith_ss [INT_LT_LADD, INT_MUL_RID]) THEN
844 `0 < m * (x + q + 1)` by PROVE_TAC [INT_LDISTRIB] THEN
845 `0 < x + q + 1` by PROVE_TAC [INT_LT_MONO, INT_MUL_RZERO] THEN
846 PROVE_TAC [elim_minus_ones, int_sub, less_to_leq_samel],
847 MATCH_MP_TAC INT_LE_TRANS THEN Q.EXISTS_TAC `m * (x + q)` THEN
848 PROVE_TAC [INT_LE_MONO, INT_MUL_RZERO, INT_LE_ADDR]
849 ]
850QED
851
852Theorem elim_eq_coeffs:
853 !m x y. ~(m = 0) ==>
854 ((&m * x = y) = &m int_divides y /\ (x = y / &m))
855Proof
856 REPEAT STRIP_TAC THEN
857 ASM_SIMP_TAC bool_ss [INT_DIVIDES] THEN EQ_TAC THEN STRIP_TAC THENL [
858 POP_ASSUM (SUBST_ALL_TAC o SYM) THEN CONJ_TAC THENL [
859 PROVE_TAC [INT_MUL_COMM],
860 ALL_TAC
861 ] THEN ONCE_REWRITE_TAC [INT_MUL_COMM] THEN
862 ASM_SIMP_TAC bool_ss [INT_MUL_DIV, INT_INJ, INT_MOD_ID, INT_DIV_ID,
863 INT_MUL_RID],
864 POP_ASSUM SUBST_ALL_TAC THEN POP_ASSUM (SUBST_ALL_TAC o SYM) THEN
865 ASM_SIMP_TAC bool_ss [INT_MUL_DIV, INT_INJ, INT_MOD_ID, INT_DIV_ID,
866 INT_MUL_RID] THEN
867 PROVE_TAC [INT_MUL_COMM]
868 ]
869QED
870
871
872val int_acnorm_ss = SSFRAG{
873 name = SOME "int_acnorm",
874 ac = [(SPEC_ALL INT_ADD_ASSOC, SPEC_ALL INT_ADD_COMM),
875 (SPEC_ALL INT_MUL_ASSOC, SPEC_ALL INT_MUL_COMM)],
876 convs = [], congs = [], dprocs = [], filter = NONE,
877 rewrs = []};
878
879(* lemma 1 from Cooper's paper
880
881 (d = gcd(um, an) = pum + qan) ==>
882 ( m | ax + b /\ n | ux + v =
883 mn | dx + bqn + vpm /\ d | av - ub )
884*)
885Theorem adhoc_lemma[local]:
886 !a b c. a + (b - c) = (a - c) + b:int
887Proof
888 SIMP_TAC (bool_ss ++ int_acnorm_ss) [INT_SUB_CALCULATE]
889QED
890Theorem adhoc_lemma2[local]:
891 !a b c. a - b + c = a + (c - b:int)
892Proof
893 SIMP_TAC (bool_ss ++ int_acnorm_ss) [INT_SUB_CALCULATE]
894QED
895
896
897Theorem cooper_lemma_1:
898 !m n a b u v p q x d.
899 (d = gcd (u * m) (a * n)) /\
900 (&d = p * &u * &m + q * &a * &n) /\
901 ~(m = 0) /\ ~(n = 0) /\ ~(a = 0) /\ ~(u = 0) ==>
902 (&m int_divides &a * x + b /\ &n int_divides &u * x + v =
903 &m * &n int_divides &d * x + v * &m * p + b * &n * q /\
904 &d int_divides &a * v - &u * b)
905Proof
906 REPEAT STRIP_TAC THEN
907 EQ_TAC THEN REPEAT STRIP_TAC THENL [
908 (* m | ax + b /\ n | ux + v ==> mn | dx + vmp + bnq *)
909 `&m * &n int_divides (&a * x + b) * &n` by
910 PROVE_TAC [INT_INJ, INT_DIVIDES_LRMUL] THEN
911 `&m * &n int_divides (&u * x + v) * &m` by
912 PROVE_TAC [INT_INJ, INT_MUL_COMM, INT_DIVIDES_LRMUL] THEN
913 `&m * &n int_divides (&a * x + b) * &n * q` by
914 PROVE_TAC [INT_DIVIDES_LMUL] THEN
915 `&m * &n int_divides (&u * x + v) * &m * p` by
916 PROVE_TAC [INT_DIVIDES_LMUL] THEN
917 `&m * &n int_divides (&a * x + b) * &n * q + (&u * x + v) * &m * p` by
918 PROVE_TAC [INT_DIVIDES_LADD] THEN
919 `&m * &n int_divides &a * x * &n * q + b * &n * q +
920 &u * x * &m * p + v * &m * p` by
921 (POP_ASSUM MP_TAC THEN
922 SIMP_TAC bool_ss [INT_RDISTRIB, INT_ADD_ASSOC]) THEN
923 `&m * &n int_divides (p * &u * &m + q * &a * &n) * x +
924 v * &m * p + b * &n * q` by
925 (POP_ASSUM MP_TAC THEN
926 SIMP_TAC (bool_ss ++ int_acnorm_ss)[INT_LDISTRIB, INT_RDISTRIB]) THEN
927 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC bool_ss [],
928 (* m | ax + b /\ n | ux + v ==> d | av - ub *)
929 `?j. &m * j = &a * x + b` by PROVE_TAC [INT_DIVIDES, INT_MUL_COMM] THEN
930 `?k. &n * k = &u * x + v` by PROVE_TAC [INT_DIVIDES, INT_MUL_COMM] THEN
931 `b = &m * j - &a * x` by
932 PROVE_TAC [INT_EQ_SUB_LADD, INT_ADD_COMM] THEN
933 `v = &n * k - &u * x` by
934 PROVE_TAC [INT_EQ_SUB_LADD, INT_ADD_COMM] THEN
935 `&u * b = &u * &m * j - &u * &a * x` by
936 PROVE_TAC [INT_SUB_LDISTRIB, INT_MUL_ASSOC] THEN
937 `&a * v = &a * &n * k - &a * &u * x` by
938 PROVE_TAC [INT_SUB_LDISTRIB, INT_MUL_ASSOC] THEN
939 `&a * v = &a * &n * k - &u * &a * x` by
940 (POP_ASSUM MP_TAC THEN SIMP_TAC (bool_ss ++ int_acnorm_ss)[]) THEN
941 `&a * v - &u * b = &a * &n * k - &u * &m * j` by
942 ASM_SIMP_TAC bool_ss [INT_SUB_SUB3, INT_SUB_ADD] THEN
943 `&d int_divides &u * &m /\ &d int_divides &a * &n` by
944 PROVE_TAC [is_gcd_def, GCD_IS_GCD, INT_NUM_DIVIDES, INT_MUL] THEN
945 `&d int_divides &u * &m * j /\ &d int_divides &a * &n * k` by
946 PROVE_TAC [INT_DIVIDES_LMUL, INT_MUL_ASSOC] THEN
947 `&d int_divides &a * &n * k - &u * &m * j` by
948 PROVE_TAC [INT_DIVIDES_LSUB] THEN
949 PROVE_TAC [],
950 (* mn | dx + vmp + bnq /\ d | av - ub ==> m | ax + b *)
951 Q.PAT_X_ASSUM `&m * &n int_divides &d * x + v * &m * p + b * &n * q`
952 ASSUME_TAC THEN
953 `&m * &n int_divides &m * p * (&u * x + v) + &n * q * (&a * x + b)` by
954 (POP_ASSUM MP_TAC THEN
955 ASM_SIMP_TAC (bool_ss ++ int_acnorm_ss)
956 [INT_LDISTRIB, INT_RDISTRIB]) THEN
957 `&a * &u * &m * &n int_divides
958 &u * &m * p * (&u * &a * x + &a * v) +
959 &a * &n * q * (&u * &a * x + &u * b)` by
960 (`~(&a * &u = 0)` by PROVE_TAC [INT_ENTIRE, INT_INJ, INT_MUL] THEN
961 `(&a * &u) * (&m * &n) int_divides
962 (&a * &u) * (&m * p * (&u * x + v) + &n * q * (&a * x + b))` by
963 PROVE_TAC [INT_DIVIDES_LRMUL, INT_MUL_COMM] THEN
964 POP_ASSUM MP_TAC THEN
965 SIMP_TAC (bool_ss ++ int_acnorm_ss)[INT_LDISTRIB]) THEN
966 `&a * &n * q = &d - &u * &m * p` by
967 (FULL_SIMP_TAC (bool_ss ++ int_acnorm_ss) [] THEN
968 PROVE_TAC [INT_EQ_SUB_RADD, INT_ADD_COMM]) THEN
969 POP_ASSUM SUBST_ALL_TAC THEN
970 POP_ASSUM (ASSUME_TAC o REWRITE_RULE [INT_SUB_RDISTRIB, adhoc_lemma]) THEN
971 POP_ASSUM (ASSUME_TAC o REWRITE_RULE [GSYM INT_SUB_LDISTRIB,
972 INT_ADD2_SUB2, INT_ADD_LID,
973 INT_SUB_REFL,
974 INT_MUL_RZERO]) THEN
975 `&u * (&a * &m * &n) int_divides
976 &u * (&m * p * (&a * v - &u * b) + &d * (&a * x + b))` by
977 (POP_ASSUM MP_TAC THEN
978 SIMP_TAC (bool_ss ++ int_acnorm_ss) [INT_LDISTRIB]) THEN
979 `&a * &m * &n int_divides
980 &m * p * (&a * v - &u * b) + &d * (&a * x + b)` by
981 PROVE_TAC [INT_DIVIDES_LRMUL, INT_INJ, INT_MUL_COMM] THEN
982 `?k. &d * k = &a * v - &u * b` by
983 PROVE_TAC [INT_DIVIDES, INT_MUL_COMM] THEN
984 `&d int_divides &a * &n` by
985 PROVE_TAC [GCD_IS_GCD, is_gcd_def, INT_MUL, INT_NUM_DIVIDES] THEN
986 `?l. &d * l = &a * &n` by
987 PROVE_TAC [INT_DIVIDES, INT_MUL_COMM] THEN
988 `&a * &m * &n int_divides
989 &d * k * &m * p + &d * (&a * x + b)` by
990 (Q.PAT_X_ASSUM `&a * &m * &n int_divides Y` MP_TAC THEN
991 Q.PAT_X_ASSUM `&d * k = X` SUBST1_TAC THEN
992 SIMP_TAC (bool_ss ++ int_acnorm_ss)[]) THEN
993 `&d * l * &m int_divides
994 &d * k * &m * p + &d * (&a * x + b)` by
995 (POP_ASSUM MP_TAC THEN POP_ASSUM SUBST1_TAC THEN
996 SIMP_TAC (bool_ss ++ int_acnorm_ss)[]) THEN
997 `&m * l int_divides k * &m * p + (&a * x + b)` by
998 (POP_ASSUM MP_TAC THEN
999 `~(&d = 0)` by PROVE_TAC [INT_INJ, GCD_EQ_0, MULT_EQ_0] THEN
1000 REWRITE_TAC [GSYM INT_MUL_ASSOC, GSYM INT_LDISTRIB] THEN
1001 DISCH_THEN (MP_TAC o
1002 CONV_RULE (BINOP_CONV (REWR_CONV INT_MUL_COMM))) THEN
1003 POP_ASSUM MP_TAC THEN
1004 SIMP_TAC (bool_ss ++ int_acnorm_ss) [INT_DIVIDES_LRMUL]) THEN
1005 `&m int_divides k * &m * p + (&a * x + b)` by
1006 PROVE_TAC [INT_DIVIDES_MUL, INT_DIVIDES_TRANS] THEN
1007 `&m int_divides k * &m * p` by
1008 PROVE_TAC [INT_DIVIDES_MUL, INT_MUL_COMM, INT_MUL_ASSOC] THEN
1009 PROVE_TAC [INT_DIVIDES_LADD],
1010 (* mn | dx + vmp + bnq /\ d | av - ub ==> n | ux + v *)
1011 Q.PAT_X_ASSUM `&m * &n int_divides &d * x + v * &m * p + b * &n * q`
1012 ASSUME_TAC THEN
1013 `&m * &n int_divides &m * p * (&u * x + v) + &n * q * (&a * x + b)` by
1014 (POP_ASSUM MP_TAC THEN
1015 ASM_SIMP_TAC (bool_ss ++ int_acnorm_ss)
1016 [INT_LDISTRIB, INT_RDISTRIB]) THEN
1017 `&a * &u * &m * &n int_divides
1018 &u * &m * p * (&u * &a * x + &a * v) +
1019 &a * &n * q * (&u * &a * x + &u * b)` by
1020 (`~(&a * &u = 0)` by PROVE_TAC [INT_ENTIRE, INT_INJ, INT_MUL] THEN
1021 `(&a * &u) * (&m * &n) int_divides
1022 (&a * &u) * (&m * p * (&u * x + v) + &n * q * (&a * x + b))` by
1023 PROVE_TAC [INT_DIVIDES_LRMUL, INT_MUL_COMM] THEN
1024 POP_ASSUM MP_TAC THEN
1025 SIMP_TAC (bool_ss ++ int_acnorm_ss)[INT_LDISTRIB]) THEN
1026 `&u * &m * p = &d - &a * &n * q` by
1027 (FULL_SIMP_TAC (bool_ss ++ int_acnorm_ss) [] THEN
1028 PROVE_TAC [INT_EQ_SUB_RADD, INT_ADD_COMM]) THEN
1029 POP_ASSUM SUBST_ALL_TAC THEN
1030 POP_ASSUM (ASSUME_TAC o REWRITE_RULE [INT_SUB_RDISTRIB, adhoc_lemma2]) THEN
1031 POP_ASSUM (ASSUME_TAC o REWRITE_RULE [GSYM INT_SUB_LDISTRIB,
1032 INT_ADD2_SUB2, INT_ADD_LID,
1033 INT_SUB_REFL,
1034 INT_MUL_RZERO]) THEN
1035 `&a * (&u * &m * &n) int_divides
1036 &a * (&n * q * (&u * b - &a * v) + &d * (&u * x + v))` by
1037 (POP_ASSUM MP_TAC THEN
1038 SIMP_TAC (bool_ss ++ int_acnorm_ss) [INT_LDISTRIB]) THEN
1039 `&u * &m * &n int_divides
1040 &n * q * (&u * b - &a * v) + &d * (&u * x + v)` by
1041 PROVE_TAC [INT_DIVIDES_LRMUL, INT_INJ, INT_MUL_COMM] THEN
1042 `?k. &d * k = &u * b - &a * v` by
1043 PROVE_TAC [INT_DIVIDES, INT_MUL_COMM, INT_DIVIDES_NEG,
1044 INT_NEG_SUB] THEN
1045 `&d int_divides &u * &m` by
1046 PROVE_TAC [GCD_IS_GCD, is_gcd_def, INT_MUL, INT_NUM_DIVIDES] THEN
1047 `?l. &d * l = &u * &m` by
1048 PROVE_TAC [INT_DIVIDES, INT_MUL_COMM] THEN
1049 `&u * &m * &n int_divides
1050 &d * k * &n * q + &d * (&u * x + v)` by
1051 (Q.PAT_X_ASSUM `&u * &m * &n int_divides Y` MP_TAC THEN
1052 Q.PAT_X_ASSUM `&d * k = X` SUBST1_TAC THEN
1053 SIMP_TAC (bool_ss ++ int_acnorm_ss)[]) THEN
1054 `&d * l * &n int_divides
1055 &d * k * &n * q + &d * (&u * x + v)` by
1056 (POP_ASSUM MP_TAC THEN POP_ASSUM SUBST1_TAC THEN
1057 SIMP_TAC (bool_ss ++ int_acnorm_ss)[]) THEN
1058 `&n * l int_divides k * &n * q + (&u * x + v)` by
1059 (POP_ASSUM MP_TAC THEN
1060 `~(&d = 0)` by PROVE_TAC [INT_INJ, GCD_EQ_0, MULT_EQ_0] THEN
1061 REWRITE_TAC [GSYM INT_MUL_ASSOC, GSYM INT_LDISTRIB] THEN
1062 DISCH_THEN (MP_TAC o
1063 CONV_RULE (BINOP_CONV (REWR_CONV INT_MUL_COMM))) THEN
1064 POP_ASSUM MP_TAC THEN
1065 SIMP_TAC (bool_ss ++ int_acnorm_ss) [INT_DIVIDES_LRMUL]) THEN
1066 `&n int_divides k * &n * q + (&u * x + v)` by
1067 PROVE_TAC [INT_DIVIDES_MUL, INT_DIVIDES_TRANS] THEN
1068 `&n int_divides k * &n * q` by
1069 PROVE_TAC [INT_DIVIDES_MUL, INT_MUL_COMM, INT_MUL_ASSOC] THEN
1070 PROVE_TAC [INT_DIVIDES_LADD]
1071 ]
1072QED
1073
1074Definition bmarker_def[nocompute]:
1075 bmarker (b:bool) = b
1076End
1077
1078Theorem bmarker_rewrites:
1079 !p q r. (q /\ bmarker p = bmarker p /\ q) /\
1080 (q /\ (bmarker p /\ r) = bmarker p /\ (q /\ r)) /\
1081 ((bmarker p /\ q) /\ r = bmarker p /\ (q /\ r))
1082Proof
1083 REWRITE_TAC [bmarker_def] THEN tautLib.TAUT_TAC
1084QED
1085
1086Theorem positive_mod_part[local]:
1087 !p q r. 0 < q /\ 0 <= r /\ r < q ==>
1088 ((p * q + r) % q = r)
1089Proof
1090 REPEAT STRIP_TAC THEN MATCH_MP_TAC INT_MOD_UNIQUE THEN
1091 ASM_SIMP_TAC bool_ss [INT_LT_GT] THEN PROVE_TAC []
1092QED
1093
1094val int_ss = srw_ss() ++ numSimps.ARITH_ss
1095val tac1 =
1096 Q.EXISTS_TAC `&n - r` THEN
1097 ASM_SIMP_TAC bool_ss [INT_LE_SUB_LADD, INT_LE_SUB_RADD, move_sub,
1098 INT_LE_LADD] THEN
1099 `0 < r` by FULL_SIMP_TAC bool_ss [INT_LE_LT] THEN
1100 FULL_SIMP_TAC int_ss [GSYM INT_ADD_ASSOC, INT_SUB_ADD2,
1101 less_to_leq_samer, INT_ADD_COMM] THEN
1102 Q.SUBGOAL_THEN `&n + q * &n = (q + 1) * &n` SUBST_ALL_TAC
1103 >- SIMP_TAC bool_ss [INT_ADD_COMM, INT_RDISTRIB, INT_MUL_LID] THEN
1104 ASM_SIMP_TAC int_ss [INT_MOD_COMMON_FACTOR]
1105val tac2 =
1106 STRIP_TAC THEN REPEAT VAR_EQ_TAC THEN
1107 FULL_SIMP_TAC bool_ss [INT_ADD_RID] THEN
1108 POP_ASSUM MP_TAC THEN
1109 `0 <= i` by PROVE_TAC [INT_LE_TRANS, INT_LE_01] THEN
1110 `i < &n` by ASM_SIMP_TAC bool_ss [less_to_leq_samel, GSYM int_sub] THEN
1111 ASM_SIMP_TAC bool_ss [positive_mod_part] THEN
1112 STRIP_TAC THEN VAR_EQ_TAC THEN FULL_SIMP_TAC int_ss []
1113
1114Theorem NOT_INT_DIVIDES:
1115 !c d. ~(c = 0) ==>
1116 (~(c int_divides d) =
1117 ?i. 1 <= i /\ i <= ABS c - 1 /\ c int_divides d + i)
1118Proof
1119 REPEAT GEN_TAC THEN
1120 Q.SPEC_THEN `c` STRIP_ASSUME_TAC INT_NUM_CASES THEN
1121 ASM_SIMP_TAC bool_ss [INT_DIVIDES_NEG, INT_ABS_NUM, INT_ABS_NEG,
1122 INT_NEG_EQ0] THEN
1123 REPEAT STRIP_TAC THEN
1124 ASM_SIMP_TAC bool_ss [INT_DIVIDES_MOD0] THEN
1125 FIRST_ASSUM (MP_TAC o Q.SPEC `d` o MATCH_MP INT_DIVISION) THEN
1126 ASM_SIMP_TAC int_ss [INT_LT] THEN STRIP_TAC THEN
1127 Q.ABBREV_TAC `q = d / &n` THEN POP_ASSUM (K ALL_TAC) THEN
1128 Q.ABBREV_TAC `r = d % &n` THEN POP_ASSUM (K ALL_TAC) THEN
1129 EQ_TAC THEN STRIP_TAC THENL [tac1,tac2,tac1,tac2]
1130QED
1131
1132Theorem NOT_INT_DIVIDES_POS:
1133 !n d. ~(n = 0) ==>
1134 (~(&n int_divides d) =
1135 ?i. (1 <= i /\ i <= &n - 1) /\ &n int_divides d + i)
1136Proof
1137 REPEAT STRIP_TAC THEN
1138 `~(&n = 0)` by ASM_SIMP_TAC bool_ss [INT_INJ] THEN
1139 ASM_SIMP_TAC bool_ss [NOT_INT_DIVIDES, INT_ABS_NUM, CONJ_ASSOC]
1140QED
1141
1142Theorem le_context_rwt1:
1143 0 <= c + x ==> x <= y ==> (0 <= c + y = T)
1144Proof
1145 PROVE_TAC [INT_LE_LADD, INT_ADD_COMM, INT_ADD_ASSOC, INT_LE_ADD2,
1146 INT_ADD_LID]
1147QED
1148
1149Theorem le_context_rwt2:
1150 0 <= c + x ==> y < ~x ==> (0 <= ~c + y = F)
1151Proof
1152 REWRITE_TAC [] THEN REPEAT STRIP_TAC THEN
1153 `c <= y` by PROVE_TAC [le_move_all_right, INT_ADD_COMM] THEN
1154 `~x <= c` by PROVE_TAC [INT_NEGNEG, le_move_all_right, INT_ADD_COMM] THEN
1155 PROVE_TAC [INT_LE_TRANS, INT_NOT_LE]
1156QED
1157
1158Theorem le_context_rwt3:
1159 0 <= c + x ==> x < y ==> ((0 = c + y) = F)
1160Proof
1161 REWRITE_TAC [] THEN REPEAT STRIP_TAC THEN
1162 PROVE_TAC [INT_LE_LADD, INT_LET_TRANS, INT_LT_REFL]
1163QED
1164
1165Theorem le_context_rwt4:
1166 0 <= c + x ==> x < ~y ==> ((0 = ~c + y) = F)
1167Proof
1168 REWRITE_TAC [] THEN REPEAT STRIP_TAC THEN
1169 POP_ASSUM (SUBST_ALL_TAC o
1170 REWRITE_RULE [INT_NEG_0, INT_NEG_ADD, INT_NEGNEG] o
1171 AP_TERM ``$~ : int -> int``) THEN
1172 PROVE_TAC [INT_LE_LADD, INT_LET_TRANS, INT_LT_REFL]
1173QED
1174
1175Theorem le_context_rwt5:
1176 0 <= c + x ==> (0 <= ~c + ~x = (0 = c + x))
1177Proof
1178 STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
1179 POP_ASSUM (ASSUME_TAC o REWRITE_RULE [INT_NEG_0, INT_NEG_ADD, INT_NEGNEG] o
1180 CONV_RULE (REWR_CONV (GSYM INT_LE_NEG))) THEN
1181 IMP_RES_TAC INT_LE_ANTISYM,
1182 POP_ASSUM (SUBST_ALL_TAC o
1183 REWRITE_RULE [INT_NEG_0, INT_NEG_ADD, INT_NEGNEG] o
1184 AP_TERM ``$~ : int -> int``) THEN
1185 REWRITE_TAC [INT_LE_REFL]
1186 ]
1187QED
1188
1189
1190Theorem eq_context_rwt1:
1191 (0i = c + x) ==> (0 <= c + y = x <= y)
1192Proof
1193 STRIP_TAC THEN ASM_REWRITE_TAC [INT_LE_LADD]
1194QED
1195
1196Theorem eq_context_rwt2:
1197 (0 = c + x) ==> (0 <= ~c + y = ~x <= y)
1198Proof
1199 STRIP_TAC THEN
1200 POP_ASSUM (ASSUME_TAC o REWRITE_RULE [INT_NEG_0, INT_NEG_ADD] o
1201 AP_TERM ``$~ : int -> int``) THEN
1202 ASM_REWRITE_TAC [INT_LE_LADD]
1203QED
1204
1205val _ = hide "bmarker";