fcpScript.sml
1(* ========================================================================= *)
2(* FILE : fcpScript.sml *)
3(* DESCRIPTION : A port, from HOL light, of John Harrison's treatment of *)
4(* finite Cartesian products (TPHOLs 2005) *)
5(* DATE : 2005 *)
6(* ========================================================================= *)
7Theory fcp
8Ancestors
9 arithmetic pred_set list iterate
10Libs
11 numLib hurdUtils mesonLib
12
13
14(* ------------------------------------------------------------------------- *)
15(* NOTES for HOL-Light users (or HOL4 porters of HOL-Light theories) *)
16(* *)
17(* FCP indexes in HOL-Light are ranged from 1 to ‘dimindex(:'N)’, while in *)
18(* HOL4 they are ranged from ‘0’ to ‘dimindex(:'N) - 1’. Thus, whenever in *)
19(* HOL-Light it says ‘1 <= i /\ i <= dimindex(:'N)’, here in HOL4 one says *)
20(* ‘i < dimindex(:'N)’ instead. (as ‘0 <= i’ is always true for naturals.) *)
21(* *)
22(* In particular, the frequently needed DIMINDEX_GE_1 in many FCP-related *)
23(* proofs in HOL-Light, is not very useful here in HOL4. Porters may need *)
24(* to use the new DIMINDEX_GT_0 instead, in some ported proofs. *)
25(* *)
26(* The other difference is that, in HOL-Light, the (') operator is total: *)
27(* ‘f ' i := 0’ if ‘1 <= i /\ i <= dimindex(:N)’ does not hold, while here *)
28(* ‘f ' i’ is unspecified if ‘i >= dimindex(:'N)’. Thus for some theorems, *)
29(* porters may need to add extra antecedents like ‘i < dimindex(:'N) ==> ’ *)
30(* to some FCP-related theorems. -- Chun Tian (binghe), May 12, 2022 *)
31(* ------------------------------------------------------------------------- *)
32
33(* ------------------------------------------------------------------------- *
34 * An isomorphic image of any finite type, 1-element for infinite ones. *
35 * ------------------------------------------------------------------------- *)
36
37val finite_image_tybij =
38 BETA_RULE
39 (define_new_type_bijections
40 {name = "finite_image_tybij",
41 ABS = "mk_finite_image",
42 REP = "dest_finite_image",
43 tyax = new_type_definition ("finite_image",
44 PROVE []
45 ``?x:'a. (\x. (x = ARB) \/ FINITE (UNIV:'a->bool)) x``)})
46
47Theorem FINITE_IMAGE_IMAGE[local]:
48 UNIV:'a finite_image->bool =
49 IMAGE mk_finite_image
50 (if FINITE(UNIV:'a->bool) then UNIV:'a->bool else {ARB})
51Proof
52 MP_TAC finite_image_tybij
53 THEN COND_CASES_TAC
54 THEN ASM_REWRITE_TAC []
55 THEN REWRITE_TAC [EXTENSION, IN_IMAGE, IN_SING, IN_UNIV]
56 THEN PROVE_TAC []
57QED
58
59(* ------------------------------------------------------------------------- *
60 * Dimension of such a type, and indexing over it. *
61 * ------------------------------------------------------------------------- *)
62
63Definition dimindex_def[nocompute]:
64 dimindex(:'a) = if FINITE (UNIV:'a->bool) then CARD (UNIV:'a->bool) else 1
65End
66
67Theorem NOT_FINITE_IMP_dimindex_1:
68 ~FINITE univ(:'a) ==> (dimindex(:'a) = 1)
69Proof
70 METIS_TAC [dimindex_def]
71QED
72
73Theorem HAS_SIZE_FINITE_IMAGE[local]:
74 (UNIV:'a finite_image->bool) HAS_SIZE dimindex(:'a)
75Proof
76 REWRITE_TAC [dimindex_def, FINITE_IMAGE_IMAGE]
77 THEN MP_TAC finite_image_tybij
78 THEN COND_CASES_TAC
79 THEN ASM_REWRITE_TAC []
80 THEN STRIP_TAC
81 THEN MATCH_MP_TAC HAS_SIZE_IMAGE_INJ
82 THEN ASM_REWRITE_TAC [HAS_SIZE, IN_UNIV, IN_SING]
83 THEN SIMP_TAC arith_ss [CARD_EMPTY, CARD_SING, CARD_INSERT, FINITE_SING,
84 FINITE_INSERT, NOT_IN_EMPTY]
85 THEN PROVE_TAC[]
86QED
87
88val CARD_FINITE_IMAGE =
89 PROVE [HAS_SIZE_FINITE_IMAGE, HAS_SIZE]
90 ``CARD (UNIV:'a finite_image->bool) = dimindex(:'a)``
91
92val FINITE_FINITE_IMAGE =
93 PROVE [HAS_SIZE_FINITE_IMAGE, HAS_SIZE]
94 ``FINITE (UNIV:'a finite_image->bool)``
95
96Theorem DIMINDEX_NONZERO[simp] =
97 METIS_PROVE [HAS_SIZE_0, UNIV_NOT_EMPTY, HAS_SIZE_FINITE_IMAGE]
98 ``~(dimindex(:'a) = 0)``
99
100Theorem DIMINDEX_GE_1[simp]:
101 1 <= dimindex(:'a)
102Proof
103 REWRITE_TAC [DECIDE ``1 <= x <=> ~(x = 0)``, DIMINDEX_NONZERO]
104QED
105
106(* |- 0 < dimindex(:'a) *)
107Theorem DIMINDEX_GT_0[simp] =
108 REWRITE_RULE [arithmeticTheory.NOT_ZERO_LT_ZERO] DIMINDEX_NONZERO
109
110Theorem DIMINDEX_FINITE_IMAGE[local]:
111 dimindex(:'a finite_image) = dimindex(:'a)
112Proof
113 GEN_REWRITE_TAC LAND_CONV empty_rewrites [dimindex_def]
114 THEN MP_TAC HAS_SIZE_FINITE_IMAGE
115 THEN SIMP_TAC std_ss [FINITE_FINITE_IMAGE, HAS_SIZE]
116QED
117
118Definition finite_index[nocompute]:
119 finite_index = @f:num->'a. !x:'a. ?!n. n < dimindex(:'a) /\ (f n = x)
120End
121
122Theorem FINITE_INDEX_WORKS_FINITE[local]:
123 FINITE (UNIV:'n->bool) ==>
124 !i:'n. ?!n. n < dimindex(:'n) /\ (finite_index n = i)
125Proof
126 DISCH_TAC
127 THEN ASM_REWRITE_TAC [finite_index, dimindex_def]
128 THEN CONV_TAC SELECT_CONV
129 THEN Q.SUBGOAL_THEN `(UNIV:'n->bool) HAS_SIZE CARD(UNIV:'n->bool)` MP_TAC
130 THEN1 PROVE_TAC [HAS_SIZE]
131 THEN DISCH_THEN (MP_TAC o MATCH_MP HAS_SIZE_INDEX)
132 THEN ASM_REWRITE_TAC [HAS_SIZE, IN_UNIV]
133QED
134
135Theorem FINITE_INDEX_WORKS[local]:
136 !i:'a finite_image. ?!n. n < dimindex(:'a) /\ (finite_index n = i)
137Proof
138 MP_TAC (MATCH_MP FINITE_INDEX_WORKS_FINITE FINITE_FINITE_IMAGE)
139 THEN PROVE_TAC [DIMINDEX_FINITE_IMAGE]
140QED
141
142Theorem FINITE_INDEX_INJ[local]:
143 !i j. i < dimindex(:'a) /\ j < dimindex(:'a) ==>
144 ((finite_index i :'a = finite_index j) = (i = j))
145Proof
146 Q.ASM_CASES_TAC `FINITE(UNIV:'a->bool)`
147 THEN ASM_REWRITE_TAC [dimindex_def]
148 THENL [
149 FIRST_ASSUM (MP_TAC o MATCH_MP FINITE_INDEX_WORKS_FINITE)
150 THEN ASM_REWRITE_TAC [dimindex_def]
151 THEN PROVE_TAC [],
152 PROVE_TAC [DECIDE ``!a. a < 1 <=> (a = 0)``]
153 ]
154QED
155
156val FORALL_FINITE_INDEX =
157 PROVE [FINITE_INDEX_WORKS]
158 ``(!k:'n finite_image. P k) =
159 (!i. i < dimindex(:'n) ==> P(finite_index i))``
160
161(* ------------------------------------------------------------------------- *
162 * Hence finite Cartesian products, with indexing and lambdas. *
163 * ------------------------------------------------------------------------- *)
164
165val cart_tybij =
166 SIMP_RULE std_ss []
167 (define_new_type_bijections
168 {name = "cart_tybij",
169 ABS = "mk_cart",
170 REP = "dest_cart",
171 tyax = new_type_definition("cart",
172 Q.prove(`?f:'b finite_image->'a. (\f. T) f`, REWRITE_TAC[]))})
173
174val () = add_infix_type {Prec = 60, ParseName = SOME "**", Name = "cart",
175 Assoc = HOLgrammars.RIGHT}
176
177val fcp_index_def =
178 Q.new_infixl_definition
179 ("fcp_index", `$fcp_index x i = dest_cart x (finite_index i)`, 500)
180
181val () = set_fixity "'" (Infixl 2000)
182Overload "'" = Term`$fcp_index`
183
184(* ---------------------------------------------------------------------- *
185 * Establish arrays as an algebraic datatype, with constructor *
186 * mk_cart, even though no user would want to define functions that way. *
187 * *
188 * When the datatype package handles function-spaces (recursing on *
189 * the right), this will allow the datatype package to define types *
190 * that recurse through arrays. *
191 * ---------------------------------------------------------------------- *)
192
193Theorem fcp_Axiom:
194 !f : ('b finite_image -> 'a) -> 'c.
195 ?g : 'a ** 'b -> 'c. !h. g (mk_cart h) = f h
196Proof
197 STRIP_TAC THEN Q.EXISTS_TAC `f o dest_cart` THEN SRW_TAC [] [cart_tybij]
198QED
199
200Theorem fcp_ind:
201 !P. (!f. P (mk_cart f)) ==> !a. P a
202Proof
203 SRW_TAC [] []
204 THEN Q.SPEC_THEN `a` (SUBST1_TAC o SYM) (CONJUNCT1 cart_tybij)
205 THEN SRW_TAC [] []
206QED
207
208(* could just call
209
210 Prim_rec.define_case_constant fcp_Axiom
211
212 but this gives the case constant the name cart_CASE *)
213
214val fcp_case_def = new_specification("fcp_case_def", ["fcp_CASE"],
215 Q.prove(
216 `?cf. !h f. cf (mk_cart h) f = f h`,
217 Q.X_CHOOSE_THEN `cf0` STRIP_ASSUME_TAC
218 (SIMP_RULE (srw_ss()) [SKOLEM_THM] fcp_Axiom)
219 THEN Q.EXISTS_TAC `\c f. cf0 f c`
220 THEN BETA_TAC
221 THEN ASM_REWRITE_TAC []
222 ))
223
224val fcp_tyinfo =
225 TypeBasePure.gen_datatype_info
226 {ax = fcp_Axiom, ind = fcp_ind, case_defs = [fcp_case_def]}
227
228val _ = TypeBase.write fcp_tyinfo
229
230Theorem CART_EQ:
231 !(x:'a ** 'b) y. (x = y) = (!i. i < dimindex(:'b) ==> (x ' i = y ' i))
232Proof
233 REPEAT GEN_TAC
234 THEN SIMP_TAC std_ss [fcp_index_def, GSYM FORALL_FINITE_INDEX]
235 THEN REWRITE_TAC [GSYM FUN_EQ_THM, ETA_AX]
236 THEN PROVE_TAC [cart_tybij]
237QED
238
239val FCP = new_binder_definition("FCP",
240 ``($FCP) = \g. @(f:'a ** 'b). (!i. i < dimindex(:'b) ==> (f ' i = g i))``)
241
242(* NOTE: generalizing ‘g’ will break blastLib.sml *)
243Theorem FCP_BETA :
244 !i. i < dimindex(:'b) ==> (((FCP) g:'a ** 'b) ' i = g i)
245Proof
246 SIMP_TAC std_ss [FCP]
247 >> CONV_TAC SELECT_CONV
248 >> Q.EXISTS_TAC `mk_cart(\k. g(@i. i < dimindex(:'b) /\
249 (finite_index i = k))):'a ** 'b`
250 >> SIMP_TAC std_ss [fcp_index_def, cart_tybij]
251 >> REPEAT STRIP_TAC
252 >> AP_TERM_TAC
253 >> MATCH_MP_TAC SELECT_UNIQUE
254 >> GEN_TAC
255 >> REWRITE_TAC []
256 >> PROVE_TAC [FINITE_INDEX_INJ, DIMINDEX_FINITE_IMAGE]
257QED
258
259Theorem FCP_UNIQUE:
260 !(f:'a ** 'b) g. (!i. i < dimindex(:'b) ==> (f ' i = g i)) = ((FCP) g = f)
261Proof
262 SIMP_TAC std_ss [CART_EQ, FCP_BETA] THEN PROVE_TAC[]
263QED
264
265Theorem FCP_ETA:
266 !g. (FCP i. g ' i) = g
267Proof
268 SIMP_TAC std_ss [CART_EQ, FCP_BETA]
269QED
270
271Theorem card_dimindex :
272 FINITE (UNIV:'a->bool) ==> (CARD (UNIV:'a->bool) = dimindex(:'a))
273Proof
274 METIS_TAC [dimindex_def]
275QED
276
277(* ------------------------------------------------------------------------- *
278 * Support for introducing finite index types *
279 * ------------------------------------------------------------------------- *)
280
281(* -------------------------------------------------------------------------
282 Sums (for concatenation)
283 ------------------------------------------------------------------------- *)
284
285Theorem sum_union[local]:
286 UNIV:('a+'b)->bool = ISL UNION ISR
287Proof
288 REWRITE_TAC [FUN_EQ_THM, UNIV_DEF, UNION_DEF]
289 THEN STRIP_TAC
290 THEN ONCE_REWRITE_TAC [GSYM SPECIFICATION]
291 THEN SIMP_TAC std_ss [GSPECIFICATION, IN_DEF, sumTheory.ISL_OR_ISR]
292QED
293
294Theorem inl_inr_bij[local]:
295 BIJ INL (UNIV:'a->bool) (ISL:'a + 'b -> bool) /\
296 BIJ INR (UNIV:'b->bool) (ISR:'a + 'b -> bool)
297Proof
298 RW_TAC std_ss [UNIV_DEF, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_DEF]
299 THEN PROVE_TAC [sumTheory.INL, sumTheory.INR]
300QED
301
302Theorem inl_inr_image[local]:
303 ((ISL:'a + 'b -> bool) = IMAGE INL (UNIV:'a->bool)) /\
304 ((ISR:'a + 'b -> bool) = IMAGE INR (UNIV:'b->bool))
305Proof
306 RW_TAC std_ss [EXTENSION, IMAGE_DEF, IN_UNIV, GSPECIFICATION]
307 THEN SIMP_TAC std_ss [IN_DEF]
308 THEN Cases_on `x`
309 THEN SIMP_TAC std_ss [sumTheory.ISL, sumTheory.ISR, sumTheory.sum_distinct]
310QED
311
312Theorem isl_isr_finite[local]:
313 (FINITE (ISL:'a + 'b -> bool) = FINITE (UNIV:'a->bool)) /\
314 (FINITE (ISR:'a + 'b -> bool) = FINITE (UNIV:'b->bool))
315Proof
316 REWRITE_TAC [inl_inr_image]
317 THEN CONJ_TAC
318 THEN MATCH_MP_TAC INJECTIVE_IMAGE_FINITE
319 THEN REWRITE_TAC [sumTheory.INR_INL_11]
320QED
321
322Theorem isl_isr_univ[local]:
323 (FINITE (UNIV:'a -> bool) ==>
324 (CARD (ISL:'a + 'b -> bool) = CARD (UNIV:'a->bool))) /\
325 (FINITE (UNIV:'b -> bool) ==>
326 (CARD (ISR:'a + 'b -> bool) = CARD (UNIV:'b->bool)))
327Proof
328 METIS_TAC [FINITE_BIJ_CARD_EQ, isl_isr_finite, inl_inr_bij]
329QED
330
331Theorem isl_isr_inter[local]:
332 (ISL:'a + 'b -> bool) INTER (ISR:'a + 'b -> bool) = {}
333Proof
334 RW_TAC std_ss [INTER_DEF, EXTENSION, NOT_IN_EMPTY, GSPECIFICATION]
335 THEN SIMP_TAC std_ss [IN_DEF]
336 THEN Cases_on `x`
337 THEN SIMP_TAC std_ss [sumTheory.ISR, sumTheory.ISL]
338QED
339
340Theorem isl_isr_union[local]:
341 FINITE (UNIV:'a -> bool) /\ FINITE (UNIV:'b -> bool) ==>
342 (CARD ((ISL:'a + 'b -> bool) UNION (ISR:'a + 'b -> bool)) =
343 CARD (ISL:'a + 'b -> bool) + CARD (ISR:'a + 'b -> bool))
344Proof
345 METIS_TAC [CARD_UNION, arithmeticTheory.ADD_0, CARD_EMPTY,
346 isl_isr_inter, isl_isr_finite]
347QED
348
349Theorem index_sum:
350 dimindex(:('a+'b)) =
351 if FINITE (UNIV:'a->bool) /\ FINITE (UNIV:'b->bool) then
352 dimindex(:'a) + dimindex(:'b)
353 else
354 1
355Proof
356 RW_TAC std_ss [dimindex_def, sum_union, isl_isr_union, isl_isr_univ,
357 FINITE_UNION]
358 THEN METIS_TAC [isl_isr_finite]
359QED
360
361Theorem finite_sum:
362 FINITE (UNIV:('a+'b)->bool) <=>
363 FINITE (UNIV:'a->bool) /\ FINITE (UNIV:'b->bool)
364Proof
365 SIMP_TAC std_ss [FINITE_UNION, sum_union, isl_isr_finite]
366QED
367
368(* ------------------------------------------------------------------------- *
369 * bit0 *
370 * ------------------------------------------------------------------------- *)
371
372Datatype: bit0 = BIT0A 'a | BIT0B 'a
373End
374
375Definition IS_BIT0A_def[nocompute]:
376 (IS_BIT0A (BIT0A x) = T) /\ (IS_BIT0A (BIT0B x) = F)
377End
378
379Definition IS_BIT0B_def[nocompute]:
380 (IS_BIT0B (BIT0A x) = F) /\ (IS_BIT0B (BIT0B x) = T)
381End
382
383Theorem IS_BIT0A_OR_IS_BIT0B[local]:
384 !x. IS_BIT0A x \/ IS_BIT0B x
385Proof
386 Cases THEN METIS_TAC [IS_BIT0A_def, IS_BIT0B_def]
387QED
388
389Theorem bit0_union[local]:
390 UNIV:('a bit0)->bool = IS_BIT0A UNION IS_BIT0B
391Proof
392 REWRITE_TAC [FUN_EQ_THM, UNIV_DEF, UNION_DEF]
393 THEN STRIP_TAC
394 THEN ONCE_REWRITE_TAC [GSYM SPECIFICATION]
395 THEN SIMP_TAC std_ss [GSPECIFICATION, IN_DEF, IS_BIT0A_OR_IS_BIT0B]
396QED
397
398Theorem is_bit0a_bij[local]:
399 BIJ BIT0A (UNIV:'a->bool) (IS_BIT0A:'a bit0->bool)
400Proof
401 RW_TAC std_ss [UNIV_DEF, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_DEF, IS_BIT0A_def]
402 THEN Cases_on `x`
403 THEN FULL_SIMP_TAC std_ss [IS_BIT0A_def, IS_BIT0B_def]
404 THEN METIS_TAC []
405QED
406
407Theorem is_bit0b_bij[local]:
408 BIJ BIT0B (UNIV:'a->bool) (IS_BIT0B:'a bit0->bool)
409Proof
410 RW_TAC std_ss [UNIV_DEF, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_DEF, IS_BIT0B_def]
411 THEN Cases_on `x`
412 THEN FULL_SIMP_TAC std_ss [IS_BIT0A_def, IS_BIT0B_def]
413 THEN METIS_TAC []
414QED
415
416Theorem is_bit0a_image[local]:
417 IS_BIT0A = IMAGE BIT0A (UNIV:'a->bool)
418Proof
419 RW_TAC std_ss [EXTENSION, IMAGE_DEF, IN_UNIV, GSPECIFICATION]
420 THEN SIMP_TAC std_ss [IN_DEF]
421 THEN Cases_on `x`
422 THEN SIMP_TAC (srw_ss()) [IS_BIT0A_def, IS_BIT0B_def]
423QED
424
425Theorem is_bit0b_image[local]:
426 IS_BIT0B = IMAGE BIT0B (UNIV:'a->bool)
427Proof
428 RW_TAC std_ss [EXTENSION, IMAGE_DEF, IN_UNIV, GSPECIFICATION]
429 THEN SIMP_TAC std_ss [IN_DEF]
430 THEN Cases_on `x`
431 THEN SIMP_TAC (srw_ss()) [IS_BIT0A_def, IS_BIT0B_def]
432QED
433
434Theorem is_bit0a_finite[local]:
435 FINITE (IS_BIT0A:'a bit0->bool) = FINITE (UNIV:'a->bool)
436Proof
437 REWRITE_TAC [is_bit0a_image]
438 THEN MATCH_MP_TAC INJECTIVE_IMAGE_FINITE
439 THEN SIMP_TAC (srw_ss()) []
440QED
441
442Theorem is_bit0b_finite[local]:
443 FINITE (IS_BIT0B:'a bit0->bool) = FINITE (UNIV:'a->bool)
444Proof
445 REWRITE_TAC [is_bit0b_image]
446 THEN MATCH_MP_TAC INJECTIVE_IMAGE_FINITE
447 THEN SIMP_TAC (srw_ss()) []
448QED
449
450Theorem is_bit0a_card[local]:
451 FINITE (UNIV:'a->bool) ==>
452 (CARD (IS_BIT0A:'a bit0->bool) = CARD (UNIV:'a->bool))
453Proof
454 METIS_TAC [FINITE_BIJ_CARD_EQ, is_bit0a_finite, is_bit0a_bij]
455QED
456
457Theorem is_bit0b_card[local]:
458 FINITE (UNIV:'a->bool) ==>
459 (CARD (IS_BIT0B:'a bit0->bool) = CARD (UNIV:'a->bool))
460Proof
461 METIS_TAC [FINITE_BIJ_CARD_EQ, is_bit0b_finite, is_bit0b_bij]
462QED
463
464Theorem is_bit0a_is_bit0b_inter[local]:
465 IS_BIT0A INTER IS_BIT0B = {}
466Proof
467 RW_TAC std_ss [INTER_DEF, EXTENSION, NOT_IN_EMPTY, GSPECIFICATION]
468 THEN Cases_on `x`
469 THEN SIMP_TAC std_ss [IN_DEF, IS_BIT0A_def, IS_BIT0B_def]
470QED
471
472Theorem is_bit0a_is_bit0b_union[local]:
473 FINITE (UNIV:'a -> bool) ==>
474 (CARD ((IS_BIT0A:'a bit0 -> bool) UNION (IS_BIT0B:'a bit0 -> bool)) =
475 CARD (IS_BIT0A:'a bit0 -> bool) + CARD (IS_BIT0B:'a bit0 -> bool))
476Proof
477 STRIP_TAC
478 THEN IMP_RES_TAC (GSYM is_bit0a_finite)
479 THEN IMP_RES_TAC (GSYM is_bit0b_finite)
480 THEN IMP_RES_TAC CARD_UNION
481 THEN FULL_SIMP_TAC std_ss [is_bit0a_is_bit0b_inter, CARD_EMPTY]
482QED
483
484Theorem index_bit0:
485 dimindex(:('a bit0)) =
486 if FINITE (UNIV:'a->bool) then 2 * dimindex(:'a) else 1
487Proof
488 RW_TAC std_ss [dimindex_def, bit0_union, is_bit0a_is_bit0b_union,
489 FINITE_UNION]
490 THEN METIS_TAC [is_bit0a_finite, is_bit0a_card, is_bit0b_finite,
491 is_bit0b_card, arithmeticTheory.TIMES2]
492QED
493
494Theorem finite_bit0:
495 FINITE (UNIV:'a bit0->bool) = FINITE (UNIV:'a->bool)
496Proof
497 SIMP_TAC std_ss [FINITE_UNION, is_bit0a_finite, is_bit0b_finite, bit0_union]
498QED
499
500(* ------------------------------------------------------------------------- *
501 * bit1 *
502 * ------------------------------------------------------------------------- *)
503
504Datatype: bit1 = BIT1A 'a | BIT1B 'a | BIT1C
505End
506
507Definition IS_BIT1A_def[nocompute]:
508 (IS_BIT1A (BIT1A x) = T) /\ (IS_BIT1A (BIT1B x) = F) /\
509 (IS_BIT1A (BIT1C) = F)
510End
511
512Definition IS_BIT1B_def[nocompute]:
513 (IS_BIT1B (BIT1A x) = F) /\ (IS_BIT1B (BIT1B x) = T) /\
514 (IS_BIT1B (BIT1C) = F)
515End
516
517Definition IS_BIT1C_def[nocompute]:
518 (IS_BIT1C (BIT1A x) = F) /\ (IS_BIT1C (BIT1B x) = F) /\
519 (IS_BIT1C (BIT1C) = T)
520End
521
522Theorem IS_BIT1A_OR_IS_BIT1B_OR_IS_BIT1C[local]:
523 !x. IS_BIT1A x \/ IS_BIT1B x \/ IS_BIT1C x
524Proof
525 Cases THEN METIS_TAC [IS_BIT1A_def, IS_BIT1B_def, IS_BIT1C_def]
526QED
527
528Theorem bit1_union[local]:
529 UNIV:('a bit1)->bool = IS_BIT1A UNION IS_BIT1B UNION IS_BIT1C
530Proof
531 REWRITE_TAC [FUN_EQ_THM, UNIV_DEF, UNION_DEF]
532 THEN STRIP_TAC
533 THEN ONCE_REWRITE_TAC [GSYM SPECIFICATION]
534 THEN SIMP_TAC std_ss [GSPECIFICATION, IN_DEF]
535 THEN METIS_TAC [IS_BIT1A_OR_IS_BIT1B_OR_IS_BIT1C]
536QED
537
538Theorem is_bit1a_bij[local]:
539 BIJ BIT1A (UNIV:'a->bool) (IS_BIT1A:'a bit1->bool)
540Proof
541 RW_TAC std_ss [UNIV_DEF, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_DEF, IS_BIT1A_def]
542 THEN Cases_on `x`
543 THEN FULL_SIMP_TAC std_ss [IS_BIT1A_def, IS_BIT1B_def, IS_BIT1C_def]
544 THEN METIS_TAC []
545QED
546
547Theorem is_bit1b_bij[local]:
548 BIJ BIT1B (UNIV:'a->bool) (IS_BIT1B:'a bit1->bool)
549Proof
550 RW_TAC std_ss [UNIV_DEF, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_DEF, IS_BIT1B_def]
551 THEN Cases_on `x`
552 THEN FULL_SIMP_TAC std_ss [IS_BIT1A_def, IS_BIT1B_def, IS_BIT1C_def]
553 THEN METIS_TAC []
554QED
555
556Theorem is_bit1a_image[local]:
557 IS_BIT1A = IMAGE BIT1A (UNIV:'a->bool)
558Proof
559 RW_TAC std_ss [EXTENSION, IMAGE_DEF, IN_UNIV, GSPECIFICATION]
560 THEN SIMP_TAC std_ss [IN_DEF]
561 THEN Cases_on `x`
562 THEN SIMP_TAC (srw_ss()) [IS_BIT1A_def, IS_BIT1B_def, IS_BIT1C_def]
563QED
564
565Theorem is_bit1b_image[local]:
566 IS_BIT1B = IMAGE BIT1B (UNIV:'a->bool)
567Proof
568 RW_TAC std_ss [EXTENSION, IMAGE_DEF, IN_UNIV, GSPECIFICATION]
569 THEN SIMP_TAC std_ss [IN_DEF]
570 THEN Cases_on `x`
571 THEN SIMP_TAC (srw_ss()) [IS_BIT1A_def, IS_BIT1B_def, IS_BIT1C_def]
572QED
573
574Theorem is_bit1a_finite[local]:
575 FINITE (IS_BIT1A:'a bit1->bool) = FINITE (UNIV:'a->bool)
576Proof
577 REWRITE_TAC [is_bit1a_image]
578 THEN MATCH_MP_TAC INJECTIVE_IMAGE_FINITE
579 THEN SIMP_TAC (srw_ss()) []
580QED
581
582Theorem is_bit1b_finite[local]:
583 FINITE (IS_BIT1B:'a bit1->bool) = FINITE (UNIV:'a->bool)
584Proof
585 REWRITE_TAC [is_bit1b_image]
586 THEN MATCH_MP_TAC INJECTIVE_IMAGE_FINITE
587 THEN SIMP_TAC (srw_ss()) []
588QED
589
590Theorem is_bit1a_card[local]:
591 FINITE (UNIV:'a->bool) ==>
592 (CARD (IS_BIT1A:'a bit1->bool) = CARD (UNIV:'a->bool))
593Proof
594 METIS_TAC [FINITE_BIJ_CARD_EQ, is_bit1a_finite, is_bit1a_bij]
595QED
596
597Theorem is_bit1b_card[local]:
598 FINITE (UNIV:'a->bool) ==>
599 (CARD (IS_BIT1B:'a bit1->bool) = CARD (UNIV:'a->bool))
600Proof
601 METIS_TAC [FINITE_BIJ_CARD_EQ, is_bit1b_finite, is_bit1b_bij]
602QED
603
604Theorem is_bit1a_is_bit1b_inter[local]:
605 IS_BIT1A INTER IS_BIT1B = {}
606Proof
607 RW_TAC std_ss [INTER_DEF, EXTENSION, NOT_IN_EMPTY, GSPECIFICATION]
608 THEN Cases_on `x`
609 THEN SIMP_TAC std_ss [IN_DEF, IS_BIT1A_def, IS_BIT1B_def, IS_BIT1C_def]
610QED
611
612Theorem IS_BIT1C_EQ_BIT1C[local]:
613 !x. IS_BIT1C x = (x = BIT1C)
614Proof
615 Cases THEN SIMP_TAC (srw_ss()) [IS_BIT1C_def]
616QED
617
618Theorem is_bit1c_sing[local]:
619 SING IS_BIT1C
620Proof
621 REWRITE_TAC [SING_DEF]
622 THEN Q.EXISTS_TAC `BIT1C`
623 THEN SIMP_TAC std_ss [FUN_EQ_THM, IS_BIT1C_EQ_BIT1C]
624 THEN METIS_TAC [IN_SING, SPECIFICATION]
625QED
626
627val is_bit1c_finite_card = REWRITE_RULE [SING_IFF_CARD1] is_bit1c_sing
628
629Theorem bit1_union_inter[local]:
630 (IS_BIT1A UNION IS_BIT1B) INTER IS_BIT1C = {}
631Proof
632 RW_TAC std_ss [INTER_DEF, EXTENSION, NOT_IN_EMPTY, GSPECIFICATION, IN_UNION]
633 THEN Cases_on `x`
634 THEN SIMP_TAC std_ss [IN_DEF, IS_BIT1A_def, IS_BIT1B_def, IS_BIT1C_def]
635QED
636
637Theorem is_bit1a_is_bit1b_is_bit1c_union[local]:
638 FINITE (UNIV:'a -> bool) ==>
639 (CARD ((IS_BIT1A:'a bit1 -> bool) UNION (IS_BIT1B:'a bit1 -> bool) UNION
640 (IS_BIT1C:'a bit1 -> bool)) =
641 CARD (IS_BIT1A:'a bit1 -> bool) + CARD (IS_BIT1B:'a bit1 -> bool) + 1)
642Proof
643 STRIP_TAC
644 THEN `FINITE (IS_BIT1A UNION IS_BIT1B)`
645 by METIS_TAC [is_bit1a_finite, is_bit1b_finite, FINITE_UNION]
646 THEN STRIP_ASSUME_TAC is_bit1c_finite_card
647 THEN IMP_RES_TAC CARD_UNION
648 THEN FULL_SIMP_TAC std_ss [bit1_union_inter, CARD_EMPTY]
649 THEN NTAC 8 (POP_ASSUM (K ALL_TAC))
650 THEN IMP_RES_TAC (GSYM is_bit1a_finite)
651 THEN IMP_RES_TAC (GSYM is_bit1b_finite)
652 THEN IMP_RES_TAC CARD_UNION
653 THEN FULL_SIMP_TAC std_ss [is_bit1a_is_bit1b_inter, CARD_EMPTY]
654QED
655
656Theorem index_bit1:
657 dimindex(:('a bit1)) =
658 if FINITE (UNIV:'a->bool) then 2 * dimindex(:'a) + 1 else 1
659Proof
660 RW_TAC std_ss [dimindex_def, bit1_union, is_bit1a_is_bit1b_is_bit1c_union,
661 FINITE_UNION]
662 THEN METIS_TAC [is_bit1a_finite, is_bit1a_card, is_bit1c_finite_card,
663 is_bit1b_finite, is_bit1b_card, arithmeticTheory.TIMES2]
664QED
665
666Theorem finite_bit1:
667 FINITE (UNIV:'a bit1->bool) = FINITE (UNIV:'a->bool)
668Proof
669 SIMP_TAC std_ss [FINITE_UNION, is_bit1a_finite, is_bit1b_finite,
670 is_bit1c_finite_card, bit1_union]
671QED
672
673(* Delete temporary constants *)
674
675val () = List.app Theory.delete_const
676 ["IS_BIT0A", "IS_BIT0B", "IS_BIT1A", "IS_BIT1B", "IS_BIT1C"]
677
678(* ------------------------------------------------------------------------ *
679 * one *
680 * ------------------------------------------------------------------------ *)
681
682Theorem one_sing[local]:
683 SING (UNIV:one->bool)
684Proof
685 REWRITE_TAC [SING_DEF]
686 THEN Q.EXISTS_TAC `()`
687 THEN SIMP_TAC std_ss [FUN_EQ_THM]
688 THEN Cases
689 THEN METIS_TAC [IN_SING, IN_UNIV, SPECIFICATION]
690QED
691
692val one_finite_card = REWRITE_RULE [SING_IFF_CARD1] one_sing
693
694Theorem index_one:
695 dimindex(:one) = 1
696Proof METIS_TAC [dimindex_def, one_finite_card]
697QED
698
699Theorem finite_one = CONJUNCT2 one_finite_card
700
701(* ------------------------------------------------------------------------ *
702 * FCP update *
703 * ------------------------------------------------------------------------ *)
704
705val FCP_ss = rewrites [FCP_BETA, FCP_ETA, CART_EQ]
706
707val () = set_fixity ":+" (Infixl 325)
708
709Definition FCP_UPDATE_def[nocompute]:
710 $:+ a b = \m:'a ** 'b. (FCP c. if a = c then b else m ' c):'a ** 'b
711End
712
713Theorem FCP_UPDATE_COMMUTES:
714 !m a b c d. ~(a = b) ==> ((a :+ c) ((b :+ d) m) = (b :+ d) ((a :+ c) m))
715Proof
716 REPEAT strip_tac
717 \\ rewrite_tac [FUN_EQ_THM]
718 \\ srw_tac [FCP_ss] [FCP_UPDATE_def]
719 \\ rw_tac std_ss []
720QED
721
722Theorem FCP_UPDATE_EQ:
723 !m a b c. (a :+ c) ((a :+ b) m) = (a :+ c) m
724Proof
725 REPEAT strip_tac
726 \\ rewrite_tac [FUN_EQ_THM]
727 \\ srw_tac [FCP_ss] [FCP_UPDATE_def]
728QED
729
730Theorem FCP_UPDATE_IMP_ID:
731 !m a v. (m ' a = v) ==> ((a :+ v) m = m)
732Proof
733 srw_tac [FCP_ss] [FCP_UPDATE_def]
734 \\ rw_tac std_ss []
735QED
736
737Theorem APPLY_FCP_UPDATE_ID:
738 !m a. (a :+ (m ' a)) m = m
739Proof
740 srw_tac [FCP_ss] [FCP_UPDATE_def]
741QED
742
743Theorem FCP_APPLY_UPDATE_THM:
744 !(m:'a ** 'b) a w b. ((a :+ w) m) ' b =
745 if b < dimindex(:'b) then
746 if a = b then w else m ' b
747 else
748 FAIL (fcp_index) ^(mk_var("index out of range", bool)) ((a :+ w) m) b
749Proof
750 srw_tac [FCP_ss] [FCP_UPDATE_def, combinTheory.FAIL_THM]
751QED
752
753(* ------------------------------------------------------------------------ *
754 * A collection of list related operations *
755 * ------------------------------------------------------------------------ *)
756
757Definition FCP_HD_def: FCP_HD v = v ' 0
758End
759
760Definition FCP_TL_def: FCP_TL v = FCP i. v ' (SUC i)
761End
762
763Definition FCP_CONS_def:
764 FCP_CONS h (v:'a ** 'b) = (0 :+ h) (FCP i. v ' (PRE i))
765End
766
767Definition FCP_MAP_def:
768 FCP_MAP f (v:'a ** 'c) = (FCP i. f (v ' i)):'b ** 'c
769End
770
771Definition FCP_EXISTS_def[nocompute]:
772 FCP_EXISTS P (v:'b ** 'a) = ?i. i < dimindex (:'a) /\ P (v ' i)
773End
774
775Definition FCP_EVERY_def[nocompute]:
776 FCP_EVERY P (v:'b ** 'a) = !i. dimindex (:'a) <= i \/ P (v ' i)
777End
778
779Definition FCP_CONCAT_def :
780 FCP_CONCAT (a:'a ** 'b) (b:'a ** 'c) =
781 (FCP i. if i < dimindex(:'c) then
782 b ' i
783 else
784 a ' (i - dimindex(:'c))): 'a ** ('b + 'c)
785End
786
787(* FCP_FST returns the "higher" dimensional part (:'a['b]) of ‘v :'a['b + 'c]’ *)
788Definition FCP_FST_def :
789 FCP_FST (v :'a ** ('b + 'c)) = (FCP i. v ' (i + dimindex (:'c))) :'a ** 'b
790End
791
792(* FCP_SND returns the "lower" dimensional part (:'a['c]) of ‘v :'a['b + 'c]’ *)
793Definition FCP_SND_def :
794 FCP_SND (v :'a ** ('b + 'c)) = (FCP i. v ' i) :'a ** 'c
795End
796
797Definition FCP_ZIP_def:
798 FCP_ZIP (a:'a ** 'b) (b:'c ** 'b) = (FCP i. (a ' i, b ' i)): ('a # 'c) ** 'b
799End
800
801Definition V2L_def: V2L (v:'a ** 'b) = GENLIST ($' v) (dimindex(:'b))
802End
803
804Definition L2V_def: L2V L = FCP i. EL i L
805End
806
807Definition FCP_FOLD_def: FCP_FOLD (f:'b -> 'a -> 'b) i v = FOLDL f i (V2L v)
808End
809
810(* Some theorems about these operations *)
811
812Theorem LENGTH_V2L:
813 !v. LENGTH (V2L (v:'a ** 'b)) = dimindex (:'b)
814Proof
815 rw [V2L_def]
816QED
817
818Theorem EL_V2L:
819 !i v. i < dimindex (:'b) ==> (EL i (V2L v) = (v:'a ** 'b) ' i)
820Proof
821 rw [V2L_def]
822QED
823
824Theorem FCP_MAP:
825 !f v. FCP_MAP f v = L2V (MAP f (V2L v))
826Proof
827 srw_tac [FCP_ss] [FCP_MAP_def, V2L_def, L2V_def, listTheory.MAP_GENLIST]
828QED
829
830Theorem FCP_TL:
831 !v. 1 < dimindex (:'b) /\ (dimindex(:'c) = dimindex(:'b) - 1) ==>
832 (FCP_TL (v:'a ** 'b) = L2V (TL (V2L v)):'a ** 'c)
833Proof
834 REPEAT strip_tac
835 \\ Cases_on `dimindex(:'b)`
836 >- prove_tac [DECIDE ``1n < n ==> n <> 0``]
837 \\ srw_tac [FCP_ss] [FCP_TL_def, V2L_def, L2V_def, listTheory.TL_GENLIST]
838QED
839
840Theorem FCP_EXISTS:
841 !P v. FCP_EXISTS P v = EXISTS P (V2L v)
842Proof
843 rw [FCP_EXISTS_def, V2L_def, listTheory.EXISTS_GENLIST]
844QED
845
846Theorem FCP_EVERY:
847 !P v. FCP_EVERY P v = EVERY P (V2L v)
848Proof
849 rw [FCP_EVERY_def, V2L_def, listTheory.EVERY_GENLIST]
850 \\ metis_tac [arithmeticTheory.NOT_LESS]
851QED
852
853Theorem FCP_HD:
854 !v. FCP_HD v = HD (V2L v)
855Proof
856 rw [FCP_HD_def, V2L_def, DIMINDEX_GE_1, listTheory.HD_GENLIST_COR,
857 DIMINDEX_GT_0]
858QED
859
860Theorem FCP_CONS:
861 !a v. FCP_CONS a (v:'a ** 'b) = L2V (a::V2L v):'a ** 'b + 1
862Proof
863 srw_tac [FCP_ss] [FCP_CONS_def, V2L_def, L2V_def, FCP_UPDATE_def]
864 \\ pop_assum mp_tac
865 \\ Cases_on `i`
866 \\ lrw [index_sum, index_one, listTheory.EL_GENLIST]
867QED
868
869Theorem V2L_L2V:
870 !x. (dimindex (:'b) = LENGTH x) ==> (V2L (L2V x:'a ** 'b) = x)
871Proof
872 rw [V2L_def, L2V_def, listTheory.LIST_EQ_REWRITE, FCP_BETA]
873QED
874
875Theorem NULL_V2L:
876 !v. ~NULL (V2L v)
877Proof
878 rw [V2L_def, listTheory.NULL_GENLIST, DIMINDEX_NONZERO]
879QED
880
881Theorem READ_TL:
882 !i a. i < dimindex (:'b) ==>
883 (((FCP_TL a):'a ** 'b) ' i = (a:'a ** 'c) ' (SUC i))
884Proof
885 rw [FCP_TL_def, FCP_BETA]
886QED
887
888Theorem READ_L2V:
889 !i a. i < dimindex (:'b) ==> ((L2V a:'a ** 'b) ' i = EL i a)
890Proof
891 rw [L2V_def, FCP_BETA]
892QED
893
894Theorem index_comp:
895 !f n.
896 (($FCP f):'a ** 'b) ' n =
897 if n < dimindex (:'b) then
898 f n
899 else
900 FAIL $' ^(mk_var("FCP out of bounds", bool))
901 (($FCP f):'a ** 'b) n
902Proof
903 srw_tac [FCP_ss] [combinTheory.FAIL_THM]
904QED
905
906Theorem fcp_subst_comp:
907 !a b f. (x :+ y) ($FCP f):'a ** 'b =
908 ($FCP (\c. if x = c then y else f c)):'a ** 'b
909Proof
910 srw_tac [FCP_ss] [FCP_UPDATE_def]
911QED
912
913val () = computeLib.add_persistent_funs ["FCP_EXISTS", "FCP_EVERY"]
914
915(* Connections between FCP_CONCAT, FCP_FST and FCP_SND *)
916Theorem FCP_CONCAT_THM :
917 !(a :'a['b]) (b :'a['c]).
918 FINITE univ(:'b) /\ FINITE univ(:'c) ==>
919 (FCP_FST (FCP_CONCAT a b) = a) /\ (FCP_SND (FCP_CONCAT a b) = b)
920Proof
921 RW_TAC std_ss [FCP_FST_def, FCP_SND_def]
922 >| [ (* goal 1 (of 2) *)
923 RW_TAC std_ss [CART_EQ, FCP_BETA] \\
924 REWRITE_TAC [FCP_CONCAT_def, index_comp] >> simp [index_sum],
925 (* goal 2 (of 2) *)
926 RW_TAC std_ss [CART_EQ, FCP_BETA] \\
927 REWRITE_TAC [FCP_CONCAT_def, index_comp] >> simp [index_sum] ]
928QED
929
930Theorem FCP_CONCAT_11 :
931 !(a :'a['b]) (b :'a['c]) c d.
932 FINITE univ(:'b) /\ FINITE univ(:'c) /\
933 (FCP_CONCAT a b = FCP_CONCAT c d) ==> (a = c) /\ (b = d)
934Proof
935 rw [FCP_CONCAT_def, CART_EQ, index_sum, FCP_BETA] >> fs []
936 >> qabbrev_tac ‘B = dimindex (:'b)’
937 >> qabbrev_tac ‘C = dimindex (:'c)’
938 >> ‘0 < B /\ 0 < C’ by rw [Abbr ‘B’, Abbr ‘C’]
939 >| [ (* goal 1 (of 2) *)
940 Q.PAT_X_ASSUM ‘!i. i < B + C ==> P’ (MP_TAC o Q.SPEC ‘i + C’) \\
941 ‘C + i < dimindex(:'b + 'c)’ by rw [index_sum] \\
942 simp [FCP_BETA],
943 (* goal 2 (of 2) *)
944 Q.PAT_X_ASSUM ‘!i. i < B + C ==> P’ (MP_TAC o Q.SPEC ‘i’) \\
945 ‘i < dimindex(:'b + 'c)’ by rw [index_sum] \\
946 simp [FCP_BETA] ]
947QED
948
949Theorem FCP_CONCAT_REDUCE :
950 !(x :'a['b + 'c]). FINITE univ(:'b) /\ FINITE univ(:'c) ==>
951 FCP_CONCAT (FCP_FST x) (FCP_SND x) = x
952Proof
953 rw [FCP_CONCAT_def, FCP_FST_def, FCP_SND_def, CART_EQ]
954 >> SRW_TAC [FCP_ss] []
955 >> rfs [NOT_LESS, index_sum]
956 >> ‘i - dimindex(:'c) < dimindex(:'b)’ by rw []
957 >> SRW_TAC [FCP_ss] []
958 >> ‘0 < dimindex(:'c)’ by PROVE_TAC [DIMINDEX_GT_0]
959 >> rw []
960QED
961
962(* from HOL-Light's "Multivariate/vector.ml" *)
963Theorem COND_COMPONENT :
964 !b x y. (if b then x else y) ' i = if b then x ' i else y ' i
965Proof
966 PROVE_TAC []
967QED
968
969(* from HOL-Light's "Library/products.ml" *)
970Theorem HAS_SIZE_CART :
971 !P m. FINITE univ(:'N) /\
972 (!i. i < dimindex(:'N) ==> {x | P i x} HAS_SIZE m i)
973 ==> {v :'a['N] | !i. i < dimindex(:'N) ==> P i (v ' i)} HAS_SIZE
974 nproduct {0 .. dimindex(:'N) - 1} m
975Proof
976 rpt GEN_TAC >> STRIP_TAC
977 >> qabbrev_tac ‘N = dimindex(:'N)’
978 >> ‘0 < N’ by rw [Abbr ‘N’]
979 >> Suff ‘!n. n < N ==> {v:'a['N] | (!i. i < N /\ i <= n ==> P i (v ' i)) /\
980 (!i. i < N /\ n < i ==> v ' i = ARB)}
981 HAS_SIZE nproduct {0 .. n} m’
982 >- (DISCH_THEN (MP_TAC o Q.SPEC ‘N - 1’) \\
983 simp [SUB_LESS_OR_EQ])
984 >> INDUCT_TAC >> rw [NPRODUCT_CLAUSES_NUMSEG]
985 >- (qabbrev_tac
986 ‘s = {v:'a['N] | P 0 (v ' 0) /\ !i. i < N /\ 0 < i ==> v ' i = ARB}’ \\
987 Know ‘s = IMAGE (\y. (FCP i. if i = 0 then y else ARB): 'a['N]) {x | P 0 x}’
988 >- (rw [Once EXTENSION] \\
989 EQ_TAC >> rw [FCP_BETA, Abbr ‘s’, CART_EQ] >| (* 3 subgoals *)
990 [ (* goal 1 (of 3) *)
991 Q.EXISTS_TAC ‘x ' 0’ >> rw [],
992 (* goal 2 (of 3) *)
993 Q.PAT_X_ASSUM ‘!i. i < N ==> x ' i = _’ (MP_TAC o Q.SPEC ‘0’) >> rw [],
994 (* goal 3 (of 3) *)
995 Q.PAT_X_ASSUM ‘!i. i < N ==> x ' i = _’ (MP_TAC o Q.SPEC ‘i’) >> rw [] ]) \\
996 Rewr' \\
997 MATCH_MP_TAC HAS_SIZE_IMAGE_INJ \\
998 rw [CART_EQ, FCP_BETA] \\
999 POP_ASSUM (MP_TAC o Q.SPEC ‘0’) >> rw [])
1000 (* stage work *)
1001 >> ‘n < N’ by rw [] >> FULL_SIMP_TAC std_ss []
1002 >> qabbrev_tac
1003 ‘s = {v:'a['N] |
1004 (!i. i < N /\ i <= SUC n ==> P i (v ' i)) /\
1005 !i. i < N /\ SUC n < i ==> v ' i = ARB}’
1006 >> qabbrev_tac ‘t = {(x,v) | x IN {x:'a | P (SUC n) x} /\
1007 v IN {v:'a['N] | (!i. i < N /\ i <= n ==> P i (v ' i)) /\
1008 (!i. i < N /\ n < i ==> v ' i = ARB)}}’
1009 >> Know ‘s = IMAGE (\(x:'a,v:'a['N]). (FCP i. if i = SUC n then x else v ' i):'a['N]) t’
1010 >- (rw [Abbr ‘s’, Abbr ‘t’, Once EXTENSION] \\
1011 EQ_TAC >> rw [] >| (* 3 subgoals *)
1012 [ (* goal 1 (of 3) *)
1013 Know ‘P (SUC n) ((x :'a['N]) ' (SUC n))’
1014 >- (FIRST_X_ASSUM MATCH_MP_TAC >> simp []) >> DISCH_TAC \\
1015 qabbrev_tac ‘y = x ' (SUC n)’ \\
1016 qabbrev_tac ‘v :'a['N] = FCP i. if i = SUC n then ARB else x ' i’ \\
1017 Q.EXISTS_TAC ‘(y,v)’ \\
1018 simp [CART_EQ, FCP_BETA, Abbr ‘y’, Abbr ‘v’] \\
1019 CONJ_TAC >- rw [] \\
1020 qabbrev_tac ‘v :'a['N] = FCP i. if i = SUC n then ARB else x ' i’ \\
1021 Q.EXISTS_TAC ‘v’ \\
1022 simp [CART_EQ, FCP_BETA, Abbr ‘v’],
1023 (* goal 2 (of 3) *)
1024 rename1 ‘P (SUC n) y’ \\
1025 simp [FCP_BETA] \\
1026 Cases_on ‘i = SUC n’ >> rw [],
1027 (* goal 3 (of 3) *)
1028 simp [FCP_BETA] ])
1029 >> Rewr'
1030 >> MATCH_MP_TAC HAS_SIZE_IMAGE_INJ
1031 >> rw []
1032 >- (gs [CART_EQ, FCP_BETA, Abbr ‘t’] \\
1033 CONJ_TAC >- (POP_ASSUM (MP_TAC o Q.SPEC ‘SUC n’) >> simp []) \\
1034 rw [] \\
1035 Cases_on ‘i = SUC n’ >- rw [] \\
1036 Q.PAT_X_ASSUM ‘!i. i < N ==> _’ (MP_TAC o Q.SPEC ‘i’) \\
1037 simp [])
1038 >> qunabbrev_tac ‘t’
1039 >> MATCH_MP_TAC HAS_SIZE_PRODUCT
1040 >> simp []
1041QED
1042
1043Theorem CARD_CART :
1044 !P. FINITE univ(:'N) /\ (!i. i < dimindex(:'N) ==> FINITE {x | P i x}) ==>
1045 CARD {v :'a['N] | !i. i < dimindex(:'N) ==> P i (v ' i)} =
1046 nproduct {0 .. dimindex(:'N) - 1} (\i. CARD {x | P i x})
1047Proof
1048 REPEAT STRIP_TAC THEN
1049 MATCH_MP_TAC(MESON[HAS_SIZE] “s HAS_SIZE n ==> CARD s = n”) THEN
1050 MATCH_MP_TAC HAS_SIZE_CART THEN
1051 simp[GSYM FINITE_HAS_SIZE]
1052QED
1053
1054(* ----------------------------------------------------------------------
1055 More cardinality results for whole universe.
1056 ---------------------------------------------------------------------- *)
1057
1058Theorem HAS_SIZE_CART_UNIV :
1059 !m. univ(:'a) HAS_SIZE m /\ FINITE univ(:'N) ==>
1060 univ(:'a['N]) HAS_SIZE m ** dimindex(:'N)
1061Proof
1062 Q.X_GEN_TAC ‘m’
1063 >> MP_TAC (Q.SPECL [‘\i x. T’, ‘\i. m’] HAS_SIZE_CART)
1064 >> rw []
1065 >> gs []
1066 >> qabbrev_tac ‘N = dimindex (:'N)’
1067 >> ‘0 < N’ by rw [Abbr ‘N’]
1068 >> qabbrev_tac ‘s = {0 .. N - 1}’
1069 >> Know ‘nproduct s (\i. m) = m ** CARD s’
1070 >- (MATCH_MP_TAC NPRODUCT_CONST >> rw [Abbr ‘s’, FINITE_NUMSEG])
1071 >> simp [Abbr ‘s’, CARD_NUMSEG]
1072 >> DISCH_THEN (art o wrap o SYM)
1073QED
1074
1075Theorem CARD_CART_UNIV :
1076 FINITE univ(:'a) /\ FINITE univ(:'N) ==>
1077 CARD univ(:'a['N]) = CARD univ(:'a) ** dimindex(:'N)
1078Proof
1079 MESON_TAC[HAS_SIZE_CART_UNIV, HAS_SIZE]
1080QED
1081
1082Theorem FINITE_CART_UNIV :
1083 FINITE univ(:'a) /\ FINITE univ(:'N) ==> FINITE univ(:'a['N])
1084Proof
1085 MESON_TAC[HAS_SIZE_CART_UNIV, HAS_SIZE]
1086QED