author  wenzelm 
Mon, 01 Mar 2010 17:09:42 +0100  
changeset 35413  4c7cba1f7ce9 
parent 35351  7425aece4ee3 
child 35625  9c818cab0dd0 
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", 
33456
fbd47f9b9b12
allow "pervasive" local theory declarations, which are applied the background theory;
wenzelm
parents:
33390
diff
changeset

25 
"notes", "obtains", "open", "output", "overloaded", "pervasive", 
fbd47f9b9b12
allow "pervasive" local theory declarations, which are applied the background theory;
wenzelm
parents:
33390
diff
changeset

26 
"shows", "structure", "unchecked", "uses", "where", ""]; 
fbd47f9b9b12
allow "pervasive" local theory declarations, which are applied the background theory;
wenzelm
parents:
33390
diff
changeset

27 

24868  28 

29 

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

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

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

5832  40 

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

41 

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

24868  44 
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

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

24868  47 
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

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

24868  50 
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

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

24868  53 
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

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

24868  56 
val _ = 
22117  57 
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

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

24868  60 
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

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

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

63 
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

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

24868  66 
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

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

24868  69 
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

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

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

72 
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

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

24868  75 
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

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

24868  78 
val _ = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw" 
17068  79 
"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

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

5832  82 

6886  83 

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

84 
(** theory commands **) 
6886  85 

5832  86 
(* classes and sorts *) 
87 

24868  88 
val _ = 
6723  89 
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

90 
(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

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

24868  93 
val _ = 
6723  94 
OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl 
14779  95 
(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

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

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

102 

103 
(* types *) 

104 

24868  105 
val _ = 
12624  106 
OuterSyntax.command "typedecl" "type declaration" K.thy_decl 
35351
7425aece4ee3
allow general mixfix syntax for type constructors;
wenzelm
parents:
35315
diff
changeset

107 
(P.type_args  P.binding  P.opt_mixfix >> (fn ((args, a), mx) => 
25495  108 
Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd))); 
5832  109 

24868  110 
val _ = 
6723  111 
OuterSyntax.command "types" "declare type abbreviations" K.thy_decl 
6727  112 
(Scan.repeat1 
35351
7425aece4ee3
allow general mixfix syntax for type constructors;
wenzelm
parents:
35315
diff
changeset

113 
(P.type_args  P.binding  (P.$$$ "="  P.!!! (P.typ  P.opt_mixfix'))) 
22796  114 
>> (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

115 
map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); 
5832  116 

24868  117 
val _ = 
6370  118 
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

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

24868  121 
val _ = 
6723  122 
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

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

125 

126 
(* consts and syntax *) 

127 

24868  128 
val _ = 
8227  129 
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

130 
(P.const_binding >> (Toplevel.theory o ObjectLogic.add_judgment_cmd)); 
8227  131 

24868  132 
val _ = 
6723  133 
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

134 
(Scan.repeat1 P.const_binding >> (Toplevel.theory o Sign.add_consts)); 
5832  135 

14642  136 
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

137 

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

139 
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

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

12142  142 
val mode_spec = 
9731  143 
(P.$$$ "output" >> K ("", false))  P.name  Scan.optional (P.$$$ "output" >> K false) true; 
144 

14900  145 
val opt_mode = 
24960  146 
Scan.optional (P.$$$ "("  P.!!! (mode_spec  P.$$$ ")")) Syntax.mode_default; 
5832  147 

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

24868  152 
val _ = 
15748  153 
OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl 
22796  154 
(opt_mode  Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.del_modesyntax)); 
15748  155 

5832  156 

157 
(* translations *) 

158 

159 
val trans_pat = 

6723  160 
Scan.optional (P.$$$ "("  P.!!! (P.xname  P.$$$ ")")) "logic"  P.string; 
5832  161 

162 
fun trans_arrow toks = 

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

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

5832  166 

167 
val trans_line = 

6723  168 
trans_pat  P.!!! (trans_arrow  trans_pat) 
5832  169 
>> (fn (left, (arr, right)) => arr (left, right)); 
170 

24868  171 
val _ = 
6723  172 
OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl 
22796  173 
(Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules)); 
5832  174 

24868  175 
val _ = 
19260  176 
OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl 
22796  177 
(Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules)); 
19260  178 

5832  179 

180 
(* axioms and definitions *) 

181 

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

182 
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

183 

24868  184 
val _ = 
6723  185 
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

186 
(Scan.repeat1 named_spec >> (Toplevel.theory o IsarCmd.add_axioms)); 
5832  187 

19631  188 
val opt_unchecked_overloaded = 
189 
Scan.optional (P.$$$ "("  P.!!! 

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

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

192 

24868  193 
val _ = 
6723  194 
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

195 
(opt_unchecked_overloaded  Scan.repeat1 named_spec 
21350  196 
>> (Toplevel.theory o IsarCmd.add_defs)); 
6370  197 

14642  198 

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

199 
(* old constdefs *) 
14642  200 

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

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

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

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

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

205 
P.binding  (P.mixfix >> pair NONE)  Scan.option P.where_ >> P.triple2; 
19076  206 

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

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

211 

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

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

215 

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

216 

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

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

218 

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

220 
OuterSyntax.local_theory "definition" "constant definition" K.thy_decl 
33287
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
32805
diff
changeset

221 
(SpecParse.constdef >> (fn args => #2 o Specification.definition_cmd args)); 
18780  222 

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

224 
OuterSyntax.local_theory "abbreviation" "constant abbreviation" K.thy_decl 
33287
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
32805
diff
changeset

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

226 
>> (fn (mode, args) => Specification.abbreviation_cmd mode args)); 
19659  227 

24868  228 
val _ = 
35413  229 
OuterSyntax.local_theory "type_notation" "add notation for type constructors" K.thy_decl 
230 
(opt_mode  P.and_list1 (P.xname  P.mixfix) 

231 
>> (fn (mode, args) => Specification.type_notation_cmd true mode args)); 

232 

233 
val _ = 

234 
OuterSyntax.local_theory "no_type_notation" "delete notation for type constructors" K.thy_decl 

235 
(opt_mode  P.and_list1 (P.xname  P.mixfix) 

236 
>> (fn (mode, args) => Specification.type_notation_cmd false mode args)); 

237 

238 
val _ = 

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

239 
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

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

241 
>> (fn (mode, args) => Specification.notation_cmd true mode args)); 
24950  242 

243 
val _ = 

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

244 
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

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 false mode args)); 
19076  247 

5832  248 

18616  249 
(* constant specifications *) 
250 

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

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

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

257 

5914  258 
(* theorems *) 
259 

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

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

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

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

264 
OuterSyntax.local_theory "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK); 
5914  265 

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

267 
OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK); 
5914  268 

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

270 
OuterSyntax.local_theory "declare" "declare theorems" K.thy_decl 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26888
diff
changeset

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

5914  274 

5832  275 
(* name space entry path *) 
276 

24868  277 
val _ = 
6723  278 
OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl 
16447  279 
(Scan.succeed (Toplevel.theory Sign.root_path)); 
5832  280 

24868  281 
val _ = 
6723  282 
OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl 
16447  283 
(Scan.succeed (Toplevel.theory Sign.local_path)); 
8723  284 

24868  285 
val _ = 
8723  286 
OuterSyntax.command "hide" "hide names from given name space" K.thy_decl 
17397  287 
((P.opt_keyword "open" >> not)  (P.name  Scan.repeat1 P.xname) >> 
26672  288 
(Toplevel.theory o uncurry IsarCmd.hide_names)); 
5832  289 

290 

291 
(* use ML text *) 

292 

30703  293 
fun propagate_env (context as Context.Proof lthy) = 
33671  294 
Context.Proof (Local_Theory.map_contexts (ML_Env.inherit context) lthy) 
30703  295 
 propagate_env context = context; 
30579
4169ddbfe1f9
command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents:
30576
diff
changeset

296 

30703  297 
fun propagate_env_prf prf = Proof.map_contexts 
31327  298 
(Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf; 
5832  299 

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

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

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

305 
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

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

307 
Toplevel.generic_theory 
30703  308 
(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

309 

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

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

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

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

316 
val _ = 

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

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

320 
val _ = 

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

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

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

327 

328 
val _ = 

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

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

5832  331 

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

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

336 

337 
val _ = 

17068  338 
OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl) 
30544  339 
(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

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

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

343 
OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl) 
33456
fbd47f9b9b12
allow "pervasive" local theory declarations, which are applied the background theory;
wenzelm
parents:
33390
diff
changeset

344 
(P.opt_keyword "pervasive"  P.ML_source >> uncurry IsarCmd.declaration); 
22088  345 

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

347 
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

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

350 
>> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d)); 
22202  351 

5832  352 

353 
(* translation functions *) 

354 

27877  355 
val trfun = P.opt_keyword "advanced"  P.ML_source; 
14642  356 

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

22117  360 
(trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation)); 
5832  361 

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

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

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

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

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

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

22117  380 
(trfun >> (Toplevel.theory o IsarCmd.print_ast_translation)); 
5832  381 

382 

383 
(* oracles *) 

384 

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

5832  389 

390 

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

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

392 

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

394 
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

395 
(P.name  P.begin >> (fn name => 
35205  396 
Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context_cmd name))); 
21306
7ab6e95e6b0b
turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents:
21269
diff
changeset

397 

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

398 

12061  399 
(* locales *) 
400 

12758  401 
val locale_val = 
30727
519f8f0fcbf3
interpretation/interpret: prefixes within locale expression are mandatory by default;
wenzelm
parents:
30703
diff
changeset

402 
SpecParse.locale_expression false  
22117  403 
Scan.optional (P.$$$ "+"  P.!!! (Scan.repeat1 SpecParse.context_element)) []  
29223  404 
Scan.repeat1 SpecParse.context_element >> pair ([], []); 
12061  405 

24868  406 
val _ = 
12061  407 
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

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

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

412 

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

30727
519f8f0fcbf3
interpretation/interpret: prefixes within locale expression are mandatory by default;
wenzelm
parents:
30703
diff
changeset

416 
(P.xname  (P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! (SpecParse.locale_expression false) 
28895  417 
>> (fn (loc, expr) => 
30727
519f8f0fcbf3
interpretation/interpret: prefixes within locale expression are mandatory by default;
wenzelm
parents:
30703
diff
changeset

418 
Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr))); 
28895  419 

420 
val _ = 

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

421 
OuterSyntax.command "interpretation" 
29223  422 
"prove interpretation of locale expression in theory" K.thy_goal 
30727
519f8f0fcbf3
interpretation/interpret: prefixes within locale expression are mandatory by default;
wenzelm
parents:
30703
diff
changeset

423 
(P.!!! (SpecParse.locale_expression true)  
519f8f0fcbf3
interpretation/interpret: prefixes within locale expression are mandatory by default;
wenzelm
parents:
30703
diff
changeset

424 
Scan.optional (P.where_  P.and_list1 (SpecParse.opt_thm_name ":"  P.prop)) [] 
519f8f0fcbf3
interpretation/interpret: prefixes within locale expression are mandatory by default;
wenzelm
parents:
30703
diff
changeset

425 
>> (fn (expr, equations) => Toplevel.print o 
519f8f0fcbf3
interpretation/interpret: prefixes within locale expression are mandatory by default;
wenzelm
parents:
30703
diff
changeset

426 
Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations))); 
29223  427 

428 
val _ = 

429 
OuterSyntax.command "interpret" 

430 
"prove interpretation of locale expression in proof context" 

431 
(K.tag_proof K.prf_goal) 

30727
519f8f0fcbf3
interpretation/interpret: prefixes within locale expression are mandatory by default;
wenzelm
parents:
30703
diff
changeset

432 
(P.!!! (SpecParse.locale_expression true) 
519f8f0fcbf3
interpretation/interpret: prefixes within locale expression are mandatory by default;
wenzelm
parents:
30703
diff
changeset

433 
>> (fn expr => Toplevel.print o Toplevel.proof' (Expression.interpret_cmd expr))); 
29223  434 

15703  435 

22299  436 
(* classes *) 
437 

24868  438 
val class_val = 
439 
SpecParse.class_expr  

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

22299  442 

24868  443 
val _ = 
444 
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

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

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

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

453 

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

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

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

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

31869  463 
P.multi_arity >> Class.instance_arity_cmd) 
25485  464 
>> (Toplevel.print oo Toplevel.theory_to_proof) 
465 
 Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I))); 

22299  466 

467 

25519  468 
(* arbitrary overloading *) 
469 

470 
val _ = 

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

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

25519  475 
>> (fn operations => Toplevel.print o 
33553  476 
Toplevel.begin_local_theory true (Theory_Target.overloading_cmd operations))); 
25519  477 

478 

22866  479 
(* code generation *) 
480 

24868  481 
val _ = 
22866  482 
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

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

35223  485 
val _ = 
486 
OuterSyntax.command "code_abstype" "define abstract code type" K.thy_goal 

487 
(P.term  P.term >> (fn (abs, rep) => Toplevel.print 

488 
o Toplevel.theory_to_proof (Code.add_abstype_cmd abs rep))); 

489 

22866  490 

5832  491 

492 
(** proof commands **) 

493 

494 
(* statements *) 

495 

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

497 
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

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

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

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

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

505 
val _ = gen_theorem Thm.corollaryK; 

5832  506 

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

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

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

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

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

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

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

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

5832  527 

5914  528 
(* facts *) 
5832  529 

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

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

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

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

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

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

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

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

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

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

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

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

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

12926  561 

5832  562 

563 
(* proof context *) 

564 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

608 

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

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

5832  614 

615 
(* proof structure *) 

616 

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

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

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

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

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

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

632 

633 
(* end proof *) 

634 

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

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

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

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

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

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

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

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

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

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

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

664 

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

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

5832  670 

671 
(* proof steps *) 

672 

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

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

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

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

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

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

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

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

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

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

700 

6773  701 
(* calculational proof commands *) 
702 

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

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

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

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

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

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

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

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

6773  726 

6742  727 
(* proof navigation *) 
5944  728 

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

33390  732 
(Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I)); 
6742  733 

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

734 

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

735 
(* nested commands *) 
25578  736 

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

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

740 

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

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

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

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

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

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

749 

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

750 

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

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

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

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

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

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

23989  771 

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

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

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

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

787 

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

33515
d066e8369a33
print_theorems: suppress concealed (global) facts, unless "!" option is given;
wenzelm
parents:
33456
diff
changeset

791 
(opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theorems)); 
5881  792 

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

796 

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

798 
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

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

801 

24868  802 
val _ = 
32804
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31869
diff
changeset

803 
OuterSyntax.improper_command "print_locale" "print locale of this theory" K.diag 
29223  804 
(opt_bang  P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale)); 
12061  805 

24868  806 
val _ = 
32804
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31869
diff
changeset

807 
OuterSyntax.improper_command "print_interps" 
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31869
diff
changeset

808 
"print interpretations of locale for this theory" K.diag 
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31869
diff
changeset

809 
(P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations)); 
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31869
diff
changeset

810 

ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31869
diff
changeset

811 
val _ = 
12061  812 
OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag 
9010  813 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); 
5832  814 

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

818 

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

822 

24868  823 
val _ = 
11666  824 
OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag 
9221  825 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules)); 
826 

24868  827 
val _ = 
12061  828 
OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag 
9010  829 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods)); 
5832  830 

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

834 

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

838 

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

842 

24868  843 
val _ = 
9454  844 
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" 
22117  845 
K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); 
9454  846 

24868  847 
val _ = 
6723  848 
OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag 
9010  849 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); 
5832  850 

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

24868  855 
val _ = 
8370  856 
OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag 
9010  857 
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); 
8370  858 

24868  859 
val _ = 
19269  860 
OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag 
22117  861 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); 
19269  862 

24868  863 
val _ = 
8464  864 
OuterSyntax.improper_command "thm" "print theorems" K.diag 
22117  865 
(opt_modes  SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); 
5832  866 

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

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

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

871 

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

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

875 

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

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

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

882 
(opt_modes  P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); 
5832  883 

24868  884 
val _ = 
6723  885 
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

886 
(opt_modes  P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); 
5832  887 

24868  888 
val _ = 
31125
80218ee73167
transferred code generator preprocessor into separate module
haftmann
parents:
30727
diff
changeset

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

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

891 
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep 
24219  892 
(Code.print_codesetup o Toplevel.theory_of))); 
5832  893 

26184  894 
val _ = 
895 
OuterSyntax.improper_command "unused_thms" "find unused theorems" K.diag 

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

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

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

899 

5832  900 

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

901 

5832  902 
(** system commands (for interactive mode only) **) 
903 

24868  904 
val _ = 
8650  905 
OuterSyntax.improper_command "cd" "change current working directory" K.diag 
14950  906 
(P.path >> (Toplevel.no_timing oo IsarCmd.cd)); 
5832  907 

24868  908 
val _ = 
6723  909 
OuterSyntax.improper_command "pwd" "print current working directory" K.diag 
9010  910 
(Scan.succeed (Toplevel.no_timing o IsarCmd.pwd)); 
5832  911 

24868  912 
val _ = 
6723  913 
OuterSyntax.improper_command "use_thy" "use theory file" K.diag 
26404  914 
(P.name >> (fn name => 
915 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.use_thy name))); 

5832  916 

24868  917 
val _ = 
7102  918 
OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag 
27494  919 
(P.name >> (fn name => 
920 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.touch_thy name))); 

7908  921 

24868  922 
val _ = 
7102  923 
OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag 
27494  924 
(P.name >> (fn name => 
925 
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.remove_thy name))); 

7102  926 

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

7931  931 

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

24868  936 
val _ = 
14934  937 
OuterSyntax.improper_command "print_drafts" "print raw source files with symbols" 
14950  938 
K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts)); 
14934  939 

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

942 

24868  943 
val _ = 
8886  944 
OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag 
9731  945 
(opt_modes  opt_limits >> (Toplevel.no_timing oo IsarCmd.pr)); 
7199  946 

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

24868  951 
val _ = 
7222  952 
OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag 
9010  953 
(Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr)); 
7222  954 

24868  955 
val _ = 
6723  956 
OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag 
26490  957 
(P.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit)); 
5832  958 

24868  959 
val _ = 
6723  960 
OuterSyntax.improper_command "quit" "quit Isabelle" K.control 
9010  961 
(P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit)); 
5832  962 

24868  963 
val _ = 
6723  964 
OuterSyntax.improper_command "exit" "exit Isar loop" K.control 
9010  965 
(Scan.succeed (Toplevel.no_timing o IsarCmd.exit)); 
5832  966 

967 
end; 

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

968 