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