6954
|
1 |
(* Title: Pure/Isar/local_defs.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
8807
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
6954
|
5 |
|
|
6 |
Local definitions.
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature LOCAL_DEFS =
|
|
10 |
sig
|
9467
|
11 |
val def: string -> Proof.context attribute list -> string * (string * string list)
|
|
12 |
-> Proof.state -> Proof.state
|
|
13 |
val def_i: string -> Proof.context attribute list -> string * (term * term list)
|
|
14 |
-> Proof.state -> Proof.state
|
6954
|
15 |
end;
|
|
16 |
|
|
17 |
structure LocalDefs: LOCAL_DEFS =
|
|
18 |
struct
|
|
19 |
|
9467
|
20 |
|
11816
|
21 |
(* export_def *)
|
6954
|
22 |
|
9467
|
23 |
fun dest_lhs cprop =
|
11816
|
24 |
let val x = #1 (Logic.dest_equals (Thm.term_of cprop))
|
9467
|
25 |
in Term.dest_Free x; Thm.cterm_of (Thm.sign_of_cterm cprop) x end
|
|
26 |
handle TERM _ => raise TERM ("Malformed definitional assumption encountered:\n" ^
|
|
27 |
quote (Display.string_of_cterm cprop), []);
|
|
28 |
|
11816
|
29 |
fun export_def _ cprops thm =
|
9467
|
30 |
thm
|
|
31 |
|> Drule.implies_intr_list cprops
|
|
32 |
|> Drule.forall_intr_list (map dest_lhs cprops)
|
|
33 |
|> Drule.forall_elim_vars 0
|
11816
|
34 |
|> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1;
|
9467
|
35 |
|
|
36 |
|
|
37 |
(* def(_i) *)
|
|
38 |
|
|
39 |
fun gen_def fix prep_term prep_pats raw_name atts (x, (raw_rhs, raw_pats)) state =
|
6954
|
40 |
let
|
9295
|
41 |
val _ = Proof.assert_forward state;
|
9324
|
42 |
val ctxt = Proof.context_of state;
|
6954
|
43 |
|
9295
|
44 |
(*rhs*)
|
7416
|
45 |
val name = if raw_name = "" then Thm.def_name x else raw_name;
|
9295
|
46 |
val rhs = prep_term ctxt raw_rhs;
|
6954
|
47 |
val T = Term.fastype_of rhs;
|
9295
|
48 |
val pats = prep_pats T (ProofContext.declare_term rhs ctxt) raw_pats;
|
|
49 |
|
|
50 |
(*lhs*)
|
9324
|
51 |
val lhs = ProofContext.bind_skolem ctxt [x] (Free (x, T));
|
6954
|
52 |
in
|
9324
|
53 |
state
|
9467
|
54 |
|> fix [([x], None)]
|
8092
|
55 |
|> Proof.match_bind_i [(pats, rhs)]
|
11816
|
56 |
|> Proof.assm_i export_def [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])]
|
6954
|
57 |
end;
|
|
58 |
|
8092
|
59 |
val def = gen_def Proof.fix ProofContext.read_term ProofContext.read_term_pats;
|
|
60 |
val def_i = gen_def Proof.fix_i ProofContext.cert_term ProofContext.cert_term_pats;
|
6954
|
61 |
|
|
62 |
|
|
63 |
end;
|