author  wenzelm 
Sun, 15 Mar 2009 15:59:43 +0100  
changeset 30526  7f9a9ec1c94d 
parent 30484  bc2a4dc6f1be 
child 30544  0ed8fe16331a 
permissions  rwrr 
5832  1 
(* Title: Pure/Isar/isar_syn.ML 
2 
Author: Markus Wenzel, TU Muenchen 

3 

6353  4 
Isar/Pure outer syntax. 
5832  5 
*) 
6 

17353  7 
structure IsarSyn: sig end = 
5832  8 
struct 
9 

17068  10 
structure P = OuterParse and K = OuterKeyword; 
5832  11 

12 

24868  13 
(** keywords **) 
14 

15 
(*keep keywords consistent with the parsers, otherwise be prepared for 

16 
unexpected errors*) 

17 

27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
27200
diff
changeset

18 
val _ = List.app OuterKeyword.keyword 
24868  19 
["!!", "!", "%", "(", ")", "+", ",", "", ":", "::", ";", "<", "<=", 
20 
"=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>", 

21 
"\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]", 

26888  22 
"advanced", "and", "assumes", "attach", "begin", "binder", 
24868  23 
"constrains", "defines", "fixes", "for", "identifier", "if", 
28721  24 
"imports", "in", "infix", "infixl", "infixr", "is", 
25003  25 
"notes", "obtains", "open", "output", "overloaded", "shows", 
24868  26 
"structure", "unchecked", "uses", "where", ""]; 
27 

28 

5832  29 
(** init and exit **) 
30 

24868  31 
val _ = 
17068  32 
OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin) 
27575  33 
(ThyHeader.args >> (Toplevel.print oo IsarCmd.init_theory)); 
5832  34 

24868  35 
val _ = 
20958  36 
OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end) 
21004  37 
(Scan.succeed (Toplevel.exit o Toplevel.end_local_theory)); 
6687  38 

5832  39 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

40 

7749  41 
(** markup commands **) 
5832  42 

24868  43 
val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

44 
(P.doc_source >> IsarCmd.header_markup); 
6353  45 

24868  46 
val _ = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

47 
K.thy_heading (P.opt_target  P.doc_source >> IsarCmd.local_theory_markup); 
5958  48 

24868  49 
val _ = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

50 
K.thy_heading (P.opt_target  P.doc_source >> IsarCmd.local_theory_markup); 
5958  51 

24868  52 
val _ = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

53 
K.thy_heading (P.opt_target  P.doc_source >> IsarCmd.local_theory_markup); 
5958  54 

24868  55 
val _ = 
22117  56 
OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

57 
K.thy_heading (P.opt_target  P.doc_source >> IsarCmd.local_theory_markup); 
5832  58 

24868  59 
val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

60 
K.thy_decl (P.opt_target  P.doc_source >> IsarCmd.local_theory_markup); 
7172  61 

27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

62 
val _ = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw" "raw document preparation text" 
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

63 
K.thy_decl (P.opt_target  P.doc_source >> IsarCmd.local_theory_markup); 
7172  64 

24868  65 
val _ = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

66 
(K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup); 
7172  67 

24868  68 
val _ = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

69 
(K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup); 
7172  70 

27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

71 
val _ = OuterSyntax.markup_command ThyOutput.Markup "subsubsect" "formal comment (proof)" 
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

72 
(K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup); 
7172  73 

24868  74 
val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)" 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

75 
(K.tag_proof K.prf_decl) (P.doc_source >> IsarCmd.proof_markup); 
7172  76 

24868  77 
val _ = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw" 
17068  78 
"raw document preparation text (proof)" (K.tag_proof K.prf_decl) 
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27854
diff
changeset

79 
(P.doc_source >> IsarCmd.proof_markup); 
7775  80 

5832  81 

6886  82 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

83 
(** theory commands **) 
6886  84 

5832  85 
(* classes and sorts *) 
86 

24868  87 
val _ = 
6723  88 
OuterSyntax.command "classes" "declare type classes" K.thy_decl 
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30334
diff
changeset

89 
(Scan.repeat1 (P.binding  Scan.optional ((P.$$$ "\\<subseteq>"  P.$$$ "<")  
24932
86ef9a828a9e
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24914
diff
changeset

90 
P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd)); 
5832  91 

24868  92 
val _ = 
6723  93 
OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl 
14779  94 
(P.and_list1 (P.xname  ((P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! P.xname)) 
24932
86ef9a828a9e
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24914
diff
changeset

95 
>> (Toplevel.theory o AxClass.axiomatize_classrel_cmd)); 
5832  96 

24868  97 
val _ = 
6723  98 
OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl 
22796  99 
(P.sort >> (Toplevel.theory o Sign.add_defsort)); 
5832  100 

24868  101 
val _ = 
19245  102 
OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl 
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30334
diff
changeset

103 
(P.binding  Scan.optional ((P.$$$ "\\<subseteq>"  P.$$$ "<")  
21462
74ddf3a522f8
added Isar syntax for adding parameters to axclasses
haftmann
parents:
21437
diff
changeset

104 
P.!!! (P.list1 P.xname)) [] 
22117  105 
 Scan.repeat (SpecParse.thm_name ":"  (P.prop >> single)) 
24219  106 
>> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y))); 
19245  107 

5832  108 

109 
(* types *) 

110 

24868  111 
val _ = 
12624  112 
OuterSyntax.command "typedecl" "type declaration" K.thy_decl 
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30334
diff
changeset

113 
(P.type_args  P.binding  P.opt_infix >> (fn ((args, a), mx) => 
25495  114 
Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd))); 
5832  115 

24868  116 
val _ = 
6723  117 
OuterSyntax.command "types" "declare type abbreviations" K.thy_decl 
6727  118 
(Scan.repeat1 
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30334
diff
changeset

119 
(P.type_args  P.binding  (P.$$$ "="  P.!!! (P.typ  P.opt_infix'))) 
22796  120 
>> (Toplevel.theory o Sign.add_tyabbrs o 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

121 
map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); 
5832  122 

24868  123 
val _ = 
6370  124 
OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols" 
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30334
diff
changeset

125 
K.thy_decl (Scan.repeat1 P.binding >> (Toplevel.theory o Sign.add_nonterminals)); 
5832  126 

24868  127 
val _ = 
6723  128 
OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl 
24932
86ef9a828a9e
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24914
diff
changeset

129 
(Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd)); 
5832  130 

131 

132 
(* consts and syntax *) 

133 

24868  134 
val _ = 
8227  135 
OuterSyntax.command "judgment" "declare objectlogic judgment" K.thy_decl 
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30334
diff
changeset

136 
(P.const_binding >> (Toplevel.theory o ObjectLogic.add_judgment_cmd)); 
8227  137 

24868  138 
val _ = 
6723  139 
OuterSyntax.command "consts" "declare constants" K.thy_decl 
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30334
diff
changeset

140 
(Scan.repeat1 P.const_binding >> (Toplevel.theory o Sign.add_consts)); 
5832  141 

14642  142 
val opt_overloaded = P.opt_keyword "overloaded"; 
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
13802
diff
changeset

143 

24868  144 
val _ = 
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
13802
diff
changeset

145 
OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
13802
diff
changeset

146 
(opt_overloaded  Scan.repeat1 P.term >> (uncurry (Toplevel.theory oo Theory.add_finals))); 
9731  147 

12142  148 
val mode_spec = 
9731  149 
(P.$$$ "output" >> K ("", false))  P.name  Scan.optional (P.$$$ "output" >> K false) true; 
150 

14900  151 
val opt_mode = 
24960  152 
Scan.optional (P.$$$ "("  P.!!! (mode_spec  P.$$$ ")")) Syntax.mode_default; 
5832  153 

24868  154 
val _ = 
6723  155 
OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl 
22796  156 
(opt_mode  Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.add_modesyntax)); 
5832  157 

24868  158 
val _ = 
15748  159 
OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl 
22796  160 
(opt_mode  Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.del_modesyntax)); 
15748  161 

5832  162 

163 
(* translations *) 

164 

165 
val trans_pat = 

6723  166 
Scan.optional (P.$$$ "("  P.!!! (P.xname  P.$$$ ")")) "logic"  P.string; 
5832  167 

168 
fun trans_arrow toks = 

10688  169 
((P.$$$ "\\<rightharpoonup>"  P.$$$ "=>") >> K Syntax.ParseRule  
170 
(P.$$$ "\\<leftharpoondown>"  P.$$$ "<=") >> K Syntax.PrintRule  

171 
(P.$$$ "\\<rightleftharpoons>"  P.$$$ "==") >> K Syntax.ParsePrintRule) toks; 

5832  172 

173 
val trans_line = 

6723  174 
trans_pat  P.!!! (trans_arrow  trans_pat) 
5832  175 
>> (fn (left, (arr, right)) => arr (left, right)); 
176 

24868  177 
val _ = 
6723  178 
OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl 
22796  179 
(Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules)); 
5832  180 

24868  181 
val _ = 
19260  182 
OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl 
22796  183 
(Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules)); 
19260  184 

5832  185 

186 
(* axioms and definitions *) 

187 

30484
bc2a4dc6f1be
old name_spec for 'axioms' and 'defs' (from spec_parse.ML);
wenzelm
parents:
30461
diff
changeset

188 
val named_spec = SpecParse.thm_name ":"  P.prop >> (fn ((x, y), z) => ((x, z), y)); 
bc2a4dc6f1be
old name_spec for 'axioms' and 'defs' (from spec_parse.ML);
wenzelm
parents:
30461
diff
changeset

189 

24868  190 
val _ = 
6723  191 
OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl 
30484
bc2a4dc6f1be
old name_spec for 'axioms' and 'defs' (from spec_parse.ML);
wenzelm
parents:
30461
diff
changeset

192 
(Scan.repeat1 named_spec >> (Toplevel.theory o IsarCmd.add_axioms)); 
5832  193 

19631  194 
val opt_unchecked_overloaded = 
195 
Scan.optional (P.$$$ "("  P.!!! 

196 
(((P.$$$ "unchecked" >> K true)  Scan.optional (P.$$$ "overloaded" >> K true) false  

197 
P.$$$ "overloaded" >> K (false, true))  P.$$$ ")")) (false, false); 

198 

24868  199 
val _ = 
6723  200 
OuterSyntax.command "defs" "define constants" K.thy_decl 
30484
bc2a4dc6f1be
old name_spec for 'axioms' and 'defs' (from spec_parse.ML);
wenzelm
parents:
30461
diff
changeset

201 
(opt_unchecked_overloaded  Scan.repeat1 named_spec 
21350  202 
>> (Toplevel.theory o IsarCmd.add_defs)); 
6370  203 

14642  204 

21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

205 
(* old constdefs *) 
14642  206 

21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

207 
val old_constdecl = 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27877
diff
changeset

208 
P.binding  P.where_ >> (fn x => (x, NONE, NoSyn))  
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27877
diff
changeset

209 
P.binding  (P.$$$ "::"  P.!!! P.typ >> SOME)  P.opt_mixfix' 
21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

210 
 Scan.option P.where_ >> P.triple1  
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27877
diff
changeset

211 
P.binding  (P.mixfix >> pair NONE)  Scan.option P.where_ >> P.triple2; 
19076  212 

22117  213 
val old_constdef = Scan.option old_constdecl  (SpecParse.opt_thm_name ":"  P.prop); 
14642  214 

19076  215 
val structs = 
216 
Scan.optional ((P.$$$ "("  P.$$$ "structure")  P.!!! (P.simple_fixes  P.$$$ ")")) []; 

217 

24868  218 
val _ = 
19076  219 
OuterSyntax.command "constdefs" "oldstyle constant definition" K.thy_decl 
21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

220 
(structs  Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs)); 
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

221 

6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

222 

6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

223 
(* constant definitions and abbreviations *) 
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

224 

6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

225 
val constdecl = 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27877
diff
changeset

226 
P.binding  
21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

227 
(P.where_ >> K (NONE, NoSyn)  
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

228 
P.$$$ "::"  P.!!! ((P.typ >> SOME)  P.opt_mixfix'  P.where_)  
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

229 
Scan.ahead (P.$$$ "(")  P.!!! (P.mixfix'  P.where_ >> pair NONE)) 
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

230 
>> P.triple2; 
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21527
diff
changeset

231 

22117  232 
val constdef = Scan.option constdecl  (SpecParse.opt_thm_name ":"  P.prop); 
5832  233 

24868  234 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

235 
OuterSyntax.local_theory "definition" "constant definition" K.thy_decl 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

236 
(constdef >> (fn args => #2 o Specification.definition_cmd args)); 
18780  237 

24868  238 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

239 
OuterSyntax.local_theory "abbreviation" "constant abbreviation" K.thy_decl 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

240 
(opt_mode  (Scan.option constdecl  P.prop) 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

241 
>> (fn (mode, args) => Specification.abbreviation_cmd mode args)); 
19659  242 

24868  243 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

244 
OuterSyntax.local_theory "notation" "add notation for constants / fixed variables" K.thy_decl 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

245 
(opt_mode  P.and_list1 (P.xname  SpecParse.locale_mixfix) 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

246 
>> (fn (mode, args) => Specification.notation_cmd true mode args)); 
24950  247 

248 
val _ = 

26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

249 
OuterSyntax.local_theory "no_notation" "delete notation for constants / fixed variables" K.thy_decl 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

250 
(opt_mode  P.and_list1 (P.xname  SpecParse.locale_mixfix) 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

251 
>> (fn (mode, args) => Specification.notation_cmd false mode args)); 
19076  252 

5832  253 

18616  254 
(* constant specifications *) 
255 

24868  256 
val _ = 
28114  257 
OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

258 
(Scan.optional P.fixes []  
30484
bc2a4dc6f1be
old name_spec for 'axioms' and 'defs' (from spec_parse.ML);
wenzelm
parents:
30461
diff
changeset

259 
Scan.optional (P.where_  P.!!! (P.and_list1 SpecParse.specs)) [] 
28114  260 
>> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y))); 
18616  261 

262 

5914  263 
(* theorems *) 
264 

26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

265 
fun theorems kind = 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

266 
SpecParse.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args); 
12712  267 

24868  268 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

269 
OuterSyntax.local_theory "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK); 
5914  270 

24868  271 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

272 
OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK); 
5914  273 

24868  274 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

275 
OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

276 
(P.and_list1 SpecParse.xthms1 
28965  277 
>> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)])); 
9589  278 

5914  279 

5832  280 
(* name space entry path *) 
281 

24868  282 
val _ = 
6723  283 
OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl 
16447  284 
(Scan.succeed (Toplevel.theory Sign.root_path)); 
5832  285 

24868  286 
val _ = 
6723  287 
OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl 
16447  288 
(Scan.succeed (Toplevel.theory Sign.local_path)); 
8723  289 

24868  290 
val _ = 
8723  291 
OuterSyntax.command "hide" "hide names from given name space" K.thy_decl 
17397  292 
((P.opt_keyword "open" >> not)  (P.name  Scan.repeat1 P.xname) >> 
26672  293 
(Toplevel.theory o uncurry IsarCmd.hide_names)); 
5832  294 

295 

296 
(* use ML text *) 

297 

24868  298 
val _ = 
26490  299 
OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.thy_decl) 
300 
(P.path >> (Toplevel.generic_theory o ThyInfo.exec_file false)); 

5832  301 

24868  302 
val _ = 
28269  303 
OuterSyntax.command "ML" "eval ML text within theory" (K.tag_ml K.thy_decl) 
27877  304 
(P.ML_source >> (fn (txt, pos) => 
26490  305 
Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); 
7891  306 

24868  307 
val _ = 
28269  308 
OuterSyntax.command "ML_prf" "eval ML text within proof" (K.tag_proof K.prf_decl) 
309 
(P.ML_source >> (fn (txt, pos) => 

310 
Toplevel.proof (Proof.map_context (Context.proof_map 

28277
f2995a28e0e4
ML_prf: inherit env for all contexts within the proof;
wenzelm
parents:
28269
diff
changeset

311 
(ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> 
f2995a28e0e4
ML_prf: inherit env for all contexts within the proof;
wenzelm
parents:
28269
diff
changeset

312 
(fn prf => Proof.map_contexts (ML_Context.inherit_env (Proof.context_of prf)) prf)))); 
28269  313 

314 
val _ = 

26396  315 
OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag) 
27877  316 
(P.ML_source >> IsarCmd.ml_diag true); 
26396  317 

318 
val _ = 

319 
OuterSyntax.command "ML_command" "silently eval ML text (diagnostic)" (K.tag_ml K.diag) 

27877  320 
(P.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false)); 
5832  321 

24868  322 
val _ = 
30461  323 
OuterSyntax.command "setup" "ML theory setup" (K.tag_ml K.thy_decl) 
324 
(P.ML_source >> (Toplevel.theory o IsarCmd.global_setup)); 

325 

326 
val _ = 

327 
OuterSyntax.local_theory "local_setup" "ML local theory setup" (K.tag_ml K.thy_decl) 

328 
(P.ML_source >> IsarCmd.local_setup); 

5832  329 

24868  330 
val _ = 
30526  331 
OuterSyntax.command "attribute_setup" "define attribute in ML" (K.tag_ml K.thy_decl) 
332 
(P.position P.name  P.!!! (P.$$$ "="  P.ML_source  P.text) 

333 
>> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt))); 

334 

335 
val _ = 

17068  336 
OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl) 
27877  337 
(P.name  P.!!! (P.$$$ "="  P.ML_source  P.text) 
26385
ae7564661e76
ML runtime compilation: pass position, tuned signature;
wenzelm
parents:
26248
diff
changeset

338 
>> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt))); 
9197  339 

24868  340 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

341 
OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl) 
27877  342 
(P.ML_source >> IsarCmd.declaration); 
22088  343 

24868  344 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

345 
OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl) 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

346 
(P.name  (P.$$$ "("  P.enum1 "" P.term  P.$$$ ")"  P.$$$ "=")  
27877  347 
P.ML_source  Scan.optional (P.$$$ "identifier"  Scan.repeat1 P.xname) [] 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

348 
>> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d)); 
22202  349 

5832  350 

351 
(* translation functions *) 

352 

27877  353 
val trfun = P.opt_keyword "advanced"  P.ML_source; 
14642  354 

24868  355 
val _ = 
17068  356 
OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" 
357 
(K.tag_ml K.thy_decl) 

22117  358 
(trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation)); 
5832  359 

24868  360 
val _ = 
17068  361 
OuterSyntax.command "parse_translation" "install parse translation functions" 
362 
(K.tag_ml K.thy_decl) 

22117  363 
(trfun >> (Toplevel.theory o IsarCmd.parse_translation)); 
5832  364 

24868  365 
val _ = 
17068  366 
OuterSyntax.command "print_translation" "install print translation functions" 
367 
(K.tag_ml K.thy_decl) 

22117  368 
(trfun >> (Toplevel.theory o IsarCmd.print_translation)); 
5832  369 

24868  370 
val _ = 
6370  371 
OuterSyntax.command "typed_print_translation" "install typed print translation functions" 
17068  372 
(K.tag_ml K.thy_decl) 
22117  373 
(trfun >> (Toplevel.theory o IsarCmd.typed_print_translation)); 
5832  374 

24868  375 
val _ = 
17068  376 
OuterSyntax.command "print_ast_translation" "install print ast translation functions" 
377 
(K.tag_ml K.thy_decl) 

22117  378 
(trfun >> (Toplevel.theory o IsarCmd.print_ast_translation)); 
5832  379 

380 

381 
(* oracles *) 

382 

24868  383 
val _ = 
17068  384 
OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl) 
30334  385 
(P.position P.name  (P.$$$ "="  P.ML_source) >> 
386 
(fn (x, y) => Toplevel.theory (IsarCmd.oracle x y))); 

5832  387 

388 

21306
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

389 
(* local theories *) 
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

390 

24868  391 
val _ = 
21306
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

392 
OuterSyntax.command "context" "enter local theory context" K.thy_decl 
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

393 
(P.name  P.begin >> (fn name => 
25290  394 
Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.context name))); 
21306
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

395 

7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

396 

12061  397 
(* locales *) 
398 

12758  399 
val locale_val = 
29223  400 
SpecParse.locale_expression  
22117  401 
Scan.optional (P.$$$ "+"  P.!!! (Scan.repeat1 SpecParse.context_element)) []  
29223  402 
Scan.repeat1 SpecParse.context_element >> pair ([], []); 
12061  403 

24868  404 
val _ = 
12061  405 
OuterSyntax.command "locale" "define named proof context" K.thy_decl 
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30334
diff
changeset

406 
(P.binding  Scan.optional (P.$$$ "="  P.!!! locale_val) (([], []), [])  P.opt_begin 
27681  407 
>> (fn ((name, (expr, elems)), begin) => 
21843  408 
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin 
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30334
diff
changeset

409 
(Expression.add_locale_cmd name Binding.empty expr elems #> snd))); 
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset

410 

24868  411 
val _ = 
28895  412 
OuterSyntax.command "sublocale" 
413 
"prove sublocale relation between a locale and a locale expression" K.thy_goal 

29033
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
29006
diff
changeset

414 
(P.xname  (P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! SpecParse.locale_expression 
28895  415 
>> (fn (loc, expr) => 
28951
e89dde5f365c
Sublocale: removed public after_qed; identifiers private to NewLocale.
ballarin
parents:
28902
diff
changeset

416 
Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)))); 
28895  417 

418 
val _ = 

15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset

419 
OuterSyntax.command "interpretation" 
29223  420 
"prove interpretation of locale expression in theory" K.thy_goal 
29225
cfea1f3719b3
Merged; updated interpretation command in isar_syn.ML.
ballarin
parents:
29223
diff
changeset

421 
(P.!!! SpecParse.locale_expression  
cfea1f3719b3
Merged; updated interpretation command in isar_syn.ML.
ballarin
parents:
29223
diff
changeset

422 
Scan.optional (P.$$$ "where"  P.and_list1 (SpecParse.opt_thm_name ":"  P.prop)) [] 
cfea1f3719b3
Merged; updated interpretation command in isar_syn.ML.
ballarin
parents:
29223
diff
changeset

423 
>> (fn (expr, equations) => Toplevel.print o 
cfea1f3719b3
Merged; updated interpretation command in isar_syn.ML.
ballarin
parents:
29223
diff
changeset

424 
Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations))); 
29223  425 

426 
val _ = 

427 
OuterSyntax.command "interpret" 

428 
"prove interpretation of locale expression in proof context" 

429 
(K.tag_proof K.prf_goal) 

430 
(P.!!! SpecParse.locale_expression 

431 
>> (fn expr => Toplevel.print o 

432 
Toplevel.proof' (fn int => Expression.interpret_cmd expr int))); 

433 

15703  434 

22299  435 
(* classes *) 
436 

24868  437 
val class_val = 
438 
SpecParse.class_expr  

26248  439 
Scan.optional (P.$$$ "+"  P.!!! (Scan.repeat1 SpecParse.context_element)) []  
440 
Scan.repeat1 SpecParse.context_element >> pair []; 

22299  441 

24868  442 
val _ = 
443 
OuterSyntax.command "class" "define type class" K.thy_decl 

30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30334
diff
changeset

444 
(P.binding  Scan.optional (P.$$$ "="  class_val) ([], [])  P.opt_begin 
26516  445 
>> (fn ((name, (supclasses, elems)), begin) => 
24938  446 
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin 
29378  447 
(Class.class_cmd name supclasses elems #> snd))); 
22299  448 

24868  449 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

450 
OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" K.thy_goal 
29358  451 
(P.xname >> Class.subclass_cmd); 
24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24871
diff
changeset

452 

95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24871
diff
changeset

453 
val _ = 
25519  454 
OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl 
25536  455 
(P.multi_arity  P.begin 
25462  456 
>> (fn arities => Toplevel.print o 
29358  457 
Toplevel.begin_local_theory true (TheoryTarget.instantiation_cmd arities))); 
24589  458 

25485  459 
val _ = 
460 
OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal 

461 
((P.xname  ((P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! P.xname) >> Class.classrel_cmd  

27113  462 
P.arity >> Class.instance_arity_cmd) 
25485  463 
>> (Toplevel.print oo Toplevel.theory_to_proof) 
464 
 Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I))); 

22299  465 

466 

25519  467 
(* arbitrary overloading *) 
468 

469 
val _ = 

470 
OuterSyntax.command "overloading" "overloaded definitions" K.thy_decl 

25861  471 
(Scan.repeat1 (P.name  (P.$$$ "\\<equiv>"  P.$$$ "==")  P.term  
26048  472 
Scan.optional (P.$$$ "("  (P.$$$ "unchecked" >> K false)  P.$$$ ")") true 
473 
>> P.triple1)  P.begin 

25519  474 
>> (fn operations => Toplevel.print o 
475 
Toplevel.begin_local_theory true (TheoryTarget.overloading_cmd operations))); 

476 

477 

22866  478 
(* code generation *) 
479 

24868  480 
val _ = 
22866  481 
OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24314
diff
changeset

482 
(Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd)); 
22866  483 

484 

5832  485 

486 
(** proof commands **) 

487 

488 
(* statements *) 

489 

17353  490 
fun gen_theorem kind = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

491 
OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

492 
(Scan.optional (SpecParse.opt_thm_name ":"  
28965  493 
Scan.ahead (SpecParse.locale_keyword  SpecParse.statement_keyword)) Attrib.empty_binding  
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

494 
SpecParse.general_statement >> (fn (a, (elems, concl)) => 
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

495 
(Specification.theorem_cmd kind NONE (K I) a elems concl))); 
5832  496 

24868  497 
val _ = gen_theorem Thm.theoremK; 
498 
val _ = gen_theorem Thm.lemmaK; 

499 
val _ = gen_theorem Thm.corollaryK; 

5832  500 

24868  501 
val _ = 
17353  502 
OuterSyntax.command "have" "state local goal" 
503 
(K.tag_proof K.prf_goal) 

22117  504 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have)); 
17353  505 

24868  506 
val _ = 
17353  507 
OuterSyntax.command "hence" "abbreviates \"then have\"" 
508 
(K.tag_proof K.prf_goal) 

22117  509 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence)); 
17353  510 

24868  511 
val _ = 
17068  512 
OuterSyntax.command "show" "state local goal, solving current obligation" 
21800
6035bfcd72d8
classified show/thus as prf_asm_goal, which is usually hilited in PG;
wenzelm
parents:
21726
diff
changeset

513 
(K.tag_proof K.prf_asm_goal) 
22117  514 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); 
5832  515 

24868  516 
val _ = 
17068  517 
OuterSyntax.command "thus" "abbreviates \"then show\"" 
21800
6035bfcd72d8
classified show/thus as prf_asm_goal, which is usually hilited in PG;
wenzelm
parents:
21726
diff
changeset

518 
(K.tag_proof K.prf_asm_goal) 
22117  519 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); 
6501  520 

5832  521 

5914  522 
(* facts *) 
5832  523 

22117  524 
val facts = P.and_list1 SpecParse.xthms1; 
9197  525 

24868  526 
val _ = 
17068  527 
OuterSyntax.command "then" "forward chaining" 
528 
(K.tag_proof K.prf_chain) 

17900  529 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain)); 
5832  530 

24868  531 
val _ = 
17068  532 
OuterSyntax.command "from" "forward chaining from given facts" 
533 
(K.tag_proof K.prf_chain) 

17900  534 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss))); 
5914  535 

24868  536 
val _ = 
17068  537 
OuterSyntax.command "with" "forward chaining from given and current facts" 
538 
(K.tag_proof K.prf_chain) 

17900  539 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss))); 
6878  540 

24868  541 
val _ = 
17068  542 
OuterSyntax.command "note" "define facts" 
543 
(K.tag_proof K.prf_decl) 

22117  544 
(SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss))); 
5832  545 

24868  546 
val _ = 
17068  547 
OuterSyntax.command "using" "augment goal facts" 
548 
(K.tag_proof K.prf_decl) 

18544  549 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.using))); 
550 

24868  551 
val _ = 
18544  552 
OuterSyntax.command "unfolding" "unfold definitions in goal and facts" 
553 
(K.tag_proof K.prf_decl) 

554 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding))); 

12926  555 

5832  556 

557 
(* proof context *) 

558 

24868  559 
val _ = 
17068  560 
OuterSyntax.command "fix" "fix local variables (Skolem constants)" 
561 
(K.tag_proof K.prf_asm) 

19844  562 
(P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix))); 
11890  563 

24868  564 
val _ = 
17068  565 
OuterSyntax.command "assume" "assume propositions" 
566 
(K.tag_proof K.prf_asm) 

22117  567 
(SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume))); 
5832  568 

24868  569 
val _ = 
17068  570 
OuterSyntax.command "presume" "assume propositions, to be established later" 
571 
(K.tag_proof K.prf_asm) 

22117  572 
(SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume))); 
6850  573 

24868  574 
val _ = 
17068  575 
OuterSyntax.command "def" "local definition" 
576 
(K.tag_proof K.prf_asm) 

18308  577 
(P.and_list1 
22117  578 
(SpecParse.opt_thm_name ":"  
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27877
diff
changeset

579 
((P.binding  P.opt_mixfix)  ((P.$$$ "\\<equiv>"  P.$$$ "==")  P.!!! P.termp))) 
18308  580 
>> (Toplevel.print oo (Toplevel.proof o Proof.def))); 
6953  581 

24868  582 
val _ = 
11890  583 
OuterSyntax.command "obtain" "generalized existence" 
17068  584 
(K.tag_proof K.prf_asm_goal) 
22117  585 
(P.parname  Scan.optional (P.fixes  P.where_) []  SpecParse.statement 
18895  586 
>> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z))); 
5832  587 

24868  588 
val _ = 
17854  589 
OuterSyntax.command "guess" "wild guessing (unstructured)" 
590 
(K.tag_proof K.prf_asm_goal) 

19844  591 
(Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess))); 
17854  592 

24868  593 
val _ = 
17068  594 
OuterSyntax.command "let" "bind text variables" 
595 
(K.tag_proof K.prf_decl) 

27378  596 
(P.and_list1 (P.and_list1 P.term  (P.$$$ "="  P.term)) 
17900  597 
>> (Toplevel.print oo (Toplevel.proof o Proof.let_bind))); 
5832  598 

11793
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11742
diff
changeset

599 
val case_spec = 
15703  600 
(P.$$$ "("  P.!!! (P.xname  Scan.repeat1 (P.maybe P.name)  P.$$$ ")")  
22117  601 
P.xname >> rpair [])  SpecParse.opt_attribs >> P.triple1; 
11793
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11742
diff
changeset

602 

24868  603 
val _ = 
17068  604 
OuterSyntax.command "case" "invoke local context" 
605 
(K.tag_proof K.prf_asm) 

17900  606 
(case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case))); 
8370  607 

5832  608 

609 
(* proof structure *) 

610 

24868  611 
val _ = 
17068  612 
OuterSyntax.command "{" "begin explicit proof block" 
613 
(K.tag_proof K.prf_open) 

17900  614 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block)); 
5832  615 

24868  616 
val _ = 
17068  617 
OuterSyntax.command "}" "end explicit proof block" 
618 
(K.tag_proof K.prf_close) 

20305  619 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block)); 
6687  620 

24868  621 
val _ = 
17068  622 
OuterSyntax.command "next" "enter next proof block" 
623 
(K.tag_proof K.prf_block) 

17900  624 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block)); 
5832  625 

626 

627 
(* end proof *) 

628 

24868  629 
val _ = 
17068  630 
OuterSyntax.command "qed" "conclude (sub)proof" 
631 
(K.tag_proof K.qed_block) 

26676  632 
(Scan.option Method.parse >> IsarCmd.qed); 
5832  633 

24868  634 
val _ = 
17068  635 
OuterSyntax.command "by" "terminal backward proof" 
636 
(K.tag_proof K.qed) 

26676  637 
(Method.parse  Scan.option Method.parse >> IsarCmd.terminal_proof); 
6404  638 

24868  639 
val _ = 
17068  640 
OuterSyntax.command ".." "default proof" 
641 
(K.tag_proof K.qed) 

26676  642 
(Scan.succeed IsarCmd.default_proof); 
8966  643 

24868  644 
val _ = 
17068  645 
OuterSyntax.command "." "immediate proof" 
646 
(K.tag_proof K.qed) 

26676  647 
(Scan.succeed IsarCmd.immediate_proof); 
6404  648 

24868  649 
val _ = 
17068  650 
OuterSyntax.command "done" "done proof" 
651 
(K.tag_proof K.qed) 

26676  652 
(Scan.succeed IsarCmd.done_proof); 
5832  653 

24868  654 
val _ = 
25108  655 
OuterSyntax.command "sorry" "skip proof (quickanddirty mode only!)" 
17068  656 
(K.tag_proof K.qed) 
26676  657 
(Scan.succeed IsarCmd.skip_proof); 
6888
d0c68ebdabc5
skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
6886
diff
changeset

658 

24868  659 
val _ = 
17068  660 
OuterSyntax.command "oops" "forget proof" 
661 
(K.tag_proof K.qed_global) 

18561  662 
(Scan.succeed Toplevel.forget_proof); 
8210  663 

5832  664 

665 
(* proof steps *) 

666 

24868  667 
val _ = 
17068  668 
OuterSyntax.command "defer" "shuffle internal proof state" 
669 
(K.tag_proof K.prf_script) 

17900  670 
(Scan.option P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer))); 
8165  671 

24868  672 
val _ = 
17068  673 
OuterSyntax.command "prefer" "shuffle internal proof state" 
674 
(K.tag_proof K.prf_script) 

17900  675 
(P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer))); 
8165  676 

24868  677 
val _ = 
17068  678 
OuterSyntax.command "apply" "initial refinement step (unstructured)" 
679 
(K.tag_proof K.prf_script) 

22117  680 
(Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply))); 
5832  681 

24868  682 
val _ = 
17068  683 
OuterSyntax.command "apply_end" "terminal refinement (unstructured)" 
684 
(K.tag_proof K.prf_script) 

22117  685 
(Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end))); 
5832  686 

24868  687 
val _ = 
17068  688 
OuterSyntax.command "proof" "backward proof" 
689 
(K.tag_proof K.prf_block) 

22117  690 
(Scan.option Method.parse >> (fn m => Toplevel.print o 
27563  691 
Toplevel.actual_proof (ProofNode.applys (Proof.proof m)) o 
692 
Toplevel.skip_proof (fn i => i + 1))); 

5832  693 

694 

6773  695 
(* calculational proof commands *) 
696 

6878  697 
val calc_args = 
22117  698 
Scan.option (P.$$$ "("  P.!!! ((SpecParse.xthms1  P.$$$ ")"))); 
6878  699 

24868  700 
val _ = 
17068  701 
OuterSyntax.command "also" "combine calculation and current facts" 
702 
(K.tag_proof K.prf_decl) 

17900  703 
(calc_args >> (Toplevel.proofs' o Calculation.also)); 
6773  704 

24868  705 
val _ = 
17068  706 
OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" 
707 
(K.tag_proof K.prf_chain) 

30189
3633f560f4c3
discontinued experimental support for Alice  too hard to maintain its many language incompatibilities, never really worked anyway;
wenzelm
parents:
30173
diff
changeset

708 
(calc_args >> (Toplevel.proofs' o Calculation.finally)); 
6773  709 

24868  710 
val _ = 
17068  711 
OuterSyntax.command "moreover" "augment calculation by current facts" 
712 
(K.tag_proof K.prf_decl) 

17900  713 
(Scan.succeed (Toplevel.proof' Calculation.moreover)); 
8562  714 

24868  715 
val _ = 
8588  716 
OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result" 
17068  717 
(K.tag_proof K.prf_chain) 
17900  718 
(Scan.succeed (Toplevel.proof' Calculation.ultimately)); 
8588  719 

6773  720 

6742  721 
(* proof navigation *) 
5944  722 

24868  723 
val _ = 
17068  724 
OuterSyntax.command "back" "backtracking of proof command" 
725 
(K.tag_proof K.prf_script) 

27563  726 
(Scan.succeed (Toplevel.print o Toplevel.actual_proof ProofNode.back o Toplevel.skip_proof I)); 
6742  727 

22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

728 

27614
f38c25d106a7
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
wenzelm
parents:
27575
diff
changeset

729 
(* nested commands *) 
25578  730 

29309  731 
val props_text = 
732 
Scan.optional ValueParse.properties []  P.position P.string >> (fn (props, (str, pos)) => 

733 
(Position.of_properties (Position.default_properties pos props), str)); 

734 

25578  735 
val _ = 
736 
OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control 

29309  737 
(props_text : (fn (pos, str) => 
27838
0340fd7cccc3
Isabelle.command: inline former OuterSyntax.prepare_command;
wenzelm
parents:
27831
diff
changeset

738 
(case OuterSyntax.parse pos str of 
0340fd7cccc3
Isabelle.command: inline former OuterSyntax.prepare_command;
wenzelm
parents:
27831
diff
changeset

739 
[tr] => Scan.succeed (K tr) 
0340fd7cccc3
Isabelle.command: inline former OuterSyntax.prepare_command;
wenzelm
parents:
27831
diff
changeset

740 
 _ => Scan.fail_with (K "exactly one command expected")) 
0340fd7cccc3
Isabelle.command: inline former OuterSyntax.prepare_command;
wenzelm
parents:
27831
diff
changeset

741 
handle ERROR msg => Scan.fail_with (K msg))); 
25578  742 

743 

22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

744 

5832  745 
(** diagnostic commands (for interactive mode only) **) 
746 

8464  747 
val opt_modes = Scan.optional (P.$$$ "("  P.!!! (Scan.repeat1 P.xname  P.$$$ ")")) []; 
20621  748 
val opt_bang = Scan.optional (P.$$$ "!" >> K true) false; 
8464  749 

24868  750 
val _ = 
7124  751 
OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing" 
9010  752 
K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin)); 
7124  753 

24868  754 
val _ = 
21714  755 
OuterSyntax.improper_command "help" "print outer syntax commands" K.diag 
24871  756 
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax)); 
21714  757 

24868  758 
val _ = 
21714  759 
OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag 
24871  760 
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax)); 
5832  761 

24868  762 
val _ = 
24115  763 
OuterSyntax.improper_command "print_configs" "print configuration options" K.diag 
764 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs)); 

23989  765 

24868  766 
val _ = 
7308  767 
OuterSyntax.improper_command "print_context" "print theory context name" K.diag 
9010  768 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_context)); 
7308  769 

24868  770 
val _ = 
6723  771 
OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag 
20621  772 
(opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory)); 
5832  773 

24868  774 
val _ = 
21726  775 
OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag 
9010  776 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax)); 
5832  777 

24868  778 
val _ = 
21726  779 
OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag 
780 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs)); 

781 

24868  782 
val _ = 
17068  783 
OuterSyntax.improper_command "print_theorems" 
784 
"print theorems of local theory or proof context" K.diag 

9010  785 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems)); 
5881  786 

24868  787 
val _ = 
12061  788 
OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag 
789 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales)); 

790 

24868  791 
val _ = 
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

792 
OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag 
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

793 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory 
24219  794 
o Toplevel.keep (Class.print_classes o Toplevel.theory_of))); 
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

795 

24868  796 
val _ = 
15596  797 
OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag 
29223  798 
(opt_bang  P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale)); 
12061  799 

24868  800 
val _ = 
12061  801 
OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag 
9010  802 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); 
5832  803 

24868  804 
val _ = 
16027  805 
OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag 
806 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset)); 

807 

24868  808 
val _ = 
12383  809 
OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag 
810 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules)); 

811 

24868  812 
val _ = 
11666  813 
OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag 
9221  814 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); 
815 

24868  816 
val _ = 
12061  817 
OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag 
9010  818 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); 
5832  819 

24868  820 
val _ = 
9221  821 
OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag 
822 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations)); 

823 

24868  824 
val _ = 
22485  825 
OuterSyntax.improper_command "thy_deps" "visualize theory dependencies" 
826 
K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps)); 

827 

24868  828 
val _ = 
20574  829 
OuterSyntax.improper_command "class_deps" "visualize class dependencies" 
830 
K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps)); 

831 

24868  832 
val _ = 
9454  833 
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" 
22117  834 
K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); 
9454  835 

24868  836 
val _ = 
6723  837 
OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag 
9010  838 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); 
5832  839 

24868  840 
val _ = 
8370  841 
OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag 
21004  842 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts)); 
5832  843 

24868  844 
val _ = 
8370  845 
OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag 
9010  846 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); 
8370  847 

24868  848 
val _ = 
19269  849 
OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag 
22117  850 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); 
19269  851 

24868  852 
val _ = 
8464  853 
OuterSyntax.improper_command "thm" "print theorems" K.diag 
22117  854 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); 
5832  855 

24868  856 
val _ = 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11101
diff
changeset

857 
OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag 
22866  858 
(opt_modes  Scan.option SpecParse.xthms1 
859 
>> (Toplevel.no_timing oo IsarCmd.print_prfs false)); 

11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11101
diff
changeset

860 

24868  861 
val _ = 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11101
diff
changeset

862 
OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag 
22117  863 
(opt_modes  Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true)); 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11101
diff
changeset

864 

24868  865 
val _ = 
6723  866 
OuterSyntax.improper_command "prop" "read and print proposition" K.diag 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

867 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); 
5832  868 

24868  869 
val _ = 
6723  870 
OuterSyntax.improper_command "term" "read and print term" K.diag 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

871 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); 
5832  872 

24868  873 
val _ = 
6723  874 
OuterSyntax.improper_command "typ" "read and print type" K.diag 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12768
diff
changeset

875 
(opt_modes  P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); 
5832  876 

24868  877 
val _ = 
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

878 
OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag 
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

879 
(Scan.succeed 
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22573
diff
changeset

880 
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep 
24219  881 
(Code.print_codesetup o Toplevel.theory_of))); 
5832  882 

26184  883 
val _ = 
884 
OuterSyntax.improper_command "unused_thms" "find unused theorems" K.diag 

885 
(Scan.option ((Scan.repeat1 (Scan.unless P.minus P.name)  P.minus)  

886 
Scan.option (Scan.repeat1 (Scan.unless P.minus P.name))) >> 

887 
(Toplevel.no_timing oo IsarCmd.unused_thms)); 

888 

5832  889 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

890 

5832  891 
(** system commands (for interactive mode only) **) 
892 

24868  893 
val _ = 
8650  894 
OuterSyntax.improper_command "cd" "change current working directory" K.diag 
14950  895 
(P.path >> (Toplevel.no_timing oo IsarCmd.cd)); 
5832  896 

24868  897 
val _ = 
6723  898 
OuterSyntax.improper_command "pwd" "print current working directory" K.diag 
9010  899 
(Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); 
5832  900 

24868  901 
val _ = 
6723  902 
OuterSyntax.improper_command "use_thy" "use theory file" K.diag 
26404  903 
(P.name >> (fn name => 
904 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.use_thy name))); 

5832  905 

24868  906 
val _ = 
7102  907 
OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag 
27494  908 
(P.name >> (fn name => 
909 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.touch_thy name))); 

7908  910 

24868  911 
val _ = 
7102  912 
OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag 
27494  913 
(P.name >> (fn name => 
914 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.remove_thy name))); 

7102  915 

24868  916 
val _ = 
7931  917 
OuterSyntax.improper_command "kill_thy" "kill theory  try to remove from loader database" 
27494  918 
K.diag (P.name >> (fn name => 
919 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.kill_thy name))); 

7931  920 

24868  921 
val _ = 
14934  922 
OuterSyntax.improper_command "display_drafts" "display raw source files with symbols" 
14950  923 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts)); 
14934  924 

24868  925 
val _ = 
14934  926 
OuterSyntax.improper_command "print_drafts" "print raw source files with symbols" 
14950  927 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts)); 
14934  928 

9731  929 
val opt_limits = 
930 
Scan.option P.nat  Scan.option (P.$$$ ","  P.!!! P.nat); 

931 

24868  932 
val _ = 
8886  933 
OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag 
9731  934 
(opt_modes  opt_limits >> (Toplevel.no_timing oo IsarCmd.pr)); 
7199  935 

24868  936 
val _ = 
7222  937 
OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag 
9010  938 
(Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr)); 
5832  939 

24868  940 
val _ = 
7222  941 
OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag 
9010  942 
(Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr)); 
7222  943 

24868  944 
val _ = 
6723  945 
OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag 
26490  946 
(P.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit)); 
5832  947 

24868  948 
val _ = 
6723  949 
OuterSyntax.improper_command "quit" "quit Isabelle" K.control 
9010  950 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); 
5832  951 

24868  952 
val _ = 
6723  953 
OuterSyntax.improper_command "exit" "exit Isar loop" K.control 
9010  954 
(Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); 
5832  955 

956 
end; 

27614
f38c25d106a7
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
wenzelm
parents:
27575
diff
changeset

957 