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