1structure patriciaLib :> patriciaLib = 2struct 3 4(* interactive use: 5 app load ["ConseqConv", "wordsLib", "listLib"] 6*) 7 8open HolKernel Parse boolLib bossLib 9open patriciaTheory patriciaSyntax; 10 11val ERR = mk_HOL_ERR "patricia" 12 13(* ------------------------------------------------------------------------- *) 14 15datatype term_ptree = 16 Empty 17 | Leaf of Arbnum.num * term 18 | Branch of Arbnum.num * int * term_ptree * term_ptree 19 20fun dest_ptree t = 21 if is_empty t 22 then Empty 23 else if is_leaf t 24 then let 25 val (k, d) = dest_leaf t 26 in 27 Leaf (numLib.dest_numeral k, d) 28 end 29 else if is_branch t 30 then let 31 val (p, m, l, r) = dest_branch t 32 in 33 Branch (numLib.dest_numeral p, numLib.int_of_term m, 34 dest_ptree l, dest_ptree r) 35 end 36 else raise ERR "dest_ptree" "" 37 38fun mk_ptree Empty = mk_empty Type.alpha 39 | mk_ptree (Leaf (k, d)) = mk_leaf (numLib.mk_numeral k, d) 40 | mk_ptree (Branch (p, m, l, r)) = 41 mk_branch (numLib.mk_numeral p, numLib.term_of_int m, 42 mk_ptree l, mk_ptree r) 43 44fun odd n = Arbnum.mod2 n = Arbnum.one 45fun even n = Arbnum.mod2 n = Arbnum.zero 46fun div_2exp x n = funpow x Arbnum.div2 n 47fun bit b n = odd (div_2exp b n) 48 49fun mod_2exp x n = 50 if x = 0 orelse n = Arbnum.zero 51 then Arbnum.zero 52 else let 53 val v = Arbnum.times2 (mod_2exp (x - 1) (Arbnum.div2 n)) 54 in 55 if even n then v else Arbnum.plus1 v 56 end 57 58fun mod_2exp_eq x a b = 59 if x = 0 60 then true 61 else odd a = odd b andalso 62 mod_2exp_eq (x - 1) (Arbnum.div2 a) (Arbnum.div2 b) 63 64fun lt_2exp x n = x = Arbnum.zero orelse Arbnum.toInt (Arbnum.log2 x) < n 65 66val empty = Empty 67 68fun every_leaf P Empty = true 69 | every_leaf P (Leaf (j, d)) = P j d 70 | every_leaf P (Branch (p, m, l, r)) = every_leaf P l andalso every_leaf P r 71 72fun is_Empty Empty = true 73 | is_Empty _ = false 74 75fun is_ptree Empty = true 76 | is_ptree (Leaf (k, d)) = true 77 | is_ptree (Branch (p, m, l, r)) = 78 lt_2exp p m andalso not(is_Empty l) andalso not(is_Empty r) andalso 79 every_leaf (fn k => fn d => mod_2exp_eq m k p andalso bit m k) l andalso 80 every_leaf (fn k => fn d => mod_2exp_eq m k p andalso not (bit m k)) r 81 andalso is_ptree l andalso is_ptree r 82 83fun branching_bit p0 p1 = 84 if odd p0 = even p1 orelse p0 = p1 85 then 0 86 else branching_bit (Arbnum.div2 p0) (Arbnum.div2 p1) + 1 87 88fun peek Empty k = NONE 89 | peek (Leaf (j, d)) k = if k = j then SOME d else NONE 90 | peek (Branch (p, m, l, r)) k = peek (if bit m k then l else r) k; 91 92fun join (p0, t0, p1, t1) = 93 let 94 val m = branching_bit p0 p1 95 in 96 if bit m p0 97 then Branch (mod_2exp m p0, m, t0, t1) 98 else Branch (mod_2exp m p0, m, t1, t0) 99 end 100 101fun add Empty x = Leaf x 102 | add (Leaf (j, d)) (x as (k, e)) = 103 if j = k then Leaf x else join (k, Leaf x, j, Leaf (j, d)) 104 | add (Branch (p, m, l, r)) (x as (k, e)) = 105 if mod_2exp_eq m k p 106 then if bit m k 107 then Branch (p, m, add l x, r) 108 else Branch (p, m, l, add r x) 109 else join (k, Leaf x, p, Branch (p, m, l, r)) 110 111fun add_list t = foldl (uncurry (C add)) t 112 113fun ptree_of_list l = add_list Empty l 114 115fun branch (_, _, Empty, t) = t 116 | branch (_, _, t, Empty) = t 117 | branch (p, m, t0, t1) = Branch (p, m, t0, t1) 118 119fun remove Empty k = Empty 120 | remove (t as Leaf (j, d)) k = if j = k then Empty else t 121 | remove (t as Branch (p, m, l, r)) k = 122 if mod_2exp_eq m k p 123 then if bit m k 124 then branch (p, m, remove l k, r) 125 else branch (p, m, l, remove r k) 126 else t 127 128local 129 fun traverse_aux Empty f = f 130 | traverse_aux (Leaf (j, d)) f = j :: f 131 | traverse_aux (Branch (p, m, l, r)) f = traverse_aux l (traverse_aux r f) 132in 133 fun traverse t = traverse_aux t [] 134end 135 136fun keys t = Listsort.sort Arbnum.compare (traverse t) 137 138fun transform f Empty = Empty 139 | transform f (Leaf (j, d)) = Leaf (j, f d) 140 | transform f (Branch (p, m, l, r)) = 141 Branch (p, m, transform f l, transform f r) 142 143local 144 fun list_of_ptree_aux Empty f = f 145 | list_of_ptree_aux (Leaf (j, d)) f = (j, d) :: f 146 | list_of_ptree_aux (Branch (p, m, l, r)) f = 147 list_of_ptree_aux l (list_of_ptree_aux r f) 148in 149 fun list_of_ptree t = list_of_ptree_aux t [] 150end 151 152fun size Empty = 0 153 | size (Leaf (j, d)) = 1 154 | size (Branch (p, m, l, r)) = size l + size r 155 156fun depth Empty = 0 157 | depth (Leaf (j, d)) = 1 158 | depth (Branch (p, m, l, r)) = 1 + (Int.max (depth l, depth r)) 159 160fun tabulate (n, f) = 161 let 162 fun h i = if i < n then add (h (i + 1)) (f i) else Empty 163 in 164 if n < 0 then raise Size else h 0 165 end 166 167infix in_ptree insert_ptree 168 169fun op in_ptree (n, t) = isSome (peek t n) 170fun op insert_ptree (n, t) = add t (n, oneSyntax.one_tm) 171 172val ptree_of_nums = foldl (op insert_ptree) Empty 173 174fun int_peek t i = peek t (Arbnum.fromInt i) 175fun int_add t (i, d) = add t (Arbnum.fromInt i, d) 176fun int_add_list t = foldl (uncurry (C int_add)) t 177fun int_ptree_of_list l = int_add_list Empty l 178fun int_remove t i = remove t (Arbnum.fromInt i) 179fun op int_in_ptree (n, t) = isSome (int_peek t n) 180fun op int_insert_ptree (n, t) = int_add t (n, oneSyntax.one_tm) 181val ptree_of_ints = foldl (op int_insert_ptree) Empty 182 183local 184 val n256 = Arbnum.fromInt 256 185 fun l2n [] = Arbnum.zero 186 | l2n (h::t) = Arbnum.+ (Arbnum.mod (h, n256), Arbnum.* (n256, l2n t)) 187in 188 fun string_to_num s = 189 l2n (List.rev 190 (Arbnum.one :: List.map (Arbnum.fromInt o Char.ord) (String.explode s))) 191end 192 193fun string_peek t i = peek t (string_to_num i) 194fun string_add t (i, d) = add t (string_to_num i, d) 195fun string_add_list t = foldl (uncurry (C string_add)) t 196fun string_ptree_of_list l = string_add_list Empty l 197fun string_remove t i = remove t (string_to_num i) 198fun op string_in_ptree (n, t) = isSome (string_peek t n) 199fun op string_insert_ptree (n, t) = string_add t (n, oneSyntax.one_tm) 200val ptree_of_strings = foldl (op string_insert_ptree) Empty 201 202fun custom_pp_term_ptree pp_empty pp_entry i t = 203 let 204 open PP 205 val l = Listsort.sort (Arbnum.compare o (fst ## fst)) (list_of_ptree t) 206 val ll = List.take (l, i) handle Subscript => l 207 val ll_len = length ll 208 val elided = length l - ll_len 209 val add_elided = 210 add_string ("|+ ... " ^ "(" ^ Int.toString elided ^ 211 (if elided = 1 then " entry" else " entries") ^ 212 " elided)") 213 in 214 if null l then pp_empty true 215 else 216 block CONSISTENT 0 [ 217 pp_empty false, 218 block CONSISTENT 0 ( 219 if null ll then [add_elided] 220 else 221 pr_list pp_entry [add_break(1,0)] ll @ 222 (if 0 < elided then [add_newline, add_elided] else []) 223 ) 224 ] 225 end 226 227fun standard_pp_empty (b: bool) = 228 PP.block PP.INCONSISTENT 0 ( 229 PP.add_string "Empty" :: 230 (if b then [] else [PP.add_break (1, 1)]) 231 ) 232 233fun standard_pp_entry (n, tm) = 234 PP.block PP.INCONSISTENT 0 [ 235 PP.add_string "|+ (", 236 PP.block PP.INCONSISTENT 4 [ 237 Arbnum.pp_num n, 238 PP.add_string ", ", 239 Hol_pp.pp_term tm, 240 PP.add_string ")" 241 ] 242 ] 243 244fun pp_term_ptree t = 245 PP.block PP.INCONSISTENT 2 [ 246 PP.add_string "``", 247 custom_pp_term_ptree standard_pp_empty standard_pp_entry 150 t, 248 PP.add_string "``" 249 ] 250 251(* ------------------------------------------------------------------------- *) 252 253local 254 val ct_conv = Conv.REWR_CONV ConseqConvTheory.AND_CLAUSES_TX 255 val cf_conv = Conv.REWR_CONV ConseqConvTheory.AND_CLAUSES_FX 256 val dt_conv = Conv.REWR_CONV ConseqConvTheory.OR_CLAUSES_TX 257 val df_conv = Conv.REWR_CONV ConseqConvTheory.OR_CLAUSES_FX 258 val it_conv = Conv.REWR_CONV ConseqConvTheory.COND_CLAUSES_CT 259 val if_conv = Conv.REWR_CONV ConseqConvTheory.COND_CLAUSES_CF 260in 261 fun CONJ_CONV cnv1 cnv2 = 262 Conv.LAND_CONV cnv1 THENC ((ct_conv THENC cnv2) ORELSEC cf_conv) 263 fun DISJ_CONV cnv1 cnv2 = 264 Conv.LAND_CONV cnv1 THENC ((df_conv THENC cnv2) ORELSEC dt_conv) 265 fun COND3_CONV cnv1 cnv2 cnv3 = 266 RATOR_CONV (RATOR_CONV (RAND_CONV cnv1)) 267 THENC ((it_conv THENC cnv2) ORELSEC (if_conv THENC cnv3)) 268end 269 270fun dest_strip t = let val (l, r) = strip_comb t in (fst (dest_const l), r) end 271 272(* ------------------------------------------------------------------------- *) 273 274local 275 val (peek_empty, peek_leaf, peek_branch) = 276 Lib.triple_of_list (List.map Drule.SPEC_ALL (CONJUNCTS PEEK_def)) 277 val p = Term.mk_var ("p", numLib.num) 278 val m = Term.mk_var ("m", numLib.num) 279 val k = Term.mk_var ("k", numLib.num) 280 val j = Term.mk_var ("j", numLib.num) 281 val leaf_rule = 282 Conv.CONV_RULE 283 (Conv.RHS_CONV (COND3_CONV Arithconv.NEQ_CONV ALL_CONV ALL_CONV)) 284 val bit_set_rule = 285 CONV_RULE (STRIP_QUANT_CONV (RHS_CONV (RATOR_CONV (RAND_CONV 286 (RATOR_CONV (RATOR_CONV (RAND_CONV wordsLib.BIT_SET_CONV))))))) 287 val branch_rule = 288 RIGHT_CONV_RULE 289 (LAND_CONV (COND3_CONV (pred_setLib.IN_CONV Arithconv.NEQ_CONV) 290 ALL_CONV ALL_CONV)) 291in 292 fun PTREE_PEEK_CONV tm = 293 let 294 val (t, i) = patriciaSyntax.dest_peek tm 295 val ty = Term.type_of t 296 val tty = patriciaSyntax.dest_ptree_type ty 297 val tsbst = [Type.alpha |-> tty] 298 val d = Term.mk_var ("d", tty) 299 val l = Term.mk_var ("l", ty) 300 val r = Term.mk_var ("r", ty) 301 val inst_ty = Thm.INST_TYPE tsbst 302 val bthm = bit_set_rule (Thm.INST [k |-> i] (inst_ty peek_branch)) 303 fun cnv tm = 304 case dest_strip (fst (patriciaSyntax.dest_peek tm)) of 305 ("Empty", []) => inst_ty peek_empty 306 | ("Leaf", [jj, dd]) => 307 leaf_rule 308 (Drule.INST_TY_TERM 309 ([k |-> i, j |-> jj, d |-> dd], tsbst) peek_leaf) 310 | ("Branch", [pp, mm, ll, rr]) => 311 let 312 val thm = branch_rule (Thm.INST [p |-> pp, m |-> mm] bthm) 313 in 314 RIGHT_CONV_RULE cnv (Thm.INST [l |-> ll, r |-> rr] thm) 315 end 316 | _ => raise ERR "PTREE_PEEK_CONV" "unexpected term" 317 in 318 cnv tm 319 end 320end 321 322val PTREE_IN_PTREE_CONV = 323 Conv.REWR_CONV IN_PTREE_def 324 THENC Conv.RAND_CONV PTREE_PEEK_CONV 325 THENC PURE_ONCE_REWRITE_CONV [optionTheory.IS_SOME_DEF] 326 327(* ------------------------------------------------------------------------- *) 328 329val BRANCHING_BIT_numeral = Q.prove( 330 `(BRANCHING_BIT 0 0 = 0) /\ 331 (!x. BRANCHING_BIT 0 (NUMERAL (BIT1 x)) = 0) /\ 332 (!x. BRANCHING_BIT (NUMERAL (BIT1 x)) 0 = 0) /\ 333 (!x. BRANCHING_BIT 0 (NUMERAL (BIT2 x)) = 334 SUC (BRANCHING_BIT 0 (NUMERAL (SUC x)))) /\ 335 (!x. BRANCHING_BIT (NUMERAL (BIT2 x)) 0 = 336 SUC (BRANCHING_BIT (NUMERAL (SUC x)) 0)) /\ 337 (!x y. BRANCHING_BIT (NUMERAL (BIT1 x)) (NUMERAL (BIT1 y)) = 338 if x = y then 0 else SUC (BRANCHING_BIT (NUMERAL x) (NUMERAL y))) /\ 339 (!x y. BRANCHING_BIT (NUMERAL (BIT2 x)) (NUMERAL (BIT2 y)) = 340 if x = y then 0 341 else SUC (BRANCHING_BIT (NUMERAL (SUC x)) (NUMERAL (SUC y)))) /\ 342 (!x y. BRANCHING_BIT (NUMERAL (BIT1 x)) (NUMERAL (BIT2 y)) = 0) /\ 343 (!x y. BRANCHING_BIT (NUMERAL (BIT2 x)) (NUMERAL (BIT1 y)) = 0)`, 344 REPEAT STRIP_TAC 345 THEN CONV_TAC 346 (LHS_CONV (ONCE_REWRITE_CONV [patriciaTheory.BRANCHING_BIT_def])) 347 THEN SIMP_TAC std_ss 348 [numeralTheory.numeral_distrib, numeralTheory.numeral_eq, 349 numeralTheory.numeral_evenodd, numeralTheory.numeral_div2] 350 ) 351 352val BRANCHING_BIT_CONV = 353 REWRITE_CONV [BRANCHING_BIT_numeral, numeralTheory.numeral_eq, 354 numeralTheory.numeral_distrib, numeralTheory.numeral_suc, 355 arithmeticTheory.NORM_0] 356 357val MOD_2EXP_CONV = 358 PURE_REWRITE_CONV 359 [numeral_bitTheory.MOD_2EXP, numeral_bitTheory.numeral_imod_2exp, 360 numeralTheory.numeral_suc, numeralTheory.numeral_sub, 361 numeralTheory.iSUB_THM, numeralTheory.numeral_lt, 362 numeralTheory.iDUB_removal, numeralTheory.numeral_distrib, 363 arithmeticTheory.NORM_0, boolTheory.COND_CLAUSES] 364 365local 366 val (add_empty, add_leaf, add_branch) = 367 Lib.triple_of_list (List.map SPEC_ALL (CONJUNCTS ADD_def)) 368 val join_rwt = 369 RIGHT_CONV_RULE (RATOR_CONV BETA_CONV THENC BETA_CONV) 370 (REWRITE_RULE [boolTheory.LET_DEF] (Drule.SPEC_ALL JOIN_def)) 371 val add_list_cnv = 372 Conv.REWR_CONV 373 (CONV_RULE (REDEPTH_CONV Conv.FUN_EQ_CONV) patriciaTheory.ADD_LIST_def) 374 val wcnv = RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV MOD_2EXP_CONV))) 375 val join_conv = 376 Conv.REWR_CONV join_rwt 377 THENC RAND_CONV BRANCHING_BIT_CONV 378 THENC BETA_CONV 379 THENC COND3_CONV wordsLib.WORD_EVAL_CONV wcnv wcnv 380 val join_rule = 381 RIGHT_CONV_RULE 382 (COND3_CONV wordsLib.WORD_EVAL_CONV 383 (COND3_CONV wordsLib.WORD_EVAL_CONV ALL_CONV ALL_CONV) 384 join_conv) 385 val add_leaf_rule = 386 RIGHT_CONV_RULE (COND3_CONV Arithconv.NEQ_CONV ALL_CONV join_conv) 387 val p = Term.mk_var ("p", numLib.num) 388 val m = Term.mk_var ("m", numLib.num) 389 val j = Term.mk_var ("j", numLib.num) 390 val k = Term.mk_var ("k", numLib.num) 391in 392 fun PTREE_ADD_CONV tm = 393 let 394 val ((t, _), is_list) = 395 (patriciaSyntax.dest_add_list tm, true) 396 handle HOL_ERR {origin_function = "dest_add_list", ...} => 397 (patriciaSyntax.dest_add tm, false) 398 val ty = Term.type_of t 399 val tty = patriciaSyntax.dest_ptree_type ty 400 val d = Term.mk_var ("d", tty) 401 val e = Term.mk_var ("e", tty) 402 val l = Term.mk_var ("l", ty) 403 val r = Term.mk_var ("r", ty) 404 val inst_ty = Thm.INST_TYPE [Type.alpha |-> tty] 405 val leaf = inst_ty add_leaf 406 val branch = inst_ty add_branch 407 fun add_conv t = 408 case (dest_strip ## pairSyntax.dest_pair) (dest_add t) of 409 (("Empty", []), (k0, e0)) => 410 Drule.INST_TY_TERM 411 ([k |-> k0, e |-> e0], [Type.alpha |-> tty]) add_empty 412 | (("Leaf", [j0, d0]), (k0, e0)) => 413 add_leaf_rule 414 (Thm.INST ([k |-> k0, e |-> e0, j |-> j0, d |-> d0]) leaf) 415 | (("Branch", [p0, m0, l0, r0]), (k0, e0)) => 416 let 417 val thm = 418 join_rule 419 (Thm.INST [l |-> l0, r |-> r0, k |-> k0, e |-> e0, 420 p |-> p0, m |-> m0] branch) 421 val (_, _, l1, r1) = 422 patriciaSyntax.dest_branch (rhs (concl thm)) 423 in 424 if patriciaSyntax.is_add r1 425 then RIGHT_CONV_RULE (RAND_CONV add_conv) thm 426 else if patriciaSyntax.is_add l1 427 then RIGHT_CONV_RULE 428 (RATOR_CONV (RAND_CONV add_conv)) thm 429 else thm 430 end 431 | _ => raise ERR "PTREE_ADD_LIST_CONV" 432 "Not Empty, Leaf or Branch"; 433 in 434 if is_list 435 then (add_list_cnv THENC listLib.FOLDL_CONV add_conv) tm 436 else add_conv tm 437 end 438end 439 440val PTREE_INSERT_PTREE_CONV = 441 Conv.REWR_CONV patriciaTheory.INSERT_PTREE_def THENC PTREE_ADD_CONV 442 443(* ------------------------------------------------------------------------- *) 444 445local 446 val (remove_empty, remove_leaf, remove_branch) = 447 Lib.triple_of_list (List.map SPEC_ALL (CONJUNCTS REMOVE_def)) 448 val remove_leaf_rule = 449 RIGHT_CONV_RULE (COND3_CONV Arithconv.NEQ_CONV ALL_CONV ALL_CONV) 450 val branch_rule = 451 RIGHT_CONV_RULE 452 (COND3_CONV wordsLib.WORD_EVAL_CONV 453 (COND3_CONV wordsLib.WORD_EVAL_CONV ALL_CONV ALL_CONV) 454 ALL_CONV) 455 val p = Term.mk_var ("p", numLib.num) 456 val m = Term.mk_var ("m", numLib.num) 457 val j = Term.mk_var ("j", numLib.num) 458 val k = Term.mk_var ("k", numLib.num) 459 val wcnv = RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV MOD_2EXP_CONV))) 460 val branch_tm = Term.prim_mk_const {Name = "BRANCH", Thy = "patricia"} 461 val remove_left = 462 patriciaSyntax.is_remove o (fn l => hd (List.drop (l, 2))) o 463 pairSyntax.strip_pair o HolKernel.dest_monop branch_tm (ERR "" "") 464in 465 fun PTREE_REMOVE_CONV tm = 466 let 467 val (t, k0) = patriciaSyntax.dest_remove tm 468 val ty = Term.type_of t 469 val tty = patriciaSyntax.dest_ptree_type ty 470 val d = Term.mk_var ("d", tty) 471 val e = Term.mk_var ("e", tty) 472 val l = Term.mk_var ("l", ty) 473 val r = Term.mk_var ("r", ty) 474 val inst_ty = Thm.INST_TYPE [Type.alpha |-> tty] 475 val leaf = inst_ty remove_leaf 476 val branch = inst_ty remove_branch 477 val branch_cnv = PURE_ONCE_REWRITE_CONV [inst_ty BRANCH_def] 478 fun remove_conv t = 479 case dest_strip (fst (dest_remove t)) of 480 ("Empty", []) => 481 Drule.INST_TY_TERM 482 ([k |-> k0], [Type.alpha |-> tty]) remove_empty 483 | ("Leaf", [j0, d0]) => 484 remove_leaf_rule 485 (Thm.INST ([k |-> k0, j |-> j0, d |-> d0]) leaf) 486 | ("Branch", [p0, m0, l0, r0]) => 487 let 488 val thm = 489 branch_rule 490 (Thm.INST [l |-> l0, r |-> r0, k |-> k0, 491 p |-> p0, m |-> m0] branch) 492 val t' = rhs (concl thm) 493 in 494 if patriciaSyntax.is_branch t' 495 then thm 496 else RIGHT_CONV_RULE 497 (Conv.RAND_CONV 498 (Conv.RAND_CONV 499 (Conv.RAND_CONV 500 ((if remove_left t' 501 then Conv.LAND_CONV 502 else Conv.RAND_CONV) remove_conv))) 503 THENC branch_cnv) thm 504 end 505 | _ => raise ERR "PTREE_REMOVE_LIST_CONV" 506 "Not Empty, Leaf or Branch"; 507 in 508 remove_conv tm 509 end 510end 511 512(* ------------------------------------------------------------------------- *) 513 514local 515 val (transform_empty, transform_leaf, transform_branch) = 516 Lib.triple_of_list (List.map SPEC_ALL (CONJUNCTS TRANSFORM_def)) 517 val j = Term.mk_var ("j", numLib.num) 518in 519 fun PTREE_TRANSFORM_CONV tcnv tm = 520 let 521 val (ff, t) = dest_transform tm 522 val (tty, rty) = Type.dom_rng (Term.type_of ff) 523 val f = Term.mk_var ("f", tty --> rty) 524 val d = Term.mk_var ("d", tty) 525 val inst_ty = 526 Drule.INST_TY_TERM 527 ([f |-> ff], [Type.beta |-> rty, Type.alpha |-> tty]) 528 val leaf = inst_ty transform_leaf 529 val branch_cnv = Conv.REWR_CONV (inst_ty transform_branch) 530 fun cnv t = 531 case dest_strip (snd (dest_transform t)) of 532 ("Empty", []) => inst_ty transform_empty 533 | ("Leaf", [jj, dd]) => 534 Conv.RIGHT_CONV_RULE (Conv.RAND_CONV tcnv) 535 (Thm.INST [j |-> jj, d |-> dd] leaf) 536 | ("Branch", [_, _, _, _]) => 537 (branch_cnv 538 THENC Conv.RAND_CONV cnv 539 THENC Conv.RATOR_CONV (Conv.RAND_CONV cnv)) t 540 | _ => raise ERR "PTREE_TRANSFORM_CONV" "Not Empty, Leaf or Branch" 541 in 542 cnv tm 543 end 544end 545 546(* ------------------------------------------------------------------------- *) 547 548local 549 val (size_empty, size_leaf, size_branch) = 550 Lib.triple_of_list (List.map SPEC_ALL (CONJUNCTS SIZE)) 551 val k = Term.mk_var ("k", numLib.num) 552in 553 fun PTREE_SIZE_CONV tm = 554 let 555 val t = dest_size tm 556 val tty = patriciaSyntax.dest_ptree_type (Term.type_of t) 557 val d = Term.mk_var ("d", tty) 558 val inst_ty = Thm.INST_TYPE [Type.alpha |-> tty] 559 val leaf = inst_ty size_leaf 560 val branch_cnv = Conv.REWR_CONV (inst_ty size_branch) 561 fun cnv t = 562 case dest_strip (dest_size t) of 563 ("Empty", []) => inst_ty size_empty 564 | ("Leaf", [kk, dd]) => Thm.INST [k |-> kk, d |-> dd] leaf 565 | ("Branch", [_, _, _, _]) => 566 (branch_cnv THENC Conv.BINOP_CONV cnv) t 567 | _ => raise ERR "PTREE_SIZE_CONV" "Not Empty, Leaf or Branch"; 568 in 569 (cnv THENC numLib.REDUCE_CONV) tm 570 end 571end 572 573(* ------------------------------------------------------------------------- *) 574 575local 576 val (depth_empty, depth_leaf, depth_branch) = 577 Lib.triple_of_list (List.map SPEC_ALL (CONJUNCTS DEPTH_def)) 578 val j = Term.mk_var ("j", numLib.num) 579in 580 fun PTREE_DEPTH_CONV tm = 581 let 582 val t = dest_depth tm 583 val tty = patriciaSyntax.dest_ptree_type (Term.type_of t) 584 val d = Term.mk_var ("d", tty) 585 val inst_ty = Thm.INST_TYPE [Type.alpha |-> tty] 586 val leaf = inst_ty depth_leaf 587 val branch_cnv = Conv.REWR_CONV (inst_ty depth_branch) 588 fun cnv t = 589 case dest_strip (dest_depth t) of 590 ("Empty", []) => inst_ty depth_empty 591 | ("Leaf", [jj, dd]) => Thm.INST [j |-> jj, d |-> dd] leaf 592 | ("Branch", [_, _, _, _]) => 593 (branch_cnv THENC Conv.RAND_CONV (Conv.BINOP_CONV cnv)) t 594 | _ => raise ERR "PTREE_DEPTH_CONV" "Not Empty, Leaf or Branch" 595 in 596 (cnv THENC numLib.REDUCE_CONV) tm 597 end 598end 599 600(* ------------------------------------------------------------------------- *) 601 602local 603 val (every_leaf_empty, every_leaf_leaf, every_leaf_branch) = 604 Lib.triple_of_list (List.map SPEC_ALL (CONJUNCTS EVERY_LEAF_def)) 605 val j = Term.mk_var ("j", numLib.num) 606in 607 fun PTREE_EVERY_LEAF_CONV ecnv tm = 608 let 609 val (pp, t) = dest_every_leaf tm 610 val tty = patriciaSyntax.dest_ptree_type (Term.type_of t) 611 val d = Term.mk_var ("d", tty) 612 val p = Term.mk_var ("P", numLib.num --> tty --> Type.bool) 613 val inst_ty = Drule.INST_TY_TERM ([p |-> pp], [Type.alpha |-> tty]) 614 val leaf = inst_ty every_leaf_leaf 615 val branch_cnv = Conv.REWR_CONV (inst_ty every_leaf_branch) 616 fun cnv t = 617 case dest_strip (snd (dest_every_leaf t)) of 618 ("Empty", []) => inst_ty every_leaf_empty 619 | ("Leaf", [jj, dd]) => 620 Conv.RIGHT_CONV_RULE ecnv (Thm.INST [j |-> jj, d |-> dd] leaf) 621 | ("Branch", [_, _, _, _]) => 622 (branch_cnv THENC CONJ_CONV cnv cnv) t 623 | _ => 624 raise ERR "PTREE_EVERY_LEAF_CONV" "Not Empty, Leaf or Branch" 625 in 626 cnv tm 627 end 628end 629 630(* ------------------------------------------------------------------------- *) 631 632local 633 val (exists_leaf_empty, exists_leaf_leaf, exists_leaf_branch) = 634 Lib.triple_of_list (List.map SPEC_ALL (CONJUNCTS EXISTS_LEAF_def)) 635 val j = Term.mk_var ("j", numLib.num) 636in 637 fun PTREE_EXISTS_LEAF_CONV ecnv tm = 638 let 639 val (pp, t) = dest_exists_leaf tm 640 val tty = patriciaSyntax.dest_ptree_type (Term.type_of t) 641 val d = Term.mk_var ("d", tty) 642 val p = Term.mk_var ("P", numLib.num --> tty --> Type.bool) 643 val inst_ty = Drule.INST_TY_TERM ([p |-> pp], [Type.alpha |-> tty]) 644 val leaf = inst_ty exists_leaf_leaf 645 val branch_cnv = Conv.REWR_CONV (inst_ty exists_leaf_branch) 646 fun cnv t = 647 case dest_strip (snd (dest_exists_leaf t)) of 648 ("Empty", []) => inst_ty exists_leaf_empty 649 | ("Leaf", [jj, dd]) => 650 Conv.RIGHT_CONV_RULE ecnv (Thm.INST [j |-> jj, d |-> dd] leaf) 651 | ("Branch", [_, _, _, _]) => 652 (branch_cnv THENC DISJ_CONV cnv cnv) t 653 | _ => 654 raise ERR "PTREE_EXISTS_LEAF_CONV" "Not Empty, Leaf or Branch" 655 in 656 cnv tm 657 end 658end 659 660(* ------------------------------------------------------------------------- *) 661 662val is_ptree_compset = wordsLib.words_compset () 663val () = computeLib.add_thms 664 [REWRITE_RULE [bitTheory.LT_TWOEXP] IS_PTREE_def, 665 (GSYM o CONJUNCT1) ptree_distinct, 666 (GSYM o CONJUNCT1 o CONJUNCT2) ptree_distinct] is_ptree_compset 667val () = computeLib.add_conv 668 (every_leaf_tm, 2, PTREE_EVERY_LEAF_CONV wordsLib.WORD_EVAL_CONV) 669 is_ptree_compset 670 671local 672 val IS_PTREE_EVAL_CONV = CHANGED_CONV (computeLib.CBV_CONV is_ptree_compset) 673 val IS_PTREE_X_CONV = 674 Conv.FIRST_CONV 675 (List.map (PART_MATCH (snd o dest_imp)) 676 [ADD_IS_PTREE, ADD_LIST_IS_PTREE, INSERT_PTREE_IS_PTREE, 677 REMOVE_IS_PTREE, PTREE_OF_NUMSET_IS_PTREE, TRANSFORM_IS_PTREE]) 678in 679 fun PTREE_IS_PTREE_CONV t = 680 let 681 val thm = ConseqConv.DEPTH_STRENGTHEN_CONSEQ_CONV IS_PTREE_X_CONV t 682 val is_ptree_thm = IS_PTREE_EVAL_CONV (fst (dest_imp (concl thm))) 683 in 684 Lib.with_exn (EQT_INTRO o MATCH_MP thm o EQT_ELIM) is_ptree_thm 685 (ERR "PTREE_IS_PTREE_CONV" "") 686 end 687 handle UNCHANGED => IS_PTREE_EVAL_CONV t 688end 689 690(* ------------------------------------------------------------------------- *) 691 692(* add conversion(s) for PTREE_OF_NUMSET *) 693 694val rhsc = rhs o concl 695val lhsc = lhs o concl 696 697val PTREE_OF_NUMSET_RWT = Q.prove( 698 `(!x t s y. 699 IS_PTREE t /\ FINITE s /\ (PTREE_OF_NUMSET t s = y) ==> 700 (PTREE_OF_NUMSET t (x INSERT s) = x INSERT_PTREE y)) /\ 701 (!s1 s2 t y. 702 IS_PTREE t /\ FINITE s1 /\ FINITE s2 /\ 703 (PTREE_OF_NUMSET t s1 = y) /\ 704 (PTREE_OF_NUMSET y s2 = z) ==> 705 (PTREE_OF_NUMSET t (s1 UNION s2) = z))`, 706 SRW_TAC [] [PTREE_OF_NUMSET_UNION, PTREE_OF_NUMSET_INSERT]) 707 708val ptee_of_numset_insert = CONJUNCT1 PTREE_OF_NUMSET_RWT 709val ptee_of_numset_union = CONJUNCT2 PTREE_OF_NUMSET_RWT 710 711fun PTREE_OF_NUMSET_CONV tm = 712 case total dest_ptree_of_numset tm of 713 SOME (t, s) => 714 if pred_setSyntax.is_insert s then 715 let val (x, y) = pred_setSyntax.dest_insert s 716 val is_ptree_thm = EQT_ELIM (PTREE_IS_PTREE_CONV (mk_is_ptree t)) 717 val finite_thm = EQT_ELIM (EVAL (pred_setSyntax.mk_finite y)) 718 val thm = PTREE_OF_NUMSET_CONV (mk_ptree_of_numset (t, y)) 719 in 720 MATCH_MP (Drule.ISPEC x ptee_of_numset_insert) 721 (LIST_CONJ [is_ptree_thm, finite_thm, thm]) 722 end 723 else if pred_setSyntax.is_empty s then 724 REWR_CONV PTREE_OF_NUMSET_EMPTY tm 725 else if pred_setSyntax.is_union s then 726 let val (s1, s2) = pred_setSyntax.dest_union s 727 val is_ptree_thm = EQT_ELIM (PTREE_IS_PTREE_CONV (mk_is_ptree t)) 728 val finite_thm1 = EQT_ELIM (EVAL (pred_setSyntax.mk_finite s1)) 729 val finite_thm2 = EQT_ELIM (EVAL (pred_setSyntax.mk_finite s2)) 730 val thm1 = PTREE_OF_NUMSET_CONV (mk_ptree_of_numset (t, s1)) 731 val thm2 = PTREE_OF_NUMSET_CONV (mk_ptree_of_numset (rhsc thm1, s2)) 732 in 733 MATCH_MP ptee_of_numset_union 734 (LIST_CONJ [is_ptree_thm, finite_thm1, finite_thm2,thm1,thm2]) 735 end 736 else raise ERR "PTREE_OF_NUMSET_CONV" "" 737 | _ => raise ERR "PTREE_OF_NUMSET_CONV" "" 738 739(* ------------------------------------------------------------------------- *) 740(* Conversion for applications of ADD, REMOVE and INSERT_PTREE (ARI) *) 741(* ------------------------------------------------------------------------- *) 742 743val DEPTH_ADD_THM = Q.prove( 744 `(c1 = t) /\ (patricia$ADD t (k,d) = c2) ==> (patricia$ADD c1 (k,d) = c2)`, 745 SRW_TAC [] []) 746 747val DEPTH_REMOVE_THM = Q.prove( 748 `(c1 = t) /\ (patricia$REMOVE t k = c2) ==> (patricia$REMOVE c1 k = c2)`, 749 SRW_TAC [] []) 750 751val DEPTH_INSERT_PTREE_THM = Q.prove( 752 `(c1 = t) /\ (patricia$INSERT_PTREE k t = c2) ==> 753 (patricia$INSERT_PTREE k c1 = c2)`, 754 SRW_TAC [] []) 755 756fun DEPTH_ARI_CONV rwt tm = 757 REWR_CONV rwt tm 758 handle HOL_ERR e => 759 if is_add tm 760 then let 761 val (t, x) = dest_add tm 762 val thm = DEPTH_ARI_CONV rwt t 763 val t' = rhsc thm 764 in 765 MATCH_MP DEPTH_ADD_THM 766 (CONJ thm (PTREE_ADD_CONV (mk_add (t', x)))) 767 end 768 else if is_remove tm 769 then let 770 val (t, k) = dest_remove tm 771 val thm = DEPTH_ARI_CONV rwt t 772 val t' = rhsc thm 773 in 774 MATCH_MP DEPTH_REMOVE_THM 775 (CONJ thm (PTREE_REMOVE_CONV (mk_remove (t', k)))) 776 end 777 else if is_insert_ptree tm 778 then let 779 val (k, t) = dest_insert_ptree tm 780 val thm = DEPTH_ARI_CONV rwt t 781 val t' = rhsc thm 782 in 783 MATCH_MP DEPTH_INSERT_PTREE_THM 784 (CONJ thm (PTREE_INSERT_PTREE_CONV 785 (mk_insert_ptree (k, t')))) 786 end 787 else raise HOL_ERR e 788 789(* ------------------------------------------------------------------------- *) 790 791val ptree_consts_ref = ref ([]:term list) 792val ptree_cache_ref = ref ([]:(term * thm) list) 793 794val ptree_strict_defn_check = ref false 795val ptree_max_cache_size = ref 10 796val ptree_new_defn_depth = ref ~1 797 798local 799 fun contains_term t1 t2 = can (find_term (can (match_term t2))) t1 800in 801 fun best_match_ptree tm = 802 let 803 fun get_best_match c [] = c 804 | get_best_match NONE (h::t) = 805 get_best_match 806 (if contains_term tm (fst h) then SOME h else NONE) t 807 | get_best_match (SOME x) (h::t) = 808 get_best_match 809 (if contains_term tm (fst h) andalso 810 term_size (fst x) < term_size (fst h) 811 then SOME h else SOME x) t 812 in 813 get_best_match NONE (!ptree_cache_ref) 814 end 815end 816 817fun remove_oldest_ptree_theorem () = 818 let 819 val n = length (!ptree_cache_ref) 820 in 821 if !ptree_max_cache_size < n 822 then ptree_cache_ref := List.take (!ptree_cache_ref, n - 1) 823 else () 824 end 825 826fun const_definition c = 827 let 828 val {Name, Thy, ...} = dest_thy_const c 829 in 830 DB.fetch Thy (Name ^ "_def") handle HOL_ERR _ => DB.fetch Thy Name 831 end 832 833fun root_const tm = 834 case Lib.total patriciaSyntax.dest_add tm of 835 SOME (t, _) => root_const t 836 | NONE => 837 (case Lib.total patriciaSyntax.dest_remove tm of 838 SOME (t, _) => root_const t 839 | NONE => 840 (case Lib.total patriciaSyntax.dest_insert_ptree tm of 841 SOME (_, t) => root_const t 842 | NONE => tm)) 843 844fun is_add_remove_insert tm = 845 is_add tm orelse is_remove tm orelse is_insert_ptree tm 846 847fun root_name tm = 848 if is_const tm 849 then let 850 val defn = rhsc (const_definition tm) 851 in 852 if is_add_remove_insert defn 853 then root_name (root_const defn) 854 else dest_const tm 855 end 856 else if is_add_remove_insert tm 857 then root_name (root_const tm) 858 else raise ERR "root_name" "" 859 860fun const_variant c = 861 let 862 val (name, typ) = root_name c handle HOL_ERR _ => ("ptree", type_of c) 863 val v = mk_var (name, typ) 864 in 865 numvariant [] v 866 end 867 868fun is_ptree_const tm = isSome (List.find (term_eq tm) (!ptree_consts_ref)) 869 870fun root_const_depth tm = 871 let 872 fun const_depth d tm = 873 case Lib.total patriciaSyntax.dest_add tm of 874 SOME (t, _) => const_depth (d + 1) t 875 | NONE => 876 (case Lib.total patriciaSyntax.dest_remove tm of 877 SOME (t, _) => const_depth (d + 1) t 878 | NONE => 879 (case Lib.total patriciaSyntax.dest_insert_ptree tm of 880 SOME (_, t) => const_depth (d + 1) t 881 | NONE => 882 if is_ptree_const tm 883 then d 884 else if not (!ptree_strict_defn_check) orelse 885 is_ptree (dest_ptree tm) 886 then ~d - 1 887 else raise ERR "root_const_depth" "")) 888 in 889 const_depth 0 tm 890 end 891 892fun insert_ptree_defn thm = 893 let 894 val (l, r) = dest_eq (concl thm) 895 val d = root_const_depth r 896 in 897 is_const l andalso (0 < d orelse d = ~1) orelse 898 raise ERR "insert_ptree_defn" "Not a patricia tree constant" 899 ; ptree_consts_ref := l::(!ptree_consts_ref) 900 end 901 902fun insert_ptree_theorem thm = 903 let 904 val (l, r) = dest_eq (concl thm) 905 in 906 is_ptree_type (type_of l) andalso root_const_depth r = ~1 orelse 907 raise ERR "insert_ptree_theorem" "Not a patricia tree constant" 908 ; ptree_cache_ref := (l, thm)::(!ptree_cache_ref) 909 end 910 911fun save_ptree_thm save thm = 912 if save 913 then (insert_ptree_theorem thm; remove_oldest_ptree_theorem (); thm) 914 else thm 915 916fun ptree_thm save tm = 917 case best_match_ptree tm of 918 SOME (_, thm) => 919 if term_eq (lhsc thm) tm 920 then let 921 val (h, t) = Lib.pluck (term_eq tm o fst) (!ptree_cache_ref) 922 in 923 ptree_cache_ref := h :: t; thm 924 end 925 else save_ptree_thm save (DEPTH_ARI_CONV thm tm) 926 | NONE => 927 let 928 val thm = const_definition (root_const tm) 929 val defn = rhsc thm 930 in 931 if is_add_remove_insert defn 932 then let 933 val rwt = DEPTH_ARI_CONV 934 (ptree_thm false (root_const defn)) defn 935 in 936 save_ptree_thm save 937 ((DEPTH_CONV (REWR_CONV thm) 938 THENC DEPTH_ARI_CONV rwt) tm) 939 end 940 else save_ptree_thm save (DEPTH_ARI_CONV thm tm) 941 end 942 943val PTREE_DEFN_CONV = ptree_thm false 944 945(* ------------------------------------------------------------------------- *) 946 947fun create_ptree_definition v tm = 948 let 949 val name = fst (dest_var v) 950 val thm = Definition.new_definition (name, mk_eq (v, tm)) 951 in 952 insert_ptree_defn thm 953 ; HOL_MESG ("Defined new ptree: " ^ name) 954 ; REWR_CONV (SYM thm) tm 955 end 956 957fun find_const_ptree tm = 958 case List.find (fn c => term_eq tm (rhsc (const_definition c))) 959 (!ptree_consts_ref) of 960 SOME c => SOME (SYM (const_definition c)) 961 | NONE => NONE 962 963fun PTREE_ARI_CONV tm = 964 let 965 val d = root_const_depth tm 966 in 967 if 0 < d andalso ((!ptree_new_defn_depth = ~1) orelse 968 d < !ptree_new_defn_depth) 969 then raise ERR "PTREE_ARI_CONV" "" 970 else if d < 0 971 then CHANGED_CONV (DEPTH_ARI_CONV (Thm.REFL (root_const tm))) tm 972 else case find_const_ptree tm of 973 SOME thm => REWR_CONV thm tm 974 | NONE => create_ptree_definition (const_variant tm) tm 975 end 976 977val DEPTH_PEEK_THM = Q.prove( 978 `(c1 = t) /\ (patricia$PEEK t k = c2) ==> (patricia$PEEK c1 k = c2)`, 979 SRW_TAC [] []) 980 981fun PTREE_PEEK_ARI_CONV tm = 982 let 983 val (t, k) = dest_peek tm 984 in 985 if is_const t andalso not (is_empty t) orelse is_add_remove_insert t 986 then let 987 val thm = ptree_thm true t 988 in 989 MATCH_MP DEPTH_PEEK_THM 990 (CONJ thm (PTREE_PEEK_CONV (mk_peek (rhsc thm, k)))) 991 end 992 else PTREE_PEEK_CONV tm 993 end 994 995fun mk_ptree_conv2 dest mk conv d_thm tm = 996 let 997 val (x, t) = dest tm 998 in 999 if is_const t andalso not (is_empty t) orelse is_add_remove_insert t 1000 then let 1001 val thm = ptree_thm true t 1002 in 1003 MATCH_MP d_thm (CONJ thm (conv (mk (x, rhsc thm)))) 1004 end 1005 else conv tm 1006 end 1007 1008val thm = Q.prove( 1009 `!f. (c1 = t) /\ (f k t = c2) ==> (f k c1 = c2)`, 1010 SRW_TAC [] []) 1011 1012val PTREE_IN_PTREE_ARI_CONV = 1013 mk_ptree_conv2 dest_in_ptree mk_in_ptree PTREE_IN_PTREE_CONV 1014 (Drule.ISPEC patriciaSyntax.in_ptree_tm thm) 1015 1016val PTREE_EVERY_LEAF_ARI_CONV = 1017 mk_ptree_conv2 dest_every_leaf mk_every_leaf (PTREE_EVERY_LEAF_CONV EVAL) 1018 (Drule.ISPEC patriciaSyntax.every_leaf_tm thm) 1019 1020val PTREE_EXISTS_LEAF_ARI_CONV = 1021 mk_ptree_conv2 dest_exists_leaf mk_exists_leaf (PTREE_EXISTS_LEAF_CONV EVAL) 1022 (Drule.ISPEC patriciaSyntax.exists_leaf_tm thm) 1023 1024val thm = Q.prove( 1025 `!f. (c1 = t) /\ (f t = c2) ==> (f c1 = c2)`, 1026 SRW_TAC [] []) 1027 1028fun mk_ptree_conv dest mk conv d_thm tm = 1029 let 1030 val t = dest tm 1031 in 1032 if is_const t andalso not (is_empty t) orelse is_add_remove_insert t 1033 then let 1034 val thm = ptree_thm true t 1035 in 1036 MATCH_MP d_thm (CONJ thm (conv (mk (rhsc thm)))) 1037 end 1038 else conv tm 1039 end 1040 1041val PTREE_SIZE_ARI_CONV = 1042 mk_ptree_conv dest_size mk_size PTREE_SIZE_CONV 1043 (Drule.ISPEC patriciaSyntax.size_tm thm) 1044 1045val PTREE_DEPTH_ARI_CONV = 1046 mk_ptree_conv dest_depth mk_depth PTREE_DEPTH_CONV 1047 (Drule.ISPEC patriciaSyntax.depth_tm thm) 1048 1049(* ------------------------------------------------------------------------- *) 1050 1051local 1052 open computeLib 1053in 1054 fun add_ptree_core compset = 1055 ( add_conv (peek_tm, 2, PTREE_PEEK_ARI_CONV) compset 1056 ; add_conv (add_tm, 2, PTREE_ARI_CONV) compset 1057 ; add_conv (remove_tm, 2, PTREE_ARI_CONV) compset 1058 ; add_conv (insert_ptree_tm, 2, PTREE_ARI_CONV) compset 1059 ; add_conv (size_tm, 1, PTREE_SIZE_ARI_CONV) compset 1060 ; add_conv (depth_tm, 1, PTREE_DEPTH_ARI_CONV) compset 1061 ; add_conv (every_leaf_tm, 2, PTREE_EVERY_LEAF_ARI_CONV) compset 1062 ; add_conv (exists_leaf_tm, 2, PTREE_EXISTS_LEAF_ARI_CONV) compset 1063 ; add_conv (in_ptree_tm, 2, PTREE_IN_PTREE_ARI_CONV) compset 1064 ; add_conv (is_ptree_tm, 1, PTREE_IS_PTREE_CONV) compset 1065 ; add_conv (ptree_of_numset_tm, 2, PTREE_OF_NUMSET_CONV) compset 1066 ; add_thms [PEEK_TRANSFORM] compset 1067 ) 1068end 1069 1070val () = add_ptree_core computeLib.the_compset 1071 1072fun add_ptree_compset compset = 1073 let 1074 open listTheory pred_setTheory 1075 in 1076 computeLib.add_thms 1077 [pairTheory.UNCURRY_DEF, 1078 optionTheory.THE_DEF, optionTheory.option_case_def, 1079 IS_EMPTY_def, FIND_def, ADD_INSERT, PEEK_TRANSFORM, 1080 FOLDL, NUMSET_OF_PTREE_def, ADD_LIST_def, LIST_TO_SET_THM, 1081 PTREE_OF_NUMSET_EMPTY, UNION_PTREE_def, COND_CLAUSES, 1082 EMPTY_DELETE, DELETE_INSERT, DELETE_UNION] compset 1083 ; add_ptree_core compset 1084 end 1085 1086fun ptree_compset () = 1087 let 1088 val compset = computeLib.new_compset [] 1089 in 1090 add_ptree_compset compset; compset 1091 end 1092 1093val PTREE_CONV = computeLib.CBV_CONV (ptree_compset ()) 1094 1095(* ------------------------------------------------------------------------- *) 1096 1097fun Define_mk_ptree s t = 1098 let 1099 val tm = mk_ptree t 1100 val def = boolSyntax.mk_eq (Term.mk_var (s, Term.type_of tm), tm) 1101 val thm = Definition.new_definition (s ^ "_def", def) 1102 in 1103 insert_ptree_defn thm 1104 ; insert_ptree_theorem thm 1105 ; remove_oldest_ptree_theorem () 1106 ; thm 1107 end 1108 1109local 1110 val is_ptree_cnv = 1111 REWR_CONV (EQT_INTRO (SPEC_ALL patriciaTheory.ADD_LIST_TO_EMPTY_IS_PTREE)) 1112 val empty_is_ptree_conv = 1113 Conv.REWR_CONV (EQT_INTRO patriciaTheory.EMPTY_IS_PTREE) 1114 fun to_add_list_cnv l = 1115 if List.null l 1116 then empty_is_ptree_conv 1117 else let 1118 val ty = Term.type_of (snd (hd l)) 1119 val tm = 1120 listSyntax.mk_list 1121 (List.map (pairSyntax.mk_pair o (numLib.mk_numeral ## I)) l, 1122 pairSyntax.mk_prod (numLib.num, ty)) 1123 val tm = 1124 patriciaSyntax.mk_add_list (patriciaSyntax.mk_empty ty, tm) 1125 in 1126 RAND_CONV (fn _ => SYM (PTREE_ADD_CONV tm)) THENC is_ptree_cnv 1127 end 1128in 1129 fun Define_mk_ptree_with_is_ptree s t = 1130 let 1131 val thm = Define_mk_ptree s t 1132 val l = list_of_ptree t 1133 val e = patriciaSyntax.mk_is_ptree (lhs (concl thm)) 1134 val is_ptree_thm = 1135 EQT_ELIM ((RAND_CONV (fn _ => thm) THENC (to_add_list_cnv l)) e) 1136 in 1137 computeLib.add_thms [is_ptree_thm] is_ptree_compset 1138 ; (thm, is_ptree_thm) 1139 end 1140end 1141 1142val dest_ptree_no_test = dest_ptree 1143 1144fun dest_ptree tm = 1145 let 1146 val t = dest_ptree_no_test tm 1147 in 1148 if is_ptree t 1149 then t 1150 else raise ERR "dest_ptree" "not a valid Patricia tree" 1151 end 1152 1153val is_ptree = Lib.can dest_ptree 1154 1155(* ------------------------------------------------------------------------- *) 1156 1157end 1158