src/Pure/Isar/local_defs.ML
author wenzelm
Fri May 05 22:09:41 2000 +0200 (2000-05-05 ago)
changeset 8807 0046be1769f9
parent 8092 badbfb6ceac0
child 9295 5fc3c1f84e8a
permissions -rw-r--r--
GPLed;
     1 (*  Title:      Pure/Isar/local_defs.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Local definitions.
     7 *)
     8 
     9 signature LOCAL_DEFS =
    10 sig
    11   val def: string -> Proof.context attribute list
    12     -> (string * string option) *  (string * string list) -> Proof.state -> Proof.state
    13   val def_i: string -> Proof.context attribute list
    14     -> (string * typ option) * (term * term list) -> Proof.state -> Proof.state
    15 end;
    16 
    17 structure LocalDefs: LOCAL_DEFS =
    18 struct
    19 
    20 val refl_tac = Tactic.rtac (Drule.standard (Drule.reflexive_thm RS Drule.triv_goal));
    21 
    22 fun gen_def fix prep_term prep_pats raw_name atts ((x, raw_T), (raw_rhs, raw_pats)) state =
    23   let
    24     fun err msg = raise Proof.STATE ("Bad local def: " ^ msg, state);
    25 
    26     val state' = fix [([x], raw_T)] state;
    27     val ctxt' = Proof.context_of state';
    28 
    29     val name = if raw_name = "" then Thm.def_name x else raw_name;
    30     val rhs = prep_term ctxt' raw_rhs;
    31     val T = Term.fastype_of rhs;
    32     val lhs = ProofContext.cert_term ctxt' (Free (x, T));
    33     val eq = Logic.mk_equals (lhs, rhs);
    34     val pats = prep_pats T (ProofContext.declare_term rhs ctxt') raw_pats;
    35   in
    36     if lhs mem Term.add_term_frees (rhs, []) then err "lhs occurs on rhs"
    37     else ();
    38     state'
    39     |> Proof.match_bind_i [(pats, rhs)]
    40     |> Proof.assm_i (refl_tac, refl_tac) [(name, atts, [(eq, ([], []))])]
    41   end;
    42 
    43 val def = gen_def Proof.fix ProofContext.read_term ProofContext.read_term_pats;
    44 val def_i = gen_def Proof.fix_i ProofContext.cert_term ProofContext.cert_term_pats;
    45 
    46 
    47 end;