Experimental interpretation code for definitions.
authorballarin
Fri Apr 13 10:01:43 2007 +0200 (2007-04-13)
changeset 22658263d42253f53
parent 22657 731622340817
child 22659 f792579b6e59
Experimental interpretation code for definitions.
src/Pure/Isar/element.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/spec_parse.ML
src/Pure/Tools/class_package.ML
src/Pure/Tools/invoke.ML
     1.1 --- a/src/Pure/Isar/element.ML	Fri Apr 13 10:00:04 2007 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Fri Apr 13 10:01:43 2007 +0200
     1.3 @@ -51,6 +51,7 @@
     1.4    val dest_witness: witness -> term * thm
     1.5    val transfer_witness: theory -> witness -> witness
     1.6    val refine_witness: Proof.state -> Proof.state Seq.seq
     1.7 +  val pretty_witness: Proof.context -> witness -> Pretty.T
     1.8    val rename: (string * (string * mixfix option)) list -> string -> string
     1.9    val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix
    1.10    val rename_term: (string * (string * mixfix option)) list -> term -> term
    1.11 @@ -307,6 +308,14 @@
    1.12        (PRECISE_CONJUNCTS ~1 (ALLGOALS
    1.13          (PRECISE_CONJUNCTS ~1 (TRYALL (Tactic.rtac Drule.protectI))))))))));
    1.14  
    1.15 +fun pretty_witness ctxt witn =
    1.16 +  let val prt_term = Pretty.quote o ProofContext.pretty_term ctxt
    1.17 +  in
    1.18 +    Pretty.block (prt_term (witness_prop witn) ::
    1.19 +      (if ! show_hyps then [Pretty.brk 2, Pretty.list "[" "]"
    1.20 +         (map prt_term (witness_hyps witn))] else []))
    1.21 +  end;
    1.22 +
    1.23  
    1.24  (* derived rules *)
    1.25  
     2.1 --- a/src/Pure/Isar/locale.ML	Fri Apr 13 10:00:04 2007 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Fri Apr 13 10:01:43 2007 +0200
     2.3 @@ -102,18 +102,22 @@
     2.4      Proof.context -> Proof.context
     2.5  
     2.6    val interpretation_i: (Proof.context -> Proof.context) ->
     2.7 -    (bool * string) * Attrib.src list -> expr -> typ Symtab.table * term Symtab.table ->
     2.8 +    (bool * string) * Attrib.src list -> expr ->
     2.9 +    (typ Symtab.table * term Symtab.table) * (term * term) list ->
    2.10      theory -> Proof.state
    2.11    val interpretation: (Proof.context -> Proof.context) ->
    2.12 -    (bool * string) * Attrib.src list -> expr -> string option list ->
    2.13 +    (bool * string) * Attrib.src list -> expr ->
    2.14 +    string option list * (string * string) list ->
    2.15      theory -> Proof.state
    2.16    val interpretation_in_locale: (Proof.context -> Proof.context) ->
    2.17      xstring * expr -> theory -> Proof.state
    2.18    val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
    2.19 -    (bool * string) * Attrib.src list -> expr -> typ Symtab.table * term Symtab.table ->
    2.20 +    (bool * string) * Attrib.src list -> expr ->
    2.21 +    (typ Symtab.table * term Symtab.table) * (term * term) list ->
    2.22      bool -> Proof.state -> Proof.state
    2.23    val interpret: (Proof.state -> Proof.state Seq.seq) ->
    2.24 -    (bool * string) * Attrib.src list -> expr -> string option list ->
    2.25 +    (bool * string) * Attrib.src list -> expr ->
    2.26 +    string option list * (string * string) list ->
    2.27      bool -> Proof.state -> Proof.state
    2.28  end;
    2.29  
    2.30 @@ -186,18 +190,28 @@
    2.31      val empty: T
    2.32      val join: T * T -> T
    2.33      val dest: theory -> T ->
    2.34 -      (term list * (((bool * string) * Attrib.src list) * Element.witness list)) list
    2.35 +      (term list *
    2.36 +        (((bool * string) * Attrib.src list) * Element.witness list *
    2.37 +         Element.witness Termtab.table)) list
    2.38      val lookup: theory -> T * term list ->
    2.39 -      (((bool * string) * Attrib.src list) * Element.witness list) option
    2.40 +      (((bool * string) * Attrib.src list) * Element.witness list *
    2.41 +       Element.witness Termtab.table) option
    2.42      val insert: theory -> term list * ((bool * string) * Attrib.src list) -> T ->
    2.43        T * (term list * (((bool * string) * Attrib.src list) * Element.witness list)) list
    2.44      val add_witness: term list -> Element.witness -> T -> T
    2.45 +    val add_equation: term list -> Element.witness -> T -> T
    2.46    end =
    2.47  struct
    2.48 -  (* a registration consists of theorems (actually, witnesses) instantiating locale
    2.49 -     assumptions and prefix (boolean flag indicates full qualification)
    2.50 -     and attributes, indexed by parameter instantiation *)
    2.51 -  type T = (((bool * string) * Attrib.src list) * Element.witness list) Termtab.table;
    2.52 +  (* A registration is indexed by parameter instantiation.  Its components are:
    2.53 +     - parameters and prefix
    2.54 +       (if the Boolean flag is set, only accesses containing the prefix are generated,
    2.55 +        otherwise the prefix may be omitted when accessing theorems etc.) 
    2.56 +     - theorems (actually witnesses) instantiating locale assumptions
    2.57 +     - theorems (equations, actually witnesses) interpreting derived concepts
    2.58 +       and indexed by lhs
    2.59 +  *)
    2.60 +  type T = (((bool * string) * Attrib.src list) * Element.witness list *
    2.61 +            Element.witness Termtab.table) Termtab.table;
    2.62  
    2.63    val empty = Termtab.empty;
    2.64  
    2.65 @@ -209,12 +223,17 @@
    2.66            | ut (s $ t) ts = ut s (t::ts)
    2.67      in ut t [] end;
    2.68  
    2.69 -  (* joining of registrations: prefix and attributes of left theory,
    2.70 -     thms are equal, no attempt to subsumption testing *)
    2.71 -  fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => reg) (r1, r2);
    2.72 +  (* joining of registrations:
    2.73 +     - prefix and attributes of right theory;
    2.74 +     - witnesses are equal, no attempt to subsumption testing;
    2.75 +     - union of equalities, if conflicting (i.e. two eqns with equal lhs)
    2.76 +       eqn of right theory takes precedence *)
    2.77 +  fun join (r1, r2) = Termtab.join (fn _ => fn ((_, _, e1), (n, w, e2)) =>
    2.78 +      (n, w, Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2);
    2.79  
    2.80    fun dest_transfer thy regs =
    2.81 -    Termtab.dest regs |> map (apsnd (apsnd (map (Element.transfer_witness thy))));
    2.82 +    Termtab.dest regs |> map (apsnd (fn (n, ws, es) =>
    2.83 +      (n, map (Element.transfer_witness thy) ws, Termtab.map (Element.transfer_witness thy) es)));
    2.84  
    2.85    fun dest thy regs = dest_transfer thy regs |> map (apfst untermify);
    2.86  
    2.87 @@ -230,7 +249,7 @@
    2.88      in
    2.89        (case subs of
    2.90          [] => NONE
    2.91 -      | ((t', (attn, thms)) :: _) =>
    2.92 +      | ((t', (attn, thms, eqns)) :: _) =>
    2.93            let
    2.94              val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
    2.95              (* thms contain Frees, not Vars *)
    2.96 @@ -241,7 +260,7 @@
    2.97                   |> map (fn ((x, 0), (_, t)) => (x, Logic.legacy_unvarify t))
    2.98                   |> Symtab.make;
    2.99              val inst_witness = Element.morph_witness (Element.inst_morphism thy (tinst', inst'));
   2.100 -          in SOME (attn, map inst_witness thms) end)
   2.101 +          in SOME (attn, map inst_witness thms, Termtab.map inst_witness eqns) end)
   2.102      end;
   2.103  
   2.104    (* add registration if not subsumed by ones already present,
   2.105 @@ -254,8 +273,8 @@
   2.106          [] => let
   2.107                  val sups =
   2.108                    filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
   2.109 -                val sups' = map (apfst untermify) sups
   2.110 -              in (Termtab.update (t, (attn, [])) regs, sups') end
   2.111 +                val sups' = map (apfst untermify) sups |> map (fn (ts, (n, w, d)) => (ts, (n, w)))
   2.112 +              in (Termtab.update (t, (attn, [], Termtab.empty)) regs, sups') end
   2.113        | _ => (regs, []))
   2.114      end;
   2.115  
   2.116 @@ -264,10 +283,22 @@
   2.117    fun add_witness ts thm regs =
   2.118      let
   2.119        val t = termify ts;
   2.120 -      val (x, thms) = the (Termtab.lookup regs t);
   2.121 +      val (x, thms, eqns) = the (Termtab.lookup regs t);
   2.122      in
   2.123 -      Termtab.update (t, (x, thm::thms)) regs
   2.124 +      Termtab.update (t, (x, thm::thms, eqns)) regs
   2.125      end;
   2.126 +
   2.127 +  (* add equation to registration, replaces previous equation with same lhs;
   2.128 +     only if instantiation is exact, otherwise exception Option raised;
   2.129 +     exception TERM raised if not a meta equality *)
   2.130 +  fun add_equation ts thm regs =
   2.131 +    let
   2.132 +      val t = termify ts;
   2.133 +      val (x, thms, eqns) = the (Termtab.lookup regs t);
   2.134 +    in
   2.135 +      Termtab.update (t, (x, thms, Termtab.update (thm |> Element.witness_prop |> Logic.dest_equals |> fst, thm) eqns)) regs
   2.136 +    end;
   2.137 +(* TODO: avoid code clone *)
   2.138  end;
   2.139  
   2.140  
   2.141 @@ -364,7 +395,8 @@
   2.142  
   2.143  (* Ids of global registrations are varified,
   2.144     Ids of local registrations are not.
   2.145 -   Thms of registrations are never varified. *)
   2.146 +   Witness thms of registrations are never varified.
   2.147 +   Varification of eqns as varification of ids. *)
   2.148  
   2.149  (* retrieve registration from theory or context *)
   2.150  
   2.151 @@ -409,7 +441,7 @@
   2.152        val _ = if not (null sups) then warning
   2.153                  ("Subsumed interpretation(s) of locale " ^
   2.154                   quote (extern thy name) ^
   2.155 -                 "\nby interpretation(s) with the following prefix(es):\n" ^
   2.156 +                 "\nwith the following prefix(es):" ^
   2.157                    commas_quote (map (fn (_, (((_, s), _), _)) => s) sups))
   2.158                else ();
   2.159      in Symtab.update (name, reg') regs end) thy_ctxt;
   2.160 @@ -425,8 +457,7 @@
   2.161      (axiom, imports, elems, params, lparams, decls, regs @ [(id, [])], intros));
   2.162  
   2.163  
   2.164 -(* add witness theorem to registration in theory or context,
   2.165 -   ignored if registration not present *)
   2.166 +(* add witness theorem to registration, ignored if registration not present *)
   2.167  
   2.168  fun add_witness (name, ps) thm =
   2.169    Symtab.map_entry name (Registrations.add_witness ps thm);
   2.170 @@ -444,33 +475,50 @@
   2.171      in (axiom, imports, elems, params, lparams, decls, map add regs, intros) end);
   2.172  
   2.173  
   2.174 +(* add equation to registration, ignored if registration not present *)
   2.175 +
   2.176 +fun add_equation (name, ps) thm =
   2.177 +  Symtab.map_entry name (Registrations.add_equation ps thm);
   2.178 +
   2.179 +fun add_global_equation id thm =
   2.180 +  GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, add_equation id thm regs));
   2.181 +
   2.182 +val add_local_equation = LocalLocalesData.map oo add_equation;
   2.183 +
   2.184 +
   2.185  (* printing of registrations *)
   2.186  
   2.187  fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt =
   2.188    let
   2.189      val ctxt = mk_ctxt thy_ctxt;
   2.190      val thy = ProofContext.theory_of ctxt;
   2.191 -
   2.192 +(* TODO: nice effect of show_wits on equations. *)
   2.193      val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
   2.194      fun prt_inst ts =
   2.195          Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
   2.196 -    fun prt_attn ((fully_qualified, prfx), atts) =
   2.197 -        if fully_qualified
   2.198 -          then Pretty.breaks (Pretty.str prfx :: Pretty.str "[!]" :: Attrib.pretty_attribs ctxt atts)
   2.199 -          else Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts);
   2.200 -    fun prt_witns witns = Pretty.enclose "[" "]"
   2.201 -      (Pretty.breaks (map (prt_term o Element.witness_prop) witns));
   2.202 -    fun prt_reg (ts, (((_, ""), []), witns)) =
   2.203 +    fun prt_attn ((false, prfx), atts) =
   2.204 +        Pretty.breaks (Pretty.str prfx :: Pretty.str "(optional)" ::
   2.205 +          Attrib.pretty_attribs ctxt atts)
   2.206 +      | prt_attn ((true, prfx), atts) =
   2.207 +        Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts);
   2.208 +    fun prt_eqns [] = Pretty.str "no equations."
   2.209 +      | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::
   2.210 +          Pretty.breaks (map (Element.pretty_witness ctxt) eqns));
   2.211 +    fun prt_core ts eqns =
   2.212 +          [prt_inst ts, Pretty.fbrk, prt_eqns (Termtab.dest eqns |> map snd)];
   2.213 +    fun prt_witns [] = Pretty.str "no witnesses."
   2.214 +      | prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 ::
   2.215 +          Pretty.breaks (map (Element.pretty_witness ctxt) witns))
   2.216 +    fun prt_reg (ts, (((_, ""), []), witns, eqns)) =
   2.217          if show_wits
   2.218 -          then Pretty.block [prt_inst ts, Pretty.fbrk, prt_witns witns]
   2.219 -          else prt_inst ts
   2.220 -      | prt_reg (ts, (attn, witns)) =
   2.221 +          then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns])
   2.222 +          else Pretty.block (prt_core ts eqns)
   2.223 +      | prt_reg (ts, (attn, witns, eqns)) =
   2.224          if show_wits
   2.225 -          then Pretty.block ((prt_attn attn @
   2.226 -            [Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk,
   2.227 -              prt_witns witns]))
   2.228 +          then Pretty.block ((prt_attn attn @ [Pretty.str ":", Pretty.brk 1] @
   2.229 +            prt_core ts eqns @ [Pretty.fbrk, prt_witns witns]))
   2.230            else Pretty.block ((prt_attn attn @
   2.231 -            [Pretty.str ":", Pretty.brk 1, prt_inst ts]));
   2.232 +            [Pretty.str ":", Pretty.brk 1] @ prt_core ts eqns));
   2.233  
   2.234      val loc_int = intern thy loc;
   2.235      val regs = get_regs thy_ctxt;
   2.236 @@ -480,7 +528,7 @@
   2.237          NONE => Pretty.str ("no interpretations in " ^ msg)
   2.238        | SOME r => let
   2.239              val r' = Registrations.dest thy r;
   2.240 -            val r'' = Library.sort_wrt (fn (_, (((_, prfx), _), _)) => prfx) r';
   2.241 +            val r'' = Library.sort_wrt (fn (_, (((_, prfx), _), _, _)) => prfx) r';
   2.242            in Pretty.big_list ("interpretations in " ^ msg ^ ":")
   2.243              (map prt_reg r'')
   2.244            end)
   2.245 @@ -1514,8 +1562,8 @@
   2.246    ||> ProofContext.restore_naming ctxt;
   2.247  
   2.248  
   2.249 -(* collect witnesses for global registration;
   2.250 -   requires parameters and flattened list of (assumed!) identifiers
   2.251 +(* collect witnesses and equations up to a particular target for global
   2.252 +   registration; requires parameters and flattened list of identifiers
   2.253     instead of recomputing it from the target *)
   2.254  
   2.255  fun collect_global_witnesses thy parms ids vts = let
   2.256 @@ -1529,9 +1577,20 @@
   2.257      val vinst = Symtab.make (parms ~~ vts);
   2.258      fun vinst_names ps = map (the o Symtab.lookup vinst) ps;
   2.259      val inst = Symtab.make (parms ~~ ts);
   2.260 -    val ids' = map (apsnd vinst_names) ids;
   2.261 -    val wits = maps (snd o the o get_global_registration thy) ids';
   2.262 -  in ((tinst, inst), wits) end;
   2.263 +    val inst_ids = map (apfst (apsnd vinst_names)) ids;
   2.264 +    val assumed_ids' = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids;
   2.265 +    val wits = maps (#2 o the o get_global_registration thy) assumed_ids';
   2.266 +
   2.267 +    val ids' = map fst inst_ids;
   2.268 +(* TODO: code duplication with activate_facts_elemss *)
   2.269 +    fun add_eqns id eqns =
   2.270 +      let
   2.271 +        val eqns' = case get_global_registration thy id
   2.272 +          of NONE => eqns
   2.273 +           | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
   2.274 +      in ((id, eqns'), eqns') end;
   2.275 +    val eqns = fold_map add_eqns ids' Termtab.empty |> snd |> Termtab.dest |> map snd;
   2.276 +  in ((tinst, inst), wits, eqns) end;
   2.277  
   2.278  
   2.279  (* store instantiations of args for all registered interpretations
   2.280 @@ -1541,16 +1600,16 @@
   2.281    let
   2.282      val parms = the_locale thy target |> #params |> map fst;
   2.283      val ids = flatten (ProofContext.init thy, intern_expr thy)
   2.284 -      (([], Symtab.empty), Expr (Locale target)) |> fst |> fst
   2.285 -      |> map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE)
   2.286 +      (([], Symtab.empty), Expr (Locale target)) |> fst |> fst;
   2.287 +(*      |> map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) *)
   2.288  
   2.289      val regs = get_global_registrations thy target;
   2.290  
   2.291      (* add args to thy for all registrations *)
   2.292  
   2.293 -    fun activate (vts, (((fully_qualified, prfx), atts2), _)) thy =
   2.294 +    fun activate (vts, (((fully_qualified, prfx), atts2), _, _)) thy =
   2.295        let
   2.296 -        val (insts, prems) = collect_global_witnesses thy parms ids vts;
   2.297 +        val (insts, prems, eqns) = collect_global_witnesses thy parms ids vts;
   2.298          val attrib = Attrib.attribute_i thy;
   2.299          val inst_atts = Args.morph_values
   2.300            (Morphism.name_morphism (NameSpace.qualified prfx) $>
   2.301 @@ -1558,7 +1617,10 @@
   2.302              Element.satisfy_morphism prems $>
   2.303              Morphism.thm_morphism Drule.standard);
   2.304          val inst_thm =
   2.305 -          Element.inst_thm thy insts #> Element.satisfy_thm prems #> Drule.standard;
   2.306 +          Element.inst_thm thy insts #> Element.satisfy_thm prems #>
   2.307 +            rewrite_rule (map Element.conclude_witness eqns) #>
   2.308 +(* TODO: or better use LocalDefs.unfold? *)
   2.309 +            Drule.standard;
   2.310          val args' = args |> map (fn ((name, atts), bs) =>
   2.311              ((name, map (attrib o inst_atts) atts),
   2.312                bs |> map (fn (ths, more_atts) =>
   2.313 @@ -1889,7 +1951,7 @@
   2.314    let
   2.315      val thy = ProofContext.theory_of ctxt;
   2.316      fun get registrations = Symtab.fold (fn (_, regs) => fn thms =>
   2.317 -        (Registrations.dest thy regs |> map (fn (_, (_, wits)) =>
   2.318 +        (Registrations.dest thy regs |> map (fn (_, (_, wits, _)) =>
   2.319            map Element.conclude_witness wits) |> flat) @ thms)
   2.320        registrations [];
   2.321      val globals = get (#3 (GlobalLocalesData.get thy));
   2.322 @@ -1933,11 +1995,20 @@
   2.323  
   2.324  (* activate instantiated facts in theory or context *)
   2.325  
   2.326 -fun gen_activate_facts_elemss get_reg note attrib std put_reg add_wit
   2.327 +structure Idtab =
   2.328 +  TableFun(type key = string * term list
   2.329 +    val ord = prod_ord string_ord (list_ord Term.fast_term_ord));
   2.330 +
   2.331 +fun gen_activate_facts_elemss mk_ctxt get_reg note attrib std put_reg add_wit add_eqn
   2.332          attn all_elemss new_elemss propss thmss thy_ctxt =
   2.333    let
   2.334 -    fun activate_elem disch ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
   2.335 +    val ctxt = mk_ctxt thy_ctxt;
   2.336 +    val (propss, eq_props) = chop (length new_elemss) propss;
   2.337 +    val (thmss, eq_thms) = chop (length new_elemss) thmss;
   2.338 +
   2.339 +    fun activate_elem eqns disch ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
   2.340          let
   2.341 +          val ctxt = mk_ctxt thy_ctxt;
   2.342            val fact_morphism =
   2.343              Morphism.name_morphism (NameSpace.qualified prfx)
   2.344              $> Morphism.thm_morphism disch;
   2.345 @@ -1948,26 +2019,31 @@
   2.346              (* append interpretation attributes *)
   2.347              |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
   2.348              (* discharge hyps *)
   2.349 -            |> map (apsnd (map (apfst (map disch))));
   2.350 +            |> map (apsnd (map (apfst (map disch))))
   2.351 +            (* unfold eqns *)
   2.352 +            |> map (apsnd (map (apfst (map (LocalDefs.unfold ctxt eqns)))))
   2.353 +(* TODO: better use attribute to unfold? *)
   2.354          in snd (note kind (fully_qualified, prfx) facts' thy_ctxt) end
   2.355 -      | activate_elem _ _ _ thy_ctxt = thy_ctxt;
   2.356 -
   2.357 -    fun activate_elems disch ((id, _), elems) thy_ctxt =
   2.358 +      | activate_elem _ _ _ _ thy_ctxt = thy_ctxt;
   2.359 +
   2.360 +    fun activate_elems eqns disch ((id, _), elems) thy_ctxt =
   2.361        let
   2.362 -        val ((prfx, atts2), _) = case get_reg thy_ctxt id
   2.363 +        val (prfx_atts, _, _) = case get_reg thy_ctxt id
   2.364           of SOME x => x
   2.365            | NONE => sys_error ("Unknown registration of " ^ quote (fst id)
   2.366                ^ " while activating facts.");
   2.367 -      in fold (activate_elem disch (prfx, atts2)) elems thy_ctxt end;
   2.368 +      in fold (activate_elem (the (Idtab.lookup eqns id)) disch prfx_atts) elems thy_ctxt end;
   2.369  
   2.370      val thy_ctxt' = thy_ctxt
   2.371        (* add registrations *)
   2.372        |> fold (fn ((id, _), _) => put_reg id attn) new_elemss
   2.373 -      (* add witnesses of Assumed elements *)
   2.374 -      |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss);
   2.375 +      (* add witnesses of Assumed elements (only those generate proof obligations) *)
   2.376 +      |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss)
   2.377 +      (* add equations *)
   2.378 +      |> fold (fn (id, thms) => fold (add_eqn id) thms) (map fst eq_props ~~ eq_thms);
   2.379  
   2.380      val prems = flat (map_filter
   2.381 -          (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id)
   2.382 +          (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' id)
   2.383              | ((_, Derived _), _) => NONE) all_elemss);
   2.384      val satisfy = Element.satisfy_morphism prems;
   2.385      val thy_ctxt'' = thy_ctxt'
   2.386 @@ -1976,14 +2052,34 @@
   2.387           (map_filter (fn ((_, Assumed _), _) => NONE
   2.388              | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
   2.389  
   2.390 +    (* Accumulate equations *)
   2.391 +    fun add_eqns ((id, _), _) eqns =
   2.392 +       let
   2.393 +         val eqns' = case get_reg thy_ctxt'' id
   2.394 +           of NONE => eqns
   2.395 +            | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
   2.396 +(*                handle Termtab.DUPS ts =>
   2.397 +                  error (implode ("Conflicting equations for terms" ::
   2.398 +                    map (quote o ProofContext.string_of_term ctxt) ts))
   2.399 +*)
   2.400 +       in ((id, eqns'), eqns') end;
   2.401 +    val all_eqns = fold_map add_eqns all_elemss Termtab.empty |> fst
   2.402 +      |> map (apsnd (map (Element.conclude_witness o snd) o Termtab.dest))
   2.403 +      |> (fn xs => fold Idtab.update xs Idtab.empty)
   2.404 +      (* Idtab.make doesn't work: can have conflicting duplicates,
   2.405 +         because instantiation may equate ids and equations are accumulated! *)
   2.406 +
   2.407 +(* TODO: can use dest_witness here? (more efficient) *)
   2.408 +
   2.409      val disch' = std o Morphism.thm satisfy;  (* FIXME *)
   2.410    in
   2.411      thy_ctxt''
   2.412      (* add facts to theory or context *)
   2.413 -    |> fold (activate_elems disch') new_elemss
   2.414 +    |> fold (activate_elems all_eqns disch') new_elemss
   2.415    end;
   2.416  
   2.417  fun global_activate_facts_elemss x = gen_activate_facts_elemss
   2.418 +      ProofContext.init
   2.419        (fn thy => fn (name, ps) =>
   2.420          get_global_registration thy (name, map Logic.varify ps))
   2.421        global_note_prefix_i
   2.422 @@ -1991,16 +2087,21 @@
   2.423        (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
   2.424        (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o
   2.425          Element.map_witness (fn (t, th) => (Logic.legacy_unvarify t, legacy_unvarify th))
   2.426 -        (* FIXME *)) x;
   2.427 +        (* FIXME *))
   2.428 +      (fn (n, ps) => add_global_equation (n, map Logic.varify ps))
   2.429 +      x;
   2.430  
   2.431  fun local_activate_facts_elemss x = gen_activate_facts_elemss
   2.432 +      I
   2.433        get_local_registration
   2.434        local_note_prefix_i
   2.435        (Attrib.attribute_i o ProofContext.theory_of) I
   2.436        put_local_registration
   2.437 -      add_local_witness x;
   2.438 -
   2.439 -fun read_instantiations read_terms is_local parms insts =
   2.440 +      add_local_witness
   2.441 +      add_local_equation
   2.442 +      x;
   2.443 +
   2.444 +fun read_instantiations read_terms is_local parms (insts, eqns) =
   2.445    let
   2.446      (* user input *)
   2.447      val insts = if length parms < length insts
   2.448 @@ -2009,24 +2110,32 @@
   2.449      val (ps, pTs) = split_list parms;
   2.450      val pvTs = map Logic.legacy_varifyT pTs;
   2.451  
   2.452 -    (* instantiations given by user *)
   2.453 -    val given = map_filter (fn (_, (NONE, _)) => NONE
   2.454 -         | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs));
   2.455 -    val (given_ps, given_insts) = split_list given;
   2.456 +    (* context for reading terms *)
   2.457      val tvars = fold Term.add_tvarsT pvTs [];
   2.458      val tfrees = fold Term.add_tfreesT pvTs [];
   2.459      val used = map (fst o fst) tvars @ map fst tfrees;
   2.460      val sorts = AList.lookup (op =) tvars;
   2.461 -    val (vs, vinst) = read_terms sorts used given_insts;
   2.462 -    val vars = foldl Term.add_term_tvar_ixns [] vs
   2.463 +
   2.464 +    (* parameter instantiations given by user *)
   2.465 +    val given = map_filter (fn (_, (NONE, _)) => NONE
   2.466 +         | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs));
   2.467 +    val (given_ps, given_insts) = split_list given;
   2.468 +
   2.469 +    (* equations given by user *)
   2.470 +    val (lefts, rights) = split_list eqns;
   2.471 +    val max_eqs = length eqns;
   2.472 +    val Ts = map (fn i => TVar (("x_", i), [])) (0 upto max_eqs - 1);
   2.473 +
   2.474 +    val (all_vs, vinst) =
   2.475 +      read_terms sorts used (given_insts @ (lefts ~~ Ts) @ (rights ~~ Ts));
   2.476 +    val vars = foldl Term.add_term_tvar_ixns [] all_vs
   2.477        |> subtract (op =) (map fst tvars)
   2.478 -      |> fold Term.add_varnames vs
   2.479 +      |> fold Term.add_varnames all_vs
   2.480      val _ = if null vars then ()
   2.481           else error ("Illegal schematic variable(s) in instantiation: " ^
   2.482             commas_quote (map Syntax.string_of_vname vars));
   2.483 -
   2.484      (* replace new types (which are TFrees) by ones with new names *)
   2.485 -    val new_Tnames = map fst (fold Term.add_tfrees vs [])
   2.486 +    val new_Tnames = map fst (fold Term.add_tfrees all_vs [])
   2.487        |> Name.names (Name.make_context used) "'a"
   2.488        |> map swap;
   2.489      val renameT =
   2.490 @@ -2035,16 +2144,21 @@
   2.491          TFree ((the o AList.lookup (op =) new_Tnames) a, s));
   2.492      val rename =
   2.493        if is_local then I
   2.494 -      else Term.map_types renameT
   2.495 +      else Term.map_types renameT;
   2.496 +    val (vs, ts) = chop (length given_insts) all_vs;
   2.497 +
   2.498      val instT = Symtab.empty
   2.499        |> fold (fn ((x, 0), T) => Symtab.update (x, renameT T)) vinst;
   2.500      val inst = Symtab.empty
   2.501        |> fold2 (fn x => fn t => Symtab.update (x, rename t)) given_ps vs;
   2.502  
   2.503 -  in (instT, inst) end;
   2.504 +    val (lefts', rights') = chop max_eqs (map rename ts);
   2.505 +
   2.506 +  in ((instT, inst), lefts' ~~ rights') end;
   2.507 +
   2.508  
   2.509  fun gen_prep_registration mk_ctxt is_local read_terms test_reg activate
   2.510 -    prep_attr prep_expr prep_instantiations
   2.511 +    prep_attr prep_expr prep_insts
   2.512      thy_ctxt raw_attn raw_expr raw_insts =
   2.513    let
   2.514      val ctxt = mk_ctxt thy_ctxt;
   2.515 @@ -2064,7 +2178,15 @@
   2.516  
   2.517      (** compute instantiation **)
   2.518  
   2.519 -    val (instT, inst1) = prep_instantiations (read_terms thy_ctxt) is_local parms raw_insts;
   2.520 +    (* consistency check: equations need to be stored in a particular locale,
   2.521 +       therefore if equations are present locale expression must be a name *)
   2.522 +
   2.523 +    val _ = case (expr, snd raw_insts) of
   2.524 +        (Locale _, _) => () | (_, []) => ()
   2.525 +      | (_, _) => error "Interpretations with `where' only permitted if locale expression is a name.";
   2.526 +
   2.527 +    (* read or certify instantiation *)
   2.528 +    val ((instT, inst1), eqns') = prep_insts (read_terms thy_ctxt) is_local parms raw_insts;
   2.529  
   2.530      (* defined params without given instantiation *)
   2.531      val not_given = filter_out (Symtab.defined inst1 o fst) parms;
   2.532 @@ -2093,8 +2215,14 @@
   2.533        |> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode)));
   2.534  
   2.535      (* remove fragments already registered with theory or context *)
   2.536 -    val new_inst_elemss = filter_out (fn ((id, _), _) => test_reg thy_ctxt id) inst_elemss;
   2.537 -    val propss = map extract_asms_elems new_inst_elemss;
   2.538 +    val new_inst_elemss = filter_out (fn ((id, _), _) =>
   2.539 +          test_reg thy_ctxt id) inst_elemss;
   2.540 +(*    val new_ids = map #1 new_inst_elemss; *)
   2.541 +
   2.542 +    (* equations *)
   2.543 +    val eqn_elems = if null eqns' then [] else [(Library.last_elem inst_elemss |> fst |> fst, map Logic.mk_equals eqns')];
   2.544 +
   2.545 +    val propss = map extract_asms_elems new_inst_elemss @ eqn_elems;
   2.546  
   2.547    in (propss, activate attn inst_elemss new_inst_elemss propss) end;
   2.548  
   2.549 @@ -2147,8 +2275,8 @@
   2.550            the target, unless already present
   2.551          - add facts of induced registrations to theory **)
   2.552  
   2.553 -    val t_ids = map_filter
   2.554 -        (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids;
   2.555 +(*    val t_ids = map_filter
   2.556 +        (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids; *)
   2.557  
   2.558      fun activate thmss thy = let
   2.559          val satisfy = Element.satisfy_thm (flat thmss);
   2.560 @@ -2160,9 +2288,9 @@
   2.561                  |> fold (add_witness_in_locale target id) thms
   2.562            | activate_id _ thy = thy;
   2.563  
   2.564 -        fun activate_reg (vts, (((fully_qualified, prfx), atts2), _)) thy =
   2.565 +        fun activate_reg (vts, (((fully_qualified, prfx), atts2), _, _)) thy =
   2.566            let
   2.567 -            val (insts, wits) = collect_global_witnesses thy fixed t_ids vts;
   2.568 +            val (insts, wits, _) = collect_global_witnesses thy fixed target_ids vts;
   2.569              fun inst_parms ps = map
   2.570                    (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps;
   2.571              val disch = Element.satisfy_thm wits;
     3.1 --- a/src/Pure/Isar/spec_parse.ML	Fri Apr 13 10:00:04 2007 +0200
     3.2 +++ b/src/Pure/Isar/spec_parse.ML	Fri Apr 13 10:01:43 2007 +0200
     3.3 @@ -23,7 +23,8 @@
     3.4      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
     3.5    val locale_mixfix: token list -> mixfix * token list
     3.6    val locale_fixes: token list -> (string * string option * mixfix) list * token list
     3.7 -  val locale_insts: token list -> string option list * token list
     3.8 +  val locale_insts: token list ->
     3.9 +    (string option list * (string * string) list) * token list
    3.10    val locale_expr: token list -> Locale.expr * token list
    3.11    val locale_expr_unless: (token list -> 'a * token list) ->
    3.12      token list -> Locale.expr * token list
    3.13 @@ -86,7 +87,8 @@
    3.14    P.params >> map Syntax.no_syn) >> flat;
    3.15  
    3.16  val locale_insts =
    3.17 -  Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) [];
    3.18 +  Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
    3.19 +  -- Scan.optional (P.$$$ "where" |-- P.and_list1 (P.term -- (P.$$$ "=" |-- P.!!! P.term))) [];
    3.20  
    3.21  local
    3.22  
     4.1 --- a/src/Pure/Tools/class_package.ML	Fri Apr 13 10:00:04 2007 +0200
     4.2 +++ b/src/Pure/Tools/class_package.ML	Fri Apr 13 10:01:43 2007 +0200
     4.3 @@ -393,7 +393,7 @@
     4.4  
     4.5  fun prove_interpretation tac prfx_atts expr insts thy =
     4.6    thy
     4.7 -  |> Locale.interpretation_i I prfx_atts expr insts
     4.8 +  |> Locale.interpretation_i I prfx_atts expr (insts, [])
     4.9    |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
    4.10    |> ProofContext.theory_of;
    4.11  
     5.1 --- a/src/Pure/Tools/invoke.ML	Fri Apr 13 10:00:04 2007 +0200
     5.2 +++ b/src/Pure/Tools/invoke.ML	Fri Apr 13 10:01:43 2007 +0200
     5.3 @@ -120,7 +120,7 @@
     5.4      "schematic invocation of locale expression in proof context"
     5.5      (K.tag_proof K.prf_goal)
     5.6      (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
     5.7 -      >> (fn (((name, expr), insts), fixes) =>
     5.8 +      >> (fn (((name, expr), (insts, _)), fixes) =>
     5.9            Toplevel.print o Toplevel.proof' (invoke name expr insts fixes)));
    5.10  
    5.11  val _ = OuterSyntax.add_parsers [invokeP];