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