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