author | wenzelm |
Tue, 07 Nov 2006 11:46:48 +0100 | |
changeset 21206 | 2af4c7b3f7ef |
parent 21036 | 0eed532acfca |
child 21230 | abfdce60b371 |
permissions | -rw-r--r-- |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/specification.ML |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
4 |
|
21036 | 5 |
Derived local theory specifications --- with type-inference and |
18810 | 6 |
toplevel polymorphism. |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
7 |
*) |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
8 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
9 |
signature SPECIFICATION = |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
10 |
sig |
20890 | 11 |
val quiet_mode: bool ref |
12 |
val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit |
|
18771 | 13 |
val read_specification: (string * string option * mixfix) list -> |
18954 | 14 |
((string * Attrib.src list) * string list) list -> local_theory -> |
18771 | 15 |
(((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) * |
18954 | 16 |
local_theory |
18771 | 17 |
val cert_specification: (string * typ option * mixfix) list -> |
18954 | 18 |
((string * Attrib.src list) * term list) list -> local_theory -> |
18771 | 19 |
(((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) * |
18954 | 20 |
local_theory |
21 |
val axiomatization: (string * string option * mixfix) list -> |
|
22 |
((bstring * Attrib.src list) * string list) list -> local_theory -> |
|
23 |
(term list * (bstring * thm list) list) * local_theory |
|
24 |
val axiomatization_i: (string * typ option * mixfix) list -> |
|
25 |
((bstring * Attrib.src list) * term list) list -> local_theory -> |
|
26 |
(term list * (bstring * thm list) list) * local_theory |
|
27 |
val definition: |
|
18786 | 28 |
((string * string option * mixfix) option * ((string * Attrib.src list) * string)) list -> |
18954 | 29 |
local_theory -> (term * (bstring * thm)) list * local_theory |
30 |
val definition_i: |
|
18786 | 31 |
((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list -> |
18954 | 32 |
local_theory -> (term * (bstring * thm)) list * local_theory |
20784 | 33 |
val abbreviation: Syntax.mode -> ((string * string option * mixfix) option * string) list -> |
19080 | 34 |
local_theory -> local_theory |
20784 | 35 |
val abbreviation_i: Syntax.mode -> ((string * typ option * mixfix) option * term) list -> |
19080 | 36 |
local_theory -> local_theory |
21206
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21036
diff
changeset
|
37 |
val notation: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory |
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21036
diff
changeset
|
38 |
val notation_i: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
20914 | 39 |
val theorems: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list |
40 |
-> local_theory -> (bstring * thm list) list * local_theory |
|
41 |
val theorems_i: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list |
|
42 |
-> local_theory -> (bstring * thm list) list * local_theory |
|
21036 | 43 |
val theorem: string -> Method.text option -> (thm list list -> local_theory -> local_theory) -> |
44 |
string * Attrib.src list -> Element.context Locale.element list -> Element.statement -> |
|
45 |
local_theory -> Proof.state |
|
46 |
val theorem_i: string -> Method.text option -> (thm list list -> local_theory -> local_theory) -> |
|
47 |
string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i -> |
|
48 |
local_theory -> Proof.state |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
49 |
end; |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
50 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
51 |
structure Specification: SPECIFICATION = |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
52 |
struct |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
53 |
|
20890 | 54 |
(* diagnostics *) |
55 |
||
56 |
val quiet_mode = ref false; |
|
57 |
||
58 |
fun print_consts _ _ [] = () |
|
59 |
| print_consts ctxt pred cs = |
|
60 |
if ! quiet_mode then () else Pretty.writeln (ProofDisplay.pretty_consts ctxt pred cs); |
|
61 |
||
21036 | 62 |
fun present_results ctxt res = |
63 |
if ! quiet_mode then () else ProofDisplay.present_results ctxt res; |
|
64 |
||
65 |
fun present_results' ctxt kind res = present_results ctxt ((kind, ""), res); |
|
20914 | 66 |
|
19664 | 67 |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
68 |
(* prepare specification *) |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
69 |
|
18828 | 70 |
fun prep_specification prep_vars prep_propp prep_att raw_vars raw_specs ctxt = |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
71 |
let |
18670 | 72 |
val thy = ProofContext.theory_of ctxt; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
73 |
|
18670 | 74 |
val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars; |
75 |
val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars; |
|
76 |
val ((specs, vs), specs_ctxt) = |
|
19585 | 77 |
prep_propp (params_ctxt, map (map (rpair []) o snd) raw_specs) |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
78 |
|> swap |>> map (map fst) |
18771 | 79 |
||>> fold_map ProofContext.inferred_param xs; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
80 |
|
18771 | 81 |
val params = vs ~~ map #3 vars; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
82 |
val names = map (fst o fst) raw_specs; |
18670 | 83 |
val atts = map (map (prep_att thy) o snd o fst) raw_specs; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
84 |
in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end; |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
85 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
86 |
fun read_specification x = |
18771 | 87 |
prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.intern_src x; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
88 |
fun cert_specification x = |
18670 | 89 |
prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
90 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
91 |
|
18771 | 92 |
(* axiomatization *) |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
93 |
|
20890 | 94 |
fun gen_axioms prep raw_vars raw_specs lthy = |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
95 |
let |
20890 | 96 |
val (vars, specs) = fst (prep raw_vars raw_specs lthy); |
18828 | 97 |
val cs = map fst vars; |
18880
b8a1c3cdf739
axiomatization: retrict parameters to occurrences in specs;
wenzelm
parents:
18828
diff
changeset
|
98 |
val spec_frees = member (op =) (fold (fold Term.add_frees o snd) specs []); |
18786 | 99 |
|
20890 | 100 |
val ((consts, axioms), lthy') = lthy |
101 |
|> LocalTheory.consts spec_frees vars |
|
20914 | 102 |
||> fold (fold Variable.fix_frees o snd) specs (* FIXME !? *) |
20890 | 103 |
||>> LocalTheory.axioms specs; |
18786 | 104 |
|
20890 | 105 |
(* FIXME generic target!? *) |
106 |
val hs = map (Term.head_of o #2 o Logic.dest_equals o Thm.prop_of o #2) consts; |
|
107 |
val lthy'' = lthy' |> LocalTheory.theory (Theory.add_finals_i false hs); |
|
108 |
||
109 |
val _ = print_consts lthy' spec_frees cs; |
|
110 |
in ((map #1 consts, axioms), lthy'') end; |
|
18786 | 111 |
|
18954 | 112 |
val axiomatization = gen_axioms read_specification; |
113 |
val axiomatization_i = gen_axioms cert_specification; |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
114 |
|
18786 | 115 |
|
116 |
(* definition *) |
|
117 |
||
20890 | 118 |
fun gen_defs prep args lthy = |
18786 | 119 |
let |
20890 | 120 |
fun define (raw_var, (raw_a, raw_prop)) lthy1 = |
18786 | 121 |
let |
20890 | 122 |
val (vars, [((raw_name, atts), [prop])]) = |
123 |
fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy1); |
|
124 |
val (((x, T), rhs), prove) = LocalDefs.derived_def lthy1 true prop; |
|
125 |
val name = Thm.def_name_optional x raw_name; |
|
18786 | 126 |
val mx = (case vars of [] => NoSyn | [((x', _), mx)] => |
127 |
if x = x' then mx |
|
128 |
else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x')); |
|
20890 | 129 |
val ((lhs, (_, th)), lthy2) = lthy1 |
130 |
(* |> LocalTheory.def ((x, mx), ((name ^ "_raw", []), rhs)); FIXME *) |
|
131 |
|> LocalTheory.def ((x, mx), ((name, []), rhs)); |
|
132 |
val ((b, [th']), lthy3) = lthy2 |
|
20914 | 133 |
|> LocalTheory.note ((name, atts), [prove lthy2 th]); |
20890 | 134 |
in (((x, T), (lhs, (b, th'))), LocalTheory.reinit lthy3) end; |
18786 | 135 |
|
20890 | 136 |
val ((cs, defs), lthy') = lthy |> fold_map define args |>> split_list; |
18880
b8a1c3cdf739
axiomatization: retrict parameters to occurrences in specs;
wenzelm
parents:
18828
diff
changeset
|
137 |
val def_frees = member (op =) (fold (Term.add_frees o fst) defs []); |
20890 | 138 |
val _ = print_consts lthy' def_frees cs; |
139 |
in (defs, lthy') end; |
|
18786 | 140 |
|
18954 | 141 |
val definition = gen_defs read_specification; |
142 |
val definition_i = gen_defs cert_specification; |
|
18786 | 143 |
|
19080 | 144 |
|
145 |
(* abbreviation *) |
|
146 |
||
20890 | 147 |
fun gen_abbrevs prep mode args lthy = |
19080 | 148 |
let |
20890 | 149 |
fun abbrev (raw_var, raw_prop) lthy1 = |
19080 | 150 |
let |
19372
3ff5f1777743
abbreviation(_i): do not expand abbreviations, do not use derived_def;
wenzelm
parents:
19080
diff
changeset
|
151 |
val ((vars, [(_, [prop])]), _) = |
3ff5f1777743
abbreviation(_i): do not expand abbreviations, do not use derived_def;
wenzelm
parents:
19080
diff
changeset
|
152 |
prep (the_list raw_var) [(("", []), [raw_prop])] |
20890 | 153 |
(lthy1 |> ProofContext.expand_abbrevs false); |
154 |
val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy1 prop)); |
|
19080 | 155 |
val mx = (case vars of [] => NoSyn | [((x', _), mx)] => |
156 |
if x = x' then mx |
|
157 |
else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote x')); |
|
158 |
in |
|
20890 | 159 |
lthy1 |
19664 | 160 |
|> LocalTheory.abbrevs mode [((x, mx), rhs)] |
19080 | 161 |
|> pair (x, T) |
162 |
end; |
|
163 |
||
20890 | 164 |
val (cs, lthy1) = lthy |
19544 | 165 |
|> ProofContext.set_syntax_mode mode |
166 |
|> fold_map abbrev args |
|
20890 | 167 |
||> ProofContext.restore_syntax_mode lthy; |
168 |
val _ = print_consts lthy1 (K false) cs; |
|
169 |
in lthy1 end; |
|
19080 | 170 |
|
171 |
val abbreviation = gen_abbrevs read_specification; |
|
172 |
val abbreviation_i = gen_abbrevs cert_specification; |
|
173 |
||
19664 | 174 |
|
175 |
(* const syntax *) |
|
176 |
||
21206
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21036
diff
changeset
|
177 |
fun gen_notation prep_const mode args lthy = |
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21036
diff
changeset
|
178 |
lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args); |
19664 | 179 |
|
21206
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21036
diff
changeset
|
180 |
val notation = gen_notation ProofContext.read_const; |
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21036
diff
changeset
|
181 |
val notation_i = gen_notation (K I); |
19664 | 182 |
|
20914 | 183 |
|
21036 | 184 |
(* fact statements *) |
20914 | 185 |
|
186 |
fun gen_theorems prep_thms prep_att kind raw_facts lthy = |
|
187 |
let |
|
188 |
val k = if kind = "" then [] else [Attrib.kind kind]; |
|
189 |
val attrib = prep_att (ProofContext.theory_of lthy); |
|
190 |
val facts = raw_facts |> map (fn ((name, atts), bs) => |
|
191 |
((name, map attrib atts), |
|
192 |
bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts @ k)))); |
|
193 |
val (res, lthy') = lthy |> LocalTheory.notes facts; |
|
21036 | 194 |
val _ = present_results' lthy' kind res; |
20914 | 195 |
in (res, lthy') end; |
196 |
||
197 |
val theorems = gen_theorems ProofContext.get_thms Attrib.intern_src; |
|
198 |
val theorems_i = gen_theorems (K I) (K I); |
|
199 |
||
21036 | 200 |
|
201 |
(* goal statements *) |
|
202 |
||
203 |
local |
|
204 |
||
205 |
val global_goal = |
|
206 |
Proof.global_goal (K (K ())) Attrib.attribute_i ProofContext.bind_propp_schematic_i; |
|
207 |
||
208 |
fun mk_shows prep_att stmt ctxt = |
|
209 |
((Attrib.map_specs prep_att stmt, []), fold (fold (Variable.fix_frees o fst) o snd) stmt ctxt); |
|
210 |
||
211 |
fun conclusion prep_att (Element.Shows concl) = (([], concl), mk_shows prep_att) |
|
212 |
| conclusion _ (Element.Obtains cases) = |
|
213 |
apfst (apfst (map Locale.Elem)) (Obtain.statement cases); |
|
214 |
||
215 |
in |
|
216 |
||
217 |
fun gen_theorem prep_att prep_stmt |
|
218 |
kind before_qed after_qed (name, raw_atts) raw_elems raw_concl lthy0 = |
|
219 |
let |
|
220 |
val _ = LocalTheory.assert lthy0; |
|
221 |
val thy = ProofContext.theory_of lthy0; |
|
21206
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21036
diff
changeset
|
222 |
|
21036 | 223 |
val (loc, ctxt, lthy) = |
224 |
(case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of |
|
225 |
(SOME loc, true) => (* workaround non-modularity of in/includes *) (* FIXME *) |
|
226 |
(warning "Re-initializing theory target for locale inclusion"; |
|
227 |
(SOME loc, ProofContext.init thy, LocalTheory.reinit lthy0)) |
|
228 |
| _ => (NONE, lthy0, lthy0)); |
|
229 |
||
230 |
val attrib = prep_att thy; |
|
231 |
val elem_attrib = Locale.map_elem |
|
232 |
(Element.map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib}); |
|
233 |
||
234 |
val ((concl_elems, concl), mk_stmt) = conclusion attrib raw_concl; |
|
235 |
val elems = map elem_attrib (raw_elems @ concl_elems); |
|
236 |
||
237 |
val (_, _, elems_ctxt, propp) = prep_stmt loc elems (map snd concl) ctxt; |
|
238 |
val ((stmt, facts), goal_ctxt) = mk_stmt (map (apsnd (K []) o fst) concl ~~ propp) elems_ctxt; |
|
239 |
||
240 |
val k = if kind = "" then [] else [Attrib.kind kind]; |
|
241 |
val names = map (fst o fst) concl; |
|
242 |
val attss = map (fn ((_, atts), _) => map attrib atts @ k) concl; |
|
243 |
val atts = map attrib raw_atts @ k; |
|
244 |
||
245 |
fun after_qed' results goal_ctxt' = |
|
246 |
let val results' = burrow (ProofContext.export_standard goal_ctxt' lthy) results in |
|
247 |
lthy |
|
248 |
|> LocalTheory.notes ((names ~~ attss) ~~ map (fn ths => [(ths, [])]) results') |
|
249 |
|> (fn (res, lthy') => |
|
250 |
(present_results lthy' ((kind, name), res); |
|
251 |
if name = "" andalso null raw_atts then lthy' |
|
252 |
else #2 (LocalTheory.notes [((name, atts), [(maps #2 res, [])])] lthy'))) |
|
253 |
|> after_qed results' |
|
254 |
end; |
|
255 |
in |
|
256 |
goal_ctxt |
|
257 |
|> global_goal kind before_qed after_qed' NONE (name, []) stmt |
|
258 |
|> Proof.refine_insert facts |
|
259 |
end; |
|
260 |
||
261 |
val theorem = gen_theorem Attrib.intern_src Locale.read_context_statement_i; |
|
262 |
val theorem_i = gen_theorem (K I) Locale.cert_context_statement; |
|
263 |
||
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
264 |
end; |
21036 | 265 |
|
266 |
end; |