1(* Title: Pure/more_thm.ML 2 Author: Makarius 3 4Further operations on type ctyp/cterm/thm, outside the inference kernel. 5*) 6 7infix aconvc; 8 9signature BASIC_THM = 10sig 11 include BASIC_THM 12 val show_consts: bool Config.T 13 val show_hyps: bool Config.T 14 val show_tags: bool Config.T 15 structure Ctermtab: TABLE 16 structure Thmtab: TABLE 17 val aconvc: cterm * cterm -> bool 18 type attribute = Context.generic * thm -> Context.generic option * thm option 19end; 20 21signature THM = 22sig 23 include THM 24 structure Ctermtab: TABLE 25 structure Thmtab: TABLE 26 val eq_ctyp: ctyp * ctyp -> bool 27 val aconvc: cterm * cterm -> bool 28 val add_tvars: thm -> ctyp list -> ctyp list 29 val add_frees: thm -> cterm list -> cterm list 30 val add_vars: thm -> cterm list -> cterm list 31 val dest_funT: ctyp -> ctyp * ctyp 32 val strip_type: ctyp -> ctyp list * ctyp 33 val all_name: Proof.context -> string * cterm -> cterm -> cterm 34 val all: Proof.context -> cterm -> cterm -> cterm 35 val mk_binop: cterm -> cterm -> cterm -> cterm 36 val dest_binop: cterm -> cterm * cterm 37 val dest_implies: cterm -> cterm * cterm 38 val dest_equals: cterm -> cterm * cterm 39 val dest_equals_lhs: cterm -> cterm 40 val dest_equals_rhs: cterm -> cterm 41 val lhs_of: thm -> cterm 42 val rhs_of: thm -> cterm 43 val fast_term_ord: cterm ord 44 val term_ord: cterm ord 45 val thm_ord: thm ord 46 val cterm_cache: (cterm -> 'a) -> cterm -> 'a 47 val thm_cache: (thm -> 'a) -> thm -> 'a 48 val is_reflexive: thm -> bool 49 val eq_thm: thm * thm -> bool 50 val eq_thm_prop: thm * thm -> bool 51 val eq_thm_strict: thm * thm -> bool 52 val equiv_thm: theory -> thm * thm -> bool 53 val class_triv: theory -> class -> thm 54 val of_sort: ctyp * sort -> thm list 55 val is_dummy: thm -> bool 56 val add_thm: thm -> thm list -> thm list 57 val del_thm: thm -> thm list -> thm list 58 val merge_thms: thm list * thm list -> thm list 59 val full_rules: thm Item_Net.T 60 val intro_rules: thm Item_Net.T 61 val elim_rules: thm Item_Net.T 62 val declare_hyps: cterm -> Proof.context -> Proof.context 63 val assume_hyps: cterm -> Proof.context -> thm * Proof.context 64 val unchecked_hyps: Proof.context -> Proof.context 65 val restore_hyps: Proof.context -> Proof.context -> Proof.context 66 val undeclared_hyps: Context.generic -> thm -> term list 67 val check_hyps: Context.generic -> thm -> thm 68 val declare_term_sorts: term -> Proof.context -> Proof.context 69 val extra_shyps': Proof.context -> thm -> sort list 70 val check_shyps: Proof.context -> thm -> thm 71 val weaken_sorts': Proof.context -> cterm -> cterm 72 val elim_implies: thm -> thm -> thm 73 val forall_intr_name: string * cterm -> thm -> thm 74 val forall_elim_var: int -> thm -> thm 75 val forall_elim_vars: int -> thm -> thm 76 val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm 77 val instantiate': ctyp option list -> cterm option list -> thm -> thm 78 val forall_intr_frees: thm -> thm 79 val unvarify_global: theory -> thm -> thm 80 val unvarify_axiom: theory -> string -> thm 81 val rename_params_rule: string list * int -> thm -> thm 82 val rename_boundvars: term -> term -> thm -> thm 83 val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory 84 val add_axiom_global: binding * term -> theory -> (string * thm) * theory 85 val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory 86 val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory 87 type attribute = Context.generic * thm -> Context.generic option * thm option 88 type binding = binding * attribute list 89 val tag_rule: string * string -> thm -> thm 90 val untag_rule: string -> thm -> thm 91 val is_free_dummy: thm -> bool 92 val tag_free_dummy: thm -> thm 93 val def_name: string -> string 94 val def_name_optional: string -> string -> string 95 val def_binding: Binding.binding -> Binding.binding 96 val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding 97 val make_def_binding: bool -> Binding.binding -> Binding.binding 98 val has_name_hint: thm -> bool 99 val get_name_hint: thm -> string 100 val put_name_hint: string -> thm -> thm 101 val theoremK: string 102 val legacy_get_kind: thm -> string 103 val kind_rule: string -> thm -> thm 104 val rule_attribute: thm list -> (Context.generic -> thm -> thm) -> attribute 105 val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute 106 val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute 107 val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic 108 val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic 109 val theory_attributes: attribute list -> thm -> theory -> thm * theory 110 val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context 111 val no_attributes: 'a -> 'a * 'b list 112 val simple_fact: 'a -> ('a * 'b list) list 113 val tag: string * string -> attribute 114 val untag: string -> attribute 115 val kind: string -> attribute 116 val register_proofs: thm list lazy -> theory -> theory 117 val consolidate_theory: theory -> unit 118 val expose_theory: theory -> unit 119 val show_consts: bool Config.T 120 val show_hyps: bool Config.T 121 val show_tags: bool Config.T 122 val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T 123 val pretty_thm: Proof.context -> thm -> Pretty.T 124 val pretty_thm_item: Proof.context -> thm -> Pretty.T 125 val pretty_thm_global: theory -> thm -> Pretty.T 126 val string_of_thm: Proof.context -> thm -> string 127 val string_of_thm_global: theory -> thm -> string 128end; 129 130structure Thm: THM = 131struct 132 133(** basic operations **) 134 135(* collecting ctyps and cterms *) 136 137val eq_ctyp = op = o apply2 Thm.typ_of; 138val op aconvc = op aconv o apply2 Thm.term_of; 139 140val add_tvars = Thm.fold_atomic_ctyps (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a); 141val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a); 142val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a); 143 144 145(* ctyp operations *) 146 147fun dest_funT cT = 148 (case Thm.typ_of cT of 149 Type ("fun", _) => let val [A, B] = Thm.dest_ctyp cT in (A, B) end 150 | T => raise TYPE ("dest_funT", [T], [])); 151 152(* ctyp version of strip_type: maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *) 153fun strip_type cT = 154 (case Thm.typ_of cT of 155 Type ("fun", _) => 156 let 157 val (cT1, cT2) = dest_funT cT; 158 val (cTs, cT') = strip_type cT2 159 in (cT1 :: cTs, cT') end 160 | _ => ([], cT)); 161 162 163(* cterm operations *) 164 165fun all_name ctxt (x, t) A = 166 let 167 val T = Thm.typ_of_cterm t; 168 val all_const = Thm.cterm_of ctxt (Const ("Pure.all", (T --> propT) --> propT)); 169 in Thm.apply all_const (Thm.lambda_name (x, t) A) end; 170 171fun all ctxt t A = all_name ctxt ("", t) A; 172 173fun mk_binop c a b = Thm.apply (Thm.apply c a) b; 174fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct); 175 176fun dest_implies ct = 177 (case Thm.term_of ct of 178 Const ("Pure.imp", _) $ _ $ _ => dest_binop ct 179 | _ => raise TERM ("dest_implies", [Thm.term_of ct])); 180 181fun dest_equals ct = 182 (case Thm.term_of ct of 183 Const ("Pure.eq", _) $ _ $ _ => dest_binop ct 184 | _ => raise TERM ("dest_equals", [Thm.term_of ct])); 185 186fun dest_equals_lhs ct = 187 (case Thm.term_of ct of 188 Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg1 ct 189 | _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct])); 190 191fun dest_equals_rhs ct = 192 (case Thm.term_of ct of 193 Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg ct 194 | _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct])); 195 196val lhs_of = dest_equals_lhs o Thm.cprop_of; 197val rhs_of = dest_equals_rhs o Thm.cprop_of; 198 199 200(* certified term order *) 201 202val fast_term_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of; 203val term_ord = Term_Ord.term_ord o apply2 Thm.term_of; 204 205 206(* thm order: ignores theory context! *) 207 208val thm_ord = 209 Term_Ord.fast_term_ord o apply2 Thm.prop_of 210 <<< list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 Thm.tpairs_of 211 <<< list_ord Term_Ord.fast_term_ord o apply2 Thm.hyps_of 212 <<< list_ord Term_Ord.sort_ord o apply2 Thm.shyps_of; 213 214 215(* tables and caches *) 216 217structure Ctermtab = Table(type key = cterm val ord = fast_term_ord); 218structure Thmtab = Table(type key = thm val ord = thm_ord); 219 220fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f; 221fun thm_cache f = Cache.create Thmtab.empty Thmtab.lookup Thmtab.update f; 222 223 224(* equality *) 225 226fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th)) 227 handle TERM _ => false; 228 229val eq_thm = is_equal o thm_ord; 230 231val eq_thm_prop = op aconv o apply2 Thm.full_prop_of; 232 233fun eq_thm_strict ths = 234 eq_thm ths andalso 235 Context.eq_thy_id (apply2 Thm.theory_id ths) andalso 236 op = (apply2 Thm.maxidx_of ths) andalso 237 op = (apply2 Thm.get_tags ths); 238 239 240(* pattern equivalence *) 241 242fun equiv_thm thy ths = 243 Pattern.equiv thy (apply2 (Thm.full_prop_of o Thm.transfer thy) ths); 244 245 246(* type classes and sorts *) 247 248fun class_triv thy c = 249 Thm.of_class (Thm.global_ctyp_of thy (TVar ((Name.aT, 0), [c])), c); 250 251fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S; 252 253 254(* misc operations *) 255 256fun is_dummy thm = 257 (case try Logic.dest_term (Thm.concl_of thm) of 258 NONE => false 259 | SOME t => Term.is_dummy_pattern (Term.head_of t)); 260 261 262(* collections of theorems in canonical order *) 263 264val add_thm = update eq_thm_prop; 265val del_thm = remove eq_thm_prop; 266val merge_thms = merge eq_thm_prop; 267 268val full_rules = Item_Net.init eq_thm_prop (single o Thm.full_prop_of); 269val intro_rules = Item_Net.init eq_thm_prop (single o Thm.concl_of); 270val elim_rules = Item_Net.init eq_thm_prop (single o Thm.major_prem_of); 271 272 273 274(** declared hyps and sort hyps **) 275 276structure Hyps = Proof_Data 277( 278 type T = {checked_hyps: bool, hyps: Termtab.set, shyps: sort Ord_List.T}; 279 fun init _ : T = {checked_hyps = true, hyps = Termtab.empty, shyps = []}; 280); 281 282fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} => 283 let val (checked_hyps', hyps', shyps') = f (checked_hyps, hyps, shyps) 284 in {checked_hyps = checked_hyps', hyps = hyps', shyps = shyps'} end); 285 286 287(* hyps *) 288 289fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) => 290 let 291 val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct; 292 val hyps' = Termtab.update (Thm.term_of ct, ()) hyps; 293 in (checked_hyps, hyps', shyps) end); 294 295fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt); 296 297val unchecked_hyps = map_hyps (fn (_, hyps, shyps) => (false, hyps, shyps)); 298 299fun restore_hyps ctxt = 300 map_hyps (fn (_, hyps, shyps) => (#checked_hyps (Hyps.get ctxt), hyps, shyps)); 301 302fun undeclared_hyps context th = 303 Thm.hyps_of th 304 |> filter_out 305 (case context of 306 Context.Theory _ => K false 307 | Context.Proof ctxt => 308 (case Hyps.get ctxt of 309 {checked_hyps = false, ...} => K true 310 | {hyps, ...} => Termtab.defined hyps)); 311 312fun check_hyps context th = 313 (case undeclared_hyps context th of 314 [] => th 315 | undeclared => 316 error (Pretty.string_of (Pretty.big_list "Undeclared hyps:" 317 (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared)))); 318 319 320(* shyps *) 321 322fun declare_term_sorts t = 323 map_hyps (fn (checked_hyps, hyps, shyps) => 324 (checked_hyps, hyps, Sorts.insert_term t shyps)); 325 326fun extra_shyps' ctxt th = 327 Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th); 328 329fun check_shyps ctxt raw_th = 330 let 331 val th = Thm.strip_shyps raw_th; 332 val extra_shyps = extra_shyps' ctxt th; 333 in 334 if null extra_shyps then th 335 else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" :: 336 Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) extra_shyps)))) 337 end; 338 339val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get; 340 341 342 343(** basic derived rules **) 344 345(*Elimination of implication 346 A A \<Longrightarrow> B 347 ------------ 348 B 349*) 350fun elim_implies thA thAB = Thm.implies_elim thAB thA; 351 352 353(* forall_intr_name *) 354 355fun forall_intr_name (a, x) th = 356 let 357 val th' = Thm.forall_intr x th; 358 val prop' = (case Thm.prop_of th' of all $ Abs (_, T, b) => all $ Abs (a, T, b)); 359 in Thm.renamed_prop prop' th' end; 360 361 362(* forall_elim_var(s) *) 363 364local 365 366fun dest_all ct = 367 (case Thm.term_of ct of 368 Const ("Pure.all", _) $ Abs (a, _, _) => 369 let val (x, ct') = Thm.dest_abs NONE (Thm.dest_arg ct) 370 in SOME ((a, Thm.ctyp_of_cterm x), ct') end 371 | _ => NONE); 372 373fun dest_all_list ct = 374 (case dest_all ct of 375 NONE => [] 376 | SOME (v, ct') => v :: dest_all_list ct'); 377 378fun forall_elim_vars_list vars i th = 379 let 380 val used = 381 (Thm.fold_terms o Term.fold_aterms) 382 (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I) th []; 383 val vars' = (Name.variant_list used (map #1 vars), vars) 384 |> ListPair.map (fn (x, (_, T)) => Thm.var ((x, i), T)); 385 in fold Thm.forall_elim vars' th end; 386 387in 388 389fun forall_elim_vars i th = 390 forall_elim_vars_list (dest_all_list (Thm.cprop_of th)) i th; 391 392fun forall_elim_var i th = 393 let 394 val vars = 395 (case dest_all (Thm.cprop_of th) of 396 SOME (v, _) => [v] 397 | NONE => raise THM ("forall_elim_var", i, [th])); 398 in forall_elim_vars_list vars i th end; 399 400end; 401 402 403(* instantiate frees *) 404 405fun instantiate_frees ([], []) th = th 406 | instantiate_frees (instT, inst) th = 407 let 408 val idx = Thm.maxidx_of th + 1; 409 fun index ((a, A), b) = (((a, idx), A), b); 410 val insts = (map index instT, map index inst); 411 val frees = (map (#1 o #1) instT, map (#1 o #1) inst); 412 413 val hyps = Thm.chyps_of th; 414 val inst_cterm = 415 Thm.generalize_cterm frees idx #> 416 Thm.instantiate_cterm insts; 417 in 418 th 419 |> fold_rev Thm.implies_intr hyps 420 |> Thm.generalize frees idx 421 |> Thm.instantiate insts 422 |> fold (elim_implies o Thm.assume o inst_cterm) hyps 423 end; 424 425 426(* instantiate by left-to-right occurrence of variables *) 427 428fun instantiate' cTs cts thm = 429 let 430 fun err msg = 431 raise TYPE ("instantiate': " ^ msg, 432 map_filter (Option.map Thm.typ_of) cTs, 433 map_filter (Option.map Thm.term_of) cts); 434 435 fun zip_vars xs ys = 436 zip_options xs ys handle ListPair.UnequalLengths => 437 err "more instantiations than variables in thm"; 438 439 val thm' = 440 Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm; 441 val thm'' = 442 Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm'; 443 in thm'' end; 444 445 446(* forall_intr_frees: generalization over all suitable Free variables *) 447 448fun forall_intr_frees th = 449 let 450 val fixed = 451 fold Term.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th) @ Thm.hyps_of th) []; 452 val frees = 453 Thm.fold_atomic_cterms (fn a => 454 (case Thm.term_of a of 455 Free v => not (member (op =) fixed v) ? insert (op aconvc) a 456 | _ => I)) th []; 457 in fold Thm.forall_intr frees th end; 458 459 460(* unvarify_global: global schematic variables *) 461 462fun unvarify_global thy th = 463 let 464 val prop = Thm.full_prop_of th; 465 val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th) 466 handle TERM (msg, _) => raise THM (msg, 0, [th]); 467 468 val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S))); 469 val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) => 470 let val T' = Term_Subst.instantiateT instT T 471 in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end); 472 in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end; 473 474fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy; 475 476 477(* user renaming of parameters in a subgoal *) 478 479(*The names, if distinct, are used for the innermost parameters of subgoal i; 480 preceding parameters may be renamed to make all parameters distinct.*) 481fun rename_params_rule (names, i) st = 482 let 483 val (_, Bs, Bi, C) = Thm.dest_state (st, i); 484 val params = map #1 (Logic.strip_params Bi); 485 val short = length params - length names; 486 val names' = 487 if short < 0 then error "More names than parameters in subgoal!" 488 else Name.variant_list names (take short params) @ names; 489 val free_names = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi []; 490 val Bi' = Logic.list_rename_params names' Bi; 491 in 492 (case duplicates (op =) names of 493 a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); st) 494 | [] => 495 (case inter (op =) names free_names of 496 a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); st) 497 | [] => Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st)) 498 end; 499 500 501(* preservation of bound variable names *) 502 503fun rename_boundvars pat obj th = 504 (case Term.rename_abs pat obj (Thm.prop_of th) of 505 NONE => th 506 | SOME prop' => Thm.renamed_prop prop' th); 507 508 509 510(** specification primitives **) 511 512(* rules *) 513 514fun stripped_sorts thy t = 515 let 516 val tfrees = rev (Term.add_tfrees t []); 517 val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees)); 518 val recover = 519 map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S)))) 520 tfrees' tfrees; 521 val strip = map (apply2 TFree) (tfrees ~~ tfrees'); 522 val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t; 523 in (strip, recover, t') end; 524 525fun add_axiom ctxt (b, prop) thy = 526 let 527 val _ = Sign.no_vars ctxt prop; 528 val (strip, recover, prop') = stripped_sorts thy prop; 529 val constraints = map (fn (TFree (_, S), T) => (T, S)) strip; 530 val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of ctxt T, S)) strip; 531 532 val thy' = thy 533 |> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop')); 534 val axm_name = Sign.full_name thy' b; 535 val axm' = Thm.axiom thy' axm_name; 536 val thm = 537 Thm.instantiate (recover, []) axm' 538 |> unvarify_global thy' 539 |> fold elim_implies of_sorts; 540 in ((axm_name, thm), thy') end; 541 542fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy; 543 544fun add_def (context as (ctxt, _)) unchecked overloaded (b, prop) thy = 545 let 546 val _ = Sign.no_vars ctxt prop; 547 val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop); 548 val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop); 549 550 val thy' = Theory.add_def context unchecked overloaded (b, concl') thy; 551 val axm_name = Sign.full_name thy' b; 552 val axm' = Thm.axiom thy' axm_name; 553 val thm = 554 Thm.instantiate (recover, []) axm' 555 |> unvarify_global thy' 556 |> fold_rev Thm.implies_intr prems; 557 in ((axm_name, thm), thy') end; 558 559fun add_def_global unchecked overloaded arg thy = 560 add_def (Defs.global_context thy) unchecked overloaded arg thy; 561 562 563 564(** theorem tags **) 565 566(* add / delete tags *) 567 568fun tag_rule tg = Thm.map_tags (insert (op =) tg); 569fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); 570 571 572(* free dummy thm -- for abstract closure *) 573 574val free_dummyN = "free_dummy"; 575fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN; 576val tag_free_dummy = tag_rule (free_dummyN, ""); 577 578 579(* def_name *) 580 581fun def_name c = c ^ "_def"; 582 583fun def_name_optional c "" = def_name c 584 | def_name_optional _ name = name; 585 586val def_binding = Binding.map_name def_name #> Binding.reset_pos; 587fun def_binding_optional b name = if Binding.is_empty name then def_binding b else name; 588fun make_def_binding cond b = if cond then def_binding b else Binding.empty; 589 590 591(* unofficial theorem names *) 592 593fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN; 594fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); 595fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else "??.unknown"; 596 597fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); 598 599 600(* theorem kinds *) 601 602val theoremK = "theorem"; 603 604fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN); 605 606fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; 607 608 609 610(** attributes **) 611 612(*attributes subsume any kind of rules or context modifiers*) 613type attribute = Context.generic * thm -> Context.generic option * thm option; 614 615type binding = binding * attribute list; 616 617fun rule_attribute ths f (x, th) = 618 (NONE, 619 (case find_first is_free_dummy (th :: ths) of 620 SOME th' => SOME th' 621 | NONE => SOME (f x th))); 622 623fun declaration_attribute f (x, th) = 624 (if is_free_dummy th then NONE else SOME (f th x), NONE); 625 626fun mixed_attribute f (x, th) = 627 let val (x', th') = f (x, th) in (SOME x', SOME th') end; 628 629fun apply_attribute (att: attribute) th x = 630 let val (x', th') = att (x, check_hyps x (Thm.transfer'' x th)) 631 in (the_default th th', the_default x x') end; 632 633fun attribute_declaration att th x = #2 (apply_attribute att th x); 634 635fun apply_attributes mk dest = 636 let 637 fun app [] th x = (th, x) 638 | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts; 639 in app end; 640 641val theory_attributes = apply_attributes Context.Theory Context.the_theory; 642val proof_attributes = apply_attributes Context.Proof Context.the_proof; 643 644fun no_attributes x = (x, []); 645fun simple_fact x = [(x, [])]; 646 647fun tag tg = rule_attribute [] (K (tag_rule tg)); 648fun untag s = rule_attribute [] (K (untag_rule s)); 649fun kind k = rule_attribute [] (K (k <> "" ? kind_rule k)); 650 651 652 653(** forked proofs **) 654 655structure Proofs = Theory_Data 656( 657 type T = thm list lazy list; 658 val empty = []; 659 fun extend _ = empty; 660 fun merge _ = empty; 661); 662 663fun register_proofs ths = 664 (Proofs.map o cons) (Lazy.map_finished (map Thm.trim_context) ths); 665 666fun force_proofs thy = rev (Proofs.get thy) |> maps (map (Thm.transfer thy) o Lazy.force); 667 668val consolidate_theory = Thm.consolidate o force_proofs; 669 670fun expose_theory thy = 671 if Proofterm.export_enabled () 672 then Thm.expose_proofs thy (force_proofs thy) else (); 673 674 675 676(** print theorems **) 677 678(* options *) 679 680val show_consts = Config.declare_option_bool ("show_consts", \<^here>); 681val show_hyps = Config.declare_bool ("show_hyps", \<^here>) (K false); 682val show_tags = Config.declare_bool ("show_tags", \<^here>) (K false); 683 684 685(* pretty_thm etc. *) 686 687fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; 688val pretty_tags = Pretty.list "[" "]" o map pretty_tag; 689 690fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = 691 let 692 val show_tags = Config.get ctxt show_tags; 693 val show_hyps = Config.get ctxt show_hyps; 694 695 val th = raw_th 696 |> perhaps (try (Thm.transfer' ctxt)) 697 |> perhaps (try Thm.strip_shyps); 698 699 val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th; 700 val extra_shyps = extra_shyps' ctxt th; 701 val tags = Thm.get_tags th; 702 val tpairs = Thm.tpairs_of th; 703 704 val q = if quote then Pretty.quote else I; 705 val prt_term = q o Syntax.pretty_term ctxt; 706 707 708 val hlen = length extra_shyps + length hyps + length tpairs; 709 val hsymbs = 710 if hlen = 0 then [] 711 else if show_hyps orelse show_hyps' then 712 [Pretty.brk 2, Pretty.list "[" "]" 713 (map (q o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @ 714 map (Syntax.pretty_sort ctxt) extra_shyps)] 715 else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; 716 val tsymbs = 717 if null tags orelse not show_tags then [] 718 else [Pretty.brk 1, pretty_tags tags]; 719 in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; 720 721fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; 722fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; 723 724fun pretty_thm_global thy = 725 pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; 726 727val string_of_thm = Pretty.string_of oo pretty_thm; 728val string_of_thm_global = Pretty.string_of oo pretty_thm_global; 729 730 731open Thm; 732 733end; 734 735structure Basic_Thm: BASIC_THM = Thm; 736open Basic_Thm; 737