82 val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory |
82 val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory |
83 val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory |
83 val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory |
84 type attribute = Context.generic * thm -> Context.generic option * thm option |
84 type attribute = Context.generic * thm -> Context.generic option * thm option |
85 type binding = binding * attribute list |
85 type binding = binding * attribute list |
86 val empty_binding: binding |
86 val empty_binding: binding |
87 val rule_attribute: (Context.generic -> thm -> thm) -> attribute |
|
88 val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute |
|
89 val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute |
|
90 val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic |
|
91 val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic |
|
92 val theory_attributes: attribute list -> thm -> theory -> thm * theory |
|
93 val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context |
|
94 val no_attributes: 'a -> 'a * 'b list |
|
95 val simple_fact: 'a -> ('a * 'b list) list |
|
96 val tag_rule: string * string -> thm -> thm |
87 val tag_rule: string * string -> thm -> thm |
97 val untag_rule: string -> thm -> thm |
88 val untag_rule: string -> thm -> thm |
98 val tag: string * string -> attribute |
|
99 val untag: string -> attribute |
|
100 val is_free_dummy: thm -> bool |
89 val is_free_dummy: thm -> bool |
101 val tag_free_dummy: thm -> thm |
90 val tag_free_dummy: thm -> thm |
102 val def_name: string -> string |
91 val def_name: string -> string |
103 val def_name_optional: string -> string -> string |
92 val def_name_optional: string -> string -> string |
104 val def_binding: Binding.binding -> Binding.binding |
93 val def_binding: Binding.binding -> Binding.binding |
107 val get_name_hint: thm -> string |
96 val get_name_hint: thm -> string |
108 val put_name_hint: string -> thm -> thm |
97 val put_name_hint: string -> thm -> thm |
109 val theoremK: string |
98 val theoremK: string |
110 val legacy_get_kind: thm -> string |
99 val legacy_get_kind: thm -> string |
111 val kind_rule: string -> thm -> thm |
100 val kind_rule: string -> thm -> thm |
|
101 val rule_attribute: thm list -> (Context.generic -> thm -> thm) -> attribute |
|
102 val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute |
|
103 val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute |
|
104 val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic |
|
105 val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic |
|
106 val theory_attributes: attribute list -> thm -> theory -> thm * theory |
|
107 val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context |
|
108 val no_attributes: 'a -> 'a * 'b list |
|
109 val simple_fact: 'a -> ('a * 'b list) list |
|
110 val tag: string * string -> attribute |
|
111 val untag: string -> attribute |
112 val kind: string -> attribute |
112 val kind: string -> attribute |
113 val register_proofs: thm list -> theory -> theory |
113 val register_proofs: thm list -> theory -> theory |
114 val join_theory_proofs: theory -> unit |
114 val join_theory_proofs: theory -> unit |
115 val show_consts_raw: Config.raw |
115 val show_consts_raw: Config.raw |
116 val show_consts: bool Config.T |
116 val show_consts: bool Config.T |
541 fun add_def_global unchecked overloaded arg thy = |
541 fun add_def_global unchecked overloaded arg thy = |
542 add_def (Defs.global_context thy) unchecked overloaded arg thy; |
542 add_def (Defs.global_context thy) unchecked overloaded arg thy; |
543 |
543 |
544 |
544 |
545 |
545 |
|
546 (*** theorem tags ***) |
|
547 |
|
548 (* add / delete tags *) |
|
549 |
|
550 fun tag_rule tg = Thm.map_tags (insert (op =) tg); |
|
551 fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); |
|
552 |
|
553 |
|
554 (* free dummy thm -- for abstract closure *) |
|
555 |
|
556 val free_dummyN = "free_dummy"; |
|
557 fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN; |
|
558 val tag_free_dummy = tag_rule (free_dummyN, ""); |
|
559 |
|
560 |
|
561 (* def_name *) |
|
562 |
|
563 fun def_name c = c ^ "_def"; |
|
564 |
|
565 fun def_name_optional c "" = def_name c |
|
566 | def_name_optional _ name = name; |
|
567 |
|
568 val def_binding = Binding.map_name def_name; |
|
569 |
|
570 fun def_binding_optional b name = |
|
571 if Binding.is_empty name then def_binding b else name; |
|
572 |
|
573 |
|
574 (* unofficial theorem names *) |
|
575 |
|
576 fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); |
|
577 |
|
578 val has_name_hint = can the_name_hint; |
|
579 val get_name_hint = the_default "??.unknown" o try the_name_hint; |
|
580 |
|
581 fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); |
|
582 |
|
583 |
|
584 (* theorem kinds *) |
|
585 |
|
586 val theoremK = "theorem"; |
|
587 |
|
588 fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN); |
|
589 |
|
590 fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; |
|
591 |
|
592 |
|
593 |
546 (** attributes **) |
594 (** attributes **) |
547 |
595 |
548 (*attributes subsume any kind of rules or context modifiers*) |
596 (*attributes subsume any kind of rules or context modifiers*) |
549 type attribute = Context.generic * thm -> Context.generic option * thm option; |
597 type attribute = Context.generic * thm -> Context.generic option * thm option; |
550 |
598 |
551 type binding = binding * attribute list; |
599 type binding = binding * attribute list; |
552 val empty_binding: binding = (Binding.empty, []); |
600 val empty_binding: binding = (Binding.empty, []); |
553 |
601 |
554 fun rule_attribute f (x, th) = (NONE, SOME (f x th)); |
602 fun rule_attribute ths f (x, th) = |
555 fun declaration_attribute f (x, th) = (SOME (f th x), NONE); |
603 (NONE, |
556 fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end; |
604 (case find_first is_free_dummy (th :: ths) of |
|
605 SOME th' => SOME th' |
|
606 | NONE => SOME (f x th))); |
|
607 |
|
608 fun declaration_attribute f (x, th) = |
|
609 (if is_free_dummy th then NONE else SOME (f th x), NONE); |
|
610 |
|
611 fun mixed_attribute f (x, th) = |
|
612 let val (x', th') = f (x, th) in (SOME x', SOME th') end; |
557 |
613 |
558 fun apply_attribute (att: attribute) th x = |
614 fun apply_attribute (att: attribute) th x = |
559 let val (x', th') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th)) |
615 let val (x', th') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th)) |
560 in (the_default th th', the_default x x') end; |
616 in (the_default th th', the_default x x') end; |
561 |
617 |
571 val proof_attributes = apply_attributes Context.Proof Context.the_proof; |
627 val proof_attributes = apply_attributes Context.Proof Context.the_proof; |
572 |
628 |
573 fun no_attributes x = (x, []); |
629 fun no_attributes x = (x, []); |
574 fun simple_fact x = [(x, [])]; |
630 fun simple_fact x = [(x, [])]; |
575 |
631 |
576 |
632 fun tag tg = rule_attribute [] (K (tag_rule tg)); |
577 |
633 fun untag s = rule_attribute [] (K (untag_rule s)); |
578 (*** theorem tags ***) |
634 fun kind k = rule_attribute [] (K (k <> "" ? kind_rule k)); |
579 |
|
580 (* add / delete tags *) |
|
581 |
|
582 fun tag_rule tg = Thm.map_tags (insert (op =) tg); |
|
583 fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); |
|
584 |
|
585 fun tag tg = rule_attribute (K (tag_rule tg)); |
|
586 fun untag s = rule_attribute (K (untag_rule s)); |
|
587 |
|
588 |
|
589 (* free dummy thm -- for abstract closure *) |
|
590 |
|
591 val free_dummyN = "free_dummy"; |
|
592 fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN; |
|
593 val tag_free_dummy = tag_rule (free_dummyN, ""); |
|
594 |
|
595 |
|
596 (* def_name *) |
|
597 |
|
598 fun def_name c = c ^ "_def"; |
|
599 |
|
600 fun def_name_optional c "" = def_name c |
|
601 | def_name_optional _ name = name; |
|
602 |
|
603 val def_binding = Binding.map_name def_name; |
|
604 |
|
605 fun def_binding_optional b name = |
|
606 if Binding.is_empty name then def_binding b else name; |
|
607 |
|
608 |
|
609 (* unofficial theorem names *) |
|
610 |
|
611 fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); |
|
612 |
|
613 val has_name_hint = can the_name_hint; |
|
614 val get_name_hint = the_default "??.unknown" o try the_name_hint; |
|
615 |
|
616 fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); |
|
617 |
|
618 |
|
619 (* theorem kinds *) |
|
620 |
|
621 val theoremK = "theorem"; |
|
622 |
|
623 fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN); |
|
624 |
|
625 fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; |
|
626 fun kind k = rule_attribute (K (k <> "" ? kind_rule k)); |
|
627 |
635 |
628 |
636 |
629 (* forked proofs *) |
637 (* forked proofs *) |
630 |
638 |
631 structure Proofs = Theory_Data |
639 structure Proofs = Theory_Data |