# HG changeset patch # User wenzelm # Date 1218725571 -7200 # Node ID c721ea6e0eb45691c7b9bb632f42b0b1afc49c6a # Parent 27a8ad9612a31ef88cc403eb63ecdb6d0ecaf4ce moved basic thm operations from structure PureThy to Thm; added position operations; tuned; diff -r 27a8ad9612a3 -r c721ea6e0eb4 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Aug 14 16:52:46 2008 +0200 +++ b/src/Pure/more_thm.ML Thu Aug 14 16:52:51 2008 +0200 @@ -33,6 +33,32 @@ val add_thm: thm -> thm list -> thm list val del_thm: thm -> thm list -> thm list val merge_thms: thm list * thm list -> thm list + val elim_implies: thm -> thm -> thm + val forall_elim_var: int -> thm -> thm + val forall_elim_vars: int -> thm -> thm + val unvarify: thm -> thm + val close_derivation: thm -> thm + val add_axiom: term list -> bstring * term -> theory -> thm * theory + val add_def: bool -> bool -> bstring * term -> theory -> thm * theory + val rule_attribute: (Context.generic -> thm -> thm) -> attribute + val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute + val theory_attributes: attribute list -> theory * thm -> theory * thm + val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm + val no_attributes: 'a -> 'a * 'b list + val simple_fact: 'a -> ('a * 'b list) list + val tag_rule: Markup.property -> thm -> thm + val untag_rule: string -> thm -> thm + val tag: Markup.property -> attribute + val untag: string -> attribute + val position_of: thm -> Position.T + val default_position: Position.T -> thm -> thm + val default_position_of: thm -> thm -> thm + val has_name_hint: thm -> bool + val get_name_hint: thm -> string + val put_name_hint: string -> thm -> thm + val get_group: thm -> string option + val put_group: string -> thm -> thm + val group: string -> attribute val axiomK: string val assumptionK: string val definitionK: string @@ -40,19 +66,13 @@ val lemmaK: string val corollaryK: string val internalK: string - val rule_attribute: (Context.generic -> thm -> thm) -> attribute - val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute - val theory_attributes: attribute list -> theory * thm -> theory * thm - val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm - val no_attributes: 'a -> 'a * 'b list - val simple_fact: 'a -> ('a * 'b list) list - val elim_implies: thm -> thm -> thm - val forall_elim_var: int -> thm -> thm - val forall_elim_vars: int -> thm -> thm - val unvarify: thm -> thm - val close_derivation: thm -> thm - val add_axiom: term list -> bstring * term -> theory -> thm * theory - val add_def: bool -> bool -> bstring * term -> theory -> thm * theory + val has_kind: thm -> bool + val get_kind: thm -> string + val kind_rule: string -> thm -> thm + val kind: string -> attribute + val kind_internal: attribute + val has_internal: Markup.property list -> bool + val is_internal: thm -> bool end; structure Thm: THM = @@ -175,37 +195,6 @@ -(** theorem kinds **) - -val axiomK = "axiom"; -val assumptionK = "assumption"; -val definitionK = "definition"; -val theoremK = "theorem"; -val lemmaK = "lemma"; -val corollaryK = "corollary"; -val internalK = Markup.internalK; - - - -(** attributes **) - -fun rule_attribute f (x, th) = (x, f x th); -fun declaration_attribute f (x, th) = (f th x, th); - -fun apply_attributes mk dest = - let - fun app [] = I - | app ((f: attribute) :: fs) = fn (x, th) => f (mk x, th) |>> dest |> app fs; - in app end; - -val theory_attributes = apply_attributes Context.Theory Context.the_theory; -val proof_attributes = apply_attributes Context.Proof Context.the_proof; - -fun no_attributes x = (x, []); -fun simple_fact x = [(x, [])]; - - - (** basic derived rules **) (*Elimination of implication @@ -296,6 +285,88 @@ val thm = unvarify (Thm.instantiate (recover_sorts, []) axm'); in (thm, thy') end; + + +(** attributes **) + +fun rule_attribute f (x, th) = (x, f x th); +fun declaration_attribute f (x, th) = (f th x, th); + +fun apply_attributes mk dest = + let + fun app [] = I + | app ((f: attribute) :: fs) = fn (x, th) => f (mk x, th) |>> dest |> app fs; + in app end; + +val theory_attributes = apply_attributes Context.Theory Context.the_theory; +val proof_attributes = apply_attributes Context.Proof Context.the_proof; + +fun no_attributes x = (x, []); +fun simple_fact x = [(x, [])]; + + + +(*** theorem tags ***) + +(* add / delete tags *) + +fun tag_rule tg = Thm.map_tags (insert (op =) tg); +fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); + +fun tag tg x = rule_attribute (K (tag_rule tg)) x; +fun untag s x = rule_attribute (K (untag_rule s)) x; + + +(* position *) + +val position_of = Position.of_properties o Thm.get_tags; + +fun default_position pos = Thm.map_tags (Position.default_properties pos); +val default_position_of = default_position o position_of; + + +(* unofficial theorem names *) + +fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); + +val has_name_hint = can the_name_hint; +val get_name_hint = the_default "??.unknown" o try the_name_hint; + +fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); + + +(* theorem groups *) + +fun get_group thm = AList.lookup (op =) (Thm.get_tags thm) Markup.groupN; + +fun put_group name = + if name = "" then I else Thm.map_tags (AList.update (op =) (Markup.groupN, name)); + +fun group name = rule_attribute (K (put_group name)); + + +(* theorem kinds *) + +val axiomK = "axiom"; +val assumptionK = "assumption"; +val definitionK = "definition"; +val theoremK = "theorem"; +val lemmaK = "lemma"; +val corollaryK = "corollary"; +val internalK = Markup.internalK; + +fun the_kind thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.kindN); + +val has_kind = can the_kind; +val get_kind = the_default "" o try the_kind; + +fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; +fun kind k x = if k = "" then x else rule_attribute (K (kind_rule k)) x; +fun kind_internal x = kind internalK x; +fun has_internal tags = exists (fn tg => tg = (Markup.kindN, internalK)) tags; +val is_internal = has_internal o Thm.get_tags; + + open Thm; end;