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