1open HolKernel boolLib bossLib stringTheory arithmeticTheory pred_setTheory finite_mapTheory prim_recTheory
2val _ = new_theory "commonUnif";
3
4val _ = Hol_datatype `
5  const = Null
6        | Bool of bool
7        | Num of num
8        | String of string`;
9
10val extension_chain = Q.store_thm(
11"extension_chain",
12`!subst source z.
13  (((FINITE (source z)) /\
14    (!m n. m < n ==> (subst m) SUBMAP (subst n)) /\
15    (!n. DISJOINT (FDOM (subst n)) (source n)) /\
16    (!n. z < n ==> (FDOM (subst n) UNION (source n) = FDOM (subst z) UNION (source z))))
17    ==> ?x. !n. x < n ==> ((subst n) = (subst x)))`,
18SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
19Q_TAC SUFF_TAC
20`!m. z <= m ==> ?n.m < n /\ CARD(source n) < CARD(source m)`
21THEN1
22(DISCH_THEN
23 (STRIP_ASSUME_TAC o SIMP_RULE (srw_ss()) [SKOLEM_THM,GSYM RIGHT_EXISTS_IMP_THM]) THEN
24`?ff.!n.ff (SUC n) < ff n`
25    by (Q.EXISTS_TAC `\n.CARD(source(FUNPOW f n z))` THEN
26        SRW_TAC [][FUNPOW_SUC] THEN
27        Q_TAC SUFF_TAC `z <= FUNPOW f n z` THEN1 METIS_TAC [] THEN
28        Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC] THEN
29        RES_TAC THEN DECIDE_TAC) THEN
30METIS_TAC [WF_LESS,WF_IFF_WELLFOUNDED,wellfounded_def]) THEN
31REPEAT STRIP_TAC THEN
32`?n.m < n /\ subst m <> subst n` by METIS_TAC [] THEN
33Q.EXISTS_TAC `n` THEN
34`z < n` by DECIDE_TAC THEN
35`(FDOM (subst n) UNION source n = FDOM (subst m) UNION source m) /\
36 FINITE (source m) /\ FINITE (source n)`
37   by METIS_TAC [LESS_OR_EQ,FINITE_UNION,FDOM_FINITE] THEN
38`subst m SUBMAP subst n` by METIS_TAC [] THEN
39`FDOM (subst m) PSUBSET FDOM (subst n)` by METIS_TAC [SUBMAP_DEF,SUBSET_DEF,PSUBSET_DEF,EQ_FDOM_SUBMAP] THEN
40`(CARD (FDOM (subst n) UNION source n) = CARD (FDOM (subst n)) + CARD (source n)) /\
41 (CARD (FDOM (subst m) UNION source m) = CARD (FDOM (subst m)) + CARD (source m)) /\
42 (CARD (FDOM (subst m) UNION source m) = CARD (FDOM (subst n) UNION source n))` by
43  METIS_TAC [CARD_UNION,ADD_0,DISJOINT_DEF,CARD_EMPTY,FDOM_FINITE] THEN
44`CARD (FDOM (subst m)) < CARD (FDOM (subst n))` by METIS_TAC [CARD_PSUBSET,FDOM_FINITE]
45THEN DECIDE_TAC)
46
47val _ = export_theory ();
48