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