1open HolKernel boolLib bossLib Parse; 2open EmitML bagTheory gcdTheory llistTheory patriciaTheory patricia_castsTheory; 3open state_transformerTheory basis_emitTheory; 4 5val _ = new_theory "extended_emit"; 6 7(* == Bags ================================================================= *) 8 9(*---------------------------------------------------------------------------*) 10(* The ML representation of bags is a datatype, not a function. So we need *) 11(* to re-create the functional aspect, via BAG_VAL. *) 12(*---------------------------------------------------------------------------*) 13 14fun ARITH q = EQT_ELIM (numLib.ARITH_CONV (Parse.Term q)); 15 16val BAG_VAL_DEF = Q.new_definition 17("BAG_VAL_DEF",`BAG_VAL b x = b(x)`); 18 19val BAG_VAL_THM = Q.prove 20(`(!x. BAG_VAL EMPTY_BAG x = 0) /\ 21 (!x b e. BAG_VAL (BAG_INSERT e b) x = 22 if (e=x) then 1 + BAG_VAL b x else BAG_VAL b x)`, 23 CONJ_TAC THENL 24 [RW_TAC arith_ss [EMPTY_BAG,BAG_VAL_DEF], 25 RW_TAC arith_ss [BAG_VAL_DEF] THEN METIS_TAC [BAG_VAL_DEF,BAG_INSERT]]); 26 27val BAG_IN_EQNS = Q.prove 28(`(!x. BAG_IN x {||} = F) /\ 29 !x y. BAG_IN x (BAG_INSERT y b) = (x = y) \/ BAG_IN x b`, 30METIS_TAC [NOT_IN_EMPTY_BAG,BAG_IN_BAG_INSERT]); 31 32val BAG_INN_EQN = Q.prove 33(`BAG_INN e n b = BAG_VAL b e >= n`, 34 RW_TAC arith_ss [BAG_VAL_DEF, BAG_INN]); 35 36val BAG_DIFF_EQNS = Q.store_thm 37("BAG_DIFF_EQNS", 38 `(!b:'a bag. BAG_DIFF b {||} = b) /\ 39 (!b:'a bag. BAG_DIFF {||} b = {||}) /\ 40 (!(x:'a) b (y:'a). BAG_DIFF (BAG_INSERT x b) {|y|} = 41 if x = y then b else BAG_INSERT x (BAG_DIFF b {|y|})) /\ 42 (!(b1:'a bag) y (b2:'a bag). 43 BAG_DIFF b1 (BAG_INSERT y b2) = BAG_DIFF (BAG_DIFF b1 {|y|}) b2)`, 44 RW_TAC arith_ss [BAG_DIFF,FUN_EQ_THM,BAG_INSERT,EMPTY_BAG] THEN 45 RW_TAC arith_ss []); 46 47val BAG_INTER_EQNS = Q.store_thm 48("BAG_INTER_EQNS", 49 `(!b:'a bag. BAG_INTER {||} b = {||}) /\ 50 (!b: 'a bag. BAG_INTER b {||} = {||}) /\ 51 (!(x:'a) b1 (b2:'a bag). 52 BAG_INTER (BAG_INSERT x b1) b2 = 53 if BAG_IN x b2 54 then BAG_INSERT x (BAG_INTER b1 (BAG_DIFF b2 {|x|})) 55 else BAG_INTER b1 b2)`, 56 RW_TAC arith_ss [BAG_INTER, EMPTY_BAG,FUN_EQ_THM,BAG_INSERT,BAG_DIFF] 57 THEN RW_TAC arith_ss [] 58 THEN FULL_SIMP_TAC arith_ss [] 59 THEN RW_TAC arith_ss [] 60 THEN FULL_SIMP_TAC arith_ss [BAG_IN, BAG_INN] 61 THEN REPEAT (POP_ASSUM MP_TAC) 62 THEN RW_TAC arith_ss []); 63 64val BAG_MERGE_EQNS = Q.store_thm 65("BAG_MERGE_EQNS", 66 `(!b:'a bag. BAG_MERGE {||} b = b) /\ 67 (!b:'a bag. BAG_MERGE b {||} = b) /\ 68 (!x:'a. !b1 b2:'a bag. 69 BAG_MERGE (BAG_INSERT x b1) b2 = 70 BAG_INSERT x (BAG_MERGE b1 (BAG_DIFF b2 {|x|})))`, 71 RW_TAC arith_ss [BAG_MERGE, EMPTY_BAG,FUN_EQ_THM,BAG_INSERT,BAG_DIFF] 72 THEN RW_TAC arith_ss [] 73 THEN FULL_SIMP_TAC arith_ss []); 74 75val SUB_BAG_EQNS = Q.store_thm 76("SUB_BAG_EQNS", 77 `(!b:'a bag. SUB_BAG {||} b = T) /\ 78 (!x:'a. !b1 b2:'a bag. 79 SUB_BAG (BAG_INSERT x b1) b2 = 80 BAG_IN x b2 /\ SUB_BAG b1 (BAG_DIFF b2 {|x|}))`, 81 RW_TAC arith_ss [SUB_BAG_EMPTY,SUB_BAG, BAG_INSERT, BAG_INN, 82 BAG_IN, BAG_DIFF,EMPTY_BAG, ARITH`!m. 0 >= m = (m=0n)`] 83 THEN REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN RW_TAC arith_ss [] 84 THEN RW_TAC arith_ss [] 85 THEN POP_ASSUM MP_TAC THEN RW_TAC arith_ss [] THENL 86 [FULL_SIMP_TAC bool_ss [ARITH `a+1n >= n = a >=n \/ (n=a+1)`] 87 THENL [RES_TAC THEN FULL_SIMP_TAC arith_ss [], 88 `b1(x) >= n-1` by DECIDE_TAC THEN 89 RES_THEN MP_TAC THEN REWRITE_TAC [] THEN DECIDE_TAC], 90 RES_THEN MP_TAC THEN ASM_REWRITE_TAC [] THEN DECIDE_TAC]); 91 92val PSUB_BAG_LEM = Q.prove 93(`!b1 b2.PSUB_BAG b1 b2 = SUB_BAG b1 b2 /\ ~SUB_BAG b2 b1`, 94 METIS_TAC [SUB_BAG_PSUB_BAG,PSUB_BAG_ANTISYM]); 95 96val SET_OF_BAG_EQNS = Q.prove 97(`(SET_OF_BAG ({||}:'a bag) = ({}:'a set)) /\ 98 (!(x:'a) b. SET_OF_BAG (BAG_INSERT x b) = x INSERT (SET_OF_BAG b))`, 99 REWRITE_TAC [SET_OF_BAG_INSERT] THEN 100 RW_TAC arith_ss [SET_OF_BAG,EMPTY_BAG,FUN_EQ_THM,NOT_IN_EMPTY_BAG, 101 pred_setTheory.EMPTY_DEF]); 102 103val BAG_OF_SET_EQNS = Q.prove 104(`(BAG_OF_SET ({}:'a set) = ({||}:'a bag)) /\ 105 (!(x:'a) (s:'a set). 106 BAG_OF_SET (x INSERT s) = if x IN s then BAG_OF_SET s 107 else BAG_INSERT x (BAG_OF_SET s))`, 108 RW_TAC bool_ss [SET_OF_EMPTY] THEN 109 RW_TAC arith_ss [BAG_OF_SET,FUN_EQ_THM,BAG_INSERT] THEN 110 METIS_TAC [pred_setTheory.IN_INSERT]); 111 112val defs = 113 map DEFN_NOSIG 114 [BAG_VAL_THM, BAG_IN_EQNS, BAG_INN_EQN, 115 INST_TYPE [beta |-> alpha] 116 (CONJ (CONJUNCT1 (CONJUNCT2 BAG_UNION_EMPTY)) 117 (CONJUNCT1 (SPEC_ALL (Q.SPEC `x` BAG_UNION_INSERT)))), 118 BAG_DIFF_EQNS, BAG_INTER_EQNS, BAG_MERGE_EQNS, 119 SUB_BAG_EQNS, PSUB_BAG_LEM, 120 CONJ BAG_FILTER_EMPTY (BAG_FILTER_BAG_INSERT), 121 CONJ (INST_TYPE [alpha |-> beta, beta |-> alpha] BAG_IMAGE_EMPTY) 122 (UNDISCH (SPEC_ALL BAG_IMAGE_FINITE_INSERT)), 123 CONJ BAG_CARD_EMPTY (UNDISCH (SPEC_ALL (CONJUNCT2 BAG_CARD_THM))), 124 SET_OF_BAG_EQNS, (*BAG_OF_SET_EQNS,*) 125 BAG_DISJOINT] 126 127val (tyg,tmg) = (type_grammar(),term_grammar()) 128val tyg' = type_grammar.remove_abbreviation tyg "bag" 129val _ = temp_set_grammars(tyg',tmg) 130val _ = new_type("bag",1) 131 132val _ = eSML "bag" 133 (ABSDATATYPE (["'a"], `bag = EMPTY_BAG | BAG_INSERT 'a bag`) 134 :: OPEN ["num", "set"] 135 :: MLSIG "type num = numML.num" 136 :: MLSIG "type 'a set = 'a setML.set" 137 :: MLSIG "val EMPTY_BAG : 'a bag" 138 :: MLSIG "val BAG_INSERT : 'a * 'a bag -> 'a bag" 139 :: MLSIG "val BAG_VAL : ''a bag -> ''a -> num" 140 :: MLSIG "val BAG_IN : ''a -> ''a bag -> bool" 141 :: MLSIG "val BAG_INN : ''a -> num -> ''a bag -> bool" 142 :: MLSIG "val BAG_UNION : ''a bag -> ''a bag -> ''a bag" 143 :: MLSIG "val BAG_DIFF : ''a bag -> ''a bag -> ''a bag" 144 :: MLSIG "val BAG_INTER : ''a bag -> ''a bag -> ''a bag" 145 :: MLSIG "val BAG_MERGE : ''a bag -> ''a bag -> ''a bag" 146 :: MLSIG "val SUB_BAG : ''a bag -> ''a bag -> bool" 147 :: MLSIG "val PSUB_BAG : ''a bag -> ''a bag -> bool" 148 :: MLSIG "val BAG_DISJOINT : ''a bag -> ''a bag -> bool" 149 :: MLSIG "val BAG_FILTER : ('a -> bool) -> 'a bag -> 'a bag" 150 :: MLSIG "val BAG_IMAGE : ('a -> 'b) -> 'a bag -> 'b bag" 151 :: MLSIG "val BAG_CARD : 'a bag -> num" 152 :: MLSIG "val SET_OF_BAG : 'a bag -> 'a set" 153(* :: MLSIG "val BAG_OF_SET : ''a set -> ''a bag" *) 154 :: defs) 155 156(* 157 (MLSIGSTRUCT ["type num = NumML.num", "type 'a set = 'a SetML.set", "", 158 "type 'a bag = EMPTY_BAG | BAG_INSERT of 'a * 'a bag"] 159*) 160 161val _ = eCAML "bag" 162 (MLSIGSTRUCT ["type num = NumML.num", "type 'a set = 'a SetML.set"] @ 163 ABSDATATYPE (["'a"], `bag = EMPTY_BAG | BAG_INSERT 'a bag`) :: 164 OPEN ["num", "set"] :: 165 map MLSIG 166 ["val _BAG_VAL : 'a bag -> 'a -> num", 167 "val _BAG_IN : 'a -> 'a bag -> bool", 168 "val _BAG_INN : 'a -> num -> 'a bag -> bool", 169 "val _BAG_UNION : 'a bag -> 'a bag -> 'a bag", 170 "val _BAG_DIFF : 'a bag -> 'a bag -> 'a bag", 171 "val _BAG_INTER : 'a bag -> 'a bag -> 'a bag", 172 "val _BAG_MERGE : 'a bag -> 'a bag -> 'a bag", 173 "val _SUB_BAG : 'a bag -> 'a bag -> bool", 174 "val _PSUB_BAG : 'a bag -> 'a bag -> bool", 175 "val _BAG_DISJOINT : 'a bag -> 'a bag -> bool", 176 "val _BAG_FILTER : ('a -> bool) -> 'a bag -> 'a bag", 177 "val _BAG_IMAGE : ('a -> 'b) -> 'a bag -> 'b bag", 178 "val _BAG_CARD : 'a bag -> num", 179 "val _SET_OF_BAG : 'a bag -> 'a set", 180 "val bag_of_list : 'a list -> 'a bag", 181 "val list_of_bag : 'a bag -> 'a list"] @ 182 map MLSTRUCT 183 ["let bag_of_list l = ListML._FOLDL (function s -> function a ->\n\ 184 \ BAG_INSERT(a,s)) EMPTY_BAG l", "", 185 "let rec list_of_bag b = match b with EMPTY_BAG -> []\n\ 186 \ | BAG_INSERT(a,s) -> a::list_of_bag s", ""] @ 187 defs) 188 189(* == GCD ================================================================== *) 190 191val defs = map DEFN [dividesTheory.compute_divides, GCD_EFFICIENTLY, lcm_def]; 192 193val _ = eSML "gcd" 194 (MLSIG "type num = numML.num" :: 195 OPEN ["num"] :: 196 defs); 197 198val _ = eCAML "gcd" 199 (MLSIGSTRUCT ["type num = NumML.num"] @ 200 OPEN ["num"] :: 201 defs); 202 203(* == Lazy lists =========================================================== *) 204 205val llcases_exists0 = prove( 206 ``!l. ?v. (l = [||]) /\ (v = n) \/ 207 ?h t. (l = h:::t) /\ (v = c (h, t))``, 208 GEN_TAC THEN Q.SPEC_THEN `l` STRUCT_CASES_TAC llist_CASES THEN 209 SRW_TAC [][EXISTS_OR_THM]) 210val llcases_exists = 211 llcases_exists0 |> GEN_ALL |> SIMP_RULE bool_ss [SKOLEM_THM] 212val llcases_def = new_specification("llcases_def", ["llcases"], 213 llcases_exists) 214 215val llcases_LNIL = llcases_def |> SPEC_ALL |> Q.INST [`l` |-> `LNIL`] 216 |> SIMP_RULE (srw_ss()) [] 217val llcases_LCONS = llcases_def |> SPEC_ALL |> Q.INST [`l` |-> `h:::t`] 218 |> SIMP_RULE (srw_ss()) [] 219 220val LLCONS_def = Define` 221 LLCONS h t = LCONS h (t ())`; 222 223val LAPPEND_llcases = prove( 224 ``LAPPEND l1 l2 = llcases l2 (\(h,t). LLCONS h (\(). LAPPEND t l2)) l1``, 225 Q.SPEC_THEN `l1` STRUCT_CASES_TAC llist_CASES THEN 226 SRW_TAC [][LLCONS_def, llcases_LCONS, llcases_LNIL]); 227 228val LMAP_llcases = prove( 229 ``LMAP f l = llcases LNIL (\(h,t). LLCONS (f h) (\(). LMAP f t)) l``, 230 Q.ISPEC_THEN `l` STRUCT_CASES_TAC llist_CASES THEN 231 SRW_TAC [][LLCONS_def, llcases_LCONS, llcases_LNIL]); 232 233val LFILTER_llcases = prove( 234 ``LFILTER P l = llcases LNIL (\(h,t). if P h then LLCONS h (\(). LFILTER P t) 235 else LFILTER P t) l``, 236 Q.ISPEC_THEN `l` STRUCT_CASES_TAC llist_CASES THEN 237 SRW_TAC [][LLCONS_def, llcases_LCONS, llcases_LNIL]); 238 239val LHD_llcases = prove( 240 ``LHD ll = llcases NONE (\(h,t). SOME h) ll``, 241 Q.ISPEC_THEN `ll` STRUCT_CASES_TAC llist_CASES THEN 242 SRW_TAC [][llcases_LCONS, llcases_LNIL]); 243 244val LTL_llcases = prove( 245 ``LTL ll = llcases NONE (\(h,t). SOME t) ll``, 246 Q.ISPEC_THEN `ll` STRUCT_CASES_TAC llist_CASES THEN 247 SRW_TAC [][llcases_LCONS, llcases_LNIL]); 248 249val LTAKE_thm = prove( 250 ``!ll. LTAKE n ll = 251 if n = 0 then SOME [] 252 else case LHD ll of 253 NONE => NONE 254 | SOME h => OPTION_MAP (\t. h::t) 255 (LTAKE (n - 1) (THE (LTL ll)))``, 256 Induct_on `n` THEN SRW_TAC [boolSimps.ETA_ss][LTAKE] THEN 257 Q.ISPEC_THEN `ll` STRUCT_CASES_TAC llist_CASES THEN 258 SRW_TAC [][] THEN Cases_on `LHD t` THEN SRW_TAC [][] THEN 259 Cases_on `OPTION_MAP (CONS x) (LTAKE (n - 1) (THE (LTL t)))` THEN 260 SRW_TAC [][]); 261 262val toList_llcases = prove( 263 ``toList ll = llcases (SOME []) (\(h,t). OPTION_MAP (\t. h::t) (toList t)) ll``, 264 Q.ISPEC_THEN `ll` STRUCT_CASES_TAC llist_CASES THEN 265 SRW_TAC [boolSimps.ETA_ss][llcases_LCONS, llcases_LNIL, toList_THM]) 266 267fun insert_const c = let val t = Parse.Term [QUOTE c] in 268 ConstMapML.prim_insert(t, (false, "", c, type_of t)) 269end 270val _ = insert_const "llcases" 271val _ = insert_const "LLCONS" 272val _ = insert_const "LCONS" 273val _ = insert_const "LNIL" 274val _ = insert_const "LUNFOLD" 275val _ = adjoin_to_theory 276{sig_ps = NONE, struct_ps = SOME (fn ppstrm => 277 let val S = PP.add_string ppstrm 278 fun NL() = PP.add_newline ppstrm 279 in S "fun insert_const c = let val t = Parse.Term [QUOTE c] in"; NL(); 280 S " ConstMapML.prim_insert(t, (false, \"\", c, type_of t))"; NL(); 281 S "end"; NL(); 282 S "val _ = insert_const \"llcases\""; NL(); 283 S "val _ = insert_const \"LLCONS\""; NL(); 284 S "val _ = insert_const \"LCONS\""; NL(); 285 S "val _ = insert_const \"LNIL\""; NL(); 286 S "val _ = insert_const \"LUNFOLD\"" 287 end)} 288 289val _ = eSML "llist" 290 (MLSIG "type 'a llist" :: 291 MLSIG "val LNIL : 'a llist" :: 292 MLSIG "val LLCONS : 'a -> (unit -> 'a llist) -> 'a llist" :: 293 MLSIG "val LCONS : 'a -> 'a llist -> 'a llist" :: 294 MLSIG "val ::: : 'a * 'a llist -> 'a llist" :: 295 MLSIG "val llcases : 'b -> ('a * 'a llist -> 'b) -> 'a llist -> 'b" :: 296 MLSIG "val LUNFOLD : ('a -> ('a * 'b) option) -> 'a -> 'b llist" :: 297 MLSIG "type num = numML.num" :: 298 OPEN ["num", "list"] :: 299 MLSTRUCT "type 'a llist = 'a seq.seq" :: 300 MLSTRUCT "fun llcases n c seq = seq.fcases seq (n,c)" :: 301 MLSTRUCT "fun LLCONS h t = seq.cons h (seq.delay t)":: 302 MLSTRUCT "fun LCONS h t = seq.cons h t":: 303 MLSTRUCT "val LNIL = seq.empty":: 304 MLSTRUCT "fun :::(h,t) = LCONS h t":: 305 MLSTRUCT "fun LUNFOLD f x = seq.delay (fn () => case f x of NONE => LNIL | SOME (y,e) => LCONS e (LUNFOLD f y))" :: 306 map DEFN [ 307 LAPPEND_llcases, LMAP_llcases, LFILTER_llcases, 308 LHD_llcases, LTL_llcases, LTAKE_thm, 309 toList_llcases]) 310 311(* == Patricia tress ======================================================= *) 312 313val _ = set_trace "Unicode" 0 314fun Datatype x = DATATYPE [QUOTE (EmitTeX.datatype_thm_to_string x)] 315 316val fun_rule = REWRITE_RULE [FUN_EQ_THM] 317 318val _ = ConstMapML.insert ``SKIP1``; 319val _ = ConstMapML.insert ``string_to_num``; 320 321val _ = temp_remove_rules_for_term "Empty" 322val _ = temp_disable_tyabbrev_printing "ptreeset" 323val _ = temp_disable_tyabbrev_printing "word_ptreeset" 324 325val defs = 326 [BRANCHING_BIT_def, PEEK_def, JOIN_def, ADD_def, BRANCH_def, 327 REMOVE_def, TRAVERSE_def, KEYS_def, TRANSFORM_def, EVERY_LEAF_def, 328 EXISTS_LEAF_def, SIZE_def, DEPTH_def, IS_PTREE_def, IN_PTREE_def, 329 INSERT_PTREE_def, patriciaTheory.IS_EMPTY_def, FIND_def, 330 fun_rule ADD_LIST_def]; 331 332val _ = eSML "patricia" 333 (OPEN ["num", "option", "set"] 334 :: MLSIG "type num = numML.num" 335 :: Datatype datatype_ptree 336 :: MLSIG "val toList : 'a ptree -> (num * 'a) list" 337 :: MLSTRUCT "fun toList Empty = []\n\ 338 \ | toList (Leaf(j,d)) = [(j,d)]\n\ 339 \ | toList (Branch(p,m,l,r)) =\n\ 340 \ listML.APPEND (toList l) (toList r)" 341 :: map DEFN defs); 342 343val _ = eCAML "patricia" 344 (MLSIGSTRUCT ["type num = NumML.num"] 345 @ Datatype datatype_ptree 346 :: MLSIG "val toList : 'a ptree -> (num * 'a) list" 347 :: MLSTRUCT "let rec toList t = match t with\n\ 348 \ Empty -> []\n\ 349 \ | Leaf(j,d) -> [(j,d)]\n\ 350 \ | Branch(p,m,l,r) ->\n\ 351 \ ListML._APPEND (toList l) (toList r)" 352 :: map DEFN defs); 353 354val _ = eSML "patricia_casts" 355 (OPEN ["num", "option", "set", "bit", "words", "patricia"] 356 :: MLSIG "type 'a ptree = 'a patriciaML.ptree" 357 :: MLSIG "type 'a word = 'a wordsML.word" 358 :: MLSIG "type num = numML.num" 359 :: MLSIG "type string = stringML.string" 360 :: MLSIG "val SKIP1 : string -> string" 361 :: MLSIG "val string_to_num : string -> num" 362 :: MLSTRUCT "type string = stringML.string" 363 :: MLSTRUCT "fun SKIP1 s = String.extract(s,1,NONE)" 364 :: MLSTRUCT "fun string_to_num s = s2n (numML.fromInt 256) stringML.ORD\n\ 365 \ (String.^(String.str (Char.chr 1), s))" 366 :: Datatype datatype_word_ptree 367 :: map DEFN 368 [THE_PTREE_def, SOME_PTREE_def, 369 PEEKw_def, ADDw_def, REMOVEw_def, TRANSFORMw_def, SIZEw_def, 370 DEPTHw_def, IN_PTREEw_def, INSERT_PTREEw_def, FINDw_def, 371 fun_rule ADD_LISTw_def, num_to_string_def, PEEKs_def, FINDs_def, 372 ADDs_def, fun_rule ADD_LISTs_def, REMOVEs_def, TRAVERSEs_def, 373 KEYSs_def, IN_PTREEs_def, INSERT_PTREEs_def]); 374 375fun adjoin_to_theory_struct l = adjoin_to_theory {sig_ps = NONE, 376 struct_ps = SOME (fn ppstrm => 377 app (fn s => (PP.add_string ppstrm s; PP.add_newline ppstrm)) l)}; 378 379val _ = adjoin_to_theory_struct 380 ["val _ = ConstMapML.insert (\ 381 \Term.prim_mk_const{Name=\"SKIP1\",Thy=\"patricia_casts\"});", 382 "val _ = ConstMapML.insert (\ 383 \Term.prim_mk_const{Name=\"string_to_num\",Thy=\"patricia_casts\"});"]; 384 385(* == State transformer ==================================================== *) 386 387val defs = map DEFN [UNIT_DEF, BIND_DEF, IGNORE_BIND_DEF, MMAP_DEF, JOIN_DEF, READ_def, WRITE_def] 388 389val _ = eSML "state_transformer" defs 390val _ = eCAML "state_transformer" defs; 391 392val _ = export_theory (); 393