added Isar/local_defs.ML;
authorwenzelm
Fri Jul 09 18:48:54 1999 +0200 (1999-07-09)
changeset 6954dbeafc269f4f
parent 6953 b3f6c39aaa2e
child 6955 9e2d97ef55d2
added Isar/local_defs.ML;
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/local_defs.ML
     1.1 --- a/src/Pure/IsaMakefile	Fri Jul 09 18:48:33 1999 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Fri Jul 09 18:48:54 1999 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4    Interface/isamode.ML Interface/proof_general.ML Isar/ROOT.ML \
     1.5    Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML \
     1.6    Isar/comment.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML \
     1.7 -  Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
     1.8 +  Isar/isar_thy.ML Isar/local_defs.ML Isar/method.ML Isar/outer_lex.ML \
     1.9    Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \
    1.10    Isar/proof_context.ML Isar/proof_data.ML Isar/proof_history.ML \
    1.11    Isar/session.ML Isar/skip_proof.ML Isar/toplevel.ML \
     2.1 --- a/src/Pure/Isar/ROOT.ML	Fri Jul 09 18:48:33 1999 +0200
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Fri Jul 09 18:48:54 1999 +0200
     2.3 @@ -16,6 +16,7 @@
     2.4  use "method.ML";
     2.5  
     2.6  (*derived proof elements*)
     2.7 +use "local_defs.ML";
     2.8  use "calculation.ML";
     2.9  use "skip_proof.ML";
    2.10  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Isar/local_defs.ML	Fri Jul 09 18:48:54 1999 +0200
     3.3 @@ -0,0 +1,49 @@
     3.4 +(*  Title:      Pure/Isar/local_defs.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Markus Wenzel, TU Muenchen
     3.7 +
     3.8 +Local definitions.
     3.9 +*)
    3.10 +
    3.11 +signature LOCAL_DEFS =
    3.12 +sig
    3.13 +  val def: string -> Proof.context attribute list
    3.14 +    -> (string * string option) *  (string * string list) -> Proof.state -> Proof.state
    3.15 +  val def_i: string -> Proof.context attribute list
    3.16 +    -> (string * typ) * (term * term list) -> Proof.state -> Proof.state
    3.17 +end;
    3.18 +
    3.19 +structure LocalDefs: LOCAL_DEFS =
    3.20 +struct
    3.21 +
    3.22 +
    3.23 +val refl_tac = Tactic.rtac Drule.reflexive_thm;
    3.24 +
    3.25 +
    3.26 +fun gen_def fix prep_term match_binds name atts ((x, raw_T), (raw_rhs, raw_pats)) state =
    3.27 +  let
    3.28 +    fun err msg = raise Proof.STATE ("Bad local def: " ^ msg, state);
    3.29 +
    3.30 +    val state' = fix [(x, raw_T)] state;
    3.31 +    val ctxt' = Proof.context_of state';
    3.32 +
    3.33 +    val rhs = prep_term ctxt' raw_rhs;
    3.34 +    val T = Term.fastype_of rhs;
    3.35 +    val lhs = ProofContext.cert_term ctxt' (Free (x, T));
    3.36 +    val eq = Logic.mk_equals (lhs, rhs);
    3.37 +  in
    3.38 +    if lhs mem Term.add_term_frees (rhs, []) then
    3.39 +      err "lhs occurs on rhs"
    3.40 +    else if not (Term.term_tfrees rhs subset Term.typ_tfrees T) then
    3.41 +      err "extra type variables on rhs"
    3.42 +    else ();
    3.43 +    state'
    3.44 +    |> match_binds [(raw_pats, raw_rhs)]   (*note: raw_rhs prepared twice!*)
    3.45 +    |> Proof.assm_i (refl_tac, refl_tac) name atts [(eq, ([], []))]
    3.46 +  end;
    3.47 +
    3.48 +val def = gen_def Proof.fix ProofContext.read_term Proof.match_bind;
    3.49 +val def_i = gen_def Proof.fix_i ProofContext.cert_term Proof.match_bind_i;
    3.50 +
    3.51 +
    3.52 +end;