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