wenzelm@14657: (*  Title:      Pure/Isar/constdefs.ML
wenzelm@14657:     ID:         $Id$
wenzelm@14657:     Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
wenzelm@14657: 
wenzelm@14657: Standard constant definitions, with type-inference and optional
wenzelm@14657: structure context; specifications need to observe strictly sequential
wenzelm@14657: dependencies; no support for overloading.
wenzelm@14657: *)
wenzelm@14657: 
wenzelm@14657: signature CONSTDEFS =
wenzelm@14657: sig
wenzelm@18668:   val add_constdefs: (string * string option) list *
wenzelm@18668:     ((bstring * string option * mixfix) option * ((bstring * Attrib.src list) * string)) list ->
wenzelm@18668:     theory -> theory
wenzelm@18668:   val add_constdefs_i: (string * typ option) list *
wenzelm@18728:     ((bstring * typ option * mixfix) option * ((bstring * attribute list) * term)) list ->
wenzelm@18668:     theory -> theory
wenzelm@14657: end;
wenzelm@14657: 
wenzelm@14657: structure Constdefs: CONSTDEFS =
wenzelm@14657: struct
wenzelm@14657: 
wenzelm@14657: (** add_constdefs(_i) **)
wenzelm@14657: 
wenzelm@18668: fun gen_constdef prep_vars prep_term prep_att
wenzelm@18668:     structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
wenzelm@14657:   let
wenzelm@14664:     fun err msg ts =
wenzelm@17065:       error (cat_lines (msg :: map (Sign.string_of_term thy) ts));
wenzelm@14664: 
wenzelm@18668:     val (_, ctxt) = thy |> ProofContext.init |> ProofContext.add_fixes_i structs;
wenzelm@18668:     val ((d, mx), ctxt') =
wenzelm@18668:       (case raw_decl of
wenzelm@18668:         NONE => ((NONE, NoSyn), ctxt)
wenzelm@18668:       | SOME raw_var =>
wenzelm@18668:           ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
wenzelm@18668:             ProofContext.add_fixes_legacy [(x, T, mx)] #> snd #> pair (SOME x, mx)));
wenzelm@14657: 
wenzelm@14657:     val prop = prep_term ctxt' raw_prop;
wenzelm@14664:     val concl = Logic.strip_imp_concl prop;
wenzelm@14664:     val (lhs, _) = Logic.dest_equals concl handle TERM _ =>
wenzelm@14664:       err "Not a meta-equality (==):" [concl];
wenzelm@14664:     val head = Term.head_of lhs;
wenzelm@14664:     val (c, T) = Term.dest_Free head handle TERM _ =>
wenzelm@14664:       err "Locally fixed variable required as head of definition:" [head];
skalberg@15531:     val _ = (case d of NONE => () | SOME c' =>
wenzelm@14719:       if c <> c' then
wenzelm@14719:         err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
wenzelm@14664:       else ());
wenzelm@14657: 
wenzelm@17065:     val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name thy c, T))] prop;
wenzelm@14657:     val name = if raw_name = "" then Thm.def_name c else raw_name;
wenzelm@14657:     val atts = map (prep_att thy) raw_atts;
wenzelm@14664: 
wenzelm@14664:     val thy' =
wenzelm@14664:       thy
wenzelm@14664:       |> Theory.add_consts_i [(c, T, mx)]
wenzelm@18668:       |> PureThy.add_defs_i false [((name, def), atts)] |> snd;
wenzelm@17853:   in ((c, T), thy') end;
wenzelm@14657: 
wenzelm@18668: fun gen_constdefs prep_vars prep_term prep_att (raw_structs, specs) thy =
wenzelm@14664:   let
wenzelm@18638:     val ctxt = ProofContext.init thy;
wenzelm@18668:     val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
wenzelm@18668:     val (decls, thy') = fold_map (gen_constdef prep_vars prep_term prep_att structs) specs thy;
wenzelm@18765:   in Pretty.writeln (LocalTheory.pretty_consts ctxt decls); thy' end;
wenzelm@14657: 
wenzelm@18668: val add_constdefs = gen_constdefs ProofContext.read_vars_legacy
wenzelm@18728:   ProofContext.read_term_legacy Attrib.attribute;
wenzelm@18668: val add_constdefs_i = gen_constdefs ProofContext.cert_vars_legacy ProofContext.cert_term (K I);
wenzelm@14657: 
wenzelm@14657: end;