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