src/Pure/Isar/local_defs.ML
author wenzelm
Wed Sep 29 13:49:07 1999 +0200 (1999-09-29)
changeset 7632 25a0d2ba3a87
parent 7502 257dd7777676
child 7667 22dc8b2455b8
permissions -rw-r--r--
removed extra shyps error;
     1 (*  Title:      Pure/Isar/local_defs.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Local definitions.
     6 *)
     7 
     8 signature LOCAL_DEFS =
     9 sig
    10   val def: string -> Proof.context attribute list
    11     -> (string * string option) *  (string * string list) -> Proof.state -> Proof.state
    12   val def_i: string -> Proof.context attribute list
    13     -> (string * typ) * (term * term list) -> Proof.state -> Proof.state
    14 end;
    15 
    16 structure LocalDefs: LOCAL_DEFS =
    17 struct
    18 
    19 
    20 val refl_tac = Tactic.rtac (Drule.standard (Drule.reflexive_thm RS Drule.triv_goal));
    21 
    22 
    23 fun gen_def fix prep_term match_binds raw_name atts ((x, raw_T), (raw_rhs, raw_pats)) state =
    24   let
    25     fun err msg = raise Proof.STATE ("Bad local def: " ^ msg, state);
    26 
    27     val state' = fix [([x], raw_T)] state;
    28     val ctxt' = Proof.context_of state';
    29 
    30     val name = if raw_name = "" then Thm.def_name x else raw_name;
    31     val rhs = prep_term ctxt' raw_rhs;
    32     val T = Term.fastype_of rhs;
    33     val lhs = ProofContext.cert_term ctxt' (Free (x, T));
    34     val eq = Logic.mk_equals (lhs, rhs);
    35   in
    36     if lhs mem Term.add_term_frees (rhs, []) then
    37       err "lhs occurs on rhs"
    38     else if not (Term.term_tfrees rhs subset Term.typ_tfrees T) then
    39       err "extra type variables on rhs"
    40     else ();
    41     state'
    42     |> match_binds [(raw_pats, raw_rhs)]   (*note: raw_rhs prepared twice!*)
    43     |> Proof.assm_i (refl_tac, refl_tac) [(name, atts, [(eq, ([], []))])]
    44   end;
    45 
    46 val def = gen_def Proof.fix ProofContext.read_term Proof.match_bind;
    47 val def_i = gen_def Proof.fix_i ProofContext.cert_term Proof.match_bind_i;
    48 
    49 
    50 end;