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