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