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