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