1open HolKernel bossLib boolLib Parse
2open BasicProvers
3
4open finite_mapTheory
5
6(* an fmaptree is a type of tree, where branching is controlled by a
7   finite-map.  The one constructor is
8
9    FTNode : 'a -> ('k |-> ('a,'k)fmaptree) -> ('a,'k)fmaptree
10
11   This is rather like a trie.
12
13   There is an induction principle (ft_ind), where you are able to assume
14   that your predicate P holds of every subtree.
15*)
16
17val _ = new_theory "fmaptree";
18
19val construct_def = Define`
20  construct a kfm kl =
21    case kl of
22      [] => SOME a
23    | h :: t => if h IN FDOM kfm then kfm ' h t
24                else NONE
25`;
26
27val (wf_rules, wf_ind, wf_cases) = Hol_reln`
28  !a fm. (!k. k IN FDOM fm ==> wf (fm ' k)) ==> wf (construct a fm)
29`;
30
31val wf_NIL_SOME = prove(
32  ``wf f ==> ?a. f [] = SOME a``,
33  ONCE_REWRITE_TAC [wf_cases] THEN SRW_TAC [][] THEN
34  SRW_TAC [][construct_def]);
35
36val construct_11 = prove(
37  ``(!k. k IN FDOM f ==> wf (f ' k)) /\
38    (!k. k IN FDOM g ==> wf (g ' k)) ==>
39    ((construct a f = construct b g) <=> (a = b) /\ (f = g))``,
40  SRW_TAC [] [EQ_IMP_THM, FUN_EQ_THM, construct_def] THENL [
41    FIRST_X_ASSUM (Q.SPEC_THEN `[]` MP_TAC) THEN SRW_TAC [][],
42    SIMP_TAC (srw_ss()) [fmap_EXT, pred_setTheory.EXTENSION] THEN
43    `!x. x IN FDOM f <=> x IN FDOM g`
44        by (GEN_TAC THEN
45            FIRST_X_ASSUM (Q.SPEC_THEN `[x]` MP_TAC) THEN SRW_TAC [][] THENL [
46              `?a. f ' x [] = SOME a` by METIS_TAC [wf_NIL_SOME],
47              `?a. g ' x [] = SOME a` by METIS_TAC [wf_NIL_SOME]
48            ] THEN
49            SRW_TAC [][]) THEN
50    SRW_TAC [][] THEN
51    FIRST_X_ASSUM (MP_TAC o Q.GEN `t` o SPEC ``x::t``) THEN
52    SRW_TAC [][FUN_EQ_THM]
53  ]);
54
55val fmaptrees_exist = new_type_definition(
56  "fmaptree",
57  prove(``?(f: 'key list -> 'value option). wf f``,
58        Q.EXISTS_TAC `construct ARB FEMPTY` THEN
59        ONCE_REWRITE_TAC [wf_cases] THEN
60        MAP_EVERY Q.EXISTS_TAC [`ARB`, `FEMPTY`] THEN
61        SRW_TAC [][]))
62
63val fmap_bij_thm = define_new_type_bijections {ABS = "fromF", REP = "toF",
64                                               name = "fmap_bij_thm",
65                                               tyax = fmaptrees_exist}
66
67val bij_nchotomy = prove(
68  ``!a. ?c. wf c /\ (a = fromF c)``,
69  METIS_TAC [fmap_bij_thm])
70
71val FTNode_def = Define`
72  FTNode i fm = fromF (construct i (toF o_f fm))
73`;
74
75val toF_composed_wf = prove(
76  ``!k. k IN FDOM f1 ==> wf ((toF o_f f1) ' k)``,
77  SRW_TAC [][o_f_FAPPLY, fmap_bij_thm]);
78
79val fromF_11 = prove(
80  ``wf x /\ wf y ==> ((fromF x = fromF y) = (x = y))``,
81  METIS_TAC [fmap_bij_thm]);
82
83val toF_11 = prove(``(toF f = toF g) = (f = g)``, METIS_TAC [fmap_bij_thm]);
84
85val toF_o_f_11 = prove(
86  ``((toF o_f f) = (toF o_f g)) = (f = g)``,
87  SRW_TAC [][EQ_IMP_THM] THEN
88  FULL_SIMP_TAC (srw_ss()) [fmap_EXT, o_f_FAPPLY] THEN
89  `!x. x IN FDOM g ==> (toF (f ' x) = toF (g ' x))`
90      by METIS_TAC [o_f_FAPPLY] THEN
91  FULL_SIMP_TAC (srw_ss()) [toF_11]);
92
93Theorem FTNode_11[simp]:
94  (FTNode i1 f1 = FTNode i2 f2) <=> (i1 = i2) /\ (f1 = f2)
95Proof
96  SRW_TAC [][FTNode_def, fromF_11, wf_rules, toF_composed_wf,
97             construct_11, toF_o_f_11]
98QED
99
100val fmaptree_nchotomy = store_thm(
101  "fmaptree_nchotomy",
102  ``!ft. ?i fm. ft = FTNode i fm``,
103  GEN_TAC THEN Q.SPEC_THEN `ft` STRUCT_CASES_TAC bij_nchotomy THEN
104  SRW_TAC [][FTNode_def, fromF_11, wf_rules, toF_composed_wf] THEN
105  RULE_ASSUM_TAC (ONCE_REWRITE_RULE [wf_cases]) THEN
106  SRW_TAC [][] THEN SRW_TAC [][construct_11, toF_composed_wf] THEN
107  Q.EXISTS_TAC `fromF o_f fm` THEN
108  SRW_TAC [][fmap_EXT, o_f_FAPPLY] THEN METIS_TAC [fmap_bij_thm]);
109
110val item_map_def = new_specification("item_map_def",
111  ["item", "map"],
112  SIMP_RULE (srw_ss()) [SKOLEM_THM] fmaptree_nchotomy);
113
114val (item_thm, map_thm) =
115    CONJ_PAIR (GSYM (SIMP_RULE (srw_ss()) [FORALL_AND_THM]
116                               (ISPEC ``FTNode i fm`` item_map_def)))
117
118val _ = (save_thm("item_thm", item_thm); export_rewrites ["item_thm"])
119val _ = (save_thm("map_thm", map_thm); export_rewrites ["map_thm"])
120
121val apply_path_def = Define`
122  (apply_path [] ft = SOME ft) /\
123  (apply_path (h::t) ft = if h IN FDOM (map ft) then apply_path t (map ft ' h)
124                          else NONE)
125`;
126
127val update_at_path_def = Define`
128  (update_at_path [] a ft = SOME (FTNode a (map ft))) /\
129  (update_at_path (h::t) a ft =
130     if h IN FDOM (map ft) then
131       case update_at_path t a (map ft ' h) of
132         NONE => NONE
133       | SOME ft' => SOME (FTNode (item ft) (map ft |+ (h,ft')))
134     else NONE)
135`;
136
137val fupd_at_path_def = Define`
138  (fupd_at_path [] f ft = f ft) /\
139  (fupd_at_path (h::t) f ft =
140     if h IN FDOM (map ft) then
141       case fupd_at_path t f (map ft ' h) of
142         NONE => NONE
143       | SOME ft' => SOME (FTNode (item ft) (map ft |+ (h, ft')))
144     else NONE)
145`;
146
147val forall_ft = prove(
148  ``(!ft. P ft) = (!f. wf f ==> P (fromF f))``,
149  METIS_TAC [fmap_bij_thm])
150
151val wf_strong_ind = IndDefLib.derive_strong_induction(wf_rules, wf_ind)
152
153val ft_ind = store_thm(
154  "ft_ind",
155  ``!P. (!a fm. (!k. k IN FDOM fm ==> P (fm ' k)) ==> P (FTNode a fm)) ==>
156        !ft. P ft``,
157  SIMP_TAC (srw_ss()) [forall_ft, FTNode_def] THEN GEN_TAC THEN STRIP_TAC THEN
158  HO_MATCH_MP_TAC wf_strong_ind THEN SRW_TAC [][] THEN
159  FIRST_X_ASSUM (Q.SPECL_THEN [`a`, `fromF o_f fm`] MP_TAC) THEN
160  SRW_TAC [][o_f_FAPPLY] THEN
161  Q_TAC SUFF_TAC `(toF o fromF) o_f fm = fm`
162        THEN1 (DISCH_THEN (SUBST1_TAC o SYM) THEN SRW_TAC [][]) THEN
163  SRW_TAC [][fmap_EXT, o_f_FAPPLY] THEN METIS_TAC [fmap_bij_thm]);
164
165open pred_setTheory boolSimps
166val list_GSPEC_cases = prove(
167  ``{ l | P l } = (if P [] then {[]} else {}) UNION
168                  { h :: t | P (h :: t) }``,
169  SRW_TAC [][EXTENSION, EQ_IMP_THM] THEN SRW_TAC [][] THEN
170  Cases_on `x` THEN SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) []);
171
172val applicable_paths_FINITE = store_thm(
173  "applicable_paths_FINITE",
174  ``!ft. FINITE { p | ?ft'. apply_path p ft = SOME ft' }``,
175  HO_MATCH_MP_TAC ft_ind THEN SRW_TAC [][] THEN
176  CONV_TAC (RAND_CONV (HO_REWR_CONV list_GSPEC_cases)) THEN
177  SRW_TAC [][apply_path_def] THEN
178  SRW_TAC [COND_elim_ss, DNF_ss, CONJ_ss][] THEN
179  Q.MATCH_ABBREV_TAC `FINITE s` THEN
180  `s = BIGUNION (IMAGE (\k. IMAGE (CONS k)
181                                  { p | ?ft'. apply_path p (fm ' k) =
182                                              SOME ft' })
183                       (FDOM fm))`
184     by (SRW_TAC [DNF_ss][Once EXTENSION, Abbr`s`] THEN METIS_TAC []) THEN
185  POP_ASSUM SUBST1_TAC THEN SRW_TAC [][] THEN SRW_TAC [][IMAGE_FINITE]);
186
187val apply_path_SNOC = store_thm(
188  "apply_path_SNOC",
189  ``!ft x p. apply_path (p ++ [x]) ft =
190             case apply_path p ft of
191               NONE => NONE
192             | SOME ft' => FLOOKUP (map ft') x``,
193  Induct_on `p` THEN
194  SRW_TAC [][apply_path_def, finite_mapTheory.FLOOKUP_DEF]);
195
196(* ----------------------------------------------------------------------
197    recursion principle
198   ---------------------------------------------------------------------- *)
199
200val (relrec_rules, relrec_ind, relrec_cases) = Hol_reln`
201  !i fm rfm. (FDOM rfm = FDOM fm) /\
202             (!d. d IN FDOM fm ==> relrec h (fm ' d) (rfm ' d))
203          ==>
204             relrec h (FTNode i fm) (h i rfm fm)
205`;
206
207val relrec_fn = prove(
208  ``!ft r1. relrec h ft r1 ==> !r2. relrec h ft r2 ==> (r1 = r2)``,
209  HO_MATCH_MP_TAC relrec_ind THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
210  ONCE_REWRITE_TAC [relrec_cases] THEN SRW_TAC [][] THEN
211  Q_TAC SUFF_TAC `rfm = rfm'` THEN1 SRW_TAC [][] THEN
212  SRW_TAC [][fmap_EXT]);
213
214val relrec_total = prove(
215  ``!ft. ?r. relrec h ft r``,
216  HO_MATCH_MP_TAC ft_ind THEN REPEAT STRIP_TAC THEN
217  ONCE_REWRITE_TAC [relrec_cases] THEN SRW_TAC [][] THEN
218  `?f. !k. k IN FDOM fm ==> relrec h (fm ' k) (f k)`
219     by METIS_TAC [] THEN
220  Q.EXISTS_TAC `FUN_FMAP f (FDOM fm)` THEN
221  SRW_TAC [][FUN_FMAP_DEF]);
222
223val fmtreerec_def = Define`
224  fmtreerec h ft = @r. relrec h ft r
225`;
226
227val fmtreerec_thm = store_thm(
228  "fmtreerec_thm",
229  ``fmtreerec h (FTNode i fm) = h i (fmtreerec h o_f fm) fm``,
230  SRW_TAC [][fmtreerec_def] THEN
231  ONCE_REWRITE_TAC [relrec_cases] THEN SRW_TAC [][] THEN
232  SELECT_ELIM_TAC THEN SRW_TAC [][] THENL [
233    Q.EXISTS_TAC `FUN_FMAP (\k. @r. relrec h (fm ' k) r) (FDOM fm)` THEN
234    SRW_TAC [][FUN_FMAP_DEF] THEN SELECT_ELIM_TAC THEN
235    METIS_TAC [relrec_total],
236    `fmtreerec h = \ft. @r. relrec h ft r`
237       by SRW_TAC [][FUN_EQ_THM, fmtreerec_def] THEN
238    POP_ASSUM SUBST_ALL_TAC THEN
239    REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN
240    SRW_TAC [][fmap_EXT, o_f_DEF] THEN METIS_TAC [relrec_fn]
241  ]);
242
243val fmtree_Axiom = store_thm(
244  "fmtree_Axiom",
245  ``!h. ?f. !i fm. f (FTNode i fm) = h i fm (f o_f fm)``,
246  GEN_TAC THEN Q.EXISTS_TAC `fmtreerec (\i r f. h i f r)` THEN
247  SRW_TAC [][fmtreerec_thm]);
248
249val _ = export_theory()
250