1 |
1 |
2 \chapter{Basic Isar elements}\label{ch:pure-syntax} |
2 \chapter{Basic Isar Elements}\label{ch:pure-syntax} |
3 |
3 |
4 Subsequently, we introduce the main part of the basic Isar theory and proof |
4 Subsequently, we introduce the main part of the basic Isar theory and proof |
5 commands as provided by Isabelle/Pure. Chapter~\ref{ch:gen-tools} describes |
5 commands as provided by Isabelle/Pure. Chapter~\ref{ch:gen-tools} describes |
6 further Isar elements as provided by generic tools and packages that are |
6 further Isar elements as provided by generic tools and packages (such as the |
7 either part of Pure Isabelle, or pre-loaded by most object logics (such as the |
7 Simplifier) that are either part of Pure Isabelle, or pre-loaded by most |
8 Simplifier). See chapter~\ref{ch:hol-tools} for actual object-logic specific |
8 object logics. See chapter~\ref{ch:hol-tools} for actual object-logic |
9 elements (for Isabelle/HOL). |
9 specific elements (for Isabelle/HOL). |
10 |
10 |
11 \medskip |
11 \medskip |
12 |
12 |
13 Isar commands may be either \emph{proper} document constructors, or |
13 Isar commands may be either \emph{proper} document constructors, or |
14 \emph{improper commands} (indicated by $^*$). Some proof methods and |
14 \emph{improper commands} (indicated by $^*$). Some proof methods and |
15 attributes introduced later may be classified as improper as well. Improper |
15 attributes introduced later are classified as improper as well. Improper Isar |
16 Isar language elements might be helpful when developing proof documents, while |
16 language elements might be helpful when developing proof documents, while |
17 their use is strongly discouraged for the final version. Typical examples are |
17 their use is strongly discouraged for the final version. Typical examples are |
18 diagnostic commands that print terms or theorems according to the current |
18 diagnostic commands that print terms or theorems according to the current |
19 context; other commands even emulate old-style tactical theorem proving, which |
19 context; other commands even emulate old-style tactical theorem proving, which |
20 facilitates porting of legacy proof scripts. |
20 facilitates porting of legacy proof scripts. |
21 |
21 |
31 \isarcmd{end} & : & \isartrans{theory}{\cdot} \\ |
31 \isarcmd{end} & : & \isartrans{theory}{\cdot} \\ |
32 \end{matharray} |
32 \end{matharray} |
33 |
33 |
34 Isabelle/Isar ``new-style'' theories are either defined via theory files or |
34 Isabelle/Isar ``new-style'' theories are either defined via theory files or |
35 interactively. Both actual theory specifications and proofs are handled |
35 interactively. Both actual theory specifications and proofs are handled |
36 uniformly --- occasionally definitional mechanisms even require some manual |
36 uniformly --- occasionally definitional mechanisms even require some explicit |
37 proof. In contrast, ``old-style'' Isabelle theories support batch processing |
37 proof as well. In contrast, ``old-style'' Isabelle theories support batch |
38 only, with the proof scripts collected in separate ML files. |
38 processing only, with the proof scripts collected in separate ML files. |
39 |
39 |
40 The first command of any theory has to be $\THEORY$, starting a new theory |
40 The first command of any theory has to be $\THEORY$, starting a new theory |
41 based on the merge of existing ones. The theory context may be also changed |
41 based on the merge of existing ones. The theory context may be also changed |
42 by $\CONTEXT$ without creating a new theory. In both cases, $\END$ concludes |
42 by $\CONTEXT$ without creating a new theory. In both cases, $\END$ concludes |
43 the theory development; it has to be the very last command of any proper |
43 the theory development; it has to be the very last command of any proper |
59 existing ones $B@1 + \cdots + B@n$. Isabelle's theory loader system ensures |
59 existing ones $B@1 + \cdots + B@n$. Isabelle's theory loader system ensures |
60 that any of the base theories are properly loaded (and fully up-to-date when |
60 that any of the base theories are properly loaded (and fully up-to-date when |
61 $\THEORY$ is executed interactively). The optional $\isarkeyword{files}$ |
61 $\THEORY$ is executed interactively). The optional $\isarkeyword{files}$ |
62 specification declares additional dependencies on ML files. Unless put in |
62 specification declares additional dependencies on ML files. Unless put in |
63 parentheses, any file will be loaded immediately via $\isarcmd{use}$ (see |
63 parentheses, any file will be loaded immediately via $\isarcmd{use}$ (see |
64 also \S\ref{sec:ML}). |
64 also \S\ref{sec:ML}). The optional ML file \texttt{$A$.ML} that may be |
|
65 associated with any theory should \emph{not} be included in |
|
66 $\isarkeyword{files}$. |
65 |
67 |
66 \item [$\CONTEXT~B$] enters an existing theory context $B$, basically in |
68 \item [$\CONTEXT~B$] enters an existing theory context $B$, basically in |
67 read-only mode, so only a limited set of commands may be performed. Just as |
69 read-only mode, so only a limited set of commands may be performed. Just as |
68 for $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date. |
70 for $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date. |
69 |
71 |
110 \end{rail} |
112 \end{rail} |
111 |
113 |
112 \begin{descr} |
114 \begin{descr} |
113 \item [$\isarkeyword{title}~title~author~date$] specifies the document title |
115 \item [$\isarkeyword{title}~title~author~date$] specifies the document title |
114 just as in typical {\LaTeX} documents. |
116 just as in typical {\LaTeX} documents. |
115 \item [$\isarkeyword{chapter}~text$, $\isarkeyword{section}~text$, |
117 \item [$\isarkeyword{chapter}$, $\isarkeyword{section}$, |
116 $\isarkeyword{subsection}~text$, and $\isarkeyword{subsubsection}~text$] |
118 $\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter |
117 mark chapter and section headings. |
119 and section headings. |
118 \item [$\TEXT~text$] specifies an actual body of prose text, including |
120 \item [$\TEXT$] specifies an actual body of prose text, including references |
119 references to formal entities.\footnote{The latter feature is not yet |
121 to formal entities.\footnote{The latter feature is not yet exploited. |
120 exploited. Nevertheless, any text of the form |
122 Nevertheless, any text of the form \texttt{\at\ttlbrace\dots\ttrbrace} |
121 \texttt{\at\ttlbrace\dots\ttrbrace} should be considered as reserved for |
123 should be considered as reserved for future use.} |
122 future use.} |
|
123 \end{descr} |
124 \end{descr} |
124 |
125 |
125 |
126 |
126 \subsection{Type classes and sorts}\label{sec:classes} |
127 \subsection{Type classes and sorts}\label{sec:classes} |
127 |
128 |
140 'defaultsort' sort comment? |
141 'defaultsort' sort comment? |
141 ; |
142 ; |
142 \end{rail} |
143 \end{rail} |
143 |
144 |
144 \begin{descr} |
145 \begin{descr} |
145 \item [$\isarkeyword{classes}~c<\vec c ~\dots$] declares class $c$ to be a |
146 \item [$\isarkeyword{classes}~c<\vec c$] declares class $c$ to be a subclass |
146 subclass of existing classes $\vec c$. Cyclic class structures are ruled |
147 of existing classes $\vec c$. Cyclic class structures are ruled out. |
147 out. |
|
148 \item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between |
148 \item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between |
149 existing classes $c@1$ and $c@2$. This is done axiomatically! The |
149 existing classes $c@1$ and $c@2$. This is done axiomatically! The |
150 $\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way |
150 $\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way |
151 introduce proven class relations. |
151 introduce proven class relations. |
152 \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for |
152 \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for |
175 'arities' (nameref '::' arity comment? +) |
175 'arities' (nameref '::' arity comment? +) |
176 ; |
176 ; |
177 \end{rail} |
177 \end{rail} |
178 |
178 |
179 \begin{descr} |
179 \begin{descr} |
180 \item [$\TYPES~(\vec\alpha)t = \tau~\dots$] introduces \emph{type synonym} |
180 \item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym} |
181 $(\vec\alpha)t$ for existing type $\tau$. Unlike actual type definitions, |
181 $(\vec\alpha)t$ for existing type $\tau$. Unlike actual type definitions, |
182 as are available in Isabelle/HOL for example, type synonyms are just purely |
182 as are available in Isabelle/HOL for example, type synonyms are just purely |
183 syntactic abbreviations, without any logical significance. Internally, type |
183 syntactic abbreviations, without any logical significance. Internally, type |
184 synonyms are fully expanded, as may be observed when printing terms or |
184 synonyms are fully expanded, as may be observed when printing terms or |
185 theorems. |
185 theorems. |
187 $t$, intended as an actual logical type. Note that some logics such as |
187 $t$, intended as an actual logical type. Note that some logics such as |
188 Isabelle/HOL provide their own version of $\isarkeyword{typedecl}$. |
188 Isabelle/HOL provide their own version of $\isarkeyword{typedecl}$. |
189 \item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors |
189 \item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors |
190 $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of |
190 $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of |
191 Isabelle's inner syntax of terms or types. |
191 Isabelle's inner syntax of terms or types. |
192 \item [$\isarkeyword{arities}~t::(\vec s)s~\dots$] augments Isabelle's |
192 \item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted |
193 order-sorted signature of types by new type constructor arities. This is |
193 signature of types by new type constructor arities. This is done |
194 done axiomatically! The $\isarkeyword{instance}$ command (see |
194 axiomatically! The $\isarkeyword{instance}$ command (see |
195 \S\ref{sec:axclass}) provides a way introduce proven type arities. |
195 \S\ref{sec:axclass}) provides a way introduce proven type arities. |
196 \end{descr} |
196 \end{descr} |
197 |
197 |
198 |
198 |
199 \subsection{Constants and simple definitions} |
199 \subsection{Constants and simple definitions} |
216 constdecl: name '::' type mixfix? comment? |
216 constdecl: name '::' type mixfix? comment? |
217 ; |
217 ; |
218 \end{rail} |
218 \end{rail} |
219 |
219 |
220 \begin{descr} |
220 \begin{descr} |
221 \item [$\CONSTS~c::\sigma~\dots$] declares constant $c$ to have any instance |
221 \item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type |
222 of type scheme $\sigma$. The optional mixfix annotations may attach |
222 scheme $\sigma$. The optional mixfix annotations may attach concrete syntax |
223 concrete syntax constants. |
223 constants. |
224 \item [$\DEFS~name: eqn~\dots$] introduces $eqn$ as a definitional axiom for |
224 \item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some |
225 some existing constant. See \cite[\S6]{isabelle-ref} for more details on |
225 existing constant. See \cite[\S6]{isabelle-ref} for more details on the |
226 the form of equations admitted as constant definitions. |
226 form of equations admitted as constant definitions. |
227 \item [$\isarkeyword{constdefs}~c::\sigma~eqn~\dots$] combines constant |
227 \item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and |
228 declarations and definitions, using canonical name $c_def$ for the |
228 definitions of constants, using canonical name $c_def$ for the definitional |
229 definitional axiom. |
229 axiom. |
230 \end{descr} |
230 \end{descr} |
231 |
231 |
232 |
232 |
233 \subsection{Syntax and translations} |
233 \subsection{Syntax and translations} |
234 |
234 |
249 |
249 |
250 \begin{descr} |
250 \begin{descr} |
251 \item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$, |
251 \item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$, |
252 except that the actual logical signature extension is omitted. Thus the |
252 except that the actual logical signature extension is omitted. Thus the |
253 context free grammar of Isabelle's inner syntax may be augmented in |
253 context free grammar of Isabelle's inner syntax may be augmented in |
254 arbitrary ways. The $mode$ argument refers to the print mode that the |
254 arbitrary ways, independently of the logic. The $mode$ argument refers to |
255 grammar rules belong; unless there is the \texttt{output} flag given, all |
255 the print mode that the grammar rules belong; unless there is the |
256 productions are added both to the input and output grammar. |
256 \texttt{output} flag given, all productions are added both to the input and |
|
257 output grammar. |
257 \item [$\isarkeyword{translations}~rules$] specifies syntactic translation |
258 \item [$\isarkeyword{translations}~rules$] specifies syntactic translation |
258 rules (also known as \emph{macros}): parse/print rules (\texttt{==}), parse |
259 rules (also known as \emph{macros}): parse/print rules (\texttt{==}), parse |
259 rules (\texttt{=>}), print rules (\texttt{<=}). Translation patterns may be |
260 rules (\texttt{=>}), or print rules (\texttt{<=}). Translation patterns may |
260 prefixed by the syntactic category to be used for parsing; the default is |
261 be prefixed by the syntactic category to be used for parsing; the default is |
261 \texttt{logic}. |
262 \texttt{logic}. |
262 \end{descr} |
263 \end{descr} |
263 |
264 |
264 |
265 |
265 \subsection{Axioms and theorems} |
266 \subsection{Axioms and theorems} |
277 ('theorems' | 'lemmas') thmdef? thmrefs |
278 ('theorems' | 'lemmas') thmdef? thmrefs |
278 ; |
279 ; |
279 \end{rail} |
280 \end{rail} |
280 |
281 |
281 \begin{descr} |
282 \begin{descr} |
282 \item [$\isarkeyword{axioms}~name: \phi~\dots$] introduces arbitrary |
283 \item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as |
283 statements as logical axioms. In fact, axioms are ``axiomatic theorems'', |
284 logical axioms. In fact, axioms are ``axiomatic theorems'', and may be |
284 and may be referred just as any other theorem later. |
285 referred later just as any other theorem. |
285 |
286 |
286 Axioms are usually only introduced when declaring new logical systems. |
287 Axioms are usually only introduced when declaring new logical systems. |
287 Everyday work is typically done the hard way, with proper definitions and |
288 Everyday work is typically done the hard way, with proper definitions and |
288 actual theorems. |
289 actual theorems. |
289 \item [$\isarkeyword{theorems}~name = thms$] stores lists of existing theorems |
290 \item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems. |
290 as $name$. Typical applications would also involve attributes (to augment |
291 Typical applications would also involve attributes, to augment the default |
291 the default simpset, for example). |
292 Simplifier context, for example. |
292 \item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but |
293 \item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but |
293 tags the results as ``lemma''. |
294 tags the results as ``lemma''. |
294 \end{descr} |
295 \end{descr} |
295 |
296 |
296 |
297 |
300 \begin{matharray}{rcl} |
301 \begin{matharray}{rcl} |
301 \isarcmd{global} & : & \isartrans{theory}{theory} \\ |
302 \isarcmd{global} & : & \isartrans{theory}{theory} \\ |
302 \isarcmd{local} & : & \isartrans{theory}{theory} \\ |
303 \isarcmd{local} & : & \isartrans{theory}{theory} \\ |
303 \end{matharray} |
304 \end{matharray} |
304 |
305 |
305 Isabelle organises any kind of names (of types, constants, theorems etc.) by |
306 Isabelle organizes any kind of names (of types, constants, theorems etc.) by |
306 hierarchically structured name spaces. Normally the user never has to control |
307 hierarchically structured name spaces. Normally the user never has to control |
307 the behaviour of name space entry by hand, yet the following commands provide |
308 the behavior of name space entry by hand, yet the following commands provide |
308 some way to do so. |
309 some way to do so. |
309 |
310 |
310 \begin{descr} |
311 \begin{descr} |
311 \item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current |
312 \item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current |
312 name declaration mode. Initially, theories start in $\isarkeyword{local}$ |
313 name declaration mode. Initially, theories start in $\isarkeyword{local}$ |
340 Furthermore, the file name is checked with the $\isarkeyword{files}$ |
341 Furthermore, the file name is checked with the $\isarkeyword{files}$ |
341 dependency declaration given in the theory header (see also |
342 dependency declaration given in the theory header (see also |
342 \S\ref{sec:begin-thy}). |
343 \S\ref{sec:begin-thy}). |
343 \item [$\isarkeyword{ML}~text$] reads and executes ML commands from $text$. |
344 \item [$\isarkeyword{ML}~text$] reads and executes ML commands from $text$. |
344 The theory context is passed just as for $\isarkeyword{use}$. |
345 The theory context is passed just as for $\isarkeyword{use}$. |
|
346 %FIXME picked up again!? |
345 \item [$\isarkeyword{setup}~text$] changes the current theory context by |
347 \item [$\isarkeyword{setup}~text$] changes the current theory context by |
346 applying setup functions $text$, which has to be an ML expression of type |
348 applying setup functions $text$, which has to be an ML expression of type |
347 $(theory \to theory)~list$. The $\isarkeyword{setup}$ command is the usual |
349 $(theory \to theory)~list$. The $\isarkeyword{setup}$ command is the usual |
348 way to initialise object-logic specific tools and packages written in ML. |
350 way to initialize object-logic specific tools and packages written in ML. |
349 \end{descr} |
351 \end{descr} |
350 |
352 |
351 |
353 |
352 \subsection{Syntax translation functions} |
354 \subsection{Syntax translation functions} |
353 |
355 |
387 \end{rail} |
389 \end{rail} |
388 |
390 |
389 \begin{descr} |
391 \begin{descr} |
390 \item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML |
392 \item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML |
391 function $text$, which has to be of type $Sign\mathord.sg \times |
393 function $text$, which has to be of type $Sign\mathord.sg \times |
392 Object\mathord.T \to term)$. |
394 Object\mathord.T \to term$. |
393 \end{descr} |
395 \end{descr} |
394 |
396 |
395 |
397 |
396 \section{Proof commands} |
398 \section{Proof commands} |
397 |
399 |
398 Proof commands provide transitions of Isar/VM machine configurations, which |
400 Proof commands provide transitions of Isar/VM machine configurations, which |
399 are block-structured, consisting of a stack of nodes with three main |
401 are block-structured, consisting of a stack of nodes with three main |
400 components: logical \emph{proof context}, local \emph{facts}, and open |
402 components: logical proof context, current facts, and open goals. Isar/VM |
401 \emph{goals}. Isar/VM transitions are \emph{typed} according to the following |
403 transitions are \emph{typed} according to the following three three different |
402 three three different modes of operation: |
404 modes of operation: |
403 \begin{descr} |
405 \begin{descr} |
404 \item [$proof(prove)$] means that a new goal has just been stated that is now |
406 \item [$proof(prove)$] means that a new goal has just been stated that is now |
405 to be \emph{proven}; the next command may refine it by some proof method |
407 to be \emph{proven}; the next command may refine it by some proof method |
406 ($\approx$ tactic), and enter a sub-proof to establish the final result. |
408 ($\approx$ tactic), and enter a sub-proof to establish the final result. |
407 \item [$proof(state)$] is like an internal theory mode: the context may be |
409 \item [$proof(state)$] is like an internal theory mode: the context may be |
408 augmented by \emph{stating} additional assumptions, intermediate result etc. |
410 augmented by \emph{stating} additional assumptions, intermediate result etc. |
409 \item [$proof(chain)$] is an intermediate mode between $proof(state)$ and |
411 \item [$proof(chain)$] is an intermediate mode between $proof(state)$ and |
410 $proof(prove)$: existing facts have been just picked up in order to use them |
412 $proof(prove)$: existing facts have been just picked up in order to use them |
411 when refining the goal to be claimed next. |
413 when refining the goal claimed next. |
412 \end{descr} |
414 \end{descr} |
413 |
415 |
414 |
416 |
415 \subsection{Formal comments}\label{sec:formal-cmt-prf} |
417 \subsection{Formal comments}\label{sec:formal-cmt-prf} |
416 |
418 |
452 |
454 |
453 Similarly, introducing some assumption $\chi$ has two effects. On the one |
455 Similarly, introducing some assumption $\chi$ has two effects. On the one |
454 hand, a local theorem is created that may be used as a fact in subsequent |
456 hand, a local theorem is created that may be used as a fact in subsequent |
455 proof steps. On the other hand, any result $\phi$ exported from the context |
457 proof steps. On the other hand, any result $\phi$ exported from the context |
456 becomes conditional wrt.\ the assumption. Thus, solving an enclosing goal |
458 becomes conditional wrt.\ the assumption. Thus, solving an enclosing goal |
457 using this result would basically introduce a new subgoal stemming from the |
459 using such a result would basically introduce a new subgoal stemming from the |
458 assumption. How this situation is handled depends on the actual version of |
460 assumption. How this situation is handled depends on the actual version of |
459 assumption command used: while $\ASSUMENAME$ solves the subgoal by unifying |
461 assumption command used: while $\ASSUMENAME$ solves the subgoal by unifying |
460 with some premise of the goal, $\PRESUMENAME$ leaves the subgoal unchanged to |
462 with some premise of the goal, $\PRESUMENAME$ leaves the subgoal unchanged to |
461 be proved later by the user. |
463 be proved later by the user. |
462 |
464 |
480 \end{rail} |
482 \end{rail} |
481 |
483 |
482 \begin{descr} |
484 \begin{descr} |
483 \item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$. |
485 \item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$. |
484 \item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems |
486 \item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems |
485 $\Phi$. Subsequent results applied to some enclosing goal (e.g.\ via |
487 $\Phi$ by assumption. Subsequent results applied to an enclosing goal |
486 $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be able to |
488 (e.g.\ via $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be |
487 unify with existing premises in the goal, while $\PRESUMENAME$ leaves $\Phi$ |
489 able to unify with existing premises in the goal, while $\PRESUMENAME$ |
488 as new subgoals. Note that several lists of assumptions may be given |
490 leaves $\Phi$ as new subgoals. |
489 (separated by $\isarkeyword{and}$); the resulting list of facts consists of |
491 |
490 all of these concatenated. |
492 Several lists of assumptions may be given (separated by |
|
493 $\isarkeyword{and}$); the resulting list of facts consists of all of these |
|
494 concatenated. |
491 \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition. |
495 \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition. |
492 In results exported from the context, $x$ is replaced by $t$. Basically, |
496 In results exported from the context, $x$ is replaced by $t$. Basically, |
493 $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$ (the |
497 $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$, with the |
494 resulting hypothetical equation is solved by reflexivity, though). |
498 resulting hypothetical equation solved by reflexivity. |
495 \end{descr} |
499 \end{descr} |
496 |
500 |
497 The internal register $prems$\indexisarreg{prems} refers to the current list |
501 The special theorem name $prems$\indexisarreg{prems} refers to all current |
498 of assumptions. |
502 assumptions. |
499 |
503 |
500 |
504 |
501 \subsection{Facts and forward chaining} |
505 \subsection{Facts and forward chaining} |
502 |
506 |
503 \indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with} |
507 \indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with} |
507 \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\ |
511 \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\ |
508 \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\ |
512 \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\ |
509 \end{matharray} |
513 \end{matharray} |
510 |
514 |
511 New facts are established either by assumption or proof of local statements. |
515 New facts are established either by assumption or proof of local statements. |
512 Any facts will usually be involved in proofs of further results: either as |
516 Any fact will usually be involved in further proofs, either as explicit |
513 explicit arguments of proof methods or when forward chaining towards the next |
517 arguments of proof methods or when forward chaining towards the next goal via |
514 goal via $\THEN$ (and variants). Note that the internal register of |
518 $\THEN$ (and variants). Note that the special theorem name |
515 \emph{current facts} may be referred as theorem list |
519 $facts$.\indexisarreg{facts} refers to the most recently established facts. |
516 $facts$.\indexisarreg{facts} |
|
517 |
|
518 \begin{rail} |
520 \begin{rail} |
519 'note' thmdef? thmrefs comment? |
521 'note' thmdef? thmrefs comment? |
520 ; |
522 ; |
521 'then' comment? |
523 'then' comment? |
522 ; |
524 ; |
527 \begin{descr} |
529 \begin{descr} |
528 \item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result |
530 \item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result |
529 as $a$. Note that attributes may be involved as well, both on the left and |
531 as $a$. Note that attributes may be involved as well, both on the left and |
530 right hand sides. |
532 right hand sides. |
531 \item [$\THEN$] indicates forward chaining by the current facts in order to |
533 \item [$\THEN$] indicates forward chaining by the current facts in order to |
532 establish the goal to be claimed next. The initial proof method invoked to |
534 establish the goal claimed next. The initial proof method invoked to refine |
533 solve that will be offered these facts to do ``anything appropriate'' (see |
535 that will be offered these facts to do ``anything appropriate'' (see also |
534 also \S\ref{sec:proof-steps}). For example, method $rule$ (see |
536 \S\ref{sec:proof-steps}). For example, method $rule$ (see |
535 \S\ref{sec:pure-meth}) would do an elimination rather than an introduction. |
537 \S\ref{sec:pure-meth}) would do an elimination rather than an introduction. |
536 \item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; also note that |
538 \item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is |
537 $\THEN$ is equivalent to $\FROM{facts}$. |
539 equivalent to $\FROM{facts}$. |
538 \item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward |
540 \item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward |
539 chaining is from earlier facts together with the current ones. |
541 chaining is from earlier facts together with the current ones. |
540 \end{descr} |
542 \end{descr} |
541 |
543 |
542 |
544 |
567 goal: thmdecl? proppat comment? |
569 goal: thmdecl? proppat comment? |
568 ; |
570 ; |
569 \end{rail} |
571 \end{rail} |
570 |
572 |
571 \begin{descr} |
573 \begin{descr} |
572 \item [$\THEOREM{name}{\phi}$] enters proof mode with $\phi$ as main goal, |
574 \item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal, |
573 eventually resulting in some theorem $\turn \phi$, which will be stored in |
575 eventually resulting in some theorem $\turn \phi$, which will be stored in |
574 the theory. |
576 the theory. |
575 \item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as |
577 \item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as |
576 ``lemma''. |
578 ``lemma''. |
577 \item [$\HAVE{name}{\phi}$] claims a local goal, eventually resulting in a |
579 \item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a |
578 theorem with the current assumption context as hypotheses. |
580 theorem with the current assumption context as hypotheses. |
579 \item [$\SHOW{name}{\phi}$] is similar to $\HAVE{name}{\phi}$, but solves some |
581 \item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some |
580 pending goal with the result \emph{exported} into the corresponding context. |
582 pending goal with the result \emph{exported} into the corresponding context. |
581 \item [$\HENCE{name}{\phi}$] abbreviates $\THEN~\HAVE{name}{\phi}$, i.e.\ |
583 \item [$\HENCE{a}{\phi}$] abbreviates $\THEN~\HAVE{a}{\phi}$, i.e.\ claims a |
582 claims a local goal to be proven by forward chaining the current facts. |
584 local goal to be proven by forward chaining the current facts. |
583 \item [$\THUS{name}{\phi}$] abbreviates $\THEN~\SHOW{name}{\phi}$. |
585 \item [$\THUS{a}{\phi}$] abbreviates $\THEN~\SHOW{a}{\phi}$. |
584 \end{descr} |
586 \end{descr} |
585 |
587 |
586 |
588 |
587 \subsection{Initial and terminal proof steps}\label{sec:proof-steps} |
589 \subsection{Initial and terminal proof steps}\label{sec:proof-steps} |
588 |
590 |
595 \isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ |
597 \isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ |
596 \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ |
598 \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ |
597 \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ |
599 \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ |
598 \end{matharray} |
600 \end{matharray} |
599 |
601 |
600 Arbitrary goal refinements via tactics is considered harmful. Consequently |
602 Arbitrary goal refinement via tactics is considered harmful. Consequently the |
601 the Isar framework admits proof methods to be invoked in two places only. |
603 Isar framework admits proof methods to be invoked in two places only. |
602 \begin{enumerate} |
604 \begin{enumerate} |
603 \item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated |
605 \item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated |
604 intermediate goal to a number of sub-goals that are to be solved later. |
606 goal to a number of sub-goals that are to be solved later. Facts are passed |
605 Facts are passed to $m@1$ for forward chaining if so indicated by |
607 to $m@1$ for forward chaining if so indicated by $proof(chain)$ mode. |
606 $proof(chain)$ mode. |
|
607 |
608 |
608 \item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining |
609 \item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining goals |
609 pending goals completely. No facts are passed to $m@2$. |
610 completely. No facts are passed to $m@2$. |
610 \end{enumerate} |
611 \end{enumerate} |
611 |
612 |
612 The only other proper way to affect pending goals is by $\SHOWNAME$, which |
613 The only other proper way to affect pending goals is by $\SHOWNAME$ (or |
613 involves an explicit statement of what is solved. |
614 $\THUSNAME$), which involves an explicit statement of what is to be solved. |
614 |
615 |
615 \medskip |
616 \medskip |
616 |
617 |
617 Also note that initial proof methods should either solve the goal completely, |
618 Also note that initial proof methods should either solve the goal completely, |
618 or constitute some well-understood deterministic reduction to new sub-goals. |
619 or constitute some well-understood deterministic reduction to new sub-goals. |
642 meth: method interest? |
643 meth: method interest? |
643 ; |
644 ; |
644 \end{rail} |
645 \end{rail} |
645 |
646 |
646 \begin{descr} |
647 \begin{descr} |
647 \item [$\PROOF{m@1}$] refines the pending goal by proof method $m@1$; facts |
648 \item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for |
648 for forward chaining are passed if so indicated by $proof(chain)$. |
649 forward chaining are passed if so indicated by $proof(chain)$ mode. |
649 \item [$\QED{m@2}$] refines any remaining goals by proof method $m@1$ and |
650 \item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and |
650 concludes the sub-proof. If the goal had been $\SHOWNAME$, some pending |
651 concludes the sub-proof. If the goal had been $\SHOWNAME$ (or $\THUSNAME$), |
651 sub-goal is solved as well by the rule resulting from the result exported to |
652 some pending sub-goal is solved as well by the rule resulting from the |
652 the enclosing goal context. Thus $\QEDNAME$ may fail for two reasons: |
653 result exported to the enclosing goal context. Thus $\QEDNAME$ may fail for |
653 either $m@2$ fails to solve all remaining goals completely, or the resulting |
654 two reasons: either $m@2$ fails to solve all remaining goals completely, or |
654 rule does not resolve with any enclosing goal. Debugging such a situation |
655 the resulting rule does not resolve with any enclosing goal. Debugging such |
655 might involve temporarily changing $\SHOWNAME$ into $\HAVENAME$, or |
656 a situation might involve temporarily changing $\SHOWNAME$ into $\HAVENAME$, |
656 weakening the local context by replacing $\ASSUMENAME$ by $\PRESUMENAME$. |
657 or softening the local context by replacing $\ASSUMENAME$ by $\PRESUMENAME$. |
657 \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}; it abbreviates |
658 \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}; it abbreviates |
658 $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both methods. |
659 $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both methods. |
659 Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done by simply |
660 Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done by simply |
660 expanding the abbreviation by hand; note that $\PROOF{m@1}$ is usually |
661 expanding the abbreviation by hand; note that $\PROOF{m@1}$ is usually |
661 sufficient to see what is going wrong. |
662 sufficient to see what is going wrong. |
662 \item [``$\DDOT$''] is a \emph{default proof}; it abbreviates $\BY{default}$. |
663 \item [``$\DDOT$''] is a \emph{default proof}; it abbreviates $\BY{default}$. |
663 \item [``$\DOT$''] is a \emph{trivial proof}, it abbreviates $\BY{-}$, where |
664 \item [``$\DOT$''] is a \emph{trivial proof}; it abbreviates $\BY{-}$. |
664 method ``$-$'' does nothing except inserting any facts into the proof state. |
|
665 \item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that |
665 \item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that |
666 \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve |
666 \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve |
667 the goal without much ado. Of course, the result is a fake theorem only, |
667 the goal without further ado. Of course, the result is a fake theorem only, |
668 involving some oracle in its internal derivation object (this is indicated |
668 involving some oracle in its internal derivation object (this is indicated |
669 as $[!]$ in the printed result). The main application of |
669 as $[!]$ in the printed result). The main application of |
670 $\isarkeyword{sorry}$ is to support top-down proof development. |
670 $\isarkeyword{sorry}$ is to support top-down proof development. |
671 \end{descr} |
671 \end{descr} |
672 |
672 |
695 'back' |
695 'back' |
696 ; |
696 ; |
697 \end{rail} |
697 \end{rail} |
698 |
698 |
699 \begin{descr} |
699 \begin{descr} |
700 \item [$\isarkeyword{apply}~m$] applies proof method $m$ in the |
700 \item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in the |
701 plain-old-tactic sense. Facts for forward chaining are ignored. |
701 plain-old-tactic sense. Facts for forward chaining are ignored. |
702 \item [$\isarkeyword{then_apply}~m$] is similar to $\isarkeyword{apply}$, but |
702 \item [$\isarkeyword{then_apply}~(m)$] is similar to $\isarkeyword{apply}$, |
703 observes the goal's facts. |
703 but observes the goal's facts. |
704 \item [$\isarkeyword{back}$] does back-tracking over the result sequence of |
704 \item [$\isarkeyword{back}$] does back-tracking over the result sequence of |
705 the last proof command. Basically, any proof command may return multiple |
705 the last proof command. Basically, any proof command may return multiple |
706 results. |
706 results. |
707 \end{descr} |
707 \end{descr} |
708 |
708 |
745 preceding statement. Also note that $\ISNAME$ is not a separate command, |
745 preceding statement. Also note that $\ISNAME$ is not a separate command, |
746 but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.). |
746 but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.). |
747 \end{descr} |
747 \end{descr} |
748 |
748 |
749 A few \emph{automatic} term abbreviations\index{automatic abbreviation} for |
749 A few \emph{automatic} term abbreviations\index{automatic abbreviation} for |
750 goals and facts are available as well. For any open goal, $\VVar{thesis}$ |
750 goals and facts are available as well. For any open goal, |
751 refers to its object-logical statement, $\VVar{thesis_prop}$ to the full |
751 $\VVar{thesis_prop}$ refers to the full proposition (which may be a rule), |
752 proposition (which may be a rule), and $\VVar{thesis_concl}$ to its (atomic) |
752 $\VVar{thesis_concl}$ to its (atomic) conclusion, and $\VVar{thesis}$ to its |
753 conclusion. |
753 object-logical statement. The latter two abstract over any meta-level |
|
754 parameters. |
754 |
755 |
755 Facts (i.e.\ assumptions and finished goals) that have an application $f(x)$ |
756 Facts (i.e.\ assumptions and finished goals) that have an application $f(x)$ |
756 as object-logic statement get $x$ bound to the special text variable |
757 as object-logic statement get $x$ bound to the special text variable |
757 ``$\dots$'' (three dots). The canonical application of this feature are |
758 ``$\dots$'' (three dots). The canonical application of this feature are |
758 calculational proofs, see \S\ref{sec:calculation}. |
759 calculational proofs (see \S\ref{sec:calculation}). |
759 |
760 |
760 |
761 |
761 \subsection{Block structure} |
762 \subsection{Block structure} |
762 |
763 |
763 While Isar is inherently block-structured, opening and closing blocks is |
764 While Isar is inherently block-structured, opening and closing blocks is |
784 \item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof, |
785 \item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof, |
785 resetting the context to the initial one. |
786 resetting the context to the initial one. |
786 \item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and |
787 \item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and |
787 close blocks. Any current facts pass through $\isarkeyword{\{\{}$ |
788 close blocks. Any current facts pass through $\isarkeyword{\{\{}$ |
788 unchanged, while $\isarkeyword{\}\}}$ causes them to be \emph{exported} into |
789 unchanged, while $\isarkeyword{\}\}}$ causes them to be \emph{exported} into |
789 the enclosing context. Thus fixed variables are generalised, assumptions |
790 the enclosing context. Thus fixed variables are generalized, assumptions |
790 discharged, and local definitions eliminated. |
791 discharged, and local definitions eliminated. There is no difference of |
|
792 $\ASSUMENAME$ and $\PRESUMENAME$ here. |
791 \end{descr} |
793 \end{descr} |
792 |
794 |
793 |
795 |
794 \section{Other commands} |
796 \section{Other commands} |
795 |
|
796 The following commands are not part of the actual proper or improper |
|
797 Isabelle/Isar syntax, but assist interactive development, for example. Also |
|
798 note that $undo$ does not apply here, since the theory or proof configuration |
|
799 is not changed. |
|
800 |
797 |
801 \subsection{Diagnostics} |
798 \subsection{Diagnostics} |
802 |
799 |
803 \indexisarcmd{typ}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{thm} |
800 \indexisarcmd{typ}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{thm} |
804 \begin{matharray}{rcl} |
801 \begin{matharray}{rcl} |
805 \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\ |
802 \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\ |
806 \isarcmd{term} & : & \isarkeep{theory~|~proof} \\ |
803 \isarcmd{term} & : & \isarkeep{theory~|~proof} \\ |
807 \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\ |
804 \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\ |
808 \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\ |
805 \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\ |
809 \end{matharray} |
806 \end{matharray} |
|
807 |
|
808 These commands are not part of the actual Isabelle/Isar syntax, but assist |
|
809 interactive development. Also note that $undo$ does not apply here, since the |
|
810 theory or proof configuration is not changed. |
810 |
811 |
811 \begin{rail} |
812 \begin{rail} |
812 'typ' type |
813 'typ' type |
813 ; |
814 ; |
814 'term' term |
815 'term' term |
824 $\isarkeyword{prop}~\phi$] read and print types / terms / propositions |
825 $\isarkeyword{prop}~\phi$] read and print types / terms / propositions |
825 according to the current theory or proof context. |
826 according to the current theory or proof context. |
826 \item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current |
827 \item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current |
827 theory or proof context. Note that any attributes included in the theorem |
828 theory or proof context. Note that any attributes included in the theorem |
828 specifications are applied to a temporary context derived from the current |
829 specifications are applied to a temporary context derived from the current |
829 theory or proof; the result is discarded. |
830 theory or proof; the result is discarded, i.e.\ attributes involved in |
|
831 $thms$ only have a temporary effect. |
830 \end{descr} |
832 \end{descr} |
831 |
833 |
832 |
834 |
833 \subsection{System operations} |
835 \subsection{System operations} |
834 |
836 |
848 process. |
850 process. |
849 \item [$\isarkeyword{pwd}~$] prints the current working directory. |
851 \item [$\isarkeyword{pwd}~$] prints the current working directory. |
850 \item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$, |
852 \item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$, |
851 $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some |
853 $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some |
852 theory given as $name$ argument. These commands are exactly the same as the |
854 theory given as $name$ argument. These commands are exactly the same as the |
853 corresponding ML functions (see also \cite[\S1 and \S6]{isabelle-ref}). |
855 corresponding ML functions (see also \cite[\S1,\S6]{isabelle-ref}). Note |
854 Note that both the ML and Isar versions of these commands may load new- and |
856 that both the ML and Isar versions of these commands may load new- and |
855 old-style theories alike. |
857 old-style theories alike. |
856 \end{descr} |
858 \end{descr} |
|
859 |
|
860 Note that these system commands are scarcely used when working with |
|
861 Proof~General, since loading of theories is done fully automatic. |
857 |
862 |
858 |
863 |
859 %%% Local Variables: |
864 %%% Local Variables: |
860 %%% mode: latex |
865 %%% mode: latex |
861 %%% TeX-master: "isar-ref" |
866 %%% TeX-master: "isar-ref" |