author | berghofe |
Wed, 10 Oct 2001 18:40:46 +0200 | |
changeset 11718 | 92706a69dacc |
parent 10464 | b7b916a82dca |
child 11816 | 545aab7410ac |
permissions | -rw-r--r-- |
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 |
|
21 |
(* export_defs *) |
|
22 |
||
23 |
local |
|
24 |
||
11718
92706a69dacc
Removed unnecessary application of Drule.standard.
berghofe
parents:
10464
diff
changeset
|
25 |
val refl_tac = Tactic.rtac (Drule.reflexive_thm RS Drule.triv_goal); |
6954 | 26 |
|
9467 | 27 |
fun dest_lhs cprop = |
28 |
let val x = #1 (Logic.dest_equals (Logic.dest_goal (Thm.term_of cprop))) |
|
29 |
in Term.dest_Free x; Thm.cterm_of (Thm.sign_of_cterm cprop) x end |
|
30 |
handle TERM _ => raise TERM ("Malformed definitional assumption encountered:\n" ^ |
|
31 |
quote (Display.string_of_cterm cprop), []); |
|
32 |
||
33 |
fun disch_defs cprops thm = |
|
34 |
thm |
|
35 |
|> Drule.implies_intr_list cprops |
|
36 |
|> Drule.forall_intr_list (map dest_lhs cprops) |
|
37 |
|> Drule.forall_elim_vars 0 |
|
38 |
|> RANGE (replicate (length cprops) refl_tac) 1; |
|
39 |
||
40 |
in |
|
41 |
||
42 |
val export_defs = (disch_defs, fn _ => fn _ => []); |
|
43 |
||
44 |
end; |
|
45 |
||
46 |
||
47 |
(* def(_i) *) |
|
48 |
||
49 |
fun gen_def fix prep_term prep_pats raw_name atts (x, (raw_rhs, raw_pats)) state = |
|
6954 | 50 |
let |
9295 | 51 |
val _ = Proof.assert_forward state; |
9324 | 52 |
val ctxt = Proof.context_of state; |
6954 | 53 |
|
9295 | 54 |
(*rhs*) |
7416 | 55 |
val name = if raw_name = "" then Thm.def_name x else raw_name; |
9295 | 56 |
val rhs = prep_term ctxt raw_rhs; |
6954 | 57 |
val T = Term.fastype_of rhs; |
9295 | 58 |
val pats = prep_pats T (ProofContext.declare_term rhs ctxt) raw_pats; |
59 |
||
60 |
(*lhs*) |
|
9324 | 61 |
val lhs = ProofContext.bind_skolem ctxt [x] (Free (x, T)); |
6954 | 62 |
in |
9324 | 63 |
state |
9467 | 64 |
|> fix [([x], None)] |
8092 | 65 |
|> Proof.match_bind_i [(pats, rhs)] |
10464 | 66 |
|> Proof.assm_i export_defs [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])] |
6954 | 67 |
end; |
68 |
||
8092 | 69 |
val def = gen_def Proof.fix ProofContext.read_term ProofContext.read_term_pats; |
70 |
val def_i = gen_def Proof.fix_i ProofContext.cert_term ProofContext.cert_term_pats; |
|
6954 | 71 |
|
72 |
||
73 |
end; |