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