src/Pure/Isar/proof_context.ML

 datatype ctxt =
   Ctxt of
    {syntax:                                      (*global/local syntax, structs, mixfixed*)
       (Syntax.syntax * Syntax.syntax * (Syntax.syntax -> Syntax.syntax)) *
       string list * string list,
+    consts: Consts.T,                            (*const abbreviations*)
     fixes: bool * (string * string) list,        (*fixes: !!x. _ with proof body flag*)
     assms:
       ((cterm list * export) list *              (*assumes and views: A ==> _*)
         (string * thm list) list),               (*prems: A |- A*)
     binds: (typ * term) Vartab.table,            (*term bindings*)

       typ Vartab.table *                         (*type constraints*)
       sort Vartab.table *                        (*default sorts*)
       string list *                              (*used type variables*)
       term list Symtab.table};                   (*type variable occurrences*)
 
-fun make_ctxt (syntax, fixes, assms, binds, thms, cases, defaults) =
-  Ctxt {syntax = syntax, fixes = fixes, assms = assms, binds = binds,
+fun make_ctxt (syntax, consts, fixes, assms, binds, thms, cases, defaults) =
+  Ctxt {syntax = syntax, consts = consts, fixes = fixes, assms = assms, binds = binds,
     thms = thms, cases = cases, defaults = defaults};
 
 structure ContextData = ProofDataFun
 (
   val name = "Isar/context";
   type T = ctxt;
   fun init thy =
-    make_ctxt (((Sign.syn_of thy, Sign.syn_of thy, I), [], []), (false, []), ([], []),
-      Vartab.empty, (NameSpace.default_naming, NameSpace.empty_table, FactIndex.empty), [],
+    make_ctxt (((Sign.syn_of thy, Sign.syn_of thy, I), [], []), Sign.consts_of thy,
+      (false, []), ([], []), Vartab.empty,
+      (NameSpace.default_naming, NameSpace.empty_table, FactIndex.empty), [],
       (Vartab.empty, Vartab.empty, [], Symtab.empty));
   fun print _ _ = ();
 );
 
 val _ = Context.add_setup ContextData.init;
 
 fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
 
 fun map_context f =
-  ContextData.map (fn Ctxt {syntax, fixes, assms, binds, thms, cases, defaults} =>
-    make_ctxt (f (syntax, fixes, assms, binds, thms, cases, defaults)));
-
-fun map_syntax f = map_context (fn (syntax, fixes, assms, binds, thms, cases, defaults) =>
-  (f syntax, fixes, assms, binds, thms, cases, defaults));
-
-fun map_fixes f = map_context (fn (syntax, fixes, assms, binds, thms, cases, defaults) =>
-  (syntax, f fixes, assms, binds, thms, cases, defaults));
-
-fun map_assms f = map_context (fn (syntax, fixes, assms, binds, thms, cases, defaults) =>
-  (syntax, fixes, f assms, binds, thms, cases, defaults));
-
-fun map_binds f = map_context (fn (syntax, fixes, assms, binds, thms, cases, defaults) =>
-  (syntax, fixes, assms, f binds, thms, cases, defaults));
-
-fun map_thms f = map_context (fn (syntax, fixes, assms, binds, thms, cases, defaults) =>
-  (syntax, fixes, assms, binds, f thms, cases, defaults));
+  ContextData.map (fn Ctxt {syntax, consts, fixes, assms, binds, thms, cases, defaults} =>
+    make_ctxt (f (syntax, consts, fixes, assms, binds, thms, cases, defaults)));
+
+fun map_syntax f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
+  (f syntax, consts, fixes, assms, binds, thms, cases, defaults));
+
+fun map_consts f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
+  (syntax, f consts, fixes, assms, binds, thms, cases, defaults));
+
+fun map_fixes f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
+  (syntax, consts, f fixes, assms, binds, thms, cases, defaults));
+
+fun map_assms f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
+  (syntax, consts, fixes, f assms, binds, thms, cases, defaults));
+
+fun map_binds f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
+  (syntax, consts, fixes, assms, f binds, thms, cases, defaults));
+
+fun map_thms f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
+  (syntax, consts, fixes, assms, binds, f thms, cases, defaults));
 
 fun map_naming f = map_thms (fn (naming, table, index) => (f naming, table, index));
 
-fun map_cases f = map_context (fn (syntax, fixes, assms, binds, thms, cases, defaults) =>
-  (syntax, fixes, assms, binds, thms, f cases, defaults));
-
-fun map_defaults f = map_context (fn (syntax, fixes, assms, binds, thms, cases, defaults) =>
-  (syntax, fixes, assms, binds, thms, cases, f defaults));
+fun map_cases f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
+  (syntax, consts, fixes, assms, binds, thms, f cases, defaults));
+
+fun map_defaults f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) =>
+  (syntax, consts, fixes, assms, binds, thms, cases, f defaults));
 
 val syntax_of = #syntax o rep_context;
+val consts_of = #consts o rep_context;
 
 val is_body = #1 o #fixes o rep_context;
 fun set_body b = map_fixes (fn (_, fixes) => (b, fixes));
 fun restore_body ctxt = set_body (is_body ctxt);
 

 
 
 (** pretty printing **)
 
 fun pretty_term' thy ctxt t =
-  Sign.pretty_term' (syn_of' thy ctxt) (Context.Proof ctxt) (context_tr' ctxt t);
+  let
+    val consts = consts_of ctxt;
+    val t' = Pattern.rewrite_term thy (Consts.abbrevs_of consts) [] t;
+  in Sign.pretty_term' (syn_of' thy ctxt) consts (Context.Proof ctxt) (context_tr' ctxt t) end;
+
 fun pretty_term ctxt t = pretty_term' (theory_of ctxt) ctxt (context_tr' ctxt t);
 fun pretty_typ ctxt T = Sign.pretty_typ (theory_of ctxt) T;
 fun pretty_sort ctxt S = Sign.pretty_sort (theory_of ctxt) S;
 fun pretty_classrel ctxt cs = Sign.pretty_classrel (theory_of ctxt) cs;
 fun pretty_arity ctxt ar = Sign.pretty_arity (theory_of ctxt) ar;

 
 
 (* read wrt. theory *)     (*exception ERROR*)
 
 fun read_def_termTs freeze pp syn ctxt (types, sorts, used) sTs =
-  Sign.read_def_terms' pp (Sign.is_logtype (theory_of ctxt)) syn
+  Sign.read_def_terms' pp (Sign.is_logtype (theory_of ctxt)) syn (consts_of ctxt)
     (Context.Proof ctxt) (types, sorts) used freeze sTs;
 
 fun read_def_termT freeze pp syn ctxt defaults sT =
   apfst hd (read_def_termTs freeze pp syn ctxt defaults [sT]);
 

   #1 o read_def_termTs freeze pp syn thy defaults o map (rpair propT);
 
 
 (* norm_term *)
 
-(*
-  - expand abbreviations (polymorphic Consts)
-  - expand term bindings (polymorphic Vars)
-  - beta contraction
-*)
-
 fun norm_term ctxt schematic =
   let
-    val thy = theory_of ctxt;
-    val tsig = Sign.tsig_of thy;
-    val expansion = Sign.const_expansion thy;
-    val binding = Vartab.lookup (binds_of ctxt);
-
-    exception SAME;
-    fun norm (Const c) =
-          (case expansion c of
-            SOME u => (norm u handle SAME => u)
-          | NONE => raise SAME)
-      | norm (Var (xi, T)) =
-          (case binding xi of
-            SOME b =>
-              let val u = Envir.expand_atom tsig T b
-              in norm u handle SAME => u end
-          | NONE =>
-              if schematic then raise SAME
-              else error ("Unbound schematic variable: " ^ Syntax.string_of_vname xi))
-      | norm (Abs (a, T, body)) =  Abs (a, T, norm body)
-      | norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body))
-      | norm (f $ t) =
-          ((case norm f of
-            Abs (_, _, body) => normh (subst_bound (t, body))
-          | nf => nf $ (norm t handle SAME => t)) handle SAME => f $ norm t)
-      | norm _ =  raise SAME
-    and normh t = norm t handle SAME => t
-  in normh end;
+    val binds = binds_of ctxt;
+    val tsig = Sign.tsig_of (theory_of ctxt);
+
+    fun norm_var (xi, T) =
+      (case Vartab.lookup binds xi of
+        SOME t => Envir.expand_atom tsig T t
+      | NONE =>
+          if schematic then Var (xi, T)
+          else error ("Unbound schematic variable: " ^ Syntax.string_of_vname xi));
+  in Envir.beta_norm o Term.map_aterms (fn Var v => norm_var v | a => a) end;
 
 
 (* dummy patterns *)
 
 val prepare_dummies =

 
 (* certify terms *)
 
 local
 
-fun gen_cert cert pattern schematic ctxt t = t
+fun gen_cert prop pattern schematic ctxt t = t
   |> (if pattern then I else norm_term ctxt schematic)
-  |> (fn t' => cert (pp ctxt) (theory_of ctxt) t'
+  |> (fn t' => #1 (Sign.certify false prop (pp ctxt) (theory_of ctxt) t')
     handle TYPE (msg, _, _) => error msg
       | TERM (msg, _) => error msg);
 
-val certify_term = #1 ooo Sign.certify_term;
-val certify_prop = #1 ooo Sign.certify_prop;
-
 in
 
-val cert_term = gen_cert certify_term false false;
-val cert_prop = gen_cert certify_prop false false;
-val cert_props = map oo gen_cert certify_prop false;
-
-fun cert_term_pats _ = map o gen_cert certify_term true false;
-val cert_prop_pats = map o gen_cert certify_prop true false;
+val cert_term = gen_cert false false false;
+val cert_prop = gen_cert true false false;
+val cert_props = map oo gen_cert true false;
+
+fun cert_term_pats _ = map o gen_cert false true false;
+val cert_prop_pats = map o gen_cert true true false;
 
 end;
 
 
 (* declare terms *)

 
 (* inferred types of parameters *)
 
 fun infer_type ctxt x =
   (case try (fn () =>
-      Sign.infer_types (pp ctxt) (theory_of ctxt) (def_type ctxt false) (def_sort ctxt)
-        (used_types ctxt) true ([Free (x, dummyT)], TypeInfer.logicT)) () of
+      Sign.infer_types (pp ctxt) (theory_of ctxt) (consts_of ctxt) (def_type ctxt false)
+        (def_sort ctxt) (used_types ctxt) true ([Free (x, dummyT)], TypeInfer.logicT)) () of
     SOME (Free (_, T), _) => T
   | _ => error ("Failed to infer type of fixed variable " ^ quote x));
 
 fun inferred_param x ctxt =
   let val T = infer_type ctxt x

   else Sign.read_tyname (theory_of ctxt) c;
 
 fun read_const ctxt c =
   (case lookup_skolem ctxt c of
     SOME c' => Free (c', dummyT)
-  | NONE => Sign.read_const (theory_of ctxt) c);
+  | NONE => Consts.read_const (consts_of ctxt) c);
 
 
 
 (** Hindley-Milner polymorphism **)
 

 fun gen_fixes prep raw_vars ctxt =
   let
     val (ys, zs) = split_list (fixes_of ctxt);
     val (vars, ctxt') = prep raw_vars ctxt;
     val xs = map #1 vars;
-    val _ = no_dups ctxt (gen_duplicates (op =) xs);
+    val _ = no_dups ctxt (duplicates (op =) xs);
     val xs' =
       if is_body ctxt then Term.variantlist (map Syntax.skolem xs, zs)
       else (no_dups ctxt (xs inter_string ys); no_dups ctxt (xs inter_string zs); xs);
     val vars' = map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars;
   in

 
 (* basic assumptions *)
 
 (*
     [A]
-     : 
+     :
      B
   --------
   #A ==> B
 *)
 fun assume_export true = Seq.single oo Drule.implies_intr_protected
   | assume_export false = Seq.single oo Drule.implies_intr_list;
 
 (*
     [A]
-     : 
+     :
      B
   -------
   A ==> B
 *)
 fun presume_export _ = assume_export false;

 (* local syntax *)
 
 val print_syntax = Syntax.print_syntax o syn_of;
 
 
+(* local consts *)
+
+fun pretty_consts ctxt =
+  let
+    val (space, consts) = #constants (Consts.dest (consts_of ctxt));
+    val globals = #2 (#constants (Consts.dest (Sign.consts_of (theory_of ctxt))));
+    fun local_abbrev (_, (_, NONE)) = I
+      | local_abbrev (c, (T, SOME t)) =
+          if Symtab.defined globals c then I else cons (c, Logic.mk_equals (Const (c, T), t));
+    val abbrevs = NameSpace.extern_table (space, Symtab.make (Symtab.fold local_abbrev consts []));
+  in
+    if null abbrevs andalso not (! verbose) then []
+    else [Pretty.big_list "abbreviations:" (map (pretty_term ctxt o #2) abbrevs)]
+  end;
+
+
 (* term bindings *)
 
 fun pretty_binds ctxt =
   let
     val binds = binds_of ctxt;

 
     val (types, sorts, used, _) = defaults_of ctxt;
   in
     verb single (K pretty_thy) @
     pretty_ctxt ctxt @
+    verb pretty_consts (K ctxt) @
     verb pretty_binds (K ctxt) @
     verb pretty_lthms (K ctxt) @
     verb pretty_cases (K ctxt) @
     verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
     verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) @