src/Pure/Isar/local_defs.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/local_defs.ML	Fri Jul 09 18:48:54 1999 +0200
@@ -0,0 +1,49 @@
+(*  Title:      Pure/Isar/local_defs.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Local definitions.
+*)
+
+signature LOCAL_DEFS =
+sig
+  val def: string -> Proof.context attribute list
+    -> (string * string option) *  (string * string list) -> Proof.state -> Proof.state
+  val def_i: string -> Proof.context attribute list
+    -> (string * typ) * (term * term list) -> Proof.state -> Proof.state
+end;
+
+structure LocalDefs: LOCAL_DEFS =
+struct
+
+
+val refl_tac = Tactic.rtac Drule.reflexive_thm;
+
+
+fun gen_def fix prep_term match_binds name atts ((x, raw_T), (raw_rhs, raw_pats)) state =
+  let
+    fun err msg = raise Proof.STATE ("Bad local def: " ^ msg, state);
+
+    val state' = fix [(x, raw_T)] state;
+    val ctxt' = Proof.context_of state';
+
+    val rhs = prep_term ctxt' raw_rhs;
+    val T = Term.fastype_of rhs;
+    val lhs = ProofContext.cert_term ctxt' (Free (x, T));
+    val eq = Logic.mk_equals (lhs, rhs);
+  in
+    if lhs mem Term.add_term_frees (rhs, []) then
+      err "lhs occurs on rhs"
+    else if not (Term.term_tfrees rhs subset Term.typ_tfrees T) then
+      err "extra type variables on rhs"
+    else ();
+    state'
+    |> match_binds [(raw_pats, raw_rhs)]   (*note: raw_rhs prepared twice!*)
+    |> Proof.assm_i (refl_tac, refl_tac) name atts [(eq, ([], []))]
+  end;
+
+val def = gen_def Proof.fix ProofContext.read_term Proof.match_bind;
+val def_i = gen_def Proof.fix_i ProofContext.cert_term Proof.match_bind_i;
+
+
+end;