src/Pure/Isar/local_defs.ML
author wenzelm
Tue, 13 Jul 1999 13:54:08 +0200
changeset 6996 1a28d968c5aa
parent 6954 dbeafc269f4f
child 7271 442456b2a8bb
permissions -rw-r--r--
handle cgoal;
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
6996
1a28d968c5aa handle cgoal;
wenzelm
parents: 6954
diff changeset
    20
val refl_tac = Tactic.rtac (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
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    23
fun gen_def fix prep_term match_binds name atts ((x, raw_T), (raw_rhs, raw_pats)) state =
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
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    27
    val state' = fix [(x, raw_T)] state;
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
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    30
    val rhs = prep_term ctxt' raw_rhs;
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    31
    val T = Term.fastype_of rhs;
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    32
    val lhs = ProofContext.cert_term ctxt' (Free (x, T));
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    33
    val eq = Logic.mk_equals (lhs, rhs);
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    34
  in
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    35
    if lhs mem Term.add_term_frees (rhs, []) then
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    36
      err "lhs occurs on rhs"
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    37
    else if not (Term.term_tfrees rhs subset Term.typ_tfrees T) then
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    38
      err "extra type variables on rhs"
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    39
    else ();
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    40
    state'
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    41
    |> match_binds [(raw_pats, raw_rhs)]   (*note: raw_rhs prepared twice!*)
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    42
    |> Proof.assm_i (refl_tac, refl_tac) name atts [(eq, ([], []))]
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    43
  end;
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    44
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    45
val def = gen_def Proof.fix ProofContext.read_term Proof.match_bind;
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    46
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
    47
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    48
dbeafc269f4f added Isar/local_defs.ML;
wenzelm
parents:
diff changeset
    49
end;