(* ========================================================================= *)
(* Definition of finite Cartesian product types. *)
(* *)
(* (c) Copyright, John Harrison 1998-2007 *)
(* ========================================================================= *)
needs "iterate.ml";;
(* ------------------------------------------------------------------------- *)
(* Association of a number with an indexing type. *)
(* ------------------------------------------------------------------------- *)
let DIMINDEX_NONZERO = prove
(`!s:A->bool. ~(dimindex(s) = 0)`,
GEN_TAC THEN REWRITE_TAC[dimindex] THEN
COND_CASES_TAC THEN ASM_SIMP_TAC[
CARD_EQ_0; ARITH] THEN SET_TAC[]);;
let CART_EQ = prove
(`!x:A^B y.
(x = y) <=> !i. 1 <= i /\ i <= dimindex(:B) ==> (x$i = y$i)`,
let LAMBDA_UNIQUE = prove
(`!f:A^B g.
(!i. 1 <= i /\ i <= dimindex(:B) ==> (f$i = g i)) <=>
((lambda) g = f)`,
let th = prove
(`?x. x
IN 1..(dimindex(:A) + dimindex(:B))`,
EXISTS_TAC `1` THEN SIMP_TAC[
IN_NUMSEG;
LE_REFL;
DIMINDEX_GE_1;
ARITH_RULE `1 <= a ==> 1 <= a + b`]) in
new_type_definition "finite_sum" ("mk_finite_sum","dest_finite_sum") th;;
let SNDCART_PASTECART = prove
(`!x y. sndcart(pastecart (x:A^M) (y:A^N)) = y`,
SIMP_TAC[pastecart; sndcart;
CART_EQ;
LAMBDA_BETA] THEN REPEAT STRIP_TAC THEN
W(fun (_,w) -> MP_TAC (PART_MATCH (lhs o rand)
LAMBDA_BETA (lhand w))) THEN
ANTS_TAC THENL
[REWRITE_TAC[
DIMINDEX_FINITE_SUM] THEN MATCH_MP_TAC
(ARITH_RULE `1 <= i /\ i <= b ==> 1 <= i + a /\ i + a <= a + b`) THEN
ASM_REWRITE_TAC[];
DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[] THEN
ASM_SIMP_TAC[
ADD_SUB; ARITH_RULE `1 <= i ==> ~(i + a <= a)`]]);;
let PASTECART_FST_SND = prove
(`!z. pastecart (fstcart z) (sndcart z) = z`,
SIMP_TAC[pastecart; fstcart; sndcart;
CART_EQ;
LAMBDA_BETA] THEN
REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_SIMP_TAC[
DIMINDEX_FINITE_SUM;
LAMBDA_BETA;
ARITH_RULE `i <= a + b ==> i - a <= b`;
ARITH_RULE `~(i <= a) ==> 1 <= i - a`;
ARITH_RULE `~(i <= a) ==> ((i - a) + a = i)`]);;
let lemma_pre = prove
(`~(n = 0) ==> ?x. x
IN 1..n`,
DISCH_TAC THEN EXISTS_TAC `1` THEN REWRITE_TAC[
IN_NUMSEG] THEN
POP_ASSUM MP_TAC THEN ARITH_TAC)
and lemma_post =
prove
(`(!a:A. mk(dest a) = a) /\ (!r. r
IN 1..n <=> dest(mk r) = r)
==> (:A)
HAS_SIZE n`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `(:A) =
IMAGE mk (1..n)` SUBST1_TAC THENL
[REWRITE_TAC[
EXTENSION;
IN_IMAGE;
IN_UNIV];
MATCH_MP_TAC
HAS_SIZE_IMAGE_INJ] THEN
ASM_MESON_TAC[
HAS_SIZE_NUMSEG_1]) in
let POST_RULE = MATCH_MP lemma_post and n_tm = `n:num` in
fun n ->
let ns = string_of_int n in
let ns' = "auto_define_finite_type_"^ns in
let th0 = INST [mk_small_numeral n,n_tm]
lemma_pre in
let th1 = MP th0 (EQF_ELIM(NUM_EQ_CONV(rand(lhand(concl th0))))) in
POST_RULE(new_type_definition ns ("mk_"^ns',"dest_"^ns') th1);;
let FINITE_CART = prove
(`!P. (!i. 1 <= i /\ i <= dimindex(:N) ==>
FINITE {x | P i x})
==>
FINITE {v:A^N | !i. 1 <= i /\ i <= dimindex(:N) ==> P i (v$i)}`,
GEN_TAC THEN DISCH_TAC THEN
SUBGOAL_THEN
`!n. n <= dimindex(:N)
==>
FINITE {v:A^N | (!i. 1 <= i /\ i <= dimindex(:N) /\ i <= n
==> P i (v$i)) /\
(!i. 1 <= i /\ i <= dimindex(:N) /\ n < i
==> v$i = @x. F)}`
(MP_TAC o SPEC `dimindex(:N)`) THEN REWRITE_TAC[
LE_REFL;
LET_ANTISYM] THEN
INDUCT_TAC THENL
[REWRITE_TAC[ARITH_RULE `1 <= i /\ i <= n /\ i <= 0 <=> F`] THEN
SIMP_TAC[ARITH_RULE `1 <= i /\ i <= n /\ 0 < i <=> 1 <= i /\ i <= n`] THEN
SUBGOAL_THEN
`{v | !i. 1 <= i /\ i <= dimindex (:N) ==> v$i = (@x. F)} =
{(lambda i. @x. F):A^N}`
(fun th -> SIMP_TAC[
FINITE_RULES;th]) THEN
SIMP_TAC[
EXTENSION;
IN_SING;
IN_ELIM_THM;
CART_EQ;
LAMBDA_BETA];
ALL_TAC] THEN
DISCH_TAC THEN
MATCH_MP_TAC
FINITE_SUBSET THEN EXISTS_TAC
`
IMAGE (\(x:A,v:A^N). (lambda i. if i = SUC n then x else v$i):A^N)
{x,v | x
IN {x:A | P (SUC n) x} /\
v
IN {v:A^N | (!i. 1 <= i /\ i <= dimindex(:N) /\ i <= n
==> P i (v$i)) /\
(!i. 1 <= i /\ i <= dimindex (:N) /\ n < i
==> v$i = (@x. F))}}` THEN
CONJ_TAC THENL
[MATCH_MP_TAC
FINITE_IMAGE THEN
ASM_SIMP_TAC[
FINITE_PRODUCT; ARITH_RULE `1 <= SUC n`;
ARITH_RULE `SUC n <= m ==> n <= m`];
ALL_TAC] THEN
REWRITE_TAC[
SUBSET;
IN_IMAGE;
IN_ELIM_PAIR_THM;
EXISTS_PAIR_THM] THEN
X_GEN_TAC `v:A^N` THEN REWRITE_TAC[
IN_ELIM_THM] THEN
STRIP_TAC THEN EXISTS_TAC `(v:A^N)$(SUC n)` THEN
EXISTS_TAC `(lambda i. if i = SUC n then @x. F else (v:A^N)$i):A^N` THEN
SIMP_TAC[
CART_EQ;
LAMBDA_BETA; ARITH_RULE `i <= n ==> ~(i = SUC n)`] THEN
ASM_MESON_TAC[
LE; ARITH_RULE `1 <= SUC n`;
ARITH_RULE `n < i /\ ~(i = SUC n) ==> SUC n < i`]);;
let PCROSS_EQ = prove
(`!s s':real^M->bool t t':real^N->bool.
s
PCROSS t = s'
PCROSS t' <=>
(s = {} \/ t = {}) /\ (s' = {} \/ t' = {}) \/ s = s' /\ t = t'`,