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