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