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