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