added fixed_abbrev;
authorwenzelm
Sat Oct 20 18:54:33 2007 +0200 (2007-10-20 ago)
changeset 25119192105867f25
parent 25118 158149a6e95b
child 25120 23fbc38f6432
added fixed_abbrev;
src/Pure/Isar/local_defs.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Sat Oct 20 18:54:31 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Sat Oct 20 18:54:33 2007 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
     1.5      (term * (bstring * thm)) list * Proof.context
     1.6    val add_def: (string * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
     1.7 +  val fixed_abbrev: (string * mixfix) * term -> Proof.context -> (term * term) * Proof.context
     1.8    val export: Proof.context -> Proof.context -> thm -> thm list * thm
     1.9    val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
    1.10    val trans_terms: Proof.context -> thm list -> thm
    1.11 @@ -106,6 +107,21 @@
    1.12    in ((lhs, th), ctxt') end;
    1.13  
    1.14  
    1.15 +(* fixed_abbrev *)
    1.16 +
    1.17 +fun fixed_abbrev ((x, mx), rhs) ctxt =
    1.18 +  let
    1.19 +    val T = Term.fastype_of rhs;
    1.20 +    val ([x'], ctxt') = ctxt
    1.21 +      |> Variable.declare_term rhs
    1.22 +      |> ProofContext.add_fixes_i [(x, SOME T, mx)];
    1.23 +    val lhs = Free (x', T);
    1.24 +    val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs));
    1.25 +    fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);
    1.26 +    val (_, ctxt'') = Assumption.add_assms abbrev_export [] ctxt';
    1.27 +  in ((lhs, rhs), ctxt'') end;
    1.28 +
    1.29 +
    1.30  (* specific export -- result based on educated guessing *)
    1.31  
    1.32  (*