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 : 'value -> ('key |-> ('key,'value)fmaptree)
11 -> ('key,'value)fmaptree
12
13 This is rather like a trie.
14
15 The type recurses under a finite map, which the datatype package
16 builds directly: a finite map is a functor in its range, so the
17 specification below is a fixed point like any other, and the
18 constructor's injectivity, the exhaustion theorem, the recursion
19 principle and the induction principle all come with it.
20
21 There is an induction principle (ft_ind), where you are able to
22 assume that your predicate P holds of every subtree.
23*)
24
25(* this specification recurses under a finite map, which the old
26 construction cannot build and the BNF package behind Datatype can *)
27Datatype: fmaptree = FTNode 'value ('key |-> fmaptree)
28End
29
30(* what the declaration saved, under the names the package gives them *)
31fun saved s = DB.fetch "-" s
32val fmaptree_11 = saved "fmaptree_11"
33val fmaptree_nchotomy = saved "fmaptree_nchotomy"
34val fmaptree_Axiom = saved "fmaptree_Axiom"
35val fmaptree_induction = saved "fmaptree_induction"
36
37Theorem FTNode_11[simp] = fmaptree_11
38
39val item_map_def = new_specification("item_map_def",
40 ["item", "map"],
41 SIMP_RULE (srw_ss()) [SKOLEM_THM] fmaptree_nchotomy);
42
43val (item_thm, map_thm) =
44 CONJ_PAIR (GSYM (SIMP_RULE (srw_ss()) [FORALL_AND_THM]
45 (ISPEC ``FTNode i fm`` item_map_def)))
46Theorem item_thm[simp] = item_thm
47Theorem map_thm[simp] = map_thm
48
49Definition apply_path_def:
50 (apply_path [] ft = SOME ft) /\
51 (apply_path (h::t) ft = if h IN FDOM (map ft) then apply_path t (map ft ' h)
52 else NONE)
53End
54
55Definition update_at_path_def:
56 (update_at_path [] a ft = SOME (FTNode a (map ft))) /\
57 (update_at_path (h::t) a ft =
58 if h IN FDOM (map ft) then
59 case update_at_path t a (map ft ' h) of
60 NONE => NONE
61 | SOME ft' => SOME (FTNode (item ft) (map ft |+ (h,ft')))
62 else NONE)
63End
64
65Definition fupd_at_path_def:
66 (fupd_at_path [] f ft = f ft) /\
67 (fupd_at_path (h::t) f ft =
68 if h IN FDOM (map ft) then
69 case fupd_at_path t f (map ft ' h) of
70 NONE => NONE
71 | SOME ft' => SOME (FTNode (item ft) (map ft |+ (h, ft')))
72 else NONE)
73End
74
75(* the package's induction principle says "for every sub-tree in the
76 finite map's range"; this is the same thing said of the keys *)
77Theorem ft_ind:
78 !P. (!a fm. (!k. k IN FDOM fm ==> P (fm ' k)) ==> P (FTNode a fm)) ==>
79 !ft. P ft
80Proof
81 gen_tac >> strip_tac >> ho_match_mp_tac fmaptree_induction >>
82 rpt strip_tac >> last_x_assum irule >> rpt strip_tac >>
83 first_x_assum irule >> simp[FRANGE_DEF] >> metis_tac[]
84QED
85
86Theorem list_GSPEC_cases[local]:
87 { l | P l } = (if P [] then {[]} else {}) UNION
88 { h :: t | P (h :: t) }
89Proof
90 SRW_TAC [][EXTENSION, EQ_IMP_THM] THEN SRW_TAC [][] THEN
91 Cases_on `x` THEN SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) []
92QED
93
94Theorem applicable_paths_FINITE:
95 !ft. FINITE { p | ?ft'. apply_path p ft = SOME ft' }
96Proof
97 HO_MATCH_MP_TAC ft_ind THEN SRW_TAC [][] THEN
98 CONV_TAC (RAND_CONV (HO_REWR_CONV list_GSPEC_cases)) THEN
99 SRW_TAC [][apply_path_def] THEN
100 SRW_TAC [COND_elim_ss, DNF_ss, CONJ_ss][] THEN
101 Q.MATCH_ABBREV_TAC `FINITE s` THEN
102 `s = BIGUNION (IMAGE (\k. IMAGE (CONS k)
103 { p | ?ft'. apply_path p (fm ' k) =
104 SOME ft' })
105 (FDOM fm))`
106 by (SRW_TAC [DNF_ss][Once EXTENSION, Abbr`s`] THEN METIS_TAC []) THEN
107 POP_ASSUM SUBST1_TAC THEN SRW_TAC [][] THEN SRW_TAC [][IMAGE_FINITE]
108QED
109
110Theorem apply_path_SNOC:
111 !ft x p. apply_path (p ++ [x]) ft =
112 case apply_path p ft of
113 NONE => NONE
114 | SOME ft' => FLOOKUP (map ft') x
115Proof
116 Induct_on `p` THEN
117 SRW_TAC [][apply_path_def, finite_mapTheory.FLOOKUP_DEF]
118QED
119
120(* ----------------------------------------------------------------------
121 recursion principle
122
123 The axiom hands the recursive results over under the finite map's
124 own map function, which is exactly the shape fmtreerec is defined
125 at; both used to be built here by hand, out of an inductive
126 relation and a choice.
127 ---------------------------------------------------------------------- *)
128
129Theorem fmtree_Axiom:
130 !h. ?f. !i fm. f (FTNode i fm) = h i fm (f o_f fm)
131Proof
132 metis_tac[fmaptree_Axiom]
133QED
134
135val fmtreerec_def = new_specification(
136 "fmtreerec_def", ["fmtreerec"],
137 SIMP_RULE (srw_ss()) [SKOLEM_THM]
138 (Q.GEN `h` (Q.SPEC `\i fm r. h i r fm` fmtree_Axiom)));
139
140Theorem fmtreerec_thm:
141 fmtreerec h (FTNode i fm) = h i (fmtreerec h o_f fm) fm
142Proof
143 simp[fmtreerec_def]
144QED