1.1 --- a/doc-src/ZF/FOL.tex Tue Aug 19 13:54:20 2003 +0200
1.2 +++ b/doc-src/ZF/FOL.tex Tue Aug 19 18:45:48 2003 +0200
1.3 @@ -12,16 +12,16 @@
1.4
1.5 \section{Syntax and rules of inference}
1.6 The logic is many-sorted, using Isabelle's type classes. The class of
1.7 -first-order terms is called \cldx{term} and is a subclass of \texttt{logic}.
1.8 +first-order terms is called \cldx{term} and is a subclass of \isa{logic}.
1.9 No types of individuals are provided, but extensions can define types such
1.10 -as \texttt{nat::term} and type constructors such as \texttt{list::(term)term}
1.11 +as \isa{nat::term} and type constructors such as \isa{list::(term)term}
1.12 (see the examples directory, \texttt{FOL/ex}). Below, the type variable
1.13 -$\alpha$ ranges over class \texttt{term}; the equality symbol and quantifiers
1.14 +$\alpha$ ranges over class \isa{term}; the equality symbol and quantifiers
1.15 are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which
1.16 belongs to class~\cldx{logic}. Figure~\ref{fol-syntax} gives the syntax.
1.17 Note that $a$\verb|~=|$b$ is translated to $\neg(a=b)$.
1.18
1.19 -Figure~\ref{fol-rules} shows the inference rules with their~\ML\ names.
1.20 +Figure~\ref{fol-rules} shows the inference rules with their names.
1.21 Negation is defined in the usual way for intuitionistic logic; $\neg P$
1.22 abbreviates $P\imp\bot$. The biconditional~($\bimp$) is defined through
1.23 $\conj$ and~$\imp$; introduction and elimination rules are derived for it.
1.24 @@ -33,7 +33,7 @@
1.25 exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
1.26
1.27 Some intuitionistic derived rules are shown in
1.28 -Fig.\ts\ref{fol-int-derived}, again with their \ML\ names. These include
1.29 +Fig.\ts\ref{fol-int-derived}, again with their names. These include
1.30 rules for the defined symbols $\neg$, $\bimp$ and $\exists!$. Natural
1.31 deduction typically involves a combination of forward and backward
1.32 reasoning, particularly with the destruction rules $(\conj E)$,
1.33 @@ -41,12 +41,11 @@
1.34 rules badly, so sequent-style rules are derived to eliminate conjunctions,
1.35 implications, and universal quantifiers. Used with elim-resolution,
1.36 \tdx{allE} eliminates a universal quantifier while \tdx{all_dupE}
1.37 -re-inserts the quantified formula for later use. The rules {\tt
1.38 -conj_impE}, etc., support the intuitionistic proof procedure
1.39 +re-inserts the quantified formula for later use. The rules
1.40 +\isa{conj\_impE}, etc., support the intuitionistic proof procedure
1.41 (see~\S\ref{fol-int-prover}).
1.42
1.43 -See the files \texttt{FOL/IFOL.thy}, \texttt{FOL/IFOL.ML} and
1.44 -\texttt{FOL/intprover.ML} for complete listings of the rules and
1.45 +See the on-line theory library for complete listings of the rules and
1.46 derived rules.
1.47
1.48 \begin{figure}
1.49 @@ -68,7 +67,7 @@
1.50 universal quantifier ($\forall$) \\
1.51 \sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 &
1.52 existential quantifier ($\exists$) \\
1.53 - \texttt{EX!} & \cdx{Ex1} & $(\alpha\To o)\To o$ & 10 &
1.54 + \isa{EX!} & \cdx{Ex1} & $(\alpha\To o)\To o$ & 10 &
1.55 unique existence ($\exists!$)
1.56 \end{tabular}
1.57 \index{*"E"X"! symbol}
1.58 @@ -195,36 +194,32 @@
1.59 FOL instantiates most of Isabelle's generic packages.
1.60 \begin{itemize}
1.61 \item
1.62 -It instantiates the simplifier. Both equality ($=$) and the biconditional
1.63 -($\bimp$) may be used for rewriting. Tactics such as \texttt{Asm_simp_tac} and
1.64 -\texttt{Full_simp_tac} refer to the default simpset (\texttt{simpset()}), which works for
1.65 -most purposes. Named simplification sets include \ttindexbold{IFOL_ss},
1.66 -for intuitionistic first-order logic, and \ttindexbold{FOL_ss},
1.67 -for classical logic. See the file
1.68 -\texttt{FOL/simpdata.ML} for a complete listing of the simplification
1.69 -rules%
1.70 -\iflabelundefined{sec:setting-up-simp}{}%
1.71 - {, and \S\ref{sec:setting-up-simp} for discussion}.
1.72 +It instantiates the simplifier, which is invoked through the method
1.73 +\isa{simp}. Both equality ($=$) and the biconditional
1.74 +($\bimp$) may be used for rewriting.
1.75
1.76 \item
1.77 -It instantiates the classical reasoner. See~\S\ref{fol-cla-prover}
1.78 +It instantiates the classical reasoner, which is invoked mainly through the
1.79 +methods \isa{blast} and \isa{auto}. See~\S\ref{fol-cla-prover}
1.80 for details.
1.81 -
1.82 -\item FOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for
1.83 - an equality throughout a subgoal and its hypotheses. This tactic uses FOL's
1.84 - general substitution rule.
1.85 +%
1.86 +%\item FOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for
1.87 +% an equality throughout a subgoal and its hypotheses. This tactic uses FOL's
1.88 +% general substitution rule.
1.89 \end{itemize}
1.90
1.91 \begin{warn}\index{simplification!of conjunctions}%
1.92 - Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The
1.93 + Simplifying $a=b\conj P(a)$ to $a=b\conj P(b)$ is often advantageous. The
1.94 left part of a conjunction helps in simplifying the right part. This effect
1.95 is not available by default: it can be slow. It can be obtained by
1.96 - including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
1.97 + including the theorem \isa{conj_cong}\index{*conj_cong (rule)}%
1.98 + as a congruence rule in
1.99 + simplification, \isa{simp cong:\ conj\_cong}.
1.100 \end{warn}
1.101
1.102
1.103 \section{Intuitionistic proof procedures} \label{fol-int-prover}
1.104 -Implication elimination (the rules~\texttt{mp} and~\texttt{impE}) pose
1.105 +Implication elimination (the rules~\isa{mp} and~\isa{impE}) pose
1.106 difficulties for automated proof. In intuitionistic logic, the assumption
1.107 $P\imp Q$ cannot be treated like $\neg P\disj Q$. Given $P\imp Q$, we may
1.108 use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated
1.109 @@ -238,21 +233,22 @@
1.110 \[ \infer[({\imp}E)]{Q}{P\imp Q &
1.111 \infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}}
1.112 \]
1.113 -The theorem prover for intuitionistic logic does not use~\texttt{impE}.\@
1.114 +The theorem prover for intuitionistic logic does not use~\isa{impE}.\@
1.115 Instead, it simplifies implications using derived rules
1.116 (Fig.\ts\ref{fol-int-derived}). It reduces the antecedents of implications
1.117 to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$.
1.118 The rules \tdx{conj_impE} and \tdx{disj_impE} are
1.119 straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and
1.120 $(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp
1.121 -S$. The other \ldots{\tt_impE} rules are unsafe; the method requires
1.122 +S$. The other \ldots\isa{\_impE} rules are unsafe; the method requires
1.123 backtracking. All the rules are derived in the same simple manner.
1.124
1.125 Dyckhoff has independently discovered similar rules, and (more importantly)
1.126 has demonstrated their completeness for propositional
1.127 logic~\cite{dyckhoff}. However, the tactics given below are not complete
1.128 for first-order logic because they discard universally quantified
1.129 -assumptions after a single use.
1.130 +assumptions after a single use. These are \ML{} functions, and are listed
1.131 +below with their \ML{} type:
1.132 \begin{ttbox}
1.133 mp_tac : int -> tactic
1.134 eq_mp_tac : int -> tactic
1.135 @@ -263,8 +259,13 @@
1.136 IntPr.fast_tac : int -> tactic
1.137 IntPr.best_tac : int -> tactic
1.138 \end{ttbox}
1.139 -Most of these belong to the structure \texttt{IntPr} and resemble the
1.140 -tactics of Isabelle's classical reasoner.
1.141 +Most of these belong to the structure \ML{} \texttt{IntPr} and resemble the
1.142 +tactics of Isabelle's classical reasoner. Note that you can use the
1.143 +\isa{tactic} method to call \ML{} tactics in an Isar script:
1.144 +\begin{isabelle}
1.145 +\isacommand{apply}\ (tactic\ {* IntPr.fast\_tac 1*})
1.146 +\end{isabelle}
1.147 +Here is a description of each tactic:
1.148
1.149 \begin{ttdescription}
1.150 \item[\ttindexbold{mp_tac} {\it i}]
1.151 @@ -336,14 +337,15 @@
1.152 classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see
1.153 Fig.\ts\ref{fol-cla-derived}).
1.154
1.155 -The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt
1.156 -Best_tac} refer to the default claset (\texttt{claset()}), which works for most
1.157 -purposes. Named clasets include \ttindexbold{prop_cs}, which includes the
1.158 -propositional rules, and \ttindexbold{FOL_cs}, which also includes quantifier
1.159 -rules. See the file \texttt{FOL/cladata.ML} for lists of the
1.160 -classical rules, and
1.161 +The classical reasoner is installed. The most useful methods are
1.162 +\isa{blast} (pure classical reasoning) and \isa{auto} (classical reasoning
1.163 +combined with simplification), but the full range of
1.164 +methods is available, including \isa{clarify},
1.165 +\isa{fast}, \isa{best} and \isa{force}.
1.166 + See the
1.167 \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
1.168 {Chap.\ts\ref{chap:classical}}
1.169 +and the \emph{Tutorial}~\cite{isa-tutorial}
1.170 for more discussion of classical proof methods.
1.171
1.172
1.173 @@ -352,106 +354,93 @@
1.174 \cite[pages~222--3]{paulson87}. Isabelle treats quantifiers differently
1.175 from {\sc lcf}-based theorem provers such as {\sc hol}.
1.176
1.177 -First, we specify that we are working in intuitionistic logic:
1.178 -\begin{ttbox}
1.179 -context IFOL.thy;
1.180 -\end{ttbox}
1.181 +The theory header must specify that we are working in intuitionistic
1.182 +logic:
1.183 +\begin{isabelle}
1.184 +\isacommand{theory}\ IFOL\_examples\ =\ IFOL:
1.185 +\end{isabelle}
1.186 The proof begins by entering the goal, then applying the rule $({\imp}I)$.
1.187 -\begin{ttbox}
1.188 -Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
1.189 -{\out Level 0}
1.190 -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.191 -{\out 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.192 -\ttbreak
1.193 -by (resolve_tac [impI] 1);
1.194 -{\out Level 1}
1.195 -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.196 -{\out 1. EX y. ALL x. Q(x,y) ==> ALL x. EX y. Q(x,y)}
1.197 -\end{ttbox}
1.198 +\begin{isabelle}
1.199 +\isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline
1.200 +\ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\
1.201 +\isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))
1.202 +\isanewline
1.203 +\isacommand{apply}\ (rule\ impI)\isanewline
1.204 +\ 1.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\
1.205 +\isasymLongrightarrow \ \isasymforall x.\ \isasymexists y.\ Q(x,\ y)
1.206 +\end{isabelle}
1.207 +Isabelle's output is shown as it would appear using Proof General.
1.208 In this example, we shall never have more than one subgoal. Applying
1.209 -$({\imp}I)$ replaces~\verb|-->| by~\verb|==>|, making
1.210 -\(\ex{y}\all{x}Q(x,y)\) an assumption. We have the choice of
1.211 +$({\imp}I)$ replaces~\isa{\isasymlongrightarrow}
1.212 +by~\isa{\isasymLongrightarrow}, so that
1.213 +\(\ex{y}\all{x}Q(x,y)\) becomes an assumption. We have the choice of
1.214 $({\exists}E)$ and $({\forall}I)$; let us try the latter.
1.215 -\begin{ttbox}
1.216 -by (resolve_tac [allI] 1);
1.217 -{\out Level 2}
1.218 -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.219 -{\out 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
1.220 -\end{ttbox}
1.221 -Applying $({\forall}I)$ replaces the \texttt{ALL~x} by \hbox{\tt!!x},
1.222 -changing the universal quantifier from object~($\forall$) to
1.223 -meta~($\Forall$). The bound variable is a {\bf parameter} of the
1.224 -subgoal. We now must choose between $({\exists}I)$ and $({\exists}E)$. What
1.225 -happens if the wrong rule is chosen?
1.226 -\begin{ttbox}
1.227 -by (resolve_tac [exI] 1);
1.228 -{\out Level 3}
1.229 -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.230 -{\out 1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
1.231 -\end{ttbox}
1.232 -The new subgoal~1 contains the function variable {\tt?y2}. Instantiating
1.233 -{\tt?y2} can replace~{\tt?y2(x)} by a term containing~\texttt{x}, even
1.234 -though~\texttt{x} is a bound variable. Now we analyse the assumption
1.235 +\begin{isabelle}
1.236 +\isacommand{apply}\ (rule\ allI)\isanewline
1.237 +\ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\
1.238 +\isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)\hfill\((*)\)
1.239 +\end{isabelle}
1.240 +Applying $({\forall}I)$ replaces the \isa{\isasymforall
1.241 +x} (in ASCII, \isa{ALL~x}) by \isa{\isasymAnd x}
1.242 +(or \isa{!!x}), replacing FOL's universal quantifier by Isabelle's
1.243 +meta universal quantifier. The bound variable is a {\bf parameter} of
1.244 +the subgoal. We now must choose between $({\exists}I)$ and
1.245 +$({\exists}E)$. What happens if the wrong rule is chosen?
1.246 +\begin{isabelle}
1.247 +\isacommand{apply}\ (rule\ exI)\isanewline
1.248 +\ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\
1.249 +\isasymLongrightarrow \ Q(x,\ ?y2(x))
1.250 +\end{isabelle}
1.251 +The new subgoal~1 contains the function variable \isa{?y2}. Instantiating
1.252 +\isa{?y2} can replace~\isa{?y2(x)} by a term containing~\isa{x}, even
1.253 +though~\isa{x} is a bound variable. Now we analyse the assumption
1.254 \(\exists y.\forall x. Q(x,y)\) using elimination rules:
1.255 -\begin{ttbox}
1.256 -by (eresolve_tac [exE] 1);
1.257 -{\out Level 4}
1.258 -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.259 -{\out 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
1.260 -\end{ttbox}
1.261 -Applying $(\exists E)$ has produced the parameter \texttt{y} and stripped the
1.262 +\begin{isabelle}
1.263 +\isacommand{apply}\ (erule\ exE)\isanewline
1.264 +\ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\ \isasymLongrightarrow \ Q(x,\ ?y2(x))
1.265 +\end{isabelle}
1.266 +Applying $(\exists E)$ has produced the parameter \isa{y} and stripped the
1.267 existential quantifier from the assumption. But the subgoal is unprovable:
1.268 -there is no way to unify \texttt{?y2(x)} with the bound variable~\texttt{y}.
1.269 -Using \texttt{choplev} we can return to the critical point. This time we
1.270 -apply $({\exists}E)$:
1.271 -\begin{ttbox}
1.272 -choplev 2;
1.273 -{\out Level 2}
1.274 -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.275 -{\out 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
1.276 -\ttbreak
1.277 -by (eresolve_tac [exE] 1);
1.278 -{\out Level 3}
1.279 -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.280 -{\out 1. !!x y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
1.281 -\end{ttbox}
1.282 +there is no way to unify \isa{?y2(x)} with the bound variable~\isa{y}.
1.283 +Using Proof General, we can return to the critical point, marked
1.284 +$(*)$ above. This time we apply $({\exists}E)$:
1.285 +\begin{isabelle}
1.286 +\isacommand{apply}\ (erule\ exE)\isanewline
1.287 +\ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\
1.288 +\isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)
1.289 +\end{isabelle}
1.290 We now have two parameters and no scheme variables. Applying
1.291 $({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are
1.292 applied to those parameters. Parameters should be produced early, as this
1.293 example demonstrates.
1.294 -\begin{ttbox}
1.295 -by (resolve_tac [exI] 1);
1.296 -{\out Level 4}
1.297 -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.298 -{\out 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y3(x,y))}
1.299 -\ttbreak
1.300 -by (eresolve_tac [allE] 1);
1.301 -{\out Level 5}
1.302 -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.303 -{\out 1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))}
1.304 -\end{ttbox}
1.305 -The subgoal has variables \texttt{?y3} and \texttt{?x4} applied to both
1.306 -parameters. The obvious projection functions unify {\tt?x4(x,y)} with~{\tt
1.307 -x} and \verb|?y3(x,y)| with~\texttt{y}.
1.308 -\begin{ttbox}
1.309 -by (assume_tac 1);
1.310 -{\out Level 6}
1.311 -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.312 -{\out No subgoals!}
1.313 -\end{ttbox}
1.314 -The theorem was proved in six tactic steps, not counting the abandoned
1.315 -ones. But proof checking is tedious; \ttindex{IntPr.fast_tac} proves the
1.316 -theorem in one step.
1.317 -\begin{ttbox}
1.318 -Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
1.319 -{\out Level 0}
1.320 -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.321 -{\out 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.322 -by (IntPr.fast_tac 1);
1.323 -{\out Level 1}
1.324 -{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.325 -{\out No subgoals!}
1.326 -\end{ttbox}
1.327 +\begin{isabelle}
1.328 +\isacommand{apply}\ (rule\ exI)\isanewline
1.329 +\ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\
1.330 +\isasymLongrightarrow \ Q(x,\ ?y3(x,\ y))
1.331 +\isanewline
1.332 +\isacommand{apply}\ (erule\ allE)\isanewline
1.333 +\ 1.\ \isasymAnd x\ y.\ Q(?x4(x,\ y),\ y)\ \isasymLongrightarrow \
1.334 +Q(x,\ ?y3(x,\ y))
1.335 +\end{isabelle}
1.336 +The subgoal has variables \isa{?y3} and \isa{?x4} applied to both
1.337 +parameters. The obvious projection functions unify \isa{?x4(x,y)} with~\isa{
1.338 +x} and \isa{?y3(x,y)} with~\isa{y}.
1.339 +\begin{isabelle}
1.340 +\isacommand{apply}\ assumption\isanewline
1.341 +No\ subgoals!\isanewline
1.342 +\isacommand{done}
1.343 +\end{isabelle}
1.344 +The theorem was proved in six method invocations, not counting the
1.345 +abandoned ones. But proof checking is tedious, and the \ML{} tactic
1.346 +\ttindex{IntPr.fast_tac} can prove the theorem in one step.
1.347 +\begin{isabelle}
1.348 +\isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline
1.349 +\ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\
1.350 +\isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))
1.351 +\isanewline
1.352 +\isacommand{by} (tactic {*IntPr.fast_tac 1*})\isanewline
1.353 +No\ subgoals!
1.354 +\end{isabelle}
1.355
1.356
1.357 \section{An example of intuitionistic negation}
1.358 @@ -463,168 +452,151 @@
1.359 28]{dummett}, $\neg P$ is classically provable if and only if it is
1.360 intuitionistically provable; therefore, $P$ is classically provable if and
1.361 only if $\neg\neg P$ is intuitionistically provable.%
1.362 -\footnote{Of course this holds only for propositional logic, not if $P$ is
1.363 - allowed to contain quantifiers.} Proving $\neg\neg P$ intuitionistically is
1.364 +\footnote{This remark holds only for propositional logic, not if $P$ is
1.365 + allowed to contain quantifiers.}
1.366 +%
1.367 +Proving $\neg\neg P$ intuitionistically is
1.368 much harder than proving~$P$ classically.
1.369
1.370 Our example is the double negation of the classical tautology $(P\imp
1.371 -Q)\disj (Q\imp P)$. When stating the goal, we command Isabelle to expand
1.372 -negations to implications using the definition $\neg P\equiv P\imp\bot$.
1.373 -This allows use of the special implication rules.
1.374 -\begin{ttbox}
1.375 -Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))";
1.376 -{\out Level 0}
1.377 -{\out ~ ~ ((P --> Q) | (Q --> P))}
1.378 -{\out 1. ((P --> Q) | (Q --> P) --> False) --> False}
1.379 -\end{ttbox}
1.380 -The first step is trivial.
1.381 -\begin{ttbox}
1.382 -by (resolve_tac [impI] 1);
1.383 -{\out Level 1}
1.384 -{\out ~ ~ ((P --> Q) | (Q --> P))}
1.385 -{\out 1. (P --> Q) | (Q --> P) --> False ==> False}
1.386 -\end{ttbox}
1.387 +Q)\disj (Q\imp P)$. The first step is apply the
1.388 +\isa{unfold} method, which expands
1.389 +negations to implications using the definition $\neg P\equiv P\imp\bot$
1.390 +and allows use of the special implication rules.
1.391 +\begin{isabelle}
1.392 +\isacommand{lemma}\ "\isachartilde \ \isachartilde \ ((P-->Q)\ |\ (Q-->P))"\isanewline
1.393 +\ 1.\ \isasymnot \ \isasymnot \ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P))
1.394 +\isanewline
1.395 +\isacommand{apply}\ (unfold\ not\_def)\isanewline
1.396 +\ 1.\ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False)\ \isasymlongrightarrow \ False%
1.397 +\end{isabelle}
1.398 +The next step is a trivial use of $(\imp I)$.
1.399 +\begin{isabelle}
1.400 +\isacommand{apply}\ (rule\ impI)\isanewline
1.401 +\ 1.\ (P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\ \isasymLongrightarrow \ False%
1.402 +\end{isabelle}
1.403 By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but
1.404 -that formula is not a theorem of intuitionistic logic. Instead we apply
1.405 -the specialized implication rule \tdx{disj_impE}. It splits the
1.406 +that formula is not a theorem of intuitionistic logic. Instead, we
1.407 +apply the specialized implication rule \tdx{disj_impE}. It splits the
1.408 assumption into two assumptions, one for each disjunct.
1.409 -\begin{ttbox}
1.410 -by (eresolve_tac [disj_impE] 1);
1.411 -{\out Level 2}
1.412 -{\out ~ ~ ((P --> Q) | (Q --> P))}
1.413 -{\out 1. [| (P --> Q) --> False; (Q --> P) --> False |] ==> False}
1.414 -\end{ttbox}
1.415 +\begin{isabelle}
1.416 +\isacommand{apply}\ (erule\ disj\_impE)\isanewline
1.417 +\ 1.\ \isasymlbrakk (P\ \isasymlongrightarrow \ Q)\ \isasymlongrightarrow \ False;\ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \
1.418 +False
1.419 +\end{isabelle}
1.420 We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but
1.421 their negations are inconsistent. Applying \tdx{imp_impE} breaks down
1.422 the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new
1.423 assumptions~$P$ and~$\neg Q$.
1.424 -\begin{ttbox}
1.425 -by (eresolve_tac [imp_impE] 1);
1.426 -{\out Level 3}
1.427 -{\out ~ ~ ((P --> Q) | (Q --> P))}
1.428 -{\out 1. [| (Q --> P) --> False; P; Q --> False |] ==> Q}
1.429 -{\out 2. [| (Q --> P) --> False; False |] ==> False}
1.430 -\end{ttbox}
1.431 +\begin{isabelle}
1.432 +\isacommand{apply}\ (erule\ imp\_impE)\isanewline
1.433 +\ 1.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ P;\ Q\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
1.434 +\ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \
1.435 +False
1.436 +\end{isabelle}
1.437 Subgoal~2 holds trivially; let us ignore it and continue working on
1.438 subgoal~1. Thanks to the assumption~$P$, we could prove $Q\imp P$;
1.439 applying \tdx{imp_impE} is simpler.
1.440 -\begin{ttbox}
1.441 -by (eresolve_tac [imp_impE] 1);
1.442 -{\out Level 4}
1.443 -{\out ~ ~ ((P --> Q) | (Q --> P))}
1.444 -{\out 1. [| P; Q --> False; Q; P --> False |] ==> P}
1.445 -{\out 2. [| P; Q --> False; False |] ==> Q}
1.446 -{\out 3. [| (Q --> P) --> False; False |] ==> False}
1.447 -\end{ttbox}
1.448 +\begin{isabelle}
1.449 +\ \isacommand{apply}\ (erule\ imp\_impE)\isanewline
1.450 +\ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ Q;\ P\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ P\isanewline
1.451 +\ 2.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
1.452 +\ 3.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ False%
1.453 +\end{isabelle}
1.454 The three subgoals are all trivial.
1.455 -\begin{ttbox}
1.456 -by (REPEAT (eresolve_tac [FalseE] 2));
1.457 -{\out Level 5}
1.458 -{\out ~ ~ ((P --> Q) | (Q --> P))}
1.459 -{\out 1. [| P; Q --> False; Q; P --> False |] ==> P}
1.460 -\ttbreak
1.461 -by (assume_tac 1);
1.462 -{\out Level 6}
1.463 -{\out ~ ~ ((P --> Q) | (Q --> P))}
1.464 -{\out No subgoals!}
1.465 -\end{ttbox}
1.466 -This proof is also trivial for \texttt{IntPr.fast_tac}.
1.467 +\begin{isabelle}
1.468 +\isacommand{apply}\ assumption\ \isanewline
1.469 +\ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\
1.470 +False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
1.471 +\ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\
1.472 +\isasymlongrightarrow \ False;\ False\isasymrbrakk \
1.473 +\isasymLongrightarrow \ False%
1.474 +\isanewline
1.475 +\isacommand{apply}\ (erule\ FalseE)+\isanewline
1.476 +No\ subgoals!\isanewline
1.477 +\isacommand{done}
1.478 +\end{isabelle}
1.479 +This proof is also trivial for the \ML{} tactic \isa{IntPr.fast_tac}.
1.480
1.481
1.482 \section{A classical example} \label{fol-cla-example}
1.483 To illustrate classical logic, we shall prove the theorem
1.484 $\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as
1.485 follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
1.486 -$\all{x}P(x)$ is true. Either way the theorem holds. First, we switch to
1.487 -classical logic:
1.488 -\begin{ttbox}
1.489 -context FOL.thy;
1.490 -\end{ttbox}
1.491 +$\all{x}P(x)$ is true. Either way the theorem holds. First, we must
1.492 +work in a theory based on classical logic:
1.493 +\begin{isabelle}
1.494 +\isacommand{theory}\ FOL\_examples\ =\ FOL:
1.495 +\end{isabelle}
1.496
1.497 The formal proof does not conform in any obvious way to the sketch given
1.498 -above. The key inference is the first one, \tdx{exCI}; this classical
1.499 -version of~$(\exists I)$ allows multiple instantiation of the quantifier.
1.500 -\begin{ttbox}
1.501 -Goal "EX y. ALL x. P(y)-->P(x)";
1.502 -{\out Level 0}
1.503 -{\out EX y. ALL x. P(y) --> P(x)}
1.504 -{\out 1. EX y. ALL x. P(y) --> P(x)}
1.505 -\ttbreak
1.506 -by (resolve_tac [exCI] 1);
1.507 -{\out Level 1}
1.508 -{\out EX y. ALL x. P(y) --> P(x)}
1.509 -{\out 1. ALL y. ~ (ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)}
1.510 -\end{ttbox}
1.511 -We can either exhibit a term {\tt?a} to satisfy the conclusion of
1.512 +above. Its key step is its first rule, \tdx{exCI}, a classical
1.513 +version of~$(\exists I)$ that allows multiple instantiation of the
1.514 +quantifier.
1.515 +\begin{isabelle}
1.516 +\isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline
1.517 +\ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x)
1.518 +\isanewline
1.519 +\isacommand{apply}\ (rule\ exCI)\isanewline
1.520 +\ 1.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ \isasymforall x.\ P(?a)\ \isasymlongrightarrow \ P(x)
1.521 +\end{isabelle}
1.522 +We can either exhibit a term \isa{?a} to satisfy the conclusion of
1.523 subgoal~1, or produce a contradiction from the assumption. The next
1.524 steps are routine.
1.525 -\begin{ttbox}
1.526 -by (resolve_tac [allI] 1);
1.527 -{\out Level 2}
1.528 -{\out EX y. ALL x. P(y) --> P(x)}
1.529 -{\out 1. !!x. ALL y. ~ (ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)}
1.530 -\ttbreak
1.531 -by (resolve_tac [impI] 1);
1.532 -{\out Level 3}
1.533 -{\out EX y. ALL x. P(y) --> P(x)}
1.534 -{\out 1. !!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)}
1.535 -\end{ttbox}
1.536 +\begin{isabelle}
1.537 +\isacommand{apply}\ (rule\ allI)\isanewline
1.538 +\ 1.\ \isasymAnd x.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ P(?a)\ \isasymlongrightarrow \ P(x)
1.539 +\isanewline
1.540 +\isacommand{apply}\ (rule\ impI)\isanewline
1.541 +\ 1.\ \isasymAnd x.\ \isasymlbrakk \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x));\ P(?a)\isasymrbrakk \ \isasymLongrightarrow \ P(x)
1.542 +\end{isabelle}
1.543 By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$
1.544 -in effect applies~$(\exists I)$ again.
1.545 -\begin{ttbox}
1.546 -by (eresolve_tac [allE] 1);
1.547 -{\out Level 4}
1.548 -{\out EX y. ALL x. P(y) --> P(x)}
1.549 -{\out 1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)}
1.550 -\end{ttbox}
1.551 +is equivalent to applying~$(\exists I)$ again.
1.552 +\begin{isabelle}
1.553 +\isacommand{apply}\ (erule\ allE)\isanewline
1.554 +\ 1.\ \isasymAnd x.\ \isasymlbrakk P(?a);\ \isasymnot \ (\isasymforall xa.\ P(?y3(x))\ \isasymlongrightarrow \ P(xa))\isasymrbrakk \ \isasymLongrightarrow \ P(x)
1.555 +\end{isabelle}
1.556 In classical logic, a negated assumption is equivalent to a conclusion. To
1.557 get this effect, we create a swapped version of $(\forall I)$ and apply it
1.558 -using \ttindex{eresolve_tac}; we could equivalently have applied $(\forall
1.559 -I)$ using \ttindex{swap_res_tac}.
1.560 -\begin{ttbox}
1.561 -allI RSN (2,swap);
1.562 -{\out val it = "[| ~(ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm}
1.563 -by (eresolve_tac [it] 1);
1.564 -{\out Level 5}
1.565 -{\out EX y. ALL x. P(y) --> P(x)}
1.566 -{\out 1. !!x xa. [| P(?a); ~ P(x) |] ==> P(?y3(x)) --> P(xa)}
1.567 -\end{ttbox}
1.568 -The previous conclusion, \texttt{P(x)}, has become a negated assumption.
1.569 -\begin{ttbox}
1.570 -by (resolve_tac [impI] 1);
1.571 -{\out Level 6}
1.572 -{\out EX y. ALL x. P(y) --> P(x)}
1.573 -{\out 1. !!x xa. [| P(?a); ~ P(x); P(?y3(x)) |] ==> P(xa)}
1.574 -\end{ttbox}
1.575 +using \ttindex{erule}.
1.576 +\begin{isabelle}
1.577 +\isacommand{apply}\ (erule\ allI\ [THEN\ [2]\ swap])\isanewline
1.578 +\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x)\isasymrbrakk \ \isasymLongrightarrow \ P(?y3(x))\ \isasymlongrightarrow \ P(xa)
1.579 +\end{isabelle}
1.580 +The operand of \isa{erule} above denotes the following theorem:
1.581 +\begin{isabelle}
1.582 +\ \ \ \ \isasymlbrakk \isasymnot \ (\isasymforall x.\ ?P1(x));\
1.583 +\isasymAnd x.\ \isasymnot \ ?P\ \isasymLongrightarrow \
1.584 +?P1(x)\isasymrbrakk \
1.585 +\isasymLongrightarrow \ ?P%
1.586 +\end{isabelle}
1.587 +The previous conclusion, \isa{P(x)}, has become a negated assumption.
1.588 +\begin{isabelle}
1.589 +\isacommand{apply}\ (rule\ impI)\isanewline
1.590 +\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(xa)
1.591 +\end{isabelle}
1.592 The subgoal has three assumptions. We produce a contradiction between the
1.593 -\index{assumptions!contradictory} assumptions~\verb|~P(x)| and~{\tt
1.594 - P(?y3(x))}. The proof never instantiates the unknown~{\tt?a}.
1.595 -\begin{ttbox}
1.596 -by (eresolve_tac [notE] 1);
1.597 -{\out Level 7}
1.598 -{\out EX y. ALL x. P(y) --> P(x)}
1.599 -{\out 1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)}
1.600 -\ttbreak
1.601 -by (assume_tac 1);
1.602 -{\out Level 8}
1.603 -{\out EX y. ALL x. P(y) --> P(x)}
1.604 -{\out No subgoals!}
1.605 -\end{ttbox}
1.606 -The civilised way to prove this theorem is through \ttindex{Blast_tac},
1.607 -which automatically uses the classical version of~$(\exists I)$:
1.608 -\begin{ttbox}
1.609 -Goal "EX y. ALL x. P(y)-->P(x)";
1.610 -{\out Level 0}
1.611 -{\out EX y. ALL x. P(y) --> P(x)}
1.612 -{\out 1. EX y. ALL x. P(y) --> P(x)}
1.613 -by (Blast_tac 1);
1.614 -{\out Depth = 0}
1.615 -{\out Depth = 1}
1.616 -{\out Depth = 2}
1.617 -{\out Level 1}
1.618 -{\out EX y. ALL x. P(y) --> P(x)}
1.619 -{\out No subgoals!}
1.620 -\end{ttbox}
1.621 +\index{assumptions!contradictory} assumptions~\isa{\isasymnot P(x)}
1.622 +and~\isa{P(?y3(x))}. The proof never instantiates the
1.623 +unknown~\isa{?a}.
1.624 +\begin{isabelle}
1.625 +\isacommand{apply}\ (erule\ notE)\isanewline
1.626 +\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(x)
1.627 +\isanewline
1.628 +\isacommand{apply}\ assumption\isanewline
1.629 +No\ subgoals!\isanewline
1.630 +\isacommand{done}
1.631 +\end{isabelle}
1.632 +The civilised way to prove this theorem is using the
1.633 +\methdx{blast} method, which automatically uses the classical form
1.634 +of the rule~$(\exists I)$:
1.635 +\begin{isabelle}
1.636 +\isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline
1.637 +\ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x)
1.638 +\isanewline
1.639 +\isacommand{by}\ blast\isanewline
1.640 +No\ subgoals!
1.641 +\end{isabelle}
1.642 If this theorem seems counterintuitive, then perhaps you are an
1.643 intuitionist. In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$
1.644 requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$,
1.645 @@ -655,17 +627,17 @@
1.646 classical logic, \texttt{FOL}, is extended with the constant
1.647 $if::[o,o,o]\To o$. The axiom \tdx{if_def} asserts the
1.648 equation~$(if)$.
1.649 -\begin{ttbox}
1.650 -If = FOL +
1.651 -consts if :: [o,o,o]=>o
1.652 -rules if_def "if(P,Q,R) == P&Q | ~P&R"
1.653 -end
1.654 -\end{ttbox}
1.655 +\begin{isabelle}
1.656 +\isacommand{theory}\ If\ =\ FOL:\isanewline
1.657 +\isacommand{constdefs}\isanewline
1.658 +\ \ if\ ::\ "[o,o,o]=>o"\isanewline
1.659 +\ \ \ "if(P,Q,R)\ ==\ P\&Q\ |\ \isachartilde P\&R"
1.660 +\end{isabelle}
1.661 We create the file \texttt{If.thy} containing these declarations. (This file
1.662 is on directory \texttt{FOL/ex} in the Isabelle distribution.) Typing
1.663 -\begin{ttbox}
1.664 +\begin{isabelle}
1.665 use_thy "If";
1.666 -\end{ttbox}
1.667 +\end{isabelle}
1.668 loads that theory and sets it to be the current context.
1.669
1.670
1.671 @@ -673,264 +645,205 @@
1.672
1.673 The derivations of the introduction and elimination rules demonstrate the
1.674 methods for rewriting with definitions. Classical reasoning is required,
1.675 -so we use \texttt{blast_tac}.
1.676 +so we use \isa{blast}.
1.677
1.678 The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$,
1.679 -concludes $if(P,Q,R)$. We propose the conclusion as the main goal
1.680 -using~\ttindex{Goalw}, which uses \texttt{if_def} to rewrite occurrences
1.681 -of $if$ in the subgoal.
1.682 -\begin{ttbox}
1.683 -val prems = Goalw [if_def]
1.684 - "[| P ==> Q; ~ P ==> R |] ==> if(P,Q,R)";
1.685 -{\out Level 0}
1.686 -{\out if(P,Q,R)}
1.687 -{\out 1. P & Q | ~ P & R}
1.688 -\end{ttbox}
1.689 -The premises (bound to the {\ML} variable \texttt{prems}) are passed as
1.690 -introduction rules to \ttindex{blast_tac}. Remember that \texttt{claset()} refers
1.691 -to the default classical set.
1.692 -\begin{ttbox}
1.693 -by (blast_tac (claset() addIs prems) 1);
1.694 -{\out Level 1}
1.695 -{\out if(P,Q,R)}
1.696 -{\out No subgoals!}
1.697 -qed "ifI";
1.698 -\end{ttbox}
1.699 +concludes $if(P,Q,R)$. We propose this lemma and immediately simplify
1.700 +using \isa{if\_def} to expand the definition of \isa{if} in the
1.701 +subgoal.
1.702 +\begin{isabelle}
1.703 +\isacommand{lemma}\ ifI: "[|\ P\ ==>\ Q;\ \isachartilde P\ ==>\ R\
1.704 +|]\ ==>\ if(P,Q,R)"\isanewline
1.705 +\ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ Q,\ R)
1.706 +\isanewline
1.707 +\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
1.708 +\ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \
1.709 +R
1.710 +\end{isabelle}
1.711 +The rule's premises, although expressed using meta-level implication
1.712 +(\isa{\isasymLongrightarrow}) are passed as ordinary implications to
1.713 +\methdx{blast}.
1.714 +\begin{isabelle}
1.715 +\isacommand{apply}\ blast\isanewline
1.716 +No\ subgoals!\isanewline
1.717 +\isacommand{done}
1.718 +\end{isabelle}
1.719
1.720
1.721 \subsection{Deriving the elimination rule}
1.722 The elimination rule has three premises, two of which are themselves rules.
1.723 The conclusion is simply $S$.
1.724 -\begin{ttbox}
1.725 -val major::prems = Goalw [if_def]
1.726 - "[| if(P,Q,R); [| P; Q |] ==> S; [| ~ P; R |] ==> S |] ==> S";
1.727 -{\out Level 0}
1.728 -{\out S}
1.729 -{\out 1. S}
1.730 -\end{ttbox}
1.731 -The major premise contains an occurrence of~$if$, but the version returned
1.732 -by \ttindex{Goalw} (and bound to the {\ML} variable~\texttt{major}) has the
1.733 -definition expanded. Now \ttindex{cut_facts_tac} inserts~\texttt{major} as an
1.734 -assumption in the subgoal, so that \ttindex{blast_tac} can break it down.
1.735 -\begin{ttbox}
1.736 -by (cut_facts_tac [major] 1);
1.737 -{\out Level 1}
1.738 -{\out S}
1.739 -{\out 1. P & Q | ~ P & R ==> S}
1.740 -\ttbreak
1.741 -by (blast_tac (claset() addIs prems) 1);
1.742 -{\out Level 2}
1.743 -{\out S}
1.744 -{\out No subgoals!}
1.745 -qed "ifE";
1.746 -\end{ttbox}
1.747 -As you may recall from
1.748 -\iflabelundefined{definitions}{{\em Introduction to Isabelle}}%
1.749 - {\S\ref{definitions}}, there are other
1.750 -ways of treating definitions when deriving a rule. We can start the
1.751 -proof using \texttt{Goal}, which does not expand definitions, instead of
1.752 -\texttt{Goalw}. We can use \ttindex{rew_tac}
1.753 -to expand definitions in the subgoals---perhaps after calling
1.754 -\ttindex{cut_facts_tac} to insert the rule's premises. We can use
1.755 -\ttindex{rewrite_rule}, which is a meta-inference rule, to expand
1.756 -definitions in the premises directly.
1.757 +\begin{isabelle}
1.758 +\isacommand{lemma}\ ifE:\isanewline
1.759 +\ \ \ "[|\ if(P,Q,R);\ \ [|P;\ Q|]\ ==>\ S;\ [|\isachartilde P;\ R|]\ ==>\ S\ |]\ ==>\ S"\isanewline
1.760 +\ 1.\ \isasymlbrakk if(P,\ Q,\ R);\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S%
1.761 +\isanewline
1.762 +\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
1.763 +\ 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%
1.764 +\end{isabelle}
1.765 +The proof script is the same as before: \isa{simp} followed by
1.766 +\isa{blast}:
1.767 +\begin{isabelle}
1.768 +\isacommand{apply}\ blast\isanewline
1.769 +No\ subgoals!\isanewline
1.770 +\isacommand{done}
1.771 +\end{isabelle}
1.772
1.773
1.774 \subsection{Using the derived rules}
1.775 -The rules just derived have been saved with the {\ML} names \tdx{ifI}
1.776 -and~\tdx{ifE}. They permit natural proofs of theorems such as the
1.777 -following:
1.778 +Our new derived rules, \tdx{ifI} and~\tdx{ifE}, permit natural
1.779 +proofs of theorems such as the following:
1.780 \begin{eqnarray*}
1.781 if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\
1.782 if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B))
1.783 \end{eqnarray*}
1.784 Proofs also require the classical reasoning rules and the $\bimp$
1.785 -introduction rule (called~\tdx{iffI}: do not confuse with~\texttt{ifI}).
1.786 +introduction rule (called~\tdx{iffI}: do not confuse with~\isa{ifI}).
1.787
1.788 To display the $if$-rules in action, let us analyse a proof step by step.
1.789 -\begin{ttbox}
1.790 -Goal "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
1.791 -{\out Level 0}
1.792 -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.793 -{\out 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.794 -\ttbreak
1.795 -by (resolve_tac [iffI] 1);
1.796 -{\out Level 1}
1.797 -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.798 -{\out 1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))}
1.799 -{\out 2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
1.800 -\end{ttbox}
1.801 +\begin{isabelle}
1.802 +\isacommand{lemma}\ if\_commute:\isanewline
1.803 +\ \ \ \ \ "if(P,\ if(Q,A,B),\
1.804 +if(Q,C,D))\ <->\ if(Q,\ if(P,A,C),\ if(P,B,D))"\isanewline
1.805 +\isacommand{apply}\ (rule\ iffI)\isanewline
1.806 +\ 1.\ if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))\ \isasymLongrightarrow \isanewline
1.807 +\isaindent{\ 1.\ }if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
1.808 +\ 2.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
1.809 +\isaindent{\ 2.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
1.810 +\end{isabelle}
1.811 The $if$-elimination rule can be applied twice in succession.
1.812 -\begin{ttbox}
1.813 -by (eresolve_tac [ifE] 1);
1.814 -{\out Level 2}
1.815 -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.816 -{\out 1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.817 -{\out 2. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.818 -{\out 3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
1.819 -\ttbreak
1.820 -by (eresolve_tac [ifE] 1);
1.821 -{\out Level 3}
1.822 -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.823 -{\out 1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.824 -{\out 2. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.825 -{\out 3. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.826 -{\out 4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
1.827 -\end{ttbox}
1.828 +\begin{isabelle}
1.829 +\isacommand{apply}\ (erule\ ifE)\isanewline
1.830 +\ 1.\ \isasymlbrakk P;\ if(Q,\ A,\ B)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
1.831 +\ 2.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
1.832 +\ 3.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
1.833 +\isaindent{\ 3.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
1.834 +\isanewline
1.835 +\isacommand{apply}\ (erule\ ifE)\isanewline
1.836 +\ 1.\ \isasymlbrakk P;\ Q;\ A\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
1.837 +\ 2.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
1.838 +\ 3.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
1.839 +\ 4.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
1.840 +\isaindent{\ 4.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
1.841 +\end{isabelle}
1.842 %
1.843 In the first two subgoals, all assumptions have been reduced to atoms. Now
1.844 $if$-introduction can be applied. Observe how the $if$-rules break down
1.845 occurrences of $if$ when they become the outermost connective.
1.846 -\begin{ttbox}
1.847 -by (resolve_tac [ifI] 1);
1.848 -{\out Level 4}
1.849 -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.850 -{\out 1. [| P; Q; A; Q |] ==> if(P,A,C)}
1.851 -{\out 2. [| P; Q; A; ~ Q |] ==> if(P,B,D)}
1.852 -{\out 3. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.853 -{\out 4. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.854 -{\out 5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
1.855 -\ttbreak
1.856 -by (resolve_tac [ifI] 1);
1.857 -{\out Level 5}
1.858 -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.859 -{\out 1. [| P; Q; A; Q; P |] ==> A}
1.860 -{\out 2. [| P; Q; A; Q; ~ P |] ==> C}
1.861 -{\out 3. [| P; Q; A; ~ Q |] ==> if(P,B,D)}
1.862 -{\out 4. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.863 -{\out 5. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.864 -{\out 6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
1.865 -\end{ttbox}
1.866 +\begin{isabelle}
1.867 +\isacommand{apply}\ (rule\ ifI)\isanewline
1.868 +\ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ A,\ C)\isanewline
1.869 +\ 2.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline
1.870 +\ 3.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
1.871 +\ 4.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
1.872 +\ 5.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
1.873 +\isaindent{\ 5.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
1.874 +\isanewline
1.875 +\isacommand{apply}\ (rule\ ifI)\isanewline
1.876 +\ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline
1.877 +\ 2.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \ C\isanewline
1.878 +\ 3.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline
1.879 +\ 4.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
1.880 +\ 5.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
1.881 +\ 6.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
1.882 +\isaindent{\ 6.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
1.883 +\end{isabelle}
1.884 Where do we stand? The first subgoal holds by assumption; the second and
1.885 third, by contradiction. This is getting tedious. We could use the classical
1.886 reasoner, but first let us extend the default claset with the derived rules
1.887 for~$if$.
1.888 -\begin{ttbox}
1.889 -AddSIs [ifI];
1.890 -AddSEs [ifE];
1.891 -\end{ttbox}
1.892 -Now we can revert to the
1.893 -initial proof state and let \ttindex{blast_tac} solve it.
1.894 -\begin{ttbox}
1.895 -choplev 0;
1.896 -{\out Level 0}
1.897 -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.898 -{\out 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.899 -by (Blast_tac 1);
1.900 -{\out Level 1}
1.901 -{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.902 -{\out No subgoals!}
1.903 -\end{ttbox}
1.904 -This tactic also solves the other example.
1.905 -\begin{ttbox}
1.906 -Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
1.907 -{\out Level 0}
1.908 -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
1.909 -{\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
1.910 -\ttbreak
1.911 -by (Blast_tac 1);
1.912 -{\out Level 1}
1.913 -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
1.914 -{\out No subgoals!}
1.915 -\end{ttbox}
1.916 +\begin{isabelle}
1.917 +\isacommand{declare}\ ifI\ [intro!]\isanewline
1.918 +\isacommand{declare}\ ifE\ [elim!]
1.919 +\end{isabelle}
1.920 +With these declarations, we could have proved this theorem with a single
1.921 +call to \isa{blast}. Here is another example:
1.922 +\begin{isabelle}
1.923 +\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline
1.924 +\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B))
1.925 +\isanewline
1.926 +\isacommand{by}\ blast
1.927 +\end{isabelle}
1.928
1.929
1.930 \subsection{Derived rules versus definitions}
1.931 Dispensing with the derived rules, we can treat $if$ as an
1.932 abbreviation, and let \ttindex{blast_tac} prove the expanded formula. Let
1.933 us redo the previous proof:
1.934 -\begin{ttbox}
1.935 -choplev 0;
1.936 -{\out Level 0}
1.937 -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
1.938 -{\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
1.939 -\end{ttbox}
1.940 -This time, simply unfold using the definition of $if$:
1.941 -\begin{ttbox}
1.942 -by (rewtac if_def);
1.943 -{\out Level 1}
1.944 -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
1.945 -{\out 1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
1.946 -{\out P & (Q & A | ~ Q & B) | ~ P & (R & A | ~ R & B)}
1.947 -\end{ttbox}
1.948 -We are left with a subgoal in pure first-order logic, which is why the
1.949 -classical reasoner can prove it given \texttt{FOL_cs} alone. (We could, of
1.950 -course, have used \texttt{Blast_tac}.)
1.951 -\begin{ttbox}
1.952 -by (blast_tac FOL_cs 1);
1.953 -{\out Level 2}
1.954 -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
1.955 -{\out No subgoals!}
1.956 -\end{ttbox}
1.957 +\begin{isabelle}
1.958 +\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline
1.959 +\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B))
1.960 +\end{isabelle}
1.961 +This time, we simply unfold using the definition of $if$:
1.962 +\begin{isabelle}
1.963 +\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
1.964 +\ 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
1.965 +\isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ A\ \isasymor \ \isasymnot \ R\ \isasymand \ B)
1.966 +\end{isabelle}
1.967 +We are left with a subgoal in pure first-order logic, and it falls to
1.968 +\isa{blast}:
1.969 +\begin{isabelle}
1.970 +\isacommand{apply}\ blast\isanewline
1.971 +No\ subgoals!
1.972 +\end{isabelle}
1.973 Expanding definitions reduces the extended logic to the base logic. This
1.974 -approach has its merits --- especially if the prover for the base logic is
1.975 -good --- but can be slow. In these examples, proofs using the default
1.976 -claset (which includes the derived rules) run about six times faster
1.977 -than proofs using \texttt{FOL_cs}.
1.978 +approach has its merits, but it can be slow. In these examples, proofs
1.979 +using the derived rules for~\isa{if} run about six
1.980 +times faster than proofs using just the rules of first-order logic.
1.981
1.982 -Expanding definitions also complicates error diagnosis. Suppose we are having
1.983 -difficulties in proving some goal. If by expanding definitions we have
1.984 -made it unreadable, then we have little hope of diagnosing the problem.
1.985 +Expanding definitions can also make it harder to diagnose errors.
1.986 +Suppose we are having difficulties in proving some goal. If by expanding
1.987 +definitions we have made it unreadable, then we have little hope of
1.988 +diagnosing the problem.
1.989
1.990 Attempts at program verification often yield invalid assertions.
1.991 Let us try to prove one:
1.992 -\begin{ttbox}
1.993 -Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
1.994 -{\out Level 0}
1.995 -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
1.996 -{\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
1.997 -by (Blast_tac 1);
1.998 -{\out by: tactic failed}
1.999 -\end{ttbox}
1.1000 -This failure message is uninformative, but we can get a closer look at the
1.1001 -situation by applying \ttindex{Step_tac}.
1.1002 -\begin{ttbox}
1.1003 -by (REPEAT (Step_tac 1));
1.1004 -{\out Level 1}
1.1005 -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
1.1006 -{\out 1. [| A; ~ P; R; ~ P; R |] ==> B}
1.1007 -{\out 2. [| B; ~ P; ~ R; ~ P; ~ R |] ==> A}
1.1008 -{\out 3. [| ~ P; R; B; ~ P; R |] ==> A}
1.1009 -{\out 4. [| ~ P; ~ R; A; ~ B; ~ P |] ==> R}
1.1010 -\end{ttbox}
1.1011 +\begin{isabelle}
1.1012 +\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline
1.1013 +\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\
1.1014 +A))
1.1015 +\end{isabelle}
1.1016 +Calling \isa{blast} yields an uninformative failure message. We can
1.1017 +get a closer look at the situation by applying \methdx{auto}.
1.1018 +\begin{isabelle}
1.1019 +\isacommand{apply}\ auto\isanewline
1.1020 +\ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline
1.1021 +\ 2.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline
1.1022 +\ 3.\ \isasymlbrakk B;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline
1.1023 +\ 4.\ \isasymlbrakk \isasymnot \ R;\ A;\ \isasymnot \ B;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \
1.1024 +False
1.1025 +\end{isabelle}
1.1026 Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false
1.1027 while~$R$ and~$A$ are true. This truth assignment reduces the main goal to
1.1028 $true\bimp false$, which is of course invalid.
1.1029
1.1030 We can repeat this analysis by expanding definitions, using just the rules of
1.1031 -FOL:
1.1032 -\begin{ttbox}
1.1033 -choplev 0;
1.1034 -{\out Level 0}
1.1035 -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
1.1036 -{\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
1.1037 -\ttbreak
1.1038 -by (rewtac if_def);
1.1039 -{\out Level 1}
1.1040 -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
1.1041 -{\out 1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
1.1042 -{\out P & (Q & A | ~ Q & B) | ~ P & (R & B | ~ R & A)}
1.1043 -by (blast_tac FOL_cs 1);
1.1044 -{\out by: tactic failed}
1.1045 -\end{ttbox}
1.1046 -Again we apply \ttindex{step_tac}:
1.1047 -\begin{ttbox}
1.1048 -by (REPEAT (step_tac FOL_cs 1));
1.1049 -{\out Level 2}
1.1050 -{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
1.1051 -{\out 1. [| A; ~ P; R; ~ P; R; ~ False |] ==> B}
1.1052 -{\out 2. [| A; ~ P; R; R; ~ False; ~ B; ~ B |] ==> Q}
1.1053 -{\out 3. [| B; ~ P; ~ R; ~ P; ~ A |] ==> R}
1.1054 -{\out 4. [| B; ~ P; ~ R; ~ Q; ~ A |] ==> R}
1.1055 -{\out 5. [| B; ~ R; ~ P; ~ A; ~ R; Q; ~ False |] ==> A}
1.1056 -{\out 6. [| ~ P; R; B; ~ P; R; ~ False |] ==> A}
1.1057 -{\out 7. [| ~ P; ~ R; A; ~ B; ~ R |] ==> P}
1.1058 -{\out 8. [| ~ P; ~ R; A; ~ B; ~ R |] ==> Q}
1.1059 -\end{ttbox}
1.1060 +first-order logic:
1.1061 +\begin{isabelle}
1.1062 +\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline
1.1063 +\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\
1.1064 +A))
1.1065 +\isanewline
1.1066 +\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
1.1067 +\ 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
1.1068 +\isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ B\ \isasymor \ \isasymnot \ R\ \isasymand \ A)
1.1069 +\end{isabelle}
1.1070 +Again \isa{blast} would fail, so we try \methdx{auto}:
1.1071 +\begin{isabelle}
1.1072 +\isacommand{apply}\ (auto)\ \isanewline
1.1073 +\ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline
1.1074 +\ 2.\ \isasymlbrakk A;\ \isasymnot \ P;\ R;\ \isasymnot \ B\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
1.1075 +\ 3.\ \isasymlbrakk B;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
1.1076 +\ 4.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ A;\ \isasymnot \ R;\ Q\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
1.1077 +\ 5.\ \isasymlbrakk B;\ \isasymnot \ Q;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
1.1078 +\ 6.\ \isasymlbrakk B;\ \isasymnot \ A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
1.1079 +\ 7.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
1.1080 +\ 8.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ Q%
1.1081 +\end{isabelle}
1.1082 Subgoal~1 yields the same countermodel as before. But each proof step has
1.1083 taken six times as long, and the final result contains twice as many subgoals.
1.1084
1.1085 -Expanding definitions causes a great increase in complexity. This is why
1.1086 -the classical prover has been designed to accept derived rules.
1.1087 +Expanding your definitions usually makes proofs more difficult. This is
1.1088 +why the classical prover has been designed to accept derived rules.
1.1089
1.1090 \index{first-order logic|)}