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