author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 55112  b1a5d603fd12 
permissions  rwrr 
29755  1 
theory Isar 
2 
imports Base 

3 
begin 

20472  4 

29759  5 
chapter {* Isar language elements *} 
6 

40126  7 
text {* The Isar proof language (see also 
8 
\cite[\S2]{isabelleisarref}) consists of three main categories of 

9 
language elements as follows. 

29759  10 

11 
\begin{enumerate} 

12 

39842  13 
\item Proof \emph{commands} define the primary language of 
14 
transactions of the underlying Isar/VM interpreter. Typical 

15 
examples are @{command "fix"}, @{command "assume"}, @{command 

39844  16 
"show"}, @{command "proof"}, and @{command "qed"}. 
39842  17 

39844  18 
Composing proof commands according to the rules of the Isar/VM leads 
19 
to expressions of structured proof text, such that both the machine 

20 
and the human reader can give it a meaning as formal reasoning. 

20472  21 

39842  22 
\item Proof \emph{methods} define a secondary language of mixed 
23 
forwardbackward refinement steps involving facts and goals. 

39846  24 
Typical examples are @{method rule}, @{method unfold}, and @{method 
39844  25 
simp}. 
29759  26 

39842  27 
Methods can occur in certain welldefined parts of the Isar proof 
28 
language, say as arguments to @{command "proof"}, @{command "qed"}, 

29 
or @{command "by"}. 

30 

31 
\item \emph{Attributes} define a tertiary language of small 

39849  32 
annotations to theorems being defined or referenced. Attributes can 
33 
modify both the context and the theorem. 

39842  34 

39849  35 
Typical examples are @{attribute intro} (which affects the context), 
36 
and @{attribute symmetric} (which affects the theorem). 

29759  37 

38 
\end{enumerate} 

39 
*} 

40 

41 

42 
section {* Proof commands *} 

20520  43 

39849  44 
text {* A \emph{proof command} is state transition of the Isar/VM 
45 
proof interpreter. 

46 

40126  47 
In principle, Isar proof commands could be defined in userspace as 
48 
well. The system is built like that in the first place: one part of 

49 
the commands are primitive, the other part is defined as derived 

50 
elements. Adding to the genuine structured proof language requires 

51 
profound understanding of the Isar/VM machinery, though, so this is 

52 
beyond the scope of this manual. 

39842  53 

54 
What can be done realistically is to define some diagnostic commands 

39844  55 
that inspect the general state of the Isar/VM, and report some 
56 
feedback to the user. Typically this involves checking of the 

39842  57 
linguistic \emph{mode} of a proof state, or peeking at the pending 
58 
goals (if available). 

39845  59 

60 
Another common application is to define a toplevel command that 

40126  61 
poses a problem to the user as Isar proof state and processes the 
62 
final result relatively to the context. Thus a proof can be 

39845  63 
incorporated into the context of some userspace tool, without 
40126  64 
modifying the Isar proof language itself. *} 
39842  65 

66 
text %mlref {* 

67 
\begin{mldecls} 

68 
@{index_ML_type Proof.state} \\ 

69 
@{index_ML Proof.assert_forward: "Proof.state > Proof.state"} \\ 

70 
@{index_ML Proof.assert_chain: "Proof.state > Proof.state"} \\ 

71 
@{index_ML Proof.assert_backward: "Proof.state > Proof.state"} \\ 

72 
@{index_ML Proof.simple_goal: "Proof.state > {context: Proof.context, goal: thm}"} \\ 

73 
@{index_ML Proof.goal: "Proof.state > 

74 
{context: Proof.context, facts: thm list, goal: thm}"} \\ 

75 
@{index_ML Proof.raw_goal: "Proof.state > 

76 
{context: Proof.context, facts: thm list, goal: thm}"} \\ 

39845  77 
@{index_ML Proof.theorem: "Method.text option > 
78 
(thm list list > Proof.context > Proof.context) > 

79 
(term * term list) list list > Proof.context > Proof.state"} \\ 

39842  80 
\end{mldecls} 
81 

82 
\begin{description} 

83 

39864  84 
\item Type @{ML_type Proof.state} represents Isar proof states. 
85 
This is a blockstructured configuration with proof context, 

86 
linguistic mode, and optional goal. The latter consists of goal 

87 
context, goal facts (``@{text "using"}''), and tactical goal state 

88 
(see \secref{sec:tacticalgoals}). 

39842  89 

90 
The general idea is that the facts shall contribute to the 

39844  91 
refinement of some parts of the tactical goal  how exactly is 
92 
defined by the proof method that is applied in that situation. 

39842  93 

94 
\item @{ML Proof.assert_forward}, @{ML Proof.assert_chain}, @{ML 

95 
Proof.assert_backward} are partial identity functions that fail 

96 
unless a certain linguistic mode is active, namely ``@{text 

97 
"proof(state)"}'', ``@{text "proof(chain)"}'', ``@{text 

98 
"proof(prove)"}'', respectively (using the terminology of 

99 
\cite{isabelleisarref}). 

100 

101 
It is advisable study the implementations of existing proof commands 

102 
for suitable modes to be asserted. 

103 

104 
\item @{ML Proof.simple_goal}~@{text "state"} returns the structured 

105 
Isar goal (if available) in the form seen by ``simple'' methods 

39846  106 
(like @{method simp} or @{method blast}). The Isar goal facts are 
39842  107 
already inserted as premises into the subgoals, which are presented 
39844  108 
individually as in @{ML Proof.goal}. 
39842  109 

110 
\item @{ML Proof.goal}~@{text "state"} returns the structured Isar 

111 
goal (if available) in the form seen by regular methods (like 

112 
@{method rule}). The auxiliary internal encoding of Pure 

113 
conjunctions is split into individual subgoals as usual. 

114 

115 
\item @{ML Proof.raw_goal}~@{text "state"} returns the structured 

116 
Isar goal (if available) in the raw internal form seen by ``raw'' 

39846  117 
methods (like @{method induct}). This form is rarely appropriate 
118 
for dignostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal} 

119 
should be used in most situations. 

39842  120 

39845  121 
\item @{ML Proof.theorem}~@{text "before_qed after_qed statement ctxt"} 
122 
initializes a toplevel Isar proof state within a given context. 

123 

124 
The optional @{text "before_qed"} method is applied at the end of 

125 
the proof, just before extracting the result (this feature is rarely 

126 
used). 

127 

128 
The @{text "after_qed"} continuation receives the extracted result 

129 
in order to apply it to the final context in a suitable way (e.g.\ 

130 
storing named facts). Note that at this generic level the target 

131 
context is specified as @{ML_type Proof.context}, but the usual 

132 
wrapping of toplevel proofs into command transactions will provide a 

40126  133 
@{ML_type local_theory} here (\chref{ch:localtheory}). This 
134 
affects the way how results are stored. 

39845  135 

136 
The @{text "statement"} is given as a nested list of terms, each 

137 
associated with optional @{keyword "is"} patterns as usual in the 

40126  138 
Isar source language. The original nested list structure over terms 
139 
is turned into one over theorems when @{text "after_qed"} is 

140 
invoked. 

39845  141 

39842  142 
\end{description} 
143 
*} 

144 

20520  145 

39843  146 
text %mlantiq {* 
147 
\begin{matharray}{rcl} 

148 
@{ML_antiquotation_def "Isar.goal"} & : & @{text ML_antiquotation} \\ 

149 
\end{matharray} 

150 

151 
\begin{description} 

152 

153 
\item @{text "@{Isar.goal}"} refers to the regular goal state (if 

154 
available) of the current proof state managed by the Isar toplevel 

155 
 as abstract value. 

156 

157 
This only works for diagnostic ML commands, such as @{command 

158 
ML_val} or @{command ML_command}. 

159 

160 
\end{description} 

161 
*} 

162 

163 
text %mlex {* The following example peeks at a certain goal configuration. *} 

164 

40964  165 
notepad 
166 
begin 

39846  167 
have A and B and C 
39866
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39865
diff
changeset

168 
ML_val {* 
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39865
diff
changeset

169 
val n = Thm.nprems_of (#goal @{Isar.goal}); 
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39865
diff
changeset

170 
@{assert} (n = 3); 
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39865
diff
changeset

171 
*} 
39843  172 
oops 
173 

39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset

174 
text {* Here we see 3 individual subgoals in the same way as regular 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset

175 
proof methods would do. *} 
39843  176 

20520  177 

20472  178 
section {* Proof methods *} 
179 

39847  180 
text {* A @{text "method"} is a function @{text "context \<rightarrow> thm\<^sup>* \<rightarrow> goal 
181 
\<rightarrow> (cases \<times> goal)\<^sup>*\<^sup>*"} that operates on the full Isar goal 

182 
configuration with context, goal facts, and tactical goal state and 

39843  183 
enumerates possible followup goal states, with the potential 
39844  184 
addition of named extensions of the proof context (\emph{cases}). 
39847  185 
The latter feature is rarely used. 
186 

187 
This means a proof method is like a structurally enhanced tactic 

188 
(cf.\ \secref{sec:tactics}). The wellformedness conditions for 

189 
tactics need to hold for methods accordingly, with the following 

190 
additions. 

191 

192 
\begin{itemize} 

193 

194 
\item Goal addressing is further limited either to operate either 

195 
uniformly on \emph{all} subgoals, or specifically on the 

196 
\emph{first} subgoal. 

197 

198 
Exception: oldstyle tactic emulations that are embedded into the 

199 
method space, e.g.\ @{method rule_tac}. 

200 

201 
\item A nontrivial method always needs to make progress: an 

202 
identical followup goal state has to be avoided.\footnote{This 

203 
enables the user to write method expressions like @{text "meth\<^sup>+"} 

204 
without looping, while the trivial donothing case can be recovered 

205 
via @{text "meth\<^sup>?"}.} 

206 

207 
Exception: trivial stuttering steps, such as ``@{method }'' or 

208 
@{method succeed}. 

209 

210 
\item Goal facts passed to the method must not be ignored. If there 

211 
is no sensible use of facts outside the goal state, facts should be 

212 
inserted into the subgoals that are addressed by the method. 

213 

214 
\end{itemize} 

215 

40126  216 
\medskip Syntactically, the language of proof methods appears as 
217 
arguments to Isar commands like @{command "by"} or @{command apply}. 

218 
Userspace additions are reasonably easy by plugging suitable 

219 
methodvalued parser functions into the framework, using the 

220 
@{command method_setup} command, for example. 

39843  221 

39844  222 
To get a better idea about the range of possibilities, consider the 
40126  223 
following Isar proof schemes. This is the general form of 
224 
structured proof text: 

39843  225 

226 
\medskip 

227 
\begin{tabular}{l} 

228 
@{command from}~@{text "facts\<^sub>1"}~@{command have}~@{text "props"}~@{command using}~@{text "facts\<^sub>2"} \\ 

229 
@{command proof}~@{text "(initial_method)"} \\ 

230 
\quad@{text "body"} \\ 

231 
@{command qed}~@{text "(terminal_method)"} \\ 

232 
\end{tabular} 

233 
\medskip 

234 

40126  235 
The goal configuration consists of @{text "facts\<^sub>1"} and 
236 
@{text "facts\<^sub>2"} appended in that order, and various @{text 

237 
"props"} being claimed. The @{text "initial_method"} is invoked 

238 
with facts and goals together and refines the problem to something 

239 
that is handled recursively in the proof @{text "body"}. The @{text 

240 
"terminal_method"} has another chance to finish any remaining 

39843  241 
subgoals, but it does not see the facts of the initial step. 
242 

40126  243 
\medskip This pattern illustrates unstructured proof scripts: 
39843  244 

39844  245 
\medskip 
39843  246 
\begin{tabular}{l} 
247 
@{command have}~@{text "props"} \\ 

39844  248 
\quad@{command using}~@{text "facts\<^sub>1"}~@{command apply}~@{text "method\<^sub>1"} \\ 
39843  249 
\quad@{command apply}~@{text "method\<^sub>2"} \\ 
39844  250 
\quad@{command using}~@{text "facts\<^sub>3"}~@{command apply}~@{text "method\<^sub>3"} \\ 
39843  251 
\quad@{command done} \\ 
252 
\end{tabular} 

253 
\medskip 

254 

40126  255 
The @{text "method\<^sub>1"} operates on the original claim while 
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset

256 
using @{text "facts\<^sub>1"}. Since the @{command apply} command 
40126  257 
structurally resets the facts, the @{text "method\<^sub>2"} will 
258 
operate on the remaining goal state without facts. The @{text 

259 
"method\<^sub>3"} will see again a collection of @{text 

260 
"facts\<^sub>3"} that has been inserted into the script explicitly. 

39843  261 

40126  262 
\medskip Empirically, any Isar proof method can be categorized as 
39847  263 
follows. 
39843  264 

265 
\begin{enumerate} 

266 

39847  267 
\item \emph{Special method with cases} with named context additions 
268 
associated with the followup goal state. 

39843  269 

39847  270 
Example: @{method "induct"}, which is also a ``raw'' method since it 
271 
operates on the internal representation of simultaneous claims as 

46134  272 
Pure conjunction (\secref{sec:logicaux}), instead of separate 
273 
subgoals (\secref{sec:tacticalgoals}). 

39843  274 

39847  275 
\item \emph{Structured method} with strong emphasis on facts outside 
276 
the goal state. 

277 

278 
Example: @{method "rule"}, which captures the key ideas behind 

279 
structured reasoning in Isar in purest form. 

39843  280 

39847  281 
\item \emph{Simple method} with weaker emphasis on facts, which are 
282 
inserted into subgoals to emulate oldstyle tactical as 

283 
``premises''. 

39843  284 

39847  285 
Examples: @{method "simp"}, @{method "blast"}, @{method "auto"}. 
39843  286 

39847  287 
\item \emph{Oldstyle tactic emulation} with detailed numeric goal 
288 
addressing and explicit references to entities of the internal goal 

289 
state (which are otherwise invisible from proper Isar proof text). 

40126  290 
The naming convention @{text "foo_tac"} makes this special 
291 
nonstandard status clear. 

39843  292 

39847  293 
Example: @{method "rule_tac"}. 
39843  294 

295 
\end{enumerate} 

296 

39847  297 
When implementing proof methods, it is advisable to study existing 
298 
implementations carefully and imitate the typical ``boiler plate'' 

299 
for contextsensitive parsing and further combinators to wrapup 

39848  300 
tactic expressions as methods.\footnote{Aliases or abbreviations of 
301 
the standard method combinators should be avoided. Note that from 

302 
Isabelle99 until Isabelle2009 the system did provide various odd 

303 
combinations of method wrappers that made user applications more 

304 
complicated than necessary.} 

39847  305 
*} 
306 

307 
text %mlref {* 

308 
\begin{mldecls} 

309 
@{index_ML_type Proof.method} \\ 

310 
@{index_ML METHOD_CASES: "(thm list > cases_tactic) > Proof.method"} \\ 

311 
@{index_ML METHOD: "(thm list > tactic) > Proof.method"} \\ 

312 
@{index_ML SIMPLE_METHOD: "tactic > Proof.method"} \\ 

313 
@{index_ML SIMPLE_METHOD': "(int > tactic) > Proof.method"} \\ 

314 
@{index_ML Method.insert_tac: "thm list > int > tactic"} \\ 

315 
@{index_ML Method.setup: "binding > (Proof.context > Proof.method) context_parser > 

316 
string > theory > theory"} \\ 

317 
\end{mldecls} 

318 

319 
\begin{description} 

320 

39864  321 
\item Type @{ML_type Proof.method} represents proof methods as 
322 
abstract type. 

39847  323 

324 
\item @{ML METHOD_CASES}~@{text "(fn facts => cases_tactic)"} wraps 

325 
@{text cases_tactic} depending on goal facts as proof method with 

326 
cases; the goal context is passed via method syntax. 

327 

328 
\item @{ML METHOD}~@{text "(fn facts => tactic)"} wraps @{text 

329 
tactic} depending on goal facts as regular proof method; the goal 

330 
context is passed via method syntax. 

331 

332 
\item @{ML SIMPLE_METHOD}~@{text "tactic"} wraps a tactic that 

333 
addresses all subgoals uniformly as simple proof method. Goal facts 

334 
are already inserted into all subgoals before @{text "tactic"} is 

335 
applied. 

336 

337 
\item @{ML SIMPLE_METHOD'}~@{text "tactic"} wraps a tactic that 

46267  338 
addresses a specific subgoal as simple proof method that operates on 
339 
subgoal 1. Goal facts are inserted into the subgoal then the @{text 

340 
"tactic"} is applied. 

39847  341 

342 
\item @{ML Method.insert_tac}~@{text "facts i"} inserts @{text 

343 
"facts"} into subgoal @{text "i"}. This is convenient to reproduce 

344 
part of the @{ML SIMPLE_METHOD} or @{ML SIMPLE_METHOD'} wrapping 

345 
within regular @{ML METHOD}, for example. 

346 

347 
\item @{ML Method.setup}~@{text "name parser description"} provides 

39848  348 
the functionality of the Isar command @{command method_setup} as ML 
349 
function. 

39847  350 

351 
\end{description} 

352 
*} 

353 

39851  354 
text %mlex {* See also @{command method_setup} in 
355 
\cite{isabelleisarref} which includes some abstract examples. 

356 

357 
\medskip The following toy examples illustrate how the goal facts 

39848  358 
and state are passed to proof methods. The predefined proof method 
359 
called ``@{method tactic}'' wraps ML source of type @{ML_type 

40149
4c35be108990
proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents:
40126
diff
changeset

360 
tactic} (abstracted over @{ML_text facts}). This allows immediate 
39848  361 
experimentation without parsing of concrete syntax. *} 
20472  362 

40964  363 
notepad 
364 
begin 

39847  365 
assume a: A and b: B 
366 

367 
have "A \<and> B" 

368 
apply (tactic {* rtac @{thm conjI} 1 *}) 

369 
using a apply (tactic {* resolve_tac facts 1 *}) 

370 
using b apply (tactic {* resolve_tac facts 1 *}) 

371 
done 

372 

373 
have "A \<and> B" 

374 
using a and b 

375 
ML_val "@{Isar.goal}" 

376 
apply (tactic {* Method.insert_tac facts 1 *}) 

377 
apply (tactic {* (rtac @{thm conjI} THEN_ALL_NEW atac) 1 *}) 

378 
done 

40964  379 
end 
39847  380 

39848  381 
text {* \medskip The next example implements a method that simplifies 
382 
the first subgoal by rewrite rules given as arguments. *} 

383 

384 
method_setup my_simp = {* 

385 
Attrib.thms >> (fn thms => fn ctxt => 

386 
SIMPLE_METHOD' (fn i => 

387 
CHANGED (asm_full_simp_tac 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48985
diff
changeset

388 
(put_simpset HOL_basic_ss ctxt addsimps thms) i))) 
39848  389 
*} "rewrite subgoal by given rules" 
390 

391 
text {* The concrete syntax wrapping of @{command method_setup} always 

392 
passesthrough the proof context at the end of parsing, but it is 

393 
not used in this example. 

394 

395 
The @{ML Attrib.thms} parser produces a list of theorems from the 

396 
usual Isar syntax involving attribute expressions etc.\ (syntax 

40126  397 
category @{syntax thmrefs}) \cite{isabelleisarref}. The resulting 
40149
4c35be108990
proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents:
40126
diff
changeset

398 
@{ML_text thms} are added to @{ML HOL_basic_ss} which already 
40126  399 
contains the basic Simplifier setup for HOL. 
39848  400 

401 
The tactic @{ML asm_full_simp_tac} is the one that is also used in 

402 
method @{method simp} by default. The extra wrapping by the @{ML 

403 
CHANGED} tactical ensures progress of simplification: identical goal 

404 
states are filtered out explicitly to make the raw tactic conform to 

405 
standard Isar method behaviour. 

406 

407 
\medskip Method @{method my_simp} can be used in Isar proofs like 

408 
this: 

39847  409 
*} 
410 

40964  411 
notepad 
412 
begin 

39848  413 
fix a b c 
39851  414 
assume a: "a = b" 
415 
assume b: "b = c" 

416 
have "a = c" by (my_simp a b) 

40964  417 
end 
39851  418 

419 
text {* Here is a similar method that operates on all subgoals, 

420 
instead of just the first one. *} 

421 

422 
method_setup my_simp_all = {* 

423 
Attrib.thms >> (fn thms => fn ctxt => 

424 
SIMPLE_METHOD 

425 
(CHANGED 

426 
(ALLGOALS (asm_full_simp_tac 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48985
diff
changeset

427 
(put_simpset HOL_basic_ss ctxt addsimps thms))))) 
39851  428 
*} "rewrite all subgoals by given rules" 
429 

40964  430 
notepad 
431 
begin 

39851  432 
fix a b c 
433 
assume a: "a = b" 

434 
assume b: "b = c" 

435 
have "a = c" and "c = b" by (my_simp_all a b) 

40964  436 
end 
39848  437 

438 
text {* \medskip Apart from explicit arguments, common proof methods 

439 
typically work with a default configuration provided by the context. 

440 
As a shortcut to rule management we use a cheap solution via functor 

40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40149
diff
changeset

441 
@{ML_functor Named_Thms} (see also @{file 
39848  442 
"~~/src/Pure/Tools/named_thms.ML"}). *} 
443 

39847  444 
ML {* 
445 
structure My_Simps = 

446 
Named_Thms 

45414  447 
(val name = @{binding my_simp} val description = "my_simp rule") 
39847  448 
*} 
449 
setup My_Simps.setup 

450 

39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset

451 
text {* This provides ML access to a list of theorems in canonical 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset

452 
declaration order via @{ML My_Simps.get}. The user can add or 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset

453 
delete rules via the attribute @{attribute my_simp}. The actual 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset

454 
proof method is now defined as before, but we append the explicit 
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset

455 
arguments and the rules from the context. *} 
39847  456 

39848  457 
method_setup my_simp' = {* 
458 
Attrib.thms >> (fn thms => fn ctxt => 

39847  459 
SIMPLE_METHOD' (fn i => 
460 
CHANGED (asm_full_simp_tac 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48985
diff
changeset

461 
(put_simpset HOL_basic_ss ctxt 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48985
diff
changeset

462 
addsimps (thms @ My_Simps.get ctxt)) i))) 
39848  463 
*} "rewrite subgoal by given rules and my_simp rules from the context" 
39847  464 

39848  465 
text {* 
466 
\medskip Method @{method my_simp'} can be used in Isar proofs 

467 
like this: 

468 
*} 

39847  469 

40964  470 
notepad 
471 
begin 

39847  472 
fix a b c 
473 
assume [my_simp]: "a \<equiv> b" 

474 
assume [my_simp]: "b \<equiv> c" 

39848  475 
have "a \<equiv> c" by my_simp' 
40964  476 
end 
39847  477 

39851  478 
text {* \medskip The @{method my_simp} variants defined above are 
479 
``simple'' methods, i.e.\ the goal facts are merely inserted as goal 

480 
premises by the @{ML SIMPLE_METHOD'} or @{ML SIMPLE_METHOD} wrapper. 

481 
For proof methods that are similar to the standard collection of 

40126  482 
@{method simp}, @{method blast}, @{method fast}, @{method auto} 
483 
there is little more that can be done. 

39847  484 

485 
Note that using the primary goal facts in the same manner as the 

39848  486 
method arguments obtained via concrete syntax or the context does 
487 
not meet the requirement of ``strong emphasis on facts'' of regular 

488 
proof methods, because rewrite rules as used above can be easily 

489 
ignored. A proof text ``@{command using}~@{text "foo"}~@{command 

490 
"by"}~@{text "my_simp"}'' where @{text "foo"} is not used would 

491 
deceive the reader. 

39847  492 

493 
\medskip The technical treatment of rules from the context requires 

494 
further attention. Above we rebuild a fresh @{ML_type simpset} from 

39848  495 
the arguments and \emph{all} rules retrieved from the context on 
496 
every invocation of the method. This does not scale to really large 

497 
collections of rules, which easily emerges in the context of a big 

498 
theory library, for example. 

39847  499 

39848  500 
This is an inherent limitation of the simplistic rule management via 
501 
functor @{ML_functor Named_Thms}, because it lacks toolspecific 

39847  502 
storage and retrieval. More realistic applications require 
503 
efficient indexstructures that organize theorems in a customized 

504 
manner, such as a discrimination net that is indexed by the 

39848  505 
lefthand sides of rewrite rules. For variations on the Simplifier, 
506 
reuse of the existing type @{ML_type simpset} is adequate, but 

40126  507 
scalability would require it be maintained statically within the 
508 
context data, not dynamically on each tool invocation. *} 

39847  509 

29759  510 

39865  511 
section {* Attributes \label{sec:attributes} *} 
20472  512 

39849  513 
text {* An \emph{attribute} is a function @{text "context \<times> thm \<rightarrow> 
514 
context \<times> thm"}, which means both a (generic) context and a theorem 

45414  515 
can be modified simultaneously. In practice this mixed form is very 
516 
rare, instead attributes are presented either as \emph{declaration 

517 
attribute:} @{text "thm \<rightarrow> context \<rightarrow> context"} or \emph{rule 

518 
attribute:} @{text "context \<rightarrow> thm \<rightarrow> thm"}. 

39849  519 

520 
Attributes can have additional arguments via concrete syntax. There 

521 
is a collection of contextsensitive parsers for various logical 

522 
entities (types, terms, theorems). These already take care of 

523 
applying morphisms to the arguments when attribute expressions are 

524 
moved into a different context (see also \secref{sec:morphisms}). 

525 

526 
When implementing declaration attributes, it is important to operate 

527 
exactly on the variant of the generic context that is provided by 

528 
the system, which is either global theory context or local proof 

529 
context. In particular, the background theory of a local context 

530 
must not be modified in this situation! *} 

531 

532 
text %mlref {* 

533 
\begin{mldecls} 

45414  534 
@{index_ML_type attribute} \\ 
39849  535 
@{index_ML Thm.rule_attribute: "(Context.generic > thm > thm) > attribute"} \\ 
536 
@{index_ML Thm.declaration_attribute: " 

537 
(thm > Context.generic > Context.generic) > attribute"} \\ 

538 
@{index_ML Attrib.setup: "binding > attribute context_parser > 

539 
string > theory > theory"} \\ 

540 
\end{mldecls} 

541 

542 
\begin{description} 

543 

39864  544 
\item Type @{ML_type attribute} represents attributes as concrete 
545 
type alias. 

39849  546 

547 
\item @{ML Thm.rule_attribute}~@{text "(fn context => rule)"} wraps 

548 
a contextdependent rule (mapping on @{ML_type thm}) as attribute. 

549 

550 
\item @{ML Thm.declaration_attribute}~@{text "(fn thm => decl)"} 

551 
wraps a theoremdependent declaration (mapping on @{ML_type 

552 
Context.generic}) as attribute. 

553 

554 
\item @{ML Attrib.setup}~@{text "name parser description"} provides 

555 
the functionality of the Isar command @{command attribute_setup} as 

556 
ML function. 

557 

558 
\end{description} 

559 
*} 

560 

45592  561 
text %mlantiq {* 
562 
\begin{matharray}{rcl} 

563 
@{ML_antiquotation_def attributes} & : & @{text ML_antiquotation} \\ 

564 
\end{matharray} 

565 

55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
51717
diff
changeset

566 
@{rail \<open> 
45592  567 
@@{ML_antiquotation attributes} attributes 
55112
b1a5d603fd12
prefer rail cartouche  avoid backslashed quotes;
wenzelm
parents:
51717
diff
changeset

568 
\<close>} 
45592  569 

570 
\begin{description} 

571 

572 
\item @{text "@{attributes [\<dots>]}"} embeds attribute source 

573 
representation into the ML text, which is particularly useful with 

574 
declarations like @{ML Local_Theory.note}. Attribute names are 

575 
internalized at compile time, but the source is unevaluated. This 

576 
means attributes with formal arguments (types, terms, theorems) may 

577 
be subject to odd effects of dynamic scoping! 

578 

579 
\end{description} 

580 
*} 

581 

39849  582 
text %mlex {* See also @{command attribute_setup} in 
583 
\cite{isabelleisarref} which includes some abstract examples. *} 

30272  584 

20472  585 
end 