47269
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Logic}%
|
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
%
|
|
11 |
\endisatagtheory
|
|
12 |
{\isafoldtheory}%
|
|
13 |
%
|
|
14 |
\isadelimtheory
|
|
15 |
%
|
|
16 |
\endisadelimtheory
|
|
17 |
%
|
|
18 |
\begin{isamarkuptext}%
|
|
19 |
\vspace{-5ex}
|
|
20 |
\section{Logic and Proof Beyond Equality}
|
|
21 |
\label{sec:Logic}
|
|
22 |
|
|
23 |
\subsection{Formulas}
|
|
24 |
|
|
25 |
The basic syntax of formulas (\textit{form} below)
|
|
26 |
provides the standard logical constructs, in decreasing precedence:
|
|
27 |
\[
|
|
28 |
\begin{array}{rcl}
|
|
29 |
|
|
30 |
\mathit{form} & ::= &
|
|
31 |
\isa{{\isaliteral{28}{\isacharparenleft}}form{\isaliteral{29}{\isacharparenright}}} ~\mid~
|
|
32 |
\isa{True} ~\mid~
|
|
33 |
\isa{False} ~\mid~
|
|
34 |
\isa{term\ {\isaliteral{3D}{\isacharequal}}\ term}\\
|
|
35 |
&\mid& \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ form} ~\mid~
|
|
36 |
\isa{form\ {\isaliteral{5C3C616E643E}{\isasymand}}\ form} ~\mid~
|
|
37 |
\isa{form\ {\isaliteral{5C3C6F723E}{\isasymor}}\ form} ~\mid~
|
|
38 |
\isa{form\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ form}\\
|
|
39 |
&\mid& \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ form} ~\mid~ \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ form}
|
|
40 |
\end{array}
|
|
41 |
\]
|
|
42 |
Terms are the ones we have seen all along, built from constant, variables,
|
|
43 |
function application and \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-abstraction, including all the syntactic
|
|
44 |
sugar like infix symbols, \isa{if}, \isa{case} etc.
|
|
45 |
\begin{warn}
|
|
46 |
Remember that formulas are simply terms of type \isa{bool}. Hence
|
|
47 |
\isa{{\isaliteral{3D}{\isacharequal}}} also works for formulas. Beware that \isa{{\isaliteral{3D}{\isacharequal}}} has a higher
|
|
48 |
precedence than the other logical operators. Hence \isa{s\ {\isaliteral{3D}{\isacharequal}}\ t\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A} means
|
|
49 |
\isa{{\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A}, and \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{3D}{\isacharequal}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A} means \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}B\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B}.
|
|
50 |
Logical equivalence can also be written with
|
|
51 |
\isa{{\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}} instead of \isa{{\isaliteral{3D}{\isacharequal}}}, where \isa{{\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}} has the same low
|
|
52 |
precedence as \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}. Hence \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A} really means
|
|
53 |
\isa{{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{29}{\isacharparenright}}}.
|
|
54 |
\end{warn}
|
|
55 |
\begin{warn}
|
|
56 |
Quantifiers need to be enclosed in parentheses if they are nested within
|
|
57 |
other constructs (just like \isa{if}, \isa{case} and \isa{let}).
|
|
58 |
\end{warn}
|
|
59 |
The most frequent logical symbols have the following ASCII representations:
|
|
60 |
\begin{center}
|
|
61 |
\begin{tabular}{l@ {\qquad}l@ {\qquad}l}
|
|
62 |
\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}} & \xsymbol{forall} & \texttt{ALL}\\
|
|
63 |
\isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}} & \xsymbol{exists} & \texttt{EX}\\
|
|
64 |
\isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}} & \xsymbol{lambda} & \texttt{\%}\\
|
|
65 |
\isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}} & \texttt{-{}->}\\
|
|
66 |
\isa{{\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}} & \texttt{<-{}->}\\
|
|
67 |
\isa{{\isaliteral{5C3C616E643E}{\isasymand}}} & \texttt{/\char`\\} & \texttt{\&}\\
|
|
68 |
\isa{{\isaliteral{5C3C6F723E}{\isasymor}}} & \texttt{\char`\\/} & \texttt{|}\\
|
|
69 |
\isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}} & \xsymbol{not} & \texttt{\char`~}\\
|
|
70 |
\isa{{\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}} & \xsymbol{noteq} & \texttt{\char`~=}
|
|
71 |
\end{tabular}
|
|
72 |
\end{center}
|
|
73 |
The first column shows the symbols, the second column ASCII representations
|
|
74 |
that Isabelle interfaces convert into the corresponding symbol,
|
|
75 |
and the third column shows ASCII representations that stay fixed.
|
|
76 |
\begin{warn}
|
|
77 |
The implication \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} is part of the Isabelle framework. It structures
|
|
78 |
theorems and proof states, separating assumptions from conclusion.
|
|
79 |
The implication \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}} is part of the logic HOL and can occur inside the
|
|
80 |
formulas that make up the assumptions and conclusion.
|
|
81 |
Theorems should be of the form \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{3B}{\isacharsemicolon}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A},
|
|
82 |
not \isa{A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A}. Both are logically equivalent
|
|
83 |
but the first one works better when using the theorem in further proofs.
|
|
84 |
\end{warn}
|
|
85 |
|
|
86 |
\subsection{Sets}
|
|
87 |
|
|
88 |
Sets of elements of type \isa{{\isaliteral{27}{\isacharprime}}a} have type \isa{{\isaliteral{27}{\isacharprime}}a\ set}.
|
|
89 |
They can be finite or infinite. Sets come with the usual notations:
|
|
90 |
\begin{itemize}
|
|
91 |
\item \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}},\quad \isa{{\isaliteral{7B}{\isacharbraceleft}}e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}e\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{7D}{\isacharbraceright}}}
|
|
92 |
\item \isa{e\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A},\quad \isa{A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ B}
|
|
93 |
\item \isa{A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B},\quad \isa{A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B},\quad \isa{A\ {\isaliteral{2D}{\isacharminus}}\ B},\quad \isa{{\isaliteral{2D}{\isacharminus}}\ A}
|
|
94 |
\end{itemize}
|
|
95 |
and much more. \isa{UNIV} is the set of all elements of some type.
|
|
96 |
Set comprehension is written \isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}}
|
|
97 |
rather than \isa{{\isaliteral{7B}{\isacharbraceleft}}x\ {\isaliteral{7C}{\isacharbar}}\ P{\isaliteral{7D}{\isacharbraceright}}}, to emphasize the variable binding nature
|
|
98 |
of the construct.
|
|
99 |
\begin{warn}
|
|
100 |
In \isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}} the \isa{x} must be a variable. Set comprehension
|
|
101 |
involving a proper term \isa{t} must be written
|
|
102 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7B}{\isacharbraceleft}}t\ {\isaliteral{7C}{\isacharbar}}x\ y\ z{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}},
|
|
103 |
where \isa{x\ y\ z} are the free variables in \isa{t}.
|
|
104 |
This is just a shorthand for \isa{{\isaliteral{7B}{\isacharbraceleft}}v{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x\ y\ z{\isaliteral{2E}{\isachardot}}\ v\ {\isaliteral{3D}{\isacharequal}}\ t\ {\isaliteral{5C3C616E643E}{\isasymand}}\ P{\isaliteral{7D}{\isacharbraceright}}}, where
|
|
105 |
\isa{v} is a new variable.
|
|
106 |
\end{warn}
|
|
107 |
|
|
108 |
Here are the ASCII representations of the mathematical symbols:
|
|
109 |
\begin{center}
|
|
110 |
\begin{tabular}{l@ {\quad}l@ {\quad}l}
|
|
111 |
\isa{{\isaliteral{5C3C696E3E}{\isasymin}}} & \texttt{\char`\\\char`\<in>} & \texttt{:}\\
|
|
112 |
\isa{{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}} & \texttt{\char`\\\char`\<subseteq>} & \texttt{<=}\\
|
|
113 |
\isa{{\isaliteral{5C3C756E696F6E3E}{\isasymunion}}} & \texttt{\char`\\\char`\<union>} & \texttt{Un}\\
|
|
114 |
\isa{{\isaliteral{5C3C696E7465723E}{\isasyminter}}} & \texttt{\char`\\\char`\<inter>} & \texttt{Int}
|
|
115 |
\end{tabular}
|
|
116 |
\end{center}
|
|
117 |
Sets also allow bounded quantifications \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ P} and
|
|
118 |
\isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ P}.
|
|
119 |
|
|
120 |
\subsection{Proof automation}
|
|
121 |
|
|
122 |
So far we have only seen \isa{simp} and \isa{auto}: Both perform
|
|
123 |
rewriting, both can also prove linear arithmetic facts (no multiplication),
|
|
124 |
and \isa{auto} is also able to prove simple logical or set-theoretic goals:%
|
|
125 |
\end{isamarkuptext}%
|
|
126 |
\isamarkuptrue%
|
|
127 |
\isacommand{lemma}\isamarkupfalse%
|
|
128 |
\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}y{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
129 |
%
|
|
130 |
\isadelimproof
|
|
131 |
%
|
|
132 |
\endisadelimproof
|
|
133 |
%
|
|
134 |
\isatagproof
|
|
135 |
\isacommand{by}\isamarkupfalse%
|
|
136 |
\ auto%
|
|
137 |
\endisatagproof
|
|
138 |
{\isafoldproof}%
|
|
139 |
%
|
|
140 |
\isadelimproof
|
|
141 |
\isanewline
|
|
142 |
%
|
|
143 |
\endisadelimproof
|
|
144 |
\isanewline
|
|
145 |
\isacommand{lemma}\isamarkupfalse%
|
|
146 |
\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ B\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ C\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ B\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
147 |
%
|
|
148 |
\isadelimproof
|
|
149 |
%
|
|
150 |
\endisadelimproof
|
|
151 |
%
|
|
152 |
\isatagproof
|
|
153 |
\isacommand{by}\isamarkupfalse%
|
|
154 |
\ auto%
|
|
155 |
\endisatagproof
|
|
156 |
{\isafoldproof}%
|
|
157 |
%
|
|
158 |
\isadelimproof
|
|
159 |
%
|
|
160 |
\endisadelimproof
|
|
161 |
%
|
|
162 |
\begin{isamarkuptext}%
|
|
163 |
where
|
|
164 |
\begin{quote}
|
|
165 |
\isacom{by} \textit{proof-method}
|
|
166 |
\end{quote}
|
|
167 |
is short for
|
|
168 |
\begin{quote}
|
|
169 |
\isacom{apply} \textit{proof-method}\\
|
|
170 |
\isacom{done}
|
|
171 |
\end{quote}
|
|
172 |
The key characteristics of both \isa{simp} and \isa{auto} are
|
|
173 |
\begin{itemize}
|
|
174 |
\item They show you were they got stuck, giving you an idea how to continue.
|
|
175 |
\item They perform the obvious steps but are highly incomplete.
|
|
176 |
\end{itemize}
|
|
177 |
A proof method is \concept{complete} if it can prove all true formulas.
|
|
178 |
There is no complete proof method for HOL, not even in theory.
|
|
179 |
Hence all our proof methods only differ in how incomplete they are.
|
|
180 |
|
|
181 |
A proof method that is still incomplete but tries harder than \isa{auto} is
|
|
182 |
\isa{fastforce}. It either succeeds or fails, it acts on the first
|
|
183 |
subgoal only, and it can be modified just like \isa{auto}, e.g.\
|
|
184 |
with \isa{simp\ add}. Here is a typical example of what \isa{fastforce}
|
|
185 |
can do:%
|
|
186 |
\end{isamarkuptext}%
|
|
187 |
\isamarkuptrue%
|
|
188 |
\isacommand{lemma}\isamarkupfalse%
|
|
189 |
\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}xs\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}ys{\isaliteral{2E}{\isachardot}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ ys\ {\isaliteral{40}{\isacharat}}\ ys{\isaliteral{3B}{\isacharsemicolon}}\ \ us\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
|
|
190 |
\ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}n{\isaliteral{2E}{\isachardot}}\ length\ us\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2B}{\isacharplus}}n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
191 |
%
|
|
192 |
\isadelimproof
|
|
193 |
%
|
|
194 |
\endisadelimproof
|
|
195 |
%
|
|
196 |
\isatagproof
|
|
197 |
\isacommand{by}\isamarkupfalse%
|
|
198 |
\ fastforce%
|
|
199 |
\endisatagproof
|
|
200 |
{\isafoldproof}%
|
|
201 |
%
|
|
202 |
\isadelimproof
|
|
203 |
%
|
|
204 |
\endisadelimproof
|
|
205 |
%
|
|
206 |
\begin{isamarkuptext}%
|
|
207 |
This lemma is out of reach for \isa{auto} because of the
|
|
208 |
quantifiers. Even \isa{fastforce} fails when the quantifier structure
|
|
209 |
becomes more complicated. In a few cases, its slow version \isa{force}
|
|
210 |
succeeds where \isa{fastforce} fails.
|
|
211 |
|
|
212 |
The method of choice for complex logical goals is \isa{blast}. In the
|
|
213 |
following example, \isa{T} and \isa{A} are two binary predicates, and it
|
|
214 |
is shown that \isa{T} is total, \isa{A} is antisymmetric and \isa{T} is
|
|
215 |
a subset of \isa{A}, then \isa{A} is a subset of \isa{T}:%
|
|
216 |
\end{isamarkuptext}%
|
|
217 |
\isamarkuptrue%
|
|
218 |
\isacommand{lemma}\isamarkupfalse%
|
|
219 |
\isanewline
|
|
220 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ y{\isaliteral{2E}{\isachardot}}\ T\ x\ y\ {\isaliteral{5C3C6F723E}{\isasymor}}\ T\ y\ x{\isaliteral{3B}{\isacharsemicolon}}\isanewline
|
|
221 |
\ \ \ \ \ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ y{\isaliteral{2E}{\isachardot}}\ A\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A\ y\ x\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{3B}{\isacharsemicolon}}\isanewline
|
|
222 |
\ \ \ \ \ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ y{\isaliteral{2E}{\isachardot}}\ T\ x\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A\ x\ y\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
|
|
223 |
\ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ y{\isaliteral{2E}{\isachardot}}\ A\ x\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ T\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
224 |
%
|
|
225 |
\isadelimproof
|
|
226 |
%
|
|
227 |
\endisadelimproof
|
|
228 |
%
|
|
229 |
\isatagproof
|
|
230 |
\isacommand{by}\isamarkupfalse%
|
|
231 |
\ blast%
|
|
232 |
\endisatagproof
|
|
233 |
{\isafoldproof}%
|
|
234 |
%
|
|
235 |
\isadelimproof
|
|
236 |
%
|
|
237 |
\endisadelimproof
|
|
238 |
%
|
|
239 |
\begin{isamarkuptext}%
|
|
240 |
We leave it to the reader to figure out why this lemma is true.
|
|
241 |
Method \isa{blast}
|
|
242 |
\begin{itemize}
|
|
243 |
\item is (in principle) a complete proof procedure for first-order formulas,
|
|
244 |
a fragment of HOL. In practice there is a search bound.
|
|
245 |
\item does no rewriting and knows very little about equality.
|
|
246 |
\item covers logic, sets and relations.
|
|
247 |
\item either succeeds or fails.
|
|
248 |
\end{itemize}
|
|
249 |
Because of its strength in logic and sets and its weakness in equality reasoning, it complements the earlier proof methods.
|
|
250 |
|
|
251 |
|
|
252 |
\subsubsection{Sledgehammer}
|
|
253 |
|
|
254 |
Command \isacom{sledgehammer} calls a number of external automatic
|
|
255 |
theorem provers (ATPs) that run for up to 30 seconds searching for a
|
|
256 |
proof. Some of these ATPs are part of the Isabelle installation, others are
|
|
257 |
queried over the internet. If successful, a proof command is generated and can
|
|
258 |
be inserted into your proof. The biggest win of \isacom{sledgehammer} is
|
|
259 |
that it will take into account the whole lemma library and you do not need to
|
|
260 |
feed in any lemma explicitly. For example,%
|
|
261 |
\end{isamarkuptext}%
|
|
262 |
\isamarkuptrue%
|
|
263 |
\isacommand{lemma}\isamarkupfalse%
|
|
264 |
\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ xs\ {\isaliteral{40}{\isacharat}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ ys\ {\isaliteral{40}{\isacharat}}\ xs{\isaliteral{3B}{\isacharsemicolon}}\ \ length\ xs\ {\isaliteral{3D}{\isacharequal}}\ length\ ys\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
265 |
\isadelimproof
|
|
266 |
%
|
|
267 |
\endisadelimproof
|
|
268 |
%
|
|
269 |
\isatagproof
|
|
270 |
%
|
|
271 |
\begin{isamarkuptxt}%
|
|
272 |
cannot be solved by any of the standard proof methods, but
|
|
273 |
\isacom{sledgehammer} finds the following proof:%
|
|
274 |
\end{isamarkuptxt}%
|
|
275 |
\isamarkuptrue%
|
|
276 |
\isacommand{by}\isamarkupfalse%
|
|
277 |
\ {\isaliteral{28}{\isacharparenleft}}metis\ append{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}conv{\isaliteral{5F}{\isacharunderscore}}conj{\isaliteral{29}{\isacharparenright}}%
|
|
278 |
\endisatagproof
|
|
279 |
{\isafoldproof}%
|
|
280 |
%
|
|
281 |
\isadelimproof
|
|
282 |
%
|
|
283 |
\endisadelimproof
|
|
284 |
%
|
|
285 |
\begin{isamarkuptext}%
|
|
286 |
We do not explain how the proof was found but what this command
|
|
287 |
means. For a start, Isabelle does not trust external tools (and in particular
|
|
288 |
not the translations from Isabelle's logic to those tools!)
|
|
289 |
and insists on a proof that it can check. This is what \isa{metis} does.
|
|
290 |
It is given a list of lemmas and tries to find a proof just using those lemmas
|
|
291 |
(and pure logic). In contrast to \isa{simp} and friends that know a lot of
|
|
292 |
lemmas already, using \isa{metis} manually is tedious because one has
|
|
293 |
to find all the relevant lemmas first. But that is precisely what
|
|
294 |
\isacom{sledgehammer} does for us.
|
|
295 |
In this case lemma \isa{append{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{5F}{\isacharunderscore}}conv{\isaliteral{5F}{\isacharunderscore}}conj} alone suffices:
|
|
296 |
\begin{isabelle}%
|
|
297 |
{\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{40}{\isacharat}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{3D}{\isacharequal}}\ take\ {\isaliteral{28}{\isacharparenleft}}length\ xs{\isaliteral{29}{\isacharparenright}}\ zs\ {\isaliteral{5C3C616E643E}{\isasymand}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ drop\ {\isaliteral{28}{\isacharparenleft}}length\ xs{\isaliteral{29}{\isacharparenright}}\ zs{\isaliteral{29}{\isacharparenright}}%
|
|
298 |
\end{isabelle}
|
|
299 |
We leave it to the reader to figure out why this lemma suffices to prove
|
|
300 |
the above lemma, even without any knowledge of what the functions \isa{take}
|
|
301 |
and \isa{drop} do. Keep in mind that the variables in the two lemmas
|
|
302 |
are independent of each other, despite the same names, and that you can
|
|
303 |
substitute arbitrary values for the free variables in a lemma.
|
|
304 |
|
|
305 |
Just as for the other proof methods we have seen, there is no guarantee that
|
|
306 |
\isacom{sledgehammer} will find a proof if it exists. Nor is
|
|
307 |
\isacom{sledgehammer} superior to the other proof methods. They are
|
|
308 |
incomparable. Therefore it is recommended to apply \isa{simp} or \isa{auto} before invoking \isacom{sledgehammer} on what is left.
|
|
309 |
|
|
310 |
\subsubsection{Arithmetic}
|
|
311 |
|
|
312 |
By arithmetic formulas we mean formulas involving variables, numbers, \isa{{\isaliteral{2B}{\isacharplus}}}, \isa{{\isaliteral{2D}{\isacharminus}}}, \isa{{\isaliteral{3D}{\isacharequal}}}, \isa{{\isaliteral{3C}{\isacharless}}}, \isa{{\isaliteral{5C3C6C653E}{\isasymle}}} and the usual logical
|
|
313 |
connectives \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}}, \isa{{\isaliteral{5C3C616E643E}{\isasymand}}}, \isa{{\isaliteral{5C3C6F723E}{\isasymor}}}, \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}},
|
|
314 |
\isa{{\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}}. Strictly speaking, this is known as \concept{linear arithmetic}
|
|
315 |
because it does not involve multiplication, although multiplication with
|
|
316 |
numbers, e.g.\ \isa{{\isadigit{2}}{\isaliteral{2A}{\isacharasterisk}}n} is allowed. Such formulas can be proved by
|
|
317 |
\isa{arith}:%
|
|
318 |
\end{isamarkuptext}%
|
|
319 |
\isamarkuptrue%
|
|
320 |
\isacommand{lemma}\isamarkupfalse%
|
|
321 |
\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ x\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{3B}{\isacharsemicolon}}\ {\isadigit{2}}{\isaliteral{2A}{\isacharasterisk}}x\ {\isaliteral{3C}{\isacharless}}\ c\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isadigit{2}}{\isaliteral{2A}{\isacharasterisk}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isadigit{2}}{\isaliteral{2A}{\isacharasterisk}}b\ {\isaliteral{2B}{\isacharplus}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
322 |
%
|
|
323 |
\isadelimproof
|
|
324 |
%
|
|
325 |
\endisadelimproof
|
|
326 |
%
|
|
327 |
\isatagproof
|
|
328 |
\isacommand{by}\isamarkupfalse%
|
|
329 |
\ arith%
|
|
330 |
\endisatagproof
|
|
331 |
{\isafoldproof}%
|
|
332 |
%
|
|
333 |
\isadelimproof
|
|
334 |
%
|
|
335 |
\endisadelimproof
|
|
336 |
%
|
|
337 |
\begin{isamarkuptext}%
|
|
338 |
In fact, \isa{auto} and \isa{simp} can prove many linear
|
|
339 |
arithmetic formulas already, like the one above, by calling a weak but fast
|
|
340 |
version of \isa{arith}. Hence it is usually not necessary to invoke
|
|
341 |
\isa{arith} explicitly.
|
|
342 |
|
|
343 |
The above example involves natural numbers, but integers (type \isa{int})
|
|
344 |
and real numbers (type \isa{real}) are supported as well. As are a number
|
|
345 |
of further operators like \isa{min} and \isa{max}. On \isa{nat} and
|
|
346 |
\isa{int}, \isa{arith} can even prove theorems with quantifiers in them,
|
|
347 |
but we will not enlarge on that here.
|
|
348 |
|
|
349 |
|
|
350 |
\subsection{Single step proofs}
|
|
351 |
|
|
352 |
Although automation is nice, it often fails, at least initially, and you need
|
|
353 |
to find out why. When \isa{fastforce} or \isa{blast} simply fail, you have
|
|
354 |
no clue why. At this point, the stepwise
|
|
355 |
application of proof rules may be necessary. For example, if \isa{blast}
|
|
356 |
fails on \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B}, you want to attack the two
|
|
357 |
conjuncts \isa{A} and \isa{B} separately. This can
|
|
358 |
be achieved by applying \emph{conjunction introduction}
|
|
359 |
\[ \isa{\mbox{}\inferrule{\mbox{{\isaliteral{3F}{\isacharquery}}P}\\\ \mbox{{\isaliteral{3F}{\isacharquery}}Q}}{\mbox{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}Q}}}\ \isa{conjI}
|
|
360 |
\]
|
|
361 |
to the proof state. We will now examine the details of this process.
|
|
362 |
|
|
363 |
\subsubsection{Instantiating unknowns}
|
|
364 |
|
|
365 |
We had briefly mentioned earlier that after proving some theorem,
|
|
366 |
Isabelle replaces all free variables \isa{x} by so called \concept{unknowns}
|
|
367 |
\isa{{\isaliteral{3F}{\isacharquery}}x}. We can see this clearly in rule \isa{conjI}.
|
|
368 |
These unknowns can later be instantiated explicitly or implicitly:
|
|
369 |
\begin{itemize}
|
|
370 |
\item By hand, using \isa{of}.
|
|
371 |
The expression \isa{conjI{\isaliteral{5B}{\isacharbrackleft}}of\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3D}{\isacharequal}}b{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{22}{\isachardoublequote}}False{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}}
|
|
372 |
instantiates the unknowns in \isa{conjI} from left to right with the
|
|
373 |
two formulas \isa{a{\isaliteral{3D}{\isacharequal}}b} and \isa{False}, yielding the rule
|
|
374 |
\begin{isabelle}%
|
|
375 |
\mbox{}\inferrule{\mbox{a\ {\isaliteral{3D}{\isacharequal}}\ b}\\\ \mbox{False}}{\mbox{a\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{5C3C616E643E}{\isasymand}}\ False}}%
|
|
376 |
\end{isabelle}
|
|
377 |
|
|
378 |
In general, \isa{th{\isaliteral{5B}{\isacharbrackleft}}of\ string\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ string\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}} instantiates
|
|
379 |
the unknowns in the theorem \isa{th} from left to right with the terms
|
|
380 |
\isa{string\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}} to \isa{string\isaliteral{5C3C5E697375623E}{}\isactrlisub n}.
|
|
381 |
|
|
382 |
\item By unification. \concept{Unification} is the process of making two
|
|
383 |
terms syntactically equal by suitable instantiations of unknowns. For example,
|
|
384 |
unifying \isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}Q} with \mbox{\isa{a\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{5C3C616E643E}{\isasymand}}\ False}} instantiates
|
|
385 |
\isa{{\isaliteral{3F}{\isacharquery}}P} with \isa{a\ {\isaliteral{3D}{\isacharequal}}\ b} and \isa{{\isaliteral{3F}{\isacharquery}}Q} with \isa{False}.
|
|
386 |
\end{itemize}
|
|
387 |
We need not instantiate all unknowns. If we want to skip a particular one we
|
|
388 |
can just write \isa{{\isaliteral{5F}{\isacharunderscore}}} instead, for example \isa{conjI{\isaliteral{5B}{\isacharbrackleft}}of\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{22}{\isachardoublequote}}False{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}}.
|
|
389 |
Unknowns can also be instantiated by name, for example
|
|
390 |
\isa{conjI{\isaliteral{5B}{\isacharbrackleft}}where\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3D}{\isacharequal}}b{\isaliteral{22}{\isachardoublequote}}\ and\ {\isaliteral{3F}{\isacharquery}}Q\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}False{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}}.
|
|
391 |
|
|
392 |
|
|
393 |
\subsubsection{Rule application}
|
|
394 |
|
|
395 |
\concept{Rule application} means applying a rule backwards to a proof state.
|
|
396 |
For example, applying rule \isa{conjI} to a proof state
|
|
397 |
\begin{quote}
|
|
398 |
\isa{{\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B}
|
|
399 |
\end{quote}
|
|
400 |
results in two subgoals, one for each premise of \isa{conjI}:
|
|
401 |
\begin{quote}
|
|
402 |
\isa{{\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A}\\
|
|
403 |
\isa{{\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ \ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}
|
|
404 |
\end{quote}
|
|
405 |
In general, the application of a rule \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{3B}{\isacharsemicolon}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A}
|
|
406 |
to a subgoal \mbox{\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C}} proceeds in two steps:
|
|
407 |
\begin{enumerate}
|
|
408 |
\item
|
|
409 |
Unify \isa{A} and \isa{C}, thus instantiating the unknowns in the rule.
|
|
410 |
\item
|
|
411 |
Replace the subgoal \isa{C} with \isa{n} new subgoals \isa{A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}} to \isa{A\isaliteral{5C3C5E697375623E}{}\isactrlisub n}.
|
|
412 |
\end{enumerate}
|
|
413 |
This is the command to apply rule \isa{xyz}:
|
|
414 |
\begin{quote}
|
|
415 |
\isacom{apply}\isa{{\isaliteral{28}{\isacharparenleft}}rule\ xyz{\isaliteral{29}{\isacharparenright}}}
|
|
416 |
\end{quote}
|
|
417 |
This is also called \concept{backchaining} with rule \isa{xyz}.
|
|
418 |
|
|
419 |
\subsubsection{Introduction rules}
|
|
420 |
|
|
421 |
Conjunction introduction (\isa{conjI}) is one example of a whole
|
|
422 |
class of rules known as \concept{introduction rules}. They explain under which
|
|
423 |
premises some logical construct can be introduced. Here are some further
|
|
424 |
useful introduction rules:
|
|
425 |
\[
|
|
426 |
\inferrule*[right=\mbox{\isa{impI}}]{\mbox{\isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q}}}{\mbox{\isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q}}}
|
|
427 |
\qquad
|
|
428 |
\inferrule*[right=\mbox{\isa{allI}}]{\mbox{\isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x}}}{\mbox{\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x}}}
|
|
429 |
\]
|
|
430 |
\[
|
|
431 |
\inferrule*[right=\mbox{\isa{iffI}}]{\mbox{\isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q}} \\ \mbox{\isa{{\isaliteral{3F}{\isacharquery}}Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P}}}
|
|
432 |
{\mbox{\isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}Q}}}
|
|
433 |
\]
|
|
434 |
These rules are part of the logical system of \concept{natural deduction}
|
|
435 |
(e.g.\ \cite{HuthRyan}). Although we intentionally de-emphasize the basic rules
|
|
436 |
of logic in favour of automatic proof methods that allow you to take bigger
|
|
437 |
steps, these rules are helpful in locating where and why automation fails.
|
|
438 |
When applied backwards, these rules decompose the goal:
|
|
439 |
\begin{itemize}
|
|
440 |
\item \isa{conjI} and \isa{iffI} split the goal into two subgoals,
|
|
441 |
\item \isa{impI} moves the left-hand side of a HOL implication into the list of assumptions,
|
|
442 |
\item and \isa{allI} removes a \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}} by turning the quantified variable into a fixed local variable of the subgoal.
|
|
443 |
\end{itemize}
|
|
444 |
Isabelle knows about these and a number of other introduction rules.
|
|
445 |
The command
|
|
446 |
\begin{quote}
|
|
447 |
\isacom{apply} \isa{rule}
|
|
448 |
\end{quote}
|
|
449 |
automatically selects the appropriate rule for the current subgoal.
|
|
450 |
|
|
451 |
You can also turn your own theorems into introduction rules by giving them
|
|
452 |
them \isa{intro} attribute, analogous to the \isa{simp} attribute. In
|
|
453 |
that case \isa{blast}, \isa{fastforce} and (to a limited extent) \isa{auto} will automatically backchain with those theorems. The \isa{intro}
|
|
454 |
attribute should be used with care because it increases the search space and
|
|
455 |
can lead to nontermination. Sometimes it is better to use it only in a
|
|
456 |
particular calls of \isa{blast} and friends. For example,
|
|
457 |
\isa{le{\isaliteral{5F}{\isacharunderscore}}trans}, transitivity of \isa{{\isaliteral{5C3C6C653E}{\isasymle}}} on type \isa{nat},
|
|
458 |
is not an introduction rule by default because of the disastrous effect
|
|
459 |
on the search space, but can be useful in specific situations:%
|
|
460 |
\end{isamarkuptext}%
|
|
461 |
\isamarkuptrue%
|
|
462 |
\isacommand{lemma}\isamarkupfalse%
|
|
463 |
\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ b{\isaliteral{3B}{\isacharsemicolon}}\ b\ {\isaliteral{5C3C6C653E}{\isasymle}}\ c{\isaliteral{3B}{\isacharsemicolon}}\ c\ {\isaliteral{5C3C6C653E}{\isasymle}}\ d{\isaliteral{3B}{\isacharsemicolon}}\ d\ {\isaliteral{5C3C6C653E}{\isasymle}}\ e\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ {\isaliteral{5C3C6C653E}{\isasymle}}\ e{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
464 |
%
|
|
465 |
\isadelimproof
|
|
466 |
%
|
|
467 |
\endisadelimproof
|
|
468 |
%
|
|
469 |
\isatagproof
|
|
470 |
\isacommand{by}\isamarkupfalse%
|
|
471 |
{\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{3A}{\isacharcolon}}\ le{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{29}{\isacharparenright}}%
|
|
472 |
\endisatagproof
|
|
473 |
{\isafoldproof}%
|
|
474 |
%
|
|
475 |
\isadelimproof
|
|
476 |
%
|
|
477 |
\endisadelimproof
|
|
478 |
%
|
|
479 |
\begin{isamarkuptext}%
|
|
480 |
Of course this is just an example and could be proved by \isa{arith}, too.
|
|
481 |
|
|
482 |
\subsubsection{Forward proof}
|
|
483 |
\label{sec:forward-proof}
|
|
484 |
|
|
485 |
Forward proof means deriving new theorems from old theorems. We have already
|
|
486 |
seen a very simple form of forward proof: the \isa{of} operator for
|
|
487 |
instantiating unknowns in a theorem. The big brother of \isa{of} is \isa{OF} for applying one theorem to others. Given a theorem \isa{A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B} called
|
|
488 |
\isa{r} and a theorem \isa{A{\isaliteral{27}{\isacharprime}}} called \isa{r{\isaliteral{27}{\isacharprime}}}, the theorem \isa{r{\isaliteral{5B}{\isacharbrackleft}}OF\ r{\isaliteral{27}{\isacharprime}}{\isaliteral{5D}{\isacharbrackright}}} is the result of applying \isa{r} to \isa{r{\isaliteral{27}{\isacharprime}}}, where \isa{r} should be viewed as a function taking a theorem \isa{A} and returning
|
|
489 |
\isa{B}. More precisely, \isa{A} and \isa{A{\isaliteral{27}{\isacharprime}}} are unified, thus
|
|
490 |
instantiating the unknowns in \isa{B}, and the result is the instantiated
|
|
491 |
\isa{B}. Of course, unification may also fail.
|
|
492 |
\begin{warn}
|
|
493 |
Application of rules to other rules operates in the forward direction: from
|
|
494 |
the premises to the conclusion of the rule; application of rules to proof
|
|
495 |
states operates in the backward direction, from the conclusion to the
|
|
496 |
premises.
|
|
497 |
\end{warn}
|
|
498 |
|
|
499 |
In general \isa{r} can be of the form \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{3B}{\isacharsemicolon}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A}
|
|
500 |
and there can be multiple argument theorems \isa{r\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}} to \isa{r\isaliteral{5C3C5E697375623E}{}\isactrlisub m}
|
|
501 |
(with \isa{m\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n}), in which case \isa{r{\isaliteral{5B}{\isacharbrackleft}}OF\ r\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ r\isaliteral{5C3C5E697375623E}{}\isactrlisub m{\isaliteral{5D}{\isacharbrackright}}} is obtained
|
|
502 |
by unifying and thus proving \isa{A\isaliteral{5C3C5E697375623E}{}\isactrlisub i} with \isa{r\isaliteral{5C3C5E697375623E}{}\isactrlisub i}, \isa{i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{5C3C646F74733E}{\isasymdots}}m}.
|
|
503 |
Here is an example, where \isa{refl} is the theorem
|
|
504 |
\isa{{\isaliteral{3F}{\isacharquery}}t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}t}:%
|
|
505 |
\end{isamarkuptext}%
|
|
506 |
\isamarkuptrue%
|
|
507 |
\isacommand{thm}\isamarkupfalse%
|
|
508 |
\ conjI{\isaliteral{5B}{\isacharbrackleft}}OF\ refl{\isaliteral{5B}{\isacharbrackleft}}of\ {\isaliteral{22}{\isachardoublequoteopen}}a{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{5D}{\isacharbrackright}}\ refl{\isaliteral{5B}{\isacharbrackleft}}of\ {\isaliteral{22}{\isachardoublequoteopen}}b{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}%
|
|
509 |
\begin{isamarkuptext}%
|
|
510 |
yields the theorem \isa{a\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{5C3C616E643E}{\isasymand}}\ b\ {\isaliteral{3D}{\isacharequal}}\ b}.
|
|
511 |
The command \isacom{thm} merely displays the result.
|
|
512 |
|
|
513 |
Forward reasoning also makes sense in connection with proof states.
|
|
514 |
Therefore \isa{blast}, \isa{fastforce} and \isa{auto} support a modifier
|
|
515 |
\isa{dest} which instructs the proof method to use certain rules in a
|
|
516 |
forward fashion. If \isa{r} is of the form \mbox{\isa{A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}, the modifier
|
|
517 |
\mbox{\isa{dest{\isaliteral{3A}{\isacharcolon}}\ r}}
|
|
518 |
allows proof search to reason forward with \isa{r}, i.e.\
|
|
519 |
to replace an assumption \isa{A{\isaliteral{27}{\isacharprime}}}, where \isa{A{\isaliteral{27}{\isacharprime}}} unifies with \isa{A},
|
|
520 |
with the correspondingly instantiated \isa{B}. For example, \isa{Suc{\isaliteral{5F}{\isacharunderscore}}leD} is the theorem \mbox{\isa{Suc\ m\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ m\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n}}, which works well for forward reasoning:%
|
|
521 |
\end{isamarkuptext}%
|
|
522 |
\isamarkuptrue%
|
|
523 |
\isacommand{lemma}\isamarkupfalse%
|
|
524 |
\ {\isaliteral{22}{\isachardoublequoteopen}}Suc{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ b\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ {\isaliteral{5C3C6C653E}{\isasymle}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
525 |
%
|
|
526 |
\isadelimproof
|
|
527 |
%
|
|
528 |
\endisadelimproof
|
|
529 |
%
|
|
530 |
\isatagproof
|
|
531 |
\isacommand{by}\isamarkupfalse%
|
|
532 |
{\isaliteral{28}{\isacharparenleft}}blast\ dest{\isaliteral{3A}{\isacharcolon}}\ Suc{\isaliteral{5F}{\isacharunderscore}}leD{\isaliteral{29}{\isacharparenright}}%
|
|
533 |
\endisatagproof
|
|
534 |
{\isafoldproof}%
|
|
535 |
%
|
|
536 |
\isadelimproof
|
|
537 |
%
|
|
538 |
\endisadelimproof
|
|
539 |
%
|
|
540 |
\begin{isamarkuptext}%
|
|
541 |
In this particular example we could have backchained with
|
|
542 |
\isa{Suc{\isaliteral{5F}{\isacharunderscore}}leD}, too, but because the premise is more complicated than the conclusion this can easily lead to nontermination.
|
|
543 |
|
|
544 |
\begin{warn}
|
|
545 |
To ease readability we will drop the question marks
|
|
546 |
in front of unknowns from now on.
|
|
547 |
\end{warn}
|
|
548 |
|
|
549 |
\section{Inductive definitions}
|
|
550 |
\label{sec:inductive-defs}
|
|
551 |
|
|
552 |
Inductive definitions are the third important definition facility, after
|
|
553 |
datatypes and recursive function. In fact, they are the key construct in the
|
|
554 |
definition of operational semantics in the second part of the book.
|
|
555 |
|
|
556 |
\subsection{An example: even numbers}
|
|
557 |
\label{sec:Logic:even}
|
|
558 |
|
|
559 |
Here is a simple example of an inductively defined predicate:
|
|
560 |
\begin{itemize}
|
|
561 |
\item 0 is even
|
|
562 |
\item If $n$ is even, so is $n+2$.
|
|
563 |
\end{itemize}
|
|
564 |
The operative word ``inductive'' means that these are the only even numbers.
|
|
565 |
In Isabelle we give the two rules the names \isa{ev{\isadigit{0}}} and \isa{evSS}
|
|
566 |
and write%
|
|
567 |
\end{isamarkuptext}%
|
|
568 |
\isamarkuptrue%
|
|
569 |
\isacommand{inductive}\isamarkupfalse%
|
|
570 |
\ ev\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
|
|
571 |
ev{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}ev\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
572 |
evSS{\isaliteral{3A}{\isacharcolon}}\ \ %
|
47306
|
573 |
\isa{{\isaliteral{22}{\isachardoublequote}}ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
|
47269
|
574 |
%
|
|
575 |
\begin{isamarkuptext}%
|
|
576 |
To get used to inductive definitions, we will first prove a few
|
|
577 |
properties of \isa{ev} informally before we descend to the Isabelle level.
|
|
578 |
|
|
579 |
How do we prove that some number is even, e.g.\ \isa{ev\ {\isadigit{4}}}? Simply by combining the defining rules for \isa{ev}:
|
|
580 |
\begin{quote}
|
|
581 |
\isa{ev\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ev\ {\isadigit{4}}}
|
|
582 |
\end{quote}
|
|
583 |
|
|
584 |
\subsubsection{Rule induction}
|
|
585 |
|
|
586 |
Showing that all even numbers have some property is more complicated. For
|
|
587 |
example, let us prove that the inductive definition of even numbers agrees
|
|
588 |
with the following recursive one:%
|
|
589 |
\end{isamarkuptext}%
|
|
590 |
\isamarkuptrue%
|
|
591 |
\isacommand{fun}\isamarkupfalse%
|
|
592 |
\ even\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
|
|
593 |
{\isaliteral{22}{\isachardoublequoteopen}}even\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ True{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
594 |
{\isaliteral{22}{\isachardoublequoteopen}}even\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ False{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
595 |
{\isaliteral{22}{\isachardoublequoteopen}}even\ {\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ even\ n{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
596 |
\begin{isamarkuptext}%
|
|
597 |
We prove \isa{ev\ m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ even\ m}. That is, we
|
|
598 |
assume \isa{ev\ m} and by induction on the form of its derivation
|
|
599 |
prove \isa{even\ m}. There are two cases corresponding to the two rules
|
|
600 |
for \isa{ev}:
|
|
601 |
\begin{description}
|
|
602 |
\item[Case \isa{ev{\isadigit{0}}}:]
|
|
603 |
\isa{ev\ m} was derived by rule \isa{ev\ {\isadigit{0}}}: \\
|
|
604 |
\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} \isa{m\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} \isa{even\ m\ {\isaliteral{3D}{\isacharequal}}\ even\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ True}
|
|
605 |
\item[Case \isa{evSS}:]
|
|
606 |
\isa{ev\ m} was derived by rule \isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}: \\
|
|
607 |
\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} \isa{m\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}} and by induction hypothesis \isa{even\ n}\\
|
|
608 |
\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} \isa{even\ m\ {\isaliteral{3D}{\isacharequal}}\ even{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ even\ n\ {\isaliteral{3D}{\isacharequal}}\ True}
|
|
609 |
\end{description}
|
|
610 |
|
|
611 |
What we have just seen is a special case of \concept{rule induction}.
|
|
612 |
Rule induction applies to propositions of this form
|
|
613 |
\begin{quote}
|
|
614 |
\isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n}
|
|
615 |
\end{quote}
|
|
616 |
That is, we want to prove a property \isa{P\ n}
|
|
617 |
for all even \isa{n}. But if we assume \isa{ev\ n}, then there must be
|
|
618 |
some derivation of this assumption using the two defining rules for
|
|
619 |
\isa{ev}. That is, we must prove
|
|
620 |
\begin{description}
|
|
621 |
\item[Case \isa{ev{\isadigit{0}}}:] \isa{P\ {\isadigit{0}}}
|
|
622 |
\item[Case \isa{evSS}:] \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}ev\ n{\isaliteral{3B}{\isacharsemicolon}}\ P\ n{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}
|
|
623 |
\end{description}
|
|
624 |
The corresponding rule is called \isa{ev{\isaliteral{2E}{\isachardot}}induct} and looks like this:
|
|
625 |
\[
|
|
626 |
\inferrule{
|
|
627 |
\mbox{\isa{ev\ n}}\\
|
|
628 |
\mbox{\isa{P\ {\isadigit{0}}}}\\
|
|
629 |
\mbox{\isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}ev\ n{\isaliteral{3B}{\isacharsemicolon}}\ P\ n{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}}}
|
|
630 |
{\mbox{\isa{P\ n}}}
|
|
631 |
\]
|
|
632 |
The first premise \isa{ev\ n} enforces that this rule can only be applied
|
|
633 |
in situations where we know that \isa{n} is even.
|
|
634 |
|
|
635 |
Note that in the induction step we may not just assume \isa{P\ n} but also
|
|
636 |
\mbox{\isa{ev\ n}}, which is simply the premise of rule \isa{evSS}. Here is an example where the local assumption \isa{ev\ n} comes in
|
|
637 |
handy: we prove \isa{ev\ m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} by induction on \isa{ev\ m}.
|
|
638 |
Case \isa{ev{\isadigit{0}}} requires us to prove \isa{ev\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}, which follows
|
|
639 |
from \isa{ev\ {\isadigit{0}}} because \isa{{\isadigit{0}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} on type \isa{nat}. In
|
|
640 |
case \isa{evSS} we have \mbox{\isa{m\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}}} and may assume
|
|
641 |
\isa{ev\ n}, which implies \isa{ev\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} because \isa{m\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ n}. We did not need the induction hypothesis at all for this proof,
|
|
642 |
it is just a case distinction on which rule was used, but having \isa{ev\ n} at our disposal in case \isa{evSS} was essential.
|
|
643 |
This case distinction over rules is also called ``rule inversion''
|
|
644 |
and is discussed in more detail in \autoref{ch:Isar}.
|
|
645 |
|
|
646 |
\subsubsection{In Isabelle}
|
|
647 |
|
|
648 |
Let us now recast the above informal proofs in Isabelle. For a start,
|
|
649 |
we use \isa{Suc} terms instead of numerals in rule \isa{evSS}:
|
|
650 |
\begin{isabelle}%
|
|
651 |
ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
|
|
652 |
\end{isabelle}
|
|
653 |
This avoids the difficulty of unifying \isa{n{\isaliteral{2B}{\isacharplus}}{\isadigit{2}}} with some numeral,
|
|
654 |
which is not automatic.
|
|
655 |
|
|
656 |
The simplest way to prove \isa{ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}} is in a forward
|
|
657 |
direction: \isa{evSS{\isaliteral{5B}{\isacharbrackleft}}OF\ evSS{\isaliteral{5B}{\isacharbrackleft}}OF\ ev{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}} yields the theorem \isa{ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}. Alternatively, you can also prove it as a lemma in backwards
|
|
658 |
fashion. Although this is more verbose, it allows us to demonstrate how each
|
|
659 |
rule application changes the proof state:%
|
|
660 |
\end{isamarkuptext}%
|
|
661 |
\isamarkuptrue%
|
|
662 |
\isacommand{lemma}\isamarkupfalse%
|
|
663 |
\ {\isaliteral{22}{\isachardoublequoteopen}}ev{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
664 |
\isadelimproof
|
|
665 |
%
|
|
666 |
\endisadelimproof
|
|
667 |
%
|
|
668 |
\isatagproof
|
|
669 |
%
|
|
670 |
\begin{isamarkuptxt}%
|
|
671 |
\begin{isabelle}%
|
|
672 |
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
|
|
673 |
\end{isabelle}%
|
|
674 |
\end{isamarkuptxt}%
|
|
675 |
\isamarkuptrue%
|
|
676 |
\isacommand{apply}\isamarkupfalse%
|
|
677 |
{\isaliteral{28}{\isacharparenleft}}rule\ evSS{\isaliteral{29}{\isacharparenright}}%
|
|
678 |
\begin{isamarkuptxt}%
|
|
679 |
\begin{isabelle}%
|
|
680 |
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
|
|
681 |
\end{isabelle}%
|
|
682 |
\end{isamarkuptxt}%
|
|
683 |
\isamarkuptrue%
|
|
684 |
\isacommand{apply}\isamarkupfalse%
|
|
685 |
{\isaliteral{28}{\isacharparenleft}}rule\ evSS{\isaliteral{29}{\isacharparenright}}%
|
|
686 |
\begin{isamarkuptxt}%
|
|
687 |
\begin{isabelle}%
|
|
688 |
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ ev\ {\isadigit{0}}%
|
|
689 |
\end{isabelle}%
|
|
690 |
\end{isamarkuptxt}%
|
|
691 |
\isamarkuptrue%
|
|
692 |
\isacommand{apply}\isamarkupfalse%
|
|
693 |
{\isaliteral{28}{\isacharparenleft}}rule\ ev{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
|
|
694 |
\isacommand{done}\isamarkupfalse%
|
|
695 |
%
|
|
696 |
\endisatagproof
|
|
697 |
{\isafoldproof}%
|
|
698 |
%
|
|
699 |
\isadelimproof
|
|
700 |
%
|
|
701 |
\endisadelimproof
|
|
702 |
%
|
|
703 |
\begin{isamarkuptext}%
|
|
704 |
\indent
|
|
705 |
Rule induction is applied by giving the induction rule explicitly via the
|
|
706 |
\isa{rule{\isaliteral{3A}{\isacharcolon}}} modifier:%
|
|
707 |
\end{isamarkuptext}%
|
|
708 |
\isamarkuptrue%
|
|
709 |
\isacommand{lemma}\isamarkupfalse%
|
|
710 |
\ {\isaliteral{22}{\isachardoublequoteopen}}ev\ m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ even\ m{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
711 |
%
|
|
712 |
\isadelimproof
|
|
713 |
%
|
|
714 |
\endisadelimproof
|
|
715 |
%
|
|
716 |
\isatagproof
|
|
717 |
\isacommand{apply}\isamarkupfalse%
|
|
718 |
{\isaliteral{28}{\isacharparenleft}}induction\ rule{\isaliteral{3A}{\isacharcolon}}\ ev{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline
|
|
719 |
\isacommand{by}\isamarkupfalse%
|
|
720 |
{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}%
|
|
721 |
\endisatagproof
|
|
722 |
{\isafoldproof}%
|
|
723 |
%
|
|
724 |
\isadelimproof
|
|
725 |
%
|
|
726 |
\endisadelimproof
|
|
727 |
%
|
|
728 |
\begin{isamarkuptext}%
|
|
729 |
Both cases are automatic. Note that if there are multiple assumptions
|
|
730 |
of the form \isa{ev\ t}, method \isa{induction} will induct on the leftmost
|
|
731 |
one.
|
|
732 |
|
|
733 |
As a bonus, we also prove the remaining direction of the equivalence of
|
|
734 |
\isa{ev} and \isa{even}:%
|
|
735 |
\end{isamarkuptext}%
|
|
736 |
\isamarkuptrue%
|
|
737 |
\isacommand{lemma}\isamarkupfalse%
|
|
738 |
\ {\isaliteral{22}{\isachardoublequoteopen}}even\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
739 |
%
|
|
740 |
\isadelimproof
|
|
741 |
%
|
|
742 |
\endisadelimproof
|
|
743 |
%
|
|
744 |
\isatagproof
|
|
745 |
\isacommand{apply}\isamarkupfalse%
|
|
746 |
{\isaliteral{28}{\isacharparenleft}}induction\ n\ rule{\isaliteral{3A}{\isacharcolon}}\ even{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}%
|
|
747 |
\begin{isamarkuptxt}%
|
|
748 |
This is a proof by computation induction on \isa{n} (see
|
|
749 |
\autoref{sec:recursive-funs}) that sets up three subgoals corresponding to
|
|
750 |
the three equations for \isa{even}:
|
|
751 |
\begin{isabelle}%
|
|
752 |
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ even\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isadigit{0}}\isanewline
|
|
753 |
\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ even\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
|
|
754 |
\ {\isadigit{3}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}even\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ n{\isaliteral{3B}{\isacharsemicolon}}\ even\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
|
|
755 |
\end{isabelle}
|
|
756 |
The first and third subgoals follow with \isa{ev{\isadigit{0}}} and \isa{evSS}, and the second subgoal is trivially true because \isa{even\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}} is \isa{False}:%
|
|
757 |
\end{isamarkuptxt}%
|
|
758 |
\isamarkuptrue%
|
|
759 |
\isacommand{by}\isamarkupfalse%
|
|
760 |
\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ ev{\isadigit{0}}\ evSS{\isaliteral{29}{\isacharparenright}}%
|
|
761 |
\endisatagproof
|
|
762 |
{\isafoldproof}%
|
|
763 |
%
|
|
764 |
\isadelimproof
|
|
765 |
%
|
|
766 |
\endisadelimproof
|
|
767 |
%
|
|
768 |
\begin{isamarkuptext}%
|
|
769 |
The rules for \isa{ev} make perfect simplification and introduction
|
|
770 |
rules because their premises are always smaller than the conclusion. It
|
|
771 |
makes sense to turn them into simplification and introduction rules
|
|
772 |
permanently, to enhance proof automation:%
|
|
773 |
\end{isamarkuptext}%
|
|
774 |
\isamarkuptrue%
|
|
775 |
\isacommand{declare}\isamarkupfalse%
|
|
776 |
\ ev{\isaliteral{2E}{\isachardot}}intros{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{2C}{\isacharcomma}}intro{\isaliteral{5D}{\isacharbrackright}}%
|
|
777 |
\begin{isamarkuptext}%
|
|
778 |
The rules of an inductive definition are not simplification rules by
|
|
779 |
default because, in contrast to recursive functions, there is no termination
|
|
780 |
requirement for inductive definitions.
|
|
781 |
|
|
782 |
\subsubsection{Inductive versus recursive}
|
|
783 |
|
|
784 |
We have seen two definitions of the notion of evenness, an inductive and a
|
|
785 |
recursive one. Which one is better? Much of the time, the recursive one is
|
|
786 |
more convenient: it allows us to do rewriting in the middle of terms, and it
|
|
787 |
expresses both the positive information (which numbers are even) and the
|
|
788 |
negative information (which numbers are not even) directly. An inductive
|
|
789 |
definition only expresses the positive information directly. The negative
|
|
790 |
information, for example, that \isa{{\isadigit{1}}} is not even, has to be proved from
|
|
791 |
it (by induction or rule inversion). On the other hand, rule induction is
|
|
792 |
Taylor made for proving \mbox{\isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n}} because it only asks you
|
|
793 |
to prove the positive cases. In the proof of \isa{even\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n} by
|
|
794 |
computation induction via \isa{even{\isaliteral{2E}{\isachardot}}induct}, we are also presented
|
|
795 |
with the trivial negative cases. If you want the convenience of both
|
|
796 |
rewriting and rule induction, you can make two definitions and show their
|
|
797 |
equivalence (as above) or make one definition and prove additional properties
|
|
798 |
from it, for example rule induction from computation induction.
|
|
799 |
|
|
800 |
But many concepts do not admit a recursive definition at all because there is
|
|
801 |
no datatype for the recursion (for example, the transitive closure of a
|
|
802 |
relation), or the recursion would not terminate (for example, the operational
|
|
803 |
semantics in the second part of this book). Even if there is a recursive
|
|
804 |
definition, if we are only interested in the positive information, the
|
|
805 |
inductive definition may be much simpler.
|
|
806 |
|
|
807 |
\subsection{The reflexive transitive closure}
|
|
808 |
\label{sec:star}
|
|
809 |
|
|
810 |
Evenness is really more conveniently expressed recursively than inductively.
|
|
811 |
As a second and very typical example of an inductive definition we define the
|
|
812 |
reflexive transitive closure. It will also be an important building block for
|
|
813 |
some of the semantics considered in the second part of the book.
|
|
814 |
|
|
815 |
The reflexive transitive closure, called \isa{star} below, is a function
|
|
816 |
that maps a binary predicate to another binary predicate: if \isa{r} is of
|
|
817 |
type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} then \isa{star\ r} is again of type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}, and \isa{star\ r\ x\ y} means that \isa{x} and \isa{y} are in
|
|
818 |
the relation \isa{star\ r}. Think \isa{r\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}} when you see \isa{star\ r}, because \isa{star\ r} is meant to be the reflexive transitive closure.
|
|
819 |
That is, \isa{star\ r\ x\ y} is meant to be true if from \isa{x} we can
|
|
820 |
reach \isa{y} in finitely many \isa{r} steps. This concept is naturally
|
|
821 |
defined inductively:%
|
|
822 |
\end{isamarkuptext}%
|
|
823 |
\isamarkuptrue%
|
|
824 |
\isacommand{inductive}\isamarkupfalse%
|
|
825 |
\ star\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \isakeyword{for}\ r\ \isakeyword{where}\isanewline
|
|
826 |
refl{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}star\ r\ x\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
827 |
step{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}r\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ star\ r\ y\ z\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ star\ r\ x\ z{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
828 |
\begin{isamarkuptext}%
|
|
829 |
The base case \isa{refl} is reflexivity: \isa{x\ {\isaliteral{3D}{\isacharequal}}\ y}. The
|
|
830 |
step case \isa{step} combines an \isa{r} step (from \isa{x} to
|
|
831 |
\isa{y}) and a \isa{star} step (from \isa{y} to \isa{z}) into a
|
|
832 |
\isa{star} step (from \isa{x} to \isa{z}).
|
|
833 |
The ``\isacom{for}~\isa{r}'' in the header is merely a hint to Isabelle
|
|
834 |
that \isa{r} is a fixed parameter of \isa{star}, in contrast to the
|
|
835 |
further parameters of \isa{star}, which change. As a result, Isabelle
|
|
836 |
generates a simpler induction rule.
|
|
837 |
|
|
838 |
By definition \isa{star\ r} is reflexive. It is also transitive, but we
|
|
839 |
need rule induction to prove that:%
|
|
840 |
\end{isamarkuptext}%
|
|
841 |
\isamarkuptrue%
|
|
842 |
\isacommand{lemma}\isamarkupfalse%
|
|
843 |
\ star{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}star\ r\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ star\ r\ y\ z\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ star\ r\ x\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
844 |
%
|
|
845 |
\isadelimproof
|
|
846 |
%
|
|
847 |
\endisadelimproof
|
|
848 |
%
|
|
849 |
\isatagproof
|
|
850 |
\isacommand{apply}\isamarkupfalse%
|
|
851 |
{\isaliteral{28}{\isacharparenleft}}induction\ rule{\isaliteral{3A}{\isacharcolon}}\ star{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}%
|
|
852 |
\begin{isamarkuptxt}%
|
|
853 |
The induction is over \isa{star\ r\ x\ y} and we try to prove
|
|
854 |
\mbox{\isa{star\ r\ y\ z\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ star\ r\ x\ z}},
|
|
855 |
which we abbreviate by \isa{P\ x\ y}. These are our two subgoals:
|
|
856 |
\begin{isabelle}%
|
|
857 |
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ star\ r\ x\ z\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ star\ r\ x\ z\isanewline
|
|
858 |
\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}u\ x\ y{\isaliteral{2E}{\isachardot}}\isanewline
|
|
859 |
\isaindent{\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}r\ u\ x{\isaliteral{3B}{\isacharsemicolon}}\ star\ r\ x\ y{\isaliteral{3B}{\isacharsemicolon}}\ star\ r\ y\ z\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ star\ r\ x\ z{\isaliteral{3B}{\isacharsemicolon}}\ star\ r\ y\ z{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
|
|
860 |
\isaindent{\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ star\ r\ u\ z%
|
|
861 |
\end{isabelle}
|
|
862 |
The first one is \isa{P\ x\ x}, the result of case \isa{refl},
|
|
863 |
and it is trivial.%
|
|
864 |
\end{isamarkuptxt}%
|
|
865 |
\isamarkuptrue%
|
|
866 |
\isacommand{apply}\isamarkupfalse%
|
|
867 |
{\isaliteral{28}{\isacharparenleft}}assumption{\isaliteral{29}{\isacharparenright}}%
|
|
868 |
\begin{isamarkuptxt}%
|
|
869 |
Let us examine subgoal \isa{{\isadigit{2}}}, case \isa{step}.
|
|
870 |
Assumptions \isa{r\ u\ x} and \mbox{\isa{star\ r\ x\ y}}
|
|
871 |
are the premises of rule \isa{step}.
|
|
872 |
Assumption \isa{star\ r\ y\ z\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ star\ r\ x\ z} is \mbox{\isa{P\ x\ y}},
|
|
873 |
the IH coming from \isa{star\ r\ x\ y}. We have to prove \isa{P\ u\ y},
|
|
874 |
which we do by assuming \isa{star\ r\ y\ z} and proving \isa{star\ r\ u\ z}.
|
|
875 |
The proof itself is straightforward: from \mbox{\isa{star\ r\ y\ z}} the IH
|
|
876 |
leads to \isa{star\ r\ x\ z} which, together with \isa{r\ u\ x},
|
|
877 |
leads to \mbox{\isa{star\ r\ u\ z}} via rule \isa{step}:%
|
|
878 |
\end{isamarkuptxt}%
|
|
879 |
\isamarkuptrue%
|
|
880 |
\isacommand{apply}\isamarkupfalse%
|
|
881 |
{\isaliteral{28}{\isacharparenleft}}metis\ step{\isaliteral{29}{\isacharparenright}}\isanewline
|
|
882 |
\isacommand{done}\isamarkupfalse%
|
|
883 |
%
|
|
884 |
\endisatagproof
|
|
885 |
{\isafoldproof}%
|
|
886 |
%
|
|
887 |
\isadelimproof
|
|
888 |
%
|
|
889 |
\endisadelimproof
|
|
890 |
%
|
|
891 |
\begin{isamarkuptext}%
|
|
892 |
\subsection{The general case}
|
|
893 |
|
|
894 |
Inductive definitions have approximately the following general form:
|
|
895 |
\begin{quote}
|
|
896 |
\isacom{inductive} \isa{I\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequote}}} \isacom{where}
|
|
897 |
\end{quote}
|
|
898 |
followed by a sequence of (possibly named) rules of the form
|
|
899 |
\begin{quote}
|
|
900 |
\isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ I\ a\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{3B}{\isacharsemicolon}}\ I\ a\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ I\ a}
|
|
901 |
\end{quote}
|
|
902 |
separated by \isa{{\isaliteral{7C}{\isacharbar}}}. As usual, \isa{n} can be 0.
|
|
903 |
The corresponding rule induction principle
|
|
904 |
\isa{I{\isaliteral{2E}{\isachardot}}induct} applies to propositions of the form
|
|
905 |
\begin{quote}
|
|
906 |
\isa{I\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x}
|
|
907 |
\end{quote}
|
|
908 |
where \isa{P} may itself be a chain of implications.
|
|
909 |
\begin{warn}
|
|
910 |
Rule induction is always on the leftmost premise of the goal.
|
|
911 |
Hence \isa{I\ x} must be the first premise.
|
|
912 |
\end{warn}
|
|
913 |
Proving \isa{I\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x} by rule induction means proving
|
|
914 |
for every rule of \isa{I} that \isa{P} is invariant:
|
|
915 |
\begin{quote}
|
|
916 |
\isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ I\ a\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ P\ a\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{3B}{\isacharsemicolon}}\ I\ a\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{3B}{\isacharsemicolon}}\ P\ a\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ a}
|
|
917 |
\end{quote}
|
|
918 |
|
|
919 |
The above format for inductive definitions is simplified in a number of
|
|
920 |
respects. \isa{I} can have any number of arguments and each rule can have
|
|
921 |
additional premises not involving \isa{I}, so-called \concept{side
|
|
922 |
conditions}. In rule inductions, these side-conditions appear as additional
|
|
923 |
assumptions. The \isacom{for} clause seen in the definition of the reflexive
|
|
924 |
transitive closure merely simplifies the form of the induction rule.%
|
|
925 |
\end{isamarkuptext}%
|
|
926 |
\isamarkuptrue%
|
|
927 |
%
|
|
928 |
\isadelimtheory
|
|
929 |
%
|
|
930 |
\endisadelimtheory
|
|
931 |
%
|
|
932 |
\isatagtheory
|
|
933 |
%
|
|
934 |
\endisatagtheory
|
|
935 |
{\isafoldtheory}%
|
|
936 |
%
|
|
937 |
\isadelimtheory
|
|
938 |
%
|
|
939 |
\endisadelimtheory
|
|
940 |
\end{isabellebody}%
|
|
941 |
%%% Local Variables:
|
|
942 |
%%% mode: latex
|
|
943 |
%%% TeX-master: "root"
|
|
944 |
%%% End:
|