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