1(* File: fmapalTacs.sml. Author: F. Lockwood Morris. Begun 6 Aug 2013. *) 2 3(* Basic conversions and conversionals, and inference rules for *) 4(* sorting lists, building FMAPALS, look-up and converting them to *) 5(* lists and uniting and restricting them. *) 6 7structure fmapalTacs :> fmapalTacs = 8struct 9(* comment out load before Holmaking *) 10(* app load ["totoTheory", "pred_setLib", 11"reduceLib", "relationTheory", "enumeralTheory", "fmapalTheory", "enumTacs", 12"totoTacs", "bossLib", "finite_mapTheory", "listLib"]; *) 13 14open Parse HolKernel boolLib bossLib; 15 16val _ = set_trace "Unicode" 0; 17open totoTheory reduceLib bossLib 18 relationTheory listTheory pairTheory optionTheory enumeralTheory pred_setLib 19 totoTacs finite_mapTheory fmapalTheory enumTacs listLib; 20 21val AR = ASM_REWRITE_TAC []; 22fun ulist x = [x]; 23 24val ERR = mk_HOL_ERR "fmapalTacs"; 25 26(* **************************************************************** *) 27(* See introductory comment in enumTacs.sml. *) 28(* **************************************************************** *) 29 30(* ********************************************************************** *) 31(* Conversions for sorting lists with constant keys *) 32(* ********************************************************************** *) 33 34val [none_any, some_none, some_some] = CONJUNCTS merge; 35 36(* none_any = |- !l cmp. merge cmp [] l = l: thm 37 some_none = |- !v5 v4 cmp. merge cmp (v4::v5) [] = v4::v5: thm 38 some_some = |- !l2 l1 cmp b2 b1 a2 a1. 39 merge cmp ((a1,b1)::l1) ((a2,b2)::l2) = 40 case apto cmp a1 a2 of 41 LESS => (a1,b1)::merge cmp l1 ((a2,b2)::l2) 42 | EQUAL => (a1,b1)::merge cmp l1 l2 43 | GREATER => (a2,b2)::merge cmp ((a1,b1)::l1) l2 *) 44 45fun merge_CONV key_conv = 46let fun merge_c t = 47((REWR_CONV some_some THENC 48 RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV key_conv))) THENC 49 cpn_REWR_CONV THENC RAND_CONV merge_c) ORELSEC 50REWR_CONV none_any ORELSEC REWR_CONV some_none) t 51in merge_c end; 52 53val [im_lengthen, im_zero, im_one] = CONJUNCTS incr_merge; 54 55(* im_lengthen = |- !l cmp. incr_merge cmp l [] = [SOME l] 56 im_zero = |- !lol l cmp. incr_merge cmp l (NONE::lol) = SOME l::lol 57 im_one = |- !m lol l cmp. 58 incr_merge cmp l (SOME m::lol) = 59 NONE::incr_merge cmp (merge cmp l m) lol *) 60 61fun incr_merge_CONV key_conv = 62let fun im_c t = ((REWR_CONV im_one THENC 63 RAND_CONV (RATOR_CONV (RAND_CONV (merge_CONV key_conv)) 64 THENC im_c)) 65 ORELSEC REWR_CONV im_zero ORELSEC REWR_CONV im_lengthen) t 66in im_c end; 67 68val [ib_base, ib_rec] = CONJUNCTS incr_build; 69 70(* ib_base = |- !cmp. incr_build cmp [] = [] : thm 71 val ib_rec = |- !cmp ab l. 72 incr_build cmp (ab::l) = incr_merge cmp [ab] (incr_build cmp l) *) 73 74fun incr_build_CONV key_conv = 75let fun ib_c t = ((REWR_CONV ib_rec THENC RAND_CONV ib_c THENC 76 incr_merge_CONV key_conv) 77 ORELSEC REWR_CONV ib_base) t 78in ib_c end; 79 80val [mo_base, mo_none, mo_some] = CONJUNCTS merge_out; 81 82(* mo_base = |- !l cmp. merge_out cmp l [] = l 83 mo_none = |- !lol l cmp. merge_out cmp l (NONE::lol) = merge_out cmp l lol 84 mo_some = |- !m lol l cmp. 85 merge_out cmp l (SOME m::lol) = merge_out cmp (merge cmp l m) lol *) 86 87fun merge_out_CONV key_conv = 88let fun mo_c t = ((REWR_CONV mo_some THENC 89 RATOR_CONV (RAND_CONV (merge_CONV key_conv)) THENC 90 mo_c) ORELSEC 91 (REWR_CONV mo_none THENC mo_c) ORELSEC 92 REWR_CONV mo_base) t 93in mo_c end; 94 95fun incr_sort_CONV keyconv = 96 (REWR_CONV incr_sort THENC RAND_CONV (incr_build_CONV keyconv) THENC 97 merge_out_CONV keyconv) ORELSEC 98(fn _ => Raise (mk_HOL_ERR "fmapalTacs" "incr_sort_CONV" 99 "not a list of explicit pairs")); 100 101(* ****************************************************************** *) 102(* fmap_TO_FMAPAL_CONV, FUN_fmap_CONV, FUN_FMAPAL_CONV *) 103(* ****************************************************************** *) 104 105(* fmap_TO_FMAPAL_CONV: convert ``fmap l`` to ``FMAPAL ...`` *) 106 107fun fmap_TO_FMAPAL_CONV keyconv cmp = 108REWR_CONV (ISPEC cmp FMAPAL_fmap) THENC 109RAND_CONV (RAND_CONV (incr_sort_CONV keyconv)) THENC 110RAND_CONV list_to_bt_CONV; 111 112(* There seems to be no pre-provided explicit notation for a finite map 113 in extension than is provided by fmap; hence we supply here only 114 fmap_TO_FMAPAL_CONV, analogous to set_TO_ENUMERAL_CONV, but no analogue for 115 DISPLAY_TO_ENUMERAL_CONV. *) 116 117(* FUN_fmap_CONV: convert FUN_FMAP f [ ... ] to fmap [ ... ], given a *) 118(* conversion for working out applications of f. *) 119 120fun FUN_fmap_CONV elemconv = 121REWR_CONV (GSYM FUN_fmap_thm) THENC 122RAND_CONV (MAP_CONV (BETA_CONV THENC RAND_CONV elemconv)); 123 124(* FUN_FMAPAL_CONV: convert FUN_FMAP f [ ... ] to FMAPAL cmp ..., *) 125(* given a conversion for evaluating applications of cmp, and cmp, and *) 126(* another conversion for working out applications of f. *) 127 128fun FUN_FMAPAL_CONV keyconv cmp elemconv = 129FUN_fmap_CONV elemconv THENC fmap_TO_FMAPAL_CONV keyconv cmp; 130 131(* ******************************************************************* *) 132(* The one pure conversion working on directly on fmaps of the form *) 133(* FMAPAL cmp ... is FAPPLY_CONV. Analogously to IN_CONV, it will *) 134(* do linear search in an fmap [ ... ] term with an equality-deciding *) 135(* conversion if it does not get the toto-evaluating conversion and *) 136(* FMAPAL cmp ... ' x term it expects. *) 137(* ******************************************************************* *) 138 139(* FAPPLY_node = |- !cmp x l a b r. 140 FMAPAL cmp (node l (a,b) r) ' x = case apto cmp x a of 141 LESS => FMAPAL cmp l ' x | EQUAL => b | GREATER => FMAPAL cmp r ' x 142 143 FAPPLY_nt = |- !cmp x. FMAPAL cmp nt ' x = FEMPTY ' x *) 144 145fun FAPPLY_CONV keyconv = 146let fun apf_c t = ((REWR_CONV FAPPLY_node THENC RATOR_CONV 147 (RATOR_CONV (RATOR_CONV (RAND_CONV keyconv))) THENC 148 cpn_REWR_CONV THENC (apf_c ORELSEC ALL_CONV)) ORELSEC 149 REWR_CONV FAPPLY_nt) t; 150 fun apf_i t = ((REWR_CONV FAPPLY_fmap_CONS THENC 151 RATOR_CONV (RATOR_CONV (RAND_CONV keyconv)) THENC 152 COND_CONV THENC 153 TRY_CONV apf_i) ORELSEC REWR_CONV FAPPLY_fmap_NIL) t 154in apf_c ORELSEC apf_i end; (* I don't seem able to report an exception. *) 155 156(* ******************************************************************* *) 157(* To perform binary operations on fmaps, or between fmaps and sets, *) 158(* efficiently, we shall deal not in equations, as with proper *) 159(* conversions, but with terms of the form ORWL cmp <fmap expn> l, *) 160(* abbreviating (<fmap expn> = fmap l) /\ ORL l, and the form OWL s m, *) 161(* abbreviating (s = set m) /\ OL m, s a <set expn>. We now give *) 162(* conversion-like functions to go back and forth between ORWL theorems*) 163(* and FMAPAL terms. enumTacs has the same for OWL and ENUMERAL. *) 164(* ******************************************************************* *) 165 166(* ***************************************************************** *) 167(* ORWL_TO_FMAPAL, FMAPAL_TO_ORWL, FMAPAL_TO_fmap_CONV *) 168(* ***************************************************************** *) 169 170(* Translate |- ORWL cmp f l to |- f = FMAPAL cmp ... . *) 171 172fun ORWL_TO_FMAPAL orwl = 173let val (eqn, orwl) = CONJ_PAIR (CONV_RULE (REWR_CONV ORWL) orwl); 174 val raw_ans = TRANS eqn (MATCH_MP ORL_FMAPAL orwl) 175in CONV_RULE (RAND_CONV (RAND_CONV list_to_bt_CONV)) raw_ans end; 176 177(* We need bt_to_orl_CONV, with _lb, _ub, _lb_ub variants, using _ac thms. *) 178 179(* Remember that the ... = LESS comparisons will in practice always come out 180 true. I can see no harm, however, in making bt_to_orl_CONV work correctly 181 for arbitrary trees. *) 182 183(* EQ_LESS_CONV converts cpn = LESS to one of T, F *) 184(* COND_EQ_LESS_CONV coverts if cpn = LESS then a else b to one of a, b *) 185 186val [lb_ub_acf_nt, lb_ub_acf_node] = CONJUNCTS bt_to_orl_lb_ub_ac; 187 188(* lb_ub_acf_nt = |- !ub m lb cmp. bt_to_orl_lb_ub_ac cmp lb nt ub m = m 189 lb_ub_acf_node = |- !y x ub r m lb l cmp. 190 bt_to_orl_lb_ub_ac cmp lb (node l (x,y) r) ub m = 191 if apto cmp lb x = LESS then 192 if apto cmp x ub = LESS then 193 bt_to_orl_lb_ub_ac cmp lb l x 194 ((x,y)::bt_to_orl_lb_ub_ac cmp x r ub m) 195 else bt_to_orl_lb_ub_ac cmp lb l ub m 196 else bt_to_orl_lb_ub_ac cmp lb r ub m *) 197 198fun bt_to_orl_lb_ub_CONV keyconv = 199let fun orluc t = 200(REWR_CONV lb_ub_acf_nt ORELSEC 201 (REWR_CONV lb_ub_acf_node THENC 202 RATOR_CONV (RATOR_CONV (RAND_CONV (LAND_CONV keyconv))) THENC 203 COND_EQ_LESS_CONV THENC 204 ((RATOR_CONV (RATOR_CONV (RAND_CONV (LAND_CONV keyconv))) THENC 205 COND_EQ_LESS_CONV THENC 206 ((RAND_CONV (RAND_CONV orluc) THENC orluc) ORELSEC 207 orluc)) ORELSEC orluc))) t 208in orluc end; 209 210val [ub_acf_nt, ub_acf_node] = CONJUNCTS bt_to_orl_ub_ac; 211 212(* ub_acf_nt = |- !ub m cmp. bt_to_orl_ub_ac cmp nt ub m = m 213 ub_acf_node = |- !y x ub r m l cmp. 214 bt_to_orl_ub_ac cmp (node l (x,y) r) ub m = 215 if apto cmp x ub = LESS then 216 bt_to_orl_ub_ac cmp l x ((x,y)::bt_to_orl_lb_ub_ac cmp x r ub m) 217 else bt_to_orl_ub_ac cmp l ub m *) 218 219fun bt_to_orl_ub_CONV keyconv = 220let fun oruc t = 221(REWR_CONV ub_acf_nt ORELSEC 222 (REWR_CONV ub_acf_node THENC 223 RATOR_CONV (RATOR_CONV (RAND_CONV (LAND_CONV keyconv))) THENC 224 COND_EQ_LESS_CONV THENC 225 ((RAND_CONV (RAND_CONV (bt_to_orl_lb_ub_CONV keyconv)) THENC oruc) 226 ORELSEC oruc))) t 227in oruc end; 228 229val [lb_acf_nt, lb_acf_node] = CONJUNCTS bt_to_orl_lb_ac; 230 231(* lb_acf_nt = |- !m lb cmp. bt_to_orl_lb_ac cmp lb nt m = m 232 lb_acf_node = |- !y x r m lb l cmp. 233 bt_to_orl_lb_ac cmp lb (node l (x,y) r) m = 234 if apto cmp lb x = LESS then 235 bt_to_orl_lb_ub_ac cmp lb l x ((x,y)::bt_to_orl_lb_ac cmp x r m) 236 else bt_to_orl_lb_ac cmp lb r m *) 237 238fun bt_to_orl_lb_CONV keyconv = 239let fun orlc t = 240(REWR_CONV lb_acf_nt ORELSEC 241 (REWR_CONV lb_acf_node THENC 242 RATOR_CONV (RATOR_CONV (RAND_CONV (LAND_CONV keyconv))) THENC 243 COND_EQ_LESS_CONV THENC 244 ((RAND_CONV (RAND_CONV orlc) THENC bt_to_orl_lb_ub_CONV keyconv) 245 ORELSEC orlc))) t 246in orlc end; 247 248(* Top-level conversion works on a bt_to_orl, not a bt_to_orl_ac, term. 249 Improved, imitating enumTacs, to check ORL_bt first. *) 250 251val [ORL_lu_nt, ORL_lu_node] = CONJUNCTS ORL_bt_lb_ub; 252 253(* ORL_lu_nt = 254 |- !ub lb cmp. ORL_bt_lb_ub cmp lb nt ub <=> (apto cmp lb ub = LESS) 255 ORL_lu_node = |- !y x ub r lb l cmp. 256 ORL_bt_lb_ub cmp lb (node l (x,y) r) ub <=> 257 ORL_bt_lb_ub cmp lb l x /\ ORL_bt_lb_ub cmp x r ub *) 258 259fun ORL_bt_lb_ub_CONV keyconv = 260let fun olu t = 261((REWR_CONV ORL_lu_nt THENC LAND_CONV keyconv THENC EQ_LESS_CONV) ORELSEC 262 (REWR_CONV ORL_lu_node THENC 263 LAND_CONV olu THENC RAND_CONV olu THENC AND_CONV)) t 264in olu end; 265 266val [ORL_l_nt, ORL_l_node] = CONJUNCTS ORL_bt_lb; 267 268(* ORL_l_nt = |- !lb cmp. ORL_bt_lb cmp lb nt <=> T 269 ORL_l_node = |- !y x r lb l cmp. 270 ORL_bt_lb cmp lb (node l (x,y) r) <=> 271 ORL_bt_lb_ub cmp lb l x /\ ORL_bt_lb cmp x r *) 272 273fun ORL_bt_lb_CONV keyconv = 274let fun ol t = 275((REWR_CONV ORL_l_node THENC 276 LAND_CONV (ORL_bt_lb_ub_CONV keyconv) THENC RAND_CONV ol THENC AND_CONV) 277 ORELSEC REWR_CONV ORL_l_nt) t 278in ol end; 279 280val [ORL_u_nt, ORL_u_node] = CONJUNCTS ORL_bt_ub; 281 282(* ORL_u_nt = |- !ub cmp. ORL_bt_ub cmp nt ub <=> T 283 ORL_u_node = |- !y x ub r l cmp. 284 ORL_bt_ub cmp (node l (x,y) r) ub <=> 285 ORL_bt_ub cmp l x /\ ORL_bt_lb_ub cmp x r ub *) 286 287fun ORL_bt_ub_CONV keyconv = 288let fun ou t = 289((REWR_CONV ORL_u_node THENC 290 LAND_CONV ou THENC RAND_CONV (ORL_bt_lb_ub_CONV keyconv) THENC AND_CONV) 291 ORELSEC REWR_CONV ORL_u_nt 292 ) t 293in ou end; 294 295val [ORL_nt, ORL_node] = CONJUNCTS ORL_bt; 296 297(* ORL_nt = |- ORL_bt cmp nt <=> T 298 ORL_node = |- ORL_bt cmp (node l (x,y) r) <=> 299 ORL_bt_ub cmp l x /\ ORL_bt_lb cmp x r *) 300 301fun ORL_bt_CONV keyconv = 302(REWR_CONV ORL_node THENC LAND_CONV (ORL_bt_ub_CONV keyconv) THENC 303 RAND_CONV (ORL_bt_lb_CONV keyconv) THENC AND_CONV) 304ORELSEC REWR_CONV ORL_nt; 305 306val [acf_nt, acf_node] = CONJUNCTS bt_to_orl_ac; 307 308(* acf_nt = |- bt_to_orl_ac cmp nt m = m 309 acf_node = |- bt_to_orl_ac cmp (node l (x,y) r) m = 310 bt_to_orl_ub_ac cmp l x ((x,y)::bt_to_orl_lb_ac cmp x r m) *) 311 312fun bt_to_orl_CONV keyconv = 313let fun oc t = 314(REWR_CONV acf_nt ORELSEC 315 (REWR_CONV acf_node THENC 316 RAND_CONV (RAND_CONV (bt_to_orl_lb_CONV keyconv)) THENC 317 bt_to_orl_ub_CONV keyconv)) t 318in REWR_CONV better_bt_to_orl THENC 319 RATOR_CONV (RATOR_CONV (RAND_CONV (ORL_bt_CONV keyconv))) THENC 320 COND_CONV THENC 321 (bt_to_list_CONV ORELSEC oc) 322end; 323 324fun FMAPAL_TO_ORWL keyconv ft = 325let val (cmp, bt) = 326 dest_binop ``FMAPAL:'a toto -> ('a#'b)bt -> ('a|->'b)`` 327 (ERR "FMAPAL_TO_ORWL" "Not a FMAPAL term") ft 328in CONV_RULE (RAND_CONV (bt_to_orl_CONV keyconv)) 329 (ISPECL [cmp, bt] ORWL_bt_to_orl) 330end; 331 332fun FMAPAL_TO_fmap_CONV keyconv t = 333 CONJUNCT1 (CONV_RULE (REWR_CONV ORWL) (FMAPAL_TO_ORWL keyconv t)); 334 335(* ***************************************************************** *) 336(* ORWL_FUNION, FUNION_CONV *) 337(* ***************************************************************** *) 338 339(* ORWL_FUNION_THM = |- !cmp s l t m. 340 ORWL cmp s l /\ ORWL cmp t m ==> ORWL cmp (s FUNION t) (merge cmp l m) *) 341 342fun ORWL_FUNION keyconv orwsl orwtm = 343CONV_RULE (RAND_CONV (merge_CONV keyconv)) 344 (MATCH_MP ORWL_FUNION_THM (CONJ orwsl orwtm)); 345 346fun FUNION_CONV keyconv ust = 347let val (s, t) = 348 dest_binop ``$FUNION:('a|->'b) -> ('a|->'b) -> ('a|->'b)`` 349 (ERR "FUNION_CONV" "Not a FUNION term") ust 350in ORWL_TO_FMAPAL (ORWL_FUNION keyconv (FMAPAL_TO_ORWL keyconv s) 351 (FMAPAL_TO_ORWL keyconv t)) 352end; 353 354(* ***************************************************************** *) 355(* ORWL_DRESTRICT *) 356(* ***************************************************************** *) 357 358val [imnone_none, imsome_none, imnone_some,imsome_some] = CONJUNCTS inter_merge; 359 360(* imnone_none = |- !cmp. inter_merge cmp [] [] = [] 361 imnone_some = |- !y m cmp. inter_merge cmp [] (y::m) = [] 362 imsome_none = |- !l cmp b a. inter_merge cmp ((a,b)::l) [] = [] 363 imsome_some = |- !y m l cmp b a. 364 inter_merge cmp ((a,b)::l) (y::m) = 365 case apto cmp a y of 366 LESS => inter_merge cmp l (y::m) 367 | EQUAL => (a,b)::inter_merge cmp l m 368 | GREATER => inter_merge cmp ((a,b)::l) m *) 369 370fun inter_merge_CONV keyconv = 371let fun interm_c t = 372((REWR_CONV imsome_some THENC 373 RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV keyconv))) THENC 374 cpn_REWR_CONV THENC (RAND_CONV interm_c ORELSEC interm_c)) ORELSEC 375REWR_CONV imnone_some ORELSEC REWR_CONV imsome_none 376 ORELSEC REWR_CONV imnone_none) 377t in interm_c end; 378 379(* ORWL_DRESTRICT_THM = |- !cmp s l t m. ORWL cmp s l /\ OWL cmp t m ==> 380 ORWL cmp (DRESTRICT s t) (inter_merge cmp l m) *) 381 382fun ORWL_DRESTRICT keyconv orwsl owtm = 383CONV_RULE (RAND_CONV (inter_merge_CONV keyconv)) 384 (MATCH_MP ORWL_DRESTRICT_THM (CONJ orwsl owtm)); 385 386(* See below for DRESTRICT_CONV *) 387 388(* ***************************************************************** *) 389(* ORWL_DRESTRICT_COMPL, DRESTRICT_CONV *) 390(* ***************************************************************** *) 391 392val [dmnone_none, dmsome_none, dmnone_some, dmsome_some] = CONJUNCTS diff_merge; 393 394(* dmnone_none = |- !cmp. diff_merge cmp [] [] = [] 395 dmnone_some = |- !y m cmp. diff_merge cmp [] (y::m) = [] 396 dmsome_none = |- !l cmp b a. diff_merge cmp ((a,b)::l) [] = (a,b)::l 397 dmsome_some = 398 |- !y m l cmp b a. 399 diff_merge cmp ((a,b)::l) (y::m) = 400 case apto cmp a y of 401 LESS => (a,b)::diff_merge cmp l (y::m) 402 | EQUAL => diff_merge cmp l m 403 | GREATER => diff_merge cmp ((a,b)::l) m *) 404 405fun diff_merge_CONV keyconv = 406let fun diffm_c t = 407((REWR_CONV dmsome_some THENC 408 RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV keyconv))) THENC 409 cpn_REWR_CONV THENC (RAND_CONV diffm_c ORELSEC diffm_c)) ORELSEC 410REWR_CONV dmnone_some ORELSEC REWR_CONV dmsome_none 411 ORELSEC REWR_CONV dmnone_none) 412t in diffm_c end; 413 414(* ORWL_DRESTRICT_COMPL_THM = |- !cmp s l t m. 415 ORWL cmp s l /\ OWL cmp t m ==> 416 ORWL cmp (DRESTRICT s (COMPL t)) (diff_merge cmp l m) *) 417 418fun ORWL_DRESTRICT_COMPL keyconv orwsl owtm = 419CONV_RULE (RAND_CONV (diff_merge_CONV keyconv)) 420 (MATCH_MP ORWL_DRESTRICT_COMPL_THM (CONJ orwsl owtm)); 421 422(* One conversion, DRESTRICT_CONV, serves for both 423 DRESTRICT ... (ENUMERAL ... ) and DRESTRICT ... (COMPL (ENUMERAL ... )) 424 terms, and even cancels multiple COMPL's. *) 425 426fun DRESTRICT_CONV keyconv mst = 427let val (s, t) = 428 dest_binop ``DRESTRICT:('a|->'b) -> 'a set -> ('a|->'b)`` 429 (ERR "DRESTRICT_CONV" "Not a DRESTRICT term") mst 430in if is_comb t andalso is_const (rator t) andalso 431 fst (dest_const (rator t)) = "COMPL" 432 then if is_comb (rand t) andalso is_const (rator (rand t)) andalso 433 fst (dest_const (rator (rand t))) = "COMPL" 434 then (RAND_CONV (REWR_CONV pred_setTheory.COMPL_COMPL) THENC 435 DRESTRICT_CONV keyconv) mst 436 else ORWL_TO_FMAPAL (ORWL_DRESTRICT_COMPL keyconv 437 (FMAPAL_TO_ORWL keyconv s) (ENUMERAL_TO_OWL keyconv (rand t))) 438 else ORWL_TO_FMAPAL (ORWL_DRESTRICT keyconv 439 (FMAPAL_TO_ORWL keyconv s) (ENUMERAL_TO_OWL keyconv t)) 440end; 441 442(* **************************************************************** *) 443(* MAP_ELEM_CONV, MAP_CONV, FDOM_CONV, o_f_CONV *) 444(* **************************************************************** *) 445 446(* Following function maps a conversion over an explicit list term 447 (blindly assuming any constant term is [] and any other is a :: l). 448 ONCE_DEPTH_CONV seems to do just as well. *) 449 450fun MAP_ELEM_CONV elemconv = 451let fun mec t = 452if is_const t then REFL t else (LAND_CONV elemconv THENC RAND_CONV mec) t 453in mec end; 454 455(* We also need listLib.MAP_CONV, simplifying a (MAP f [ ... ]) term. *) 456 457(* bt_FST_FDOM = |- !cmp t. FDOM (FMAPAL cmp t) = ENUMERAL cmp (bt_map FST t)*) 458 459(* bt_map = |- (!f. bt_map f nt = nt) /\ 460 !f l x r. bt_map f (node l x r) = node (bt_map f l) (f x) (bt_map f r) *) 461 462val [bm_nft, bm_node] = CONJUNCTS bt_map; 463 464fun bt_map_CONV fconv ft = 465let val f = rator (rand ft); 466 fun bmn t = 467 (REWR_CONV bm_nft ORELSEC 468 (REWR_CONV bm_node THENC (RATOR_CONV (RAND_CONV fconv)) THENC 469 RAND_CONV bmn THENC 470 RATOR_CONV (RATOR_CONV (RAND_CONV bmn)))) t 471in bmn ft end; 472 473val FDOM_CONV = (REWR_CONV bt_FST_FDOM THENC 474 RAND_CONV (bt_map_CONV (REWR_CONV FST))) ORELSEC 475 (REWR_CONV fmap_FDOM THENC 476 RAND_CONV (MAP_CONV (REWR_CONV FST))); 477 478(* We may save work with a separate IN_FDOM_CONV, also made to *) 479(* work (slowly) for fmap [ .... ] too. *) 480 481val [in_fdom_nt, in_fdom_node] = CONJUNCTS FMAPAL_FDOM_THM; 482 483(* in_fdom_nt = |- !cmp x. x IN FDOM (FMAPAL cmp nt) <=> F 484 in_fdom_node = |- !cmp x a b l r. 485 x IN FDOM (FMAPAL cmp (node l (a,b) r)) <=> 486 case apto cmp x a of 487 LESS => x IN FDOM (FMAPAL cmp l) 488 | EQUAL => T 489 | GREATER => x IN FDOM (FMAPAL cmp r) *) 490 491val [notinfdomnil,infdomcons] = CONJUNCTS fmap_FDOM_rec; 492 493(* notinfdomnil = |- !x. x IN FDOM (fmap []) <=> F 494 infdomcons = |- !x w z l. 495 x IN FDOM (fmap ((w,z)::l)) <=> (x = w) \/ x IN FDOM (fmap l) *) 496 497val [T_OR, F_OR] = CONJUNCTS (prove (``(!p. T \/ p = T) /\ (!p. F \/ p = p)``, 498 REWRITE_TAC [OR_CLAUSES])); 499 500fun IN_FDOM_CONV keyconv = 501let fun ifc t = 502((REWR_CONV in_fdom_node THENC 503 RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV keyconv))) THENC 504 cpn_REWR_CONV THENC (ifc ORELSEC ALL_CONV)) ORELSEC 505 REWR_CONV in_fdom_nt) t; 506fun ifl t = ((REWR_CONV infdomcons THENC RATOR_CONV (RAND_CONV keyconv) THENC 507 ((REWR_CONV F_OR THENC ifl) ORELSEC REWR_CONV T_OR)) 508 ORELSEC REWR_CONV notinfdomnil) t 509in ifc ORELSEC ifl end; 510 511(* o_f_CONV works out terms of the form f o_f FMAPAL ... to FMAPAL ...., given 512 a conversion for working out f, also terms of the form 513 f o_f fmap [ ... ] to fmap [ ......... ]. *) 514 515fun o_f_CONV fconv = 516 (REWR_CONV o_f_bt_map THENC 517 RAND_CONV (bt_map_CONV (REWR_CONV AP_SND THENC (RAND_CONV fconv)))) ORELSEC 518 (REWR_CONV o_f_fmap THENC (RAND_CONV 519 (MAP_CONV (REWR_CONV AP_SND THENC (RAND_CONV fconv))))); 520 521(* **************************************************************** *) 522(* fmap_FUPDATE_CONV, FMAPAL_FUPDATE_CONV *) 523(* **************************************************************** *) 524 525val [lrc_NIL, lrc_CONS] = CONJUNCTS list_rplacv_cn; 526 527fun list_rplacv_CONV eqconv = 528let fun lrcn t = 529((REWR_CONV lrc_CONS THENC RATOR_CONV (RATOR_CONV (RAND_CONV eqconv)) THENC 530 COND_CONV THENC TRY_CONV lrcn) ORELSEC 531 REWR_CONV lrc_NIL) t 532in lrcn THENC REPEATC BETA_CONV end; 533 534(* Following conversion reduces terms of the form fmap [ ... ] |+ (x,y), 535 provided a pair (x,w) already occurs in [ ... ]. *) 536 537val NOT_CONS_NIL_EQN = prove (``!ab:'a#'b l. ((ab::l) = []) = F``, 538REWRITE_TAC [NOT_CONS_NIL]); 539 540fun fmap_FUPDATE_CONV eqconv t = 541let val (fm, pair) = dest_binop 542 ``FUPDATE:('a |-> 'b) -> 'a # 'b -> ('a |-> 'b)`` 543 (ERR "FUPDATE_CONV" "Not a FUPDATE term") t; 544 val (x,y) = dest_binop ``$, : 'a -> 'b -> 'a # 'b`` 545 (ERR "FUPDATE_CONV" "Not an explicit pair") pair; 546 val l = dest_monop ``fmap: ('a#'b)list -> ('a|->'b)`` 547 (ERR "FUPDATE_CONV" "not an fmap [ .. ] term") fm; 548 val th = ISPECL [x, y, l] list_rplacv_thm; 549 val th' = CONV_RULE (RAND_CONV (list_rplacv_CONV eqconv) THENC 550 REWR_CONV LET_THM THENC BETA_CONV) th; 551 val th'' = (CONV_RULE (RATOR_CONV (RATOR_CONV (RAND_CONV 552 (REWR_CONV NOT_CONS_NIL_EQN))) THENC 553 COND_CONV) th') 554 handle _ => raise (ERR "FUPDATE_CONV" 555 "FUPDATE_CONV will not extend the domain"); 556in CONJUNCT2 th'' end; 557 558(* *** now FMAPAL_FUPDATE_CONV, treatment modeled on fmap_FUPDATE_CONV *** *) 559 560val [brc_nt, brc_node] = CONJUNCTS bt_rplacv_cn; 561 562(* brc_nt = |- !y x cn cmp. bt_rplacv_cn cmp (x,y) nt cn = nt 563 brc_node = |- !z y x w r l cn cmp. 564 bt_rplacv_cn cmp (x,y) (node l (w,z) r) cn = 565 case apto cmp x w of 566 LESS => bt_rplacv_cn cmp (x,y) l (\m. cn (node m (w,z) r)) 567 | EQUAL => cn (node l (x,y) r) 568 | GREATER => bt_rplacv_cn cmp (x,y) r (\m. cn (node l (w,z) m)) *) 569 570fun bt_rplacv_CONV keyconv = 571let fun brcn t = 572((REWR_CONV brc_node THENC 573 RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV keyconv))) THENC 574 cpn_REWR_CONV THENC TRY_CONV brcn) ORELSEC 575 REWR_CONV brc_nt) t 576in brcn THENC REPEATC BETA_CONV end; 577 578(* Following conversion reduces terms of the form 579 FMAPAL cmp ... |+ (x,y), 580 provided a pair (x,w) already occurs in ... . *) 581 582val NOT_node_nt_EQN = prove (``!ab:'a#'b l r. ((node l ab r) = nt) = F``, 583REWRITE_TAC [GSYM bt_distinct]); 584 585fun FMAPAL_FUPDATE_CONV keyconv t = 586let val (fm, pair) = dest_binop 587 ``FUPDATE:('a |-> 'b) -> 'a # 'b -> ('a |-> 'b)`` 588 (ERR "FUPDATE_CONV" "Not a FUPDATE term") t; 589 val (x,y) = dest_binop ``$, : 'a -> 'b -> 'a # 'b`` 590 (ERR "FUPDATE_CONV" "Not an explicit pair") pair; 591 val (cmp, bt) = dest_binop ``FMAPAL: 'a toto -> ('a#'b)bt -> ('a|->'b)`` 592 (ERR "FUPDATE_CONV" "not a FMAPAL ... term") fm; 593 val th = ISPECL [cmp, x, y, bt] bt_rplacv_thm; 594 val th' = CONV_RULE (RAND_CONV (bt_rplacv_CONV keyconv) THENC 595 REWR_CONV LET_THM THENC BETA_CONV) th; 596 val th'' = (CONV_RULE (RATOR_CONV (RATOR_CONV (RAND_CONV 597 (REWR_CONV NOT_node_nt_EQN))) THENC 598 COND_CONV) th') 599 handle _ => raise (ERR "FUPDATE_CONV" 600 "FMAPAL_FUPDATE_CONV will not extend the domain"); 601in CONJUNCT2 th'' end; 602 603fun FUPDATE_CONV keyconv t = 604if is_const (rator (rand (rator t))) (* should then be fmap *) 605then fmap_FUPDATE_CONV keyconv t 606else FMAPAL_FUPDATE_CONV keyconv t; 607 608(* ******************************************************************* *) 609(* FMAP_EXPR_CONV *) 610(* ******************************************************************* *) 611 612fun FMAPAL_EXPR_TO_ORWL keyconv t = 613let val c = rator (rator t) 614in if is_const c then 615 let val d = fst (dest_const c) 616 in if d = "FMAPAL" then FMAPAL_TO_ORWL keyconv t 617 else if d = "FUNION" then ORWL_FUNION keyconv 618 (FMAPAL_EXPR_TO_ORWL keyconv (rand (rator t))) 619 (FMAPAL_EXPR_TO_ORWL keyconv (rand t)) 620 else if d = "DRESTRICT" then 621 if is_const (rator (rand t)) andalso 622 fst (dest_const (rator (rand t))) = "COMPL" then 623 ORWL_DRESTRICT_COMPL keyconv 624 (FMAPAL_EXPR_TO_ORWL keyconv (rand (rator t))) 625 (ENUMERAL_TO_OWL keyconv (rand (rand t))) 626 else 627 ORWL_DRESTRICT keyconv 628 (FMAPAL_EXPR_TO_ORWL keyconv (rand (rator t))) 629 (ENUMERAL_TO_OWL keyconv (rand t)) 630 else raise (ERR "FMAPAL_EXPR_TO_ORWL" "not a recognized binary operator") 631 end 632 else raise (ERR "FMAPAL_EXPR_TO_ORWL" "not a binary operation") 633end; 634 635fun FMAP_EXPR_CONV keyconv t = ORWL_TO_FMAPAL (FMAPAL_EXPR_TO_ORWL keyconv t); 636 637 638(* ********************* sorting: set_TO_ORWL ************************* *) 639(* The function set_TO_ORWL accepts fmap [ ... ] term and returns the *) 640(* corresponding OWL theorem. *) 641(* ******************************************************************** *) 642 643fun fmap_TO_ORWL keyconv cmp fmapl = 644let val th = ISPECL [cmp, rand fmapl] fmap_ORWL_thm 645in CONV_RULE (RAND_CONV (incr_sort_CONV keyconv)) th end; 646 647(* Examples for debugging: *) 648(* ************************************************** 649 650val mg = Term`merge numto [(1,T); (2,T); (5,T)] [(1,F); (3,F)]`; 651merge_CONV numto_CONV mg; 652val img = Term`incr_merge numto [(1,()); (5,())] 653 [SOME [(2,()); (3,())]]`; 654val imz = Term`incr_merge numto [(3,())] 655 [NONE; SOME [(2,()); (3,())]]`; 656incr_merge_CONV numto_CONV img; 657incr_merge_CONV numto_CONV imz; 658 659 val ibl = Term`incr_build numto 660 [(3,()); (1,()); (3,()); (4,()); (2,()); (1,())]`; 661incr_build_CONV numto_CONV ibl; 662 663val mo5 = Term`merge_out numto [(5,())] 664 [NONE; SOME [(1,()); (3,())]; SOME [(1,()); (2,()); (3,()); (4,())]]`; 665merge_out_CONV numto_CONV mo5; 666 667incr_sort_CONV numto_CONV ``incr_sort numto [6,T;5,T;4,T;3,T;2,T;1,T]``; 668 669fmap_TO_FMAPAL_CONV numto_CONV ``numto`` 670 ``fmap [(10,T); (9,F); (8,T); (7,F); (6,T); (5,F); (4,T); (3,F); (2,T)]``; 671 672FUN_FMAPAL_CONV numto_CONV ``numto`` REDUCE_CONV ``FUN_FMAP SUC (set [1;3;5])``; 673 674 val apft = Term`(FMAPAL numto (node nt (5,T) nt)) ' 5`; 675 FAPPLY_CONV numto_CONV apft; 676 val fpt = 677 ``fmap [(10,T); (9,F); (8,T); (7,F); (6,T); (5,F); (4,T); (3,F); (2,T)]``; 678 val fmt = rand (concl (fmap_TO_FMAPAL_CONV numto_CONV ``numto`` fpt)); 679 FAPPLY_CONV numto_CONV ``^fmt ' 8``; 680 FAPPLY_CONV numto_CONV ``^fmt ' 9``; 681 FAPPLY_CONV numto_CONV ``^fmt ' 1``; 682 FAPPLY_CONV REDUCE_CONV ``^fpt ' 8``; 683 FAPPLY_CONV REDUCE_CONV ``^fpt ' 9``; 684 FAPPLY_CONV REDUCE_CONV ``^fpt ' 1``; 685 686val fake = ASSUME ``ORWL numto (fmap [5,T; 4,F; 3,T]) [5,T; 4,F; 3,T]``; 687ORWL_TO_FMAPAL fake; 688 689val cmp = ``numto``; 690val tbt = rand (rand (concl (fmap_TO_FMAPAL_CONV numto_CONV ``numto`` 691 ``fmap [1,T;2,F;3,T;4,F;5,T]``))); 692val bolt = ``bt_to_orl_lb_ub_ac ^cmp 0 ^tbt 4 []``; 693val bolt' = ``bt_to_orl_lb_ub_ac ^cmp 0 ^tbt 8 []``; 694val bolt'' = ``bt_to_orl_lb_ub_ac ^cmp 2 ^tbt 5 []``; 695bt_to_orl_lb_ub_CONV numto_CONV bolt; 696 697val bult = ``bt_to_orl_ub_ac ^cmp ^tbt 4 []``; 698val bult' = ``bt_to_orl_ub_ac ^cmp ^tbt 8 []``; 699bt_to_orl_ub_CONV numto_CONV bult; 700 701val bllt = ``bt_to_orl_lb_ac ^cmp 2 ^tbt []``; 702val bllt' = ``bt_to_orl_lb_ac ^cmp 0 ^tbt []``; 703bt_to_orl_lb_CONV numto_CONV bllt; 704 705val blt = ``bt_to_orl numto ^tbt``; 706bt_to_orl_CONV numto_CONV blt; 707val badbt = ``node (node nt (1,T) nt) (3,T) (node (node nt (3,F) nt) 708 (4,F) (node nt (1,F) nt))``; 709val badblt = ``bt_to_orl numto ^badbt``; 710bt_to_orl_CONV numto_CONV badblt; 711 712val tft = rand (concl (fmap_TO_FMAPAL_CONV numto_CONV ``numto`` 713 ``fmap [4,F;1,T;3,T;5,T;2,F]``)); 714val orwa = FMAPAL_TO_ORWL numto_CONV tft; 715 716val orwb = FMAPAL_TO_ORWL numto_CONV 717 (rand (concl (fmap_TO_FMAPAL_CONV numto_CONV ``numto`` 718 ``fmap [0,F;3,T;1,T;8,F]``))); 719ORWL_FUNION numto_CONV orwa orwb; 720 721val wft = rand (concl (fmap_TO_FMAPAL_CONV numto_CONV ``numto`` 722 ``fmap [8,F;3,T;1,T;0,F]``)); 723val utwft = ``^tft FUNION ^wft``; 724val u = FUNION_CONV numto_CONV utwft; 725FMAPAL_TO_fmap_CONV numto_CONV (rand (concl u)); 726 727val ig = Term`inter_merge numto [1,T; 2,F; 5,T] [1; 3]`; 728inter_merge_CONV numto_CONV ig; 729 730val owb = ENUMERAL_TO_OWL numto_CONV 731 (rand (concl (DISPLAY_TO_ENUMERAL_CONV numto_CONV ``numto`` ``{0;3;1;8}``))); 732ORWL_DRESTRICT numto_CONV orwa owb; 733 734val dg = Term`diff_merge numto [1,T; 2,F; 5,T] [1; 3]`; 735diff_merge_CONV numto_CONV dg; 736 737ORWL_DRESTRICT_COMPL numto_CONV orwa owb; 738 739val wet = 740 rand (concl (DISPLAY_TO_ENUMERAL_CONV numto_CONV ``numto`` ``{8;3;1;0}``)); 741val dtweft = ``DRESTRICT ^tft ^wet``; 742DRESTRICT_CONV numto_CONV dtweft; 743val dctweft = ``DRESTRICT ^tft (COMPL ^wet)``; 744DRESTRICT_CONV numto_CONV dctweft; 745val dccccctweft = 746 ``DRESTRICT ^tft (COMPL (COMPL (COMPL (COMPL (COMPL ^wet)))))``; 747DRESTRICT_CONV numto_CONV dccccctweft; 748 749MAP_ELEM_CONV (RAND_CONV (DISPLAY_TO_ENUMERAL_CONV numto_CONV ``numto``)) 750 ``[(2, {4; 3}); (3, {2}); (4, {3; 1}); (1, {})]``; 751 752FDOM_CONV 753 ``FDOM (FMAPAL numto (node nt (4,F) (node (node nt (3,T) nt) (5,T) nt)))``; 754FDOM_CONV ``FDOM (fmap [(4, F); (3, T); (5, T)])``; 755 756o_f_CONV REDUCE_CONV ``$~ o_f ^tft``; 757o_f_CONV REDUCE_CONV 758``$~ o_f (FMAPAL numto (node nt (4,F) (node (node nt (3,T) nt) (5,T) nt)))``; 759o_f_CONV REDUCE_CONV 760``$~ o_f (fmap [(4, F); (3, T); (5, T)])``; 761 762IN_FDOM_CONV numto_CONV ``5 IN FDOM ^tft``; 763IN_FDOM_CONV numto_CONV ``6 IN FDOM ^tft``; 764IN_FDOM_CONV REDUCE_CONV ``3 IN FDOM (fmap [(4, F); (3, T); (5, T)])``; 765IN_FDOM_CONV REDUCE_CONV ``2 IN FDOM (fmap [(4, F); (3, T); (5, T)])``; 766 767list_rplacv_CONV REDUCE_CONV 768 ``list_rplacv_cn (3,T) [(1,F); (2,F); (3,F); (4,F); (5,F)] (\m.m)``; 769list_rplacv_CONV REDUCE_CONV ``list_rplacv_cn (3,T) [(1,F); (2,F)] (\m.m)``; 770 771val t = ``fmap [(1,F); (2,F); (3,F); (4,F); (5,F)] |+ (3,T)``; 772val tbad = ``fmap [(1,F); (2,F)] |+ (3,T)``; 773val eqconv = REDUCE_CONV; 774fmap_FUPDATE_CONV eqconv t; 775(* Deliberately gives "will not extend domain" error: *) 776fmap_FUPDATE_CONV eqconv tbad; 777 778val tf = rand (concl (fmap_TO_FMAPAL_CONV numto_CONV ``numto`` 779 ``fmap [(1,F); (2,F); (3,F); (4,F); (5,F)]``)); 780FMAPAL_FUPDATE_CONV numto_CONV ``FUPDATE ^tf (3,T)``; 781(* Deliberately gives "will not extend domain" error: *) 782FMAPAL_FUPDATE_CONV numto_CONV ``FUPDATE ^tf (6,T)``; 783 784bt_rplacv_CONV numto_CONV ``bt_rplacv_cn numto (3,T) ^(rand tf) (\m.m)``; 785bt_rplacv_CONV numto_CONV ``bt_rplacv_cn numto (0,T) ^(rand tf) (\m.m)``; 786 787val wet = 788 rand (concl (DISPLAY_TO_ENUMERAL_CONV numto_CONV ``numto`` ``{8;3;1;0}``)); 789val dtweft = ``DRESTRICT ^tft ^wet``; 790FMAPAL_EXPR_TO_ORWL numto_CONV ``^tft FUNION (DRESTRICT ^wft ^wet)``; 791FMAPAL_EXPR_TO_ORWL numto_CONV ``^tft FUNION (DRESTRICT ^wft (COMPL ^wet))``; 792val dctweft = ``DRESTRICT ^tft (COMPL ^wet)``; 793FMAPAL_EXPR_TO_ORWL numto_CONV ``^dctweft FUNION ^tft``; 794 795FMAP_EXPR_CONV numto_CONV ``(^tft) FUNION DRESTRICT (^wft) (^wet)``; 796FMAP_EXPR_CONV numto_CONV ``(^tft) FUNION DRESTRICT (^wft) (COMPL ^wet)``; 797 798fmap_TO_ORWL numto_CONV ``numto`` ``fmap [(5,T); (3,F); (3,T)]``; 799********************** *) 800end; 801