# HG changeset patch
# User wenzelm
# Date 916144761 -3600
# Node ID 4d2d5556b4f9357781d5184e50f35e1a473315a9
# Parent  bb60ec0bcd741e3c1cc21594c6e3ee0adefa0711
signature BASIC_THM;
theorem / axiom deriv: added tags;
get/put_name_tags;
type attribute;

diff -r bb60ec0bcd74 -r 4d2d5556b4f9 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Jan 12 13:37:40 1999 +0100
+++ b/src/Pure/thm.ML	Tue Jan 12 13:39:21 1999 +0100
@@ -7,7 +7,7 @@
 theorems, meta rules (including resolution and simplification).
 *)
 
-signature THM =
+signature BASIC_THM =
   sig
   (*certified types*)
   type ctyp
@@ -41,12 +41,13 @@
 
   (*proof terms [must DUPLICATE declaration as a specification]*)
   datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
+  type tag		(* = string * string list *)
   val keep_derivs       : deriv_kind ref
   datatype rule = 
       MinProof                          
     | Oracle		  of string * Sign.sg * Object.T
-    | Axiom               of string
-    | Theorem             of string       
+    | Axiom               of string * tag list
+    | Theorem             of string * tag list
     | Assume              of cterm
     | Implies_intr        of cterm
     | Implies_intr_shyps
@@ -77,18 +78,18 @@
     | CongC               of cterm
     | Rewrite_cterm       of cterm
     | Rename_params_rule  of string list * int;
-
-  type deriv   (* = rule mtree *)
+  type deriv	(* = rule mtree *)
 
   (*meta theorems*)
   type thm
-  exception THM of string * int * thm list
   val rep_thm           : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
                                   shyps: sort list, hyps: term list, 
                                   prop: term}
   val crep_thm          : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
                                   shyps: sort list, hyps: cterm list, 
                                   prop: cterm}
+  exception THM of string * int * thm list
+  type 'a attribute 	(* = 'a * thm -> 'a * thm *)
   val eq_thm		: thm * thm -> bool
   val sign_of_thm       : thm -> Sign.sg
   val transfer_sg	: Sign.sg -> thm -> thm
@@ -104,8 +105,6 @@
   val implies_intr_shyps: thm -> thm
   val get_axiom         : theory -> xstring -> thm
   val get_def           : theory -> xstring -> thm
-  val name_thm          : string * thm -> thm
-  val name_of_thm	: thm -> string
   val axioms_of         : theory -> (string * thm) list
 
   (*meta rules*)
@@ -175,6 +174,19 @@
   val invoke_oracle     : theory -> xstring -> Sign.sg * Object.T -> thm
 end;
 
+signature THM =
+sig
+  include BASIC_THM
+  val no_attributes	: 'a -> 'a * 'b attribute list
+  val apply_attributes	: ('a * thm) * 'a attribute list -> ('a * thm)
+  val applys_attributes	: ('a * thm list) * 'a attribute list -> ('a * thm list)
+  val get_name_tags	: thm -> string * tag list
+  val put_name_tags	: string * tag list -> thm -> thm
+  val name_of_thm	: thm -> string
+  val tags_of_thm	: thm -> tag list
+  val name_thm		: string * thm -> thm
+end;
+
 structure Thm: THM =
 struct
 
@@ -294,14 +306,17 @@
 
 (*** Derivations ***)
 
+(*tags provide additional comment, apart from the axiom/theorem name*)
+type tag = string * string list;
+
 (*Names of rules in derivations.  Includes logically trivial rules, if 
   executed in ML.*)
 datatype rule = 
     MinProof                            (*for building minimal proof terms*)
   | Oracle              of string * Sign.sg * Object.T       (*oracles*)
 (*Axioms/theorems*)
-  | Axiom               of string
-  | Theorem             of string
+  | Axiom               of string * tag list
+  | Theorem             of string * tag list
 (*primitive inferences and compound versions of them*)
   | Assume              of cterm
   | Implies_intr        of cterm
@@ -404,6 +419,13 @@
 (*errors involving theorems*)
 exception THM of string * int * thm list;
 
+(*attributes subsume any kind of rules or addXXXs modifiers*)
+type 'a attribute = 'a * thm -> 'a * thm;
+
+fun no_attributes x = (x, []);
+fun apply_attributes (x_th, atts) = Library.apply atts x_th;
+fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths;
+
 (*equality of theorems uses equality of signatures and the
   a-convertible test for terms*)
 fun eq_thm (th1, th2) =
@@ -584,7 +606,7 @@
               Some t =>
                 Some (fix_shyps [] []
                   (Thm {sign_ref = Sign.self_ref sign,
-                    der = infer_derivs (Axiom name, []),
+                    der = infer_derivs (Axiom (name, []), []),
                     maxidx = maxidx_of_term t,
                     shyps = [], 
                     hyps = [], 
@@ -605,19 +627,31 @@
   map (fn (s, _) => (s, get_axiom thy s))
     (Symtab.dest (#axioms (rep_theory thy)));
 
-(*Attach a label to a theorem to make proof objects more readable*)
-fun name_thm (name, th as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
+
+(* name and tags -- make proof objects more readable *)
+
+fun get_name_tags (Thm {der, ...}) =
   (case der of
-    Join (Theorem _, _) => th
-  | Join (Axiom _, _) => th
-  | _ => Thm {sign_ref = sign_ref, der = Join (Theorem name, [der]),
-      maxidx = maxidx, shyps = shyps, hyps = hyps, prop = prop});
+    Join (Theorem x, _) => x
+  | Join (Axiom x, _) => x
+  | _ => ("", []));
 
-fun name_of_thm (Thm {der, ...}) =
-  (case der of
-    Join (Theorem name, _) => name
-  | Join (Axiom name, _) => name
-  | _ => "");
+fun put_name_tags x (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
+  let
+    val der' =
+      (case der of
+        Join (Theorem _, ds) => Join (Theorem x, ds)
+      | Join (Axiom _, ds) => Join (Axiom x, ds)
+      | _ => Join (Theorem x, [der]));
+  in
+    Thm {sign_ref = sign_ref, der = der', maxidx = maxidx,
+      shyps = shyps, hyps = hyps, prop = prop}
+  end;
+
+val name_of_thm = #1 o get_name_tags;
+val tags_of_thm = #2 o get_name_tags;
+
+fun name_thm (name, thm) = put_name_tags (name, tags_of_thm thm) thm;
 
 
 (*Compression of theorems -- a separate rule, not integrated with the others,
@@ -2289,4 +2323,6 @@
 
 end;
 
-open Thm;
+
+structure BasicThm: BASIC_THM = Thm;
+open BasicThm;