src/Pure/Isar/constdefs.ML
author wenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610 bafd82950e24
parent 35845 e5980f0ad025
child 36865 7330e4eefbd7
permissions -rw-r--r--
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
     1 (*  Title:      Pure/Isar/constdefs.ML
     2     Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
     3 
     4 Old-style constant definitions, with type-inference and optional
     5 structure context; specifications need to observe strictly sequential
     6 dependencies; no support for overloading.
     7 *)
     8 
     9 signature CONSTDEFS =
    10 sig
    11   val add_constdefs: (binding * string option) list *
    12     ((binding * string option * mixfix) option * (Attrib.binding * string)) list -> theory -> theory
    13   val add_constdefs_i: (binding * typ option) list *
    14     ((binding * typ option * mixfix) option * (Thm.binding * term)) list -> theory -> theory
    15 end;
    16 
    17 structure Constdefs: CONSTDEFS =
    18 struct
    19 
    20 (** add_constdefs(_i) **)
    21 
    22 fun gen_constdef prep_vars prep_prop prep_att
    23     structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
    24   let
    25     val _ = legacy_feature ("\"constdefs\"; prefer \"definition\" instead");
    26 
    27     fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
    28 
    29     val thy_ctxt = ProofContext.init_global thy;
    30     val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt);
    31     val ((d, mx), var_ctxt) =
    32       (case raw_decl of
    33         NONE => ((NONE, NoSyn), struct_ctxt)
    34       | SOME raw_var =>
    35           struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
    36             ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx)));
    37 
    38     val prop = prep_prop var_ctxt raw_prop;
    39     val (c, T) = #1 (Local_Defs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
    40     val _ =
    41       (case Option.map Name.of_binding d of
    42         NONE => ()
    43       | SOME c' =>
    44           if c <> c' then
    45             err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
    46           else ());
    47     val b = Binding.name c;
    48 
    49     val head = Const (Sign.full_bname thy c, T);
    50     val def = Term.subst_atomic [(Free (c, T), head)] prop;
    51     val name = Thm.def_binding_optional b raw_name;
    52     val atts = map (prep_att thy) raw_atts;
    53 
    54     val thy' =
    55       thy
    56       |> Sign.add_consts_i [(b, T, mx)]
    57       |> PureThy.add_defs false [((name, def), atts)]
    58       |-> (fn [thm] =>  (* FIXME thm vs. atts !? *)
    59         Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify_global head], [thm]) #>
    60         Code.add_default_eqn thm);
    61   in ((c, T), thy') end;
    62 
    63 fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
    64   let
    65     val ctxt = ProofContext.init_global thy;
    66     val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
    67     val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
    68   in Pretty.writeln (Proof_Display.pretty_consts ctxt (K true) decls); thy' end;
    69 
    70 val add_constdefs = gen_constdefs ProofContext.read_vars Syntax.read_prop Attrib.attribute;
    71 val add_constdefs_i = gen_constdefs ProofContext.cert_vars ProofContext.cert_prop (K I);
    72 
    73 end;