5832

1 
(* Title: Pure/Isar/isar_syn.ML


2 
ID: $Id$


3 
Author: Markus Wenzel, TU Muenchen


4 

6353

5 
Isar/Pure outer syntax.

5832

6 


7 
TODO:

6245

8 
 add_parsers: warn if command name coincides with other keyword (if


9 
not already present) (!?);

5832

10 
 constdefs;


11 
 axclass axioms: attribs;


12 
 instance: theory_to_proof (with special attribute to add result arity);

5896

13 
 witness: eliminate (!);

5832

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


15 
 check evaluation of transformers (exns!);


16 
 'result' command;

5958

17 
 '' (comment) option almost everywhere:

6353

18 
 'thms': xthms1 (vs. 'thm' (!?));

5832

19 
*)


20 


21 
signature ISAR_SYN =


22 
sig


23 
val keywords: string list


24 
val parsers: OuterSyntax.parser list


25 
end;


26 


27 
structure IsarSyn: ISAR_SYN =


28 
struct


29 


30 
open OuterParse;


31 


32 


33 
(** init and exit **)


34 


35 
val theoryP =


36 
OuterSyntax.parser false "theory" "begin theory"

6245

37 
(OuterSyntax.theory_header >> (Toplevel.print oo IsarThy.theory));

5832

38 


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


40 
val endP =


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


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


43 

6245

44 
val contextP =


45 
OuterSyntax.parser true "context" "switch theory context"


46 
(name >> (Toplevel.print oo IsarThy.context));


47 


48 
val update_contextP =


49 
OuterSyntax.parser true "update_context" "switch theory context, forcing update"


50 
(name >> (Toplevel.print oo IsarThy.update_context));


51 

5832

52 


53 


54 
(** theory sections **)


55 


56 
(* formal comments *)


57 


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

5958

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


60 

6353

61 
val titleP = OuterSyntax.parser false "title" "document title"


62 
((text  Scan.optional text ""  Scan.optional text "")


63 
>> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));


64 

5958

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


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


67 


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


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


70 


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


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


73 


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


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

5832

76 


77 


78 
(* classes and sorts *)


79 


80 
val classesP =


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


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


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


84 


85 
val classrelP =


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


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


88 


89 
val defaultsortP =


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


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


92 


93 


94 
(* types *)


95 


96 
val typedeclP =

6353

97 
OuterSyntax.parser false "typedecl" "Pure type declaration"

5832

98 
(type_args  name  opt_infix


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


100 


101 
val typeabbrP =


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


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


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


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


106 


107 
val nontermP =


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


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


110 


111 
val aritiesP =


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


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


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


115 


116 


117 
(* consts and syntax *)


118 


119 
val constsP =


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


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


122 


123 
val opt_mode =


124 
Scan.optional


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


126 
("", true);


127 


128 
val syntaxP =


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


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


131 


132 


133 
(* translations *)


134 


135 
val trans_pat =


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


137 


138 
fun trans_arrow toks =


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


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


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


142 


143 
val trans_line =


144 
trans_pat  !!! (trans_arrow  trans_pat)


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


146 


147 
val translationsP =


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


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


150 


151 


152 
(* axioms and definitions *)


153 

5914

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


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

5832

156 


157 
val axiomsP =


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


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


160 


161 
val defsP =


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


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


164 


165 

5914

166 
(* theorems *)


167 


168 
val facts = opt_thm_name "="  xthms1;


169 


170 
val theoremsP =


171 
OuterSyntax.parser false "theorems" "define theorems"


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


173 


174 
val lemmasP =


175 
OuterSyntax.parser false "lemmas" "define lemmas"


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


177 


178 

5832

179 
(* axclass *)


180 


181 
val axclassP =


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


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


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


185 


186 


187 
(* instance *)


188 


189 
val opt_witness =


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


191 


192 
val instanceP =


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


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


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


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


197 


198 


199 
(* name space entry path *)


200 


201 
val globalP =


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


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


204 


205 
val localP =


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


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


208 


209 
val pathP =


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


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


212 


213 


214 
(* use ML text *)


215 


216 
val useP =

6265

217 
OuterSyntax.parser false "use" "eval ML text from file"

5958

218 
(name >> IsarCmd.use);

5832

219 


220 
val mlP =


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


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


223 


224 
val setupP =


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


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


227 


228 


229 
(* translation functions *)


230 


231 
val parse_ast_translationP =


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


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


234 


235 
val parse_translationP =


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


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


238 


239 
val print_translationP =


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


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


242 


243 
val typed_print_translationP =


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


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


246 


247 
val print_ast_translationP =


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


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


250 


251 
val token_translationP =


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


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


254 


255 


256 
(* oracles *)


257 


258 
val oracleP =


259 
OuterSyntax.parser false "oracle" "install oracle"


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


261 


262 


263 


264 
(** proof commands **)


265 


266 
(* statements *)


267 

5937

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


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


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

5832

271 


272 
val theoremP =


273 
OuterSyntax.parser false "theorem" "state theorem"


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


275 


276 
val lemmaP =


277 
OuterSyntax.parser false "lemma" "state lemma"


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


279 


280 
val showP =


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


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


283 


284 
val haveP =


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


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


287 


288 

5914

289 
(* facts *)

5832

290 


291 
val thenP =


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


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


294 


295 
val fromP =

5914

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


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


298 


299 
val factsP =


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


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

5832

302 


303 


304 
(* proof context *)


305 


306 
val assumeP =


307 
OuterSyntax.parser false "assume" "assume propositions"

6013

308 
(opt_thm_name ":"  and_list1 propp >>

5832

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


310 


311 
val fixP =


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

6013

313 
(and_list1 (name  Scan.option ($$$ "::"  typ))

5832

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


315 


316 
val letP =


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

6013

318 
(and_list1 (enum1 "as" term  ($$$ "="  term))

5832

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


320 


321 


322 
(* proof structure *)


323 


324 
val beginP =


325 
OuterSyntax.parser false "begin" "begin block"


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


327 


328 
val nextP =


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


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


331 


332 


333 
(* end proof *)


334 


335 
val qedP =


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


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


338 


339 
val qed_withP =


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


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


342 


343 
val kill_proofP =


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


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


346 


347 


348 
(* proof steps *)


349 


350 
fun gen_stepP meth int name cmt f =


351 
OuterSyntax.parser int name cmt


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


353 


354 
val stepP = gen_stepP method;


355 

5881

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


357 
val then_refineP =


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

5832

359 


360 


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


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


363 

6108

364 
val immediate_proofP =


365 
OuterSyntax.parser false "." "immediate proof"


366 
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.immediate_proof));

5832

367 


368 
val default_proofP =


369 
OuterSyntax.parser false ".." "default proof"


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


371 


372 


373 
(* proof history *)


374 


375 
val clear_undoP =


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


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


378 


379 
val undoP =


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


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


382 


383 
val redoP =


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


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


386 

5944

387 
val undosP =


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


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


390 


391 
val redosP =


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


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


394 

5832

395 
val backP =


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


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


398 


399 
val prevP =


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


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


402 


403 
val upP =


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


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


406 


407 
val topP =


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


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


410 


411 


412 


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


414 


415 
val print_commandsP =


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


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


418 


419 
val print_theoryP =


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


421 
(Scan.succeed IsarCmd.print_theory);


422 


423 
val print_syntaxP =


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


425 
(Scan.succeed IsarCmd.print_syntax);


426 

5881

427 
val print_theoremsP =


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


429 
(Scan.succeed IsarCmd.print_theorems);


430 

5832

431 
val print_attributesP =

5881

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

5832

433 
(Scan.succeed IsarCmd.print_attributes);


434 


435 
val print_methodsP =

5881

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

5832

437 
(Scan.succeed IsarCmd.print_methods);


438 


439 
val print_bindsP =


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


441 
(Scan.succeed IsarCmd.print_binds);


442 


443 
val print_lthmsP =


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


445 
(Scan.succeed IsarCmd.print_lthms);


446 

5896

447 
val print_thmsP =

5914

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

5832

449 


450 
val print_propP =

5924

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

5832

452 
(term >> IsarCmd.print_prop);


453 


454 
val print_termP =

5924

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

5832

456 
(term >> IsarCmd.print_term);


457 


458 
val print_typeP =

6353

459 
OuterSyntax.parser true "type" "read and print type"

5832

460 
(typ >> IsarCmd.print_type);


461 


462 


463 


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


465 


466 
val cdP =


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

5958

468 
(name >> IsarCmd.cd);

5832

469 


470 
val pwdP =


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


472 
(Scan.succeed IsarCmd.pwd);


473 


474 
val use_thyP =

6196

475 
OuterSyntax.parser true "use_thy" "use theory file"

5958

476 
(name >> IsarCmd.use_thy);

5832

477 

6196

478 
val update_thyP =


479 
OuterSyntax.parser true "update_thy" "update theory file"

6197

480 
(name >> IsarCmd.update_thy);

5832

481 


482 
val prP =


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


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


485 


486 


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


488 


489 
val commitP =


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


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


492 


493 
val quitP =


494 
OuterSyntax.parser true "quit" "quit Isabelle"


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


496 


497 
val exitP =


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


499 
(Scan.succeed IsarCmd.exit);


500 

5991

501 
val restartP =


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


503 
(Scan.succeed IsarCmd.restart);


504 

5832

505 
val breakP =

5914

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

5832

507 
(Scan.succeed IsarCmd.break);


508 


509 


510 


511 
(** the Pure outer syntax **)


512 


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


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


515 


516 
val keywords =

5958

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

6265

518 
"?", "[", "]", "and", "as", "binder", "files", "infixl", "infixr", "is",

6013

519 
"output", "{", "", "}"];

5832

520 


521 
val parsers = [


522 
(*theory structure*)

6245

523 
theoryP, endP, contextP, update_contextP,

5832

524 
(*theory sections*)

6353

525 
textP, titleP, chapterP, sectionP, subsectionP, subsubsectionP, classesP,

5958

526 
classrelP, defaultsortP, typedeclP, typeabbrP, nontermP, aritiesP,


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


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


529 
parse_ast_translationP, parse_translationP, print_translationP,


530 
typed_print_translationP, print_ast_translationP,


531 
token_translationP, oracleP,

5832

532 
(*proof commands*)


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

5914

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

6108

535 
then_refineP, proofP, terminal_proofP, immediate_proofP,

5944

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


537 
prevP, upP, topP,

5832

538 
(*diagnostic commands*)


539 
print_commandsP, print_theoryP, print_syntaxP, print_attributesP,

5881

540 
print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,

5914

541 
print_thmsP, print_propP, print_termP, print_typeP,

5832

542 
(*system commands*)

6196

543 
cdP, pwdP, use_thyP, update_thyP, prP, commitP, quitP, exitP,


544 
restartP, breakP];

5832

545 


546 


547 
end;


548 


549 

6196

550 
(*install the Pure outer syntax*)

5832

551 
OuterSyntax.add_keywords IsarSyn.keywords;


552 
OuterSyntax.add_parsers IsarSyn.parsers;
