src/Pure/Isar/locale.ML

 (*  Title:      Pure/Isar/locale.ML
     ID:         $Id$
-    Author:     Markus Wenzel, TU München
+    Author:     Markus Wenzel, LMU München
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Locales -- Isar proof contexts as meta-level predicates, with local
 syntax and implicit structures.
 

 end;
 
 structure Locale: LOCALE =
 struct
 
-
 (** locale elements and expressions **)
 
 type context = ProofContext.context;
 
 datatype ('typ, 'term, 'fact, 'att) elem =

 
 fun inst_thm [] th = th
   | inst_thm env th =
       let
         val {sign, hyps, prop, maxidx, ...} = Thm.rep_thm th;
-        val cert = Thm.cterm_of sign and certT = Thm.ctyp_of sign;
-        val names = foldr Term.add_term_tfree_names (prop :: hyps, []);
-        val env' = filter (fn ((a, _), _) => a mem_string names) env;
+        val cert = Thm.cterm_of sign;
+        val certT = Thm.ctyp_of sign;
+        val occs = foldr Term.add_term_tfree_names (prop :: hyps, []);
+        val env' = filter (fn ((a, _), _) => a mem_string occs) env;
       in
         if null env' then th
         else
           th
           |> Drule.implies_intr_list (map cert hyps)
-          |> Drule.tvars_intr_list names
+          |> Drule.tvars_intr_list (map (#1 o #1) env')
           |> (fn (th', al) => th' |>
             Thm.instantiate ((map (fn ((a, _), T) => (the (assoc (al, a)), certT T)) env'), []))
           |> (fn th'' => Drule.implies_elim_list th''
               (map (Thm.assume o cert o inst_term env') hyps))
       end;

         val envs = unify_parms ctxt fixed_parms (map (#2 o #1) elemss);
         fun inst (((name, ps), elems), env) =
           ((name, map (apsnd (apsome (inst_type env))) ps), map (inst_elem env) elems);
       in map inst (elemss ~~ envs) end;
 
-fun flatten_expr ctxt expr =
+fun flatten_expr ctxt (prev_idents, expr) =
   let
     val thy = ProofContext.theory_of ctxt;
 
     fun renaming (Some x :: xs) (y :: ys) = (y, x) :: renaming xs ys
       | renaming (None :: xs) (y :: ys) = renaming xs ys

           else ((map (apfst (rename ren)) ps, map (rename ren) qs),
             map (rename_elem ren o #1) elems);
         val elems'' = map (rename_facts [NameSpace.base name, space_implode "_" xs]) elems';
       in ((name, params'), elems'') end;
 
-    val raw_elemss = unique_parms ctxt (map eval (#1 (identify (([], []), expr))));
+    val idents = gen_rems (op =) (#1 (identify (([], []), expr)), prev_idents);
+    val raw_elemss = unique_parms ctxt (map eval idents);
     val elemss = unify_elemss ctxt [] raw_elemss;
-  in elemss end;
+  in (prev_idents @ idents, elemss) end;
 
 end;
 
 
 (* activate elements *)
 
-fun declare_fixes fixes =
-  ProofContext.add_syntax fixes o
-  ProofContext.fix_direct (map (fn (x, T, _) => ([x], T)) fixes);
-
 local
 
-fun activate_elem (Fixes fixes) = declare_fixes fixes
+fun activate_elem (Fixes fixes) = ProofContext.add_fixes fixes
   | activate_elem (Assumes asms) =
       #1 o ProofContext.assume_i ProofContext.export_assume asms o
       ProofContext.fix_frees (flat (map (map #1 o #2) asms))
   | activate_elem (Defines defs) = (fn ctxt => #1 (ProofContext.assume_i ProofContext.export_def
       (map (fn ((name, atts), (t, ps)) =>

 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
 
 local
 
 fun declare_int_elem i (ctxt, Fixes fixes) =
-      (ctxt |> declare_fixes (map (fn (x, T, mx) =>
+      (ctxt |> ProofContext.add_fixes (map (fn (x, T, mx) =>
         (x, apsome (Term.map_type_tfree (Type.param i)) T, mx)) fixes), [])
   | declare_int_elem _ (ctxt, _) = (ctxt, []);
 
 fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) =
-      (ctxt |> declare_fixes (prep_fixes ctxt fixes), [])
+      (ctxt |> ProofContext.add_fixes (prep_fixes ctxt fixes), [])
   | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
   | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
   | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
 
 fun declare_elems prep_fixes ((ctxt, i), ((name, ps), elems)) =

 
 fun close_frees ctxt t =
   let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Term.add_frees ([], t)))
   in Term.list_all_free (frees, t) end;
 
+fun no_binds _ [] = []
+  | no_binds ctxt _ = raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt);
+
 fun closeup ctxt (Assumes asms) = Assumes (asms |> map (fn (a, propps) =>
-      (a, map (fn (t, _) => (close_frees ctxt t, ([], []))) propps)))
-  | closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, _)) =>
-      (a, (close_frees ctxt (#2 (ProofContext.cert_def ctxt t)), []))))
+      (a, map (fn (t, (ps, qs)) => (close_frees ctxt t,
+        (no_binds ctxt ps, no_binds ctxt qs))) propps)))
+  | closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, ps)) =>
+      (a, (close_frees ctxt (#2 (ProofContext.cert_def ctxt t)), no_binds ctxt ps))))
   | closeup ctxt elem = elem;
 
 fun finish_elem parms _ (Fixes fixes, _) = Ext (Fixes (map (fn (x, _, mx) =>
       (x, assoc_string (parms, x), mx)) fixes))
   | finish_elem _ close (Assumes asms, propp) = Ext (close (Assumes (map #1 asms ~~ propp)))

 
 fun prep_context_statement prep_expr prep_elemss prep_facts
     close fixed_params import elements raw_concl context =
   let
     val sign = ProofContext.sign_of context;
-    fun flatten (Elem (Fixes fixes)) = [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))]
-      | flatten (Elem elem) = [(("", []), Ext elem)]
-      | flatten (Expr expr) = map (apsnd Int) (flatten_expr context (prep_expr sign expr));
+    fun flatten (ids, Elem (Fixes fixes)) =
+          (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
+      | flatten (ids, Elem elem) = (ids, [(("", []), Ext elem)])
+      | flatten (ids, Expr expr) =
+          let val (ids', elemss) = flatten_expr context (ids, prep_expr sign expr)
+          in (ids', map (apsnd Int) elemss) end
     val activate = activate_facts prep_facts;
 
-    val raw_import_elemss = flatten (Expr import);
-    val raw_elemss = flat (map flatten elements);
+    val (import_ids, raw_import_elemss) = flatten ([], Expr import);
+    val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
     val (parms, all_elemss, concl) =
       prep_elemss close context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
 
     val n = length raw_import_elemss;
     val (import_ctxt, import_elemss) = foldl_map activate (context, take (n, all_elemss));

     val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
     val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt;
 
     fun prt_syn syn =
       let val s = (case syn of None => "(structure)" | Some mx => Syntax.string_of_mixfix mx)
-      in if s = "" then [] else [Pretty.brk 4, Pretty.str s] end;
+      in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end;
     fun prt_fix (x, Some T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
           prt_typ T :: Pretty.brk 1 :: prt_syn syn)
       | prt_fix (x, None, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);
 
     fun prt_name "" = [Pretty.brk 1]