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