1open HolKernel boolLib bossLib Parse finite_mapTheory arithmeticTheory prim_recTheory pred_setTheory relationTheory ntermTheory ramanaLib 2 3val _ = new_theory "nsubst" 4 5val _ = type_abbrev ("nsubst", ``:(num |-> 'a nterm)``); 6 7val nvR_def = Define` 8 nvR s y x = case FLOOKUP s x of SOME t => y IN nvars t | _ => F`; 9 10val nwfs_def = Define`nwfs s = WF (nvR s)`; 11 12val nwfs_FEMPTY = RWstore_thm( 13"nwfs_FEMPTY", 14`nwfs FEMPTY`, 15SRW_TAC [][nwfs_def] THEN 16Q_TAC SUFF_TAC `nvR FEMPTY = EMPTY_REL` THEN1 METIS_TAC [WF_EMPTY_REL] THEN 17SRW_TAC [][FUN_EQ_THM,nvR_def]) 18 19val nwfs_no_cycles = Q.store_thm( 20 "nwfs_no_cycles", 21 `nwfs s <=> !v. ~(nvR s)^+ v v`, 22 EQ_TAC THEN1 METIS_TAC [WF_TC,nwfs_def,WF_NOT_REFL] THEN 23 SRW_TAC [] [nwfs_def,WF_IFF_WELLFOUNDED,wellfounded_def] THEN 24 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 25 `!n. (f n) IN FDOM s /\ f (SUC n) IN nvars (s ' (f n))` by 26 (STRIP_TAC THEN Q.PAT_X_ASSUM `!n.nvR s (f (SUC n)) (f n)` (Q.SPEC_THEN `n` MP_TAC) 27 THEN FULL_SIMP_TAC (srw_ss()) [nvR_def] THEN Cases_on `FLOOKUP s (f n)` THEN 28 Q.PAT_X_ASSUM `FLOOKUP s (f n) = Z` MP_TAC THEN SRW_TAC [] [FLOOKUP_DEF]) 29 THEN 30 `!n m. (nvR s)^+ (f (SUC (n + m))) (f n)` by 31 (REPEAT STRIP_TAC THEN Induct_on `m` THEN1 32 (SRW_TAC [] [] THEN METIS_TAC [TC_SUBSET]) THEN 33 Q.PAT_X_ASSUM `!n. f n IN FDOM s /\ Z` (Q.SPEC_THEN `SUC (n + m)` MP_TAC) 34 THEN SRW_TAC [] [] THEN 35 `(nvR s) (f (SUC (SUC (n + m)))) (f (SUC (n + m)))` 36 by METIS_TAC [nvR_def,FLOOKUP_DEF] THEN 37 METIS_TAC [TC_RULES,ADD_SUC]) 38 THEN 39 `?n m. f (SUC (n + m)) = f n` by 40 (`~INJ f (count (SUC (CARD (FDOM s)))) (FDOM s)` 41 by (SRW_TAC [] [PHP,CARD_COUNT,COUNT_SUC,CARD_DEF]) THEN 42 FULL_SIMP_TAC (srw_ss()) [INJ_DEF] THEN1 METIS_TAC [] THEN 43 ASSUME_TAC (Q.SPECL [`x`,`y`] LESS_LESS_CASES) THEN 44 FULL_SIMP_TAC (srw_ss()) [] THEN1 METIS_TAC [] THENL [ 45 Q.EXISTS_TAC `x` THEN Q.EXISTS_TAC `y - x - 1`, 46 Q.EXISTS_TAC `y` THEN Q.EXISTS_TAC `x - y - 1` 47 ] THEN SRW_TAC [ARITH_ss] [ADD1]) 48 THEN METIS_TAC []); 49 50val nwfs_SUBMAP = Q.store_thm( 51"nwfs_SUBMAP", 52`nwfs sx /\ s SUBMAP sx ==> nwfs s`, 53SRW_TAC [][nwfs_def,SUBMAP_DEF] THEN 54Q_TAC SUFF_TAC `!y x.nvR s y x ==> nvR sx y x` 55 THEN1 METIS_TAC [WF_SUBSET] THEN 56SRW_TAC [][nvR_def,FLOOKUP_DEF] THEN 57METIS_TAC []); 58 59val _ = export_theory () 60