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