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