1(* File: enumTacs.sml. Author: F. Lockwood Morris. Begun 6 Aug 2013. *) 2 3(* Basic conversions and conversionals, and inference rules for *) 4(* sorting lists, building ENUMERALS, look-up and converting them to *) 5(* OWL's, performing merge-based opns. on OWL's, recovering ENUMERALS. *) 6 7structure enumTacs :> enumTacs = 8struct 9(* comment out load before Holmaking *) 10(* app load ["totoTheory", "pred_setLib", "reduceLib", "relationTheory", 11 "enumeralTheory", "totoTacs", "bossLib", "finite_mapTheory"]; *) 12 13open Parse HolKernel boolLib; 14 15val _ = set_trace "Unicode" 0; 16open totoTheory reduceLib bossLib 17 relationTheory listTheory pairTheory optionTheory enumeralTheory pred_setLib 18 totoTacs finite_mapTheory; 19 20structure Parse = struct 21 open Parse 22 val (Type,Term) = parse_from_grammars enumeralTheory.enumeral_grammars 23end 24open Parse 25 26val AR = ASM_REWRITE_TAC []; 27fun ulist x = [x]; 28 29val ERR = mk_HOL_ERR "enumTacs"; 30 31(* ********************************************************************* *) 32(* The style of writing conversions here is modeled on that expounded *) 33(* by Lawrence Paulson in "A higher-order implementation of rewriting". *) 34(* It takes REWR_CONV (which he in that paper called "REWRITE_CONV") *) 35(* as the workhorse, leaving to it the work of matching terms and types, *) 36(* but avoiding searching. As an easily grasped example of the style, *) 37(* here is an equivalent of the listLib's REVERSE_CONV: *) 38(* ********************************************************************* *) 39 40(* REVERSE_REV = |- !L. REVERSE L = REV L [] *) 41 42val [rev_nil, rev_rec] = CONJUNCTS REV_DEF; 43 44(* rev_nil = |- !acc. REV [] acc = acc 45 rev_rec = |- !h t acc. REV (h::t) acc = REV t (h::acc) *) 46 47val REVERS_CONV = 48let fun rev_conv t = ((REWR_CONV rev_rec THENC rev_conv) ORELSEC 49 REWR_CONV rev_nil) t 50in REWR_CONV REVERSE_REV THENC rev_conv end; 51 52(* ******************************************************************* *) 53(* EQ_LESS_CONV, COND_EQ_LESS_CONV *) 54(* ******************************************************************* *) 55 56(* EQ_LESS_CONV converts cpn = LESS to one of T, F *) 57 58val LESS_T = SPEC ``LESS`` (INST_TYPE [alpha |-> ``:cpn``] REFL_CLAUSE); 59val GREATER_F = prove (``(GREATER = LESS) = F``,REWRITE_TAC [all_cpn_distinct]); 60val EQUAL_F = prove (``(EQUAL = LESS) = F``,REWRITE_TAC [all_cpn_distinct]); 61 62val EQ_LESS_CONV = REWR_CONV LESS_T ORELSEC REWR_CONV GREATER_F ORELSEC 63 REWR_CONV EQUAL_F ORELSEC 64(fn _ => Raise (mk_HOL_ERR "enumTacs" "EQ_LESS_CONV" "not a ... = LESS")); 65 66(* A replacement for cpn_REWR_CONV when instead of case <cpn> of LESS => ... 67 we have if <cpn> = LESS then ... else ... .*) 68 69val EQ_LESS_REWR = prove (``!v0 v1:'a. (if LESS = LESS then v0 else v1) = v0``, 70RW_TAC bool_ss []); 71 72val EQ_GREATER_REWR = prove (``!v0 v1:'a. 73(if GREATER = LESS then v0 else v1) = v1``, RW_TAC bool_ss []); 74 75val EQ_EQUAL_REWR = prove (``!v0 v1:'a. 76(if EQUAL = LESS then v0 else v1) = v1``, RW_TAC bool_ss []); 77 78val COND_EQ_LESS_CONV = REWR_CONV EQ_LESS_REWR ORELSEC REWR_CONV EQ_GREATER_REWR 79 ORELSEC REWR_CONV EQ_EQUAL_REWR ORELSEC 80(fn _ => Raise (mk_HOL_ERR "enumTacs" "COND_EQ_LESS_CONV" "not if ... = LESS")); 81 82(* ********************************************************************** *) 83(* Conversions for sorting lists with constant keys *) 84(* ********************************************************************** *) 85 86val [none_none, some_none, none_some, some_some] = CONJUNCTS smerge; 87 88(* none_none = |- !cmp. smerge cmp [] [] = [] 89 none_some = |- !y m cmp. smerge cmp [] (y::m) = y::m 90 some_none = |- !x l cmp. smerge cmp (x::l) [] = x::l 91 some_some = |- !y x m l cmp. smerge cmp (x::l) (y::m) = 92 case apto cmp x y of 93 LESS => x::smerge cmp l (y::m) 94 | EQUAL => x::smerge cmp l m 95 | GREATER => y::smerge cmp (x::l) m *) 96 97fun smerge_CONV key_conv = 98let fun merge_c t = 99((REWR_CONV some_some THENC 100 RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV key_conv))) THENC 101 cpn_REWR_CONV THENC RAND_CONV merge_c) ORELSEC 102REWR_CONV none_some ORELSEC REWR_CONV some_none ORELSEC REWR_CONV none_none) t 103in merge_c end; 104 105val [im_lengthen, im_zero, im_one] = CONJUNCTS incr_smerge; 106 107(* im_lengthen = |- !l cmp. incr_smerge cmp l [] = [SOME l] 108 im_zero = |- !lol l cmp. incr_smerge cmp l (NONE::lol) = SOME l::lol 109 im_one = |- !m lol l cmp. 110 incr_smerge cmp l (SOME m::lol) = 111 NONE::incr_smerge cmp (smerge cmp l m) lol *) 112 113fun incr_smerge_CONV key_conv = 114let fun im_c t = ((REWR_CONV im_one THENC 115 RAND_CONV (RATOR_CONV (RAND_CONV (smerge_CONV key_conv)) 116 THENC im_c)) 117 ORELSEC REWR_CONV im_zero ORELSEC REWR_CONV im_lengthen) t 118in im_c end; 119 120val [ib_base, ib_rec] = CONJUNCTS incr_sbuild; 121 122(* ib_base = |- !cmp. incr_sbuild cmp [] = [] 123 ib_rec = 124 |- !cmp x l. 125 incr_sbuild cmp (x::l) = incr_smerge cmp [x] (incr_sbuild cmp l) *) 126 127fun incr_sbuild_CONV key_conv = 128let fun ib_c t = ((REWR_CONV ib_rec THENC RAND_CONV ib_c THENC 129 incr_smerge_CONV key_conv) 130 ORELSEC REWR_CONV ib_base) t 131in ib_c end; 132 133val [mo_base, mo_none, mo_some] = CONJUNCTS smerge_out; 134 135(* mo_base = |- !l cmp. smerge_out cmp l [] = l 136 mo_none = 137 |- !lol l cmp. smerge_out cmp l (NONE::lol) = smerge_out cmp l lol 138 mo_some = 139 |- !m lol l cmp. 140 smerge_out cmp l (SOME m::lol) = 141 smerge_out cmp (smerge cmp l m) lol *) 142 143fun smerge_out_CONV key_conv = 144let fun mo_c t = ((REWR_CONV mo_some THENC 145 RATOR_CONV (RAND_CONV (smerge_CONV key_conv)) THENC 146 mo_c) ORELSEC 147 (REWR_CONV mo_none THENC mo_c) ORELSEC 148 REWR_CONV mo_base) t 149in mo_c end; 150 151fun incr_ssort_CONV key_conv = 152 (REWR_CONV incr_ssort THENC RAND_CONV (incr_sbuild_CONV key_conv) THENC 153 smerge_out_CONV key_conv) ORELSEC 154(fn _ => Raise (mk_HOL_ERR "enumTacs" "incr_ssort_CONV" 155 "not an explicit list")); 156 157(* ******************************************************************** *) 158(* BL_ACCUM_CONV, BL_CONS_CONV, bt_rev_CONV *) 159(* ******************************************************************** *) 160 161val [umnbl, umzer, umone] = CONJUNCTS BL_ACCUM; 162 163(* umnbl = |- !a ac. BL_ACCUM a ac nbl = onebl a ac nbl 164 umzer = |- !a ac bl. BL_ACCUM a ac (zerbl bl) = onebl a ac bl 165 umone = 166 |- !a ac r rft bl. 167 BL_ACCUM a ac (onebl r rft bl) = 168 zerbl (BL_ACCUM a (node ac r rft) bl) *) 169 170fun BL_ACCUM_CONV t = 171((REWR_CONV umone THENC RAND_CONV BL_ACCUM_CONV) ORELSEC 172 REWR_CONV umzer ORELSEC 173 REWR_CONV umnbl) t; 174 175val BL_CONS_CONV = (REWR_CONV BL_CONS THENC BL_ACCUM_CONV) ORELSEC 176(fn _ => Raise (mk_HOL_ERR "rbtTacs" "BL_CONS_CNV" "bad call of BL_CONS")); 177 178val [rnt, rnode] = CONJUNCTS bt_rev; 179 180(* rnt = |- !bl. bt_rev nt bl = bl 181 rnode = |- !lft r rft bl. 182 bt_rev (node lft r rft) bl = bt_rev lft (onebl r rft bl) *) 183 184fun bt_rev_CONV t = 185((REWR_CONV rnode THENC bt_rev_CONV) ORELSEC REWR_CONV rnt) t; 186 187(* ****************************************************************** *) 188(* bt_to_list_CONV (used by bt_to_ol_CONV); *) 189(* bl_to_bt_CONV, list_to_bl_CONV, list_to_bt_CONV *) 190(* ****************************************************************** *) 191 192(* bt_to_list_CONV works out terms of the form bt_to_list_ac t [] *) 193 194val [bt_list_nt, bt_list_node] = CONJUNCTS bt_to_list_ac; 195 196(* bt_list_nt = |- !m. bt_to_list_ac nt m = m 197 bt_list_node = |- !l x r m. 198 bt_to_list_ac (node l x r) m = 199 bt_to_list_ac l (x::bt_to_list_ac r m) *) 200 201val bt_to_list_CONV = 202let fun btl t = ((REWR_CONV bt_list_node THENC 203 RAND_CONV (RAND_CONV btl) THENC btl) ORELSEC 204 REWR_CONV bt_list_nt) t 205in btl end; 206 207val [lb_nil, lb_rec] = CONJUNCTS list_to_bl; 208 209(* lb_nil = |- list_to_bl [] = nbl 210 lb_rec = |- !a l. list_to_bl (a::l) = BL_CONS a (list_to_bl l) *) 211 212fun list_to_bl_CONV t = 213((REWR_CONV lb_rec THENC RAND_CONV list_to_bl_CONV THENC BL_CONS_CONV) 214 ORELSEC REWR_CONV lb_nil ORELSEC 215 (fn _ => Raise (mk_HOL_ERR "rbtTacs" "list_to_bl" "not an explicit list"))) t; 216 217val [blr_nbl, blr_zer, blr_one] = CONJUNCTS bl_rev; 218 219(* blr_nbl = |- !ft. bl_rev ft nbl = ft 220 blr_zer = |- !ft b. bl_rev ft (zerbl b) = bl_rev ft b 221 blr_one = |- !ft a f b. bl_rev ft (onebl a f b) = bl_rev (node ft a f) b *) 222 223fun bl_rev_CONV t = 224((REWR_CONV blr_one THENC bl_rev_CONV) ORELSEC 225 (REWR_CONV blr_zer THENC bl_rev_CONV) ORELSEC 226 REWR_CONV blr_nbl) t; 227 228val bl_to_bt_CONV = RATOR_CONV (REWR_CONV bl_to_bt) THENC bl_rev_CONV; 229 230val list_to_bt_CONV = REWR_CONV list_to_bt THENC 231 RAND_CONV list_to_bl_CONV THENC bl_to_bt_CONV; 232 233(* ******************************************************************* *) 234(* set_TO_ENUMERAL_CONV, DISPLAY_TO_set_CONV, DISPLAY_TO_ENUMERAL_CONV *) 235(* ******************************************************************* *) 236 237(* Convert ``set l`` to ``ENUMERAL ...`` *) 238 239fun set_TO_ENUMERAL_CONV keyconv cmp = 240REWR_CONV (ISPEC cmp ENUMERAL_set) THENC 241RAND_CONV (RAND_CONV (incr_ssort_CONV keyconv)) THENC 242RAND_CONV list_to_bt_CONV; 243 244val LIST_TO_SET_NIL = prove ( 245``{} = set ([]:'a list)``, REWRITE_TAC [LIST_TO_SET_THM]); 246 247val LIST_TO_SET_CONS = prove ( 248``!a:'a l s. (s = set l) ==> (a INSERT s = set (a :: l))``, 249REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [LIST_TO_SET_THM]); 250 251(* DISPLAY_TO_set_CONV { ... } proves { ... } = set [ ... ] *) 252 253fun DISPLAY_TO_set_CONV t = 254if is_const t then 255let val (s, ty) = dest_const t; 256 val ety = hd (snd (dest_type ty)) 257in INST_TYPE [alpha |-> ety] LIST_TO_SET_NIL end 258else 259let val (elem, st) = dest_binop (Term`($INSERT):'a->('a->bool)->'a->bool`) 260 (ERR "DISPLAY_TO_set_CONV" "not a finite set extension") t; 261 val ety = type_of elem 262in SPEC elem (MATCH_MP (INST_TYPE [alpha |-> ety] LIST_TO_SET_CONS) 263 (DISPLAY_TO_set_CONV st)) end; 264 265fun DISPLAY_TO_ENUMERAL_CONV keyconv cmp = 266 DISPLAY_TO_set_CONV THENC set_TO_ENUMERAL_CONV keyconv cmp; 267 268(* ******************************************************************* *) 269(* The one pure conversion working on directly on sets of the form *) 270(* ENUMERAL cmp ... is IN_CONV, which we allow to fall back on *) 271(* pred_setLib.IN_CONV in case it is given an equality-decider and *) 272(* a { ... } set in place of a cmp-evaluator and ENUMERAL cmp ... set. *) 273(* ******************************************************************* *) 274 275(* IN_node = |- !cmp x l y r. x IN ENUMERAL cmp (node l y r) <=> 276 case apto cmp x y of 277 LESS => x IN ENUMERAL cmp l 278 | EQUAL => T 279 | GREATER => x IN ENUMERAL cmp r 280 281 NOT_IN_nt = |- !cmp y. y IN ENUMERAL cmp nt <=> F *) 282 283fun IN_CONV key_conv = 284let fun apf_c t = 285 ((REWR_CONV IN_node THENC 286 RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV key_conv))) THENC 287 cpn_REWR_CONV THENC (apf_c ORELSEC ALL_CONV)) ORELSEC 288 REWR_CONV NOT_IN_nt) t 289 handle _ => pred_setLib.IN_CONV key_conv t 290in apf_c end; 291 292(* ******************************************************************* *) 293(* To perform binary operations on sets efficiently, we shall deal not *) 294(* in equations, as with proper conversions, but with conjunctions of *) 295(* the form |- (<set expn> = set l) /\ OL cmp l, where l is an expli- *) 296(* citly displayed list. We now give conversion-like functions to go *) 297(* back and forth between such conjunctions -- strictly abbreviations *) 298(* of them as OWL cmp <set expn> l -- and ENUMERAL cmp ... sets. *) 299(* ******************************************************************* *) 300 301(* Translate |- OWL cmp s l to |- s = ENUMERAL cmp ... . *) 302 303fun OWL_TO_ENUMERAL owl = 304let val (eqn, ol) = CONJ_PAIR (CONV_RULE (REWR_CONV OWL) owl); 305 val raw_ans = TRANS eqn (MATCH_MP OL_ENUMERAL ol) 306in CONV_RULE (RAND_CONV (RAND_CONV list_to_bt_CONV)) raw_ans end; 307 308(* We need bt_to_ol_CONV, with _lb, _ub, _lb_ub variants, using _ac thms. *) 309 310(* Remember that the ... = LESS comparisons will in practice always come out 311 true. I can see no harm, however, in making bt_to_ol_CONV work correctly 312 for arbitrary trees. *) 313 314val [lb_ub_ac_nt, lb_ub_ac_node] = CONJUNCTS bt_to_ol_lb_ub_ac; 315 316(* lb_ub_ac_nt = |- !cmp lb ub m. bt_to_ol_lb_ub_ac cmp lb nt ub m = m 317 lb_ub_ac_node = 318 |- !cmp lb l x r ub m. 319 bt_to_ol_lb_ub_ac cmp lb (node l x r) ub m = 320 if apto cmp lb x = LESS then 321 if apto cmp x ub = LESS then 322 bt_to_ol_lb_ub_ac cmp lb l x 323 (x::bt_to_ol_lb_ub_ac cmp x r ub m) 324 else bt_to_ol_lb_ub_ac cmp lb l ub m 325 else bt_to_ol_lb_ub_ac cmp lb r ub m *) 326 327fun bt_to_ol_lb_ub_CONV keyconv = 328let fun oluc t = 329(REWR_CONV lb_ub_ac_nt ORELSEC 330 (REWR_CONV lb_ub_ac_node THENC 331 RATOR_CONV (RATOR_CONV (RAND_CONV (LAND_CONV keyconv))) THENC 332 COND_EQ_LESS_CONV THENC 333 ((RATOR_CONV (RATOR_CONV (RAND_CONV (LAND_CONV keyconv))) THENC 334 COND_EQ_LESS_CONV THENC 335 ((RAND_CONV (RAND_CONV oluc) THENC oluc) ORELSEC 336 oluc)) ORELSEC oluc))) t 337in oluc end; 338 339val [ub_ac_nt, ub_ac_node] = CONJUNCTS bt_to_ol_ub_ac; 340 341(* ub_ac_nt = |- !cmp ub m. bt_to_ol_ub_ac cmp nt ub m = m 342 ub_ac_node = |- !cmp l x r ub m. 343 bt_to_ol_ub_ac cmp (node l x r) ub m = 344 if apto cmp x ub = LESS then 345 bt_to_ol_ub_ac cmp l x (x::bt_to_ol_lb_ub_ac cmp x r ub m) 346 else bt_to_ol_ub_ac cmp l ub m *) 347 348fun bt_to_ol_ub_CONV keyconv = 349let fun ouc t = 350(REWR_CONV ub_ac_nt ORELSEC 351 (REWR_CONV ub_ac_node THENC 352 RATOR_CONV (RATOR_CONV (RAND_CONV (LAND_CONV keyconv))) THENC 353 COND_EQ_LESS_CONV THENC 354 ((RAND_CONV (RAND_CONV (bt_to_ol_lb_ub_CONV keyconv)) THENC ouc) 355 ORELSEC ouc))) t 356in ouc end; 357 358val [lb_ac_nt, lb_ac_node] = CONJUNCTS bt_to_ol_lb_ac; 359 360(* lb_ac_nt = |- !cmp lb m. bt_to_ol_lb_ac cmp lb nt m = m 361 lb_ac_node = |- !cmp lb l x r m. 362 bt_to_ol_lb_ac cmp lb (node l x r) m = 363 if apto cmp lb x = LESS then 364 bt_to_ol_lb_ub_ac cmp lb l x (x::bt_to_ol_lb_ac cmp x r m) 365 else bt_to_ol_lb_ac cmp lb r m *) 366 367fun bt_to_ol_lb_CONV keyconv = 368let fun olc t = 369(REWR_CONV lb_ac_nt ORELSEC 370 (REWR_CONV lb_ac_node THENC 371 RATOR_CONV (RATOR_CONV (RAND_CONV (LAND_CONV keyconv))) THENC 372 COND_EQ_LESS_CONV THENC 373 ((RAND_CONV (RAND_CONV olc) THENC bt_to_ol_lb_ub_CONV keyconv) 374 ORELSEC olc))) t 375in olc end; 376 377(* Top-level conversion works on a bt_to_ol, not a bt_to_ol_ac, term. 378 Improved to check OL_bt first, and if this comes out T, as it always 379 should, to use bt_to_list_CONV in place of bt_to_ol_lb/ub_CONV. *) 380 381val [aTT, aTF, aFT, aFF] = CONJUNCTS (prove ( 382``(T/\T <=> T) /\ (T/\F <=> F) /\ (F/\T <=> F) /\ (F/\F <=> F)``, 383REWRITE_TAC [AND_CLAUSES])); 384 385val AND_CONV = REWR_CONV aTT ORELSEC REWR_CONV aTF ORELSEC 386 REWR_CONV aFT ORELSEC REWR_CONV aFF; 387 388val [OL_lu_nt, OL_lu_node] = CONJUNCTS OL_bt_lb_ub; 389 390(* OL_lu_nt = 391 |- !cmp lb ub. OL_bt_lb_ub cmp lb nt ub <=> (apto cmp lb ub = LESS) 392 OL_lu_node = |- !cmp lb l x r ub. 393 OL_bt_lb_ub cmp lb (node l x r) ub <=> 394 OL_bt_lb_ub cmp lb l x /\ OL_bt_lb_ub cmp x r ub *) 395 396fun OL_bt_lb_ub_CONV keyconv = 397let fun olu t = 398((REWR_CONV OL_lu_nt THENC LAND_CONV keyconv THENC EQ_LESS_CONV) ORELSEC 399 (REWR_CONV OL_lu_node THENC 400 LAND_CONV olu THENC RAND_CONV olu THENC AND_CONV)) t 401in olu end; 402 403val [OL_l_nt, OL_l_node] = CONJUNCTS OL_bt_lb; 404 405(* OL_l_nt = |- !cmp lb. OL_bt_lb cmp lb nt <=> T 406 OL_l_node = 407 |- !cmp lb l x r. OL_bt_lb cmp lb (node l x r) <=> 408 OL_bt_lb_ub cmp lb l x /\ OL_bt_lb cmp x r *) 409 410fun OL_bt_lb_CONV keyconv = 411let fun ol t = 412((REWR_CONV OL_l_node THENC 413 LAND_CONV (OL_bt_lb_ub_CONV keyconv) THENC RAND_CONV ol THENC AND_CONV) 414 ORELSEC REWR_CONV OL_l_nt) t 415in ol end; 416 417val [OL_u_nt, OL_u_node] = CONJUNCTS OL_bt_ub; 418 419(* OL_u_nt = |- !cmp ub. OL_bt_ub cmp nt ub <=> T 420 OL_u_node = |- !cmp l x r ub. 421 OL_bt_ub cmp (node l x r) ub <=> 422 OL_bt_ub cmp l x /\ OL_bt_lb_ub cmp x r ub *) 423 424fun OL_bt_ub_CONV keyconv = 425let fun ou t = 426((REWR_CONV OL_u_node THENC 427 LAND_CONV ou THENC RAND_CONV (OL_bt_lb_ub_CONV keyconv) THENC AND_CONV) 428 ORELSEC REWR_CONV OL_u_nt 429 ) t 430in ou end; 431 432val [OL_nt, OL_node] = CONJUNCTS OL_bt; 433 434(* OL_nt = |- !cmp. OL_bt cmp nt <=> T 435 OL_node = |- !cmp l x r. 436 OL_bt cmp (node l x r) <=> OL_bt_ub cmp l x /\ OL_bt_lb cmp x r *) 437 438fun OL_bt_CONV keyconv = 439(REWR_CONV OL_node THENC LAND_CONV (OL_bt_ub_CONV keyconv) THENC 440 RAND_CONV (OL_bt_lb_CONV keyconv) THENC AND_CONV) 441ORELSEC REWR_CONV OL_nt; 442 443val [ac_nt, ac_node] = CONJUNCTS bt_to_ol_ac; 444 445(* ac_nt = |- !cmp m. bt_to_ol_ac cmp nt m = m 446 ac_node = |- !cmp l x r m. 447 bt_to_ol_ac cmp (node l x r) m = 448 bt_to_ol_ub_ac cmp l x (x::bt_to_ol_lb_ac cmp x r m) *) 449 450fun bt_to_ol_CONV keyconv = 451let fun oc t = 452(REWR_CONV ac_nt ORELSEC 453 (REWR_CONV ac_node THENC 454 RAND_CONV (RAND_CONV (bt_to_ol_lb_CONV keyconv)) THENC 455 bt_to_ol_ub_CONV keyconv)) t 456in REWR_CONV better_bt_to_ol THENC 457 RATOR_CONV (RATOR_CONV (RAND_CONV (OL_bt_CONV keyconv))) THENC 458 COND_CONV THENC 459 (bt_to_list_CONV ORELSEC oc) 460end; 461 462fun ENUMERAL_TO_OWL keyconv et = 463let val (cmp, bt) = 464 dest_binop ``ENUMERAL:'a toto -> 'a bt -> 'a set`` 465 (ERR "ENUMERAL_TO_OWL" "Not an ENUMERAL term") et 466in CONV_RULE (RAND_CONV (bt_to_ol_CONV keyconv)) 467 (ISPECL [cmp, bt] OWL_bt_to_ol) 468end; 469 470(* ***************************************************************** *) 471(* **** set_TO_DISPLAY_CONV, an inverse to DISPLAY_TO_set_CONV ***** *) 472(* **** ENUMERAL_TO_set_CONV, an inverse to set_TO_ENUMERAL_CONV *** *) 473(* ENUMERAL_TO_DISPLAY_CONV, an inverse to DISPLAY_TO_ENUMERAL_CONV *) 474(* TO_set_CONV, converts ENUMERAL, { ... }, set [... ] to set [... ] *) 475(* ***************************************************************** *) 476 477fun ENUMERAL_TO_set_CONV keyconv t = 478 CONJUNCT1 (CONV_RULE (REWR_CONV OWL) (ENUMERAL_TO_OWL keyconv t)); 479 480fun set_TO_DISPLAY_CONV t = 481let val ttype = type_of t; 482 val elem_type = hd (snd (dest_type ttype)); 483 val foldrt = mk_comb (mk_comb (mk_comb 484 (mk_const ("FOLDR", type_subst [alpha |-> elem_type, beta |-> ttype] 485 ``:('a -> 'b -> 'b) -> 'b -> 'a list -> 'b``), 486 mk_const ("INSERT", type_subst [alpha |-> elem_type] 487 ``:'a -> ('a -> bool) -> 'a -> bool``)), 488 mk_const ("EMPTY", type_subst [alpha |-> elem_type] ``:'a -> bool``)), 489 rand t); 490 val iet = rand (concl (REWRITE_CONV [FOLDR] foldrt)) 491in SYM (DISPLAY_TO_set_CONV iet) end; 492 493fun ENUMERAL_TO_DISPLAY_CONV keyconv = ENUMERAL_TO_set_CONV keyconv 494 THENC set_TO_DISPLAY_CONV; 495 496fun TO_set_CONV keyconv = (* keyconv not used if we are converting from 497 { ... } or leaving set [ ... ] alone. *) 498ENUMERAL_TO_set_CONV keyconv ORELSEC DISPLAY_TO_set_CONV ORELSEC REFL; 499 500(* ***************************************************************** *) 501(* OWL_UNION, UNION_CONV *) 502(* ***************************************************************** *) 503 504(* OWL_UNION_THM = |- !cmp s l t m. 505 OWL cmp s l /\ OWL cmp t m ==> OWL cmp (s UNION t) (smerge cmp l m) *) 506 507fun OWL_UNION keyconv owsl owtm = 508CONV_RULE (RAND_CONV (smerge_CONV keyconv)) 509 (MATCH_MP OWL_UNION_THM (CONJ owsl owtm)); 510 511fun UNION_CONV keyconv ust = 512let val (s, t) = 513 dest_binop ``$UNION:'a set -> 'a set -> 'a set`` 514 (ERR "UNION_CONV" "Not a UNION term") ust 515in OWL_TO_ENUMERAL (OWL_UNION keyconv (ENUMERAL_TO_OWL keyconv s) 516 (ENUMERAL_TO_OWL keyconv t)) 517 handle _ => pred_setLib.UNION_CONV keyconv ust 518end; 519 520(* ***************************************************************** *) 521(* OWL_INTER, INTER_CONV *) 522(* ***************************************************************** *) 523 524val [inone_none, isome_none, inone_some, isome_some] = CONJUNCTS sinter; 525 526(* inone_none = |- !cmp. sinter cmp [] [] = [] 527 inone_some = |- !y m cmp. sinter cmp [] (y::m) = [] 528 isome_none = |- !x l cmp. sinter cmp (x::l) [] = [] 529 isome_some = |- !y x m l cmp. sinter cmp (x::l) (y::m) = 530 case apto cmp x y of 531 LESS => sinter cmp l (y::m) 532 | EQUAL => x::sinter cmp l m 533 | GREATER => sinter cmp (x::l) m *) 534 535fun sinter_CONV key_conv = 536let fun inter_c t = 537((REWR_CONV isome_some THENC 538 RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV key_conv))) THENC 539 cpn_REWR_CONV THENC (RAND_CONV inter_c ORELSEC inter_c)) ORELSEC 540REWR_CONV inone_some ORELSEC REWR_CONV isome_none ORELSEC REWR_CONV inone_none) 541t in inter_c end; 542 543(* OWL_INTER_THM = |- !cmp s l t m. 544 OWL cmp s l /\ OWL cmp t m ==> OWL cmp (s INTER t) (sinter cmp l m) *) 545 546fun OWL_INTER keyconv owsl owtm = 547CONV_RULE (RAND_CONV (sinter_CONV keyconv)) 548 (MATCH_MP OWL_INTER_THM (CONJ owsl owtm)); 549 550fun INTER_CONV keyconv ist = 551let val (s, t) = 552 dest_binop ``$INTER:'a set -> 'a set -> 'a set`` 553 (ERR "INTER_CONV" "Not a INTER term") ist 554in OWL_TO_ENUMERAL (OWL_INTER keyconv (ENUMERAL_TO_OWL keyconv s) 555 (ENUMERAL_TO_OWL keyconv t)) 556end; 557 558(* ***************************************************************** *) 559(* OWL_DIFF, SET_DIFF_CONV *) 560(* ***************************************************************** *) 561 562val [dnone_none, dsome_none, dnone_some, dsome_some] = CONJUNCTS sdiff; 563 564(* dnone_none = |- !cmp. sdiff cmp [] [] = [] 565 dnone_some = |- !y m cmp. sdiff cmp [] (y::m) = [] 566 dsome_none = |- !x l cmp. sdiff cmp (x::l) [] = x::l 567 dsome_some = 568 |- !y x m l cmp. 569 sdiff cmp (x::l) (y::m) = 570 case apto cmp x y of 571 LESS => x::sdiff cmp l (y::m) 572 | EQUAL => sdiff cmp l m 573 | GREATER => sdiff cmp (x::l) m *) 574 575fun sdiff_CONV key_conv = 576let fun diff_c t = 577((REWR_CONV dsome_some THENC 578 RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV key_conv))) THENC 579 cpn_REWR_CONV THENC (RAND_CONV diff_c ORELSEC diff_c)) ORELSEC 580REWR_CONV dnone_some ORELSEC REWR_CONV dsome_none ORELSEC REWR_CONV dnone_none) 581t in diff_c end; 582 583(* OWL_DIFF_THM = |- !cmp s l t m. 584 OWL cmp s l /\ OWL cmp t m ==> OWL cmp (s DIFF t) (sdiff cmp l m) *) 585 586fun OWL_DIFF keyconv owsl owtm = 587CONV_RULE (RAND_CONV (sdiff_CONV keyconv)) 588 (MATCH_MP OWL_DIFF_THM (CONJ owsl owtm)); 589 590fun SET_DIFF_CONV keyconv ist = 591let val (s, t) = 592 dest_binop ``$DIFF:'a set -> 'a set -> 'a set`` 593 (ERR "SET_DIFF_CONV" "Not a DIFF term") ist 594in OWL_TO_ENUMERAL (OWL_DIFF keyconv (ENUMERAL_TO_OWL keyconv s) 595 (ENUMERAL_TO_OWL keyconv t)) 596end; 597 598(* ******************************************************************* *) 599(* SET_EXPR_CONV *) 600(* ******************************************************************* *) 601 602(* The purpose of SET_EXPR_CONV is to reduce expressions consisting of *) 603(* more than one UNION, INTER, and/or DIFF applied to ENUMERAL terms, *) 604(* avoiding the overhead of repeated conversion to (mainly) and from *) 605(* the form of OWL theorems. *) 606 607fun SET_EXPR_TO_OWL keyconv t = 608let val c = rator (rator t) 609in if is_const c then 610 let val d = fst (dest_const c) 611 in if d = "ENUMERAL" then ENUMERAL_TO_OWL keyconv t 612 else let val (owl1, owl2) = (SET_EXPR_TO_OWL keyconv (rand (rator t)), 613 SET_EXPR_TO_OWL keyconv (rand t)) 614 in if d = "UNION" then OWL_UNION keyconv owl1 owl2 615 else if d = "INTER" then OWL_INTER keyconv owl1 owl2 616 else if d = "DIFF" then OWL_DIFF keyconv owl1 owl2 617 else raise (ERR "SET_EXPR_TO_OWL" "unrecognized binary operator") 618 end 619 end 620 else raise (ERR "SET_EXPR_TO_OWL" "not a binary operation") 621end; 622 623fun SET_EXPR_CONV keyconv t = OWL_TO_ENUMERAL (SET_EXPR_TO_OWL keyconv t); 624 625(* ********************* sorting: set_TO_OWL **************************** *) 626(* The function set_TO_OWL accepts either a set [ ... ] or a { ... } term *) 627(* and returns the corresponding OWL theorem. *) 628(* ********************************************************************** *) 629 630fun set_TO_OWL keyconv cmp setl = 631let val eqn = (DISPLAY_TO_set_CONV ORELSEC REFL) setl; 632 val th = ISPECL [cmp, rand (rand (concl eqn))] set_OWL_thm 633in CONV_RULE (RAND_CONV (incr_ssort_CONV keyconv) THENC 634 RATOR_CONV (RAND_CONV (REWR_CONV (SYM eqn)))) th end; 635 636(* Test Cases: ****************************************************** 637load "stringLib"; open stringLib; 638 639REVERS_CONV (Term`REVERSE [1; 2; 3; 4; 5]`); 640(* val it = |- REVERSE [1; 2; 3; 4; 5] = [5; 4; 3; 2; 1] : thm *) 641 642val mg = Term`smerge numto [1; 2; 5] [1; 3]`; 643smerge_CONV numto_CONV mg; 644 645val img = Term`incr_smerge numto [1; 5] 646 [SOME [2; 3]]`; 647val imz = Term`incr_smerge numto [3] 648 [NONE; SOME [2; 3]]`; 649incr_smerge_CONV numto_CONV img; 650incr_smerge_CONV numto_CONV imz; 651 652val ibl = Term`incr_sbuild numto [3; 1; 3; 4; 2; 1]`; 653incr_sbuild_CONV numto_CONV ibl; 654 655val mo5 = Term`smerge_out numto [5] 656 [NONE; SOME [1; 3]; SOME [1; 2; 3; 4]]`; 657smerge_out_CONV numto_CONV mo5; 658 659incr_ssort_CONV numto_CONV ``incr_ssort numto [3; 1; 3; 4; 2; 1]``; 660 661val blco = Term`BL_CONS 5 (onebl 7 nt (zerbl (onebl 11 662 (node (node nt 8 nt) 9 (node nt 10 nt)) nbl)))`; 663BL_CONS_CONV blco; 664 665val ltb = Term`list_to_bl [(1,()); (2,()); (3,()); (4,())]`; 666list_to_bl_CONV ltb; 667 668set_TO_ENUMERAL_CONV numto_CONV ``numto`` 669 ``set [10; 9; 8; 7; 6; 5; 4; 3; 2; 1]``; 670 671val bltt = Term`bl_to_bt (onebl (1,()) nt 672 (zerbl 673 (onebl (3,()) 674 (node (node nt (5,()) nt) (7,()) (node nt (9,()) nt)) 675 nbl)))`; 676bl_to_bt_CONV bltt; 677 678list_to_bt_CONV (Term`list_to_bt [(1,()); (2,()); (3,()); (4,())]`); 679 680DISPLAY_TO_set_CONV (Term`{5; 4; 6; 3; 3; 2}`); 681 682DISPLAY_TO_ENUMERAL_CONV numto_CONV ``numto`` ``{3; 4; 6; 7; 7; 7; 7; 3; 3}``; 683 684DISPLAY_TO_ENUMERAL_CONV numto_CONV ``numto`` ``{5; 6; 4; 8; 8; 8; 3; 1}``; 685 686val s100 = Term`{0;1;2;3;4;5;6;7;8;9;10;19;18;17;16;15;14;13;12;11; 687 20;22;24;26;28;30;29;27;25;23;21;39;38;37;36;35;34;33;32;31; 688 40;41;42;43;44;45;56;57;48;49;50;59;58;57;56;55;54;53;52;51; 689 60;63;66;69;61;64;67;62;65;68;79;75;71;78;74;70;77;73;76;72; 690 99;98;96;93;89;84;80;82;85;88;92;95;97;81;83;87;92;91;90;94}`; 691 692val s50 = Term`{10;19;18;17;16;15;14;13;12;11; 693 40;41;42;43;44;45;56;57;48;49;50;59;58;57;56;55;54;53;52;51; 694 99;98;96;93;89;84;80;82;85;88;92;95;97;81;83;87;92;91;90;94}`; 695 696val t50 = DISPLAY_TO_ENUMERAL_CONV numto_CONV (Term`numto`) s50; 697 (* 14977 infs. 0.064s *) 698val qt50 = DISPLAY_TO_ENUMERAL_CONV qk_numto_CONV (Term`qk_numto`) s50; 699 (* 13112 infs 0.064s *) 700val t100 = DISPLAY_TO_ENUMERAL_CONV numto_CONV (Term`numto`) s100; 701 (* 30873 infs. 0.140s *) 702val qt100 = DISPLAY_TO_ENUMERAL_CONV qk_numto_CONV (Term`qk_numto`) s100; 703 (* 29400 infs 0.148s*) 704 705val apft = Term`5 IN ENUMERAL numto (node nt 5 nt)`; 706IN_CONV numto_CONV apft; 707val apgt = Term`6 IN ENUMERAL numto (node nt 5 nt)`; 708IN_CONV numto_CONV apgt; 709IN_CONV REDUCE_CONV ``5 IN {3; 5; 2}``; (* fall-back to pred_setLib *) 710IN_CONV REDUCE_CONV ``6 IN {3; 5; 2}``; 711 712val fake = ASSUME ``OWL numto {5; 4; 3} [3; 4; 5]``; 713 OWL_TO_ENUMERAL fake; 714 715bt_to_list_CONV ``bt_to_list_ac 716 (node (node nt 1 nt) 2 (node (node nt 3 nt) 4 (node nt 5 nt))) []``; 717 718val cmp = ``numto``; 719val tbt = rand (rand (concl (DISPLAY_TO_ENUMERAL_CONV 720 numto_CONV ``numto`` ``{1;2;3;4;5}``))); 721val bolt = ``bt_to_ol_lb_ub_ac ^cmp 0 ^tbt 4 []``; 722val bolt' = ``bt_to_ol_lb_ub_ac ^cmp 0 ^tbt 8 []``; 723val bolt'' = ``bt_to_ol_lb_ub_ac ^cmp 2 ^tbt 5 []``; 724bt_to_ol_lb_ub_CONV numto_CONV bolt; 725 726val bult = ``bt_to_ol_ub_ac ^cmp ^tbt 4 []``; 727val bult' = ``bt_to_ol_ub_ac ^cmp ^tbt 8 []``; 728bt_to_ol_ub_CONV numto_CONV bult; 729 730val bllt = ``bt_to_ol_lb_ac ^cmp 2 ^tbt []``; 731val bllt' = ``bt_to_ol_lb_ac ^cmp 0 ^tbt []``; 732bt_to_ol_lb_CONV numto_CONV bllt; 733 734val blt = ``bt_to_ol numto ^tbt``; 735bt_to_ol_CONV numto_CONV blt; 736val badbt = ``node (node nt 1 nt) 3 (node (node nt 3 nt) 4 (node nt 1 nt))``; 737val badblt = ``bt_to_ol numto ^badbt``; 738bt_to_ol_CONV numto_CONV badblt; 739 740val tet = rand (concl (DISPLAY_TO_ENUMERAL_CONV 741 numto_CONV ``numto`` ``{4;1;3;5;2}``)); 742val owa = ENUMERAL_TO_OWL numto_CONV tet; 743 744set_TO_DISPLAY_CONV ``set [5;4;3;2;1]``; 745ENUMERAL_TO_set_CONV numto_CONV tet; 746ENUMERAL_TO_DISPLAY_CONV numto_CONV tet; 747 748TO_set_CONV numto_CONV tet; 749TO_set_CONV NO_CONV ``{5; 4; 3; 2; 1}``; 750TO_set_CONV NO_CONV ``set [5; 4; 3; 2; 1]``; 751 752val owb = ENUMERAL_TO_OWL numto_CONV (rand (concl 753 (DISPLAY_TO_ENUMERAL_CONV numto_CONV ``numto`` ``{0;3;1;8}``))); 754OWL_UNION numto_CONV owa owb; 755OWL_UNION numto_CONV owb owa; 756 757val wet = rand (concl (DISPLAY_TO_ENUMERAL_CONV 758 numto_CONV ``numto`` ``{8;3;1;0}``)); 759val utwet = ``^tet UNION ^wet``; 760UNION_CONV numto_CONV utwet; 761UNION_CONV REDUCE_CONV ``{1;5} UNION {3;2}``; 762 763val ig = Term`sinter numto [1; 2; 5] [1; 3]`; 764sinter_CONV numto_CONV ig; 765 766OWL_INTER numto_CONV owa owb; 767 768val itwet = ``^tet INTER ^wet``; 769INTER_CONV numto_CONV itwet; 770 771val ig' = Term`sdiff numto [1; 2; 5] [1; 3]`; 772sdiff_CONV numto_CONV ig'; 773 774OWL_DIFF numto_CONV owa owb; 775 776val itwet' = ``^tet DIFF ^wet``; 777SET_DIFF_CONV numto_CONV itwet'; 778 779val ta = rand (concl (DISPLAY_TO_ENUMERAL_CONV 780 numto_CONV ``numto`` ``{4;1;3;5;2}``)); 781val tb = rand (concl (DISPLAY_TO_ENUMERAL_CONV 782 numto_CONV ``numto`` ``{3; 4; 6; 7; 3}``)); 783val tc = rand (concl (DISPLAY_TO_ENUMERAL_CONV 784 numto_CONV ``numto`` 785 ``{5; 6; 4; 8; 3; 1}``)); 786 787SET_EXPR_TO_OWL numto_CONV ``(^ta) UNION (^tb) INTER (^tc)``; 788 789SET_EXPR_CONV numto_CONV ``(^ta) UNION (^tb) INTER (^tc)``; 790SET_EXPR_CONV numto_CONV ``(^tb) UNION (^tc) DIFF (^ta)``; 791SET_EXPR_CONV numto_CONV ta; (* expensive identity function, though 792 it would prune unreachable parts of the tree if there could be any. *) 793 794set_TO_OWL numto_CONV ``numto`` ``set [5; 3; 3; 3; 4; 2; 3; 1]``; 795set_TO_OWL numto_CONV ``numto`` ``{5; 3; 3; 3; 4; 2; 3; 1}``; 796********************************************************************* *) 797end; 798