src/Doc/Intro/document/foundations.tex
 author haftmann Sun Oct 08 22:28:22 2017 +0200 (23 months ago) changeset 66816 212a3334e7da parent 48985 5386df44a037 permissions -rw-r--r--
more fundamental definition of div and mod on int
 lcp@105  1 \part{Foundations}  lcp@296  2 The following sections discuss Isabelle's logical foundations in detail:  lcp@105  3 representing logical syntax in the typed $\lambda$-calculus; expressing  lcp@105  4 inference rules in Isabelle's meta-logic; combining rules by resolution.  lcp@296  5 lcp@296  6 If you wish to use Isabelle immediately, please turn to  lcp@296  7 page~\pageref{chap:getting}. You can always read about foundations later,  lcp@296  8 either by returning to this point or by looking up particular items in the  lcp@296  9 index.  lcp@105  10 lcp@105  11 \begin{figure}  lcp@105  12 \begin{eqnarray*}  lcp@105  13  \neg P & \hbox{abbreviates} & P\imp\bot \\  lcp@105  14  P\bimp Q & \hbox{abbreviates} & (P\imp Q) \conj (Q\imp P)  lcp@105  15 \end{eqnarray*}  lcp@105  16 \vskip 4ex  lcp@105  17 lcp@105  18 $$\begin{array}{c@{\qquad\qquad}c}  lcp@105  19  \infer[({\conj}I)]{P\conj Q}{P & Q} &  lcp@105  20  \infer[({\conj}E1)]{P}{P\conj Q} \qquad  lcp@105  21  \infer[({\conj}E2)]{Q}{P\conj Q} \$4ex]  lcp@105  22 lcp@105  23  \infer[({\disj}I1)]{P\disj Q}{P} \qquad  lcp@105  24  \infer[({\disj}I2)]{P\disj Q}{Q} &  lcp@105  25  \infer[({\disj}E)]{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}}\\[4ex]  lcp@105  26 lcp@105  27  \infer[({\imp}I)]{P\imp Q}{\infer*{Q}{[P]}} &  lcp@105  28  \infer[({\imp}E)]{Q}{P\imp Q & P} \\[4ex]  lcp@105  29 lcp@105  30  &  lcp@105  31  \infer[({\bot}E)]{P}{\bot}\\[4ex]  lcp@105  32 lcp@105  33  \infer[({\forall}I)*]{\forall x.P}{P} &  lcp@105  34  \infer[({\forall}E)]{P[t/x]}{\forall x.P} \\[3ex]  lcp@105  35 lcp@105  36  \infer[({\exists}I)]{\exists x.P}{P[t/x]} &  lcp@105  37  \infer[({\exists}E)*]{Q}{{\exists x.P} & \infer*{Q}{[P]} } \\[3ex]  lcp@105  38 lcp@105  39  {t=t} \,(refl) & \vcenter{\infer[(subst)]{P[u/x]}{t=u & P[t/x]}}  lcp@105  40 \end{array}$$  lcp@105  41 lcp@105  42 \bigskip\bigskip  lcp@105  43 *{\em Eigenvariable conditions\/}:  lcp@105  44 lcp@105  45 \forall I: provided x is not free in the assumptions  lcp@105  46 lcp@105  47 \exists E: provided x is not free in Q or any assumption except P  lcp@105  48 \caption{Intuitionistic first-order logic} \label{fol-fig}  lcp@105  49 \end{figure}  lcp@105  50 lcp@296  51 \section{Formalizing logical syntax in Isabelle}\label{sec:logical-syntax}  lcp@331  52 \index{first-order logic}  lcp@331  53 lcp@105  54 Figure~\ref{fol-fig} presents intuitionistic first-order logic,  lcp@296  55 including equality. Let us see how to formalize  lcp@105  56 this logic in Isabelle, illustrating the main features of Isabelle's  lcp@105  57 polymorphic meta-logic.  lcp@105  58 lcp@331  59 \index{lambda calc@\lambda-calculus}  lcp@312  60 Isabelle represents syntax using the simply typed \lambda-calculus. We  lcp@312  61 declare a type for each syntactic category of the logic. We declare a  lcp@312  62 constant for each symbol of the logic, giving each n-place operation an  lcp@312  63 n-argument curried function type. Most importantly,  lcp@312  64 \lambda-abstraction represents variable binding in quantifiers.  lcp@105  65 lcp@331  66 \index{types!syntax of}\index{types!function}\index{*fun type}  lcp@331  67 \index{type constructors}  lcp@331  68 Isabelle has \ML-style polymorphic types such as~(\alpha)list, where  lcp@331  69 list is a type constructor and \alpha is a type variable; for example,  lcp@105  70 (bool)list is the type of lists of booleans. Function types have the  lcp@312  71 form (\sigma,\tau)fun or \sigma\To\tau, where \sigma and \tau are  lcp@312  72 types. Curried function types may be abbreviated:  lcp@105  73 \[ \sigma@1\To (\cdots \sigma@n\To \tau\cdots) \quad \hbox{as} \quad  wenzelm@3103  74 [\sigma@1, \ldots, \sigma@n] \To \tau$  lcp@105  75   wenzelm@3103  76 \index{terms!syntax of} The syntax for terms is summarised below.  wenzelm@3103  77 Note that there are two versions of function application syntax  wenzelm@3103  78 available in Isabelle: either $t\,u$, which is the usual form for  wenzelm@3103  79 higher-order languages, or $t(u)$, trying to look more like  paulson@3485  80 first-order. The latter syntax is used throughout the manual.  lcp@105  81 $ lcp@312  82 \index{lambda abs@\lambda-abstractions}\index{function applications}  lcp@105  83 \begin{array}{ll}  lcp@296  84  t :: \tau & \hbox{type constraint, on a term or bound variable} \\  lcp@105  85  \lambda x.t & \hbox{abstraction} \\  lcp@105  86  \lambda x@1\ldots x@n.t  lcp@105  87  & \hbox{curried abstraction, \lambda x@1. \ldots \lambda x@n.t} \\  lcp@105  88  t(u) & \hbox{application} \\  lcp@105  89  t (u@1, \ldots, u@n) & \hbox{curried application, t(u@1)\ldots(u@n)}  lcp@105  90 \end{array}  lcp@105  91 $  lcp@105  92 lcp@105  93 lcp@296  94 \subsection{Simple types and constants}\index{types!simple|bold}  lcp@296  95 lcp@296  96 The syntactic categories of our logic (Fig.\ts\ref{fol-fig}) are {\bf  lcp@296  97  formulae} and {\bf terms}. Formulae denote truth values, so (following  lcp@296  98 tradition) let us call their type~$o$. To allow~0 and~$Suc(t)$ as terms,  lcp@296  99 let us declare a type~$nat$ of natural numbers. Later, we shall see  lcp@296  100 how to admit terms of other types.  lcp@105  101 lcp@312  102 \index{constants}\index{*nat type}\index{*o type}  lcp@105  103 After declaring the types~$o$ and~$nat$, we may declare constants for the  lcp@105  104 symbols of our logic. Since $\bot$ denotes a truth value (falsity) and 0  lcp@105  105 denotes a number, we put \begin{eqnarray*}  lcp@105  106  \bot & :: & o \\  lcp@105  107  0 & :: & nat.  lcp@105  108 \end{eqnarray*}  lcp@105  109 If a symbol requires operands, the corresponding constant must have a  lcp@105  110 function type. In our logic, the successor function  lcp@105  111 ($Suc$) is from natural numbers to natural numbers, negation ($\neg$) is a  lcp@105  112 function from truth values to truth values, and the binary connectives are  lcp@105  113 curried functions taking two truth values as arguments:  lcp@105  114 \begin{eqnarray*}  lcp@105  115  Suc & :: & nat\To nat \\  lcp@105  116  {\neg} & :: & o\To o \\  lcp@105  117  \conj,\disj,\imp,\bimp & :: & [o,o]\To o  lcp@105  118 \end{eqnarray*}  lcp@296  119 The binary connectives can be declared as infixes, with appropriate  lcp@296  120 precedences, so that we write $P\conj Q\disj R$ instead of  lcp@296  121 $\disj(\conj(P,Q), R)$.  lcp@105  122 lcp@331  123 Section~\ref{sec:defining-theories} below describes the syntax of Isabelle  lcp@331  124 theory files and illustrates it by extending our logic with mathematical  lcp@331  125 induction.  lcp@105  126 lcp@105  127 lcp@105  128 \subsection{Polymorphic types and constants} \label{polymorphic}  lcp@105  129 \index{types!polymorphic|bold}  lcp@296  130 \index{equality!polymorphic}  lcp@312  131 \index{constants!polymorphic}  lcp@296  132 lcp@105  133 Which type should we assign to the equality symbol? If we tried  lcp@105  134 $[nat,nat]\To o$, then equality would be restricted to the natural  lcp@312  135 numbers; we should have to declare different equality symbols for each  lcp@105  136 type. Isabelle's type system is polymorphic, so we could declare  lcp@105  137 \begin{eqnarray*}  lcp@296  138  {=} & :: & [\alpha,\alpha]\To o,  lcp@105  139 \end{eqnarray*}  lcp@296  140 where the type variable~$\alpha$ ranges over all types.  lcp@105  141 But this is also wrong. The declaration is too polymorphic; $\alpha$  lcp@296  142 includes types like~$o$ and $nat\To nat$. Thus, it admits  lcp@105  143 $\bot=\neg(\bot)$ and $Suc=Suc$ as formulae, which is acceptable in  lcp@105  144 higher-order logic but not in first-order logic.  lcp@105  145 lcp@296  146 Isabelle's {\bf type classes}\index{classes} control  lcp@296  147 polymorphism~\cite{nipkow-prehofer}. Each type variable belongs to a  lcp@296  148 class, which denotes a set of types. Classes are partially ordered by the  lcp@296  149 subclass relation, which is essentially the subset relation on the sets of  lcp@296  150 types. They closely resemble the classes of the functional language  lcp@296  151 Haskell~\cite{haskell-tutorial,haskell-report}.  lcp@105  152 lcp@312  153 \index{*logic class}\index{*term class}  lcp@105  154 Isabelle provides the built-in class $logic$, which consists of the logical  lcp@105  155 types: the ones we want to reason about. Let us declare a class $term$, to  lcp@105  156 consist of all legal types of terms in our logic. The subclass structure  lcp@105  157 is now $term\le logic$.  lcp@105  158 lcp@312  159 \index{*nat type}  lcp@296  160 We put $nat$ in class $term$ by declaring $nat{::}term$. We declare the  lcp@296  161 equality constant by  lcp@105  162 \begin{eqnarray*}  lcp@105  163  {=} & :: & [\alpha{::}term,\alpha]\To o  lcp@105  164 \end{eqnarray*}  lcp@296  165 where $\alpha{::}term$ constrains the type variable~$\alpha$ to class  lcp@296  166 $term$. Such type variables resemble Standard~\ML's equality type  lcp@296  167 variables.  lcp@296  168 lcp@312  169 We give~$o$ and function types the class $logic$ rather than~$term$, since  lcp@105  170 they are not legal types for terms. We may introduce new types of class  lcp@105  171 $term$ --- for instance, type $string$ or $real$ --- at any time. We can  lcp@331  172 even declare type constructors such as~$list$, and state that type  lcp@296  173 $(\tau)list$ belongs to class~$term$ provided $\tau$ does; equality  lcp@105  174 applies to lists of natural numbers but not to lists of formulae. We may  lcp@105  175 summarize this paragraph by a set of {\bf arity declarations} for type  lcp@312  176 constructors:\index{arities!declaring}  lcp@312  177 \begin{eqnarray*}\index{*o type}\index{*fun type}  lcp@312  178  o & :: & logic \\  lcp@312  179  fun & :: & (logic,logic)logic \\  lcp@105  180  nat, string, real & :: & term \\  lcp@312  181  list & :: & (term)term  lcp@105  182 \end{eqnarray*}  lcp@312  183 (Recall that $fun$ is the type constructor for function types.)  lcp@331  184 In \rmindex{higher-order logic}, equality does apply to truth values and  lcp@296  185 functions; this requires the arity declarations ${o::term}$  lcp@312  186 and ${fun::(term,term)term}$. The class system can also handle  lcp@105  187 overloading.\index{overloading|bold} We could declare $arith$ to be the  lcp@105  188 subclass of $term$ consisting of the arithmetic' types, such as~$nat$.  lcp@105  189 Then we could declare the operators  lcp@105  190 \begin{eqnarray*}  lcp@105  191  {+},{-},{\times},{/} & :: & [\alpha{::}arith,\alpha]\To \alpha  lcp@105  192 \end{eqnarray*}  lcp@105  193 If we declare new types $real$ and $complex$ of class $arith$, then we  lcp@331  194 in effect have three sets of operators:  lcp@105  195 \begin{eqnarray*}  lcp@105  196  {+},{-},{\times},{/} & :: & [nat,nat]\To nat \\  lcp@105  197  {+},{-},{\times},{/} & :: & [real,real]\To real \\  lcp@105  198  {+},{-},{\times},{/} & :: & [complex,complex]\To complex  lcp@105  199 \end{eqnarray*}  lcp@105  200 Isabelle will regard these as distinct constants, each of which can be defined  lcp@296  201 separately. We could even introduce the type $(\alpha)vector$ and declare  lcp@296  202 its arity as $(arith)arith$. Then we could declare the constant  lcp@105  203 \begin{eqnarray*}  lcp@296  204  {+} & :: & [(\alpha)vector,(\alpha)vector]\To (\alpha)vector  lcp@105  205 \end{eqnarray*}  lcp@296  206 and specify it in terms of ${+} :: [\alpha,\alpha]\To \alpha$.  lcp@105  207 lcp@296  208 A type variable may belong to any finite number of classes. Suppose that  lcp@296  209 we had declared yet another class $ord \le term$, the class of all  lcp@105  210 ordered' types, and a constant  lcp@105  211 \begin{eqnarray*}  lcp@105  212  {\le} & :: & [\alpha{::}ord,\alpha]\To o.  lcp@105  213 \end{eqnarray*}  lcp@105  214 In this context the variable $x$ in $x \le (x+x)$ will be assigned type  lcp@296  215 $\alpha{::}\{arith,ord\}$, which means $\alpha$ belongs to both $arith$ and  lcp@296  216 $ord$. Semantically the set $\{arith,ord\}$ should be understood as the  lcp@296  217 intersection of the sets of types represented by $arith$ and $ord$. Such  lcp@296  218 intersections of classes are called \bfindex{sorts}. The empty  lcp@296  219 intersection of classes, $\{\}$, contains all types and is thus the {\bf  lcp@296  220  universal sort}.  lcp@105  221 lcp@296  222 Even with overloading, each term has a unique, most general type. For this  lcp@296  223 to be possible, the class and type declarations must satisfy certain  lcp@331  224 technical constraints; see  lcp@331  225 \iflabelundefined{sec:ref-defining-theories}%  lcp@331  226  {Sect.\ Defining Theories in the {\em Reference Manual}}%  lcp@331  227  {\S\ref{sec:ref-defining-theories}}.  lcp@105  228 lcp@296  229 lcp@105  230 \subsection{Higher types and quantifiers}  lcp@312  231 \index{types!higher|bold}\index{quantifiers}  lcp@105  232 Quantifiers are regarded as operations upon functions. Ignoring polymorphism  lcp@105  233 for the moment, consider the formula $\forall x. P(x)$, where $x$ ranges  lcp@105  234 over type~$nat$. This is true if $P(x)$ is true for all~$x$. Abstracting  lcp@105  235 $P(x)$ into a function, this is the same as saying that $\lambda x.P(x)$  lcp@105  236 returns true for all arguments. Thus, the universal quantifier can be  lcp@105  237 represented by a constant  lcp@105  238 \begin{eqnarray*}  lcp@105  239  \forall & :: & (nat\To o) \To o,  lcp@105  240 \end{eqnarray*}  lcp@105  241 which is essentially an infinitary truth table. The representation of $\forall  lcp@105  242 x. P(x)$ is $\forall(\lambda x. P(x))$.  lcp@105  243 lcp@105  244 The existential quantifier is treated  lcp@105  245 in the same way. Other binding operators are also easily handled; for  lcp@105  246 instance, the summation operator $\Sigma@{k=i}^j f(k)$ can be represented as  lcp@105  247 $\Sigma(i,j,\lambda k.f(k))$, where  lcp@105  248 \begin{eqnarray*}  lcp@105  249  \Sigma & :: & [nat,nat, nat\To nat] \To nat.  lcp@105  250 \end{eqnarray*}  lcp@105  251 Quantifiers may be polymorphic. We may define $\forall$ and~$\exists$ over  lcp@105  252 all legal types of terms, not just the natural numbers, and  lcp@105  253 allow summations over all arithmetic types:  lcp@105  254 \begin{eqnarray*}  lcp@105  255  \forall,\exists & :: & (\alpha{::}term\To o) \To o \\  lcp@105  256  \Sigma & :: & [nat,nat, nat\To \alpha{::}arith] \To \alpha  lcp@105  257 \end{eqnarray*}  lcp@105  258 Observe that the index variables still have type $nat$, while the values  lcp@105  259 being summed may belong to any arithmetic type.  lcp@105  260 lcp@105  261 lcp@105  262 \section{Formalizing logical rules in Isabelle}  lcp@312  263 \index{meta-implication|bold}  lcp@312  264 \index{meta-quantifiers|bold}  lcp@312  265 \index{meta-equality|bold}  lcp@296  266 lcp@296  267 Object-logics are formalized by extending Isabelle's  paulson@1878  268 meta-logic~\cite{paulson-found}, which is intuitionistic higher-order logic.  lcp@296  269 The meta-level connectives are {\bf implication}, the {\bf universal  lcp@296  270  quantifier}, and {\bf equality}.  lcp@105  271 \begin{itemize}  lcp@105  272  \item The implication $$\phi\Imp \psi$$ means $$\phi$$ implies  lcp@105  273 $$\psi$$', and expresses logical {\bf entailment}.  lcp@105  274 lcp@105  275  \item The quantification $$\Forall x.\phi$$ means $$\phi$$ is true for  lcp@105  276 all $x$', and expresses {\bf generality} in rules and axiom schemes.  lcp@105  277 lcp@105  278 \item The equality $$a\equiv b$$ means $a$ equals $b$', for expressing  lcp@312  279  {\bf definitions} (see~\S\ref{definitions}).\index{definitions}  lcp@312  280  Equalities left over from the unification process, so called {\bf  lcp@312  281  flex-flex constraints},\index{flex-flex constraints} are written $a\qeq  lcp@312  282  b$. The two equality symbols have the same logical meaning.  lcp@105  283 lcp@105  284 \end{itemize}  lcp@312  285 The syntax of the meta-logic is formalized in the same manner  lcp@312  286 as object-logics, using the simply typed $\lambda$-calculus. Analogous to  lcp@105  287 type~$o$ above, there is a built-in type $prop$ of meta-level truth values.  lcp@105  288 Meta-level formulae will have this type. Type $prop$ belongs to  lcp@105  289 class~$logic$; also, $\sigma\To\tau$ belongs to $logic$ provided $\sigma$  lcp@105  290 and $\tau$ do. Here are the types of the built-in connectives:  lcp@312  291 \begin{eqnarray*}\index{*prop type}\index{*logic class}  lcp@105  292  \Imp & :: & [prop,prop]\To prop \\  lcp@105  293  \Forall & :: & (\alpha{::}logic\To prop) \To prop \\  lcp@105  294  {\equiv} & :: & [\alpha{::}\{\},\alpha]\To prop \\  lcp@312  295  \qeq & :: & [\alpha{::}\{\},\alpha]\To prop  lcp@105  296 \end{eqnarray*}  lcp@312  297 The polymorphism in $\Forall$ is restricted to class~$logic$ to exclude  lcp@312  298 certain types, those used just for parsing. The type variable  lcp@312  299 $\alpha{::}\{\}$ ranges over the universal sort.  lcp@105  300 lcp@105  301 In our formalization of first-order logic, we declared a type~$o$ of  lcp@105  302 object-level truth values, rather than using~$prop$ for this purpose. If  lcp@105  303 we declared the object-level connectives to have types such as  lcp@105  304 ${\neg}::prop\To prop$, then these connectives would be applicable to  lcp@105  305 meta-level formulae. Keeping $prop$ and $o$ as separate types maintains  lcp@105  306 the distinction between the meta-level and the object-level. To formalize  lcp@105  307 the inference rules, we shall need to relate the two levels; accordingly,  lcp@105  308 we declare the constant  lcp@312  309 \index{*Trueprop constant}  lcp@105  310 \begin{eqnarray*}  lcp@105  311  Trueprop & :: & o\To prop.  lcp@105  312 \end{eqnarray*}  lcp@105  313 We may regard $Trueprop$ as a meta-level predicate, reading $Trueprop(P)$ as  lcp@105  314 $P$ is true at the object-level.' Put another way, $Trueprop$ is a coercion  lcp@105  315 from $o$ to $prop$.  lcp@105  316 lcp@105  317 lcp@105  318 \subsection{Expressing propositional rules}  lcp@312  319 \index{rules!propositional}  lcp@105  320 We shall illustrate the use of the meta-logic by formalizing the rules of  lcp@296  321 Fig.\ts\ref{fol-fig}. Each object-level rule is expressed as a meta-level  lcp@105  322 axiom.  lcp@105  323 lcp@105  324 One of the simplest rules is $(\conj E1)$. Making  lcp@105  325 everything explicit, its formalization in the meta-logic is  wenzelm@3103  326 $$ wenzelm@3103  327 \Forall P\;Q. Trueprop(P\conj Q) \Imp Trueprop(P). \eqno(\conj E1)  wenzelm@3103  328 $$  lcp@105  329 This may look formidable, but it has an obvious reading: for all object-level  lcp@105  330 truth values $P$ and~$Q$, if $P\conj Q$ is true then so is~$P$. The  lcp@105  331 reading is correct because the meta-logic has simple models, where  lcp@105  332 types denote sets and $\Forall$ really means for all.'  lcp@105  333 lcp@312  334 \index{*Trueprop constant}  lcp@105  335 Isabelle adopts notational conventions to ease the writing of rules. We may  lcp@105  336 hide the occurrences of $Trueprop$ by making it an implicit coercion.  lcp@105  337 Outer universal quantifiers may be dropped. Finally, the nested implication  lcp@312  338 \index{meta-implication}  lcp@105  339 $\phi@1\Imp(\cdots \phi@n\Imp\psi\cdots)$  lcp@105  340 may be abbreviated as $\List{\phi@1; \ldots; \phi@n} \Imp \psi$, which  lcp@105  341 formalizes a rule of $n$~premises.  lcp@105  342 lcp@105  343 Using these conventions, the conjunction rules become the following axioms.  lcp@105  344 These fully specify the properties of~$\conj$:  lcp@105  345 $$\List{P; Q} \Imp P\conj Q \eqno(\conj I)$$  lcp@105  346 $$P\conj Q \Imp P \qquad P\conj Q \Imp Q \eqno(\conj E1,2)$$  lcp@105  347 lcp@105  348 \noindent  lcp@105  349 Next, consider the disjunction rules. The discharge of assumption in  lcp@105  350 $(\disj E)$ is expressed using $\Imp$:  lcp@331  351 \index{assumptions!discharge of}%  lcp@105  352 $$P \Imp P\disj Q \qquad Q \Imp P\disj Q \eqno(\disj I1,2)$$  lcp@105  353 $$\List{P\disj Q; P\Imp R; Q\Imp R} \Imp R \eqno(\disj E)$$  lcp@331  354 %  lcp@312  355 To understand this treatment of assumptions in natural  lcp@105  356 deduction, look at implication. The rule $({\imp}I)$ is the classic  lcp@105  357 example of natural deduction: to prove that $P\imp Q$ is true, assume $P$  lcp@105  358 is true and show that $Q$ must then be true. More concisely, if $P$  lcp@105  359 implies $Q$ (at the meta-level), then $P\imp Q$ is true (at the  lcp@105  360 object-level). Showing the coercion explicitly, this is formalized as  lcp@105  361 $(Trueprop(P)\Imp Trueprop(Q)) \Imp Trueprop(P\imp Q).$  lcp@105  362 The rule $({\imp}E)$ is straightforward; hiding $Trueprop$, the axioms to  lcp@105  363 specify $\imp$ are  lcp@105  364 $$(P \Imp Q) \Imp P\imp Q \eqno({\imp}I)$$  lcp@105  365 $$\List{P\imp Q; P} \Imp Q. \eqno({\imp}E)$$  lcp@105  366 lcp@105  367 \noindent  lcp@105  368 Finally, the intuitionistic contradiction rule is formalized as the axiom  lcp@105  369 $$\bot \Imp P. \eqno(\bot E)$$  lcp@105  370 lcp@105  371 \begin{warn}  lcp@105  372 Earlier versions of Isabelle, and certain  paulson@1878  373 papers~\cite{paulson-found,paulson700}, use $\List{P}$ to mean $Trueprop(P)$.  lcp@105  374 \end{warn}  lcp@105  375 lcp@105  376 \subsection{Quantifier rules and substitution}  lcp@312  377 \index{quantifiers}\index{rules!quantifier}\index{substitution|bold}  lcp@312  378 \index{variables!bound}\index{lambda abs@$\lambda$-abstractions}  lcp@312  379 \index{function applications}  lcp@312  380 lcp@105  381 Isabelle expresses variable binding using $\lambda$-abstraction; for instance,  lcp@105  382 $\forall x.P$ is formalized as $\forall(\lambda x.P)$. Recall that $F(t)$  lcp@105  383 is Isabelle's syntax for application of the function~$F$ to the argument~$t$;  lcp@105  384 it is not a meta-notation for substitution. On the other hand, a substitution  lcp@105  385 will take place if $F$ has the form $\lambda x.P$; Isabelle transforms  lcp@105  386 $(\lambda x.P)(t)$ to~$P[t/x]$ by $\beta$-conversion. Thus, we can express  lcp@105  387 inference rules that involve substitution for bound variables.  lcp@105  388 lcp@105  389 \index{parameters|bold}\index{eigenvariables|see{parameters}}  lcp@105  390 A logic may attach provisos to certain of its rules, especially quantifier  lcp@105  391 rules. We cannot hope to formalize arbitrary provisos. Fortunately, those  lcp@105  392 typical of quantifier rules always have the same form, namely $x$ not free in  lcp@105  393 \ldots {\it (some set of formulae)},' where $x$ is a variable (called a {\bf  lcp@105  394 parameter} or {\bf eigenvariable}) in some premise. Isabelle treats  lcp@105  395 provisos using~$\Forall$, its inbuilt notion of for all'.  lcp@312  396 \index{meta-quantifiers}  lcp@105  397 lcp@105  398 The purpose of the proviso $x$ not free in \ldots' is  lcp@105  399 to ensure that the premise may not make assumptions about the value of~$x$,  lcp@105  400 and therefore holds for all~$x$. We formalize $(\forall I)$ by  lcp@105  401 $\left(\Forall x. Trueprop(P(x))\right) \Imp Trueprop(\forall x.P(x)).$  lcp@105  402 This means, if $P(x)$ is true for all~$x$, then $\forall x.P(x)$ is true.'  lcp@105  403 The $\forall E$ rule exploits $\beta$-conversion. Hiding $Trueprop$, the  lcp@105  404 $\forall$ axioms are  lcp@105  405 $$\left(\Forall x. P(x)\right) \Imp \forall x.P(x) \eqno(\forall I)$$  wenzelm@3103  406 $$(\forall x.P(x)) \Imp P(t). \eqno(\forall E)$$  lcp@105  407 lcp@105  408 \noindent  lcp@105  409 We have defined the object-level universal quantifier~($\forall$)  lcp@105  410 using~$\Forall$. But we do not require meta-level counterparts of all the  lcp@105  411 connectives of the object-logic! Consider the existential quantifier:  wenzelm@3103  412 $$P(t) \Imp \exists x.P(x) \eqno(\exists I)$$  lcp@105  413 $$\List{\exists x.P(x);\; \Forall x. P(x)\Imp Q} \Imp Q \eqno(\exists E)$$  lcp@105  414 Let us verify $(\exists E)$ semantically. Suppose that the premises  lcp@312  415 hold; since $\exists x.P(x)$ is true, we may choose an~$a$ such that $P(a)$ is  lcp@105  416 true. Instantiating $\Forall x. P(x)\Imp Q$ with $a$ yields $P(a)\Imp Q$, and  lcp@105  417 we obtain the desired conclusion, $Q$.  lcp@105  418 lcp@105  419 The treatment of substitution deserves mention. The rule  lcp@105  420 $\infer{P[u/t]}{t=u & P}$  lcp@105  421 would be hard to formalize in Isabelle. It calls for replacing~$t$ by $u$  lcp@105  422 throughout~$P$, which cannot be expressed using $\beta$-conversion. Our  lcp@312  423 rule~$(subst)$ uses~$P$ as a template for substitution, inferring $P[u/x]$  lcp@312  424 from~$P[t/x]$. When we formalize this as an axiom, the template becomes a  lcp@312  425 function variable:  wenzelm@3103  426 $$\List{t=u; P(t)} \Imp P(u). \eqno(subst)$$  lcp@105  427 lcp@105  428 lcp@105  429 \subsection{Signatures and theories}  lcp@312  430 \index{signatures|bold}  lcp@312  431 paulson@6170  432 A {\bf signature} contains the information necessary for type-checking,  wenzelm@3103  433 parsing and pretty printing a term. It specifies type classes and their  lcp@331  434 relationships, types and their arities, constants and their types, etc. It  wenzelm@3103  435 also contains grammar rules, specified using mixfix declarations.  lcp@105  436 lcp@105  437 Two signatures can be merged provided their specifications are compatible ---  lcp@105  438 they must not, for example, assign different types to the same constant.  lcp@105  439 Under similar conditions, a signature can be extended. Signatures are  lcp@105  440 managed internally by Isabelle; users seldom encounter them.  lcp@105  441 wenzelm@9695  442 \index{theories|bold} A {\bf theory} consists of a signature plus a collection  wenzelm@9695  443 of axioms. The Pure theory contains only the meta-logic. Theories can be  wenzelm@9695  444 combined provided their signatures are compatible. A theory definition  wenzelm@9695  445 extends an existing theory with further signature specifications --- classes,  wenzelm@9695  446 types, constants and mixfix declarations --- plus lists of axioms and  wenzelm@9695  447 definitions etc., expressed as strings to be parsed. A theory can formalize a  wenzelm@9695  448 small piece of mathematics, such as lists and their operations, or an entire  wenzelm@9695  449 logic. A mathematical development typically involves many theories in a  wenzelm@9695  450 hierarchy. For example, the Pure theory could be extended to form a theory  wenzelm@9695  451 for Fig.\ts\ref{fol-fig}; this could be extended in two separate ways to form  wenzelm@9695  452 a theory for natural numbers and a theory for lists; the union of these two  wenzelm@9695  453 could be extended into a theory defining the length of a list:  lcp@296  454 \begin{tt}  lcp@296  455 $ lcp@105  456 \begin{array}{c@{}c@{}c@{}c@{}c}  wenzelm@3103  457  {} & {} &\hbox{Pure}& {} & {} \\  wenzelm@3103  458  {} & {} & \downarrow & {} & {} \\  wenzelm@3103  459  {} & {} &\hbox{FOL} & {} & {} \\  wenzelm@3103  460  {} & \swarrow & {} & \searrow & {} \\  lcp@105  461  \hbox{Nat} & {} & {} & {} & \hbox{List} \\  wenzelm@3103  462  {} & \searrow & {} & \swarrow & {} \\  wenzelm@3103  463  {} & {} &\hbox{Nat}+\hbox{List}& {} & {} \\  wenzelm@3103  464  {} & {} & \downarrow & {} & {} \\  wenzelm@3103  465  {} & {} & \hbox{Length} & {} & {}  lcp@105  466 \end{array}  lcp@105  467 $  lcp@331  468 \end{tt}%  lcp@105  469 Each Isabelle proof typically works within a single theory, which is  lcp@105  470 associated with the proof state. However, many different theories may  lcp@105  471 coexist at the same time, and you may work in each of these during a single  lcp@105  472 session.  lcp@105  473 lcp@331  474 \begin{warn}\index{constants!clashes with variables}%  lcp@296  475  Confusing problems arise if you work in the wrong theory. Each theory  lcp@296  476  defines its own syntax. An identifier may be regarded in one theory as a  wenzelm@3103  477  constant and in another as a variable, for example.  lcp@296  478 \end{warn}  lcp@105  479 lcp@105  480 \section{Proof construction in Isabelle}  lcp@296  481 I have elsewhere described the meta-logic and demonstrated it by  paulson@1878  482 formalizing first-order logic~\cite{paulson-found}. There is a one-to-one  lcp@296  483 correspondence between meta-level proofs and object-level proofs. To each  lcp@296  484 use of a meta-level axiom, such as $(\forall I)$, there is a use of the  lcp@296  485 corresponding object-level rule. Object-level assumptions and parameters  lcp@296  486 have meta-level counterparts. The meta-level formalization is {\bf  lcp@296  487  faithful}, admitting no incorrect object-level inferences, and {\bf  lcp@296  488  adequate}, admitting all correct object-level inferences. These  lcp@296  489 properties must be demonstrated separately for each object-logic.  lcp@105  490 lcp@105  491 The meta-logic is defined by a collection of inference rules, including  lcp@331  492 equational rules for the $\lambda$-calculus and logical rules. The rules  lcp@105  493 for~$\Imp$ and~$\Forall$ resemble those for~$\imp$ and~$\forall$ in  lcp@296  494 Fig.\ts\ref{fol-fig}. Proofs performed using the primitive meta-rules  lcp@105  495 would be lengthy; Isabelle proofs normally use certain derived rules.  lcp@105  496 {\bf Resolution}, in particular, is convenient for backward proof.  lcp@105  497 lcp@105  498 Unification is central to theorem proving. It supports quantifier  lcp@105  499 reasoning by allowing certain unknown' terms to be instantiated later,  lcp@105  500 possibly in stages. When proving that the time required to sort $n$  lcp@105  501 integers is proportional to~$n^2$, we need not state the constant of  lcp@105  502 proportionality; when proving that a hardware adder will deliver the sum of  lcp@105  503 its inputs, we need not state how many clock ticks will be required. Such  lcp@105  504 quantities often emerge from the proof.  lcp@105  505 lcp@312  506 Isabelle provides {\bf schematic variables}, or {\bf  lcp@312  507  unknowns},\index{unknowns} for unification. Logically, unknowns are free  lcp@312  508 variables. But while ordinary variables remain fixed, unification may  lcp@312  509 instantiate unknowns. Unknowns are written with a ?\ prefix and are  lcp@312  510 frequently subscripted: $\Var{a}$, $\Var{a@1}$, $\Var{a@2}$, \ldots,  lcp@312  511 $\Var{P}$, $\Var{P@1}$, \ldots.  lcp@105  512 lcp@105  513 Recall that an inference rule of the form  lcp@105  514 $\infer{\phi}{\phi@1 & \ldots & \phi@n}$  lcp@105  515 is formalized in Isabelle's meta-logic as the axiom  lcp@312  516 $\List{\phi@1; \ldots; \phi@n} \Imp \phi$.\index{resolution}  lcp@296  517 Such axioms resemble Prolog's Horn clauses, and can be combined by  lcp@105  518 resolution --- Isabelle's principal proof method. Resolution yields both  lcp@105  519 forward and backward proof. Backward proof works by unifying a goal with  lcp@105  520 the conclusion of a rule, whose premises become new subgoals. Forward proof  lcp@105  521 works by unifying theorems with the premises of a rule, deriving a new theorem.  lcp@105  522 lcp@312  523 Isabelle formulae require an extended notion of resolution.  lcp@296  524 They differ from Horn clauses in two major respects:  lcp@105  525 \begin{itemize}  lcp@105  526  \item They are written in the typed $\lambda$-calculus, and therefore must be  lcp@105  527 resolved using higher-order unification.  lcp@105  528 lcp@296  529 \item The constituents of a clause need not be atomic formulae. Any  lcp@296  530  formula of the form $Trueprop(\cdots)$ is atomic, but axioms such as  lcp@296  531  ${\imp}I$ and $\forall I$ contain non-atomic formulae.  lcp@105  532 \end{itemize}  lcp@296  533 Isabelle has little in common with classical resolution theorem provers  lcp@105  534 such as Otter~\cite{wos-bledsoe}. At the meta-level, Isabelle proves  lcp@105  535 theorems in their positive form, not by refutation. However, an  lcp@105  536 object-logic that includes a contradiction rule may employ a refutation  lcp@105  537 proof procedure.  lcp@105  538 lcp@105  539 lcp@105  540 \subsection{Higher-order unification}  lcp@105  541 \index{unification!higher-order|bold}  lcp@105  542 Unification is equation solving. The solution of $f(\Var{x},c) \qeq  lcp@105  543 f(d,\Var{y})$ is $\Var{x}\equiv d$ and $\Var{y}\equiv c$. {\bf  lcp@105  544 Higher-order unification} is equation solving for typed $\lambda$-terms.  lcp@105  545 To handle $\beta$-conversion, it must reduce $(\lambda x.t)u$ to $t[u/x]$.  lcp@105  546 That is easy --- in the typed $\lambda$-calculus, all reduction sequences  lcp@105  547 terminate at a normal form. But it must guess the unknown  lcp@105  548 function~$\Var{f}$ in order to solve the equation  lcp@105  549  \label{hou-eqn}  lcp@105  550  \Var{f}(t) \qeq g(u@1,\ldots,u@k).  lcp@105  551   lcp@105  552 Huet's~\cite{huet75} search procedure solves equations by imitation and  lcp@312  553 projection. {\bf Imitation} makes~$\Var{f}$ apply the leading symbol (if a  lcp@312  554 constant) of the right-hand side. To solve equation~(\ref{hou-eqn}), it  lcp@312  555 guesses  lcp@105  556 $\Var{f} \equiv \lambda x. g(\Var{h@1}(x),\ldots,\Var{h@k}(x)),$  lcp@105  557 where $\Var{h@1}$, \ldots, $\Var{h@k}$ are new unknowns. Assuming there are no  lcp@105  558 other occurrences of~$\Var{f}$, equation~(\ref{hou-eqn}) simplifies to the  lcp@105  559 set of equations  lcp@105  560 $\Var{h@1}(t)\qeq u@1 \quad\ldots\quad \Var{h@k}(t)\qeq u@k.$  lcp@105  561 If the procedure solves these equations, instantiating $\Var{h@1}$, \ldots,  lcp@105  562 $\Var{h@k}$, then it yields an instantiation for~$\Var{f}$.  lcp@105  563 lcp@105  564 {\bf Projection} makes $\Var{f}$ apply one of its arguments. To solve  lcp@105  565 equation~(\ref{hou-eqn}), if $t$ expects~$m$ arguments and delivers a  lcp@105  566 result of suitable type, it guesses  lcp@105  567 $\Var{f} \equiv \lambda x. x(\Var{h@1}(x),\ldots,\Var{h@m}(x)),$  lcp@105  568 where $\Var{h@1}$, \ldots, $\Var{h@m}$ are new unknowns. Assuming there are no  lcp@105  569 other occurrences of~$\Var{f}$, equation~(\ref{hou-eqn}) simplifies to the  lcp@105  570 equation  wenzelm@3103  571 $t(\Var{h@1}(t),\ldots,\Var{h@m}(t)) \qeq g(u@1,\ldots,u@k).$  lcp@105  572 lcp@331  573 \begin{warn}\index{unification!incompleteness of}%  lcp@105  574 Huet's unification procedure is complete. Isabelle's polymorphic version,  lcp@105  575 which solves for type unknowns as well as for term unknowns, is incomplete.  lcp@105  576 The problem is that projection requires type information. In  lcp@105  577 equation~(\ref{hou-eqn}), if the type of~$t$ is unknown, then projections  lcp@105  578 are possible for all~$m\geq0$, and the types of the $\Var{h@i}$ will be  lcp@105  579 similarly unconstrained. Therefore, Isabelle never attempts such  lcp@105  580 projections, and may fail to find unifiers where a type unknown turns out  lcp@105  581 to be a function type.  lcp@105  582 \end{warn}  lcp@105  583 lcp@312  584 \index{unknowns!function|bold}  lcp@105  585 Given $\Var{f}(t@1,\ldots,t@n)\qeq u$, Huet's procedure could make up to  lcp@105  586 $n+1$ guesses. The search tree and set of unifiers may be infinite. But  lcp@105  587 higher-order unification can work effectively, provided you are careful  lcp@105  588 with {\bf function unknowns}:  lcp@105  589 \begin{itemize}  lcp@105  590  \item Equations with no function unknowns are solved using first-order  lcp@105  591 unification, extended to treat bound variables. For example, $\lambda x.x  lcp@105  592 \qeq \lambda x.\Var{y}$ has no solution because $\Var{y}\equiv x$ would  lcp@105  593 capture the free variable~$x$.  lcp@105  594 lcp@105  595  \item An occurrence of the term $\Var{f}(x,y,z)$, where the arguments are  lcp@105  596 distinct bound variables, causes no difficulties. Its projections can only  lcp@105  597 match the corresponding variables.  lcp@105  598 lcp@105  599  \item Even an equation such as $\Var{f}(a)\qeq a+a$ is all right. It has  lcp@105  600 four solutions, but Isabelle evaluates them lazily, trying projection before  paulson@3485  601 imitation. The first solution is usually the one desired:  lcp@105  602 $\Var{f}\equiv \lambda x. x+x \quad  lcp@105  603  \Var{f}\equiv \lambda x. a+x \quad  lcp@105  604  \Var{f}\equiv \lambda x. x+a \quad  lcp@105  605  \Var{f}\equiv \lambda x. a+a$  lcp@105  606  \item Equations such as $\Var{f}(\Var{x},\Var{y})\qeq t$ and  lcp@105  607 $\Var{f}(\Var{g}(x))\qeq t$ admit vast numbers of unifiers, and must be  lcp@105  608 avoided.  lcp@105  609 \end{itemize}  lcp@105  610 In problematic cases, you may have to instantiate some unknowns before  lcp@105  611 invoking unification.  lcp@105  612 lcp@105  613 lcp@105  614 \subsection{Joining rules by resolution} \label{joining}  lcp@105  615 \index{resolution|bold}  lcp@105  616 Let $\List{\psi@1; \ldots; \psi@m} \Imp \psi$ and $\List{\phi@1; \ldots;  lcp@105  617 \phi@n} \Imp \phi$ be two Isabelle theorems, representing object-level rules.  lcp@105  618 Choosing some~$i$ from~1 to~$n$, suppose that $\psi$ and $\phi@i$ have a  lcp@105  619 higher-order unifier. Writing $Xs$ for the application of substitution~$s$ to  lcp@105  620 expression~$X$, this means there is some~$s$ such that $\psi s\equiv \phi@i s$.  lcp@105  621 By resolution, we may conclude  lcp@105  622 $(\List{\phi@1; \ldots; \phi@{i-1}; \psi@1; \ldots; \psi@m;  lcp@105  623  \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.  lcp@105  624 $  lcp@105  625 The substitution~$s$ may instantiate unknowns in both rules. In short,  lcp@105  626 resolution is the following rule:  lcp@105  627 $\infer[(\psi s\equiv \phi@i s)]  lcp@105  628  {(\List{\phi@1; \ldots; \phi@{i-1}; \psi@1; \ldots; \psi@m;  lcp@105  629  \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s}  lcp@105  630  {\List{\psi@1; \ldots; \psi@m} \Imp \psi & &  lcp@105  631  \List{\phi@1; \ldots; \phi@n} \Imp \phi}  lcp@105  632 $  lcp@105  633 It operates at the meta-level, on Isabelle theorems, and is justified by  lcp@105  634 the properties of $\Imp$ and~$\Forall$. It takes the number~$i$ (for  lcp@105  635 $1\leq i\leq n$) as a parameter and may yield infinitely many conclusions,  lcp@105  636 one for each unifier of $\psi$ with $\phi@i$. Isabelle returns these  lcp@105  637 conclusions as a sequence (lazy list).  lcp@105  638 wenzelm@3103  639 Resolution expects the rules to have no outer quantifiers~($\Forall$).  wenzelm@3103  640 It may rename or instantiate any schematic variables, but leaves free  wenzelm@3103  641 variables unchanged. When constructing a theory, Isabelle puts the  wenzelm@3106  642 rules into a standard form with all free variables converted into  wenzelm@3106  643 schematic ones; for instance, $({\imp}E)$ becomes  lcp@105  644 $\List{\Var{P}\imp \Var{Q}; \Var{P}} \Imp \Var{Q}.  lcp@105  645 $  lcp@105  646 When resolving two rules, the unknowns in the first rule are renamed, by  lcp@105  647 subscripting, to make them distinct from the unknowns in the second rule. To  lcp@331  648 resolve $({\imp}E)$ with itself, the first copy of the rule becomes  lcp@105  649 $\List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}} \Imp \Var{Q@1}.$  lcp@105  650 Resolving this with $({\imp}E)$ in the first premise, unifying $\Var{Q@1}$ with  lcp@105  651 $\Var{P}\imp \Var{Q}$, is the meta-level inference  lcp@105  652 $\infer{\List{\Var{P@1}\imp (\Var{P}\imp \Var{Q}); \Var{P@1}; \Var{P}}  lcp@105  653  \Imp\Var{Q}.}  lcp@105  654  {\List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}} \Imp \Var{Q@1} & &  lcp@105  655  \List{\Var{P}\imp \Var{Q}; \Var{P}} \Imp \Var{Q}}  lcp@105  656 $  lcp@105  657 Renaming the unknowns in the resolvent, we have derived the  lcp@331  658 object-level rule\index{rules!derived}  lcp@105  659 $\infer{Q.}{R\imp (P\imp Q) & R & P}$  lcp@105  660 Joining rules in this fashion is a simple way of proving theorems. The  lcp@105  661 derived rules are conservative extensions of the object-logic, and may permit  lcp@105  662 simpler proofs. Let us consider another example. Suppose we have the axiom  lcp@105  663 $$\forall x\,y. Suc(x)=Suc(y)\imp x=y. \eqno (inject)$$  lcp@105  664 lcp@105  665 \noindent  lcp@105  666 The standard form of $(\forall E)$ is  lcp@105  667 $\forall x.\Var{P}(x) \Imp \Var{P}(\Var{t})$.  lcp@105  668 Resolving $(inject)$ with $(\forall E)$ replaces $\Var{P}$ by  lcp@105  669 $\lambda x. \forall y. Suc(x)=Suc(y)\imp x=y$ and leaves $\Var{t}$  lcp@105  670 unchanged, yielding  lcp@105  671 $\forall y. Suc(\Var{t})=Suc(y)\imp \Var{t}=y.$  lcp@105  672 Resolving this with $(\forall E)$ puts a subscript on~$\Var{t}$  lcp@105  673 and yields  lcp@105  674 $Suc(\Var{t@1})=Suc(\Var{t})\imp \Var{t@1}=\Var{t}.$  lcp@105  675 Resolving this with $({\imp}E)$ increases the subscripts and yields  lcp@105  676 $Suc(\Var{t@2})=Suc(\Var{t@1})\Imp \Var{t@2}=\Var{t@1}.  lcp@105  677 $  lcp@105  678 We have derived the rule  lcp@105  679 $\infer{m=n,}{Suc(m)=Suc(n)}$  lcp@105  680 which goes directly from $Suc(m)=Suc(n)$ to $m=n$. It is handy for simplifying  lcp@105  681 an equation like $Suc(Suc(Suc(m)))=Suc(Suc(Suc(0)))$.  lcp@105  682 lcp@105  683 lcp@296  684 \section{Lifting a rule into a context}  lcp@105  685 The rules $({\imp}I)$ and $(\forall I)$ may seem unsuitable for  lcp@105  686 resolution. They have non-atomic premises, namely $P\Imp Q$ and $\Forall  lcp@105  687 x.P(x)$, while the conclusions of all the rules are atomic (they have the form  lcp@105  688 $Trueprop(\cdots)$). Isabelle gets round the problem through a meta-inference  lcp@105  689 called \bfindex{lifting}. Let us consider how to construct proofs such as  lcp@105  690 $\infer[({\imp}I)]{P\imp(Q\imp R)}  lcp@105  691  {\infer[({\imp}I)]{Q\imp R}  lcp@296  692  {\infer*{R}{[P,Q]}}}  lcp@105  693  \qquad  lcp@105  694  \infer[(\forall I)]{\forall x\,y.P(x,y)}  lcp@105  695  {\infer[(\forall I)]{\forall y.P(x,y)}{P(x,y)}}  lcp@105  696 $  lcp@105  697 lcp@296  698 \subsection{Lifting over assumptions}  lcp@312  699 \index{assumptions!lifting over}  lcp@105  700 Lifting over $\theta\Imp{}$ is the following meta-inference rule:  lcp@105  701 $\infer{\List{\theta\Imp\phi@1; \ldots; \theta\Imp\phi@n} \Imp  lcp@105  702  (\theta \Imp \phi)}  lcp@105  703  {\List{\phi@1; \ldots; \phi@n} \Imp \phi}$  lcp@105  704 This is clearly sound: if $\List{\phi@1; \ldots; \phi@n} \Imp \phi$ is true and  lcp@296  705 $\theta\Imp\phi@1$, \ldots, $\theta\Imp\phi@n$ and $\theta$ are all true then  lcp@105  706 $\phi$ must be true. Iterated lifting over a series of meta-formulae  lcp@105  707 $\theta@k$, \ldots, $\theta@1$ yields an object-rule whose conclusion is  lcp@105  708 $\List{\theta@1; \ldots; \theta@k} \Imp \phi$. Typically the $\theta@i$ are  lcp@105  709 the assumptions in a natural deduction proof; lifting copies them into a rule's  lcp@105  710 premises and conclusion.  lcp@105  711 lcp@105  712 When resolving two rules, Isabelle lifts the first one if necessary. The  lcp@105  713 standard form of $({\imp}I)$ is  lcp@105  714 $(\Var{P} \Imp \Var{Q}) \Imp \Var{P}\imp \Var{Q}.$  lcp@105  715 To resolve this rule with itself, Isabelle modifies one copy as follows: it  lcp@105  716 renames the unknowns to $\Var{P@1}$ and $\Var{Q@1}$, then lifts the rule over  lcp@296  717 $\Var{P}\Imp{}$ to obtain  lcp@296  718 $(\Var{P}\Imp (\Var{P@1} \Imp \Var{Q@1})) \Imp (\Var{P} \Imp  lcp@296  719  (\Var{P@1}\imp \Var{Q@1})).$  lcp@296  720 Using the $\List{\cdots}$ abbreviation, this can be written as  lcp@105  721 $\List{\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}; \Var{P}}  lcp@105  722  \Imp \Var{P@1}\imp \Var{Q@1}.$  lcp@105  723 Unifying $\Var{P}\Imp \Var{P@1}\imp\Var{Q@1}$ with $\Var{P} \Imp  lcp@105  724 \Var{Q}$ instantiates $\Var{Q}$ to ${\Var{P@1}\imp\Var{Q@1}}$.  lcp@105  725 Resolution yields  lcp@105  726 $(\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}) \Imp  lcp@105  727 \Var{P}\imp(\Var{P@1}\imp\Var{Q@1}).$  lcp@105  728 This represents the derived rule  lcp@105  729 $\infer{P\imp(Q\imp R).}{\infer*{R}{[P,Q]}}$  lcp@105  730 lcp@296  731 \subsection{Lifting over parameters}  lcp@312  732 \index{parameters!lifting over}  lcp@105  733 An analogous form of lifting handles premises of the form $\Forall x\ldots\,$.  lcp@105  734 Here, lifting prefixes an object-rule's premises and conclusion with $\Forall  lcp@105  735 x$. At the same time, lifting introduces a dependence upon~$x$. It replaces  lcp@105  736 each unknown $\Var{a}$ in the rule by $\Var{a'}(x)$, where $\Var{a'}$ is a new  lcp@105  737 unknown (by subscripting) of suitable type --- necessarily a function type. In  lcp@105  738 short, lifting is the meta-inference  lcp@105  739 $\infer{\List{\Forall x.\phi@1^x; \ldots; \Forall x.\phi@n^x}  lcp@105  740  \Imp \Forall x.\phi^x,}  lcp@105  741  {\List{\phi@1; \ldots; \phi@n} \Imp \phi}$  lcp@296  742 %  lcp@296  743 where $\phi^x$ stands for the result of lifting unknowns over~$x$ in  lcp@296  744 $\phi$. It is not hard to verify that this meta-inference is sound. If  lcp@296  745 $\phi\Imp\psi$ then $\phi^x\Imp\psi^x$ for all~$x$; so if $\phi^x$ is true  lcp@296  746 for all~$x$ then so is $\psi^x$. Thus, from $\phi\Imp\psi$ we conclude  lcp@296  747 $(\Forall x.\phi^x) \Imp (\Forall x.\psi^x)$.  lcp@296  748 lcp@105  749 For example, $(\disj I)$ might be lifted to  lcp@105  750 $(\Forall x.\Var{P@1}(x)) \Imp (\Forall x. \Var{P@1}(x)\disj \Var{Q@1}(x))$  lcp@105  751 and $(\forall I)$ to  lcp@105  752 $(\Forall x\,y.\Var{P@1}(x,y)) \Imp (\Forall x. \forall y.\Var{P@1}(x,y)).$  lcp@105  753 Isabelle has renamed a bound variable in $(\forall I)$ from $x$ to~$y$,  lcp@105  754 avoiding a clash. Resolving the above with $(\forall I)$ is the meta-inference  lcp@105  755 $\infer{\Forall x\,y.\Var{P@1}(x,y)) \Imp \forall x\,y.\Var{P@1}(x,y)) }  lcp@105  756  {(\Forall x\,y.\Var{P@1}(x,y)) \Imp  lcp@105  757  (\Forall x. \forall y.\Var{P@1}(x,y)) &  lcp@105  758  (\Forall x.\Var{P}(x)) \Imp (\forall x.\Var{P}(x))}$  lcp@105  759 Here, $\Var{P}$ is replaced by $\lambda x.\forall y.\Var{P@1}(x,y)$; the  lcp@105  760 resolvent expresses the derived rule  lcp@105  761 $\vcenter{ \infer{\forall x\,y.Q(x,y)}{Q(x,y)} }  lcp@105  762  \quad\hbox{provided x, y not free in the assumptions}  lcp@105  763 $  paulson@1878  764 I discuss lifting and parameters at length elsewhere~\cite{paulson-found}.  lcp@296  765 Miller goes into even greater detail~\cite{miller-mixed}.  lcp@105  766 lcp@105  767 lcp@105  768 \section{Backward proof by resolution}  lcp@312  769 \index{resolution!in backward proof}  lcp@296  770 lcp@105  771 Resolution is convenient for deriving simple rules and for reasoning  lcp@105  772 forward from facts. It can also support backward proof, where we start  lcp@105  773 with a goal and refine it to progressively simpler subgoals until all have  lcp@296  774 been solved. {\sc lcf} and its descendants {\sc hol} and Nuprl provide  wenzelm@3103  775 tactics and tacticals, which constitute a sophisticated language for  lcp@296  776 expressing proof searches. {\bf Tactics} refine subgoals while {\bf  lcp@296  777  tacticals} combine tactics.  lcp@105  778 lcp@312  779 \index{LCF system}  lcp@105  780 Isabelle's tactics and tacticals work differently from {\sc lcf}'s. An  lcp@296  781 Isabelle rule is bidirectional: there is no distinction between  lcp@105  782 inputs and outputs. {\sc lcf} has a separate tactic for each rule;  lcp@105  783 Isabelle performs refinement by any rule in a uniform fashion, using  lcp@105  784 resolution.  lcp@105  785 lcp@105  786 Isabelle works with meta-level theorems of the form  lcp@105  787 $$\List{\phi@1; \ldots; \phi@n} \Imp \phi$$.  lcp@105  788 We have viewed this as the {\bf rule} with premises  lcp@105  789 $\phi@1$,~\ldots,~$\phi@n$ and conclusion~$\phi$. It can also be viewed as  lcp@312  790 the {\bf proof state}\index{proof state}  lcp@312  791 with subgoals $\phi@1$,~\ldots,~$\phi@n$ and main  lcp@105  792 goal~$\phi$.  lcp@105  793 lcp@105  794 To prove the formula~$\phi$, take $\phi\Imp \phi$ as the initial proof  lcp@105  795 state. This assertion is, trivially, a theorem. At a later stage in the  lcp@105  796 backward proof, a typical proof state is $\List{\phi@1; \ldots; \phi@n}  lcp@296  797 \Imp \phi$. This proof state is a theorem, ensuring that the subgoals  lcp@296  798 $\phi@1$,~\ldots,~$\phi@n$ imply~$\phi$. If $n=0$ then we have  lcp@105  799 proved~$\phi$ outright. If $\phi$ contains unknowns, they may become  lcp@105  800 instantiated during the proof; a proof state may be $\List{\phi@1; \ldots;  lcp@105  801 \phi@n} \Imp \phi'$, where $\phi'$ is an instance of~$\phi$.  lcp@105  802 lcp@105  803 \subsection{Refinement by resolution}  lcp@105  804 To refine subgoal~$i$ of a proof state by a rule, perform the following  lcp@105  805 resolution:  lcp@105  806 $\infer{\hbox{new proof state}}{\hbox{rule} & & \hbox{proof state}}$  lcp@331  807 Suppose the rule is $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$ after  lcp@331  808 lifting over subgoal~$i$'s assumptions and parameters. If the proof state  lcp@331  809 is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, then the new proof state is  lcp@331  810 (for~$1\leq i\leq n$)  lcp@105  811 $(\List{\phi@1; \ldots; \phi@{i-1}; \psi'@1;  lcp@105  812  \ldots; \psi'@m; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.$  lcp@105  813 Substitution~$s$ unifies $\psi'$ with~$\phi@i$. In the proof state,  lcp@105  814 subgoal~$i$ is replaced by $m$ new subgoals, the rule's instantiated premises.  lcp@105  815 If some of the rule's unknowns are left un-instantiated, they become new  lcp@105  816 unknowns in the proof state. Refinement by~$(\exists I)$, namely  lcp@105  817 $\Var{P}(\Var{t}) \Imp \exists x. \Var{P}(x),$  lcp@105  818 inserts a new unknown derived from~$\Var{t}$ by subscripting and lifting.  lcp@105  819 We do not have to specify an existential witness' when  lcp@105  820 applying~$(\exists I)$. Further resolutions may instantiate unknowns in  lcp@105  821 the proof state.  lcp@105  822 lcp@105  823 \subsection{Proof by assumption}  lcp@312  824 \index{assumptions!use of}  lcp@105  825 In the course of a natural deduction proof, parameters $x@1$, \ldots,~$x@l$ and  lcp@105  826 assumptions $\theta@1$, \ldots, $\theta@k$ accumulate, forming a context for  lcp@105  827 each subgoal. Repeated lifting steps can lift a rule into any context. To  lcp@105  828 aid readability, Isabelle puts contexts into a normal form, gathering the  lcp@105  829 parameters at the front:  lcp@105  830  \label{context-eqn}  lcp@105  831 \Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta.  lcp@105  832   lcp@105  833 Under the usual reading of the connectives, this expresses that $\theta$  lcp@105  834 follows from $\theta@1$,~\ldots~$\theta@k$ for arbitrary  lcp@105  835 $x@1$,~\ldots,~$x@l$. It is trivially true if $\theta$ equals any of  lcp@105  836 $\theta@1$,~\ldots~$\theta@k$, or is unifiable with any of them. This  lcp@105  837 models proof by assumption in natural deduction.  lcp@105  838 lcp@105  839 Isabelle automates the meta-inference for proof by assumption. Its arguments  lcp@105  840 are the meta-theorem $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, and some~$i$  lcp@105  841 from~1 to~$n$, where $\phi@i$ has the form~(\ref{context-eqn}). Its results  lcp@105  842 are meta-theorems of the form  lcp@105  843 $(\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \phi@n} \Imp \phi)s$  lcp@105  844 for each $s$ and~$j$ such that $s$ unifies $\lambda x@1 \ldots x@l. \theta@j$  lcp@105  845 with $\lambda x@1 \ldots x@l. \theta$. Isabelle supplies the parameters  lcp@105  846 $x@1$,~\ldots,~$x@l$ to higher-order unification as bound variables, which  lcp@105  847 regards them as unique constants with a limited scope --- this enforces  paulson@1878  848 parameter provisos~\cite{paulson-found}.  lcp@105  849 lcp@296  850 The premise represents a proof state with~$n$ subgoals, of which the~$i$th  lcp@296  851 is to be solved by assumption. Isabelle searches the subgoal's context for  lcp@296  852 an assumption~$\theta@j$ that can solve it. For each unifier, the  lcp@296  853 meta-inference returns an instantiated proof state from which the $i$th  lcp@296  854 subgoal has been removed. Isabelle searches for a unifying assumption; for  lcp@296  855 readability and robustness, proofs do not refer to assumptions by number.  lcp@105  856 lcp@296  857 Consider the proof state  lcp@296  858 $(\List{P(a); P(b)} \Imp P(\Var{x})) \Imp Q(\Var{x}).$  lcp@105  859 Proof by assumption (with $i=1$, the only possibility) yields two results:  lcp@105  860 \begin{itemize}  lcp@105  861  \item $Q(a)$, instantiating $\Var{x}\equiv a$  lcp@105  862  \item $Q(b)$, instantiating $\Var{x}\equiv b$  lcp@105  863 \end{itemize}  lcp@105  864 Here, proof by assumption affects the main goal. It could also affect  lcp@296  865 other subgoals; if we also had the subgoal ${\List{P(b); P(c)} \Imp  lcp@296  866  P(\Var{x})}$, then $\Var{x}\equiv a$ would transform it to ${\List{P(b);  lcp@296  867  P(c)} \Imp P(a)}$, which might be unprovable.  lcp@296  868 lcp@105  869 lcp@105  870 \subsection{A propositional proof} \label{prop-proof}  lcp@105  871 \index{examples!propositional}  lcp@105  872 Our first example avoids quantifiers. Given the main goal $P\disj P\imp  lcp@105  873 P$, Isabelle creates the initial state  lcp@296  874 $(P\disj P\imp P)\Imp (P\disj P\imp P).$  lcp@296  875 %  lcp@105  876 Bear in mind that every proof state we derive will be a meta-theorem,  lcp@296  877 expressing that the subgoals imply the main goal. Our aim is to reach the  lcp@296  878 state $P\disj P\imp P$; this meta-theorem is the desired result.  lcp@296  879 lcp@296  880 The first step is to refine subgoal~1 by (${\imp}I)$, creating a new state  lcp@296  881 where $P\disj P$ is an assumption:  lcp@105  882 $(P\disj P\Imp P)\Imp (P\disj P\imp P)$  lcp@105  883 The next step is $(\disj E)$, which replaces subgoal~1 by three new subgoals.  lcp@105  884 Because of lifting, each subgoal contains a copy of the context --- the  lcp@105  885 assumption $P\disj P$. (In fact, this assumption is now redundant; we shall  lcp@105  886 shortly see how to get rid of it!) The new proof state is the following  lcp@105  887 meta-theorem, laid out for clarity:  lcp@105  888 $\begin{array}{l@{}l@{\qquad\qquad}l}  lcp@105  889  \lbrakk\;& P\disj P\Imp \Var{P@1}\disj\Var{Q@1}; & \hbox{(subgoal 1)} \\  lcp@105  890  & \List{P\disj P; \Var{P@1}} \Imp P; & \hbox{(subgoal 2)} \\  lcp@105  891  & \List{P\disj P; \Var{Q@1}} \Imp P & \hbox{(subgoal 3)} \\  lcp@105  892  \rbrakk\;& \Imp (P\disj P\imp P) & \hbox{(main goal)}  lcp@105  893  \end{array}  lcp@105  894 $  lcp@105  895 Notice the unknowns in the proof state. Because we have applied $(\disj E)$,  lcp@105  896 we must prove some disjunction, $\Var{P@1}\disj\Var{Q@1}$. Of course,  lcp@105  897 subgoal~1 is provable by assumption. This instantiates both $\Var{P@1}$ and  lcp@105  898 $\Var{Q@1}$ to~$P$ throughout the proof state:  lcp@105  899 $\begin{array}{l@{}l@{\qquad\qquad}l}  lcp@105  900  \lbrakk\;& \List{P\disj P; P} \Imp P; & \hbox{(subgoal 1)} \\  lcp@105  901  & \List{P\disj P; P} \Imp P & \hbox{(subgoal 2)} \\  lcp@105  902  \rbrakk\;& \Imp (P\disj P\imp P) & \hbox{(main goal)}  lcp@105  903  \end{array}$  lcp@105  904 Both of the remaining subgoals can be proved by assumption. After two such  lcp@296  905 steps, the proof state is $P\disj P\imp P$.  lcp@296  906 lcp@105  907 lcp@105  908 \subsection{A quantifier proof}  lcp@105  909 \index{examples!with quantifiers}  lcp@105  910 To illustrate quantifiers and $\Forall$-lifting, let us prove  lcp@105  911 $(\exists x.P(f(x)))\imp(\exists x.P(x))$. The initial proof  lcp@105  912 state is the trivial meta-theorem  lcp@105  913 $(\exists x.P(f(x)))\imp(\exists x.P(x)) \Imp  lcp@105  914  (\exists x.P(f(x)))\imp(\exists x.P(x)).$  lcp@105  915 As above, the first step is refinement by (${\imp}I)$:  lcp@105  916 $(\exists x.P(f(x))\Imp \exists x.P(x)) \Imp  lcp@105  917  (\exists x.P(f(x)))\imp(\exists x.P(x))  lcp@105  918 $  lcp@105  919 The next step is $(\exists E)$, which replaces subgoal~1 by two new subgoals.  lcp@105  920 Both have the assumption $\exists x.P(f(x))$. The new proof  lcp@105  921 state is the meta-theorem  lcp@105  922 $\begin{array}{l@{}l@{\qquad\qquad}l}  lcp@105  923  \lbrakk\;& \exists x.P(f(x)) \Imp \exists x.\Var{P@1}(x); & \hbox{(subgoal 1)} \\  lcp@105  924  & \Forall x.\List{\exists x.P(f(x)); \Var{P@1}(x)} \Imp  lcp@105  925  \exists x.P(x) & \hbox{(subgoal 2)} \\  lcp@105  926  \rbrakk\;& \Imp (\exists x.P(f(x)))\imp(\exists x.P(x)) & \hbox{(main goal)}  lcp@105  927  \end{array}  lcp@105  928 $  lcp@105  929 The unknown $\Var{P@1}$ appears in both subgoals. Because we have applied  lcp@105  930 $(\exists E)$, we must prove $\exists x.\Var{P@1}(x)$, where $\Var{P@1}(x)$ may  lcp@105  931 become any formula possibly containing~$x$. Proving subgoal~1 by assumption  lcp@105  932 instantiates $\Var{P@1}$ to~$\lambda x.P(f(x))$:  lcp@105  933 $\left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp  lcp@105  934  \exists x.P(x)\right)  lcp@105  935  \Imp (\exists x.P(f(x)))\imp(\exists x.P(x))  lcp@105  936 $  lcp@105  937 The next step is refinement by $(\exists I)$. The rule is lifted into the  lcp@296  938 context of the parameter~$x$ and the assumption $P(f(x))$. This copies  lcp@296  939 the context to the subgoal and allows the existential witness to  lcp@105  940 depend upon~$x$:  lcp@105  941 $\left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp  lcp@105  942  P(\Var{x@2}(x))\right)  lcp@105  943  \Imp (\exists x.P(f(x)))\imp(\exists x.P(x))  lcp@105  944 $  lcp@105  945 The existential witness, $\Var{x@2}(x)$, consists of an unknown  lcp@105  946 applied to a parameter. Proof by assumption unifies $\lambda x.P(f(x))$  lcp@105  947 with $\lambda x.P(\Var{x@2}(x))$, instantiating $\Var{x@2}$ to $f$. The final  lcp@105  948 proof state contains no subgoals: $(\exists x.P(f(x)))\imp(\exists x.P(x))$.  lcp@105  949 lcp@105  950 lcp@105  951 \subsection{Tactics and tacticals}  lcp@105  952 \index{tactics|bold}\index{tacticals|bold}  lcp@105  953 {\bf Tactics} perform backward proof. Isabelle tactics differ from those  lcp@105  954 of {\sc lcf}, {\sc hol} and Nuprl by operating on entire proof states,  lcp@105  955 rather than on individual subgoals. An Isabelle tactic is a function that  lcp@105  956 takes a proof state and returns a sequence (lazy list) of possible  lcp@296  957 successor states. Lazy lists are coded in ML as functions, a standard  paulson@6592  958 technique~\cite{paulson-ml2}. Isabelle represents proof states by theorems.  lcp@105  959 lcp@105  960 Basic tactics execute the meta-rules described above, operating on a  lcp@105  961 given subgoal. The {\bf resolution tactics} take a list of rules and  lcp@105  962 return next states for each combination of rule and unifier. The {\bf  lcp@105  963 assumption tactic} examines the subgoal's assumptions and returns next  lcp@105  964 states for each combination of assumption and unifier. Lazy lists are  lcp@105  965 essential because higher-order resolution may return infinitely many  lcp@105  966 unifiers. If there are no matching rules or assumptions then no next  lcp@105  967 states are generated; a tactic application that returns an empty list is  lcp@105  968 said to {\bf fail}.  lcp@105  969 lcp@105  970 Sequences realize their full potential with {\bf tacticals} --- operators  lcp@105  971 for combining tactics. Depth-first search, breadth-first search and  lcp@105  972 best-first search (where a heuristic function selects the best state to  lcp@105  973 explore) return their outcomes as a sequence. Isabelle provides such  lcp@105  974 procedures in the form of tacticals. Simpler procedures can be expressed  lcp@312  975 directly using the basic tacticals {\tt THEN}, {\tt ORELSE} and {\tt REPEAT}:  lcp@312  976 \begin{ttdescription}  lcp@312  977 \item[$tac1$ THEN $tac2$] is a tactic for sequential composition. Applied  lcp@105  978 to a proof state, it returns all states reachable in two steps by applying  lcp@105  979 $tac1$ followed by~$tac2$.  lcp@105  980 lcp@312  981 \item[$tac1$ ORELSE $tac2$] is a choice tactic. Applied to a state, it  lcp@105  982 tries~$tac1$ and returns the result if non-empty; otherwise, it uses~$tac2$.  lcp@105  983 lcp@312  984 \item[REPEAT $tac$] is a repetition tactic. Applied to a state, it  lcp@331  985 returns all states reachable by applying~$tac$ as long as possible --- until  lcp@331  986 it would fail.  lcp@312  987 \end{ttdescription}  lcp@105  988 For instance, this tactic repeatedly applies $tac1$ and~$tac2$, giving  lcp@105  989 $tac1$ priority:  lcp@312  990 \begin{center} \tt  lcp@312  991 REPEAT($tac1$ ORELSE $tac2$)  lcp@312  992 \end{center}  lcp@105  993 lcp@105  994 lcp@105  995 \section{Variations on resolution}  lcp@105  996 In principle, resolution and proof by assumption suffice to prove all  lcp@105  997 theorems. However, specialized forms of resolution are helpful for working  lcp@105  998 with elimination rules. Elim-resolution applies an elimination rule to an  lcp@105  999 assumption; destruct-resolution is similar, but applies a rule in a forward  lcp@105  1000 style.  lcp@105  1001 lcp@105  1002 The last part of the section shows how the techniques for proving theorems  lcp@105  1003 can also serve to derive rules.  lcp@105  1004 lcp@105  1005 \subsection{Elim-resolution}  lcp@312  1006 \index{elim-resolution|bold}\index{assumptions!deleting}  lcp@312  1007 lcp@105  1008 Consider proving the theorem $((R\disj R)\disj R)\disj R\imp R$. By  lcp@331  1009 $({\imp}I)$, we prove~$R$ from the assumption $((R\disj R)\disj R)\disj R$.  lcp@105  1010 Applying $(\disj E)$ to this assumption yields two subgoals, one that  lcp@105  1011 assumes~$R$ (and is therefore trivial) and one that assumes $(R\disj  lcp@105  1012 R)\disj R$. This subgoal admits another application of $(\disj E)$. Since  lcp@105  1013 natural deduction never discards assumptions, we eventually generate a  lcp@105  1014 subgoal containing much that is redundant:  lcp@105  1015 $\List{((R\disj R)\disj R)\disj R; (R\disj R)\disj R; R\disj R; R} \Imp R.$  lcp@105  1016 In general, using $(\disj E)$ on the assumption $P\disj Q$ creates two new  lcp@105  1017 subgoals with the additional assumption $P$ or~$Q$. In these subgoals,  lcp@331  1018 $P\disj Q$ is redundant. Other elimination rules behave  lcp@331  1019 similarly. In first-order logic, only universally quantified  lcp@105  1020 assumptions are sometimes needed more than once --- say, to prove  lcp@105  1021 $P(f(f(a)))$ from the assumptions $\forall x.P(x)\imp P(f(x))$ and~$P(a)$.  lcp@105  1022 lcp@105  1023 Many logics can be formulated as sequent calculi that delete redundant  lcp@105  1024 assumptions after use. The rule $(\disj E)$ might become  lcp@105  1025 $\infer[\disj\hbox{-left}]  lcp@105  1026  {\Gamma,P\disj Q,\Delta \turn \Theta}  lcp@105  1027  {\Gamma,P,\Delta \turn \Theta && \Gamma,Q,\Delta \turn \Theta}$  lcp@105  1028 In backward proof, a goal containing $P\disj Q$ on the left of the~$\turn$  lcp@105  1029 (that is, as an assumption) splits into two subgoals, replacing $P\disj Q$  lcp@105  1030 by $P$ or~$Q$. But the sequent calculus, with its explicit handling of  lcp@105  1031 assumptions, can be tiresome to use.  lcp@105  1032 lcp@105  1033 Elim-resolution is Isabelle's way of getting sequent calculus behaviour  lcp@105  1034 from natural deduction rules. It lets an elimination rule consume an  lcp@296  1035 assumption. Elim-resolution combines two meta-theorems:  lcp@296  1036 \begin{itemize}  lcp@296  1037  \item a rule $\List{\psi@1; \ldots; \psi@m} \Imp \psi$  lcp@296  1038  \item a proof state $\List{\phi@1; \ldots; \phi@n} \Imp \phi$  lcp@296  1039 \end{itemize}  lcp@296  1040 The rule must have at least one premise, thus $m>0$. Write the rule's  lcp@296  1041 lifted form as $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$. Suppose we  lcp@296  1042 wish to change subgoal number~$i$.  lcp@296  1043 lcp@296  1044 Ordinary resolution would attempt to reduce~$\phi@i$,  lcp@296  1045 replacing subgoal~$i$ by $m$ new ones. Elim-resolution tries  lcp@296  1046 simultaneously to reduce~$\phi@i$ and to solve~$\psi'@1$ by assumption; it  lcp@105  1047 returns a sequence of next states. Each of these replaces subgoal~$i$ by  lcp@105  1048 instances of $\psi'@2$, \ldots, $\psi'@m$ from which the selected  lcp@105  1049 assumption has been deleted. Suppose $\phi@i$ has the parameter~$x$ and  lcp@105  1050 assumptions $\theta@1$,~\ldots,~$\theta@k$. Then $\psi'@1$, the rule's first  lcp@105  1051 premise after lifting, will be  lcp@105  1052 $$\Forall x. \List{\theta@1; \ldots; \theta@k}\Imp \psi^{x}@1$$.  lcp@296  1053 Elim-resolution tries to unify $\psi'\qeq\phi@i$ and  lcp@296  1054 $\lambda x. \theta@j \qeq \lambda x. \psi^{x}@1$ simultaneously, for  lcp@296  1055 $j=1$,~\ldots,~$k$.  lcp@105  1056 lcp@105  1057 Let us redo the example from~\S\ref{prop-proof}. The elimination rule  lcp@105  1058 is~$(\disj E)$,  lcp@105  1059 $\List{\Var{P}\disj \Var{Q};\; \Var{P}\Imp \Var{R};\; \Var{Q}\Imp \Var{R}}  lcp@105  1060  \Imp \Var{R}$  lcp@105  1061 and the proof state is $(P\disj P\Imp P)\Imp (P\disj P\imp P)$. The  lcp@331  1062 lifted rule is  lcp@105  1063 $\begin{array}{l@{}l}  lcp@105  1064  \lbrakk\;& P\disj P \Imp \Var{P@1}\disj\Var{Q@1}; \\  lcp@105  1065  & \List{P\disj P ;\; \Var{P@1}} \Imp \Var{R@1}; \\  lcp@105  1066  & \List{P\disj P ;\; \Var{Q@1}} \Imp \Var{R@1} \\  paulson@1865  1067  \rbrakk\;& \Imp (P\disj P \Imp \Var{R@1})  lcp@105  1068  \end{array}  lcp@105  1069 $  lcp@331  1070 Unification takes the simultaneous equations  lcp@105  1071 $P\disj P \qeq \Var{P@1}\disj\Var{Q@1}$ and $\Var{R@1} \qeq P$, yielding  lcp@105  1072 $\Var{P@1}\equiv\Var{Q@1}\equiv\Var{R@1} \equiv P$. The new proof state  lcp@331  1073 is simply  lcp@105  1074 $\List{P \Imp P;\; P \Imp P} \Imp (P\disj P\imp P).  lcp@105  1075 $  lcp@105  1076 Elim-resolution's simultaneous unification gives better control  lcp@105  1077 than ordinary resolution. Recall the substitution rule:  lcp@105  1078 $$\List{\Var{t}=\Var{u}; \Var{P}(\Var{t})} \Imp \Var{P}(\Var{u})  wenzelm@3103  1079 \eqno(subst)$$  lcp@105  1080 Unsuitable for ordinary resolution because $\Var{P}(\Var{u})$ admits many  lcp@105  1081 unifiers, $(subst)$ works well with elim-resolution. It deletes some  lcp@105  1082 assumption of the form $x=y$ and replaces every~$y$ by~$x$ in the subgoal  lcp@105  1083 formula. The simultaneous unification instantiates $\Var{u}$ to~$y$; if  lcp@105  1084 $y$ is not an unknown, then $\Var{P}(y)$ can easily be unified with another  lcp@105  1085 formula.  lcp@105  1086 lcp@105  1087 In logical parlance, the premise containing the connective to be eliminated  lcp@105  1088 is called the \bfindex{major premise}. Elim-resolution expects the major  lcp@105  1089 premise to come first. The order of the premises is significant in  lcp@105  1090 Isabelle.  lcp@105  1091 lcp@105  1092 \subsection{Destruction rules} \label{destruct}  lcp@312  1093 \index{rules!destruction}\index{rules!elimination}  lcp@312  1094 \index{forward proof}  lcp@312  1095 lcp@296  1096 Looking back to Fig.\ts\ref{fol-fig}, notice that there are two kinds of  lcp@105  1097 elimination rule. The rules $({\conj}E1)$, $({\conj}E2)$, $({\imp}E)$ and  lcp@105  1098 $({\forall}E)$ extract the conclusion from the major premise. In Isabelle  lcp@312  1099 parlance, such rules are called {\bf destruction rules}; they are readable  lcp@105  1100 and easy to use in forward proof. The rules $({\disj}E)$, $({\bot}E)$ and  lcp@105  1101 $({\exists}E)$ work by discharging assumptions; they support backward proof  lcp@105  1102 in a style reminiscent of the sequent calculus.  lcp@105  1103 lcp@105  1104 The latter style is the most general form of elimination rule. In natural  lcp@105  1105 deduction, there is no way to recast $({\disj}E)$, $({\bot}E)$ or  lcp@105  1106 $({\exists}E)$ as destruction rules. But we can write general elimination  lcp@105  1107 rules for $\conj$, $\imp$ and~$\forall$:  lcp@105  1108 $ lcp@105  1109 \infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \qquad  lcp@105  1110 \infer{R}{P\imp Q & P & \infer*{R}{[Q]}} \qquad  lcp@105  1111 \infer{Q}{\forall x.P & \infer*{Q}{[P[t/x]]}}  lcp@105  1112 $  lcp@105  1113 Because they are concise, destruction rules are simpler to derive than the  lcp@105  1114 corresponding elimination rules. To facilitate their use in backward  lcp@105  1115 proof, Isabelle provides a means of transforming a destruction rule such as  lcp@105  1116 $\infer[\quad\hbox{to the elimination rule}\quad]{Q}{P@1 & \ldots & P@m}  lcp@105  1117  \infer{R.}{P@1 & \ldots & P@m & \infer*{R}{[Q]}}  lcp@105  1118 $  lcp@331  1119 {\bf Destruct-resolution}\index{destruct-resolution} combines this  lcp@331  1120 transformation with elim-resolution. It applies a destruction rule to some  lcp@331  1121 assumption of a subgoal. Given the rule above, it replaces the  lcp@331  1122 assumption~$P@1$ by~$Q$, with new subgoals of showing instances of $P@2$,  lcp@331  1123 \ldots,~$P@m$. Destruct-resolution works forward from a subgoal's  lcp@331  1124 assumptions. Ordinary resolution performs forward reasoning from theorems,  lcp@331  1125 as illustrated in~\S\ref{joining}.  lcp@105  1126 lcp@105  1127 lcp@105  1128 \subsection{Deriving rules by resolution} \label{deriving}  lcp@312  1129 \index{rules!derived|bold}\index{meta-assumptions!syntax of}  lcp@105  1130 The meta-logic, itself a form of the predicate calculus, is defined by a  lcp@105  1131 system of natural deduction rules. Each theorem may depend upon  lcp@105  1132 meta-assumptions. The theorem that~$\phi$ follows from the assumptions  lcp@105  1133 $\phi@1$, \ldots, $\phi@n$ is written  lcp@105  1134 $\phi \quad [\phi@1,\ldots,\phi@n].$  lcp@105  1135 A more conventional notation might be $\phi@1,\ldots,\phi@n \turn \phi$,  lcp@105  1136 but Isabelle's notation is more readable with large formulae.  lcp@105  1137 lcp@105  1138 Meta-level natural deduction provides a convenient mechanism for deriving  lcp@105  1139 new object-level rules. To derive the rule  lcp@105  1140 $\infer{\phi,}{\theta@1 & \ldots & \theta@k}$  lcp@105  1141 assume the premises $\theta@1$,~\ldots,~$\theta@k$ at the  lcp@105  1142 meta-level. Then prove $\phi$, possibly using these assumptions.  lcp@105  1143 Starting with a proof state $\phi\Imp\phi$, assumptions may accumulate,  lcp@105  1144 reaching a final state such as  lcp@105  1145 $\phi \quad [\theta@1,\ldots,\theta@k].$  lcp@105  1146 The meta-rule for $\Imp$ introduction discharges an assumption.  lcp@105  1147 Discharging them in the order $\theta@k,\ldots,\theta@1$ yields the  lcp@105  1148 meta-theorem $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, with no  lcp@105  1149 assumptions. This represents the desired rule.  lcp@105  1150 Let us derive the general $\conj$ elimination rule:  wenzelm@3103  1151 $$\infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \eqno(\conj E)$$  lcp@105  1152 We assume $P\conj Q$ and $\List{P;Q}\Imp R$, and commence backward proof in  lcp@105  1153 the state $R\Imp R$. Resolving this with the second assumption yields the  lcp@105  1154 state  lcp@105  1155 $\phantom{\List{P\conj Q;\; P\conj Q}}  lcp@105  1156  \llap{\List{P;Q}}\Imp R \quad [\,\List{P;Q}\Imp R\,].$  lcp@331  1157 Resolving subgoals~1 and~2 with~$({\conj}E1)$ and~$({\conj}E2)$,  lcp@105  1158 respectively, yields the state  lcp@331  1159 $\List{P\conj \Var{Q@1};\; \Var{P@2}\conj Q}\Imp R  lcp@331  1160  \quad [\,\List{P;Q}\Imp R\,].  lcp@331  1161 $  lcp@331  1162 The unknowns $\Var{Q@1}$ and~$\Var{P@2}$ arise from unconstrained  lcp@331  1163 subformulae in the premises of~$({\conj}E1)$ and~$({\conj}E2)$. Resolving  lcp@331  1164 both subgoals with the assumption $P\conj Q$ instantiates the unknowns to yield  lcp@105  1165 $R \quad [\, \List{P;Q}\Imp R, P\conj Q \,].$  lcp@105  1166 The proof may use the meta-assumptions in any order, and as often as  lcp@105  1167 necessary; when finished, we discharge them in the correct order to  lcp@105  1168 obtain the desired form:  lcp@105  1169 $\List{P\conj Q;\; \List{P;Q}\Imp R} \Imp R$  lcp@105  1170 We have derived the rule using free variables, which prevents their  lcp@105  1171 premature instantiation during the proof; we may now replace them by  lcp@105  1172 schematic variables.  lcp@105  1173 lcp@105  1174 \begin{warn}  lcp@331  1175  Schematic variables are not allowed in meta-assumptions, for a variety of  lcp@331  1176  reasons. Meta-assumptions remain fixed throughout a proof.  lcp@105  1177 \end{warn}  lcp@105  1178`