src/Pure/Isar/isar_syn.ML
author wenzelm
Fri Mar 19 11:24:00 1999 +0100 (1999-03-19)
changeset 6404 2daaf2943c79
parent 6370 e71ac23a9111
child 6501 392333eb31cb
permissions -rw-r--r--
common qed and end of proofs;
     1 (*  Title:      Pure/Isar/isar_syn.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Isar/Pure outer syntax.
     6 
     7 TODO:
     8   - '--' (comment) option almost everywhere:
     9   - add_parsers: warn if command name coincides with other keyword (if
    10     not already present) (!?);
    11   - 'result' (interactive): print current result (?);
    12   - check evaluation of transformers (exns!);
    13   - 'thms': xthms1 (vs. 'thm' (!?));
    14 *)
    15 
    16 signature ISAR_SYN =
    17 sig
    18   val keywords: string list
    19   val parsers: OuterSyntax.parser list
    20 end;
    21 
    22 structure IsarSyn: ISAR_SYN =
    23 struct
    24 
    25 open OuterParse;
    26 
    27 
    28 (** init and exit **)
    29 
    30 val theoryP =
    31   OuterSyntax.command "theory" "begin theory"
    32     (OuterSyntax.theory_header >> (Toplevel.print oo IsarThy.theory));
    33 
    34 (*end current theory / sub-proof / excursion*)
    35 val endP =
    36   OuterSyntax.command "end" "end current block / theory / excursion"
    37     (Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.proof IsarThy.end_block));
    38 
    39 val contextP =
    40   OuterSyntax.improper_command "context" "switch theory context"
    41     (name >> (Toplevel.print oo IsarThy.context));
    42 
    43 val update_contextP =
    44   OuterSyntax.improper_command "update_context" "switch theory context, forcing update"
    45     (name >> (Toplevel.print oo IsarThy.update_context));
    46 
    47 
    48 
    49 (** theory sections **)
    50 
    51 (* formal comments *)
    52 
    53 val textP = OuterSyntax.command "text" "formal comments"
    54   (text >> (Toplevel.theory o IsarThy.add_text));
    55 
    56 val titleP = OuterSyntax.command "title" "document title"
    57   ((text -- Scan.optional text "" -- Scan.optional text "")
    58     >> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));
    59 
    60 val chapterP = OuterSyntax.command "chapter" "chapter heading"
    61   (text >> (Toplevel.theory o IsarThy.add_chapter));
    62 
    63 val sectionP = OuterSyntax.command "section" "section heading"
    64   (text >> (Toplevel.theory o IsarThy.add_section));
    65 
    66 val subsectionP = OuterSyntax.command "subsection" "subsection heading"
    67   (text >> (Toplevel.theory o IsarThy.add_subsection));
    68 
    69 val subsubsectionP = OuterSyntax.command "subsubsection" "subsubsection heading"
    70   (text >> (Toplevel.theory o IsarThy.add_subsubsection));
    71 
    72 
    73 (* classes and sorts *)
    74 
    75 val classesP =
    76   OuterSyntax.command "classes" "declare type classes"
    77     (Scan.repeat1 (name -- Scan.optional ($$$ "<" |-- !!! (list1 xname)) [])
    78       >> (Toplevel.theory o Theory.add_classes));
    79 
    80 val classrelP =
    81   OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)"
    82     (xname -- ($$$ "<" |-- !!! xname) >> (Toplevel.theory o Theory.add_classrel o single));
    83 
    84 val defaultsortP =
    85   OuterSyntax.command "defaultsort" "declare default sort"
    86     (sort >> (Toplevel.theory o Theory.add_defsort));
    87 
    88 
    89 (* types *)
    90 
    91 val typedeclP =
    92   OuterSyntax.command "typedecl" "Pure type declaration"
    93     (type_args -- name -- opt_infix
    94       >> (fn ((args, a), mx) => Toplevel.theory (PureThy.add_typedecls [(a, args, mx)])));
    95 
    96 val typeabbrP =
    97   OuterSyntax.command "types" "declare type abbreviations"
    98     (Scan.repeat1 (type_args -- name -- ($$$ "=" |-- !!! (typ -- opt_infix)))
    99       >> (Toplevel.theory o Theory.add_tyabbrs o
   100         map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
   101 
   102 val nontermP =
   103   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
   104     (Scan.repeat1 name >> (Toplevel.theory o Theory.add_nonterminals));
   105 
   106 val aritiesP =
   107   OuterSyntax.command "arities" "state type arities (axiomatic!)"
   108     (Scan.repeat1 (xname -- ($$$ "::" |-- !!! arity) >> triple2)
   109       >> (Toplevel.theory o Theory.add_arities));
   110 
   111 
   112 (* consts and syntax *)
   113 
   114 val constsP =
   115   OuterSyntax.command "consts" "declare constants"
   116     (Scan.repeat1 const >> (Toplevel.theory o Theory.add_consts));
   117 
   118 val opt_mode =
   119   Scan.optional
   120     ($$$ "(" |-- !!! (name -- Scan.optional ($$$ "output" >> K false) true --| $$$ ")"))
   121     ("", true);
   122 
   123 val syntaxP =
   124   OuterSyntax.command "syntax" "declare syntactic constants"
   125     (opt_mode -- Scan.repeat1 const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
   126 
   127 
   128 (* translations *)
   129 
   130 val trans_pat =
   131   Scan.optional ($$$ "(" |-- !!! (xname --| $$$ ")")) "logic" -- string;
   132 
   133 fun trans_arrow toks =
   134   ($$$ "=>" >> K Syntax.ParseRule ||
   135     $$$ "<=" >> K Syntax.PrintRule ||
   136     $$$ "==" >> K Syntax.ParsePrintRule) toks;
   137 
   138 val trans_line =
   139   trans_pat -- !!! (trans_arrow -- trans_pat)
   140     >> (fn (left, (arr, right)) => arr (left, right));
   141 
   142 val translationsP =
   143   OuterSyntax.command "translations" "declare syntax translation rules"
   144     (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
   145 
   146 
   147 (* axioms and definitions *)
   148 
   149 val axiomsP =
   150   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)"
   151     (Scan.repeat1 spec_name >> (Toplevel.theory o IsarThy.add_axioms));
   152 
   153 val defsP =
   154   OuterSyntax.command "defs" "define constants"
   155     (Scan.repeat1 spec_opt_name >> (Toplevel.theory o IsarThy.add_defs));
   156 
   157 val constdefsP =
   158   OuterSyntax.command "constdefs" "declare and define constants"
   159     (Scan.repeat1 (const -- term) >> (Toplevel.theory o IsarThy.add_constdefs));
   160 
   161 
   162 (* theorems *)
   163 
   164 val facts = opt_thm_name "=" -- xthms1;
   165 
   166 val theoremsP =
   167   OuterSyntax.command "theorems" "define theorems"
   168     (facts >> (Toplevel.theory o IsarThy.have_theorems));
   169 
   170 val lemmasP =
   171   OuterSyntax.command "lemmas" "define lemmas"
   172     (facts >> (Toplevel.theory o IsarThy.have_lemmas));
   173 
   174 
   175 (* name space entry path *)
   176 
   177 val globalP =
   178   OuterSyntax.command "global" "disable prefixing of theory name"
   179     (Scan.succeed (Toplevel.theory PureThy.global_path));
   180 
   181 val localP =
   182   OuterSyntax.command "local" "enable prefixing of theory name"
   183     (Scan.succeed (Toplevel.theory PureThy.local_path));
   184 
   185 val pathP =
   186   OuterSyntax.command "path" "modify name-space entry path"
   187     (xname >> (Toplevel.theory o Theory.add_path));
   188 
   189 
   190 (* use ML text *)
   191 
   192 val useP =
   193   OuterSyntax.command "use" "eval ML text from file"
   194     (name >> IsarCmd.use);
   195 
   196 val mlP =
   197   OuterSyntax.command "ML" "eval ML text"
   198     (text >> (fn txt => IsarCmd.use_mltext txt o IsarCmd.use_mltext_theory txt));
   199 
   200 val setupP =
   201   OuterSyntax.command "setup" "apply ML theory transformer"
   202     (text >> (Toplevel.theory o IsarThy.use_setup));
   203 
   204 
   205 (* translation functions *)
   206 
   207 val parse_ast_translationP =
   208   OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
   209     (text >> (Toplevel.theory o IsarThy.parse_ast_translation));
   210 
   211 val parse_translationP =
   212   OuterSyntax.command "parse_translation" "install parse translation functions"
   213     (text >> (Toplevel.theory o IsarThy.parse_translation));
   214 
   215 val print_translationP =
   216   OuterSyntax.command "print_translation" "install print translation functions"
   217     (text >> (Toplevel.theory o IsarThy.print_translation));
   218 
   219 val typed_print_translationP =
   220   OuterSyntax.command "typed_print_translation" "install typed print translation functions"
   221     (text >> (Toplevel.theory o IsarThy.typed_print_translation));
   222 
   223 val print_ast_translationP =
   224   OuterSyntax.command "print_ast_translation" "install print ast translation functions"
   225     (text >> (Toplevel.theory o IsarThy.print_ast_translation));
   226 
   227 val token_translationP =
   228   OuterSyntax.command "token_translation" "install token translation functions"
   229     (text >> (Toplevel.theory o IsarThy.token_translation));
   230 
   231 
   232 (* oracles *)
   233 
   234 val oracleP =
   235   OuterSyntax.command "oracle" "install oracle"
   236     (name -- text >> (Toplevel.theory o IsarThy.add_oracle));
   237 
   238 
   239 
   240 (** proof commands **)
   241 
   242 (* statements *)
   243 
   244 val is_props = $$$ "(" |-- !!! (Scan.repeat1 ($$$ "is" |-- prop) --| $$$ ")");
   245 val propp = prop -- Scan.optional is_props [];
   246 fun statement f = opt_thm_name ":" -- propp >> (fn ((x, y), z) => f x y z);
   247 
   248 val theoremP =
   249   OuterSyntax.command "theorem" "state theorem"
   250     (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   251 
   252 val lemmaP =
   253   OuterSyntax.command "lemma" "state lemma"
   254     (statement IsarThy.lemma >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   255 
   256 val showP =
   257   OuterSyntax.command "show" "state local goal, solving current obligation"
   258     (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof f));
   259 
   260 val haveP =
   261   OuterSyntax.command "have" "state local goal"
   262     (statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));
   263 
   264 
   265 (* facts *)
   266 
   267 val thenP =
   268   OuterSyntax.command "then" "forward chaining"
   269     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.chain));
   270 
   271 val fromP =
   272   OuterSyntax.command "from" "forward chaining from given facts"
   273     (xthms1 >> (fn x => Toplevel.print o Toplevel.proof (IsarThy.from_facts x)));
   274 
   275 val factsP =
   276   OuterSyntax.command "note" "define facts"
   277     (facts >> (Toplevel.proof o IsarThy.have_facts));
   278 
   279 
   280 (* proof context *)
   281 
   282 val assumeP =
   283   OuterSyntax.command "assume" "assume propositions"
   284     (opt_thm_name ":" -- Scan.repeat1 propp >>
   285       (fn ((x, y), z) => Toplevel.print o Toplevel.proof (IsarThy.assume x y z)));
   286 
   287 val fixP =
   288   OuterSyntax.command "fix" "fix variables (Skolem constants)"
   289     (Scan.repeat1 (name -- Scan.option ($$$ "::" |-- typ))
   290       >> (fn xs => Toplevel.print o Toplevel.proof (IsarThy.fix xs)));
   291 
   292 val letP =
   293   OuterSyntax.command "let" "bind text variables"
   294     (and_list1 (enum1 "as" term -- ($$$ "=" |-- term))
   295       >> (fn bs => Toplevel.print o Toplevel.proof (IsarThy.match_bind bs)));
   296 
   297 
   298 (* proof structure *)
   299 
   300 val beginP =
   301   OuterSyntax.command "begin" "begin block"
   302     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));
   303 
   304 val nextP =
   305   OuterSyntax.command "next" "enter next block"
   306     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.next_block));
   307 
   308 
   309 (* end proof *)
   310 
   311 val kill_proofP =
   312   OuterSyntax.improper_command "kill" "abort current proof"
   313     (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
   314 
   315 val qed_withP =
   316   OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
   317     (Scan.option name -- Scan.option attribs -- Scan.option method
   318       >> (uncurry IsarThy.global_qed_with));
   319 
   320 val qedP =
   321   OuterSyntax.command "qed" "conclude (sub-)proof"
   322     (Scan.option method >> IsarThy.qed);
   323 
   324 val terminal_proofP =
   325   OuterSyntax.command "by" "terminal backward proof"
   326     (method >> (Toplevel.print oo IsarThy.terminal_proof));
   327 
   328 val immediate_proofP =
   329   OuterSyntax.command "." "immediate proof"
   330     (Scan.succeed (Toplevel.print o IsarThy.immediate_proof));
   331 
   332 val default_proofP =
   333   OuterSyntax.command ".." "default proof"
   334     (Scan.succeed (Toplevel.print o IsarThy.default_proof));
   335 
   336 
   337 (* proof steps *)
   338 
   339 val refineP =
   340   OuterSyntax.improper_command "refine" "unstructured backward proof step, ignoring facts"
   341     (method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
   342 
   343 val then_refineP =
   344   OuterSyntax.improper_command "then_refine" "unstructured backward proof step, using facts"
   345     (method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
   346 
   347 val proofP =
   348   OuterSyntax.command "proof" "backward proof"
   349     (Scan.option method >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   350 
   351 
   352 (* proof history *)
   353 
   354 val clear_undoP =
   355   OuterSyntax.improper_command "clear_undo" "clear proof command undo information"
   356     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.clear));
   357 
   358 val undoP =
   359   OuterSyntax.improper_command "undo" "undo proof command"
   360     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.undo));
   361 
   362 val redoP =
   363   OuterSyntax.improper_command "redo" "redo proof command"
   364     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.redo));
   365 
   366 val undosP =
   367   OuterSyntax.improper_command "undos" "undo proof commands"
   368     (nat >> (fn n => Toplevel.print o Toplevel.proof (ProofHistory.undos n)));
   369 
   370 val redosP =
   371   OuterSyntax.improper_command "redos" "redo proof commands"
   372     (nat >> (fn n => Toplevel.print o Toplevel.proof (ProofHistory.redos n)));
   373 
   374 val backP =
   375   OuterSyntax.improper_command "back" "backtracking of proof command"
   376     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));
   377 
   378 val prevP =
   379   OuterSyntax.improper_command "prev" "previous proof state"
   380     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.prev));
   381 
   382 val upP =
   383   OuterSyntax.improper_command "up" "upper proof state"
   384     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.up));
   385 
   386 val topP =
   387   OuterSyntax.improper_command "top" "to initial proof state"
   388     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));
   389 
   390 
   391 
   392 (** diagnostic commands (for interactive mode only) **)
   393 
   394 val print_commandsP =
   395   OuterSyntax.improper_command "help" "print outer syntax (global)"
   396     (Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
   397 
   398 val print_theoryP =
   399   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)"
   400     (Scan.succeed IsarCmd.print_theory);
   401 
   402 val print_syntaxP =
   403   OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)"
   404     (Scan.succeed IsarCmd.print_syntax);
   405 
   406 val print_theoremsP =
   407   OuterSyntax.improper_command "print_theorems" "print theorems known in this theory"
   408     (Scan.succeed IsarCmd.print_theorems);
   409 
   410 val print_attributesP =
   411   OuterSyntax.improper_command "print_attributes" "print attributes known in this theory"
   412     (Scan.succeed IsarCmd.print_attributes);
   413 
   414 val print_methodsP =
   415   OuterSyntax.improper_command "print_methods" "print methods known in this theory"
   416     (Scan.succeed IsarCmd.print_methods);
   417 
   418 val print_bindsP =
   419   OuterSyntax.improper_command "print_binds" "print term bindings of proof context"
   420     (Scan.succeed IsarCmd.print_binds);
   421 
   422 val print_lthmsP =
   423   OuterSyntax.improper_command "print_facts" "print local theorems of proof context"
   424     (Scan.succeed IsarCmd.print_lthms);
   425 
   426 val print_thmsP =
   427   OuterSyntax.improper_command "thm" "print theorems" (xthm >> IsarCmd.print_thms);
   428 
   429 val print_propP =
   430   OuterSyntax.improper_command "prop" "read and print proposition"
   431     (term >> IsarCmd.print_prop);
   432 
   433 val print_termP =
   434   OuterSyntax.improper_command "term" "read and print term"
   435     (term >> IsarCmd.print_term);
   436 
   437 val print_typeP =
   438   OuterSyntax.improper_command "type" "read and print type"
   439     (typ >> IsarCmd.print_type);
   440 
   441 
   442 
   443 (** system commands (for interactive mode only) **)
   444 
   445 val cdP =
   446   OuterSyntax.improper_command "cd" "change current working directory"
   447     (name >> IsarCmd.cd);
   448 
   449 val pwdP =
   450   OuterSyntax.improper_command "pwd" "print current working directory"
   451     (Scan.succeed IsarCmd.pwd);
   452 
   453 val use_thyP =
   454   OuterSyntax.improper_command "use_thy" "use theory file"
   455     (name >> IsarCmd.use_thy);
   456 
   457 val update_thyP =
   458   OuterSyntax.improper_command "update_thy" "update theory file"
   459     (name >> IsarCmd.update_thy);
   460 
   461 val prP =
   462   OuterSyntax.improper_command "pr" "print current toplevel state"
   463     (Scan.succeed (Toplevel.print o Toplevel.imperative (K ())));
   464 
   465 
   466 val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
   467 
   468 val commitP =
   469   OuterSyntax.improper_command "commit" "commit current session to ML database"
   470     (opt_unit >> (K IsarCmd.use_commit));
   471 
   472 val quitP =
   473   OuterSyntax.improper_command "quit" "quit Isabelle"
   474     (opt_unit >> (K IsarCmd.quit));
   475 
   476 val exitP =
   477   OuterSyntax.improper_command "exit" "exit Isar loop"
   478     (Scan.succeed IsarCmd.exit);
   479 
   480 val restartP =
   481   OuterSyntax.improper_command "restart" "restart Isar loop"
   482     (Scan.succeed IsarCmd.restart);
   483 
   484 val breakP =
   485   OuterSyntax.improper_command "break" "discontinue excursion (keep current state)"
   486     (Scan.succeed IsarCmd.break);
   487 
   488 
   489 
   490 (** the Pure outer syntax **)
   491 
   492 (*keep keywords consistent with the parsers, including those in
   493   outer_parse.ML, otherwise be prepared for unexpected errors*)
   494 
   495 val keywords =
   496  ["(", ")", "*", "+", "--", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",
   497   "?", "[", "]", "and", "as", "binder", "files", "infixl", "infixr", "is",
   498   "output", "{", "|", "}"];
   499 
   500 val parsers = [
   501   (*theory structure*)
   502   theoryP, endP, contextP, update_contextP,
   503   (*theory sections*)
   504   textP, titleP, chapterP, sectionP, subsectionP, subsubsectionP,
   505   classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
   506   aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
   507   constdefsP, theoremsP, lemmasP, globalP, localP, pathP, useP, mlP,
   508   setupP, parse_ast_translationP, parse_translationP,
   509   print_translationP, typed_print_translationP,
   510   print_ast_translationP, token_translationP, oracleP,
   511   (*proof commands*)
   512   theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
   513   factsP, beginP, nextP, kill_proofP, qed_withP, qedP,
   514   terminal_proofP, immediate_proofP, default_proofP, refineP,
   515   then_refineP, proofP, clear_undoP, undoP, redoP, undosP, redosP,
   516   backP, prevP, upP, topP,
   517   (*diagnostic commands*)
   518   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   519   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
   520   print_thmsP, print_propP, print_termP, print_typeP,
   521   (*system commands*)
   522   cdP, pwdP, use_thyP, update_thyP, prP, commitP, quitP, exitP,
   523   restartP, breakP];
   524 
   525 
   526 end;
   527 
   528 
   529 (*install the Pure outer syntax*)
   530 OuterSyntax.add_keywords IsarSyn.keywords;
   531 OuterSyntax.add_parsers IsarSyn.parsers;