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