listRangeScript.sml
1(* ------------------------------------------------------------------------- *)
2(* List of Range of Numbers *)
3(* ------------------------------------------------------------------------- *)
4Theory listRange[bare]
5Ancestors
6 arithmetic list pred_set divides
7Libs
8 HolKernel Parse boolLib BasicProvers TotalDefn simpLib numSimps
9 numLib metisLib pred_setSimps listSimps
10
11
12val decide_tac = DECIDE_TAC;
13val metis_tac = METIS_TAC;
14val qabbrev_tac = Q.ABBREV_TAC;
15val qexists_tac = Q.EXISTS_TAC;
16fun simp l = ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) l;
17fun fs l = FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) l;
18fun rfs l = REV_FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) l;
19val rw = SRW_TAC [ARITH_ss];
20val Know = Q_TAC KNOW_TAC;
21fun wrap a = [a];
22val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap);
23
24(* ------------------------------------------------------------------------- *)
25(* Range Conjunction and Disjunction *)
26(* ------------------------------------------------------------------------- *)
27
28(* Theorem: a <= j /\ j <= a <=> (j = a) *)
29(* Proof: trivial by arithmetic. *)
30Theorem every_range_sing:
31 !a j. a <= j /\ j <= a <=> (j = a)
32Proof
33 decide_tac
34QED
35
36(* Theorem: a <= b ==>
37 ((!j. a <= j /\ j <= b ==> f j) <=> (f a /\ !j. a + 1 <= j /\ j <= b ==> f j)) *)
38(* Proof:
39 If part: !j. a <= j /\ j <= b ==> f j ==>
40 f a /\ !j. a + 1 <= j /\ j <= b ==> f j
41 This is trivial since a + 1 = SUC a.
42 Only-if part: f a /\ !j. a + 1 <= j /\ j <= b ==> f j ==>
43 !j. a <= j /\ j <= b ==> f j
44 Note a <= j <=> a = j or a < j by arithmetic
45 If a = j, this is trivial.
46 If a < j, then a + 1 <= j, also trivial.
47*)
48Theorem every_range_cons:
49 !f a b. a <= b ==>
50 ((!j. a <= j /\ j <= b ==> f j) <=> (f a /\ !j. a + 1 <= j /\ j <= b ==> f j))
51Proof
52 rw[EQ_IMP_THM] >>
53 `(a = j) \/ (a < j)` by decide_tac >-
54 fs[] >>
55 fs[]
56QED
57
58(* Theorem: a <= b ==> ((!j. PRE a <= j /\ j <= b ==> f j) <=> (f (PRE a) /\ !j. a <= j /\ j <= b ==> f j)) *)
59(* Proof:
60 !j. PRE a <= j /\ j <= b ==> f j
61 <=> !j. (PRE a = j \/ a <= j) /\ j <= b ==> f j by arithmetic
62 <=> !j. (j = PRE a ==> f j) /\ a <= j /\ j <= b ==> f j by RIGHT_AND_OVER_OR, DISJ_IMP_THM
63 <=> !j. a <= j /\ j <= b ==> f j /\ f (PRE a)
64*)
65Theorem every_range_split_head:
66 !f a b. a <= b ==>
67 ((!j. PRE a <= j /\ j <= b ==> f j) <=> (f (PRE a) /\ !j. a <= j /\ j <= b ==> f j))
68Proof
69 rpt strip_tac >>
70 `!j. PRE a <= j <=> PRE a = j \/ a <= j` by decide_tac >>
71 metis_tac[]
72QED
73
74(* Theorem: a <= b ==> ((!j. a <= j /\ j <= SUC b ==> f j) <=> (f (SUC b) /\ !j. a <= j /\ j <= b ==> f j)) *)
75(* Proof:
76 !j. a <= j /\ j <= SUC b ==> f j
77 <=> !j. a <= j /\ (j <= b \/ j = SUC b) ==> f j by arithmetic
78 <=> !j. a <= j /\ j <= b ==> f j /\ (j = SUC b ==> f j) by LEFT_AND_OVER_OR, DISJ_IMP_THM
79 <=> !j. a <= j /\ j <= b ==> f j /\ f (SUC b)
80*)
81Theorem every_range_split_last:
82 !f a b. a <= b ==>
83 ((!j. a <= j /\ j <= SUC b ==> f j) <=> (f (SUC b) /\ !j. a <= j /\ j <= b ==> f j))
84Proof
85 rpt strip_tac >>
86 `!j. j <= SUC b <=> j <= b \/ j = SUC b` by decide_tac >>
87 metis_tac[]
88QED
89
90(* Theorem: a <= b ==> ((!j. a <= j /\ j <= b ==> f j) <=> (f a /\ f b /\ !j. a < j /\ j < b ==> f j)) *)
91(* Proof:
92 !j. a <= j /\ j <= b ==> f j
93 <=> !j. (a < j \/ a = j) /\ (j < b \/ j = b) ==> f j by arithmetic
94 <=> !j. a = j ==> f j /\ j = b ==> f j /\ !j. a < j /\ j < b ==> f j by LEFT_AND_OVER_OR, DISJ_IMP_THM
95 <=> f a /\ f b /\ !j. a < j /\ j < b ==> f j
96*)
97Theorem every_range_less_ends:
98 !f a b. a <= b ==>
99 ((!j. a <= j /\ j <= b ==> f j) <=> (f a /\ f b /\ !j. a < j /\ j < b ==> f j))
100Proof
101 rpt strip_tac >>
102 `!m n. m <= n <=> m < n \/ m = n` by decide_tac >>
103 metis_tac[]
104QED
105
106(* Theorem: a < b /\ f a /\ ~f b ==>
107 ?m. a <= m /\ m < b /\ (!j. a <= j /\ j <= m ==> f j) /\ ~f (SUC m) *)
108(* Proof:
109 Let s = {p | a <= p /\ p < b /\ (!j. a <= j /\ j <= p ==> f j)}
110 Pick m = MAX_SET s.
111 Note f a ==> a IN s by every_range_sing
112 so s <> {} by MEMBER_NOT_EMPTY
113 Also s SUBSET (count b) by SUBSET_DEF
114 so FINITE s by FINITE_COUNT, SUBSET_FINITE
115 ==> m IN s by MAX_SET_IN_SET
116 Thus a <= m /\ m < b /\ (!j. a <= j /\ j <= m ==> f j)
117 It remains to show: ~f (SUC m).
118 By contradiction, suppose f (SUC m).
119 Since m < b, SUC m <= b.
120 But ~f b, so SUC m <> b by given
121 Thus a <= m < SUC m, and SUC m < b,
122 and !j. a <= j /\ j <= SUC m ==> f j)
123 ==> SUC m IN s by every_range_split_last
124 Then SUC m <= m by X_LE_MAX_SET
125 which is impossible by LESS_SUC
126*)
127Theorem every_range_span_max:
128 !f a b. a < b /\ f a /\ ~f b ==>
129 ?m. a <= m /\ m < b /\ (!j. a <= j /\ j <= m ==> f j) /\ ~f (SUC m)
130Proof
131 rpt strip_tac >>
132 qabbrev_tac `s = {p | a <= p /\ p < b /\ (!j. a <= j /\ j <= p ==> f j)}` >>
133 qabbrev_tac `m = MAX_SET s` >>
134 qexists_tac `m` >>
135 `a IN s` by fs[every_range_sing, Abbr`s`] >>
136 `s SUBSET (count b)` by fs[SUBSET_DEF, Abbr`s`] >>
137 `FINITE s /\ s <> {}` by metis_tac[FINITE_COUNT, SUBSET_FINITE, MEMBER_NOT_EMPTY] >>
138 `m IN s` by fs[MAX_SET_IN_SET, Abbr`m`] >>
139 rfs[Abbr`s`] >>
140 spose_not_then strip_assume_tac >>
141 qabbrev_tac `s = {p | a <= p /\ p < b /\ (!j. a <= j /\ j <= p ==> f j)}` >>
142 `SUC m <> b` by metis_tac[] >>
143 `a <= SUC m /\ SUC m < b` by decide_tac >>
144 `SUC m IN s` by fs[every_range_split_last, Abbr`s`] >>
145 `SUC m <= m` by simp[X_LE_MAX_SET, Abbr`m`] >>
146 decide_tac
147QED
148
149(* Theorem: a < b /\ ~f a /\ f b ==>
150 ?m. a < m /\ m <= b /\ (!j. m <= j /\ j <= b ==> f j) /\ ~f (PRE m) *)
151(* Proof:
152 Let s = {p | a < p /\ p <= b /\ (!j. p <= j /\ j <= b ==> f j)}
153 Pick m = MIN_SET s.
154 Note f b ==> b IN s by every_range_sing
155 so s <> {} by MEMBER_NOT_EMPTY
156 ==> m IN s by MIN_SET_IN_SET
157 Thus a < m /\ m <= b /\ (!j. m <= j /\ j <= b ==> f j)
158 It remains to show: ~f (PRE m).
159 By contradiction, suppose f (PRE m).
160 Since a < m, a <= PRE m.
161 But ~f a, so PRE m <> a by given
162 Thus a < PRE m, and PRE m <= b,
163 and !j. PRE m <= j /\ j <= b ==> f j)
164 ==> PRE m IN s by every_range_split_head
165 Then m <= PRE m by MIN_SET_PROPERTY
166 which is impossible by PRE_LESS, a < m ==> 0 < m
167*)
168Theorem every_range_span_min:
169 !f a b. a < b /\ ~f a /\ f b ==>
170 ?m. a < m /\ m <= b /\ (!j. m <= j /\ j <= b ==> f j) /\ ~f (PRE m)
171Proof
172 rpt strip_tac >>
173 qabbrev_tac `s = {p | a < p /\ p <= b /\ (!j. p <= j /\ j <= b ==> f j)}` >>
174 qabbrev_tac `m = MIN_SET s` >>
175 qexists_tac `m` >>
176 `b IN s` by fs[every_range_sing, Abbr`s`] >>
177 `s <> {}` by metis_tac[MEMBER_NOT_EMPTY] >>
178 `m IN s` by fs[MIN_SET_IN_SET, Abbr`m`] >>
179 rfs[Abbr`s`] >>
180 spose_not_then strip_assume_tac >>
181 qabbrev_tac `s = {p | a < p /\ p <= b /\ (!j. p <= j /\ j <= b ==> f j)}` >>
182 `PRE m <> a` by metis_tac[] >>
183 `a < PRE m /\ PRE m <= b` by decide_tac >>
184 `PRE m IN s` by fs[every_range_split_head, Abbr`s`] >>
185 `m <= PRE m` by simp[MIN_SET_PROPERTY, Abbr`m`] >>
186 decide_tac
187QED
188
189(* Theorem: ?j. a <= j /\ j <= a <=> (j = a) *)
190(* Proof: trivial by arithmetic. *)
191Theorem exists_range_sing:
192 !a. ?j. a <= j /\ j <= a <=> (j = a)
193Proof
194 metis_tac[LESS_EQ_REFL]
195QED
196
197(* Theorem: a <= b ==>
198 ((?j. a <= j /\ j <= b /\ f j) <=> (f a \/ ?j. a + 1 <= j /\ j <= b /\ f j)) *)
199(* Proof:
200 If part: ?j. a <= j /\ j <= b /\ f j ==>
201 f a \/ ?j. a + 1 <= j /\ j <= b /\ f j
202 This is trivial since a + 1 = SUC a.
203 Only-if part: f a /\ ?j. a + 1 <= j /\ j <= b /\ f j ==>
204 ?j. a <= j /\ j <= b /\ f j
205 Note a <= j <=> a = j or a < j by arithmetic
206 If a = j, this is trivial.
207 If a < j, then a + 1 <= j, also trivial.
208*)
209Theorem exists_range_cons:
210 !f a b. a <= b ==>
211 ((?j. a <= j /\ j <= b /\ f j) <=> (f a \/ ?j. a + 1 <= j /\ j <= b /\ f j))
212Proof
213 rw[EQ_IMP_THM] >| [
214 `(a = j) \/ (a < j)` by decide_tac >-
215 fs[] >>
216 `a + 1 <= j` by decide_tac >>
217 metis_tac[],
218 metis_tac[LESS_EQ_REFL],
219 `a <= j` by decide_tac >>
220 metis_tac[]
221 ]
222QED
223
224(* ------------------------------------------------------------------------- *)
225(* List Range *)
226(* ------------------------------------------------------------------------- *)
227
228Definition listRangeINC_def:
229 listRangeINC m n = GENLIST (\i. m + i) (n + 1 - m)
230End
231
232val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
233 fixity = Closefix,
234 paren_style = OnlyIfNecessary,
235 pp_elements = [TOK "[", TM, HardSpace 1, TOK "..",
236 BreakSpace(1,1), TM, BreakSpace(0,0),
237 TOK "]"],
238 term_name = "listRangeINC" }
239
240Theorem listRangeINC_SING[simp]:
241 [m .. m] = [m]
242Proof
243 SIMP_TAC (srw_ss()) [listRangeINC_def]
244QED
245
246Theorem MEM_listRangeINC[simp]:
247 MEM x [m .. n] <=> m <= x /\ x <= n
248Proof
249 SIMP_TAC (srw_ss() ++ ARITH_ss)
250 [listRangeINC_def, MEM_GENLIST, EQ_IMP_THM] THEN
251 STRIP_TAC THEN Q.EXISTS_TAC `x - m` THEN DECIDE_TAC
252QED
253
254Theorem listRangeINC_CONS:
255 m <= n ==> ([m .. n] = m :: [m+1 .. n])
256Proof
257 SIMP_TAC (srw_ss()) [listRangeINC_def] THEN STRIP_TAC THEN
258 `(n + 1 - m = SUC (n - m)) /\ (n + 1 - (m + 1) = n - m)` by DECIDE_TAC THEN
259 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) [GENLIST_CONS, GENLIST_FUN_EQ]
260QED
261
262Theorem listRangeINC_EMPTY:
263 n < m ==> ([m .. n] = [])
264Proof
265 SRW_TAC [][listRangeINC_def] THEN
266 `n + 1 - m = 0` by DECIDE_TAC THEN SRW_TAC[][]
267QED
268
269Definition listRangeLHI_def:
270 listRangeLHI m n = GENLIST (\i. m + i) (n - m)
271End
272
273val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
274 fixity = Closefix,
275 paren_style = OnlyIfNecessary,
276 pp_elements = [TOK "[", TM, HardSpace 1, TOK "..<",
277 BreakSpace(1,1), TM, BreakSpace(0,0),
278 TOK "]"],
279 term_name = "listRangeLHI" }
280
281Theorem listRangeLHI_EQ[simp]:
282 [m ..< m] = []
283Proof
284 SRW_TAC[][listRangeLHI_def]
285QED
286
287Theorem MEM_listRangeLHI[simp]:
288 MEM x [m ..< n] <=> m <= x /\ x < n
289Proof
290 SRW_TAC[ARITH_ss][listRangeLHI_def, MEM_GENLIST, EQ_IMP_THM] THEN
291 Q.EXISTS_TAC `x - m` THEN DECIDE_TAC
292QED
293
294Theorem listRangeLHI_EMPTY:
295 hi <= lo ==> ([lo ..< hi] = [])
296Proof
297 SRW_TAC[][listRangeLHI_def] THEN
298 `hi - lo = 0` by DECIDE_TAC THEN
299 SRW_TAC[][]
300QED
301
302Theorem listRangeLHI_CONS:
303 lo < hi ==> ([lo ..< hi] = lo :: [lo + 1 ..< hi])
304Proof
305 SRW_TAC[][listRangeLHI_def] THEN
306 `hi - lo = SUC (hi - (lo + 1))` by DECIDE_TAC THEN
307 SRW_TAC[ARITH_ss][listTheory.GENLIST_CONS, listTheory.GENLIST_FUN_EQ]
308QED
309
310Theorem listRangeLHI_ALL_DISTINCT[simp]:
311 ALL_DISTINCT [lo ..< hi]
312Proof
313 Induct_on `hi - lo` THEN SRW_TAC[][listRangeLHI_EMPTY] THEN
314 `lo < hi` by DECIDE_TAC THEN
315 SRW_TAC[ARITH_ss][listRangeLHI_CONS]
316QED
317
318Theorem LENGTH_listRangeLHI[simp]:
319 LENGTH [lo ..< hi] = hi - lo
320Proof
321 SRW_TAC[][listRangeLHI_def]
322QED
323
324Theorem EL_listRangeLHI:
325 lo + i < hi ==> (EL i [lo ..< hi] = lo + i)
326Proof
327 Q.ID_SPEC_TAC `i` THEN Induct_on `hi - lo` THEN
328 SRW_TAC[ARITH_ss][listRangeLHI_EMPTY] THEN
329 `lo < hi` by DECIDE_TAC THEN
330 SRW_TAC[ARITH_ss][listRangeLHI_CONS] THEN
331 Cases_on `i` THEN
332 SRW_TAC[ARITH_ss][]
333QED
334
335(* Theorem: [m .. n] = [m ..< SUC n] *)
336(* Proof:
337 = [m .. n]
338 = GENLIST (\i. m + i) (n + 1 - m) by listRangeINC_def
339 = [m ..< (n + 1)] by listRangeLHI_def
340 = [m ..< SUC n] by ADD1
341*)
342Theorem listRangeINC_to_LHI:
343 !m n. [m .. n] = [m ..< SUC n]
344Proof
345 rw[listRangeLHI_def, listRangeINC_def, ADD1]
346QED
347
348(* Theorem: set [1 .. n] = IMAGE SUC (count n) *)
349(* Proof:
350 x IN set [1 .. n]
351 <=> 1 <= x /\ x <= n by listRangeINC_MEM
352 <=> 0 < x /\ PRE x < n by arithmetic
353 <=> 0 < SUC (PRE x) /\ PRE x < n by SUC_PRE, 0 < x
354 <=> x IN IMAGE SUC (count n) by IN_COUNT, IN_IMAGE
355*)
356Theorem listRangeINC_SET:
357 !n. set [1 .. n] = IMAGE SUC (count n)
358Proof
359 rw[EXTENSION, EQ_IMP_THM] >>
360 `0 < x /\ PRE x < n` by decide_tac >>
361 metis_tac[SUC_PRE]
362QED
363
364(* Theorem: LENGTH [m .. n] = n + 1 - m *)
365(* Proof:
366 LENGTH [m .. n]
367 = LENGTH (GENLIST (\i. m + i) (n + 1 - m)) by listRangeINC_def
368 = n + 1 - m by LENGTH_GENLIST
369*)
370Theorem listRangeINC_LEN:
371 !m n. LENGTH [m .. n] = n + 1 - m
372Proof
373 rw[listRangeINC_def]
374QED
375
376(* Theorem: ([m .. n] = []) <=> (n + 1 <= m) *)
377(* Proof:
378 [m .. n] = []
379 <=> LENGTH [m .. n] = 0 by LENGTH_NIL
380 <=> n + 1 - m = 0 by listRangeINC_LEN
381 <=> n + 1 <= m by arithmetic
382*)
383Theorem listRangeINC_NIL:
384 !m n. ([m .. n] = []) <=> (n + 1 <= m)
385Proof
386 metis_tac[listRangeINC_LEN, LENGTH_NIL, DECIDE``(n + 1 - m = 0) <=> (n + 1 <= m)``]
387QED
388
389(* Rename a theorem *)
390Theorem listRangeINC_MEM =
391 MEM_listRangeINC |> GEN ``x:num`` |> GEN ``n:num`` |> GEN ``m:num``;
392(*
393val listRangeINC_MEM = |- !m n x. MEM x [m .. n] <=> m <= x /\ x <= n: thm
394*)
395
396(*
397EL_listRangeLHI
398|- lo + i < hi ==> EL i [lo ..< hi] = lo + i
399*)
400
401(* Theorem: m + i <= n ==> (EL i [m .. n] = m + i) *)
402(* Proof: by listRangeINC_def *)
403Theorem listRangeINC_EL:
404 !m n i. m + i <= n ==> (EL i [m .. n] = m + i)
405Proof
406 rw[listRangeINC_def]
407QED
408
409(* Theorem: EVERY P [m .. n] <=> !x. m <= x /\ x <= n ==> P x *)
410(* Proof:
411 EVERY P [m .. n]
412 <=> !x. MEM x [m .. n] ==> P x by EVERY_MEM
413 <=> !x. m <= x /\ x <= n ==> P x by MEM_listRangeINC
414*)
415Theorem listRangeINC_EVERY:
416 !P m n. EVERY P [m .. n] <=> !x. m <= x /\ x <= n ==> P x
417Proof
418 rw[EVERY_MEM, MEM_listRangeINC]
419QED
420
421
422(* Theorem: EXISTS P [m .. n] <=> ?x. m <= x /\ x <= n /\ P x *)
423(* Proof:
424 EXISTS P [m .. n]
425 <=> ?x. MEM x [m .. n] /\ P x by EXISTS_MEM
426 <=> ?x. m <= x /\ x <= n /\ P e by MEM_listRangeINC
427*)
428Theorem listRangeINC_EXISTS:
429 !P m n. EXISTS P [m .. n] <=> ?x. m <= x /\ x <= n /\ P x
430Proof
431 metis_tac[EXISTS_MEM, MEM_listRangeINC]
432QED
433
434(* Theorem: EVERY P [m .. n] <=> ~(EXISTS ($~ o P) [m .. n]) *)
435(* Proof:
436 EVERY P [m .. n]
437 <=> !x. m <= x /\ x <= n ==> P x by listRangeINC_EVERY
438 <=> ~(?x. m <= x /\ x <= n /\ ~(P x)) by negation
439 <=> ~(EXISTS ($~ o P) [m .. m]) by listRangeINC_EXISTS
440*)
441Theorem listRangeINC_EVERY_EXISTS:
442 !P m n. EVERY P [m .. n] <=> ~(EXISTS ($~ o P) [m .. n])
443Proof
444 rw[listRangeINC_EVERY, listRangeINC_EXISTS]
445QED
446
447(* Theorem: EXISTS P [m .. n] <=> ~(EVERY ($~ o P) [m .. n]) *)
448(* Proof:
449 EXISTS P [m .. n]
450 <=> ?x. m <= x /\ x <= m /\ P x by listRangeINC_EXISTS
451 <=> ~(!x. m <= x /\ x <= n ==> ~(P x)) by negation
452 <=> ~(EVERY ($~ o P) [m .. n]) by listRangeINC_EVERY
453*)
454Theorem listRangeINC_EXISTS_EVERY:
455 !P m n. EXISTS P [m .. n] <=> ~(EVERY ($~ o P) [m .. n])
456Proof
457 rw[listRangeINC_EXISTS, listRangeINC_EVERY]
458QED
459
460(* Theorem: m <= n + 1 ==> ([m .. (n + 1)] = SNOC (n + 1) [m .. n]) *)
461(* Proof:
462 [m .. (n + 1)]
463 = GENLIST (\i. m + i) ((n + 1) + 1 - m) by listRangeINC_def
464 = GENLIST (\i. m + i) (1 + (n + 1 - m)) by arithmetic
465 = GENLIST (\i. m + i) (n + 1 - m) ++ GENLIST (\t. (\i. m + i) (t + n + 1 - m)) 1 by GENLIST_APPEND
466 = [m .. n] ++ GENLIST (\t. (\i. m + i) (t + n + 1 - m)) 1 by listRangeINC_def
467 = [m .. n] ++ [(\t. (\i. m + i) (t + n + 1 - m)) 0] by GENLIST_1
468 = [m .. n] ++ [m + n + 1 - m] by function evaluation
469 = [m .. n] ++ [n + 1] by arithmetic
470 = SNOC (n + 1) [m .. n] by SNOC_APPEND
471*)
472Theorem listRangeINC_SNOC:
473 !m n. m <= n + 1 ==> ([m .. (n + 1)] = SNOC (n + 1) [m .. n])
474Proof
475 rw[listRangeINC_def, SNOC_APPEND] >>
476 `(n + 2 - m = 1 + (n + 1 - m)) /\ (n + 1 - m + m = n + 1)` by decide_tac >>
477 rw_tac std_ss [GENLIST_APPEND, GENLIST_1]
478QED
479
480(* Theorem: m <= n + 1 ==> (FRONT [m .. (n + 1)] = [m .. n]) *)
481(* Proof:
482 FRONT [m .. (n + 1)]
483 = FRONT (SNOC (n + 1) [m .. n])) by listRangeINC_SNOC
484 = [m .. n] by FRONT_SNOC
485*)
486Theorem listRangeINC_FRONT:
487 !m n. m <= n + 1 ==> (FRONT [m .. (n + 1)] = [m .. n])
488Proof
489 simp[listRangeINC_SNOC, FRONT_SNOC]
490QED
491
492(* Theorem: m <= n ==> (LAST [m .. n] = n) *)
493(* Proof:
494 Let ls = [m .. n]
495 Note ls <> [] by listRangeINC_NIL
496 so LAST ls
497 = EL (PRE (LENGTH ls)) ls by LAST_EL
498 = EL (PRE (n + 1 - m)) ls by listRangeINC_LEN
499 = EL (n - m) ls by arithmetic
500 = n by listRangeINC_EL
501 Or
502 LAST [m .. n]
503 = LAST (GENLIST (\i. m + i) (n + 1 - m)) by listRangeINC_def
504 = LAST (GENLIST (\i. m + i) (SUC (n - m)) by arithmetic, m <= n
505 = (\i. m + i) (n - m) by GENLIST_LAST
506 = m + (n - m) by function application
507 = n by m <= n
508 Or
509 If n = 0, then m <= 0 means m = 0.
510 LAST [0 .. 0] = LAST [0] = 0 = n by LAST_DEF
511 Otherwise n = SUC k.
512 LAST [m .. n]
513 = LAST (SNOC n [m .. k]) by listRangeINC_SNOC, ADD1
514 = n by LAST_SNOC
515*)
516Theorem listRangeINC_LAST:
517 !m n. m <= n ==> (LAST [m .. n] = n)
518Proof
519 rpt strip_tac >>
520 Cases_on `n` >-
521 fs[] >>
522 metis_tac[listRangeINC_SNOC, LAST_SNOC, ADD1]
523QED
524
525(* Theorem: REVERSE [m .. n] = MAP (\x. n - x + m) [m .. n] *)
526(* Proof:
527 REVERSE [m .. n]
528 = REVERSE (GENLIST (\i. m + i) (n + 1 - m)) by listRangeINC_def
529 = GENLIST (\x. (\i. m + i) (PRE (n + 1 - m) - x)) (n + 1 - m) by REVERSE_GENLIST
530 = GENLIST (\x. (\i. m + i) (n - m - x)) (n + 1 - m) by PRE
531 = GENLIST (\x. (m + n - m - x) (n + 1 - m) by function application
532 = GENLIST (\x. n - x) (n + 1 - m) by arithmetic
533
534 MAP (\x. n - x + m) [m .. n]
535 = MAP (\x. n - x + m) (GENLIST (\i. m + i) (n + 1 - m)) by listRangeINC_def
536 = GENLIST ((\x. n - x + m) o (\i. m + i)) (n + 1 - m) by MAP_GENLIST
537 = GENLIST (\i. n - (m + i) + m) (n + 1 - m) by function composition
538 = GENLIST (\i. n - i) (n + 1 - m) by arithmetic
539*)
540Theorem listRangeINC_REVERSE:
541 !m n. REVERSE [m .. n] = MAP (\x. n - x + m) [m .. n]
542Proof
543 rpt strip_tac >>
544 `(\m'. PRE (n + 1 - m) - m' + m) = ((\x. n - x + m) o (\i. i + m))`
545 by rw[FUN_EQ_THM, combinTheory.o_THM] >>
546 rw[listRangeINC_def, REVERSE_GENLIST, MAP_GENLIST]
547QED
548
549(* Theorem: REVERSE (MAP f [m .. n]) = MAP (f o (\x. n - x + m)) [m .. n] *)
550(* Proof:
551 REVERSE (MAP f [m .. n])
552 = MAP f (REVERSE [m .. n]) by MAP_REVERSE
553 = MAP f (MAP (\x. n - x + m) [m .. n]) by listRangeINC_REVERSE
554 = MAP (f o (\x. n - x + m)) [m .. n] by MAP_MAP_o
555*)
556Theorem listRangeINC_REVERSE_MAP:
557 !f m n. REVERSE (MAP f [m .. n]) = MAP (f o (\x. n - x + m)) [m .. n]
558Proof
559 metis_tac[MAP_REVERSE, listRangeINC_REVERSE, MAP_MAP_o]
560QED
561
562(* Theorem: MAP f [(m + 1) .. (n + 1)] = MAP (f o SUC) [m .. n] *)
563(* Proof:
564 Note (\i. (m + 1) + i) = SUC o (\i. (m + i)) by FUN_EQ_THM
565 MAP f [(m + 1) .. (n + 1)]
566 = MAP f (GENLIST (\i. (m + 1) + i) ((n + 1) + 1 - (m + 1))) by listRangeINC_def
567 = MAP f (GENLIST (\i. (m + 1) + i) (n + 1 - m)) by arithmetic
568 = MAP f (GENLIST (SUC o (\i. (m + i))) (n + 1 - m)) by above
569 = MAP (f o SUC) (GENLIST (\i. (m + i)) (n + 1 - m)) by MAP_GENLIST
570 = MAP (f o SUC) [m .. n] by listRangeINC_def
571*)
572Theorem listRangeINC_MAP_SUC:
573 !f m n. MAP f [(m + 1) .. (n + 1)] = MAP (f o SUC) [m .. n]
574Proof
575 rpt strip_tac >>
576 `(\i. (m + 1) + i) = SUC o (\i. (m + i))` by rw[FUN_EQ_THM] >>
577 rw[listRangeINC_def, MAP_GENLIST]
578QED
579
580(* Theorem: a <= b /\ b <= c ==> ([a .. b] ++ [(b + 1) .. c] = [a .. c]) *)
581(* Proof:
582 By listRangeINC_def, this is to show:
583 GENLIST (\i. a + i) (b + 1 - a) ++ GENLIST (\i. b + (i + 1)) (c - b) = GENLIST (\i. a + i) (c + 1 - a)
584 Let f = \i. a + i.
585 Note (\t. f (t + (b + 1 - a))) = (\i. b + (i + 1)) by FUN_EQ_THM
586 Thus GENLIST (\i. b + (i + 1)) (c - b) = GENLIST (\t. f (t + (b + 1 - a))) (c - b) by GENLIST_FUN_EQ
587 Now (c - b) + (b + 1 - a) = c + 1 - a by a <= b /\ b <= c
588 The result follows by GENLIST_APPEND
589*)
590Theorem listRangeINC_APPEND:
591 !a b c. a <= b /\ b <= c ==> ([a .. b] ++ [(b + 1) .. c] = [a .. c])
592Proof
593 rw[listRangeINC_def] >>
594 qabbrev_tac `f = \i. a + i` >>
595 `(\t. f (t + (b + 1 - a))) = (\i. b + (i + 1))` by rw[FUN_EQ_THM, Abbr`f`] >>
596 `GENLIST (\i. b + (i + 1)) (c - b) = GENLIST (\t. f (t + (b + 1 - a))) (c - b)` by rw[GSYM GENLIST_FUN_EQ] >>
597 `(c - b) + (b + 1 - a) = c + 1 - a` by decide_tac >>
598 metis_tac[GENLIST_APPEND]
599QED
600
601(* Theorem: SUM [m .. n] = SUM [1 .. n] - SUM [1 .. (m - 1)] *)
602(* Proof:
603 If m = 0,
604 Then [1 .. (m-1)] = [1 .. 0] = [] by listRangeINC_EMPTY
605 SUM [0 .. n]
606 = SUM (0::[1 .. n]) by listRangeINC_CONS
607 = 0 + SUM [1 .. n] by SUM_CONS
608 = SUM [1 .. n] - 0 by arithmetic
609 = SUM [1 .. n] - SUM [] by SUM_NIL
610 If m = 1,
611 Then [1 .. (m-1)] = [1 .. 0] = [] by listRangeINC_EMPTY
612 SUM [1 .. n]
613 = SUM [1 .. n] - 0 by arithmetic
614 = SUM [1 .. n] - SUM [] by SUM_NIL
615 Otherwise 1 < m, or 1 <= m - 1.
616 If n < m,
617 Then SUM [m .. n] = 0 by listRangeINC_EMPTY
618 If n = 0,
619 Then SUM [1 .. 0] = 0 by listRangeINC_EMPTY
620 and 0 - SUM [1 .. (m - 1)] = 0 by integer subtraction
621 If n <> 0,
622 Then 1 <= n /\ n <= m - 1 by arithmetic
623 ==> [1 .. m - 1] =
624 [1 .. n] ++ [(n + 1) .. (m - 1)] by listRangeINC_APPEND
625 or SUM [1 .. m - 1]
626 = SUM [1 .. n] + SUM [(n + 1) .. (m - 1)] by SUM_APPEND
627 Thus SUM [1 .. n] - SUM [1 .. m - 1] = 0 by subtraction
628 If ~(n < m), then m <= n.
629 Note m - 1 < n /\ (m - 1 + 1 = m) by arithmetic
630 Thus [1 .. n] = [1 .. (m - 1)] ++ [m .. n] by listRangeINC_APPEND
631 or SUM [1 .. n]
632 = SUM [1 .. (m - 1)] + SUM [m .. n] by SUM_APPEND
633 The result follows by subtraction
634*)
635Theorem listRangeINC_SUM:
636 !m n. SUM [m .. n] = SUM [1 .. n] - SUM [1 .. (m - 1)]
637Proof
638 rpt strip_tac >>
639 Cases_on `m = 0` >-
640 rw[listRangeINC_EMPTY, listRangeINC_CONS] >>
641 Cases_on `m = 1` >-
642 rw[listRangeINC_EMPTY] >>
643 Cases_on `n < m` >| [
644 Cases_on `n = 0` >-
645 rw[listRangeINC_EMPTY] >>
646 `1 <= n /\ n <= m - 1` by decide_tac >>
647 `[1 .. m - 1] = [1 .. n] ++ [(n + 1) .. (m - 1)]` by rw[listRangeINC_APPEND] >>
648 `SUM [1 .. m - 1] = SUM [1 .. n] + SUM [(n + 1) .. (m - 1)]` by rw[GSYM SUM_APPEND] >>
649 `SUM [m .. n] = 0` by rw[listRangeINC_EMPTY] >>
650 decide_tac,
651 `1 <= m - 1 /\ m - 1 <= n /\ (m - 1 + 1 = m)` by decide_tac >>
652 `[1 .. n] = [1 .. (m - 1)] ++ [m .. n]` by metis_tac[listRangeINC_APPEND] >>
653 `SUM [1 .. n] = SUM [1 .. (m - 1)] + SUM [m .. n]` by rw[GSYM SUM_APPEND] >>
654 decide_tac
655 ]
656QED
657
658(* Theorem: [1 .. n] = GENLIST SUC n *)
659(* Proof: by listRangeINC_def *)
660Theorem listRangeINC_1_n:
661 !n. [1 .. n] = GENLIST SUC n
662Proof
663 rpt strip_tac >>
664 `(\i. i + 1) = SUC` by rw[FUN_EQ_THM] >>
665 rw[listRangeINC_def]
666QED
667
668(* Theorem: MAP f [1 .. n] = GENLIST (f o SUC) n *)
669(* Proof:
670 MAP f [1 .. n]
671 = MAP f (GENLIST SUC n) by listRangeINC_1_n
672 = GENLIST (f o SUC) n by MAP_GENLIST
673*)
674Theorem listRangeINC_MAP:
675 !f n. MAP f [1 .. n] = GENLIST (f o SUC) n
676Proof
677 rw[listRangeINC_1_n, MAP_GENLIST]
678QED
679
680(* Theorem: SUM (MAP f [1 .. (SUC n)]) = f (SUC n) + SUM (MAP f [1 .. n]) *)
681(* Proof:
682 SUM (MAP f [1 .. (SUC n)])
683 = SUM (MAP f (SNOC (SUC n) [1 .. n])) by listRangeINC_SNOC
684 = SUM (SNOC (f (SUC n)) (MAP f [1 .. n])) by MAP_SNOC
685 = f (SUC n) + SUM (MAP f [1 .. n]) by SUM_SNOC
686*)
687Theorem listRangeINC_SUM_MAP:
688 !f n. SUM (MAP f [1 .. (SUC n)]) = f (SUC n) + SUM (MAP f [1 .. n])
689Proof
690 rw[listRangeINC_SNOC, MAP_SNOC, SUM_SNOC, ADD1]
691QED
692
693(* Theorem: m < j /\ j <= n ==> [m .. n] = [m .. j-1] ++ j::[j+1 .. n] *)
694(* Proof:
695 Note m < j implies m <= j-1.
696 [m .. n]
697 = [m .. j-1] ++ [j .. n] by listRangeINC_APPEND, m <= j-1
698 = [m .. j-1] ++ j::[j+1 .. n] by listRangeINC_CONS, j <= n
699*)
700Theorem listRangeINC_SPLIT:
701 !m n j. m < j /\ j <= n ==> [m .. n] = [m .. j-1] ++ j::[j+1 .. n]
702Proof
703 rpt strip_tac >>
704 `m <= j - 1 /\ j - 1 <= n /\ (j - 1) + 1 = j` by decide_tac >>
705 `[m .. n] = [m .. j-1] ++ [j .. n]` by metis_tac[listRangeINC_APPEND] >>
706 simp[listRangeINC_CONS]
707QED
708
709(* Theorem: [m ..< (n + 1)] = [m .. n] *)
710(* Proof:
711 [m ..< (n + 1)]
712 = GENLIST (\i. m + i) (n + 1 - m) by listRangeLHI_def
713 = [m .. n] by listRangeINC_def
714*)
715Theorem listRangeLHI_to_INC:
716 !m n. [m ..< (n + 1)] = [m .. n]
717Proof
718 rw[listRangeLHI_def, listRangeINC_def]
719QED
720
721(* Theorem: set [0 ..< n] = count n *)
722(* Proof:
723 x IN set [0 ..< n]
724 <=> 0 <= x /\ x < n by listRangeLHI_MEM
725 <=> x < n by arithmetic
726 <=> x IN count n by IN_COUNT
727*)
728Theorem listRangeLHI_SET:
729 !n. set [0 ..< n] = count n
730Proof
731 simp[EXTENSION]
732QED
733
734(* Theorem alias *)
735Theorem listRangeLHI_LEN = LENGTH_listRangeLHI |> GEN_ALL |> SPEC ``m:num`` |> SPEC ``n:num`` |> GEN_ALL;
736(* val listRangeLHI_LEN = |- !n m. LENGTH [m ..< n] = n - m: thm *)
737
738(* Theorem: ([m ..< n] = []) <=> n <= m *)
739(* Proof:
740 If n = 0, LHS = T, RHS = T hence true.
741 If n <> 0, then n = SUC k by num_CASES
742 [m ..< n] = []
743 <=> [m ..< SUC k] = [] by n = SUC k
744 <=> [m .. k] = [] by listRangeLHI_to_INC
745 <=> k + 1 <= m by listRangeINC_NIL
746 <=> n <= m by ADD1
747*)
748Theorem listRangeLHI_NIL:
749 !m n. ([m ..< n] = []) <=> n <= m
750Proof
751 rpt strip_tac >>
752 Cases_on `n` >-
753 rw[listRangeLHI_def] >>
754 rw[listRangeLHI_to_INC, listRangeINC_NIL, ADD1]
755QED
756
757(* Theorem: MEM x [m ..< n] <=> m <= x /\ x < n *)
758(* Proof: by MEM_listRangeLHI *)
759Theorem listRangeLHI_MEM:
760 !m n x. MEM x [m ..< n] <=> m <= x /\ x < n
761Proof
762 rw[MEM_listRangeLHI]
763QED
764
765(* Theorem: m + i < n ==> EL i [m ..< n] = m + i *)
766(* Proof: EL_listRangeLHI *)
767Theorem listRangeLHI_EL:
768 !m n i. m + i < n ==> (EL i [m ..< n] = m + i)
769Proof
770 rw[EL_listRangeLHI]
771QED
772
773(* Theorem: EVERY P [m ..< n] <=> !x. m <= x /\ x < n ==> P x *)
774(* Proof:
775 EVERY P [m ..< n]
776 <=> !x. MEM x [m ..< n] ==> P e by EVERY_MEM
777 <=> !x. m <= x /\ x < n ==> P e by MEM_listRangeLHI
778*)
779Theorem listRangeLHI_EVERY:
780 !P m n. EVERY P [m ..< n] <=> !x. m <= x /\ x < n ==> P x
781Proof
782 rw[EVERY_MEM, MEM_listRangeLHI]
783QED
784
785(* Theorem: m <= n ==> ([m ..< n + 1] = SNOC n [m ..< n]) *)
786(* Proof:
787 If n = 0,
788 Then m = 0 by m <= n
789 LHS = [0 ..< 1] = [0]
790 RHS = SNOC 0 [0 ..< 0]
791 = SNOC 0 [] by listRangeLHI_def
792 = [0] = LHS by SNOC
793 If n <> 0,
794 Then n = (n - 1) + 1 by arithmetic
795 [m ..< n + 1]
796 = [m .. n] by listRangeLHI_to_INC
797 = SNOC n [m .. n - 1] by listRangeINC_SNOC, m <= (n - 1) + 1
798 = SNOC n [m ..< n] by listRangeLHI_to_INC
799*)
800Theorem listRangeLHI_SNOC:
801 !m n. m <= n ==> ([m ..< n + 1] = SNOC n [m ..< n])
802Proof
803 rpt strip_tac >>
804 Cases_on `n = 0` >| [
805 `m = 0` by decide_tac >>
806 rw[listRangeLHI_def],
807 `n = (n - 1) + 1` by decide_tac >>
808 `[m ..< n + 1] = [m .. n]` by rw[listRangeLHI_to_INC] >>
809 `_ = SNOC n [m .. n - 1]` by metis_tac[listRangeINC_SNOC] >>
810 `_ = SNOC n [m ..< n]` by rw[GSYM listRangeLHI_to_INC] >>
811 rw[]
812 ]
813QED
814
815(* Theorem: m <= n ==> (FRONT [m .. < n + 1] = [m .. <n]) *)
816(* Proof:
817 FRONT [m ..< n + 1]
818 = FRONT (SNOC n [m ..< n])) by listRangeLHI_SNOC
819 = [m ..< n] by FRONT_SNOC
820*)
821Theorem listRangeLHI_FRONT:
822 !m n. m <= n ==> (FRONT [m ..< n + 1] = [m ..< n])
823Proof
824 simp[listRangeLHI_SNOC, FRONT_SNOC]
825QED
826
827(* Theorem: m <= n ==> (LAST [m ..< n + 1] = n) *)
828(* Proof:
829 LAST [m ..< n + 1]
830 = LAST (SNOC n [m ..< n]) by listRangeLHI_SNOC
831 = n by LAST_SNOC
832*)
833Theorem listRangeLHI_LAST:
834 !m n. m <= n ==> (LAST [m ..< n + 1] = n)
835Proof
836 simp[listRangeLHI_SNOC, LAST_SNOC]
837QED
838
839(* Theorem: REVERSE [m ..< n] = MAP (\x. n - 1 - x + m) [m ..< n] *)
840(* Proof:
841 If n = 0,
842 LHS = REVERSE [] by listRangeLHI_def
843 = [] by REVERSE_DEF
844 = MAP f [] = RHS by MAP
845 If n <> 0,
846 Then n = k + 1 for some k by num_CASES, ADD1
847 REVERSE [m ..< n]
848 = REVERSE [m .. k] by listRangeLHI_to_INC
849 = MAP (\x. k - x + m) [m .. k] by listRangeINC_REVERSE
850 = MAP (\x. n - 1 - x + m) [m ..< n] by listRangeLHI_to_INC
851*)
852Theorem listRangeLHI_REVERSE:
853 !m n. REVERSE [m ..< n] = MAP (\x. n - 1 - x + m) [m ..< n]
854Proof
855 rpt strip_tac >>
856 Cases_on `n` >-
857 rw[listRangeLHI_def] >>
858 `REVERSE [m ..< SUC n'] = REVERSE [m .. n']` by rw[listRangeLHI_to_INC, ADD1] >>
859 `_ = MAP (\x. n' - x + m) [m .. n']` by rw[listRangeINC_REVERSE] >>
860 `_ = MAP (\x. n' - x + m) [m ..< (SUC n')]` by rw[GSYM listRangeLHI_to_INC, ADD1] >>
861 rw[]
862QED
863
864(* Theorem: REVERSE (MAP f [m ..< n]) = MAP (f o (\x. n - 1 - x + m)) [m ..< n] *)
865(* Proof:
866 REVERSE (MAP f [m ..< n])
867 = MAP f (REVERSE [m ..< n]) by MAP_REVERSE
868 = MAP f (MAP (\x. n - 1 - x + m) [m ..< n]) by listRangeLHI_REVERSE
869 = MAP (f o (\x. n - 1 - x + m)) [m ..< n] by MAP_MAP_o
870*)
871Theorem listRangeLHI_REVERSE_MAP:
872 !f m n. REVERSE (MAP f [m ..< n]) = MAP (f o (\x. n - 1 - x + m)) [m ..< n]
873Proof
874 metis_tac[MAP_REVERSE, listRangeLHI_REVERSE, MAP_MAP_o]
875QED
876
877(* Theorem: MAP f [(m + 1) ..< (n + 1)] = MAP (f o SUC) [m ..< n] *)
878(* Proof:
879 Note (\i. (m + 1) + i) = SUC o (\i. (m + i)) by FUN_EQ_THM
880 MAP f [(m + 1) ..< (n + 1)]
881 = MAP f (GENLIST (\i. (m + 1) + i) ((n + 1) - (m + 1))) by listRangeLHI_def
882 = MAP f (GENLIST (\i. (m + 1) + i) (n - m)) by arithmetic
883 = MAP f (GENLIST (SUC o (\i. (m + i))) (n - m)) by above
884 = MAP (f o SUC) (GENLIST (\i. (m + i)) (n - m)) by MAP_GENLIST
885 = MAP (f o SUC) [m ..< n] by listRangeLHI_def
886*)
887Theorem listRangeLHI_MAP_SUC:
888 !f m n. MAP f [(m + 1) ..< (n + 1)] = MAP (f o SUC) [m ..< n]
889Proof
890 rpt strip_tac >>
891 `(\i. (m + 1) + i) = SUC o (\i. (m + i))` by rw[FUN_EQ_THM] >>
892 rw[listRangeLHI_def, MAP_GENLIST]
893QED
894
895(* Theorem: a <= b /\ b <= c ==> [a ..< b] ++ [b ..< c] = [a ..< c] *)
896(* Proof:
897 If a = b,
898 LHS = [a ..< a] ++ [a ..< c]
899 = [] ++ [a ..< c] by listRangeLHI_def
900 = [a ..< c] = RHS by APPEND
901 If a <> b,
902 Then a < b, by a <= b
903 so b <> 0, and c <> 0 by b <= c
904 Let b = b' + 1, c = c' + 1 by num_CASES, ADD1
905 Then a <= b' /\ b' <= c.
906 [a ..< b] ++ [b ..< c]
907 = [a .. b'] ++ [b' + 1 .. c'] by listRangeLHI_to_INC
908 = [a .. c'] by listRangeINC_APPEND
909 = [a ..< c] by listRangeLHI_to_INC
910*)
911Theorem listRangeLHI_APPEND:
912 !a b c. a <= b /\ b <= c ==> ([a ..< b] ++ [b ..< c] = [a ..< c])
913Proof
914 rpt strip_tac >>
915 `(a = b) \/ (a < b)` by decide_tac >-
916 rw[listRangeLHI_def] >>
917 `b <> 0 /\ c <> 0` by decide_tac >>
918 `?b' c'. (b = b' + 1) /\ (c = c' + 1)` by metis_tac[num_CASES, ADD1] >>
919 `a <= b' /\ b' <= c` by decide_tac >>
920 `[a ..< b] ++ [b ..< c] = [a .. b'] ++ [b' + 1 .. c']` by rw[listRangeLHI_to_INC] >>
921 `_ = [a .. c']` by rw[listRangeINC_APPEND] >>
922 `_ = [a ..< c]` by rw[GSYM listRangeLHI_to_INC] >>
923 rw[]
924QED
925
926(* Theorem: SUM [m ..< n] = SUM [1 ..< n] - SUM [1 ..< m] *)
927(* Proof:
928 If n = 0,
929 LHS = SUM [m ..< 0] = SUM [] = 0 by listRangeLHI_EMPTY
930 RHS = SUM [1 ..< 0] - SUM [1 ..< m]
931 = SUM [] - SUM [1 ..< m] by listRangeLHI_EMPTY
932 = 0 - SUM [1 ..< m] = 0 = LHS by integer subtraction
933 If m = 0,
934 LHS = SUM [0 ..< n]
935 = SUM (0 :: [1 ..< n]) by listRangeLHI_CONS
936 = 0 + SUM [1 ..< n] by SUM
937 = SUM [1 ..< n] by arithmetic
938 RHS = SUM [1 ..< n] - SUM [1 ..< 0] by integer subtraction
939 = SUM [1 ..< n] - SUM [] by listRangeLHI_EMPTY
940 = SUM [1 ..< n] - 0 by SUM
941 = LHS
942 Otherwise,
943 n <> 0, and m <> 0.
944 Let n = n' + 1, m = m' + 1 by num_CASES, ADD1
945 SUM [m ..< n]
946 = SUM [m .. n'] by listRangeLHI_to_INC
947 = SUM [1 .. n'] - SUM [1 .. m - 1] by listRangeINC_SUM
948 = SUM [1 .. n'] - SUM [1 .. m'] by m' = m - 1
949 = SUM [1 ..< n] - SUM [1 ..< m] by listRangeLHI_to_INC
950*)
951Theorem listRangeLHI_SUM:
952 !m n. SUM [m ..< n] = SUM [1 ..< n] - SUM [1 ..< m]
953Proof
954 rpt strip_tac >>
955 Cases_on `n = 0` >-
956 rw[listRangeLHI_EMPTY] >>
957 Cases_on `m = 0` >-
958 rw[listRangeLHI_EMPTY, listRangeLHI_CONS] >>
959 `?n' m'. (n = n' + 1) /\ (m = m' + 1)` by metis_tac[num_CASES, ADD1] >>
960 `SUM [m ..< n] = SUM [m .. n']` by rw[listRangeLHI_to_INC] >>
961 `_ = SUM [1 .. n'] - SUM [1 .. m - 1]` by rw[GSYM listRangeINC_SUM] >>
962 `_ = SUM [1 .. n'] - SUM [1 .. m']` by rw[] >>
963 `_ = SUM [1 ..< n] - SUM [1 ..< m]` by rw[GSYM listRangeLHI_to_INC] >>
964 rw[]
965QED
966
967(* Theorem: [0 ..< n] = GENLIST I n *)
968(* Proof: by listRangeINC_def *)
969Theorem listRangeLHI_0_n:
970 !n. [0 ..< n] = GENLIST I n
971Proof
972 rpt strip_tac >>
973 `(\i:num. i) = I` by rw[FUN_EQ_THM] >>
974 rw[listRangeLHI_def]
975QED
976
977(* Theorem: MAP f [0 ..< n] = GENLIST f n *)
978(* Proof:
979 MAP f [0 ..< n]
980 = MAP f (GENLIST I n) by listRangeLHI_0_n
981 = GENLIST (f o I) n by MAP_GENLIST
982 = GENLIST f n by I_THM
983*)
984Theorem listRangeLHI_MAP:
985 !f n. MAP f [0 ..< n] = GENLIST f n
986Proof
987 rw[listRangeLHI_0_n, MAP_GENLIST]
988QED
989
990(* Theorem: SUM (MAP f [0 ..< (SUC n)]) = f n + SUM (MAP f [0 ..< n]) *)
991(* Proof:
992 SUM (MAP f [0 ..< (SUC n)])
993 = SUM (MAP f (SNOC n [0 ..< n])) by listRangeLHI_SNOC
994 = SUM (SNOC (f n) (MAP f [0 ..< n])) by MAP_SNOC
995 = f n + SUM (MAP f [0 ..< n]) by SUM_SNOC
996*)
997Theorem listRangeLHI_SUM_MAP:
998 !f n. SUM (MAP f [0 ..< (SUC n)]) = f n + SUM (MAP f [0 ..< n])
999Proof
1000 rw[listRangeLHI_SNOC, MAP_SNOC, SUM_SNOC, ADD1]
1001QED
1002
1003(* Theorem: m <= j /\ j < n ==> [m ..< n] = [m ..< j] ++ j::[j+1 ..< n] *)
1004(* Proof:
1005 Note j < n implies j <= n.
1006 [m ..< n]
1007 = [m ..< j] ++ [j ..< n] by listRangeLHI_APPEND, j <= n
1008 = [m ..< j] ++ j::[j+1 ..< n] by listRangeLHI_CONS, j < n
1009*)
1010Theorem listRangeLHI_SPLIT:
1011 !m n j. m <= j /\ j < n ==> [m ..< n] = [m ..< j] ++ j::[j+1 ..< n]
1012Proof
1013 rpt strip_tac >>
1014 `[m ..< n] = [m ..< j] ++ [j ..< n]` by simp[listRangeLHI_APPEND] >>
1015 simp[listRangeLHI_CONS]
1016QED
1017
1018(* listRangeTheory.listRangeLHI_ALL_DISTINCT |- ALL_DISTINCT [lo ..< hi] *)
1019
1020(* Theorem: ALL_DISTINCT [m .. n] *)
1021(* Proof:
1022 ALL_DISTINCT [m .. n]
1023 <=> ALL_DISTINCT [m ..< n + 1] by listRangeLHI_to_INC
1024 <=> T by listRangeLHI_ALL_DISTINCT
1025*)
1026Theorem listRangeINC_ALL_DISTINCT:
1027 !m n. ALL_DISTINCT [m .. n]
1028Proof
1029 metis_tac[listRangeLHI_to_INC, listRangeLHI_ALL_DISTINCT]
1030QED
1031
1032(* Theorem: m <= n ==> EVERY P [m - 1 .. n] <=> (P (m - 1) /\ EVERY P [m ..n]) *)
1033(* Proof:
1034 EVERY P [m - 1 .. n]
1035 <=> !x. m - 1 <= x /\ x <= n ==> P x by listRangeINC_EVERY
1036 <=> !x. (m - 1 = x \/ m <= x) /\ x <= n ==> P x by arithmetic
1037 <=> !x. (x = m - 1 ==> P x) /\ m <= x /\ x <= n ==> P x
1038 by RIGHT_AND_OVER_OR, DISJ_IMP_THM
1039 <=> P (m - 1) /\ EVERY P [m .. n] by listRangeINC_EVERY
1040*)
1041Theorem listRangeINC_EVERY_split_head:
1042 !P m n. m <= n ==> (EVERY P [m - 1 .. n] <=> P (m - 1) /\ EVERY P [m ..n])
1043Proof
1044 rw[listRangeINC_EVERY] >>
1045 `!x. m <= x + 1 <=> m - 1 = x \/ m <= x` by decide_tac >>
1046 (rw[EQ_IMP_THM] >> metis_tac[])
1047QED
1048
1049(* Theorem: m <= n ==> (EVERY P [m .. (n + 1)] <=> P (n + 1) /\ EVERY P [m .. n]) *)
1050(* Proof:
1051 EVERY P [m .. (n + 1)]
1052 <=> !x. m <= x /\ x <= n + 1 ==> P x by listRangeINC_EVERY
1053 <=> !x. m <= x /\ (x <= n \/ x = n + 1) ==> P x by arithmetic
1054 <=> !x. m <= x /\ x <= n ==> P x /\ P (n + 1) by LEFT_AND_OVER_OR, DISJ_IMP_THM
1055 <=> P (n + 1) /\ EVERY P [m .. n] by listRangeINC_EVERY
1056*)
1057Theorem listRangeINC_EVERY_split_last:
1058 !P m n. m <= n ==> (EVERY P [m .. (n + 1)] <=> P (n + 1) /\ EVERY P [m .. n])
1059Proof
1060 rw[listRangeINC_EVERY] >>
1061 `!x. x <= n + 1 <=> x <= n \/ x = n + 1` by decide_tac >>
1062 metis_tac[]
1063QED
1064
1065(* Theorem: m <= n ==> (EVERY P [m .. n] <=> P n /\ EVERY P [m ..< n]) *)
1066(* Proof:
1067 EVERY P [m .. n]
1068 <=> !x. m <= x /\ x <= n ==> P x by listRangeINC_EVERY
1069 <=> !x. m <= x /\ (x < n \/ x = n) ==> P x by arithmetic
1070 <=> !x. m <= x /\ x < n ==> P x /\ P n by LEFT_AND_OVER_OR, DISJ_IMP_THM
1071 <=> P n /\ EVERY P [m ..< n] by listRangeLHI_EVERY
1072*)
1073Theorem listRangeINC_EVERY_less_last:
1074 !P m n. m <= n ==> (EVERY P [m .. n] <=> P n /\ EVERY P [m ..< n])
1075Proof
1076 rw[listRangeINC_EVERY, listRangeLHI_EVERY] >>
1077 `!x. x <= n <=> x < n \/ x = n` by decide_tac >>
1078 metis_tac[]
1079QED
1080
1081(* Theorem: m < n /\ P m /\ ~P n ==>
1082 ?k. m <= k /\ k < n /\ EVERY P [m .. k] /\ ~P (SUC k) *)
1083(* Proof:
1084 m < n /\ P m /\ ~P n
1085 ==> ?k. m <= k /\ k < m /\
1086 (!j. m <= j /\ j <= k ==> P j) /\ ~P (SUC k) by every_range_span_max
1087 ==> ?k. m <= k /\ k < m /\
1088 EVERY P [m .. k] /\ ~P (SUC k) by listRangeINC_EVERY
1089*)
1090Theorem listRangeINC_EVERY_span_max:
1091 !P m n. m < n /\ P m /\ ~P n ==>
1092 ?k. m <= k /\ k < n /\ EVERY P [m .. k] /\ ~P (SUC k)
1093Proof
1094 simp[listRangeINC_EVERY, every_range_span_max]
1095QED
1096
1097(* Theorem: m < n /\ ~P m /\ P n ==>
1098 ?k. m < k /\ k <= n /\ EVERY P [k .. n] /\ ~P (PRE k) *)
1099(* Proof:
1100 m < n /\ P m /\ ~P n
1101 ==> ?k. m < k /\ k <= n /\
1102 (!j. k <= j /\ j <= n ==> P j) /\ ~P (PRE k) by every_range_span_min
1103 ==> ?k. m < k /\ k <= n /\
1104 EVERY P [k .. n] /\ ~P (PRE k) by listRangeINC_EVERY
1105*)
1106Theorem listRangeINC_EVERY_span_min:
1107 !P m n. m < n /\ ~P m /\ P n ==>
1108 ?k. m < k /\ k <= n /\ EVERY P [k .. n] /\ ~P (PRE k)
1109Proof
1110 simp[listRangeINC_EVERY, every_range_span_min]
1111QED
1112
1113(* temporarily make divides an infix *)
1114val _ = temp_set_fixity "divides" (Infixl 480);
1115
1116(* Theorem: 0 < n /\ m <= x /\ x divides n ==> MEM x [m .. n] *)
1117(* Proof:
1118 Note x divdes n ==> x <= n by DIVIDES_LE, 0 < n
1119 so MEM x [m .. n] by listRangeINC_MEM
1120*)
1121Theorem listRangeINC_has_divisors:
1122 !m n x. 0 < n /\ m <= x /\ x divides n ==> MEM x [m .. n]
1123Proof
1124 rw[listRangeINC_MEM, DIVIDES_LE]
1125QED
1126
1127(* Theorem: 0 < n /\ m <= x /\ x divides n ==> MEM x [m ..< n + 1] *)
1128(* Proof:
1129 Note the condition implies:
1130 MEM x [m .. n] by listRangeINC_has_divisors
1131 = MEM x [m ..< n + 1] by listRangeLHI_to_INC
1132*)
1133Theorem listRangeLHI_has_divisors:
1134 !m n x. 0 < n /\ m <= x /\ x divides n ==> MEM x [m ..< n + 1]
1135Proof
1136 metis_tac[listRangeINC_has_divisors, listRangeLHI_to_INC]
1137QED
1138
1139(* ------------------------------------------------------------------------- *)
1140(* isPREFIX-related theorems (by Chun Tian) *)
1141(* ------------------------------------------------------------------------- *)
1142
1143Theorem isPREFIX_listRangeLHI :
1144 !m n m' n'. m = m' /\ n <= n' ==> [m ..< n] <<= [m' ..< n']
1145Proof
1146 rw [listRangeLHI_def, isPREFIX_GENLIST]
1147QED
1148
1149Theorem isPREFIX_listRangeINC :
1150 !m n m' n'. m = m' /\ n <= n' ==> [m .. n] <<= [m' .. n']
1151Proof
1152 rw [listRangeINC_def, isPREFIX_GENLIST]
1153QED
1154
1155Theorem listRangeLHI_11 :
1156 !m n m' n'. m < n /\ m' < n' ==>
1157 ([m ..< n] = [m' ..< n'] <=> m = m' /\ n = n')
1158Proof
1159 rpt GEN_TAC >> STRIP_TAC
1160 >> reverse EQ_TAC >- rw []
1161 >> rw [LIST_EQ_REWRITE, listRangeLHI_EL]
1162 >- (rfs [listRangeLHI_EL] \\
1163 FIRST_X_ASSUM MATCH_MP_TAC \\
1164 Q.EXISTS_TAC ‘0’ >> rw [])
1165 >> rfs [listRangeLHI_EL]
1166 >> POP_ASSUM (MP_TAC o Q.SPEC ‘0’)
1167 >> rw []
1168QED
1169Theorem listRangeINC_11 :
1170 !m n m' n'. m <= n /\ m' <= n' ==>
1171 ([m .. n] = [m' .. n'] <=> m = m' /\ n = n')
1172Proof
1173 rw [listRangeINC_to_LHI]
1174 >> Know ‘[m ..< SUC n] = [m' ..< SUC n'] <=> m = m' /\ SUC n = SUC n'’
1175 >- (MATCH_MP_TAC listRangeLHI_11 >> rw [])
1176 >> Rewr'
1177 >> rw []
1178QED
1179
1180Theorem isPREFIX_listRangeLHI_EQ :
1181 !m n m' n'. m < n /\ m' < n' ==>
1182 ([m ..< n] <<= [m' ..< n'] <=> m = m' /\ n <= n')
1183Proof
1184 rpt GEN_TAC >> STRIP_TAC
1185 >> reverse EQ_TAC
1186 >- rw [listRangeLHI_def, isPREFIX_GENLIST]
1187 >> rw [listRangeLHI_CONS]
1188 >> Cases_on ‘m + 1 = n’ >- POP_ASSUM (fs o wrap o SYM)
1189 >> Cases_on ‘m + 1 = n'’
1190 >- (POP_ASSUM (fs o wrap o SYM) \\
1191 fs [listRangeLHI_NIL])
1192 >> CCONTR_TAC
1193 >> ‘n' <= n’ by rw []
1194 >> ‘[m + 1 ..< n'] <<= [m + 1 ..< n]’ by PROVE_TAC [isPREFIX_listRangeLHI]
1195 >> ‘[m + 1 ..< n] = [m + 1 ..< n']’ by PROVE_TAC [isPREFIX_ANTISYM]
1196 >> Know ‘[m + 1 ..< n] = [m + 1 ..< n'] <=> m + 1 = m + 1 /\ n = n'’
1197 >- (MATCH_MP_TAC listRangeLHI_11 >> simp [])
1198 >> rw []
1199QED
1200
1201Theorem isPREFIX_listRangeINC_EQ :
1202 !m n m' n'. m <= n /\ m' <= n' ==>
1203 ([m .. n] <<= [m' .. n'] <=> m = m' /\ n <= n')
1204Proof
1205 rw [listRangeINC_to_LHI]
1206 >> Know ‘[m ..< SUC n] <<= [m' ..< SUC n'] <=> m = m' /\ SUC n <= SUC n'’
1207 >- (MATCH_MP_TAC isPREFIX_listRangeLHI_EQ >> rw [])
1208 >> Rewr'
1209 >> rw []
1210QED
1211