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