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