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