1.1 --- a/etc/isar-keywords-ZF.el	Thu Mar 10 09:11:57 2005 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Thu Mar 10 17:48:36 2005 +0100
     1.3 @@ -74,6 +74,7 @@
     1.4      "init_toplevel"
     1.5      "instance"
     1.6      "instantiate"
     1.7 +    "interpretation"
     1.8      "judgment"
     1.9      "kill"
    1.10      "kill_thy"
    1.11 @@ -109,11 +110,11 @@
    1.12      "print_drafts"
    1.13      "print_facts"
    1.14      "print_induct_rules"
    1.15 +    "print_interps"
    1.16      "print_intros"
    1.17      "print_locale"
    1.18      "print_locales"
    1.19      "print_methods"
    1.20 -    "print_registrations"
    1.21      "print_rules"
    1.22      "print_simpset"
    1.23      "print_syntax"
    1.24 @@ -132,7 +133,6 @@
    1.25      "realizability"
    1.26      "realizers"
    1.27      "redo"
    1.28 -    "registration"
    1.29      "remove_thy"
    1.30      "rep_datatype"
    1.31      "sect"
    1.32 @@ -261,11 +261,11 @@
    1.33      "print_drafts"
    1.34      "print_facts"
    1.35      "print_induct_rules"
    1.36 +    "print_interps"
    1.37      "print_intros"
    1.38      "print_locale"
    1.39      "print_locales"
    1.40      "print_methods"
    1.41 -    "print_registrations"
    1.42      "print_rules"
    1.43      "print_simpset"
    1.44      "print_syntax"
    1.45 @@ -364,8 +364,8 @@
    1.46  (defconst isar-keywords-theory-goal
    1.47    '("corollary"
    1.48      "instance"
    1.49 +    "interpretation"
    1.50      "lemma"
    1.51 -    "registration"
    1.52      "theorem"))
    1.53  
    1.54  (defconst isar-keywords-qed

     2.1 --- a/etc/isar-keywords.el	Thu Mar 10 09:11:57 2005 +0100
     2.2 +++ b/etc/isar-keywords.el	Thu Mar 10 17:48:36 2005 +0100
     2.3 @@ -77,6 +77,7 @@
     2.4      "init_toplevel"
     2.5      "instance"
     2.6      "instantiate"
     2.7 +    "interpretation"
     2.8      "judgment"
     2.9      "kill"
    2.10      "kill_thy"
    2.11 @@ -112,11 +113,11 @@
    2.12      "print_drafts"
    2.13      "print_facts"
    2.14      "print_induct_rules"
    2.15 +    "print_interps"
    2.16      "print_intros"
    2.17      "print_locale"
    2.18      "print_locales"
    2.19      "print_methods"
    2.20 -    "print_registrations"
    2.21      "print_rules"
    2.22      "print_simpset"
    2.23      "print_syntax"
    2.24 @@ -137,7 +138,6 @@
    2.25      "recdef_tc"
    2.26      "record"
    2.27      "redo"
    2.28 -    "registration"
    2.29      "refute"
    2.30      "refute_params"
    2.31      "remove_thy"
    2.32 @@ -286,11 +286,11 @@
    2.33      "print_drafts"
    2.34      "print_facts"
    2.35      "print_induct_rules"
    2.36 +    "print_interps"
    2.37      "print_intros"
    2.38      "print_locale"
    2.39      "print_locales"
    2.40      "print_methods"
    2.41 -    "print_registrations"
    2.42      "print_rules"
    2.43      "print_simpset"
    2.44      "print_syntax"
    2.45 @@ -395,9 +395,9 @@
    2.46    '("ax_specification"
    2.47      "corollary"
    2.48      "instance"
    2.49 +    "interpretation"
    2.50      "lemma"
    2.51      "recdef_tc"
    2.52 -    "registration"
    2.53      "specification"
    2.54      "theorem"
    2.55      "typedef"))

     3.1 --- a/src/FOL/ex/LocaleTest.thy	Thu Mar 10 09:11:57 2005 +0100
     3.2 +++ b/src/FOL/ex/LocaleTest.thy	Thu Mar 10 17:48:36 2005 +0100
     3.3 @@ -10,19 +10,19 @@
     3.4  
     3.5  theory LocaleTest = FOL:
     3.6  
     3.7 -(* registration input syntax *)
     3.8 +(* interpretation input syntax *)
     3.9  
    3.10  locale L
    3.11  locale M = fixes a and b and c
    3.12  
    3.13 -registration test [simp]: L + M a b c [x y z] .
    3.14 +interpretation test [simp]: L + M a b c [x y z] .
    3.15  
    3.16 -print_registrations L
    3.17 -print_registrations M
    3.18 +print_interps L
    3.19 +print_interps M
    3.20  
    3.21 -registration test [simp]: L .
    3.22 +interpretation test [simp]: L .
    3.23  
    3.24 -registration L .
    3.25 +interpretation L .
    3.26  
    3.27  (* processing of locale expression *)
    3.28  
    3.29 @@ -44,33 +44,47 @@
    3.30  
    3.31  ML {* set Toplevel.debug *}
    3.32  
    3.33 -registration p1: C ["X::'b" "Y"] by (auto intro: A.intro C_axioms.intro)
    3.34 +ML {* set show_hyps *}
    3.35 +
    3.36 +interpretation p1: C ["X::'b" "Y::'b"] by (auto intro: A.intro C_axioms.intro)
    3.37    (* both X and Y get type 'b since 'b is the internal type of parameter b,
    3.38       not wanted, but put up with for now. *)
    3.39  
    3.40 -ML {* set show_hyps *}
    3.41 -
    3.42 -print_registrations A
    3.43 -
    3.44 -(* thm asm_A a.asm_A p1.a.asm_A *)
    3.45 +print_interps A
    3.46  
    3.47  (*
    3.48 -registration p2: D [X Y Z] sorry
    3.49 -
    3.50 -print_registrations D
    3.51 +thm asm_A a.asm_A p1.a.asm_A
    3.52  *)
    3.53  
    3.54 -registration p3: D [X Y] by (auto intro: A.intro)
    3.55 +interpretation p2: D [X Y "Y = X"] by (auto intro: A.intro simp: eq_commute)
    3.56  
    3.57 -print_registrations A
    3.58 -print_registrations B
    3.59 -print_registrations C
    3.60 -print_registrations D
    3.61 +print_interps D
    3.62  
    3.63 -(* not permitted
    3.64 -registration p4: A ["?x10"] apply (rule A.intro) apply rule done
    3.65 +(*
    3.66 +thm p2.a.asm_A
    3.67 +*)
    3.68  
    3.69 -print_registrations A
    3.70 +interpretation p3: D [X Y] by (auto intro: A.intro)
    3.71 +
    3.72 +(* duplicate: not registered *)
    3.73 +(*
    3.74 +thm p3.a.asm_A
    3.75 +*)
    3.76 +
    3.77 +print_interps A
    3.78 +print_interps B
    3.79 +print_interps C
    3.80 +print_interps D
    3.81 +
    3.82 +(* not permitted *)
    3.83 +(*
    3.84 +interpretation p4: A ["x::?'a1"] apply (rule A.intro) apply rule done
    3.85 +*)
    3.86 +print_interps A
    3.87 +
    3.88 +(* without a prefix *)
    3.89 +(* TODO!!!
    3.90 +interpretation A [Z] apply - apply (auto intro: A.intro) done
    3.91  *)
    3.92  
    3.93  end

     4.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Mar 10 09:11:57 2005 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 10 17:48:36 2005 +0100
     4.3 @@ -315,9 +315,9 @@
     4.4  val view_val =
     4.5    Scan.optional (P.$$$ "[" |-- Scan.repeat1 uterm --| P.$$$ "]") [];
     4.6  
     4.7 -val registrationP =
     4.8 -  OuterSyntax.command "registration"
     4.9 -  "prove and register instance of locale expression" K.thy_goal
    4.10 +val interpretationP =
    4.11 +  OuterSyntax.command "interpretation"
    4.12 +  "prove and register interpretation of locale expression" K.thy_goal
    4.13    ((P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val
    4.14       >> IsarThy.register_globally)
    4.15     >> (Toplevel.print oo Toplevel.theory_to_proof));
    4.16 @@ -594,8 +594,8 @@
    4.17      (locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
    4.18  
    4.19  val print_registrationsP =
    4.20 -  OuterSyntax.improper_command "print_registrations"
    4.21 -    "print registrations of named locale in this theory" K.diag
    4.22 +  OuterSyntax.improper_command "print_interps"
    4.23 +    "print interpretations of named locale in this theory" K.diag
    4.24      (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
    4.25  
    4.26  val print_attributesP =
    4.27 @@ -800,7 +800,7 @@
    4.28    default_proofP, immediate_proofP, done_proofP, skip_proofP,
    4.29    forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
    4.30    finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,
    4.31 -  redoP, undos_proofP, undoP, killP, registrationP, instantiateP,
    4.32 +  redoP, undos_proofP, undoP, killP, interpretationP, instantiateP,
    4.33    (*diagnostic commands*)
    4.34    pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
    4.35    print_syntaxP, print_theoremsP, print_localesP, print_localeP,

     5.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Mar 10 09:11:57 2005 +0100
     5.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Mar 10 17:48:36 2005 +0100
     5.3 @@ -625,21 +625,20 @@
     5.4  val context = init_context (ThyInfo.quiet_update_thy true);
     5.5  
     5.6  
     5.7 -(* global locale registration *)
     5.8 +(* global registration of locale interpretation *)
     5.9  
    5.10  fun register_globally (((prfx, atts), expr), insts) b (* bool *) thy =
    5.11    let
    5.12 -    val (thy', propss, activate) =
    5.13 -          Locale.prep_registration (prfx, []) expr insts thy;
    5.14 -(* TODO: convert atts *)
    5.15 -    fun register id (thy, thm) = let
    5.16 +    val (thy', propss, activate) = Locale.prep_registration
    5.17 +          (prfx, map (Attrib.global_attribute thy) atts) expr insts thy;
    5.18 +    fun witness id (thy, thm) = let
    5.19          val thm' = Drule.freeze_all thm;
    5.20        in
    5.21 -        (Locale.global_activate_thm id thm' thy, thm')
    5.22 +        (Locale.global_add_witness id thm' thy, thm')
    5.23        end;
    5.24    in
    5.25      multi_theorem_i Drule.internalK activate ("", []) [] 
    5.26 -      (map (fn (id as (n, _), props) => ((NameSpace.base n, [register id]), 
    5.27 +      (map (fn (id as (n, _), props) => ((NameSpace.base n, [witness id]), 
    5.28          map (fn prop => (prop, ([], []))) props)) propss) b thy'
    5.29    end;
    5.30  

     6.1 --- a/src/Pure/Isar/locale.ML	Thu Mar 10 09:11:57 2005 +0100
     6.2 +++ b/src/Pure/Isar/locale.ML	Thu Mar 10 17:48:36 2005 +0100
     6.3 @@ -90,7 +90,7 @@
     6.4    val prep_registration:
     6.5      string * theory attribute list -> expr -> string option list -> theory ->
     6.6      theory * ((string * term list) * term list) list * (theory -> theory)
     6.7 -  val global_activate_thm:
     6.8 +  val global_add_witness:
     6.9      string * term list -> thm -> theory -> theory
    6.10  
    6.11    val setup: (theory -> theory) list
    6.12 @@ -218,10 +218,10 @@
    6.13            regs)
    6.14        end handle Termlisttab.DUP _ => regs));
    6.15  
    6.16 -(* add theorem to registration in theory,
    6.17 +(* add witness theorem to registration in theory,
    6.18     ignored if registration not present *)
    6.19  
    6.20 -fun global_put_registration_thm (name, ps) thm =
    6.21 +fun global_add_witness (name, ps) thm =
    6.22    LocalesData.map (fn (space, locs, regs) =>
    6.23      (space, locs, let
    6.24          val tab = valOf (Symtab.lookup (regs, name));
    6.25 @@ -271,8 +271,8 @@
    6.26      val loc_regs = Symtab.lookup (regs, loc_int);
    6.27    in
    6.28      (case loc_regs of
    6.29 -        NONE => Pretty.str "No registrations."
    6.30 -      | SOME r => Pretty.big_list "registrations:"
    6.31 +        NONE => Pretty.str "No interpretations."
    6.32 +      | SOME r => Pretty.big_list "interpretations:"
    6.33            (map prt_inst (Termlisttab.dest r)))
    6.34      |> Pretty.writeln
    6.35    end;
    6.36 @@ -1610,7 +1610,7 @@
    6.37  
    6.38  
    6.39  
    6.40 -(** Registration commands **)
    6.41 +(** Interpretation commands **)
    6.42  
    6.43  local
    6.44  
    6.45 @@ -1761,10 +1761,12 @@
    6.46        let
    6.47          (* extract theory attributes *)
    6.48          val (Notes facts) = map_attrib_element_i fst (Notes facts);
    6.49 +        (* add attributs from registration *)
    6.50          val facts' = map (apfst (apsnd (fn a => a @ atts))) facts;
    6.51 -        val facts'' = map (apsnd (map (apfst (map disch)))) facts';
    6.52 +        (* discharge hyps and varify *)
    6.53 +        val facts'' = map (apsnd (map (apfst (map (Drule.standard o disch))))) facts';
    6.54        in
    6.55 -        fst (note_thmss_qualified' "" prfx facts thy)
    6.56 +        fst (note_thmss_qualified' "" prfx facts'' thy)
    6.57        end;
    6.58  
    6.59  fun activate_facts_elems disch (thy, (id, elems)) =
    6.60 @@ -1782,9 +1784,8 @@
    6.61                Option.map snd (global_get_registration thy id)
    6.62                  handle Option => error ("(internal) unknown registration of " ^
    6.63                    quote (fst id) ^ " while activating facts.")) all_elemss);
    6.64 -        fun disch thm = let
    6.65 -          in Drule.satisfy_hyps prems thm end;
    6.66 -      in Library.foldl (activate_facts_elems disch) (thy, new_elemss) end;
    6.67 +      in Library.foldl (activate_facts_elems (Drule.satisfy_hyps prems))
    6.68 +        (thy, new_elemss) end;
    6.69  
    6.70  in
    6.71  
    6.72 @@ -1803,23 +1804,34 @@
    6.73  
    6.74      (** compute instantiation **)
    6.75  
    6.76 -    (* user input *)
    6.77 +    (* check user input *)
    6.78      val insts = if length parms < length insts
    6.79           then error "More arguments than parameters in instantiation."
    6.80           else insts @ replicate (length parms - length insts) NONE;
    6.81 +
    6.82      val (ps, pTs) = split_list parms;
    6.83      val pvTs = map Type.varifyT pTs;
    6.84 +
    6.85 +    (* instantiations given by user *)
    6.86      val given = List.mapPartial (fn (_, (NONE, _)) => NONE
    6.87           | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs));
    6.88      val (given_ps, given_insts) = split_list given;
    6.89      val tvars = foldr Term.add_typ_tvars [] pvTs;
    6.90      val used = foldr Term.add_typ_varnames [] pvTs;
    6.91      fun sorts (a, i) = assoc (tvars, (a, i));
    6.92 -    val (tvs, tvinst) = Sign.read_def_terms (sign, K NONE, sorts) used true
    6.93 +    val (vs, vinst) = Sign.read_def_terms (sign, K NONE, sorts) used true
    6.94           given_insts;
    6.95 -    val tinst = Symtab.make (map (fn ((x, 0), T) => (x, Type.unvarifyT T)
    6.96 -                  | ((_, n), _) => error "Var in prep_registration") tvinst);
    6.97 -    val inst = Symtab.make (given_ps ~~ map Logic.unvarify tvs);
    6.98 +    (* replace new types (which are TFrees) by ones with new names *)
    6.99 +    val new_Tnames = foldr Term.add_term_tfree_names [] vs;
   6.100 +    val new_Tnames' = Term.invent_names used "'a" (length new_Tnames);
   6.101 +    val renameT = Term.map_type_tfree (fn (a, s) =>
   6.102 +          TFree (valOf (assoc (new_Tnames ~~ new_Tnames', a)), s));
   6.103 +    val rename = Term.map_term_types renameT;
   6.104 +
   6.105 +    val tinst = Symtab.make (map
   6.106 +                (fn ((x, 0), T) => (x, T |> renameT |> Type.unvarifyT)
   6.107 +                  | ((_, n), _) => error "Var in prep_registration") vinst);
   6.108 +    val inst = Symtab.make (given_ps ~~ map (Logic.unvarify o rename) vs);
   6.109  
   6.110      (* defined params without user input *)
   6.111      val not_given = List.mapPartial (fn (x, (NONE, T)) => SOME (x, T)
   6.112 @@ -1836,7 +1848,7 @@
   6.113  
   6.114      (** compute proof obligations **)
   6.115  
   6.116 -    (* restore small ids *)
   6.117 +    (* restore "small" ids *)
   6.118      val ids' = map (fn ((n, ps), _) =>
   6.119            (n, map (fn p => Free (p, valOf (assoc (parms, p)))) ps)) ids;
   6.120  
   6.121 @@ -1846,17 +1858,10 @@
   6.122              map (fn Int e => e) elems)) 
   6.123            (ids' ~~ all_elemss);
   6.124  
   6.125 -(*
   6.126 -    (* varify ids, props are varified after they are proved *)
   6.127 -    val inst_elemss' = map (fn ((n, ps), elems) =>
   6.128 -          ((n, map Logic.varify ps), elems)) inst_elemss;
   6.129 -*)
   6.130 -
   6.131      (* remove fragments already registered with theory *)
   6.132      val new_inst_elemss = List.filter (fn (id, _) =>
   6.133            is_none (global_get_registration thy id)) inst_elemss;
   6.134  
   6.135 -
   6.136      val propss = extract_asms_elemss new_inst_elemss;
   6.137  
   6.138  
   6.139 @@ -1867,11 +1872,6 @@
   6.140  
   6.141    in (thy', propss, activate_facts_elemss inst_elemss new_inst_elemss) end;
   6.142  
   6.143 -
   6.144 -(* Add registrations and theorems to theory context *)
   6.145 -
   6.146 -val global_activate_thm = global_put_registration_thm
   6.147 -
   6.148  end;  (* local *)
   6.149  
   6.150  

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

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