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