cart.ml

   1 (* ========================================================================= *)
   2 (* Definition of finite Cartesian product types.                             *)
   3 (*                                                                           *)
   4 (*              (c) Copyright, John Harrison 1998-2007                       *)
   5 (* ========================================================================= *)
   6
   7 needs "iterate.ml";;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Association of a number with an indexing type.                            *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let dimindex = new_definition
  14   `dimindex(s:A->bool) = if FINITE(:A) then CARD(:A) else 1`;;
  15
  16 let DIMINDEX_NONZERO = prove
  17  (`!s:A->bool. ~(dimindex(s) = 0)`,
  18   GEN_TAC THEN REWRITE_TAC[dimindex] THEN
  19   COND_CASES_TAC THEN ASM_SIMP_TAC[CARD_EQ_0; ARITH] THEN SET_TAC[]);;
  20
  21 let DIMINDEX_GE_1 = prove
  22  (`!s:A->bool. 1 <= dimindex(s)`,
  23   REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`; DIMINDEX_NONZERO]);;
  24
  25 let DIMINDEX_UNIV = prove
  26  (`!s. dimindex(s:A->bool) = dimindex(:A)`,
  27   REWRITE_TAC[dimindex]);;
  28
  29 let DIMINDEX_UNIQUE = prove
  30  (`(:A) HAS_SIZE n ==> dimindex(:A) = n`,
  31   MESON_TAC[dimindex; HAS_SIZE]);;
  32
  33 (* ------------------------------------------------------------------------- *)
  34 (* An indexing type with that size, parametrized by base type.               *)
  35 (* ------------------------------------------------------------------------- *)
  36
  37 let finite_image_tybij =
  38   new_type_definition "finite_image" ("finite_index","dest_finite_image")
  39   (prove
  40    (`?x. x IN 1..dimindex(:A)`,
  41     EXISTS_TAC `1` THEN REWRITE_TAC[IN_NUMSEG; LE_REFL; DIMINDEX_GE_1]));;
  42
  43 let FINITE_IMAGE_IMAGE = prove
  44  (`UNIV:(A)finite_image->bool = IMAGE finite_index (1..dimindex(:A))`,
  45   REWRITE_TAC[EXTENSION; IN_UNIV; IN_IMAGE] THEN
  46   MESON_TAC[finite_image_tybij]);;
  47
  48 (* ------------------------------------------------------------------------- *)
  49 (* Dimension of such a type, and indexing over it.                           *)
  50 (* ------------------------------------------------------------------------- *)
  51
  52 let HAS_SIZE_FINITE_IMAGE = prove
  53  (`!s. (UNIV:(A)finite_image->bool) HAS_SIZE dimindex(s:A->bool)`,
  54   GEN_TAC THEN SIMP_TAC[FINITE_IMAGE_IMAGE] THEN
  55   MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN
  56   ONCE_REWRITE_TAC[DIMINDEX_UNIV] THEN REWRITE_TAC[HAS_SIZE_NUMSEG_1] THEN
  57   MESON_TAC[finite_image_tybij]);;
  58
  59 let CARD_FINITE_IMAGE = prove
  60  (`!s. CARD(UNIV:(A)finite_image->bool) = dimindex(s:A->bool)`,
  61   MESON_TAC[HAS_SIZE_FINITE_IMAGE; HAS_SIZE]);;
  62
  63 let FINITE_FINITE_IMAGE = prove
  64  (`FINITE(UNIV:(A)finite_image->bool)`,
  65   MESON_TAC[HAS_SIZE_FINITE_IMAGE; HAS_SIZE]);;
  66
  67 let DIMINDEX_FINITE_IMAGE = prove
  68  (`!s t. dimindex(s:(A)finite_image->bool) = dimindex(t:A->bool)`,
  69   REPEAT GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [dimindex] THEN
  70   MP_TAC(ISPEC `t:A->bool` HAS_SIZE_FINITE_IMAGE) THEN
  71   SIMP_TAC[FINITE_FINITE_IMAGE; HAS_SIZE]);;
  72
  73 let FINITE_INDEX_WORKS = prove
  74  (`!i:(A)finite_image.
  75         ?!n. 1 <= n /\ n <= dimindex(:A) /\ (finite_index n = i)`,
  76   REWRITE_TAC[CONJ_ASSOC; GSYM IN_NUMSEG] THEN MESON_TAC[finite_image_tybij]);;
  77
  78 let FINITE_INDEX_INJ = prove
  79  (`!i j. 1 <= i /\ i <= dimindex(:A) /\
  80          1 <= j /\ j <= dimindex(:A)
  81          ==> ((finite_index i :A finite_image = finite_index j) <=>
  82               (i = j))`,
  83   MESON_TAC[FINITE_INDEX_WORKS]);;
  84
  85 let FORALL_FINITE_INDEX = prove
  86  (`(!k:(N)finite_image. P k) =
  87    (!i. 1 <= i /\ i <= dimindex(:N) ==> P(finite_index i))`,
  88   MESON_TAC[FINITE_INDEX_WORKS]);;
  89
  90 (* ------------------------------------------------------------------------- *)
  91 (* Hence finite Cartesian products, with indexing and lambdas.               *)
  92 (* ------------------------------------------------------------------------- *)
  93
  94 let cart_tybij =
  95   new_type_definition "cart" ("mk_cart","dest_cart")
  96    (prove(`?f:(B)finite_image->A. T`,REWRITE_TAC[]));;
  97
  98 parse_as_infix("$",(25,"left"));;
  99
 100 let finite_index = new_definition
 101   `x$i = dest_cart x (finite_index i)`;;
 102
 103 let CART_EQ = prove
 104  (`!x:A^B y.
 105     (x = y) <=> !i. 1 <= i /\ i <= dimindex(:B) ==> (x$i = y$i)`,
 106   REPEAT GEN_TAC THEN REWRITE_TAC[finite_index; GSYM FORALL_FINITE_INDEX] THEN
 107   REWRITE_TAC[GSYM FUN_EQ_THM; ETA_AX] THEN MESON_TAC[cart_tybij]);;
 108
 109 parse_as_binder "lambda";;
 110
 111 let lambda = new_definition
 112   `(lambda) g =
 113      @f:A^B. !i. 1 <= i /\ i <= dimindex(:B) ==> (f$i = g i)`;;
 114
 115 let LAMBDA_BETA = prove
 116  (`!i. 1 <= i /\ i <= dimindex(:B)
 117        ==> (((lambda) g:A^B) $i = g i)`,
 118   REWRITE_TAC[lambda] THEN CONV_TAC SELECT_CONV THEN
 119   EXISTS_TAC `mk_cart(\k. g(@i. 1 <= i /\  i <= dimindex(:B) /\
 120                                 (finite_index i = k))):A^B` THEN
 121   REWRITE_TAC[finite_index; REWRITE_RULE[] cart_tybij] THEN
 122   REPEAT STRIP_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC SELECT_UNIQUE THEN
 123   GEN_TAC THEN REWRITE_TAC[] THEN
 124   ASM_MESON_TAC[FINITE_INDEX_INJ; DIMINDEX_FINITE_IMAGE]);;
 125
 126 let LAMBDA_UNIQUE = prove
 127  (`!f:A^B g.
 128         (!i. 1 <= i /\ i <= dimindex(:B) ==> (f$i = g i)) <=>
 129         ((lambda) g = f)`,
 130   SIMP_TAC[CART_EQ; LAMBDA_BETA] THEN MESON_TAC[]);;
 131
 132 let LAMBDA_ETA = prove
 133  (`!g. (lambda i. g$i) = g`,
 134   REWRITE_TAC[CART_EQ; LAMBDA_BETA]);;
 135
 136 (* ------------------------------------------------------------------------- *)
 137 (* For some purposes we can avoid side-conditions on the index.              *)
 138 (* ------------------------------------------------------------------------- *)
 139
 140 let FINITE_INDEX_INRANGE = prove
 141  (`!i. ?k. 1 <= k /\ k <= dimindex(:N) /\ !x:A^N. x$i = x$k`,
 142   REWRITE_TAC[finite_index] THEN MESON_TAC[FINITE_INDEX_WORKS]);;
 143
 144 let FINITE_INDEX_INRANGE_2 = prove
 145  (`!i. ?k. 1 <= k /\ k <= dimindex(:N) /\
 146            (!x:A^N. x$i = x$k) /\ (!y:B^N. y$i = y$k)`,
 147   REWRITE_TAC[finite_index] THEN MESON_TAC[FINITE_INDEX_WORKS]);;
 148
 149 let CART_EQ_FULL = prove
 150  (`!x y:A^N. x = y <=> !i. x$i = y$i`,
 151   REPEAT GEN_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN SIMP_TAC[CART_EQ]);;
 152
 153 (* ------------------------------------------------------------------------- *)
 154 (* We need a non-standard sum to "paste" together Cartesian products.        *)
 155 (* ------------------------------------------------------------------------- *)
 156
 157 let finite_sum_tybij =
 158   let th = prove
 159    (`?x. x IN 1..(dimindex(:A) + dimindex(:B))`,
 160     EXISTS_TAC `1` THEN SIMP_TAC[IN_NUMSEG; LE_REFL; DIMINDEX_GE_1;
 161       ARITH_RULE `1 <= a ==> 1 <= a + b`]) in
 162   new_type_definition "finite_sum" ("mk_finite_sum","dest_finite_sum") th;;
 163
 164 let pastecart = new_definition
 165   `(pastecart:A^M->A^N->A^(M,N)finite_sum) f g =
 166         lambda i. if i <= dimindex(:M) then f$i
 167                   else g$(i - dimindex(:M))`;;
 168
 169 let fstcart = new_definition
 170   `(fstcart:A^(M,N)finite_sum->A^M) f = lambda i. f$i`;;
 171
 172 let sndcart = new_definition
 173   `(sndcart:A^(M,N)finite_sum->A^N) f =
 174         lambda i. f$(i + dimindex(:M))`;;
 175
 176 let FINITE_SUM_IMAGE = prove
 177  (`UNIV:(A,B)finite_sum->bool =
 178        IMAGE mk_finite_sum (1..(dimindex(:A)+dimindex(:B)))`,
 179   REWRITE_TAC[EXTENSION; IN_UNIV; IN_IMAGE] THEN
 180   MESON_TAC[finite_sum_tybij]);;
 181
 182 let DIMINDEX_HAS_SIZE_FINITE_SUM = prove
 183  (`(UNIV:(M,N)finite_sum->bool) HAS_SIZE (dimindex(:M) + dimindex(:N))`,
 184   SIMP_TAC[FINITE_SUM_IMAGE] THEN
 185   MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN
 186   ONCE_REWRITE_TAC[DIMINDEX_UNIV] THEN REWRITE_TAC[HAS_SIZE_NUMSEG_1] THEN
 187   MESON_TAC[finite_sum_tybij]);;
 188
 189 let DIMINDEX_FINITE_SUM = prove
 190  (`dimindex(:(M,N)finite_sum) = dimindex(:M) + dimindex(:N)`,
 191   GEN_REWRITE_TAC LAND_CONV [dimindex] THEN
 192   REWRITE_TAC[REWRITE_RULE[HAS_SIZE] DIMINDEX_HAS_SIZE_FINITE_SUM]);;
 193
 194 let FSTCART_PASTECART = prove
 195  (`!x y. fstcart(pastecart (x:A^M) (y:A^N)) = x`,
 196   SIMP_TAC[pastecart; fstcart; CART_EQ; LAMBDA_BETA; DIMINDEX_FINITE_SUM;
 197            ARITH_RULE `a <= b ==> a <= b + c`]);;
 198
 199 let SNDCART_PASTECART = prove
 200  (`!x y. sndcart(pastecart (x:A^M) (y:A^N)) = y`,
 201   SIMP_TAC[pastecart; sndcart; CART_EQ; LAMBDA_BETA] THEN REPEAT STRIP_TAC THEN
 202   W(fun (_,w) -> MP_TAC (PART_MATCH (lhs o rand) LAMBDA_BETA (lhand w))) THEN
 203   ANTS_TAC THENL
 204    [REWRITE_TAC[DIMINDEX_FINITE_SUM] THEN MATCH_MP_TAC
 205      (ARITH_RULE `1 <= i /\ i <= b ==> 1 <= i + a /\ i + a <= a + b`) THEN
 206     ASM_REWRITE_TAC[];
 207     DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[] THEN
 208     ASM_SIMP_TAC[ADD_SUB; ARITH_RULE `1 <= i ==> ~(i + a <= a)`]]);;
 209
 210 let PASTECART_FST_SND = prove
 211  (`!z. pastecart (fstcart z) (sndcart z) = z`,
 212   SIMP_TAC[pastecart; fstcart; sndcart; CART_EQ; LAMBDA_BETA] THEN
 213   REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 214   ASM_SIMP_TAC[DIMINDEX_FINITE_SUM; LAMBDA_BETA;
 215      ARITH_RULE `i <= a + b ==> i - a <= b`;
 216      ARITH_RULE `~(i <= a) ==> 1 <= i - a`;
 217      ARITH_RULE `~(i <= a) ==> ((i - a) + a = i)`]);;
 218
 219 let PASTECART_EQ = prove
 220  (`!x y. (x = y) <=> (fstcart x = fstcart y) /\ (sndcart x = sndcart y)`,
 221   MESON_TAC[PASTECART_FST_SND]);;
 222
 223 let FORALL_PASTECART = prove
 224  (`(!p. P p) <=> !x y. P (pastecart x y)`,
 225   MESON_TAC[PASTECART_FST_SND; FSTCART_PASTECART; SNDCART_PASTECART]);;
 226
 227 let EXISTS_PASTECART = prove
 228  (`(?p. P p) <=> ?x y. P (pastecart x y)`,
 229   MESON_TAC[PASTECART_FST_SND; FSTCART_PASTECART; SNDCART_PASTECART]);;
 230
 231 let PASTECART_INJ = prove
 232  (`!x:real^M y:real^N w z. pastecart x y = pastecart w z <=> x = w /\ y = z`,
 233   REWRITE_TAC[PASTECART_EQ; FSTCART_PASTECART; SNDCART_PASTECART]);;
 234
 235 (* ------------------------------------------------------------------------- *)
 236 (* Automatically define a type of size n.                                    *)
 237 (* ------------------------------------------------------------------------- *)
 238
 239 let define_finite_type =
 240   let lemma_pre = prove
 241    (`~(n = 0) ==> ?x. x IN 1..n`,
 242     DISCH_TAC THEN EXISTS_TAC `1` THEN REWRITE_TAC[IN_NUMSEG] THEN
 243     POP_ASSUM MP_TAC THEN ARITH_TAC)
 244   and lemma_post = prove
 245    (`(!a:A. mk(dest a) = a) /\ (!r. r IN 1..n <=> dest(mk r) = r)
 246      ==> (:A) HAS_SIZE n`,
 247     REPEAT STRIP_TAC THEN
 248     SUBGOAL_THEN `(:A) = IMAGE mk (1..n)` SUBST1_TAC THENL
 249      [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_UNIV];
 250       MATCH_MP_TAC HAS_SIZE_IMAGE_INJ] THEN
 251     ASM_MESON_TAC[HAS_SIZE_NUMSEG_1]) in
 252   let POST_RULE = MATCH_MP lemma_post and n_tm = `n:num` in
 253   fun n ->
 254     let ns = string_of_int n in
 255     let ns' = "auto_define_finite_type_"^ns in
 256     let th0 = INST [mk_small_numeral n,n_tm] lemma_pre in
 257     let th1 = MP th0 (EQF_ELIM(NUM_EQ_CONV(rand(lhand(concl th0))))) in
 258     POST_RULE(new_type_definition ns ("mk_"^ns',"dest_"^ns') th1);;
 259
 260 (* ------------------------------------------------------------------------- *)
 261 (* Predefine the cases 2, 3 and 4, which are especially useful for real^N.   *)
 262 (* ------------------------------------------------------------------------- *)
 263
 264 let HAS_SIZE_1 = prove
 265  (`(:1) HAS_SIZE 1`,
 266   SUBGOAL_THEN `(:1) = {one}` SUBST1_TAC THENL
 267    [REWRITE_TAC[EXTENSION; IN_UNIV; IN_SING] THEN MESON_TAC[one];
 268     SIMP_TAC[NOT_IN_EMPTY; HAS_SIZE; FINITE_RULES; CARD_CLAUSES; ARITH]]);;
 269
 270 let HAS_SIZE_2 = define_finite_type 2;;
 271
 272 let HAS_SIZE_3 = define_finite_type 3;;
 273
 274 let HAS_SIZE_4 = define_finite_type 4;;
 275
 276 let DIMINDEX_1 = MATCH_MP DIMINDEX_UNIQUE HAS_SIZE_1;;
 277 let DIMINDEX_2 = MATCH_MP DIMINDEX_UNIQUE HAS_SIZE_2;;
 278 let DIMINDEX_3 = MATCH_MP DIMINDEX_UNIQUE HAS_SIZE_3;;
 279 let DIMINDEX_4 = MATCH_MP DIMINDEX_UNIQUE HAS_SIZE_4;;
 280
 281 (* ------------------------------------------------------------------------- *)
 282 (* Finiteness lemma.                                                         *)
 283 (* ------------------------------------------------------------------------- *)
 284
 285 let FINITE_CART = prove
 286  (`!P. (!i. 1 <= i /\ i <= dimindex(:N) ==> FINITE {x | P i x})
 287        ==> FINITE {v:A^N | !i. 1 <= i /\ i <= dimindex(:N) ==> P i (v$i)}`,
 288   GEN_TAC THEN DISCH_TAC THEN
 289   SUBGOAL_THEN
 290    `!n. n <= dimindex(:N)
 291         ==> FINITE {v:A^N | (!i. 1 <= i /\ i <= dimindex(:N) /\ i <= n
 292                                  ==> P i (v$i)) /\
 293                             (!i. 1 <= i /\ i <= dimindex(:N) /\ n < i
 294                                  ==> v$i = @x. F)}`
 295    (MP_TAC o SPEC `dimindex(:N)`) THEN REWRITE_TAC[LE_REFL; LET_ANTISYM] THEN
 296   INDUCT_TAC THENL
 297    [REWRITE_TAC[ARITH_RULE `1 <= i /\ i <= n /\ i <= 0 <=> F`] THEN
 298     SIMP_TAC[ARITH_RULE `1 <= i /\ i <= n /\ 0 < i <=> 1 <= i /\ i <= n`] THEN
 299     SUBGOAL_THEN
 300      `{v | !i. 1 <= i /\ i <= dimindex (:N) ==> v$i = (@x. F)} =
 301       {(lambda i. @x. F):A^N}`
 302      (fun th -> SIMP_TAC[FINITE_RULES;th]) THEN
 303     SIMP_TAC[EXTENSION; IN_SING; IN_ELIM_THM; CART_EQ; LAMBDA_BETA];
 304     ALL_TAC] THEN
 305   DISCH_TAC THEN
 306   MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC
 307    `IMAGE (\(x:A,v:A^N). (lambda i. if i = SUC n then x else v$i):A^N)
 308           {x,v | x IN {x:A | P (SUC n) x} /\
 309                  v IN {v:A^N | (!i. 1 <= i /\ i <= dimindex(:N) /\ i <= n
 310                                 ==> P i (v$i)) /\
 311                            (!i. 1 <= i /\ i <= dimindex (:N) /\ n < i
 312                                 ==> v$i = (@x. F))}}` THEN
 313   CONJ_TAC THENL
 314    [MATCH_MP_TAC FINITE_IMAGE THEN
 315     ASM_SIMP_TAC[FINITE_PRODUCT; ARITH_RULE `1 <= SUC n`;
 316                  ARITH_RULE `SUC n <= m ==> n <= m`];
 317     ALL_TAC] THEN
 318   REWRITE_TAC[SUBSET; IN_IMAGE; IN_ELIM_PAIR_THM; EXISTS_PAIR_THM] THEN
 319   X_GEN_TAC `v:A^N` THEN REWRITE_TAC[IN_ELIM_THM] THEN
 320   STRIP_TAC THEN EXISTS_TAC `(v:A^N)$(SUC n)` THEN
 321   EXISTS_TAC `(lambda i. if i = SUC n then @x. F else (v:A^N)$i):A^N` THEN
 322   SIMP_TAC[CART_EQ; LAMBDA_BETA; ARITH_RULE `i <= n ==> ~(i = SUC n)`] THEN
 323   ASM_MESON_TAC[LE; ARITH_RULE `1 <= SUC n`;
 324                 ARITH_RULE `n < i /\ ~(i = SUC n) ==> SUC n < i`]);;
 325
 326 (* ------------------------------------------------------------------------- *)
 327 (* More cardinality results for whole universe.                              *)
 328 (* ------------------------------------------------------------------------- *)
 329
 330 let HAS_SIZE_CART_UNIV = prove
 331  (`!m. (:A) HAS_SIZE m ==> (:A^N) HAS_SIZE m EXP (dimindex(:N))`,
 332   REPEAT STRIP_TAC THEN
 333   SUBGOAL_THEN
 334    `(:(N)finite_image->A) HAS_SIZE m EXP (dimindex(:N))`
 335   MP_TAC THENL
 336    [ASM_SIMP_TAC[HAS_SIZE_FUNSPACE_UNIV; HAS_SIZE_FINITE_IMAGE];
 337     DISCH_THEN(MP_TAC o ISPEC `mk_cart:((N)finite_image->A)->A^N` o
 338       MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT] HAS_SIZE_IMAGE_INJ)) THEN
 339     REWRITE_TAC[IN_UNIV] THEN
 340     ANTS_TAC THENL [MESON_TAC[cart_tybij]; MATCH_MP_TAC EQ_IMP] THEN
 341     AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC SURJECTIVE_IMAGE_EQ THEN
 342     REWRITE_TAC[IN_UNIV] THEN MESON_TAC[cart_tybij]]);;
 343
 344 let CARD_CART_UNIV = prove
 345  (`FINITE(:A) ==> CARD(:A^N) = CARD(:A) EXP dimindex(:N)`,
 346   MESON_TAC[HAS_SIZE_CART_UNIV; HAS_SIZE]);;
 347
 348 let FINITE_CART_UNIV = prove
 349  (`FINITE(:A) ==> FINITE(:A^N)`,
 350   MESON_TAC[HAS_SIZE_CART_UNIV; HAS_SIZE]);;
 351
 352 (* ------------------------------------------------------------------------- *)
 353 (* Explicit construction of a vector from a list of components.              *)
 354 (* ------------------------------------------------------------------------- *)
 355
 356 let vector = new_definition
 357   `(vector l):A^N = lambda i. EL (i - 1) l`;;
 358
 359 (* ------------------------------------------------------------------------- *)
 360 (* Convenient set membership elimination theorem.                            *)
 361 (* ------------------------------------------------------------------------- *)
 362
 363 let IN_ELIM_PASTECART_THM = prove
 364  (`!P a b. pastecart a b IN {pastecart x y | P x y} <=> P a b`,
 365   REWRITE_TAC[IN_ELIM_THM; PASTECART_EQ;
 366               FSTCART_PASTECART; SNDCART_PASTECART] THEN
 367   MESON_TAC[]);;
 368
 369 (* ------------------------------------------------------------------------- *)
 370 (* Variant of product types using pasting of vectors.                        *)
 371 (* ------------------------------------------------------------------------- *)
 372
 373 parse_as_infix("PCROSS",(22,"right"));;
 374
 375 let PCROSS = new_definition
 376  `s PCROSS t = {pastecart (x:A^M) (y:A^N) | x IN s /\ y IN t}`;;
 377
 378 let FORALL_IN_PCROSS = prove
 379  (`(!z. z IN s PCROSS t ==> P z) <=>
 380    (!x y. x IN s /\ y IN t ==> P(pastecart x y))`,
 381   REWRITE_TAC[PCROSS; FORALL_IN_GSPEC]);;
 382
 383 let EXISTS_IN_PCROSS = prove
 384  (`(?z. z IN s PCROSS t /\ P z) <=>
 385    (?x y. x IN s /\ y IN t /\ P(pastecart x y))`,
 386   REWRITE_TAC[PCROSS; EXISTS_IN_GSPEC; CONJ_ASSOC]);;
 387
 388 let PASTECART_IN_PCROSS = prove
 389  (`!s t x y. (pastecart x y) IN (s PCROSS t) <=> x IN s /\ y IN t`,
 390   REWRITE_TAC[PCROSS; IN_ELIM_PASTECART_THM]);;
 391
 392 let PCROSS_EQ_EMPTY = prove
 393  (`!s t. s PCROSS t = {} <=> s = {} \/ t = {}`,
 394   REWRITE_TAC[PCROSS] THEN SET_TAC[]);;
 395
 396 let PCROSS_EMPTY = prove
 397  (`(!s. s PCROSS {} = {}) /\ (!t. {} PCROSS t = {})`,
 398   REWRITE_TAC[PCROSS_EQ_EMPTY]);;
 399
 400 let SUBSET_PCROSS = prove
 401  (`!s t s' t'. s PCROSS t SUBSET s' PCROSS t' <=>
 402                 s = {} \/ t = {} \/ s SUBSET s' /\ t SUBSET t'`,
 403   SIMP_TAC[PCROSS; EXTENSION; IN_ELIM_PASTECART_THM; SUBSET;
 404    FORALL_PASTECART; PASTECART_IN_PCROSS; NOT_IN_EMPTY] THEN MESON_TAC[]);;
 405
 406 let PCROSS_MONO = prove
 407  (`!s t s' t'. s SUBSET s' /\ t SUBSET t' ==> s PCROSS t SUBSET s' PCROSS t'`,
 408   SIMP_TAC[SUBSET_PCROSS]);;
 409
 410 let PCROSS_EQ = prove
 411  (`!s s':real^M->bool t t':real^N->bool.
 412         s PCROSS t = s' PCROSS t' <=>
 413         (s = {} \/ t = {}) /\ (s' = {} \/ t' = {}) \/ s = s' /\ t = t'`,
 414   REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ; SUBSET_PCROSS] THEN SET_TAC[]);;
 415
 416 let UNIV_PCROSS_UNIV = prove
 417  (`(:A^M) PCROSS (:A^N) = (:A^(M,N)finite_sum)`,
 418   REWRITE_TAC[EXTENSION; FORALL_PASTECART; PASTECART_IN_PCROSS; IN_UNIV]);;
 419
 420 let HAS_SIZE_PCROSS = prove
 421  (`!(s:A^M->bool) (t:A^N->bool) m n.
 422         s HAS_SIZE m /\ t HAS_SIZE n ==> (s PCROSS t) HAS_SIZE (m * n)`,
 423   REPEAT GEN_TAC THEN DISCH_TAC THEN
 424   FIRST_ASSUM(MP_TAC o MATCH_MP HAS_SIZE_PRODUCT) THEN
 425   MATCH_MP_TAC EQ_IMP THEN SPEC_TAC(`m * n:num`,`k:num`) THEN
 426   MATCH_MP_TAC BIJECTIONS_HAS_SIZE_EQ THEN
 427   EXISTS_TAC `\(x:A^M,y:A^N). pastecart x y` THEN
 428   EXISTS_TAC `\z:A^(M,N)finite_sum. fstcart z,sndcart z` THEN
 429   REWRITE_TAC[FORALL_IN_GSPEC; PASTECART_IN_PCROSS] THEN
 430   REWRITE_TAC[IN_ELIM_PAIR_THM; PASTECART_FST_SND] THEN
 431   REWRITE_TAC[FORALL_IN_PCROSS; FSTCART_PASTECART; SNDCART_PASTECART]);;
 432
 433 let FINITE_PCROSS = prove
 434  (`!(s:A^M->bool) (t:A^N->bool).
 435         FINITE s /\ FINITE t ==> FINITE(s PCROSS t)`,
 436   MESON_TAC[REWRITE_RULE[HAS_SIZE] HAS_SIZE_PCROSS]);;
 437
 438 let FINITE_PCROSS_EQ = prove
 439  (`!(s:A^M->bool) (t:A^N->bool).
 440         FINITE(s PCROSS t) <=> s = {} \/ t = {} \/ FINITE s /\ FINITE t`,
 441   REPEAT GEN_TAC THEN
 442   MAP_EVERY ASM_CASES_TAC [`s:A^M->bool = {}`; `t:A^N->bool = {}`] THEN
 443   ASM_REWRITE_TAC[PCROSS_EMPTY; FINITE_EMPTY] THEN
 444   EQ_TAC THEN SIMP_TAC[FINITE_PCROSS] THEN REPEAT STRIP_TAC THEN
 445   MATCH_MP_TAC FINITE_SUBSET THENL
 446    [EXISTS_TAC `IMAGE fstcart ((s PCROSS t):A^(M,N)finite_sum->bool)`;
 447     EXISTS_TAC `IMAGE sndcart ((s PCROSS t):A^(M,N)finite_sum->bool)`] THEN
 448   ASM_SIMP_TAC[FINITE_IMAGE; SUBSET; IN_IMAGE; EXISTS_PASTECART] THEN
 449   REWRITE_TAC[PASTECART_IN_PCROSS; FSTCART_PASTECART; SNDCART_PASTECART] THEN
 450   ASM SET_TAC[]);;
 451
 452 let IMAGE_FSTCART_PCROSS = prove
 453  (`!s:real^M->bool t:real^N->bool.
 454         IMAGE fstcart (s PCROSS t) = if t = {} then {} else s`,
 455   REPEAT GEN_TAC THEN COND_CASES_TAC THEN
 456   ASM_REWRITE_TAC[PCROSS_EMPTY; IMAGE_CLAUSES] THEN
 457   REWRITE_TAC[EXTENSION; IN_IMAGE] THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
 458   REWRITE_TAC[EXISTS_IN_PCROSS; FSTCART_PASTECART] THEN ASM SET_TAC[]);;
 459
 460 let IMAGE_SNDCART_PCROSS = prove
 461  (`!s:real^M->bool t:real^N->bool.
 462         IMAGE sndcart (s PCROSS t) = if s = {} then {} else t`,
 463   REPEAT GEN_TAC THEN COND_CASES_TAC THEN
 464   ASM_REWRITE_TAC[PCROSS_EMPTY; IMAGE_CLAUSES] THEN
 465   REWRITE_TAC[EXTENSION; IN_IMAGE] THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
 466   REWRITE_TAC[EXISTS_IN_PCROSS; SNDCART_PASTECART] THEN ASM SET_TAC[]);;
 467
 468 let PCROSS_INTER = prove
 469  (`(!s t u. s PCROSS (t INTER u) = (s PCROSS t) INTER (s PCROSS u)) /\
 470    (!s t u. (s INTER t) PCROSS u = (s PCROSS u) INTER (t PCROSS u))`,
 471   REWRITE_TAC[EXTENSION; FORALL_PASTECART; IN_INTER; PASTECART_IN_PCROSS] THEN
 472   REPEAT STRIP_TAC THEN CONV_TAC TAUT);;
 473
 474 let PCROSS_UNION = prove
 475  (`(!s t u. s PCROSS (t UNION u) = (s PCROSS t) UNION (s PCROSS u)) /\
 476    (!s t u. (s UNION t) PCROSS u = (s PCROSS u) UNION (t PCROSS u))`,
 477   REWRITE_TAC[EXTENSION; FORALL_PASTECART; IN_UNION; PASTECART_IN_PCROSS] THEN
 478   REPEAT STRIP_TAC THEN CONV_TAC TAUT);;
 479
 480 let PCROSS_DIFF = prove
 481  (`(!s t u. s PCROSS (t DIFF u) = (s PCROSS t) DIFF (s PCROSS u)) /\
 482    (!s t u. (s DIFF t) PCROSS u = (s PCROSS u) DIFF (t PCROSS u))`,
 483   REWRITE_TAC[EXTENSION; FORALL_PASTECART; IN_DIFF; PASTECART_IN_PCROSS] THEN
 484   REPEAT STRIP_TAC THEN CONV_TAC TAUT);;
 485
 486 let INTER_PCROSS = prove
 487  (`!s s' t t'.
 488       (s PCROSS t) INTER (s' PCROSS t') = (s INTER s') PCROSS (t INTER t')`,
 489   REWRITE_TAC[EXTENSION; IN_INTER; FORALL_PASTECART; PASTECART_IN_PCROSS] THEN
 490   CONV_TAC TAUT);;
 491
 492 let PCROSS_UNIONS_UNIONS,PCROSS_UNIONS = (CONJ_PAIR o prove)
 493  (`(!f g. (UNIONS f) PCROSS (UNIONS g) =
 494           UNIONS {s PCROSS t | s IN f /\ t IN g}) /\
 495    (!s f. s PCROSS (UNIONS f) = UNIONS {s PCROSS t | t IN f}) /\
 496    (!f t. (UNIONS f) PCROSS t = UNIONS {s PCROSS t | s IN f})`,
 497   REWRITE_TAC[UNIONS_GSPEC; EXTENSION; FORALL_PASTECART; IN_ELIM_THM;
 498               PASTECART_IN_PCROSS] THEN
 499   SET_TAC[]);;