doc-src/ZF/FOL.tex
 author haftmann Tue Oct 10 13:59:12 2006 +0200 (2006-10-10) changeset 20950 981fa0ce23ed parent 14158 15bab630ae31 child 30099 dde11464969c permissions -rw-r--r--
 paulson@6121  1 %% $Id$  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@14154  363 \isacommand{theory}\ IFOL\_examples\ =\ IFOL:  paulson@14154  364 \end{isabelle}  paulson@6121  365 The proof begins by entering the goal, then applying the rule $({\imp}I)$.  paulson@14154  366 \begin{isabelle}  paulson@14154  367 \isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline  paulson@14154  368 \ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\  paulson@14154  369 \isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))  paulson@14154  370 \isanewline  paulson@14154  371 \isacommand{apply}\ (rule\ impI)\isanewline  paulson@14154  372 \ 1.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\  paulson@14154  373 \isasymLongrightarrow \ \isasymforall x.\ \isasymexists y.\ Q(x,\ y)  paulson@14154  374 \end{isabelle}  paulson@14154  375 Isabelle's output is shown as it would appear using Proof General.  paulson@6121  376 In this example, we shall never have more than one subgoal. Applying  paulson@14154  377 $({\imp}I)$ replaces~\isa{\isasymlongrightarrow}  paulson@14154  378 by~\isa{\isasymLongrightarrow}, so that  paulson@14154  379 $$\ex{y}\all{x}Q(x,y)$$ becomes an assumption. We have the choice of  paulson@6121  380 $({\exists}E)$ and $({\forall}I)$; let us try the latter.  paulson@14154  381 \begin{isabelle}  paulson@14154  382 \isacommand{apply}\ (rule\ allI)\isanewline  paulson@14154  383 \ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\  paulson@14154  384 \isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)\hfill$$(*)$$  paulson@14154  385 \end{isabelle}  paulson@14154  386 Applying $({\forall}I)$ replaces the \isa{\isasymforall  paulson@14154  387 x} (in ASCII, \isa{ALL~x}) by \isa{\isasymAnd x}  paulson@14154  388 (or \isa{!!x}), replacing FOL's universal quantifier by Isabelle's  paulson@14154  389 meta universal quantifier. The bound variable is a {\bf parameter} of  paulson@14154  390 the subgoal. We now must choose between $({\exists}I)$ and  paulson@14154  391 $({\exists}E)$. What happens if the wrong rule is chosen?  paulson@14154  392 \begin{isabelle}  paulson@14154  393 \isacommand{apply}\ (rule\ exI)\isanewline  paulson@14154  394 \ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\  paulson@14154  395 \isasymLongrightarrow \ Q(x,\ ?y2(x))  paulson@14154  396 \end{isabelle}  paulson@14154  397 The new subgoal~1 contains the function variable \isa{?y2}. Instantiating  paulson@14154  398 \isa{?y2} can replace~\isa{?y2(x)} by a term containing~\isa{x}, even  paulson@14154  399 though~\isa{x} is a bound variable. Now we analyse the assumption  paulson@6121  400 $$\exists y.\forall x. Q(x,y)$$ using elimination rules:  paulson@14154  401 \begin{isabelle}  paulson@14154  402 \isacommand{apply}\ (erule\ exE)\isanewline  paulson@14154  403 \ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\ \isasymLongrightarrow \ Q(x,\ ?y2(x))  paulson@14154  404 \end{isabelle}  paulson@14154  405 Applying $(\exists E)$ has produced the parameter \isa{y} and stripped the  paulson@6121  406 existential quantifier from the assumption. But the subgoal is unprovable:  paulson@14154  407 there is no way to unify \isa{?y2(x)} with the bound variable~\isa{y}.  paulson@14154  408 Using Proof General, we can return to the critical point, marked  paulson@14154  409 $(*)$ above. This time we apply $({\exists}E)$:  paulson@14154  410 \begin{isabelle}  paulson@14154  411 \isacommand{apply}\ (erule\ exE)\isanewline  paulson@14154  412 \ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\  paulson@14154  413 \isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)  paulson@14154  414 \end{isabelle}  paulson@6121  415 We now have two parameters and no scheme variables. Applying  paulson@6121  416 $({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are  paulson@6121  417 applied to those parameters. Parameters should be produced early, as this  paulson@6121  418 example demonstrates.  paulson@14154  419 \begin{isabelle}  paulson@14154  420 \isacommand{apply}\ (rule\ exI)\isanewline  paulson@14154  421 \ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\  paulson@14154  422 \isasymLongrightarrow \ Q(x,\ ?y3(x,\ y))  paulson@14154  423 \isanewline  paulson@14154  424 \isacommand{apply}\ (erule\ allE)\isanewline  paulson@14154  425 \ 1.\ \isasymAnd x\ y.\ Q(?x4(x,\ y),\ y)\ \isasymLongrightarrow \  paulson@14154  426 Q(x,\ ?y3(x,\ y))  paulson@14154  427 \end{isabelle}  paulson@14154  428 The subgoal has variables \isa{?y3} and \isa{?x4} applied to both  paulson@14154  429 parameters. The obvious projection functions unify \isa{?x4(x,y)} with~\isa{  paulson@14154  430 x} and \isa{?y3(x,y)} with~\isa{y}.  paulson@14154  431 \begin{isabelle}  paulson@14154  432 \isacommand{apply}\ assumption\isanewline  paulson@14154  433 No\ subgoals!\isanewline  paulson@14154  434 \isacommand{done}  paulson@14154  435 \end{isabelle}  paulson@14154  436 The theorem was proved in six method invocations, not counting the  paulson@14154  437 abandoned ones. But proof checking is tedious, and the \ML{} tactic  paulson@14154  438 \ttindex{IntPr.fast_tac} can prove the theorem in one step.  paulson@14154  439 \begin{isabelle}  paulson@14154  440 \isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline  paulson@14154  441 \ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\  paulson@14154  442 \isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))  paulson@14154  443 \isanewline  paulson@14154  444 \isacommand{by} (tactic {*IntPr.fast_tac 1*})\isanewline  paulson@14154  445 No\ subgoals!  paulson@14154  446 \end{isabelle}  paulson@6121  447 paulson@6121  448 paulson@6121  449 \section{An example of intuitionistic negation}  paulson@6121  450 The following example demonstrates the specialized forms of implication  paulson@6121  451 elimination. Even propositional formulae can be difficult to prove from  paulson@6121  452 the basic rules; the specialized rules help considerably.  paulson@6121  453 paulson@6121  454 Propositional examples are easy to invent. As Dummett notes~\cite[page  paulson@6121  455 28]{dummett}, $\neg P$ is classically provable if and only if it is  paulson@6121  456 intuitionistically provable; therefore, $P$ is classically provable if and  paulson@6121  457 only if $\neg\neg P$ is intuitionistically provable.%  paulson@14154  458 \footnote{This remark holds only for propositional logic, not if $P$ is  paulson@14154  459  allowed to contain quantifiers.}  paulson@14154  460 %  paulson@14154  461 Proving $\neg\neg P$ intuitionistically is  paulson@6121  462 much harder than proving~$P$ classically.  paulson@6121  463 paulson@6121  464 Our example is the double negation of the classical tautology $(P\imp  paulson@14154  465 Q)\disj (Q\imp P)$. The first step is apply the  paulson@14154  466 \isa{unfold} method, which expands  paulson@14154  467 negations to implications using the definition $\neg P\equiv P\imp\bot$  paulson@14154  468 and allows use of the special implication rules.  paulson@14154  469 \begin{isabelle}  paulson@14154  470 \isacommand{lemma}\ "\isachartilde \ \isachartilde \ ((P-->Q)\ |\ (Q-->P))"\isanewline  paulson@14154  471 \ 1.\ \isasymnot \ \isasymnot \ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P))  paulson@14154  472 \isanewline  paulson@14154  473 \isacommand{apply}\ (unfold\ not\_def)\isanewline  paulson@14154  474 \ 1.\ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False)\ \isasymlongrightarrow \ False%  paulson@14154  475 \end{isabelle}  paulson@14154  476 The next step is a trivial use of $(\imp I)$.  paulson@14154  477 \begin{isabelle}  paulson@14154  478 \isacommand{apply}\ (rule\ impI)\isanewline  paulson@14154  479 \ 1.\ (P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\ \isasymLongrightarrow \ False%  paulson@14154  480 \end{isabelle}  paulson@6121  481 By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but  paulson@14154  482 that formula is not a theorem of intuitionistic logic. Instead, we  paulson@14154  483 apply the specialized implication rule \tdx{disj_impE}. It splits the  paulson@6121  484 assumption into two assumptions, one for each disjunct.  paulson@14154  485 \begin{isabelle}  paulson@14154  486 \isacommand{apply}\ (erule\ disj\_impE)\isanewline  paulson@14154  487 \ 1.\ \isasymlbrakk (P\ \isasymlongrightarrow \ Q)\ \isasymlongrightarrow \ False;\ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \  paulson@14154  488 False  paulson@14154  489 \end{isabelle}  paulson@6121  490 We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but  paulson@6121  491 their negations are inconsistent. Applying \tdx{imp_impE} breaks down  paulson@6121  492 the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new  paulson@6121  493 assumptions~$P$ and~$\neg Q$.  paulson@14154  494 \begin{isabelle}  paulson@14154  495 \isacommand{apply}\ (erule\ imp\_impE)\isanewline  paulson@14154  496 \ 1.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ P;\ Q\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline  paulson@14154  497 \ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \  paulson@14154  498 False  paulson@14154  499 \end{isabelle}  paulson@6121  500 Subgoal~2 holds trivially; let us ignore it and continue working on  paulson@6121  501 subgoal~1. Thanks to the assumption~$P$, we could prove $Q\imp P$;  paulson@6121  502 applying \tdx{imp_impE} is simpler.  paulson@14154  503 \begin{isabelle}  paulson@14154  504 \ \isacommand{apply}\ (erule\ imp\_impE)\isanewline  paulson@14154  505 \ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ Q;\ P\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ P\isanewline  paulson@14154  506 \ 2.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline  paulson@14154  507 \ 3.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ False%  paulson@14154  508 \end{isabelle}  paulson@6121  509 The three subgoals are all trivial.  paulson@14154  510 \begin{isabelle}  paulson@14154  511 \isacommand{apply}\ assumption\ \isanewline  paulson@14154  512 \ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\  paulson@14154  513 False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline  paulson@14154  514 \ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\  paulson@14154  515 \isasymlongrightarrow \ False;\ False\isasymrbrakk \  paulson@14154  516 \isasymLongrightarrow \ False%  paulson@14154  517 \isanewline  paulson@14154  518 \isacommand{apply}\ (erule\ FalseE)+\isanewline  paulson@14154  519 No\ subgoals!\isanewline  paulson@14154  520 \isacommand{done}  paulson@14154  521 \end{isabelle}  paulson@14154  522 This proof is also trivial for the \ML{} tactic \isa{IntPr.fast_tac}.  paulson@6121  523 paulson@6121  524 paulson@6121  525 \section{A classical example} \label{fol-cla-example}  paulson@6121  526 To illustrate classical logic, we shall prove the theorem  paulson@6121  527 $\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as  paulson@6121  528 follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise  paulson@14154  529 $\all{x}P(x)$ is true. Either way the theorem holds. First, we must  paulson@14158  530 work in a theory based on classical logic, the theory \isa{FOL}:  paulson@14154  531 \begin{isabelle}  paulson@14154  532 \isacommand{theory}\ FOL\_examples\ =\ FOL:  paulson@14154  533 \end{isabelle}  paulson@6121  534 paulson@6121  535 The formal proof does not conform in any obvious way to the sketch given  paulson@14154  536 above. Its key step is its first rule, \tdx{exCI}, a classical  paulson@14154  537 version of~$(\exists I)$ that allows multiple instantiation of the  paulson@14154  538 quantifier.  paulson@14154  539 \begin{isabelle}  paulson@14154  540 \isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline  paulson@14154  541 \ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x)  paulson@14154  542 \isanewline  paulson@14154  543 \isacommand{apply}\ (rule\ exCI)\isanewline  paulson@14154  544 \ 1.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ \isasymforall x.\ P(?a)\ \isasymlongrightarrow \ P(x)  paulson@14154  545 \end{isabelle}  paulson@14154  546 We can either exhibit a term \isa{?a} to satisfy the conclusion of  paulson@6121  547 subgoal~1, or produce a contradiction from the assumption. The next  paulson@6121  548 steps are routine.  paulson@14154  549 \begin{isabelle}  paulson@14154  550 \isacommand{apply}\ (rule\ allI)\isanewline  paulson@14154  551 \ 1.\ \isasymAnd x.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ P(?a)\ \isasymlongrightarrow \ P(x)  paulson@14154  552 \isanewline  paulson@14154  553 \isacommand{apply}\ (rule\ impI)\isanewline  paulson@14154  554 \ 1.\ \isasymAnd x.\ \isasymlbrakk \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x));\ P(?a)\isasymrbrakk \ \isasymLongrightarrow \ P(x)  paulson@14154  555 \end{isabelle}  paulson@6121  556 By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$  paulson@14154  557 is equivalent to applying~$(\exists I)$ again.  paulson@14154  558 \begin{isabelle}  paulson@14154  559 \isacommand{apply}\ (erule\ allE)\isanewline  paulson@14154  560 \ 1.\ \isasymAnd x.\ \isasymlbrakk P(?a);\ \isasymnot \ (\isasymforall xa.\ P(?y3(x))\ \isasymlongrightarrow \ P(xa))\isasymrbrakk \ \isasymLongrightarrow \ P(x)  paulson@14154  561 \end{isabelle}  paulson@6121  562 In classical logic, a negated assumption is equivalent to a conclusion. To  paulson@8249  563 get this effect, we create a swapped version of $(\forall I)$ and apply it  paulson@14154  564 using \ttindex{erule}.  paulson@14154  565 \begin{isabelle}  paulson@14154  566 \isacommand{apply}\ (erule\ allI\ [THEN\ [2]\ swap])\isanewline  paulson@14154  567 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x)\isasymrbrakk \ \isasymLongrightarrow \ P(?y3(x))\ \isasymlongrightarrow \ P(xa)  paulson@14154  568 \end{isabelle}  paulson@14154  569 The operand of \isa{erule} above denotes the following theorem:  paulson@14154  570 \begin{isabelle}  paulson@14154  571 \ \ \ \ \isasymlbrakk \isasymnot \ (\isasymforall x.\ ?P1(x));\  paulson@14154  572 \isasymAnd x.\ \isasymnot \ ?P\ \isasymLongrightarrow \  paulson@14154  573 ?P1(x)\isasymrbrakk \  paulson@14154  574 \isasymLongrightarrow \ ?P%  paulson@14154  575 \end{isabelle}  paulson@14154  576 The previous conclusion, \isa{P(x)}, has become a negated assumption.  paulson@14154  577 \begin{isabelle}  paulson@14154  578 \isacommand{apply}\ (rule\ impI)\isanewline  paulson@14154  579 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(xa)  paulson@14154  580 \end{isabelle}  paulson@6121  581 The subgoal has three assumptions. We produce a contradiction between the  paulson@14154  582 \index{assumptions!contradictory} assumptions~\isa{\isasymnot P(x)}  paulson@14154  583 and~\isa{P(?y3(x))}. The proof never instantiates the  paulson@14154  584 unknown~\isa{?a}.  paulson@14154  585 \begin{isabelle}  paulson@14154  586 \isacommand{apply}\ (erule\ notE)\isanewline  paulson@14154  587 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(x)  paulson@14154  588 \isanewline  paulson@14154  589 \isacommand{apply}\ assumption\isanewline  paulson@14154  590 No\ subgoals!\isanewline  paulson@14154  591 \isacommand{done}  paulson@14154  592 \end{isabelle}  paulson@14154  593 The civilised way to prove this theorem is using the  paulson@14154  594 \methdx{blast} method, which automatically uses the classical form  paulson@14154  595 of the rule~$(\exists I)$:  paulson@14154  596 \begin{isabelle}  paulson@14154  597 \isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline  paulson@14154  598 \ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x)  paulson@14154  599 \isanewline  paulson@14154  600 \isacommand{by}\ blast\isanewline  paulson@14154  601 No\ subgoals!  paulson@14154  602 \end{isabelle}  paulson@6121  603 If this theorem seems counterintuitive, then perhaps you are an  paulson@6121  604 intuitionist. In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$  paulson@6121  605 requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$,  paulson@6121  606 which we cannot do without further knowledge about~$P$.  paulson@6121  607 paulson@6121  608 paulson@6121  609 \section{Derived rules and the classical tactics}  paulson@6121  610 Classical first-order logic can be extended with the propositional  paulson@6121  611 connective $if(P,Q,R)$, where  paulson@6121  612 $$if(P,Q,R) \equiv P\conj Q \disj \neg P \conj R. \eqno(if)$$  paulson@6121  613 Theorems about $if$ can be proved by treating this as an abbreviation,  paulson@6121  614 replacing $if(P,Q,R)$ by $P\conj Q \disj \neg P \conj R$ in subgoals. But  paulson@6121  615 this duplicates~$P$, causing an exponential blowup and an unreadable  paulson@6121  616 formula. Introducing further abbreviations makes the problem worse.  paulson@6121  617 paulson@6121  618 Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$  paulson@6121  619 directly, without reference to its definition. The simple identity  paulson@6121  620 $if(P,Q,R) \,\bimp\, (P\imp Q)\conj (\neg P\imp R)$  paulson@6121  621 suggests that the  paulson@6121  622 $if$-introduction rule should be  paulson@6121  623 $\infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]} & \infer*{R}{[\neg P]}}$  paulson@6121  624 The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the  paulson@6121  625 elimination rules for~$\disj$ and~$\conj$.  paulson@6121  626 $\infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]}  paulson@6121  627  & \infer*{S}{[\neg P,R]}}  paulson@6121  628 $  paulson@6121  629 Having made these plans, we get down to work with Isabelle. The theory of  paulson@6121  630 classical logic, \texttt{FOL}, is extended with the constant  paulson@6121  631 $if::[o,o,o]\To o$. The axiom \tdx{if_def} asserts the  paulson@6121  632 equation~$(if)$.  paulson@14154  633 \begin{isabelle}  paulson@14154  634 \isacommand{theory}\ If\ =\ FOL:\isanewline  paulson@14154  635 \isacommand{constdefs}\isanewline  paulson@14154  636 \ \ if\ ::\ "[o,o,o]=>o"\isanewline  paulson@14154  637 \ \ \ "if(P,Q,R)\ ==\ P\&Q\ |\ \isachartilde P\&R"  paulson@14154  638 \end{isabelle}  paulson@6121  639 We create the file \texttt{If.thy} containing these declarations. (This file  paulson@6121  640 is on directory \texttt{FOL/ex} in the Isabelle distribution.) Typing  paulson@14154  641 \begin{isabelle}  paulson@6121  642 use_thy "If";  paulson@14154  643 \end{isabelle}  paulson@6121  644 loads that theory and sets it to be the current context.  paulson@6121  645 paulson@6121  646 paulson@6121  647 \subsection{Deriving the introduction rule}  paulson@6121  648 paulson@6121  649 The derivations of the introduction and elimination rules demonstrate the  paulson@6121  650 methods for rewriting with definitions. Classical reasoning is required,  paulson@14154  651 so we use \isa{blast}.  paulson@6121  652 paulson@6121  653 The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$,  paulson@14154  654 concludes $if(P,Q,R)$. We propose this lemma and immediately simplify  paulson@14154  655 using \isa{if\_def} to expand the definition of \isa{if} in the  paulson@14154  656 subgoal.  paulson@14154  657 \begin{isabelle}  paulson@14154  658 \isacommand{lemma}\ ifI: "[|\ P\ ==>\ Q;\ \isachartilde P\ ==>\ R\  paulson@14154  659 |]\ ==>\ if(P,Q,R)"\isanewline  paulson@14154  660 \ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ Q,\ R)  paulson@14154  661 \isanewline  paulson@14154  662 \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline  paulson@14154  663 \ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \  paulson@14154  664 R  paulson@14154  665 \end{isabelle}  paulson@14154  666 The rule's premises, although expressed using meta-level implication  paulson@14154  667 (\isa{\isasymLongrightarrow}) are passed as ordinary implications to  paulson@14154  668 \methdx{blast}.  paulson@14154  669 \begin{isabelle}  paulson@14154  670 \isacommand{apply}\ blast\isanewline  paulson@14154  671 No\ subgoals!\isanewline  paulson@14154  672 \isacommand{done}  paulson@14154  673 \end{isabelle}  paulson@6121  674 paulson@6121  675 paulson@6121  676 \subsection{Deriving the elimination rule}  paulson@6121  677 The elimination rule has three premises, two of which are themselves rules.  paulson@6121  678 The conclusion is simply $S$.  paulson@14154  679 \begin{isabelle}  paulson@14154  680 \isacommand{lemma}\ ifE:\isanewline  paulson@14154  681 \ \ \ "[|\ if(P,Q,R);\ \ [|P;\ Q|]\ ==>\ S;\ [|\isachartilde P;\ R|]\ ==>\ S\ |]\ ==>\ S"\isanewline  paulson@14154  682 \ 1.\ \isasymlbrakk if(P,\ Q,\ R);\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S%  paulson@14154  683 \isanewline  paulson@14154  684 \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline  paulson@14154  685 \ 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  686 \end{isabelle}  paulson@14154  687 The proof script is the same as before: \isa{simp} followed by  paulson@14154  688 \isa{blast}:  paulson@14154  689 \begin{isabelle}  paulson@14154  690 \isacommand{apply}\ blast\isanewline  paulson@14154  691 No\ subgoals!\isanewline  paulson@14154  692 \isacommand{done}  paulson@14154  693 \end{isabelle}  paulson@6121  694 paulson@6121  695 paulson@6121  696 \subsection{Using the derived rules}  paulson@14154  697 Our new derived rules, \tdx{ifI} and~\tdx{ifE}, permit natural  paulson@14154  698 proofs of theorems such as the following:  paulson@6121  699 \begin{eqnarray*}  paulson@6121  700  if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\  paulson@6121  701  if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B))  paulson@6121  702 \end{eqnarray*}  paulson@6121  703 Proofs also require the classical reasoning rules and the $\bimp$  paulson@14154  704 introduction rule (called~\tdx{iffI}: do not confuse with~\isa{ifI}).  paulson@6121  705 paulson@6121  706 To display the $if$-rules in action, let us analyse a proof step by step.  paulson@14154  707 \begin{isabelle}  paulson@14154  708 \isacommand{lemma}\ if\_commute:\isanewline  paulson@14154  709 \ \ \ \ \ "if(P,\ if(Q,A,B),\  paulson@14154  710 if(Q,C,D))\ <->\ if(Q,\ if(P,A,C),\ if(P,B,D))"\isanewline  paulson@14154  711 \isacommand{apply}\ (rule\ iffI)\isanewline  paulson@14154  712 \ 1.\ if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))\ \isasymLongrightarrow \isanewline  paulson@14154  713 \isaindent{\ 1.\ }if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline  paulson@14154  714 \ 2.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline  paulson@14154  715 \isaindent{\ 2.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))  paulson@14154  716 \end{isabelle}  paulson@6121  717 The $if$-elimination rule can be applied twice in succession.  paulson@14154  718 \begin{isabelle}  paulson@14154  719 \isacommand{apply}\ (erule\ ifE)\isanewline  paulson@14154  720 \ 1.\ \isasymlbrakk P;\ if(Q,\ A,\ B)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline  paulson@14154  721 \ 2.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline  paulson@14154  722 \ 3.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline  paulson@14154  723 \isaindent{\ 3.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))  paulson@14154  724 \isanewline  paulson@14154  725 \isacommand{apply}\ (erule\ ifE)\isanewline  paulson@14154  726 \ 1.\ \isasymlbrakk P;\ Q;\ A\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline  paulson@14154  727 \ 2.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline  paulson@14154  728 \ 3.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline  paulson@14154  729 \ 4.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline  paulson@14154  730 \isaindent{\ 4.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))  paulson@14154  731 \end{isabelle}  paulson@6121  732 %  paulson@6121  733 In the first two subgoals, all assumptions have been reduced to atoms. Now  paulson@6121  734 $if$-introduction can be applied. Observe how the $if$-rules break down  paulson@6121  735 occurrences of $if$ when they become the outermost connective.  paulson@14154  736 \begin{isabelle}  paulson@14154  737 \isacommand{apply}\ (rule\ ifI)\isanewline  paulson@14154  738 \ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ A,\ C)\isanewline  paulson@14154  739 \ 2.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline  paulson@14154  740 \ 3.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline  paulson@14154  741 \ 4.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline  paulson@14154  742 \ 5.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline  paulson@14154  743 \isaindent{\ 5.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))  paulson@14154  744 \isanewline  paulson@14154  745 \isacommand{apply}\ (rule\ ifI)\isanewline  paulson@14154  746 \ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline  paulson@14154  747 \ 2.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \ C\isanewline  paulson@14154  748 \ 3.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline  paulson@14154  749 \ 4.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline  paulson@14154  750 \ 5.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline  paulson@14154  751 \ 6.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline  paulson@14154  752 \isaindent{\ 6.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))  paulson@14154  753 \end{isabelle}  paulson@6121  754 Where do we stand? The first subgoal holds by assumption; the second and  paulson@6121  755 third, by contradiction. This is getting tedious. We could use the classical  paulson@6121  756 reasoner, but first let us extend the default claset with the derived rules  paulson@6121  757 for~$if$.  paulson@14154  758 \begin{isabelle}  paulson@14154  759 \isacommand{declare}\ ifI\ [intro!]\isanewline  paulson@14154  760 \isacommand{declare}\ ifE\ [elim!]  paulson@14154  761 \end{isabelle}  paulson@14154  762 With these declarations, we could have proved this theorem with a single  paulson@14154  763 call to \isa{blast}. Here is another example:  paulson@14154  764 \begin{isabelle}  paulson@14154  765 \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline  paulson@14154  766 \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B))  paulson@14154  767 \isanewline  paulson@14154  768 \isacommand{by}\ blast  paulson@14154  769 \end{isabelle}  paulson@6121  770 paulson@6121  771 paulson@6121  772 \subsection{Derived rules versus definitions}  paulson@6121  773 Dispensing with the derived rules, we can treat $if$ as an  paulson@6121  774 abbreviation, and let \ttindex{blast_tac} prove the expanded formula. Let  paulson@6121  775 us redo the previous proof:  paulson@14154  776 \begin{isabelle}  paulson@14154  777 \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline  paulson@14154  778 \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B))  paulson@14154  779 \end{isabelle}  paulson@14154  780 This time, we simply unfold using the definition of $if$:  paulson@14154  781 \begin{isabelle}  paulson@14154  782 \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline  paulson@14154  783 \ 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  784 \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  785 \end{isabelle}  paulson@14154  786 We are left with a subgoal in pure first-order logic, and it falls to  paulson@14154  787 \isa{blast}:  paulson@14154  788 \begin{isabelle}  paulson@14154  789 \isacommand{apply}\ blast\isanewline  paulson@14154  790 No\ subgoals!  paulson@14154  791 \end{isabelle}  paulson@6121  792 Expanding definitions reduces the extended logic to the base logic. This  paulson@14154  793 approach has its merits, but it can be slow. In these examples, proofs  paulson@14154  794 using the derived rules for~\isa{if} run about six  paulson@14154  795 times faster than proofs using just the rules of first-order logic.  paulson@6121  796 paulson@14154  797 Expanding definitions can also make it harder to diagnose errors.  paulson@14154  798 Suppose we are having difficulties in proving some goal. If by expanding  paulson@14154  799 definitions we have made it unreadable, then we have little hope of  paulson@14154  800 diagnosing the problem.  paulson@6121  801 paulson@6121  802 Attempts at program verification often yield invalid assertions.  paulson@6121  803 Let us try to prove one:  paulson@14154  804 \begin{isabelle}  paulson@14154  805 \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline  paulson@14154  806 \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\  paulson@14154  807 A))  paulson@14154  808 \end{isabelle}  paulson@14154  809 Calling \isa{blast} yields an uninformative failure message. We can  paulson@14154  810 get a closer look at the situation by applying \methdx{auto}.  paulson@14154  811 \begin{isabelle}  paulson@14154  812 \isacommand{apply}\ auto\isanewline  paulson@14154  813 \ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline  paulson@14154  814 \ 2.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline  paulson@14154  815 \ 3.\ \isasymlbrakk B;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline  paulson@14154  816 \ 4.\ \isasymlbrakk \isasymnot \ R;\ A;\ \isasymnot \ B;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \  paulson@14154  817 False  paulson@14154  818 \end{isabelle}  paulson@6121  819 Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false  paulson@6121  820 while~$R$ and~$A$ are true. This truth assignment reduces the main goal to  paulson@6121  821 $true\bimp false$, which is of course invalid.  paulson@6121  822 wenzelm@9695  823 We can repeat this analysis by expanding definitions, using just the rules of  paulson@14154  824 first-order logic:  paulson@14154  825 \begin{isabelle}  paulson@14154  826 \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline  paulson@14154  827 \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\  paulson@14154  828 A))  paulson@14154  829 \isanewline  paulson@14154  830 \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline  paulson@14154  831 \ 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  832 \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  833 \end{isabelle}  paulson@14154  834 Again \isa{blast} would fail, so we try \methdx{auto}:  paulson@14154  835 \begin{isabelle}  paulson@14154  836 \isacommand{apply}\ (auto)\ \isanewline  paulson@14154  837 \ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline  paulson@14154  838 \ 2.\ \isasymlbrakk A;\ \isasymnot \ P;\ R;\ \isasymnot \ B\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline  paulson@14154  839 \ 3.\ \isasymlbrakk B;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline  paulson@14154  840 \ 4.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ A;\ \isasymnot \ R;\ Q\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline  paulson@14154  841 \ 5.\ \isasymlbrakk B;\ \isasymnot \ Q;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline  paulson@14154  842 \ 6.\ \isasymlbrakk B;\ \isasymnot \ A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline  paulson@14154  843 \ 7.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline  paulson@14154  844 \ 8.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ Q%  paulson@14154  845 \end{isabelle}  paulson@6121  846 Subgoal~1 yields the same countermodel as before. But each proof step has  paulson@6121  847 taken six times as long, and the final result contains twice as many subgoals.  paulson@6121  848 paulson@14154  849 Expanding your definitions usually makes proofs more difficult. This is  paulson@14154  850 why the classical prover has been designed to accept derived rules.  paulson@6121  851 paulson@6121  852 \index{first-order logic|)}