|
1 (* Title: Pure/ex/Def.thy |
|
2 Author: Makarius |
|
3 |
|
4 Primitive constant definition, without fact definition; |
|
5 automatic expansion via Simplifier (simproc). |
|
6 *) |
|
7 |
|
8 theory Def |
|
9 imports Pure |
|
10 keywords "def" :: thy_defn |
|
11 begin |
|
12 |
|
13 ML \<open> |
|
14 signature DEF = |
|
15 sig |
|
16 val get_def: Proof.context -> cterm -> thm option |
|
17 val def: (binding * typ option * mixfix) option -> |
|
18 (binding * typ option * mixfix) list -> term -> local_theory -> term * local_theory |
|
19 val def_cmd: (binding * string option * mixfix) option -> |
|
20 (binding * string option * mixfix) list -> string -> local_theory -> term * local_theory |
|
21 end; |
|
22 |
|
23 structure Def: DEF = |
|
24 struct |
|
25 |
|
26 (* context data *) |
|
27 |
|
28 type def = {lhs: term, mk_eq: morphism -> thm}; |
|
29 |
|
30 val eq_def : def * def -> bool = op aconv o apply2 #lhs; |
|
31 |
|
32 fun transform_def phi ({lhs, mk_eq}: def) = |
|
33 {lhs = Morphism.term phi lhs, mk_eq = Morphism.transform phi mk_eq}; |
|
34 |
|
35 structure Data = Generic_Data |
|
36 ( |
|
37 type T = def Item_Net.T; |
|
38 val empty : T = Item_Net.init eq_def (single o #lhs); |
|
39 val extend = I; |
|
40 val merge = Item_Net.merge; |
|
41 ); |
|
42 |
|
43 fun declare_def lhs eq lthy = |
|
44 let |
|
45 val eq0 = Thm.trim_context eq; |
|
46 val def: def = {lhs = lhs, mk_eq = fn phi => Morphism.thm phi eq0}; |
|
47 in |
|
48 lthy |> Local_Theory.declaration {syntax = false, pervasive = true} |
|
49 (fn phi => (Data.map o Item_Net.update) (transform_def phi def)) |
|
50 end; |
|
51 |
|
52 fun get_def ctxt ct = |
|
53 let |
|
54 val thy = Proof_Context.theory_of ctxt; |
|
55 val data = Data.get (Context.Proof ctxt); |
|
56 val t = Thm.term_of ct; |
|
57 fun match_def {lhs, mk_eq} = |
|
58 if Pattern.matches thy (lhs, t) then |
|
59 let |
|
60 val inst = Thm.match (Thm.cterm_of ctxt lhs, ct); |
|
61 val eq = |
|
62 Morphism.form mk_eq |
|
63 |> Thm.transfer thy |
|
64 |> Thm.instantiate inst; |
|
65 in SOME eq end |
|
66 else NONE; |
|
67 in Item_Net.retrieve_matching data t |> get_first match_def end; |
|
68 |
|
69 |
|
70 (* simproc setup *) |
|
71 |
|
72 val _ = |
|
73 (Theory.setup o Named_Target.theory_map) |
|
74 (Simplifier.define_simproc \<^binding>\<open>expand_def\<close> |
|
75 {lhss = [Free ("x", TFree ("'a", []))], proc = K get_def}); |
|
76 |
|
77 |
|
78 (* Isar command *) |
|
79 |
|
80 fun gen_def prep_spec raw_var raw_params raw_spec lthy = |
|
81 let |
|
82 val ((vars, xs, get_pos, spec), _) = lthy |
|
83 |> prep_spec (the_list raw_var) raw_params [] raw_spec; |
|
84 val (((x, _), rhs), prove) = Local_Defs.derived_def lthy get_pos {conditional = false} spec; |
|
85 val _ = Name.reject_internal (x, []); |
|
86 val (b, mx) = |
|
87 (case (vars, xs) of |
|
88 ([], []) => (Binding.make (x, (case get_pos x of [] => Position.none | p :: _ => p)), NoSyn) |
|
89 | ([(b, _, mx)], [y]) => |
|
90 if x = y then (b, mx) |
|
91 else |
|
92 error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^ |
|
93 Position.here (Binding.pos_of b))); |
|
94 val ((lhs, (_, eq)), lthy') = lthy |
|
95 |> Local_Theory.define_internal ((b, mx), (Binding.empty_atts, rhs)); |
|
96 |
|
97 (*sanity check for original specification*) |
|
98 val _: thm = prove lthy' eq; |
|
99 in (lhs, declare_def lhs eq lthy') end; |
|
100 |
|
101 val def = gen_def Specification.check_spec_open; |
|
102 val def_cmd = gen_def Specification.read_spec_open; |
|
103 |
|
104 val _ = |
|
105 Outer_Syntax.local_theory \<^command_keyword>\<open>def\<close> |
|
106 "primitive constant definition, without fact definition" |
|
107 (Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes |
|
108 >> (fn ((decl, spec), params) => #2 o def_cmd decl params spec)); |
|
109 |
|
110 end; |
|
111 \<close> |
|
112 |
|
113 end |