91 and "extract_type" "extract" :: thy_decl |
91 and "extract_type" "extract" :: thy_decl |
92 and "find_theorems" "find_consts" :: diag |
92 and "find_theorems" "find_consts" :: diag |
93 and "named_theorems" :: thy_decl |
93 and "named_theorems" :: thy_decl |
94 begin |
94 begin |
95 |
95 |
96 ML_file "Isar/isar_syn.ML" |
96 section \<open>Isar commands\<close> |
|
97 |
|
98 ML \<open> |
|
99 local |
|
100 |
|
101 (** theory commands **) |
|
102 |
|
103 (* sorts *) |
|
104 |
|
105 val _ = |
|
106 Outer_Syntax.local_theory @{command_keyword default_sort} |
|
107 "declare default sort for explicit type variables" |
|
108 (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy)); |
|
109 |
|
110 |
|
111 (* types *) |
|
112 |
|
113 val _ = |
|
114 Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration" |
|
115 (Parse.type_args -- Parse.binding -- Parse.opt_mixfix |
|
116 >> (fn ((args, a), mx) => |
|
117 Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd)); |
|
118 |
|
119 val _ = |
|
120 Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation" |
|
121 (Parse.type_args -- Parse.binding -- |
|
122 (@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')) |
|
123 >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)); |
|
124 |
|
125 val _ = |
|
126 Outer_Syntax.command @{command_keyword nonterminal} |
|
127 "declare syntactic type constructors (grammar nonterminal symbols)" |
|
128 (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global)); |
|
129 |
|
130 |
|
131 (* consts and syntax *) |
|
132 |
|
133 val _ = |
|
134 Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment" |
|
135 (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd)); |
|
136 |
|
137 val _ = |
|
138 Outer_Syntax.command @{command_keyword consts} "declare constants" |
|
139 (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd)); |
|
140 |
|
141 val mode_spec = |
|
142 (@{keyword "output"} >> K ("", false)) || |
|
143 Parse.name -- Scan.optional (@{keyword "output"} >> K false) true; |
|
144 |
|
145 val opt_mode = |
|
146 Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default; |
|
147 |
|
148 val _ = |
|
149 Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses" |
|
150 (opt_mode -- Scan.repeat1 Parse.const_decl |
|
151 >> (Toplevel.theory o uncurry Sign.add_syntax_cmd)); |
|
152 |
|
153 val _ = |
|
154 Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses" |
|
155 (opt_mode -- Scan.repeat1 Parse.const_decl |
|
156 >> (Toplevel.theory o uncurry Sign.del_syntax_cmd)); |
|
157 |
|
158 |
|
159 (* translations *) |
|
160 |
|
161 val trans_pat = |
|
162 Scan.optional |
|
163 (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic" |
|
164 -- Parse.inner_syntax Parse.string; |
|
165 |
|
166 fun trans_arrow toks = |
|
167 ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"}) >> K Syntax.Parse_Rule || |
|
168 (@{keyword "\<leftharpoondown>"} || @{keyword "<="}) >> K Syntax.Print_Rule || |
|
169 (@{keyword "\<rightleftharpoons>"} || @{keyword "=="}) >> K Syntax.Parse_Print_Rule) toks; |
|
170 |
|
171 val trans_line = |
|
172 trans_pat -- Parse.!!! (trans_arrow -- trans_pat) |
|
173 >> (fn (left, (arr, right)) => arr (left, right)); |
|
174 |
|
175 val _ = |
|
176 Outer_Syntax.command @{command_keyword translations} "add syntax translation rules" |
|
177 (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations)); |
|
178 |
|
179 val _ = |
|
180 Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules" |
|
181 (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations)); |
|
182 |
|
183 |
|
184 (* constant definitions and abbreviations *) |
|
185 |
|
186 val _ = |
|
187 Outer_Syntax.local_theory' @{command_keyword definition} "constant definition" |
|
188 (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args)); |
|
189 |
|
190 val _ = |
|
191 Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation" |
|
192 (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop) |
|
193 >> (fn (mode, args) => Specification.abbreviation_cmd mode args)); |
|
194 |
|
195 val _ = |
|
196 Outer_Syntax.local_theory @{command_keyword type_notation} |
|
197 "add concrete syntax for type constructors" |
|
198 (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix) |
|
199 >> (fn (mode, args) => Specification.type_notation_cmd true mode args)); |
|
200 |
|
201 val _ = |
|
202 Outer_Syntax.local_theory @{command_keyword no_type_notation} |
|
203 "delete concrete syntax for type constructors" |
|
204 (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix) |
|
205 >> (fn (mode, args) => Specification.type_notation_cmd false mode args)); |
|
206 |
|
207 val _ = |
|
208 Outer_Syntax.local_theory @{command_keyword notation} |
|
209 "add concrete syntax for constants / fixed variables" |
|
210 (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) |
|
211 >> (fn (mode, args) => Specification.notation_cmd true mode args)); |
|
212 |
|
213 val _ = |
|
214 Outer_Syntax.local_theory @{command_keyword no_notation} |
|
215 "delete concrete syntax for constants / fixed variables" |
|
216 (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) |
|
217 >> (fn (mode, args) => Specification.notation_cmd false mode args)); |
|
218 |
|
219 |
|
220 (* constant specifications *) |
|
221 |
|
222 val _ = |
|
223 Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification" |
|
224 (Scan.optional Parse.fixes [] -- |
|
225 Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) [] |
|
226 >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y))); |
|
227 |
|
228 |
|
229 (* theorems *) |
|
230 |
|
231 val _ = |
|
232 Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems" |
|
233 (Parse_Spec.name_facts -- Parse.for_fixes >> |
|
234 (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes)); |
|
235 |
|
236 val _ = |
|
237 Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems" |
|
238 (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes |
|
239 >> (fn (facts, fixes) => |
|
240 #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes)); |
|
241 |
|
242 val _ = |
|
243 Outer_Syntax.local_theory @{command_keyword named_theorems} |
|
244 "declare named collection of theorems" |
|
245 (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >> |
|
246 fold (fn (b, descr) => snd o Named_Theorems.declare b descr)); |
|
247 |
|
248 |
|
249 (* hide names *) |
|
250 |
|
251 local |
|
252 |
|
253 fun hide_names command_keyword what hide parse prep = |
|
254 Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space") |
|
255 ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) => |
|
256 (Toplevel.theory (fn thy => |
|
257 let val ctxt = Proof_Context.init_global thy |
|
258 in fold (hide fully o prep ctxt) args thy end)))); |
|
259 |
|
260 in |
|
261 |
|
262 val _ = |
|
263 hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class |
|
264 Proof_Context.read_class; |
|
265 |
|
266 val _ = |
|
267 hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const |
|
268 ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false}); |
|
269 |
|
270 val _ = |
|
271 hide_names @{command_keyword hide_const} "consts" Sign.hide_const Parse.const |
|
272 ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false}); |
|
273 |
|
274 val _ = |
|
275 hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact |
|
276 (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of); |
|
277 |
|
278 end; |
|
279 |
|
280 |
|
281 (* use ML text *) |
|
282 |
|
283 local |
|
284 |
|
285 fun ML_file_cmd debug files = Toplevel.generic_theory (fn gthy => |
|
286 let |
|
287 val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy); |
|
288 val provide = Resources.provide (src_path, digest); |
|
289 val source = Input.source true (cat_lines lines) (pos, pos); |
|
290 val flags: ML_Compiler.flags = |
|
291 {SML = false, exchange = false, redirect = true, verbose = true, |
|
292 debug = debug, writeln = writeln, warning = warning}; |
|
293 in |
|
294 gthy |
|
295 |> ML_Context.exec (fn () => ML_Context.eval_source flags source) |
|
296 |> Local_Theory.propagate_ml_env |
|
297 |> Context.mapping provide (Local_Theory.background_theory provide) |
|
298 end); |
|
299 |
|
300 fun SML_file_cmd debug files = Toplevel.theory (fn thy => |
|
301 let |
|
302 val ([{lines, pos, ...}: Token.file], thy') = files thy; |
|
303 val source = Input.source true (cat_lines lines) (pos, pos); |
|
304 val flags: ML_Compiler.flags = |
|
305 {SML = true, exchange = false, redirect = true, verbose = true, |
|
306 debug = debug, writeln = writeln, warning = warning}; |
|
307 in |
|
308 thy' |> Context.theory_map |
|
309 (ML_Context.exec (fn () => ML_Context.eval_source flags source)) |
|
310 end); |
|
311 |
|
312 in |
|
313 |
|
314 val _ = |
|
315 Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file" |
|
316 (Resources.parse_files "ML_file" >> ML_file_cmd NONE); |
|
317 |
|
318 val _ = |
|
319 Outer_Syntax.command ("ML_file_debug", @{here}) |
|
320 "read and evaluate Isabelle/ML file (with debugger information)" |
|
321 (Resources.parse_files "ML_file_debug" >> ML_file_cmd (SOME true)); |
|
322 |
|
323 val _ = |
|
324 Outer_Syntax.command ("ML_file_no_debug", @{here}) |
|
325 "read and evaluate Isabelle/ML file (no debugger information)" |
|
326 (Resources.parse_files "ML_file_no_debug" >> ML_file_cmd (SOME false)); |
|
327 |
|
328 val _ = |
|
329 Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file" |
|
330 (Resources.provide_parse_files "SML_file" >> SML_file_cmd NONE); |
|
331 |
|
332 val _ = |
|
333 Outer_Syntax.command @{command_keyword SML_file_debug} |
|
334 "read and evaluate Standard ML file (with debugger information)" |
|
335 (Resources.provide_parse_files "SML_file_debug" >> SML_file_cmd (SOME true)); |
|
336 |
|
337 val _ = |
|
338 Outer_Syntax.command @{command_keyword SML_file_no_debug} |
|
339 "read and evaluate Standard ML file (no debugger information)" |
|
340 (Resources.provide_parse_files "SML_file_no_debug" >> SML_file_cmd (SOME false)); |
|
341 |
|
342 end; |
|
343 |
|
344 val _ = |
|
345 Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment" |
|
346 (Parse.ML_source >> (fn source => |
|
347 let |
|
348 val flags: ML_Compiler.flags = |
|
349 {SML = true, exchange = true, redirect = false, verbose = true, |
|
350 debug = NONE, writeln = writeln, warning = warning}; |
|
351 in |
|
352 Toplevel.theory |
|
353 (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source))) |
|
354 end)); |
|
355 |
|
356 val _ = |
|
357 Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment" |
|
358 (Parse.ML_source >> (fn source => |
|
359 let |
|
360 val flags: ML_Compiler.flags = |
|
361 {SML = false, exchange = true, redirect = false, verbose = true, |
|
362 debug = NONE, writeln = writeln, warning = warning}; |
|
363 in |
|
364 Toplevel.generic_theory |
|
365 (ML_Context.exec (fn () => ML_Context.eval_source flags source) #> |
|
366 Local_Theory.propagate_ml_env) |
|
367 end)); |
|
368 |
|
369 val _ = |
|
370 Outer_Syntax.command @{command_keyword ML_prf} "ML text within proof" |
|
371 (Parse.ML_source >> (fn source => |
|
372 Toplevel.proof (Proof.map_context (Context.proof_map |
|
373 (ML_Context.exec (fn () => |
|
374 ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #> |
|
375 Proof.propagate_ml_env))); |
|
376 |
|
377 val _ = |
|
378 Outer_Syntax.command @{command_keyword ML_val} "diagnostic ML text" |
|
379 (Parse.ML_source >> Isar_Cmd.ml_diag true); |
|
380 |
|
381 val _ = |
|
382 Outer_Syntax.command @{command_keyword ML_command} "diagnostic ML text (silent)" |
|
383 (Parse.ML_source >> Isar_Cmd.ml_diag false); |
|
384 |
|
385 val _ = |
|
386 Outer_Syntax.command @{command_keyword setup} "ML setup for global theory" |
|
387 (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup)); |
|
388 |
|
389 val _ = |
|
390 Outer_Syntax.local_theory @{command_keyword local_setup} "ML setup for local theory" |
|
391 (Parse.ML_source >> Isar_Cmd.local_setup); |
|
392 |
|
393 val _ = |
|
394 Outer_Syntax.local_theory @{command_keyword attribute_setup} "define attribute in ML" |
|
395 (Parse.position Parse.name -- |
|
396 Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "") |
|
397 >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt)); |
|
398 |
|
399 val _ = |
|
400 Outer_Syntax.local_theory @{command_keyword method_setup} "define proof method in ML" |
|
401 (Parse.position Parse.name -- |
|
402 Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "") |
|
403 >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt)); |
|
404 |
|
405 val _ = |
|
406 Outer_Syntax.local_theory @{command_keyword declaration} "generic ML declaration" |
|
407 (Parse.opt_keyword "pervasive" -- Parse.ML_source |
|
408 >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt)); |
|
409 |
|
410 val _ = |
|
411 Outer_Syntax.local_theory @{command_keyword syntax_declaration} "generic ML syntax declaration" |
|
412 (Parse.opt_keyword "pervasive" -- Parse.ML_source |
|
413 >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt)); |
|
414 |
|
415 val _ = |
|
416 Outer_Syntax.local_theory @{command_keyword simproc_setup} "define simproc in ML" |
|
417 (Parse.position Parse.name -- |
|
418 (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword "="}) -- |
|
419 Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) [] |
|
420 >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d)); |
|
421 |
|
422 |
|
423 (* translation functions *) |
|
424 |
|
425 val _ = |
|
426 Outer_Syntax.command @{command_keyword parse_ast_translation} |
|
427 "install parse ast translation functions" |
|
428 (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation)); |
|
429 |
|
430 val _ = |
|
431 Outer_Syntax.command @{command_keyword parse_translation} |
|
432 "install parse translation functions" |
|
433 (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation)); |
|
434 |
|
435 val _ = |
|
436 Outer_Syntax.command @{command_keyword print_translation} |
|
437 "install print translation functions" |
|
438 (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation)); |
|
439 |
|
440 val _ = |
|
441 Outer_Syntax.command @{command_keyword typed_print_translation} |
|
442 "install typed print translation functions" |
|
443 (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation)); |
|
444 |
|
445 val _ = |
|
446 Outer_Syntax.command @{command_keyword print_ast_translation} |
|
447 "install print ast translation functions" |
|
448 (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation)); |
|
449 |
|
450 |
|
451 (* oracles *) |
|
452 |
|
453 val _ = |
|
454 Outer_Syntax.command @{command_keyword oracle} "declare oracle" |
|
455 (Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >> |
|
456 (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y))); |
|
457 |
|
458 |
|
459 (* bundled declarations *) |
|
460 |
|
461 val _ = |
|
462 Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations" |
|
463 ((Parse.binding --| @{keyword "="}) -- Parse.xthms1 -- Parse.for_fixes |
|
464 >> (uncurry Bundle.bundle_cmd)); |
|
465 |
|
466 val _ = |
|
467 Outer_Syntax.command @{command_keyword include} |
|
468 "include declarations from bundle in proof body" |
|
469 (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.include_cmd)); |
|
470 |
|
471 val _ = |
|
472 Outer_Syntax.command @{command_keyword including} |
|
473 "include declarations from bundle in goal refinement" |
|
474 (Scan.repeat1 (Parse.position Parse.xname) >> (Toplevel.proof o Bundle.including_cmd)); |
|
475 |
|
476 val _ = |
|
477 Outer_Syntax.command @{command_keyword print_bundles} |
|
478 "print bundles of declarations" |
|
479 (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of))); |
|
480 |
|
481 |
|
482 (* local theories *) |
|
483 |
|
484 val _ = |
|
485 Outer_Syntax.command @{command_keyword context} "begin local theory context" |
|
486 ((Parse.position Parse.xname >> (fn name => |
|
487 Toplevel.begin_local_theory true (Named_Target.begin name)) || |
|
488 Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element |
|
489 >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems))) |
|
490 --| Parse.begin); |
|
491 |
|
492 |
|
493 (* locales *) |
|
494 |
|
495 val locale_val = |
|
496 Parse_Spec.locale_expression -- |
|
497 Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] || |
|
498 Scan.repeat1 Parse_Spec.context_element >> pair ([], []); |
|
499 |
|
500 val _ = |
|
501 Outer_Syntax.command @{command_keyword locale} "define named specification context" |
|
502 (Parse.binding -- |
|
503 Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin |
|
504 >> (fn ((name, (expr, elems)), begin) => |
|
505 Toplevel.begin_local_theory begin |
|
506 (Expression.add_locale_cmd name Binding.empty expr elems #> snd))); |
|
507 |
|
508 val _ = |
|
509 Outer_Syntax.command @{command_keyword experiment} "open private specification context" |
|
510 (Scan.repeat Parse_Spec.context_element --| Parse.begin |
|
511 >> (fn elems => |
|
512 Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd))); |
|
513 |
|
514 val interpretation_args = |
|
515 Parse.!!! Parse_Spec.locale_expression -- |
|
516 Scan.optional |
|
517 (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []; |
|
518 |
|
519 val _ = |
|
520 Outer_Syntax.command @{command_keyword interpret} |
|
521 "prove interpretation of locale expression in proof context" |
|
522 (interpretation_args >> (fn (expr, equations) => |
|
523 Toplevel.proof (Interpretation.interpret_cmd expr equations))); |
|
524 |
|
525 val interpretation_args_with_defs = |
|
526 Parse.!!! Parse_Spec.locale_expression -- |
|
527 (Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" |
|
528 -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] -- |
|
529 Scan.optional |
|
530 (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []); |
|
531 |
|
532 val _ = |
|
533 Outer_Syntax.local_theory_to_proof @{command_keyword global_interpretation} |
|
534 "prove interpretation of locale expression into global theory" |
|
535 (interpretation_args_with_defs |
|
536 >> (fn (expr, (defs, equations)) => Interpretation.global_interpretation_cmd expr defs equations)); |
|
537 |
|
538 val _ = |
|
539 Outer_Syntax.command @{command_keyword sublocale} |
|
540 "prove sublocale relation between a locale and a locale expression" |
|
541 ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) -- |
|
542 interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) => |
|
543 Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations))) |
|
544 || interpretation_args_with_defs >> (fn (expr, (defs, equations)) => |
|
545 Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs equations))); |
|
546 |
|
547 val _ = |
|
548 Outer_Syntax.command @{command_keyword interpretation} |
|
549 "prove interpretation of locale expression in local theory or into global theory" |
|
550 (interpretation_args >> (fn (expr, equations) => |
|
551 Toplevel.local_theory_to_proof NONE NONE (Interpretation.isar_interpretation_cmd expr equations))); |
|
552 |
|
553 |
|
554 |
|
555 (* classes *) |
|
556 |
|
557 val class_val = |
|
558 Parse_Spec.class_expression -- |
|
559 Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] || |
|
560 Scan.repeat1 Parse_Spec.context_element >> pair []; |
|
561 |
|
562 val _ = |
|
563 Outer_Syntax.command @{command_keyword class} "define type class" |
|
564 (Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin |
|
565 >> (fn ((name, (supclasses, elems)), begin) => |
|
566 Toplevel.begin_local_theory begin |
|
567 (Class_Declaration.class_cmd name supclasses elems #> snd))); |
|
568 |
|
569 val _ = |
|
570 Outer_Syntax.local_theory_to_proof @{command_keyword subclass} "prove a subclass relation" |
|
571 (Parse.class >> Class_Declaration.subclass_cmd); |
|
572 |
|
573 val _ = |
|
574 Outer_Syntax.command @{command_keyword instantiation} "instantiate and prove type arity" |
|
575 (Parse.multi_arity --| Parse.begin |
|
576 >> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities))); |
|
577 |
|
578 val _ = |
|
579 Outer_Syntax.command @{command_keyword instance} "prove type arity or subclass relation" |
|
580 ((Parse.class -- |
|
581 ((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd || |
|
582 Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof || |
|
583 Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I))); |
|
584 |
|
585 |
|
586 (* arbitrary overloading *) |
|
587 |
|
588 val _ = |
|
589 Outer_Syntax.command @{command_keyword overloading} "overloaded definitions" |
|
590 (Scan.repeat1 (Parse.name --| (@{keyword "=="} || @{keyword "\<equiv>"}) -- Parse.term -- |
|
591 Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true |
|
592 >> Scan.triple1) --| Parse.begin |
|
593 >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations))); |
|
594 |
|
595 |
|
596 (* code generation *) |
|
597 |
|
598 val _ = |
|
599 Outer_Syntax.command @{command_keyword code_datatype} |
|
600 "define set of code datatype constructors" |
|
601 (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd)); |
|
602 |
|
603 |
|
604 |
|
605 (** proof commands **) |
|
606 |
|
607 val _ = |
|
608 Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context" |
|
609 (Parse.begin >> K Proof.begin_notepad); |
|
610 |
|
611 |
|
612 (* statements *) |
|
613 |
|
614 val structured_statement = |
|
615 Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes |
|
616 >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows)); |
|
617 |
|
618 val structured_statement' = |
|
619 Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes |
|
620 >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows)); |
|
621 |
|
622 |
|
623 fun theorem spec schematic descr = |
|
624 Outer_Syntax.local_theory_to_proof' spec |
|
625 ("state " ^ descr) |
|
626 (Scan.optional (Parse_Spec.opt_thm_name ":" --| |
|
627 Scan.ahead (Parse_Spec.includes >> K "" || |
|
628 Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding -- |
|
629 Scan.optional Parse_Spec.includes [] -- |
|
630 Parse_Spec.general_statement >> (fn ((a, includes), (elems, concl)) => |
|
631 ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) |
|
632 Thm.theoremK NONE (K I) a includes elems concl))); |
|
633 |
|
634 val _ = theorem @{command_keyword theorem} false "theorem"; |
|
635 val _ = theorem @{command_keyword lemma} false "lemma"; |
|
636 val _ = theorem @{command_keyword corollary} false "corollary"; |
|
637 val _ = theorem @{command_keyword proposition} false "proposition"; |
|
638 val _ = theorem @{command_keyword schematic_goal} true "schematic goal"; |
|
639 |
|
640 |
|
641 val _ = |
|
642 Outer_Syntax.command @{command_keyword have} "state local goal" |
|
643 (structured_statement >> (fn (a, b, c, d) => |
|
644 Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2))); |
|
645 |
|
646 val _ = |
|
647 Outer_Syntax.command @{command_keyword show} "state local goal, to refine pending subgoals" |
|
648 (structured_statement >> (fn (a, b, c, d) => |
|
649 Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2))); |
|
650 |
|
651 val _ = |
|
652 Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\"" |
|
653 (structured_statement >> (fn (a, b, c, d) => |
|
654 Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2))); |
|
655 |
|
656 val _ = |
|
657 Outer_Syntax.command @{command_keyword thus} "old-style alias of \"then show\"" |
|
658 (structured_statement >> (fn (a, b, c, d) => |
|
659 Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2))); |
|
660 |
|
661 |
|
662 (* facts *) |
|
663 |
|
664 val facts = Parse.and_list1 Parse.xthms1; |
|
665 |
|
666 val _ = |
|
667 Outer_Syntax.command @{command_keyword then} "forward chaining" |
|
668 (Scan.succeed (Toplevel.proof Proof.chain)); |
|
669 |
|
670 val _ = |
|
671 Outer_Syntax.command @{command_keyword from} "forward chaining from given facts" |
|
672 (facts >> (Toplevel.proof o Proof.from_thmss_cmd)); |
|
673 |
|
674 val _ = |
|
675 Outer_Syntax.command @{command_keyword with} "forward chaining from given and current facts" |
|
676 (facts >> (Toplevel.proof o Proof.with_thmss_cmd)); |
|
677 |
|
678 val _ = |
|
679 Outer_Syntax.command @{command_keyword note} "define facts" |
|
680 (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd)); |
|
681 |
|
682 val _ = |
|
683 Outer_Syntax.command @{command_keyword supply} "define facts during goal refinement (unstructured)" |
|
684 (Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd)); |
|
685 |
|
686 val _ = |
|
687 Outer_Syntax.command @{command_keyword using} "augment goal facts" |
|
688 (facts >> (Toplevel.proof o Proof.using_cmd)); |
|
689 |
|
690 val _ = |
|
691 Outer_Syntax.command @{command_keyword unfolding} "unfold definitions in goal and facts" |
|
692 (facts >> (Toplevel.proof o Proof.unfolding_cmd)); |
|
693 |
|
694 |
|
695 (* proof context *) |
|
696 |
|
697 val _ = |
|
698 Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)" |
|
699 (Parse.fixes >> (Toplevel.proof o Proof.fix_cmd)); |
|
700 |
|
701 val _ = |
|
702 Outer_Syntax.command @{command_keyword assume} "assume propositions" |
|
703 (structured_statement' >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c))); |
|
704 |
|
705 val _ = |
|
706 Outer_Syntax.command @{command_keyword presume} "assume propositions, to be established later" |
|
707 (structured_statement' >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c))); |
|
708 |
|
709 val _ = |
|
710 Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)" |
|
711 (Parse.and_list1 |
|
712 (Parse_Spec.opt_thm_name ":" -- |
|
713 ((Parse.binding -- Parse.opt_mixfix) -- |
|
714 ((@{keyword "\<equiv>"} || @{keyword "=="}) |-- Parse.!!! Parse.termp))) |
|
715 >> (Toplevel.proof o Proof.def_cmd)); |
|
716 |
|
717 val _ = |
|
718 Outer_Syntax.command @{command_keyword consider} "state cases rule" |
|
719 (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd)); |
|
720 |
|
721 val _ = |
|
722 Outer_Syntax.command @{command_keyword obtain} "generalized elimination" |
|
723 (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement |
|
724 >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z))); |
|
725 |
|
726 val _ = |
|
727 Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)" |
|
728 (Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd)); |
|
729 |
|
730 val _ = |
|
731 Outer_Syntax.command @{command_keyword let} "bind text variables" |
|
732 (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term)) |
|
733 >> (Toplevel.proof o Proof.let_bind_cmd)); |
|
734 |
|
735 val _ = |
|
736 Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables" |
|
737 (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) |
|
738 >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args))); |
|
739 |
|
740 val _ = |
|
741 Outer_Syntax.command @{command_keyword case} "invoke local context" |
|
742 (Parse_Spec.opt_thm_name ":" -- |
|
743 (@{keyword "("} |-- |
|
744 Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding) |
|
745 --| @{keyword ")"}) || |
|
746 Parse.position Parse.xname >> rpair []) >> (Toplevel.proof o Proof.case_cmd)); |
|
747 |
|
748 |
|
749 (* proof structure *) |
|
750 |
|
751 val _ = |
|
752 Outer_Syntax.command @{command_keyword "{"} "begin explicit proof block" |
|
753 (Scan.succeed (Toplevel.proof Proof.begin_block)); |
|
754 |
|
755 val _ = |
|
756 Outer_Syntax.command @{command_keyword "}"} "end explicit proof block" |
|
757 (Scan.succeed (Toplevel.proof Proof.end_block)); |
|
758 |
|
759 val _ = |
|
760 Outer_Syntax.command @{command_keyword next} "enter next proof block" |
|
761 (Scan.succeed (Toplevel.proof Proof.next_block)); |
|
762 |
|
763 |
|
764 (* end proof *) |
|
765 |
|
766 val _ = |
|
767 Outer_Syntax.command @{command_keyword qed} "conclude proof" |
|
768 (Scan.option Method.parse >> (fn m => |
|
769 (Option.map Method.report m; |
|
770 Isar_Cmd.qed m))); |
|
771 |
|
772 val _ = |
|
773 Outer_Syntax.command @{command_keyword by} "terminal backward proof" |
|
774 (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) => |
|
775 (Method.report m1; |
|
776 Option.map Method.report m2; |
|
777 Isar_Cmd.terminal_proof (m1, m2)))); |
|
778 |
|
779 val _ = |
|
780 Outer_Syntax.command @{command_keyword ".."} "default proof" |
|
781 (Scan.succeed Isar_Cmd.default_proof); |
|
782 |
|
783 val _ = |
|
784 Outer_Syntax.command @{command_keyword "."} "immediate proof" |
|
785 (Scan.succeed Isar_Cmd.immediate_proof); |
|
786 |
|
787 val _ = |
|
788 Outer_Syntax.command @{command_keyword done} "done proof" |
|
789 (Scan.succeed Isar_Cmd.done_proof); |
|
790 |
|
791 val _ = |
|
792 Outer_Syntax.command @{command_keyword sorry} "skip proof (quick-and-dirty mode only!)" |
|
793 (Scan.succeed Isar_Cmd.skip_proof); |
|
794 |
|
795 val _ = |
|
796 Outer_Syntax.command @{command_keyword "\<proof>"} "dummy proof (quick-and-dirty mode only!)" |
|
797 (Scan.succeed Isar_Cmd.skip_proof); |
|
798 |
|
799 val _ = |
|
800 Outer_Syntax.command @{command_keyword oops} "forget proof" |
|
801 (Scan.succeed (Toplevel.forget_proof true)); |
|
802 |
|
803 |
|
804 (* proof steps *) |
|
805 |
|
806 val _ = |
|
807 Outer_Syntax.command @{command_keyword defer} "shuffle internal proof state" |
|
808 (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer)); |
|
809 |
|
810 val _ = |
|
811 Outer_Syntax.command @{command_keyword prefer} "shuffle internal proof state" |
|
812 (Parse.nat >> (Toplevel.proof o Proof.prefer)); |
|
813 |
|
814 val _ = |
|
815 Outer_Syntax.command @{command_keyword apply} "initial goal refinement step (unstructured)" |
|
816 (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m)))); |
|
817 |
|
818 val _ = |
|
819 Outer_Syntax.command @{command_keyword apply_end} "terminal goal refinement step (unstructured)" |
|
820 (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m)))); |
|
821 |
|
822 val _ = |
|
823 Outer_Syntax.command @{command_keyword proof} "backward proof step" |
|
824 (Scan.option Method.parse >> (fn m => |
|
825 (Option.map Method.report m; Toplevel.proofs (Proof.proof m)))); |
|
826 |
|
827 |
|
828 (* subgoal focus *) |
|
829 |
|
830 local |
|
831 |
|
832 val opt_fact_binding = |
|
833 Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) |
|
834 Attrib.empty_binding; |
|
835 |
|
836 val for_params = |
|
837 Scan.optional |
|
838 (@{keyword "for"} |-- |
|
839 Parse.!!! ((Scan.option Parse.dots >> is_some) -- |
|
840 (Scan.repeat1 (Parse.position (Parse.maybe Parse.name))))) |
|
841 (false, []); |
|
842 |
|
843 in |
|
844 |
|
845 val _ = |
|
846 Outer_Syntax.command @{command_keyword subgoal} |
|
847 "focus on first subgoal within backward refinement" |
|
848 (opt_fact_binding -- (Scan.option (@{keyword "premises"} |-- Parse.!!! opt_fact_binding)) -- |
|
849 for_params >> (fn ((a, b), c) => |
|
850 Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c))); |
|
851 |
|
852 end; |
|
853 |
|
854 |
|
855 (* calculation *) |
|
856 |
|
857 val calculation_args = |
|
858 Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"}))); |
|
859 |
|
860 val _ = |
|
861 Outer_Syntax.command @{command_keyword also} "combine calculation and current facts" |
|
862 (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd)); |
|
863 |
|
864 val _ = |
|
865 Outer_Syntax.command @{command_keyword finally} |
|
866 "combine calculation and current facts, exhibit result" |
|
867 (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd)); |
|
868 |
|
869 val _ = |
|
870 Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts" |
|
871 (Scan.succeed (Toplevel.proof' Calculation.moreover)); |
|
872 |
|
873 val _ = |
|
874 Outer_Syntax.command @{command_keyword ultimately} |
|
875 "augment calculation by current facts, exhibit result" |
|
876 (Scan.succeed (Toplevel.proof' Calculation.ultimately)); |
|
877 |
|
878 val _ = |
|
879 Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules" |
|
880 (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of))); |
|
881 |
|
882 |
|
883 (* proof navigation *) |
|
884 |
|
885 fun report_back () = |
|
886 Output.report [Markup.markup Markup.bad "Explicit backtracking"]; |
|
887 |
|
888 val _ = |
|
889 Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command" |
|
890 (Scan.succeed |
|
891 (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o |
|
892 Toplevel.skip_proof report_back)); |
|
893 |
|
894 |
|
895 |
|
896 (** diagnostic commands (for interactive mode only) **) |
|
897 |
|
898 val opt_modes = |
|
899 Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []; |
|
900 |
|
901 val _ = |
|
902 Outer_Syntax.command @{command_keyword help} |
|
903 "retrieve outer syntax commands according to name patterns" |
|
904 (Scan.repeat Parse.name >> |
|
905 (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats))); |
|
906 |
|
907 val _ = |
|
908 Outer_Syntax.command @{command_keyword print_commands} "print outer syntax commands" |
|
909 (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of))); |
|
910 |
|
911 val _ = |
|
912 Outer_Syntax.command @{command_keyword print_options} "print configuration options" |
|
913 (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of))); |
|
914 |
|
915 val _ = |
|
916 Outer_Syntax.command @{command_keyword print_context} |
|
917 "print context of local theory target" |
|
918 (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context))); |
|
919 |
|
920 val _ = |
|
921 Outer_Syntax.command @{command_keyword print_theory} |
|
922 "print logical theory contents" |
|
923 (Parse.opt_bang >> (fn b => |
|
924 Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of))); |
|
925 |
|
926 val _ = |
|
927 Outer_Syntax.command @{command_keyword print_definitions} |
|
928 "print dependencies of definitional theory content" |
|
929 (Parse.opt_bang >> (fn b => |
|
930 Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of))); |
|
931 |
|
932 val _ = |
|
933 Outer_Syntax.command @{command_keyword print_syntax} |
|
934 "print inner syntax of context" |
|
935 (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of))); |
|
936 |
|
937 val _ = |
|
938 Outer_Syntax.command @{command_keyword print_defn_rules} |
|
939 "print definitional rewrite rules of context" |
|
940 (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of))); |
|
941 |
|
942 val _ = |
|
943 Outer_Syntax.command @{command_keyword print_abbrevs} |
|
944 "print constant abbreviations of context" |
|
945 (Parse.opt_bang >> (fn b => |
|
946 Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of))); |
|
947 |
|
948 val _ = |
|
949 Outer_Syntax.command @{command_keyword print_theorems} |
|
950 "print theorems of local theory or proof context" |
|
951 (Parse.opt_bang >> (fn b => |
|
952 Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b))); |
|
953 |
|
954 val _ = |
|
955 Outer_Syntax.command @{command_keyword print_locales} |
|
956 "print locales of this theory" |
|
957 (Parse.opt_bang >> (fn b => |
|
958 Toplevel.keep (Locale.print_locales b o Toplevel.theory_of))); |
|
959 |
|
960 val _ = |
|
961 Outer_Syntax.command @{command_keyword print_classes} |
|
962 "print classes of this theory" |
|
963 (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of))); |
|
964 |
|
965 val _ = |
|
966 Outer_Syntax.command @{command_keyword print_locale} |
|
967 "print locale of this theory" |
|
968 (Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) => |
|
969 Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name))); |
|
970 |
|
971 val _ = |
|
972 Outer_Syntax.command @{command_keyword print_interps} |
|
973 "print interpretations of locale for this theory or proof context" |
|
974 (Parse.position Parse.xname >> (fn name => |
|
975 Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name))); |
|
976 |
|
977 val _ = |
|
978 Outer_Syntax.command @{command_keyword print_dependencies} |
|
979 "print dependencies of locale expression" |
|
980 (Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (b, expr) => |
|
981 Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr))); |
|
982 |
|
983 val _ = |
|
984 Outer_Syntax.command @{command_keyword print_attributes} |
|
985 "print attributes of this theory" |
|
986 (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of))); |
|
987 |
|
988 val _ = |
|
989 Outer_Syntax.command @{command_keyword print_simpset} |
|
990 "print context of Simplifier" |
|
991 (Parse.opt_bang >> (fn b => |
|
992 Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of))); |
|
993 |
|
994 val _ = |
|
995 Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules" |
|
996 (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of))); |
|
997 |
|
998 val _ = |
|
999 Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory" |
|
1000 (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of))); |
|
1001 |
|
1002 val _ = |
|
1003 Outer_Syntax.command @{command_keyword print_antiquotations} |
|
1004 "print document antiquotations" |
|
1005 (Parse.opt_bang >> (fn b => |
|
1006 Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of))); |
|
1007 |
|
1008 val _ = |
|
1009 Outer_Syntax.command @{command_keyword print_ML_antiquotations} |
|
1010 "print ML antiquotations" |
|
1011 (Parse.opt_bang >> (fn b => |
|
1012 Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of))); |
|
1013 |
|
1014 val _ = |
|
1015 Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies" |
|
1016 (Scan.succeed |
|
1017 (Toplevel.keep (Toplevel.theory_of #> (fn thy => |
|
1018 Locale.pretty_locale_deps thy |
|
1019 |> map (fn {name, parents, body} => |
|
1020 ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents)) |
|
1021 |> Graph_Display.display_graph_old)))); |
|
1022 |
|
1023 val _ = |
|
1024 Outer_Syntax.command @{command_keyword print_term_bindings} |
|
1025 "print term bindings of proof context" |
|
1026 (Scan.succeed |
|
1027 (Toplevel.keep |
|
1028 (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of))); |
|
1029 |
|
1030 val _ = |
|
1031 Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context" |
|
1032 (Parse.opt_bang >> (fn b => |
|
1033 Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of))); |
|
1034 |
|
1035 val _ = |
|
1036 Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context" |
|
1037 (Scan.succeed |
|
1038 (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of))); |
|
1039 |
|
1040 val _ = |
|
1041 Outer_Syntax.command @{command_keyword print_statement} |
|
1042 "print theorems as long statements" |
|
1043 (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_stmts); |
|
1044 |
|
1045 val _ = |
|
1046 Outer_Syntax.command @{command_keyword thm} "print theorems" |
|
1047 (opt_modes -- Parse.xthms1 >> Isar_Cmd.print_thms); |
|
1048 |
|
1049 val _ = |
|
1050 Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems" |
|
1051 (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs false); |
|
1052 |
|
1053 val _ = |
|
1054 Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems" |
|
1055 (opt_modes -- Scan.option Parse.xthms1 >> Isar_Cmd.print_prfs true); |
|
1056 |
|
1057 val _ = |
|
1058 Outer_Syntax.command @{command_keyword prop} "read and print proposition" |
|
1059 (opt_modes -- Parse.term >> Isar_Cmd.print_prop); |
|
1060 |
|
1061 val _ = |
|
1062 Outer_Syntax.command @{command_keyword term} "read and print term" |
|
1063 (opt_modes -- Parse.term >> Isar_Cmd.print_term); |
|
1064 |
|
1065 val _ = |
|
1066 Outer_Syntax.command @{command_keyword typ} "read and print type" |
|
1067 (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort)) |
|
1068 >> Isar_Cmd.print_type); |
|
1069 |
|
1070 val _ = |
|
1071 Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup" |
|
1072 (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of))); |
|
1073 |
|
1074 val _ = |
|
1075 Outer_Syntax.command @{command_keyword print_state} |
|
1076 "print current proof state (if present)" |
|
1077 (opt_modes >> (fn modes => |
|
1078 Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state)))); |
|
1079 |
|
1080 val _ = |
|
1081 Outer_Syntax.command @{command_keyword welcome} "print welcome message" |
|
1082 (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ())))); |
|
1083 |
|
1084 val _ = |
|
1085 Outer_Syntax.command @{command_keyword display_drafts} |
|
1086 "display raw source files with symbols" |
|
1087 (Scan.repeat1 Parse.path >> (fn names => |
|
1088 Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names))))); |
|
1089 |
|
1090 |
|
1091 (* deps *) |
|
1092 |
|
1093 local |
|
1094 val theory_bounds = |
|
1095 Parse.position Parse.theory_xname >> single || |
|
1096 (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"}); |
|
1097 in |
|
1098 |
|
1099 val _ = |
|
1100 Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies" |
|
1101 (Scan.option theory_bounds -- Scan.option theory_bounds >> |
|
1102 (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args))); |
|
1103 |
|
1104 end; |
|
1105 |
|
1106 local |
|
1107 val class_bounds = |
|
1108 Parse.sort >> single || |
|
1109 (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"}); |
|
1110 in |
|
1111 |
|
1112 val _ = |
|
1113 Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies" |
|
1114 (Scan.option class_bounds -- Scan.option class_bounds >> (fn args => |
|
1115 Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args))); |
|
1116 |
|
1117 end; |
|
1118 |
|
1119 val _ = |
|
1120 Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies" |
|
1121 (Parse.xthms1 >> (fn args => |
|
1122 Toplevel.keep (fn st => |
|
1123 Thm_Deps.thm_deps (Toplevel.theory_of st) |
|
1124 (Attrib.eval_thms (Toplevel.context_of st) args)))); |
|
1125 |
|
1126 local |
|
1127 val thy_names = |
|
1128 Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname)); |
|
1129 in |
|
1130 |
|
1131 val _ = |
|
1132 Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems" |
|
1133 (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range => |
|
1134 Toplevel.keep (fn st => |
|
1135 let |
|
1136 val thy = Toplevel.theory_of st; |
|
1137 val ctxt = Toplevel.context_of st; |
|
1138 fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]); |
|
1139 val check = Theory.check ctxt; |
|
1140 in |
|
1141 Thm_Deps.unused_thms |
|
1142 (case opt_range of |
|
1143 NONE => (Theory.parents_of thy, [thy]) |
|
1144 | SOME (xs, NONE) => (map check xs, [thy]) |
|
1145 | SOME (xs, SOME ys) => (map check xs, map check ys)) |
|
1146 |> map pretty_thm |> Pretty.writeln_chunks |
|
1147 end))); |
|
1148 |
|
1149 end; |
|
1150 |
|
1151 |
|
1152 (* find *) |
|
1153 |
|
1154 val _ = |
|
1155 Outer_Syntax.command @{command_keyword find_consts} |
|
1156 "find constants by name / type patterns" |
|
1157 (Find_Consts.query_parser >> (fn spec => |
|
1158 Toplevel.keep (fn st => |
|
1159 Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec)))); |
|
1160 |
|
1161 local |
|
1162 val options = |
|
1163 Scan.optional |
|
1164 (Parse.$$$ "(" |-- |
|
1165 Parse.!!! (Scan.option Parse.nat -- |
|
1166 Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")")) |
|
1167 (NONE, true); |
|
1168 in |
|
1169 |
|
1170 val _ = |
|
1171 Outer_Syntax.command @{command_keyword find_theorems} |
|
1172 "find theorems meeting specified criteria" |
|
1173 (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) => |
|
1174 Toplevel.keep (fn st => |
|
1175 Pretty.writeln |
|
1176 (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec)))); |
|
1177 |
|
1178 end; |
|
1179 |
|
1180 |
|
1181 |
|
1182 (** extraction of programs from proofs **) |
|
1183 |
|
1184 val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") []; |
|
1185 |
|
1186 val _ = |
|
1187 Outer_Syntax.command @{command_keyword realizers} |
|
1188 "specify realizers for primitive axioms / theorems, together with correctness proof" |
|
1189 (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >> |
|
1190 (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers |
|
1191 (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy))); |
|
1192 |
|
1193 val _ = |
|
1194 Outer_Syntax.command @{command_keyword realizability} |
|
1195 "add equations characterizing realizability" |
|
1196 (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns)); |
|
1197 |
|
1198 val _ = |
|
1199 Outer_Syntax.command @{command_keyword extract_type} |
|
1200 "add equations characterizing type of extracted program" |
|
1201 (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns)); |
|
1202 |
|
1203 val _ = |
|
1204 Outer_Syntax.command @{command_keyword extract} "extract terms from proofs" |
|
1205 (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy => |
|
1206 Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy))); |
|
1207 |
|
1208 |
|
1209 |
|
1210 (** end **) |
|
1211 |
|
1212 val _ = |
|
1213 Outer_Syntax.command @{command_keyword end} "end context" |
|
1214 (Scan.succeed |
|
1215 (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o |
|
1216 Toplevel.end_proof (K Proof.end_notepad))); |
|
1217 |
|
1218 in end; |
|
1219 \<close> |
97 |
1220 |
98 |
1221 |
99 section \<open>Basic attributes\<close> |
1222 section \<open>Basic attributes\<close> |
100 |
1223 |
101 attribute_setup tagged = |
1224 attribute_setup tagged = |