Registrations of global locale interpretations: improved, better naming.

--- a/etc/isar-keywords-ZF.el	Thu Mar 10 09:11:57 2005 +0100
+++ b/etc/isar-keywords-ZF.el	Thu Mar 10 17:48:36 2005 +0100
@@ -74,6 +74,7 @@
     "init_toplevel"
     "instance"
     "instantiate"
+    "interpretation"
     "judgment"
     "kill"
     "kill_thy"
@@ -109,11 +110,11 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
+    "print_interps"
     "print_intros"
     "print_locale"
     "print_locales"
     "print_methods"
-    "print_registrations"
     "print_rules"
     "print_simpset"
     "print_syntax"
@@ -132,7 +133,6 @@
     "realizability"
     "realizers"
     "redo"
-    "registration"
     "remove_thy"
     "rep_datatype"
     "sect"
@@ -261,11 +261,11 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
+    "print_interps"
     "print_intros"
     "print_locale"
     "print_locales"
     "print_methods"
-    "print_registrations"
     "print_rules"
     "print_simpset"
     "print_syntax"
@@ -364,8 +364,8 @@
 (defconst isar-keywords-theory-goal
   '("corollary"
     "instance"
+    "interpretation"
     "lemma"
-    "registration"
     "theorem"))
 
 (defconst isar-keywords-qed

--- a/etc/isar-keywords.el	Thu Mar 10 09:11:57 2005 +0100
+++ b/etc/isar-keywords.el	Thu Mar 10 17:48:36 2005 +0100
@@ -77,6 +77,7 @@
     "init_toplevel"
     "instance"
     "instantiate"
+    "interpretation"
     "judgment"
     "kill"
     "kill_thy"
@@ -112,11 +113,11 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
+    "print_interps"
     "print_intros"
     "print_locale"
     "print_locales"
     "print_methods"
-    "print_registrations"
     "print_rules"
     "print_simpset"
     "print_syntax"
@@ -137,7 +138,6 @@
     "recdef_tc"
     "record"
     "redo"
-    "registration"
     "refute"
     "refute_params"
     "remove_thy"
@@ -286,11 +286,11 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
+    "print_interps"
     "print_intros"
     "print_locale"
     "print_locales"
     "print_methods"
-    "print_registrations"
     "print_rules"
     "print_simpset"
     "print_syntax"
@@ -395,9 +395,9 @@
   '("ax_specification"
     "corollary"
     "instance"
+    "interpretation"
     "lemma"
     "recdef_tc"
-    "registration"
     "specification"
     "theorem"
     "typedef"))

--- a/src/FOL/ex/LocaleTest.thy	Thu Mar 10 09:11:57 2005 +0100
+++ b/src/FOL/ex/LocaleTest.thy	Thu Mar 10 17:48:36 2005 +0100
@@ -10,19 +10,19 @@
 
 theory LocaleTest = FOL:
 
-(* registration input syntax *)
+(* interpretation input syntax *)
 
 locale L
 locale M = fixes a and b and c
 
-registration test [simp]: L + M a b c [x y z] .
+interpretation test [simp]: L + M a b c [x y z] .
 
-print_registrations L
-print_registrations M
+print_interps L
+print_interps M
 
-registration test [simp]: L .
+interpretation test [simp]: L .
 
-registration L .
+interpretation L .
 
 (* processing of locale expression *)
 
@@ -44,33 +44,47 @@
 
 ML {* set Toplevel.debug *}
 
-registration p1: C ["X::'b" "Y"] by (auto intro: A.intro C_axioms.intro)
+ML {* set show_hyps *}
+
+interpretation p1: C ["X::'b" "Y::'b"] by (auto intro: A.intro C_axioms.intro)
   (* both X and Y get type 'b since 'b is the internal type of parameter b,
      not wanted, but put up with for now. *)
 
-ML {* set show_hyps *}
-
-print_registrations A
-
-(* thm asm_A a.asm_A p1.a.asm_A *)
+print_interps A
 
 (*
-registration p2: D [X Y Z] sorry
+thm asm_A a.asm_A p1.a.asm_A
+*)
+
+interpretation p2: D [X Y "Y = X"] by (auto intro: A.intro simp: eq_commute)
 
-print_registrations D
+print_interps D
+
+(*
+thm p2.a.asm_A
 *)
 
-registration p3: D [X Y] by (auto intro: A.intro)
+interpretation p3: D [X Y] by (auto intro: A.intro)
+
+(* duplicate: not registered *)
+(*
+thm p3.a.asm_A
+*)
 
-print_registrations A
-print_registrations B
-print_registrations C
-print_registrations D
+print_interps A
+print_interps B
+print_interps C
+print_interps D
 
-(* not permitted
-registration p4: A ["?x10"] apply (rule A.intro) apply rule done
+(* not permitted *)
+(*
+interpretation p4: A ["x::?'a1"] apply (rule A.intro) apply rule done
+*)
+print_interps A
 
-print_registrations A
+(* without a prefix *)
+(* TODO!!!
+interpretation A [Z] apply - apply (auto intro: A.intro) done
 *)
 
 end

--- a/src/Pure/Isar/isar_syn.ML	Thu Mar 10 09:11:57 2005 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 10 17:48:36 2005 +0100
@@ -315,9 +315,9 @@
 val view_val =
   Scan.optional (P.$$$ "[" |-- Scan.repeat1 uterm --| P.$$$ "]") [];
 
-val registrationP =
-  OuterSyntax.command "registration"
-  "prove and register instance of locale expression" K.thy_goal
+val interpretationP =
+  OuterSyntax.command "interpretation"
+  "prove and register interpretation of locale expression" K.thy_goal
   ((P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val
      >> IsarThy.register_globally)
    >> (Toplevel.print oo Toplevel.theory_to_proof));
@@ -594,8 +594,8 @@
     (locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
 
 val print_registrationsP =
-  OuterSyntax.improper_command "print_registrations"
-    "print registrations of named locale in this theory" K.diag
+  OuterSyntax.improper_command "print_interps"
+    "print interpretations of named locale in this theory" K.diag
     (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
 
 val print_attributesP =
@@ -800,7 +800,7 @@
   default_proofP, immediate_proofP, done_proofP, skip_proofP,
   forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
   finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,
-  redoP, undos_proofP, undoP, killP, registrationP, instantiateP,
+  redoP, undos_proofP, undoP, killP, interpretationP, instantiateP,
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   print_syntaxP, print_theoremsP, print_localesP, print_localeP,

--- a/src/Pure/Isar/isar_thy.ML	Thu Mar 10 09:11:57 2005 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Thu Mar 10 17:48:36 2005 +0100
@@ -625,21 +625,20 @@
 val context = init_context (ThyInfo.quiet_update_thy true);
 
 
-(* global locale registration *)
+(* global registration of locale interpretation *)
 
 fun register_globally (((prfx, atts), expr), insts) b (* bool *) thy =
   let
-    val (thy', propss, activate) =
-          Locale.prep_registration (prfx, []) expr insts thy;
-(* TODO: convert atts *)
-    fun register id (thy, thm) = let
+    val (thy', propss, activate) = Locale.prep_registration
+          (prfx, map (Attrib.global_attribute thy) atts) expr insts thy;
+    fun witness id (thy, thm) = let
         val thm' = Drule.freeze_all thm;
       in
-        (Locale.global_activate_thm id thm' thy, thm')
+        (Locale.global_add_witness id thm' thy, thm')
       end;
   in
     multi_theorem_i Drule.internalK activate ("", []) [] 
-      (map (fn (id as (n, _), props) => ((NameSpace.base n, [register id]), 
+      (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]), 
         map (fn prop => (prop, ([], []))) props)) propss) b thy'
   end;
 

--- a/src/Pure/Isar/locale.ML	Thu Mar 10 09:11:57 2005 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Mar 10 17:48:36 2005 +0100
@@ -90,7 +90,7 @@
   val prep_registration:
     string * theory attribute list -> expr -> string option list -> theory ->
     theory * ((string * term list) * term list) list * (theory -> theory)
-  val global_activate_thm:
+  val global_add_witness:
     string * term list -> thm -> theory -> theory
 
   val setup: (theory -> theory) list
@@ -218,10 +218,10 @@
           regs)
       end handle Termlisttab.DUP _ => regs));
 
-(* add theorem to registration in theory,
+(* add witness theorem to registration in theory,
    ignored if registration not present *)
 
-fun global_put_registration_thm (name, ps) thm =
+fun global_add_witness (name, ps) thm =
   LocalesData.map (fn (space, locs, regs) =>
     (space, locs, let
         val tab = valOf (Symtab.lookup (regs, name));
@@ -271,8 +271,8 @@
     val loc_regs = Symtab.lookup (regs, loc_int);
   in
     (case loc_regs of
-        NONE => Pretty.str "No registrations."
-      | SOME r => Pretty.big_list "registrations:"
+        NONE => Pretty.str "No interpretations."
+      | SOME r => Pretty.big_list "interpretations:"
           (map prt_inst (Termlisttab.dest r)))
     |> Pretty.writeln
   end;
@@ -1610,7 +1610,7 @@
 
 
 
-(** Registration commands **)
+(** Interpretation commands **)
 
 local
 
@@ -1761,10 +1761,12 @@
       let
         (* extract theory attributes *)
         val (Notes facts) = map_attrib_element_i fst (Notes facts);
+        (* add attributs from registration *)
         val facts' = map (apfst (apsnd (fn a => a @ atts))) facts;
-        val facts'' = map (apsnd (map (apfst (map disch)))) facts';
+        (* discharge hyps and varify *)
+        val facts'' = map (apsnd (map (apfst (map (Drule.standard o disch))))) facts';
       in
-        fst (note_thmss_qualified' "" prfx facts thy)
+        fst (note_thmss_qualified' "" prfx facts'' thy)
       end;
 
 fun activate_facts_elems disch (thy, (id, elems)) =
@@ -1782,9 +1784,8 @@
               Option.map snd (global_get_registration thy id)
                 handle Option => error ("(internal) unknown registration of " ^
                   quote (fst id) ^ " while activating facts.")) all_elemss);
-        fun disch thm = let
-          in Drule.satisfy_hyps prems thm end;
-      in Library.foldl (activate_facts_elems disch) (thy, new_elemss) end;
+      in Library.foldl (activate_facts_elems (Drule.satisfy_hyps prems))
+        (thy, new_elemss) end;
 
 in
 
@@ -1803,23 +1804,34 @@
 
     (** compute instantiation **)
 
-    (* user input *)
+    (* check user input *)
     val insts = if length parms < length insts
          then error "More arguments than parameters in instantiation."
          else insts @ replicate (length parms - length insts) NONE;
+
     val (ps, pTs) = split_list parms;
     val pvTs = map Type.varifyT pTs;
+
+    (* instantiations given by user *)
     val given = List.mapPartial (fn (_, (NONE, _)) => NONE
          | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs));
     val (given_ps, given_insts) = split_list given;
     val tvars = foldr Term.add_typ_tvars [] pvTs;
     val used = foldr Term.add_typ_varnames [] pvTs;
     fun sorts (a, i) = assoc (tvars, (a, i));
-    val (tvs, tvinst) = Sign.read_def_terms (sign, K NONE, sorts) used true
+    val (vs, vinst) = Sign.read_def_terms (sign, K NONE, sorts) used true
          given_insts;
-    val tinst = Symtab.make (map (fn ((x, 0), T) => (x, Type.unvarifyT T)
-                  | ((_, n), _) => error "Var in prep_registration") tvinst);
-    val inst = Symtab.make (given_ps ~~ map Logic.unvarify tvs);
+    (* replace new types (which are TFrees) by ones with new names *)
+    val new_Tnames = foldr Term.add_term_tfree_names [] vs;
+    val new_Tnames' = Term.invent_names used "'a" (length new_Tnames);
+    val renameT = Term.map_type_tfree (fn (a, s) =>
+          TFree (valOf (assoc (new_Tnames ~~ new_Tnames', a)), s));
+    val rename = Term.map_term_types renameT;
+
+    val tinst = Symtab.make (map
+                (fn ((x, 0), T) => (x, T |> renameT |> Type.unvarifyT)
+                  | ((_, n), _) => error "Var in prep_registration") vinst);
+    val inst = Symtab.make (given_ps ~~ map (Logic.unvarify o rename) vs);
 
     (* defined params without user input *)
     val not_given = List.mapPartial (fn (x, (NONE, T)) => SOME (x, T)
@@ -1836,7 +1848,7 @@
 
     (** compute proof obligations **)
 
-    (* restore small ids *)
+    (* restore "small" ids *)
     val ids' = map (fn ((n, ps), _) =>
           (n, map (fn p => Free (p, valOf (assoc (parms, p)))) ps)) ids;
 
@@ -1846,17 +1858,10 @@
             map (fn Int e => e) elems)) 
           (ids' ~~ all_elemss);
 
-(*
-    (* varify ids, props are varified after they are proved *)
-    val inst_elemss' = map (fn ((n, ps), elems) =>
-          ((n, map Logic.varify ps), elems)) inst_elemss;
-*)
-
     (* remove fragments already registered with theory *)
     val new_inst_elemss = List.filter (fn (id, _) =>
           is_none (global_get_registration thy id)) inst_elemss;
 
-
     val propss = extract_asms_elemss new_inst_elemss;
 
 
@@ -1867,11 +1872,6 @@
 
   in (thy', propss, activate_facts_elemss inst_elemss new_inst_elemss) end;
 
-
-(* Add registrations and theorems to theory context *)
-
-val global_activate_thm = global_put_registration_thm
-
 end;  (* local *)
 
 

--- a/src/Pure/Isar/toplevel.ML	Thu Mar 10 09:11:57 2005 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Mar 10 17:48:36 2005 +0100
@@ -471,6 +471,8 @@
   | exn_message (THM (msg, i, thms)) = msg_on_debug (THM (msg, i, thms))
   | exn_message Option = raised "Option"
   | exn_message UnequalLengths = raised "UnequalLengths"
+  | exn_message Empty = raised "Empty"
+  | exn_message Subscript = raised "Subscript"
   | exn_message exn = General.exnMessage exn
 and fail_message kind ((name, pos), exn) =
   "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_message exn;

--- a/src/Pure/term.ML	Thu Mar 10 09:11:57 2005 +0100
+++ b/src/Pure/term.ML	Thu Mar 10 17:48:36 2005 +0100
@@ -133,6 +133,7 @@
   val maxidx_of_terms: term list -> int
   val variant: string list -> string -> string
   val variantlist: string list * string list -> string list
+        (* note reversed order of args wrt. variant! *)
   val variant_abs: string * typ * term -> string * term
   val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
   val add_new_id: string list * string -> string list