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