paulson@30036
|
1 |
%!TEX root = logics-ZF.tex
|
paulson@6121
|
2 |
\chapter{First-Order Logic}
|
paulson@6121
|
3 |
\index{first-order logic|(}
|
paulson@6121
|
4 |
|
paulson@6121
|
5 |
Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc
|
paulson@6121
|
6 |
nk}. Intuitionistic first-order logic is defined first, as theory
|
paulson@6121
|
7 |
\thydx{IFOL}. Classical logic, theory \thydx{FOL}, is
|
paulson@6121
|
8 |
obtained by adding the double negation rule. Basic proof procedures are
|
paulson@6121
|
9 |
provided. The intuitionistic prover works with derived rules to simplify
|
paulson@6121
|
10 |
implications in the assumptions. Classical~\texttt{FOL} employs Isabelle's
|
paulson@6121
|
11 |
classical reasoner, which simulates a sequent calculus.
|
paulson@6121
|
12 |
|
paulson@6121
|
13 |
\section{Syntax and rules of inference}
|
paulson@6121
|
14 |
The logic is many-sorted, using Isabelle's type classes. The class of
|
paulson@14154
|
15 |
first-order terms is called \cldx{term} and is a subclass of \isa{logic}.
|
paulson@6121
|
16 |
No types of individuals are provided, but extensions can define types such
|
paulson@14154
|
17 |
as \isa{nat::term} and type constructors such as \isa{list::(term)term}
|
paulson@6121
|
18 |
(see the examples directory, \texttt{FOL/ex}). Below, the type variable
|
paulson@14154
|
19 |
$\alpha$ ranges over class \isa{term}; the equality symbol and quantifiers
|
paulson@6121
|
20 |
are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which
|
paulson@6121
|
21 |
belongs to class~\cldx{logic}. Figure~\ref{fol-syntax} gives the syntax.
|
paulson@6121
|
22 |
Note that $a$\verb|~=|$b$ is translated to $\neg(a=b)$.
|
paulson@6121
|
23 |
|
paulson@14154
|
24 |
Figure~\ref{fol-rules} shows the inference rules with their names.
|
paulson@6121
|
25 |
Negation is defined in the usual way for intuitionistic logic; $\neg P$
|
paulson@6121
|
26 |
abbreviates $P\imp\bot$. The biconditional~($\bimp$) is defined through
|
paulson@6121
|
27 |
$\conj$ and~$\imp$; introduction and elimination rules are derived for it.
|
paulson@6121
|
28 |
|
paulson@6121
|
29 |
The unique existence quantifier, $\exists!x.P(x)$, is defined in terms
|
paulson@6121
|
30 |
of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
|
paulson@6121
|
31 |
quantifications. For instance, $\exists!x\;y.P(x,y)$ abbreviates
|
paulson@6121
|
32 |
$\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
|
paulson@6121
|
33 |
exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
|
paulson@6121
|
34 |
|
paulson@6121
|
35 |
Some intuitionistic derived rules are shown in
|
paulson@14154
|
36 |
Fig.\ts\ref{fol-int-derived}, again with their names. These include
|
paulson@6121
|
37 |
rules for the defined symbols $\neg$, $\bimp$ and $\exists!$. Natural
|
paulson@6121
|
38 |
deduction typically involves a combination of forward and backward
|
paulson@6121
|
39 |
reasoning, particularly with the destruction rules $(\conj E)$,
|
paulson@6121
|
40 |
$({\imp}E)$, and~$(\forall E)$. Isabelle's backward style handles these
|
paulson@6121
|
41 |
rules badly, so sequent-style rules are derived to eliminate conjunctions,
|
paulson@6121
|
42 |
implications, and universal quantifiers. Used with elim-resolution,
|
paulson@6121
|
43 |
\tdx{allE} eliminates a universal quantifier while \tdx{all_dupE}
|
paulson@14154
|
44 |
re-inserts the quantified formula for later use. The rules
|
paulson@14154
|
45 |
\isa{conj\_impE}, etc., support the intuitionistic proof procedure
|
paulson@6121
|
46 |
(see~\S\ref{fol-int-prover}).
|
paulson@6121
|
47 |
|
paulson@14154
|
48 |
See the on-line theory library for complete listings of the rules and
|
paulson@6121
|
49 |
derived rules.
|
paulson@6121
|
50 |
|
paulson@6121
|
51 |
\begin{figure}
|
paulson@6121
|
52 |
\begin{center}
|
paulson@6121
|
53 |
\begin{tabular}{rrr}
|
paulson@6121
|
54 |
\it name &\it meta-type & \it description \\
|
paulson@6121
|
55 |
\cdx{Trueprop}& $o\To prop$ & coercion to $prop$\\
|
paulson@6121
|
56 |
\cdx{Not} & $o\To o$ & negation ($\neg$) \\
|
paulson@6121
|
57 |
\cdx{True} & $o$ & tautology ($\top$) \\
|
paulson@6121
|
58 |
\cdx{False} & $o$ & absurdity ($\bot$)
|
paulson@6121
|
59 |
\end{tabular}
|
paulson@6121
|
60 |
\end{center}
|
paulson@6121
|
61 |
\subcaption{Constants}
|
paulson@6121
|
62 |
|
paulson@6121
|
63 |
\begin{center}
|
paulson@6121
|
64 |
\begin{tabular}{llrrr}
|
paulson@6121
|
65 |
\it symbol &\it name &\it meta-type & \it priority & \it description \\
|
paulson@6121
|
66 |
\sdx{ALL} & \cdx{All} & $(\alpha\To o)\To o$ & 10 &
|
paulson@6121
|
67 |
universal quantifier ($\forall$) \\
|
paulson@6121
|
68 |
\sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 &
|
paulson@6121
|
69 |
existential quantifier ($\exists$) \\
|
paulson@14154
|
70 |
\isa{EX!} & \cdx{Ex1} & $(\alpha\To o)\To o$ & 10 &
|
paulson@6121
|
71 |
unique existence ($\exists!$)
|
paulson@6121
|
72 |
\end{tabular}
|
paulson@6121
|
73 |
\index{*"E"X"! symbol}
|
paulson@6121
|
74 |
\end{center}
|
paulson@6121
|
75 |
\subcaption{Binders}
|
paulson@6121
|
76 |
|
paulson@6121
|
77 |
\begin{center}
|
paulson@6121
|
78 |
\index{*"= symbol}
|
paulson@6121
|
79 |
\index{&@{\tt\&} symbol}
|
paulson@6121
|
80 |
\index{*"| symbol}
|
paulson@6121
|
81 |
\index{*"-"-"> symbol}
|
paulson@6121
|
82 |
\index{*"<"-"> symbol}
|
paulson@6121
|
83 |
\begin{tabular}{rrrr}
|
paulson@6121
|
84 |
\it symbol & \it meta-type & \it priority & \it description \\
|
paulson@6121
|
85 |
\tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\
|
paulson@6121
|
86 |
\tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\
|
paulson@6121
|
87 |
\tt | & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\
|
paulson@6121
|
88 |
\tt --> & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\
|
paulson@6121
|
89 |
\tt <-> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$)
|
paulson@6121
|
90 |
\end{tabular}
|
paulson@6121
|
91 |
\end{center}
|
paulson@6121
|
92 |
\subcaption{Infixes}
|
paulson@6121
|
93 |
|
paulson@6121
|
94 |
\dquotes
|
paulson@6121
|
95 |
\[\begin{array}{rcl}
|
paulson@6121
|
96 |
formula & = & \hbox{expression of type~$o$} \\
|
paulson@6121
|
97 |
& | & term " = " term \quad| \quad term " \ttilde= " term \\
|
paulson@6121
|
98 |
& | & "\ttilde\ " formula \\
|
paulson@6121
|
99 |
& | & formula " \& " formula \\
|
paulson@6121
|
100 |
& | & formula " | " formula \\
|
paulson@6121
|
101 |
& | & formula " --> " formula \\
|
paulson@6121
|
102 |
& | & formula " <-> " formula \\
|
paulson@6121
|
103 |
& | & "ALL~" id~id^* " . " formula \\
|
paulson@6121
|
104 |
& | & "EX~~" id~id^* " . " formula \\
|
paulson@6121
|
105 |
& | & "EX!~" id~id^* " . " formula
|
paulson@6121
|
106 |
\end{array}
|
paulson@6121
|
107 |
\]
|
paulson@6121
|
108 |
\subcaption{Grammar}
|
paulson@6121
|
109 |
\caption{Syntax of \texttt{FOL}} \label{fol-syntax}
|
paulson@6121
|
110 |
\end{figure}
|
paulson@6121
|
111 |
|
paulson@6121
|
112 |
|
paulson@6121
|
113 |
\begin{figure}
|
paulson@6121
|
114 |
\begin{ttbox}
|
paulson@6121
|
115 |
\tdx{refl} a=a
|
paulson@6121
|
116 |
\tdx{subst} [| a=b; P(a) |] ==> P(b)
|
paulson@6121
|
117 |
\subcaption{Equality rules}
|
paulson@6121
|
118 |
|
paulson@6121
|
119 |
\tdx{conjI} [| P; Q |] ==> P&Q
|
paulson@6121
|
120 |
\tdx{conjunct1} P&Q ==> P
|
paulson@6121
|
121 |
\tdx{conjunct2} P&Q ==> Q
|
paulson@6121
|
122 |
|
paulson@6121
|
123 |
\tdx{disjI1} P ==> P|Q
|
paulson@6121
|
124 |
\tdx{disjI2} Q ==> P|Q
|
paulson@6121
|
125 |
\tdx{disjE} [| P|Q; P ==> R; Q ==> R |] ==> R
|
paulson@6121
|
126 |
|
paulson@6121
|
127 |
\tdx{impI} (P ==> Q) ==> P-->Q
|
paulson@6121
|
128 |
\tdx{mp} [| P-->Q; P |] ==> Q
|
paulson@6121
|
129 |
|
paulson@6121
|
130 |
\tdx{FalseE} False ==> P
|
paulson@6121
|
131 |
\subcaption{Propositional rules}
|
paulson@6121
|
132 |
|
paulson@6121
|
133 |
\tdx{allI} (!!x. P(x)) ==> (ALL x.P(x))
|
paulson@6121
|
134 |
\tdx{spec} (ALL x.P(x)) ==> P(x)
|
paulson@6121
|
135 |
|
paulson@6121
|
136 |
\tdx{exI} P(x) ==> (EX x.P(x))
|
paulson@6121
|
137 |
\tdx{exE} [| EX x.P(x); !!x. P(x) ==> R |] ==> R
|
paulson@6121
|
138 |
\subcaption{Quantifier rules}
|
paulson@6121
|
139 |
|
paulson@6121
|
140 |
\tdx{True_def} True == False-->False
|
paulson@6121
|
141 |
\tdx{not_def} ~P == P-->False
|
paulson@6121
|
142 |
\tdx{iff_def} P<->Q == (P-->Q) & (Q-->P)
|
paulson@6121
|
143 |
\tdx{ex1_def} EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)
|
paulson@6121
|
144 |
\subcaption{Definitions}
|
paulson@6121
|
145 |
\end{ttbox}
|
paulson@6121
|
146 |
|
paulson@6121
|
147 |
\caption{Rules of intuitionistic logic} \label{fol-rules}
|
paulson@6121
|
148 |
\end{figure}
|
paulson@6121
|
149 |
|
paulson@6121
|
150 |
|
paulson@6121
|
151 |
\begin{figure}
|
paulson@6121
|
152 |
\begin{ttbox}
|
paulson@6121
|
153 |
\tdx{sym} a=b ==> b=a
|
paulson@6121
|
154 |
\tdx{trans} [| a=b; b=c |] ==> a=c
|
paulson@6121
|
155 |
\tdx{ssubst} [| b=a; P(a) |] ==> P(b)
|
paulson@6121
|
156 |
\subcaption{Derived equality rules}
|
paulson@6121
|
157 |
|
paulson@6121
|
158 |
\tdx{TrueI} True
|
paulson@6121
|
159 |
|
paulson@6121
|
160 |
\tdx{notI} (P ==> False) ==> ~P
|
paulson@6121
|
161 |
\tdx{notE} [| ~P; P |] ==> R
|
paulson@6121
|
162 |
|
paulson@6121
|
163 |
\tdx{iffI} [| P ==> Q; Q ==> P |] ==> P<->Q
|
paulson@6121
|
164 |
\tdx{iffE} [| P <-> Q; [| P-->Q; Q-->P |] ==> R |] ==> R
|
paulson@6121
|
165 |
\tdx{iffD1} [| P <-> Q; P |] ==> Q
|
paulson@6121
|
166 |
\tdx{iffD2} [| P <-> Q; Q |] ==> P
|
paulson@6121
|
167 |
|
paulson@6121
|
168 |
\tdx{ex1I} [| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x)
|
paulson@6121
|
169 |
\tdx{ex1E} [| EX! x.P(x); !!x.[| P(x); ALL y. P(y) --> y=x |] ==> R
|
paulson@6121
|
170 |
|] ==> R
|
paulson@6121
|
171 |
\subcaption{Derived rules for \(\top\), \(\neg\), \(\bimp\) and \(\exists!\)}
|
paulson@6121
|
172 |
|
paulson@6121
|
173 |
\tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
|
paulson@6121
|
174 |
\tdx{impE} [| P-->Q; P; Q ==> R |] ==> R
|
paulson@6121
|
175 |
\tdx{allE} [| ALL x.P(x); P(x) ==> R |] ==> R
|
paulson@6121
|
176 |
\tdx{all_dupE} [| ALL x.P(x); [| P(x); ALL x.P(x) |] ==> R |] ==> R
|
paulson@6121
|
177 |
\subcaption{Sequent-style elimination rules}
|
paulson@6121
|
178 |
|
paulson@6121
|
179 |
\tdx{conj_impE} [| (P&Q)-->S; P-->(Q-->S) ==> R |] ==> R
|
paulson@6121
|
180 |
\tdx{disj_impE} [| (P|Q)-->S; [| P-->S; Q-->S |] ==> R |] ==> R
|
paulson@6121
|
181 |
\tdx{imp_impE} [| (P-->Q)-->S; [| P; Q-->S |] ==> Q; S ==> R |] ==> R
|
paulson@6121
|
182 |
\tdx{not_impE} [| ~P --> S; P ==> False; S ==> R |] ==> R
|
paulson@6121
|
183 |
\tdx{iff_impE} [| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P;
|
paulson@6121
|
184 |
S ==> R |] ==> R
|
paulson@6121
|
185 |
\tdx{all_impE} [| (ALL x.P(x))-->S; !!x.P(x); S ==> R |] ==> R
|
paulson@6121
|
186 |
\tdx{ex_impE} [| (EX x.P(x))-->S; P(a)-->S ==> R |] ==> R
|
paulson@6121
|
187 |
\end{ttbox}
|
paulson@6121
|
188 |
\subcaption{Intuitionistic simplification of implication}
|
paulson@6121
|
189 |
\caption{Derived rules for intuitionistic logic} \label{fol-int-derived}
|
paulson@6121
|
190 |
\end{figure}
|
paulson@6121
|
191 |
|
paulson@6121
|
192 |
|
paulson@6121
|
193 |
\section{Generic packages}
|
wenzelm@9695
|
194 |
FOL instantiates most of Isabelle's generic packages.
|
paulson@6121
|
195 |
\begin{itemize}
|
paulson@6121
|
196 |
\item
|
paulson@14154
|
197 |
It instantiates the simplifier, which is invoked through the method
|
paulson@14154
|
198 |
\isa{simp}. Both equality ($=$) and the biconditional
|
paulson@14154
|
199 |
($\bimp$) may be used for rewriting.
|
paulson@6121
|
200 |
|
paulson@6121
|
201 |
\item
|
paulson@14154
|
202 |
It instantiates the classical reasoner, which is invoked mainly through the
|
paulson@14154
|
203 |
methods \isa{blast} and \isa{auto}. See~\S\ref{fol-cla-prover}
|
paulson@6121
|
204 |
for details.
|
paulson@14154
|
205 |
%
|
paulson@14154
|
206 |
%\item FOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for
|
paulson@14154
|
207 |
% an equality throughout a subgoal and its hypotheses. This tactic uses FOL's
|
paulson@14154
|
208 |
% general substitution rule.
|
paulson@6121
|
209 |
\end{itemize}
|
paulson@6121
|
210 |
|
paulson@6121
|
211 |
\begin{warn}\index{simplification!of conjunctions}%
|
paulson@14154
|
212 |
Simplifying $a=b\conj P(a)$ to $a=b\conj P(b)$ is often advantageous. The
|
paulson@6121
|
213 |
left part of a conjunction helps in simplifying the right part. This effect
|
paulson@6121
|
214 |
is not available by default: it can be slow. It can be obtained by
|
paulson@14154
|
215 |
including the theorem \isa{conj_cong}\index{*conj_cong (rule)}%
|
paulson@14154
|
216 |
as a congruence rule in
|
paulson@14154
|
217 |
simplification, \isa{simp cong:\ conj\_cong}.
|
paulson@6121
|
218 |
\end{warn}
|
paulson@6121
|
219 |
|
paulson@6121
|
220 |
|
paulson@6121
|
221 |
\section{Intuitionistic proof procedures} \label{fol-int-prover}
|
paulson@14154
|
222 |
Implication elimination (the rules~\isa{mp} and~\isa{impE}) pose
|
paulson@6121
|
223 |
difficulties for automated proof. In intuitionistic logic, the assumption
|
paulson@6121
|
224 |
$P\imp Q$ cannot be treated like $\neg P\disj Q$. Given $P\imp Q$, we may
|
paulson@6121
|
225 |
use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated
|
paulson@6121
|
226 |
use of $P\imp Q$. If the proof of~$P$ fails then the whole branch of the
|
paulson@6121
|
227 |
proof must be abandoned. Thus intuitionistic propositional logic requires
|
paulson@6121
|
228 |
backtracking.
|
paulson@6121
|
229 |
|
paulson@6121
|
230 |
For an elementary example, consider the intuitionistic proof of $Q$ from
|
paulson@6121
|
231 |
$P\imp Q$ and $(P\imp Q)\imp P$. The implication $P\imp Q$ is needed
|
paulson@6121
|
232 |
twice:
|
paulson@6121
|
233 |
\[ \infer[({\imp}E)]{Q}{P\imp Q &
|
paulson@6121
|
234 |
\infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}}
|
paulson@6121
|
235 |
\]
|
paulson@14154
|
236 |
The theorem prover for intuitionistic logic does not use~\isa{impE}.\@
|
paulson@6121
|
237 |
Instead, it simplifies implications using derived rules
|
paulson@6121
|
238 |
(Fig.\ts\ref{fol-int-derived}). It reduces the antecedents of implications
|
paulson@6121
|
239 |
to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$.
|
paulson@6121
|
240 |
The rules \tdx{conj_impE} and \tdx{disj_impE} are
|
paulson@6121
|
241 |
straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and
|
paulson@6121
|
242 |
$(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp
|
paulson@14154
|
243 |
S$. The other \ldots\isa{\_impE} rules are unsafe; the method requires
|
paulson@6121
|
244 |
backtracking. All the rules are derived in the same simple manner.
|
paulson@6121
|
245 |
|
paulson@6121
|
246 |
Dyckhoff has independently discovered similar rules, and (more importantly)
|
paulson@6121
|
247 |
has demonstrated their completeness for propositional
|
paulson@6121
|
248 |
logic~\cite{dyckhoff}. However, the tactics given below are not complete
|
paulson@6121
|
249 |
for first-order logic because they discard universally quantified
|
paulson@14154
|
250 |
assumptions after a single use. These are \ML{} functions, and are listed
|
paulson@14154
|
251 |
below with their \ML{} type:
|
paulson@6121
|
252 |
\begin{ttbox}
|
paulson@6121
|
253 |
mp_tac : int -> tactic
|
paulson@6121
|
254 |
eq_mp_tac : int -> tactic
|
paulson@6121
|
255 |
IntPr.safe_step_tac : int -> tactic
|
paulson@6121
|
256 |
IntPr.safe_tac : tactic
|
paulson@6121
|
257 |
IntPr.inst_step_tac : int -> tactic
|
paulson@6121
|
258 |
IntPr.step_tac : int -> tactic
|
paulson@6121
|
259 |
IntPr.fast_tac : int -> tactic
|
paulson@6121
|
260 |
IntPr.best_tac : int -> tactic
|
paulson@6121
|
261 |
\end{ttbox}
|
paulson@14158
|
262 |
Most of these belong to the structure \ML{} structure \texttt{IntPr} and resemble the
|
paulson@14158
|
263 |
tactics of Isabelle's classical reasoner. There are no corresponding
|
paulson@14158
|
264 |
Isar methods, but you can use the
|
paulson@14154
|
265 |
\isa{tactic} method to call \ML{} tactics in an Isar script:
|
paulson@14154
|
266 |
\begin{isabelle}
|
paulson@14154
|
267 |
\isacommand{apply}\ (tactic\ {* IntPr.fast\_tac 1*})
|
paulson@14154
|
268 |
\end{isabelle}
|
paulson@14154
|
269 |
Here is a description of each tactic:
|
paulson@6121
|
270 |
|
paulson@6121
|
271 |
\begin{ttdescription}
|
paulson@6121
|
272 |
\item[\ttindexbold{mp_tac} {\it i}]
|
paulson@6121
|
273 |
attempts to use \tdx{notE} or \tdx{impE} within the assumptions in
|
paulson@6121
|
274 |
subgoal $i$. For each assumption of the form $\neg P$ or $P\imp Q$, it
|
paulson@6121
|
275 |
searches for another assumption unifiable with~$P$. By
|
paulson@6121
|
276 |
contradiction with $\neg P$ it can solve the subgoal completely; by Modus
|
paulson@6121
|
277 |
Ponens it can replace the assumption $P\imp Q$ by $Q$. The tactic can
|
paulson@6121
|
278 |
produce multiple outcomes, enumerating all suitable pairs of assumptions.
|
paulson@6121
|
279 |
|
paulson@6121
|
280 |
\item[\ttindexbold{eq_mp_tac} {\it i}]
|
paulson@6121
|
281 |
is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
|
paulson@6121
|
282 |
is safe.
|
paulson@6121
|
283 |
|
paulson@6121
|
284 |
\item[\ttindexbold{IntPr.safe_step_tac} $i$] performs a safe step on
|
paulson@6121
|
285 |
subgoal~$i$. This may include proof by assumption or Modus Ponens (taking
|
paulson@6121
|
286 |
care not to instantiate unknowns), or \texttt{hyp_subst_tac}.
|
paulson@6121
|
287 |
|
paulson@6121
|
288 |
\item[\ttindexbold{IntPr.safe_tac}] repeatedly performs safe steps on all
|
paulson@6121
|
289 |
subgoals. It is deterministic, with at most one outcome.
|
paulson@6121
|
290 |
|
paulson@6121
|
291 |
\item[\ttindexbold{IntPr.inst_step_tac} $i$] is like \texttt{safe_step_tac},
|
paulson@6121
|
292 |
but allows unknowns to be instantiated.
|
paulson@6121
|
293 |
|
paulson@6121
|
294 |
\item[\ttindexbold{IntPr.step_tac} $i$] tries \texttt{safe_tac} or {\tt
|
paulson@6121
|
295 |
inst_step_tac}, or applies an unsafe rule. This is the basic step of
|
paulson@6121
|
296 |
the intuitionistic proof procedure.
|
paulson@6121
|
297 |
|
paulson@6121
|
298 |
\item[\ttindexbold{IntPr.fast_tac} $i$] applies \texttt{step_tac}, using
|
paulson@6121
|
299 |
depth-first search, to solve subgoal~$i$.
|
paulson@6121
|
300 |
|
paulson@6121
|
301 |
\item[\ttindexbold{IntPr.best_tac} $i$] applies \texttt{step_tac}, using
|
paulson@6121
|
302 |
best-first search (guided by the size of the proof state) to solve subgoal~$i$.
|
paulson@6121
|
303 |
\end{ttdescription}
|
paulson@6121
|
304 |
Here are some of the theorems that \texttt{IntPr.fast_tac} proves
|
paulson@6121
|
305 |
automatically. The latter three date from {\it Principia Mathematica}
|
paulson@6121
|
306 |
(*11.53, *11.55, *11.61)~\cite{principia}.
|
paulson@6121
|
307 |
\begin{ttbox}
|
paulson@6121
|
308 |
~~P & ~~(P --> Q) --> ~~Q
|
paulson@6121
|
309 |
(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))
|
paulson@6121
|
310 |
(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))
|
paulson@6121
|
311 |
(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))
|
paulson@6121
|
312 |
\end{ttbox}
|
paulson@6121
|
313 |
|
paulson@6121
|
314 |
|
paulson@6121
|
315 |
|
paulson@6121
|
316 |
\begin{figure}
|
paulson@6121
|
317 |
\begin{ttbox}
|
paulson@6121
|
318 |
\tdx{excluded_middle} ~P | P
|
paulson@6121
|
319 |
|
paulson@6121
|
320 |
\tdx{disjCI} (~Q ==> P) ==> P|Q
|
paulson@6121
|
321 |
\tdx{exCI} (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)
|
paulson@6121
|
322 |
\tdx{impCE} [| P-->Q; ~P ==> R; Q ==> R |] ==> R
|
paulson@6121
|
323 |
\tdx{iffCE} [| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
|
paulson@6121
|
324 |
\tdx{notnotD} ~~P ==> P
|
paulson@6121
|
325 |
\tdx{swap} ~P ==> (~Q ==> P) ==> Q
|
paulson@6121
|
326 |
\end{ttbox}
|
paulson@6121
|
327 |
\caption{Derived rules for classical logic} \label{fol-cla-derived}
|
paulson@6121
|
328 |
\end{figure}
|
paulson@6121
|
329 |
|
paulson@6121
|
330 |
|
paulson@6121
|
331 |
\section{Classical proof procedures} \label{fol-cla-prover}
|
paulson@6121
|
332 |
The classical theory, \thydx{FOL}, consists of intuitionistic logic plus
|
paulson@6121
|
333 |
the rule
|
paulson@6121
|
334 |
$$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$
|
paulson@6121
|
335 |
\noindent
|
wenzelm@9695
|
336 |
Natural deduction in classical logic is not really all that natural. FOL
|
wenzelm@9695
|
337 |
derives classical introduction rules for $\disj$ and~$\exists$, as well as
|
wenzelm@9695
|
338 |
classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see
|
wenzelm@9695
|
339 |
Fig.\ts\ref{fol-cla-derived}).
|
paulson@6121
|
340 |
|
paulson@14154
|
341 |
The classical reasoner is installed. The most useful methods are
|
paulson@14154
|
342 |
\isa{blast} (pure classical reasoning) and \isa{auto} (classical reasoning
|
paulson@14154
|
343 |
combined with simplification), but the full range of
|
paulson@14154
|
344 |
methods is available, including \isa{clarify},
|
paulson@14154
|
345 |
\isa{fast}, \isa{best} and \isa{force}.
|
paulson@14154
|
346 |
See the
|
paulson@6121
|
347 |
\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
|
paulson@6121
|
348 |
{Chap.\ts\ref{chap:classical}}
|
paulson@14154
|
349 |
and the \emph{Tutorial}~\cite{isa-tutorial}
|
paulson@6121
|
350 |
for more discussion of classical proof methods.
|
paulson@6121
|
351 |
|
paulson@6121
|
352 |
|
paulson@6121
|
353 |
\section{An intuitionistic example}
|
paulson@14158
|
354 |
Here is a session similar to one in the book {\em Logic and Computation}
|
paulson@14158
|
355 |
\cite[pages~222--3]{paulson87}. It illustrates the treatment of
|
paulson@14158
|
356 |
quantifier reasoning, which is different in Isabelle than it is in
|
paulson@14158
|
357 |
{\sc lcf}-based theorem provers such as {\sc hol}.
|
paulson@6121
|
358 |
|
paulson@14158
|
359 |
The theory header specifies that we are working in intuitionistic
|
paulson@14158
|
360 |
logic by designating \isa{IFOL} rather than \isa{FOL} as the parent
|
paulson@14158
|
361 |
theory:
|
paulson@14154
|
362 |
\begin{isabelle}
|
paulson@30036
|
363 |
\isacommand{theory}\ IFOL\_examples\ \isacommand{imports}\ IFOL\isanewline
|
paulson@30036
|
364 |
\isacommand{begin}
|
paulson@14154
|
365 |
\end{isabelle}
|
paulson@6121
|
366 |
The proof begins by entering the goal, then applying the rule $({\imp}I)$.
|
paulson@14154
|
367 |
\begin{isabelle}
|
paulson@14154
|
368 |
\isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline
|
paulson@14154
|
369 |
\ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\
|
paulson@14154
|
370 |
\isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))
|
paulson@14154
|
371 |
\isanewline
|
paulson@14154
|
372 |
\isacommand{apply}\ (rule\ impI)\isanewline
|
paulson@14154
|
373 |
\ 1.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\
|
paulson@14154
|
374 |
\isasymLongrightarrow \ \isasymforall x.\ \isasymexists y.\ Q(x,\ y)
|
paulson@14154
|
375 |
\end{isabelle}
|
paulson@14154
|
376 |
Isabelle's output is shown as it would appear using Proof General.
|
paulson@6121
|
377 |
In this example, we shall never have more than one subgoal. Applying
|
paulson@14154
|
378 |
$({\imp}I)$ replaces~\isa{\isasymlongrightarrow}
|
paulson@14154
|
379 |
by~\isa{\isasymLongrightarrow}, so that
|
paulson@14154
|
380 |
\(\ex{y}\all{x}Q(x,y)\) becomes an assumption. We have the choice of
|
paulson@6121
|
381 |
$({\exists}E)$ and $({\forall}I)$; let us try the latter.
|
paulson@14154
|
382 |
\begin{isabelle}
|
paulson@14154
|
383 |
\isacommand{apply}\ (rule\ allI)\isanewline
|
paulson@14154
|
384 |
\ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\
|
paulson@14154
|
385 |
\isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)\hfill\((*)\)
|
paulson@14154
|
386 |
\end{isabelle}
|
paulson@14154
|
387 |
Applying $({\forall}I)$ replaces the \isa{\isasymforall
|
paulson@14154
|
388 |
x} (in ASCII, \isa{ALL~x}) by \isa{\isasymAnd x}
|
paulson@14154
|
389 |
(or \isa{!!x}), replacing FOL's universal quantifier by Isabelle's
|
paulson@14154
|
390 |
meta universal quantifier. The bound variable is a {\bf parameter} of
|
paulson@14154
|
391 |
the subgoal. We now must choose between $({\exists}I)$ and
|
paulson@14154
|
392 |
$({\exists}E)$. What happens if the wrong rule is chosen?
|
paulson@14154
|
393 |
\begin{isabelle}
|
paulson@14154
|
394 |
\isacommand{apply}\ (rule\ exI)\isanewline
|
paulson@14154
|
395 |
\ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\
|
paulson@14154
|
396 |
\isasymLongrightarrow \ Q(x,\ ?y2(x))
|
paulson@14154
|
397 |
\end{isabelle}
|
paulson@14154
|
398 |
The new subgoal~1 contains the function variable \isa{?y2}. Instantiating
|
paulson@14154
|
399 |
\isa{?y2} can replace~\isa{?y2(x)} by a term containing~\isa{x}, even
|
paulson@14154
|
400 |
though~\isa{x} is a bound variable. Now we analyse the assumption
|
paulson@6121
|
401 |
\(\exists y.\forall x. Q(x,y)\) using elimination rules:
|
paulson@14154
|
402 |
\begin{isabelle}
|
paulson@14154
|
403 |
\isacommand{apply}\ (erule\ exE)\isanewline
|
paulson@14154
|
404 |
\ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\ \isasymLongrightarrow \ Q(x,\ ?y2(x))
|
paulson@14154
|
405 |
\end{isabelle}
|
paulson@14154
|
406 |
Applying $(\exists E)$ has produced the parameter \isa{y} and stripped the
|
paulson@6121
|
407 |
existential quantifier from the assumption. But the subgoal is unprovable:
|
paulson@14154
|
408 |
there is no way to unify \isa{?y2(x)} with the bound variable~\isa{y}.
|
paulson@14154
|
409 |
Using Proof General, we can return to the critical point, marked
|
paulson@14154
|
410 |
$(*)$ above. This time we apply $({\exists}E)$:
|
paulson@14154
|
411 |
\begin{isabelle}
|
paulson@14154
|
412 |
\isacommand{apply}\ (erule\ exE)\isanewline
|
paulson@14154
|
413 |
\ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\
|
paulson@14154
|
414 |
\isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)
|
paulson@14154
|
415 |
\end{isabelle}
|
paulson@6121
|
416 |
We now have two parameters and no scheme variables. Applying
|
paulson@6121
|
417 |
$({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are
|
paulson@6121
|
418 |
applied to those parameters. Parameters should be produced early, as this
|
paulson@6121
|
419 |
example demonstrates.
|
paulson@14154
|
420 |
\begin{isabelle}
|
paulson@14154
|
421 |
\isacommand{apply}\ (rule\ exI)\isanewline
|
paulson@14154
|
422 |
\ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\
|
paulson@14154
|
423 |
\isasymLongrightarrow \ Q(x,\ ?y3(x,\ y))
|
paulson@14154
|
424 |
\isanewline
|
paulson@14154
|
425 |
\isacommand{apply}\ (erule\ allE)\isanewline
|
paulson@14154
|
426 |
\ 1.\ \isasymAnd x\ y.\ Q(?x4(x,\ y),\ y)\ \isasymLongrightarrow \
|
paulson@14154
|
427 |
Q(x,\ ?y3(x,\ y))
|
paulson@14154
|
428 |
\end{isabelle}
|
paulson@14154
|
429 |
The subgoal has variables \isa{?y3} and \isa{?x4} applied to both
|
paulson@14154
|
430 |
parameters. The obvious projection functions unify \isa{?x4(x,y)} with~\isa{
|
paulson@14154
|
431 |
x} and \isa{?y3(x,y)} with~\isa{y}.
|
paulson@14154
|
432 |
\begin{isabelle}
|
paulson@14154
|
433 |
\isacommand{apply}\ assumption\isanewline
|
paulson@14154
|
434 |
No\ subgoals!\isanewline
|
paulson@14154
|
435 |
\isacommand{done}
|
paulson@14154
|
436 |
\end{isabelle}
|
paulson@14154
|
437 |
The theorem was proved in six method invocations, not counting the
|
paulson@14154
|
438 |
abandoned ones. But proof checking is tedious, and the \ML{} tactic
|
paulson@14154
|
439 |
\ttindex{IntPr.fast_tac} can prove the theorem in one step.
|
paulson@14154
|
440 |
\begin{isabelle}
|
paulson@14154
|
441 |
\isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline
|
paulson@14154
|
442 |
\ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\
|
paulson@14154
|
443 |
\isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))
|
paulson@14154
|
444 |
\isanewline
|
paulson@30036
|
445 |
\isacommand{by} (tactic \ttlbrace*IntPr.fast_tac 1*\ttrbrace)\isanewline
|
paulson@14154
|
446 |
No\ subgoals!
|
paulson@14154
|
447 |
\end{isabelle}
|
paulson@6121
|
448 |
|
paulson@6121
|
449 |
|
paulson@6121
|
450 |
\section{An example of intuitionistic negation}
|
paulson@6121
|
451 |
The following example demonstrates the specialized forms of implication
|
paulson@6121
|
452 |
elimination. Even propositional formulae can be difficult to prove from
|
paulson@6121
|
453 |
the basic rules; the specialized rules help considerably.
|
paulson@6121
|
454 |
|
paulson@6121
|
455 |
Propositional examples are easy to invent. As Dummett notes~\cite[page
|
paulson@6121
|
456 |
28]{dummett}, $\neg P$ is classically provable if and only if it is
|
paulson@6121
|
457 |
intuitionistically provable; therefore, $P$ is classically provable if and
|
paulson@6121
|
458 |
only if $\neg\neg P$ is intuitionistically provable.%
|
paulson@14154
|
459 |
\footnote{This remark holds only for propositional logic, not if $P$ is
|
paulson@14154
|
460 |
allowed to contain quantifiers.}
|
paulson@14154
|
461 |
%
|
paulson@14154
|
462 |
Proving $\neg\neg P$ intuitionistically is
|
paulson@6121
|
463 |
much harder than proving~$P$ classically.
|
paulson@6121
|
464 |
|
paulson@6121
|
465 |
Our example is the double negation of the classical tautology $(P\imp
|
paulson@14154
|
466 |
Q)\disj (Q\imp P)$. The first step is apply the
|
paulson@14154
|
467 |
\isa{unfold} method, which expands
|
paulson@14154
|
468 |
negations to implications using the definition $\neg P\equiv P\imp\bot$
|
paulson@14154
|
469 |
and allows use of the special implication rules.
|
paulson@14154
|
470 |
\begin{isabelle}
|
paulson@14154
|
471 |
\isacommand{lemma}\ "\isachartilde \ \isachartilde \ ((P-->Q)\ |\ (Q-->P))"\isanewline
|
paulson@14154
|
472 |
\ 1.\ \isasymnot \ \isasymnot \ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P))
|
paulson@14154
|
473 |
\isanewline
|
paulson@14154
|
474 |
\isacommand{apply}\ (unfold\ not\_def)\isanewline
|
paulson@14154
|
475 |
\ 1.\ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False)\ \isasymlongrightarrow \ False%
|
paulson@14154
|
476 |
\end{isabelle}
|
paulson@14154
|
477 |
The next step is a trivial use of $(\imp I)$.
|
paulson@14154
|
478 |
\begin{isabelle}
|
paulson@14154
|
479 |
\isacommand{apply}\ (rule\ impI)\isanewline
|
paulson@14154
|
480 |
\ 1.\ (P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\ \isasymLongrightarrow \ False%
|
paulson@14154
|
481 |
\end{isabelle}
|
paulson@6121
|
482 |
By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but
|
paulson@14154
|
483 |
that formula is not a theorem of intuitionistic logic. Instead, we
|
paulson@14154
|
484 |
apply the specialized implication rule \tdx{disj_impE}. It splits the
|
paulson@6121
|
485 |
assumption into two assumptions, one for each disjunct.
|
paulson@14154
|
486 |
\begin{isabelle}
|
paulson@14154
|
487 |
\isacommand{apply}\ (erule\ disj\_impE)\isanewline
|
paulson@14154
|
488 |
\ 1.\ \isasymlbrakk (P\ \isasymlongrightarrow \ Q)\ \isasymlongrightarrow \ False;\ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \
|
paulson@14154
|
489 |
False
|
paulson@14154
|
490 |
\end{isabelle}
|
paulson@6121
|
491 |
We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but
|
paulson@6121
|
492 |
their negations are inconsistent. Applying \tdx{imp_impE} breaks down
|
paulson@6121
|
493 |
the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new
|
paulson@6121
|
494 |
assumptions~$P$ and~$\neg Q$.
|
paulson@14154
|
495 |
\begin{isabelle}
|
paulson@14154
|
496 |
\isacommand{apply}\ (erule\ imp\_impE)\isanewline
|
paulson@14154
|
497 |
\ 1.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ P;\ Q\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
|
paulson@14154
|
498 |
\ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \
|
paulson@14154
|
499 |
False
|
paulson@14154
|
500 |
\end{isabelle}
|
paulson@6121
|
501 |
Subgoal~2 holds trivially; let us ignore it and continue working on
|
paulson@6121
|
502 |
subgoal~1. Thanks to the assumption~$P$, we could prove $Q\imp P$;
|
paulson@6121
|
503 |
applying \tdx{imp_impE} is simpler.
|
paulson@14154
|
504 |
\begin{isabelle}
|
paulson@14154
|
505 |
\ \isacommand{apply}\ (erule\ imp\_impE)\isanewline
|
paulson@14154
|
506 |
\ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ Q;\ P\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ P\isanewline
|
paulson@14154
|
507 |
\ 2.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
|
paulson@14154
|
508 |
\ 3.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ False%
|
paulson@14154
|
509 |
\end{isabelle}
|
paulson@6121
|
510 |
The three subgoals are all trivial.
|
paulson@14154
|
511 |
\begin{isabelle}
|
paulson@14154
|
512 |
\isacommand{apply}\ assumption\ \isanewline
|
paulson@14154
|
513 |
\ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\
|
paulson@14154
|
514 |
False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
|
paulson@14154
|
515 |
\ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\
|
paulson@14154
|
516 |
\isasymlongrightarrow \ False;\ False\isasymrbrakk \
|
paulson@14154
|
517 |
\isasymLongrightarrow \ False%
|
paulson@14154
|
518 |
\isanewline
|
paulson@14154
|
519 |
\isacommand{apply}\ (erule\ FalseE)+\isanewline
|
paulson@14154
|
520 |
No\ subgoals!\isanewline
|
paulson@14154
|
521 |
\isacommand{done}
|
paulson@14154
|
522 |
\end{isabelle}
|
paulson@14154
|
523 |
This proof is also trivial for the \ML{} tactic \isa{IntPr.fast_tac}.
|
paulson@6121
|
524 |
|
paulson@6121
|
525 |
|
paulson@6121
|
526 |
\section{A classical example} \label{fol-cla-example}
|
paulson@6121
|
527 |
To illustrate classical logic, we shall prove the theorem
|
paulson@6121
|
528 |
$\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as
|
paulson@6121
|
529 |
follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
|
paulson@14154
|
530 |
$\all{x}P(x)$ is true. Either way the theorem holds. First, we must
|
paulson@14158
|
531 |
work in a theory based on classical logic, the theory \isa{FOL}:
|
paulson@14154
|
532 |
\begin{isabelle}
|
paulson@30036
|
533 |
\isacommand{theory}\ FOL\_examples\ \isacommand{imports}\ FOL\isanewline
|
paulson@30036
|
534 |
\isacommand{begin}
|
paulson@14154
|
535 |
\end{isabelle}
|
paulson@6121
|
536 |
|
paulson@6121
|
537 |
The formal proof does not conform in any obvious way to the sketch given
|
paulson@14154
|
538 |
above. Its key step is its first rule, \tdx{exCI}, a classical
|
paulson@14154
|
539 |
version of~$(\exists I)$ that allows multiple instantiation of the
|
paulson@14154
|
540 |
quantifier.
|
paulson@14154
|
541 |
\begin{isabelle}
|
paulson@14154
|
542 |
\isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline
|
paulson@14154
|
543 |
\ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x)
|
paulson@14154
|
544 |
\isanewline
|
paulson@14154
|
545 |
\isacommand{apply}\ (rule\ exCI)\isanewline
|
paulson@14154
|
546 |
\ 1.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ \isasymforall x.\ P(?a)\ \isasymlongrightarrow \ P(x)
|
paulson@14154
|
547 |
\end{isabelle}
|
paulson@14154
|
548 |
We can either exhibit a term \isa{?a} to satisfy the conclusion of
|
paulson@6121
|
549 |
subgoal~1, or produce a contradiction from the assumption. The next
|
paulson@6121
|
550 |
steps are routine.
|
paulson@14154
|
551 |
\begin{isabelle}
|
paulson@14154
|
552 |
\isacommand{apply}\ (rule\ allI)\isanewline
|
paulson@14154
|
553 |
\ 1.\ \isasymAnd x.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ P(?a)\ \isasymlongrightarrow \ P(x)
|
paulson@14154
|
554 |
\isanewline
|
paulson@14154
|
555 |
\isacommand{apply}\ (rule\ impI)\isanewline
|
paulson@14154
|
556 |
\ 1.\ \isasymAnd x.\ \isasymlbrakk \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x));\ P(?a)\isasymrbrakk \ \isasymLongrightarrow \ P(x)
|
paulson@14154
|
557 |
\end{isabelle}
|
paulson@6121
|
558 |
By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$
|
paulson@14154
|
559 |
is equivalent to applying~$(\exists I)$ again.
|
paulson@14154
|
560 |
\begin{isabelle}
|
paulson@14154
|
561 |
\isacommand{apply}\ (erule\ allE)\isanewline
|
paulson@14154
|
562 |
\ 1.\ \isasymAnd x.\ \isasymlbrakk P(?a);\ \isasymnot \ (\isasymforall xa.\ P(?y3(x))\ \isasymlongrightarrow \ P(xa))\isasymrbrakk \ \isasymLongrightarrow \ P(x)
|
paulson@14154
|
563 |
\end{isabelle}
|
paulson@6121
|
564 |
In classical logic, a negated assumption is equivalent to a conclusion. To
|
paulson@8249
|
565 |
get this effect, we create a swapped version of $(\forall I)$ and apply it
|
paulson@14154
|
566 |
using \ttindex{erule}.
|
paulson@14154
|
567 |
\begin{isabelle}
|
paulson@14154
|
568 |
\isacommand{apply}\ (erule\ allI\ [THEN\ [2]\ swap])\isanewline
|
paulson@14154
|
569 |
\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x)\isasymrbrakk \ \isasymLongrightarrow \ P(?y3(x))\ \isasymlongrightarrow \ P(xa)
|
paulson@14154
|
570 |
\end{isabelle}
|
paulson@14154
|
571 |
The operand of \isa{erule} above denotes the following theorem:
|
paulson@14154
|
572 |
\begin{isabelle}
|
paulson@14154
|
573 |
\ \ \ \ \isasymlbrakk \isasymnot \ (\isasymforall x.\ ?P1(x));\
|
paulson@14154
|
574 |
\isasymAnd x.\ \isasymnot \ ?P\ \isasymLongrightarrow \
|
paulson@14154
|
575 |
?P1(x)\isasymrbrakk \
|
paulson@14154
|
576 |
\isasymLongrightarrow \ ?P%
|
paulson@14154
|
577 |
\end{isabelle}
|
paulson@14154
|
578 |
The previous conclusion, \isa{P(x)}, has become a negated assumption.
|
paulson@14154
|
579 |
\begin{isabelle}
|
paulson@14154
|
580 |
\isacommand{apply}\ (rule\ impI)\isanewline
|
paulson@14154
|
581 |
\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(xa)
|
paulson@14154
|
582 |
\end{isabelle}
|
paulson@6121
|
583 |
The subgoal has three assumptions. We produce a contradiction between the
|
paulson@14154
|
584 |
\index{assumptions!contradictory} assumptions~\isa{\isasymnot P(x)}
|
paulson@14154
|
585 |
and~\isa{P(?y3(x))}. The proof never instantiates the
|
paulson@14154
|
586 |
unknown~\isa{?a}.
|
paulson@14154
|
587 |
\begin{isabelle}
|
paulson@14154
|
588 |
\isacommand{apply}\ (erule\ notE)\isanewline
|
paulson@14154
|
589 |
\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(x)
|
paulson@14154
|
590 |
\isanewline
|
paulson@14154
|
591 |
\isacommand{apply}\ assumption\isanewline
|
paulson@14154
|
592 |
No\ subgoals!\isanewline
|
paulson@14154
|
593 |
\isacommand{done}
|
paulson@14154
|
594 |
\end{isabelle}
|
paulson@14154
|
595 |
The civilised way to prove this theorem is using the
|
paulson@14154
|
596 |
\methdx{blast} method, which automatically uses the classical form
|
paulson@14154
|
597 |
of the rule~$(\exists I)$:
|
paulson@14154
|
598 |
\begin{isabelle}
|
paulson@14154
|
599 |
\isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline
|
paulson@14154
|
600 |
\ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x)
|
paulson@14154
|
601 |
\isanewline
|
paulson@14154
|
602 |
\isacommand{by}\ blast\isanewline
|
paulson@14154
|
603 |
No\ subgoals!
|
paulson@14154
|
604 |
\end{isabelle}
|
paulson@6121
|
605 |
If this theorem seems counterintuitive, then perhaps you are an
|
paulson@6121
|
606 |
intuitionist. In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$
|
paulson@6121
|
607 |
requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$,
|
paulson@6121
|
608 |
which we cannot do without further knowledge about~$P$.
|
paulson@6121
|
609 |
|
paulson@6121
|
610 |
|
paulson@6121
|
611 |
\section{Derived rules and the classical tactics}
|
paulson@6121
|
612 |
Classical first-order logic can be extended with the propositional
|
paulson@6121
|
613 |
connective $if(P,Q,R)$, where
|
paulson@6121
|
614 |
$$ if(P,Q,R) \equiv P\conj Q \disj \neg P \conj R. \eqno(if) $$
|
paulson@6121
|
615 |
Theorems about $if$ can be proved by treating this as an abbreviation,
|
paulson@6121
|
616 |
replacing $if(P,Q,R)$ by $P\conj Q \disj \neg P \conj R$ in subgoals. But
|
paulson@6121
|
617 |
this duplicates~$P$, causing an exponential blowup and an unreadable
|
paulson@6121
|
618 |
formula. Introducing further abbreviations makes the problem worse.
|
paulson@6121
|
619 |
|
paulson@6121
|
620 |
Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$
|
paulson@6121
|
621 |
directly, without reference to its definition. The simple identity
|
paulson@6121
|
622 |
\[ if(P,Q,R) \,\bimp\, (P\imp Q)\conj (\neg P\imp R) \]
|
paulson@6121
|
623 |
suggests that the
|
paulson@6121
|
624 |
$if$-introduction rule should be
|
paulson@6121
|
625 |
\[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]} & \infer*{R}{[\neg P]}} \]
|
paulson@6121
|
626 |
The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the
|
paulson@6121
|
627 |
elimination rules for~$\disj$ and~$\conj$.
|
paulson@6121
|
628 |
\[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]}
|
paulson@6121
|
629 |
& \infer*{S}{[\neg P,R]}}
|
paulson@6121
|
630 |
\]
|
paulson@6121
|
631 |
Having made these plans, we get down to work with Isabelle. The theory of
|
paulson@6121
|
632 |
classical logic, \texttt{FOL}, is extended with the constant
|
paulson@6121
|
633 |
$if::[o,o,o]\To o$. The axiom \tdx{if_def} asserts the
|
paulson@6121
|
634 |
equation~$(if)$.
|
paulson@14154
|
635 |
\begin{isabelle}
|
paulson@30036
|
636 |
\isacommand{theory}\ If\ \isacommand{imports}\ FOL\isanewline
|
paulson@30036
|
637 |
\isacommand{begin}\isanewline
|
paulson@14154
|
638 |
\isacommand{constdefs}\isanewline
|
paulson@14154
|
639 |
\ \ if\ ::\ "[o,o,o]=>o"\isanewline
|
paulson@14154
|
640 |
\ \ \ "if(P,Q,R)\ ==\ P\&Q\ |\ \isachartilde P\&R"
|
paulson@14154
|
641 |
\end{isabelle}
|
paulson@6121
|
642 |
We create the file \texttt{If.thy} containing these declarations. (This file
|
paulson@6121
|
643 |
is on directory \texttt{FOL/ex} in the Isabelle distribution.) Typing
|
paulson@14154
|
644 |
\begin{isabelle}
|
paulson@6121
|
645 |
use_thy "If";
|
paulson@14154
|
646 |
\end{isabelle}
|
paulson@6121
|
647 |
loads that theory and sets it to be the current context.
|
paulson@6121
|
648 |
|
paulson@6121
|
649 |
|
paulson@6121
|
650 |
\subsection{Deriving the introduction rule}
|
paulson@6121
|
651 |
|
paulson@6121
|
652 |
The derivations of the introduction and elimination rules demonstrate the
|
paulson@6121
|
653 |
methods for rewriting with definitions. Classical reasoning is required,
|
paulson@14154
|
654 |
so we use \isa{blast}.
|
paulson@6121
|
655 |
|
paulson@6121
|
656 |
The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$,
|
paulson@14154
|
657 |
concludes $if(P,Q,R)$. We propose this lemma and immediately simplify
|
paulson@14154
|
658 |
using \isa{if\_def} to expand the definition of \isa{if} in the
|
paulson@14154
|
659 |
subgoal.
|
paulson@14154
|
660 |
\begin{isabelle}
|
paulson@14154
|
661 |
\isacommand{lemma}\ ifI: "[|\ P\ ==>\ Q;\ \isachartilde P\ ==>\ R\
|
paulson@14154
|
662 |
|]\ ==>\ if(P,Q,R)"\isanewline
|
paulson@14154
|
663 |
\ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ Q,\ R)
|
paulson@14154
|
664 |
\isanewline
|
paulson@14154
|
665 |
\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
|
paulson@14154
|
666 |
\ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \
|
paulson@14154
|
667 |
R
|
paulson@14154
|
668 |
\end{isabelle}
|
paulson@14154
|
669 |
The rule's premises, although expressed using meta-level implication
|
paulson@14154
|
670 |
(\isa{\isasymLongrightarrow}) are passed as ordinary implications to
|
paulson@14154
|
671 |
\methdx{blast}.
|
paulson@14154
|
672 |
\begin{isabelle}
|
paulson@14154
|
673 |
\isacommand{apply}\ blast\isanewline
|
paulson@14154
|
674 |
No\ subgoals!\isanewline
|
paulson@14154
|
675 |
\isacommand{done}
|
paulson@14154
|
676 |
\end{isabelle}
|
paulson@6121
|
677 |
|
paulson@6121
|
678 |
|
paulson@6121
|
679 |
\subsection{Deriving the elimination rule}
|
paulson@6121
|
680 |
The elimination rule has three premises, two of which are themselves rules.
|
paulson@6121
|
681 |
The conclusion is simply $S$.
|
paulson@14154
|
682 |
\begin{isabelle}
|
paulson@14154
|
683 |
\isacommand{lemma}\ ifE:\isanewline
|
paulson@14154
|
684 |
\ \ \ "[|\ if(P,Q,R);\ \ [|P;\ Q|]\ ==>\ S;\ [|\isachartilde P;\ R|]\ ==>\ S\ |]\ ==>\ S"\isanewline
|
paulson@14154
|
685 |
\ 1.\ \isasymlbrakk if(P,\ Q,\ R);\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S%
|
paulson@14154
|
686 |
\isanewline
|
paulson@14154
|
687 |
\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
|
paulson@14154
|
688 |
\ 1.\ \isasymlbrakk P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R;\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S%
|
paulson@14154
|
689 |
\end{isabelle}
|
paulson@14154
|
690 |
The proof script is the same as before: \isa{simp} followed by
|
paulson@14154
|
691 |
\isa{blast}:
|
paulson@14154
|
692 |
\begin{isabelle}
|
paulson@14154
|
693 |
\isacommand{apply}\ blast\isanewline
|
paulson@14154
|
694 |
No\ subgoals!\isanewline
|
paulson@14154
|
695 |
\isacommand{done}
|
paulson@14154
|
696 |
\end{isabelle}
|
paulson@6121
|
697 |
|
paulson@6121
|
698 |
|
paulson@6121
|
699 |
\subsection{Using the derived rules}
|
paulson@14154
|
700 |
Our new derived rules, \tdx{ifI} and~\tdx{ifE}, permit natural
|
paulson@14154
|
701 |
proofs of theorems such as the following:
|
paulson@6121
|
702 |
\begin{eqnarray*}
|
paulson@6121
|
703 |
if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\
|
paulson@6121
|
704 |
if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B))
|
paulson@6121
|
705 |
\end{eqnarray*}
|
paulson@6121
|
706 |
Proofs also require the classical reasoning rules and the $\bimp$
|
paulson@14154
|
707 |
introduction rule (called~\tdx{iffI}: do not confuse with~\isa{ifI}).
|
paulson@6121
|
708 |
|
paulson@6121
|
709 |
To display the $if$-rules in action, let us analyse a proof step by step.
|
paulson@14154
|
710 |
\begin{isabelle}
|
paulson@14154
|
711 |
\isacommand{lemma}\ if\_commute:\isanewline
|
paulson@14154
|
712 |
\ \ \ \ \ "if(P,\ if(Q,A,B),\
|
paulson@14154
|
713 |
if(Q,C,D))\ <->\ if(Q,\ if(P,A,C),\ if(P,B,D))"\isanewline
|
paulson@14154
|
714 |
\isacommand{apply}\ (rule\ iffI)\isanewline
|
paulson@14154
|
715 |
\ 1.\ if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))\ \isasymLongrightarrow \isanewline
|
paulson@14154
|
716 |
\isaindent{\ 1.\ }if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
|
paulson@14154
|
717 |
\ 2.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
|
paulson@14154
|
718 |
\isaindent{\ 2.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
|
paulson@14154
|
719 |
\end{isabelle}
|
paulson@6121
|
720 |
The $if$-elimination rule can be applied twice in succession.
|
paulson@14154
|
721 |
\begin{isabelle}
|
paulson@14154
|
722 |
\isacommand{apply}\ (erule\ ifE)\isanewline
|
paulson@14154
|
723 |
\ 1.\ \isasymlbrakk P;\ if(Q,\ A,\ B)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
|
paulson@14154
|
724 |
\ 2.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
|
paulson@14154
|
725 |
\ 3.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
|
paulson@14154
|
726 |
\isaindent{\ 3.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
|
paulson@14154
|
727 |
\isanewline
|
paulson@14154
|
728 |
\isacommand{apply}\ (erule\ ifE)\isanewline
|
paulson@14154
|
729 |
\ 1.\ \isasymlbrakk P;\ Q;\ A\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
|
paulson@14154
|
730 |
\ 2.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
|
paulson@14154
|
731 |
\ 3.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
|
paulson@14154
|
732 |
\ 4.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
|
paulson@14154
|
733 |
\isaindent{\ 4.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
|
paulson@14154
|
734 |
\end{isabelle}
|
paulson@6121
|
735 |
%
|
paulson@6121
|
736 |
In the first two subgoals, all assumptions have been reduced to atoms. Now
|
paulson@6121
|
737 |
$if$-introduction can be applied. Observe how the $if$-rules break down
|
paulson@6121
|
738 |
occurrences of $if$ when they become the outermost connective.
|
paulson@14154
|
739 |
\begin{isabelle}
|
paulson@14154
|
740 |
\isacommand{apply}\ (rule\ ifI)\isanewline
|
paulson@14154
|
741 |
\ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ A,\ C)\isanewline
|
paulson@14154
|
742 |
\ 2.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline
|
paulson@14154
|
743 |
\ 3.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
|
paulson@14154
|
744 |
\ 4.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
|
paulson@14154
|
745 |
\ 5.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
|
paulson@14154
|
746 |
\isaindent{\ 5.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
|
paulson@14154
|
747 |
\isanewline
|
paulson@14154
|
748 |
\isacommand{apply}\ (rule\ ifI)\isanewline
|
paulson@14154
|
749 |
\ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline
|
paulson@14154
|
750 |
\ 2.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \ C\isanewline
|
paulson@14154
|
751 |
\ 3.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline
|
paulson@14154
|
752 |
\ 4.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
|
paulson@14154
|
753 |
\ 5.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
|
paulson@14154
|
754 |
\ 6.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
|
paulson@14154
|
755 |
\isaindent{\ 6.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
|
paulson@14154
|
756 |
\end{isabelle}
|
paulson@6121
|
757 |
Where do we stand? The first subgoal holds by assumption; the second and
|
paulson@6121
|
758 |
third, by contradiction. This is getting tedious. We could use the classical
|
paulson@6121
|
759 |
reasoner, but first let us extend the default claset with the derived rules
|
paulson@6121
|
760 |
for~$if$.
|
paulson@14154
|
761 |
\begin{isabelle}
|
paulson@14154
|
762 |
\isacommand{declare}\ ifI\ [intro!]\isanewline
|
paulson@14154
|
763 |
\isacommand{declare}\ ifE\ [elim!]
|
paulson@14154
|
764 |
\end{isabelle}
|
paulson@14154
|
765 |
With these declarations, we could have proved this theorem with a single
|
paulson@14154
|
766 |
call to \isa{blast}. Here is another example:
|
paulson@14154
|
767 |
\begin{isabelle}
|
paulson@14154
|
768 |
\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline
|
paulson@14154
|
769 |
\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B))
|
paulson@14154
|
770 |
\isanewline
|
paulson@14154
|
771 |
\isacommand{by}\ blast
|
paulson@14154
|
772 |
\end{isabelle}
|
paulson@6121
|
773 |
|
paulson@6121
|
774 |
|
paulson@6121
|
775 |
\subsection{Derived rules versus definitions}
|
paulson@6121
|
776 |
Dispensing with the derived rules, we can treat $if$ as an
|
paulson@6121
|
777 |
abbreviation, and let \ttindex{blast_tac} prove the expanded formula. Let
|
paulson@6121
|
778 |
us redo the previous proof:
|
paulson@14154
|
779 |
\begin{isabelle}
|
paulson@14154
|
780 |
\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline
|
paulson@14154
|
781 |
\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B))
|
paulson@14154
|
782 |
\end{isabelle}
|
paulson@14154
|
783 |
This time, we simply unfold using the definition of $if$:
|
paulson@14154
|
784 |
\begin{isabelle}
|
paulson@14154
|
785 |
\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
|
paulson@14154
|
786 |
\ 1.\ (P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R)\ \isasymand \ A\ \isasymor \ (\isasymnot \ P\ \isasymor \ \isasymnot \ Q)\ \isasymand \ (P\ \isasymor \ \isasymnot \ R)\ \isasymand \ B\ \isasymlongleftrightarrow \isanewline
|
paulson@14154
|
787 |
\isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ A\ \isasymor \ \isasymnot \ R\ \isasymand \ B)
|
paulson@14154
|
788 |
\end{isabelle}
|
paulson@14154
|
789 |
We are left with a subgoal in pure first-order logic, and it falls to
|
paulson@14154
|
790 |
\isa{blast}:
|
paulson@14154
|
791 |
\begin{isabelle}
|
paulson@14154
|
792 |
\isacommand{apply}\ blast\isanewline
|
paulson@14154
|
793 |
No\ subgoals!
|
paulson@14154
|
794 |
\end{isabelle}
|
paulson@6121
|
795 |
Expanding definitions reduces the extended logic to the base logic. This
|
paulson@14154
|
796 |
approach has its merits, but it can be slow. In these examples, proofs
|
paulson@14154
|
797 |
using the derived rules for~\isa{if} run about six
|
paulson@14154
|
798 |
times faster than proofs using just the rules of first-order logic.
|
paulson@6121
|
799 |
|
paulson@14154
|
800 |
Expanding definitions can also make it harder to diagnose errors.
|
paulson@14154
|
801 |
Suppose we are having difficulties in proving some goal. If by expanding
|
paulson@14154
|
802 |
definitions we have made it unreadable, then we have little hope of
|
paulson@14154
|
803 |
diagnosing the problem.
|
paulson@6121
|
804 |
|
paulson@6121
|
805 |
Attempts at program verification often yield invalid assertions.
|
paulson@6121
|
806 |
Let us try to prove one:
|
paulson@14154
|
807 |
\begin{isabelle}
|
paulson@14154
|
808 |
\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline
|
paulson@14154
|
809 |
\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\
|
paulson@14154
|
810 |
A))
|
paulson@14154
|
811 |
\end{isabelle}
|
paulson@14154
|
812 |
Calling \isa{blast} yields an uninformative failure message. We can
|
paulson@14154
|
813 |
get a closer look at the situation by applying \methdx{auto}.
|
paulson@14154
|
814 |
\begin{isabelle}
|
paulson@14154
|
815 |
\isacommand{apply}\ auto\isanewline
|
paulson@14154
|
816 |
\ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline
|
paulson@14154
|
817 |
\ 2.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline
|
paulson@14154
|
818 |
\ 3.\ \isasymlbrakk B;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline
|
paulson@14154
|
819 |
\ 4.\ \isasymlbrakk \isasymnot \ R;\ A;\ \isasymnot \ B;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \
|
paulson@14154
|
820 |
False
|
paulson@14154
|
821 |
\end{isabelle}
|
paulson@6121
|
822 |
Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false
|
paulson@6121
|
823 |
while~$R$ and~$A$ are true. This truth assignment reduces the main goal to
|
paulson@6121
|
824 |
$true\bimp false$, which is of course invalid.
|
paulson@6121
|
825 |
|
wenzelm@9695
|
826 |
We can repeat this analysis by expanding definitions, using just the rules of
|
paulson@14154
|
827 |
first-order logic:
|
paulson@14154
|
828 |
\begin{isabelle}
|
paulson@14154
|
829 |
\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline
|
paulson@14154
|
830 |
\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\
|
paulson@14154
|
831 |
A))
|
paulson@14154
|
832 |
\isanewline
|
paulson@14154
|
833 |
\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
|
paulson@14154
|
834 |
\ 1.\ (P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R)\ \isasymand \ A\ \isasymor \ (\isasymnot \ P\ \isasymor \ \isasymnot \ Q)\ \isasymand \ (P\ \isasymor \ \isasymnot \ R)\ \isasymand \ B\ \isasymlongleftrightarrow \isanewline
|
paulson@14154
|
835 |
\isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ B\ \isasymor \ \isasymnot \ R\ \isasymand \ A)
|
paulson@14154
|
836 |
\end{isabelle}
|
paulson@14154
|
837 |
Again \isa{blast} would fail, so we try \methdx{auto}:
|
paulson@14154
|
838 |
\begin{isabelle}
|
paulson@14154
|
839 |
\isacommand{apply}\ (auto)\ \isanewline
|
paulson@14154
|
840 |
\ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline
|
paulson@14154
|
841 |
\ 2.\ \isasymlbrakk A;\ \isasymnot \ P;\ R;\ \isasymnot \ B\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
|
paulson@14154
|
842 |
\ 3.\ \isasymlbrakk B;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
|
paulson@14154
|
843 |
\ 4.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ A;\ \isasymnot \ R;\ Q\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
|
paulson@14154
|
844 |
\ 5.\ \isasymlbrakk B;\ \isasymnot \ Q;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
|
paulson@14154
|
845 |
\ 6.\ \isasymlbrakk B;\ \isasymnot \ A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
|
paulson@14154
|
846 |
\ 7.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
|
paulson@14154
|
847 |
\ 8.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ Q%
|
paulson@14154
|
848 |
\end{isabelle}
|
paulson@6121
|
849 |
Subgoal~1 yields the same countermodel as before. But each proof step has
|
paulson@6121
|
850 |
taken six times as long, and the final result contains twice as many subgoals.
|
paulson@6121
|
851 |
|
paulson@14154
|
852 |
Expanding your definitions usually makes proofs more difficult. This is
|
paulson@14154
|
853 |
why the classical prover has been designed to accept derived rules.
|
paulson@6121
|
854 |
|
paulson@6121
|
855 |
\index{first-order logic|)}
|