src/Pure/Isar/isar_syn.ML
author haftmann
Wed Feb 14 10:06:17 2007 +0100 (2007-02-14 ago)
changeset 22321 e5cddafe2629
parent 22299 a1293efe7ea5
child 22331 7df6bc8cf0b0
permissions -rw-r--r--
class package now using Locale.interpretation_i
     1 (*  Title:      Pure/Isar/isar_syn.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Isar/Pure outer syntax.
     6 *)
     7 
     8 structure IsarSyn: sig end =
     9 struct
    10 
    11 structure P = OuterParse and K = OuterKeyword;
    12 
    13 
    14 (** init and exit **)
    15 
    16 val theoryP =
    17   OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
    18     (ThyHeader.args >> (Toplevel.print oo IsarCmd.theory));
    19 
    20 val endP =
    21   OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
    22     (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
    23 
    24 
    25 (** markup commands **)
    26 
    27 val headerP = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag
    28   (P.position P.text >> IsarCmd.add_header);
    29 
    30 val chapterP = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading"
    31   K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_chapter);
    32 
    33 val sectionP = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading"
    34   K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_section);
    35 
    36 val subsectionP = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading"
    37   K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsection);
    38 
    39 val subsubsectionP =
    40   OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading"
    41   K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsubsection);
    42 
    43 val textP = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)"
    44   K.thy_decl (P.opt_target -- P.position P.text >> IsarCmd.add_text);
    45 
    46 val text_rawP = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw"
    47   "raw document preparation text"
    48   K.thy_decl (P.position P.text >> IsarCmd.add_text_raw);
    49 
    50 val sectP = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)"
    51   (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_sect);
    52 
    53 val subsectP = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)"
    54   (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_subsect);
    55 
    56 val subsubsectP = OuterSyntax.markup_command ThyOutput.Markup "subsubsect"
    57   "formal comment (proof)" (K.tag_proof K.prf_heading)
    58   (P.position P.text >> IsarCmd.add_subsubsect);
    59 
    60 val txtP = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)"
    61   (K.tag_proof K.prf_decl) (P.position P.text >> IsarCmd.add_txt);
    62 
    63 val txt_rawP = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw"
    64   "raw document preparation text (proof)" (K.tag_proof K.prf_decl)
    65   (P.position P.text >> IsarCmd.add_txt_raw);
    66 
    67 
    68 
    69 (** theory sections **)
    70 
    71 (* classes and sorts *)
    72 
    73 val classesP =
    74   OuterSyntax.command "classes" "declare type classes" K.thy_decl
    75     (Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    76         P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class));
    77 
    78 val classrelP =
    79   OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
    80     (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname))
    81     >> (Toplevel.theory o AxClass.axiomatize_classrel));
    82 
    83 val defaultsortP =
    84   OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
    85     (P.sort >> (Toplevel.theory o Theory.add_defsort));
    86 
    87 val axclassP =
    88   OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
    89     (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    90         P.!!! (P.list1 P.xname)) []
    91         -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
    92         -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
    93       >> (fn ((x, y), z) => Toplevel.theory (snd o AxClass.define_class x y z)));
    94 
    95 
    96 (* types *)
    97 
    98 val typedeclP =
    99   OuterSyntax.command "typedecl" "type declaration" K.thy_decl
   100     (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
   101       Toplevel.theory (Theory.add_typedecls [(a, args, mx)])));
   102 
   103 val typeabbrP =
   104   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
   105     (Scan.repeat1
   106       (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
   107       >> (Toplevel.theory o Theory.add_tyabbrs o
   108         map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
   109 
   110 val nontermP =
   111   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
   112     K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Theory.add_nonterminals));
   113 
   114 val aritiesP =
   115   OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
   116     (Scan.repeat1 (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2)
   117       >> (Toplevel.theory o fold AxClass.axiomatize_arity));
   118 
   119 
   120 (* consts and syntax *)
   121 
   122 val judgmentP =
   123   OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
   124     (P.const >> (Toplevel.theory o ObjectLogic.add_judgment));
   125 
   126 val constsP =
   127   OuterSyntax.command "consts" "declare constants" K.thy_decl
   128     (Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts));
   129 
   130 val opt_overloaded = P.opt_keyword "overloaded";
   131 
   132 val finalconstsP =
   133   OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl
   134     (opt_overloaded -- Scan.repeat1 P.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
   135 
   136 val mode_spec =
   137   (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
   138 
   139 val opt_mode =
   140   Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.default_mode;
   141 
   142 val syntaxP =
   143   OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
   144     (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
   145 
   146 val no_syntaxP =
   147   OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl
   148     (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.del_modesyntax));
   149 
   150 
   151 (* translations *)
   152 
   153 val trans_pat =
   154   Scan.optional (P.$$$ "(" |-- P.!!! (P.xname --| P.$$$ ")")) "logic" -- P.string;
   155 
   156 fun trans_arrow toks =
   157   ((P.$$$ "\\<rightharpoonup>" || P.$$$ "=>") >> K Syntax.ParseRule ||
   158     (P.$$$ "\\<leftharpoondown>" || P.$$$ "<=") >> K Syntax.PrintRule ||
   159     (P.$$$ "\\<rightleftharpoons>" || P.$$$ "==") >> K Syntax.ParsePrintRule) toks;
   160 
   161 val trans_line =
   162   trans_pat -- P.!!! (trans_arrow -- trans_pat)
   163     >> (fn (left, (arr, right)) => arr (left, right));
   164 
   165 val translationsP =
   166   OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
   167     (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
   168 
   169 val no_translationsP =
   170   OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl
   171     (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.del_trrules));
   172 
   173 
   174 (* axioms and definitions *)
   175 
   176 val axiomsP =
   177   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
   178     (Scan.repeat1 SpecParse.spec_name >> (Toplevel.theory o IsarCmd.add_axioms));
   179 
   180 val opt_unchecked_overloaded =
   181   Scan.optional (P.$$$ "(" |-- P.!!!
   182     (((P.$$$ "unchecked" >> K true) -- Scan.optional (P.$$$ "overloaded" >> K true) false ||
   183       P.$$$ "overloaded" >> K (false, true)) --| P.$$$ ")")) (false, false);
   184 
   185 val defsP =
   186   OuterSyntax.command "defs" "define constants" K.thy_decl
   187     (opt_unchecked_overloaded -- Scan.repeat1 SpecParse.spec_name
   188       >> (Toplevel.theory o IsarCmd.add_defs));
   189 
   190 
   191 (* old constdefs *)
   192 
   193 val old_constdecl =
   194   P.name --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
   195   P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
   196     --| Scan.option P.where_ >> P.triple1 ||
   197   P.name -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
   198 
   199 val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
   200 
   201 val structs =
   202   Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (P.simple_fixes --| P.$$$ ")")) [];
   203 
   204 val constdefsP =
   205   OuterSyntax.command "constdefs" "old-style constant definition" K.thy_decl
   206     (structs -- Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs));
   207 
   208 
   209 (* constant definitions and abbreviations *)
   210 
   211 val constdecl =
   212   P.name --
   213     (P.where_ >> K (NONE, NoSyn) ||
   214       P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
   215       Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
   216   >> P.triple2;
   217 
   218 val constdef = Scan.option constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
   219 
   220 val definitionP =
   221   OuterSyntax.command "definition" "constant definition" K.thy_decl
   222     (P.opt_target -- constdef
   223     >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args)));
   224 
   225 val abbreviationP =
   226   OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
   227     (P.opt_target -- opt_mode -- (Scan.option constdecl -- P.prop)
   228     >> (fn ((loc, mode), args) =>
   229         Toplevel.local_theory loc (Specification.abbreviation mode args)));
   230 
   231 val notationP =
   232   OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
   233     (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
   234     >> (fn ((loc, mode), args) =>
   235         Toplevel.local_theory loc (Specification.notation mode args)));
   236 
   237 
   238 (* constant specifications *)
   239 
   240 val axiomatizationP =
   241   OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
   242     (P.opt_target --
   243      (Scan.optional P.fixes [] --
   244       Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) [])
   245     >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization x y)));
   246 
   247 
   248 (* theorems *)
   249 
   250 fun theorems kind = P.opt_target -- SpecParse.name_facts
   251   >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args));
   252 
   253 val theoremsP =
   254   OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
   255 
   256 val lemmasP =
   257   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
   258 
   259 val declareP =
   260   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
   261     (P.opt_target -- (P.and_list1 SpecParse.xthms1 >> flat)
   262       >> (fn (loc, args) => Toplevel.local_theory loc
   263           (#2 o Specification.theorems "" [(("", []), args)])));
   264 
   265 
   266 (* name space entry path *)
   267 
   268 val globalP =
   269   OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
   270     (Scan.succeed (Toplevel.theory Sign.root_path));
   271 
   272 val localP =
   273   OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
   274     (Scan.succeed (Toplevel.theory Sign.local_path));
   275 
   276 val hideP =
   277   OuterSyntax.command "hide" "hide names from given name space" K.thy_decl
   278     ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >>
   279       (Toplevel.theory o uncurry Sign.hide_names));
   280 
   281 
   282 (* use ML text *)
   283 
   284 val useP =
   285   OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.diag)
   286     (P.path >> (Toplevel.no_timing oo IsarCmd.use));
   287 
   288 val mlP =
   289   OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.diag)
   290     (P.text >> IsarCmd.use_mltext true);
   291 
   292 val ml_commandP =
   293   OuterSyntax.command "ML_command" "eval ML text" (K.tag_ml K.diag)
   294     (P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
   295 
   296 val ml_setupP =
   297   OuterSyntax.command "ML_setup" "eval ML text (may change theory)" (K.tag_ml K.thy_decl)
   298     (P.text >> IsarCmd.use_mltext_theory);
   299 
   300 val setupP =
   301   OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
   302     (Scan.option P.text >> (Toplevel.theory o IsarCmd.generic_setup));
   303 
   304 val method_setupP =
   305   OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
   306     (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2))
   307       >> (Toplevel.theory o Method.method_setup));
   308 
   309 val declarationP =
   310   OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
   311     (P.opt_target -- P.text
   312     >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt)));
   313 
   314 val simproc_setupP =
   315   OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
   316     (P.opt_target --
   317       P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text --
   318       Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
   319     >> (fn ((((loc, a), b), c), d) => Toplevel.local_theory loc (IsarCmd.simproc_setup a b c d)));
   320 
   321 
   322 (* translation functions *)
   323 
   324 val trfun = P.opt_keyword "advanced" -- P.text;
   325 
   326 val parse_ast_translationP =
   327   OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
   328     (K.tag_ml K.thy_decl)
   329     (trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation));
   330 
   331 val parse_translationP =
   332   OuterSyntax.command "parse_translation" "install parse translation functions"
   333     (K.tag_ml K.thy_decl)
   334     (trfun >> (Toplevel.theory o IsarCmd.parse_translation));
   335 
   336 val print_translationP =
   337   OuterSyntax.command "print_translation" "install print translation functions"
   338     (K.tag_ml K.thy_decl)
   339     (trfun >> (Toplevel.theory o IsarCmd.print_translation));
   340 
   341 val typed_print_translationP =
   342   OuterSyntax.command "typed_print_translation" "install typed print translation functions"
   343     (K.tag_ml K.thy_decl)
   344     (trfun >> (Toplevel.theory o IsarCmd.typed_print_translation));
   345 
   346 val print_ast_translationP =
   347   OuterSyntax.command "print_ast_translation" "install print ast translation functions"
   348     (K.tag_ml K.thy_decl)
   349     (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
   350 
   351 val token_translationP =
   352   OuterSyntax.command "token_translation" "install token translation functions"
   353     (K.tag_ml K.thy_decl)
   354     (P.text >> (Toplevel.theory o IsarCmd.token_translation));
   355 
   356 
   357 (* oracles *)
   358 
   359 val oracleP =
   360   OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
   361     (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=")
   362       -- P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
   363 
   364 
   365 (* local theories *)
   366 
   367 val contextP =
   368   OuterSyntax.command "context" "enter local theory context" K.thy_decl
   369     (P.name --| P.begin >> (fn name =>
   370       Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init (SOME name))));
   371 
   372 
   373 (* locales *)
   374 
   375 val locale_val =
   376   (SpecParse.locale_expr --
   377     Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
   378   Scan.repeat1 SpecParse.context_element >> pair Locale.empty);
   379 
   380 val localeP =
   381   OuterSyntax.command "locale" "define named proof context" K.thy_decl
   382     ((P.opt_keyword "open" >> not) -- P.name
   383         -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
   384         -- P.opt_begin
   385       >> (fn (((is_open, name), (expr, elems)), begin) =>
   386           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
   387             (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin false)));
   388 
   389 val interpretationP =
   390   OuterSyntax.command "interpretation"
   391     "prove and register interpretation of locale expression in theory or locale" K.thy_goal
   392     (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
   393       >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
   394       SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts >> (fn ((x, y), z) =>
   395         Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation I x y z)));
   396 
   397 val interpretP =
   398   OuterSyntax.command "interpret"
   399     "prove and register interpretation of locale expression in proof context"
   400     (K.tag_proof K.prf_goal)
   401     (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
   402       >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Locale.interpret Seq.single x y z)));
   403 
   404 
   405 (* classes *)
   406 
   407 local
   408 
   409 val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes")
   410 
   411 val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
   412 val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element);
   413 
   414 val parse_arity =
   415   (P.xname --| P.$$$ "::" -- P.!!! P.arity)
   416     >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort));
   417 
   418 in
   419 
   420 val classP =
   421   OuterSyntax.command classK "define type class" K.thy_decl (
   422     P.name --| P.$$$ "="
   423     -- (
   424       class_subP --| P.$$$ "+" -- class_bodyP
   425       || class_subP >> rpair []
   426       || class_bodyP >> pair [])
   427     -- P.opt_begin
   428     >> (fn ((bname, (supclasses, elems)), begin) =>
   429         Toplevel.begin_local_theory begin
   430           (ClassPackage.class_cmd bname supclasses elems #-> TheoryTarget.begin true)));
   431 
   432 val instanceP =
   433   OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
   434       P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
   435            >> ClassPackage.instance_class_cmd
   436       || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
   437            >> ClassPackage.instance_sort_cmd (*experimental: by interpretation of locales*)
   438       || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
   439            >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
   440     ) >> (Toplevel.print oo Toplevel.theory_to_proof));
   441 
   442 val print_classesP =
   443   OuterSyntax.improper_command print_classesK "print classes of this theory" K.diag
   444     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
   445       o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
   446 
   447 end;
   448 
   449 
   450 
   451 (** proof commands **)
   452 
   453 (* statements *)
   454 
   455 fun gen_theorem kind =
   456   OuterSyntax.command kind ("state " ^ kind) K.thy_goal
   457     (P.opt_target -- Scan.optional (SpecParse.opt_thm_name ":" --|
   458       Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) ("", []) --
   459       SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) =>
   460       (Toplevel.print o
   461        Toplevel.local_theory_to_proof loc
   462          (Specification.theorem kind NONE (K I) a elems concl))));
   463 
   464 val theoremP = gen_theorem Thm.theoremK;
   465 val lemmaP = gen_theorem Thm.lemmaK;
   466 val corollaryP = gen_theorem Thm.corollaryK;
   467 
   468 val haveP =
   469   OuterSyntax.command "have" "state local goal"
   470     (K.tag_proof K.prf_goal)
   471     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
   472 
   473 val henceP =
   474   OuterSyntax.command "hence" "abbreviates \"then have\""
   475     (K.tag_proof K.prf_goal)
   476     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
   477 
   478 val showP =
   479   OuterSyntax.command "show" "state local goal, solving current obligation"
   480     (K.tag_proof K.prf_asm_goal)
   481     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
   482 
   483 val thusP =
   484   OuterSyntax.command "thus" "abbreviates \"then show\""
   485     (K.tag_proof K.prf_asm_goal)
   486     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
   487 
   488 
   489 (* facts *)
   490 
   491 val facts = P.and_list1 SpecParse.xthms1;
   492 
   493 val thenP =
   494   OuterSyntax.command "then" "forward chaining"
   495     (K.tag_proof K.prf_chain)
   496     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
   497 
   498 val fromP =
   499   OuterSyntax.command "from" "forward chaining from given facts"
   500     (K.tag_proof K.prf_chain)
   501     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss)));
   502 
   503 val withP =
   504   OuterSyntax.command "with" "forward chaining from given and current facts"
   505     (K.tag_proof K.prf_chain)
   506     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss)));
   507 
   508 val noteP =
   509   OuterSyntax.command "note" "define facts"
   510     (K.tag_proof K.prf_decl)
   511     (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss)));
   512 
   513 val usingP =
   514   OuterSyntax.command "using" "augment goal facts"
   515     (K.tag_proof K.prf_decl)
   516     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using)));
   517 
   518 val unfoldingP =
   519   OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
   520     (K.tag_proof K.prf_decl)
   521     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding)));
   522 
   523 
   524 (* proof context *)
   525 
   526 val fixP =
   527   OuterSyntax.command "fix" "fix local variables (Skolem constants)"
   528     (K.tag_proof K.prf_asm)
   529     (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
   530 
   531 val assumeP =
   532   OuterSyntax.command "assume" "assume propositions"
   533     (K.tag_proof K.prf_asm)
   534     (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume)));
   535 
   536 val presumeP =
   537   OuterSyntax.command "presume" "assume propositions, to be established later"
   538     (K.tag_proof K.prf_asm)
   539     (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume)));
   540 
   541 val defP =
   542   OuterSyntax.command "def" "local definition"
   543     (K.tag_proof K.prf_asm)
   544     (P.and_list1
   545       (SpecParse.opt_thm_name ":" --
   546         ((P.name -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
   547     >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
   548 
   549 val obtainP =
   550   OuterSyntax.command "obtain" "generalized existence"
   551     (K.tag_proof K.prf_asm_goal)
   552     (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement
   553       >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
   554 
   555 val guessP =
   556   OuterSyntax.command "guess" "wild guessing (unstructured)"
   557     (K.tag_proof K.prf_asm_goal)
   558     (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
   559 
   560 val letP =
   561   OuterSyntax.command "let" "bind text variables"
   562     (K.tag_proof K.prf_decl)
   563     (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term))
   564       >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind)));
   565 
   566 val case_spec =
   567   (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
   568     P.xname >> rpair []) -- SpecParse.opt_attribs >> P.triple1;
   569 
   570 val caseP =
   571   OuterSyntax.command "case" "invoke local context"
   572     (K.tag_proof K.prf_asm)
   573     (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case)));
   574 
   575 
   576 (* proof structure *)
   577 
   578 val begin_blockP =
   579   OuterSyntax.command "{" "begin explicit proof block"
   580     (K.tag_proof K.prf_open)
   581     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
   582 
   583 val end_blockP =
   584   OuterSyntax.command "}" "end explicit proof block"
   585     (K.tag_proof K.prf_close)
   586     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
   587 
   588 val nextP =
   589   OuterSyntax.command "next" "enter next proof block"
   590     (K.tag_proof K.prf_block)
   591     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
   592 
   593 
   594 (* end proof *)
   595 
   596 val qedP =
   597   OuterSyntax.command "qed" "conclude (sub-)proof"
   598     (K.tag_proof K.qed_block)
   599     (Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.qed));
   600 
   601 val terminal_proofP =
   602   OuterSyntax.command "by" "terminal backward proof"
   603     (K.tag_proof K.qed)
   604     (Method.parse -- Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.terminal_proof));
   605 
   606 val default_proofP =
   607   OuterSyntax.command ".." "default proof"
   608     (K.tag_proof K.qed)
   609     (Scan.succeed (Toplevel.print3 o IsarCmd.default_proof));
   610 
   611 val immediate_proofP =
   612   OuterSyntax.command "." "immediate proof"
   613     (K.tag_proof K.qed)
   614     (Scan.succeed (Toplevel.print3 o IsarCmd.immediate_proof));
   615 
   616 val done_proofP =
   617   OuterSyntax.command "done" "done proof"
   618     (K.tag_proof K.qed)
   619     (Scan.succeed (Toplevel.print3 o IsarCmd.done_proof));
   620 
   621 val skip_proofP =
   622   OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)"
   623     (K.tag_proof K.qed)
   624     (Scan.succeed (Toplevel.print3 o IsarCmd.skip_proof));
   625 
   626 val forget_proofP =
   627   OuterSyntax.command "oops" "forget proof"
   628     (K.tag_proof K.qed_global)
   629     (Scan.succeed Toplevel.forget_proof);
   630 
   631 
   632 (* proof steps *)
   633 
   634 val deferP =
   635   OuterSyntax.command "defer" "shuffle internal proof state"
   636     (K.tag_proof K.prf_script)
   637     (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
   638 
   639 val preferP =
   640   OuterSyntax.command "prefer" "shuffle internal proof state"
   641     (K.tag_proof K.prf_script)
   642     (P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
   643 
   644 val applyP =
   645   OuterSyntax.command "apply" "initial refinement step (unstructured)"
   646     (K.tag_proof K.prf_script)
   647     (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
   648 
   649 val apply_endP =
   650   OuterSyntax.command "apply_end" "terminal refinement (unstructured)"
   651     (K.tag_proof K.prf_script)
   652     (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
   653 
   654 val proofP =
   655   OuterSyntax.command "proof" "backward proof"
   656     (K.tag_proof K.prf_block)
   657     (Scan.option Method.parse >> (fn m => Toplevel.print o
   658       Toplevel.actual_proof (ProofHistory.applys (Proof.proof m)) o
   659       Toplevel.skip_proof (History.apply (fn i => i + 1))));
   660 
   661 
   662 (* calculational proof commands *)
   663 
   664 val calc_args =
   665   Scan.option (P.$$$ "(" |-- P.!!! ((SpecParse.xthms1 --| P.$$$ ")")));
   666 
   667 val alsoP =
   668   OuterSyntax.command "also" "combine calculation and current facts"
   669     (K.tag_proof K.prf_decl)
   670     (calc_args >> (Toplevel.proofs' o Calculation.also));
   671 
   672 val finallyP =
   673   OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
   674     (K.tag_proof K.prf_chain)
   675     (calc_args >> (Toplevel.proofs' o Calculation.finally));
   676 
   677 val moreoverP =
   678   OuterSyntax.command "moreover" "augment calculation by current facts"
   679     (K.tag_proof K.prf_decl)
   680     (Scan.succeed (Toplevel.proof' Calculation.moreover));
   681 
   682 val ultimatelyP =
   683   OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result"
   684     (K.tag_proof K.prf_chain)
   685     (Scan.succeed (Toplevel.proof' Calculation.ultimately));
   686 
   687 
   688 (* proof navigation *)
   689 
   690 val backP =
   691   OuterSyntax.command "back" "backtracking of proof command"
   692     (K.tag_proof K.prf_script)
   693     (Scan.succeed (Toplevel.print o IsarCmd.back));
   694 
   695 
   696 (* history *)
   697 
   698 val cannot_undoP =
   699   OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
   700     (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo));
   701 
   702 val redoP =
   703   OuterSyntax.improper_command "redo" "redo last command" K.control
   704     (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo));
   705 
   706 val undos_proofP =
   707   OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control
   708     (P.nat >> ((Toplevel.no_timing o Toplevel.print) oo IsarCmd.undos_proof));
   709 
   710 val undoP =
   711   OuterSyntax.improper_command "undo" "undo last command" K.control
   712     (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.undo));
   713 
   714 val killP =
   715   OuterSyntax.improper_command "kill" "kill current history node" K.control
   716     (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.kill));
   717 
   718 
   719 
   720 (** diagnostic commands (for interactive mode only) **)
   721 
   722 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
   723 val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;
   724 
   725 val pretty_setmarginP =
   726   OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
   727     K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
   728 
   729 val helpP =
   730   OuterSyntax.improper_command "help" "print outer syntax commands" K.diag
   731     (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
   732 
   733 val print_commandsP =
   734   OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag
   735     (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
   736 
   737 val print_contextP =
   738   OuterSyntax.improper_command "print_context" "print theory context name" K.diag
   739     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
   740 
   741 val print_theoryP =
   742   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
   743     (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
   744 
   745 val print_syntaxP =
   746   OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag
   747     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
   748 
   749 val print_abbrevsP =
   750   OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag
   751     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
   752 
   753 val print_theoremsP =
   754   OuterSyntax.improper_command "print_theorems"
   755       "print theorems of local theory or proof context" K.diag
   756     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems));
   757 
   758 val print_localesP =
   759   OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
   760     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
   761 
   762 val print_localeP =
   763   OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
   764     (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
   765 
   766 val print_registrationsP =
   767   OuterSyntax.improper_command "print_interps"
   768     "print interpretations of named locale" K.diag
   769     (Scan.optional (P.$$$ "!" >> K true) false -- P.xname
   770       >> (Toplevel.no_timing oo uncurry IsarCmd.print_registrations));
   771 
   772 val print_attributesP =
   773   OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
   774     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
   775 
   776 val print_simpsetP =
   777   OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag
   778     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset));
   779 
   780 val print_rulesP =
   781   OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag
   782     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
   783 
   784 val print_induct_rulesP =
   785   OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules" K.diag
   786     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_induct_rules));
   787 
   788 val print_trans_rulesP =
   789   OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag
   790     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
   791 
   792 val print_methodsP =
   793   OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag
   794     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods));
   795 
   796 val print_antiquotationsP =
   797   OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag
   798     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
   799 
   800 val class_depsP =
   801   OuterSyntax.improper_command "class_deps" "visualize class dependencies"
   802     K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
   803 
   804 val thm_depsP =
   805   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
   806     K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
   807 
   808 val criterion =
   809   P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindTheorems.Name ||
   810   P.reserved "intro" >> K FindTheorems.Intro ||
   811   P.reserved "elim" >> K FindTheorems.Elim ||
   812   P.reserved "dest" >> K FindTheorems.Dest ||
   813   P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Simp ||
   814   P.term >> FindTheorems.Pattern;
   815 
   816 val find_theoremsP =
   817   OuterSyntax.improper_command "find_theorems"
   818     "print theorems meeting specified criteria" K.diag
   819     (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
   820      Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
   821       >> (Toplevel.no_timing oo IsarCmd.find_theorems));
   822 
   823 val print_bindsP =
   824   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
   825     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
   826 
   827 val print_factsP =
   828   OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag
   829     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
   830 
   831 val print_casesP =
   832   OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
   833     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
   834 
   835 val print_stmtsP =
   836   OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag
   837     (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
   838 
   839 val print_thmsP =
   840   OuterSyntax.improper_command "thm" "print theorems" K.diag
   841     (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
   842 
   843 val print_prfsP =
   844   OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
   845     (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
   846 
   847 val print_full_prfsP =
   848   OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
   849     (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
   850 
   851 val print_propP =
   852   OuterSyntax.improper_command "prop" "read and print proposition" K.diag
   853     (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
   854 
   855 val print_termP =
   856   OuterSyntax.improper_command "term" "read and print term" K.diag
   857     (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term));
   858 
   859 val print_typeP =
   860   OuterSyntax.improper_command "typ" "read and print type" K.diag
   861     (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
   862 
   863 
   864 
   865 (** system commands (for interactive mode only) **)
   866 
   867 val cdP =
   868   OuterSyntax.improper_command "cd" "change current working directory" K.diag
   869     (P.path >> (Toplevel.no_timing oo IsarCmd.cd));
   870 
   871 val pwdP =
   872   OuterSyntax.improper_command "pwd" "print current working directory" K.diag
   873     (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
   874 
   875 val use_thyP =
   876   OuterSyntax.improper_command "use_thy" "use theory file" K.diag
   877     (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy));
   878 
   879 val use_thy_onlyP =
   880   OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML"
   881     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy_only));
   882 
   883 val update_thyP =
   884   OuterSyntax.improper_command "update_thy" "update theory file" K.diag
   885     (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy));
   886 
   887 val update_thy_onlyP =
   888   OuterSyntax.improper_command "update_thy_only" "update theory file, ignoring associated ML"
   889     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy_only));
   890 
   891 val touch_thyP =
   892   OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
   893     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
   894 
   895 val touch_all_thysP =
   896   OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag
   897     (Scan.succeed (Toplevel.no_timing o IsarCmd.touch_all_thys));
   898 
   899 val touch_child_thysP =
   900   OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
   901     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys));
   902 
   903 val remove_thyP =
   904   OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
   905     (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy));
   906 
   907 val kill_thyP =
   908   OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
   909     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy));
   910 
   911 val display_draftsP =
   912   OuterSyntax.improper_command "display_drafts" "display raw source files with symbols"
   913     K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
   914 
   915 val print_draftsP =
   916   OuterSyntax.improper_command "print_drafts" "print raw source files with symbols"
   917     K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
   918 
   919 val opt_limits =
   920   Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat);
   921 
   922 val prP =
   923   OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag
   924     (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
   925 
   926 val disable_prP =
   927   OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag
   928     (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
   929 
   930 val enable_prP =
   931   OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
   932     (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
   933 
   934 val commitP =
   935   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
   936     (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit));
   937 
   938 val quitP =
   939   OuterSyntax.improper_command "quit" "quit Isabelle" K.control
   940     (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
   941 
   942 val exitP =
   943   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
   944     (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
   945 
   946 val init_toplevelP =
   947   OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control
   948     (Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel));
   949 
   950 val welcomeP =
   951   OuterSyntax.improper_command "welcome" "print welcome message" K.diag
   952     (Scan.succeed (Toplevel.no_timing o IsarCmd.welcome));
   953 
   954 
   955 
   956 (** the Pure outer syntax **)
   957 
   958 (*keep keywords consistent with the parsers, including those in
   959   outer_parse.ML, otherwise be prepared for unexpected errors*)
   960 
   961 val _ = OuterSyntax.add_keywords
   962  ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
   963   "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
   964   "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
   965   "advanced", "and", "assumes", "attach", "begin", "binder", "concl",
   966   "constrains", "defines", "fixes", "for", "identifier", "if",
   967   "imports", "in", "includes", "infix", "infixl", "infixr", "is",
   968   "notes", "obtains", "open", "output", "overloaded", "shows",
   969   "structure", "unchecked", "uses", "where", "|"];
   970 
   971 val _ = OuterSyntax.add_parsers [
   972   (*theory structure*)
   973   theoryP, endP,
   974   (*markup commands*)
   975   headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
   976   text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
   977   (*theory sections*)
   978   classesP, classrelP, defaultsortP, axclassP, typedeclP, typeabbrP,
   979   nontermP, aritiesP, judgmentP, constsP, finalconstsP, syntaxP,
   980   no_syntaxP, translationsP, no_translationsP, axiomsP, defsP,
   981   constdefsP, definitionP, abbreviationP, notationP, axiomatizationP,
   982   theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP,
   983   ml_commandP, ml_setupP, setupP, method_setupP, declarationP,
   984   simproc_setupP, parse_ast_translationP, parse_translationP,
   985   print_translationP, typed_print_translationP,
   986   print_ast_translationP, token_translationP, oracleP, contextP,
   987   localeP, classP, instanceP,
   988   (*proof commands*)
   989   theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
   990   assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
   991   withP, noteP, usingP, unfoldingP, begin_blockP, end_blockP, nextP,
   992   qedP, terminal_proofP, default_proofP, immediate_proofP,
   993   done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP,
   994   apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
   995   cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP,
   996   interpretP,
   997   (*diagnostic commands*)
   998   pretty_setmarginP, helpP, print_classesP, print_commandsP, print_contextP,
   999   print_theoryP, print_syntaxP, print_abbrevsP, print_factsP,
  1000   print_theoremsP, print_localesP, print_localeP,
  1001   print_registrationsP, print_attributesP, print_simpsetP,
  1002   print_rulesP, print_induct_rulesP, print_trans_rulesP,
  1003   print_methodsP, print_antiquotationsP, class_depsP, thm_depsP,
  1004   find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
  1005   print_thmsP, print_prfsP, print_full_prfsP, print_propP,
  1006   print_termP, print_typeP,
  1007   (*system commands*)
  1008   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
  1009   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
  1010   kill_thyP, display_draftsP, print_draftsP, prP, disable_prP,
  1011   enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
  1012 
  1013 end;