16 |
16 |
17 structure LocalDefs: LOCAL_DEFS = |
17 structure LocalDefs: LOCAL_DEFS = |
18 struct |
18 struct |
19 |
19 |
20 |
20 |
21 (* export_defs *) |
21 (* export_def *) |
22 |
|
23 local |
|
24 |
|
25 val refl_tac = Tactic.rtac (Drule.reflexive_thm RS Drule.triv_goal); |
|
26 |
22 |
27 fun dest_lhs cprop = |
23 fun dest_lhs cprop = |
28 let val x = #1 (Logic.dest_equals (Logic.dest_goal (Thm.term_of cprop))) |
24 let val x = #1 (Logic.dest_equals (Thm.term_of cprop)) |
29 in Term.dest_Free x; Thm.cterm_of (Thm.sign_of_cterm cprop) x end |
25 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" ^ |
26 handle TERM _ => raise TERM ("Malformed definitional assumption encountered:\n" ^ |
31 quote (Display.string_of_cterm cprop), []); |
27 quote (Display.string_of_cterm cprop), []); |
32 |
28 |
33 fun disch_defs cprops thm = |
29 fun export_def _ cprops thm = |
34 thm |
30 thm |
35 |> Drule.implies_intr_list cprops |
31 |> Drule.implies_intr_list cprops |
36 |> Drule.forall_intr_list (map dest_lhs cprops) |
32 |> Drule.forall_intr_list (map dest_lhs cprops) |
37 |> Drule.forall_elim_vars 0 |
33 |> Drule.forall_elim_vars 0 |
38 |> RANGE (replicate (length cprops) refl_tac) 1; |
34 |> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1; |
39 |
|
40 in |
|
41 |
|
42 val export_defs = (disch_defs, fn _ => fn _ => []); |
|
43 |
|
44 end; |
|
45 |
35 |
46 |
36 |
47 (* def(_i) *) |
37 (* def(_i) *) |
48 |
38 |
49 fun gen_def fix prep_term prep_pats raw_name atts (x, (raw_rhs, raw_pats)) state = |
39 fun gen_def fix prep_term prep_pats raw_name atts (x, (raw_rhs, raw_pats)) state = |
61 val lhs = ProofContext.bind_skolem ctxt [x] (Free (x, T)); |
51 val lhs = ProofContext.bind_skolem ctxt [x] (Free (x, T)); |
62 in |
52 in |
63 state |
53 state |
64 |> fix [([x], None)] |
54 |> fix [([x], None)] |
65 |> Proof.match_bind_i [(pats, rhs)] |
55 |> Proof.match_bind_i [(pats, rhs)] |
66 |> Proof.assm_i export_defs [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])] |
56 |> Proof.assm_i export_def [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])] |
67 end; |
57 end; |
68 |
58 |
69 val def = gen_def Proof.fix ProofContext.read_term ProofContext.read_term_pats; |
59 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; |
60 val def_i = gen_def Proof.fix_i ProofContext.cert_term ProofContext.cert_term_pats; |
71 |
61 |