author | wenzelm |
Wed, 10 Feb 2016 10:53:30 +0100 | |
changeset 62276 | bed456ada96e |
parent 62275 | 374d1b6c473d |
child 62277 | c9b1897d4173 |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
2 |
||
29716 | 3 |
theory Framework |
42651 | 4 |
imports Base Main |
29716 | 5 |
begin |
6 |
||
58618 | 7 |
chapter \<open>The Isabelle/Isar Framework \label{ch:isar-framework}\<close> |
29716 | 8 |
|
58618 | 9 |
text \<open> |
58552 | 10 |
Isabelle/Isar @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD" and |
62276 | 11 |
"Nipkow-TYPES02" and "Wiedijk:1999:Mizar" and "Wenzel-Paulson:2006" and |
12 |
"Wenzel:2006:Festschrift"} is a generic framework for developing formal |
|
13 |
mathematical documents with full proof checking. Definitions, statements and |
|
14 |
proofs are organized as theories. A collection of theories sources may be |
|
15 |
presented as a printed document; see also \chref{ch:document-prep}. |
|
29716 | 16 |
|
62276 | 17 |
The main concern of Isar is the design of a human-readable structured proof |
18 |
language, which is called the ``primary proof format'' in Isar terminology. |
|
19 |
Such a primary proof language is somewhere in the middle between the |
|
20 |
extremes of primitive proof objects and actual natural language. |
|
29716 | 21 |
|
62276 | 22 |
Thus Isar challenges the traditional way of recording informal proofs in |
62275 | 23 |
mathematical prose, as well as the common tendency to see fully formal |
24 |
proofs directly as objects of some logical calculus (e.g.\ \<open>\<lambda>\<close>-terms in a |
|
62276 | 25 |
version of type theory). Technically, Isar is an interpreter of a simple |
26 |
block-structured language for describing the data flow of local facts and |
|
27 |
goals, interspersed with occasional invocations of proof methods. Everything |
|
28 |
is reduced to logical inferences internally, but these steps are somewhat |
|
29 |
marginal compared to the overall bookkeeping of the interpretation process. |
|
30 |
Thanks to careful design of the syntax and semantics of Isar language |
|
31 |
elements, a formal record of Isar commands may later appear as an |
|
32 |
intelligible text to the human reader. |
|
29716 | 33 |
|
62275 | 34 |
The Isar proof language has emerged from careful analysis of some inherent |
62276 | 35 |
virtues of the logical framework Isabelle/Pure @{cite "paulson-found" and |
36 |
"paulson700"}, notably composition of higher-order natural deduction rules, |
|
37 |
which is a generalization of Gentzen's original calculus @{cite |
|
38 |
"Gentzen:1935"}. The approach of generic inference systems in Pure is |
|
39 |
continued by Isar towards actual proof texts. See also |
|
40 |
\figref{fig:natural-deduction} |
|
41 |
||
42 |
\begin{figure}[htb] |
|
43 |
||
44 |
\begin{center} |
|
45 |
\begin{minipage}[t]{0.9\textwidth} |
|
46 |
||
47 |
\textbf{Inferences:} |
|
48 |
\begin{center} |
|
49 |
\begin{tabular}{l@ {\qquad}l} |
|
50 |
\infer{\<open>B\<close>}{\<open>A \<longrightarrow> B\<close> & \<open>A\<close>} & |
|
51 |
\infer{\<open>A \<longrightarrow> B\<close>}{\infer*{\<open>B\<close>}{\<open>[A]\<close>}} \\ |
|
52 |
\end{tabular} |
|
53 |
\end{center} |
|
29716 | 54 |
|
62276 | 55 |
\textbf{Isabelle/Pure:} |
56 |
\begin{center} |
|
57 |
\begin{tabular}{l@ {\qquad}l} |
|
58 |
\<open>(A \<longrightarrow> B) \<Longrightarrow> A \<Longrightarrow> B\<close> & |
|
59 |
\<open>(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B\<close> |
|
60 |
\end{tabular} |
|
61 |
\end{center} |
|
62 |
||
63 |
\textbf{Isabelle/Isar:} |
|
64 |
\begin{center} |
|
65 |
\begin{minipage}[t]{0.4\textwidth} |
|
66 |
@{theory_text [display, indent = 2] |
|
67 |
\<open>have "A \<longrightarrow> B" \<proof> |
|
68 |
also have A \<proof> |
|
69 |
finally have B .\<close>} |
|
70 |
\end{minipage} |
|
71 |
\begin{minipage}[t]{0.4\textwidth} |
|
72 |
@{theory_text [display, indent = 2] |
|
73 |
\<open>have "A \<longrightarrow> B" |
|
74 |
proof |
|
75 |
assume A |
|
76 |
then show B \<proof> |
|
77 |
qed\<close>} |
|
78 |
\end{minipage} |
|
79 |
\end{center} |
|
80 |
||
81 |
\end{minipage} |
|
82 |
\end{center} |
|
83 |
||
84 |
\caption{Natural Deduction via inferences according to Gentzen, rules in |
|
85 |
Isabelle/Pure, and proofs in Isabelle/Isar}\label{fig:natural-deduction} |
|
86 |
||
87 |
\end{figure} |
|
29721 | 88 |
|
61421 | 89 |
\<^medskip> |
62276 | 90 |
Concrete applications require another intermediate layer: an object-logic. |
91 |
Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is most |
|
92 |
commonly used; elementary examples are given in the directory @{file |
|
93 |
"~~/src/HOL/Isar_Examples"}. Some examples demonstrate how to start a fresh |
|
94 |
object-logic from Isabelle/Pure, and use Isar proofs from the very start, |
|
95 |
despite the lack of advanced proof tools at such an early stage (e.g.\ see |
|
96 |
@{file "~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy"}). Isabelle/FOL |
|
97 |
@{cite "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, |
|
98 |
but are much less developed. |
|
99 |
||
100 |
In order to illustrate natural deduction in Isar, we shall subsequently |
|
101 |
refer to the background theory and library of Isabelle/HOL. This includes |
|
102 |
common notions of predicate logic, naive set-theory etc.\ using fairly |
|
103 |
standard mathematical notation. From the perspective of generic natural |
|
104 |
deduction there is nothing special about the logical connectives of HOL |
|
105 |
(\<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<forall>\<close>, \<open>\<exists>\<close>, etc.), only the resulting reasoning principles are |
|
106 |
relevant to the user. There are similar rules available for set-theory |
|
107 |
operators (\<open>\<inter>\<close>, \<open>\<union>\<close>, \<open>\<Inter>\<close>, \<open>\<Union>\<close>, etc.), or any other theory developed in the |
|
108 |
library (lattice theory, topology etc.). |
|
29721 | 109 |
|
62275 | 110 |
Subsequently we briefly review fragments of Isar proof texts corresponding |
111 |
directly to such general deduction schemes. The examples shall refer to |
|
112 |
set-theory, to minimize the danger of understanding connectives of predicate |
|
113 |
logic as something special. |
|
29721 | 114 |
|
61421 | 115 |
\<^medskip> |
62275 | 116 |
The following deduction performs \<open>\<inter>\<close>-introduction, working forwards from |
117 |
assumptions towards the conclusion. We give both the Isar text, and depict |
|
62276 | 118 |
the primitive rule involved, as determined by unification of fact and goal |
119 |
statements against rules that are declared in the library context. |
|
58618 | 120 |
\<close> |
29721 | 121 |
|
58618 | 122 |
text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close> |
29721 | 123 |
|
124 |
(*<*) |
|
40964 | 125 |
notepad |
126 |
begin |
|
62276 | 127 |
fix x :: 'a and A B |
29721 | 128 |
(*>*) |
129 |
assume "x \<in> A" and "x \<in> B" |
|
130 |
then have "x \<in> A \<inter> B" .. |
|
131 |
(*<*) |
|
40964 | 132 |
end |
29721 | 133 |
(*>*) |
134 |
||
58618 | 135 |
text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close> |
29721 | 136 |
|
58618 | 137 |
text \<open> |
62276 | 138 |
\infer{\<open>x \<in> A \<inter> B\<close>}{\<open>x \<in> A\<close> & \<open>x \<in> B\<close>} |
58618 | 139 |
\<close> |
29721 | 140 |
|
58618 | 141 |
text_raw \<open>\end{minipage}\<close> |
29721 | 142 |
|
58618 | 143 |
text \<open> |
61421 | 144 |
\<^medskip> |
62276 | 145 |
Note that \<^theory_text>\<open>assume\<close> augments the proof context, \<^theory_text>\<open>then\<close> indicates that the |
146 |
current fact shall be used in the next step, and \<^theory_text>\<open>have\<close> states an |
|
147 |
intermediate goal. The two dots ``\<^theory_text>\<open>..\<close>'' refer to a complete proof of this |
|
148 |
claim, using the indicated facts and a canonical rule from the context. We |
|
149 |
could have been more explicit here by spelling out the final proof step via |
|
150 |
the \<^theory_text>\<open>by\<close> command: |
|
58618 | 151 |
\<close> |
29721 | 152 |
|
153 |
(*<*) |
|
40964 | 154 |
notepad |
155 |
begin |
|
62276 | 156 |
fix x :: 'a and A B |
29721 | 157 |
(*>*) |
158 |
assume "x \<in> A" and "x \<in> B" |
|
159 |
then have "x \<in> A \<inter> B" by (rule IntI) |
|
160 |
(*<*) |
|
40964 | 161 |
end |
29721 | 162 |
(*>*) |
163 |
||
58618 | 164 |
text \<open> |
62275 | 165 |
The format of the \<open>\<inter>\<close>-introduction rule represents the most basic inference, |
166 |
which proceeds from given premises to a conclusion, without any nested proof |
|
167 |
context involved. |
|
29721 | 168 |
|
62276 | 169 |
The next example performs backwards introduction of \<open>\<Inter>\<A>\<close>, the intersection |
170 |
of all sets within a given set. This requires a nested proof of set |
|
171 |
membership within a local context, where \<open>A\<close> is an arbitrary-but-fixed |
|
172 |
member of the collection: |
|
58618 | 173 |
\<close> |
29721 | 174 |
|
58618 | 175 |
text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close> |
29721 | 176 |
|
177 |
(*<*) |
|
40964 | 178 |
notepad |
179 |
begin |
|
62276 | 180 |
fix x :: 'a and \<A> |
29721 | 181 |
(*>*) |
182 |
have "x \<in> \<Inter>\<A>" |
|
183 |
proof |
|
184 |
fix A |
|
185 |
assume "A \<in> \<A>" |
|
62271 | 186 |
show "x \<in> A" \<proof> |
29721 | 187 |
qed |
188 |
(*<*) |
|
40964 | 189 |
end |
29721 | 190 |
(*>*) |
191 |
||
58618 | 192 |
text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close> |
29721 | 193 |
|
58618 | 194 |
text \<open> |
62276 | 195 |
\infer{\<open>x \<in> \<Inter>\<A>\<close>}{\infer*{\<open>x \<in> A\<close>}{\<open>[A][A \<in> \<A>]\<close>}} |
58618 | 196 |
\<close> |
29721 | 197 |
|
58618 | 198 |
text_raw \<open>\end{minipage}\<close> |
29721 | 199 |
|
58618 | 200 |
text \<open> |
61421 | 201 |
\<^medskip> |
62275 | 202 |
This Isar reasoning pattern again refers to the primitive rule depicted |
62276 | 203 |
above. The system determines it in the ``\<^theory_text>\<open>proof\<close>'' step, which could have |
204 |
been spelled out more explicitly as ``\<^theory_text>\<open>proof (rule InterI)\<close>''. Note that |
|
205 |
the rule involves both a local parameter \<open>A\<close> and an assumption \<open>A \<in> \<A>\<close> in |
|
206 |
the nested reasoning. Such compound rules typically demands a genuine |
|
207 |
sub-proof in Isar, working backwards rather than forwards as seen before. In |
|
208 |
the proof body we encounter the \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close> outline of nested |
|
209 |
sub-proofs that is typical for Isar. The final \<^theory_text>\<open>show\<close> is like \<^theory_text>\<open>have\<close> |
|
210 |
followed by an additional refinement of the enclosing claim, using the rule |
|
211 |
derived from the proof body. |
|
29721 | 212 |
|
61421 | 213 |
\<^medskip> |
62276 | 214 |
The next example involves \<open>\<Union>\<A>\<close>, which can be characterized as the set of |
215 |
all \<open>x\<close> such that \<open>\<exists>A. x \<in> A \<and> A \<in> \<A>\<close>. The elimination rule for \<open>x \<in> \<Union>\<A>\<close> |
|
216 |
does not mention \<open>\<exists>\<close> and \<open>\<and>\<close> at all, but admits to obtain directly a local |
|
217 |
\<open>A\<close> such that \<open>x \<in> A\<close> and \<open>A \<in> \<A>\<close> hold. This corresponds to the following |
|
218 |
Isar proof and inference rule, respectively: |
|
58618 | 219 |
\<close> |
29721 | 220 |
|
58618 | 221 |
text_raw \<open>\medskip\begin{minipage}{0.6\textwidth}\<close> |
29721 | 222 |
|
223 |
(*<*) |
|
40964 | 224 |
notepad |
225 |
begin |
|
62276 | 226 |
fix x :: 'a and \<A> C |
29721 | 227 |
(*>*) |
228 |
assume "x \<in> \<Union>\<A>" |
|
229 |
then have C |
|
230 |
proof |
|
231 |
fix A |
|
232 |
assume "x \<in> A" and "A \<in> \<A>" |
|
62271 | 233 |
show C \<proof> |
29721 | 234 |
qed |
235 |
(*<*) |
|
40964 | 236 |
end |
29721 | 237 |
(*>*) |
238 |
||
58618 | 239 |
text_raw \<open>\end{minipage}\begin{minipage}{0.4\textwidth}\<close> |
29721 | 240 |
|
58618 | 241 |
text \<open> |
62276 | 242 |
\infer{\<open>C\<close>}{\<open>x \<in> \<Union>\<A>\<close> & \infer*{\<open>C\<close>~}{\<open>[A][x \<in> A, A \<in> \<A>]\<close>}} |
58618 | 243 |
\<close> |
29721 | 244 |
|
58618 | 245 |
text_raw \<open>\end{minipage}\<close> |
29721 | 246 |
|
58618 | 247 |
text \<open> |
61421 | 248 |
\<^medskip> |
62275 | 249 |
Although the Isar proof follows the natural deduction rule closely, the text |
250 |
reads not as natural as anticipated. There is a double occurrence of an |
|
62276 | 251 |
arbitrary conclusion \<open>C\<close>, which represents the final result, but is |
62275 | 252 |
irrelevant for now. This issue arises for any elimination rule involving |
62276 | 253 |
local parameters. Isar provides the derived language element \<^theory_text>\<open>obtain\<close>, |
254 |
which is able to perform the same elimination proof more conveniently: |
|
58618 | 255 |
\<close> |
29721 | 256 |
|
257 |
(*<*) |
|
40964 | 258 |
notepad |
259 |
begin |
|
62276 | 260 |
fix x :: 'a and \<A> |
29721 | 261 |
(*>*) |
262 |
assume "x \<in> \<Union>\<A>" |
|
263 |
then obtain A where "x \<in> A" and "A \<in> \<A>" .. |
|
264 |
(*<*) |
|
40964 | 265 |
end |
29721 | 266 |
(*>*) |
267 |
||
58618 | 268 |
text \<open> |
62276 | 269 |
Here we avoid to mention the final conclusion \<open>C\<close> and return to plain |
270 |
forward reasoning. The rule involved in the ``\<^theory_text>\<open>..\<close>'' proof is the same as |
|
271 |
before. |
|
58618 | 272 |
\<close> |
29716 | 273 |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
274 |
|
58618 | 275 |
section \<open>The Pure framework \label{sec:framework-pure}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
276 |
|
58618 | 277 |
text \<open> |
58552 | 278 |
The Pure logic @{cite "paulson-found" and "paulson700"} is an intuitionistic |
62275 | 279 |
fragment of higher-order logic @{cite "church40"}. In type-theoretic |
280 |
parlance, there are three levels of \<open>\<lambda>\<close>-calculus with corresponding arrows |
|
281 |
\<open>\<Rightarrow>\<close>/\<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>: |
|
29735 | 282 |
|
61421 | 283 |
\<^medskip> |
29735 | 284 |
\begin{tabular}{ll} |
61493 | 285 |
\<open>\<alpha> \<Rightarrow> \<beta>\<close> & syntactic function space (terms depending on terms) \\ |
286 |
\<open>\<And>x. B(x)\<close> & universal quantification (proofs depending on terms) \\ |
|
287 |
\<open>A \<Longrightarrow> B\<close> & implication (proofs depending on proofs) \\ |
|
29735 | 288 |
\end{tabular} |
61421 | 289 |
\<^medskip> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
290 |
|
62275 | 291 |
Here only the types of syntactic terms, and the propositions of proof terms |
292 |
have been shown. The \<open>\<lambda>\<close>-structure of proofs can be recorded as an optional |
|
293 |
feature of the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"}, |
|
294 |
but the formal system can never depend on them due to \<^emph>\<open>proof irrelevance\<close>. |
|
29735 | 295 |
|
62275 | 296 |
On top of this most primitive layer of proofs, Pure implements a generic |
297 |
calculus for nested natural deduction rules, similar to @{cite |
|
298 |
"Schroeder-Heister:1984"}. Here object-logic inferences are internalized as |
|
299 |
formulae over \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close>. Combining such rule statements may involve |
|
300 |
higher-order unification @{cite "paulson-natural"}. |
|
58618 | 301 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
302 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
303 |
|
58618 | 304 |
subsection \<open>Primitive inferences\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
305 |
|
58618 | 306 |
text \<open> |
62275 | 307 |
Term syntax provides explicit notation for abstraction \<open>\<lambda>x :: \<alpha>. b(x)\<close> and |
308 |
application \<open>b a\<close>, while types are usually implicit thanks to |
|
309 |
type-inference; terms of type \<open>prop\<close> are called propositions. Logical |
|
310 |
statements are composed via \<open>\<And>x :: \<alpha>. B(x)\<close> and \<open>A \<Longrightarrow> B\<close>. Primitive reasoning |
|
311 |
operates on judgments of the form \<open>\<Gamma> \<turnstile> \<phi>\<close>, with standard introduction and |
|
312 |
elimination rules for \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> that refer to fixed parameters \<open>x\<^sub>1, \<dots>, |
|
313 |
x\<^sub>m\<close> and hypotheses \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> from the context \<open>\<Gamma>\<close>; the corresponding |
|
314 |
proof terms are left implicit. The subsequent inference rules define \<open>\<Gamma> \<turnstile> \<phi>\<close> |
|
62276 | 315 |
inductively, relative to a collection of axioms from the implicit background |
316 |
theory: |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
317 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
318 |
\[ |
62276 | 319 |
\infer{\<open>\<turnstile> A\<close>}{\<open>A\<close> \mbox{~is axiom}} |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
320 |
\qquad |
61493 | 321 |
\infer{\<open>A \<turnstile> A\<close>}{} |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
322 |
\] |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
323 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
324 |
\[ |
61493 | 325 |
\infer{\<open>\<Gamma> \<turnstile> \<And>x. B(x)\<close>}{\<open>\<Gamma> \<turnstile> B(x)\<close> & \<open>x \<notin> \<Gamma>\<close>} |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
326 |
\qquad |
61493 | 327 |
\infer{\<open>\<Gamma> \<turnstile> B(a)\<close>}{\<open>\<Gamma> \<turnstile> \<And>x. B(x)\<close>} |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
328 |
\] |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
329 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
330 |
\[ |
61493 | 331 |
\infer{\<open>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<Gamma> \<turnstile> B\<close>} |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
332 |
\qquad |
61493 | 333 |
\infer{\<open>\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B\<close>}{\<open>\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B\<close> & \<open>\<Gamma>\<^sub>2 \<turnstile> A\<close>} |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
334 |
\] |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
335 |
|
62275 | 336 |
Furthermore, Pure provides a built-in equality \<open>\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop\<close> with |
337 |
axioms for reflexivity, substitution, extensionality, and \<open>\<alpha>\<beta>\<eta>\<close>-conversion |
|
338 |
on \<open>\<lambda>\<close>-terms. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
339 |
|
61421 | 340 |
\<^medskip> |
62276 | 341 |
|
62275 | 342 |
An object-logic introduces another layer on top of Pure, e.g.\ with types |
343 |
\<open>i\<close> for individuals and \<open>o\<close> for propositions, term constants \<open>Trueprop :: o |
|
344 |
\<Rightarrow> prop\<close> as (implicit) derivability judgment and connectives like \<open>\<and> :: o \<Rightarrow> o |
|
345 |
\<Rightarrow> o\<close> or \<open>\<forall> :: (i \<Rightarrow> o) \<Rightarrow> o\<close>, and axioms for object-level rules such as |
|
346 |
\<open>conjI: A \<Longrightarrow> B \<Longrightarrow> A \<and> B\<close> or \<open>allI: (\<And>x. B x) \<Longrightarrow> \<forall>x. B x\<close>. Derived object rules |
|
347 |
are represented as theorems of Pure. After the initial object-logic setup, |
|
62276 | 348 |
further axiomatizations are usually avoided: definitional principles are |
349 |
used instead (e.g.\ \<^theory_text>\<open>definition\<close>, \<^theory_text>\<open>inductive\<close>, \<^theory_text>\<open>fun\<close>, \<^theory_text>\<open>function\<close>). |
|
58618 | 350 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
351 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
352 |
|
58618 | 353 |
subsection \<open>Reasoning with rules \label{sec:framework-resolution}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
354 |
|
58618 | 355 |
text \<open> |
62275 | 356 |
Primitive inferences mostly serve foundational purposes. The main reasoning |
357 |
mechanisms of Pure operate on nested natural deduction rules expressed as |
|
358 |
formulae, using \<open>\<And>\<close> to bind local parameters and \<open>\<Longrightarrow>\<close> to express entailment. |
|
359 |
Multiple parameters and premises are represented by repeating these |
|
29735 | 360 |
connectives in a right-associative manner. |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
361 |
|
62276 | 362 |
Thanks to the Pure theorem @{prop "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"} the |
363 |
connectives \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> commute. So we may assume w.l.o.g.\ that rule |
|
364 |
statements always observe the normal form where quantifiers are pulled in |
|
365 |
front of implications at each level of nesting. This means that any Pure |
|
366 |
proposition may be presented as a \<^emph>\<open>Hereditary Harrop Formula\<close> @{cite |
|
367 |
"Miller:1991"} which is of the form \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. H\<^sub>1 \<Longrightarrow> \<dots> H\<^sub>n \<Longrightarrow> A\<close> for \<open>m, n |
|
368 |
\<ge> 0\<close>, and \<open>A\<close> atomic, and \<open>H\<^sub>1, \<dots>, H\<^sub>n\<close> being recursively of the same |
|
369 |
format. Following the convention that outermost quantifiers are implicit, |
|
370 |
Horn clauses \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A\<close> are a special case of this. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
371 |
|
62276 | 372 |
For example, the \<open>\<inter>\<close>-introduction rule encountered before is represented as |
373 |
a Pure theorem as follows: |
|
29735 | 374 |
\[ |
61493 | 375 |
\<open>IntI:\<close>~@{prop "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B"} |
29735 | 376 |
\] |
377 |
||
62275 | 378 |
This is a plain Horn clause, since no further nesting on the left is |
379 |
involved. The general \<open>\<Inter>\<close>-introduction corresponds to a Hereditary Harrop |
|
380 |
Formula with one additional level of nesting: |
|
29735 | 381 |
\[ |
61493 | 382 |
\<open>InterI:\<close>~@{prop "(\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A) \<Longrightarrow> x \<in> \<Inter>\<A>"} |
29735 | 383 |
\] |
384 |
||
61421 | 385 |
\<^medskip> |
62275 | 386 |
Goals are also represented as rules: \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C\<close> states that the |
387 |
sub-goals \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> entail the result \<open>C\<close>; for \<open>n = 0\<close> the goal is |
|
62276 | 388 |
finished. To allow \<open>C\<close> being a rule statement itself, there is an internal |
62275 | 389 |
protective marker \<open># :: prop \<Rightarrow> prop\<close>, which is defined as identity and |
390 |
hidden from the user. We initialize and finish goal states as follows: |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
391 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
392 |
\[ |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
393 |
\begin{array}{c@ {\qquad}c} |
61493 | 394 |
\infer[(@{inference_def init})]{\<open>C \<Longrightarrow> #C\<close>}{} & |
395 |
\infer[(@{inference_def finish})]{\<open>C\<close>}{\<open>#C\<close>} |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
396 |
\end{array} |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
397 |
\] |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
398 |
|
62275 | 399 |
Goal states are refined in intermediate proof steps until a finished form is |
400 |
achieved. Here the two main reasoning principles are @{inference |
|
401 |
resolution}, for back-chaining a rule against a sub-goal (replacing it by |
|
402 |
zero or more sub-goals), and @{inference assumption}, for solving a sub-goal |
|
403 |
(finding a short-circuit with local assumptions). Below \<open>\<^vec>x\<close> stands |
|
62276 | 404 |
for \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> (for \<open>n \<ge> 0\<close>). |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
405 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
406 |
\[ |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
407 |
\infer[(@{inference_def resolution})] |
61493 | 408 |
{\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>\<close>} |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
409 |
{\begin{tabular}{rl} |
61493 | 410 |
\<open>rule:\<close> & |
411 |
\<open>\<^vec>A \<^vec>a \<Longrightarrow> B \<^vec>a\<close> \\ |
|
412 |
\<open>goal:\<close> & |
|
413 |
\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C\<close> \\ |
|
414 |
\<open>goal unifier:\<close> & |
|
415 |
\<open>(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
416 |
\end{tabular}} |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
417 |
\] |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
418 |
|
61421 | 419 |
\<^medskip> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
420 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
421 |
\[ |
61493 | 422 |
\infer[(@{inference_def assumption})]{\<open>C\<vartheta>\<close>} |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
423 |
{\begin{tabular}{rl} |
61493 | 424 |
\<open>goal:\<close> & |
425 |
\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C\<close> \\ |
|
62276 | 426 |
\<open>assm unifier:\<close> & \<open>A\<vartheta> = H\<^sub>i\<vartheta>\<close>~~\mbox{for some~\<open>H\<^sub>i\<close>} \\ |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
427 |
\end{tabular}} |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
428 |
\] |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
429 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
430 |
The following trace illustrates goal-oriented reasoning in |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
431 |
Isabelle/Pure: |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
432 |
|
29735 | 433 |
{\footnotesize |
61421 | 434 |
\<^medskip> |
29735 | 435 |
\begin{tabular}{r@ {\quad}l} |
61493 | 436 |
\<open>(A \<and> B \<Longrightarrow> B \<and> A) \<Longrightarrow> #(A \<and> B \<Longrightarrow> B \<and> A)\<close> & \<open>(init)\<close> \\ |
437 |
\<open>(A \<and> B \<Longrightarrow> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>\<close> & \<open>(resolution B \<Longrightarrow> A \<Longrightarrow> B \<and> A)\<close> \\ |
|
438 |
\<open>(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> (A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>\<close> & \<open>(resolution A \<and> B \<Longrightarrow> B)\<close> \\ |
|
439 |
\<open>(A \<and> B \<Longrightarrow> A) \<Longrightarrow> #\<dots>\<close> & \<open>(assumption)\<close> \\ |
|
440 |
\<open>(A \<and> B \<Longrightarrow> A \<and> B) \<Longrightarrow> #\<dots>\<close> & \<open>(resolution A \<and> B \<Longrightarrow> A)\<close> \\ |
|
441 |
\<open>#\<dots>\<close> & \<open>(assumption)\<close> \\ |
|
442 |
\<open>A \<and> B \<Longrightarrow> B \<and> A\<close> & \<open>(finish)\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
443 |
\end{tabular} |
61421 | 444 |
\<^medskip> |
29735 | 445 |
} |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
446 |
|
62275 | 447 |
Compositions of @{inference assumption} after @{inference resolution} occurs |
448 |
quite often, typically in elimination steps. Traditional Isabelle tactics |
|
449 |
accommodate this by a combined @{inference_def elim_resolution} principle. |
|
450 |
In contrast, Isar uses a slightly more refined combination, where the |
|
451 |
assumptions to be closed are marked explicitly, using again the protective |
|
452 |
marker \<open>#\<close>: |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
453 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
454 |
\[ |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
455 |
\infer[(@{inference refinement})] |
61493 | 456 |
{\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>G' (\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>\<close>} |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
457 |
{\begin{tabular}{rl} |
61493 | 458 |
\<open>sub\<hyphen>proof:\<close> & |
459 |
\<open>\<^vec>G \<^vec>a \<Longrightarrow> B \<^vec>a\<close> \\ |
|
460 |
\<open>goal:\<close> & |
|
461 |
\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C\<close> \\ |
|
462 |
\<open>goal unifier:\<close> & |
|
463 |
\<open>(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>\<close> \\ |
|
464 |
\<open>assm unifiers:\<close> & |
|
465 |
\<open>(\<lambda>\<^vec>x. G\<^sub>j (\<^vec>a \<^vec>x))\<vartheta> = #H\<^sub>i\<vartheta>\<close> \\ |
|
466 |
& \quad (for each marked \<open>G\<^sub>j\<close> some \<open>#H\<^sub>i\<close>) \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
467 |
\end{tabular}} |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
468 |
\] |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
469 |
|
62276 | 470 |
Here the \<open>sub\<hyphen>proof\<close> rule stems from the main \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close> |
471 |
outline of Isar (cf.\ \secref{sec:framework-subproof}): each assumption |
|
472 |
indicated in the text results in a marked premise \<open>G\<close> above. The marking |
|
473 |
enforces resolution against one of the sub-goal's premises. Consequently, |
|
474 |
\<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close> enables to fit the result of a sub-proof quite |
|
475 |
robustly into a pending sub-goal, while maintaining a good measure of |
|
476 |
flexibility. |
|
58618 | 477 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
478 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
479 |
|
58618 | 480 |
section \<open>The Isar proof language \label{sec:framework-isar}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
481 |
|
58618 | 482 |
text \<open> |
62275 | 483 |
Structured proofs are presented as high-level expressions for composing |
484 |
entities of Pure (propositions, facts, and goals). The Isar proof language |
|
485 |
allows to organize reasoning within the underlying rule calculus of Pure, |
|
486 |
but Isar is not another logical calculus! |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
487 |
|
62275 | 488 |
Isar is an exercise in sound minimalism. Approximately half of the language |
489 |
is introduced as primitive, the rest defined as derived concepts. The |
|
490 |
following grammar describes the core language (category \<open>proof\<close>), which is |
|
62276 | 491 |
embedded into theory specification elements such as \<^theory_text>\<open>theorem\<close>; see also |
492 |
\secref{sec:framework-stmt} for the separate category \<open>statement\<close>. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
493 |
|
61421 | 494 |
\<^medskip> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
495 |
\begin{tabular}{rcl} |
61493 | 496 |
\<open>theory\<hyphen>stmt\<close> & = & @{command "theorem"}~\<open>statement proof |\<close>~~@{command "definition"}~\<open>\<dots> | \<dots>\<close> \\[1ex] |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
497 |
|
61493 | 498 |
\<open>proof\<close> & = & \<open>prfx\<^sup>*\<close>~@{command "proof"}~\<open>method\<^sup>? stmt\<^sup>*\<close>~@{command "qed"}~\<open>method\<^sup>?\<close> \\[1ex] |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
499 |
|
61493 | 500 |
\<open>prfx\<close> & = & @{command "using"}~\<open>facts\<close> \\ |
501 |
& \<open>|\<close> & @{command "unfolding"}~\<open>facts\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
502 |
|
61493 | 503 |
\<open>stmt\<close> & = & @{command "{"}~\<open>stmt\<^sup>*\<close>~@{command "}"} \\ |
504 |
& \<open>|\<close> & @{command "next"} \\ |
|
505 |
& \<open>|\<close> & @{command "note"}~\<open>name = facts\<close> \\ |
|
506 |
& \<open>|\<close> & @{command "let"}~\<open>term = term\<close> \\ |
|
507 |
& \<open>|\<close> & @{command "fix"}~\<open>var\<^sup>+\<close> \\ |
|
508 |
& \<open>|\<close> & @{command assume}~\<open>\<guillemotleft>inference\<guillemotright> name: props\<close> \\ |
|
509 |
& \<open>|\<close> & @{command "then"}\<open>\<^sup>?\<close>~\<open>goal\<close> \\ |
|
510 |
\<open>goal\<close> & = & @{command "have"}~\<open>name: props proof\<close> \\ |
|
511 |
& \<open>|\<close> & @{command "show"}~\<open>name: props proof\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
512 |
\end{tabular} |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
513 |
|
61421 | 514 |
\<^medskip> |
62275 | 515 |
Simultaneous propositions or facts may be separated by the @{keyword "and"} |
516 |
keyword. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
517 |
|
61421 | 518 |
\<^medskip> |
62275 | 519 |
The syntax for terms and propositions is inherited from Pure (and the |
520 |
object-logic). A \<open>pattern\<close> is a \<open>term\<close> with schematic variables, to be bound |
|
521 |
by higher-order matching. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
522 |
|
61421 | 523 |
\<^medskip> |
62275 | 524 |
Facts may be referenced by name or proposition. For example, the result of |
62276 | 525 |
``\<^theory_text>\<open>have a: A \<proof>\<close>'' becomes available both as \<open>a\<close> and |
62275 | 526 |
\isacharbackquoteopen\<open>A\<close>\isacharbackquoteclose. Moreover, fact expressions |
527 |
may involve attributes that modify either the theorem or the background |
|
528 |
context. For example, the expression ``\<open>a [OF b]\<close>'' refers to the |
|
529 |
composition of two facts according to the @{inference resolution} inference |
|
530 |
of \secref{sec:framework-resolution}, while ``\<open>a [intro]\<close>'' declares a fact |
|
531 |
as introduction rule in the context. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
532 |
|
62275 | 533 |
The special fact called ``@{fact this}'' always refers to the last result, |
534 |
as produced by @{command note}, @{command assume}, @{command have}, or |
|
535 |
@{command show}. Since @{command note} occurs frequently together with |
|
536 |
@{command then} we provide some abbreviations: |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
537 |
|
61421 | 538 |
\<^medskip> |
29737
866841668584
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
wenzelm
parents:
29735
diff
changeset
|
539 |
\begin{tabular}{rcl} |
61493 | 540 |
@{command from}~\<open>a\<close> & \<open>\<equiv>\<close> & @{command note}~\<open>a\<close>~@{command then} \\ |
541 |
@{command with}~\<open>a\<close> & \<open>\<equiv>\<close> & @{command from}~\<open>a \<AND> this\<close> \\ |
|
29737
866841668584
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
wenzelm
parents:
29735
diff
changeset
|
542 |
\end{tabular} |
61421 | 543 |
\<^medskip> |
29737
866841668584
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
wenzelm
parents:
29735
diff
changeset
|
544 |
|
62275 | 545 |
The \<open>method\<close> category is essentially a parameter and may be populated later. |
546 |
Methods use the facts indicated by @{command "then"} or @{command using}, |
|
547 |
and then operate on the goal state. Some basic methods are predefined: |
|
548 |
``@{method "-"}'' leaves the goal unchanged, ``@{method this}'' applies the |
|
549 |
facts as rules to the goal, ``@{method (Pure) "rule"}'' applies the facts to |
|
550 |
another rule and the result to the goal (both ``@{method this}'' and |
|
551 |
``@{method (Pure) rule}'' refer to @{inference resolution} of |
|
552 |
\secref{sec:framework-resolution}). The secondary arguments to ``@{method |
|
553 |
(Pure) rule}'' may be specified explicitly as in ``\<open>(rule a)\<close>'', or picked |
|
554 |
from the context. In the latter case, the system first tries rules declared |
|
555 |
as @{attribute (Pure) elim} or @{attribute (Pure) dest}, followed by those |
|
556 |
declared as @{attribute (Pure) intro}. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
557 |
|
62275 | 558 |
The default method for @{command proof} is ``@{method standard}'' (arguments |
559 |
picked from the context), for @{command qed} it is ``@{method "succeed"}''. |
|
560 |
Further abbreviations for terminal proof steps are ``@{command |
|
561 |
"by"}~\<open>method\<^sub>1 method\<^sub>2\<close>'' for ``@{command proof}~\<open>method\<^sub>1\<close>~@{command |
|
562 |
qed}~\<open>method\<^sub>2\<close>'', and ``@{command ".."}'' for ``@{command "by"}~@{method |
|
563 |
standard}, and ``@{command "."}'' for ``@{command "by"}~@{method this}''. |
|
564 |
The @{command unfolding} element operates directly on the current facts and |
|
565 |
goal by applying equalities. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
566 |
|
61421 | 567 |
\<^medskip> |
568 |
Block structure can be indicated explicitly by ``@{command |
|
62275 | 569 |
"{"}~\<open>\<dots>\<close>~@{command "}"}'', although the body of a sub-proof already involves |
570 |
implicit nesting. In any case, @{command next} jumps into the next section |
|
571 |
of a block, i.e.\ it acts like closing an implicit block scope and opening |
|
572 |
another one; there is no direct correspondence to subgoals here. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
573 |
|
62275 | 574 |
The remaining elements @{command fix} and @{command assume} build up a local |
575 |
context (see \secref{sec:framework-context}), while @{command show} refines |
|
576 |
a pending sub-goal by the rule resulting from a nested sub-proof (see |
|
577 |
\secref{sec:framework-subproof}). Further derived concepts will support |
|
578 |
calculational reasoning (see \secref{sec:framework-calc}). |
|
58618 | 579 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
580 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
581 |
|
58618 | 582 |
subsection \<open>Context elements \label{sec:framework-context}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
583 |
|
58618 | 584 |
text \<open> |
62275 | 585 |
In judgments \<open>\<Gamma> \<turnstile> \<phi>\<close> of the primitive framework, \<open>\<Gamma>\<close> essentially acts like a |
586 |
proof context. Isar elaborates this idea towards a higher-level notion, with |
|
587 |
additional information for type-inference, term abbreviations, local facts, |
|
588 |
hypotheses etc. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
589 |
|
62275 | 590 |
The element @{command fix}~\<open>x :: \<alpha>\<close> declares a local parameter, i.e.\ an |
591 |
arbitrary-but-fixed entity of a given type; in results exported from the |
|
592 |
context, \<open>x\<close> may become anything. The @{command assume}~\<open>\<guillemotleft>inference\<guillemotright>\<close> |
|
593 |
element provides a general interface to hypotheses: ``@{command |
|
594 |
assume}~\<open>\<guillemotleft>inference\<guillemotright> A\<close>'' produces \<open>A \<turnstile> A\<close> locally, while the included |
|
595 |
inference tells how to discharge \<open>A\<close> from results \<open>A \<turnstile> B\<close> later on. There is |
|
596 |
no user-syntax for \<open>\<guillemotleft>inference\<guillemotright>\<close>, i.e.\ it may only occur internally when |
|
597 |
derived commands are defined in ML. |
|
29737
866841668584
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
wenzelm
parents:
29735
diff
changeset
|
598 |
|
866841668584
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
wenzelm
parents:
29735
diff
changeset
|
599 |
At the user-level, the default inference for @{command assume} is |
62275 | 600 |
@{inference discharge} as given below. The additional variants @{command |
601 |
presume} and @{command def} are defined as follows: |
|
29737
866841668584
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
wenzelm
parents:
29735
diff
changeset
|
602 |
|
61421 | 603 |
\<^medskip> |
29737
866841668584
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
wenzelm
parents:
29735
diff
changeset
|
604 |
\begin{tabular}{rcl} |
61493 | 605 |
@{command presume}~\<open>A\<close> & \<open>\<equiv>\<close> & @{command assume}~\<open>\<guillemotleft>weak\<hyphen>discharge\<guillemotright> A\<close> \\ |
606 |
@{command def}~\<open>x \<equiv> a\<close> & \<open>\<equiv>\<close> & @{command fix}~\<open>x\<close>~@{command assume}~\<open>\<guillemotleft>expansion\<guillemotright> x \<equiv> a\<close> \\ |
|
29737
866841668584
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
wenzelm
parents:
29735
diff
changeset
|
607 |
\end{tabular} |
61421 | 608 |
\<^medskip> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
609 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
610 |
\[ |
61493 | 611 |
\infer[(@{inference_def discharge})]{\<open>\<strut>\<Gamma> - A \<turnstile> #A \<Longrightarrow> B\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B\<close>} |
29737
866841668584
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
wenzelm
parents:
29735
diff
changeset
|
612 |
\] |
866841668584
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
wenzelm
parents:
29735
diff
changeset
|
613 |
\[ |
61493 | 614 |
\infer[(@{inference_def "weak\<hyphen>discharge"})]{\<open>\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B\<close>} |
29737
866841668584
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
wenzelm
parents:
29735
diff
changeset
|
615 |
\] |
866841668584
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
wenzelm
parents:
29735
diff
changeset
|
616 |
\[ |
61493 | 617 |
\infer[(@{inference_def expansion})]{\<open>\<strut>\<Gamma> - (x \<equiv> a) \<turnstile> B a\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B x\<close>} |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
618 |
\] |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
619 |
|
61421 | 620 |
\<^medskip> |
62275 | 621 |
Note that @{inference discharge} and @{inference "weak\<hyphen>discharge"} differ in |
62276 | 622 |
the marker for \<open>A\<close>, which is relevant when the result of a @{command |
62275 | 623 |
fix}-@{command assume}-@{command show} outline is composed with a pending |
624 |
goal, cf.\ \secref{sec:framework-subproof}. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
625 |
|
62275 | 626 |
The most interesting derived context element in Isar is @{command obtain} |
627 |
@{cite \<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized elimination steps |
|
628 |
in a purely forward manner. The @{command obtain} command takes a |
|
629 |
specification of parameters \<open>\<^vec>x\<close> and assumptions \<open>\<^vec>A\<close> to be |
|
630 |
added to the context, together with a proof of a case rule stating that this |
|
631 |
extension is conservative (i.e.\ may be removed from closed results later |
|
632 |
on): |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
633 |
|
61421 | 634 |
\<^medskip> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
635 |
\begin{tabular}{l} |
62276 | 636 |
\<open>\<langle>facts\<rangle>\<close>~~@{command obtain}~\<open>\<^vec>x \<WHERE> \<^vec>A \<^vec>x \<proof> \<equiv>\<close> \\[0.5ex] |
61493 | 637 |
\quad @{command have}~\<open>case: \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<rangle>\<close> \\ |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
638 |
\quad @{command proof}~@{method "-"} \\ |
61493 | 639 |
\qquad @{command fix}~\<open>thesis\<close> \\ |
640 |
\qquad @{command assume}~\<open>[intro]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close> \\ |
|
62276 | 641 |
\qquad @{command show}~\<open>thesis\<close>~@{command using}~\<open>\<langle>facts\<rangle> \<proof>\<close> \\ |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
642 |
\quad @{command qed} \\ |
61493 | 643 |
\quad @{command fix}~\<open>\<^vec>x\<close>~@{command assume}~\<open>\<guillemotleft>elimination case\<guillemotright> \<^vec>A \<^vec>x\<close> \\ |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
644 |
\end{tabular} |
61421 | 645 |
\<^medskip> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
646 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
647 |
\[ |
61493 | 648 |
\infer[(@{inference elimination})]{\<open>\<Gamma> \<turnstile> B\<close>}{ |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
649 |
\begin{tabular}{rl} |
61493 | 650 |
\<open>case:\<close> & |
651 |
\<open>\<Gamma> \<turnstile> \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\[0.2ex] |
|
652 |
\<open>result:\<close> & |
|
653 |
\<open>\<Gamma> \<union> \<^vec>A \<^vec>y \<turnstile> B\<close> \\[0.2ex] |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
654 |
\end{tabular}} |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
655 |
\] |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
656 |
|
62275 | 657 |
Here the name ``\<open>thesis\<close>'' is a specific convention for an |
658 |
arbitrary-but-fixed proposition; in the primitive natural deduction rules |
|
659 |
shown before we have occasionally used \<open>C\<close>. The whole statement of |
|
660 |
``@{command obtain}~\<open>x\<close>~@{keyword "where"}~\<open>A x\<close>'' may be read as a claim |
|
661 |
that \<open>A x\<close> may be assumed for some arbitrary-but-fixed \<open>x\<close>. Also note that |
|
662 |
``@{command obtain}~\<open>A \<AND> B\<close>'' without parameters is similar to |
|
663 |
``@{command have}~\<open>A \<AND> B\<close>'', but the latter involves multiple |
|
664 |
sub-goals. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
665 |
|
61421 | 666 |
\<^medskip> |
62275 | 667 |
The subsequent Isar proof texts explain all context elements introduced |
668 |
above using the formal proof language itself. After finishing a local proof |
|
669 |
within a block, we indicate the exported result via @{command note}. |
|
58618 | 670 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
671 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
672 |
(*<*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
673 |
theorem True |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
674 |
proof |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
675 |
(*>*) |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
676 |
text_raw \<open>\begin{minipage}[t]{0.45\textwidth}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
677 |
{ |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
678 |
fix x |
62271 | 679 |
have "B x" \<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
680 |
} |
58618 | 681 |
note \<open>\<And>x. B x\<close> |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
682 |
text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*) |
29735 | 683 |
{ |
684 |
assume A |
|
62271 | 685 |
have B \<proof> |
29735 | 686 |
} |
58618 | 687 |
note \<open>A \<Longrightarrow> B\<close> |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
688 |
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*) |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
689 |
{ |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
690 |
def x \<equiv> a |
62271 | 691 |
have "B x" \<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
692 |
} |
58618 | 693 |
note \<open>B a\<close> |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
694 |
text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*) |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
695 |
{ |
62271 | 696 |
obtain x where "A x" \<proof> |
697 |
have B \<proof> |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
698 |
} |
58618 | 699 |
note \<open>B\<close> |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
700 |
text_raw \<open>\end{minipage}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
701 |
(*<*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
702 |
qed |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
703 |
(*>*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
704 |
|
58618 | 705 |
text \<open> |
61421 | 706 |
\<^bigskip> |
62275 | 707 |
This illustrates the meaning of Isar context elements without goals getting |
708 |
in between. |
|
58618 | 709 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
710 |
|
61421 | 711 |
|
58618 | 712 |
subsection \<open>Structured statements \label{sec:framework-stmt}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
713 |
|
58618 | 714 |
text \<open> |
61493 | 715 |
The category \<open>statement\<close> of top-level theorem specifications |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
716 |
is defined as follows: |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
717 |
|
61421 | 718 |
\<^medskip> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
719 |
\begin{tabular}{rcl} |
61493 | 720 |
\<open>statement\<close> & \<open>\<equiv>\<close> & \<open>name: props \<AND> \<dots>\<close> \\ |
721 |
& \<open>|\<close> & \<open>context\<^sup>* conclusion\<close> \\[0.5ex] |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
722 |
|
61493 | 723 |
\<open>context\<close> & \<open>\<equiv>\<close> & \<open>\<FIXES> vars \<AND> \<dots>\<close> \\ |
724 |
& \<open>|\<close> & \<open>\<ASSUMES> name: props \<AND> \<dots>\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
725 |
|
61493 | 726 |
\<open>conclusion\<close> & \<open>\<equiv>\<close> & \<open>\<SHOWS> name: props \<AND> \<dots>\<close> \\ |
727 |
& \<open>|\<close> & \<open>\<OBTAINS> vars \<AND> \<dots> \<WHERE> name: props \<AND> \<dots>\<close> \\ |
|
728 |
& & \quad \<open>\<BBAR> \<dots>\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
729 |
\end{tabular} |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
730 |
|
61421 | 731 |
\<^medskip> |
62275 | 732 |
A simple \<open>statement\<close> consists of named propositions. The full form admits |
733 |
local context elements followed by the actual conclusions, such as |
|
734 |
``@{keyword "fixes"}~\<open>x\<close>~@{keyword "assumes"}~\<open>A x\<close>~@{keyword "shows"}~\<open>B |
|
735 |
x\<close>''. The final result emerges as a Pure rule after discharging the context: |
|
736 |
@{prop "\<And>x. A x \<Longrightarrow> B x"}. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
737 |
|
62275 | 738 |
The @{keyword "obtains"} variant is another abbreviation defined below; |
739 |
unlike @{command obtain} (cf.\ \secref{sec:framework-context}) there may be |
|
740 |
several ``cases'' separated by ``\<open>\<BBAR>\<close>'', each consisting of several |
|
741 |
parameters (\<open>vars\<close>) and several premises (\<open>props\<close>). This specifies |
|
742 |
multi-branch elimination rules. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
743 |
|
61421 | 744 |
\<^medskip> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
745 |
\begin{tabular}{l} |
61493 | 746 |
\<open>\<OBTAINS> \<^vec>x \<WHERE> \<^vec>A \<^vec>x \<BBAR> \<dots> \<equiv>\<close> \\[0.5ex] |
747 |
\quad \<open>\<FIXES> thesis\<close> \\ |
|
748 |
\quad \<open>\<ASSUMES> [intro]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis \<AND> \<dots>\<close> \\ |
|
749 |
\quad \<open>\<SHOWS> thesis\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
750 |
\end{tabular} |
61421 | 751 |
\<^medskip> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
752 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
753 |
Presenting structured statements in such an ``open'' format usually |
62275 | 754 |
simplifies the subsequent proof, because the outer structure of the problem |
755 |
is already laid out directly. E.g.\ consider the following canonical |
|
756 |
patterns for \<open>\<SHOWS>\<close> and \<open>\<OBTAINS>\<close>, respectively: |
|
58618 | 757 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
758 |
|
58618 | 759 |
text_raw \<open>\begin{minipage}{0.5\textwidth}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
760 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
761 |
theorem |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
762 |
fixes x and y |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
763 |
assumes "A x" and "B y" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
764 |
shows "C x y" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
765 |
proof - |
58618 | 766 |
from \<open>A x\<close> and \<open>B y\<close> |
62271 | 767 |
show "C x y" \<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
768 |
qed |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
769 |
|
58618 | 770 |
text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
771 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
772 |
theorem |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
773 |
obtains x and y |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
774 |
where "A x" and "B y" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
775 |
proof - |
62271 | 776 |
have "A a" and "B b" \<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
777 |
then show thesis .. |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
778 |
qed |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
779 |
|
58618 | 780 |
text_raw \<open>\end{minipage}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
781 |
|
58618 | 782 |
text \<open> |
61421 | 783 |
\<^medskip> |
62275 | 784 |
Here local facts \isacharbackquoteopen\<open>A x\<close>\isacharbackquoteclose\ and |
785 |
\isacharbackquoteopen\<open>B y\<close>\isacharbackquoteclose\ are referenced |
|
786 |
immediately; there is no need to decompose the logical rule structure again. |
|
787 |
In the second proof the final ``@{command then}~@{command |
|
788 |
show}~\<open>thesis\<close>~@{command ".."}'' involves the local rule case \<open>\<And>x y. A x \<Longrightarrow> B |
|
789 |
y \<Longrightarrow> thesis\<close> for the particular instance of terms \<open>a\<close> and \<open>b\<close> produced in the |
|
790 |
body. \<close> |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
791 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
792 |
|
58618 | 793 |
subsection \<open>Structured proof refinement \label{sec:framework-subproof}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
794 |
|
58618 | 795 |
text \<open> |
62275 | 796 |
By breaking up the grammar for the Isar proof language, we may understand a |
797 |
proof text as a linear sequence of individual proof commands. These are |
|
798 |
interpreted as transitions of the Isar virtual machine (Isar/VM), which |
|
799 |
operates on a block-structured configuration in single steps. This allows |
|
800 |
users to write proof texts in an incremental manner, and inspect |
|
801 |
intermediate configurations for debugging. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
802 |
|
62275 | 803 |
The basic idea is analogous to evaluating algebraic expressions on a stack |
804 |
machine: \<open>(a + b) \<cdot> c\<close> then corresponds to a sequence of single transitions |
|
805 |
for each symbol \<open>(, a, +, b, ), \<cdot>, c\<close>. In Isar the algebraic values are |
|
806 |
facts or goals, and the operations are inferences. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
807 |
|
61421 | 808 |
\<^medskip> |
62275 | 809 |
The Isar/VM state maintains a stack of nodes, each node contains the local |
810 |
proof context, the linguistic mode, and a pending goal (optional). The mode |
|
811 |
determines the type of transition that may be performed next, it essentially |
|
812 |
alternates between forward and backward reasoning, with an intermediate |
|
813 |
stage for chained facts (see \figref{fig:isar-vm}). |
|
29738 | 814 |
|
815 |
\begin{figure}[htb] |
|
816 |
\begin{center} |
|
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48279
diff
changeset
|
817 |
\includegraphics[width=0.8\textwidth]{isar-vm} |
29738 | 818 |
\end{center} |
819 |
\caption{Isar/VM modes}\label{fig:isar-vm} |
|
820 |
\end{figure} |
|
821 |
||
62275 | 822 |
For example, in \<open>state\<close> mode Isar acts like a mathematical scratch-pad, |
823 |
accepting declarations like @{command fix}, @{command assume}, and claims |
|
824 |
like @{command have}, @{command show}. A goal statement changes the mode to |
|
825 |
\<open>prove\<close>, which means that we may now refine the problem via @{command |
|
826 |
unfolding} or @{command proof}. Then we are again in \<open>state\<close> mode of a proof |
|
827 |
body, which may issue @{command show} statements to solve pending sub-goals. |
|
828 |
A concluding @{command qed} will return to the original \<open>state\<close> mode one |
|
829 |
level upwards. The subsequent Isar/VM trace indicates block structure, |
|
830 |
linguistic mode, goal state, and inferences: |
|
58618 | 831 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
832 |
|
58618 | 833 |
text_raw \<open>\begingroup\footnotesize\<close> |
40964 | 834 |
(*<*)notepad begin |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
835 |
(*>*) |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
836 |
text_raw \<open>\begin{minipage}[t]{0.18\textwidth}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
837 |
have "A \<longrightarrow> B" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
838 |
proof |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
839 |
assume A |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
840 |
show B |
62271 | 841 |
\<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
842 |
qed |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
843 |
text_raw \<open>\end{minipage}\quad |
29735 | 844 |
\begin{minipage}[t]{0.06\textwidth} |
61493 | 845 |
\<open>begin\<close> \\ |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
846 |
\\ |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
847 |
\\ |
61493 | 848 |
\<open>begin\<close> \\ |
849 |
\<open>end\<close> \\ |
|
850 |
\<open>end\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
851 |
\end{minipage} |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
852 |
\begin{minipage}[t]{0.08\textwidth} |
61493 | 853 |
\<open>prove\<close> \\ |
854 |
\<open>state\<close> \\ |
|
855 |
\<open>state\<close> \\ |
|
856 |
\<open>prove\<close> \\ |
|
857 |
\<open>state\<close> \\ |
|
858 |
\<open>state\<close> \\ |
|
29735 | 859 |
\end{minipage}\begin{minipage}[t]{0.35\textwidth} |
61493 | 860 |
\<open>(A \<longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)\<close> \\ |
861 |
\<open>(A \<Longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
862 |
\\ |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
863 |
\\ |
61493 | 864 |
\<open>#(A \<longrightarrow> B)\<close> \\ |
865 |
\<open>A \<longrightarrow> B\<close> \\ |
|
29735 | 866 |
\end{minipage}\begin{minipage}[t]{0.4\textwidth} |
61493 | 867 |
\<open>(init)\<close> \\ |
868 |
\<open>(resolution impI)\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
869 |
\\ |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
870 |
\\ |
61493 | 871 |
\<open>(refinement #A \<Longrightarrow> B)\<close> \\ |
872 |
\<open>(finish)\<close> \\ |
|
58618 | 873 |
\end{minipage}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
874 |
(*<*) |
40964 | 875 |
end |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
876 |
(*>*) |
58618 | 877 |
text_raw \<open>\endgroup\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
878 |
|
58618 | 879 |
text \<open> |
61420 | 880 |
Here the @{inference refinement} inference from |
62275 | 881 |
\secref{sec:framework-resolution} mediates composition of Isar sub-proofs |
882 |
nicely. Observe that this principle incorporates some degree of freedom in |
|
883 |
proof composition. In particular, the proof body allows parameters and |
|
884 |
assumptions to be re-ordered, or commuted according to Hereditary Harrop |
|
885 |
Form. Moreover, context elements that are not used in a sub-proof may be |
|
886 |
omitted altogether. For example: |
|
58618 | 887 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
888 |
|
58618 | 889 |
text_raw \<open>\begin{minipage}{0.5\textwidth}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
890 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
891 |
(*<*) |
40964 | 892 |
notepad |
893 |
begin |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
894 |
(*>*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
895 |
have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
896 |
proof - |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
897 |
fix x and y |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
898 |
assume "A x" and "B y" |
62271 | 899 |
show "C x y" \<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
900 |
qed |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
901 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
902 |
text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
903 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
904 |
(*<*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
905 |
next |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
906 |
(*>*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
907 |
have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
908 |
proof - |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
909 |
fix x assume "A x" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
910 |
fix y assume "B y" |
62271 | 911 |
show "C x y" \<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
912 |
qed |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
913 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
914 |
text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
915 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
916 |
(*<*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
917 |
next |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
918 |
(*>*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
919 |
have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
920 |
proof - |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
921 |
fix y assume "B y" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
922 |
fix x assume "A x" |
62271 | 923 |
show "C x y" \<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
924 |
qed |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
925 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
926 |
text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
927 |
(*<*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
928 |
next |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
929 |
(*>*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
930 |
have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
931 |
proof - |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
932 |
fix y assume "B y" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
933 |
fix x |
62271 | 934 |
show "C x y" \<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
935 |
qed |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
936 |
(*<*) |
40964 | 937 |
end |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
938 |
(*>*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
939 |
|
58618 | 940 |
text_raw \<open>\end{minipage}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
941 |
|
58618 | 942 |
text \<open> |
61421 | 943 |
\<^medskip> |
62275 | 944 |
Such ``peephole optimizations'' of Isar texts are practically important to |
945 |
improve readability, by rearranging contexts elements according to the |
|
946 |
natural flow of reasoning in the body, while still observing the overall |
|
947 |
scoping rules. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
948 |
|
61421 | 949 |
\<^medskip> |
62275 | 950 |
This illustrates the basic idea of structured proof processing in Isar. The |
951 |
main mechanisms are based on natural deduction rule composition within the |
|
952 |
Pure framework. In particular, there are no direct operations on goal states |
|
953 |
within the proof body. Moreover, there is no hidden automated reasoning |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
954 |
involved, just plain unification. |
58618 | 955 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
956 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
957 |
|
58618 | 958 |
subsection \<open>Calculational reasoning \label{sec:framework-calc}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
959 |
|
58618 | 960 |
text \<open> |
29735 | 961 |
The existing Isar infrastructure is sufficiently flexible to support |
62275 | 962 |
calculational reasoning (chains of transitivity steps) as derived concept. |
963 |
The generic proof elements introduced below depend on rules declared as |
|
964 |
@{attribute trans} in the context. It is left to the object-logic to provide |
|
965 |
a suitable rule collection for mixed relations of \<open>=\<close>, \<open><\<close>, \<open>\<le>\<close>, \<open>\<subset>\<close>, \<open>\<subseteq>\<close> |
|
966 |
etc. Due to the flexibility of rule composition |
|
967 |
(\secref{sec:framework-resolution}), substitution of equals by equals is |
|
968 |
covered as well, even substitution of inequalities involving monotonicity |
|
969 |
conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"} and @{cite |
|
970 |
"Bauer-Wenzel:2001"}. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
971 |
|
62275 | 972 |
The generic calculational mechanism is based on the observation that rules |
973 |
such as \<open>trans:\<close>~@{prop "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"} proceed from the premises |
|
974 |
towards the conclusion in a deterministic fashion. Thus we may reason in |
|
975 |
forward mode, feeding intermediate results into rules selected from the |
|
976 |
context. The course of reasoning is organized by maintaining a secondary |
|
977 |
fact called ``@{fact calculation}'', apart from the primary ``@{fact this}'' |
|
978 |
already provided by the Isar primitives. In the definitions below, |
|
29735 | 979 |
@{attribute OF} refers to @{inference resolution} |
62275 | 980 |
(\secref{sec:framework-resolution}) with multiple rule arguments, and |
981 |
\<open>trans\<close> represents to a suitable rule from the context: |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
982 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
983 |
\begin{matharray}{rcl} |
61493 | 984 |
@{command "also"}\<open>\<^sub>0\<close> & \equiv & @{command "note"}~\<open>calculation = this\<close> \\ |
985 |
@{command "also"}\<open>\<^sub>n\<^sub>+\<^sub>1\<close> & \equiv & @{command "note"}~\<open>calculation = trans [OF calculation this]\<close> \\[0.5ex] |
|
986 |
@{command "finally"} & \equiv & @{command "also"}~@{command "from"}~\<open>calculation\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
987 |
\end{matharray} |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
988 |
|
62275 | 989 |
The start of a calculation is determined implicitly in the text: here |
990 |
@{command also} sets @{fact calculation} to the current result; any |
|
991 |
subsequent occurrence will update @{fact calculation} by combination with |
|
992 |
the next result and a transitivity rule. The calculational sequence is |
|
993 |
concluded via @{command finally}, where the final result is exposed for use |
|
994 |
in a concluding claim. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
995 |
|
62275 | 996 |
Here is a canonical proof pattern, using @{command have} to establish the |
997 |
intermediate results: |
|
58618 | 998 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
999 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
1000 |
(*<*) |
40964 | 1001 |
notepad |
1002 |
begin |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
1003 |
(*>*) |
62271 | 1004 |
have "a = b" \<proof> |
1005 |
also have "\<dots> = c" \<proof> |
|
1006 |
also have "\<dots> = d" \<proof> |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
1007 |
finally have "a = d" . |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
1008 |
(*<*) |
40964 | 1009 |
end |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
1010 |
(*>*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
1011 |
|
58618 | 1012 |
text \<open> |
62275 | 1013 |
The term ``\<open>\<dots>\<close>'' above is a special abbreviation provided by the |
1014 |
Isabelle/Isar syntax layer: it statically refers to the right-hand side |
|
1015 |
argument of the previous statement given in the text. Thus it happens to |
|
1016 |
coincide with relevant sub-expressions in the calculational chain, but the |
|
1017 |
exact correspondence is dependent on the transitivity rules being involved. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
1018 |
|
61421 | 1019 |
\<^medskip> |
62275 | 1020 |
Symmetry rules such as @{prop "x = y \<Longrightarrow> y = x"} are like transitivities with |
1021 |
only one premise. Isar maintains a separate rule collection declared via the |
|
1022 |
@{attribute sym} attribute, to be used in fact expressions ``\<open>a |
|
1023 |
[symmetric]\<close>'', or single-step proofs ``@{command assume}~\<open>x = y\<close>~@{command |
|
1024 |
then}~@{command have}~\<open>y = x\<close>~@{command ".."}''. |
|
58618 | 1025 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
1026 |
|
29742 | 1027 |
end |