1(* non-interactive mode 2*) 3structure subtypeTools :> subtypeTools = 4struct 5open HolKernel Parse boolLib; 6 7(* interactive mode 8val () = loadPath := "../ho_prover" :: !loadPath; 9val () = app load 10 ["Susp", 11 "combinTheory", 12 "pred_setTheory", 13 "prob_extraTheory", 14 "BasicProvers", 15 "HurdUseful", 16 "ho_basicTools", 17 "ho_discrimTools", 18 "ho_proverTools", 19 "subtypeTheory"]; 20val () = show_assums := true; 21*) 22 23open Susp combinTheory pred_setTheory BasicProvers 24 hurdUtils subtypeTheory ho_discrimTools 25 ho_proverTools ho_basicTools; 26 27infixr 0 oo ## ++ << || THENC ORELSEC THENR ORELSER -->; 28infix 1 >> |->; 29infix thenf orelsef then_frule orelse_frule join_frule; 30 31val op++ = op THEN; 32val op<< = op THENL; 33val op|| = op ORELSE; 34val op>> = op THEN1; 35val !! = REPEAT; 36 37(* ------------------------------------------------------------------------- *) 38(* Debugging. *) 39(* ------------------------------------------------------------------------- *) 40 41val trace_level = ref 0; 42val _ = Feedback.register_trace ("subtypeTools", trace_level, 10); 43fun trace l s = if l > !trace_level then () else say (s ^ "\n"); 44fun trace_x l s f x = 45 if l > !trace_level then () else say (s ^ ":\n" ^ f x ^ "\n"); 46fun trace_CONV l s tm = (trace_x l s term_to_string tm; ALL_CONV tm); 47 48(* ------------------------------------------------------------------------- *) 49(* Term operations *) 50(* ------------------------------------------------------------------------- *) 51 52fun genvar_dest_foralls tm = 53 let 54 val (vars, body) = dest_foralls tm 55 val (gvars, (sub, _)) = term_new_vars vars 56 in 57 (gvars, subst sub body) 58 end; 59 60fun mk_in (v, set) = 61 let 62 val v_type = type_of v 63 val in_type = v_type --> (v_type --> bool) --> bool 64 val in_const = mk_const ("IN", in_type) 65 in 66 list_mk_comb (in_const, [v, set]) 67 end; 68val dest_in = dest_binop "IN"; 69val is_in = can dest_in; 70 71fun mk_subset (set1, set2) = 72 let 73 val set_type = type_of set1 74 val subset_type = set_type --> set_type --> bool 75 val subset_const = mk_const ("SUBSET", subset_type) 76 in 77 list_mk_comb (subset_const, [set1, set2]) 78 end; 79val dest_subset = dest_binop "SUBSET"; 80val is_subset = can dest_subset; 81 82(* ------------------------------------------------------------------------- *) 83(* vterms *) 84(* ------------------------------------------------------------------------- *) 85 86fun term_to_vterm tm = 87 let 88 val vars = (free_vars tm, type_vars_in_term tm) 89 val (vars', (sub, _)) = new_vars vars 90 in 91 (vars', pinst sub tm) 92 end; 93 94(* ========================================================================= *) 95(* Some general functions operating on congruences. *) 96(* ========================================================================= *) 97 98local 99 fun imp_conv tm = (if is_imp tm then ALL_CONV else REWR_CONV EQ_T_IMP) tm 100 101 fun conj_conv tm = 102 (if Teq tm then ALL_CONV else FORALLS_CONV imp_conv) tm 103 104 val canon_conv = 105 FORALLS_CONV 106 (imp_conv THENC 107 RATOR_CONV 108 (RAND_CONV (EXACT_CONV T ORELSEC CONJUNCT_CONV (FORALLS_CONV imp_conv)))) 109in 110 val cong_canon = CONV_RULE canon_conv 111end; 112 113fun find_matching_cong congs tm = 114 let 115 val ((sub, thk), (vars, th)) = 116 case ovdiscrim_ho_match congs tm of c :: _ => c 117 | [] => raise ERR "find_matching_cong" "no applicable congruence" 118 val vars' = vars_after_subst vars sub 119 val conv = RAND_CONV (RATOR_CONV (RAND_CONV (K (SYM (thk ()))))) 120 val (vars'', (sub', _)) = new_vars vars' 121 val th' = (PINST sub THENR CONV_RULE conv THENR PINST sub') th 122 in 123 (vars'', th') 124 end; 125 126(* Function cacheing *) 127type 'a ccache = (term * int, 'a) Binarymap.dict ref 128 129fun new_cache () : 'a ccache = 130 ref (Binarymap.mkDict (pair_compare(Term.compare, Int.compare))) 131 132fun cache_lookup c (a, b_thk) = 133 case Binarymap.peek(!c, a) of 134 SOME b => b 135 | NONE => let 136 val b = b_thk () 137 val _ = c := Binarymap.insert(!c,a,b) 138 in 139 b 140 end 141 142fun cachef f = 143 let 144 val c = new_cache () 145 in 146 fn a => cache_lookup c (a, fn () => f a) 147 end; 148 149(* ========================================================================= *) 150(* Predicate subtype-checking. *) 151(* ========================================================================= *) 152 153(* Types *) 154 155datatype psubtype_context = PSUBTYPE_CONTEXT of 156 {facts : factdb, subtypes : vthm ovdiscrim}; 157 158datatype subtype_context = SUBTYPE_CONTEXT of 159 {pure : psubtype_context susp, 160 ccache : vthm list ccache}; 161 162datatype subtype_context_element = 163 SC_SUBTYPE of thm 164 | SC_SIMPLIFICATION of thm 165 | SC_JUDGEMENT of thm; 166 167(* Tuning *) 168 169val cache_subtypes = ref true; 170val subtype_depth = ref 3; 171 172(* (Quite delicate :-) interface to the higher-order prover *) 173 174val set_cnf_frule : fact_rule = 175 first_frule 176 [neg_frule, true_frule, false_frule, disj_frule, conj_frule, 177 forall_frule, exists_frule, (*bool_lrule,*) equal_frule, merge_frule]; 178 179val set_factdb = 180 (factdb_add_norm set_cnf_frule o 181 factdb_add_norm basic_rewrite_frule) 182 null_factdb; 183 184fun set_meson_frule db : fact_rule = 185 joinl_frule [biresolution_frule db, equality_frule, k1_frule]; 186 187fun set_prove_depth db depth vgoal = 188 meson_prove_reduce_depth db (set_meson_frule db) depth vgoal; 189 190(* Basic operations *) 191 192val empty_psubtype_context = 193 PSUBTYPE_CONTEXT {facts = set_factdb, subtypes = empty_ovdiscrim}; 194 195fun dest_psubtype_context (PSUBTYPE_CONTEXT sc) = sc; 196val psubtype_context_facts = #facts o dest_psubtype_context; 197val psubtype_context_subtypes = #subtypes o dest_psubtype_context; 198fun psubtype_context_update_facts f (PSUBTYPE_CONTEXT {facts, subtypes}) = 199 PSUBTYPE_CONTEXT {facts = f facts, subtypes = subtypes}; 200fun psubtype_context_update_subtypes f (PSUBTYPE_CONTEXT {facts, subtypes}) = 201 PSUBTYPE_CONTEXT {facts = facts, subtypes = f subtypes}; 202 203fun new_subtype_context () = 204 SUBTYPE_CONTEXT 205 {pure = delay (K empty_psubtype_context), 206 ccache = new_cache ()}; 207 208fun dest_subtype_context (SUBTYPE_CONTEXT sc) = sc; 209val subtype_context_pure = force o #pure o dest_subtype_context; 210val subtype_context_ccache = #ccache o dest_subtype_context; 211val subtype_context_facts = psubtype_context_facts o subtype_context_pure; 212val subtype_context_subtypes = psubtype_context_subtypes o subtype_context_pure; 213fun subtype_context_update_facts f (SUBTYPE_CONTEXT {pure, ccache}) = 214 SUBTYPE_CONTEXT 215 {pure = delay (fn () => psubtype_context_update_facts f (force pure)), 216 ccache = ccache}; 217fun subtype_context_update_subtypes f (SUBTYPE_CONTEXT {pure, ccache}) = 218 SUBTYPE_CONTEXT 219 {pure = delay (fn () => psubtype_context_update_subtypes f (force pure)), 220 ccache = ccache}; 221 222fun subtype_context_initialize sc = (subtype_context_pure sc; sc); 223 224(* Pretty-printing *) 225open PP 226fun pp_psubtype_context (PSUBTYPE_CONTEXT c) = 227 block CONSISTENT 1 [ 228 block CONSISTENT 2 [ 229 add_string "{#facts =", 230 add_break (1, 0), 231 pp_int (factdb_size (#facts c)), 232 add_string "," 233 ], 234 add_break (1, 0), 235 block CONSISTENT 2 [ 236 add_string "#subtypes =", 237 add_break (1, 0), 238 pp_int (ovdiscrim_size (#subtypes c)), 239 add_string "}" 240 ] 241 ] 242 243val pp_subtype_context = pp_map subtype_context_pure pp_psubtype_context; 244 245(* Adding to psubtype_contexts *) 246 247fun add_subtype_vthm (vars, th) = 248 let 249 val tm = (fst o dest_in o snd o dest_imp o concl) th 250 in 251 ovdiscrim_add ((vars, tm), (vars, th)) 252 end; 253 254val add_subtype_thm = add_subtype_vthm o thm_to_vthm o cong_canon; 255 256fun add_simplification th = factdb_add_norm (rewrite_frule [thm_to_vthm th]); 257 258fun subtype_context_add_fact vth = 259 subtype_context_update_facts (factdb_add_vthm vth); 260 261fun subtype_context_add_judgement th = 262 subtype_context_add_fact (thm_to_vthm (TRYR (MATCH_MP EQ_SUBSET_SUBSET) th)); 263 264val subtype_context_add_judgements = C (trans subtype_context_add_judgement); 265 266fun subtype_context_add (SC_SUBTYPE th) = 267 subtype_context_update_subtypes (add_subtype_thm th) 268 | subtype_context_add (SC_SIMPLIFICATION th) = 269 subtype_context_update_facts (add_simplification th) 270 | subtype_context_add (SC_JUDGEMENT th) = subtype_context_add_judgement th; 271 272(* The type-checking engine *) 273 274type cond_prover = vars * substitution -> ((vars * substitution) * thm) list; 275 276local 277 fun conj res [] = res 278 | conj res ((vs, ts, []) :: others) = 279 conj ((vs, REV_CONJUNCTS ts) :: res) others 280 | conj res (((vars, sub), ts, p :: ps) :: others) = 281 let 282 val vts = p (vars, sub) 283 fun f ((vars', sub'), t) = 284 ((vars', refine_subst sub sub'), t :: map (PINST sub') ts, ps) 285 in 286 conj res (map f vts @ others) 287 end; 288in 289 fun conj_provers [] = raise BUG "string_provers" "no provers to string" 290 | conj_provers (ps : cond_prover list) : cond_prover = 291 fn vs => conj [] [(vs, [], ps)] 292end; 293 294fun k_prover th : cond_prover = fn vars_sub => [(vars_sub, th)]; 295 296fun dest_trivial cond = 297 let 298 val (bvars, (asm, heart)) = ((I ## dest_imp) o dest_foralls) cond 299 val (elt, set) = dest_in heart 300 val _ = assert (fst (dest_const set) = "UNIV") 301 in 302 (bvars, asm, elt) 303 end; 304val is_trivial = can dest_trivial; 305 306fun prove_trivial cond = 307 let 308 val (bvars, asm, elt) = dest_trivial cond 309 in 310 GENL (rev bvars) (DISCH asm (ISPEC elt IN_UNIV)) 311 end; 312 313fun subtype_check ccache congs stricttypechecking depth = 314 let 315 fun cached_basic_subtypes facts tm = 316 if not (!cache_subtypes) orelse not (null (free_vars tm)) then 317 basic_subtypes facts tm 318 else 319 cache_lookup ccache 320 ((tm, depth), fn () => basic_subtypes facts tm) 321 and basic_subtypes facts tm = 322 let 323 val _ = trace_x 4 "basic_subtypes: tm" term_to_string tm 324 val (vars, th) = find_matching_cong congs tm 325 val conds = (conjuncts o fst o dest_imp o concl) th 326 val _ = 327 trace_x 4 "basic_subtypes: conds" 328 (list_to_string term_to_string) conds 329 val cond_provers = map (cond_prover facts) conds 330 val cond_results = conj_provers cond_provers (vars, empty_subst) 331 val _ = 332 assert (not stricttypechecking orelse not (null cond_results)) 333 (ERR "subtypecheck" 334 ("no basic type for subterm:\n" ^ term_to_string tm)) 335 fun process_result ((vars', sub'), th') = (vars', MP (PINST sub' th) th') 336 in 337 partial_map (total process_result) cond_results 338 end 339 and cond_prover facts cond = 340 if Teq cond then k_prover TRUTH 341 else if not stricttypechecking andalso is_trivial cond then 342 k_prover (prove_trivial cond) 343 else 344 let 345 val (bvars, body) = genvar_dest_foralls cond 346 val (asm, elt_set) = dest_imp body 347 val (elt, set) = dest_in elt_set 348 val elt_th = QCONV (N_BETA_CONV (length bvars)) elt 349 val elt' = RHS elt_th 350 val facts' = factdb_add_vthm (empty_vars, ASSUME asm) facts 351 val basics = cached_basic_subtypes facts' elt' 352 val facts'' = factdb_add_vthms basics facts' 353 val canon_rule = 354 CONV_RULE (RATOR_CONV (RAND_CONV (K (SYM elt_th)))) THENR 355 DISCH asm THENR 356 GENL (rev bvars) 357 fun canon_result (s, (v, th)) = ((v, s), canon_rule th) 358 in 359 fn (before_vars, before_sub) => 360 let 361 val set' = pinst before_sub set 362 val goal = mk_in (elt', set') 363 val pre_results = set_prove_depth facts'' depth (before_vars, goal) 364 val results = map canon_result pre_results 365 in 366 results 367 end 368 end 369 in 370 cached_basic_subtypes 371 end; 372 373fun SUBTYPE_CHECK stricttypechecking depth sc tm = 374 subtype_check (subtype_context_ccache sc) (subtype_context_subtypes sc) 375 stricttypechecking depth (subtype_context_facts sc) tm; 376 377(* Type skeletons are perhaps useful for free variables *) 378(* (or maybe are best left in the closet...) *) 379(* Example: *) 380(* Input: ('a -> 'b) -> 'c *) 381(* Output: !v : ('a -> 'b) -> 'c. v IN (UNIV -> UNIV) -> UNIV *) 382 383local 384 val UNIV = ``UNIV : 'a -> bool`` 385 386 fun set ty = ty --> bool 387in 388 fun mk_skeleton_eq ty = 389 if can dom_rng ty then 390 let 391 val (dom, rng) = dom_rng ty 392 val (dom_eq, rng_eq) = Df mk_skeleton_eq (dom, rng) 393 val c = mk_const ("FUNSET", set dom --> set rng --> set ty) 394 val set_eq = MK_COMB (MK_COMB (REFL c, dom_eq), rng_eq) 395 in 396 TRANS set_eq (INST_TY [alpha |-> dom, beta |-> rng] UNIV_FUNSET_UNIV) 397 end 398 else REFL (inst_ty [alpha |-> ty] UNIV) 399 400 val mk_skeleton = MATCH_MP IN_EQ_UNIV_IMP o mk_skeleton_eq 401end; 402 403(* HOL conversions and tactics *) 404 405fun SUBTYPE_MATCH depth sc (vars, goal) = 406 let 407 val (elt, _) = dest_in goal 408 val subtypes = SUBTYPE_CHECK false depth sc elt 409 val facts = factdb_add_vthms subtypes (subtype_context_facts sc) 410 val res = set_prove_depth facts depth (vars, goal) 411 in 412 res 413 end; 414 415fun SUBTYPE_PROVE depth sc goal = 416 (case SUBTYPE_MATCH depth sc (empty_vars, goal) of (_, (_, th)) :: _ => th 417 | [] => raise ERR "SUBTYPE_PROVE" "couldn't!") 418 419fun SUBTYPE_CONV_DEPTH depth sc goal = EQT_INTRO (SUBTYPE_PROVE depth sc goal); 420 421val SUBTYPE_CONV = SUBTYPE_CONV_DEPTH (!subtype_depth); 422 423fun SUBTYPE_TAC sc : tactic = 424 ASSUM_LIST 425 (fn ths => 426 CONV_TAC (SUBTYPE_CONV (subtype_context_add_judgements ths sc))); 427 428(* ========================================================================= *) 429(* A simplifier skeleton using predicate subtyping as a decision procedure. *) 430(* ========================================================================= *) 431 432(* Types *) 433 434type c_rule = ho_substitution -> vthm -> vthm list; 435type c_rewr = ho_substitution -> conv -> (term -> thm) -> conv; 436 437datatype context = CONTEXT of 438 {subtypes : subtype_context, 439 forwards : thm list, 440 rules : c_rule ovdiscrim, 441 congs : vthm ovdiscrim, 442 rewrs : c_rewr ovdiscrim}; 443 444datatype context_element = 445 C_THM of thm 446 | C_REWR of vterm * c_rewr 447 | C_CONG of thm 448 | C_RULE of vterm * c_rule 449 | C_SUBTYPE of subtype_context_element 450 | C_FORWARDS of thm; 451 452(* Tuning parameters *) 453 454val simplify_max_traversals = ref 5; 455val simplify_max_depth = ref 3; 456val simplify_max_rewrites = ref 10; 457val simplify_subtype_depth = ref 3; 458val simplify_forwards = ref 10; 459 460(* Pretty-printing *) 461 462fun pp_context (CONTEXT c) = 463 block INCONSISTENT 1 [ 464 block CONSISTENT 2 [ 465 add_string "{subtypes =", 466 add_break (1, 0), 467 pp_subtype_context (#subtypes c), 468 add_string "," 469 ], 470 add_break (1, 0), 471 472 block CONSISTENT 2 [ 473 add_string "#forwards =", 474 add_break (1, 0), 475 pp_int (length (#forwards c)), 476 add_string "," 477 ], 478 add_break (1, 0), 479 480 block CONSISTENT 2 [ 481 add_string "#congs =", 482 add_break (1, 0), 483 pp_int (ovdiscrim_size (#congs c)), 484 add_string "," 485 ], 486 add_break (1, 0), 487 488 block CONSISTENT 2 [ 489 add_string "#rules =", 490 add_break (1, 0), 491 pp_int (ovdiscrim_size (#rules c)), 492 add_string "," 493 ], 494 add_break (1, 0), 495 496 block CONSISTENT 2 [ 497 add_string "#rewrs =", 498 add_break (1, 0), 499 pp_int (ovdiscrim_size (#rewrs c)), 500 add_string "}" 501 ] 502 ] 503 504(* Basic context operations *) 505 506fun new_context () = CONTEXT 507 {subtypes = new_subtype_context (), 508 forwards = [], 509 rules = empty_ovdiscrim, 510 congs = empty_ovdiscrim, 511 rewrs = empty_ovdiscrim}; 512 513fun dest_context (CONTEXT c) = c; 514val context_subtypes = #subtypes o dest_context; 515val context_forwards = #forwards o dest_context; 516val context_rules = #rules o dest_context; 517val context_congs = #congs o dest_context; 518val context_rewrs = #rewrs o dest_context; 519 520fun context_update_subtypes f 521 (CONTEXT {subtypes, forwards, rules, congs, rewrs}) = 522 CONTEXT {subtypes = f subtypes, forwards = forwards, rules = rules, 523 congs = congs, rewrs = rewrs}; 524 525fun context_update_forwards f 526 (CONTEXT {subtypes, forwards, rules, congs, rewrs}) = 527 CONTEXT {subtypes = subtypes, forwards = f forwards, rules = rules, 528 congs = congs, rewrs = rewrs}; 529 530fun context_update_rules f 531 (CONTEXT {subtypes, forwards, rules, congs, rewrs}) = 532 CONTEXT {subtypes = subtypes, forwards = forwards, rules = f rules, 533 congs = congs, rewrs = rewrs}; 534 535fun context_update_congs f 536 (CONTEXT {subtypes, forwards, rules, congs, rewrs}) = 537 CONTEXT {subtypes = subtypes, forwards = forwards, rules = rules, 538 congs = f congs, rewrs = rewrs}; 539 540fun context_update_rewrs f 541 (CONTEXT {subtypes, forwards, rules, congs, rewrs}) = 542 CONTEXT {subtypes = subtypes, forwards = forwards, rules = rules, 543 congs = congs, rewrs = f rewrs}; 544 545fun rewr_vthm_to_rewr (vars : vars, th) : vterm * c_rewr = 546 let 547 val (cond, (pat, _)) = ((I ## dest_eq) o dest_imp o concl) th 548 val f = ho_subst_COND_REWR th o (if Teq cond then K (K TRUTH) else I) 549 fun rewr ho_sub _ prover (_ : term) = f prover ho_sub 550 in 551 ((vars, pat), rewr) 552 end; 553 554local 555 val undisch_asm = ((fst o dest_imp o concl) ## UNDISCH) o D 556 557 fun imp_rule (asms, (vars, th)) = 558 let 559 val (asm, th') = undisch_asm th 560 in 561 (asm :: asms, (vars, th')) 562 end 563 564 fun is_subterm tm1 tm2 = can (find_term (aconv tm1)) tm2 565 566 fun good_rewr (vars, _) th = 567 let 568 val _ = trace_x 2 "vthm_to_rewr_vthms: th" thm_to_string th 569 val (asm, (l, r)) = ((I ## dest_eq) o dest_imp o concl) th 570 val res = 571 not (is_subterm l asm) andalso not (is_subterm l r) andalso 572 (HOLset.isSubset (listset vars Isct FVLset [asm, r], FVs l)) 573 val _ = trace 2 574 ("vthm_to_rewr_vthms: " ^ (if res then "accepted" else "rejected")) 575 in 576 res 577 end; 578in 579 fun vthm_to_rewr_vthms rules = 580 let 581 fun break res [] = res 582 | break res ((asms, (vars, th)) :: rest) = 583 let 584 val tm = concl th 585 val matches = ovdiscrim_ho_match rules tm 586 in 587 case partial_first (fn (s, f) => total (f s) (vars, th)) matches of 588 SOME split => break res (map (add_fst asms) split @ rest) 589 | NONE => 590 if is_imp tm then 591 break res (imp_rule (asms, (vars, th)) :: rest) 592 else 593 let 594 val rewr_thm = 595 ((if is_eq (concl th) then ALL_RULE else EQT_INTRO) THENR 596 CONV_RULE (REPEATC EQ_NEG_BOOL_CONV) THENR 597 (if null asms then DISCH T else DISCH_CONJUNCTS asms)) th 598 val res' = 599 (if good_rewr vars rewr_thm then cons (vars, rewr_thm) 600 else I) res 601 in 602 break res' rest 603 end 604 end 605 in 606 fn vthm => break [] [([], vthm)] 607 end; 608end; 609 610fun thm_to_rewr_vthms rules = vthm_to_rewr_vthms rules o thm_to_vthm; 611 612fun vthm_to_rewrs rules = map rewr_vthm_to_rewr o vthm_to_rewr_vthms rules; 613fun thm_to_rewrs rules = vthm_to_rewrs rules o thm_to_vthm; 614 615fun pattern_thing (tm, r) = 616 (term_to_vterm tm, fn (_ : ho_substitution) => r); 617 618fun pattern_rewr x : vterm * c_rewr = pattern_thing x; 619 620fun pattern_rule x : vterm * c_rule = pattern_thing x; 621 622(* Adding things to contexts *) 623 624val context_add_subtype = context_update_subtypes o subtype_context_add; 625val context_add_forwards = context_update_forwards o cons; 626val context_add_rewr = context_update_rewrs o ovdiscrim_add; 627val context_add_rewrs = C (trans context_add_rewr); 628val context_add_rule = context_update_rules o ovdiscrim_add; 629 630local 631 fun prepare (vars, th) = 632 let 633 val tm = (fst o dest_eq o snd o dest_imp o concl) th 634 in 635 ((vars, tm), (vars, th)) 636 end; 637 638 val prepare_cong = prepare o thm_to_vthm o cong_canon; 639in 640 val context_add_cong = context_update_congs o ovdiscrim_add o prepare_cong 641end; 642 643fun context_add_fact x ctext = 644 (context_update_subtypes (subtype_context_add_fact x) o 645 context_add_rewrs (vthm_to_rewrs (context_rules ctext) x)) ctext; 646 647val context_add_facts = C (trans context_add_fact); 648 649fun context_add_thm x ctext = 650 context_add_rewrs (thm_to_rewrs (context_rules ctext) x) ctext; 651 652val context_add_thms = C (trans context_add_thm); 653 654fun context_add_element (C_THM th) = context_add_thm th 655 | context_add_element (C_FORWARDS th) = context_add_forwards th 656 | context_add_element (C_REWR r) = context_add_rewr r 657 | context_add_element (C_CONG c) = context_add_cong c 658 | context_add_element (C_RULE r) = context_add_rule r 659 | context_add_element (C_SUBTYPE s) = context_add_subtype s; 660 661val context_add_elements = C (trans context_add_element); 662 663(* The core rewriting engine *) 664 665local 666 local 667 fun align vars' vars opat tm = 668 let 669 val (bvar, body) = dest_abs tm 670 val _ = assert (is_genvar bvar) (ERR "alpha_align" "not a genvar abs") 671 val (v, sub_opat) = 672 if (case opat of SOME pat => is_abs pat | NONE => false) then 673 (I ## SOME) (dest_abs (grab opat)) 674 else (mk_var ("v", type_of bvar), NONE) 675 val v' = variant (all_vars body @ vars') v 676 in 677 mk_abs (v', align (v' :: vars') (bvar :: vars) sub_opat body) 678 end 679 handle (HOL_ERR _) => subst (zipwith (curry op|->) vars vars') tm 680 in 681 fun alpha_align pat tm = 682 let 683 val res = align [] [] (SOME pat) tm 684 in 685 res 686 end 687 end; 688 689 fun match_align bvars l r tm = 690 let 691 val n = length bvars 692 val tm_abs = trans (curry mk_abs) tm bvars 693 val l_body = N n rator l 694 val tm_pretty_abs = alpha_align l_body tm_abs 695 val tm' = fold (C (curry mk_comb)) tm_pretty_abs bvars 696 val tm_th = QCONV (N n (fn c => RATOR_CONV c THENC BETA_CONV) ALL_CONV) tm' 697 val (r_var, r_bvs) = list_dest_comb r 698 val _ = assert (tml_eq bvars (rev r_bvs)) (BUG "match_align" "bvar panic") 699 val res = (([r_var |-> tm_pretty_abs], []), SYM tm_th) 700 in 701 res 702 end 703 handle (h as HOL_ERR _) => raise err_BUG "match_align" h; 704 705 fun eval_rewr rewr ctext cond = 706 let 707 val (bvars, body) = genvar_dest_foralls cond 708 val (asm, (l, r)) = ((I ## dest_eq) o dest_imp) body 709 val ctext' = 710 if Teq asm then ctext 711 else context_add_fact (empty_vars, ASSUME asm) ctext 712 val raw_eq = QCONV (N_BETA_CONV (length bvars) THENC rewr ctext') l 713 val (sub, match_eq) = match_align bvars l r (RHS raw_eq) 714 val res_eq = (DISCH asm THENR GENL (rev bvars)) (TRANS raw_eq match_eq) 715 in 716 (sub, res_eq) 717 end 718 handle (h as HOL_ERR _) => raise err_BUG "eval_rewr" h; 719 720 fun eval_rewrs _ _ res [] = res 721 | eval_rewrs rewr ctext (sub, CONDS) (cond :: rest) = 722 let 723 val (sub', COND) = eval_rewr rewr ctext (pinst sub cond) 724 in 725 eval_rewrs rewr ctext (refine_subst sub sub', COND :: CONDS) rest 726 end 727 handle (h as HOL_ERR _) => raise err_BUG "eval_rewrs" h; 728 729 fun execute_cong rewr ctext (vars, th) = 730 let 731 val conds = (conjuncts o fst o dest_imp o concl) th 732 val (sub, CONDS) = eval_rewrs rewr ctext (empty_subst, []) conds 733 val res = MP (PINST sub th) (REV_CONJUNCTS CONDS) 734 in 735 res 736 end 737 handle (h as HOL_ERR _) => raise err_BUG "execute_cong" h; 738in 739 fun SIMPLIFY_CONG_CONV rewr ctext tm = 740 let 741 val cong = find_matching_cong (context_congs ctext) tm 742 val res = execute_cong rewr ctext cong 743 in 744 res 745 end 746end; 747 748fun SIMPLIFY_REWR_CONV simper prover rewrs tm = 749 let 750 val _ = trace_x 4 "SIMPLIFY_REWR_CONV: input" term_to_string tm 751 val matches = ovdiscrim_ho_match rewrs tm 752 val _ = 753 trace_x 4 "SIMPLIFY_REWR_CONV: #matches" (int_to_string o length) matches 754 val conv = FIRSTC (map (fn (ho_sub, f) => f ho_sub simper prover) matches) 755 in 756 (QCONV conv THENC 757 trace_CONV 4 "SIMPLIFY_REWR_CONV result") tm 758 end; 759 760(* Warning: do not eta-reduce this function! *) 761fun GEN_SIMPLIFY_CONV s p ctext tm = 762 QCONV 763 ((TRYC o REPEATC_CUTOFF (!simplify_max_traversals) o CHANGED_CONV) 764 (trace_CONV 2 "GEN_SIMPLIFY_CONV input" THENC 765 TRYC (REPEATC_CUTOFF (!simplify_max_rewrites) 766 (SIMPLIFY_REWR_CONV (GEN_SIMPLIFY_CONV s p ctext) 767 (s ctext) (context_rewrs ctext))) THENC 768 trace_CONV 2 "GEN_SIMPLIFY_CONV after rewr" THENC 769 TRYC (p ctext) THENC 770 TRYC (SIMPLIFY_CONG_CONV (GEN_SIMPLIFY_CONV s p) ctext) THENC 771 trace_CONV 2 "GEN_SIMPLIFY_CONV result")) tm; 772 773val no_prover_conv : context -> conv = K NO_CONV; 774 775fun subtype_prover_conv ctext = 776 QCONV (SUBTYPE_CONV_DEPTH (!simplify_subtype_depth) (context_subtypes ctext)); 777 778(* Warning: do not eta-reduce this function! *) 779fun SIMPLIFY_CONV_DEPTH 0 _ _ = raise ERR "SIMPLIFY_CONV" "too deep!" 780 | SIMPLIFY_CONV_DEPTH n ctext tm = 781 QCONV 782 (GEN_SIMPLIFY_CONV (EQT_ELIM oo SIMPLIFY_CONV_DEPTH (n - 1)) 783 subtype_prover_conv ctext) tm; 784 785fun SIMPLIFY_CONV' ctext tm = 786 QCONV (SIMPLIFY_CONV_DEPTH (!simplify_max_depth) ctext) tm; 787 788fun SIMPLIFY_CONV ctext = 789 QCONV 790 (trace_CONV 1 "SIMPLIFY_CONV input" THENC 791 GEN_SIMPLIFY_CONV (EQT_ELIM oo SIMPLIFY_CONV') no_prover_conv ctext THENC 792 TRYC (subtype_prover_conv ctext) THENC 793 trace_CONV 1 "SIMPLIFY_CONV result"); 794 795fun SIMPLIFY_TAC_X conv ctext ths = 796 let 797 val ths' = map GEN_ALL ths 798 in 799 ASSUM_LIST 800 (CONV_TAC o 801 conv o 802 C context_add_facts ctext o 803 map thm_to_vthm o 804 MATCH_MP_DEPTH (!simplify_forwards) (ths' @ context_forwards ctext) o 805 append ths') 806 end; 807 808fun PRESIMPLIFY_TAC ctext ths = 809 EVERY (map (ASSUME_TAC o GEN_ALL) ths) 810 ++ ASM_MATCH_MP_TAC (ths @ context_forwards ctext); 811 812val SIMPLIFY_TAC' = SIMPLIFY_TAC_X SIMPLIFY_CONV'; 813val SIMPLIFY_TAC = SIMPLIFY_TAC_X SIMPLIFY_CONV; 814 815fun ASM_SIMPLIFY_TAC_X tac ctext ths = POP_ASSUM_TAC (tac ctext ths); 816val ASM_SIMPLIFY_TAC' = ASM_SIMPLIFY_TAC_X SIMPLIFY_TAC'; 817val ASM_SIMPLIFY_TAC = ASM_SIMPLIFY_TAC_X SIMPLIFY_TAC; 818 819fun SIMPLIFY_TACS ctext = 820 (SIMPLIFY_TAC ctext, ASM_SIMPLIFY_TAC ctext, 821 SIMPLIFY_TAC' ctext, ASM_SIMPLIFY_TAC' ctext); 822 823(* ------------------------------------------------------------------------- *) 824(* Simplification modules. *) 825(* ------------------------------------------------------------------------- *) 826 827datatype precontext = PRECONTEXT of (string * context_element list) list; 828 829val empty_precontext = PRECONTEXT []; 830 831val pp_precontext = pp_map (fn PRECONTEXT pc => map fst pc) (pp_list pp_string); 832 833fun precontext_add (n, f) (PRECONTEXT p) = 834 (assert (not (exists (curry op= n o fst) p)) 835 (ERR "precontext_add" (n ^ " already exists in precontext")); 836 PRECONTEXT (p @ [(n, f)])); 837 838fun precontext_compile (PRECONTEXT p) = 839 (context_update_subtypes subtype_context_initialize o 840 context_add_elements (flatten (map snd p))) (new_context ()); 841 842fun precontext_merge (PRECONTEXT p1) (PRECONTEXT p2) = 843 PRECONTEXT (p1 @ filter (fn (n, _) => not (exists (equal n o fst) p1)) p2); 844 845fun precontext_mergel [] = empty_precontext 846 | precontext_mergel (p::rest) = precontext_merge p (precontext_mergel rest); 847 848(* ------------------------------------------------------------------------- *) 849(* Subtype-checking examples. *) 850(* ------------------------------------------------------------------------- *) 851 852(* 853set_trace "subtypeTools" 3; 854 855val stc = tt4 SUBTYPE_CHECK true 3 (context_subtypes hol_c); 856 857stc ``!f :: UNIV -> UNIV. f x``; 858stc ``!f :: UNIV -> UNIV -> UNIV. f x x``; 859stc ``\x. x``; 860stc ``\x. [x]``; 861stc ``!x :: nzreal. x / x = 1``; 862stc ``\x y :: nzreal. MAP inv [x; y]``; 863stc ``\x :: negreal. FUNPOW inv n x``; 864stc ``\x :: posreal. sqrt (FUNPOW inv n x)``; 865stc ``MAP inv (~1 :: MAP sqrt [1; 1])``; 866stc ``!x :: P. x IN P /\ x IN Q``; 867 868stc ``~3 : real``; 869 870ff stc ``inv x * x = 1``; 871stc ``x IN nzreal ==> (inv x * x = 1)``; 872stc ``inv IN (real -> nzreal) ==> (inv x * x = 1)``; 873stc ``inv IN (real -> real) ==> (inv x * x = 1)``; 874*) 875 876(* ------------------------------------------------------------------------- *) 877(* Subtype-checking plus rewriting examples. *) 878(* ------------------------------------------------------------------------- *) 879 880(* 881allow_trace "execute_cong"; 882allow_trace "eval_rewr"; 883allow_trace "match_align"; 884allow_trace "alpha_align"; 885allow_trace "SIMPLIFY_TYPECHECK"; 886allow_trace "SIMPLIFY_TYPECHECK: (tm, res)"; 887allow_trace "SUBTYPE_MATCH"; 888allow_trace "GEN_SIMPLIFY_CONV input"; 889allow_trace "GEN_SIMPLIFY_CONV result"; 890reset_traces (); 891allow_trace "SIMPLIFY_CONV"; 892 893tt prove 894(``~3 IN nzreal``, 895 SUBTYPE_TAC (context_subtypes hol_c)); 896 897tt prove 898(``(MAP inv (CONS (~1) (MAP sqrt [3; 1]))) IN list nzreal``, 899 SUBTYPE_TAC (context_subtypes hol_c)); 900 901tt prove 902(``(\x :: negreal. FUNPOW inv n x) IN negreal -> negreal``, 903 SUBTYPE_TAC (context_subtypes hol_c)); 904 905tt prove 906(``(!x :: nzreal. x / x = 1) ==> (5 / 5 = 3 / 3)``, 907 SIMPLIFY_TAC hol_c []); 908*) 909 910 911(* non-interactive mode 912*) 913end; 914