iterateScript.sml
1(* ========================================================================= *)
2(* Generic iterated operations and special cases of sums over N *)
3(* *)
4(* (c) Copyright 2014-2015, *)
5(* Muhammad Qasim, *)
6(* Osman Hasan, *)
7(* Hardware Verification Group, *)
8(* Concordia University *)
9(* *)
10(* Contact: <m_qasi@ece.concordia.ca> *)
11(* *)
12(* Note: This theory was ported from HOL Light's iterate.ml *)
13(* *)
14(* (c) Copyright, John Harrison 1998-2007 *)
15(* (c) Copyright, Lars Schewe 2007 *)
16(* ========================================================================= *)
17
18Theory iterate[bare]
19Ancestors
20 prim_rec combin quotient arithmetic pair pred_set option
21 relation permutes
22Libs
23 HolKernel Parse boolLib BasicProvers numLib tautLib Arith
24 metisLib mesonLib pred_setLib simpLib pureSimps numSimps
25 hurdUtils TotalDefn computeLib TypeBase boolSimps unwindLib
26
27val qexists_tac = Q.EXISTS_TAC;
28val qabbrev_tac = Q.ABBREV_TAC;
29val qid_spec_tac = Q.ID_SPEC_TAC;
30val rename = Q.RENAME_TAC;
31val rename1 = Q.RENAME1_TAC;
32val rw = SRW_TAC [];
33fun simp ths = ASM_SIMP_TAC (srw_ss()) ths;
34fun fs ths = FULL_SIMP_TAC (srw_ss()) ths;
35fun rfs ths = REV_FULL_SIMP_TAC (srw_ss()) ths;
36
37val metis_tac = METIS_TAC;
38
39val _ = augment_srw_ss [ARITH_ss];
40
41val GEN_REWR_TAC = Lib.C Rewrite.GEN_REWRITE_TAC Rewrite.empty_rewrites;
42
43(* ------------------------------------------------------------------------- *)
44(* MESON, METIS, SET_TAC, SET_RULE, ASSERT_TAC, ASM_ARITH_TAC *)
45(* ------------------------------------------------------------------------- *)
46
47fun METIS ths tm = prove(tm,METIS_TAC ths);
48
49val DISC_RW_KILL = DISCH_TAC >> ONCE_ASM_REWRITE_TAC [] \\
50 POP_ASSUM K_TAC;
51
52fun ASSERT_TAC tm = SUBGOAL_THEN tm STRIP_ASSUME_TAC;
53
54val ASM_ARITH_TAC = rpt (POP_ASSUM MP_TAC) >> ARITH_TAC;
55
56Theorem CONJ_EQ_IMP[local] :
57 !p q r. p /\ q ==> r <=> p ==> q ==> r
58Proof
59 REWRITE_TAC [AND_IMP_INTRO]
60QED
61
62(* Minimal hol-light compatibility layer *)
63val FINITE_SUBSET = SUBSET_FINITE_I; (* pred_setTheory *)
64
65Theorem LEFT_IMP_EXISTS_THM[local] :
66 !P Q. (?x. P x) ==> Q <=> (!x. P x ==> Q)
67Proof
68 SIMP_TAC std_ss [PULL_EXISTS]
69QED
70
71Theorem FORALL_IN_GSPEC[local] :
72 (!P f. (!z. z IN {f x | P x} ==> Q z) <=> (!x. P x ==> Q(f x))) /\
73 (!P f. (!z. z IN {f x y | P x y} ==> Q z) <=>
74 (!x y. P x y ==> Q(f x y))) /\
75 (!P f. (!z. z IN {f w x y | P w x y} ==> Q z) <=>
76 (!w x y. P w x y ==> Q(f w x y)))
77Proof
78 SRW_TAC [][] THEN SET_TAC []
79QED
80
81Theorem CONJ_ACI[local] :
82 !p q. (p /\ q <=> q /\ p) /\
83 ((p /\ q) /\ r <=> p /\ (q /\ r)) /\
84 (p /\ (q /\ r) <=> q /\ (p /\ r)) /\
85 (p /\ p <=> p) /\
86 (p /\ (p /\ q) <=> p /\ q)
87Proof
88 METIS_TAC [CONJ_ASSOC, CONJ_SYM]
89QED
90
91(* ------------------------------------------------------------------------- *)
92(* misc. *)
93(* ------------------------------------------------------------------------- *)
94
95Theorem FINITE_SUBSET_IMAGE:
96 !f:'a->'b s t.
97 FINITE(t) /\ t SUBSET (IMAGE f s) <=>
98 ?s'. FINITE s' /\ s' SUBSET s /\ (t = IMAGE f s')
99Proof
100 REPEAT GEN_TAC THEN EQ_TAC THENL
101 [ALL_TAC, ASM_MESON_TAC[IMAGE_FINITE, IMAGE_SUBSET]] THEN
102 STRIP_TAC THEN
103 EXISTS_TAC ``IMAGE (\y. @x. x IN s /\ ((f:'a->'b)(x) = y)) t`` THEN
104 ASM_SIMP_TAC std_ss [IMAGE_FINITE] THEN
105 SIMP_TAC std_ss [EXTENSION, SUBSET_DEF, FORALL_IN_IMAGE] THEN CONJ_TAC THENL
106 [METIS_TAC[SUBSET_DEF, IN_IMAGE], ALL_TAC] THEN
107 REWRITE_TAC[IN_IMAGE] THEN X_GEN_TAC ``y:'b`` THEN
108 SIMP_TAC std_ss [GSYM RIGHT_EXISTS_AND_THM] THEN
109 ONCE_REWRITE_TAC[CONJ_SYM] THEN
110 REWRITE_TAC[UNWIND_THM2, GSYM CONJ_ASSOC] THEN
111 METIS_TAC [SUBSET_DEF, IN_IMAGE]
112QED
113
114Theorem EXISTS_FINITE_SUBSET_IMAGE:
115 !P f s.
116 (?t. FINITE t /\ t SUBSET IMAGE f s /\ P t) <=>
117 (?t. FINITE t /\ t SUBSET s /\ P (IMAGE f t))
118Proof
119 REWRITE_TAC[FINITE_SUBSET_IMAGE, CONJ_ASSOC] THEN MESON_TAC[]
120QED
121
122Theorem FORALL_FINITE_SUBSET_IMAGE:
123 !P f s. (!t. FINITE t /\ t SUBSET IMAGE f s ==> P t) <=>
124 (!t. FINITE t /\ t SUBSET s ==> P(IMAGE f t))
125Proof
126 REPEAT GEN_TAC THEN
127 ONCE_REWRITE_TAC [METIS [] ``(FINITE t /\ t SUBSET IMAGE f s ==> P t) =
128 (\t. FINITE t /\ t SUBSET IMAGE f s ==> P t) t``] THEN
129 ONCE_REWRITE_TAC [METIS [] ``(FINITE t /\ t SUBSET s ==> P (IMAGE f t)) =
130 (\t. FINITE t /\ t SUBSET s ==> P (IMAGE f t)) t``] THEN
131 ONCE_REWRITE_TAC [MESON[] ``(!x. P x) <=> ~(?x. ~P x)``] THEN
132 SIMP_TAC std_ss [NOT_IMP, GSYM CONJ_ASSOC, EXISTS_FINITE_SUBSET_IMAGE]
133QED
134
135Theorem EMPTY_BIGUNION:
136 !s. (BIGUNION s = {}) <=> !t. t IN s ==> (t = {})
137Proof
138 SET_TAC[]
139QED
140
141Theorem UPPER_BOUND_FINITE_SET:
142 !f:('a->num) s. FINITE(s) ==> ?a. !x. x IN s ==> f(x) <= a
143Proof
144 rpt strip_tac >> qexists_tac ‘MAX_SET (IMAGE f s)’ >>
145 rpt strip_tac >> irule X_LE_MAX_SET >> simp[]
146QED
147
148Theorem BOUNDS_LINEAR:
149 !A B C. (!n:num. A * n <= B * n + C) <=> A <= B
150Proof
151 REPEAT GEN_TAC THEN EQ_TAC THENL
152 [CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_LESS_EQUAL] THEN
153 DISCH_THEN(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LT_EXISTS]) THEN
154 REWRITE_TAC[RIGHT_ADD_DISTRIB, LE_ADD_LCANCEL] THEN
155 DISCH_THEN(MP_TAC o SPEC ``SUC C``) THEN
156 REWRITE_TAC[NOT_LESS_EQUAL, MULT_CLAUSES, ADD_CLAUSES, LT_SUC_LE] THEN
157 ARITH_TAC,
158 DISCH_THEN(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
159 ARITH_TAC]
160QED
161
162Theorem BOUNDS_LINEAR_0:
163 !A B. (!n:num. A * n <= B) <=> (A = 0)
164Proof
165 REPEAT GEN_TAC THEN
166 MP_TAC (SPECL [``A:num``, ``0:num``, ``B:num``] BOUNDS_LINEAR) THEN
167 REWRITE_TAC[MULT_CLAUSES, ADD_CLAUSES, LE]
168QED
169
170Theorem FINITE_POWERSET:
171 !s. FINITE s ==> FINITE {t | t SUBSET s}
172Proof
173 METIS_TAC [FINITE_POW, POW_DEF]
174QED
175
176Theorem LE_ADD:
177 !m n:num. m <= m + n
178Proof
179 GEN_TAC THEN INDUCT_TAC THEN
180 ASM_SIMP_TAC arith_ss [LE, ADD_CLAUSES, LESS_EQ_REFL]
181QED
182
183Theorem LE_ADDR:
184 !m n:num. n <= m + n
185Proof
186 ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_ACCEPT_TAC LE_ADD
187QED
188
189Theorem ADD_SUB2:
190 !m n:num. (m + n) - m = n
191Proof
192 ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_ACCEPT_TAC ADD_SUB
193QED
194
195Theorem ADD_SUBR2:
196 !m n:num. m - (m + n) = 0
197Proof
198 REWRITE_TAC[SUB_EQ_0, LESS_EQ_ADD]
199QED
200
201Theorem ADD_SUBR:
202 !m n:num. n - (m + n) = 0
203Proof
204 ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_ACCEPT_TAC ADD_SUBR2
205QED
206
207Theorem TRANSITIVE_STEPWISE_LE_EQ:
208 !R. (!x. R x x) /\ (!x y z. R x y /\ R y z ==> R x z)
209 ==> ((!m n. m <= n ==> R m n) <=> (!n. R n (SUC n)))
210Proof
211 REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC std_ss [LE, LESS_EQ_REFL] THEN
212 DISCH_TAC THEN SIMP_TAC std_ss [LE_EXISTS, LEFT_IMP_EXISTS_THM] THEN
213 GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN ASM_MESON_TAC[]
214QED
215
216Theorem TRANSITIVE_STEPWISE_LE:
217 !R. (!x. R x x) /\ (!x y z. R x y /\ R y z ==> R x z) /\
218 (!n. R n (SUC n))
219 ==> !m n. m <= n ==> R m n
220Proof
221 REPEAT GEN_TAC THEN MATCH_MP_TAC(TAUT
222 `(a /\ a' ==> (c <=> b)) ==> a /\ a' /\ b ==> c`) THEN
223 MATCH_ACCEPT_TAC TRANSITIVE_STEPWISE_LE_EQ
224QED
225
226Theorem TRANSITIVE_STEPWISE_LT_EQ :
227 !R. (!x y z. R x y /\ R y z ==> R x z)
228 ==> ((!m n. m < n ==> R m n) <=> (!n. R n (SUC n)))
229Proof
230 REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC std_ss [LESS_THM] THEN
231 DISCH_TAC THEN SIMP_TAC std_ss [LT_EXISTS] THEN
232 KNOW_TAC ``(!m n. (?d. n = m + SUC d) ==> R m n) =
233 (!m d n. (n = m + SUC d) ==> R m (m + SUC d))`` THENL
234 [METIS_TAC [LEFT_EXISTS_IMP_THM, SWAP_FORALL_THM], ALL_TAC] THEN
235 DISC_RW_KILL THEN GEN_TAC THEN
236 SIMP_TAC std_ss [LEFT_FORALL_IMP_THM, EXISTS_REFL, ADD_CLAUSES] THEN
237 INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN ASM_MESON_TAC[]
238QED
239
240Theorem TRANSITIVE_STEPWISE_LT :
241 !R. (!x y z. R x y /\ R y z ==> R x z) /\ (!n. R n (SUC n))
242 ==> !m n. m < n ==> R m n
243Proof
244 REPEAT GEN_TAC THEN MATCH_MP_TAC(TAUT
245 `(a ==> (c <=> b)) ==> a /\ b ==> c`) THEN
246 MATCH_ACCEPT_TAC TRANSITIVE_STEPWISE_LT_EQ
247QED
248
249Theorem LAMBDA_PAIR:
250 (\(x,y). P x y) = (\p. P (FST p) (SND p))
251Proof
252 SIMP_TAC std_ss [FUN_EQ_THM, FORALL_PROD] THEN
253 SIMP_TAC std_ss []
254QED
255
256Theorem NOT_EQ:
257 !a b. (a <> b) = ~(a = b)
258Proof METIS_TAC []
259QED
260
261Theorem POWERSET_CLAUSES:
262 ({s | s SUBSET {}} = {{}}) /\
263 ((!a:'a t. {s | s SUBSET (a INSERT t)} =
264 {s | s SUBSET t} UNION IMAGE (\s. a INSERT s) {s | s SUBSET t}))
265Proof
266 REWRITE_TAC[SUBSET_INSERT_DELETE, SUBSET_EMPTY, SET_RULE
267 ``(!a. {x | x = a} = {a}) /\ (!a. {x | a = x} = {a})``] THEN
268 MAP_EVERY X_GEN_TAC [``a:'a``, ``t:'a->bool``] THEN
269 MATCH_MP_TAC SUBSET_ANTISYM THEN REWRITE_TAC[UNION_SUBSET] THEN
270 ONCE_REWRITE_TAC[SUBSET_DEF] THEN
271 SIMP_TAC std_ss [FORALL_IN_IMAGE, FORALL_IN_GSPEC] THEN
272 SIMP_TAC std_ss [GSPECIFICATION, IN_UNION, IN_IMAGE] THEN
273 CONJ_TAC THENL [ALL_TAC, SET_TAC[]] THEN
274 X_GEN_TAC ``s:'a->bool`` THEN
275 ASM_CASES_TAC ``(a:'a) IN s`` THENL [ALL_TAC, ASM_SET_TAC[]] THEN
276 STRIP_TAC THEN DISJ2_TAC THEN EXISTS_TAC ``s DELETE (a:'a)`` THEN
277 ASM_SET_TAC[]
278QED
279
280Theorem SIMPLE_IMAGE_GEN:
281 !f P. {f x | P x} = IMAGE f {x | P x}
282Proof
283 SET_TAC[]
284QED
285
286Theorem FUN_IN_IMAGE:
287 !f s x. x IN s ==> f(x) IN IMAGE f s
288Proof
289 SET_TAC[]
290QED
291
292Theorem DIFF_BIGINTER2 : (* was: DIFF_BIGINTER *)
293 !u s. u DIFF BIGINTER s = BIGUNION {u DIFF t | t IN s}
294Proof
295 SIMP_TAC std_ss [BIGUNION_GSPEC] THEN SET_TAC[]
296QED
297
298Theorem BIGINTER_BIGUNION:
299 !s. BIGINTER s = UNIV DIFF (BIGUNION {UNIV DIFF t | t IN s})
300Proof
301 REWRITE_TAC[GSYM DIFF_BIGINTER2] THEN SET_TAC[]
302QED
303
304Theorem BIGUNION_BIGINTER:
305 !s. BIGUNION s = UNIV DIFF (BIGINTER {UNIV DIFF t | t IN s})
306Proof
307 GEN_TAC THEN GEN_REWR_TAC I [EXTENSION] THEN
308 SIMP_TAC std_ss [IN_BIGUNION, IN_UNIV, IN_DIFF, BIGINTER_GSPEC,
309 GSPECIFICATION] THEN
310 MESON_TAC[]
311QED
312
313(* ------------------------------------------------------------------------- *)
314(* Recursion over finite sets; based on Ching-Tsun's code (archive 713). *)
315(* ------------------------------------------------------------------------- *)
316
317Definition FINREC:
318 (FINREC (f:'a->'b->'b) b s a 0 <=> (s = {}) /\ (a = b)) /\
319 (FINREC (f:'a->'b->'b) b s a (SUC n) <=>
320 ?x c. x IN s /\
321 FINREC f b (s DELETE x) c n /\
322 (a = f x c))
323End
324
325Theorem FINREC_1_LEMMA:
326 !f b s a. FINREC f b s a (SUC 0) <=> ?x. (s = {x}) /\ (a = f x b)
327Proof
328 REWRITE_TAC[FINREC] THEN REPEAT GEN_TAC THEN AP_TERM_TAC THEN ABS_TAC THEN
329 SIMP_TAC std_ss [GSPECIFICATION] THEN EQ_TAC THENL [METIS_TAC [DELETE_EQ_SING],
330 STRIP_TAC THEN ASM_REWRITE_TAC [IN_SING, SING_DELETE]]
331QED
332
333Theorem FINREC_SUC_LEMMA:
334 !(f:'a->'b->'b) b.
335 (!x y s. ~(x = y) ==> (f x (f y s) = f y (f x s)))
336 ==> !n s z.
337 FINREC f b s z (SUC n)
338 ==> !x. x IN s ==> ?w. FINREC f b (s DELETE x) w n /\
339 (z = f x w)
340Proof
341 REPEAT GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THENL
342 [REWRITE_TAC[FINREC_1_LEMMA] THEN REWRITE_TAC[FINREC] THEN
343 REPEAT GEN_TAC THEN STRIP_TAC THEN STRIP_TAC THEN
344 ASM_REWRITE_TAC[IN_INSERT, NOT_IN_EMPTY] THEN
345 DISCH_THEN SUBST1_TAC THEN EXISTS_TAC ``b:'b`` THEN
346 ASM_REWRITE_TAC[SING_DELETE], REPEAT GEN_TAC THEN
347 GEN_REWR_TAC LAND_CONV [FINREC] THEN
348 DISCH_THEN(X_CHOOSE_THEN ``y:'a`` MP_TAC) THEN
349 DISCH_THEN(X_CHOOSE_THEN ``c:'b`` STRIP_ASSUME_TAC) THEN
350 X_GEN_TAC ``x:'a`` THEN DISCH_TAC THEN
351 ASM_CASES_TAC ``x:'a = y`` THEN ASM_REWRITE_TAC[] THENL
352 [EXISTS_TAC ``c:'b`` THEN ASM_REWRITE_TAC[],
353 UNDISCH_TAC ``FINREC (f:'a->'b->'b) b (s DELETE y) c (SUC n)`` THEN
354 DISCH_THEN(ANTE_RES_THEN (MP_TAC o SPEC ``x:'a``)) THEN
355 ONCE_ASM_REWRITE_TAC[IN_DELETE] THEN ONCE_ASM_REWRITE_TAC[IN_DELETE] THEN
356 ONCE_ASM_REWRITE_TAC[IN_DELETE] THEN ONCE_ASM_REWRITE_TAC[IN_DELETE] THEN
357 ONCE_ASM_REWRITE_TAC[IN_DELETE] THEN
358 DISCH_THEN(X_CHOOSE_THEN ``v:'b`` STRIP_ASSUME_TAC) THEN
359 EXISTS_TAC ``(f:'a->'b->'b) y v`` THEN ONCE_ASM_REWRITE_TAC[FINREC] THEN
360 CONJ_TAC THENL [MAP_EVERY EXISTS_TAC [``y:'a``, ``v:'b``] THEN
361 ONCE_REWRITE_TAC[DELETE_COMM] THEN ONCE_ASM_REWRITE_TAC[IN_DELETE] THEN
362 ONCE_ASM_REWRITE_TAC[IN_DELETE] THEN ONCE_ASM_REWRITE_TAC[IN_DELETE] THEN
363 METIS_TAC [], METIS_TAC []]]]
364QED
365
366Theorem FINREC_UNIQUE_LEMMA:
367 !(f:'a->'b->'b) b.
368 (!x y s. ~(x = y) ==> (f x (f y s) = f y (f x s)))
369 ==> !n1 n2 s a1 a2.
370 FINREC f b s a1 n1 /\ FINREC f b s a2 n2
371 ==> (a1 = a2) /\ (n1 = n2)
372Proof
373 REPEAT GEN_TAC THEN DISCH_TAC THEN
374 INDUCT_TAC THEN INDUCT_TAC THENL
375 [REWRITE_TAC[FINREC] THEN MESON_TAC[NOT_IN_EMPTY],
376 REWRITE_TAC[FINREC] THEN MESON_TAC[NOT_IN_EMPTY],
377 REWRITE_TAC[FINREC] THEN MESON_TAC[NOT_IN_EMPTY],
378 IMP_RES_THEN ASSUME_TAC FINREC_SUC_LEMMA THEN REPEAT GEN_TAC THEN
379 DISCH_THEN(fn th => MP_TAC(CONJUNCT1 th) THEN MP_TAC th) THEN
380 DISCH_THEN(CONJUNCTS_THEN (ANTE_RES_THEN ASSUME_TAC)) THEN
381 REWRITE_TAC[FINREC] THEN STRIP_TAC THEN ASM_MESON_TAC[]]
382QED
383
384Theorem FINREC_EXISTS_LEMMA:
385 !(f:'a->'b->'b) b s. FINITE s ==> ?a n. FINREC f b s a n
386Proof
387 REPEAT GEN_TAC THEN
388 KNOW_TAC ``(?a:'b n. FINREC f b s a n) = (\s. ?a:'b n. FINREC f b s a n) s`` THENL
389 [FULL_SIMP_TAC std_ss [], DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
390 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN REPEAT STRIP_TAC THENL
391 [MAP_EVERY EXISTS_TAC [``b:'b``, ``0:num``] THEN REWRITE_TAC[FINREC],
392 MAP_EVERY EXISTS_TAC [``(f:'a->'b->'b) e a``, ``SUC n``] THEN
393 REWRITE_TAC[FINREC] THEN MAP_EVERY EXISTS_TAC [``e:'a``, ``a:'b``] THEN
394 FULL_SIMP_TAC std_ss [IN_INSERT] THEN
395 EVAL_TAC THEN FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT]]]
396QED
397
398Theorem FINREC_FUN_LEMMA:
399 !P (R:'a->'b->'c->bool).
400 (!s. P s ==> ?a n. R s a n) /\
401 (!n1 n2 s a1 a2.
402 R s a1 n1 /\ R s a2 n2 ==> (a1 = a2) /\ (n1 = n2)) ==>
403 ?f. !s a. P s ==> ((?n. R s a n) <=> (f s = a))
404Proof
405 REPEAT STRIP_TAC THEN EXISTS_TAC ``\s:'a. @a:'b. ?n:'c. R s a n`` THEN
406 REPEAT STRIP_TAC THEN BETA_TAC THEN EQ_TAC THENL [STRIP_TAC THEN
407 MATCH_MP_TAC SELECT_UNIQUE THEN ASM_MESON_TAC[],
408 DISCH_THEN(SUBST1_TAC o SYM) THEN CONV_TAC SELECT_CONV THEN ASM_MESON_TAC[]]
409QED
410
411Theorem FINREC_FUN :
412 !(f:'a->'b->'b) b.
413 (!x y s. ~(x = y) ==> (f x (f y s) = f y (f x s)))
414 ==> ?g. (g {} = b) /\
415 !s x. FINITE s /\ x IN s
416 ==> (g s = f x (g (s DELETE x)))
417Proof
418 REPEAT STRIP_TAC THEN IMP_RES_THEN MP_TAC FINREC_UNIQUE_LEMMA THEN
419 REPEAT STRIP_TAC THEN
420 KNOW_TAC ``!n1 n2 s a1 a2. FINREC f b s a1 n1 /\
421 FINREC f b s a2 n2 ==> (a1 = a2) /\ (n1 = n2)``
422 THEN1 METIS_TAC [] THEN
423 DISCH_THEN (MP_TAC o CONJ (SPECL [``f:'a->'b->'b``, ``b:'b``] FINREC_EXISTS_LEMMA)) THEN
424 DISCH_THEN(MP_TAC o MATCH_MP FINREC_FUN_LEMMA) THEN
425 DISCH_THEN(X_CHOOSE_TAC ``g:('a->bool)->'b``) THEN
426 EXISTS_TAC ``g:('a->bool)->'b`` THEN CONJ_TAC THENL
427 [ SUBGOAL_THEN ``FINITE(EMPTY:'a->bool)``
428 (ANTE_RES_THEN (fn th => GEN_REWR_TAC I [GSYM th])) THENL
429 [REWRITE_TAC[FINITE_EMPTY],
430 EXISTS_TAC ``0:num`` THEN REWRITE_TAC[FINREC]],
431 REPEAT STRIP_TAC THEN
432 ANTE_RES_THEN MP_TAC (ASSUME ``FINITE(s:'a->bool)``) THEN
433 DISCH_THEN(ASSUME_TAC o GSYM) THEN ASM_REWRITE_TAC[] THEN
434 FIRST_ASSUM(MP_TAC o SPEC ``(g:('a->bool)->'b) s``) THEN
435 REWRITE_TAC[] THEN REWRITE_TAC[GSYM LEFT_FORALL_IMP_THM] THEN
436 INDUCT_TAC THENL
437 [ ASM_REWRITE_TAC[FINREC] THEN DISCH_TAC THEN UNDISCH_TAC ``x:'a IN s`` THEN
438 ASM_REWRITE_TAC[NOT_IN_EMPTY],
439 IMP_RES_THEN ASSUME_TAC FINREC_SUC_LEMMA THEN
440 DISCH_THEN(ANTE_RES_THEN (MP_TAC o SPEC ``x:'a``)) THEN
441 ASM_REWRITE_TAC[] THEN
442 DISCH_THEN(X_CHOOSE_THEN ``w:'b`` (CONJUNCTS_THEN ASSUME_TAC)) THEN
443 SUBGOAL_THEN ``(g (s DELETE x:'a) = w:'b)`` SUBST1_TAC THENL
444 [ SUBGOAL_THEN ``FINITE(s DELETE x:'a)`` MP_TAC THENL
445 [ FULL_SIMP_TAC std_ss [FINITE_DELETE],
446 DISCH_THEN(ANTE_RES_THEN (MP_TAC o GSYM)) THEN
447 DISCH_THEN(fn th => REWRITE_TAC[th]) THEN
448 METIS_TAC [] ],
449 ASM_REWRITE_TAC [] ] ] ]
450QED
451
452Theorem SET_RECURSION_LEMMA:
453 !(f:'a->'b->'b) b.
454 (!x y s. ~(x = y) ==> (f x (f y s) = f y (f x s)))
455 ==> ?g. (g {} = b) /\
456 !x s. FINITE s
457 ==> (g (x INSERT s) =
458 if x IN s then g s else f x (g s))
459Proof
460 REPEAT GEN_TAC THEN
461 DISCH_THEN(MP_TAC o SPEC ``b:'b`` o MATCH_MP FINREC_FUN) THEN
462 DISCH_THEN(X_CHOOSE_THEN ``g:('a->bool)->'b`` STRIP_ASSUME_TAC) THEN
463 EXISTS_TAC ``g:('a->bool)->'b`` THEN ASM_REWRITE_TAC[] THEN
464 REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
465 DISCH_TAC THENL
466 [AP_TERM_TAC THEN REWRITE_TAC[GSYM ABSORPTION] THEN ASM_REWRITE_TAC[],
467 SUBGOAL_THEN ``FINITE(x:'a INSERT s) /\ x IN (x INSERT s)`` MP_TAC THENL
468 [REWRITE_TAC[IN_INSERT] THEN ASM_MESON_TAC[FINITE_INSERT],
469 DISCH_THEN(ANTE_RES_THEN SUBST1_TAC) THEN
470 REPEAT AP_TERM_TAC THEN UNDISCH_TAC ``~(x:'a IN s)`` THEN DISCH_TAC THEN
471 EVAL_TAC THEN FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT, SUBSET_REFL]]]
472QED
473
474(* This is HOL Light's definition of ‘ITSET’ *)
475Theorem ITSET_alt :
476 !(f:'a->'b->'b) s b.
477 (!x y z. f x (f y z) = f y (f x z)) /\ FINITE s ==>
478 ITSET f s b =
479 (@g. (g {} = b) /\
480 !x s. FINITE s ==>
481 (g (x INSERT s) = if x IN s then g s else f x (g s))) s
482Proof
483 RW_TAC std_ss []
484 >> SELECT_ELIM_TAC
485 >> CONJ_TAC
486 >- (MATCH_MP_TAC SET_RECURSION_LEMMA >> rw [])
487 >> rpt STRIP_TAC
488 >> Q.PAT_X_ASSUM ‘FINITE s’ MP_TAC
489 >> Q.SPEC_TAC (‘s’, ‘s’)
490 >> HO_MATCH_MP_TAC FINITE_INDUCT
491 >> CONJ_TAC >- rw [ITSET_THM, FINITE_EMPTY]
492 >> rpt STRIP_TAC
493 >> Q.PAT_X_ASSUM ‘!x s. FINITE s ==> P’
494 (fn th => ONCE_REWRITE_TAC [MATCH_MP th (ASSUME “FINITE s”)])
495 >> simp []
496 >> Know ‘ITSET f (e INSERT s) b = f e (ITSET f (s DELETE e) b)’
497 >- (MATCH_MP_TAC COMMUTING_ITSET_RECURSES >> rw [])
498 >> Rewr'
499 >> Suff ‘s DELETE e = s’ >- rw []
500 >> rw [GSYM DELETE_NON_ELEMENT]
501QED
502
503Theorem FINITE_RECURSION :
504 !(f:'a->'b->'b) b.
505 (!x y s. ~(x = y) ==> (f x (f y s) = f y (f x s)))
506 ==> (ITSET f {} b = b) /\
507 !x s. FINITE s
508 ==> (ITSET f (x INSERT s) b =
509 if x IN s then ITSET f s b
510 else f x (ITSET f s b))
511Proof
512 RW_TAC std_ss [ITSET_EMPTY]
513 >> Cases_on `x IN s`
514 >- (`x INSERT s = s` by PROVE_TAC [ABSORPTION] >> art [])
515 >> ASM_SIMP_TAC std_ss []
516 >> Know `ITSET f s b = ITSET f (s DELETE x) b`
517 >- (`s DELETE x = s` by PROVE_TAC [DELETE_NON_ELEMENT] >> art [])
518 >> Rewr'
519 >> MATCH_MP_TAC COMMUTING_ITSET_RECURSES
520 >> rename1 `i IN s` >> RW_TAC std_ss []
521 >> Cases_on `x = y` >- art []
522 >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
523QED
524
525Theorem CARD_UNION_EQ:
526 !s t u.
527 FINITE u /\ (s INTER t = {}) /\ (s UNION t = u)
528 ==> (CARD s + CARD t = CARD u)
529Proof
530 REPEAT STRIP_TAC THEN KNOW_TAC ``FINITE (s:'a->bool) /\ FINITE (t:'a->bool)``
531 THENL [METIS_TAC [FINITE_UNION], ALL_TAC] THEN STRIP_TAC THEN
532 ASSUME_TAC CARD_UNION THEN
533 POP_ASSUM (MP_TAC o Q.SPEC `s`) THEN FULL_SIMP_TAC std_ss [] THEN
534 DISCH_TAC THEN POP_ASSUM (MP_TAC o Q.SPEC `t`) THEN
535 FULL_SIMP_TAC std_ss [CARD_EMPTY]
536QED
537
538Theorem SUBSET_RESTRICT:
539 !s P. {x | x IN s /\ P x} SUBSET s
540Proof
541 SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION]
542QED
543
544Theorem FINITE_RESTRICT:
545 !s:'a->bool P. FINITE s ==> FINITE {x | x IN s /\ P x}
546Proof
547METIS_TAC[SUBSET_RESTRICT, SUBSET_FINITE]
548QED
549
550(* ------------------------------------------------------------------------- *)
551(* Choosing a smaller subset of a given size. *)
552(* ------------------------------------------------------------------------- *)
553
554Theorem SET_PROVE_CASES:
555 !P:('a->bool)->bool.
556 P {} /\ (!a s. ~(a IN s) ==> P(a INSERT s))
557 ==> !s. P s
558Proof
559 MESON_TAC[SET_CASES]
560QED
561
562Theorem CHOOSE_SUBSET_STRONG:
563 !n s:'a->bool.
564 (FINITE s ==> n <= CARD s) ==> ?t. t SUBSET s /\ t HAS_SIZE n
565Proof
566 INDUCT_TAC THEN REWRITE_TAC[HAS_SIZE_0, HAS_SIZE_SUC] THENL
567 [MESON_TAC[EMPTY_SUBSET], ALL_TAC] THEN
568 ONCE_REWRITE_TAC [METIS [] ``((FINITE s ==> SUC n <= CARD s) ==>
569 ?t. t SUBSET s /\ t <> {} /\ !a. a IN t ==> t DELETE a HAS_SIZE n) =
570 (\s. (FINITE s ==> SUC n <= CARD s) ==>
571 ?t. t SUBSET s /\ t <> {} /\ !a. a IN t ==> t DELETE a HAS_SIZE n) s``] THEN
572 MATCH_MP_TAC SET_PROVE_CASES THEN BETA_TAC THEN
573 REWRITE_TAC[FINITE_EMPTY, CARD_EMPTY, CARD_INSERT, ARITH_PROVE ``~(SUC n <= 0)``] THEN
574 MAP_EVERY X_GEN_TAC [``a:'a``, ``s:'a->bool``] THEN DISCH_TAC THEN
575 ASM_SIMP_TAC std_ss [CARD_EMPTY, CARD_INSERT, FINITE_INSERT,
576 DECIDE “x <= SUC y <=> x <= y \/ x = SUC y”] THEN
577 DISCH_TAC THEN
578 FIRST_X_ASSUM(MP_TAC o SPEC ``s:'a->bool``) THEN ASM_REWRITE_TAC[] THEN
579 DISCH_THEN(X_CHOOSE_THEN ``t:'a->bool`` STRIP_ASSUME_TAC) THEN
580 EXISTS_TAC ``(a:'a) INSERT t`` THEN
581 REPEAT(CONJ_TAC THENL [ASM_SET_TAC[], ALL_TAC]) THEN
582 RULE_ASSUM_TAC(REWRITE_RULE[HAS_SIZE]) THEN
583 ASM_SIMP_TAC std_ss [HAS_SIZE, CARD_DELETE, FINITE_INSERT, FINITE_DELETE,
584 CARD_EMPTY, CARD_INSERT] THEN
585 GEN_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[SUC_SUB1] THEN
586 ASM_SET_TAC[]
587QED
588
589Theorem CHOOSE_SUBSET:
590 !s:'a->bool. FINITE s ==> !n. n <= CARD s ==> ?t. t SUBSET s /\ t HAS_SIZE n
591Proof
592 MESON_TAC[CHOOSE_SUBSET_STRONG]
593QED
594
595Theorem HAS_SIZE_NUMSEG_LT:
596 !n. {m | m < n} HAS_SIZE n
597Proof
598 INDUCT_TAC THENL
599 [SUBGOAL_THEN ``{m:num | m < 0} = {}``
600 (fn th => REWRITE_TAC[HAS_SIZE_0, th]) THEN
601 SIMP_TAC std_ss [EXTENSION, NOT_IN_EMPTY, GSPECIFICATION, LESS_THM, NOT_LESS_0],
602 SUBGOAL_THEN ``{m | m < SUC n} = n INSERT {m | m < n}`` SUBST1_TAC THENL
603 [SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INSERT] THEN ARITH_TAC,
604 ALL_TAC] THEN
605 RULE_ASSUM_TAC(REWRITE_RULE[HAS_SIZE]) THEN
606 ASM_SIMP_TAC std_ss [HAS_SIZE, CARD_EMPTY, CARD_INSERT, FINITE_INSERT] THEN
607 SIMP_TAC std_ss [GSPECIFICATION, LESS_REFL]]
608QED
609
610Theorem FINITE_NUMSEG_LT:
611 !n:num. FINITE {m | m < n}
612Proof
613 REWRITE_TAC[REWRITE_RULE[HAS_SIZE] HAS_SIZE_NUMSEG_LT]
614QED
615
616Theorem HAS_SIZE_NUMSEG_LE:
617 !n. {m | m <= n} HAS_SIZE (n + 1)
618Proof
619 REWRITE_TAC[GSYM LT_SUC_LE, HAS_SIZE_NUMSEG_LT, ADD1]
620QED
621
622Theorem FINITE_NUMSEG_LE:
623 !n:num. FINITE {m | m <= n}
624Proof
625 SIMP_TAC std_ss [REWRITE_RULE[HAS_SIZE] HAS_SIZE_NUMSEG_LE]
626QED
627
628(* ------------------------------------------------------------------------- *)
629(* A natural notation for segments of the naturals. *)
630(* ------------------------------------------------------------------------- *)
631
632Definition numseg:
633 numseg m n = {x:num | m <= x /\ x <= n}
634End
635
636(* syntax is similar to the version also available for lists, where
637 listRangeTheory has [ m .. n ]
638 *)
639val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
640 fixity = Closefix,
641 paren_style = OnlyIfNecessary,
642 pp_elements = [TOK "{", TM, HardSpace 1, TOK "..",
643 BreakSpace(1,1), TM, BreakSpace(0,0),
644 TOK "}"],
645 term_name = "numseg" }
646
647Theorem IN_NUMSEG[simp]:
648 x IN {m .. n} <=> m <= x /\ x <= n
649Proof
650 simp[numseg]
651QED
652
653(* ‘count n’ re-expressed by numseg *)
654Theorem COUNT_NUMSEG :
655 !n. 0 < n ==> count n = {0..n-1}
656Proof
657 rw [Once EXTENSION]
658QED
659
660Theorem FINITE_NUMSEG:
661 !m n. FINITE {m..n}
662Proof
663 rw[numseg] >> irule FINITE_SUBSET >> irule_at Any FINITE_COUNT >>
664 qexists_tac ‘n + 1’ >> simp[SUBSET_DEF]
665QED
666
667Theorem NUMSEG_COMBINE_R:
668 !m p n. m <= p + 1 /\ p <= n ==> {m..p} UNION {p+1..n} = {m..n}
669Proof
670 simp[EXTENSION]
671QED
672
673Theorem NUMSEG_COMBINE_L:
674 !m p n. m <= p /\ p <= n + 1 ==> {m..p-1} UNION {p..n} = {m..n}
675Proof
676 simp[EXTENSION]
677QED
678
679Theorem NUMSEG_LREC:
680 !m n. m <= n ==> m INSERT {m+1..n} = {m..n}
681Proof
682 simp[EXTENSION]
683QED
684
685Theorem NUMSEG_RREC:
686 !m n. m <= n ==> n INSERT {m..n-1} = {m..n}
687Proof
688 simp[EXTENSION]
689QED
690
691Theorem NUMSEG_REC:
692 !m n. m <= SUC n ==> {m..SUC n} = SUC n INSERT {m..n}
693Proof SIMP_TAC std_ss [GSYM NUMSEG_RREC, SUC_SUB1]
694QED
695
696Theorem IN_NUMSEG_0:
697 !m n. m IN {0..n} <=> m <= n
698Proof simp[]
699QED
700
701Theorem NUMSEG_SING: !n. {n..n} = {n}
702Proof simp[EXTENSION]
703QED
704
705Theorem NUMSEG_EMPTY:
706 !m n. {m..n} = {} <=> n < m
707Proof
708 simp[EXTENSION] >> MESON_TAC[NOT_LESS_EQUAL, LESS_EQ_TRANS, LESS_EQ_REFL]
709QED
710
711Theorem CARD_NUMSEG_LEMMA:
712 !m d. CARD{m..m+d} = d + 1
713Proof
714 GEN_TAC THEN INDUCT_TAC THEN
715 fs[NUMSEG_SING, ADD_CLAUSES, NUMSEG_REC, FINITE_NUMSEG]
716QED
717
718Theorem CARD_NUMSEG:
719 !m n. CARD {m..n} = n + 1 - m
720Proof
721 REPEAT GEN_TAC >> Cases_on ‘m <= n’
722 >- (full_simp_tac bool_ss [LE_EXISTS, CARD_NUMSEG_LEMMA] >> simp[])
723 >> fs[NOT_LESS_EQUAL]
724 >> drule_then assume_tac (iffRL NUMSEG_EMPTY)
725 >> simp[]
726QED
727
728Theorem HAS_SIZE_NUMSEG:
729 !m n. {m..n} HAS_SIZE ((n + 1:num) - m)
730Proof
731 REWRITE_TAC[HAS_SIZE, FINITE_NUMSEG, CARD_NUMSEG]
732QED
733
734Theorem CARD_NUMSEG_1:
735 !n. CARD{1..n} = n
736Proof
737 simp[CARD_NUMSEG]
738QED
739
740Theorem HAS_SIZE_NUMSEG_1:
741 !n. {1..n} HAS_SIZE n
742Proof
743 REWRITE_TAC[CARD_NUMSEG, HAS_SIZE, FINITE_NUMSEG] THEN ARITH_TAC
744QED
745
746Theorem NUMSEG_CLAUSES:
747 (!m. {m..0} = if m = 0 then {0} else {}) /\
748 !m n. {m..SUC n} = if m <= SUC n then SUC n INSERT {m..n} else {m..n}
749Proof
750 rw[] >> simp[NUMSEG_EMPTY, NUMSEG_SING, NUMSEG_REC] >> simp[EXTENSION]
751QED
752
753Theorem FINITE_INDEX_NUMSEG:
754 !s:'a->bool.
755 FINITE s =
756 ?f. (!i j. i IN {1..CARD s} /\ j IN {1..CARD s} /\ f i = f j ==> i = j) /\
757 s = IMAGE f {1..CARD s}
758Proof
759 GEN_TAC >> reverse EQ_TAC >- MESON_TAC[FINITE_NUMSEG, IMAGE_FINITE] >>
760 qid_spec_tac ‘s’ >> Induct_on ‘FINITE’ >> rw[NUMSEG_EMPTY] >>
761 rename [‘e NOTIN s’, ‘s = IMAGE f _’] >> qabbrev_tac ‘C = CARD s’ >>
762 qexists_tac ‘f (| SUC C |-> e |)’ >> simp[combinTheory.APPLY_UPDATE_THM] >>
763 reverse conj_tac
764 >- (simp[EXTENSION, combinTheory.APPLY_UPDATE_THM, AllCaseEqs(), SF DNF_ss] >>
765 metis_tac[LE, DECIDE “x <= y ==> x <> SUC y”]) >>
766 rpt gen_tac >> simp[AllCaseEqs()] >>
767 ‘!i. 1 <= i /\ i <= C ==> f i <> e’ by (rfs[] >> rw[Abbr ‘C’] >> metis_tac[]) >>
768 simp[LE] >> rpt strip_tac >> metis_tac[]
769QED
770
771Theorem FINITE_INDEX_NUMBERS:
772 !s:'a->bool.
773 FINITE s =
774 ?k:num->bool f. (!i j. i IN k /\ j IN k /\ (f i = f j) ==> (i = j)) /\
775 FINITE k /\ (s = IMAGE f k)
776Proof
777 MESON_TAC[FINITE_INDEX_NUMSEG, FINITE_NUMSEG, IMAGE_FINITE]
778QED
779
780Theorem DISJOINT_NUMSEG:
781 !m n p q. DISJOINT {m..n} {p..q} <=> n < p \/ q < m \/ n < m \/ q < p
782Proof
783 simp[DISJOINT_DEF, EXTENSION, NOT_LESS_EQUAL] >> rpt gen_tac >> eq_tac >>
784 simp[] >> MESON_TAC[LESS_ANTISYM]
785QED
786
787Theorem NUMSEG_ADD_SPLIT:
788 !m n p. m <= n + 1 ==> {m..n+p} = {m..n} UNION {n+1..n+p}
789Proof
790 REWRITE_TAC[EXTENSION, IN_UNION, IN_NUMSEG] THEN ARITH_TAC
791QED
792
793Theorem NUMSEG_OFFSET_IMAGE:
794 !m n p. {m+p..n+p} = IMAGE (\i. i + p) {m..n}
795Proof
796 simp[EXTENSION, EQ_IMP_THM] >> rpt strip_tac >> rename [‘m + p <= x’] >>
797 qexists_tac ‘x - p’ >> simp[]
798QED
799
800Theorem SUBSET_NUMSEG:
801 !m n p q. {m..n} SUBSET {p..q} <=> n < m \/ p <= m /\ n <= q
802Proof
803 simp[SUBSET_DEF, EQ_IMP_THM] >>
804 MESON_TAC[LESS_EQ_TRANS, NOT_LESS_EQUAL, LESS_EQ_REFL]
805QED
806
807(* ------------------------------------------------------------------------- *)
808(* Equivalence with the more ad-hoc comprehension notation. *)
809(* ------------------------------------------------------------------------- *)
810
811Theorem NUMSEG_LE:
812 !n. {x | x <= n} = {0..n}
813Proof
814 simp[EXTENSION]
815QED
816
817Theorem NUMSEG_LT:
818 !n. {x | x < n} = if n = 0 then {} else {0..n-1}
819Proof
820 rw[EXTENSION]
821QED
822
823Theorem FROM_INTER_NUMSEG_GEN:
824 !k m n. (from k) INTER {m..n} = if m < k then {k..n} else {m..n}
825Proof
826 REPEAT GEN_TAC THEN COND_CASES_TAC THEN POP_ASSUM MP_TAC THEN
827 SIMP_TAC std_ss [from_def, GSPECIFICATION, IN_INTER, IN_NUMSEG, EXTENSION] THEN
828 ARITH_TAC
829QED
830
831Theorem FROM_INTER_NUMSEG_MAX:
832 !m n p. from p INTER {m..n} = {MAX p m..n}
833Proof
834 SIMP_TAC arith_ss [EXTENSION, IN_INTER, IN_NUMSEG, IN_FROM] THEN ARITH_TAC
835QED
836
837Theorem FROM_INTER_NUMSEG:
838 !k n. (from k) INTER {0..n} = {k..n}
839Proof
840 SIMP_TAC std_ss [from_def, GSPECIFICATION, IN_INTER, IN_NUMSEG, EXTENSION] THEN
841 ARITH_TAC
842QED
843
844Theorem INFINITE_FROM:
845 !n. INFINITE(from n)
846Proof
847 GEN_TAC THEN KNOW_TAC ``from n = univ(:num) DIFF {i | i < n}`` THENL
848 [SIMP_TAC std_ss [EXTENSION, from_def, IN_DIFF, IN_UNIV, GSPECIFICATION] THEN
849 ARITH_TAC, DISCH_TAC THEN ASM_REWRITE_TAC [] THEN
850 MATCH_MP_TAC INFINITE_DIFF_FINITE' THEN
851 REWRITE_TAC [FINITE_NUMSEG_LT, num_INFINITE]]
852QED
853
854(* ------------------------------------------------------------------------- *)
855(* Topological sorting of a finite set. *)
856(* ------------------------------------------------------------------------- *)
857
858val _ = temp_set_fixity "<<" (Infix(NONASSOC, 450))
859
860Theorem TOPOLOGICAL_SORT:
861 !(<<). (!x y:'a. x << y /\ y << x ==> (x = y)) /\
862 (!x y z. x << y /\ y << z ==> x << z)
863 ==> !n s. s HAS_SIZE n
864 ==> ?f. (s = IMAGE f {1..n}) /\
865 (!j k. j IN {1..n} /\ k IN {1..n} /\ j < k
866 ==> ~(f k << f j))
867Proof
868 GEN_TAC THEN DISCH_TAC THEN
869 SUBGOAL_THEN ``!n s. s HAS_SIZE n /\ ~(s = {})
870 ==> ?a:'a. a IN s /\ !b. b IN (s DELETE a) ==> ~(b << a)``
871 ASSUME_TAC THENL
872 [INDUCT_TAC THEN
873 REWRITE_TAC[HAS_SIZE_0, HAS_SIZE_SUC, TAUT `~(a /\ ~a)`] THEN
874 X_GEN_TAC ``s:'a->bool`` THEN STRIP_TAC THEN
875 UNDISCH_TAC ``(s:'a->bool) <> {}`` THEN DISCH_TAC THEN
876 FIRST_X_ASSUM(MP_TAC o REWRITE_RULE [GSYM MEMBER_NOT_EMPTY]) THEN
877 DISCH_THEN(X_CHOOSE_TAC ``a:'a``) THEN
878 FIRST_X_ASSUM(MP_TAC o SPEC ``a:'a``) THEN ASM_REWRITE_TAC[] THEN
879 DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC ``s DELETE (a:'a)``) THEN
880 ASM_SIMP_TAC std_ss [SET_RULE ``a IN s ==> ((s DELETE a = {}) <=> (s = {a}))``] THEN
881 ASM_CASES_TAC ``s = {a:'a}`` THEN ASM_SIMP_TAC std_ss [] THENL
882 [EXISTS_TAC ``a:'a`` THEN SET_TAC[], ALL_TAC] THEN
883 DISCH_THEN(X_CHOOSE_THEN ``b:'a`` STRIP_ASSUME_TAC) THEN
884 ASM_CASES_TAC ``((a:'a) << (b:'a)) :bool`` THENL
885 [EXISTS_TAC ``a:'a``, EXISTS_TAC ``b:'a``] THEN ASM_SET_TAC[],
886 ALL_TAC] THEN
887 INDUCT_TAC THENL
888 [SIMP_TAC arith_ss [HAS_SIZE_0, NUMSEG_CLAUSES, IMAGE_EMPTY, IMAGE_INSERT, NOT_IN_EMPTY],
889 ALL_TAC] THEN
890 REWRITE_TAC[HAS_SIZE_SUC] THEN X_GEN_TAC ``s:'a->bool`` THEN STRIP_TAC THEN
891 FIRST_X_ASSUM(MP_TAC o SPECL [``SUC n``, ``s:'a->bool``]) THEN
892 ASM_REWRITE_TAC[HAS_SIZE_SUC] THEN
893 DISCH_THEN(X_CHOOSE_THEN ``a:'a`` MP_TAC) THEN STRIP_TAC THEN
894 FIRST_X_ASSUM(MP_TAC o SPEC ``s DELETE (a:'a)``) THEN ASM_SIMP_TAC std_ss [] THEN
895 DISCH_THEN(X_CHOOSE_THEN ``f:num->'a`` STRIP_ASSUME_TAC) THEN
896 EXISTS_TAC ``\k. if k = 1n then a:'a else f(k - 1)`` THEN
897 SIMP_TAC std_ss [ARITH_PROVE ``1 <= k ==> ~(SUC k = 1)``, SUC_SUB1] THEN
898 SUBGOAL_THEN ``!i. i IN {1..SUC n} <=> i = 1 \/ 1 < i /\ i - 1 IN {1..n}``
899 (fn th => REWRITE_TAC[EXTENSION, IN_IMAGE, th])
900 THENL [REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC, ALL_TAC] THEN CONJ_TAC THENL
901 [X_GEN_TAC ``b:'a`` THEN ASM_CASES_TAC ``b:'a = a`` THENL
902 [METIS_TAC[], ALL_TAC] THEN
903 FIRST_ASSUM(fn th => ONCE_REWRITE_TAC[MATCH_MP
904 (SET_RULE ``~(b = a) ==> (b IN s <=> b IN (s DELETE a))``) th]) THEN
905 ONCE_REWRITE_TAC[COND_RAND] THEN
906 ASM_REWRITE_TAC[IN_IMAGE, IN_NUMSEG] THEN
907 EQ_TAC THENL [ALL_TAC, METIS_TAC[]] THEN
908 DISCH_THEN(X_CHOOSE_TAC ``i:num``) THEN EXISTS_TAC ``i + 1:num`` THEN
909 ASM_SIMP_TAC arith_ss [ARITH_PROVE ``1 <= x ==> 1 < x + 1 /\ ~(x + 1 = 1:num)``, ADD_SUB],
910 MAP_EVERY X_GEN_TAC [``j:num``, ``k:num``] THEN
911 MAP_EVERY ASM_CASES_TAC [``j = 1:num``, ``k = 1:num``] THEN
912 ASM_REWRITE_TAC[LESS_REFL] THENL
913 [STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SET_TAC[],
914 ARITH_TAC,
915 STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
916 ASM_SIMP_TAC arith_ss []]]
917QED
918
919(* Another form using relationTheory and (count n), added by Chun Tian
920
921 NOTE: the set sorting is slightly different with list sorting, as there are
922 no duplicated elements in sets, thus the sorting result (given by an index
923 function) has strict orders for each pair of elements.
924
925 Also, the sorting requirements is slightly different: list sorting requires
926 ‘transitive’ and ‘total’ (cf. sortingTheory.QSORT_SORTED), while set sorting
927 here requires ‘transitive’ and ‘antisymmetric’. (‘~R x y’ also means that
928 x and y are incomparable, i.e. some part of ‘f’ is an "antichain".)
929 *)
930Theorem TOPOLOGICAL_SORT' :
931 !R s n. transitive R /\ antisymmetric R /\ s HAS_SIZE n ==>
932 ?f. s = IMAGE f (count n) /\
933 !j k. j < n /\ k < n /\ j < k ==> ~(R (f k) (f j))
934Proof
935 RW_TAC std_ss []
936 >> MP_TAC (REWRITE_RULE [GSYM transitive_def, GSYM antisymmetric_def]
937 (Q.SPEC ‘R’ TOPOLOGICAL_SORT))
938 >> RW_TAC std_ss []
939 >> POP_ASSUM (MP_TAC o (Q.SPECL [‘n’, ‘s’]))
940 >> RW_TAC std_ss [IN_NUMSEG]
941 >> Q.EXISTS_TAC ‘f o SUC’
942 >> CONJ_TAC
943 >- (rw [Once EXTENSION, IN_IMAGE, IN_COUNT, IN_NUMSEG] \\
944 EQ_TAC >> rw [] >| (* 2 subgoals *)
945 [ (* goal 1 (of 2) *)
946 rename1 ‘i <= n’ >> Q.EXISTS_TAC ‘PRE i’ >> rw [] \\
947 Suff ‘SUC (PRE i) = i’ >- Rewr \\
948 rw [GSYM SUC_PRE],
949 (* goal 2 (of 2) *)
950 rename1 ‘i < n’ >> Q.EXISTS_TAC ‘SUC i’ >> rw [] ])
951 >> RW_TAC arith_ss []
952QED
953
954(* ------------------------------------------------------------------------- *)
955(* Generic iteration of operation over set with finite support. *)
956(* ------------------------------------------------------------------------- *)
957
958Definition neutral[nocompute]:
959 neutral op = @x. !y. (op x y = y) /\ (op y x = y)
960End
961
962(* NOTE: The set of all numbers of the involved type, ‘op’ and ‘neutral op’
963 actually form an Abelian Monoid (also called Commutative Monoid), i.e.
964
965 |- monoidal op <=>
966 AbelianMonoid <| carrier = UNIV, op = op, id = (neutral op) |>
967
968 (see also AbelianMonoid_def in examples/algebra/monoid/monoidScript.sml)
969 *)
970Definition monoidal[nocompute]:
971 monoidal op <=> (!x y. op x y = op y x) /\
972 (!x y z. op x (op y z) = op (op x y) z) /\
973 (!x:'a. op (neutral op) x = x)
974End
975
976Theorem MONOIDAL_AC:
977 !op. monoidal op
978 ==> (!a. op (neutral op) a = a) /\
979 (!a. op a (neutral op) = a) /\
980 (!a b. op a b = op b a) /\
981 (!a b c. op (op a b) c = op a (op b c)) /\
982 (!a b c. op a (op b c) = op b (op a c))
983Proof
984 REWRITE_TAC[monoidal] THEN MESON_TAC[]
985QED
986
987Definition support[nocompute]:
988 support op (f:'a->'b) s = {x | x IN s /\ ~(f x = neutral op)}
989End
990
991Definition iterate[nocompute]:
992 iterate op (s:'a->bool) f =
993 if FINITE(support op f s)
994 then ITSET (\x a. op (f x) a) (support op f s) (neutral op)
995 else neutral op
996End
997
998Theorem IN_SUPPORT:
999 !op f x s. x IN (support op f s) <=> x IN s /\ ~(f x = neutral op)
1000Proof
1001 SIMP_TAC std_ss [support, GSPECIFICATION]
1002QED
1003
1004Theorem SUPPORT_SUPPORT:
1005 !op f s. support op f (support op f s) = support op f s
1006Proof
1007 SIMP_TAC std_ss [support, GSPECIFICATION, EXTENSION]
1008QED
1009
1010Theorem SUPPORT_EMPTY:
1011 !op f s. (!x. x IN s ==> (f(x) = neutral op)) <=> (support op f s = {})
1012Proof
1013 SIMP_TAC std_ss [IN_SUPPORT, EXTENSION, GSPECIFICATION, NOT_IN_EMPTY] THEN
1014 MESON_TAC[]
1015QED
1016
1017Theorem SUPPORT_SUBSET:
1018 !op f s. (support op f s) SUBSET s
1019Proof
1020 SIMP_TAC std_ss [SUBSET_DEF, IN_SUPPORT]
1021QED
1022
1023Theorem FINITE_SUPPORT:
1024 !op f s. FINITE s ==> FINITE(support op f s)
1025Proof
1026 MESON_TAC[SUPPORT_SUBSET, SUBSET_FINITE]
1027QED
1028
1029Theorem SUPPORT_CLAUSES:
1030 (!f. support op f {} = {}) /\
1031 (!f x s. support op f (x INSERT s) =
1032 if f(x) = neutral op then support op f s
1033 else x INSERT (support op f s)) /\
1034 (!f x s. support op f (s DELETE x) = (support op f s) DELETE x) /\
1035 (!f s t. support op f (s UNION t) =
1036 (support op f s) UNION (support op f t)) /\
1037 (!f s t. support op f (s INTER t) =
1038 (support op f s) INTER (support op f t)) /\
1039 (!f s t. support op f (s DIFF t) =
1040 (support op f s) DIFF (support op f t)) /\
1041 (!f g s. support op g (IMAGE f s) = IMAGE f (support op (g o f) s))
1042Proof
1043 SIMP_TAC std_ss [support, EXTENSION, GSPECIFICATION, IN_INSERT, IN_DELETE, o_THM,
1044 IN_IMAGE, NOT_IN_EMPTY, IN_UNION, IN_INTER, IN_DIFF, COND_RAND] THEN
1045 REPEAT STRIP_TAC THEN TRY COND_CASES_TAC THEN ASM_MESON_TAC[]
1046QED
1047
1048Theorem SUPPORT_DELTA:
1049 !op s f a. support op (\x. if x = a then f(x) else neutral op) s =
1050 if a IN s then support op f {a} else {}
1051Proof
1052 SIMP_TAC std_ss [EXTENSION, support, GSPECIFICATION, IN_SING] THEN
1053 REPEAT GEN_TAC THEN REPEAT COND_CASES_TAC THEN
1054 FULL_SIMP_TAC std_ss [GSPECIFICATION, NOT_IN_EMPTY]
1055QED
1056
1057Theorem FINITE_SUPPORT_DELTA:
1058 !op f a. FINITE(support op (\x. if x = a then f(x) else neutral op) s)
1059Proof
1060 REWRITE_TAC[SUPPORT_DELTA] THEN REPEAT GEN_TAC THEN COND_CASES_TAC THEN
1061 SIMP_TAC std_ss [FINITE_EMPTY, FINITE_INSERT, FINITE_SUPPORT]
1062QED
1063
1064(* ------------------------------------------------------------------------- *)
1065(* Key lemmas about the generic notion. *)
1066(* ------------------------------------------------------------------------- *)
1067
1068Theorem ITERATE_SUPPORT:
1069 !op f s. iterate op (support op f s) f = iterate op s f
1070Proof
1071 SIMP_TAC std_ss [iterate, SUPPORT_SUPPORT]
1072QED
1073
1074Theorem ITERATE_EXPAND_CASES:
1075 !op f s. iterate op s f =
1076 if FINITE(support op f s) then iterate op (support op f s) f
1077 else neutral op
1078Proof
1079 SIMP_TAC std_ss [iterate, SUPPORT_SUPPORT]
1080QED
1081
1082Theorem ITERATE_CLAUSES_GEN:
1083 !op. monoidal op
1084 ==> (!(f:'a->'b). iterate op {} f = neutral op) /\
1085 (!f x s. monoidal op /\ FINITE(support op (f:'a->'b) s)
1086 ==> (iterate op (x INSERT s) f =
1087 if x IN s then iterate op s f
1088 else op (f x) (iterate op s f)))
1089Proof
1090 GEN_TAC THEN STRIP_TAC THEN CONV_TAC AND_FORALL_CONV THEN
1091 GEN_TAC THEN MP_TAC(ISPECL [``\x a. (op:'b->'b->'b) ((f:'a->'b)(x)) a``,
1092 ``neutral op :'b``] FINITE_RECURSION) THEN
1093 KNOW_TAC ``(!(x :'a) (y :'a) (s :'b). x <> y ==>
1094 ((\(x :'a) (a :'b). (op :'b -> 'b -> 'b) ((f :'a -> 'b) x) a) x
1095 ((\(x :'a) (a :'b). op (f x) a) y s) = (\(x :'a) (a :'b). op (f x) a) y
1096 ((\(x :'a) (a :'b). op (f x) a) x s)))`` THENL
1097 [ASM_MESON_TAC [monoidal], FULL_SIMP_TAC std_ss [] THEN REPEAT STRIP_TAC THEN
1098 ASM_REWRITE_TAC[iterate, SUPPORT_CLAUSES, FINITE_EMPTY, FINITE_INSERT] THEN
1099 GEN_REWR_TAC (LAND_CONV o RATOR_CONV o LAND_CONV) [COND_RAND] THEN
1100 ASM_REWRITE_TAC[SUPPORT_CLAUSES, FINITE_INSERT, COND_ID] THEN
1101 ASM_CASES_TAC ``(f:'a->'b) x = neutral op`` THEN ASM_SIMP_TAC std_ss [IN_SUPPORT] THEN
1102 COND_CASES_TAC THEN ASM_MESON_TAC[monoidal]]
1103QED
1104
1105Theorem ITERATE_CLAUSES:
1106 !op. monoidal op
1107 ==> (!f:('b->'a). iterate op {} f = neutral op) /\
1108 (!f:('b->'a) x s. FINITE(s)
1109 ==> (iterate op (x INSERT s) f =
1110 if x IN s then iterate op s f
1111 else op (f x) (iterate op s f)))
1112Proof
1113 SIMP_TAC std_ss [ITERATE_CLAUSES_GEN, FINITE_SUPPORT]
1114QED
1115
1116Theorem ITERATE_UNION:
1117 !op. monoidal op
1118 ==> !f s t. FINITE s /\ FINITE t /\ DISJOINT s t
1119 ==> (iterate op (s UNION t) f =
1120 op (iterate op s f) (iterate op t f))
1121Proof
1122 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN GEN_TAC THEN
1123 REWRITE_TAC [GSYM AND_IMP_INTRO] THEN SIMP_TAC std_ss [RIGHT_FORALL_IMP_THM] THEN
1124 REPEAT DISCH_TAC THEN
1125 KNOW_TAC ``!t. (DISJOINT (s :'b -> bool) (t :'b -> bool) ==>
1126 (iterate (op :'a -> 'a -> 'a) (s UNION t) (f :'b -> 'a) =
1127 op (iterate op s f) (iterate op t f))) = (\t. DISJOINT s t ==>
1128 (iterate op (s UNION t) f = op (iterate op s f) (iterate op t f))) t``
1129 THENL [FULL_SIMP_TAC std_ss [], DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
1130 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
1131 ASM_SIMP_TAC std_ss [ITERATE_CLAUSES, UNION_EMPTY] THEN
1132 SIMP_TAC std_ss [GSYM RIGHT_FORALL_IMP_THM] THEN
1133 ONCE_REWRITE_TAC [DISJOINT_SYM] THEN FULL_SIMP_TAC std_ss [DISJOINT_INSERT]
1134 THEN ONCE_REWRITE_TAC [UNION_COMM] THEN SIMP_TAC std_ss [INSERT_UNION] THEN
1135 ASM_SIMP_TAC std_ss [ITERATE_CLAUSES, IN_UNION, UNION_EMPTY,
1136 FINITE_UNION] THEN ASM_MESON_TAC[monoidal]]
1137QED
1138
1139Theorem ITERATE_UNION_GEN:
1140 !op. monoidal op
1141 ==> !(f:'a->'b) s t. FINITE(support op f s) /\ FINITE(support op f t) /\
1142 DISJOINT (support op f s) (support op f t)
1143 ==> (iterate op (s UNION t) f =
1144 op (iterate op s f) (iterate op t f))
1145Proof
1146 ONCE_REWRITE_TAC[GSYM ITERATE_SUPPORT] THEN
1147 SIMP_TAC std_ss [SUPPORT_CLAUSES, ITERATE_UNION]
1148QED
1149
1150Theorem lemma[local]:
1151 !t s. t SUBSET s ==> (s = (s DIFF t) UNION t) /\ DISJOINT (s DIFF t) t
1152Proof
1153 rpt STRIP_TAC
1154 >| [ (* goal 1 (of 2) *)
1155 SIMP_TAC std_ss [UNION_DEF, DIFF_DEF, EXTENSION, GSPECIFICATION] \\
1156 GEN_TAC \\
1157 EQ_TAC >- FULL_SIMP_TAC std_ss [] \\
1158 STRIP_TAC \\
1159 FULL_SIMP_TAC std_ss [SUBSET_DEF],
1160 (* goal 2 (of 2) *)
1161 SIMP_TAC std_ss [DISJOINT_DEF, INTER_DEF, DIFF_DEF,
1162 EXTENSION, GSPECIFICATION, NOT_IN_EMPTY] ]
1163QED
1164
1165Theorem ITERATE_DIFF:
1166 !op. monoidal op
1167 ==> !f s t. FINITE s /\ t SUBSET s
1168 ==> (op (iterate op (s DIFF t) f) (iterate op t f) =
1169 iterate op s f)
1170Proof
1171 MESON_TAC[lemma, ITERATE_UNION, FINITE_UNION, SUBSET_FINITE, SUBSET_DIFF]
1172QED
1173
1174Theorem ITERATE_DIFF_GEN:
1175 !op. monoidal op
1176 ==> !f:'a->'b s t. FINITE (support op f s) /\
1177 (support op f t) SUBSET (support op f s)
1178 ==> (op (iterate op (s DIFF t) f) (iterate op t f) =
1179 iterate op s f)
1180Proof
1181 ONCE_REWRITE_TAC[GSYM ITERATE_SUPPORT] THEN
1182 SIMP_TAC std_ss [SUPPORT_CLAUSES, ITERATE_DIFF]
1183QED
1184
1185
1186Theorem lemma1[local]:
1187 !a b. a UNION b = ((a DIFF b) UNION (b DIFF a)) UNION (a INTER b)
1188Proof
1189 REPEAT GEN_TAC THEN REWRITE_TAC [UNION_DEF, DIFF_DEF, INTER_DEF]
1190 THEN SIMP_TAC std_ss [EXTENSION, GSPECIFICATION] THEN GEN_TAC THEN
1191 EQ_TAC THEN STRIP_TAC THEN RW_TAC std_ss []
1192QED
1193
1194Theorem lemma2[local]:
1195 !s t f. op (iterate op s f) (iterate op t f) =
1196 op (iterate op (s DIFF t UNION s INTER t) f)
1197 (iterate op (t DIFF s UNION s INTER t) f)
1198Proof
1199 REPEAT GEN_TAC THEN
1200 KNOW_TAC ``((s:'a->bool) = s DIFF t UNION s INTER t) /\
1201 ((t:'a->bool)= t DIFF s UNION s INTER t)`` THENL
1202 [REWRITE_TAC [DIFF_DEF, UNION_DEF, DIFF_DEF, INTER_DEF] THEN
1203 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION] THEN CONJ_TAC THENL
1204 [GEN_TAC THEN EQ_TAC THENL [RW_TAC std_ss [], RW_TAC std_ss []],
1205 GEN_TAC THEN EQ_TAC THENL [RW_TAC std_ss [], RW_TAC std_ss []]],
1206 DISCH_TAC THEN METIS_TAC []]
1207QED
1208
1209Theorem lemma3[local]:
1210 !s t. DISJOINT (s DIFF t UNION t DIFF s) (s INTER s') /\
1211 DISJOINT (s DIFF t) (t DIFF s) /\
1212 DISJOINT (s DIFF t) (t INTER s) /\
1213 DISJOINT (s DIFF t) (s INTER t)
1214Proof
1215 REPEAT GEN_TAC THEN
1216 REWRITE_TAC [DISJOINT_DEF, DIFF_DEF, UNION_DEF, INTER_DEF] THEN
1217 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION] THEN
1218 CONV_TAC CONJ_FORALL_CONV THEN GEN_TAC THEN CONJ_TAC THENL
1219 [EQ_TAC THENL [RW_TAC std_ss [], RW_TAC std_ss [NOT_IN_EMPTY]], CONJ_TAC THENL
1220 [EQ_TAC THENL [RW_TAC std_ss [], RW_TAC std_ss [NOT_IN_EMPTY]], CONJ_TAC THENL
1221 [EQ_TAC THENL [RW_TAC std_ss [], RW_TAC std_ss [NOT_IN_EMPTY]],
1222 EQ_TAC THENL [RW_TAC std_ss [], RW_TAC std_ss [NOT_IN_EMPTY]]]]]
1223QED
1224
1225Theorem ITERATE_INCL_EXCL:
1226 !op. monoidal op
1227 ==> !s t f. FINITE s /\ FINITE t
1228 ==> (op (iterate op s f) (iterate op t f) =
1229 op (iterate op (s UNION t) f)
1230 (iterate op (s INTER t) f))
1231Proof
1232 REPEAT STRIP_TAC THEN
1233 ONCE_REWRITE_TAC [lemma1] THEN GEN_REWR_TAC (LAND_CONV) [lemma2] THEN
1234 KNOW_TAC ``(FINITE ((s:'b->bool) DIFF (t:'b->bool) UNION (t DIFF s))) /\
1235 (FINITE (s INTER t)) /\ (DISJOINT (s DIFF t UNION (t DIFF s)) (s INTER t))`` THENL
1236 [FULL_SIMP_TAC std_ss [FINITE_DIFF, FINITE_UNION, FINITE_INTER] THEN
1237 SIMP_TAC std_ss [DISJOINT_DEF, DIFF_DEF, UNION_DEF, INTER_DEF, EXTENSION, GSPECIFICATION]
1238 THEN GEN_TAC THEN EQ_TAC THENL [RW_TAC std_ss [], RW_TAC std_ss [NOT_IN_EMPTY]],
1239 STRIP_TAC THEN ASM_SIMP_TAC std_ss [ITERATE_UNION, FINITE_UNION, FINITE_DIFF,
1240 FINITE_INTER, lemma3] THEN METIS_TAC [MONOIDAL_AC]]
1241QED
1242
1243Theorem ITERATE_CLOSED:
1244 !op. monoidal op
1245 ==> !P. P(neutral op) /\ (!x y. P x /\ P y ==> P (op x y))
1246 ==> !f:'a->'b s. (!x. x IN s /\ ~(f x = neutral op) ==> P(f x))
1247 ==> P(iterate op s f)
1248Proof
1249 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
1250 REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[GSYM IN_SUPPORT] THEN
1251 COND_CASES_TAC THEN ASM_SIMP_TAC std_ss [] THEN POP_ASSUM MP_TAC THEN
1252 SPEC_TAC(``support op (f:'a->'b) s``,``s:'a->bool``) THEN
1253 GEN_TAC THEN KNOW_TAC ``(monoidal (op :'b -> 'b -> 'b) ==>
1254 (P :'b -> bool) (neutral op) ==> (!(x :'b) (y :'b). P x /\
1255 P y ==> P (op x y)) ==> (!(x :'a). x IN s ==>
1256 P ((f :'a -> 'b) x)) ==> P (iterate op s f)) =
1257 ((\s. monoidal op ==> P (neutral op) ==>
1258 (!x y. P x /\ P y ==> P (op x y)) ==> (!x. x IN s ==> P (f x)) ==>
1259 P (iterate op s f))s)`` THENL [FULL_SIMP_TAC std_ss [],
1260 DISCH_TAC THEN ONCE_ASM_REWRITE_TAC []
1261 THEN MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
1262 ASM_SIMP_TAC std_ss [ITERATE_CLAUSES, FINITE_INSERT, IN_INSERT]]
1263QED
1264
1265Theorem ITERATE_RELATED:
1266 !op. monoidal op
1267 ==> !R. R (neutral op) (neutral op) /\
1268 (!x1 y1 x2 y2. R x1 x2 /\ R y1 y2 ==> R (op x1 y1) (op x2 y2))
1269 ==> !f:'a->'b g s.
1270 FINITE s /\
1271 (!x. x IN s ==> R (f x) (g x))
1272 ==> R (iterate op s f) (iterate op s g)
1273Proof
1274 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN
1275 GEN_TAC THEN REWRITE_TAC[GSYM AND_IMP_INTRO] THEN GEN_TAC THEN
1276 KNOW_TAC ``(!x. x IN s ==> R (f x) (g x)) ==>
1277 R (iterate op s f) (iterate op s g) <=> (\s. (!x. x IN s ==> R (f x) (g x)) ==>
1278 R (iterate op s f) (iterate op s g)) s`` THENL [FULL_SIMP_TAC std_ss [],
1279 DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
1280 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
1281 ASM_SIMP_TAC std_ss [ITERATE_CLAUSES, FINITE_INSERT, IN_INSERT]]
1282QED
1283
1284Theorem ITERATE_EQ_NEUTRAL:
1285 !op. monoidal op
1286 ==> !f:'a->'b s. (!x. x IN s ==> (f(x) = neutral op))
1287 ==> (iterate op s f = neutral op)
1288Proof
1289 REPEAT STRIP_TAC THEN
1290 SUBGOAL_THEN ``support op (f:'a->'b) s = {}`` ASSUME_TAC THENL
1291 [ASM_MESON_TAC[EXTENSION, NOT_IN_EMPTY, IN_SUPPORT],
1292 ASM_MESON_TAC[ITERATE_CLAUSES, FINITE_EMPTY, ITERATE_SUPPORT]]
1293QED
1294
1295Theorem ITERATE_SING:
1296 !op. monoidal op ==> !f:'a->'b x. (iterate op {x} f = f x)
1297Proof
1298 SIMP_TAC std_ss [ITERATE_CLAUSES, FINITE_EMPTY, NOT_IN_EMPTY] THEN
1299 MESON_TAC[monoidal]
1300QED
1301
1302Theorem ITERATE_DELETE:
1303 !op. monoidal op
1304 ==> !(f:'a->'b) s a. FINITE s /\ a IN s
1305 ==> (op (f a) (iterate op (s DELETE a) f) = iterate op s f)
1306Proof
1307 METIS_TAC[ITERATE_CLAUSES, FINITE_DELETE, IN_DELETE, INSERT_DELETE]
1308QED
1309
1310Theorem ITERATE_DELTA:
1311 !op. monoidal op
1312 ==> !f a s. iterate op s (\x. if x = a then f(x) else neutral op) =
1313 if a IN s then f(a) else neutral op
1314Proof
1315 GEN_TAC THEN DISCH_TAC THEN ONCE_REWRITE_TAC[GSYM ITERATE_SUPPORT] THEN
1316 REWRITE_TAC[SUPPORT_DELTA] THEN REPEAT GEN_TAC THEN COND_CASES_TAC THEN
1317 ASM_SIMP_TAC std_ss [ITERATE_CLAUSES] THEN REWRITE_TAC[SUPPORT_CLAUSES] THEN
1318 COND_CASES_TAC THEN ASM_SIMP_TAC std_ss [ITERATE_CLAUSES, ITERATE_SING]
1319QED
1320
1321Theorem lemma[local]:
1322 (a <=> a') /\ (a' ==> (b = b'))
1323 ==> ((if a then b else c) = (if a' then b' else c))
1324Proof
1325 METIS_TAC []
1326QED
1327
1328Theorem ITERATE_IMAGE:
1329 !op. monoidal op
1330 ==> !f:'a->'b g:'b->'c s.
1331 (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))
1332 ==> (iterate op (IMAGE f s) g = iterate op s (g o f))
1333Proof
1334 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN GEN_TAC THEN
1335 SUBGOAL_THEN ``!s. FINITE s /\
1336 (!x y:'a. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))
1337 ==> (iterate op (IMAGE f s) (g:'b->'c) = iterate op s (g o f))``
1338 ASSUME_TAC THENL [REWRITE_TAC[GSYM AND_IMP_INTRO] THEN GEN_TAC THEN
1339 KNOW_TAC ``((!x y. x IN s ==> y IN s ==> (f x = f y) ==> (x = y)) ==>
1340 (iterate op (IMAGE f s) g = iterate op s (g o f))) =
1341 (\s. (!x y. x IN s ==> y IN s ==> (f x = f y) ==> (x = y)) ==>
1342 (iterate op (IMAGE f s) g = iterate op s (g o f))) s``
1343 THENL [FULL_SIMP_TAC std_ss [], DISCH_TAC THEN ONCE_ASM_REWRITE_TAC []
1344 THEN MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
1345 ASM_SIMP_TAC std_ss [ITERATE_CLAUSES, IMAGE_EMPTY, IMAGE_INSERT, IMAGE_FINITE] THEN
1346 REWRITE_TAC[o_THM, IN_INSERT] THEN REPEAT STRIP_TAC THEN COND_CASES_TAC THENL
1347 [METIS_TAC[IN_IMAGE], METIS_TAC[IN_IMAGE]]], GEN_TAC THEN DISCH_TAC
1348 THEN ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN REPEAT STRIP_TAC THEN
1349 MATCH_MP_TAC lemma THEN REWRITE_TAC[SUPPORT_CLAUSES] THEN REPEAT STRIP_TAC THENL
1350 [MATCH_MP_TAC FINITE_IMAGE_INJ_EQ THEN ASM_MESON_TAC[IN_SUPPORT],
1351 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[IN_SUPPORT]]]
1352QED
1353
1354Theorem ITERATE_BIJECTION:
1355 !op. monoidal op
1356 ==> !(f:'a->'b) p s.
1357 (!x. x IN s ==> (p x IN s)) /\
1358 (!y. y IN s ==> ?!x. x IN s /\ (p x = y))
1359 ==> (iterate op s f = iterate op s (f o p))
1360Proof
1361 REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1362 EXISTS_TAC ``iterate op (IMAGE (p:'a->'a) s) (f:'a->'b)`` THEN CONJ_TAC THENL
1363 [AP_THM_TAC THEN AP_TERM_TAC THEN SIMP_TAC std_ss[EXTENSION, IN_IMAGE] THEN METIS_TAC [],
1364 METIS_TAC[ITERATE_IMAGE]]
1365QED
1366
1367Theorem ITERATE_PERMUTES :
1368 !op. monoidal op
1369 ==> !(f:'a->'b) p s. p PERMUTES s
1370 ==> (iterate op s f = iterate op s (f o p))
1371Proof
1372 RW_TAC std_ss [BIJ_ALT, IN_FUNSET]
1373 >> irule ITERATE_BIJECTION
1374 >> RW_TAC std_ss []
1375 >> ONCE_REWRITE_TAC [EQ_SYM_EQ]
1376 >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
1377QED
1378
1379Theorem lemma1[local]:
1380 {a,b | F} = {}
1381Proof
1382 SRW_TAC [][EXTENSION]
1383QED
1384
1385Theorem lemma2[local]:
1386 {i,j | i IN a INSERT s /\ j IN t i} =
1387 IMAGE (\j. a,j) (t a) UNION {i,j | i IN s /\ j IN t i}
1388Proof
1389 SRW_TAC [][EXTENSION] THEN SET_TAC []
1390QED
1391
1392Theorem ITERATE_ITERATE_PRODUCT:
1393 !op. monoidal op
1394 ==> !s:'a->bool t:'a->'b->bool x:'a->'b->'c.
1395 FINITE s /\ (!i. i IN s ==> FINITE(t i))
1396 ==> (iterate op s (\i. iterate op (t i) (x i)) =
1397 iterate op {i,j | i IN s /\ j IN t i} (\(i,j). x i j))
1398Proof
1399 GEN_TAC THEN DISCH_TAC THEN
1400 SIMP_TAC std_ss [GSYM AND_IMP_INTRO, RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN
1401 KNOW_TAC ``(!t:'a->'b->bool. (!i. i IN s ==> FINITE (t i)) ==>
1402 !x:'a->'b->'c. iterate op s (\i. iterate op (t i) (x i)) =
1403 iterate op {(i,j) | i IN s /\ j IN t i} (\(i,j). x i j)) =
1404 (\s. !t:'a->'b->bool. (!i. i IN s ==> FINITE (t i)) ==>
1405 !x:'a->'b->'c. iterate op s (\i. iterate op (t i) (x i)) =
1406 iterate op {(i,j) | i IN s /\ j IN t i} (\(i,j). x i j)) (s:'a->bool)``
1407 THENL [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISC_RW_KILL THEN
1408 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
1409 ASM_SIMP_TAC std_ss [NOT_IN_EMPTY, lemma1, ITERATE_CLAUSES] THEN
1410 REWRITE_TAC[lemma2] THEN ASM_SIMP_TAC std_ss [FINITE_INSERT, ITERATE_CLAUSES,
1411 IN_INSERT] THEN REPEAT STRIP_TAC THEN
1412 FIRST_ASSUM(fn th =>
1413 W(MP_TAC o PART_MATCH (lhand o rand) (MATCH_MP ITERATE_UNION th) o
1414 rand o snd)) THEN
1415 KNOW_TAC ``FINITE (IMAGE (\j. (e,j)) ((t:'a->'b->bool) e)) /\
1416 FINITE {(i,j) | i IN (s:'a->bool) /\ j IN t i} /\
1417 DISJOINT (IMAGE (\j. (e,j)) (t e)) {(i,j) | i IN s /\ j IN t i}`` THENL
1418 [ASM_SIMP_TAC std_ss [IMAGE_FINITE, FINITE_PRODUCT_DEPENDENT, IN_INSERT] THEN
1419 SIMP_TAC std_ss [DISJOINT_DEF, EXTENSION, IN_IMAGE, IN_INTER, NOT_IN_EMPTY,
1420 GSPECIFICATION, EXISTS_PROD, FORALL_PROD, PAIR_EQ] THEN ASM_MESON_TAC[],
1421 ALL_TAC] THEN DISCH_TAC THEN ASM_REWRITE_TAC [] THEN
1422 DISCH_THEN SUBST1_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
1423 FIRST_ASSUM(fn th =>
1424 W(MP_TAC o PART_MATCH (lhand o rand) (MATCH_MP ITERATE_IMAGE th) o
1425 rand o snd)) THEN KNOW_TAC ``(!x:'b y:'b. x IN (t:'a->'b->bool) (e:'a) /\
1426 y IN t e /\ ((\j. (e,j)) x = (\j. (e,j)) y) ==> (x = y))`` THENL
1427 [SIMP_TAC std_ss [FORALL_PROD], ALL_TAC] THEN DISCH_TAC THEN
1428 ASM_REWRITE_TAC [] THEN DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[o_DEF] THEN
1429 CONV_TAC(ONCE_DEPTH_CONV BETA_CONV) THEN FULL_SIMP_TAC std_ss [ETA_AX]
1430 THEN AP_TERM_TAC THEN METIS_TAC []
1431QED
1432
1433Theorem ITERATE_EQ:
1434 !op. monoidal op
1435 ==> !f:'a->'b g s.
1436 (!x. x IN s ==> (f x = g x)) ==> (iterate op s f = iterate op s g)
1437Proof
1438 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
1439 SUBGOAL_THEN ``support op g s = support op (f:'a->'b) s`` SUBST1_TAC THENL
1440 [REWRITE_TAC[EXTENSION, IN_SUPPORT] THEN ASM_MESON_TAC[], COND_CASES_TAC THEN
1441 ASM_REWRITE_TAC[] THEN SUBGOAL_THEN
1442 ``FINITE(support op (f:'a->'b) s) /\
1443 (!x. x IN (support op f s) ==> (f x = g x))``
1444 MP_TAC THENL [ASM_MESON_TAC[IN_SUPPORT], REWRITE_TAC[GSYM AND_IMP_INTRO] THEN
1445 SPEC_TAC(``support op (f:'a->'b) s``,``t:'a->bool``) THEN GEN_TAC THEN
1446 KNOW_TAC ``(!x. x IN t ==> (f x = g x)) ==> (iterate op t f = iterate op t g) <=>
1447 (\t. (!x. x IN t ==> (f x = g x)) ==> (iterate op t f = iterate op t g)) t``
1448 THENL [FULL_SIMP_TAC std_ss [], DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
1449 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN ASM_SIMP_TAC std_ss [ITERATE_CLAUSES] THEN
1450 MESON_TAC[IN_INSERT]]]]
1451QED
1452
1453Theorem ITERATE_EQ_GENERAL:
1454 !op. monoidal op
1455 ==> !s:'a->bool t:'b->bool f:'a->'c g h.
1456 (!y. y IN t ==> ?!x. x IN s /\ (h(x) = y)) /\
1457 (!x. x IN s ==> h(x) IN t /\ (g(h x) = f x))
1458 ==> (iterate op s f = iterate op t g)
1459Proof
1460 REPEAT STRIP_TAC THEN
1461 SUBGOAL_THEN ``t = IMAGE (h:'a->'b) s`` SUBST1_TAC THENL
1462 [REWRITE_TAC[EXTENSION, IN_IMAGE] THEN ASM_MESON_TAC[],
1463 MATCH_MP_TAC EQ_TRANS THEN
1464 EXISTS_TAC ``iterate op s ((g:'b->'c) o (h:'a->'b))`` THEN CONJ_TAC THENL
1465 [ASM_MESON_TAC[ITERATE_EQ, o_THM],
1466 CONV_TAC SYM_CONV THEN
1467 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP ITERATE_IMAGE) THEN
1468 ASM_MESON_TAC[]]]
1469QED
1470
1471Theorem ITERATE_EQ_GENERAL_INVERSES:
1472 !op. monoidal op
1473 ==> !s:'a->bool t:'b->bool f:'a->'c g h k.
1474 (!y. y IN t ==> k(y) IN s /\ (h(k y) = y)) /\
1475 (!x. x IN s ==> h(x) IN t /\ (k(h x) = x) /\ (g(h x) = f x))
1476 ==> (iterate op s f = iterate op t g)
1477Proof
1478 REPEAT STRIP_TAC THEN
1479 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP ITERATE_EQ_GENERAL) THEN
1480 EXISTS_TAC ``h:'a->'b`` THEN ASM_MESON_TAC[]
1481QED
1482
1483Theorem ITERATE_INJECTION:
1484 !op. monoidal op
1485 ==> !f:'a->'b p:'a->'a s.
1486 FINITE s /\
1487 (!x. x IN s ==> p x IN s) /\
1488 (!x y. x IN s /\ y IN s /\ (p x = p y) ==> (x = y))
1489 ==> (iterate op s (f o p) = iterate op s f)
1490Proof
1491 REPEAT STRIP_TAC THEN CONV_TAC SYM_CONV THEN
1492 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP ITERATE_BIJECTION) THEN
1493 MP_TAC(ISPECL [``s:'a->bool``, ``p:'a->'a``] SURJECTIVE_IFF_INJECTIVE) THEN
1494 ASM_REWRITE_TAC[SUBSET_DEF, IN_IMAGE] THEN ASM_MESON_TAC[]
1495QED
1496
1497Theorem ITERATE_UNION_NONZERO:
1498 !op. monoidal op
1499 ==> !f:'a->'b s t.
1500 FINITE(s) /\ FINITE(t) /\
1501 (!x. x IN (s INTER t) ==> (f x = neutral(op)))
1502 ==> (iterate op (s UNION t) f =
1503 op (iterate op s f) (iterate op t f))
1504Proof
1505 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM ITERATE_SUPPORT] THEN
1506 REWRITE_TAC[SUPPORT_CLAUSES] THEN KNOW_TAC
1507 ``FINITE (support op (f :'a -> 'b) (s :'a -> bool)) /\
1508 FINITE (support op f (t :'a -> bool)) /\
1509 DISJOINT (support op f s) (support op f t)`` THENL
1510 [ASM_SIMP_TAC std_ss [FINITE_SUPPORT, DISJOINT_DEF, IN_INTER,
1511 IN_SUPPORT, EXTENSION] THEN ASM_MESON_TAC[IN_INTER, NOT_IN_EMPTY],
1512 ASM_MESON_TAC[ITERATE_UNION]]
1513QED
1514
1515Theorem ITERATE_OP:
1516 !op. monoidal op
1517 ==> !f g s. FINITE s
1518 ==> (iterate op s (\x. op (f x) (g x)) =
1519 op (iterate op s f) (iterate op s g))
1520Proof
1521 GEN_TAC THEN DISCH_TAC THEN
1522 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
1523 KNOW_TAC ``((iterate :('a -> 'a -> 'a) -> ('b -> bool) -> ('b -> 'a) -> 'a)
1524 (op :'a -> 'a -> 'a) s
1525 (\(x :'b). op ((f :'b -> 'a) x) ((g :'b -> 'a) x)) =
1526 op (iterate op s f) (iterate op s g)) =
1527 (\s. ((iterate :('a -> 'a -> 'a) -> ('b -> bool) -> ('b -> 'a) -> 'a)
1528 (op :'a -> 'a -> 'a) s
1529 (\(x :'b). op ((f :'b -> 'a) x) ((g :'b -> 'a) x)) =
1530 op (iterate op s f) (iterate op s g)))s ``THENL [FULL_SIMP_TAC std_ss [],
1531 DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
1532 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
1533 ASM_SIMP_TAC std_ss [ITERATE_CLAUSES, MONOIDAL_AC]]
1534QED
1535
1536Theorem ITERATE_SUPERSET:
1537 !op. monoidal op
1538 ==> !f:'a->'b u v.
1539 u SUBSET v /\
1540 (!x. x IN v /\ ~(x IN u) ==> (f(x) = neutral op))
1541 ==> (iterate op v f = iterate op u f)
1542Proof
1543 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM ITERATE_SUPPORT] THEN
1544 AP_THM_TAC THEN AP_TERM_TAC THEN
1545 SIMP_TAC std_ss [support, EXTENSION, GSPECIFICATION] THEN
1546 ASM_MESON_TAC[SUBSET_DEF]
1547QED
1548
1549Theorem ITERATE_IMAGE_NONZERO:
1550 !op. monoidal op
1551 ==> !g:'b->'c f:'a->'b s.
1552 FINITE s /\
1553 (!x y. x IN s /\ y IN s /\ ~(x = y) /\ (f x = f y)
1554 ==> (g(f x) = neutral op))
1555 ==> (iterate op (IMAGE f s) g = iterate op s (g o f))
1556Proof
1557 GEN_TAC THEN DISCH_TAC THEN
1558 GEN_TAC THEN GEN_TAC THEN ONCE_REWRITE_TAC[GSYM AND_IMP_INTRO] THEN GEN_TAC THEN
1559 KNOW_TAC `` ((!(x :'a) (y :'a).
1560 x IN s /\ y IN s /\ x <> y /\ ((f :'a -> 'b) x = f y) ==>
1561 ((g :'b -> 'c) (f x) = neutral (op :'c -> 'c -> 'c))) ==>
1562 (iterate op (IMAGE f s) g = iterate op s (g o f))) = (\s. (!(x :'a) (y :'a).
1563 x IN s /\ y IN s /\ x <> y /\ ((f :'a -> 'b) x = f y) ==>
1564 ((g :'b -> 'c) (f x) = neutral (op :'c -> 'c -> 'c))) ==>
1565 (iterate op (IMAGE f s) g = iterate op s (g o f))) s`` THENL
1566 [FULL_SIMP_TAC std_ss [], DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
1567 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
1568 ASM_SIMP_TAC std_ss [IMAGE_EMPTY, IMAGE_INSERT, ITERATE_CLAUSES, IMAGE_FINITE]
1569 THEN SIMP_TAC std_ss [GSYM RIGHT_FORALL_IMP_THM] THEN
1570 MAP_EVERY X_GEN_TAC [``s':'a->bool``,``a:'a``] THEN
1571 REWRITE_TAC[IN_INSERT] THEN REPEAT STRIP_TAC THEN
1572 SUBGOAL_THEN ``iterate op s' ((g:'b->'c) o (f:'a->'b)) = iterate op (IMAGE f s') g``
1573 SUBST1_TAC THENL [ASM_MESON_TAC[], ALL_TAC] THEN
1574 REWRITE_TAC[IN_IMAGE] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[o_THM] THEN
1575 SUBGOAL_THEN ``(g:'b->'c) ((f:'a->'b) a) = neutral op`` SUBST1_TAC THEN
1576 ASM_MESON_TAC[MONOIDAL_AC]]
1577QED
1578
1579Theorem lemma[local]:
1580 !s. DISJOINT {x | x IN s /\ P x} {x | x IN s /\ ~P x}
1581Proof
1582 GEN_TAC THEN SIMP_TAC std_ss [DISJOINT_DEF, INTER_DEF, EXTENSION, GSPECIFICATION]
1583 THEN GEN_TAC THEN EQ_TAC THENL
1584 [RW_TAC std_ss [], RW_TAC std_ss [NOT_IN_EMPTY]]
1585QED
1586
1587Theorem ITERATE_CASES:
1588 !op. monoidal op
1589 ==> !s P f g:'a->'b.
1590 FINITE s
1591 ==> (iterate op s (\x. if P x then f x else g x) =
1592 op (iterate op {x | x IN s /\ P x} f)
1593 (iterate op {x | x IN s /\ ~P x} g))
1594Proof
1595 REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1596 EXISTS_TAC
1597 ``op (iterate op {x | x IN s /\ P x} (\x. if P x then f x else (g:'a->'b) x))
1598 (iterate op {x | x IN s /\ ~P x} (\x. if P x then f x else g x))`` THEN
1599 CONJ_TAC THENL [KNOW_TAC ``FINITE {(x:'a) | x IN s /\ P x} /\
1600 FINITE {x | x IN s /\ ~P x} /\ DISJOINT {x | x IN s /\ P x} {x | x IN s /\ ~P x}``
1601 THENL [FULL_SIMP_TAC std_ss [FINITE_RESTRICT, lemma], STRIP_TAC THEN
1602 FULL_SIMP_TAC std_ss [GSYM ITERATE_UNION] THEN AP_THM_TAC THEN AP_TERM_TAC
1603 THEN FULL_SIMP_TAC std_ss [UNION_DEF, EXTENSION, GSPECIFICATION] THEN METIS_TAC []],
1604 BINOP_TAC THEN FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP ITERATE_EQ) THEN
1605 SIMP_TAC std_ss [GSPECIFICATION]]
1606QED
1607
1608Theorem ITERATE_OP_GEN:
1609 !op. monoidal op
1610 ==> !f g:'a->'b s.
1611 FINITE(support op f s) /\ FINITE(support op g s)
1612 ==> (iterate op s (\x. op (f x) (g x)) =
1613 op (iterate op s f) (iterate op s g))
1614Proof
1615 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM ITERATE_SUPPORT] THEN
1616 MATCH_MP_TAC EQ_TRANS THEN
1617 EXISTS_TAC ``iterate op (support op f s UNION support op g s)
1618 (\x. op ((f:'a->'b) x) (g x))`` THEN
1619 CONJ_TAC THENL [CONV_TAC SYM_CONV,
1620 ASM_SIMP_TAC std_ss [ITERATE_OP, FINITE_UNION] THEN BINOP_TAC] THEN
1621 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP ITERATE_SUPERSET) THEN
1622 SIMP_TAC std_ss [support, GSPECIFICATION, SUBSET_DEF, IN_UNION] THEN
1623 ASM_MESON_TAC[monoidal]
1624QED
1625
1626Theorem ITERATE_CLAUSES_NUMSEG:
1627 !op. monoidal op
1628 ==> (!m. iterate op {m..0} f = if m = 0 then f(0) else neutral op) /\
1629 (!m n. iterate op {m..SUC n} f =
1630 if m <= SUC n then op (iterate op {m..n} f) (f(SUC n))
1631 else iterate op {m..n} f)
1632Proof
1633 REWRITE_TAC[NUMSEG_CLAUSES] THEN REPEAT STRIP_TAC THEN
1634 COND_CASES_TAC THEN
1635 ASM_SIMP_TAC std_ss [ITERATE_CLAUSES, FINITE_NUMSEG, IN_NUMSEG, FINITE_EMPTY] THEN
1636 REWRITE_TAC[ARITH_PROVE ``~(SUC n <= n)``, NOT_IN_EMPTY] THEN
1637 ASM_MESON_TAC[monoidal]
1638QED
1639
1640Theorem ITERATE_PAIR:
1641 !op. monoidal op
1642 ==> !f m n. iterate op {2*m..2*n+1} f =
1643 iterate op {m..n} (\i. op (f(2*i)) (f(2*i+1)))
1644Proof
1645 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN GEN_TAC THEN
1646 INDUCT_TAC THEN CONV_TAC REDUCE_CONV THENL
1647 [REWRITE_TAC [ONE] THEN ASM_SIMP_TAC std_ss [ITERATE_CLAUSES_NUMSEG] THEN
1648 REWRITE_TAC [ONE] THEN
1649 REWRITE_TAC[ARITH_PROVE ``2 * m <= SUC 0 <=> (m = 0)``] THEN
1650 COND_CASES_TAC THEN ASM_REWRITE_TAC[MULT_EQ_0],
1651 REWRITE_TAC[ARITH_PROVE ``2 * SUC n + 1 = SUC(SUC(2 * n + 1))``] THEN
1652 ASM_SIMP_TAC std_ss [ITERATE_CLAUSES_NUMSEG] THEN
1653 REWRITE_TAC[ARITH_PROVE ``2 * m <= SUC(SUC(2 * n + 1)) <=> m <= SUC n``,
1654 ARITH_PROVE ``2 * m <= SUC(2 * n + 1) <=> m <= SUC n``] THEN
1655 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
1656 REWRITE_TAC[ARITH_PROVE ``2 * SUC n = SUC(2 * n + 1)``,
1657 ARITH_PROVE ``2 * SUC n + 1 = SUC(SUC(2 * n + 1))``] THEN
1658 ASM_MESON_TAC[monoidal]]
1659QED
1660
1661(* ------------------------------------------------------------------------- *)
1662(* Sums of natural numbers. *)
1663(* ------------------------------------------------------------------------- *)
1664
1665Definition nsum :
1666 (nsum :('a->bool)->('a->num)->num) = iterate (+)
1667End
1668
1669Theorem NEUTRAL_ADD:
1670 neutral((+):num->num->num) = 0
1671Proof
1672 REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
1673 MESON_TAC[ADD_CLAUSES]
1674QED
1675
1676Theorem NEUTRAL_MUL:
1677 neutral(( * ):num->num->num) = 1
1678Proof
1679 REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
1680 MESON_TAC[MULT_CLAUSES, MULT_EQ_1]
1681QED
1682
1683Theorem MONOIDAL_ADD:
1684 monoidal((+):num->num->num)
1685Proof
1686 REWRITE_TAC[monoidal, NEUTRAL_ADD] THEN ARITH_TAC
1687QED
1688
1689Theorem MONOIDAL_MUL:
1690 monoidal(( * ):num->num->num)
1691Proof
1692 REWRITE_TAC[monoidal, NEUTRAL_MUL] THEN ARITH_TAC
1693QED
1694
1695Theorem NSUM_DEGENERATE:
1696 !f s. ~(FINITE {x | x IN s /\ ~(f x = 0:num)}) ==> (nsum s f = 0:num)
1697Proof
1698 REPEAT GEN_TAC THEN REWRITE_TAC[nsum] THEN
1699 SIMP_TAC std_ss [iterate, support, NEUTRAL_ADD]
1700QED
1701
1702Theorem NSUM_CLAUSES:
1703 (!f. nsum {} f = 0) /\
1704 (!x f s. FINITE(s)
1705 ==> (nsum (x INSERT s) f =
1706 if x IN s then nsum s f else f(x) + nsum s f))
1707Proof
1708 REWRITE_TAC[nsum, GSYM NEUTRAL_ADD] THEN
1709 KNOW_TAC ``monoidal ((+):num->num->num)`` THENL [REWRITE_TAC[MONOIDAL_ADD],
1710 METIS_TAC [ITERATE_CLAUSES]]
1711QED
1712
1713Theorem NSUM_UNION:
1714 !f s t. FINITE s /\ FINITE t /\ DISJOINT s t
1715 ==> (nsum (s UNION t) f = nsum s f + nsum t f)
1716Proof
1717 SIMP_TAC std_ss [nsum, ITERATE_UNION, MONOIDAL_ADD]
1718QED
1719
1720Theorem NSUM_DIFF:
1721 !f s t. FINITE s /\ t SUBSET s
1722 ==> (nsum (s DIFF t) f = nsum s f - nsum t f)
1723Proof
1724 REPEAT STRIP_TAC THEN
1725 MATCH_MP_TAC(ARITH_PROVE ``(x + z = y:num) ==> (x = y - z)``) THEN
1726 ASM_SIMP_TAC std_ss [nsum, ITERATE_DIFF, MONOIDAL_ADD]
1727QED
1728
1729Theorem NSUM_INCL_EXCL:
1730 !s t (f:'a->num).
1731 FINITE s /\ FINITE t
1732 ==> (nsum s f + nsum t f = nsum (s UNION t) f + nsum (s INTER t) f)
1733Proof
1734 REWRITE_TAC[nsum, GSYM NEUTRAL_ADD] THEN
1735 MATCH_MP_TAC ITERATE_INCL_EXCL THEN REWRITE_TAC[MONOIDAL_ADD]
1736QED
1737
1738Theorem NSUM_SUPPORT:
1739 !f s. nsum (support (+) f s) f = nsum s f
1740Proof
1741 SIMP_TAC std_ss [nsum, iterate, SUPPORT_SUPPORT]
1742QED
1743
1744Theorem NSUM_ADD:
1745 !f g s. FINITE s ==> (nsum s (\x. f(x) + g(x)) = nsum s f + nsum s g)
1746Proof
1747 SIMP_TAC std_ss [nsum, ITERATE_OP, MONOIDAL_ADD]
1748QED
1749
1750Theorem NSUM_ADD_GEN:
1751 !f g s.
1752 FINITE {x | x IN s /\ ~(f x = 0)} /\ FINITE {x | x IN s /\ ~(g x = 0:num)}
1753 ==> (nsum s (\x. f x + g x) = nsum s f + nsum s g)
1754Proof
1755 REWRITE_TAC[GSYM NEUTRAL_ADD, GSYM support, nsum] THEN
1756 MATCH_MP_TAC ITERATE_OP_GEN THEN ACCEPT_TAC MONOIDAL_ADD
1757QED
1758
1759Theorem NSUM_EQ_0:
1760 !f s. (!x:'a. x IN s ==> (f(x) = 0:num)) ==> (nsum s f = 0:num)
1761Proof
1762 REWRITE_TAC[nsum, GSYM NEUTRAL_ADD] THEN
1763 SIMP_TAC std_ss [ITERATE_EQ_NEUTRAL, MONOIDAL_ADD]
1764QED
1765
1766Theorem NSUM_0:
1767 !s:'a->bool. nsum s (\n. 0:num) = 0:num
1768Proof
1769 SIMP_TAC std_ss [NSUM_EQ_0]
1770QED
1771
1772Theorem NSUM_LMUL:
1773 !f c s:'a->bool. nsum s (\x. c * f(x)) = c * nsum s f
1774Proof
1775 REPEAT GEN_TAC THEN ASM_CASES_TAC ``c = 0:num`` THEN
1776 ASM_REWRITE_TAC[MULT_CLAUSES, NSUM_0] THEN REWRITE_TAC[nsum] THEN
1777 ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
1778 SUBGOAL_THEN ``support (+) (\x:'a. (c:num) * f(x)) s = support (+) f s`` SUBST1_TAC
1779 THENL [ASM_SIMP_TAC std_ss [support, MULT_EQ_0, NEUTRAL_ADD], ALL_TAC] THEN
1780 COND_CASES_TAC THEN REWRITE_TAC[NEUTRAL_ADD, MULT_CLAUSES] THEN
1781 POP_ASSUM MP_TAC THEN
1782 SPEC_TAC(``support (+) f (s:'a->bool)``,``t:'a->bool``) THEN
1783 REWRITE_TAC[GSYM nsum] THEN Q.ABBREV_TAC `ss = support $+ f s` THEN
1784 KNOW_TAC ``((nsum ss (\x. c * f x) = c * nsum ss f) =
1785 (\ss. (nsum ss (\x. c * f x) = c * nsum ss f)) ss)`` THENL
1786 [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISCH_TAC THEN
1787 ONCE_ASM_REWRITE_TAC [] THEN HO_MATCH_MP_TAC FINITE_INDUCT THEN
1788 BETA_TAC THEN SIMP_TAC std_ss [NSUM_CLAUSES, MULT_CLAUSES, LEFT_ADD_DISTRIB]
1789QED
1790
1791Theorem NSUM_RMUL:
1792 !f c s:'a->bool. nsum s (\x. f(x) * c) = nsum s f * c
1793Proof
1794 ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[NSUM_LMUL]
1795QED
1796
1797Theorem NSUM_LE:
1798 !f g s. FINITE(s) /\ (!x. x IN s ==> f(x) <= g(x))
1799 ==> nsum s f <= nsum s g
1800Proof
1801 ONCE_REWRITE_TAC[GSYM AND_IMP_INTRO] THEN REPEAT GEN_TAC THEN
1802 KNOW_TAC ``((!x. x IN s ==> f x <= g x) ==> nsum s f <= nsum s g) =
1803 (\s. (!x. x IN s ==> f x <= g x) ==> nsum s f <= nsum s g) s`` THENL
1804 [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISCH_TAC THEN ONCE_ASM_REWRITE_TAC []
1805 THEN MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
1806 SIMP_TAC std_ss [NSUM_CLAUSES, LESS_EQ_REFL, LESS_EQ_LESS_EQ_MONO, IN_INSERT]
1807QED
1808
1809Theorem NSUM_LT:
1810 !f g s:'a->bool.
1811 FINITE(s) /\ (!x. x IN s ==> f(x) <= g(x)) /\
1812 (?x. x IN s /\ f(x) < g(x))
1813 ==> nsum s f < nsum s g
1814Proof
1815 REPEAT GEN_TAC THEN
1816 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1817 DISCH_THEN(X_CHOOSE_THEN ``a:'a`` STRIP_ASSUME_TAC) THEN
1818 SUBGOAL_THEN ``s = (a:'a) INSERT (s DELETE a)`` SUBST1_TAC THENL
1819 [UNDISCH_TAC ``a:'a IN s`` THEN SET_TAC[], ALL_TAC] THEN
1820 ASM_SIMP_TAC std_ss [NSUM_CLAUSES, FINITE_DELETE, IN_DELETE] THEN
1821 ASM_SIMP_TAC std_ss [ARITH_PROVE ``m < p /\ n <= q ==> m + n < p + q:num``,
1822 NSUM_LE, IN_DELETE, FINITE_DELETE]
1823QED
1824
1825Theorem NSUM_LT_ALL:
1826 !f g s. FINITE s /\ ~(s = {}) /\ (!x. x IN s ==> f(x) < g(x))
1827 ==> nsum s f < nsum s g
1828Proof
1829 MESON_TAC[MEMBER_NOT_EMPTY, LESS_IMP_LESS_OR_EQ, NSUM_LT]
1830QED
1831
1832Theorem NSUM_EQ:
1833 !f g s. (!x. x IN s ==> (f x = g x)) ==> (nsum s f = nsum s g)
1834Proof
1835 REWRITE_TAC[nsum] THEN
1836 MATCH_MP_TAC ITERATE_EQ THEN REWRITE_TAC[MONOIDAL_ADD]
1837QED
1838
1839Theorem NSUM_CONST:
1840 !c s. FINITE s ==> (nsum s (\n. c) = (CARD s) * c)
1841Proof
1842 REPEAT GEN_TAC THEN KNOW_TAC ``(nsum s (\n. c) = CARD s * c) =
1843 (\s. (nsum s (\n. c) = CARD s * c)) s ``
1844 THENL [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISCH_TAC THEN
1845 ONCE_ASM_REWRITE_TAC [] THEN MATCH_MP_TAC FINITE_INDUCT THEN
1846 BETA_TAC THEN SIMP_TAC std_ss [NSUM_CLAUSES, CARD_DEF] THEN
1847 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [ADD1, RIGHT_ADD_DISTRIB]
1848 THEN ARITH_TAC
1849QED
1850
1851Theorem NSUM_POS_BOUND:
1852 !f b s. FINITE s /\ nsum s f <= b ==> !x:'a. x IN s ==> f x <= b
1853Proof
1854 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM AND_IMP_INTRO] THEN
1855 KNOW_TAC ``(nsum s f <= b ==> !x. x IN s ==> f x <= b) =
1856 (\s. nsum s f <= b ==> !x. x IN s ==> f x <= b) s`` THENL
1857 [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISCH_TAC THEN
1858 ONCE_ASM_REWRITE_TAC [] THEN MATCH_MP_TAC FINITE_INDUCT THEN
1859 BETA_TAC THEN SIMP_TAC std_ss [NSUM_CLAUSES, NOT_IN_EMPTY, IN_INSERT]
1860 THEN MESON_TAC[ZERO_LESS_EQ, ARITH_PROVE
1861 ``0:num <= x /\ 0:num <= y /\ x + y <= b ==> x <= b /\ y <= b``]
1862QED
1863
1864Theorem NSUM_EQ_0_IFF:
1865 !s. FINITE s ==> ((nsum s f = 0:num) <=> !x. x IN s ==> (f x = 0:num))
1866Proof
1867 REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC std_ss [NSUM_EQ_0] THEN
1868 ASM_MESON_TAC[LESS_EQ_0, NSUM_POS_BOUND]
1869QED
1870
1871Theorem NSUM_POS_LT:
1872 !f s:'a->bool.
1873 FINITE s /\ (?x. x IN s /\ 0:num < f x)
1874 ==> 0:num < nsum s f
1875Proof
1876 SIMP_TAC std_ss [ARITH_PROVE ``0:num < n <=> ~(n = 0:num)``, NSUM_EQ_0_IFF]
1877 THEN MESON_TAC[]
1878QED
1879
1880Theorem NSUM_POS_LT_ALL:
1881 !s f:'a->num.
1882 FINITE s /\ ~(s = {}) /\ (!i. i IN s ==> 0:num < f i) ==> 0:num < nsum s f
1883Proof
1884 REPEAT STRIP_TAC THEN MATCH_MP_TAC NSUM_POS_LT THEN
1885 ASM_MESON_TAC[MEMBER_NOT_EMPTY]
1886QED
1887
1888Theorem NSUM_DELETE:
1889 !f s a. FINITE s /\ a IN s ==> (f(a) + nsum(s DELETE a) f = nsum s f)
1890Proof
1891 SIMP_TAC std_ss [nsum, ITERATE_DELETE, MONOIDAL_ADD]
1892QED
1893
1894Theorem NSUM_SING:
1895 !f x. nsum {x} f = f(x)
1896Proof
1897 SIMP_TAC std_ss [NSUM_CLAUSES, FINITE_EMPTY, FINITE_INSERT,
1898 NOT_IN_EMPTY, ADD_CLAUSES]
1899QED
1900
1901Theorem NSUM_DELTA:
1902 !s a. nsum s (\x. if x = a:'a then b else 0:num) = if a IN s then b else 0:num
1903Proof
1904 REWRITE_TAC[nsum, GSYM NEUTRAL_ADD] THEN
1905 SIMP_TAC std_ss [ITERATE_DELTA, MONOIDAL_ADD]
1906QED
1907
1908Theorem NSUM_SWAP:
1909 !f:'a->'b->num s t.
1910 FINITE(s) /\ FINITE(t)
1911 ==> (nsum s (\i. nsum t (f i)) = nsum t (\j. nsum s (\i. f i j)))
1912Proof
1913 GEN_TAC THEN SIMP_TAC std_ss [GSYM AND_IMP_INTRO, RIGHT_FORALL_IMP_THM] THEN
1914 GEN_TAC THEN KNOW_TAC ``( !t. FINITE t ==>
1915 (nsum s (\i. nsum t (f i)) = nsum t (\j. nsum s (\i. (f:'a->'b->num) i j)))) =
1916 (\s. !t. FINITE t ==>
1917 (nsum s (\i. nsum t (f i)) = nsum t (\j. nsum s (\i. (f:'a->'b->num) i j)))) s`` THENL
1918 [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISCH_TAC THEN ONCE_ASM_REWRITE_TAC []
1919 THEN MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
1920 SIMP_TAC std_ss [NSUM_CLAUSES, NSUM_0, NSUM_ADD, ETA_AX] THEN METIS_TAC []
1921QED
1922
1923Theorem NSUM_IMAGE:
1924 !f g s. (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))
1925 ==> (nsum (IMAGE f s) g = nsum s (g o f))
1926Proof
1927 REWRITE_TAC[nsum, GSYM NEUTRAL_ADD] THEN
1928 MATCH_MP_TAC ITERATE_IMAGE THEN REWRITE_TAC[MONOIDAL_ADD]
1929QED
1930
1931Theorem NSUM_SUPERSET:
1932 !f:'a->num u v.
1933 u SUBSET v /\ (!x. x IN v /\ ~(x IN u) ==> (f(x) = 0:num))
1934 ==> (nsum v f = nsum u f)
1935Proof
1936 SIMP_TAC std_ss [nsum, GSYM NEUTRAL_ADD, ITERATE_SUPERSET, MONOIDAL_ADD]
1937QED
1938
1939Theorem NSUM_UNION_RZERO:
1940 !f:'a->num u v.
1941 FINITE u /\ (!x. x IN v /\ ~(x IN u) ==> (f(x) = 0:num))
1942 ==> (nsum (u UNION v) f = nsum u f)
1943Proof
1944 REPEAT STRIP_TAC THEN
1945 ONCE_REWRITE_TAC [SET_RULE ``u UNION v = u UNION (v DIFF u)``] THEN
1946 MATCH_MP_TAC NSUM_SUPERSET THEN ASM_MESON_TAC[IN_UNION, IN_DIFF, SUBSET_DEF]
1947QED
1948
1949Theorem NSUM_UNION_LZERO:
1950 !f:'a->num u v.
1951 FINITE v /\ (!x. x IN u /\ ~(x IN v) ==> (f(x) = 0:num))
1952 ==> (nsum (u UNION v) f = nsum v f)
1953Proof
1954 MESON_TAC[NSUM_UNION_RZERO, UNION_COMM]
1955QED
1956
1957Theorem NSUM_RESTRICT:
1958 !f s. FINITE s ==> (nsum s (\x. if x IN s then f(x) else 0:num) = nsum s f)
1959Proof
1960 REPEAT STRIP_TAC THEN MATCH_MP_TAC NSUM_EQ THEN ASM_SIMP_TAC std_ss []
1961QED
1962
1963Theorem NSUM_BOUND:
1964 !s f b. FINITE s /\ (!x:'a. x IN s ==> f(x) <= b)
1965 ==> nsum s f <= (CARD s) * b
1966Proof
1967 SIMP_TAC std_ss [GSYM NSUM_CONST, NSUM_LE]
1968QED
1969
1970Theorem NSUM_BOUND_GEN:
1971 !s f b. FINITE s /\ ~(s = {}) /\ (!x:'a. x IN s ==> f(x) <= b DIV (CARD s))
1972 ==> nsum s f <= b
1973Proof
1974 REPEAT STRIP_TAC THEN KNOW_TAC ``0 < CARD s`` THENL
1975 [METIS_TAC [CARD_EQ_0, NOT_ZERO_LT_ZERO], ALL_TAC] THEN
1976 STRIP_TAC THEN FULL_SIMP_TAC std_ss [X_LE_DIV] THEN
1977 SUBGOAL_THEN ``nsum s (\x. CARD(s:'a->bool) * f x) <= CARD s * b`` MP_TAC THENL
1978 [ASM_SIMP_TAC arith_ss [NSUM_BOUND],
1979 ASM_SIMP_TAC std_ss [NSUM_LMUL, LE_MULT_LCANCEL, CARD_EQ_0]]
1980QED
1981
1982Theorem NSUM_BOUND_LT:
1983 !s f b. FINITE s /\ (!x:'a. x IN s ==> f x <= b) /\ (?x. x IN s /\ f x < b)
1984 ==> nsum s f < (CARD s) * b
1985Proof
1986 REPEAT STRIP_TAC THEN MATCH_MP_TAC LESS_LESS_EQ_TRANS THEN
1987 EXISTS_TAC ``nsum s (\x:'a. b)`` THEN CONJ_TAC THENL
1988 [MATCH_MP_TAC NSUM_LT THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[],
1989 ASM_SIMP_TAC std_ss [NSUM_CONST, LESS_EQ_REFL]]
1990QED
1991
1992Theorem NSUM_BOUND_LT_ALL:
1993 !s f b. FINITE s /\ ~(s = {}) /\ (!x. x IN s ==> f(x) < b)
1994 ==> nsum s f < (CARD s) * b
1995Proof
1996 MESON_TAC[MEMBER_NOT_EMPTY, LESS_IMP_LESS_OR_EQ, NSUM_BOUND_LT]
1997QED
1998
1999Theorem NSUM_BOUND_LT_GEN:
2000 !s f b. FINITE s /\ ~(s = {}) /\ (!x:'a. x IN s ==> f(x) < b DIV (CARD s))
2001 ==> nsum s f < b
2002Proof
2003 REPEAT STRIP_TAC THEN MATCH_MP_TAC LESS_LESS_EQ_TRANS THEN
2004 EXISTS_TAC ``nsum (s:'a->bool) (\a. f(a) + 1:num)`` THEN CONJ_TAC THENL
2005 [MATCH_MP_TAC NSUM_LT_ALL THEN ASM_SIMP_TAC std_ss [] THEN ARITH_TAC,
2006 MATCH_MP_TAC NSUM_BOUND_GEN THEN
2007 ASM_SIMP_TAC std_ss [ARITH_PROVE ``a + 1:num <= b <=> a < b``]]
2008QED
2009
2010Theorem NSUM_UNION_EQ:
2011 !s t u. FINITE u /\ (s INTER t = {}) /\ (s UNION t = u)
2012 ==> (nsum s f + nsum t f = nsum u f)
2013Proof
2014 MESON_TAC[NSUM_UNION, DISJOINT_DEF, SUBSET_FINITE, SUBSET_UNION]
2015QED
2016
2017Theorem NSUM_EQ_SUPERSET:
2018 !f s t:'a->bool.
2019 FINITE t /\ t SUBSET s /\
2020 (!x. x IN t ==> (f x = g x)) /\
2021 (!x. x IN s /\ ~(x IN t) ==> (f(x) = 0:num))
2022 ==> (nsum s f = nsum t g)
2023Proof
2024 MESON_TAC[NSUM_SUPERSET, NSUM_EQ]
2025QED
2026
2027Theorem NSUM_RESTRICT_SET:
2028 !P s f. nsum {x:'a | x IN s /\ P x} f = nsum s (\x. if P x then f(x) else 0:num)
2029Proof
2030 ONCE_REWRITE_TAC[GSYM NSUM_SUPPORT] THEN
2031 SIMP_TAC std_ss [support, NEUTRAL_ADD, GSPECIFICATION] THEN
2032 REWRITE_TAC[METIS []``~((if P x then f x else a) = a) <=> P x /\ ~(f x = a)``,
2033 GSYM CONJ_ASSOC] THEN
2034 REPEAT GEN_TAC THEN MATCH_MP_TAC NSUM_EQ THEN SIMP_TAC std_ss [GSPECIFICATION]
2035QED
2036
2037Theorem NSUM_NSUM_RESTRICT:
2038 !R f s t.
2039 FINITE s /\ FINITE t
2040 ==> (nsum s (\x. nsum {y | y IN t /\ R x y} (\y. f x y)) =
2041 nsum t (\y. nsum {x | x IN s /\ R x y} (\x. f x y)))
2042Proof
2043 REPEAT GEN_TAC THEN SIMP_TAC std_ss [NSUM_RESTRICT_SET] THEN
2044 ASSUME_TAC NSUM_SWAP THEN POP_ASSUM (MP_TAC o Q.SPECL
2045 [`(\x y. if R x y then f x y else 0)`,`s`, `t`]) THEN
2046 FULL_SIMP_TAC std_ss []
2047QED
2048
2049Theorem CARD_EQ_NSUM:
2050 !s. FINITE s ==> ((CARD s) = nsum s (\x. 1:num))
2051Proof
2052 SIMP_TAC std_ss [NSUM_CONST, MULT_CLAUSES]
2053QED
2054
2055Theorem NSUM_MULTICOUNT_GEN:
2056 !R:'a->'b->bool s t k.
2057 FINITE s /\ FINITE t /\
2058 (!j. j IN t ==> (CARD {i | i IN s /\ R i j} = k(j)))
2059 ==> (nsum s (\i. (CARD {j | j IN t /\ R i j})) =
2060 nsum t (\i. (k i)))
2061Proof
2062 REPEAT GEN_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN
2063 DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
2064 MATCH_MP_TAC EQ_TRANS THEN
2065 EXISTS_TAC ``nsum s (\i:'a. nsum {j:'b | j IN t /\ R i j} (\j. 1:num))`` THEN
2066 CONJ_TAC THENL
2067 [MATCH_MP_TAC NSUM_EQ THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
2068 ASM_SIMP_TAC std_ss [CARD_EQ_NSUM, FINITE_RESTRICT],
2069 ASSUME_TAC NSUM_NSUM_RESTRICT THEN POP_ASSUM (MP_TAC o Q.SPEC `R`)
2070 THEN FULL_SIMP_TAC std_ss [] THEN DISCH_TAC THEN MATCH_MP_TAC NSUM_EQ
2071 THEN ASM_SIMP_TAC std_ss [NSUM_CONST, FINITE_RESTRICT] THEN
2072 REWRITE_TAC[MULT_CLAUSES]]
2073QED
2074
2075Theorem NSUM_MULTICOUNT:
2076 !R:'a->'b->bool s t k.
2077 FINITE s /\ FINITE t /\
2078 (!j. j IN t ==> (CARD {i | i IN s /\ R i j} = k))
2079 ==> (nsum s (\i. (CARD {j | j IN t /\ R i j})) = (k * CARD t))
2080Proof
2081 REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
2082 EXISTS_TAC ``nsum t (\i:'b. k)`` THEN CONJ_TAC THENL
2083 [KNOW_TAC ``?j. !i:'b. &k = &(j i):num`` THENL
2084 [EXISTS_TAC ``(\i:'b. k:num)`` THEN METIS_TAC [], ALL_TAC] THEN
2085 STRIP_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
2086 MATCH_MP_TAC NSUM_MULTICOUNT_GEN THEN FULL_SIMP_TAC std_ss [],
2087 ASM_SIMP_TAC std_ss [NSUM_CONST] THEN ARITH_TAC]
2088QED
2089
2090Theorem NSUM_IMAGE_GEN:
2091 !f:'a->'b g s.
2092 FINITE s
2093 ==> (nsum s g =
2094 nsum (IMAGE f s) (\y. nsum {x | x IN s /\ (f(x) = y)} g))
2095Proof
2096 REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
2097 ``nsum s (\x:'a. nsum {y:'b | y IN IMAGE f s /\ (f x = y)} (\y. g x))`` THEN
2098 CONJ_TAC THENL
2099 [MATCH_MP_TAC NSUM_EQ THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC ``x:'a`` THEN
2100 DISCH_TAC THEN BETA_TAC THEN
2101 SUBGOAL_THEN ``{y | y IN IMAGE (f:'a->'b) s /\ (f x = y)} = {(f x)}``
2102 (fn th => REWRITE_TAC[th, NSUM_SING, o_THM]) THEN
2103 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, IN_SING, IN_IMAGE] THEN
2104 ASM_MESON_TAC[],
2105 GEN_REWR_TAC (funpow 2 RAND_CONV o ABS_CONV o RAND_CONV)
2106 [GSYM ETA_AX] THEN KNOW_TAC ``FINITE (IMAGE (f:'a->'b) s)`` THENL
2107 [METIS_TAC [IMAGE_FINITE], ALL_TAC] THEN DISCH_TAC THEN
2108 ASSUME_TAC NSUM_NSUM_RESTRICT THEN
2109 POP_ASSUM (MP_TAC o Q.SPEC `(\x y. f x = y)`) THEN
2110 FULL_SIMP_TAC std_ss []]
2111QED
2112
2113Theorem NSUM_GROUP:
2114 !f:'a->'b g s t.
2115 FINITE s /\ IMAGE f s SUBSET t
2116 ==> (nsum t (\y. nsum {x | x IN s /\ (f(x) = y)} g) = nsum s g)
2117Proof
2118 REPEAT STRIP_TAC THEN
2119 MP_TAC(ISPECL [``f:'a->'b``, ``g:'a->num``, ``s:'a->bool``] NSUM_IMAGE_GEN) THEN
2120 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
2121 MATCH_MP_TAC NSUM_SUPERSET THEN ASM_REWRITE_TAC[] THEN
2122 REPEAT STRIP_TAC THEN BETA_TAC THEN MATCH_MP_TAC NSUM_EQ_0 THEN
2123 FULL_SIMP_TAC std_ss [GSPECIFICATION, IN_IMAGE] THEN METIS_TAC []
2124QED
2125
2126Theorem NSUM_SUBSET:
2127 !u v f. FINITE u /\ FINITE v /\ (!x:'a. x IN (u DIFF v) ==> (f(x) = 0:num))
2128 ==> nsum u f <= nsum v f
2129Proof
2130 REPEAT STRIP_TAC THEN
2131 MP_TAC(ISPECL [``f:'a->num``, ``u INTER v :'a->bool``] NSUM_UNION) THEN
2132 DISCH_THEN(fn th => MP_TAC(SPEC ``v DIFF u :'a->bool`` th) THEN
2133 MP_TAC(SPEC ``u DIFF v :'a->bool`` th)) THEN
2134 REWRITE_TAC[SET_RULE ``(u INTER v) UNION (u DIFF v) = u``,
2135 SET_RULE ``(u INTER v) UNION (v DIFF u) = v``] THEN
2136 ASM_SIMP_TAC std_ss [FINITE_DIFF, FINITE_INTER] THEN
2137 KNOW_TAC ``DISJOINT (u INTER v) (u DIFF v) /\ DISJOINT (u INTER v) (v DIFF u)``
2138 THENL [SET_TAC[], ALL_TAC] THEN RW_TAC std_ss [] THEN
2139 ASM_SIMP_TAC std_ss [NSUM_EQ_0]
2140QED
2141
2142Theorem NSUM_SUBSET_SIMPLE:
2143 !u v f. FINITE v /\ u SUBSET v ==> nsum u f <= nsum v f
2144Proof
2145 REPEAT STRIP_TAC THEN MATCH_MP_TAC NSUM_SUBSET THEN
2146 ASM_MESON_TAC[IN_DIFF, SUBSET_DEF, SUBSET_FINITE]
2147QED
2148
2149Theorem NSUM_LE_GEN:
2150 !f g s. (!x:'a. x IN s ==> f x <= g x) /\ FINITE {x | x IN s /\ ~(g x = 0:num)}
2151 ==> nsum s f <= nsum s g
2152Proof
2153 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM NSUM_SUPPORT] THEN
2154 REWRITE_TAC[support, NEUTRAL_ADD] THEN
2155 MATCH_MP_TAC LESS_EQ_TRANS THEN
2156 EXISTS_TAC ``nsum {x | x IN s /\ ~(g(x:'a) = 0:num)} f`` THEN
2157 CONJ_TAC THENL
2158 [MATCH_MP_TAC NSUM_SUBSET THEN
2159 ASM_SIMP_TAC std_ss [GSPECIFICATION, IN_DIFF] THEN
2160 CONJ_TAC THENL [ALL_TAC, ASM_MESON_TAC[LE]] THEN
2161 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[GSYM AND_IMP_INTRO]
2162 SUBSET_FINITE)) THEN
2163 SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION] THEN ASM_MESON_TAC[LE],
2164 MATCH_MP_TAC NSUM_LE THEN ASM_SIMP_TAC std_ss [GSPECIFICATION]]
2165QED
2166
2167Theorem NSUM_IMAGE_NONZERO:
2168 !d:'b->num i:'a->'b s.
2169 FINITE s /\
2170 (!x y. x IN s /\ y IN s /\ ~(x = y) /\ (i x = i y) ==> (d(i x) = 0:num))
2171 ==> (nsum (IMAGE i s) d = nsum s (d o i))
2172Proof
2173 REWRITE_TAC[GSYM NEUTRAL_ADD, nsum] THEN
2174 MATCH_MP_TAC ITERATE_IMAGE_NONZERO THEN REWRITE_TAC[MONOIDAL_ADD]
2175QED
2176
2177Theorem NSUM_BIJECTION:
2178 !f p s:'a->bool.
2179 (!x. x IN s ==> p(x) IN s) /\
2180 (!y. y IN s ==> ?!x. x IN s /\ (p(x) = y))
2181 ==> (nsum s f = nsum s (f o p))
2182Proof
2183 REWRITE_TAC[nsum] THEN MATCH_MP_TAC ITERATE_BIJECTION THEN
2184 REWRITE_TAC[MONOIDAL_ADD]
2185QED
2186
2187Theorem NSUM_NSUM_PRODUCT:
2188 !s:'a->bool t:'a->'b->bool x.
2189 FINITE s /\ (!i. i IN s ==> FINITE(t i))
2190 ==> (nsum s (\i. nsum (t i) (x i)) =
2191 nsum {i,j | i IN s /\ j IN t i} (\(i,j). x i j))
2192Proof
2193 REWRITE_TAC[nsum] THEN MATCH_MP_TAC ITERATE_ITERATE_PRODUCT THEN
2194 REWRITE_TAC[MONOIDAL_ADD]
2195QED
2196
2197Theorem NSUM_EQ_GENERAL:
2198 !s:'a->bool t:'b->bool f g h.
2199 (!y. y IN t ==> ?!x. x IN s /\ (h(x) = y)) /\
2200 (!x. x IN s ==> h(x) IN t /\ (g(h x) = f x))
2201 ==> (nsum s f = nsum t g)
2202Proof
2203 REWRITE_TAC[nsum] THEN MATCH_MP_TAC ITERATE_EQ_GENERAL THEN
2204 REWRITE_TAC[MONOIDAL_ADD]
2205QED
2206
2207Theorem NSUM_EQ_GENERAL_INVERSES:
2208 !s:'a->bool t:'b->bool f g h k.
2209 (!y. y IN t ==> k(y) IN s /\ (h(k y) = y)) /\
2210 (!x. x IN s ==> h(x) IN t /\ (k(h x) = x) /\ (g(h x) = f x))
2211 ==> (nsum s f = nsum t g)
2212Proof
2213 REWRITE_TAC[nsum] THEN MATCH_MP_TAC ITERATE_EQ_GENERAL_INVERSES THEN
2214 REWRITE_TAC[MONOIDAL_ADD]
2215QED
2216
2217Theorem NSUM_INJECTION:
2218 !f p s. FINITE s /\
2219 (!x. x IN s ==> p x IN s) /\
2220 (!x y. x IN s /\ y IN s /\ (p x = p y) ==> (x = y))
2221 ==> (nsum s (f o p) = nsum s f)
2222Proof
2223 REWRITE_TAC[nsum] THEN MATCH_MP_TAC ITERATE_INJECTION THEN
2224 REWRITE_TAC[MONOIDAL_ADD]
2225QED
2226
2227Theorem NSUM_UNION_NONZERO:
2228 !f s t. FINITE s /\ FINITE t /\ (!x. x IN s INTER t ==> (f(x) = 0:num))
2229 ==> (nsum (s UNION t) f = nsum s f + nsum t f)
2230Proof
2231 REWRITE_TAC[nsum, GSYM NEUTRAL_ADD] THEN
2232 MATCH_MP_TAC ITERATE_UNION_NONZERO THEN REWRITE_TAC[MONOIDAL_ADD]
2233QED
2234
2235Theorem NSUM_BIGUNION_NONZERO:
2236 !f s. FINITE s /\ (!t:'a->bool. t IN s ==> FINITE t) /\
2237 (!t1 t2 x. t1 IN s /\ t2 IN s /\ ~(t1 = t2) /\ x IN t1 /\ x IN t2
2238 ==> (f x = 0))
2239 ==> (nsum (BIGUNION s) f = nsum s (\t. nsum t f))
2240Proof
2241 GEN_TAC THEN ONCE_REWRITE_TAC[GSYM AND_IMP_INTRO] THEN GEN_TAC THEN
2242 KNOW_TAC ``((!(t:'a->bool). t IN s ==> FINITE t) /\
2243 (!t1 t2 x.
2244 t1 IN s /\ t2 IN s /\ t1 <> t2 /\ x IN t1 /\ x IN t2 ==>
2245 (f x = 0)) ==>
2246 (nsum (BIGUNION s) f = nsum s (\t. nsum t f))) =
2247 (\s. (!(t:'a->bool). t IN s ==> FINITE t) /\
2248 (!t1 t2 x.
2249 t1 IN s /\ t2 IN s /\ t1 <> t2 /\ x IN t1 /\ x IN t2 ==>
2250 (f x = 0)) ==>
2251 (nsum (BIGUNION s) f = nsum s (\t. nsum t f))) s `` THENL
2252 [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISCH_TAC THEN
2253 ONCE_ASM_REWRITE_TAC [] THEN MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2254 REWRITE_TAC[BIGUNION_EMPTY, BIGUNION_INSERT, NSUM_CLAUSES, IN_INSERT] THEN
2255 SIMP_TAC std_ss [GSYM RIGHT_FORALL_IMP_THM] THEN
2256 MAP_EVERY X_GEN_TAC [``(s':('a->bool)->bool)``, ``t:'a->bool``] THEN
2257 DISCH_THEN(fn th => STRIP_TAC THEN MP_TAC th) THEN REPEAT STRIP_TAC THEN
2258 UNDISCH_TAC ``FINITE (s':('a->bool)->bool)`` THEN
2259 UNDISCH_TAC ``(t :'a -> bool) NOTIN (s' :('a -> bool) -> bool) `` THEN
2260 ONCE_REWRITE_TAC[AND_IMP_INTRO] THEN ASM_SIMP_TAC std_ss [NSUM_CLAUSES]
2261 THEN KNOW_TAC ``nsum (BIGUNION s') f = nsum s' (\t. nsum t f)`` THENL
2262 [METIS_TAC [], ALL_TAC] THEN GEN_REWR_TAC (LAND_CONV) [EQ_SYM_EQ]
2263 THEN DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
2264 STRIP_TAC THEN MATCH_MP_TAC NSUM_UNION_NONZERO THEN
2265 ASM_SIMP_TAC std_ss [FINITE_BIGUNION, IN_INTER, IN_BIGUNION] THEN
2266 ASM_MESON_TAC[]
2267QED
2268
2269Theorem NSUM_CASES:
2270 !s P f g. FINITE s
2271 ==> (nsum s (\x:'a. if P x then f x else g x) =
2272 nsum {x | x IN s /\ P x} f + nsum {x | x IN s /\ ~P x} g)
2273Proof
2274 REWRITE_TAC[nsum, GSYM NEUTRAL_ADD] THEN
2275 MATCH_MP_TAC ITERATE_CASES THEN REWRITE_TAC[MONOIDAL_ADD]
2276QED
2277
2278Theorem NSUM_CLOSED:
2279 !P f:'a->num s.
2280 P(0) /\ (!x y. P x /\ P y ==> P(x + y)) /\ (!a. a IN s ==> P(f a))
2281 ==> P(nsum s f)
2282Proof
2283 REPEAT STRIP_TAC THEN MP_TAC(MATCH_MP ITERATE_CLOSED MONOIDAL_ADD) THEN
2284 DISCH_THEN(MP_TAC o SPEC ``P:num->bool``) THEN
2285 ASM_SIMP_TAC std_ss [NEUTRAL_ADD, GSYM nsum]
2286QED
2287
2288Theorem NSUM_ADD_NUMSEG:
2289 !f g m n. nsum{m..n} (\i. f(i) + g(i)) = nsum{m..n} f + nsum{m..n} g
2290Proof
2291 SIMP_TAC std_ss [NSUM_ADD, FINITE_NUMSEG]
2292QED
2293
2294Theorem NSUM_LE_NUMSEG:
2295 !f g m n. (!i. m <= i /\ i <= n ==> f(i) <= g(i))
2296 ==> nsum{m..n} f <= nsum{m..n} g
2297Proof
2298 SIMP_TAC std_ss [NSUM_LE, FINITE_NUMSEG, IN_NUMSEG]
2299QED
2300
2301Theorem NSUM_EQ_NUMSEG:
2302 !f g m n. (!i. m <= i /\ i <= n ==> (f(i) = g(i)))
2303 ==> (nsum{m..n} f = nsum{m..n} g)
2304Proof
2305 MESON_TAC[NSUM_EQ, FINITE_NUMSEG, IN_NUMSEG]
2306QED
2307
2308Theorem NSUM_CONST_NUMSEG:
2309 !c m n. nsum{m..n} (\n. c) = ((n + 1:num) - m) * c
2310Proof
2311 SIMP_TAC std_ss [NSUM_CONST, FINITE_NUMSEG, CARD_NUMSEG]
2312QED
2313
2314Theorem NSUM_EQ_0_NUMSEG:
2315 !f m n. (!i. m <= i /\ i <= n ==> (f(i) = 0:num)) ==> (nsum{m..n} f = 0:num)
2316Proof
2317 SIMP_TAC std_ss [NSUM_EQ_0, IN_NUMSEG]
2318QED
2319
2320Theorem NSUM_EQ_0_IFF_NUMSEG:
2321 !f m n. (nsum {m..n} f = 0:num) <=> !i. m <= i /\ i <= n ==> (f i = 0:num)
2322Proof
2323 SIMP_TAC std_ss [NSUM_EQ_0_IFF, FINITE_NUMSEG, IN_NUMSEG]
2324QED
2325
2326Theorem NSUM_TRIV_NUMSEG:
2327 !f m n. n < m ==> (nsum{m..n} f = 0:num)
2328Proof
2329 MESON_TAC[NSUM_EQ_0_NUMSEG, LESS_EQ_TRANS, NOT_LESS]
2330QED
2331
2332Theorem NSUM_SING_NUMSEG:
2333 !f n. nsum{n..n} f = f(n)
2334Proof
2335 SIMP_TAC std_ss [NSUM_SING, NUMSEG_SING]
2336QED
2337
2338Theorem NSUM_CLAUSES_NUMSEG:
2339 (!m. nsum{m..0} f = if m = 0:num then f 0 else 0) /\
2340 (!m n. nsum{m..SUC n} f = if m <= SUC n then nsum{m..n} f + f(SUC n)
2341 else nsum{m..n} f)
2342Proof
2343 MP_TAC(MATCH_MP ITERATE_CLAUSES_NUMSEG MONOIDAL_ADD) THEN
2344 REWRITE_TAC[NEUTRAL_ADD, nsum]
2345QED
2346
2347Theorem NSUM_SWAP_NUMSEG:
2348 !a b c d f.
2349 nsum{a..b} (\i. nsum{c..d} (f i)) =
2350 nsum{c..d} (\j. nsum{a..b} (\i. f i j))
2351Proof
2352 REPEAT GEN_TAC THEN MATCH_MP_TAC NSUM_SWAP THEN REWRITE_TAC[FINITE_NUMSEG]
2353QED
2354
2355Theorem NSUM_ADD_SPLIT:
2356 !f m n p.
2357 m <= n + 1:num ==> (nsum {m..n+p} f = nsum{m..n} f + nsum{n+1..n+p} f)
2358Proof
2359 METIS_TAC [NUMSEG_ADD_SPLIT, NSUM_UNION, DISJOINT_NUMSEG, FINITE_NUMSEG,
2360 ARITH_PROVE ``x:num < x + 1:num``]
2361QED
2362
2363Theorem NSUM_OFFSET:
2364 !p f m n. nsum{m+p..n+p} f = nsum{m..n} (\i. f(i + p))
2365Proof
2366 SIMP_TAC std_ss [NUMSEG_OFFSET_IMAGE, NSUM_IMAGE, EQ_ADD_RCANCEL, FINITE_NUMSEG] THEN
2367 SIMP_TAC std_ss [o_DEF]
2368QED
2369
2370Theorem NSUM_OFFSET_0:
2371 !f m n. m <= n ==> (nsum{m..n} f = nsum{0..n-m} (\i. f(i + m)))
2372Proof
2373 SIMP_TAC std_ss [GSYM NSUM_OFFSET, ADD_CLAUSES, SUB_ADD]
2374QED
2375
2376Theorem NSUM_CLAUSES_LEFT:
2377 !f m n. m <= n ==> (nsum{m..n} f = f(m) + nsum{m+1..n} f)
2378Proof
2379 SIMP_TAC std_ss [GSYM NUMSEG_LREC, NSUM_CLAUSES, FINITE_NUMSEG, IN_NUMSEG] THEN
2380 ARITH_TAC
2381QED
2382
2383Theorem NSUM_CLAUSES_RIGHT:
2384 !f m n. 0:num < n /\ m <= n ==> (nsum{m..n} f = nsum{m..n-1} f + f(n))
2385Proof
2386 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
2387 SIMP_TAC std_ss [LESS_REFL, NSUM_CLAUSES_NUMSEG, SUC_SUB1]
2388QED
2389
2390Theorem NSUM_PAIR:
2391 !f m n. nsum{2*m..2*n+1} f = nsum{m..n} (\i. f(2*i) + f(2*i+1:num))
2392Proof
2393 MP_TAC(MATCH_MP ITERATE_PAIR MONOIDAL_ADD) THEN
2394 REWRITE_TAC[nsum, NEUTRAL_ADD]
2395QED
2396
2397Theorem MOD_NSUM_MOD:
2398 !f:'a->num n s.
2399 FINITE s /\ ~(n = 0:num)
2400 ==> ((nsum s f) MOD n = nsum s (\i. f(i) MOD n) MOD n)
2401Proof
2402 GEN_TAC THEN GEN_TAC THEN
2403 ASM_CASES_TAC ``n = 0:num`` THEN ASM_REWRITE_TAC[] THEN
2404 GEN_TAC THEN KNOW_TAC ``(nsum s f MOD n = nsum s (\i. f i MOD n) MOD n) =
2405 (\s. (nsum s f MOD n = nsum s (\i. f i MOD n) MOD n))s``
2406 THENL [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISCH_TAC THEN
2407 ONCE_ASM_REWRITE_TAC [] THEN MATCH_MP_TAC FINITE_INDUCT THEN
2408 BETA_TAC THEN FULL_SIMP_TAC std_ss [NSUM_CLAUSES, NOT_ZERO_LT_ZERO] THEN
2409 REPEAT STRIP_TAC THEN ASSUME_TAC MOD_PLUS THEN
2410 POP_ASSUM (MP_TAC o Q.SPEC `n`) THEN FULL_SIMP_TAC std_ss [] THEN DISCH_TAC
2411 THEN POP_ASSUM (MP_TAC o Q.SPECL [`f e`, `nsum s f`]) THEN ASM_REWRITE_TAC []
2412 THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
2413 FULL_SIMP_TAC std_ss [MOD_PLUS, ADD_MOD]
2414QED
2415
2416Theorem MOD_NSUM_MOD_NUMSEG:
2417 !f a b n.
2418 ~(n = 0:num)
2419 ==> ((nsum{a..b} f) MOD n = nsum{a..b} (\i. f i MOD n) MOD n)
2420Proof
2421 METIS_TAC[MOD_NSUM_MOD, FINITE_NUMSEG]
2422QED
2423
2424Theorem NSUM_CONG:
2425 (!f g s. (!x. x IN s ==> (f(x) = g(x)))
2426 ==> (nsum s (\i. f(i)) = nsum s g)) /\
2427 (!f g a b. (!i. a <= i /\ i <= b ==> (f(i) = g(i)))
2428 ==> (nsum{a..b} (\i. f(i)) = nsum{a..b} g)) /\
2429 (!f g p. (!x. p x ==> (f x = g x))
2430 ==> (nsum {y | p y} (\i. f(i)) = nsum {y | p y} g))
2431Proof
2432 REPEAT STRIP_TAC
2433 >> MATCH_MP_TAC NSUM_EQ
2434 >> ASM_SIMP_TAC std_ss [GSPECIFICATION, IN_NUMSEG]
2435QED
2436
2437(* ------------------------------------------------------------------------- *)
2438(* Thanks to finite sums, we can express cardinality of finite union. *)
2439(* ------------------------------------------------------------------------- *)
2440
2441Theorem CARD_BIGUNION:
2442 !s:('a->bool)->bool.
2443 FINITE s /\ (!t. t IN s ==> FINITE t) /\
2444 (!t u. t IN s /\ u IN s /\ ~(t = u) ==> (t INTER u = {}))
2445 ==> (CARD(BIGUNION s) = nsum s CARD)
2446Proof
2447 ONCE_REWRITE_TAC[GSYM AND_IMP_INTRO] THEN GEN_TAC THEN
2448 KNOW_TAC ``((!t. t IN s ==> FINITE t) /\
2449 (!t u. t IN s /\ u IN s /\ t <> u ==> (t INTER u = {})) ==>
2450 (CARD (BIGUNION s) = nsum s CARD)) =
2451 (\s. (!t. t IN s ==> FINITE t) /\
2452 (!t u. t IN s /\ u IN s /\ t <> u ==> (t INTER u = {})) ==>
2453 (CARD (BIGUNION s) = nsum s CARD)) (s:('a->bool)->bool)`` THENL
2454 [FULL_SIMP_TAC std_ss [], DISC_RW_KILL THEN
2455 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2456 REWRITE_TAC[BIGUNION_EMPTY, BIGUNION_INSERT, NOT_IN_EMPTY, IN_INSERT] THEN
2457 REWRITE_TAC[CARD_DEF, NSUM_CLAUSES] THEN
2458 SIMP_TAC std_ss [GSYM RIGHT_FORALL_IMP_THM] THEN
2459 MAP_EVERY X_GEN_TAC [``f:('a->bool)->bool``, ``t:'a->bool``] THEN
2460 DISCH_THEN(fn th => STRIP_TAC THEN MP_TAC th) THEN
2461 ASM_SIMP_TAC std_ss [NSUM_CLAUSES] THEN REPEAT STRIP_TAC THEN
2462 FULL_SIMP_TAC std_ss [] THEN
2463 UNDISCH_TAC ``CARD (BIGUNION f) = nsum f CARD`` THEN
2464 GEN_REWR_TAC LAND_CONV [EQ_SYM_EQ] THEN RW_TAC std_ss [] THEN
2465 MATCH_MP_TAC (GSYM CARD_UNION_EQ) THEN FULL_SIMP_TAC std_ss [] THEN
2466 CONJ_TAC THENL [METIS_TAC [FINITE_BIGUNION, FINITE_UNION], ALL_TAC] THEN
2467 CONV_TAC SYM_CONV THEN
2468 KNOW_TAC ``(!s t. t INTER BIGUNION s = BIGUNION {t INTER x | x IN s})`` THENL
2469 [ONCE_REWRITE_TAC[EXTENSION] THEN
2470 SIMP_TAC std_ss [IN_BIGUNION, GSPECIFICATION, IN_INTER] THEN
2471 MESON_TAC[IN_INTER], ALL_TAC] THEN
2472 DISC_RW_KILL THEN
2473 SIMP_TAC std_ss [SET_RULE ``!s. (BIGUNION s = {}) <=> !t. t IN s ==> (t = {})``, GSPECIFICATION] THEN
2474 METIS_TAC[]]
2475QED
2476
2477(* ========================================================================= *)
2478(* Products of natural numbers and real numbers (productScript.sml) *)
2479(* ========================================================================= *)
2480
2481Definition nproduct :
2482 nproduct = iterate(( * ):num->num->num)
2483End
2484
2485Theorem NPRODUCT_CLAUSES:
2486 (!f. nproduct {} f = 1) /\
2487 (!x f s. FINITE(s)
2488 ==> (nproduct (x INSERT s) f =
2489 if x IN s then nproduct s f else f(x) * nproduct s f))
2490Proof
2491 REWRITE_TAC[nproduct, GSYM NEUTRAL_MUL] THEN
2492 METIS_TAC [SWAP_FORALL_THM, ITERATE_CLAUSES, MONOIDAL_MUL]
2493QED
2494
2495Theorem NPRODUCT_SUPPORT:
2496 !f s. nproduct (support ( * ) f s) f = nproduct s f
2497Proof
2498 REWRITE_TAC[nproduct, ITERATE_SUPPORT]
2499QED
2500
2501Theorem NPRODUCT_UNION:
2502 !f s t. FINITE s /\ FINITE t /\ DISJOINT s t
2503 ==> ((nproduct (s UNION t) f = nproduct s f * nproduct t f))
2504Proof
2505 SIMP_TAC std_ss [nproduct, ITERATE_UNION, MONOIDAL_MUL]
2506QED
2507
2508Theorem NPRODUCT_IMAGE:
2509 !f g s. (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))
2510 ==> (nproduct (IMAGE f s) g = nproduct s (g o f))
2511Proof
2512 REWRITE_TAC[nproduct, GSYM NEUTRAL_MUL] THEN
2513 MATCH_MP_TAC ITERATE_IMAGE THEN REWRITE_TAC[MONOIDAL_MUL]
2514QED
2515
2516Theorem NPRODUCT_ADD_SPLIT:
2517 !f m n p.
2518 m <= n + 1
2519 ==> ((nproduct {m..n+p} f = nproduct{m..n} f * nproduct{n+1..n+p} f))
2520Proof
2521 METIS_TAC [NUMSEG_ADD_SPLIT, NPRODUCT_UNION, DISJOINT_NUMSEG, FINITE_NUMSEG,
2522 ARITH_PROVE ``x < x + 1:num``]
2523QED
2524
2525Theorem NPRODUCT_POS_LT:
2526 !f s. FINITE s /\ (!x. x IN s ==> 0 < f x) ==> 0 < nproduct s f
2527Proof
2528 GEN_TAC THEN REWRITE_TAC[CONJ_EQ_IMP] THEN
2529 ONCE_REWRITE_TAC [METIS []
2530 ``!s. ((!x. x IN s ==> 0 < f x) ==> 0 < nproduct s f) =
2531 (\s. (!x. x IN s ==> 0 < f x) ==> 0 < nproduct s f) s``] THEN
2532 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2533 SIMP_TAC arith_ss [NPRODUCT_CLAUSES, IN_INSERT, ZERO_LESS_MULT]
2534QED
2535
2536Theorem NPRODUCT_POS_LT_NUMSEG:
2537 !f m n. (!x. m <= x /\ x <= n ==> 0 < f x) ==> 0 < nproduct{m..n} f
2538Proof
2539 SIMP_TAC std_ss [NPRODUCT_POS_LT, FINITE_NUMSEG, IN_NUMSEG]
2540QED
2541
2542Theorem NPRODUCT_OFFSET:
2543 !f m p. nproduct{m+p..n+p} f = nproduct{m..n} (\i. f(i + p))
2544Proof
2545 SIMP_TAC std_ss [NUMSEG_OFFSET_IMAGE, NPRODUCT_IMAGE,
2546 EQ_ADD_RCANCEL, FINITE_NUMSEG] THEN
2547 SIMP_TAC std_ss [o_DEF]
2548QED
2549
2550Theorem NPRODUCT_SING:
2551 !f x. nproduct {x} f = f(x)
2552Proof
2553 SIMP_TAC std_ss [NPRODUCT_CLAUSES, FINITE_EMPTY, FINITE_INSERT, NOT_IN_EMPTY, MULT_CLAUSES]
2554QED
2555
2556Theorem NPRODUCT_SING_NUMSEG:
2557 !f n. nproduct{n..n} f = f(n)
2558Proof
2559 REWRITE_TAC[NUMSEG_SING, NPRODUCT_SING]
2560QED
2561
2562Theorem NPRODUCT_CLAUSES_NUMSEG:
2563 (!m. nproduct{m..0n} f = if m = 0 then f(0) else 1) /\
2564 (!m n. nproduct{m..SUC n} f = if m <= SUC n then nproduct{m..n} f * f(SUC n)
2565 else nproduct{m..n} f)
2566Proof
2567 REWRITE_TAC[NUMSEG_CLAUSES] THEN REPEAT STRIP_TAC THEN
2568 COND_CASES_TAC THEN
2569 ASM_SIMP_TAC std_ss [NPRODUCT_SING, NPRODUCT_CLAUSES, FINITE_NUMSEG, IN_NUMSEG] THEN
2570 SIMP_TAC arith_ss [ARITH_PROVE ``~(SUC n <= n)``]
2571QED
2572
2573Theorem NPRODUCT_EQ:
2574 !f g s. (!x. x IN s ==> (f x = g x)) ==> (nproduct s f = nproduct s g)
2575Proof
2576 REWRITE_TAC[nproduct] THEN MATCH_MP_TAC ITERATE_EQ THEN
2577 SIMP_TAC std_ss [MONOIDAL_MUL]
2578QED
2579
2580Theorem NPRODUCT_EQ_NUMSEG:
2581 !f g m n. (!i. m <= i /\ i <= n ==> (f(i) = g(i)))
2582 ==> (nproduct{m..n} f = nproduct{m..n} g)
2583Proof
2584 MESON_TAC[NPRODUCT_EQ, FINITE_NUMSEG, IN_NUMSEG]
2585QED
2586
2587Theorem NPRODUCT_EQ_0:
2588 !f s. FINITE s ==> ((nproduct s f = 0) <=> ?x. x IN s /\ (f(x) = 0))
2589Proof
2590 GEN_TAC THEN
2591 ONCE_REWRITE_TAC [METIS []
2592 ``!s. ((nproduct s f = 0) <=> ?x. x IN s /\ (f x = 0)) =
2593 (\s. ((nproduct s f = 0) <=> ?x. x IN s /\ (f x = 0))) s``] THEN
2594 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2595 SIMP_TAC arith_ss [NPRODUCT_CLAUSES, MULT_EQ_0, IN_INSERT, NOT_IN_EMPTY] THEN
2596 MESON_TAC[]
2597QED
2598
2599Theorem NPRODUCT_EQ_0_NUMSEG:
2600 !f m n. (nproduct{m..n} f = 0) <=> ?x. m <= x /\ x <= n /\ (f(x) = 0)
2601Proof
2602 SIMP_TAC std_ss [NPRODUCT_EQ_0, FINITE_NUMSEG, IN_NUMSEG, GSYM CONJ_ASSOC]
2603QED
2604
2605Theorem NPRODUCT_LE:
2606 !f s. FINITE s /\ (!x. x IN s ==> 0 <= f(x) /\ f(x) <= g(x))
2607 ==> nproduct s f <= nproduct s g
2608Proof
2609 GEN_TAC THEN REWRITE_TAC[CONJ_EQ_IMP] THEN
2610 ONCE_REWRITE_TAC [METIS []
2611 ``!s. ((!x. x IN s ==> 0 <= f x /\ f x <= g x) ==>
2612 nproduct s f <= nproduct s g) =
2613 (\s. (!x. x IN s ==> 0 <= f x /\ f x <= g x) ==>
2614 nproduct s f <= nproduct s g) s``] THEN
2615 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2616 SIMP_TAC std_ss [IN_INSERT, NPRODUCT_CLAUSES, NOT_IN_EMPTY, LESS_EQ_REFL] THEN
2617 MESON_TAC[LESS_MONO_MULT2, ZERO_LESS_EQ]
2618QED
2619
2620Theorem NPRODUCT_LE_NUMSEG:
2621 !f m n. (!i. m <= i /\ i <= n ==> 0 <= f(i) /\ f(i) <= g(i))
2622 ==> nproduct{m..n} f <= nproduct{m..n} g
2623Proof
2624 SIMP_TAC std_ss [NPRODUCT_LE, FINITE_NUMSEG, IN_NUMSEG]
2625QED
2626
2627Theorem NPRODUCT_EQ_1:
2628 !f s. (!x:'a. x IN s ==> (f(x) = 1)) ==> (nproduct s f = 1)
2629Proof
2630 REWRITE_TAC[nproduct, GSYM NEUTRAL_MUL] THEN
2631 SIMP_TAC std_ss [ITERATE_EQ_NEUTRAL, MONOIDAL_MUL]
2632QED
2633
2634Theorem NPRODUCT_EQ_1_NUMSEG:
2635 !f m n. (!i. m <= i /\ i <= n ==> (f(i) = 1)) ==> (nproduct{m..n} f = 1)
2636Proof
2637 SIMP_TAC std_ss [NPRODUCT_EQ_1, IN_NUMSEG]
2638QED
2639
2640Theorem NPRODUCT_MUL_GEN:
2641 !f g s.
2642 FINITE {x | x IN s /\ ~(f x = 1)} /\ FINITE {x | x IN s /\ ~(g x = 1)}
2643 ==> (nproduct s (\x. f x * g x) = nproduct s f * nproduct s g)
2644Proof
2645 SIMP_TAC std_ss [GSYM NEUTRAL_MUL, GSYM support, nproduct] THEN
2646 MATCH_MP_TAC ITERATE_OP_GEN THEN ACCEPT_TAC MONOIDAL_MUL
2647QED
2648
2649Theorem NPRODUCT_MUL:
2650 !f g s. FINITE s
2651 ==> (nproduct s (\x. f x * g x) = nproduct s f * nproduct s g)
2652Proof
2653 GEN_TAC THEN GEN_TAC THEN
2654 ONCE_REWRITE_TAC [METIS []
2655 ``(nproduct s (\x. f x * g x) = nproduct s f * nproduct s g) =
2656 (\s. (nproduct s (\x. f x * g x) = nproduct s f * nproduct s g)) s``] THEN
2657 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2658 SIMP_TAC arith_ss [NPRODUCT_CLAUSES, MULT_CLAUSES]
2659QED
2660
2661Theorem NPRODUCT_MUL_NUMSEG:
2662 !f g m n.
2663 nproduct{m..n} (\x. f x * g x) = nproduct{m..n} f * nproduct{m..n} g
2664Proof
2665 SIMP_TAC std_ss [NPRODUCT_MUL, FINITE_NUMSEG]
2666QED
2667
2668Theorem NPRODUCT_CONST:
2669 !c s. FINITE s ==> (nproduct s (\x. c) = c EXP (CARD s))
2670Proof
2671 GEN_TAC THEN
2672 ONCE_REWRITE_TAC [METIS []
2673 ``(nproduct s (\x. c) = c EXP (CARD s)) =
2674 (\s. (nproduct s (\x. c) = c EXP (CARD s))) s``] THEN
2675 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2676 SIMP_TAC arith_ss [NPRODUCT_CLAUSES, CARD_EMPTY, CARD_INSERT, EXP]
2677QED
2678
2679Theorem NPRODUCT_CONST_NUMSEG:
2680 !c m n. nproduct {m..n} (\x. c) = c EXP ((n + 1) - m)
2681Proof
2682 SIMP_TAC std_ss [NPRODUCT_CONST, CARD_NUMSEG, FINITE_NUMSEG]
2683QED
2684
2685Theorem NPRODUCT_CONST_NUMSEG_1:
2686 !c n. nproduct{1n..n} (\x. c) = c EXP n
2687Proof
2688 SIMP_TAC arith_ss [NPRODUCT_CONST, CARD_NUMSEG_1, FINITE_NUMSEG]
2689QED
2690
2691Theorem NPRODUCT_ONE:
2692 !s. nproduct s (\n. 1) = 1
2693Proof
2694 SIMP_TAC std_ss [NPRODUCT_EQ_1]
2695QED
2696
2697Theorem NPRODUCT_CLOSED:
2698 !P f:'a->num s.
2699 P(1) /\ (!x y. P x /\ P y ==> P(x * y)) /\ (!a. a IN s ==> P(f a))
2700 ==> P(nproduct s f)
2701Proof
2702 REPEAT STRIP_TAC THEN MP_TAC(MATCH_MP ITERATE_CLOSED MONOIDAL_MUL) THEN
2703 DISCH_THEN(MP_TAC o SPEC ``P:num->bool``) THEN
2704 ASM_SIMP_TAC std_ss [NEUTRAL_MUL, GSYM nproduct]
2705QED
2706
2707Theorem NPRODUCT_CLAUSES_LEFT:
2708 !f m n. m <= n ==> (nproduct{m..n} f = f(m) * nproduct{m+1n..n} f)
2709Proof
2710 SIMP_TAC std_ss [GSYM NUMSEG_LREC, NPRODUCT_CLAUSES, FINITE_NUMSEG, IN_NUMSEG] THEN
2711 ARITH_TAC
2712QED
2713
2714Theorem NPRODUCT_CLAUSES_RIGHT:
2715 !f m n. 0 < n /\ m <= n ==> (nproduct{m..n} f = nproduct{m..n-1n} f * f(n))
2716Proof
2717 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
2718 SIMP_TAC std_ss [LESS_REFL, NPRODUCT_CLAUSES_NUMSEG, SUC_SUB1]
2719QED
2720
2721Theorem NPRODUCT_SUPERSET:
2722 !f:'a->num u v.
2723 u SUBSET v /\ (!x. x IN v /\ ~(x IN u) ==> (f(x) = 1))
2724 ==> (nproduct v f = nproduct u f)
2725Proof
2726 SIMP_TAC std_ss [nproduct, GSYM NEUTRAL_MUL, ITERATE_SUPERSET, MONOIDAL_MUL]
2727QED
2728
2729Theorem NPRODUCT_PAIR:
2730 !f m n. nproduct{2n*m..2n*n+1n} f = nproduct{m..n} (\i. f(2*i) * f(2*i+1))
2731Proof
2732 MP_TAC(MATCH_MP ITERATE_PAIR MONOIDAL_MUL) THEN
2733 REWRITE_TAC[nproduct, NEUTRAL_MUL]
2734QED
2735
2736Theorem NPRODUCT_DELETE:
2737 !f s a. FINITE s /\ a IN s
2738 ==> (f(a) * nproduct(s DELETE a) f = nproduct s f)
2739Proof
2740 SIMP_TAC std_ss [nproduct, ITERATE_DELETE, MONOIDAL_MUL]
2741QED
2742
2743Theorem NPRODUCT_FACT:
2744 !n. nproduct{1n..n} (\m. m) = FACT n
2745Proof
2746 INDUCT_TAC THEN SIMP_TAC arith_ss [NPRODUCT_CLAUSES_NUMSEG, FACT] THEN
2747 ASM_SIMP_TAC std_ss [ARITH_PROVE ``1 <= SUC n``, MULT_SYM]
2748QED
2749
2750Theorem NPRODUCT_DELTA:
2751 !s a. nproduct s (\x. if x = a then b else 1) =
2752 (if a IN s then b else 1)
2753Proof
2754 REWRITE_TAC[nproduct, GSYM NEUTRAL_MUL] THEN
2755 SIMP_TAC std_ss [ITERATE_DELTA, MONOIDAL_MUL]
2756QED
2757
2758(* ------------------------------------------------------------------------- *)
2759(* Extend congruences. *)
2760(* ------------------------------------------------------------------------- *)
2761
2762Theorem NPRODUCT_CONG :
2763 (!f g s. (!x. x IN s ==> (f(x) = g(x)))
2764 ==> (nproduct s (\i. f(i)) = nproduct s g)) /\
2765 (!f g a b. (!i. a <= i /\ i <= b ==> (f(i) = g(i)))
2766 ==> (nproduct{a..b} (\i. f(i)) = nproduct{a..b} g)) /\
2767 (!f g p. (!x. p x ==> (f x = g x))
2768 ==> (nproduct {y | p y} (\i. f(i)) = nproduct {y | p y} g))
2769Proof
2770 rpt STRIP_TAC
2771 >> MATCH_MP_TAC NPRODUCT_EQ
2772 >> ASM_SIMP_TAC std_ss [GSPECIFICATION, IN_NUMSEG]
2773QED
2774
2775(* ------------------------------------------------------------------------- *)
2776(* Using additivity of lifted function to encode definedness. *)
2777(* ------------------------------------------------------------------------- *)
2778
2779(* moved here from integrationTheory *)
2780Definition lifted :
2781 (lifted op NONE _ = NONE) /\
2782 (lifted op _ NONE = NONE) /\
2783 (lifted op (SOME x) (SOME y) = SOME(op x y))
2784End
2785
2786Theorem NEUTRAL_LIFTED:
2787 !op. monoidal op ==> (neutral(lifted op) = SOME(neutral op))
2788Proof
2789 REWRITE_TAC[neutral, monoidal] THEN REPEAT STRIP_TAC THEN
2790 MATCH_MP_TAC SELECT_UNIQUE THEN
2791 SIMP_TAC std_ss [FORALL_OPTION, lifted, NOT_NONE_SOME, option_CLAUSES] THEN
2792 ASM_MESON_TAC[]
2793QED
2794
2795Theorem MONOIDAL_LIFTED:
2796 !op. monoidal op ==> monoidal(lifted op)
2797Proof
2798 REPEAT STRIP_TAC THEN ASM_SIMP_TAC std_ss [NEUTRAL_LIFTED, monoidal] THEN
2799 SIMP_TAC std_ss [FORALL_OPTION, lifted, NOT_NONE_SOME, option_CLAUSES] THEN
2800 ASM_MESON_TAC[monoidal]
2801QED
2802
2803Theorem ITERATE_SOME:
2804 !op. monoidal op ==> !f s. FINITE s
2805 ==> (iterate (lifted op) s (\x. SOME(f x)) =
2806 SOME(iterate op s f))
2807Proof
2808 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
2809 KNOW_TAC ``!(s :'b -> bool).
2810 FINITE s ==>
2811 (\s. (iterate (lifted (op :'a -> 'a -> 'a)) s
2812 (\(x :'b). SOME ((f :'b -> 'a) x)) =
2813 SOME (iterate op s f))) s`` THENL
2814 [ALL_TAC, SIMP_TAC std_ss []] THEN
2815 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2816 ASM_SIMP_TAC std_ss [ITERATE_CLAUSES, MONOIDAL_LIFTED, NEUTRAL_LIFTED] THEN
2817 SIMP_TAC std_ss [lifted]
2818QED
2819
2820Theorem NEUTRAL_AND:
2821 neutral(/\) = T
2822Proof
2823 SIMP_TAC std_ss [neutral, FORALL_BOOL] THEN METIS_TAC[]
2824QED
2825
2826Theorem MONOIDAL_AND:
2827 monoidal(/\)
2828Proof
2829 REWRITE_TAC [monoidal] THEN
2830 SIMP_TAC std_ss [NEUTRAL_AND, CONJ_ACI]
2831QED
2832
2833Theorem ITERATE_AND:
2834 !p s. FINITE s ==> (iterate(/\) s p <=> !x. x IN s ==> p x)
2835Proof
2836 GEN_TAC THEN
2837 ONCE_REWRITE_TAC [METIS [] ``!s. ((iterate(/\) s p <=> !x. x IN s ==> p x)) =
2838 (\s. (iterate(/\) s p <=> !x. x IN s ==> p x)) s``] THEN
2839 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
2840 ASM_SIMP_TAC std_ss [MONOIDAL_AND, NEUTRAL_AND, ITERATE_CLAUSES] THEN SET_TAC[]
2841QED
2842
2843(* ------------------------------------------------------------------------- *)
2844(* Permutations of index set for iterated operations. *)
2845(* ------------------------------------------------------------------------- *)
2846
2847Theorem ITERATE_PERMUTE :
2848 !op. monoidal op ==>
2849 !(f:'a -> 'b) p s. p permutes s ==>
2850 (iterate op s f = iterate op s (f o p))
2851Proof
2852 REPEAT STRIP_TAC THEN
2853 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP ITERATE_BIJECTION) THEN
2854 PROVE_TAC[permutes]
2855QED
2856
2857Theorem NSUM_PERMUTE :
2858 !f p s. p permutes s ==> (nsum s f = nsum s (f o p))
2859Proof
2860 REWRITE_TAC[nsum] THEN MATCH_MP_TAC ITERATE_PERMUTE THEN
2861 REWRITE_TAC[MONOIDAL_ADD]
2862QED
2863
2864Theorem NSUM_PERMUTE_COUNT :
2865 !f p n. p permutes (count n) ==> (nsum (count n) f = nsum (count n) (f o p))
2866Proof
2867 PROVE_TAC[NSUM_PERMUTE, FINITE_COUNT]
2868QED
2869
2870Theorem NSUM_PERMUTE_NUMSEG :
2871 !f p m n. p permutes (count n DIFF count m) ==>
2872 (nsum (count n DIFF count m) f = nsum (count n DIFF count m) (f o p))
2873Proof
2874 PROVE_TAC[NSUM_PERMUTE, FINITE_COUNT, FINITE_DIFF]
2875QED
2876
2877Theorem TRANSFORM_2D_NUM :
2878 !P. (!m n : num. P m n ==> P n m) /\ (!m n. P m (m + n)) ==> (!m n. P m n)
2879Proof
2880 rpt STRIP_TAC
2881 >> Know `m <= n \/ n <= m` >- DECIDE_TAC
2882 >> RW_TAC std_ss [LESS_EQ_EXISTS]
2883 >> PROVE_TAC []
2884QED
2885
2886Theorem TRIANGLE_2D_NUM :
2887 !P. (!d n. P n (d + n)) ==> (!m n : num. m <= n ==> P m n)
2888Proof
2889 RW_TAC std_ss [LESS_EQ_EXISTS]
2890 >> PROVE_TAC [ADD_COMM]
2891QED
2892