src/Pure/Pure.thy
author ballarin
Sun Mar 04 12:22:48 2018 +0100 (16 months ago)
changeset 67764 0f8cb5568b63
parent 67740 b6ce18784872
child 67777 2d3c1091527b
permissions -rw-r--r--
Drop rewrites after defines in interpretations.
     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       (fn x => (x, []))) ([], []));
   627 
   628 val _ =
   629   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretation\<close>
   630     "prove interpretation of locale expression into global theory"
   631     (interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
   632       Interpretation.global_interpretation_cmd expr defs equations));
   633 
   634 val _ =
   635   Outer_Syntax.command \<^command_keyword>\<open>sublocale\<close>
   636     "prove sublocale relation between a locale and a locale expression"
   637     ((Parse.position Parse.name --| (\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><\<close>) --
   638       interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) =>
   639         Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations)))
   640     || interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
   641         Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs equations)));
   642 
   643 val _ =
   644   Outer_Syntax.command \<^command_keyword>\<open>interpretation\<close>
   645     "prove interpretation of locale expression in local theory or into global theory"
   646     (Parse.!!! Parse_Spec.locale_expression >> (fn expr =>
   647       Toplevel.local_theory_to_proof NONE NONE
   648         (Interpretation.isar_interpretation_cmd expr [])));
   649 
   650 in end\<close>
   651 
   652 
   653 subsubsection \<open>Type classes\<close>
   654 
   655 ML \<open>
   656 local
   657 
   658 val class_val =
   659   Parse_Spec.class_expression --
   660     Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   661   Scan.repeat1 Parse_Spec.context_element >> pair [];
   662 
   663 val _ =
   664   Outer_Syntax.command \<^command_keyword>\<open>class\<close> "define type class"
   665    (Parse.binding -- Scan.optional (\<^keyword>\<open>=\<close> |-- class_val) ([], []) -- Parse.opt_begin
   666     >> (fn ((name, (supclasses, elems)), begin) =>
   667         Toplevel.begin_local_theory begin
   668           (Class_Declaration.class_cmd name supclasses elems #> snd)));
   669 
   670 val _ =
   671   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>subclass\<close> "prove a subclass relation"
   672     (Parse.class >> Class_Declaration.subclass_cmd);
   673 
   674 val _ =
   675   Outer_Syntax.command \<^command_keyword>\<open>instantiation\<close> "instantiate and prove type arity"
   676    (Parse.multi_arity --| Parse.begin
   677      >> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
   678 
   679 val _ =
   680   Outer_Syntax.command \<^command_keyword>\<open>instance\<close> "prove type arity or subclass relation"
   681   ((Parse.class --
   682     ((\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><\<close>) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
   683     Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
   684     Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I)));
   685 
   686 in end\<close>
   687 
   688 
   689 subsubsection \<open>Arbitrary overloading\<close>
   690 
   691 ML \<open>
   692 local
   693 
   694 val _ =
   695   Outer_Syntax.command \<^command_keyword>\<open>overloading\<close> "overloaded definitions"
   696    (Scan.repeat1 (Parse.name --| (\<^keyword>\<open>==\<close> || \<^keyword>\<open>\<equiv>\<close>) -- Parse.term --
   697       Scan.optional (\<^keyword>\<open>(\<close> |-- (\<^keyword>\<open>unchecked\<close> >> K false) --| \<^keyword>\<open>)\<close>) true
   698       >> Scan.triple1) --| Parse.begin
   699    >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
   700 
   701 in end\<close>
   702 
   703 
   704 subsection \<open>Proof commands\<close>
   705 
   706 ML \<open>
   707 local
   708 
   709 val _ =
   710   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>notepad\<close> "begin proof context"
   711     (Parse.begin >> K Proof.begin_notepad);
   712 
   713 in end\<close>
   714 
   715 
   716 subsubsection \<open>Statements\<close>
   717 
   718 ML \<open>
   719 local
   720 
   721 val structured_statement =
   722   Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
   723     >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
   724 
   725 val _ =
   726   Outer_Syntax.command \<^command_keyword>\<open>have\<close> "state local goal"
   727     (structured_statement >> (fn (a, b, c, d) =>
   728       Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2)));
   729 
   730 val _ =
   731   Outer_Syntax.command \<^command_keyword>\<open>show\<close> "state local goal, to refine pending subgoals"
   732     (structured_statement >> (fn (a, b, c, d) =>
   733       Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2)));
   734 
   735 val _ =
   736   Outer_Syntax.command \<^command_keyword>\<open>hence\<close> "old-style alias of \"then have\""
   737     (structured_statement >> (fn (a, b, c, d) =>
   738       Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2)));
   739 
   740 val _ =
   741   Outer_Syntax.command \<^command_keyword>\<open>thus\<close> "old-style alias of  \"then show\""
   742     (structured_statement >> (fn (a, b, c, d) =>
   743       Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2)));
   744 
   745 in end\<close>
   746 
   747 
   748 subsubsection \<open>Local facts\<close>
   749 
   750 ML \<open>
   751 local
   752 
   753 val facts = Parse.and_list1 Parse.thms1;
   754 
   755 val _ =
   756   Outer_Syntax.command \<^command_keyword>\<open>then\<close> "forward chaining"
   757     (Scan.succeed (Toplevel.proof Proof.chain));
   758 
   759 val _ =
   760   Outer_Syntax.command \<^command_keyword>\<open>from\<close> "forward chaining from given facts"
   761     (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
   762 
   763 val _ =
   764   Outer_Syntax.command \<^command_keyword>\<open>with\<close> "forward chaining from given and current facts"
   765     (facts >> (Toplevel.proof o Proof.with_thmss_cmd));
   766 
   767 val _ =
   768   Outer_Syntax.command \<^command_keyword>\<open>note\<close> "define facts"
   769     (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
   770 
   771 val _ =
   772   Outer_Syntax.command \<^command_keyword>\<open>supply\<close> "define facts during goal refinement (unstructured)"
   773     (Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd));
   774 
   775 val _ =
   776   Outer_Syntax.command \<^command_keyword>\<open>using\<close> "augment goal facts"
   777     (facts >> (Toplevel.proof o Proof.using_cmd));
   778 
   779 val _ =
   780   Outer_Syntax.command \<^command_keyword>\<open>unfolding\<close> "unfold definitions in goal and facts"
   781     (facts >> (Toplevel.proof o Proof.unfolding_cmd));
   782 
   783 in end\<close>
   784 
   785 
   786 subsubsection \<open>Proof context\<close>
   787 
   788 ML \<open>
   789 local
   790 
   791 val structured_statement =
   792   Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes
   793     >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
   794 
   795 val _ =
   796   Outer_Syntax.command \<^command_keyword>\<open>fix\<close> "fix local variables (Skolem constants)"
   797     (Parse.vars >> (Toplevel.proof o Proof.fix_cmd));
   798 
   799 val _ =
   800   Outer_Syntax.command \<^command_keyword>\<open>assume\<close> "assume propositions"
   801     (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c)));
   802 
   803 val _ =
   804   Outer_Syntax.command \<^command_keyword>\<open>presume\<close> "assume propositions, to be established later"
   805     (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
   806 
   807 val _ =
   808   Outer_Syntax.command \<^command_keyword>\<open>define\<close> "local definition (non-polymorphic)"
   809     ((Parse.vars --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes
   810       >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b)));
   811 
   812 val _ =
   813   Outer_Syntax.command \<^command_keyword>\<open>consider\<close> "state cases rule"
   814     (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd));
   815 
   816 val _ =
   817   Outer_Syntax.command \<^command_keyword>\<open>obtain\<close> "generalized elimination"
   818     (Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement
   819       >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e)));
   820 
   821 val _ =
   822   Outer_Syntax.command \<^command_keyword>\<open>guess\<close> "wild guessing (unstructured)"
   823     (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd));
   824 
   825 val _ =
   826   Outer_Syntax.command \<^command_keyword>\<open>let\<close> "bind text variables"
   827     (Parse.and_list1 (Parse.and_list1 Parse.term -- (\<^keyword>\<open>=\<close> |-- Parse.term))
   828       >> (Toplevel.proof o Proof.let_bind_cmd));
   829 
   830 val _ =
   831   Outer_Syntax.command \<^command_keyword>\<open>write\<close> "add concrete syntax for constants / fixed variables"
   832     (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   833     >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
   834 
   835 val _ =
   836   Outer_Syntax.command \<^command_keyword>\<open>case\<close> "invoke local context"
   837     (Parse_Spec.opt_thm_name ":" --
   838       (\<^keyword>\<open>(\<close> |--
   839         Parse.!!! (Parse.position Parse.name -- Scan.repeat (Parse.maybe Parse.binding)
   840           --| \<^keyword>\<open>)\<close>) ||
   841         Parse.position Parse.name >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
   842 
   843 in end\<close>
   844 
   845 
   846 subsubsection \<open>Proof structure\<close>
   847 
   848 ML \<open>
   849 local
   850 
   851 val _ =
   852   Outer_Syntax.command \<^command_keyword>\<open>{\<close> "begin explicit proof block"
   853     (Scan.succeed (Toplevel.proof Proof.begin_block));
   854 
   855 val _ =
   856   Outer_Syntax.command \<^command_keyword>\<open>}\<close> "end explicit proof block"
   857     (Scan.succeed (Toplevel.proof Proof.end_block));
   858 
   859 val _ =
   860   Outer_Syntax.command \<^command_keyword>\<open>next\<close> "enter next proof block"
   861     (Scan.succeed (Toplevel.proof Proof.next_block));
   862 
   863 in end\<close>
   864 
   865 
   866 subsubsection \<open>End proof\<close>
   867 
   868 ML \<open>
   869 local
   870 
   871 val _ =
   872   Outer_Syntax.command \<^command_keyword>\<open>qed\<close> "conclude proof"
   873     (Scan.option Method.parse >> (fn m =>
   874      (Option.map Method.report m;
   875       Isar_Cmd.qed m)));
   876 
   877 val _ =
   878   Outer_Syntax.command \<^command_keyword>\<open>by\<close> "terminal backward proof"
   879     (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
   880      (Method.report m1;
   881       Option.map Method.report m2;
   882       Isar_Cmd.terminal_proof (m1, m2))));
   883 
   884 val _ =
   885   Outer_Syntax.command \<^command_keyword>\<open>..\<close> "default proof"
   886     (Scan.succeed Isar_Cmd.default_proof);
   887 
   888 val _ =
   889   Outer_Syntax.command \<^command_keyword>\<open>.\<close> "immediate proof"
   890     (Scan.succeed Isar_Cmd.immediate_proof);
   891 
   892 val _ =
   893   Outer_Syntax.command \<^command_keyword>\<open>done\<close> "done proof"
   894     (Scan.succeed Isar_Cmd.done_proof);
   895 
   896 val _ =
   897   Outer_Syntax.command \<^command_keyword>\<open>sorry\<close> "skip proof (quick-and-dirty mode only!)"
   898     (Scan.succeed Isar_Cmd.skip_proof);
   899 
   900 val _ =
   901   Outer_Syntax.command \<^command_keyword>\<open>\<proof>\<close> "dummy proof (quick-and-dirty mode only!)"
   902     (Scan.succeed Isar_Cmd.skip_proof);
   903 
   904 val _ =
   905   Outer_Syntax.command \<^command_keyword>\<open>oops\<close> "forget proof"
   906     (Scan.succeed (Toplevel.forget_proof true));
   907 
   908 in end\<close>
   909 
   910 
   911 subsubsection \<open>Proof steps\<close>
   912 
   913 ML \<open>
   914 local
   915 
   916 val _ =
   917   Outer_Syntax.command \<^command_keyword>\<open>defer\<close> "shuffle internal proof state"
   918     (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
   919 
   920 val _ =
   921   Outer_Syntax.command \<^command_keyword>\<open>prefer\<close> "shuffle internal proof state"
   922     (Parse.nat >> (Toplevel.proof o Proof.prefer));
   923 
   924 val _ =
   925   Outer_Syntax.command \<^command_keyword>\<open>apply\<close> "initial goal refinement step (unstructured)"
   926     (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m))));
   927 
   928 val _ =
   929   Outer_Syntax.command \<^command_keyword>\<open>apply_end\<close> "terminal goal refinement step (unstructured)"
   930     (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m))));
   931 
   932 val _ =
   933   Outer_Syntax.command \<^command_keyword>\<open>proof\<close> "backward proof step"
   934     (Scan.option Method.parse >> (fn m =>
   935       (Option.map Method.report m;
   936        Toplevel.proof (fn state =>
   937          let
   938           val state' = state |> Proof.proof m |> Seq.the_result "";
   939           val _ =
   940             Output.information
   941               (Proof_Context.print_cases_proof (Proof.context_of state) (Proof.context_of state'));
   942         in state' end))))
   943 
   944 in end\<close>
   945 
   946 
   947 subsubsection \<open>Subgoal focus\<close>
   948 
   949 ML \<open>
   950 local
   951 
   952 val opt_fact_binding =
   953   Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
   954     Binding.empty_atts;
   955 
   956 val for_params =
   957   Scan.optional
   958     (\<^keyword>\<open>for\<close> |--
   959       Parse.!!! ((Scan.option Parse.dots >> is_some) --
   960         (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
   961     (false, []);
   962 
   963 val _ =
   964   Outer_Syntax.command \<^command_keyword>\<open>subgoal\<close>
   965     "focus on first subgoal within backward refinement"
   966     (opt_fact_binding -- (Scan.option (\<^keyword>\<open>premises\<close> |-- Parse.!!! opt_fact_binding)) --
   967       for_params >> (fn ((a, b), c) =>
   968         Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
   969 
   970 in end\<close>
   971 
   972 
   973 subsubsection \<open>Calculation\<close>
   974 
   975 ML \<open>
   976 local
   977 
   978 val calculation_args =
   979   Scan.option (\<^keyword>\<open>(\<close> |-- Parse.!!! ((Parse.thms1 --| \<^keyword>\<open>)\<close>)));
   980 
   981 val _ =
   982   Outer_Syntax.command \<^command_keyword>\<open>also\<close> "combine calculation and current facts"
   983     (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd));
   984 
   985 val _ =
   986   Outer_Syntax.command \<^command_keyword>\<open>finally\<close>
   987     "combine calculation and current facts, exhibit result"
   988     (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd));
   989 
   990 val _ =
   991   Outer_Syntax.command \<^command_keyword>\<open>moreover\<close> "augment calculation by current facts"
   992     (Scan.succeed (Toplevel.proof' Calculation.moreover));
   993 
   994 val _ =
   995   Outer_Syntax.command \<^command_keyword>\<open>ultimately\<close>
   996     "augment calculation by current facts, exhibit result"
   997     (Scan.succeed (Toplevel.proof' Calculation.ultimately));
   998 
   999 val _ =
  1000   Outer_Syntax.command \<^command_keyword>\<open>print_trans_rules\<close> "print transitivity rules"
  1001     (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
  1002 
  1003 in end\<close>
  1004 
  1005 
  1006 subsubsection \<open>Proof navigation\<close>
  1007 
  1008 ML \<open>
  1009 local
  1010 
  1011 fun report_back () =
  1012   Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"];
  1013 
  1014 val _ =
  1015   Outer_Syntax.command \<^command_keyword>\<open>back\<close> "explicit backtracking of proof command"
  1016     (Scan.succeed
  1017      (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
  1018       Toplevel.skip_proof report_back));
  1019 
  1020 in end\<close>
  1021 
  1022 
  1023 subsection \<open>Diagnostic commands (for interactive mode only)\<close>
  1024 
  1025 ML \<open>
  1026 local
  1027 
  1028 val opt_modes =
  1029   Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\<open>)\<close>)) [];
  1030 
  1031 val _ =
  1032   Outer_Syntax.command \<^command_keyword>\<open>help\<close>
  1033     "retrieve outer syntax commands according to name patterns"
  1034     (Scan.repeat Parse.name >>
  1035       (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats)));
  1036 
  1037 val _ =
  1038   Outer_Syntax.command \<^command_keyword>\<open>print_commands\<close> "print outer syntax commands"
  1039     (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of)));
  1040 
  1041 val _ =
  1042   Outer_Syntax.command \<^command_keyword>\<open>print_options\<close> "print configuration options"
  1043     (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
  1044 
  1045 val _ =
  1046   Outer_Syntax.command \<^command_keyword>\<open>print_context\<close>
  1047     "print context of local theory target"
  1048     (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
  1049 
  1050 val _ =
  1051   Outer_Syntax.command \<^command_keyword>\<open>print_theory\<close>
  1052     "print logical theory contents"
  1053     (Parse.opt_bang >> (fn b =>
  1054       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of)));
  1055 
  1056 val _ =
  1057   Outer_Syntax.command \<^command_keyword>\<open>print_definitions\<close>
  1058     "print dependencies of definitional theory content"
  1059     (Parse.opt_bang >> (fn b =>
  1060       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of)));
  1061 
  1062 val _ =
  1063   Outer_Syntax.command \<^command_keyword>\<open>print_syntax\<close>
  1064     "print inner syntax of context"
  1065     (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
  1066 
  1067 val _ =
  1068   Outer_Syntax.command \<^command_keyword>\<open>print_defn_rules\<close>
  1069     "print definitional rewrite rules of context"
  1070     (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
  1071 
  1072 val _ =
  1073   Outer_Syntax.command \<^command_keyword>\<open>print_abbrevs\<close>
  1074     "print constant abbreviations of context"
  1075     (Parse.opt_bang >> (fn b =>
  1076       Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
  1077 
  1078 val _ =
  1079   Outer_Syntax.command \<^command_keyword>\<open>print_theorems\<close>
  1080     "print theorems of local theory or proof context"
  1081     (Parse.opt_bang >> (fn b =>
  1082       Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
  1083 
  1084 val _ =
  1085   Outer_Syntax.command \<^command_keyword>\<open>print_locales\<close>
  1086     "print locales of this theory"
  1087     (Parse.opt_bang >> (fn b =>
  1088       Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
  1089 
  1090 val _ =
  1091   Outer_Syntax.command \<^command_keyword>\<open>print_classes\<close>
  1092     "print classes of this theory"
  1093     (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of)));
  1094 
  1095 val _ =
  1096   Outer_Syntax.command \<^command_keyword>\<open>print_locale\<close>
  1097     "print locale of this theory"
  1098     (Parse.opt_bang -- Parse.position Parse.name >> (fn (b, name) =>
  1099       Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
  1100 
  1101 val _ =
  1102   Outer_Syntax.command \<^command_keyword>\<open>print_interps\<close>
  1103     "print interpretations of locale for this theory or proof context"
  1104     (Parse.position Parse.name >> (fn name =>
  1105       Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
  1106 
  1107 val _ =
  1108   Outer_Syntax.command \<^command_keyword>\<open>print_dependencies\<close>
  1109     "print dependencies of locale expression"
  1110     (Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (b, expr) =>
  1111       Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
  1112 
  1113 val _ =
  1114   Outer_Syntax.command \<^command_keyword>\<open>print_attributes\<close>
  1115     "print attributes of this theory"
  1116     (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
  1117 
  1118 val _ =
  1119   Outer_Syntax.command \<^command_keyword>\<open>print_simpset\<close>
  1120     "print context of Simplifier"
  1121     (Parse.opt_bang >> (fn b =>
  1122       Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
  1123 
  1124 val _ =
  1125   Outer_Syntax.command \<^command_keyword>\<open>print_rules\<close> "print intro/elim rules"
  1126     (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
  1127 
  1128 val _ =
  1129   Outer_Syntax.command \<^command_keyword>\<open>print_methods\<close> "print methods of this theory"
  1130     (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
  1131 
  1132 val _ =
  1133   Outer_Syntax.command \<^command_keyword>\<open>print_antiquotations\<close>
  1134     "print document antiquotations"
  1135     (Parse.opt_bang >> (fn b =>
  1136       Toplevel.keep (Document_Antiquotation.print_antiquotations b o Toplevel.context_of)));
  1137 
  1138 val _ =
  1139   Outer_Syntax.command \<^command_keyword>\<open>print_ML_antiquotations\<close>
  1140     "print ML antiquotations"
  1141     (Parse.opt_bang >> (fn b =>
  1142       Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
  1143 
  1144 val _ =
  1145   Outer_Syntax.command \<^command_keyword>\<open>locale_deps\<close> "visualize locale dependencies"
  1146     (Scan.succeed
  1147       (Toplevel.keep (Toplevel.theory_of #> (fn thy =>
  1148         Locale.pretty_locale_deps thy
  1149         |> map (fn {name, parents, body} =>
  1150           ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
  1151         |> Graph_Display.display_graph_old))));
  1152 
  1153 val _ =
  1154   Outer_Syntax.command \<^command_keyword>\<open>print_term_bindings\<close>
  1155     "print term bindings of proof context"
  1156     (Scan.succeed
  1157       (Toplevel.keep
  1158         (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
  1159 
  1160 val _ =
  1161   Outer_Syntax.command \<^command_keyword>\<open>print_facts\<close> "print facts of proof context"
  1162     (Parse.opt_bang >> (fn b =>
  1163       Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
  1164 
  1165 val _ =
  1166   Outer_Syntax.command \<^command_keyword>\<open>print_cases\<close> "print cases of proof context"
  1167     (Scan.succeed
  1168       (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
  1169 
  1170 val _ =
  1171   Outer_Syntax.command \<^command_keyword>\<open>print_statement\<close>
  1172     "print theorems as long statements"
  1173     (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts);
  1174 
  1175 val _ =
  1176   Outer_Syntax.command \<^command_keyword>\<open>thm\<close> "print theorems"
  1177     (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms);
  1178 
  1179 val _ =
  1180   Outer_Syntax.command \<^command_keyword>\<open>prf\<close> "print proof terms of theorems"
  1181     (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false);
  1182 
  1183 val _ =
  1184   Outer_Syntax.command \<^command_keyword>\<open>full_prf\<close> "print full proof terms of theorems"
  1185     (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true);
  1186 
  1187 val _ =
  1188   Outer_Syntax.command \<^command_keyword>\<open>prop\<close> "read and print proposition"
  1189     (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
  1190 
  1191 val _ =
  1192   Outer_Syntax.command \<^command_keyword>\<open>term\<close> "read and print term"
  1193     (opt_modes -- Parse.term >> Isar_Cmd.print_term);
  1194 
  1195 val _ =
  1196   Outer_Syntax.command \<^command_keyword>\<open>typ\<close> "read and print type"
  1197     (opt_modes -- (Parse.typ -- Scan.option (\<^keyword>\<open>::\<close> |-- Parse.!!! Parse.sort))
  1198       >> Isar_Cmd.print_type);
  1199 
  1200 val _ =
  1201   Outer_Syntax.command \<^command_keyword>\<open>print_codesetup\<close> "print code generator setup"
  1202     (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
  1203 
  1204 val _ =
  1205   Outer_Syntax.command \<^command_keyword>\<open>print_state\<close>
  1206     "print current proof state (if present)"
  1207     (opt_modes >> (fn modes =>
  1208       Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state))));
  1209 
  1210 val _ =
  1211   Outer_Syntax.command \<^command_keyword>\<open>welcome\<close> "print welcome message"
  1212     (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ()))));
  1213 
  1214 in end\<close>
  1215 
  1216 
  1217 subsection \<open>Dependencies\<close>
  1218 
  1219 ML \<open>
  1220 local
  1221 
  1222 val theory_bounds =
  1223   Parse.position Parse.theory_name >> single ||
  1224   (\<^keyword>\<open>(\<close> |-- Parse.enum "|" (Parse.position Parse.theory_name) --| \<^keyword>\<open>)\<close>);
  1225 
  1226 val _ =
  1227   Outer_Syntax.command \<^command_keyword>\<open>thy_deps\<close> "visualize theory dependencies"
  1228     (Scan.option theory_bounds -- Scan.option theory_bounds >>
  1229       (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args)));
  1230 
  1231 
  1232 val class_bounds =
  1233   Parse.sort >> single ||
  1234   (\<^keyword>\<open>(\<close> |-- Parse.enum "|" Parse.sort --| \<^keyword>\<open>)\<close>);
  1235 
  1236 val _ =
  1237   Outer_Syntax.command \<^command_keyword>\<open>class_deps\<close> "visualize class dependencies"
  1238     (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
  1239       Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args)));
  1240 
  1241 
  1242 val _ =
  1243   Outer_Syntax.command \<^command_keyword>\<open>thm_deps\<close> "visualize theorem dependencies"
  1244     (Parse.thms1 >> (fn args =>
  1245       Toplevel.keep (fn st =>
  1246         Thm_Deps.thm_deps (Toplevel.theory_of st)
  1247           (Attrib.eval_thms (Toplevel.context_of st) args))));
  1248 
  1249 
  1250 val thy_names =
  1251   Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_name));
  1252 
  1253 val _ =
  1254   Outer_Syntax.command \<^command_keyword>\<open>unused_thms\<close> "find unused theorems"
  1255     (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range =>
  1256         Toplevel.keep (fn st =>
  1257           let
  1258             val thy = Toplevel.theory_of st;
  1259             val ctxt = Toplevel.context_of st;
  1260             fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
  1261             val check = Theory.check ctxt;
  1262           in
  1263             Thm_Deps.unused_thms
  1264               (case opt_range of
  1265                 NONE => (Theory.parents_of thy, [thy])
  1266               | SOME (xs, NONE) => (map check xs, [thy])
  1267               | SOME (xs, SOME ys) => (map check xs, map check ys))
  1268             |> map pretty_thm |> Pretty.writeln_chunks
  1269           end)));
  1270 
  1271 in end\<close>
  1272 
  1273 
  1274 subsubsection \<open>Find consts and theorems\<close>
  1275 
  1276 ML \<open>
  1277 local
  1278 
  1279 val _ =
  1280   Outer_Syntax.command \<^command_keyword>\<open>find_consts\<close>
  1281     "find constants by name / type patterns"
  1282     (Find_Consts.query_parser >> (fn spec =>
  1283       Toplevel.keep (fn st =>
  1284         Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec))));
  1285 
  1286 val options =
  1287   Scan.optional
  1288     (Parse.$$$ "(" |--
  1289       Parse.!!! (Scan.option Parse.nat --
  1290         Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")"))
  1291     (NONE, true);
  1292 
  1293 val _ =
  1294   Outer_Syntax.command \<^command_keyword>\<open>find_theorems\<close>
  1295     "find theorems meeting specified criteria"
  1296     (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) =>
  1297       Toplevel.keep (fn st =>
  1298         Pretty.writeln
  1299           (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec))));
  1300 
  1301 in end\<close>
  1302 
  1303 
  1304 subsection \<open>Code generation\<close>
  1305 
  1306 ML \<open>
  1307 local
  1308 
  1309 val _ =
  1310   Outer_Syntax.command \<^command_keyword>\<open>code_datatype\<close>
  1311     "define set of code datatype constructors"
  1312     (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.declare_datatype_cmd));
  1313 
  1314 in end\<close>
  1315 
  1316 
  1317 subsection \<open>Extraction of programs from proofs\<close>
  1318 
  1319 ML \<open>
  1320 local
  1321 
  1322 val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
  1323 
  1324 val _ =
  1325   Outer_Syntax.command \<^command_keyword>\<open>realizers\<close>
  1326     "specify realizers for primitive axioms / theorems, together with correctness proof"
  1327     (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
  1328      (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
  1329        (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
  1330 
  1331 val _ =
  1332   Outer_Syntax.command \<^command_keyword>\<open>realizability\<close>
  1333     "add equations characterizing realizability"
  1334     (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
  1335 
  1336 val _ =
  1337   Outer_Syntax.command \<^command_keyword>\<open>extract_type\<close>
  1338     "add equations characterizing type of extracted program"
  1339     (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
  1340 
  1341 val _ =
  1342   Outer_Syntax.command \<^command_keyword>\<open>extract\<close> "extract terms from proofs"
  1343     (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
  1344       Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
  1345 
  1346 in end\<close>
  1347 
  1348 
  1349 section \<open>Auxiliary lemmas\<close>
  1350 
  1351 subsection \<open>Meta-level connectives in assumptions\<close>
  1352 
  1353 lemma meta_mp:
  1354   assumes "PROP P \<Longrightarrow> PROP Q" and "PROP P"
  1355   shows "PROP Q"
  1356     by (rule \<open>PROP P \<Longrightarrow> PROP Q\<close> [OF \<open>PROP P\<close>])
  1357 
  1358 lemmas meta_impE = meta_mp [elim_format]
  1359 
  1360 lemma meta_spec:
  1361   assumes "\<And>x. PROP P x"
  1362   shows "PROP P x"
  1363     by (rule \<open>\<And>x. PROP P x\<close>)
  1364 
  1365 lemmas meta_allE = meta_spec [elim_format]
  1366 
  1367 lemma swap_params:
  1368   "(\<And>x y. PROP P x y) \<equiv> (\<And>y x. PROP P x y)" ..
  1369 
  1370 
  1371 subsection \<open>Meta-level conjunction\<close>
  1372 
  1373 lemma all_conjunction:
  1374   "(\<And>x. PROP A x &&& PROP B x) \<equiv> ((\<And>x. PROP A x) &&& (\<And>x. PROP B x))"
  1375 proof
  1376   assume conj: "\<And>x. PROP A x &&& PROP B x"
  1377   show "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)"
  1378   proof -
  1379     fix x
  1380     from conj show "PROP A x" by (rule conjunctionD1)
  1381     from conj show "PROP B x" by (rule conjunctionD2)
  1382   qed
  1383 next
  1384   assume conj: "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)"
  1385   fix x
  1386   show "PROP A x &&& PROP B x"
  1387   proof -
  1388     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
  1389     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
  1390   qed
  1391 qed
  1392 
  1393 lemma imp_conjunction:
  1394   "(PROP A \<Longrightarrow> PROP B &&& PROP C) \<equiv> ((PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C))"
  1395 proof
  1396   assume conj: "PROP A \<Longrightarrow> PROP B &&& PROP C"
  1397   show "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)"
  1398   proof -
  1399     assume "PROP A"
  1400     from conj [OF \<open>PROP A\<close>] show "PROP B" by (rule conjunctionD1)
  1401     from conj [OF \<open>PROP A\<close>] show "PROP C" by (rule conjunctionD2)
  1402   qed
  1403 next
  1404   assume conj: "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)"
  1405   assume "PROP A"
  1406   show "PROP B &&& PROP C"
  1407   proof -
  1408     from \<open>PROP A\<close> show "PROP B" by (rule conj [THEN conjunctionD1])
  1409     from \<open>PROP A\<close> show "PROP C" by (rule conj [THEN conjunctionD2])
  1410   qed
  1411 qed
  1412 
  1413 lemma conjunction_imp:
  1414   "(PROP A &&& PROP B \<Longrightarrow> PROP C) \<equiv> (PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C)"
  1415 proof
  1416   assume r: "PROP A &&& PROP B \<Longrightarrow> PROP C"
  1417   assume ab: "PROP A" "PROP B"
  1418   show "PROP C"
  1419   proof (rule r)
  1420     from ab show "PROP A &&& PROP B" .
  1421   qed
  1422 next
  1423   assume r: "PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C"
  1424   assume conj: "PROP A &&& PROP B"
  1425   show "PROP C"
  1426   proof (rule r)
  1427     from conj show "PROP A" by (rule conjunctionD1)
  1428     from conj show "PROP B" by (rule conjunctionD2)
  1429   qed
  1430 qed
  1431 
  1432 end