author  wenzelm 
Tue, 24 Mar 2009 15:43:37 +0100  
changeset 30703  a1a47e653eb7 
parent 30579  4169ddbfe1f9 
child 30727  519f8f0fcbf3 
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 _ = 
30579
4169ddbfe1f9
command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents:
30576
diff
changeset

275 
OuterSyntax.local_theory "declare" "declare theorems" K.thy_decl 
26988
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 

30703  298 
fun propagate_env (context as Context.Proof lthy) = 
30579
4169ddbfe1f9
command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents:
30576
diff
changeset

299 
Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy) 
30703  300 
 propagate_env context = context; 
30579
4169ddbfe1f9
command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents:
30576
diff
changeset

301 

30703  302 
fun propagate_env_prf prf = Proof.map_contexts 
30579
4169ddbfe1f9
command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents:
30576
diff
changeset

303 
(Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf; 
5832  304 

24868  305 
val _ = 
30579
4169ddbfe1f9
command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents:
30576
diff
changeset

306 
OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl) 
30703  307 
(P.path >> (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env))); 
7891  308 

24868  309 
val _ = 
30579
4169ddbfe1f9
command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents:
30576
diff
changeset

310 
OuterSyntax.command "ML" "ML text within theory or local theory" (K.tag_ml K.thy_decl) 
4169ddbfe1f9
command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents:
30576
diff
changeset

311 
(P.ML_source >> (fn (txt, pos) => 
4169ddbfe1f9
command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents:
30576
diff
changeset

312 
Toplevel.generic_theory 
30703  313 
(ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env))); 
30579
4169ddbfe1f9
command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents:
30576
diff
changeset

314 

4169ddbfe1f9
command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents:
30576
diff
changeset

315 
val _ = 
4169ddbfe1f9
command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents:
30576
diff
changeset

316 
OuterSyntax.command "ML_prf" "ML text within proof" (K.tag_proof K.prf_decl) 
28269  317 
(P.ML_source >> (fn (txt, pos) => 
318 
Toplevel.proof (Proof.map_context (Context.proof_map 

30703  319 
(ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf))); 
28269  320 

321 
val _ = 

30579
4169ddbfe1f9
command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents:
30576
diff
changeset

322 
OuterSyntax.command "ML_val" "diagnostic ML text" (K.tag_ml K.diag) 
27877  323 
(P.ML_source >> IsarCmd.ml_diag true); 
26396  324 

325 
val _ = 

30579
4169ddbfe1f9
command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents:
30576
diff
changeset

326 
OuterSyntax.command "ML_command" "diagnostic ML text (silent)" (K.tag_ml K.diag) 
27877  327 
(P.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false)); 
5832  328 

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

332 

333 
val _ = 

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

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

5832  336 

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

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

341 

342 
val _ = 

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

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

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

348 
OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl) 
27877  349 
(P.ML_source >> IsarCmd.declaration); 
22088  350 

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

352 
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

353 
(P.name  (P.$$$ "("  P.enum1 "" P.term  P.$$$ ")"  P.$$$ "=")  
27877  354 
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

355 
>> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d)); 
22202  356 

5832  357 

358 
(* translation functions *) 

359 

27877  360 
val trfun = P.opt_keyword "advanced"  P.ML_source; 
14642  361 

24868  362 
val _ = 
17068  363 
OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" 
364 
(K.tag_ml K.thy_decl) 

22117  365 
(trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation)); 
5832  366 

24868  367 
val _ = 
17068  368 
OuterSyntax.command "parse_translation" "install parse translation functions" 
369 
(K.tag_ml K.thy_decl) 

22117  370 
(trfun >> (Toplevel.theory o IsarCmd.parse_translation)); 
5832  371 

24868  372 
val _ = 
17068  373 
OuterSyntax.command "print_translation" "install print translation functions" 
374 
(K.tag_ml K.thy_decl) 

22117  375 
(trfun >> (Toplevel.theory o IsarCmd.print_translation)); 
5832  376 

24868  377 
val _ = 
6370  378 
OuterSyntax.command "typed_print_translation" "install typed print translation functions" 
17068  379 
(K.tag_ml K.thy_decl) 
22117  380 
(trfun >> (Toplevel.theory o IsarCmd.typed_print_translation)); 
5832  381 

24868  382 
val _ = 
17068  383 
OuterSyntax.command "print_ast_translation" "install print ast translation functions" 
384 
(K.tag_ml K.thy_decl) 

22117  385 
(trfun >> (Toplevel.theory o IsarCmd.print_ast_translation)); 
5832  386 

387 

388 
(* oracles *) 

389 

24868  390 
val _ = 
17068  391 
OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl) 
30334  392 
(P.position P.name  (P.$$$ "="  P.ML_source) >> 
393 
(fn (x, y) => Toplevel.theory (IsarCmd.oracle x y))); 

5832  394 

395 

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

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

397 

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

399 
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

400 
(P.name  P.begin >> (fn name => 
25290  401 
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

402 

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

403 

12061  404 
(* locales *) 
405 

12758  406 
val locale_val = 
29223  407 
SpecParse.locale_expression  
22117  408 
Scan.optional (P.$$$ "+"  P.!!! (Scan.repeat1 SpecParse.context_element)) []  
29223  409 
Scan.repeat1 SpecParse.context_element >> pair ([], []); 
12061  410 

24868  411 
val _ = 
12061  412 
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

413 
(P.binding  Scan.optional (P.$$$ "="  P.!!! locale_val) (([], []), [])  P.opt_begin 
27681  414 
>> (fn ((name, (expr, elems)), begin) => 
21843  415 
(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

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

417 

24868  418 
val _ = 
28895  419 
OuterSyntax.command "sublocale" 
420 
"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

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

423 
Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)))); 
28895  424 

425 
val _ = 

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

426 
OuterSyntax.command "interpretation" 
29223  427 
"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

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

429 
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

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

431 
Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations))); 
29223  432 

433 
val _ = 

434 
OuterSyntax.command "interpret" 

435 
"prove interpretation of locale expression in proof context" 

436 
(K.tag_proof K.prf_goal) 

437 
(P.!!! SpecParse.locale_expression 

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

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

440 

15703  441 

22299  442 
(* classes *) 
443 

24868  444 
val class_val = 
445 
SpecParse.class_expr  

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

22299  448 

24868  449 
val _ = 
450 
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

451 
(P.binding  Scan.optional (P.$$$ "="  class_val) ([], [])  P.opt_begin 
26516  452 
>> (fn ((name, (supclasses, elems)), begin) => 
24938  453 
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin 
29378  454 
(Class.class_cmd name supclasses elems #> snd))); 
22299  455 

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

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

459 

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

460 
val _ = 
25519  461 
OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl 
25536  462 
(P.multi_arity  P.begin 
25462  463 
>> (fn arities => Toplevel.print o 
29358  464 
Toplevel.begin_local_theory true (TheoryTarget.instantiation_cmd arities))); 
24589  465 

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

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

27113  469 
P.arity >> Class.instance_arity_cmd) 
25485  470 
>> (Toplevel.print oo Toplevel.theory_to_proof) 
471 
 Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I))); 

22299  472 

473 

25519  474 
(* arbitrary overloading *) 
475 

476 
val _ = 

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

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

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

483 

484 

22866  485 
(* code generation *) 
486 

24868  487 
val _ = 
22866  488 
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

489 
(Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd)); 
22866  490 

491 

5832  492 

493 
(** proof commands **) 

494 

495 
(* statements *) 

496 

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

498 
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

499 
(Scan.optional (SpecParse.opt_thm_name ":"  
28965  500 
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

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

502 
(Specification.theorem_cmd kind NONE (K I) a elems concl))); 
5832  503 

24868  504 
val _ = gen_theorem Thm.theoremK; 
505 
val _ = gen_theorem Thm.lemmaK; 

506 
val _ = gen_theorem Thm.corollaryK; 

5832  507 

24868  508 
val _ = 
17353  509 
OuterSyntax.command "have" "state local goal" 
510 
(K.tag_proof K.prf_goal) 

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

24868  513 
val _ = 
17353  514 
OuterSyntax.command "hence" "abbreviates \"then have\"" 
515 
(K.tag_proof K.prf_goal) 

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

24868  518 
val _ = 
17068  519 
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

520 
(K.tag_proof K.prf_asm_goal) 
22117  521 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); 
5832  522 

24868  523 
val _ = 
17068  524 
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

525 
(K.tag_proof K.prf_asm_goal) 
22117  526 
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); 
6501  527 

5832  528 

5914  529 
(* facts *) 
5832  530 

22117  531 
val facts = P.and_list1 SpecParse.xthms1; 
9197  532 

24868  533 
val _ = 
17068  534 
OuterSyntax.command "then" "forward chaining" 
535 
(K.tag_proof K.prf_chain) 

17900  536 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain)); 
5832  537 

24868  538 
val _ = 
17068  539 
OuterSyntax.command "from" "forward chaining from given facts" 
540 
(K.tag_proof K.prf_chain) 

17900  541 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss))); 
5914  542 

24868  543 
val _ = 
17068  544 
OuterSyntax.command "with" "forward chaining from given and current facts" 
545 
(K.tag_proof K.prf_chain) 

17900  546 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss))); 
6878  547 

24868  548 
val _ = 
17068  549 
OuterSyntax.command "note" "define facts" 
550 
(K.tag_proof K.prf_decl) 

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

24868  553 
val _ = 
17068  554 
OuterSyntax.command "using" "augment goal facts" 
555 
(K.tag_proof K.prf_decl) 

18544  556 
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.using))); 
557 

24868  558 
val _ = 
18544  559 
OuterSyntax.command "unfolding" "unfold definitions in goal and facts" 
560 
(K.tag_proof K.prf_decl) 

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

12926  562 

5832  563 

564 
(* proof context *) 

565 

24868  566 
val _ = 
17068  567 
OuterSyntax.command "fix" "fix local variables (Skolem constants)" 
568 
(K.tag_proof K.prf_asm) 

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

24868  571 
val _ = 
17068  572 
OuterSyntax.command "assume" "assume propositions" 
573 
(K.tag_proof K.prf_asm) 

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

24868  576 
val _ = 
17068  577 
OuterSyntax.command "presume" "assume propositions, to be established later" 
578 
(K.tag_proof K.prf_asm) 

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

24868  581 
val _ = 
17068  582 
OuterSyntax.command "def" "local definition" 
583 
(K.tag_proof K.prf_asm) 

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

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

24868  589 
val _ = 
11890  590 
OuterSyntax.command "obtain" "generalized existence" 
17068  591 
(K.tag_proof K.prf_asm_goal) 
22117  592 
(P.parname  Scan.optional (P.fixes  P.where_) []  SpecParse.statement 
18895  593 
>> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z))); 
5832  594 

24868  595 
val _ = 
17854  596 
OuterSyntax.command "guess" "wild guessing (unstructured)" 
597 
(K.tag_proof K.prf_asm_goal) 

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

24868  600 
val _ = 
17068  601 
OuterSyntax.command "let" "bind text variables" 
602 
(K.tag_proof K.prf_decl) 

27378  603 
(P.and_list1 (P.and_list1 P.term  (P.$$$ "="  P.term)) 
17900  604 
>> (Toplevel.print oo (Toplevel.proof o Proof.let_bind))); 
5832  605 

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

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

609 

24868  610 
val _ = 
17068  611 
OuterSyntax.command "case" "invoke local context" 
612 
(K.tag_proof K.prf_asm) 

17900  613 
(case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case))); 
8370  614 

5832  615 

616 
(* proof structure *) 

617 

24868  618 
val _ = 
17068  619 
OuterSyntax.command "{" "begin explicit proof block" 
620 
(K.tag_proof K.prf_open) 

17900  621 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block)); 
5832  622 

24868  623 
val _ = 
17068  624 
OuterSyntax.command "}" "end explicit proof block" 
625 
(K.tag_proof K.prf_close) 

20305  626 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block)); 
6687  627 

24868  628 
val _ = 
17068  629 
OuterSyntax.command "next" "enter next proof block" 
630 
(K.tag_proof K.prf_block) 

17900  631 
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block)); 
5832  632 

633 

634 
(* end proof *) 

635 

24868  636 
val _ = 
17068  637 
OuterSyntax.command "qed" "conclude (sub)proof" 
638 
(K.tag_proof K.qed_block) 

26676  639 
(Scan.option Method.parse >> IsarCmd.qed); 
5832  640 

24868  641 
val _ = 
17068  642 
OuterSyntax.command "by" "terminal backward proof" 
643 
(K.tag_proof K.qed) 

26676  644 
(Method.parse  Scan.option Method.parse >> IsarCmd.terminal_proof); 
6404  645 

24868  646 
val _ = 
17068  647 
OuterSyntax.command ".." "default proof" 
648 
(K.tag_proof K.qed) 

26676  649 
(Scan.succeed IsarCmd.default_proof); 
8966  650 

24868  651 
val _ = 
17068  652 
OuterSyntax.command "." "immediate proof" 
653 
(K.tag_proof K.qed) 

26676  654 
(Scan.succeed IsarCmd.immediate_proof); 
6404  655 

24868  656 
val _ = 
17068  657 
OuterSyntax.command "done" "done proof" 
658 
(K.tag_proof K.qed) 

26676  659 
(Scan.succeed IsarCmd.done_proof); 
5832  660 

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

665 

24868  666 
val _ = 
17068  667 
OuterSyntax.command "oops" "forget proof" 
668 
(K.tag_proof K.qed_global) 

18561  669 
(Scan.succeed Toplevel.forget_proof); 
8210  670 

5832  671 

672 
(* proof steps *) 

673 

24868  674 
val _ = 
17068  675 
OuterSyntax.command "defer" "shuffle internal proof state" 
676 
(K.tag_proof K.prf_script) 

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

24868  679 
val _ = 
17068  680 
OuterSyntax.command "prefer" "shuffle internal proof state" 
681 
(K.tag_proof K.prf_script) 

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

24868  684 
val _ = 
17068  685 
OuterSyntax.command "apply" "initial refinement step (unstructured)" 
686 
(K.tag_proof K.prf_script) 

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

24868  689 
val _ = 
17068  690 
OuterSyntax.command "apply_end" "terminal refinement (unstructured)" 
691 
(K.tag_proof K.prf_script) 

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

24868  694 
val _ = 
17068  695 
OuterSyntax.command "proof" "backward proof" 
696 
(K.tag_proof K.prf_block) 

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

5832  700 

701 

6773  702 
(* calculational proof commands *) 
703 

6878  704 
val calc_args = 
22117  705 
Scan.option (P.$$$ "("  P.!!! ((SpecParse.xthms1  P.$$$ ")"))); 
6878  706 

24868  707 
val _ = 
17068  708 
OuterSyntax.command "also" "combine calculation and current facts" 
709 
(K.tag_proof K.prf_decl) 

17900  710 
(calc_args >> (Toplevel.proofs' o Calculation.also)); 
6773  711 

24868  712 
val _ = 
17068  713 
OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" 
714 
(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

715 
(calc_args >> (Toplevel.proofs' o Calculation.finally)); 
6773  716 

24868  717 
val _ = 
17068  718 
OuterSyntax.command "moreover" "augment calculation by current facts" 
719 
(K.tag_proof K.prf_decl) 

17900  720 
(Scan.succeed (Toplevel.proof' Calculation.moreover)); 
8562  721 

24868  722 
val _ = 
8588  723 
OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result" 
17068  724 
(K.tag_proof K.prf_chain) 
17900  725 
(Scan.succeed (Toplevel.proof' Calculation.ultimately)); 
8588  726 

6773  727 

6742  728 
(* proof navigation *) 
5944  729 

24868  730 
val _ = 
17068  731 
OuterSyntax.command "back" "backtracking of proof command" 
732 
(K.tag_proof K.prf_script) 

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

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

735 

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

736 
(* nested commands *) 
25578  737 

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

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

741 

25578  742 
val _ = 
743 
OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control 

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

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

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

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

748 
handle ERROR msg => Scan.fail_with (K msg))); 
25578  749 

750 

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

751 

5832  752 
(** diagnostic commands (for interactive mode only) **) 
753 

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

24868  757 
val _ = 
7124  758 
OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing" 
9010  759 
K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin)); 
7124  760 

24868  761 
val _ = 
21714  762 
OuterSyntax.improper_command "help" "print outer syntax commands" K.diag 
24871  763 
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax)); 
21714  764 

24868  765 
val _ = 
21714  766 
OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag 
24871  767 
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax)); 
5832  768 

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

23989  772 

24868  773 
val _ = 
7308  774 
OuterSyntax.improper_command "print_context" "print theory context name" K.diag 
9010  775 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_context)); 
7308  776 

24868  777 
val _ = 
6723  778 
OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag 
20621  779 
(opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory)); 
5832  780 

24868  781 
val _ = 
21726  782 
OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag 
9010  783 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax)); 
5832  784 

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

788 

24868  789 
val _ = 
17068  790 
OuterSyntax.improper_command "print_theorems" 
791 
"print theorems of local theory or proof context" K.diag 

9010  792 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems)); 
5881  793 

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

797 

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

799 
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

800 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory 
24219  801 
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

802 

24868  803 
val _ = 
15596  804 
OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag 
29223  805 
(opt_bang  P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale)); 
12061  806 

24868  807 
val _ = 
12061  808 
OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag 
9010  809 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); 
5832  810 

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

814 

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

818 

24868  819 
val _ = 
11666  820 
OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag 
9221  821 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); 
822 

24868  823 
val _ = 
12061  824 
OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag 
9010  825 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); 
5832  826 

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

830 

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

834 

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

838 

24868  839 
val _ = 
9454  840 
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" 
22117  841 
K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); 
9454  842 

24868  843 
val _ = 
6723  844 
OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag 
9010  845 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); 
5832  846 

24868  847 
val _ = 
8370  848 
OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag 
21004  849 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts)); 
5832  850 

24868  851 
val _ = 
8370  852 
OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag 
9010  853 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); 
8370  854 

24868  855 
val _ = 
19269  856 
OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag 
22117  857 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); 
19269  858 

24868  859 
val _ = 
8464  860 
OuterSyntax.improper_command "thm" "print theorems" K.diag 
22117  861 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); 
5832  862 

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

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

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

867 

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

869 
OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag 
22117  870 
(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

871 

24868  872 
val _ = 
6723  873 
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

874 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); 
5832  875 

24868  876 
val _ = 
6723  877 
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

878 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); 
5832  879 

24868  880 
val _ = 
6723  881 
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

882 
(opt_modes  P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); 
5832  883 

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

885 
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

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

887 
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep 
24219  888 
(Code.print_codesetup o Toplevel.theory_of))); 
5832  889 

26184  890 
val _ = 
891 
OuterSyntax.improper_command "unused_thms" "find unused theorems" K.diag 

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

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

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

895 

5832  896 

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

897 

5832  898 
(** system commands (for interactive mode only) **) 
899 

24868  900 
val _ = 
8650  901 
OuterSyntax.improper_command "cd" "change current working directory" K.diag 
14950  902 
(P.path >> (Toplevel.no_timing oo IsarCmd.cd)); 
5832  903 

24868  904 
val _ = 
6723  905 
OuterSyntax.improper_command "pwd" "print current working directory" K.diag 
9010  906 
(Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); 
5832  907 

24868  908 
val _ = 
6723  909 
OuterSyntax.improper_command "use_thy" "use theory file" K.diag 
26404  910 
(P.name >> (fn name => 
911 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.use_thy name))); 

5832  912 

24868  913 
val _ = 
7102  914 
OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag 
27494  915 
(P.name >> (fn name => 
916 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.touch_thy name))); 

7908  917 

24868  918 
val _ = 
7102  919 
OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag 
27494  920 
(P.name >> (fn name => 
921 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.remove_thy name))); 

7102  922 

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

7931  927 

24868  928 
val _ = 
14934  929 
OuterSyntax.improper_command "display_drafts" "display raw source files with symbols" 
14950  930 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts)); 
14934  931 

24868  932 
val _ = 
14934  933 
OuterSyntax.improper_command "print_drafts" "print raw source files with symbols" 
14950  934 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts)); 
14934  935 

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

938 

24868  939 
val _ = 
8886  940 
OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag 
9731  941 
(opt_modes  opt_limits >> (Toplevel.no_timing oo IsarCmd.pr)); 
7199  942 

24868  943 
val _ = 
7222  944 
OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag 
9010  945 
(Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr)); 
5832  946 

24868  947 
val _ = 
7222  948 
OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag 
9010  949 
(Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr)); 
7222  950 

24868  951 
val _ = 
6723  952 
OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag 
26490  953 
(P.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit)); 
5832  954 

24868  955 
val _ = 
6723  956 
OuterSyntax.improper_command "quit" "quit Isabelle" K.control 
9010  957 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); 
5832  958 

24868  959 
val _ = 
6723  960 
OuterSyntax.improper_command "exit" "exit Isar loop" K.control 
9010  961 
(Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); 
5832  962 

963 
end; 

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

964 