author | wenzelm |
Wed, 10 Feb 2016 14:14:43 +0100 | |
changeset 62278 | c04e97be39d3 |
parent 62277 | c9b1897d4173 |
child 63039 | 1a20fd9cf281 |
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 |
|
62277 | 207 |
subproof in Isar, working backwards rather than forwards as seen before. In |
62276 | 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 |
62277 | 209 |
subproofs that is typical for Isar. The final \<^theory_text>\<open>show\<close> is like \<^theory_text>\<open>have\<close> |
62276 | 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 |
62277 | 387 |
subgoals \<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 |
|
62277 | 401 |
resolution}, for back-chaining a rule against a subgoal (replacing it by |
402 |
zero or more subgoals), and @{inference assumption}, for solving a subgoal |
|
62275 | 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. |
|
62277 | 450 |
In contrast, Isar uses a combined refinement rule as follows:\footnote{For |
451 |
simplicity and clarity, the presentation ignores \<^emph>\<open>weak premises\<close> as |
|
452 |
introduced via \<^theory_text>\<open>presume\<close> or \<^theory_text>\<open>show \<dots> when\<close>.} |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
453 |
|
62277 | 454 |
{\small |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
455 |
\[ |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
456 |
\infer[(@{inference refinement})] |
62277 | 457 |
{\<open>C\<vartheta>\<close>} |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
458 |
{\begin{tabular}{rl} |
62277 | 459 |
\<open>subgoal:\<close> & |
61493 | 460 |
\<open>(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C\<close> \\ |
62277 | 461 |
\<open>subproof:\<close> & |
462 |
\<open>\<^vec>G \<^vec>a \<Longrightarrow> B \<^vec>a\<close> \quad for schematic \<open>\<^vec>a\<close> \\ |
|
463 |
\<open>concl unifier:\<close> & |
|
61493 | 464 |
\<open>(\<lambda>\<^vec>x. B (\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>\<close> \\ |
465 |
\<open>assm unifiers:\<close> & |
|
62277 | 466 |
\<open>(\<lambda>\<^vec>x. G\<^sub>j (\<^vec>a \<^vec>x))\<vartheta> = H\<^sub>i\<vartheta>\<close> \quad for each \<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}} |
62277 | 468 |
\]} |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
469 |
|
62277 | 470 |
Here the \<open>subproof\<close> rule stems from the main \<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close> |
62276 | 471 |
outline of Isar (cf.\ \secref{sec:framework-subproof}): each assumption |
62277 | 472 |
indicated in the text results in a marked premise \<open>G\<close> above. Consequently, |
473 |
\<^theory_text>\<open>fix\<close>-\<^theory_text>\<open>assume\<close>-\<^theory_text>\<open>show\<close> enables to fit the result of a subproof quite |
|
474 |
robustly into a pending subgoal, while maintaining a good measure of |
|
475 |
flexibility: the subproof only needs to fit modulo unification, and its |
|
476 |
assumptions may be a proper subset of the subgoal premises (see |
|
477 |
\secref{sec:framework-subproof}). |
|
58618 | 478 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
479 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
480 |
|
58618 | 481 |
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
|
482 |
|
58618 | 483 |
text \<open> |
62275 | 484 |
Structured proofs are presented as high-level expressions for composing |
485 |
entities of Pure (propositions, facts, and goals). The Isar proof language |
|
486 |
allows to organize reasoning within the underlying rule calculus of Pure, |
|
62278 | 487 |
but Isar is not another logical calculus. Isar merely imposes certain |
488 |
structure and policies on Pure inferences. |
|
489 |
||
490 |
Isar is intended as an exercise in minimalism. Approximately half of the |
|
491 |
language is introduced as primitive, the rest defined as derived concepts. |
|
492 |
The grammar in \appref{ap:main-grammar} describes the core language |
|
493 |
(category \<open>proof\<close>), which is embedded into the main outer theory syntax via |
|
494 |
elements that require a proof (e.g.\ \<^theory_text>\<open>theorem\<close>, \<^theory_text>\<open>lemma\<close>, \<^theory_text>\<open>function\<close>, |
|
495 |
\<^theory_text>\<open>termination\<close>). |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
496 |
|
62278 | 497 |
The syntax for terms and propositions is inherited from Pure (and the |
498 |
object-logic). A \<open>pattern\<close> is a \<open>term\<close> with schematic variables, to be bound |
|
499 |
by higher-order matching. Simultaneous propositions or facts may be |
|
500 |
separated by the \<^theory_text>\<open>and\<close> keyword. |
|
501 |
||
502 |
\<^medskip> |
|
503 |
Facts may be referenced by name or proposition. For example, the result of |
|
504 |
``\<^theory_text>\<open>have a: A \<proof>\<close>'' becomes accessible both via the name \<open>a\<close> and the |
|
505 |
literal proposition \<open>\<open>A\<close>\<close>. Moreover, fact expressions may involve attributes |
|
506 |
that modify either the theorem or the background context. For example, the |
|
507 |
expression ``\<open>a [OF b]\<close>'' refers to the composition of two facts according |
|
508 |
to the @{inference resolution} inference of |
|
509 |
\secref{sec:framework-resolution}, while ``\<open>a [intro]\<close>'' declares a fact as |
|
510 |
introduction rule in the context. |
|
511 |
||
512 |
The special fact called ``@{fact this}'' always refers to the last result, |
|
513 |
as produced by \<^theory_text>\<open>note\<close>, \<^theory_text>\<open>assume\<close>, \<^theory_text>\<open>have\<close>, or \<^theory_text>\<open>show\<close>. Since \<^theory_text>\<open>note\<close> occurs |
|
514 |
frequently together with \<^theory_text>\<open>then\<close>, there are some abbreviations: |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
515 |
|
61421 | 516 |
\<^medskip> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
517 |
\begin{tabular}{rcl} |
62278 | 518 |
\<^theory_text>\<open>from a\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>note a then\<close> \\ |
519 |
\<^theory_text>\<open>with a\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>from a and this\<close> \\ |
|
29737
866841668584
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
wenzelm
parents:
29735
diff
changeset
|
520 |
\end{tabular} |
61421 | 521 |
\<^medskip> |
29737
866841668584
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
wenzelm
parents:
29735
diff
changeset
|
522 |
|
62278 | 523 |
The \<open>method\<close> category is essentially a parameter of the Isar language and |
524 |
may be populated later. The command \<^theory_text>\<open>method_setup\<close> allows to define proof |
|
525 |
methods semantically in Isabelle/ML. The Eisbach language allows to define |
|
526 |
proof methods symbolically, as recursive expressions over existing methods |
|
527 |
@{cite "Matichuk-et-al:2014"}; see also @{file "~~/src/HOL/Eisbach"}. |
|
528 |
||
529 |
Methods use the facts indicated by \<^theory_text>\<open>then\<close> or \<^theory_text>\<open>using\<close>, and then operate on |
|
530 |
the goal state. Some basic methods are predefined in Pure: ``@{method "-"}'' |
|
531 |
leaves the goal unchanged, ``@{method this}'' applies the facts as rules to |
|
532 |
the goal, ``@{method (Pure) "rule"}'' applies the facts to another rule and |
|
533 |
the result to the goal (both ``@{method this}'' and ``@{method (Pure) |
|
534 |
rule}'' refer to @{inference resolution} of |
|
62275 | 535 |
\secref{sec:framework-resolution}). The secondary arguments to ``@{method |
536 |
(Pure) rule}'' may be specified explicitly as in ``\<open>(rule a)\<close>'', or picked |
|
537 |
from the context. In the latter case, the system first tries rules declared |
|
538 |
as @{attribute (Pure) elim} or @{attribute (Pure) dest}, followed by those |
|
539 |
declared as @{attribute (Pure) intro}. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
540 |
|
62278 | 541 |
The default method for \<^theory_text>\<open>proof\<close> is ``@{method standard}'' (which subsumes |
542 |
@{method rule} with arguments picked from the context), for \<^theory_text>\<open>qed\<close> it is |
|
543 |
``@{method "succeed"}''. Further abbreviations for terminal proof steps are |
|
544 |
``\<^theory_text>\<open>by method\<^sub>1 method\<^sub>2\<close>'' for ``\<^theory_text>\<open>proof method\<^sub>1 qed method\<^sub>2\<close>'', and |
|
545 |
``\<^theory_text>\<open>..\<close>'' for ``\<^theory_text>\<open>by standard\<close>, and ``\<^theory_text>\<open>.\<close>'' for ``\<^theory_text>\<open>by this\<close>''. The command |
|
546 |
``\<^theory_text>\<open>unfolding facts\<close>'' operates directly on the goal by applying equalities. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
547 |
|
61421 | 548 |
\<^medskip> |
62278 | 549 |
Block structure can be indicated explicitly by ``\<^theory_text>\<open>{ \<dots> }\<close>'', although the |
550 |
body of a subproof ``\<^theory_text>\<open>proof \<dots> qed\<close>'' already provides implicit nesting. In |
|
551 |
both situations, \<^theory_text>\<open>next\<close> jumps into the next section of a block, i.e.\ it |
|
552 |
acts like closing an implicit block scope and opening another one. There is |
|
553 |
no direct connection to subgoals here! |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
554 |
|
62278 | 555 |
The commands \<^theory_text>\<open>fix\<close> and \<^theory_text>\<open>assume\<close> build up a local context (see |
556 |
\secref{sec:framework-context}), while \<^theory_text>\<open>show\<close> refines a pending subgoal by |
|
557 |
the rule resulting from a nested subproof (see |
|
62275 | 558 |
\secref{sec:framework-subproof}). Further derived concepts will support |
559 |
calculational reasoning (see \secref{sec:framework-calc}). |
|
58618 | 560 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
561 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
562 |
|
58618 | 563 |
subsection \<open>Context elements \label{sec:framework-context}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
564 |
|
58618 | 565 |
text \<open> |
62275 | 566 |
In judgments \<open>\<Gamma> \<turnstile> \<phi>\<close> of the primitive framework, \<open>\<Gamma>\<close> essentially acts like a |
62278 | 567 |
proof context. Isar elaborates this idea towards a more advanced concept, |
568 |
with additional information for type-inference, term abbreviations, local |
|
569 |
facts, hypotheses etc. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
570 |
|
62278 | 571 |
The element \<^theory_text>\<open>fix x :: \<alpha>\<close> declares a local parameter, i.e.\ an |
62275 | 572 |
arbitrary-but-fixed entity of a given type; in results exported from the |
62278 | 573 |
context, \<open>x\<close> may become anything. The \<^theory_text>\<open>assume \<guillemotleft>inference\<guillemotright>\<close> element provides |
574 |
a general interface to hypotheses: \<^theory_text>\<open>assume \<guillemotleft>inference\<guillemotright> A\<close> produces \<open>A \<turnstile> A\<close> |
|
575 |
locally, while the included inference tells how to discharge \<open>A\<close> from |
|
576 |
results \<open>A \<turnstile> B\<close> later on. There is no surface syntax for \<open>\<guillemotleft>inference\<guillemotright>\<close>, |
|
577 |
i.e.\ it may only occur internally when 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
|
578 |
|
62278 | 579 |
The default inference for \<^theory_text>\<open>assume\<close> is @{inference export} as given below. |
580 |
The derived element \<^theory_text>\<open>def x \<equiv> a\<close> is defined as \<^theory_text>\<open>fix x assume \<guillemotleft>expand\<guillemotright> x \<equiv> |
|
581 |
a\<close>, with the subsequent inference @{inference expand}. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
582 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
583 |
\[ |
62278 | 584 |
\infer[(@{inference_def export})]{\<open>\<strut>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<strut>\<Gamma> \<turnstile> B\<close>} |
585 |
\qquad |
|
586 |
\infer[(@{inference_def expand})]{\<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
|
587 |
\] |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
588 |
|
61421 | 589 |
\<^medskip> |
62278 | 590 |
The most interesting derived context element in Isar is \<^theory_text>\<open>obtain\<close> @{cite |
591 |
\<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized elimination steps in a |
|
592 |
purely forward manner. The \<^theory_text>\<open>obtain\<close> command takes a specification of |
|
593 |
parameters \<open>\<^vec>x\<close> and assumptions \<open>\<^vec>A\<close> to be added to the context, |
|
594 |
together with a proof of a case rule stating that this extension is |
|
595 |
conservative (i.e.\ may be removed from closed results later on): |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
596 |
|
61421 | 597 |
\<^medskip> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
598 |
\begin{tabular}{l} |
62278 | 599 |
\<^theory_text>\<open>\<langle>facts\<rangle> obtain "\<^vec>x" where "\<^vec>A" "\<^vec>x" \<proof> \<equiv>\<close> \\[0.5ex] |
600 |
\quad \<^theory_text>\<open>have "case": "\<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis"\<close> \\ |
|
601 |
\quad \<^theory_text>\<open>proof -\<close> \\ |
|
602 |
\qquad \<^theory_text>\<open>fix thesis\<close> \\ |
|
603 |
\qquad \<^theory_text>\<open>assume [intro]: "\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"\<close> \\ |
|
604 |
\qquad \<^theory_text>\<open>show thesis using \<langle>facts\<rangle> \<proof>\<close> \\ |
|
605 |
\quad \<^theory_text>\<open>qed\<close> \\ |
|
606 |
\quad \<^theory_text>\<open>fix "\<^vec>x" assume \<guillemotleft>elimination "case"\<guillemotright> "\<^vec>A \<^vec>x"\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
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 elimination})]{\<open>\<Gamma> \<turnstile> B\<close>}{ |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
612 |
\begin{tabular}{rl} |
61493 | 613 |
\<open>case:\<close> & |
614 |
\<open>\<Gamma> \<turnstile> \<And>thesis. (\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\[0.2ex] |
|
615 |
\<open>result:\<close> & |
|
616 |
\<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
|
617 |
\end{tabular}} |
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 |
|
62275 | 620 |
Here the name ``\<open>thesis\<close>'' is a specific convention for an |
621 |
arbitrary-but-fixed proposition; in the primitive natural deduction rules |
|
622 |
shown before we have occasionally used \<open>C\<close>. The whole statement of |
|
62278 | 623 |
``\<^theory_text>\<open>obtain x where A x\<close>'' can be read as a claim that \<open>A x\<close> may be assumed |
624 |
for some arbitrary-but-fixed \<open>x\<close>. Also note that ``\<^theory_text>\<open>obtain A and B\<close>'' |
|
625 |
without parameters is similar to ``\<^theory_text>\<open>have A and B\<close>'', but the latter |
|
626 |
involves multiple subgoals that need to be proven separately. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
627 |
|
61421 | 628 |
\<^medskip> |
62275 | 629 |
The subsequent Isar proof texts explain all context elements introduced |
630 |
above using the formal proof language itself. After finishing a local proof |
|
62278 | 631 |
within a block, the exported result is indicated via \<^theory_text>\<open>note\<close>. |
58618 | 632 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
633 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
634 |
(*<*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
635 |
theorem True |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
636 |
proof |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
637 |
(*>*) |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
638 |
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
|
639 |
{ |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
640 |
fix x |
62271 | 641 |
have "B x" \<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
642 |
} |
58618 | 643 |
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
|
644 |
text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*) |
29735 | 645 |
{ |
646 |
assume A |
|
62271 | 647 |
have B \<proof> |
29735 | 648 |
} |
58618 | 649 |
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
|
650 |
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
|
651 |
{ |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
652 |
def x \<equiv> a |
62271 | 653 |
have "B x" \<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
654 |
} |
58618 | 655 |
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
|
656 |
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
|
657 |
{ |
62271 | 658 |
obtain x where "A x" \<proof> |
659 |
have B \<proof> |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
660 |
} |
58618 | 661 |
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
|
662 |
text_raw \<open>\end{minipage}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
663 |
(*<*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
664 |
qed |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
665 |
(*>*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
666 |
|
58618 | 667 |
text \<open> |
61421 | 668 |
\<^bigskip> |
62278 | 669 |
This explains the meaning of Isar context elements without, without goal |
670 |
states getting in the way. |
|
58618 | 671 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
672 |
|
61421 | 673 |
|
58618 | 674 |
subsection \<open>Structured statements \label{sec:framework-stmt}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
675 |
|
58618 | 676 |
text \<open> |
62278 | 677 |
The syntax of top-level theorem statements is defined as follows: |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
678 |
|
61421 | 679 |
\<^medskip> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
680 |
\begin{tabular}{rcl} |
62278 | 681 |
\<open>statement\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>name: props and \<dots>\<close> \\ |
61493 | 682 |
& \<open>|\<close> & \<open>context\<^sup>* conclusion\<close> \\[0.5ex] |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
683 |
|
62278 | 684 |
\<open>context\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>fixes vars and \<dots>\<close> \\ |
685 |
& \<open>|\<close> & \<^theory_text>\<open>assumes name: props and \<dots>\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
686 |
|
62278 | 687 |
\<open>conclusion\<close> & \<open>\<equiv>\<close> & \<^theory_text>\<open>shows name: props and \<dots>\<close> \\ |
688 |
& \<open>|\<close> & \<^theory_text>\<open>obtains vars and \<dots> where name: props and \<dots>\<close> \\ |
|
61493 | 689 |
& & \quad \<open>\<BBAR> \<dots>\<close> \\ |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
690 |
\end{tabular} |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
691 |
|
61421 | 692 |
\<^medskip> |
62278 | 693 |
A simple statement consists of named propositions. The full form admits |
694 |
local context elements followed by the actual conclusions, such as ``\<^theory_text>\<open>fixes |
|
695 |
x assumes A x shows B x\<close>''. The final result emerges as a Pure rule after |
|
696 |
discharging the context: @{prop "\<And>x. A x \<Longrightarrow> B x"}. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
697 |
|
62278 | 698 |
The \<^theory_text>\<open>obtains\<close> variant is another abbreviation defined below; unlike |
699 |
\<^theory_text>\<open>obtain\<close> (cf.\ \secref{sec:framework-context}) there may be several |
|
700 |
``cases'' separated by ``\<open>\<BBAR>\<close>'', each consisting of several parameters |
|
701 |
(\<open>vars\<close>) and several premises (\<open>props\<close>). This specifies multi-branch |
|
702 |
elimination rules. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
703 |
|
61421 | 704 |
\<^medskip> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
705 |
\begin{tabular}{l} |
62278 | 706 |
\<^theory_text>\<open>obtains "\<^vec>x" where "\<^vec>A" "\<^vec>x" "\<BBAR>" \<dots> \<equiv>\<close> \\[0.5ex] |
707 |
\quad \<^theory_text>\<open>fixes thesis\<close> \\ |
|
708 |
\quad \<^theory_text>\<open>assumes [intro]: "\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis" and \<dots>\<close> \\ |
|
709 |
\quad \<^theory_text>\<open>shows thesis\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
710 |
\end{tabular} |
61421 | 711 |
\<^medskip> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
712 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
713 |
Presenting structured statements in such an ``open'' format usually |
62275 | 714 |
simplifies the subsequent proof, because the outer structure of the problem |
715 |
is already laid out directly. E.g.\ consider the following canonical |
|
62278 | 716 |
patterns for \<^theory_text>\<open>shows\<close> and \<^theory_text>\<open>obtains\<close>, respectively: |
58618 | 717 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
718 |
|
58618 | 719 |
text_raw \<open>\begin{minipage}{0.5\textwidth}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
720 |
|
62278 | 721 |
theorem |
722 |
fixes x and y |
|
723 |
assumes "A x" and "B y" |
|
724 |
shows "C x y" |
|
725 |
proof - |
|
726 |
from \<open>A x\<close> and \<open>B y\<close> |
|
727 |
show "C x y" \<proof> |
|
728 |
qed |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
729 |
|
58618 | 730 |
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
|
731 |
|
62278 | 732 |
theorem |
733 |
obtains x and y |
|
734 |
where "A x" and "B y" |
|
735 |
proof - |
|
736 |
have "A a" and "B b" \<proof> |
|
737 |
then show thesis .. |
|
738 |
qed |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
739 |
|
58618 | 740 |
text_raw \<open>\end{minipage}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
741 |
|
58618 | 742 |
text \<open> |
61421 | 743 |
\<^medskip> |
62278 | 744 |
Here local facts \<open>\<open>A x\<close>\<close> and \<open>\<open>B y\<close>\<close> are referenced immediately; there is no |
745 |
need to decompose the logical rule structure again. In the second proof the |
|
746 |
final ``\<^theory_text>\<open>then show thesis ..\<close>'' involves the local rule case \<open>\<And>x y. A x \<Longrightarrow> B |
|
62275 | 747 |
y \<Longrightarrow> thesis\<close> for the particular instance of terms \<open>a\<close> and \<open>b\<close> produced in the |
62278 | 748 |
body. |
749 |
\<close> |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
750 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
751 |
|
58618 | 752 |
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
|
753 |
|
58618 | 754 |
text \<open> |
62275 | 755 |
By breaking up the grammar for the Isar proof language, we may understand a |
756 |
proof text as a linear sequence of individual proof commands. These are |
|
757 |
interpreted as transitions of the Isar virtual machine (Isar/VM), which |
|
758 |
operates on a block-structured configuration in single steps. This allows |
|
759 |
users to write proof texts in an incremental manner, and inspect |
|
760 |
intermediate configurations for debugging. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
761 |
|
62275 | 762 |
The basic idea is analogous to evaluating algebraic expressions on a stack |
763 |
machine: \<open>(a + b) \<cdot> c\<close> then corresponds to a sequence of single transitions |
|
764 |
for each symbol \<open>(, a, +, b, ), \<cdot>, c\<close>. In Isar the algebraic values are |
|
765 |
facts or goals, and the operations are inferences. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
766 |
|
61421 | 767 |
\<^medskip> |
62275 | 768 |
The Isar/VM state maintains a stack of nodes, each node contains the local |
769 |
proof context, the linguistic mode, and a pending goal (optional). The mode |
|
770 |
determines the type of transition that may be performed next, it essentially |
|
771 |
alternates between forward and backward reasoning, with an intermediate |
|
772 |
stage for chained facts (see \figref{fig:isar-vm}). |
|
29738 | 773 |
|
774 |
\begin{figure}[htb] |
|
775 |
\begin{center} |
|
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48279
diff
changeset
|
776 |
\includegraphics[width=0.8\textwidth]{isar-vm} |
29738 | 777 |
\end{center} |
778 |
\caption{Isar/VM modes}\label{fig:isar-vm} |
|
779 |
\end{figure} |
|
780 |
||
62275 | 781 |
For example, in \<open>state\<close> mode Isar acts like a mathematical scratch-pad, |
62278 | 782 |
accepting declarations like \<^theory_text>\<open>fix\<close>, \<^theory_text>\<open>assume\<close>, and claims like \<^theory_text>\<open>have\<close>, |
783 |
\<^theory_text>\<open>show\<close>. A goal statement changes the mode to \<open>prove\<close>, which means that we |
|
784 |
may now refine the problem via \<^theory_text>\<open>unfolding\<close> or \<^theory_text>\<open>proof\<close>. Then we are again |
|
785 |
in \<open>state\<close> mode of a proof body, which may issue \<^theory_text>\<open>show\<close> statements to solve |
|
786 |
pending subgoals. A concluding \<^theory_text>\<open>qed\<close> will return to the original \<open>state\<close> |
|
787 |
mode one level upwards. The subsequent Isar/VM trace indicates block |
|
788 |
structure, linguistic mode, goal state, and inferences: |
|
58618 | 789 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
790 |
|
58618 | 791 |
text_raw \<open>\begingroup\footnotesize\<close> |
40964 | 792 |
(*<*)notepad begin |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
793 |
(*>*) |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
794 |
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
|
795 |
have "A \<longrightarrow> B" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
796 |
proof |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
797 |
assume A |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
798 |
show B |
62271 | 799 |
\<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
800 |
qed |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
801 |
text_raw \<open>\end{minipage}\quad |
29735 | 802 |
\begin{minipage}[t]{0.06\textwidth} |
61493 | 803 |
\<open>begin\<close> \\ |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
804 |
\\ |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
805 |
\\ |
61493 | 806 |
\<open>begin\<close> \\ |
807 |
\<open>end\<close> \\ |
|
808 |
\<open>end\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
809 |
\end{minipage} |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
810 |
\begin{minipage}[t]{0.08\textwidth} |
61493 | 811 |
\<open>prove\<close> \\ |
812 |
\<open>state\<close> \\ |
|
813 |
\<open>state\<close> \\ |
|
814 |
\<open>prove\<close> \\ |
|
815 |
\<open>state\<close> \\ |
|
816 |
\<open>state\<close> \\ |
|
29735 | 817 |
\end{minipage}\begin{minipage}[t]{0.35\textwidth} |
61493 | 818 |
\<open>(A \<longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)\<close> \\ |
819 |
\<open>(A \<Longrightarrow> B) \<Longrightarrow> #(A \<longrightarrow> B)\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
820 |
\\ |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
821 |
\\ |
61493 | 822 |
\<open>#(A \<longrightarrow> B)\<close> \\ |
823 |
\<open>A \<longrightarrow> B\<close> \\ |
|
29735 | 824 |
\end{minipage}\begin{minipage}[t]{0.4\textwidth} |
61493 | 825 |
\<open>(init)\<close> \\ |
826 |
\<open>(resolution impI)\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
827 |
\\ |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
828 |
\\ |
61493 | 829 |
\<open>(refinement #A \<Longrightarrow> B)\<close> \\ |
830 |
\<open>(finish)\<close> \\ |
|
58618 | 831 |
\end{minipage}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
832 |
(*<*) |
40964 | 833 |
end |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
834 |
(*>*) |
58618 | 835 |
text_raw \<open>\endgroup\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
836 |
|
58618 | 837 |
text \<open> |
61420 | 838 |
Here the @{inference refinement} inference from |
62277 | 839 |
\secref{sec:framework-resolution} mediates composition of Isar subproofs |
62275 | 840 |
nicely. Observe that this principle incorporates some degree of freedom in |
841 |
proof composition. In particular, the proof body allows parameters and |
|
842 |
assumptions to be re-ordered, or commuted according to Hereditary Harrop |
|
62277 | 843 |
Form. Moreover, context elements that are not used in a subproof may be |
62275 | 844 |
omitted altogether. For example: |
58618 | 845 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
846 |
|
58618 | 847 |
text_raw \<open>\begin{minipage}{0.5\textwidth}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
848 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
849 |
(*<*) |
40964 | 850 |
notepad |
851 |
begin |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
852 |
(*>*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
853 |
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
|
854 |
proof - |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
855 |
fix x and y |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
856 |
assume "A x" and "B y" |
62271 | 857 |
show "C x y" \<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
858 |
qed |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
859 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
860 |
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
|
861 |
|
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 |
next |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
864 |
(*>*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
865 |
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
|
866 |
proof - |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
867 |
fix x assume "A x" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
868 |
fix y assume "B y" |
62271 | 869 |
show "C x y" \<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
870 |
qed |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
871 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
872 |
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
|
873 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
874 |
(*<*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
875 |
next |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
876 |
(*>*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
877 |
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
|
878 |
proof - |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
879 |
fix y assume "B y" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
880 |
fix x assume "A x" |
62271 | 881 |
show "C x y" \<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
882 |
qed |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
883 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58618
diff
changeset
|
884 |
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
|
885 |
(*<*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
886 |
next |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
887 |
(*>*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
888 |
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
|
889 |
proof - |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
890 |
fix y assume "B y" |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
891 |
fix x |
62271 | 892 |
show "C x y" \<proof> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
893 |
qed |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
894 |
(*<*) |
40964 | 895 |
end |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
896 |
(*>*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
897 |
|
58618 | 898 |
text_raw \<open>\end{minipage}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
899 |
|
58618 | 900 |
text \<open> |
61421 | 901 |
\<^medskip> |
62278 | 902 |
Such fine-tuning of Isar text is practically important to improve |
903 |
readability. Contexts elements are rearranged according to the natural flow |
|
904 |
of reasoning in the body, while still observing the overall scoping rules. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
905 |
|
61421 | 906 |
\<^medskip> |
62275 | 907 |
This illustrates the basic idea of structured proof processing in Isar. The |
908 |
main mechanisms are based on natural deduction rule composition within the |
|
909 |
Pure framework. In particular, there are no direct operations on goal states |
|
910 |
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
|
911 |
involved, just plain unification. |
58618 | 912 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
913 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
914 |
|
58618 | 915 |
subsection \<open>Calculational reasoning \label{sec:framework-calc}\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
916 |
|
58618 | 917 |
text \<open> |
29735 | 918 |
The existing Isar infrastructure is sufficiently flexible to support |
62275 | 919 |
calculational reasoning (chains of transitivity steps) as derived concept. |
920 |
The generic proof elements introduced below depend on rules declared as |
|
921 |
@{attribute trans} in the context. It is left to the object-logic to provide |
|
922 |
a suitable rule collection for mixed relations of \<open>=\<close>, \<open><\<close>, \<open>\<le>\<close>, \<open>\<subset>\<close>, \<open>\<subseteq>\<close> |
|
923 |
etc. Due to the flexibility of rule composition |
|
924 |
(\secref{sec:framework-resolution}), substitution of equals by equals is |
|
925 |
covered as well, even substitution of inequalities involving monotonicity |
|
926 |
conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"} and @{cite |
|
927 |
"Bauer-Wenzel:2001"}. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
928 |
|
62275 | 929 |
The generic calculational mechanism is based on the observation that rules |
930 |
such as \<open>trans:\<close>~@{prop "x = y \<Longrightarrow> y = z \<Longrightarrow> x = z"} proceed from the premises |
|
931 |
towards the conclusion in a deterministic fashion. Thus we may reason in |
|
932 |
forward mode, feeding intermediate results into rules selected from the |
|
933 |
context. The course of reasoning is organized by maintaining a secondary |
|
934 |
fact called ``@{fact calculation}'', apart from the primary ``@{fact this}'' |
|
935 |
already provided by the Isar primitives. In the definitions below, |
|
29735 | 936 |
@{attribute OF} refers to @{inference resolution} |
62275 | 937 |
(\secref{sec:framework-resolution}) with multiple rule arguments, and |
938 |
\<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
|
939 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
940 |
\begin{matharray}{rcl} |
62278 | 941 |
\<^theory_text>\<open>also"\<^sub>0"\<close> & \equiv & \<^theory_text>\<open>note calculation = this\<close> \\ |
942 |
\<^theory_text>\<open>also"\<^sub>n\<^sub>+\<^sub>1"\<close> & \equiv & \<^theory_text>\<open>note calculation = trans [OF calculation this]\<close> \\[0.5ex] |
|
943 |
\<^theory_text>\<open>finally\<close> & \equiv & \<^theory_text>\<open>also from calculation\<close> \\ |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
944 |
\end{matharray} |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
945 |
|
62275 | 946 |
The start of a calculation is determined implicitly in the text: here |
62278 | 947 |
\<^theory_text>\<open>also\<close> sets @{fact calculation} to the current result; any subsequent |
948 |
occurrence will update @{fact calculation} by combination with the next |
|
949 |
result and a transitivity rule. The calculational sequence is concluded via |
|
950 |
\<^theory_text>\<open>finally\<close>, where the final result is exposed for use in a concluding claim. |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
951 |
|
62278 | 952 |
Here is a canonical proof pattern, using \<^theory_text>\<open>have\<close> to establish the |
62275 | 953 |
intermediate results: |
58618 | 954 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
955 |
|
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
956 |
(*<*) |
40964 | 957 |
notepad |
958 |
begin |
|
62278 | 959 |
fix a b c d :: 'a |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
960 |
(*>*) |
62271 | 961 |
have "a = b" \<proof> |
962 |
also have "\<dots> = c" \<proof> |
|
963 |
also have "\<dots> = d" \<proof> |
|
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
964 |
finally have "a = d" . |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
965 |
(*<*) |
40964 | 966 |
end |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
967 |
(*>*) |
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
968 |
|
58618 | 969 |
text \<open> |
62278 | 970 |
The term ``\<open>\<dots>\<close>'' (literal ellipsis) is a special abbreviation provided by |
971 |
the Isabelle/Isar term syntax: it statically refers to the right-hand side |
|
62275 | 972 |
argument of the previous statement given in the text. Thus it happens to |
973 |
coincide with relevant sub-expressions in the calculational chain, but the |
|
974 |
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
|
975 |
|
61421 | 976 |
\<^medskip> |
62275 | 977 |
Symmetry rules such as @{prop "x = y \<Longrightarrow> y = x"} are like transitivities with |
978 |
only one premise. Isar maintains a separate rule collection declared via the |
|
979 |
@{attribute sym} attribute, to be used in fact expressions ``\<open>a |
|
62278 | 980 |
[symmetric]\<close>'', or single-step proofs ``\<^theory_text>\<open>assume "x = y" then have "y = x" |
981 |
..\<close>''. |
|
58618 | 982 |
\<close> |
29729
c2e926455fcc
more on Isar framework -- mostly from Trybulec Festschrift;
wenzelm
parents:
29721
diff
changeset
|
983 |
|
29742 | 984 |
end |