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