Hi Abid,
| I was going through the theory and found finite_sum, which is the addition
| of dimensions, but here i need product or multiplication of dimensions. Can
| anyone help me out please.
I think the following should work --- I should probably add it to the system
as it might be useful for others too.
let finite_prod_tybij =
let th = prove
(`?x. x IN 1..(dimindex(:A) * dimindex(:B))`,
EXISTS_TAC `1` THEN REWRITE_TAC[IN_NUMSEG; LE_REFL] THEN
MESON_TAC[LE_1; DIMINDEX_GE_1; MULT_EQ_0]) in
new_type_definition "finite_prod" ("mk_finite_prod","dest_finite_prod") th;;
let FINITE_PROD_IMAGE = prove
(`UNIV:(A,B)finite_prod->bool =
IMAGE mk_finite_prod (1..(dimindex(:A)*dimindex(:B)))`,
REWRITE_TAC[EXTENSION; IN_UNIV; IN_IMAGE] THEN
MESON_TAC[finite_prod_tybij]);;
let DIMINDEX_HAS_SIZE_FINITE_PROD = prove
(`(UNIV:(M,N)finite_prod->bool) HAS_SIZE (dimindex(:M) * dimindex(:N))`,
SIMP_TAC[FINITE_PROD_IMAGE] THEN
MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN
ONCE_REWRITE_TAC[DIMINDEX_UNIV] THEN REWRITE_TAC[HAS_SIZE_NUMSEG_1] THEN
MESON_TAC[finite_prod_tybij]);;
let DIMINDEX_FINITE_PROD = prove
(`dimindex(:(M,N)finite_prod) = dimindex(:M) * dimindex(:N)`,
GEN_REWRITE_TAC LAND_CONV [dimindex] THEN
REWRITE_TAC[REWRITE_RULE[HAS_SIZE] DIMINDEX_HAS_SIZE_FINITE_PROD]);;
John.
------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
