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