paulson@30036: %!TEX root = logics-ZF.tex paulson@6121: \chapter{First-Order Logic} paulson@6121: \index{first-order logic|(} paulson@6121: paulson@6121: Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc paulson@6121: nk}. Intuitionistic first-order logic is defined first, as theory paulson@6121: \thydx{IFOL}. Classical logic, theory \thydx{FOL}, is paulson@6121: obtained by adding the double negation rule. Basic proof procedures are paulson@6121: provided. The intuitionistic prover works with derived rules to simplify paulson@6121: implications in the assumptions. Classical~\texttt{FOL} employs Isabelle's paulson@6121: classical reasoner, which simulates a sequent calculus. paulson@6121: paulson@6121: \section{Syntax and rules of inference} paulson@6121: The logic is many-sorted, using Isabelle's type classes. The class of paulson@14154: first-order terms is called \cldx{term} and is a subclass of \isa{logic}. paulson@6121: No types of individuals are provided, but extensions can define types such paulson@14154: as \isa{nat::term} and type constructors such as \isa{list::(term)term} paulson@6121: (see the examples directory, \texttt{FOL/ex}). Below, the type variable paulson@14154: $\alpha$ ranges over class \isa{term}; the equality symbol and quantifiers paulson@6121: are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which paulson@6121: belongs to class~\cldx{logic}. Figure~\ref{fol-syntax} gives the syntax. paulson@6121: Note that $a$\verb|~=|$b$ is translated to $\neg(a=b)$. paulson@6121: paulson@14154: Figure~\ref{fol-rules} shows the inference rules with their names. paulson@6121: Negation is defined in the usual way for intuitionistic logic; $\neg P$ paulson@6121: abbreviates $P\imp\bot$. The biconditional~($\bimp$) is defined through paulson@6121: $\conj$ and~$\imp$; introduction and elimination rules are derived for it. paulson@6121: paulson@6121: The unique existence quantifier, $\exists!x.P(x)$, is defined in terms paulson@6121: of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested paulson@6121: quantifications. For instance, $\exists!x\;y.P(x,y)$ abbreviates paulson@6121: $\exists!x. \exists!y.P(x,y)$; note that this does not mean that there paulson@6121: exists a unique pair $(x,y)$ satisfying~$P(x,y)$. paulson@6121: paulson@6121: Some intuitionistic derived rules are shown in paulson@14154: Fig.\ts\ref{fol-int-derived}, again with their names. These include paulson@6121: rules for the defined symbols $\neg$, $\bimp$ and $\exists!$. Natural paulson@6121: deduction typically involves a combination of forward and backward paulson@6121: reasoning, particularly with the destruction rules $(\conj E)$, paulson@6121: $({\imp}E)$, and~$(\forall E)$. Isabelle's backward style handles these paulson@6121: rules badly, so sequent-style rules are derived to eliminate conjunctions, paulson@6121: implications, and universal quantifiers. Used with elim-resolution, paulson@6121: \tdx{allE} eliminates a universal quantifier while \tdx{all_dupE} paulson@14154: re-inserts the quantified formula for later use. The rules paulson@14154: \isa{conj\_impE}, etc., support the intuitionistic proof procedure paulson@6121: (see~\S\ref{fol-int-prover}). paulson@6121: paulson@14154: See the on-line theory library for complete listings of the rules and paulson@6121: derived rules. paulson@6121: paulson@6121: \begin{figure} paulson@6121: \begin{center} paulson@6121: \begin{tabular}{rrr} paulson@6121: \it name &\it meta-type & \it description \\ paulson@6121: \cdx{Trueprop}& $o\To prop$ & coercion to $prop$\\ paulson@6121: \cdx{Not} & $o\To o$ & negation ($\neg$) \\ paulson@6121: \cdx{True} & $o$ & tautology ($\top$) \\ paulson@6121: \cdx{False} & $o$ & absurdity ($\bot$) paulson@6121: \end{tabular} paulson@6121: \end{center} paulson@6121: \subcaption{Constants} paulson@6121: paulson@6121: \begin{center} paulson@6121: \begin{tabular}{llrrr} paulson@6121: \it symbol &\it name &\it meta-type & \it priority & \it description \\ paulson@6121: \sdx{ALL} & \cdx{All} & $(\alpha\To o)\To o$ & 10 & paulson@6121: universal quantifier ($\forall$) \\ paulson@6121: \sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 & paulson@6121: existential quantifier ($\exists$) \\ paulson@14154: \isa{EX!} & \cdx{Ex1} & $(\alpha\To o)\To o$ & 10 & paulson@6121: unique existence ($\exists!$) paulson@6121: \end{tabular} paulson@6121: \index{*"E"X"! symbol} paulson@6121: \end{center} paulson@6121: \subcaption{Binders} paulson@6121: paulson@6121: \begin{center} paulson@6121: \index{*"= symbol} paulson@6121: \index{&@{\tt\&} symbol} paulson@6121: \index{*"| symbol} paulson@6121: \index{*"-"-"> symbol} paulson@6121: \index{*"<"-"> symbol} paulson@6121: \begin{tabular}{rrrr} paulson@6121: \it symbol & \it meta-type & \it priority & \it description \\ paulson@6121: \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\ paulson@6121: \tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\ paulson@6121: \tt | & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\ paulson@6121: \tt --> & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\ paulson@6121: \tt <-> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$) paulson@6121: \end{tabular} paulson@6121: \end{center} paulson@6121: \subcaption{Infixes} paulson@6121: paulson@6121: \dquotes paulson@6121: \[\begin{array}{rcl} paulson@6121: formula & = & \hbox{expression of type~$o$} \\ paulson@6121: & | & term " = " term \quad| \quad term " \ttilde= " term \\ paulson@6121: & | & "\ttilde\ " formula \\ paulson@6121: & | & formula " \& " formula \\ paulson@6121: & | & formula " | " formula \\ paulson@6121: & | & formula " --> " formula \\ paulson@6121: & | & formula " <-> " formula \\ paulson@6121: & | & "ALL~" id~id^* " . " formula \\ paulson@6121: & | & "EX~~" id~id^* " . " formula \\ paulson@6121: & | & "EX!~" id~id^* " . " formula paulson@6121: \end{array} paulson@6121: \] paulson@6121: \subcaption{Grammar} paulson@6121: \caption{Syntax of \texttt{FOL}} \label{fol-syntax} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@6121: \begin{ttbox} paulson@6121: \tdx{refl} a=a paulson@6121: \tdx{subst} [| a=b; P(a) |] ==> P(b) paulson@6121: \subcaption{Equality rules} paulson@6121: paulson@6121: \tdx{conjI} [| P; Q |] ==> P&Q paulson@6121: \tdx{conjunct1} P&Q ==> P paulson@6121: \tdx{conjunct2} P&Q ==> Q paulson@6121: paulson@6121: \tdx{disjI1} P ==> P|Q paulson@6121: \tdx{disjI2} Q ==> P|Q paulson@6121: \tdx{disjE} [| P|Q; P ==> R; Q ==> R |] ==> R paulson@6121: paulson@6121: \tdx{impI} (P ==> Q) ==> P-->Q paulson@6121: \tdx{mp} [| P-->Q; P |] ==> Q paulson@6121: paulson@6121: \tdx{FalseE} False ==> P paulson@6121: \subcaption{Propositional rules} paulson@6121: paulson@6121: \tdx{allI} (!!x. P(x)) ==> (ALL x.P(x)) paulson@6121: \tdx{spec} (ALL x.P(x)) ==> P(x) paulson@6121: paulson@6121: \tdx{exI} P(x) ==> (EX x.P(x)) paulson@6121: \tdx{exE} [| EX x.P(x); !!x. P(x) ==> R |] ==> R paulson@6121: \subcaption{Quantifier rules} paulson@6121: paulson@6121: \tdx{True_def} True == False-->False paulson@6121: \tdx{not_def} ~P == P-->False paulson@6121: \tdx{iff_def} P<->Q == (P-->Q) & (Q-->P) paulson@6121: \tdx{ex1_def} EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x) paulson@6121: \subcaption{Definitions} paulson@6121: \end{ttbox} paulson@6121: paulson@6121: \caption{Rules of intuitionistic logic} \label{fol-rules} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@6121: \begin{ttbox} paulson@6121: \tdx{sym} a=b ==> b=a paulson@6121: \tdx{trans} [| a=b; b=c |] ==> a=c paulson@6121: \tdx{ssubst} [| b=a; P(a) |] ==> P(b) paulson@6121: \subcaption{Derived equality rules} paulson@6121: paulson@6121: \tdx{TrueI} True paulson@6121: paulson@6121: \tdx{notI} (P ==> False) ==> ~P paulson@6121: \tdx{notE} [| ~P; P |] ==> R paulson@6121: paulson@6121: \tdx{iffI} [| P ==> Q; Q ==> P |] ==> P<->Q paulson@6121: \tdx{iffE} [| P <-> Q; [| P-->Q; Q-->P |] ==> R |] ==> R paulson@6121: \tdx{iffD1} [| P <-> Q; P |] ==> Q paulson@6121: \tdx{iffD2} [| P <-> Q; Q |] ==> P paulson@6121: paulson@6121: \tdx{ex1I} [| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x) paulson@6121: \tdx{ex1E} [| EX! x.P(x); !!x.[| P(x); ALL y. P(y) --> y=x |] ==> R paulson@6121: |] ==> R paulson@6121: \subcaption{Derived rules for \(\top\), \(\neg\), \(\bimp\) and \(\exists!\)} paulson@6121: paulson@6121: \tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R paulson@6121: \tdx{impE} [| P-->Q; P; Q ==> R |] ==> R paulson@6121: \tdx{allE} [| ALL x.P(x); P(x) ==> R |] ==> R paulson@6121: \tdx{all_dupE} [| ALL x.P(x); [| P(x); ALL x.P(x) |] ==> R |] ==> R paulson@6121: \subcaption{Sequent-style elimination rules} paulson@6121: paulson@6121: \tdx{conj_impE} [| (P&Q)-->S; P-->(Q-->S) ==> R |] ==> R paulson@6121: \tdx{disj_impE} [| (P|Q)-->S; [| P-->S; Q-->S |] ==> R |] ==> R paulson@6121: \tdx{imp_impE} [| (P-->Q)-->S; [| P; Q-->S |] ==> Q; S ==> R |] ==> R paulson@6121: \tdx{not_impE} [| ~P --> S; P ==> False; S ==> R |] ==> R paulson@6121: \tdx{iff_impE} [| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P; paulson@6121: S ==> R |] ==> R paulson@6121: \tdx{all_impE} [| (ALL x.P(x))-->S; !!x.P(x); S ==> R |] ==> R paulson@6121: \tdx{ex_impE} [| (EX x.P(x))-->S; P(a)-->S ==> R |] ==> R paulson@6121: \end{ttbox} paulson@6121: \subcaption{Intuitionistic simplification of implication} paulson@6121: \caption{Derived rules for intuitionistic logic} \label{fol-int-derived} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \section{Generic packages} wenzelm@9695: FOL instantiates most of Isabelle's generic packages. paulson@6121: \begin{itemize} paulson@6121: \item paulson@14154: It instantiates the simplifier, which is invoked through the method paulson@14154: \isa{simp}. Both equality ($=$) and the biconditional paulson@14154: ($\bimp$) may be used for rewriting. paulson@6121: paulson@6121: \item paulson@14154: It instantiates the classical reasoner, which is invoked mainly through the paulson@14154: methods \isa{blast} and \isa{auto}. See~\S\ref{fol-cla-prover} paulson@6121: for details. paulson@14154: % paulson@14154: %\item FOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for paulson@14154: % an equality throughout a subgoal and its hypotheses. This tactic uses FOL's paulson@14154: % general substitution rule. paulson@6121: \end{itemize} paulson@6121: paulson@6121: \begin{warn}\index{simplification!of conjunctions}% paulson@14154: Simplifying $a=b\conj P(a)$ to $a=b\conj P(b)$ is often advantageous. The paulson@6121: left part of a conjunction helps in simplifying the right part. This effect paulson@6121: is not available by default: it can be slow. It can be obtained by paulson@14154: including the theorem \isa{conj_cong}\index{*conj_cong (rule)}% paulson@14154: as a congruence rule in paulson@14154: simplification, \isa{simp cong:\ conj\_cong}. paulson@6121: \end{warn} paulson@6121: paulson@6121: paulson@6121: \section{Intuitionistic proof procedures} \label{fol-int-prover} paulson@14154: Implication elimination (the rules~\isa{mp} and~\isa{impE}) pose paulson@6121: difficulties for automated proof. In intuitionistic logic, the assumption paulson@6121: $P\imp Q$ cannot be treated like $\neg P\disj Q$. Given $P\imp Q$, we may paulson@6121: use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated paulson@6121: use of $P\imp Q$. If the proof of~$P$ fails then the whole branch of the paulson@6121: proof must be abandoned. Thus intuitionistic propositional logic requires paulson@6121: backtracking. paulson@6121: paulson@6121: For an elementary example, consider the intuitionistic proof of $Q$ from paulson@6121: $P\imp Q$ and $(P\imp Q)\imp P$. The implication $P\imp Q$ is needed paulson@6121: twice: paulson@6121: \[ \infer[({\imp}E)]{Q}{P\imp Q & paulson@6121: \infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}} paulson@6121: \] paulson@14154: The theorem prover for intuitionistic logic does not use~\isa{impE}.\@ paulson@6121: Instead, it simplifies implications using derived rules paulson@6121: (Fig.\ts\ref{fol-int-derived}). It reduces the antecedents of implications paulson@6121: to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$. paulson@6121: The rules \tdx{conj_impE} and \tdx{disj_impE} are paulson@6121: straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and paulson@6121: $(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp paulson@14154: S$. The other \ldots\isa{\_impE} rules are unsafe; the method requires paulson@6121: backtracking. All the rules are derived in the same simple manner. paulson@6121: paulson@6121: Dyckhoff has independently discovered similar rules, and (more importantly) paulson@6121: has demonstrated their completeness for propositional paulson@6121: logic~\cite{dyckhoff}. However, the tactics given below are not complete paulson@6121: for first-order logic because they discard universally quantified paulson@14154: assumptions after a single use. These are \ML{} functions, and are listed paulson@14154: below with their \ML{} type: paulson@6121: \begin{ttbox} paulson@6121: mp_tac : int -> tactic paulson@6121: eq_mp_tac : int -> tactic paulson@6121: IntPr.safe_step_tac : int -> tactic paulson@6121: IntPr.safe_tac : tactic paulson@6121: IntPr.inst_step_tac : int -> tactic paulson@6121: IntPr.step_tac : int -> tactic paulson@6121: IntPr.fast_tac : int -> tactic paulson@6121: IntPr.best_tac : int -> tactic paulson@6121: \end{ttbox} paulson@14158: Most of these belong to the structure \ML{} structure \texttt{IntPr} and resemble the paulson@14158: tactics of Isabelle's classical reasoner. There are no corresponding paulson@14158: Isar methods, but you can use the paulson@14154: \isa{tactic} method to call \ML{} tactics in an Isar script: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (tactic\ {* IntPr.fast\_tac 1*}) paulson@14154: \end{isabelle} paulson@14154: Here is a description of each tactic: paulson@6121: paulson@6121: \begin{ttdescription} paulson@6121: \item[\ttindexbold{mp_tac} {\it i}] paulson@6121: attempts to use \tdx{notE} or \tdx{impE} within the assumptions in paulson@6121: subgoal $i$. For each assumption of the form $\neg P$ or $P\imp Q$, it paulson@6121: searches for another assumption unifiable with~$P$. By paulson@6121: contradiction with $\neg P$ it can solve the subgoal completely; by Modus paulson@6121: Ponens it can replace the assumption $P\imp Q$ by $Q$. The tactic can paulson@6121: produce multiple outcomes, enumerating all suitable pairs of assumptions. paulson@6121: paulson@6121: \item[\ttindexbold{eq_mp_tac} {\it i}] paulson@6121: is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it paulson@6121: is safe. paulson@6121: paulson@6121: \item[\ttindexbold{IntPr.safe_step_tac} $i$] performs a safe step on paulson@6121: subgoal~$i$. This may include proof by assumption or Modus Ponens (taking paulson@6121: care not to instantiate unknowns), or \texttt{hyp_subst_tac}. paulson@6121: paulson@6121: \item[\ttindexbold{IntPr.safe_tac}] repeatedly performs safe steps on all paulson@6121: subgoals. It is deterministic, with at most one outcome. paulson@6121: paulson@6121: \item[\ttindexbold{IntPr.inst_step_tac} $i$] is like \texttt{safe_step_tac}, paulson@6121: but allows unknowns to be instantiated. paulson@6121: paulson@6121: \item[\ttindexbold{IntPr.step_tac} $i$] tries \texttt{safe_tac} or {\tt paulson@6121: inst_step_tac}, or applies an unsafe rule. This is the basic step of paulson@6121: the intuitionistic proof procedure. paulson@6121: paulson@6121: \item[\ttindexbold{IntPr.fast_tac} $i$] applies \texttt{step_tac}, using paulson@6121: depth-first search, to solve subgoal~$i$. paulson@6121: paulson@6121: \item[\ttindexbold{IntPr.best_tac} $i$] applies \texttt{step_tac}, using paulson@6121: best-first search (guided by the size of the proof state) to solve subgoal~$i$. paulson@6121: \end{ttdescription} paulson@6121: Here are some of the theorems that \texttt{IntPr.fast_tac} proves paulson@6121: automatically. The latter three date from {\it Principia Mathematica} paulson@6121: (*11.53, *11.55, *11.61)~\cite{principia}. paulson@6121: \begin{ttbox} paulson@6121: ~~P & ~~(P --> Q) --> ~~Q paulson@6121: (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y))) paulson@6121: (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y))) paulson@6121: (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y))) paulson@6121: \end{ttbox} paulson@6121: paulson@6121: paulson@6121: paulson@6121: \begin{figure} paulson@6121: \begin{ttbox} paulson@6121: \tdx{excluded_middle} ~P | P paulson@6121: paulson@6121: \tdx{disjCI} (~Q ==> P) ==> P|Q paulson@6121: \tdx{exCI} (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x) paulson@6121: \tdx{impCE} [| P-->Q; ~P ==> R; Q ==> R |] ==> R paulson@6121: \tdx{iffCE} [| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R paulson@6121: \tdx{notnotD} ~~P ==> P paulson@6121: \tdx{swap} ~P ==> (~Q ==> P) ==> Q paulson@6121: \end{ttbox} paulson@6121: \caption{Derived rules for classical logic} \label{fol-cla-derived} paulson@6121: \end{figure} paulson@6121: paulson@6121: paulson@6121: \section{Classical proof procedures} \label{fol-cla-prover} paulson@6121: The classical theory, \thydx{FOL}, consists of intuitionistic logic plus paulson@6121: the rule paulson@6121: $$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$ paulson@6121: \noindent wenzelm@9695: Natural deduction in classical logic is not really all that natural. FOL wenzelm@9695: derives classical introduction rules for $\disj$ and~$\exists$, as well as wenzelm@9695: classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see wenzelm@9695: Fig.\ts\ref{fol-cla-derived}). paulson@6121: paulson@14154: The classical reasoner is installed. The most useful methods are paulson@14154: \isa{blast} (pure classical reasoning) and \isa{auto} (classical reasoning paulson@14154: combined with simplification), but the full range of paulson@14154: methods is available, including \isa{clarify}, paulson@14154: \isa{fast}, \isa{best} and \isa{force}. paulson@14154: See the paulson@6121: \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% paulson@6121: {Chap.\ts\ref{chap:classical}} paulson@14154: and the \emph{Tutorial}~\cite{isa-tutorial} paulson@6121: for more discussion of classical proof methods. paulson@6121: paulson@6121: paulson@6121: \section{An intuitionistic example} paulson@14158: Here is a session similar to one in the book {\em Logic and Computation} paulson@14158: \cite[pages~222--3]{paulson87}. It illustrates the treatment of paulson@14158: quantifier reasoning, which is different in Isabelle than it is in paulson@14158: {\sc lcf}-based theorem provers such as {\sc hol}. paulson@6121: paulson@14158: The theory header specifies that we are working in intuitionistic paulson@14158: logic by designating \isa{IFOL} rather than \isa{FOL} as the parent paulson@14158: theory: paulson@14154: \begin{isabelle} paulson@30036: \isacommand{theory}\ IFOL\_examples\ \isacommand{imports}\ IFOL\isanewline paulson@30036: \isacommand{begin} paulson@14154: \end{isabelle} paulson@6121: The proof begins by entering the goal, then applying the rule $({\imp}I)$. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline paulson@14154: \ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\ paulson@14154: \isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y)) paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ (rule\ impI)\isanewline paulson@14154: \ 1.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\ paulson@14154: \isasymLongrightarrow \ \isasymforall x.\ \isasymexists y.\ Q(x,\ y) paulson@14154: \end{isabelle} paulson@14154: Isabelle's output is shown as it would appear using Proof General. paulson@6121: In this example, we shall never have more than one subgoal. Applying paulson@14154: $({\imp}I)$ replaces~\isa{\isasymlongrightarrow} paulson@14154: by~\isa{\isasymLongrightarrow}, so that paulson@14154: \(\ex{y}\all{x}Q(x,y)\) becomes an assumption. We have the choice of paulson@6121: $({\exists}E)$ and $({\forall}I)$; let us try the latter. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ allI)\isanewline paulson@14154: \ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\ paulson@14154: \isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)\hfill\((*)\) paulson@14154: \end{isabelle} paulson@14154: Applying $({\forall}I)$ replaces the \isa{\isasymforall paulson@14154: x} (in ASCII, \isa{ALL~x}) by \isa{\isasymAnd x} paulson@14154: (or \isa{!!x}), replacing FOL's universal quantifier by Isabelle's paulson@14154: meta universal quantifier. The bound variable is a {\bf parameter} of paulson@14154: the subgoal. We now must choose between $({\exists}I)$ and paulson@14154: $({\exists}E)$. What happens if the wrong rule is chosen? paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ exI)\isanewline paulson@14154: \ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\ paulson@14154: \isasymLongrightarrow \ Q(x,\ ?y2(x)) paulson@14154: \end{isabelle} paulson@14154: The new subgoal~1 contains the function variable \isa{?y2}. Instantiating paulson@14154: \isa{?y2} can replace~\isa{?y2(x)} by a term containing~\isa{x}, even paulson@14154: though~\isa{x} is a bound variable. Now we analyse the assumption paulson@6121: \(\exists y.\forall x. Q(x,y)\) using elimination rules: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (erule\ exE)\isanewline paulson@14154: \ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\ \isasymLongrightarrow \ Q(x,\ ?y2(x)) paulson@14154: \end{isabelle} paulson@14154: Applying $(\exists E)$ has produced the parameter \isa{y} and stripped the paulson@6121: existential quantifier from the assumption. But the subgoal is unprovable: paulson@14154: there is no way to unify \isa{?y2(x)} with the bound variable~\isa{y}. paulson@14154: Using Proof General, we can return to the critical point, marked paulson@14154: $(*)$ above. This time we apply $({\exists}E)$: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (erule\ exE)\isanewline paulson@14154: \ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\ paulson@14154: \isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y) paulson@14154: \end{isabelle} paulson@6121: We now have two parameters and no scheme variables. Applying paulson@6121: $({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are paulson@6121: applied to those parameters. Parameters should be produced early, as this paulson@6121: example demonstrates. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ exI)\isanewline paulson@14154: \ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\ paulson@14154: \isasymLongrightarrow \ Q(x,\ ?y3(x,\ y)) paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ (erule\ allE)\isanewline paulson@14154: \ 1.\ \isasymAnd x\ y.\ Q(?x4(x,\ y),\ y)\ \isasymLongrightarrow \ paulson@14154: Q(x,\ ?y3(x,\ y)) paulson@14154: \end{isabelle} paulson@14154: The subgoal has variables \isa{?y3} and \isa{?x4} applied to both paulson@14154: parameters. The obvious projection functions unify \isa{?x4(x,y)} with~\isa{ paulson@14154: x} and \isa{?y3(x,y)} with~\isa{y}. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ assumption\isanewline paulson@14154: No\ subgoals!\isanewline paulson@14154: \isacommand{done} paulson@14154: \end{isabelle} paulson@14154: The theorem was proved in six method invocations, not counting the paulson@14154: abandoned ones. But proof checking is tedious, and the \ML{} tactic paulson@14154: \ttindex{IntPr.fast_tac} can prove the theorem in one step. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline paulson@14154: \ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\ paulson@14154: \isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y)) paulson@14154: \isanewline paulson@30036: \isacommand{by} (tactic \ttlbrace*IntPr.fast_tac 1*\ttrbrace)\isanewline paulson@14154: No\ subgoals! paulson@14154: \end{isabelle} paulson@6121: paulson@6121: paulson@6121: \section{An example of intuitionistic negation} paulson@6121: The following example demonstrates the specialized forms of implication paulson@6121: elimination. Even propositional formulae can be difficult to prove from paulson@6121: the basic rules; the specialized rules help considerably. paulson@6121: paulson@6121: Propositional examples are easy to invent. As Dummett notes~\cite[page paulson@6121: 28]{dummett}, $\neg P$ is classically provable if and only if it is paulson@6121: intuitionistically provable; therefore, $P$ is classically provable if and paulson@6121: only if $\neg\neg P$ is intuitionistically provable.% paulson@14154: \footnote{This remark holds only for propositional logic, not if $P$ is paulson@14154: allowed to contain quantifiers.} paulson@14154: % paulson@14154: Proving $\neg\neg P$ intuitionistically is paulson@6121: much harder than proving~$P$ classically. paulson@6121: paulson@6121: Our example is the double negation of the classical tautology $(P\imp paulson@14154: Q)\disj (Q\imp P)$. The first step is apply the paulson@14154: \isa{unfold} method, which expands paulson@14154: negations to implications using the definition $\neg P\equiv P\imp\bot$ paulson@14154: and allows use of the special implication rules. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "\isachartilde \ \isachartilde \ ((P-->Q)\ |\ (Q-->P))"\isanewline paulson@14154: \ 1.\ \isasymnot \ \isasymnot \ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)) paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ (unfold\ not\_def)\isanewline paulson@14154: \ 1.\ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False)\ \isasymlongrightarrow \ False% paulson@14154: \end{isabelle} paulson@14154: The next step is a trivial use of $(\imp I)$. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ impI)\isanewline paulson@14154: \ 1.\ (P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\ \isasymLongrightarrow \ False% paulson@14154: \end{isabelle} paulson@6121: By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but paulson@14154: that formula is not a theorem of intuitionistic logic. Instead, we paulson@14154: apply the specialized implication rule \tdx{disj_impE}. It splits the paulson@6121: assumption into two assumptions, one for each disjunct. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (erule\ disj\_impE)\isanewline paulson@14154: \ 1.\ \isasymlbrakk (P\ \isasymlongrightarrow \ Q)\ \isasymlongrightarrow \ False;\ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ paulson@14154: False paulson@14154: \end{isabelle} paulson@6121: We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but paulson@6121: their negations are inconsistent. Applying \tdx{imp_impE} breaks down paulson@6121: the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new paulson@6121: assumptions~$P$ and~$\neg Q$. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (erule\ imp\_impE)\isanewline paulson@14154: \ 1.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ P;\ Q\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline paulson@14154: \ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ paulson@14154: False paulson@14154: \end{isabelle} paulson@6121: Subgoal~2 holds trivially; let us ignore it and continue working on paulson@6121: subgoal~1. Thanks to the assumption~$P$, we could prove $Q\imp P$; paulson@6121: applying \tdx{imp_impE} is simpler. paulson@14154: \begin{isabelle} paulson@14154: \ \isacommand{apply}\ (erule\ imp\_impE)\isanewline paulson@14154: \ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ Q;\ P\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ P\isanewline paulson@14154: \ 2.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline paulson@14154: \ 3.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ False% paulson@14154: \end{isabelle} paulson@6121: The three subgoals are all trivial. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ assumption\ \isanewline paulson@14154: \ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ paulson@14154: False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline paulson@14154: \ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ paulson@14154: \isasymlongrightarrow \ False;\ False\isasymrbrakk \ paulson@14154: \isasymLongrightarrow \ False% paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ (erule\ FalseE)+\isanewline paulson@14154: No\ subgoals!\isanewline paulson@14154: \isacommand{done} paulson@14154: \end{isabelle} paulson@14154: This proof is also trivial for the \ML{} tactic \isa{IntPr.fast_tac}. paulson@6121: paulson@6121: paulson@6121: \section{A classical example} \label{fol-cla-example} paulson@6121: To illustrate classical logic, we shall prove the theorem paulson@6121: $\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as paulson@6121: follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise paulson@14154: $\all{x}P(x)$ is true. Either way the theorem holds. First, we must paulson@14158: work in a theory based on classical logic, the theory \isa{FOL}: paulson@14154: \begin{isabelle} paulson@30036: \isacommand{theory}\ FOL\_examples\ \isacommand{imports}\ FOL\isanewline paulson@30036: \isacommand{begin} paulson@14154: \end{isabelle} paulson@6121: paulson@6121: The formal proof does not conform in any obvious way to the sketch given paulson@14154: above. Its key step is its first rule, \tdx{exCI}, a classical paulson@14154: version of~$(\exists I)$ that allows multiple instantiation of the paulson@14154: quantifier. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline paulson@14154: \ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x) paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ (rule\ exCI)\isanewline paulson@14154: \ 1.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ \isasymforall x.\ P(?a)\ \isasymlongrightarrow \ P(x) paulson@14154: \end{isabelle} paulson@14154: We can either exhibit a term \isa{?a} to satisfy the conclusion of paulson@6121: subgoal~1, or produce a contradiction from the assumption. The next paulson@6121: steps are routine. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ allI)\isanewline paulson@14154: \ 1.\ \isasymAnd x.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ P(?a)\ \isasymlongrightarrow \ P(x) paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ (rule\ impI)\isanewline paulson@14154: \ 1.\ \isasymAnd x.\ \isasymlbrakk \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x));\ P(?a)\isasymrbrakk \ \isasymLongrightarrow \ P(x) paulson@14154: \end{isabelle} paulson@6121: By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$ paulson@14154: is equivalent to applying~$(\exists I)$ again. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (erule\ allE)\isanewline paulson@14154: \ 1.\ \isasymAnd x.\ \isasymlbrakk P(?a);\ \isasymnot \ (\isasymforall xa.\ P(?y3(x))\ \isasymlongrightarrow \ P(xa))\isasymrbrakk \ \isasymLongrightarrow \ P(x) paulson@14154: \end{isabelle} paulson@6121: In classical logic, a negated assumption is equivalent to a conclusion. To paulson@8249: get this effect, we create a swapped version of $(\forall I)$ and apply it paulson@14154: using \ttindex{erule}. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (erule\ allI\ [THEN\ [2]\ swap])\isanewline paulson@14154: \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x)\isasymrbrakk \ \isasymLongrightarrow \ P(?y3(x))\ \isasymlongrightarrow \ P(xa) paulson@14154: \end{isabelle} paulson@14154: The operand of \isa{erule} above denotes the following theorem: paulson@14154: \begin{isabelle} paulson@14154: \ \ \ \ \isasymlbrakk \isasymnot \ (\isasymforall x.\ ?P1(x));\ paulson@14154: \isasymAnd x.\ \isasymnot \ ?P\ \isasymLongrightarrow \ paulson@14154: ?P1(x)\isasymrbrakk \ paulson@14154: \isasymLongrightarrow \ ?P% paulson@14154: \end{isabelle} paulson@14154: The previous conclusion, \isa{P(x)}, has become a negated assumption. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ impI)\isanewline paulson@14154: \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(xa) paulson@14154: \end{isabelle} paulson@6121: The subgoal has three assumptions. We produce a contradiction between the paulson@14154: \index{assumptions!contradictory} assumptions~\isa{\isasymnot P(x)} paulson@14154: and~\isa{P(?y3(x))}. The proof never instantiates the paulson@14154: unknown~\isa{?a}. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (erule\ notE)\isanewline paulson@14154: \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(x) paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ assumption\isanewline paulson@14154: No\ subgoals!\isanewline paulson@14154: \isacommand{done} paulson@14154: \end{isabelle} paulson@14154: The civilised way to prove this theorem is using the paulson@14154: \methdx{blast} method, which automatically uses the classical form paulson@14154: of the rule~$(\exists I)$: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline paulson@14154: \ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x) paulson@14154: \isanewline paulson@14154: \isacommand{by}\ blast\isanewline paulson@14154: No\ subgoals! paulson@14154: \end{isabelle} paulson@6121: If this theorem seems counterintuitive, then perhaps you are an paulson@6121: intuitionist. In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$ paulson@6121: requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$, paulson@6121: which we cannot do without further knowledge about~$P$. paulson@6121: paulson@6121: paulson@6121: \section{Derived rules and the classical tactics} paulson@6121: Classical first-order logic can be extended with the propositional paulson@6121: connective $if(P,Q,R)$, where paulson@6121: $$ if(P,Q,R) \equiv P\conj Q \disj \neg P \conj R. \eqno(if) $$ paulson@6121: Theorems about $if$ can be proved by treating this as an abbreviation, paulson@6121: replacing $if(P,Q,R)$ by $P\conj Q \disj \neg P \conj R$ in subgoals. But paulson@6121: this duplicates~$P$, causing an exponential blowup and an unreadable paulson@6121: formula. Introducing further abbreviations makes the problem worse. paulson@6121: paulson@6121: Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$ paulson@6121: directly, without reference to its definition. The simple identity paulson@6121: \[ if(P,Q,R) \,\bimp\, (P\imp Q)\conj (\neg P\imp R) \] paulson@6121: suggests that the paulson@6121: $if$-introduction rule should be paulson@6121: \[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]} & \infer*{R}{[\neg P]}} \] paulson@6121: The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the paulson@6121: elimination rules for~$\disj$ and~$\conj$. paulson@6121: \[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]} paulson@6121: & \infer*{S}{[\neg P,R]}} paulson@6121: \] paulson@6121: Having made these plans, we get down to work with Isabelle. The theory of paulson@6121: classical logic, \texttt{FOL}, is extended with the constant paulson@6121: $if::[o,o,o]\To o$. The axiom \tdx{if_def} asserts the paulson@6121: equation~$(if)$. paulson@14154: \begin{isabelle} paulson@30036: \isacommand{theory}\ If\ \isacommand{imports}\ FOL\isanewline paulson@30036: \isacommand{begin}\isanewline paulson@14154: \isacommand{constdefs}\isanewline paulson@14154: \ \ if\ ::\ "[o,o,o]=>o"\isanewline paulson@14154: \ \ \ "if(P,Q,R)\ ==\ P\&Q\ |\ \isachartilde P\&R" paulson@14154: \end{isabelle} paulson@6121: We create the file \texttt{If.thy} containing these declarations. (This file paulson@6121: is on directory \texttt{FOL/ex} in the Isabelle distribution.) Typing paulson@14154: \begin{isabelle} paulson@6121: use_thy "If"; paulson@14154: \end{isabelle} paulson@6121: loads that theory and sets it to be the current context. paulson@6121: paulson@6121: paulson@6121: \subsection{Deriving the introduction rule} paulson@6121: paulson@6121: The derivations of the introduction and elimination rules demonstrate the paulson@6121: methods for rewriting with definitions. Classical reasoning is required, paulson@14154: so we use \isa{blast}. paulson@6121: paulson@6121: The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$, paulson@14154: concludes $if(P,Q,R)$. We propose this lemma and immediately simplify paulson@14154: using \isa{if\_def} to expand the definition of \isa{if} in the paulson@14154: subgoal. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ ifI: "[|\ P\ ==>\ Q;\ \isachartilde P\ ==>\ R\ paulson@14154: |]\ ==>\ if(P,Q,R)"\isanewline paulson@14154: \ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ Q,\ R) paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline paulson@14154: \ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ paulson@14154: R paulson@14154: \end{isabelle} paulson@14154: The rule's premises, although expressed using meta-level implication paulson@14154: (\isa{\isasymLongrightarrow}) are passed as ordinary implications to paulson@14154: \methdx{blast}. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ blast\isanewline paulson@14154: No\ subgoals!\isanewline paulson@14154: \isacommand{done} paulson@14154: \end{isabelle} paulson@6121: paulson@6121: paulson@6121: \subsection{Deriving the elimination rule} paulson@6121: The elimination rule has three premises, two of which are themselves rules. paulson@6121: The conclusion is simply $S$. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ ifE:\isanewline paulson@14154: \ \ \ "[|\ if(P,Q,R);\ \ [|P;\ Q|]\ ==>\ S;\ [|\isachartilde P;\ R|]\ ==>\ S\ |]\ ==>\ S"\isanewline paulson@14154: \ 1.\ \isasymlbrakk if(P,\ Q,\ R);\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S% paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline paulson@14154: \ 1.\ \isasymlbrakk P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R;\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S% paulson@14154: \end{isabelle} paulson@14154: The proof script is the same as before: \isa{simp} followed by paulson@14154: \isa{blast}: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ blast\isanewline paulson@14154: No\ subgoals!\isanewline paulson@14154: \isacommand{done} paulson@14154: \end{isabelle} paulson@6121: paulson@6121: paulson@6121: \subsection{Using the derived rules} paulson@14154: Our new derived rules, \tdx{ifI} and~\tdx{ifE}, permit natural paulson@14154: proofs of theorems such as the following: paulson@6121: \begin{eqnarray*} paulson@6121: if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\ paulson@6121: if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B)) paulson@6121: \end{eqnarray*} paulson@6121: Proofs also require the classical reasoning rules and the $\bimp$ paulson@14154: introduction rule (called~\tdx{iffI}: do not confuse with~\isa{ifI}). paulson@6121: paulson@6121: To display the $if$-rules in action, let us analyse a proof step by step. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ if\_commute:\isanewline paulson@14154: \ \ \ \ \ "if(P,\ if(Q,A,B),\ paulson@14154: if(Q,C,D))\ <->\ if(Q,\ if(P,A,C),\ if(P,B,D))"\isanewline paulson@14154: \isacommand{apply}\ (rule\ iffI)\isanewline paulson@14154: \ 1.\ if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))\ \isasymLongrightarrow \isanewline paulson@14154: \isaindent{\ 1.\ }if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline paulson@14154: \ 2.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline paulson@14154: \isaindent{\ 2.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) paulson@14154: \end{isabelle} paulson@6121: The $if$-elimination rule can be applied twice in succession. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (erule\ ifE)\isanewline paulson@14154: \ 1.\ \isasymlbrakk P;\ if(Q,\ A,\ B)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline paulson@14154: \ 2.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline paulson@14154: \ 3.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline paulson@14154: \isaindent{\ 3.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ (erule\ ifE)\isanewline paulson@14154: \ 1.\ \isasymlbrakk P;\ Q;\ A\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline paulson@14154: \ 2.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline paulson@14154: \ 3.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline paulson@14154: \ 4.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline paulson@14154: \isaindent{\ 4.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) paulson@14154: \end{isabelle} paulson@6121: % paulson@6121: In the first two subgoals, all assumptions have been reduced to atoms. Now paulson@6121: $if$-introduction can be applied. Observe how the $if$-rules break down paulson@6121: occurrences of $if$ when they become the outermost connective. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (rule\ ifI)\isanewline paulson@14154: \ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ A,\ C)\isanewline paulson@14154: \ 2.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline paulson@14154: \ 3.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline paulson@14154: \ 4.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline paulson@14154: \ 5.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline paulson@14154: \isaindent{\ 5.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ (rule\ ifI)\isanewline paulson@14154: \ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline paulson@14154: \ 2.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \ C\isanewline paulson@14154: \ 3.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline paulson@14154: \ 4.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline paulson@14154: \ 5.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline paulson@14154: \ 6.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline paulson@14154: \isaindent{\ 6.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) paulson@14154: \end{isabelle} paulson@6121: Where do we stand? The first subgoal holds by assumption; the second and paulson@6121: third, by contradiction. This is getting tedious. We could use the classical paulson@6121: reasoner, but first let us extend the default claset with the derived rules paulson@6121: for~$if$. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{declare}\ ifI\ [intro!]\isanewline paulson@14154: \isacommand{declare}\ ifE\ [elim!] paulson@14154: \end{isabelle} paulson@14154: With these declarations, we could have proved this theorem with a single paulson@14154: call to \isa{blast}. Here is another example: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline paulson@14154: \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B)) paulson@14154: \isanewline paulson@14154: \isacommand{by}\ blast paulson@14154: \end{isabelle} paulson@6121: paulson@6121: paulson@6121: \subsection{Derived rules versus definitions} paulson@6121: Dispensing with the derived rules, we can treat $if$ as an paulson@6121: abbreviation, and let \ttindex{blast_tac} prove the expanded formula. Let paulson@6121: us redo the previous proof: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline paulson@14154: \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B)) paulson@14154: \end{isabelle} paulson@14154: This time, we simply unfold using the definition of $if$: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline paulson@14154: \ 1.\ (P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R)\ \isasymand \ A\ \isasymor \ (\isasymnot \ P\ \isasymor \ \isasymnot \ Q)\ \isasymand \ (P\ \isasymor \ \isasymnot \ R)\ \isasymand \ B\ \isasymlongleftrightarrow \isanewline paulson@14154: \isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ A\ \isasymor \ \isasymnot \ R\ \isasymand \ B) paulson@14154: \end{isabelle} paulson@14154: We are left with a subgoal in pure first-order logic, and it falls to paulson@14154: \isa{blast}: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ blast\isanewline paulson@14154: No\ subgoals! paulson@14154: \end{isabelle} paulson@6121: Expanding definitions reduces the extended logic to the base logic. This paulson@14154: approach has its merits, but it can be slow. In these examples, proofs paulson@14154: using the derived rules for~\isa{if} run about six paulson@14154: times faster than proofs using just the rules of first-order logic. paulson@6121: paulson@14154: Expanding definitions can also make it harder to diagnose errors. paulson@14154: Suppose we are having difficulties in proving some goal. If by expanding paulson@14154: definitions we have made it unreadable, then we have little hope of paulson@14154: diagnosing the problem. paulson@6121: paulson@6121: Attempts at program verification often yield invalid assertions. paulson@6121: Let us try to prove one: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline paulson@14154: \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\ paulson@14154: A)) paulson@14154: \end{isabelle} paulson@14154: Calling \isa{blast} yields an uninformative failure message. We can paulson@14154: get a closer look at the situation by applying \methdx{auto}. paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ auto\isanewline paulson@14154: \ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline paulson@14154: \ 2.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline paulson@14154: \ 3.\ \isasymlbrakk B;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline paulson@14154: \ 4.\ \isasymlbrakk \isasymnot \ R;\ A;\ \isasymnot \ B;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \ paulson@14154: False paulson@14154: \end{isabelle} paulson@6121: Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false paulson@6121: while~$R$ and~$A$ are true. This truth assignment reduces the main goal to paulson@6121: $true\bimp false$, which is of course invalid. paulson@6121: wenzelm@9695: We can repeat this analysis by expanding definitions, using just the rules of paulson@14154: first-order logic: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline paulson@14154: \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\ paulson@14154: A)) paulson@14154: \isanewline paulson@14154: \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline paulson@14154: \ 1.\ (P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R)\ \isasymand \ A\ \isasymor \ (\isasymnot \ P\ \isasymor \ \isasymnot \ Q)\ \isasymand \ (P\ \isasymor \ \isasymnot \ R)\ \isasymand \ B\ \isasymlongleftrightarrow \isanewline paulson@14154: \isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ B\ \isasymor \ \isasymnot \ R\ \isasymand \ A) paulson@14154: \end{isabelle} paulson@14154: Again \isa{blast} would fail, so we try \methdx{auto}: paulson@14154: \begin{isabelle} paulson@14154: \isacommand{apply}\ (auto)\ \isanewline paulson@14154: \ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline paulson@14154: \ 2.\ \isasymlbrakk A;\ \isasymnot \ P;\ R;\ \isasymnot \ B\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline paulson@14154: \ 3.\ \isasymlbrakk B;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline paulson@14154: \ 4.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ A;\ \isasymnot \ R;\ Q\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline paulson@14154: \ 5.\ \isasymlbrakk B;\ \isasymnot \ Q;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline paulson@14154: \ 6.\ \isasymlbrakk B;\ \isasymnot \ A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline paulson@14154: \ 7.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline paulson@14154: \ 8.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ Q% paulson@14154: \end{isabelle} paulson@6121: Subgoal~1 yields the same countermodel as before. But each proof step has paulson@6121: taken six times as long, and the final result contains twice as many subgoals. paulson@6121: paulson@14154: Expanding your definitions usually makes proofs more difficult. This is paulson@14154: why the classical prover has been designed to accept derived rules. paulson@6121: paulson@6121: \index{first-order logic|)}