src/Pure/Pure.thy
author wenzelm
Sun Dec 03 13:22:09 2017 +0100 (17 months ago)
changeset 67119 acb0807ddb56
parent 67105 05ff3e6dbbce
child 67147 dea94b1aabc3
permissions -rw-r--r--
discontinued old 'def' command;
     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" :: 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 consider} "state cases rule"
   811     (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd));
   812 
   813 val _ =
   814   Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
   815     (Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement
   816       >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e)));
   817 
   818 val _ =
   819   Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"
   820     (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd));
   821 
   822 val _ =
   823   Outer_Syntax.command @{command_keyword let} "bind text variables"
   824     (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword =} |-- Parse.term))
   825       >> (Toplevel.proof o Proof.let_bind_cmd));
   826 
   827 val _ =
   828   Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables"
   829     (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   830     >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
   831 
   832 val _ =
   833   Outer_Syntax.command @{command_keyword case} "invoke local context"
   834     (Parse_Spec.opt_thm_name ":" --
   835       (@{keyword "("} |--
   836         Parse.!!! (Parse.position Parse.name -- Scan.repeat (Parse.maybe Parse.binding)
   837           --| @{keyword ")"}) ||
   838         Parse.position Parse.name >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
   839 
   840 in end\<close>
   841 
   842 
   843 subsubsection \<open>Proof structure\<close>
   844 
   845 ML \<open>
   846 local
   847 
   848 val _ =
   849   Outer_Syntax.command @{command_keyword "{"} "begin explicit proof block"
   850     (Scan.succeed (Toplevel.proof Proof.begin_block));
   851 
   852 val _ =
   853   Outer_Syntax.command @{command_keyword "}"} "end explicit proof block"
   854     (Scan.succeed (Toplevel.proof Proof.end_block));
   855 
   856 val _ =
   857   Outer_Syntax.command @{command_keyword next} "enter next proof block"
   858     (Scan.succeed (Toplevel.proof Proof.next_block));
   859 
   860 in end\<close>
   861 
   862 
   863 subsubsection \<open>End proof\<close>
   864 
   865 ML \<open>
   866 local
   867 
   868 val _ =
   869   Outer_Syntax.command @{command_keyword qed} "conclude proof"
   870     (Scan.option Method.parse >> (fn m =>
   871      (Option.map Method.report m;
   872       Isar_Cmd.qed m)));
   873 
   874 val _ =
   875   Outer_Syntax.command @{command_keyword by} "terminal backward proof"
   876     (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
   877      (Method.report m1;
   878       Option.map Method.report m2;
   879       Isar_Cmd.terminal_proof (m1, m2))));
   880 
   881 val _ =
   882   Outer_Syntax.command @{command_keyword ".."} "default proof"
   883     (Scan.succeed Isar_Cmd.default_proof);
   884 
   885 val _ =
   886   Outer_Syntax.command @{command_keyword "."} "immediate proof"
   887     (Scan.succeed Isar_Cmd.immediate_proof);
   888 
   889 val _ =
   890   Outer_Syntax.command @{command_keyword done} "done proof"
   891     (Scan.succeed Isar_Cmd.done_proof);
   892 
   893 val _ =
   894   Outer_Syntax.command @{command_keyword sorry} "skip proof (quick-and-dirty mode only!)"
   895     (Scan.succeed Isar_Cmd.skip_proof);
   896 
   897 val _ =
   898   Outer_Syntax.command @{command_keyword \<proof>} "dummy proof (quick-and-dirty mode only!)"
   899     (Scan.succeed Isar_Cmd.skip_proof);
   900 
   901 val _ =
   902   Outer_Syntax.command @{command_keyword oops} "forget proof"
   903     (Scan.succeed (Toplevel.forget_proof true));
   904 
   905 in end\<close>
   906 
   907 
   908 subsubsection \<open>Proof steps\<close>
   909 
   910 ML \<open>
   911 local
   912 
   913 val _ =
   914   Outer_Syntax.command @{command_keyword defer} "shuffle internal proof state"
   915     (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
   916 
   917 val _ =
   918   Outer_Syntax.command @{command_keyword prefer} "shuffle internal proof state"
   919     (Parse.nat >> (Toplevel.proof o Proof.prefer));
   920 
   921 val _ =
   922   Outer_Syntax.command @{command_keyword apply} "initial goal refinement step (unstructured)"
   923     (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m))));
   924 
   925 val _ =
   926   Outer_Syntax.command @{command_keyword apply_end} "terminal goal refinement step (unstructured)"
   927     (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m))));
   928 
   929 val _ =
   930   Outer_Syntax.command @{command_keyword proof} "backward proof step"
   931     (Scan.option Method.parse >> (fn m =>
   932       (Option.map Method.report m;
   933        Toplevel.proof (fn state =>
   934          let
   935           val state' = state |> Proof.proof m |> Seq.the_result "";
   936           val _ =
   937             Output.information
   938               (Proof_Context.print_cases_proof (Proof.context_of state) (Proof.context_of state'));
   939         in state' end))))
   940 
   941 in end\<close>
   942 
   943 
   944 subsubsection \<open>Subgoal focus\<close>
   945 
   946 ML \<open>
   947 local
   948 
   949 val opt_fact_binding =
   950   Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
   951     Binding.empty_atts;
   952 
   953 val for_params =
   954   Scan.optional
   955     (@{keyword for} |--
   956       Parse.!!! ((Scan.option Parse.dots >> is_some) --
   957         (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
   958     (false, []);
   959 
   960 val _ =
   961   Outer_Syntax.command @{command_keyword subgoal}
   962     "focus on first subgoal within backward refinement"
   963     (opt_fact_binding -- (Scan.option (@{keyword premises} |-- Parse.!!! opt_fact_binding)) --
   964       for_params >> (fn ((a, b), c) =>
   965         Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
   966 
   967 in end\<close>
   968 
   969 
   970 subsubsection \<open>Calculation\<close>
   971 
   972 ML \<open>
   973 local
   974 
   975 val calculation_args =
   976   Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.thms1 --| @{keyword ")"})));
   977 
   978 val _ =
   979   Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
   980     (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd));
   981 
   982 val _ =
   983   Outer_Syntax.command @{command_keyword finally}
   984     "combine calculation and current facts, exhibit result"
   985     (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd));
   986 
   987 val _ =
   988   Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts"
   989     (Scan.succeed (Toplevel.proof' Calculation.moreover));
   990 
   991 val _ =
   992   Outer_Syntax.command @{command_keyword ultimately}
   993     "augment calculation by current facts, exhibit result"
   994     (Scan.succeed (Toplevel.proof' Calculation.ultimately));
   995 
   996 val _ =
   997   Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
   998     (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
   999 
  1000 in end\<close>
  1001 
  1002 
  1003 subsubsection \<open>Proof navigation\<close>
  1004 
  1005 ML \<open>
  1006 local
  1007 
  1008 fun report_back () =
  1009   Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"];
  1010 
  1011 val _ =
  1012   Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"
  1013     (Scan.succeed
  1014      (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
  1015       Toplevel.skip_proof report_back));
  1016 
  1017 in end\<close>
  1018 
  1019 
  1020 subsection \<open>Diagnostic commands (for interactive mode only)\<close>
  1021 
  1022 ML \<open>
  1023 local
  1024 
  1025 val opt_modes =
  1026   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
  1027 
  1028 val _ =
  1029   Outer_Syntax.command @{command_keyword help}
  1030     "retrieve outer syntax commands according to name patterns"
  1031     (Scan.repeat Parse.name >>
  1032       (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats)));
  1033 
  1034 val _ =
  1035   Outer_Syntax.command @{command_keyword print_commands} "print outer syntax commands"
  1036     (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of)));
  1037 
  1038 val _ =
  1039   Outer_Syntax.command @{command_keyword print_options} "print configuration options"
  1040     (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
  1041 
  1042 val _ =
  1043   Outer_Syntax.command @{command_keyword print_context}
  1044     "print context of local theory target"
  1045     (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
  1046 
  1047 val _ =
  1048   Outer_Syntax.command @{command_keyword print_theory}
  1049     "print logical theory contents"
  1050     (Parse.opt_bang >> (fn b =>
  1051       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of)));
  1052 
  1053 val _ =
  1054   Outer_Syntax.command @{command_keyword print_definitions}
  1055     "print dependencies of definitional theory content"
  1056     (Parse.opt_bang >> (fn b =>
  1057       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of)));
  1058 
  1059 val _ =
  1060   Outer_Syntax.command @{command_keyword print_syntax}
  1061     "print inner syntax of context"
  1062     (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
  1063 
  1064 val _ =
  1065   Outer_Syntax.command @{command_keyword print_defn_rules}
  1066     "print definitional rewrite rules of context"
  1067     (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
  1068 
  1069 val _ =
  1070   Outer_Syntax.command @{command_keyword print_abbrevs}
  1071     "print constant abbreviations of context"
  1072     (Parse.opt_bang >> (fn b =>
  1073       Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
  1074 
  1075 val _ =
  1076   Outer_Syntax.command @{command_keyword print_theorems}
  1077     "print theorems of local theory or proof context"
  1078     (Parse.opt_bang >> (fn b =>
  1079       Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
  1080 
  1081 val _ =
  1082   Outer_Syntax.command @{command_keyword print_locales}
  1083     "print locales of this theory"
  1084     (Parse.opt_bang >> (fn b =>
  1085       Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
  1086 
  1087 val _ =
  1088   Outer_Syntax.command @{command_keyword print_classes}
  1089     "print classes of this theory"
  1090     (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of)));
  1091 
  1092 val _ =
  1093   Outer_Syntax.command @{command_keyword print_locale}
  1094     "print locale of this theory"
  1095     (Parse.opt_bang -- Parse.position Parse.name >> (fn (b, name) =>
  1096       Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
  1097 
  1098 val _ =
  1099   Outer_Syntax.command @{command_keyword print_interps}
  1100     "print interpretations of locale for this theory or proof context"
  1101     (Parse.position Parse.name >> (fn name =>
  1102       Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
  1103 
  1104 val _ =
  1105   Outer_Syntax.command @{command_keyword print_dependencies}
  1106     "print dependencies of locale expression"
  1107     (Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (b, expr) =>
  1108       Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
  1109 
  1110 val _ =
  1111   Outer_Syntax.command @{command_keyword print_attributes}
  1112     "print attributes of this theory"
  1113     (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
  1114 
  1115 val _ =
  1116   Outer_Syntax.command @{command_keyword print_simpset}
  1117     "print context of Simplifier"
  1118     (Parse.opt_bang >> (fn b =>
  1119       Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
  1120 
  1121 val _ =
  1122   Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules"
  1123     (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
  1124 
  1125 val _ =
  1126   Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory"
  1127     (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
  1128 
  1129 val _ =
  1130   Outer_Syntax.command @{command_keyword print_antiquotations}
  1131     "print document antiquotations"
  1132     (Parse.opt_bang >> (fn b =>
  1133       Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
  1134 
  1135 val _ =
  1136   Outer_Syntax.command @{command_keyword print_ML_antiquotations}
  1137     "print ML antiquotations"
  1138     (Parse.opt_bang >> (fn b =>
  1139       Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
  1140 
  1141 val _ =
  1142   Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies"
  1143     (Scan.succeed
  1144       (Toplevel.keep (Toplevel.theory_of #> (fn thy =>
  1145         Locale.pretty_locale_deps thy
  1146         |> map (fn {name, parents, body} =>
  1147           ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
  1148         |> Graph_Display.display_graph_old))));
  1149 
  1150 val _ =
  1151   Outer_Syntax.command @{command_keyword print_term_bindings}
  1152     "print term bindings of proof context"
  1153     (Scan.succeed
  1154       (Toplevel.keep
  1155         (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
  1156 
  1157 val _ =
  1158   Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context"
  1159     (Parse.opt_bang >> (fn b =>
  1160       Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
  1161 
  1162 val _ =
  1163   Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context"
  1164     (Scan.succeed
  1165       (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
  1166 
  1167 val _ =
  1168   Outer_Syntax.command @{command_keyword print_statement}
  1169     "print theorems as long statements"
  1170     (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts);
  1171 
  1172 val _ =
  1173   Outer_Syntax.command @{command_keyword thm} "print theorems"
  1174     (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms);
  1175 
  1176 val _ =
  1177   Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems"
  1178     (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false);
  1179 
  1180 val _ =
  1181   Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems"
  1182     (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true);
  1183 
  1184 val _ =
  1185   Outer_Syntax.command @{command_keyword prop} "read and print proposition"
  1186     (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
  1187 
  1188 val _ =
  1189   Outer_Syntax.command @{command_keyword term} "read and print term"
  1190     (opt_modes -- Parse.term >> Isar_Cmd.print_term);
  1191 
  1192 val _ =
  1193   Outer_Syntax.command @{command_keyword typ} "read and print type"
  1194     (opt_modes -- (Parse.typ -- Scan.option (@{keyword ::} |-- Parse.!!! Parse.sort))
  1195       >> Isar_Cmd.print_type);
  1196 
  1197 val _ =
  1198   Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup"
  1199     (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
  1200 
  1201 val _ =
  1202   Outer_Syntax.command @{command_keyword print_state}
  1203     "print current proof state (if present)"
  1204     (opt_modes >> (fn modes =>
  1205       Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state))));
  1206 
  1207 val _ =
  1208   Outer_Syntax.command @{command_keyword welcome} "print welcome message"
  1209     (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ()))));
  1210 
  1211 val _ =
  1212   Outer_Syntax.command @{command_keyword display_drafts}
  1213     "display raw source files with symbols"
  1214     (Scan.repeat1 Parse.path >> (fn names =>
  1215       Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names)))));
  1216 
  1217 in end\<close>
  1218 
  1219 
  1220 subsection \<open>Dependencies\<close>
  1221 
  1222 ML \<open>
  1223 local
  1224 
  1225 val theory_bounds =
  1226   Parse.position Parse.theory_name >> single ||
  1227   (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_name) --| @{keyword ")"});
  1228 
  1229 val _ =
  1230   Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
  1231     (Scan.option theory_bounds -- Scan.option theory_bounds >>
  1232       (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args)));
  1233 
  1234 
  1235 val class_bounds =
  1236   Parse.sort >> single ||
  1237   (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
  1238 
  1239 val _ =
  1240   Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
  1241     (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
  1242       Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args)));
  1243 
  1244 
  1245 val _ =
  1246   Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
  1247     (Parse.thms1 >> (fn args =>
  1248       Toplevel.keep (fn st =>
  1249         Thm_Deps.thm_deps (Toplevel.theory_of st)
  1250           (Attrib.eval_thms (Toplevel.context_of st) args))));
  1251 
  1252 
  1253 val thy_names =
  1254   Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_name));
  1255 
  1256 val _ =
  1257   Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
  1258     (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range =>
  1259         Toplevel.keep (fn st =>
  1260           let
  1261             val thy = Toplevel.theory_of st;
  1262             val ctxt = Toplevel.context_of st;
  1263             fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
  1264             val check = Theory.check ctxt;
  1265           in
  1266             Thm_Deps.unused_thms
  1267               (case opt_range of
  1268                 NONE => (Theory.parents_of thy, [thy])
  1269               | SOME (xs, NONE) => (map check xs, [thy])
  1270               | SOME (xs, SOME ys) => (map check xs, map check ys))
  1271             |> map pretty_thm |> Pretty.writeln_chunks
  1272           end)));
  1273 
  1274 in end\<close>
  1275 
  1276 
  1277 subsubsection \<open>Find consts and theorems\<close>
  1278 
  1279 ML \<open>
  1280 local
  1281 
  1282 val _ =
  1283   Outer_Syntax.command @{command_keyword find_consts}
  1284     "find constants by name / type patterns"
  1285     (Find_Consts.query_parser >> (fn spec =>
  1286       Toplevel.keep (fn st =>
  1287         Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec))));
  1288 
  1289 val options =
  1290   Scan.optional
  1291     (Parse.$$$ "(" |--
  1292       Parse.!!! (Scan.option Parse.nat --
  1293         Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")"))
  1294     (NONE, true);
  1295 
  1296 val _ =
  1297   Outer_Syntax.command @{command_keyword find_theorems}
  1298     "find theorems meeting specified criteria"
  1299     (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) =>
  1300       Toplevel.keep (fn st =>
  1301         Pretty.writeln
  1302           (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec))));
  1303 
  1304 in end\<close>
  1305 
  1306 
  1307 subsection \<open>Code generation\<close>
  1308 
  1309 ML \<open>
  1310 local
  1311 
  1312 val _ =
  1313   Outer_Syntax.command @{command_keyword code_datatype}
  1314     "define set of code datatype constructors"
  1315     (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.declare_datatype_cmd));
  1316 
  1317 in end\<close>
  1318 
  1319 
  1320 subsection \<open>Extraction of programs from proofs\<close>
  1321 
  1322 ML \<open>
  1323 local
  1324 
  1325 val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
  1326 
  1327 val _ =
  1328   Outer_Syntax.command @{command_keyword realizers}
  1329     "specify realizers for primitive axioms / theorems, together with correctness proof"
  1330     (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
  1331      (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
  1332        (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
  1333 
  1334 val _ =
  1335   Outer_Syntax.command @{command_keyword realizability}
  1336     "add equations characterizing realizability"
  1337     (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
  1338 
  1339 val _ =
  1340   Outer_Syntax.command @{command_keyword extract_type}
  1341     "add equations characterizing type of extracted program"
  1342     (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
  1343 
  1344 val _ =
  1345   Outer_Syntax.command @{command_keyword extract} "extract terms from proofs"
  1346     (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
  1347       Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
  1348 
  1349 in end\<close>
  1350 
  1351 
  1352 section \<open>Auxiliary lemmas\<close>
  1353 
  1354 subsection \<open>Meta-level connectives in assumptions\<close>
  1355 
  1356 lemma meta_mp:
  1357   assumes "PROP P \<Longrightarrow> PROP Q" and "PROP P"
  1358   shows "PROP Q"
  1359     by (rule \<open>PROP P \<Longrightarrow> PROP Q\<close> [OF \<open>PROP P\<close>])
  1360 
  1361 lemmas meta_impE = meta_mp [elim_format]
  1362 
  1363 lemma meta_spec:
  1364   assumes "\<And>x. PROP P x"
  1365   shows "PROP P x"
  1366     by (rule \<open>\<And>x. PROP P x\<close>)
  1367 
  1368 lemmas meta_allE = meta_spec [elim_format]
  1369 
  1370 lemma swap_params:
  1371   "(\<And>x y. PROP P x y) \<equiv> (\<And>y x. PROP P x y)" ..
  1372 
  1373 
  1374 subsection \<open>Meta-level conjunction\<close>
  1375 
  1376 lemma all_conjunction:
  1377   "(\<And>x. PROP A x &&& PROP B x) \<equiv> ((\<And>x. PROP A x) &&& (\<And>x. PROP B x))"
  1378 proof
  1379   assume conj: "\<And>x. PROP A x &&& PROP B x"
  1380   show "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)"
  1381   proof -
  1382     fix x
  1383     from conj show "PROP A x" by (rule conjunctionD1)
  1384     from conj show "PROP B x" by (rule conjunctionD2)
  1385   qed
  1386 next
  1387   assume conj: "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)"
  1388   fix x
  1389   show "PROP A x &&& PROP B x"
  1390   proof -
  1391     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
  1392     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
  1393   qed
  1394 qed
  1395 
  1396 lemma imp_conjunction:
  1397   "(PROP A \<Longrightarrow> PROP B &&& PROP C) \<equiv> ((PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C))"
  1398 proof
  1399   assume conj: "PROP A \<Longrightarrow> PROP B &&& PROP C"
  1400   show "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)"
  1401   proof -
  1402     assume "PROP A"
  1403     from conj [OF \<open>PROP A\<close>] show "PROP B" by (rule conjunctionD1)
  1404     from conj [OF \<open>PROP A\<close>] show "PROP C" by (rule conjunctionD2)
  1405   qed
  1406 next
  1407   assume conj: "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)"
  1408   assume "PROP A"
  1409   show "PROP B &&& PROP C"
  1410   proof -
  1411     from \<open>PROP A\<close> show "PROP B" by (rule conj [THEN conjunctionD1])
  1412     from \<open>PROP A\<close> show "PROP C" by (rule conj [THEN conjunctionD2])
  1413   qed
  1414 qed
  1415 
  1416 lemma conjunction_imp:
  1417   "(PROP A &&& PROP B \<Longrightarrow> PROP C) \<equiv> (PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C)"
  1418 proof
  1419   assume r: "PROP A &&& PROP B \<Longrightarrow> PROP C"
  1420   assume ab: "PROP A" "PROP B"
  1421   show "PROP C"
  1422   proof (rule r)
  1423     from ab show "PROP A &&& PROP B" .
  1424   qed
  1425 next
  1426   assume r: "PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C"
  1427   assume conj: "PROP A &&& PROP B"
  1428   show "PROP C"
  1429   proof (rule r)
  1430     from conj show "PROP A" by (rule conjunctionD1)
  1431     from conj show "PROP B" by (rule conjunctionD2)
  1432   qed
  1433 qed
  1434 
  1435 end