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;


15 
 '' (comment) option everywhere;


16 
 'chapter', 'section' etc.;


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"


55 
(text >> K (Toplevel.keep (K ())));


56 


57 


58 
(* classes and sorts *)


59 


60 
val classesP =


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


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


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


64 


65 
val classrelP =


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


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


68 


69 
val defaultsortP =


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


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


72 


73 


74 
(* types *)


75 


76 
val typedeclP =


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


78 
(type_args  name  opt_infix


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


80 


81 
val typeabbrP =


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


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


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


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


86 


87 
val nontermP =


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


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


90 


91 
val aritiesP =


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


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


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


95 


96 


97 
(* consts and syntax *)


98 


99 
val constsP =


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


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


102 


103 
val opt_mode =


104 
Scan.optional


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


106 
("", true);


107 


108 
val syntaxP =


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


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


111 


112 


113 
(* translations *)


114 


115 
val trans_pat =


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


117 


118 
fun trans_arrow toks =


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


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


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


122 


123 
val trans_line =


124 
trans_pat  !!! (trans_arrow  trans_pat)


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


126 


127 
val translationsP =


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


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


130 


131 


132 
(* axioms and definitions *)


133 


134 
val spec = thm_name  prop >> (fn ((x, y), z) => ((x, z), y));


135 
val spec' = opt_thm_name  prop >> (fn ((x, y), z) => ((x, z), y));


136 


137 
val axiomsP =


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


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


140 


141 
val defsP =


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


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


144 


145 


146 
(* axclass *)


147 


148 
val axclassP =


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


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


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


152 


153 


154 
(* instance *)


155 


156 
val opt_witness =


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


158 


159 
val instanceP =


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


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


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


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


164 


165 


166 
(* name space entry path *)


167 


168 
val globalP =


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


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


171 


172 
val localP =


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


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


175 


176 
val pathP =


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


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


179 


180 


181 
(* use ML text *)


182 


183 
val useP =


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


185 
(string >> IsarCmd.use);


186 


187 
val mlP =


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


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


190 


191 
val setupP =


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


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


194 


195 


196 
(* translation functions *)


197 


198 
val parse_ast_translationP =


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


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


201 


202 
val parse_translationP =


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


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


205 


206 
val print_translationP =


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


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


209 


210 
val typed_print_translationP =


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


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


213 


214 
val print_ast_translationP =


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


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


217 


218 
val token_translationP =


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


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


221 


222 


223 
(* oracles *)


224 


225 
val oracleP =


226 
OuterSyntax.parser false "oracle" "install oracle"


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


228 


229 


230 


231 
(** proof commands **)


232 


233 
(* statements *)


234 


235 
fun statement f = opt_thm_name  prop >> (fn ((x, y), z) => f x y z);


236 


237 
val theoremP =


238 
OuterSyntax.parser false "theorem" "state theorem"


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


240 


241 
val lemmaP =


242 
OuterSyntax.parser false "lemma" "state lemma"


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


244 


245 
val showP =


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


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


248 


249 
val haveP =


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


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


252 


253 


254 
(* forward chaining *)


255 


256 
val thenP =


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


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


259 


260 
val fromP =


261 
OuterSyntax.parser false "from" "forward chaining, from given facts"


262 
(enum1 "," xname >> (fn x => Toplevel.print o Toplevel.proof (IsarThy.from_facts x)));


263 


264 


265 
(* proof context *)


266 


267 
val assumeP =


268 
OuterSyntax.parser false "assume" "assume propositions"


269 
(opt_thm_name  enum1 "," prop >>


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


271 


272 
val fixP =


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


274 
(enum1 "," (name  Scan.option ($$$ "::"  typ))


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


276 


277 
val letP =


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


279 
(enum1 "and" (term  ($$$ "="  term))


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


281 


282 


283 
(* proof structure *)


284 


285 
val beginP =


286 
OuterSyntax.parser false "begin" "begin block"


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


288 


289 
val nextP =


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


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


292 


293 


294 
(* end proof *)


295 


296 
val qedP =


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


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


299 


300 
val qed_withP =


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


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


303 


304 
val kill_proofP =


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


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


307 


308 


309 
(* proof steps *)


310 


311 
fun gen_stepP meth int name cmt f =


312 
OuterSyntax.parser int name cmt


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


314 


315 
val stepP = gen_stepP method;


316 

5881

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


318 
val then_refineP =


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

5832

320 


321 


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


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


324 


325 
val trivial_proofP =


326 
OuterSyntax.parser false "." "trivial proof"


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


328 


329 
val default_proofP =


330 
OuterSyntax.parser false ".." "default proof"


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


332 


333 


334 
(* proof history *)


335 


336 
val clear_undoP =


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


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


339 


340 
val undoP =


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


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


343 


344 
val redoP =


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


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


347 


348 
val backP =


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


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


351 


352 
val prevP =


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


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


355 


356 
val upP =


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


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


359 


360 
val topP =


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


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


363 


364 


365 


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


367 


368 
val print_commandsP =


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


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


371 


372 
val print_theoryP =


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


374 
(Scan.succeed IsarCmd.print_theory);


375 


376 
val print_syntaxP =


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


378 
(Scan.succeed IsarCmd.print_syntax);


379 

5881

380 
val print_theoremsP =


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


382 
(Scan.succeed IsarCmd.print_theorems);


383 

5832

384 
val print_attributesP =

5881

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

5832

386 
(Scan.succeed IsarCmd.print_attributes);


387 


388 
val print_methodsP =

5881

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

5832

390 
(Scan.succeed IsarCmd.print_methods);


391 


392 
val print_bindsP =


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


394 
(Scan.succeed IsarCmd.print_binds);


395 


396 
val print_lthmsP =


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


398 
(Scan.succeed IsarCmd.print_lthms);


399 

5896

400 
val print_thmsP =


401 
OuterSyntax.parser true "thms" "print theorems"


402 
(xname  opt_attribs >> IsarCmd.print_thms);


403 

5832

404 
val print_thmP =

5896

405 
OuterSyntax.parser true "thm" "print theorem"


406 
(xname  opt_attribs >> IsarCmd.print_thm);

5832

407 


408 
val print_propP =


409 
OuterSyntax.parser true "print_prop" "read and print proposition"


410 
(term >> IsarCmd.print_prop);


411 


412 
val print_termP =


413 
OuterSyntax.parser true "print_term" "read and print term"


414 
(term >> IsarCmd.print_term);


415 


416 
val print_typeP =


417 
OuterSyntax.parser true "print_type" "read and print type"


418 
(typ >> IsarCmd.print_type);


419 


420 


421 


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


423 


424 
val cdP =


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


426 
(string >> IsarCmd.cd);


427 


428 
val pwdP =


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


430 
(Scan.succeed IsarCmd.pwd);


431 


432 
val use_thyP =


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


434 
(string >> IsarCmd.use_thy);


435 


436 
val loadP =


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

5881

438 
(name >> IsarCmd.load);

5832

439 


440 
val prP =


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


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


443 


444 


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


446 


447 
val commitP =


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


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


450 


451 
val quitP =


452 
OuterSyntax.parser true "quit" "quit Isabelle"


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


454 


455 
val exitP =


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


457 
(Scan.succeed IsarCmd.exit);


458 


459 
val breakP =


460 
OuterSyntax.parser true "break" "discontinue execution"


461 
(Scan.succeed IsarCmd.break);


462 


463 


464 


465 
(** the Pure outer syntax **)


466 


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


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


469 


470 
val keywords =


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


472 
"?", "[", "]", "and", "binder", "infixl", "infixr", "mixfix", "output",


473 
"{", "", "}"];


474 


475 
val parsers = [


476 
(*theory structure*)


477 
contextP, theoryP, endP,


478 
(*theory sections*)


479 
textP, classesP, classrelP, defaultsortP, typedeclP, typeabbrP,


480 
nontermP, aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,


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


482 
parse_ast_translationP, parse_translationP, print_translationP,


483 
typed_print_translationP, print_ast_translationP,


484 
token_translationP, oracleP,


485 
(*proof commands*)


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

5881

487 
beginP, nextP, qedP, qed_withP, kill_proofP, refineP, then_refineP,


488 
proofP, terminal_proofP, trivial_proofP, default_proofP,


489 
clear_undoP, undoP, redoP, backP, prevP, upP, topP,

5832

490 
(*diagnostic commands*)


491 
print_commandsP, print_theoryP, print_syntaxP, print_attributesP,

5881

492 
print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,

5896

493 
print_thmP, print_thmsP, print_propP, print_termP, print_typeP,

5832

494 
(*system commands*)


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


496 


497 


498 
end;


499 


500 


501 
(* install the Pure outer syntax *)


502 


503 
OuterSyntax.add_keywords IsarSyn.keywords;


504 
OuterSyntax.add_parsers IsarSyn.parsers;
