src/Pure/Pure.thy
author wenzelm
Fri Jul 15 23:46:28 2016 +0200 (2016-07-15)
changeset 63510 0fc8be2f8176
parent 63451 c4c587aedee8
child 63513 9f8d06f23c09
permissions -rw-r--r--
singleton result for 'proof' command (without backtracking), e.g. relevant for well-defined output;
     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; Toplevel.proof (Proof.proof m #> Seq.the_result ""))));
   906 
   907 in end\<close>
   908 
   909 
   910 subsubsection \<open>Subgoal focus\<close>
   911 
   912 ML \<open>
   913 local
   914 
   915 val opt_fact_binding =
   916   Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
   917     Binding.empty_atts;
   918 
   919 val for_params =
   920   Scan.optional
   921     (@{keyword "for"} |--
   922       Parse.!!! ((Scan.option Parse.dots >> is_some) --
   923         (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
   924     (false, []);
   925 
   926 val _ =
   927   Outer_Syntax.command @{command_keyword subgoal}
   928     "focus on first subgoal within backward refinement"
   929     (opt_fact_binding -- (Scan.option (@{keyword "premises"} |-- Parse.!!! opt_fact_binding)) --
   930       for_params >> (fn ((a, b), c) =>
   931         Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
   932 
   933 in end\<close>
   934 
   935 
   936 subsubsection \<open>Calculation\<close>
   937 
   938 ML \<open>
   939 local
   940 
   941 val calculation_args =
   942   Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.thms1 --| @{keyword ")"})));
   943 
   944 val _ =
   945   Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
   946     (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd));
   947 
   948 val _ =
   949   Outer_Syntax.command @{command_keyword finally}
   950     "combine calculation and current facts, exhibit result"
   951     (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd));
   952 
   953 val _ =
   954   Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts"
   955     (Scan.succeed (Toplevel.proof' Calculation.moreover));
   956 
   957 val _ =
   958   Outer_Syntax.command @{command_keyword ultimately}
   959     "augment calculation by current facts, exhibit result"
   960     (Scan.succeed (Toplevel.proof' Calculation.ultimately));
   961 
   962 val _ =
   963   Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
   964     (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
   965 
   966 in end\<close>
   967 
   968 
   969 subsubsection \<open>Proof navigation\<close>
   970 
   971 ML \<open>
   972 local
   973 
   974 fun report_back () =
   975   Output.report [Markup.markup Markup.bad "Explicit backtracking"];
   976 
   977 val _ =
   978   Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"
   979     (Scan.succeed
   980      (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
   981       Toplevel.skip_proof report_back));
   982 
   983 in end\<close>
   984 
   985 
   986 subsection \<open>Diagnostic commands (for interactive mode only)\<close>
   987 
   988 ML \<open>
   989 local
   990 
   991 val opt_modes =
   992   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
   993 
   994 val _ =
   995   Outer_Syntax.command @{command_keyword help}
   996     "retrieve outer syntax commands according to name patterns"
   997     (Scan.repeat Parse.name >>
   998       (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats)));
   999 
  1000 val _ =
  1001   Outer_Syntax.command @{command_keyword print_commands} "print outer syntax commands"
  1002     (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of)));
  1003 
  1004 val _ =
  1005   Outer_Syntax.command @{command_keyword print_options} "print configuration options"
  1006     (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
  1007 
  1008 val _ =
  1009   Outer_Syntax.command @{command_keyword print_context}
  1010     "print context of local theory target"
  1011     (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
  1012 
  1013 val _ =
  1014   Outer_Syntax.command @{command_keyword print_theory}
  1015     "print logical theory contents"
  1016     (Parse.opt_bang >> (fn b =>
  1017       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of)));
  1018 
  1019 val _ =
  1020   Outer_Syntax.command @{command_keyword print_definitions}
  1021     "print dependencies of definitional theory content"
  1022     (Parse.opt_bang >> (fn b =>
  1023       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of)));
  1024 
  1025 val _ =
  1026   Outer_Syntax.command @{command_keyword print_syntax}
  1027     "print inner syntax of context"
  1028     (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
  1029 
  1030 val _ =
  1031   Outer_Syntax.command @{command_keyword print_defn_rules}
  1032     "print definitional rewrite rules of context"
  1033     (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
  1034 
  1035 val _ =
  1036   Outer_Syntax.command @{command_keyword print_abbrevs}
  1037     "print constant abbreviations of context"
  1038     (Parse.opt_bang >> (fn b =>
  1039       Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
  1040 
  1041 val _ =
  1042   Outer_Syntax.command @{command_keyword print_theorems}
  1043     "print theorems of local theory or proof context"
  1044     (Parse.opt_bang >> (fn b =>
  1045       Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
  1046 
  1047 val _ =
  1048   Outer_Syntax.command @{command_keyword print_locales}
  1049     "print locales of this theory"
  1050     (Parse.opt_bang >> (fn b =>
  1051       Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
  1052 
  1053 val _ =
  1054   Outer_Syntax.command @{command_keyword print_classes}
  1055     "print classes of this theory"
  1056     (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of)));
  1057 
  1058 val _ =
  1059   Outer_Syntax.command @{command_keyword print_locale}
  1060     "print locale of this theory"
  1061     (Parse.opt_bang -- Parse.position Parse.name >> (fn (b, name) =>
  1062       Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
  1063 
  1064 val _ =
  1065   Outer_Syntax.command @{command_keyword print_interps}
  1066     "print interpretations of locale for this theory or proof context"
  1067     (Parse.position Parse.name >> (fn name =>
  1068       Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
  1069 
  1070 val _ =
  1071   Outer_Syntax.command @{command_keyword print_dependencies}
  1072     "print dependencies of locale expression"
  1073     (Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (b, expr) =>
  1074       Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
  1075 
  1076 val _ =
  1077   Outer_Syntax.command @{command_keyword print_attributes}
  1078     "print attributes of this theory"
  1079     (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
  1080 
  1081 val _ =
  1082   Outer_Syntax.command @{command_keyword print_simpset}
  1083     "print context of Simplifier"
  1084     (Parse.opt_bang >> (fn b =>
  1085       Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
  1086 
  1087 val _ =
  1088   Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules"
  1089     (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
  1090 
  1091 val _ =
  1092   Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory"
  1093     (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
  1094 
  1095 val _ =
  1096   Outer_Syntax.command @{command_keyword print_antiquotations}
  1097     "print document antiquotations"
  1098     (Parse.opt_bang >> (fn b =>
  1099       Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
  1100 
  1101 val _ =
  1102   Outer_Syntax.command @{command_keyword print_ML_antiquotations}
  1103     "print ML antiquotations"
  1104     (Parse.opt_bang >> (fn b =>
  1105       Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
  1106 
  1107 val _ =
  1108   Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies"
  1109     (Scan.succeed
  1110       (Toplevel.keep (Toplevel.theory_of #> (fn thy =>
  1111         Locale.pretty_locale_deps thy
  1112         |> map (fn {name, parents, body} =>
  1113           ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
  1114         |> Graph_Display.display_graph_old))));
  1115 
  1116 val _ =
  1117   Outer_Syntax.command @{command_keyword print_term_bindings}
  1118     "print term bindings of proof context"
  1119     (Scan.succeed
  1120       (Toplevel.keep
  1121         (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
  1122 
  1123 val _ =
  1124   Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context"
  1125     (Parse.opt_bang >> (fn b =>
  1126       Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
  1127 
  1128 val _ =
  1129   Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context"
  1130     (Scan.succeed
  1131       (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
  1132 
  1133 val _ =
  1134   Outer_Syntax.command @{command_keyword print_statement}
  1135     "print theorems as long statements"
  1136     (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts);
  1137 
  1138 val _ =
  1139   Outer_Syntax.command @{command_keyword thm} "print theorems"
  1140     (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms);
  1141 
  1142 val _ =
  1143   Outer_Syntax.command @{command_keyword prf} "print proof terms of theorems"
  1144     (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false);
  1145 
  1146 val _ =
  1147   Outer_Syntax.command @{command_keyword full_prf} "print full proof terms of theorems"
  1148     (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true);
  1149 
  1150 val _ =
  1151   Outer_Syntax.command @{command_keyword prop} "read and print proposition"
  1152     (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
  1153 
  1154 val _ =
  1155   Outer_Syntax.command @{command_keyword term} "read and print term"
  1156     (opt_modes -- Parse.term >> Isar_Cmd.print_term);
  1157 
  1158 val _ =
  1159   Outer_Syntax.command @{command_keyword typ} "read and print type"
  1160     (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
  1161       >> Isar_Cmd.print_type);
  1162 
  1163 val _ =
  1164   Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup"
  1165     (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
  1166 
  1167 val _ =
  1168   Outer_Syntax.command @{command_keyword print_state}
  1169     "print current proof state (if present)"
  1170     (opt_modes >> (fn modes =>
  1171       Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state))));
  1172 
  1173 val _ =
  1174   Outer_Syntax.command @{command_keyword welcome} "print welcome message"
  1175     (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ()))));
  1176 
  1177 val _ =
  1178   Outer_Syntax.command @{command_keyword display_drafts}
  1179     "display raw source files with symbols"
  1180     (Scan.repeat1 Parse.path >> (fn names =>
  1181       Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names)))));
  1182 
  1183 in end\<close>
  1184 
  1185 
  1186 subsection \<open>Dependencies\<close>
  1187 
  1188 ML \<open>
  1189 local
  1190 
  1191 val theory_bounds =
  1192   Parse.position Parse.theory_name >> single ||
  1193   (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_name) --| @{keyword ")"});
  1194 
  1195 val _ =
  1196   Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
  1197     (Scan.option theory_bounds -- Scan.option theory_bounds >>
  1198       (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args)));
  1199 
  1200 
  1201 val class_bounds =
  1202   Parse.sort >> single ||
  1203   (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
  1204 
  1205 val _ =
  1206   Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
  1207     (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
  1208       Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args)));
  1209 
  1210 
  1211 val _ =
  1212   Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
  1213     (Parse.thms1 >> (fn args =>
  1214       Toplevel.keep (fn st =>
  1215         Thm_Deps.thm_deps (Toplevel.theory_of st)
  1216           (Attrib.eval_thms (Toplevel.context_of st) args))));
  1217 
  1218 
  1219 val thy_names =
  1220   Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_name));
  1221 
  1222 val _ =
  1223   Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
  1224     (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range =>
  1225         Toplevel.keep (fn st =>
  1226           let
  1227             val thy = Toplevel.theory_of st;
  1228             val ctxt = Toplevel.context_of st;
  1229             fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
  1230             val check = Theory.check ctxt;
  1231           in
  1232             Thm_Deps.unused_thms
  1233               (case opt_range of
  1234                 NONE => (Theory.parents_of thy, [thy])
  1235               | SOME (xs, NONE) => (map check xs, [thy])
  1236               | SOME (xs, SOME ys) => (map check xs, map check ys))
  1237             |> map pretty_thm |> Pretty.writeln_chunks
  1238           end)));
  1239 
  1240 in end\<close>
  1241 
  1242 
  1243 subsubsection \<open>Find consts and theorems\<close>
  1244 
  1245 ML \<open>
  1246 local
  1247 
  1248 val _ =
  1249   Outer_Syntax.command @{command_keyword find_consts}
  1250     "find constants by name / type patterns"
  1251     (Find_Consts.query_parser >> (fn spec =>
  1252       Toplevel.keep (fn st =>
  1253         Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec))));
  1254 
  1255 val options =
  1256   Scan.optional
  1257     (Parse.$$$ "(" |--
  1258       Parse.!!! (Scan.option Parse.nat --
  1259         Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")"))
  1260     (NONE, true);
  1261 
  1262 val _ =
  1263   Outer_Syntax.command @{command_keyword find_theorems}
  1264     "find theorems meeting specified criteria"
  1265     (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) =>
  1266       Toplevel.keep (fn st =>
  1267         Pretty.writeln
  1268           (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec))));
  1269 
  1270 in end\<close>
  1271 
  1272 
  1273 subsection \<open>Code generation\<close>
  1274 
  1275 ML \<open>
  1276 local
  1277 
  1278 val _ =
  1279   Outer_Syntax.command @{command_keyword code_datatype}
  1280     "define set of code datatype constructors"
  1281     (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
  1282 
  1283 in end\<close>
  1284 
  1285 
  1286 subsection \<open>Extraction of programs from proofs\<close>
  1287 
  1288 ML \<open>
  1289 local
  1290 
  1291 val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
  1292 
  1293 val _ =
  1294   Outer_Syntax.command @{command_keyword realizers}
  1295     "specify realizers for primitive axioms / theorems, together with correctness proof"
  1296     (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
  1297      (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
  1298        (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
  1299 
  1300 val _ =
  1301   Outer_Syntax.command @{command_keyword realizability}
  1302     "add equations characterizing realizability"
  1303     (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
  1304 
  1305 val _ =
  1306   Outer_Syntax.command @{command_keyword extract_type}
  1307     "add equations characterizing type of extracted program"
  1308     (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
  1309 
  1310 val _ =
  1311   Outer_Syntax.command @{command_keyword extract} "extract terms from proofs"
  1312     (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
  1313       Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
  1314 
  1315 in end\<close>
  1316 
  1317 
  1318 section \<open>Auxiliary lemmas\<close>
  1319 
  1320 subsection \<open>Meta-level connectives in assumptions\<close>
  1321 
  1322 lemma meta_mp:
  1323   assumes "PROP P \<Longrightarrow> PROP Q" and "PROP P"
  1324   shows "PROP Q"
  1325     by (rule \<open>PROP P \<Longrightarrow> PROP Q\<close> [OF \<open>PROP P\<close>])
  1326 
  1327 lemmas meta_impE = meta_mp [elim_format]
  1328 
  1329 lemma meta_spec:
  1330   assumes "\<And>x. PROP P x"
  1331   shows "PROP P x"
  1332     by (rule \<open>\<And>x. PROP P x\<close>)
  1333 
  1334 lemmas meta_allE = meta_spec [elim_format]
  1335 
  1336 lemma swap_params:
  1337   "(\<And>x y. PROP P x y) \<equiv> (\<And>y x. PROP P x y)" ..
  1338 
  1339 
  1340 subsection \<open>Meta-level conjunction\<close>
  1341 
  1342 lemma all_conjunction:
  1343   "(\<And>x. PROP A x &&& PROP B x) \<equiv> ((\<And>x. PROP A x) &&& (\<And>x. PROP B x))"
  1344 proof
  1345   assume conj: "\<And>x. PROP A x &&& PROP B x"
  1346   show "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)"
  1347   proof -
  1348     fix x
  1349     from conj show "PROP A x" by (rule conjunctionD1)
  1350     from conj show "PROP B x" by (rule conjunctionD2)
  1351   qed
  1352 next
  1353   assume conj: "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)"
  1354   fix x
  1355   show "PROP A x &&& PROP B x"
  1356   proof -
  1357     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
  1358     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
  1359   qed
  1360 qed
  1361 
  1362 lemma imp_conjunction:
  1363   "(PROP A \<Longrightarrow> PROP B &&& PROP C) \<equiv> ((PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C))"
  1364 proof
  1365   assume conj: "PROP A \<Longrightarrow> PROP B &&& PROP C"
  1366   show "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)"
  1367   proof -
  1368     assume "PROP A"
  1369     from conj [OF \<open>PROP A\<close>] show "PROP B" by (rule conjunctionD1)
  1370     from conj [OF \<open>PROP A\<close>] show "PROP C" by (rule conjunctionD2)
  1371   qed
  1372 next
  1373   assume conj: "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)"
  1374   assume "PROP A"
  1375   show "PROP B &&& PROP C"
  1376   proof -
  1377     from \<open>PROP A\<close> show "PROP B" by (rule conj [THEN conjunctionD1])
  1378     from \<open>PROP A\<close> show "PROP C" by (rule conj [THEN conjunctionD2])
  1379   qed
  1380 qed
  1381 
  1382 lemma conjunction_imp:
  1383   "(PROP A &&& PROP B \<Longrightarrow> PROP C) \<equiv> (PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C)"
  1384 proof
  1385   assume r: "PROP A &&& PROP B \<Longrightarrow> PROP C"
  1386   assume ab: "PROP A" "PROP B"
  1387   show "PROP C"
  1388   proof (rule r)
  1389     from ab show "PROP A &&& PROP B" .
  1390   qed
  1391 next
  1392   assume r: "PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C"
  1393   assume conj: "PROP A &&& PROP B"
  1394   show "PROP C"
  1395   proof (rule r)
  1396     from conj show "PROP A" by (rule conjunctionD1)
  1397     from conj show "PROP B" by (rule conjunctionD2)
  1398   qed
  1399 qed
  1400 
  1401 end