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