OmegaScript.sml
1(* ----------------------------------------------------------------------
2 Theory development that underlies the Omega decision procedure.
3 Michael Norrish, November 2001
4 ---------------------------------------------------------------------- *)
5
6Theory Omega
7Ancestors
8 integer list[qualified] int_arith[qualified]
9Libs
10 simpLib boolSimps BasicProvers TotalDefn CooperMath
11
12val _ = ParseExtras.temp_loose_equality()
13
14val ARITH_ss = numSimps.ARITH_ss
15
16val FORALL_PROD = pairTheory.FORALL_PROD;
17
18Definition MAP2_def:
19 (MAP2 pad f [] [] = []) /\
20 (MAP2 pad f [] (y::ys) = (f pad y) :: MAP2 pad f [] ys) /\
21 (MAP2 pad f (x::xs) [] = (f x pad) :: MAP2 pad f xs []) /\
22 (MAP2 pad f (x::xs) (y::ys) = f x y :: MAP2 pad f xs ys)
23End
24
25Theorem MAP2_zero_ADD:
26 !xs. (MAP2 0i $+ [] xs = xs) /\
27 (MAP2 0 $+ xs [] = xs)
28Proof
29 Induct THEN ASM_SIMP_TAC bool_ss [MAP2_def, INT_ADD_LID, INT_ADD_RID]
30QED
31
32Definition sumc_def:
33 (sumc _ [] = 0i) /\
34 (sumc [] _ = 0) /\
35 (sumc (c::cs) (v::vs) = c * v + sumc cs vs)
36End
37
38val sumc_ind = DB.fetch "-" "sumc_ind";
39
40Theorem sumc_thm:
41 !cs vs c v.
42 (sumc [] vs = 0) /\
43 (sumc cs [] = 0) /\
44 (sumc (c::cs) (v::vs) = c * v + sumc cs vs)
45Proof
46 HO_MATCH_MP_TAC sumc_ind THEN SIMP_TAC bool_ss [sumc_def]
47QED
48
49Theorem sumc_ADD:
50 !cs vs ds. sumc cs vs + sumc ds vs =
51 sumc (MAP2 0 $+ cs ds) vs
52Proof
53 HO_MATCH_MP_TAC sumc_ind THEN REPEAT STRIP_TAC THENL [
54 SIMP_TAC bool_ss [sumc_thm, MAP2_def, INT_ADD_LID],
55 SIMP_TAC bool_ss [sumc_thm, MAP2_def, INT_ADD_LID,
56 MAP2_zero_ADD],
57 Cases_on `ds` THEN
58 SIMP_TAC bool_ss [sumc_thm, MAP2_zero_ADD, INT_ADD_RID, MAP2_def,
59 INT_RDISTRIB] THEN
60 POP_ASSUM (fn th => REWRITE_TAC [GSYM th]) THEN
61 CONV_TAC (AC_CONV(INT_ADD_ASSOC, INT_ADD_COMM))
62 ]
63QED
64
65val MULT_AC = AC INT_MUL_COMM INT_MUL_ASSOC
66val ADD_AC = AC INT_ADD_COMM INT_ADD_ASSOC
67Theorem sumc_MULT:
68 !cs vs f. f * sumc cs vs = sumc (MAP (\x. f * x) cs) vs
69Proof
70 Induct THEN SRW_TAC [][sumc_thm] THEN
71 Cases_on `vs` THEN
72 SRW_TAC [][sumc_thm, INT_LDISTRIB, MULT_AC]
73QED
74
75Theorem sumc_singleton:
76 !f (c:int). sumc (MAP f [c]) [1] = f c
77Proof
78 REWRITE_TAC [INT_ADD_RID, sumc_def, listTheory.MAP,
79 INT_MUL_RID]
80QED
81Theorem sumc_nonsingle:
82 !f cs (c:int) v vs. sumc (MAP f (c::cs)) (v::vs) =
83 f c * v + sumc (MAP f cs) vs
84Proof
85 REWRITE_TAC [sumc_def, listTheory.MAP]
86QED
87
88Definition modhat_def:
89 modhat x y = x - y * ((2 * x + y) / (2 * y))
90End
91
92Theorem MAP_MAP[local]:
93 !l f g. MAP f (MAP g l) = MAP (f o g) l
94Proof
95 Induct THEN SRW_TAC [][combinTheory.o_THM]
96QED
97
98Theorem MAP2_MAP[local]:
99 !l f g pad. MAP2 pad f (MAP g l) l = MAP (\x. f (g x) x) l
100Proof
101 Induct THEN SRW_TAC [][MAP2_def]
102QED
103
104Theorem MAP_MAP2[local]:
105 !l f g h. MAP (\x. f (g x) (h x)) l = MAP2 0i f (MAP g l) (MAP h l)
106Proof
107 Induct THEN SRW_TAC [][MAP2_def]
108QED
109
110Theorem MAP_ID[local]:
111 !l. MAP (\x.x) l = l
112Proof Induct THEN SRW_TAC [][]
113QED
114
115val _ = print "Proving eliminability of equalities\n";
116
117Theorem equality_removal0[local]:
118 !c x cs vs.
119 0 < c /\ (c * x + sumc cs vs = 0) ==>
120 ?s. x = ~(c + 1) * s + sumc (MAP (\x. modhat x (c + 1)) cs) vs
121Proof
122 REPEAT STRIP_TAC THEN
123 ONCE_REWRITE_TAC [INT_ADD_COMM] THEN
124 SIMP_TAC (srw_ss()) [GSYM int_sub, INT_EQ_SUB_LADD, GSYM INT_NEG_LMUL] THEN
125 CONV_TAC (BINDER_CONV (LHS_CONV (REWR_CONV INT_ADD_COMM))) THEN
126 SIMP_TAC (srw_ss()) [GSYM INT_EQ_SUB_LADD] THEN
127 SIMP_TAC (srw_ss()) [int_sub] THEN
128 Q_TAC SUFF_TAC
129 `(c + 1) int_divides sumc (MAP (\x. modhat x (c + 1)) cs) vs + ~x` THEN1
130 PROVE_TAC [INT_DIVIDES, INT_MUL_COMM] THEN
131 Q_TAC SUFF_TAC
132 `c * (c + 1) int_divides
133 c * (sumc (MAP (\x. modhat x (c+ 1)) cs) vs + ~x)` THEN1
134 PROVE_TAC [INT_DIVIDES_MUL_BOTH, INT_LT_REFL] THEN
135 CONV_TAC (RAND_CONV (SIMP_CONV bool_ss [INT_LDISTRIB, GSYM INT_NEG_RMUL,
136 sumc_MULT, MAP_MAP,
137 combinTheory.o_DEF])) THEN
138 `~(c * x) = sumc cs vs` by
139 FULL_SIMP_TAC (srw_ss()) [GSYM INT_EQ_SUB_LADD] THEN
140 ASM_SIMP_TAC (srw_ss()) [sumc_ADD, MAP2_MAP, modhat_def, int_sub] THEN
141 CONV_TAC (RAND_CONV (SIMP_CONV (srw_ss()) [INT_LDISTRIB,
142 GSYM INT_ADD_ASSOC])) THEN
143 `(\x. c * x + (c * ~((c + 1) * ((2 * x + (c + 1)) / (2 * c + 2))) + x)) =
144 (\x. (c + 1) * (x + ~(c * ((2 * x + (c + 1)) / (2 * c + 2)))))` by
145 SIMP_TAC (srw_ss())
146 [INT_LDISTRIB, INT_RDISTRIB, INT_NEG_ADD, GSYM INT_NEG_RMUL,
147 GSYM INT_NEG_LMUL, MULT_AC, ADD_AC] THEN
148 POP_ASSUM SUBST_ALL_TAC THEN
149 `(\x. (c + 1) * (x + ~(c * ((2 * x + (c + 1)) / (2 * c + 2))))) =
150 (\x. (c + 1) * x) o
151 (\x. x + ~(c * ((2 * x + (c + 1)) / (2 * c + 2))))` by
152 SIMP_TAC (srw_ss()) [combinTheory.o_DEF] THEN
153 POP_ASSUM SUBST_ALL_TAC THEN
154 REWRITE_TAC [GSYM MAP_MAP, GSYM sumc_MULT] THEN
155 `~(c + 1 = 0)` by (STRIP_TAC THEN
156 FULL_SIMP_TAC (srw_ss()) [GSYM INT_EQ_SUB_LADD]) THEN
157 Q_TAC SUFF_TAC
158 `c int_divides
159 sumc (MAP (\x. x + ~(c * ((2 * x + (c + 1)) / (2 * c + 2)))) cs) vs`
160 THEN1 PROVE_TAC [INT_DIVIDES_MUL_BOTH, INT_MUL_COMM] THEN
161
162 Q.SPECL_THEN [`cs`, `$int_add`, `\x.x`] (MP_TAC o SIMP_RULE bool_ss [])
163 (INST_TYPE [alpha |-> ``:int``, beta |-> ``:int``]
164 MAP_MAP2) THEN
165 DISCH_THEN (fn th => SIMP_TAC (srw_ss()) [th, GSYM sumc_ADD, MAP_ID]) THEN
166 `(\x. ~(c * ((2 * x + (c + 1)) / (2 * c + 2)))) =
167 (\x. c * x) o (\x. ~((2 * x + (c + 1)) / (2 * c + 2)))` by
168 SIMP_TAC (srw_ss()) [combinTheory.o_DEF, INT_NEG_RMUL] THEN
169 POP_ASSUM SUBST_ALL_TAC THEN
170 REWRITE_TAC [GSYM MAP_MAP, GSYM sumc_MULT] THEN
171 Q_TAC SUFF_TAC `c int_divides sumc cs vs` THEN1
172 PROVE_TAC [INT_DIVIDES_LADD, INT_DIVIDES_MUL] THEN
173 PROVE_TAC [INT_DIVIDES, INT_MUL_COMM, INT_DIVIDES_NEG, INT_NEG_LMUL]
174QED
175
176Theorem equality_removal:
177 !c x cs vs.
178 0 < c ==>
179 ((0 = c * x + sumc cs vs) =
180 ?s. (x = ~(c + 1) * s + sumc (MAP (\x. modhat x (c + 1)) cs) vs) /\
181 (0 = c * x + sumc cs vs))
182Proof
183 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THEN SRW_TAC [][] THEN
184 MATCH_MP_TAC equality_removal0 THEN SRW_TAC [][]
185QED
186
187val _ = print "Proving eliminability of quantifiers\n"
188Definition evalupper_def:
189 (evalupper (x:int) [] = T) /\
190 (evalupper x ((c,y) :: cs) = &c * x <= y /\ evalupper x cs)
191End
192Definition evallower_def:
193 (evallower (x:int) [] = T) /\
194 (evallower x ((c,y) :: cs) = y <= &c * x /\ evallower x cs)
195End
196
197Theorem lt_mono[local]:
198 !n (x:int) y. 0 < n ==> (&n * x < & n * y = x < y)
199Proof
200 REPEAT STRIP_TAC THEN
201 CONV_TAC (BINOP_CONV (LAND_CONV (REWR_CONV (GSYM INT_ADD_LID)))) THEN
202 REWRITE_TAC [GSYM INT_LT_SUB_LADD, GSYM INT_SUB_LDISTRIB] THEN
203 SRW_TAC [ARITH_ss][INT_MUL_SIGN_CASES]
204QED
205
206Theorem le_mono[local]:
207 !n (x:int) y. 0 < n ==> (&n * x <= & n * y = x <= y)
208Proof
209 REPEAT STRIP_TAC THEN
210 CONV_TAC (BINOP_CONV (LAND_CONV (REWR_CONV (GSYM INT_ADD_LID)))) THEN
211 REWRITE_TAC [GSYM INT_LT_SUB_LADD, GSYM INT_SUB_LDISTRIB] THEN
212 SRW_TAC [ARITH_ss][INT_MUL_SIGN_CASES, INT_LE_LT, lt_mono]
213QED
214
215Theorem less_exists[local]:
216 !p:int q. p < q = ?m. (q = p + m) /\ 0 < m
217Proof
218 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
219 Q.EXISTS_TAC `q - p` THEN
220 SRW_TAC [][INT_EQ_SUB_LADD, INT_LT_SUB_LADD],
221 SRW_TAC [][]
222 ]
223QED
224
225Theorem ile_mono[local]:
226 !n x y. 0i < n ==> (n * x <= n * y = x <= y)
227Proof
228 REPEAT STRIP_TAC THEN
229 `?m. n = &m` by PROVE_TAC [NUM_POSINT_EXISTS, INT_LE_LT] THEN
230 FULL_SIMP_TAC (srw_ss()) [INT_LT, le_mono]
231QED
232Theorem ilt_mono[local]:
233 !n x y. 0i < n ==> (n * x < n * y = x < y)
234Proof
235 REPEAT STRIP_TAC THEN
236 `?m. n = &m` by PROVE_TAC [NUM_POSINT_EXISTS, INT_LE_LT] THEN
237 FULL_SIMP_TAC (srw_ss()) [lt_mono]
238QED
239
240Theorem div_le[local]:
241 !c x y:int. 0 < c ==> (c * x <= y = x <= y / c)
242Proof
243 REPEAT STRIP_TAC THEN
244 `~(c = 0) /\ ~(c < 0)` by PROVE_TAC [INT_LT_REFL, INT_LT_ANTISYM] THEN
245 Q.SPEC_THEN `c` MP_TAC INT_DIVISION THEN SRW_TAC [][] THEN
246 POP_ASSUM (Q.SPEC_THEN `y` STRIP_ASSUME_TAC) THEN
247 Q.ABBREV_TAC `q = y / c` THEN POP_ASSUM (K ALL_TAC) THEN
248 Q.ABBREV_TAC `r = y % c` THEN POP_ASSUM (K ALL_TAC) THEN SRW_TAC [][] THEN
249 EQ_TAC THEN STRIP_TAC THENL [
250 SPOSE_NOT_THEN (ASSUME_TAC o REWRITE_RULE [INT_NOT_LE]) THEN
251 `?i. (x = q + i) /\ 0 < i` by PROVE_TAC [less_exists] THEN
252 FIRST_X_ASSUM SUBST_ALL_TAC THEN
253 FULL_SIMP_TAC (srw_ss()) [INT_LDISTRIB, MULT_AC] THEN
254 `c * i < c` by PROVE_TAC [INT_LET_TRANS] THEN
255 `i < 1` by PROVE_TAC [ilt_mono, INT_MUL_RID] THEN
256 PROVE_TAC [INT_DISCRETE, INT_ADD_LID],
257 MATCH_MP_TAC INT_LE_TRANS THEN Q.EXISTS_TAC `c * q` THEN
258 SRW_TAC [][ile_mono, MULT_AC]
259 ]
260QED
261
262Theorem smaller_satisfies_uppers:
263 !uppers x y. evalupper x uppers /\ y < x ==> evalupper y uppers
264Proof
265 Induct THEN ASM_SIMP_TAC (srw_ss()) [FORALL_PROD, evalupper_def] THEN
266 REVERSE (REPEAT STRIP_TAC) THEN1 PROVE_TAC [] THEN
267 `(p_1 = 0) \/ 0 < p_1` by SRW_TAC [ARITH_ss][] THEN1
268 (POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC (srw_ss())[]) THEN
269 PROVE_TAC [INT_LET_TRANS, lt_mono, INT_LE_LT]
270QED
271
272Theorem bigger_satisfies_lowers:
273 !lowers x y. evallower x lowers /\ x < y ==> evallower y lowers
274Proof
275 Induct THEN SRW_TAC [][evallower_def] THEN
276 Cases_on `h` THEN FULL_SIMP_TAC (srw_ss()) [evallower_def] THEN
277 Q_TAC SUFF_TAC `r <= &q * y` THEN1 PROVE_TAC [] THEN
278 `(q = 0) \/ 0 < q` by SRW_TAC [ARITH_ss][]
279 THEN1 FULL_SIMP_TAC (srw_ss())[] THEN
280 PROVE_TAC [INT_LET_TRANS, lt_mono, INT_LE_LT]
281QED
282
283Theorem LE_SIGN_CASES[local]:
284 !x y:int. 0 <= x * y = 0 <= x /\ 0 <= y \/ x <= 0 /\ y <= 0
285Proof
286 REWRITE_TAC [INT_LE_LT, INT_MUL_SIGN_CASES, INT_ENTIRE,
287 Q.ISPEC `0i` EQ_SYM_EQ] THEN
288 REPEAT GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] THEN
289 PROVE_TAC [INT_LT_NEGTOTAL, INT_NEG_GT0]
290QED
291
292Theorem LE_LT1[local]:
293 !x y. x <= y = x < y + 1
294Proof
295 REPEAT GEN_TAC THEN EQ_TAC THEN1 REWRITE_TAC [INT_LT_ADD1] THEN
296 Q.SPECL_THEN [`y`, `x`] ASSUME_TAC
297 (REWRITE_RULE [DE_MORGAN_THM] INT_DISCRETE) THEN
298 REWRITE_TAC [IMP_DISJ_THM, GSYM INT_NOT_LT] THEN PROVE_TAC []
299QED
300
301Theorem M_LE_XM[local]:
302 !m x. m <= m * x = 0 <= m /\ 0 < x \/ m <= 0 /\ x <= 1
303Proof
304 REPEAT GEN_TAC THEN
305 CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV (GSYM INT_MUL_RID) THENC
306 REWR_CONV (GSYM INT_ADD_LID)))) THEN
307 REWRITE_TAC [GSYM INT_LE_SUB_LADD, GSYM INT_SUB_LDISTRIB,
308 LE_SIGN_CASES] THEN
309 SRW_TAC [] [INT_LE_SUB_LADD, INT_LE_SUB_RADD] THEN
310 EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] THEN
311 FULL_SIMP_TAC (srw_ss()) [LE_LT1]
312QED
313
314Definition fst_nzero_def: fst_nzero x = 0n < FST x
315End
316Definition fst1_def: fst1 x = (FST x = 1n)
317End
318
319val _ = augment_srw_ss [rewrites [fst1_def, fst_nzero_def]]
320
321Theorem onlylowers_satisfiable:
322 !lowers. EVERY fst_nzero lowers ==> ?x. evallower x lowers
323Proof
324 Induct THEN SRW_TAC [][evallower_def] THEN
325 Cases_on `h` THEN
326 FULL_SIMP_TAC (srw_ss()) [evallower_def] THEN
327 Q.EXISTS_TAC `if x < r / &q + 1 then r / &q + 1 else x` THEN
328 MP_TAC (Q.SPEC `&q` INT_DIVISION) THEN
329 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss)[] THEN
330 DISCH_THEN (Q.SPEC_THEN `r` STRIP_ASSUME_TAC) THEN
331 Q.ABBREV_TAC `rdivq = r / &q` THEN
332 Q.ABBREV_TAC `rmodq = r % &q` THEN
333 COND_CASES_TAC THENL [
334 ASM_SIMP_TAC(srw_ss() ++ ARITH_ss) [INT_LDISTRIB, INT_MUL_COMM] THEN
335 PROVE_TAC [bigger_satisfies_lowers],
336 FULL_SIMP_TAC (srw_ss())[INT_NOT_LT] THEN
337 MATCH_MP_TAC INT_LE_TRANS THEN Q.EXISTS_TAC `rdivq * &q + &q` THEN
338 ASM_SIMP_TAC (srw_ss()) [INT_LT_IMP_LE] THEN
339 `&q * (rdivq + 1) <= &q * x` by PROVE_TAC [le_mono] THEN
340 POP_ASSUM MP_TAC THEN
341 SIMP_TAC (srw_ss() ++ ARITH_ss) [INT_LDISTRIB, INT_MUL_COMM]
342 ]
343QED
344
345Theorem onlyuppers_satisfiable:
346 !uppers. EVERY fst_nzero uppers ==> ?x. evalupper x uppers
347Proof
348 Induct THEN ASM_SIMP_TAC (srw_ss()) [FORALL_PROD, evalupper_def] THEN
349 CONV_TAC (RENAME_VARS_CONV ["c", "L"]) THEN REPEAT STRIP_TAC THEN
350 `?y. evalupper y uppers` by PROVE_TAC [] THEN
351 ASM_SIMP_TAC (srw_ss()) [div_le] THEN
352 Q.EXISTS_TAC `if y < L / &c then y else L / &c` THEN COND_CASES_TAC THEN
353 FULL_SIMP_TAC (srw_ss()) [INT_NOT_LT, INT_LE_LT] THEN
354 PROVE_TAC [smaller_satisfies_uppers]
355QED
356
357Definition rshadow_row_def:
358 (rshadow_row (upperc, (uppery:int)) [] = T) /\
359 (rshadow_row (upperc, uppery) ((lowerc, lowery) :: rs) =
360 (&upperc * lowery <= &lowerc * uppery) /\
361 rshadow_row (upperc, uppery) rs)
362End
363
364Definition real_shadow_def:
365 (real_shadow [] lowers = T) /\
366 (real_shadow (upper::ls) lowers =
367 rshadow_row upper lowers /\ real_shadow ls lowers)
368End
369
370Theorem rshadow_row_FOLDL[local]:
371 !lowers lc ly.
372 rshadow_row (lc,ly) lowers =
373 FOLDL (\a r. &lc * SND r <= &(FST r) * ly /\ a) T lowers
374Proof
375 CONV_TAC (STRIP_QUANT_CONV
376 (LHS_CONV (REWR_CONV (tautLib.TAUT_PROVE ``p = T /\ p``)))) THEN
377 Q.SPEC_TAC (`T`, `acc`) THEN CONV_TAC SWAP_VARS_CONV THEN
378 Induct THEN SIMP_TAC (srw_ss())[rshadow_row_def, FORALL_PROD] THEN
379 POP_ASSUM (fn th => REWRITE_TAC [GSYM th]) THEN PROVE_TAC []
380QED
381
382Theorem singleton_real_shadow:
383 !c L x.
384 &c * x <= L /\ 0 < c ==>
385 !lowers.
386 EVERY fst_nzero lowers /\ evallower x lowers ==>
387 rshadow_row (c,L) lowers
388Proof
389 REPEAT GEN_TAC THEN STRIP_TAC THEN
390 Induct THEN ASM_SIMP_TAC (srw_ss()) [evallower_def, rshadow_row_def,
391 FORALL_PROD] THEN
392 CONV_TAC (RENAME_VARS_CONV ["rc", "ry"]) THEN
393 REPEAT STRIP_TAC THEN
394 `&c * ry <= &c * (&rc * x)` by PROVE_TAC [le_mono] THEN
395 `&rc * (&c * x) <= &rc * L` by PROVE_TAC [le_mono] THEN
396 `&c * (&rc * x) <= &rc * L` by PROVE_TAC [INT_MUL_COMM, INT_MUL_ASSOC] THEN
397 PROVE_TAC [INT_LE_TRANS]
398QED
399
400Theorem real_shadow_revimp_uppers1:
401 !uppers lowers L x.
402 rshadow_row (1, L) lowers /\ evallower x lowers /\
403 evalupper x uppers /\ EVERY fst_nzero lowers /\
404 EVERY fst1 uppers ==>
405 ?x. x <= L /\ evalupper x uppers /\ evallower x lowers
406Proof
407 Induct THENL [
408 SIMP_TAC (srw_ss())[evalupper_def] THEN
409 Induct THENL [
410 SRW_TAC [][rshadow_row_def, evallower_def] THEN PROVE_TAC [INT_LE_REFL],
411 ASM_SIMP_TAC (srw_ss()) [rshadow_row_def, evallower_def,
412 FORALL_PROD] THEN
413 PROVE_TAC [bigger_satisfies_lowers, INT_LE_LT, INT_LE_REFL]
414 ],
415 SIMP_TAC (srw_ss())[FORALL_PROD, evalupper_def] THEN
416 REPEAT STRIP_TAC THEN
417 `?y. y <= L /\ evalupper y uppers /\ evallower y lowers` by PROVE_TAC [] THEN
418 Q.EXISTS_TAC `if x < y then x else y` THEN
419 COND_CASES_TAC THEN ASM_SIMP_TAC (srw_ss()) [] THENL [
420 PROVE_TAC [INT_LTE_TRANS, INT_LE_LT],
421 PROVE_TAC [INT_NOT_LT, INT_LE_TRANS]
422 ]
423 ]
424QED
425
426Theorem real_shadow_revimp_lowers1:
427 !uppers lowers c L x.
428 0 < c /\ rshadow_row (c, L) lowers /\ evalupper x uppers /\
429 evallower x lowers /\ EVERY fst_nzero uppers /\
430 EVERY fst1 lowers ==>
431 ?x. &c * x <= L /\ evalupper x uppers /\ evallower x lowers
432Proof
433 Induct THENL [
434 SIMP_TAC (srw_ss())[evalupper_def] THEN
435 Induct THENL [
436 SRW_TAC [][rshadow_row_def, evallower_def] THEN
437 Q.EXISTS_TAC `L / &c` THEN
438 Q.SPEC_THEN `&c` MP_TAC INT_DIVISION THEN
439 SRW_TAC [ARITH_ss][] THEN
440 POP_ASSUM (Q.SPEC_THEN `L` STRIP_ASSUME_TAC) THEN
441 Q.ABBREV_TAC `Ldivc = L / &c` THEN
442 Q.ABBREV_TAC `Lmodc = L % &c` THEN
443 ASM_SIMP_TAC (srw_ss())[INT_MUL_COMM],
444 ASM_SIMP_TAC (srw_ss())[FORALL_PROD, rshadow_row_def,
445 evallower_def] THEN
446 REPEAT STRIP_TAC THEN
447 `?y. &c * y <= L /\ evallower y lowers` by PROVE_TAC[] THEN
448 Q.EXISTS_TAC `if y < p_2 then p_2 else y` THEN
449 COND_CASES_TAC THEN ASM_SIMP_TAC (srw_ss())[] THENL [
450 PROVE_TAC [bigger_satisfies_lowers],
451 PROVE_TAC [INT_NOT_LT]
452 ]
453 ],
454 SIMP_TAC (srw_ss()) [FORALL_PROD, evalupper_def] THEN
455 CONV_TAC (RENAME_VARS_CONV ["c1", "L1"]) THEN
456 REPEAT STRIP_TAC THEN
457 `?y. &c * y <= L /\ evalupper y uppers /\ evallower y lowers`
458 by PROVE_TAC[] THEN
459 Q.EXISTS_TAC `if x < y then x else y` THEN COND_CASES_TAC THEN
460 ASM_SIMP_TAC (srw_ss())[] THENL [
461 `&c * x < &c * y` by PROVE_TAC [lt_mono] THEN
462 PROVE_TAC [INT_LTE_TRANS, INT_LE_LT],
463 `&c1 * y <= &c1 * x` by PROVE_TAC [le_mono, INT_NOT_LT] THEN
464 PROVE_TAC [INT_LE_TRANS]
465 ]
466 ]
467QED
468
469val lemma =
470 SIMP_RULE bool_ss [AND_IMP_INTRO, GSYM RIGHT_FORALL_IMP_THM]
471 singleton_real_shadow
472
473Theorem real_shadow_always_implied:
474 !uppers lowers x.
475 evalupper x uppers /\ evallower x lowers /\
476 EVERY fst_nzero uppers /\ EVERY fst_nzero lowers ==>
477 real_shadow uppers lowers
478Proof
479 Induct THEN ASM_SIMP_TAC (srw_ss())[evalupper_def, real_shadow_def,
480 FORALL_PROD] THEN
481 PROVE_TAC [lemma]
482QED
483
484val IMP_AND_THM =
485 tautLib.TAUT_PROVE ``!p q r. p ==> q /\ r = (p ==> q) /\ (p ==> r)``
486
487val _ = print "Proving exact shadow case\n"
488Theorem exact_shadow_case:
489 !uppers lowers.
490 EVERY fst_nzero uppers /\ EVERY fst_nzero lowers ==>
491 (EVERY fst1 uppers \/ EVERY fst1 lowers) ==>
492 ((?x. evalupper x uppers /\ evallower x lowers) =
493 real_shadow uppers lowers)
494Proof
495 SIMP_TAC (srw_ss()) [EQ_IMP_THM, IMP_AND_THM, FORALL_AND_THM] THEN
496 REPEAT CONJ_TAC THENL [
497 PROVE_TAC [real_shadow_always_implied],
498 (* "reverse" implication case *)
499 SIMP_TAC (srw_ss()) [DISJ_IMP_THM, FORALL_AND_THM, IMP_AND_THM] THEN
500 CONJ_TAC THENL [
501 (* uppers all one *)
502 Induct THENL [
503 SRW_TAC [][evalupper_def, real_shadow_def, onlylowers_satisfiable],
504 SIMP_TAC (srw_ss()) [evalupper_def, real_shadow_def,
505 FORALL_PROD] THEN
506 SRW_TAC [][] THEN
507 FIRST_X_ASSUM (Q.SPECL_THEN [`lowers`] MP_TAC) THEN
508 ASM_SIMP_TAC (srw_ss())[] THEN STRIP_TAC THEN
509 PROVE_TAC [real_shadow_revimp_uppers1]
510 ],
511 (* lowers all one *)
512 Induct THENL [
513 SRW_TAC [][evalupper_def, real_shadow_def, onlylowers_satisfiable],
514 SIMP_TAC (srw_ss()) [evalupper_def, real_shadow_def,
515 FORALL_PROD] THEN
516 REPEAT STRIP_TAC THEN FULL_SIMP_TAC (srw_ss())[] THEN
517 FIRST_X_ASSUM (Q.SPECL_THEN [`lowers`] MP_TAC) THEN
518 ASM_SIMP_TAC (srw_ss())[] THEN
519 PROVE_TAC [real_shadow_revimp_lowers1]
520 ]
521 ]
522 ]
523QED
524
525Definition dark_shadow_cond_row_def:
526 (dark_shadow_cond_row (c,L:int) [] = T) /\
527 (dark_shadow_cond_row (c,L) ((d,R)::t) =
528 ~(?i. &c * &d * i < &c * R /\ &c * R <= &d * L /\
529 &d * L < &c * &d * (i + 1)) /\ dark_shadow_cond_row (c,L) t)
530End
531
532Definition dark_shadow_condition_def:
533 (dark_shadow_condition [] lowers = T) /\
534 (dark_shadow_condition ((c,L)::uppers) lowers =
535 dark_shadow_cond_row (c,L) lowers /\
536 dark_shadow_condition uppers lowers)
537End
538
539Theorem constraint_mid_existence[local]:
540 !x i j. 0 < x ==>
541 ((!k. x * k < i ==> x * (k + 1) <= j) =
542 (?k. i <= x * k /\ x * k <= j))
543Proof
544 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
545 Q.SPEC_THEN `x` MP_TAC INT_DIVISION THEN
546 `~(x = 0)` by PROVE_TAC [INT_LT_REFL] THEN
547 `~(x < 0)` by PROVE_TAC [INT_LT_ANTISYM] THEN
548 ASM_SIMP_TAC (srw_ss())[] THEN
549 DISCH_THEN (Q.SPEC_THEN `j` STRIP_ASSUME_TAC) THEN
550 Q.ABBREV_TAC `jdivx = j / x` THEN
551 Q.ABBREV_TAC `jmodx = j % x` THEN
552 SPOSE_NOT_THEN (Q.SPEC_THEN `jdivx` MP_TAC) THEN
553 ASM_SIMP_TAC (srw_ss()) [INT_MUL_COMM] THEN
554 FIRST_X_ASSUM (Q.SPEC_THEN `jdivx` MP_TAC) THEN
555 Q_TAC SUFF_TAC `~(x * (jdivx + 1) <= j)` THEN1
556 PROVE_TAC [INT_NOT_LE, INT_MUL_COMM] THEN
557 ASM_SIMP_TAC (srw_ss()) [INT_LDISTRIB, INT_ADD_COMM, INT_MUL_COMM] THEN
558 ASM_SIMP_TAC (srw_ss()) [INT_NOT_LE],
559 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
560 FULL_SIMP_TAC (srw_ss()) [INT_NOT_LE] THEN
561 `?n. x = &n` by PROVE_TAC [NUM_POSINT_EXISTS, INT_LE_LT] THEN
562 POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC (srw_ss())[] THEN
563 `&n * k' < &n * k` by PROVE_TAC [INT_LTE_TRANS] THEN
564 `&n * k < &n * (k' + 1)` by PROVE_TAC [INT_LET_TRANS] THEN
565 PROVE_TAC [INT_DISCRETE, lt_mono]
566 ]
567QED
568
569Theorem dark_shadowrow_constraint_imp[local]:
570 !lowers uppers c L x.
571 0 < c /\ EVERY fst_nzero lowers /\
572 evalupper x uppers /\ evallower x lowers /\ &c * x <= L ==>
573 dark_shadow_cond_row (c,L) lowers
574Proof
575 Induct THENL [
576 SRW_TAC [][evallower_def, dark_shadow_cond_row_def],
577 SIMP_TAC (srw_ss()) [FORALL_PROD, evallower_def,
578 dark_shadow_cond_row_def] THEN
579 CONV_TAC (RENAME_VARS_CONV ["d", "R"]) THEN REPEAT STRIP_TAC THENL [
580 `&c * R <= &c * (&d * x)` by PROVE_TAC [le_mono] THEN
581 `&d * (&c * x) <= &d * L` by PROVE_TAC [le_mono] THEN
582 `&c * R <= (&c * &d) * x /\ (&c * &d) * x <= &d * L` by
583 PROVE_TAC [INT_MUL_COMM, INT_MUL_ASSOC] THEN
584 `&c * R <= &d * L` by PROVE_TAC [INT_LE_TRANS] THEN
585 ASM_SIMP_TAC (srw_ss())[GSYM IMP_DISJ_THM] THEN
586 REPEAT STRIP_TAC THEN FULL_SIMP_TAC (srw_ss())[] THEN
587 `&(c * d) * i < &(c * d) * x` by PROVE_TAC [INT_LTE_TRANS] THEN
588 `&(c * d) * x < &(c * d) * (i + 1)` by PROVE_TAC [INT_LET_TRANS] THEN
589 `0 < c * d` by SRW_TAC [][arithmeticTheory.LESS_MULT2] THEN
590 `i < x /\ x < i + 1` by PROVE_TAC [lt_mono] THEN
591 PROVE_TAC [INT_DISCRETE],
592 PROVE_TAC []
593 ]
594 ]
595QED
596
597Theorem dark_shadow_constraint_implied[local]:
598 !uppers lowers x.
599 evalupper x uppers /\ evallower x lowers /\
600 EVERY fst_nzero uppers /\ EVERY fst_nzero lowers ==>
601 dark_shadow_condition uppers lowers
602Proof
603 Induct THENL [
604 SRW_TAC [][dark_shadow_condition_def],
605 SIMP_TAC (srw_ss()) [FORALL_PROD, evalupper_def,
606 dark_shadow_condition_def] THEN
607 PROVE_TAC [dark_shadowrow_constraint_imp]
608 ]
609QED
610
611Theorem real_darkrow_implies_evals[local]:
612 !uppers lowers x c L.
613 0 < c /\ evalupper x uppers /\ evallower x lowers /\
614 EVERY fst_nzero uppers /\ EVERY fst_nzero lowers /\
615 rshadow_row (c,L) lowers /\ dark_shadow_cond_row (c,L) lowers ==>
616 ?y. &c * y <= L /\ evalupper y uppers /\ evallower y lowers
617Proof
618 Induct THENL [
619 SIMP_TAC (srw_ss()) [evalupper_def] THEN
620 Induct THENL [
621 SIMP_TAC (srw_ss()) [evallower_def, rshadow_row_def,
622 dark_shadow_cond_row_def] THEN REPEAT STRIP_TAC THEN
623 Q.EXISTS_TAC `L / &c` THEN
624 Q.SPEC_THEN `&c` MP_TAC INT_DIVISION THEN
625 SRW_TAC [ARITH_ss][] THEN
626 POP_ASSUM (Q.SPEC_THEN `L` STRIP_ASSUME_TAC) THEN
627 Q.ABBREV_TAC `Ldivc = L / &c` THEN
628 Q.ABBREV_TAC `Lmodc = L % &c` THEN
629 ASM_SIMP_TAC (srw_ss())[INT_MUL_COMM],
630 SIMP_TAC (srw_ss()) [evallower_def, rshadow_row_def,
631 dark_shadow_cond_row_def, FORALL_PROD] THEN
632 CONV_TAC (RENAME_VARS_CONV ["d", "R"]) THEN REPEAT STRIP_TAC THEN
633 FIRST_X_ASSUM (MP_TAC o assert (is_forall o concl)) THEN
634 ASM_SIMP_TAC (srw_ss())[GSYM IMP_DISJ_THM] THEN STRIP_TAC THEN
635 `?y. &c * y <= L /\ evallower y lowers` by PROVE_TAC [] THEN
636 `&c * &d * y <= &d * L` by PROVE_TAC [le_mono, INT_MUL_ASSOC,
637 INT_MUL_COMM] THEN
638 `&c * R <= &c * &d * x` by PROVE_TAC [le_mono, INT_MUL_ASSOC,
639 INT_MUL_COMM] THEN
640 Cases_on `&c * R <= &c * &d * y` THENL [
641 Q.EXISTS_TAC `y` THEN ASM_SIMP_TAC (srw_ss()) [] THEN
642 PROVE_TAC [le_mono, INT_MUL_COMM, INT_MUL_ASSOC],
643 ALL_TAC
644 ] THEN
645 `0 < &(c * d)` by
646 ASM_SIMP_TAC (srw_ss()) [arithmeticTheory.LESS_MULT2] THEN
647 `?j. &c * R <= &(c * d) * j /\ &(c * d) * j <= &d * L` by
648 PROVE_TAC [constraint_mid_existence, INT_NOT_LT] THEN
649 FULL_SIMP_TAC (srw_ss()) [INT_NOT_LE] THEN
650 Q.EXISTS_TAC `j` THEN
651 `&c * &d * j <= &d * L` by PROVE_TAC [INT_MUL] THEN
652 `&c * j <= L` by PROVE_TAC [le_mono, INT_MUL_ASSOC, INT_MUL_COMM] THEN
653 `&c * R <= &c * &d * j` by PROVE_TAC [INT_MUL] THEN
654 `R <= &d * j` by PROVE_TAC [le_mono, INT_MUL_ASSOC, INT_MUL_COMM] THEN
655 Q_TAC SUFF_TAC `y < j` THEN1 PROVE_TAC [bigger_satisfies_lowers] THEN
656 Q_TAC SUFF_TAC `&d * y < &d * j` THEN1 PROVE_TAC [lt_mono] THEN
657 Q_TAC SUFF_TAC `&c * (&d * y) < &c * (&d * j)` THEN1
658 PROVE_TAC [lt_mono] THEN
659 MATCH_MP_TAC INT_LTE_TRANS THEN
660 Q.EXISTS_TAC `&c * R` THEN
661 PROVE_TAC [INT_MUL, INT_MUL_ASSOC, INT_MUL_COMM]
662 ],
663 SIMP_TAC (srw_ss()) [evalupper_def, FORALL_PROD] THEN
664 CONV_TAC (RENAME_VARS_CONV ["d", "L2"]) THEN REPEAT STRIP_TAC THEN
665 `?z. &c * z <= L /\ evalupper z uppers /\ evallower z lowers` by
666 (FIRST_X_ASSUM MATCH_MP_TAC THEN PROVE_TAC []) THEN
667 Q.EXISTS_TAC `if x < z then x else z` THEN COND_CASES_TAC THEN
668 ASM_SIMP_TAC (srw_ss())[] THENL [
669 PROVE_TAC [INT_LTE_TRANS, INT_LE_LT, lt_mono],
670 PROVE_TAC [INT_LE_TRANS, INT_NOT_LE, le_mono]
671 ]
672 ]
673QED
674
675
676Theorem real_darkcond_implies_evals[local]:
677 !uppers lowers.
678 EVERY fst_nzero uppers /\ EVERY fst_nzero lowers /\
679 real_shadow uppers lowers /\ dark_shadow_condition uppers lowers ==>
680 ?x. evalupper x uppers /\ evallower x lowers
681Proof
682 Induct THENL [
683 SIMP_TAC (srw_ss()) [evalupper_def, onlylowers_satisfiable],
684 SIMP_TAC (srw_ss()) [evalupper_def, FORALL_PROD, dark_shadow_condition_def,
685 real_shadow_def] THEN
686 CONV_TAC (RENAME_VARS_CONV ["c", "L"]) THEN REPEAT STRIP_TAC THEN
687 `?y. evalupper y uppers /\ evallower y lowers` by PROVE_TAC [] THEN
688 REWRITE_TAC [GSYM CONJ_ASSOC] THEN
689 MATCH_MP_TAC real_darkrow_implies_evals THEN PROVE_TAC []
690 ]
691QED
692
693
694Theorem basic_shadow_equivalence:
695 !uppers lowers.
696 EVERY fst_nzero uppers /\ EVERY fst_nzero lowers ==>
697 ((?x. evalupper x uppers /\ evallower x lowers) =
698 real_shadow uppers lowers /\ dark_shadow_condition uppers lowers)
699Proof
700 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
701 CONJ_TAC THEN1
702 (MATCH_MP_TAC real_shadow_always_implied THEN PROVE_TAC []) THEN
703 PROVE_TAC [dark_shadow_constraint_implied],
704 PROVE_TAC [real_darkcond_implies_evals]
705 ]
706QED
707
708Definition dark_shadow_row_def:
709 (dark_shadow_row c L [] = T) /\
710 (dark_shadow_row c (L:int) ((d,R)::rs) =
711 &d * L - &c * R >= (&c - 1) * (&d - 1) /\ dark_shadow_row c L rs)
712End
713Definition dark_shadow_def:
714 (dark_shadow [] lowers = T) /\
715 (dark_shadow ((c,L)::uppers) lowers =
716 dark_shadow_row c L lowers /\ dark_shadow uppers lowers)
717End
718
719Theorem move_subs_out[local]:
720 !x:int y z. (x - y + z = x + z - y) /\ (x - y - z = x - (y + z)) /\
721 (x + (y - z) = x + y - z)
722Proof
723 REPEAT STRIP_TAC THENL [
724 Q.SPECL_THEN [`x`, `z`, `y`, `0`]
725 (ACCEPT_TAC o SYM o
726 REWRITE_RULE [INT_SUB_RZERO, INT_ADD_RID])
727 INT_ADD2_SUB2,
728 Q.SPECL_THEN [`x`, `0`, `y`, `z`]
729 (ACCEPT_TAC o SYM o
730 REWRITE_RULE [INT_SUB_LZERO, GSYM int_sub,
731 INT_ADD_RID])
732 INT_ADD2_SUB2,
733 SRW_TAC [][int_sub, ADD_AC]
734 ]
735QED
736
737
738Theorem lemma0[local]:
739 !c d (L:int) R i.
740 0 < c /\ 0 < d ==>
741 &c * &d * i < &c * R /\ &c * R <= &d * L /\
742 &d * L < &c * &d * (i + 1) ==>
743 &d * L - &c * R <= &c * &d - &c - &d
744Proof
745 REPEAT STRIP_TAC THEN
746 `&c * &d * (i + 1) - &d * L >= &d` by
747 (`&c * &d * (i + 1) - &d * L = &d * (&c * (i + 1) - L)` by
748 SRW_TAC [][INT_SUB_LDISTRIB, MULT_AC] THEN
749 POP_ASSUM SUBST_ALL_TAC THEN
750 REWRITE_TAC [int_ge] THEN
751 Q_TAC SUFF_TAC `1 <= &c * (i + 1) - L` THEN1
752 PROVE_TAC [INT_MUL_RID, le_mono, INT_LT] THEN
753 SRW_TAC [][LE_LT1, INT_LT_SUB_LADD] THEN
754 Q_TAC SUFF_TAC `&d * L < &d * (&c * (i + 1))` THEN1
755 PROVE_TAC [lt_mono, INT_LT] THEN
756 FULL_SIMP_TAC (srw_ss())[MULT_AC]) THEN
757 `&c * R - &c * &d * i >= &c` by
758 (`&c * R - &c * &d * i = &c * (R - &d * i)` by
759 SRW_TAC [][INT_SUB_LDISTRIB, MULT_AC] THEN
760 POP_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC [int_ge] THEN
761 Q_TAC SUFF_TAC `1 <= R - &d * i` THEN1
762 PROVE_TAC [INT_MUL_RID, le_mono, INT_LT] THEN
763 SRW_TAC [][LE_LT1, INT_LT_SUB_LADD] THEN
764 PROVE_TAC [INT_MUL_ASSOC, INT_LT, lt_mono]) THEN
765 FULL_SIMP_TAC (srw_ss()) [int_ge, INT_LE_SUB_LADD, move_subs_out,
766 INT_LE_SUB_RADD] THEN
767 `(&d + &d * L) + (&c + &(c * d) * i) <= &(c * d) * (i + 1) + &c * R` by
768 PROVE_TAC [INT_LE_ADD2] THEN
769 FULL_SIMP_TAC (srw_ss()) [INT_LDISTRIB, ADD_AC,
770 arithmeticTheory.MULT_CLAUSES] THEN
771 Q_TAC SUFF_TAC `&(c * d) * i + (&c + &d + & d * L) <=
772 &(c * d) * i + (&c * R + &(c * d))` THEN1
773 SRW_TAC [][ADD_AC] THEN
774 ASM_SIMP_TAC bool_ss [ADD_AC]
775QED
776
777val lemma =
778 CONV_RULE (STRIP_QUANT_CONV
779 (RAND_CONV
780 (CONTRAPOS_CONV THENC
781 SIMP_CONV (srw_ss()) [move_subs_out, INT_NOT_LE,
782 INT_LT_SUB_RADD, INT_NOT_LT,
783 INT_LT_SUB_LADD, LE_LT1] THENC
784 SIMP_CONV (srw_ss()) [ADD_AC])) THENC
785 SIMP_CONV bool_ss [AND_IMP_INTRO])
786 lemma0
787
788
789Theorem dark_shadow_row_implies_row_condition[local]:
790 !lowers c L.
791 EVERY fst_nzero lowers /\ 0 < c /\
792 dark_shadow_row c L lowers ==> dark_shadow_cond_row (c,L) lowers
793Proof
794 Induct THEN1 SRW_TAC [][dark_shadow_row_def, dark_shadow_cond_row_def] THEN
795 ASM_SIMP_TAC (srw_ss()) [FORALL_PROD, dark_shadow_row_def,
796 dark_shadow_cond_row_def] THEN
797 CONV_TAC (RENAME_VARS_CONV ["d", "R"]) THEN
798 SIMP_TAC (srw_ss()) [INT_SUB_LDISTRIB, INT_SUB_RDISTRIB,
799 arithmeticTheory.MULT_CLAUSES, int_ge, move_subs_out,
800 INT_LT_SUB_RADD, INT_LT_SUB_LADD, LE_LT1] THEN
801 SRW_TAC [][ADD_AC] THEN
802 FULL_SIMP_TAC (srw_ss()) [INT_ADD_ASSOC] THEN
803 FULL_SIMP_TAC (srw_ss()) [INT_NOT_LT, INT_NOT_LE, ADD_AC, LE_LT1] THEN
804 PROVE_TAC [lemma]
805QED
806
807Theorem dark_shadow_implies_dark_condition[local]:
808 !uppers lowers.
809 EVERY fst_nzero uppers /\ EVERY fst_nzero lowers ==>
810 (dark_shadow uppers lowers ==> dark_shadow_condition uppers lowers)
811Proof
812 Induct THEN1 SRW_TAC [][dark_shadow_condition_def] THEN
813 ASM_SIMP_TAC (srw_ss()) [FORALL_PROD, dark_shadow_row_implies_row_condition,
814 dark_shadow_def, dark_shadow_condition_def]
815QED
816
817Theorem mult_lemma[local]:
818 !c:int d p q.
819 0 < c /\ 0 < d /\ 0 < p /\ 0 < q /\ c < d /\ p < q ==>
820 d + c * p <= d * q
821Proof
822 REPEAT STRIP_TAC THEN
823 `?e. (q = p + e) /\ 0 < e` by PROVE_TAC [less_exists] THEN
824 SRW_TAC [][INT_LDISTRIB] THEN
825 CONV_TAC (LAND_CONV (REWR_CONV INT_ADD_COMM)) THEN
826 MATCH_MP_TAC INT_LE_ADD2 THEN CONJ_TAC THENL [
827 PROVE_TAC [ile_mono, INT_MUL_COMM, INT_LE_LT],
828 CONV_TAC (LAND_CONV (REWR_CONV (GSYM INT_MUL_RID))) THEN
829 SRW_TAC [][ile_mono] THEN
830 SRW_TAC [][LE_LT1]
831 ]
832QED
833
834Theorem neg_eliminate[local]:
835 !x y. (x + ~y = x - y) /\ (~x + y = y - x)
836Proof
837 PROVE_TAC [int_sub, INT_ADD_COMM]
838QED
839
840Theorem div_lemma0[local]:
841 !n c d. 0 < c /\ c <= d /\ 0 < n ==> ~n / c <= ~n / d
842Proof
843 REPEAT STRIP_TAC THEN
844 Cases_on `c = d` THEN1 PROVE_TAC [INT_LE_REFL] THEN
845 `c < d` by PROVE_TAC [INT_LE_LT] THEN
846 `0 < d /\ ~(c = 0) /\ ~(d = 0) /\ ~(c < 0) /\ ~(d < 0)` by
847 PROVE_TAC [INT_LT_TRANS, INT_LT_REFL, INT_LT_ANTISYM] THEN
848 Q.SPEC_THEN `c` MP_TAC INT_DIVISION THEN SRW_TAC [][] THEN
849 POP_ASSUM (Q.SPEC_THEN `~n` STRIP_ASSUME_TAC) THEN
850 Q.ABBREV_TAC `p = ~n / c` THEN POP_ASSUM (K ALL_TAC) THEN
851 Q.ABBREV_TAC `r = ~n % c` THEN POP_ASSUM (K ALL_TAC) THEN
852 Q.SPEC_THEN `d` MP_TAC INT_DIVISION THEN
853 DISCH_THEN (fn imp => FIRST_ASSUM (ASSUME_TAC o MATCH_MP imp)) THEN
854 POP_ASSUM (Q.SPEC_THEN `~n` STRIP_ASSUME_TAC) THEN
855 Q.ABBREV_TAC `q = ~n / d` THEN POP_ASSUM (K ALL_TAC) THEN
856 Q.ABBREV_TAC `s = ~n % d` THEN POP_ASSUM (K ALL_TAC) THEN
857 POP_ASSUM MP_TAC THEN SRW_TAC [][] THEN
858 `r = ~n - p * c` by PROVE_TAC [INT_ADD_SUB] THEN
859 POP_ASSUM SUBST_ALL_TAC THEN
860 `s = ~n - q * d` by PROVE_TAC [INT_ADD_SUB] THEN
861 POP_ASSUM SUBST_ALL_TAC THEN
862 FULL_SIMP_TAC (srw_ss()) [INT_LE_SUB_LADD, INT_LE_SUB_RADD,
863 INT_LT_SUB_LADD, INT_LT_SUB_RADD] THEN
864 `p < 0` by (SPOSE_NOT_THEN (ASSUME_TAC o REWRITE_RULE [INT_NOT_LT]) THEN
865 `?m. p = &m` by PROVE_TAC [NUM_POSINT_EXISTS] THEN
866 POP_ASSUM SUBST_ALL_TAC THEN
867 `?m1. c = &m1` by PROVE_TAC [NUM_POSINT_EXISTS, INT_LE_LT] THEN
868 POP_ASSUM SUBST_ALL_TAC THEN
869 `?m2. n = &m2` by PROVE_TAC [NUM_POSINT_EXISTS, INT_LE_LT] THEN
870 POP_ASSUM SUBST_ALL_TAC THEN
871 FULL_SIMP_TAC (srw_ss()) [INT_LE_CALCULATE, INT_LT_CALCULATE,
872 INT_EQ_CALCULATE]) THEN
873 Q.ABBREV_TAC `i = ~p` THEN `p = ~i` by PROVE_TAC [INT_NEGNEG] THEN
874 POP_ASSUM SUBST_ALL_TAC THEN POP_ASSUM (K ALL_TAC) THEN
875 `q < 0` by (SPOSE_NOT_THEN (ASSUME_TAC o REWRITE_RULE [INT_NOT_LT]) THEN
876 `?m. q = &m` by PROVE_TAC [NUM_POSINT_EXISTS] THEN
877 POP_ASSUM SUBST_ALL_TAC THEN
878 `?m1. d = &m1` by PROVE_TAC [NUM_POSINT_EXISTS, INT_LE_LT] THEN
879 POP_ASSUM SUBST_ALL_TAC THEN
880 `?m2. n = &m2` by PROVE_TAC [NUM_POSINT_EXISTS, INT_LE_LT] THEN
881 POP_ASSUM SUBST_ALL_TAC THEN
882 FULL_SIMP_TAC (srw_ss()) [INT_LE_CALCULATE, INT_LT_CALCULATE,
883 INT_EQ_CALCULATE]) THEN
884 Q.ABBREV_TAC `j = ~q` THEN `q = ~j` by PROVE_TAC [INT_NEGNEG] THEN
885 POP_ASSUM SUBST_ALL_TAC THEN POP_ASSUM (K ALL_TAC) THEN
886 FULL_SIMP_TAC (srw_ss()) [INT_LE_NEG, INT_NEG_LT0, GSYM INT_NEG_LMUL,
887 neg_eliminate, INT_LT_SUB_LADD,
888 INT_LT_SUB_RADD] THEN
889 SPOSE_NOT_THEN (ASSUME_TAC o REWRITE_RULE [INT_NOT_LE]) THEN
890 Q.SPECL_THEN [`c`,`d`,`i`,`j`] MP_TAC mult_lemma THEN
891 SRW_TAC [][] THEN STRIP_TAC THEN
892 `d + i * c < d + n` by PROVE_TAC [INT_LET_TRANS, INT_MUL_COMM] THEN
893 FULL_SIMP_TAC (srw_ss())[] THEN
894 `i * c < i * c` by PROVE_TAC [INT_LTE_TRANS] THEN
895 PROVE_TAC [INT_LT_REFL]
896QED
897
898Theorem div_lemma[local]:
899 !c c' d.
900 0 < c /\ 0 < c' /\ 0 < d /\ c <= c' ==>
901 (c * d - c - d) / c <= (c' * d - c' - d) / c'
902Proof
903 REPEAT STRIP_TAC THEN
904 REWRITE_TAC [int_sub] THEN
905 `~(c = 0) /\ ~(c' = 0)` by PROVE_TAC [INT_LT_REFL] THEN
906 `~(c < 0) /\ ~(c' < 0)` by PROVE_TAC [INT_LT_ANTISYM] THEN
907 `c * d + ~c = c * (d + ~1)` by SRW_TAC [][INT_LDISTRIB,
908 GSYM INT_NEG_RMUL] THEN
909 POP_ASSUM SUBST_ALL_TAC THEN
910 `(c * (d + ~1)) % c = 0` by
911 PROVE_TAC [INT_MUL_COMM, INT_MOD_COMMON_FACTOR] THEN
912 `(c * (d + ~1) + ~d) / c = (c * (d + ~1)) / c + ~d / c` by
913 PROVE_TAC [INT_ADD_DIV] THEN
914 `(c * (d + ~1)) / c = (c / c) * (d + ~1)` by
915 (ONCE_REWRITE_TAC [INT_MUL_COMM] THEN
916 MATCH_MP_TAC INT_MUL_DIV THEN PROVE_TAC [INT_MOD_ID]) THEN
917 SRW_TAC [][] THEN
918 `c' * d + ~c' = c' * (d + ~1)` by SRW_TAC [][INT_LDISTRIB,
919 GSYM INT_NEG_RMUL] THEN
920 POP_ASSUM SUBST_ALL_TAC THEN
921 `(c' * (d + ~1)) % c' = 0` by
922 PROVE_TAC [INT_MUL_COMM, INT_MOD_COMMON_FACTOR] THEN
923 `(c' * (d + ~1) + ~d) / c' = (c' * (d + ~1)) / c' + ~d / c'` by
924 PROVE_TAC [INT_ADD_DIV] THEN
925 `(c' * (d + ~1)) / c' = (c' / c') * (d + ~1)` by
926 (ONCE_REWRITE_TAC [INT_MUL_COMM] THEN
927 MATCH_MP_TAC INT_MUL_DIV THEN
928 PROVE_TAC [INT_MOD_ID]) THEN
929 SRW_TAC [][div_lemma0]
930QED
931
932val _ = print "Now proving properties of nightmare function\n"
933Definition nightmare_def:
934 (nightmare x c uppers lowers [] = F) /\
935 (nightmare x c uppers lowers ((d,R)::rs) =
936 (?i. (0 <= i /\ i <= (&c * &d - &c - &d) / &c) /\ (&d * x = R + i) /\
937 evalupper x uppers /\ evallower x lowers) \/
938 nightmare x c uppers lowers rs)
939End
940
941Theorem nightmare_implies_LHS:
942 !rs x uppers lowers c.
943 nightmare x c uppers lowers rs ==>
944 evalupper x uppers /\ evallower x lowers
945Proof
946 Induct THEN1 SRW_TAC [][nightmare_def] THEN
947 ASM_SIMP_TAC (srw_ss()) [nightmare_def, FORALL_PROD] THEN
948 PROVE_TAC []
949QED
950
951Theorem dark_shadow_FORALL:
952 !uppers lowers.
953 dark_shadow uppers lowers =
954 !c d L R. MEM (c,L) uppers /\ MEM (d,R) lowers ==>
955 &d * L - &c * R >= (&c - 1) * (&d - 1)
956Proof
957 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
958 Induct_on `uppers` THEN1 SRW_TAC [][] THEN
959 ASM_SIMP_TAC (srw_ss()) [FORALL_PROD, dark_shadow_def] THEN
960 REVERSE (REPEAT STRIP_TAC) THEN1 PROVE_TAC [] THEN
961 Q.PAT_X_ASSUM `dark_shadow xs ys` (K ALL_TAC) THEN
962 Q.PAT_X_ASSUM `dark_shadow xs ys ==> Q` (K ALL_TAC) THEN
963 Induct_on `lowers` THEN1 SRW_TAC [][] THEN
964 ASM_SIMP_TAC (srw_ss()) [FORALL_PROD, dark_shadow_row_def] THEN
965 SRW_TAC [][] THEN PROVE_TAC [],
966 Induct_on `uppers` THEN1 SRW_TAC [][dark_shadow_def] THEN
967 ASM_SIMP_TAC (srw_ss()) [FORALL_PROD, dark_shadow_def, DISJ_IMP_THM,
968 FORALL_AND_THM, RIGHT_AND_OVER_OR] THEN
969 POP_ASSUM (K ALL_TAC) THEN REPEAT STRIP_TAC THEN
970 POP_ASSUM (K ALL_TAC) THEN
971 Induct_on `lowers` THEN
972 ASM_SIMP_TAC (srw_ss())[dark_shadow_row_def, FORALL_PROD]
973 ]
974QED
975
976Theorem real_shadow_FORALL:
977 !uppers lowers.
978 real_shadow uppers lowers =
979 !c d L R. MEM (c,L) uppers /\ MEM (d,R) lowers ==> &c * R <= &d * L
980Proof
981 Induct THEN
982 ASM_SIMP_TAC (srw_ss()) [FORALL_PROD, real_shadow_def] THEN
983 POP_ASSUM (K ALL_TAC) THEN REPEAT STRIP_TAC THEN EQ_TAC THEN
984 STRIP_TAC THEN
985 FULL_SIMP_TAC (srw_ss()) [DISJ_IMP_THM, RIGHT_AND_OVER_OR,
986 FORALL_AND_THM] THEN
987 POP_ASSUM (K ALL_TAC) THEN Induct_on `lowers` THEN
988 ASM_SIMP_TAC (srw_ss()) [FORALL_PROD, rshadow_row_def,
989 DISJ_IMP_THM, FORALL_AND_THM]
990QED
991
992Theorem evalupper_FORALL:
993 !uppers x. evalupper x uppers = !c L. MEM (c,L) uppers ==> &c * x <= L
994Proof
995 Induct THEN
996 ASM_SIMP_TAC (srw_ss())[evalupper_def, FORALL_PROD, DISJ_IMP_THM,
997 FORALL_AND_THM]
998QED
999
1000Theorem evallower_FORALL:
1001 !lowers x. evallower x lowers = !d R. MEM (d,R) lowers ==> R <= &d * x
1002Proof
1003 Induct THEN
1004 ASM_SIMP_TAC (srw_ss())[evallower_def, FORALL_PROD, DISJ_IMP_THM,
1005 FORALL_AND_THM]
1006QED
1007
1008Theorem nightmare_EXISTS:
1009 !rs x c uppers lowers.
1010 nightmare x c uppers lowers rs =
1011 ?i d R.
1012 0 <= i /\ i <= (&d * &c - &c - &d) / &c /\ MEM (d,R) rs /\
1013 evalupper x uppers /\ evallower x lowers /\
1014 (&d * x = R + i)
1015Proof
1016 Induct THEN
1017 ASM_SIMP_TAC (srw_ss()) [nightmare_def, FORALL_PROD] THEN
1018 POP_ASSUM (K ALL_TAC) THEN REPEAT STRIP_TAC THEN EQ_TAC THEN
1019 SRW_TAC [][] THEN PROVE_TAC [arithmeticTheory.MULT_COMM]
1020QED
1021
1022Theorem final_equivalence:
1023 !uppers lowers m.
1024 EVERY fst_nzero uppers /\ EVERY fst_nzero lowers /\
1025 EVERY (\p. FST p <= m) uppers ==>
1026 ((?x. evalupper x uppers /\ evallower x lowers) =
1027 real_shadow uppers lowers /\
1028 (dark_shadow uppers lowers \/
1029 ?x. nightmare x m uppers lowers lowers))
1030Proof
1031 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
1032 CONJ_TAC THEN1 PROVE_TAC [basic_shadow_equivalence] THEN
1033 Q_TAC SUFF_TAC
1034 `~dark_shadow uppers lowers ==>
1035 ?x. nightmare x m uppers lowers lowers` THEN1 PROVE_TAC [] THEN
1036 STRIP_TAC THEN
1037 FULL_SIMP_TAC (srw_ss()) [dark_shadow_FORALL, nightmare_EXISTS, int_ge,
1038 listTheory.EVERY_MEM, INT_NOT_LE,
1039 FORALL_PROD] THEN
1040 `&c * x <= L` by PROVE_TAC [evalupper_FORALL] THEN
1041 `R <= &d * x` by PROVE_TAC [evallower_FORALL] THEN
1042 `0 < c /\ 0 < d /\ c <= m` by PROVE_TAC [] THEN
1043 `&d * (&c * x) <= &d * L /\ &c * R <= &c * (&d * x)` by
1044 PROVE_TAC [le_mono] THEN
1045 `&d * L - &c * R < &(c * d) - &c - (&d - 1)` by
1046 FULL_SIMP_TAC (srw_ss())
1047 [INT_SUB_LDISTRIB, INT_SUB_RDISTRIB, MULT_AC,
1048 arithmeticTheory.MULT_CLAUSES] THEN
1049 `&d * L <= &c * R + (&(c * d) - &c - &d)` by
1050 FULL_SIMP_TAC (srw_ss())
1051 [move_subs_out, LE_LT1, INT_LT_SUB_LADD, MULT_AC, ADD_AC,
1052 INT_LT_SUB_RADD] THEN
1053 `&d * (&c * x) <= &c * R + (&(c * d) - &c - &d)` by
1054 PROVE_TAC [INT_LE_TRANS] THEN
1055 `&c * (&d * x - R) <= &(c * d) - &c - &d` by
1056 FULL_SIMP_TAC (srw_ss())
1057 [move_subs_out, LE_LT1, INT_LT_SUB_LADD, MULT_AC, ADD_AC,
1058 INT_LT_SUB_RADD, INT_SUB_LDISTRIB] THEN
1059 `&d * x - R <= (&(c * d) - &c - &d) / &c` by
1060 PROVE_TAC [div_le, INT_LT] THEN
1061 MAP_EVERY Q.EXISTS_TAC [`x`, `&d * x - R`, `d`, `R`] THEN
1062 SRW_TAC [][INT_LE_SUB_LADD] THEN
1063 MATCH_MP_TAC INT_LE_TRANS THEN
1064 Q.EXISTS_TAC ` (&(c * d) - &c - &d) / &c` THEN SRW_TAC [][] THEN
1065 Q.SPECL_THEN [`&c`,`&m`,`&d`] MP_TAC div_lemma THEN
1066 ASM_SIMP_TAC (srw_ss())[arithmeticTheory.MULT_COMM] THEN
1067 PROVE_TAC [arithmeticTheory.LESS_LESS_EQ_TRANS],
1068 PROVE_TAC [dark_shadow_implies_dark_condition, basic_shadow_equivalence],
1069 PROVE_TAC [nightmare_implies_LHS]
1070 ]
1071QED
1072
1073Theorem darkrow_implies_realrow:
1074 !lowers c L. 0 < c /\ EVERY fst_nzero lowers /\
1075 dark_shadow_row c L lowers ==> rshadow_row (c,L) lowers
1076Proof
1077 Induct THEN1 SRW_TAC [][dark_shadow_row_def, rshadow_row_def] THEN
1078 ASM_SIMP_TAC (srw_ss()) [FORALL_PROD, dark_shadow_row_def, rshadow_row_def,
1079 int_ge, INT_LE_SUB_LADD] THEN
1080 REPEAT STRIP_TAC THEN
1081 Q_TAC SUFF_TAC `0 <= (&c - 1) * (&p_1 - 1)` THEN1
1082 PROVE_TAC [INT_LE_TRANS, INT_LE_ADDL] THEN
1083 MATCH_MP_TAC INT_LE_MUL THEN
1084 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) [INT_LE_SUB_LADD]
1085QED
1086
1087Theorem dark_implies_real:
1088 !uppers lowers. EVERY fst_nzero uppers /\ EVERY fst_nzero lowers /\
1089 dark_shadow uppers lowers ==> real_shadow uppers lowers
1090Proof
1091 Induct THEN
1092 ASM_SIMP_TAC (srw_ss()) [FORALL_PROD, dark_shadow_def, real_shadow_def,
1093 darkrow_implies_realrow]
1094QED
1095
1096(* theorems specially designed for use in the decision procedure *)
1097
1098Theorem alternative_equivalence:
1099 !uppers lowers m.
1100 EVERY fst_nzero uppers /\ EVERY fst_nzero lowers /\
1101 EVERY (\p. FST p <= m) uppers ==>
1102 ((?x. evalupper x uppers /\ evallower x lowers) =
1103 dark_shadow uppers lowers \/ ?x. nightmare x m uppers lowers lowers)
1104Proof
1105 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
1106 Q.SPECL_THEN [`uppers`, `lowers`, `m`] MP_TAC final_equivalence THEN
1107 ASM_REWRITE_TAC [] THEN PROVE_TAC [],
1108 Q.SPECL_THEN [`uppers`, `lowers`, `m`] MP_TAC final_equivalence THEN
1109 ASM_REWRITE_TAC [] THEN PROVE_TAC [dark_implies_real],
1110 PROVE_TAC [nightmare_implies_LHS]
1111 ]
1112QED
1113
1114Theorem eval_base:
1115 p = ((evalupper x [] /\ evallower x []) /\ T) /\ p
1116Proof
1117 REWRITE_TAC [evalupper_def, evallower_def]
1118QED
1119
1120Theorem eval_step_upper1:
1121 ((evalupper x ups /\ evallower x lows) /\ ex) /\ &c * x <= r =
1122 (evalupper x ((c,r)::ups) /\ evallower x lows) /\ ex
1123Proof
1124 REWRITE_TAC [evalupper_def, evallower_def] THEN
1125 CONV_TAC (AC_CONV (CONJ_ASSOC, CONJ_COMM))
1126QED
1127Theorem eval_step_upper2:
1128 ((evalupper x ups /\ evallower x lows) /\ ex) /\ (&c * x <= r /\ p) =
1129 ((evalupper x ((c,r)::ups) /\ evallower x lows) /\ ex) /\ p
1130Proof
1131 REWRITE_TAC [evalupper_def, evallower_def] THEN
1132 CONV_TAC (AC_CONV (CONJ_ASSOC, CONJ_COMM))
1133QED
1134Theorem eval_step_lower1:
1135 ((evalupper x ups /\ evallower x lows) /\ ex) /\ r <= &c * x =
1136 (evalupper x ups /\ evallower x ((c,r)::lows)) /\ ex
1137Proof
1138 REWRITE_TAC [evalupper_def, evallower_def] THEN
1139 CONV_TAC (AC_CONV (CONJ_ASSOC, CONJ_COMM))
1140QED
1141Theorem eval_step_lower2:
1142 ((evalupper x ups /\ evallower x lows) /\ ex) /\ (r <= &c * x /\ p) =
1143 ((evalupper x ups /\ evallower x ((c,r)::lows)) /\ ex) /\ p
1144Proof
1145 REWRITE_TAC [evalupper_def, evallower_def] THEN
1146 CONV_TAC (AC_CONV (CONJ_ASSOC, CONJ_COMM))
1147QED
1148Theorem eval_step_extra1:
1149 ((evalupper x ups /\ evallower x lows) /\ T) /\ ex' =
1150 (evalupper x ups /\ evallower x lows) /\ ex'
1151Proof
1152 REWRITE_TAC [CONJ_ASSOC]
1153QED
1154Theorem eval_step_extra2:
1155 ((evalupper x ups /\ evallower x lows) /\ ex) /\ ex' =
1156 (evalupper x ups /\ evallower x lows) /\ (ex /\ ex')
1157Proof
1158 REWRITE_TAC [CONJ_ASSOC]
1159QED
1160Theorem eval_step_extra3:
1161 ((evalupper x ups /\ evallower x lows) /\ T) /\ (ex' /\ p) =
1162 ((evalupper x ups /\ evallower x lows) /\ ex') /\ p
1163Proof
1164 REWRITE_TAC [CONJ_ASSOC]
1165QED
1166Theorem eval_step_extra4:
1167 ((evalupper x ups /\ evallower x lows) /\ ex) /\ (ex' /\ p) =
1168 ((evalupper x ups /\ evallower x lows) /\ (ex /\ ex')) /\ p
1169Proof
1170 REWRITE_TAC [CONJ_ASSOC]
1171QED
1172
1173Definition calc_nightmare_def:
1174 (calc_nightmare x c [] = F) /\
1175 (calc_nightmare x c ((d,R)::rs) =
1176 (?i. (0 <= i /\ i <= (&c * &d - &c - &d) / &c) /\
1177 (&d * x = R + i)) \/
1178 calc_nightmare x c rs)
1179End
1180
1181Theorem calculational_nightmare:
1182 !rs. nightmare x c uppers lowers rs =
1183 calc_nightmare x c rs /\ evalupper x uppers /\ evallower x lowers
1184Proof
1185 Induct THEN SRW_TAC [][nightmare_def, calc_nightmare_def] THEN
1186 Cases_on `h` THEN SRW_TAC [][nightmare_def, calc_nightmare_def] THEN
1187 PROVE_TAC []
1188QED
1189
1190Theorem SYM_RDISTRIB[unlisted] = GSYM INT_RDISTRIB;
1191Theorem SYM_ADD_ASSOC[unlisted] = GSYM INT_ADD_ASSOC;
1192Theorem SYM_NEG_LMUL[unlisted] = GSYM INT_NEG_LMUL;
1193Theorem SYM_NEG_RMUL[unlisted] = GSYM INT_NEG_RMUL;
1194Theorem SYM_MULT_LEFT_1[unlisted] = GSYM arithmeticTheory.MULT_LEFT_1;
1195Theorem SYM_MUL_LID[unlisted] = GSYM INT_MUL_LID;
1196Theorem SYM_EQ_NEG[unlisted] = GSYM INT_EQ_NEG;
1197
1198Theorem EX_REFL[unlisted] = EQT_INTRO (SPEC_ALL EXISTS_REFL);
1199
1200Theorem front_put_thm[unlisted]:
1201 !x y. x = y + (x + ~y)
1202Proof
1203 REPEAT GEN_TAC THEN
1204 CONV_TAC (RAND_CONV (RAND_CONV (REWR_CONV INT_ADD_COMM))) THEN
1205 REWRITE_TAC [INT_ADD_ASSOC, INT_ADD_RINV, INT_ADD_LID]
1206QED
1207
1208
1209Theorem EVERY_SUMMAND_lt_elim[unlisted] =
1210 SPEC_ALL int_arithTheory.less_to_leq_samer;
1211
1212local
1213val tac = REWRITE_TAC [GSYM int_le, INT_NOT_LE, EVERY_SUMMAND_lt_elim,
1214 int_gt, INT_LE_RADD, int_ge, GSYM INT_LE_ANTISYM, DE_MORGAN_THM]
1215in
1216
1217Theorem EVERY_SUMMAND_not_le[unlisted]:
1218 ~(x <= y) = (y + 1i <= x)
1219Proof
1220 tac
1221QED
1222
1223Theorem EVERY_SUMMAND_not_lt[unlisted]:
1224 ~(x:int < y) <=> y <= x
1225Proof
1226 tac
1227QED
1228
1229Theorem EVERY_SUMMAND_not_gt[unlisted]:
1230 ~(x:int > y) <=> x <= y
1231Proof
1232 tac
1233QED
1234
1235Theorem EVERY_SUMMAND_not_ge[unlisted]:
1236 ~(x >= y) <=> x + 1i <= y
1237Proof
1238 tac
1239QED
1240
1241Theorem EVERY_SUMMAND_not_eq[unlisted]:
1242 ~(x = y:int) <=> y + 1 <= x \/ x + 1 <= y
1243Proof
1244 tac
1245QED
1246
1247Theorem EVERY_SUMMAND_ge_elim[unlisted]:
1248 x:int >= y <=> y <= x
1249Proof
1250 tac
1251QED
1252
1253Theorem EVERY_SUMMAND_gt_elim[unlisted]:
1254 x > y <=> y + 1i <= x
1255Proof
1256 tac
1257QED
1258
1259Theorem EVERY_SUMMAND_eq_elim[unlisted]:
1260 (x:int = y) <=> (x <= y /\ y <= x)
1261Proof
1262 tac
1263QED
1264
1265end;
1266
1267Theorem COND_FA_THEN_THM[unlisted]:
1268 (if p then !x:'a. P x else q) = !x. if p then P x else q
1269Proof
1270 COND_CASES_TAC THEN REWRITE_TAC []
1271QED
1272
1273Theorem COND_FA_ELSE_THM[unlisted]:
1274 (if p then q else !x:'a. P x) = !x. if p then q else P x
1275Proof
1276 COND_CASES_TAC THEN REWRITE_TAC []
1277QED
1278
1279Theorem COND_EX_THEN_THM[unlisted]:
1280 (if p then ?x:'a. P x else q) = ?x. if p then P x else q
1281Proof
1282 COND_CASES_TAC THEN REWRITE_TAC []
1283QED
1284
1285Theorem COND_EX_ELSE_THM[unlisted]:
1286 (if p then q else ?x:'a. P x) = ?x. if p then q else P x
1287Proof
1288 COND_CASES_TAC THEN REWRITE_TAC []
1289QED
1290
1291Theorem not_beq[unlisted]:
1292 ~(b1 = b2) <=> b1 /\ ~b2 \/ ~b1 /\ b2
1293Proof
1294 BOOL_CASES_TAC ``b1:bool`` THEN REWRITE_TAC []
1295QED
1296
1297Theorem beq[unlisted]:
1298 (b1 = b2) <=> b1 /\ b2 \/ ~b1 /\ ~b2
1299Proof
1300 BOOL_CASES_TAC ``b1:bool`` THEN REWRITE_TAC []
1301QED
1302
1303Theorem FLIP_COND[unlisted]:
1304 (if g then t:'a else e) = if ~g then e else t
1305Proof
1306 COND_CASES_TAC THEN REWRITE_TAC []
1307QED
1308
1309Theorem refl_case[unlisted]:
1310 !u P. (?i:int. (u <= i /\ i <= u) /\ P i) = P u
1311Proof
1312 REWRITE_TAC [INT_LE_ANTISYM] THEN REPEAT GEN_TAC THEN EQ_TAC THEN
1313 STRIP_TAC THEN ASM_REWRITE_TAC [] THEN Q.EXISTS_TAC `u` THEN
1314 ASM_REWRITE_TAC []
1315QED
1316
1317Theorem nonrefl_case[unlisted]:
1318 !lo hi P. (?i:int. (lo <= i /\ i <= hi) /\ P i) <=>
1319 lo <= hi /\ (P lo \/ ?i. (lo + 1 <= i /\ i <= hi) /\ P i)
1320Proof
1321 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
1322 Q.ASM_CASES_TAC `i = lo` THENL [
1323 POP_ASSUM SUBST_ALL_TAC THEN ASM_REWRITE_TAC [],
1324 REWRITE_TAC [LEFT_AND_OVER_OR] THEN
1325 DISJ2_TAC THEN CONJ_TAC THENL [
1326 IMP_RES_TAC INT_LE_TRANS,
1327 ALL_TAC
1328 ] THEN Q.EXISTS_TAC `i` THEN ASM_REWRITE_TAC [] THEN
1329 REWRITE_TAC [GSYM int_arithTheory.less_to_leq_samer] THEN
1330 RULE_ASSUM_TAC (REWRITE_RULE [INT_LE_LT]) THEN
1331 POP_ASSUM_LIST (MAP_EVERY STRIP_ASSUME_TAC) THEN
1332 POP_ASSUM SUBST_ALL_TAC THEN
1333 FIRST_X_ASSUM (fn th => MP_TAC th THEN REWRITE_TAC [] THEN NO_TAC)
1334 ],
1335 Q.EXISTS_TAC `lo` THEN ASM_REWRITE_TAC [INT_LE_REFL],
1336 Q.EXISTS_TAC `i` THEN ASM_REWRITE_TAC [] THEN
1337 MATCH_MP_TAC INT_LE_TRANS THEN Q.EXISTS_TAC `lo + 1` THEN
1338 ASM_REWRITE_TAC [INT_LE_ADDR] THEN CONV_TAC CooperMath.REDUCE_CONV
1339 ]
1340QED