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(* ========================================================================= *) 7 8open HolKernel Parse boolLib bossLib; 9open pred_setTheory listTheory 10 11val () = new_theory "fcp"; 12val _ = set_grammar_ancestry ["list"] 13 14(* ------------------------------------------------------------------------- *) 15 16val qDefine = Feedback.trace ("Define.storage_message", 0) zDefine 17 18val CARD_CLAUSES = 19 CONJ CARD_EMPTY 20 (PROVE [CARD_INSERT] 21 ``!x s. 22 FINITE s ==> 23 (CARD (x INSERT s) = (if x IN s then CARD s else SUC (CARD s)))``) 24 25val IMAGE_CLAUSES = CONJ IMAGE_EMPTY IMAGE_INSERT 26val FINITE_RULES = CONJ FINITE_EMPTY FINITE_INSERT 27val NOT_SUC = numTheory.NOT_SUC 28val SUC_INJ = prim_recTheory.INV_SUC_EQ 29val LT = CONJ (DECIDE ``!m. ~(m < 0)``) prim_recTheory.LESS_THM 30val LT_REFL = prim_recTheory.LESS_REFL 31 32(* ------------------------------------------------------------------------- *) 33 34val CARD_IMAGE_INJ = Q.prove( 35 `!(f:'a->'b) s. 36 (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y)) /\ 37 FINITE s ==> (CARD (IMAGE f s) = CARD s)`, 38 GEN_TAC 39 THEN REWRITE_TAC [DECIDE ``a /\ b ==> c <=> b ==> a ==> c``] 40 THEN Q.SPEC_THEN 41 `\s. (!x y. (f x = f y) ==> y IN s ==> x IN s ==> (x = y)) ==> 42 (CARD (IMAGE f s) = CARD s)` 43 (MATCH_MP_TAC o BETA_RULE) FINITE_INDUCT 44 THEN REWRITE_TAC [NOT_IN_EMPTY, IMAGE_CLAUSES] 45 THEN REPEAT STRIP_TAC 46 THEN ASM_SIMP_TAC std_ss [CARD_CLAUSES, IMAGE_FINITE, IN_IMAGE] 47 THEN COND_CASES_TAC 48 THEN PROVE_TAC [IN_INSERT] 49 ) 50 51val HAS_SIZE_IMAGE_INJ = Q.prove( 52 `!(f:'a->'b) s n. 53 (!x y. x IN s /\ y IN s /\ (f(x) = f(y)) ==> (x = y)) /\ 54 (s HAS_SIZE n) ==> ((IMAGE f s) HAS_SIZE n)`, 55 SIMP_TAC std_ss [HAS_SIZE, IMAGE_FINITE] THEN PROVE_TAC[CARD_IMAGE_INJ]) 56 57val HAS_SIZE_INDEX = Q.prove( 58 `!s n. 59 (s HAS_SIZE n) ==> 60 ?f:num->'a. (!m. m < n ==> f(m) IN s) /\ 61 (!x. x IN s ==> ?!m. m < n /\ (f m = x))`, 62 CONV_TAC SWAP_VARS_CONV 63 THEN numLib.INDUCT_TAC 64 THEN SIMP_TAC std_ss [HAS_SIZE_0, HAS_SIZE_SUC, LT, NOT_IN_EMPTY] 65 THEN Q.X_GEN_TAC `s:'a->bool` 66 THEN REWRITE_TAC [EXTENSION, NOT_IN_EMPTY] 67 THEN SIMP_TAC std_ss [NOT_FORALL_THM] 68 THEN DISCH_THEN 69 (CONJUNCTS_THEN2 (Q.X_CHOOSE_TAC `a:'a`) (MP_TAC o Q.SPEC `a:'a`)) 70 THEN ASM_REWRITE_TAC[] 71 THEN DISCH_TAC 72 THEN FIRST_X_ASSUM (MP_TAC o Q.SPEC `s DELETE (a:'a)`) 73 THEN ASM_REWRITE_TAC [] 74 THEN DISCH_THEN (Q.X_CHOOSE_THEN `f:num->'a` STRIP_ASSUME_TAC) 75 THEN Q.EXISTS_TAC `\m:num. if m < n then f(m) else a:'a` 76 THEN CONJ_TAC 77 THENL [ 78 GEN_TAC 79 THEN REWRITE_TAC [] 80 THEN BETA_TAC 81 THEN COND_CASES_TAC 82 THEN PROVE_TAC [IN_DELETE], 83 ALL_TAC 84 ] 85 THEN Q.X_GEN_TAC `x:'a` 86 THEN DISCH_TAC 87 THEN ASM_REWRITE_TAC [] 88 THEN FIRST_X_ASSUM (MP_TAC o Q.SPEC `x:'a`) 89 THEN ASM_SIMP_TAC (std_ss++boolSimps.COND_elim_ss) [IN_DELETE] 90 THEN Q.ASM_CASES_TAC `a:'a = x` 91 THEN ASM_SIMP_TAC std_ss [] 92 THEN PROVE_TAC [LT_REFL, IN_DELETE] 93 ) 94 95(* ------------------------------------------------------------------------- * 96 * An isomorphic image of any finite type, 1-element for infinite ones. * 97 * ------------------------------------------------------------------------- *) 98 99val finite_image_tybij = 100 BETA_RULE 101 (define_new_type_bijections 102 {name = "finite_image_tybij", 103 ABS = "mk_finite_image", 104 REP = "dest_finite_image", 105 tyax = new_type_definition ("finite_image", 106 PROVE [] 107 ``?x:'a. (\x. (x = ARB) \/ FINITE (UNIV:'a->bool)) x``)}) 108 109val FINITE_IMAGE_IMAGE = Q.prove( 110 `UNIV:'a finite_image->bool = 111 IMAGE mk_finite_image 112 (if FINITE(UNIV:'a->bool) then UNIV:'a->bool else {ARB})`, 113 MP_TAC finite_image_tybij 114 THEN COND_CASES_TAC 115 THEN ASM_REWRITE_TAC [] 116 THEN REWRITE_TAC [EXTENSION, IN_IMAGE, IN_SING, IN_UNIV] 117 THEN PROVE_TAC [] 118 ) 119 120(* ------------------------------------------------------------------------- * 121 * Dimension of such a type, and indexing over it. * 122 * ------------------------------------------------------------------------- *) 123 124val dimindex_def = zDefine` 125 dimindex(:'a) = if FINITE (UNIV:'a->bool) then CARD (UNIV:'a->bool) else 1` 126 127val NOT_FINITE_IMP_dimindex_1 = Q.store_thm("NOT_FINITE_IMP_dimindex_1", 128 `~FINITE univ(:'a) ==> (dimindex(:'a) = 1)`, 129 METIS_TAC [dimindex_def]) 130 131val HAS_SIZE_FINITE_IMAGE = Q.prove( 132 `(UNIV:'a finite_image->bool) HAS_SIZE dimindex(:'a)`, 133 REWRITE_TAC [dimindex_def, FINITE_IMAGE_IMAGE] 134 THEN MP_TAC finite_image_tybij 135 THEN COND_CASES_TAC 136 THEN ASM_REWRITE_TAC [] 137 THEN STRIP_TAC 138 THEN MATCH_MP_TAC HAS_SIZE_IMAGE_INJ 139 THEN ASM_REWRITE_TAC [HAS_SIZE, IN_UNIV, IN_SING] 140 THEN SIMP_TAC arith_ss [CARD_EMPTY, CARD_SING, CARD_INSERT, FINITE_SING, 141 FINITE_INSERT, NOT_IN_EMPTY] 142 THEN PROVE_TAC[]) 143 144val CARD_FINITE_IMAGE = 145 PROVE [HAS_SIZE_FINITE_IMAGE, HAS_SIZE] 146 ``CARD (UNIV:'a finite_image->bool) = dimindex(:'a)`` 147 148val FINITE_FINITE_IMAGE = 149 PROVE [HAS_SIZE_FINITE_IMAGE, HAS_SIZE] 150 ``FINITE (UNIV:'a finite_image->bool)`` 151 152val DIMINDEX_NONZERO = 153 METIS_PROVE [HAS_SIZE_0, UNIV_NOT_EMPTY, HAS_SIZE_FINITE_IMAGE] 154 ``~(dimindex(:'a) = 0)`` 155 156val DIMINDEX_GE_1 = Q.store_thm("DIMINDEX_GE_1", 157 `1 <= dimindex(:'a)`, 158 REWRITE_TAC [DECIDE ``1 <= x <=> ~(x = 0)``, DIMINDEX_NONZERO] 159 ) 160 161val DIMINDEX_GT_0 = 162 REWRITE_RULE [arithmeticTheory.NOT_ZERO_LT_ZERO] DIMINDEX_NONZERO 163 164val DIMINDEX_FINITE_IMAGE = Q.prove( 165 `dimindex(:'a finite_image) = dimindex(:'a)`, 166 GEN_REWRITE_TAC LAND_CONV empty_rewrites [dimindex_def] 167 THEN MP_TAC HAS_SIZE_FINITE_IMAGE 168 THEN SIMP_TAC std_ss [FINITE_FINITE_IMAGE, HAS_SIZE] 169 ) 170 171val finite_index = zDefine` 172 finite_index = @f:num->'a. !x:'a. ?!n. n < dimindex(:'a) /\ (f n = x)` 173 174val FINITE_INDEX_WORKS_FINITE = Q.prove( 175 `FINITE (UNIV:'n->bool) ==> 176 !i:'n. ?!n. n < dimindex(:'n) /\ (finite_index n = i)`, 177 DISCH_TAC 178 THEN ASM_REWRITE_TAC [finite_index, dimindex_def] 179 THEN CONV_TAC SELECT_CONV 180 THEN Q.SUBGOAL_THEN `(UNIV:'n->bool) HAS_SIZE CARD(UNIV:'n->bool)` MP_TAC 181 THEN1 PROVE_TAC [HAS_SIZE] 182 THEN DISCH_THEN (MP_TAC o MATCH_MP HAS_SIZE_INDEX) 183 THEN ASM_REWRITE_TAC [HAS_SIZE, IN_UNIV] 184 ) 185 186val FINITE_INDEX_WORKS = Q.prove( 187 `!i:'a finite_image. ?!n. n < dimindex(:'a) /\ (finite_index n = i)`, 188 MP_TAC (MATCH_MP FINITE_INDEX_WORKS_FINITE FINITE_FINITE_IMAGE) 189 THEN PROVE_TAC [DIMINDEX_FINITE_IMAGE] 190 ) 191 192val FINITE_INDEX_INJ = Q.prove( 193 `!i j. i < dimindex(:'a) /\ j < dimindex(:'a) ==> 194 ((finite_index i :'a = finite_index j) = (i = j))`, 195 Q.ASM_CASES_TAC `FINITE(UNIV:'a->bool)` 196 THEN ASM_REWRITE_TAC [dimindex_def] 197 THENL [ 198 FIRST_ASSUM (MP_TAC o MATCH_MP FINITE_INDEX_WORKS_FINITE) 199 THEN ASM_REWRITE_TAC [dimindex_def] 200 THEN PROVE_TAC [], 201 PROVE_TAC [DECIDE ``!a. a < 1 <=> (a = 0)``] 202 ]) 203 204val FORALL_FINITE_INDEX = 205 PROVE [FINITE_INDEX_WORKS] 206 ``(!k:'n finite_image. P k) = 207 (!i. i < dimindex(:'n) ==> P(finite_index i))`` 208 209(* ------------------------------------------------------------------------- * 210 * Hence finite Cartesian products, with indexing and lambdas. * 211 * ------------------------------------------------------------------------- *) 212 213val cart_tybij = 214 SIMP_RULE std_ss [] 215 (define_new_type_bijections 216 {name = "cart_tybij", 217 ABS = "mk_cart", 218 REP = "dest_cart", 219 tyax = new_type_definition("cart", 220 Q.prove(`?f:'b finite_image->'a. (\f. T) f`, REWRITE_TAC[]))}) 221 222val () = add_infix_type {Prec = 60, ParseName = SOME "**", Name = "cart", 223 Assoc = HOLgrammars.RIGHT} 224 225val fcp_index_def = 226 Q.new_infixl_definition 227 ("fcp_index", `$fcp_index x i = dest_cart x (finite_index i)`, 500) 228 229val () = set_fixity "'" (Infixl 2000) 230val () = overload_on ("'", Term`$fcp_index`) 231 232(* ---------------------------------------------------------------------- * 233 * Establish arrays as an algebraic datatype, with constructor * 234 * mk_cart, even though no user would want to define functions that way. * 235 * * 236 * When the datatype package handles function-spaces (recursing on * 237 * the right), this will allow the datatype package to define types * 238 * that recurse through arrays. * 239 * ---------------------------------------------------------------------- *) 240 241val fcp_Axiom = Q.store_thm("fcp_Axiom", 242 `!f : ('b finite_image -> 'a) -> 'c. 243 ?g : 'a ** 'b -> 'c. !h. g (mk_cart h) = f h`, 244 STRIP_TAC THEN Q.EXISTS_TAC `f o dest_cart` THEN SRW_TAC [] [cart_tybij]) 245 246val fcp_ind = Q.store_thm("fcp_ind", 247 `!P. (!f. P (mk_cart f)) ==> !a. P a`, 248 SRW_TAC [] [] 249 THEN Q.SPEC_THEN `a` (SUBST1_TAC o SYM) (CONJUNCT1 cart_tybij) 250 THEN SRW_TAC [] [] 251 ) 252 253(* could just call 254 255 Prim_rec.define_case_constant fcp_Axiom 256 257 but this gives the case constant the name cart_CASE *) 258 259val fcp_case_def = new_specification("fcp_case_def", ["fcp_CASE"], 260 Q.prove( 261 `?cf. !h f. cf (mk_cart h) f = f h`, 262 Q.X_CHOOSE_THEN `cf0` STRIP_ASSUME_TAC 263 (SIMP_RULE (srw_ss()) [SKOLEM_THM] fcp_Axiom) 264 THEN Q.EXISTS_TAC `\c f. cf0 f c` 265 THEN BETA_TAC 266 THEN ASM_REWRITE_TAC [] 267 )) 268 269val fcp_tyinfo = 270 TypeBasePure.gen_datatype_info 271 {ax = fcp_Axiom, ind = fcp_ind, case_defs = [fcp_case_def]} 272 273val _ = TypeBase.write fcp_tyinfo 274 275local (* and here the palaver to make this persistent; this should be easier 276 (even without the faff I went through with PP-blocks etc to make it 277 look pretty) *) 278 fun out _ = 279 let 280 val S = PP.add_string 281 val Brk = PP.add_break 282 val Blk = PP.block PP.CONSISTENT 283 in 284 Blk 2 [ 285 S "val _ = let", Brk (1,0), 286 Blk 2 [ 287 S "val tyi = ", Brk (0,0), 288 Blk 2 [ 289 S "TypeBasePure.gen_datatype_info {", Brk (0,0), 290 S "ax = fcp_Axiom,", Brk (1,0), 291 S "ind = fcp_ind,", Brk (1,0), 292 S "case_defs = [fcp_case_def]", Brk (1,~2), 293 S "}" 294 ] 295 ], 296 Brk (1,~2), 297 S "in", Brk(1,0), 298 S "TypeBase.write tyi", Brk(1,~2), 299 S "end" 300 ] 301 end 302in 303 val _ = adjoin_to_theory {sig_ps = NONE, struct_ps = SOME out} 304end 305 306val CART_EQ = Q.store_thm("CART_EQ", 307 `!(x:'a ** 'b) y. (x = y) = (!i. i < dimindex(:'b) ==> (x ' i = y ' i))`, 308 REPEAT GEN_TAC 309 THEN SIMP_TAC std_ss [fcp_index_def, GSYM FORALL_FINITE_INDEX] 310 THEN REWRITE_TAC [GSYM FUN_EQ_THM, ETA_AX] 311 THEN PROVE_TAC [cart_tybij] 312 ) 313 314val FCP = new_binder_definition("FCP", 315 ``($FCP) = \g. @(f:'a ** 'b). (!i. i < dimindex(:'b) ==> (f ' i = g i))``) 316 317val FCP_BETA = Q.store_thm("FCP_BETA", 318 `!i. i < dimindex(:'b) ==> (((FCP) g:'a ** 'b) ' i = g i)`, 319 SIMP_TAC std_ss [FCP] 320 THEN CONV_TAC SELECT_CONV 321 THEN Q.EXISTS_TAC `mk_cart(\k. g(@i. i < dimindex(:'b) /\ 322 (finite_index i = k))):'a ** 'b` 323 THEN SIMP_TAC std_ss [fcp_index_def, cart_tybij] 324 THEN REPEAT STRIP_TAC 325 THEN AP_TERM_TAC 326 THEN MATCH_MP_TAC SELECT_UNIQUE 327 THEN GEN_TAC 328 THEN REWRITE_TAC [] 329 THEN PROVE_TAC [FINITE_INDEX_INJ, DIMINDEX_FINITE_IMAGE] 330 ) 331 332val FCP_UNIQUE = Q.store_thm("FCP_UNIQUE", 333 `!(f:'a ** 'b) g. (!i. i < dimindex(:'b) ==> (f ' i = g i)) = ((FCP) g = f)`, 334 SIMP_TAC std_ss [CART_EQ, FCP_BETA] THEN PROVE_TAC[]) 335 336val FCP_ETA = Q.store_thm("FCP_ETA", 337 `!g. (FCP i. g ' i) = g`, 338 SIMP_TAC std_ss [CART_EQ, FCP_BETA]) 339 340val card_dimindex = save_thm("card_dimindex", 341 METIS_PROVE [dimindex_def] 342 ``FINITE (UNIV:'a->bool) ==> (CARD (UNIV:'a->bool) = dimindex(:'a))``) 343 344(* ------------------------------------------------------------------------- * 345 * Support for introducing finite index types * 346 * ------------------------------------------------------------------------- *) 347 348(* ------------------------------------------------------------------------- 349 Sums (for concatenation) 350 ------------------------------------------------------------------------- *) 351 352val sum_union = Q.prove( 353 `UNIV:('a+'b)->bool = ISL UNION ISR`, 354 REWRITE_TAC [FUN_EQ_THM, UNIV_DEF, UNION_DEF] 355 THEN STRIP_TAC 356 THEN ONCE_REWRITE_TAC [GSYM SPECIFICATION] 357 THEN SIMP_TAC std_ss [GSPECIFICATION, IN_DEF, sumTheory.ISL_OR_ISR] 358 ) 359 360val inl_inr_bij = Q.prove( 361 `BIJ INL (UNIV:'a->bool) (ISL:'a + 'b -> bool) /\ 362 BIJ INR (UNIV:'b->bool) (ISR:'a + 'b -> bool)`, 363 RW_TAC std_ss [UNIV_DEF, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_DEF] 364 THEN PROVE_TAC [sumTheory.INL, sumTheory.INR] 365 ) 366 367val inl_inr_image = Q.prove( 368 `((ISL:'a + 'b -> bool) = IMAGE INL (UNIV:'a->bool)) /\ 369 ((ISR:'a + 'b -> bool) = IMAGE INR (UNIV:'b->bool))`, 370 RW_TAC std_ss [EXTENSION, IMAGE_DEF, IN_UNIV, GSPECIFICATION] 371 THEN SIMP_TAC std_ss [IN_DEF] 372 THEN Cases_on `x` 373 THEN SIMP_TAC std_ss [sumTheory.ISL, sumTheory.ISR, sumTheory.sum_distinct] 374 ) 375 376val isl_isr_finite = Q.prove( 377 `(FINITE (ISL:'a + 'b -> bool) = FINITE (UNIV:'a->bool)) /\ 378 (FINITE (ISR:'a + 'b -> bool) = FINITE (UNIV:'b->bool))`, 379 REWRITE_TAC [inl_inr_image] 380 THEN CONJ_TAC 381 THEN MATCH_MP_TAC INJECTIVE_IMAGE_FINITE 382 THEN REWRITE_TAC [sumTheory.INR_INL_11] 383 ) 384 385val isl_isr_univ = Q.prove( 386 `(FINITE (UNIV:'a -> bool) ==> 387 (CARD (ISL:'a + 'b -> bool) = CARD (UNIV:'a->bool))) /\ 388 (FINITE (UNIV:'b -> bool) ==> 389 (CARD (ISR:'a + 'b -> bool) = CARD (UNIV:'b->bool)))`, 390 METIS_TAC [FINITE_BIJ_CARD_EQ, isl_isr_finite, inl_inr_bij]) 391 392val isl_isr_inter = Q.prove( 393 `(ISL:'a + 'b -> bool) INTER (ISR:'a + 'b -> bool) = {}`, 394 RW_TAC std_ss [INTER_DEF, EXTENSION, NOT_IN_EMPTY, GSPECIFICATION] 395 THEN SIMP_TAC std_ss [IN_DEF] 396 THEN Cases_on `x` 397 THEN SIMP_TAC std_ss [sumTheory.ISR, sumTheory.ISL] 398 ) 399 400val isl_isr_union = Q.prove( 401 `FINITE (UNIV:'a -> bool) /\ FINITE (UNIV:'b -> bool) ==> 402 (CARD ((ISL:'a + 'b -> bool) UNION (ISR:'a + 'b -> bool)) = 403 CARD (ISL:'a + 'b -> bool) + CARD (ISR:'a + 'b -> bool))`, 404 METIS_TAC [CARD_UNION, arithmeticTheory.ADD_0, CARD_EMPTY, 405 isl_isr_inter, isl_isr_finite]) 406 407val index_sum = Q.store_thm("index_sum", 408 `dimindex(:('a+'b)) = 409 if FINITE (UNIV:'a->bool) /\ FINITE (UNIV:'b->bool) then 410 dimindex(:'a) + dimindex(:'b) 411 else 412 1`, 413 RW_TAC std_ss [dimindex_def, sum_union, isl_isr_union, isl_isr_univ, 414 FINITE_UNION] 415 THEN METIS_TAC [isl_isr_finite] 416 ) 417 418val finite_sum = Q.store_thm("finite_sum", 419 `FINITE (UNIV:('a+'b)->bool) <=> 420 FINITE (UNIV:'a->bool) /\ FINITE (UNIV:'b->bool)`, 421 SIMP_TAC std_ss [FINITE_UNION, sum_union, isl_isr_finite]) 422 423(* ------------------------------------------------------------------------- * 424 * bit0 * 425 * ------------------------------------------------------------------------- *) 426 427val () = Hol_datatype `bit0 = BIT0A of 'a | BIT0B of 'a` 428 429val IS_BIT0A_def = qDefine` 430 (IS_BIT0A (BIT0A x) = T) /\ (IS_BIT0A (BIT0B x) = F)` 431 432val IS_BIT0B_def = qDefine` 433 (IS_BIT0B (BIT0A x) = F) /\ (IS_BIT0B (BIT0B x) = T)` 434 435val IS_BIT0A_OR_IS_BIT0B = Q.prove( 436 `!x. IS_BIT0A x \/ IS_BIT0B x`, 437 Cases THEN METIS_TAC [IS_BIT0A_def, IS_BIT0B_def]) 438 439val bit0_union = Q.prove( 440 `UNIV:('a bit0)->bool = IS_BIT0A UNION IS_BIT0B`, 441 REWRITE_TAC [FUN_EQ_THM, UNIV_DEF, UNION_DEF] 442 THEN STRIP_TAC 443 THEN ONCE_REWRITE_TAC [GSYM SPECIFICATION] 444 THEN SIMP_TAC std_ss [GSPECIFICATION, IN_DEF, IS_BIT0A_OR_IS_BIT0B] 445 ) 446 447val is_bit0a_bij = Q.prove( 448 `BIJ BIT0A (UNIV:'a->bool) (IS_BIT0A:'a bit0->bool)`, 449 RW_TAC std_ss [UNIV_DEF, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_DEF, IS_BIT0A_def] 450 THEN Cases_on `x` 451 THEN FULL_SIMP_TAC std_ss [IS_BIT0A_def, IS_BIT0B_def] 452 THEN METIS_TAC [] 453 ) 454 455val is_bit0b_bij = Q.prove( 456 `BIJ BIT0B (UNIV:'a->bool) (IS_BIT0B:'a bit0->bool)`, 457 RW_TAC std_ss [UNIV_DEF, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_DEF, IS_BIT0B_def] 458 THEN Cases_on `x` 459 THEN FULL_SIMP_TAC std_ss [IS_BIT0A_def, IS_BIT0B_def] 460 THEN METIS_TAC [] 461 ) 462 463val is_bit0a_image = Q.prove( 464 `IS_BIT0A = IMAGE BIT0A (UNIV:'a->bool)`, 465 RW_TAC std_ss [EXTENSION, IMAGE_DEF, IN_UNIV, GSPECIFICATION] 466 THEN SIMP_TAC std_ss [IN_DEF] 467 THEN Cases_on `x` 468 THEN SIMP_TAC (srw_ss()) [IS_BIT0A_def, IS_BIT0B_def] 469 ) 470 471val is_bit0b_image = Q.prove( 472 `IS_BIT0B = IMAGE BIT0B (UNIV:'a->bool)`, 473 RW_TAC std_ss [EXTENSION, IMAGE_DEF, IN_UNIV, GSPECIFICATION] 474 THEN SIMP_TAC std_ss [IN_DEF] 475 THEN Cases_on `x` 476 THEN SIMP_TAC (srw_ss()) [IS_BIT0A_def, IS_BIT0B_def] 477 ) 478 479val is_bit0a_finite = Q.prove( 480 `FINITE (IS_BIT0A:'a bit0->bool) = FINITE (UNIV:'a->bool)`, 481 REWRITE_TAC [is_bit0a_image] 482 THEN MATCH_MP_TAC INJECTIVE_IMAGE_FINITE 483 THEN SIMP_TAC (srw_ss()) [] 484 ) 485 486val is_bit0b_finite = Q.prove( 487 `FINITE (IS_BIT0B:'a bit0->bool) = FINITE (UNIV:'a->bool)`, 488 REWRITE_TAC [is_bit0b_image] 489 THEN MATCH_MP_TAC INJECTIVE_IMAGE_FINITE 490 THEN SIMP_TAC (srw_ss()) [] 491 ) 492 493val is_bit0a_card = Q.prove( 494 `FINITE (UNIV:'a->bool) ==> 495 (CARD (IS_BIT0A:'a bit0->bool) = CARD (UNIV:'a->bool))`, 496 METIS_TAC [FINITE_BIJ_CARD_EQ, is_bit0a_finite, is_bit0a_bij]) 497 498val is_bit0b_card = Q.prove( 499 `FINITE (UNIV:'a->bool) ==> 500 (CARD (IS_BIT0B:'a bit0->bool) = CARD (UNIV:'a->bool))`, 501 METIS_TAC [FINITE_BIJ_CARD_EQ, is_bit0b_finite, is_bit0b_bij]) 502 503val is_bit0a_is_bit0b_inter = Q.prove( 504 `IS_BIT0A INTER IS_BIT0B = {}`, 505 RW_TAC std_ss [INTER_DEF, EXTENSION, NOT_IN_EMPTY, GSPECIFICATION] 506 THEN Cases_on `x` 507 THEN SIMP_TAC std_ss [IN_DEF, IS_BIT0A_def, IS_BIT0B_def] 508 ) 509 510val is_bit0a_is_bit0b_union = Q.prove( 511 `FINITE (UNIV:'a -> bool) ==> 512 (CARD ((IS_BIT0A:'a bit0 -> bool) UNION (IS_BIT0B:'a bit0 -> bool)) = 513 CARD (IS_BIT0A:'a bit0 -> bool) + CARD (IS_BIT0B:'a bit0 -> bool))`, 514 STRIP_TAC 515 THEN IMP_RES_TAC (GSYM is_bit0a_finite) 516 THEN IMP_RES_TAC (GSYM is_bit0b_finite) 517 THEN IMP_RES_TAC CARD_UNION 518 THEN FULL_SIMP_TAC std_ss [is_bit0a_is_bit0b_inter, CARD_EMPTY] 519 ) 520 521val index_bit0 = Q.store_thm("index_bit0", 522 `dimindex(:('a bit0)) = 523 if FINITE (UNIV:'a->bool) then 2 * dimindex(:'a) else 1`, 524 RW_TAC std_ss [dimindex_def, bit0_union, is_bit0a_is_bit0b_union, 525 FINITE_UNION] 526 THEN METIS_TAC [is_bit0a_finite, is_bit0a_card, is_bit0b_finite, 527 is_bit0b_card, arithmeticTheory.TIMES2] 528 ) 529 530val finite_bit0 = Q.store_thm("finite_bit0", 531 `FINITE (UNIV:'a bit0->bool) = FINITE (UNIV:'a->bool)`, 532 SIMP_TAC std_ss [FINITE_UNION, is_bit0a_finite, is_bit0b_finite, bit0_union]) 533 534(* ------------------------------------------------------------------------- * 535 * bit1 * 536 * ------------------------------------------------------------------------- *) 537 538val () = Hol_datatype `bit1 = BIT1A of 'a | BIT1B of 'a | BIT1C` 539 540val IS_BIT1A_def = qDefine` 541 (IS_BIT1A (BIT1A x) = T) /\ (IS_BIT1A (BIT1B x) = F) /\ 542 (IS_BIT1A (BIT1C) = F)` 543 544val IS_BIT1B_def = qDefine` 545 (IS_BIT1B (BIT1A x) = F) /\ (IS_BIT1B (BIT1B x) = T) /\ 546 (IS_BIT1B (BIT1C) = F)` 547 548val IS_BIT1C_def = qDefine` 549 (IS_BIT1C (BIT1A x) = F) /\ (IS_BIT1C (BIT1B x) = F) /\ 550 (IS_BIT1C (BIT1C) = T)` 551 552val IS_BIT1A_OR_IS_BIT1B_OR_IS_BIT1C = Q.prove( 553 `!x. IS_BIT1A x \/ IS_BIT1B x \/ IS_BIT1C x`, 554 Cases THEN METIS_TAC [IS_BIT1A_def, IS_BIT1B_def, IS_BIT1C_def]) 555 556val bit1_union = Q.prove( 557 `UNIV:('a bit1)->bool = IS_BIT1A UNION IS_BIT1B UNION IS_BIT1C`, 558 REWRITE_TAC [FUN_EQ_THM, UNIV_DEF, UNION_DEF] 559 THEN STRIP_TAC 560 THEN ONCE_REWRITE_TAC [GSYM SPECIFICATION] 561 THEN SIMP_TAC std_ss [GSPECIFICATION, IN_DEF] 562 THEN METIS_TAC [IS_BIT1A_OR_IS_BIT1B_OR_IS_BIT1C] 563 ) 564 565val is_bit1a_bij = Q.prove( 566 `BIJ BIT1A (UNIV:'a->bool) (IS_BIT1A:'a bit1->bool)`, 567 RW_TAC std_ss [UNIV_DEF, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_DEF, IS_BIT1A_def] 568 THEN Cases_on `x` 569 THEN FULL_SIMP_TAC std_ss [IS_BIT1A_def, IS_BIT1B_def, IS_BIT1C_def] 570 THEN METIS_TAC [] 571 ) 572 573val is_bit1b_bij = Q.prove( 574 `BIJ BIT1B (UNIV:'a->bool) (IS_BIT1B:'a bit1->bool)`, 575 RW_TAC std_ss [UNIV_DEF, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_DEF, IS_BIT1B_def] 576 THEN Cases_on `x` 577 THEN FULL_SIMP_TAC std_ss [IS_BIT1A_def, IS_BIT1B_def, IS_BIT1C_def] 578 THEN METIS_TAC [] 579 ) 580 581val is_bit1a_image = Q.prove( 582 `IS_BIT1A = IMAGE BIT1A (UNIV:'a->bool)`, 583 RW_TAC std_ss [EXTENSION, IMAGE_DEF, IN_UNIV, GSPECIFICATION] 584 THEN SIMP_TAC std_ss [IN_DEF] 585 THEN Cases_on `x` 586 THEN SIMP_TAC (srw_ss()) [IS_BIT1A_def, IS_BIT1B_def, IS_BIT1C_def] 587 ) 588 589val is_bit1b_image = Q.prove( 590 `IS_BIT1B = IMAGE BIT1B (UNIV:'a->bool)`, 591 RW_TAC std_ss [EXTENSION, IMAGE_DEF, IN_UNIV, GSPECIFICATION] 592 THEN SIMP_TAC std_ss [IN_DEF] 593 THEN Cases_on `x` 594 THEN SIMP_TAC (srw_ss()) [IS_BIT1A_def, IS_BIT1B_def, IS_BIT1C_def] 595 ) 596 597val is_bit1a_finite = Q.prove( 598 `FINITE (IS_BIT1A:'a bit1->bool) = FINITE (UNIV:'a->bool)`, 599 REWRITE_TAC [is_bit1a_image] 600 THEN MATCH_MP_TAC INJECTIVE_IMAGE_FINITE 601 THEN SIMP_TAC (srw_ss()) [] 602 ) 603 604val is_bit1b_finite = Q.prove( 605 `FINITE (IS_BIT1B:'a bit1->bool) = FINITE (UNIV:'a->bool)`, 606 REWRITE_TAC [is_bit1b_image] 607 THEN MATCH_MP_TAC INJECTIVE_IMAGE_FINITE 608 THEN SIMP_TAC (srw_ss()) [] 609 ) 610 611val is_bit1a_card = Q.prove( 612 `FINITE (UNIV:'a->bool) ==> 613 (CARD (IS_BIT1A:'a bit1->bool) = CARD (UNIV:'a->bool))`, 614 METIS_TAC [FINITE_BIJ_CARD_EQ, is_bit1a_finite, is_bit1a_bij]) 615 616val is_bit1b_card = Q.prove( 617 `FINITE (UNIV:'a->bool) ==> 618 (CARD (IS_BIT1B:'a bit1->bool) = CARD (UNIV:'a->bool))`, 619 METIS_TAC [FINITE_BIJ_CARD_EQ, is_bit1b_finite, is_bit1b_bij]) 620 621val is_bit1a_is_bit1b_inter = Q.prove( 622 `IS_BIT1A INTER IS_BIT1B = {}`, 623 RW_TAC std_ss [INTER_DEF, EXTENSION, NOT_IN_EMPTY, GSPECIFICATION] 624 THEN Cases_on `x` 625 THEN SIMP_TAC std_ss [IN_DEF, IS_BIT1A_def, IS_BIT1B_def, IS_BIT1C_def]) 626 627val IS_BIT1C_EQ_BIT1C = Q.prove( 628 `!x. IS_BIT1C x = (x = BIT1C)`, 629 Cases THEN SIMP_TAC (srw_ss()) [IS_BIT1C_def]) 630 631val is_bit1c_sing = Q.prove( 632 `SING IS_BIT1C`, 633 REWRITE_TAC [SING_DEF] 634 THEN Q.EXISTS_TAC `BIT1C` 635 THEN SIMP_TAC std_ss [FUN_EQ_THM, IS_BIT1C_EQ_BIT1C] 636 THEN METIS_TAC [IN_SING, SPECIFICATION] 637 ) 638 639val is_bit1c_finite_card = REWRITE_RULE [SING_IFF_CARD1] is_bit1c_sing 640 641val bit1_union_inter = Q.prove( 642 `(IS_BIT1A UNION IS_BIT1B) INTER IS_BIT1C = {}`, 643 RW_TAC std_ss [INTER_DEF, EXTENSION, NOT_IN_EMPTY, GSPECIFICATION, IN_UNION] 644 THEN Cases_on `x` 645 THEN SIMP_TAC std_ss [IN_DEF, IS_BIT1A_def, IS_BIT1B_def, IS_BIT1C_def] 646 ) 647 648val is_bit1a_is_bit1b_is_bit1c_union = Q.prove( 649 `FINITE (UNIV:'a -> bool) ==> 650 (CARD ((IS_BIT1A:'a bit1 -> bool) UNION (IS_BIT1B:'a bit1 -> bool) UNION 651 (IS_BIT1C:'a bit1 -> bool)) = 652 CARD (IS_BIT1A:'a bit1 -> bool) + CARD (IS_BIT1B:'a bit1 -> bool) + 1)`, 653 STRIP_TAC 654 THEN `FINITE (IS_BIT1A UNION IS_BIT1B)` 655 by METIS_TAC [is_bit1a_finite, is_bit1b_finite, FINITE_UNION] 656 THEN STRIP_ASSUME_TAC is_bit1c_finite_card 657 THEN IMP_RES_TAC CARD_UNION 658 THEN FULL_SIMP_TAC std_ss [bit1_union_inter, CARD_EMPTY] 659 THEN NTAC 8 (POP_ASSUM (K ALL_TAC)) 660 THEN IMP_RES_TAC (GSYM is_bit1a_finite) 661 THEN IMP_RES_TAC (GSYM is_bit1b_finite) 662 THEN IMP_RES_TAC CARD_UNION 663 THEN FULL_SIMP_TAC std_ss [is_bit1a_is_bit1b_inter, CARD_EMPTY] 664 ) 665 666val index_bit1 = Q.store_thm("index_bit1", 667 `dimindex(:('a bit1)) = 668 if FINITE (UNIV:'a->bool) then 2 * dimindex(:'a) + 1 else 1`, 669 RW_TAC std_ss [dimindex_def, bit1_union, is_bit1a_is_bit1b_is_bit1c_union, 670 FINITE_UNION] 671 THEN METIS_TAC [is_bit1a_finite, is_bit1a_card, is_bit1c_finite_card, 672 is_bit1b_finite, is_bit1b_card, arithmeticTheory.TIMES2] 673 ) 674 675val finite_bit1 = Q.store_thm("finite_bit1", 676 `FINITE (UNIV:'a bit1->bool) = FINITE (UNIV:'a->bool)`, 677 SIMP_TAC std_ss [FINITE_UNION, is_bit1a_finite, is_bit1b_finite, 678 is_bit1c_finite_card, bit1_union]) 679 680(* Delete temporary constants *) 681 682val () = List.app Theory.delete_const 683 ["IS_BIT0A", "IS_BIT0B", "IS_BIT1A", "IS_BIT1B", "IS_BIT1C"] 684 685(* ------------------------------------------------------------------------ * 686 * one * 687 * ------------------------------------------------------------------------ *) 688 689val one_sing = Q.prove( 690 `SING (UNIV:one->bool)`, 691 REWRITE_TAC [SING_DEF] 692 THEN Q.EXISTS_TAC `()` 693 THEN SIMP_TAC std_ss [FUN_EQ_THM] 694 THEN Cases 695 THEN METIS_TAC [IN_SING, IN_UNIV, SPECIFICATION] 696 ) 697 698val one_finite_card = REWRITE_RULE [SING_IFF_CARD1] one_sing 699 700val index_one = Q.store_thm("index_one", 701 `dimindex(:one) = 1`, METIS_TAC [dimindex_def, one_finite_card]) 702 703val finite_one = save_thm("finite_one", CONJUNCT2 one_finite_card) 704 705(* ------------------------------------------------------------------------ * 706 * FCP update * 707 * ------------------------------------------------------------------------ *) 708 709val FCP_ss = rewrites [FCP_BETA, FCP_ETA, CART_EQ] 710 711val () = set_fixity ":+" (Infixl 325) 712 713val FCP_UPDATE_def = 714 Lib.with_flag (computeLib.auto_import_definitions, false) 715 (xDefine "FCP_UPDATE") 716 `$:+ a b = \m:'a ** 'b. (FCP c. if a = c then b else m ' c):'a ** 'b` 717 718val FCP_UPDATE_COMMUTES = Q.store_thm ("FCP_UPDATE_COMMUTES", 719 `!m a b c d. ~(a = b) ==> ((a :+ c) ((b :+ d) m) = (b :+ d) ((a :+ c) m))`, 720 REPEAT strip_tac 721 \\ rewrite_tac [FUN_EQ_THM] 722 \\ srw_tac [FCP_ss] [FCP_UPDATE_def] 723 \\ rw_tac std_ss [] 724 ) 725 726val FCP_UPDATE_EQ = Q.store_thm("FCP_UPDATE_EQ", 727 `!m a b c. (a :+ c) ((a :+ b) m) = (a :+ c) m`, 728 REPEAT strip_tac 729 \\ rewrite_tac [FUN_EQ_THM] 730 \\ srw_tac [FCP_ss] [FCP_UPDATE_def] 731 ) 732 733val FCP_UPDATE_IMP_ID = Q.store_thm("FCP_UPDATE_IMP_ID", 734 `!m a v. (m ' a = v) ==> ((a :+ v) m = m)`, 735 srw_tac [FCP_ss] [FCP_UPDATE_def] 736 \\ rw_tac std_ss [] 737 ) 738 739val APPLY_FCP_UPDATE_ID = Q.store_thm("APPLY_FCP_UPDATE_ID", 740 `!m a. (a :+ (m ' a)) m = m`, 741 srw_tac [FCP_ss] [FCP_UPDATE_def]) 742 743val FCP_APPLY_UPDATE_THM = Q.store_thm("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`, 749 srw_tac [FCP_ss] [FCP_UPDATE_def, combinTheory.FAIL_THM]) 750 751(* ------------------------------------------------------------------------ * 752 * A collection of list related operations * 753 * ------------------------------------------------------------------------ *) 754 755val FCP_HD_def = Define `FCP_HD v = v ' 0` 756 757val FCP_TL_def = Define `FCP_TL v = FCP i. v ' (SUC i)` 758 759val FCP_CONS_def = Define` 760 FCP_CONS h (v:'a ** 'b) = (0 :+ h) (FCP i. v ' (PRE i))` 761 762val FCP_MAP_def = Define` 763 FCP_MAP f (v:'a ** 'c) = (FCP i. f (v ' i)):'b ** 'c` 764 765val FCP_EXISTS_def = zDefine` 766 FCP_EXISTS P (v:'b ** 'a) = ?i. i < dimindex (:'a) /\ P (v ' i)` 767 768val FCP_EVERY_def = zDefine` 769 FCP_EVERY P (v:'b ** 'a) = !i. dimindex (:'a) <= i \/ P (v ' i)` 770 771val FCP_CONCAT_def = Define` 772 FCP_CONCAT (a:'a ** 'b) (b:'a ** 'c) = 773 (FCP i. if i < dimindex(:'c) then 774 b ' i 775 else 776 a ' (i - dimindex(:'c))): 'a ** ('b + 'c)` 777 778val FCP_FST_def = Define 779 ���FCP_FST (a :'a['b + 'c]) = (FCP(i :num). a ' ((i + dimindex (:'c)) :num)) :'a['b]���; 780 781val FCP_SND_def = Define 782 ���FCP_SND (b :'a['b + 'c]) = (FCP(i :num). b ' i) :'a['c]���; 783 784val FCP_ZIP_def = Define` 785 FCP_ZIP (a:'a ** 'b) (b:'c ** 'b) = (FCP i. (a ' i, b ' i)): ('a # 'c) ** 'b` 786 787val V2L_def = Define `V2L (v:'a ** 'b) = GENLIST ($' v) (dimindex(:'b))` 788 789val L2V_def = Define `L2V L = FCP i. EL i L` 790 791val FCP_FOLD_def = Define `FCP_FOLD (f:'b -> 'a -> 'b) i v = FOLDL f i (V2L v)` 792 793(* Some theorems about these operations *) 794 795val LENGTH_V2L = Q.store_thm("LENGTH_V2L", 796 `!v. LENGTH (V2L (v:'a ** 'b)) = dimindex (:'b)`, 797 rw [V2L_def]) 798 799val EL_V2L = Q.store_thm("EL_V2L", 800 `!i v. i < dimindex (:'b) ==> (EL i (V2L v) = (v:'a ** 'b) ' i)`, 801 rw [V2L_def]) 802 803val FCP_MAP = Q.store_thm("FCP_MAP", 804 `!f v. FCP_MAP f v = L2V (MAP f (V2L v))`, 805 srw_tac [FCP_ss] [FCP_MAP_def, V2L_def, L2V_def, listTheory.MAP_GENLIST]) 806 807val FCP_TL = Q.store_thm("FCP_TL", 808 `!v. 1 < dimindex (:'b) /\ (dimindex(:'c) = dimindex(:'b) - 1) ==> 809 (FCP_TL (v:'a ** 'b) = L2V (TL (V2L v)):'a ** 'c)`, 810 REPEAT strip_tac 811 \\ Cases_on `dimindex(:'b)` 812 >- prove_tac [DECIDE ``1n < n ==> n <> 0``] 813 \\ srw_tac [FCP_ss] [FCP_TL_def, V2L_def, L2V_def, listTheory.TL_GENLIST] 814 ) 815 816val FCP_EXISTS = Q.store_thm("FCP_EXISTS", 817 `!P v. FCP_EXISTS P v = EXISTS P (V2L v)`, 818 rw [FCP_EXISTS_def, V2L_def, listTheory.EXISTS_GENLIST]) 819 820val FCP_EVERY = Q.store_thm("FCP_EVERY", 821 `!P v. FCP_EVERY P v = EVERY P (V2L v)`, 822 rw [FCP_EVERY_def, V2L_def, listTheory.EVERY_GENLIST] 823 \\ metis_tac [arithmeticTheory.NOT_LESS] 824 ) 825 826val FCP_HD = Q.store_thm("FCP_HD", 827 `!v. FCP_HD v = HD (V2L v)`, 828 rw [FCP_HD_def, V2L_def, DIMINDEX_GE_1, listTheory.HD_GENLIST_COR, 829 DIMINDEX_GT_0]) 830 831val FCP_CONS = Q.store_thm("FCP_CONS", 832 `!a v. FCP_CONS a (v:'a ** 'b) = L2V (a::V2L v):'a ** 'b + 1`, 833 srw_tac [FCP_ss] [FCP_CONS_def, V2L_def, L2V_def, FCP_UPDATE_def] 834 \\ pop_assum mp_tac 835 \\ Cases_on `i` 836 \\ lrw [index_sum, index_one, listTheory.EL_GENLIST] 837 ) 838 839val V2L_L2V = Q.store_thm("V2L_L2V", 840 `!x. (dimindex (:'b) = LENGTH x) ==> (V2L (L2V x:'a ** 'b) = x)`, 841 rw [V2L_def, L2V_def, listTheory.LIST_EQ_REWRITE, FCP_BETA]) 842 843val NULL_V2L = Q.store_thm("NULL_V2L", 844 `!v. ~NULL (V2L v)`, 845 rw [V2L_def, listTheory.NULL_GENLIST, DIMINDEX_NONZERO]) 846 847val READ_TL = Q.store_thm("READ_TL", 848 `!i a. i < dimindex (:'b) ==> 849 (((FCP_TL a):'a ** 'b) ' i = (a:'a ** 'c) ' (SUC i))`, 850 rw [FCP_TL_def, FCP_BETA]) 851 852val READ_L2V = Q.store_thm("READ_L2V", 853 `!i a. i < dimindex (:'b) ==> ((L2V a:'a ** 'b) ' i = EL i a)`, 854 rw [L2V_def, FCP_BETA]) 855 856val index_comp = Q.store_thm("index_comp", 857 `!f n. 858 (($FCP f):'a ** 'b) ' n = 859 if n < dimindex (:'b) then 860 f n 861 else 862 FAIL $' ^(mk_var("FCP out of bounds", bool)) 863 (($FCP f):'a ** 'b) n`, 864 srw_tac [FCP_ss] [combinTheory.FAIL_THM]) 865 866val fcp_subst_comp = Q.store_thm("fcp_subst_comp", 867 `!a b f. (x :+ y) ($FCP f):'a ** 'b = 868 ($FCP (\c. if x = c then y else f c)):'a ** 'b`, 869 srw_tac [FCP_ss] [FCP_UPDATE_def]) 870 871val () = computeLib.add_persistent_funs ["FCP_EXISTS", "FCP_EVERY"] 872 873(* connections to FCP_FST and FCP_SND, added by Chun Tian *) 874Theorem FCP_CONCAT_THM : 875 !(a :'a['b]) (b :'a['c]). 876 FINITE univ(:'b) /\ FINITE univ(:'c) ==> 877 (FCP_FST (FCP_CONCAT a b) = a) /\ (FCP_SND (FCP_CONCAT a b) = b) 878Proof 879 RW_TAC std_ss [FCP_FST_def, FCP_SND_def] 880 >| [ (* goal 1 (of 2) *) 881 RW_TAC std_ss [CART_EQ, FCP_BETA] \\ 882 REWRITE_TAC [FCP_CONCAT_def, index_comp] >> simp [index_sum], 883 (* goal 2 (of 2) *) 884 RW_TAC std_ss [CART_EQ, FCP_BETA] \\ 885 REWRITE_TAC [FCP_CONCAT_def, index_comp] >> simp [index_sum] ] 886QED 887 888Theorem FCP_CONCAT_11 : (* added by Chun Tian *) 889 !(a :'a['b]) (b :'a['c]) c d. 890 FINITE univ(:'b) /\ FINITE univ(:'c) /\ 891 (FCP_CONCAT a b = FCP_CONCAT c d) ==> (a = c) /\ (b = d) 892Proof 893 METIS_TAC [FCP_CONCAT_THM] 894QED 895 896(* ------------------------------------------------------------------------- *) 897 898val () = export_theory() 899