5832

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);

5896

11 
 witness: eliminate (!);

5832

12 
 result (interactive): print current result (?);


13 
 check evaluation of transformers (exns!);


14 
 'result' command;

5958

15 
 '' (comment) option almost everywhere:

5914

16 
 'thm': xthms1;

5832

17 
*)


18 


19 
signature ISAR_SYN =


20 
sig


21 
val keywords: string list


22 
val parsers: OuterSyntax.parser list


23 
end;


24 


25 
structure IsarSyn: ISAR_SYN =


26 
struct


27 


28 
open OuterParse;


29 


30 


31 
(** init and exit **)


32 


33 
val contextP =


34 
OuterSyntax.parser false "context" "switch theory context"


35 
(name >> (fn x => Toplevel.print o Toplevel.init_theory (IsarThy.the_theory x) (K ())));


36 


37 
val theoryP =


38 
OuterSyntax.parser false "theory" "begin theory"


39 
(name  ($$$ "="  !!! (enum "+" name  (Scan.ahead eof  $$$ ":")))


40 
>> (fn x => Toplevel.print o


41 
Toplevel.init_theory (IsarThy.begin_theory x) IsarThy.end_theory));


42 


43 
(*end current theory / subproof / excursion*)


44 
val endP =


45 
OuterSyntax.parser false "end" "end current theory / subproof / excursion"


46 
(Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.proof IsarThy.end_block));


47 


48 


49 


50 
(** theory sections **)


51 


52 
(* formal comments *)


53 


54 
val textP = OuterSyntax.parser false "text" "formal comments"

5958

55 
(text >> (Toplevel.theory o IsarThy.add_text));


56 


57 
val chapterP = OuterSyntax.parser false "chapter" "chapter heading"


58 
(text >> (Toplevel.theory o IsarThy.add_chapter));


59 


60 
val sectionP = OuterSyntax.parser false "section" "section heading"


61 
(text >> (Toplevel.theory o IsarThy.add_section));


62 


63 
val subsectionP = OuterSyntax.parser false "subsection" "subsection heading"


64 
(text >> (Toplevel.theory o IsarThy.add_subsection));


65 


66 
val subsubsectionP = OuterSyntax.parser false "subsubsection" "subsubsection heading"


67 
(text >> (Toplevel.theory o IsarThy.add_subsubsection));

5832

68 


69 


70 
(* classes and sorts *)


71 


72 
val classesP =


73 
OuterSyntax.parser false "classes" "declare type classes"


74 
(Scan.repeat1 (name  Scan.optional ($$$ "<"  !!! (list1 xname)) [])


75 
>> (Toplevel.theory o Theory.add_classes));


76 


77 
val classrelP =


78 
OuterSyntax.parser false "classrel" "state inclusion of type classes (axiomatic!)"


79 
(xname  ($$$ "<"  !!! xname) >> (Toplevel.theory o Theory.add_classrel o single));


80 


81 
val defaultsortP =


82 
OuterSyntax.parser false "defaultsort" "declare default sort"


83 
(sort >> (Toplevel.theory o Theory.add_defsort));


84 


85 


86 
(* types *)


87 


88 
val typedeclP =


89 
OuterSyntax.parser false "typedecl" "declare logical type"


90 
(type_args  name  opt_infix


91 
>> (fn ((args, a), mx) => Toplevel.theory (PureThy.add_typedecls [(a, args, mx)])));


92 


93 
val typeabbrP =


94 
OuterSyntax.parser false "types" "declare type abbreviations"


95 
(Scan.repeat1 (type_args  name  ($$$ "="  !!! (typ  opt_infix)))


96 
>> (Toplevel.theory o Theory.add_tyabbrs o


97 
map (fn ((args, a), (T, mx)) => (a, args, T, mx))));


98 


99 
val nontermP =


100 
OuterSyntax.parser false "nonterminals" "declare types treated as grammar nonterminal symbols"


101 
(Scan.repeat1 name >> (Toplevel.theory o Theory.add_nonterminals));


102 


103 
val aritiesP =


104 
OuterSyntax.parser false "arities" "state type arities (axiomatic!)"


105 
(Scan.repeat1 (xname  ($$$ "::"  !!! arity) >> triple2)


106 
>> (Toplevel.theory o Theory.add_arities));


107 


108 


109 
(* consts and syntax *)


110 


111 
val constsP =


112 
OuterSyntax.parser false "consts" "declare constants"


113 
(Scan.repeat1 const >> (Toplevel.theory o Theory.add_consts));


114 


115 
val opt_mode =


116 
Scan.optional


117 
($$$ "("  !!! (name  Scan.optional ($$$ "output" >> K false) true  $$$ ")"))


118 
("", true);


119 


120 
val syntaxP =


121 
OuterSyntax.parser false "syntax" "declare syntactic constants"


122 
(opt_mode  Scan.repeat1 const >> (Toplevel.theory o uncurry Theory.add_modesyntax));


123 


124 


125 
(* translations *)


126 


127 
val trans_pat =


128 
Scan.optional ($$$ "("  !!! (xname  $$$ ")")) "logic"  string;


129 


130 
fun trans_arrow toks =


131 
($$$ "=>" >> K Syntax.ParseRule 


132 
$$$ "<=" >> K Syntax.PrintRule 


133 
$$$ "==" >> K Syntax.ParsePrintRule) toks;


134 


135 
val trans_line =


136 
trans_pat  !!! (trans_arrow  trans_pat)


137 
>> (fn (left, (arr, right)) => arr (left, right));


138 


139 
val translationsP =


140 
OuterSyntax.parser false "translations" "declare syntax translation rules"


141 
(Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));


142 


143 


144 
(* axioms and definitions *)


145 

5914

146 
val spec = thm_name ":"  prop >> (fn ((x, y), z) => ((x, z), y));


147 
val spec' = opt_thm_name ":"  prop >> (fn ((x, y), z) => ((x, z), y));

5832

148 


149 
val axiomsP =


150 
OuterSyntax.parser false "axioms" "state arbitrary propositions (axiomatic!)"


151 
(Scan.repeat1 spec >> (Toplevel.theory o IsarThy.add_axioms));


152 


153 
val defsP =


154 
OuterSyntax.parser false "defs" "define constants"


155 
(Scan.repeat1 spec' >> (Toplevel.theory o IsarThy.add_defs));


156 


157 

5914

158 
(* theorems *)


159 


160 
val facts = opt_thm_name "="  xthms1;


161 


162 
val theoremsP =


163 
OuterSyntax.parser false "theorems" "define theorems"


164 
(facts >> (Toplevel.theory o IsarThy.have_theorems));


165 


166 
val lemmasP =


167 
OuterSyntax.parser false "lemmas" "define lemmas"


168 
(facts >> (Toplevel.theory o IsarThy.have_lemmas));


169 


170 

5832

171 
(* axclass *)


172 


173 
val axclassP =


174 
OuterSyntax.parser false "axclass" "define axiomatic type class"


175 
(name  Scan.optional ($$$ "<"  !!! (list1 xname)) []  Scan.repeat (spec >> fst)


176 
>> (Toplevel.theory o uncurry AxClass.add_axclass));


177 


178 


179 
(* instance *)


180 


181 
val opt_witness =


182 
Scan.optional ($$$ "("  !!! (list1 xname  $$$ ")")) [];


183 


184 
val instanceP =


185 
OuterSyntax.parser false "instance" "prove type arity"


186 
((xname  ($$$ "<"  xname) >> AxClass.add_inst_subclass 


187 
xname  ($$$ "::"  arity) >> (AxClass.add_inst_arity o triple2))


188 
 opt_witness >> (fn (f, x) => Toplevel.theory (f x [] None)));


189 


190 


191 
(* name space entry path *)


192 


193 
val globalP =


194 
OuterSyntax.parser false "global" "disable prefixing of theory name"


195 
(Scan.succeed (Toplevel.theory PureThy.global_path));


196 


197 
val localP =


198 
OuterSyntax.parser false "local" "enable prefixing of theory name"


199 
(Scan.succeed (Toplevel.theory PureThy.local_path));


200 


201 
val pathP =


202 
OuterSyntax.parser false "path" "modify namespace entry path"


203 
(xname >> (Toplevel.theory o Theory.add_path));


204 


205 


206 
(* use ML text *)


207 


208 
val useP =


209 
OuterSyntax.parser true "use" "eval ML text from file"

5958

210 
(name >> IsarCmd.use);

5832

211 


212 
val mlP =


213 
OuterSyntax.parser false "ML" "eval ML text"


214 
(text >> (fn txt => IsarCmd.use_mltext txt o IsarCmd.use_mltext_theory txt));


215 


216 
val setupP =


217 
OuterSyntax.parser false "setup" "apply ML theory transformer"


218 
(text >> (Toplevel.theory o IsarThy.use_setup));


219 


220 


221 
(* translation functions *)


222 


223 
val parse_ast_translationP =


224 
OuterSyntax.parser false "parse_ast_translation" "install parse ast translation functions"


225 
(text >> (Toplevel.theory o IsarThy.parse_ast_translation));


226 


227 
val parse_translationP =


228 
OuterSyntax.parser false "parse_translation" "install parse translation functions"


229 
(text >> (Toplevel.theory o IsarThy.parse_translation));


230 


231 
val print_translationP =


232 
OuterSyntax.parser false "print_translation" "install print translation functions"


233 
(text >> (Toplevel.theory o IsarThy.print_translation));


234 


235 
val typed_print_translationP =


236 
OuterSyntax.parser false "typed_print_translation" "install typed print translation functions"


237 
(text >> (Toplevel.theory o IsarThy.typed_print_translation));


238 


239 
val print_ast_translationP =


240 
OuterSyntax.parser false "print_ast_translation" "install print ast translation functions"


241 
(text >> (Toplevel.theory o IsarThy.print_ast_translation));


242 


243 
val token_translationP =


244 
OuterSyntax.parser false "token_translation" "install token translation functions"


245 
(text >> (Toplevel.theory o IsarThy.token_translation));


246 


247 


248 
(* oracles *)


249 


250 
val oracleP =


251 
OuterSyntax.parser false "oracle" "install oracle"


252 
(name  text >> (Toplevel.theory o IsarThy.add_oracle));


253 


254 


255 


256 
(** proof commands **)


257 


258 
(* statements *)


259 

5937

260 
val is_props = $$$ "("  !!! (Scan.repeat1 ($$$ "is"  prop)  $$$ ")");


261 
val propp = prop  Scan.optional is_props [];


262 
fun statement f = opt_thm_name ":"  propp >> (fn ((x, y), z) => f x y z);

5832

263 


264 
val theoremP =


265 
OuterSyntax.parser false "theorem" "state theorem"


266 
(statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));


267 


268 
val lemmaP =


269 
OuterSyntax.parser false "lemma" "state lemma"


270 
(statement IsarThy.lemma >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));


271 


272 
val showP =


273 
OuterSyntax.parser false "show" "state local goal, solving current obligation"


274 
(statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof f));


275 


276 
val haveP =


277 
OuterSyntax.parser false "have" "state local goal"


278 
(statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));


279 


280 

5914

281 
(* facts *)

5832

282 


283 
val thenP =


284 
OuterSyntax.parser false "then" "forward chaining"


285 
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.chain));


286 


287 
val fromP =

5914

288 
OuterSyntax.parser false "from" "forward chaining from given facts"


289 
(xthms1 >> (fn x => Toplevel.print o Toplevel.proof (IsarThy.from_facts x)));


290 


291 
val factsP =


292 
OuterSyntax.parser false "note" "define facts"


293 
(facts >> (Toplevel.proof o IsarThy.have_facts));

5832

294 


295 


296 
(* proof context *)


297 


298 
val assumeP =


299 
OuterSyntax.parser false "assume" "assume propositions"

5937

300 
(opt_thm_name ":"  Scan.repeat1 propp >>

5832

301 
(fn ((x, y), z) => Toplevel.print o Toplevel.proof (IsarThy.assume x y z)));


302 


303 
val fixP =


304 
OuterSyntax.parser false "fix" "fix variables (Skolem constants)"

5914

305 
(Scan.repeat1 (name  Scan.option ($$$ "::"  typ))

5832

306 
>> (fn xs => Toplevel.print o Toplevel.proof (IsarThy.fix xs)));


307 


308 
val letP =


309 
OuterSyntax.parser false "let" "bind text variables"

5937

310 
(enum1 "and" (enum1 "as" term  ($$$ "="  term))

5832

311 
>> (fn bs => Toplevel.print o Toplevel.proof (IsarThy.match_bind bs)));


312 


313 


314 
(* proof structure *)


315 


316 
val beginP =


317 
OuterSyntax.parser false "begin" "begin block"


318 
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));


319 


320 
val nextP =


321 
OuterSyntax.parser false "next" "enter next block"


322 
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.next_block));


323 


324 


325 
(* end proof *)


326 


327 
val qedP =


328 
OuterSyntax.parser false "qed" "conclude proof"


329 
(Scan.succeed (Toplevel.proof_to_theory IsarThy.qed));


330 


331 
val qed_withP =


332 
OuterSyntax.parser true "qed_with" "conclude proof, may patch name and attributes"


333 
(Scan.option name  Scan.option attribs >> (Toplevel.proof_to_theory o IsarThy.qed_with));


334 


335 
val kill_proofP =


336 
OuterSyntax.parser true "kill" "abort current proof"


337 
(Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));


338 


339 


340 
(* proof steps *)


341 


342 
fun gen_stepP meth int name cmt f =


343 
OuterSyntax.parser int name cmt


344 
(meth >> (fn txt => Toplevel.print o Toplevel.proof (f txt)));


345 


346 
val stepP = gen_stepP method;


347 

5881

348 
val refineP = stepP true "refine" "unstructured backward proof step, ignoring facts" IsarThy.tac;


349 
val then_refineP =


350 
stepP true "then_refine" "unstructured backward proof step, using facts" IsarThy.then_tac;

5832

351 


352 


353 
val proofP = gen_stepP (Scan.option method) false "proof" "backward proof" IsarThy.proof;


354 
val terminal_proofP = stepP false "by" "terminal backward proof" IsarThy.terminal_proof;


355 


356 
val trivial_proofP =


357 
OuterSyntax.parser false "." "trivial proof"


358 
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.trivial_proof));


359 


360 
val default_proofP =


361 
OuterSyntax.parser false ".." "default proof"


362 
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.default_proof));


363 


364 


365 
(* proof history *)


366 


367 
val clear_undoP =


368 
OuterSyntax.parser true "clear_undo" "clear proof command undo information"


369 
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.clear));


370 


371 
val undoP =


372 
OuterSyntax.parser true "undo" "undo proof command"


373 
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.undo));


374 


375 
val redoP =


376 
OuterSyntax.parser true "redo" "redo proof command"


377 
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.redo));


378 

5944

379 
val undosP =


380 
OuterSyntax.parser true "undos" "undo proof commands"


381 
(nat >> (fn n => Toplevel.print o Toplevel.proof (ProofHistory.undos n)));


382 


383 
val redosP =


384 
OuterSyntax.parser true "redos" "redo proof commands"


385 
(nat >> (fn n => Toplevel.print o Toplevel.proof (ProofHistory.redos n)));


386 

5832

387 
val backP =


388 
OuterSyntax.parser true "back" "backtracking of proof command"


389 
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));


390 


391 
val prevP =


392 
OuterSyntax.parser true "prev" "previous proof state"


393 
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.prev));


394 


395 
val upP =


396 
OuterSyntax.parser true "up" "upper proof state"


397 
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.up));


398 


399 
val topP =


400 
OuterSyntax.parser true "top" "to initial proof state"


401 
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));


402 


403 


404 


405 
(** diagnostic commands (for interactive mode only) **)


406 


407 
val print_commandsP =


408 
OuterSyntax.parser true "help" "print outer syntax (global)"


409 
(Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));


410 


411 
val print_theoryP =


412 
OuterSyntax.parser true "print_theory" "print logical theory contents (verbose!)"


413 
(Scan.succeed IsarCmd.print_theory);


414 


415 
val print_syntaxP =


416 
OuterSyntax.parser true "print_syntax" "print inner syntax of theory (verbose!)"


417 
(Scan.succeed IsarCmd.print_syntax);


418 

5881

419 
val print_theoremsP =


420 
OuterSyntax.parser true "print_theorems" "print theorems known in this theory"


421 
(Scan.succeed IsarCmd.print_theorems);


422 

5832

423 
val print_attributesP =

5881

424 
OuterSyntax.parser true "print_attributes" "print attributes known in this theory"

5832

425 
(Scan.succeed IsarCmd.print_attributes);


426 


427 
val print_methodsP =

5881

428 
OuterSyntax.parser true "print_methods" "print methods known in this theory"

5832

429 
(Scan.succeed IsarCmd.print_methods);


430 


431 
val print_bindsP =


432 
OuterSyntax.parser true "print_binds" "print term bindings of proof context"


433 
(Scan.succeed IsarCmd.print_binds);


434 


435 
val print_lthmsP =


436 
OuterSyntax.parser true "print_facts" "print local theorems of proof context"


437 
(Scan.succeed IsarCmd.print_lthms);


438 

5896

439 
val print_thmsP =

5914

440 
OuterSyntax.parser true "thm" "print theorems" (xthm >> IsarCmd.print_thms);

5832

441 


442 
val print_propP =

5924

443 
OuterSyntax.parser true "prop" "read and print proposition"

5832

444 
(term >> IsarCmd.print_prop);


445 


446 
val print_termP =

5924

447 
OuterSyntax.parser true "term" "read and print term"

5832

448 
(term >> IsarCmd.print_term);


449 


450 
val print_typeP =

5924

451 
OuterSyntax.parser true "typ" "read and print type"

5832

452 
(typ >> IsarCmd.print_type);


453 


454 


455 


456 
(** system commands (for interactive mode only) **)


457 


458 
val cdP =


459 
OuterSyntax.parser true "cd" "change current working directory"

5958

460 
(name >> IsarCmd.cd);

5832

461 


462 
val pwdP =


463 
OuterSyntax.parser true "pwd" "print current working directory"


464 
(Scan.succeed IsarCmd.pwd);


465 


466 
val use_thyP =


467 
OuterSyntax.parser true "use_thy" "use_thy theory file"

5958

468 
(name >> IsarCmd.use_thy);

5832

469 


470 
val loadP =


471 
OuterSyntax.parser true "load" "load theory file"

5881

472 
(name >> IsarCmd.load);

5832

473 


474 
val prP =


475 
OuterSyntax.parser true "pr" "print current toplevel state"


476 
(Scan.succeed (Toplevel.print o Toplevel.imperative (K ())));


477 


478 


479 
val opt_unit = Scan.optional ($$$ "("  $$$ ")" >> (K ())) ();


480 


481 
val commitP =


482 
OuterSyntax.parser true "commit" "commit current session to ML database"


483 
(opt_unit >> (K IsarCmd.use_commit));


484 


485 
val quitP =


486 
OuterSyntax.parser true "quit" "quit Isabelle"


487 
(opt_unit >> (K IsarCmd.quit));


488 


489 
val exitP =


490 
OuterSyntax.parser true "exit" "exit Isar loop"


491 
(Scan.succeed IsarCmd.exit);


492 

5991

493 
val restartP =


494 
OuterSyntax.parser true "restart" "restart Isar loop"


495 
(Scan.succeed IsarCmd.restart);


496 

5832

497 
val breakP =

5914

498 
OuterSyntax.parser true "break" "discontinue excursion (keep current state)"

5832

499 
(Scan.succeed IsarCmd.break);


500 


501 


502 


503 
(** the Pure outer syntax **)


504 


505 
(*keep keywords consistent with the parsers, including those in


506 
outer_parse.ML, otherwise be prepared for unexpected errors*)


507 


508 
val keywords =

5958

509 
["(", ")", "*", "+", "", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",

5937

510 
"?", "[", "]", "and", "as", "binder", "infixl", "infixr", "is",


511 
"mixfix", "output", "{", "", "}"];

5832

512 


513 
val parsers = [


514 
(*theory structure*)


515 
contextP, theoryP, endP,


516 
(*theory sections*)

5958

517 
textP, chapterP, sectionP, subsectionP, subsubsectionP, classesP,


518 
classrelP, defaultsortP, typedeclP, typeabbrP, nontermP, aritiesP,


519 
constsP, syntaxP, translationsP, axiomsP, defsP, theoremsP, lemmasP,


520 
axclassP, instanceP, globalP, localP, pathP, useP, mlP, setupP,


521 
parse_ast_translationP, parse_translationP, print_translationP,


522 
typed_print_translationP, print_ast_translationP,


523 
token_translationP, oracleP,

5832

524 
(*proof commands*)


525 
theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,

5914

526 
factsP, beginP, nextP, qedP, qed_withP, kill_proofP, refineP,


527 
then_refineP, proofP, terminal_proofP, trivial_proofP,

5944

528 
default_proofP, clear_undoP, undoP, redoP, undosP, redosP, backP,


529 
prevP, upP, topP,

5832

530 
(*diagnostic commands*)


531 
print_commandsP, print_theoryP, print_syntaxP, print_attributesP,

5881

532 
print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,

5914

533 
print_thmsP, print_propP, print_termP, print_typeP,

5832

534 
(*system commands*)

5991

535 
cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, restartP, breakP];

5832

536 


537 


538 
end;


539 


540 


541 
(* install the Pure outer syntax *)


542 


543 
OuterSyntax.add_keywords IsarSyn.keywords;


544 
OuterSyntax.add_parsers IsarSyn.parsers;
