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