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

5914

17 
 'thm': xthms1;

5832

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 / subproof / excursion*)


45 
val endP =


46 
OuterSyntax.parser false "end" "end current theory / subproof / 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 

5914

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

5832

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 

5914

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 

5832

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 namespace 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 

5937

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


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


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

5832

252 


253 
val theoremP =


254 
OuterSyntax.parser false "theorem" "state theorem"


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


256 


257 
val lemmaP =


258 
OuterSyntax.parser false "lemma" "state lemma"


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


260 


261 
val showP =


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


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


264 


265 
val haveP =


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


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


268 


269 

5914

270 
(* facts *)

5832

271 


272 
val thenP =


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


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


275 


276 
val fromP =

5914

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


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


279 


280 
val factsP =


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


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

5832

283 


284 


285 
(* proof context *)


286 


287 
val assumeP =


288 
OuterSyntax.parser false "assume" "assume propositions"

5937

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

5832

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


291 


292 
val fixP =


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

5914

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

5832

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


296 


297 
val letP =


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

5937

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

5832

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


301 


302 


303 
(* proof structure *)


304 


305 
val beginP =


306 
OuterSyntax.parser false "begin" "begin block"


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


308 


309 
val nextP =


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


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


312 


313 


314 
(* end proof *)


315 


316 
val qedP =


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


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


319 


320 
val qed_withP =


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


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


323 


324 
val kill_proofP =


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


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


327 


328 


329 
(* proof steps *)


330 


331 
fun gen_stepP meth int name cmt f =


332 
OuterSyntax.parser int name cmt


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


334 


335 
val stepP = gen_stepP method;


336 

5881

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


338 
val then_refineP =


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

5832

340 


341 


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


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


344 


345 
val trivial_proofP =


346 
OuterSyntax.parser false "." "trivial proof"


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


348 


349 
val default_proofP =


350 
OuterSyntax.parser false ".." "default proof"


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


352 


353 


354 
(* proof history *)


355 


356 
val clear_undoP =


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


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


359 


360 
val undoP =


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


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


363 


364 
val redoP =


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


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


367 


368 
val backP =


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


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


371 


372 
val prevP =


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


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


375 


376 
val upP =


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


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


379 


380 
val topP =


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


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


383 


384 


385 


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


387 


388 
val print_commandsP =


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


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


391 


392 
val print_theoryP =


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


394 
(Scan.succeed IsarCmd.print_theory);


395 


396 
val print_syntaxP =


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


398 
(Scan.succeed IsarCmd.print_syntax);


399 

5881

400 
val print_theoremsP =


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


402 
(Scan.succeed IsarCmd.print_theorems);


403 

5832

404 
val print_attributesP =

5881

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

5832

406 
(Scan.succeed IsarCmd.print_attributes);


407 


408 
val print_methodsP =

5881

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

5832

410 
(Scan.succeed IsarCmd.print_methods);


411 


412 
val print_bindsP =


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


414 
(Scan.succeed IsarCmd.print_binds);


415 


416 
val print_lthmsP =


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


418 
(Scan.succeed IsarCmd.print_lthms);


419 

5896

420 
val print_thmsP =

5914

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

5832

422 


423 
val print_propP =

5924

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

5832

425 
(term >> IsarCmd.print_prop);


426 


427 
val print_termP =

5924

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

5832

429 
(term >> IsarCmd.print_term);


430 


431 
val print_typeP =

5924

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

5832

433 
(typ >> IsarCmd.print_type);


434 


435 


436 


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


438 


439 
val cdP =


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


441 
(string >> IsarCmd.cd);


442 


443 
val pwdP =


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


445 
(Scan.succeed IsarCmd.pwd);


446 


447 
val use_thyP =


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


449 
(string >> IsarCmd.use_thy);


450 


451 
val loadP =


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

5881

453 
(name >> IsarCmd.load);

5832

454 


455 
val prP =


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


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


458 


459 


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


461 


462 
val commitP =


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


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


465 


466 
val quitP =


467 
OuterSyntax.parser true "quit" "quit Isabelle"


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


469 


470 
val exitP =


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


472 
(Scan.succeed IsarCmd.exit);


473 


474 
val breakP =

5914

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

5832

476 
(Scan.succeed IsarCmd.break);


477 


478 


479 


480 
(** the Pure outer syntax **)


481 


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


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


484 


485 
val keywords =


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

5937

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


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

5832

489 


490 
val parsers = [


491 
(*theory structure*)


492 
contextP, theoryP, endP,


493 
(*theory sections*)


494 
textP, classesP, classrelP, defaultsortP, typedeclP, typeabbrP,


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

5914

496 
theoremsP, lemmasP, axclassP, instanceP, globalP, localP, pathP,


497 
useP, mlP, setupP, parse_ast_translationP, parse_translationP,


498 
print_translationP, typed_print_translationP,


499 
print_ast_translationP, token_translationP, oracleP,

5832

500 
(*proof commands*)


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

5914

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


503 
then_refineP, proofP, terminal_proofP, trivial_proofP,


504 
default_proofP, clear_undoP, undoP, redoP, backP, prevP, upP, topP,

5832

505 
(*diagnostic commands*)


506 
print_commandsP, print_theoryP, print_syntaxP, print_attributesP,

5881

507 
print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,

5914

508 
print_thmsP, print_propP, print_termP, print_typeP,

5832

509 
(*system commands*)


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


511 


512 


513 
end;


514 


515 


516 
(* install the Pure outer syntax *)


517 


518 
OuterSyntax.add_keywords IsarSyn.keywords;


519 
OuterSyntax.add_parsers IsarSyn.parsers;
