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