6 Local definitions. |
6 Local definitions. |
7 *) |
7 *) |
8 |
8 |
9 signature LOCAL_DEFS = |
9 signature LOCAL_DEFS = |
10 sig |
10 sig |
11 val def: string -> Proof.context attribute list |
11 val def: string -> Proof.context attribute list -> string * (string * string list) |
12 -> (string * string option) * (string * string list) -> Proof.state -> Proof.state |
12 -> Proof.state -> Proof.state |
13 val def_i: string -> Proof.context attribute list |
13 val def_i: string -> Proof.context attribute list -> string * (term * term list) |
14 -> (string * typ option) * (term * term list) -> Proof.state -> Proof.state |
14 -> Proof.state -> Proof.state |
15 end; |
15 end; |
16 |
16 |
17 structure LocalDefs: LOCAL_DEFS = |
17 structure LocalDefs: LOCAL_DEFS = |
18 struct |
18 struct |
19 |
19 |
|
20 |
|
21 (* export_defs *) |
|
22 |
|
23 local |
|
24 |
20 val refl_tac = Tactic.rtac (Drule.standard (Drule.reflexive_thm RS Drule.triv_goal)); |
25 val refl_tac = Tactic.rtac (Drule.standard (Drule.reflexive_thm RS Drule.triv_goal)); |
21 |
26 |
22 fun gen_def fix prep_term prep_pats raw_name atts ((x, raw_T), (raw_rhs, raw_pats)) state = |
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 = |
23 let |
50 let |
24 val _ = Proof.assert_forward state; |
51 val _ = Proof.assert_forward state; |
25 val ctxt = Proof.context_of state; |
52 val ctxt = Proof.context_of state; |
26 |
53 |
27 (*rhs*) |
54 (*rhs*) |
32 |
59 |
33 (*lhs*) |
60 (*lhs*) |
34 val lhs = ProofContext.bind_skolem ctxt [x] (Free (x, T)); |
61 val lhs = ProofContext.bind_skolem ctxt [x] (Free (x, T)); |
35 in |
62 in |
36 state |
63 state |
37 |> fix [([x], raw_T)] |
64 |> fix [([x], None)] |
38 |> Proof.match_bind_i [(pats, rhs)] |
65 |> Proof.match_bind_i [(pats, rhs)] |
39 |> Proof.assm_i (refl_tac, refl_tac) [(name, atts, [(Logic.mk_equals (lhs, rhs), ([], []))])] |
66 |> Proof.assm_i export_defs [(name, atts, [(Logic.mk_equals (lhs, rhs), ([], []))])] |
40 end; |
67 end; |
41 |
68 |
42 val def = gen_def Proof.fix ProofContext.read_term ProofContext.read_term_pats; |
69 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; |
70 val def_i = gen_def Proof.fix_i ProofContext.cert_term ProofContext.cert_term_pats; |
44 |
71 |