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