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