lcp@105: %% $Id$ lcp@284: \part{Advanced Methods} lcp@105: Before continuing, it might be wise to try some of your own examples in lcp@105: Isabelle, reinforcing your knowledge of the basic functions. lcp@105: wenzelm@3103: Look through {\em Isabelle's Object-Logics\/} and try proving some wenzelm@3103: simple theorems. You probably should begin with first-order logic wenzelm@3103: ({\tt FOL} or~{\tt LK}). Try working some of the examples provided, wenzelm@3103: and others from the literature. Set theory~({\tt ZF}) and wenzelm@3103: Constructive Type Theory~({\tt CTT}) form a richer world for wenzelm@3103: mathematical reasoning and, again, many examples are in the wenzelm@3103: literature. Higher-order logic~({\tt HOL}) is Isabelle's most paulson@3485: elaborate logic. Its types and functions are identified with those of wenzelm@3103: the meta-logic. lcp@105: lcp@105: Choose a logic that you already understand. Isabelle is a proof lcp@105: tool, not a teaching tool; if you do not know how to do a particular proof lcp@105: on paper, then you certainly will not be able to do it on the machine. lcp@105: Even experienced users plan large proofs on paper. lcp@105: lcp@105: We have covered only the bare essentials of Isabelle, but enough to perform lcp@105: substantial proofs. By occasionally dipping into the {\em Reference lcp@105: Manual}, you can learn additional tactics, subgoal commands and tacticals. lcp@105: lcp@105: lcp@105: \section{Deriving rules in Isabelle} lcp@105: \index{rules!derived} lcp@105: A mathematical development goes through a progression of stages. Each lcp@105: stage defines some concepts and derives rules about them. We shall see how lcp@105: to derive rules, perhaps involving definitions, using Isabelle. The lcp@310: following section will explain how to declare types, constants, rules and lcp@105: definitions. lcp@105: lcp@105: lcp@296: \subsection{Deriving a rule using tactics and meta-level assumptions} lcp@296: \label{deriving-example} lcp@310: \index{examples!of deriving rules}\index{assumptions!of main goal} lcp@296: lcp@307: The subgoal module supports the derivation of rules, as discussed in wenzelm@3103: \S\ref{deriving}. The \ttindex{goal} command, when supplied a goal of wenzelm@3103: the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates wenzelm@3103: $\phi\Imp\phi$ as the initial proof state and returns a list wenzelm@3103: consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$, wenzelm@3103: \ldots,~$k$. These meta-assumptions are also recorded internally, wenzelm@3103: allowing {\tt result} (which is called by {\tt qed}) to discharge them lcp@307: in the original order. lcp@105: lcp@307: Let us derive $\conj$ elimination using Isabelle. lcp@310: Until now, calling {\tt goal} has returned an empty list, which we have lcp@105: thrown away. In this example, the list contains the two premises of the lcp@105: rule. We bind them to the \ML\ identifiers {\tt major} and {\tt lcp@105: minor}:\footnote{Some ML compilers will print a message such as {\em lcp@105: binding not exhaustive}. This warns that {\tt goal} must return a lcp@105: 2-element list. Otherwise, the pattern-match will fail; ML will lcp@310: raise exception \xdx{Match}.} lcp@105: \begin{ttbox} lcp@105: val [major,minor] = goal FOL.thy lcp@105: "[| P&Q; [| P; Q |] ==> R |] ==> R"; lcp@105: {\out Level 0} lcp@105: {\out R} lcp@105: {\out 1. R} lcp@105: {\out val major = "P & Q [P & Q]" : thm} lcp@105: {\out val minor = "[| P; Q |] ==> R [[| P; Q |] ==> R]" : thm} lcp@105: \end{ttbox} lcp@105: Look at the minor premise, recalling that meta-level assumptions are lcp@105: shown in brackets. Using {\tt minor}, we reduce $R$ to the subgoals lcp@105: $P$ and~$Q$: lcp@105: \begin{ttbox} lcp@105: by (resolve_tac [minor] 1); lcp@105: {\out Level 1} lcp@105: {\out R} lcp@105: {\out 1. P} lcp@105: {\out 2. Q} lcp@105: \end{ttbox} lcp@105: Deviating from~\S\ref{deriving}, we apply $({\conj}E1)$ forwards from the lcp@105: assumption $P\conj Q$ to obtain the theorem~$P\;[P\conj Q]$. lcp@105: \begin{ttbox} lcp@105: major RS conjunct1; lcp@105: {\out val it = "P [P & Q]" : thm} lcp@105: \ttbreak lcp@105: by (resolve_tac [major RS conjunct1] 1); lcp@105: {\out Level 2} lcp@105: {\out R} lcp@105: {\out 1. Q} lcp@105: \end{ttbox} lcp@105: Similarly, we solve the subgoal involving~$Q$. lcp@105: \begin{ttbox} lcp@105: major RS conjunct2; lcp@105: {\out val it = "Q [P & Q]" : thm} lcp@105: by (resolve_tac [major RS conjunct2] 1); lcp@105: {\out Level 3} lcp@105: {\out R} lcp@105: {\out No subgoals!} lcp@105: \end{ttbox} lcp@105: Calling \ttindex{topthm} returns the current proof state as a theorem. wenzelm@3103: Note that it contains assumptions. Calling \ttindex{qed} discharges wenzelm@3103: the assumptions --- both occurrences of $P\conj Q$ are discharged as wenzelm@3103: one --- and makes the variables schematic. lcp@105: \begin{ttbox} lcp@105: topthm(); lcp@105: {\out val it = "R [P & Q, P & Q, [| P; Q |] ==> R]" : thm} wenzelm@3103: qed "conjE"; lcp@105: {\out val conjE = "[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R" : thm} lcp@105: \end{ttbox} lcp@105: lcp@105: lcp@105: \subsection{Definitions and derived rules} \label{definitions} lcp@310: \index{rules!derived}\index{definitions!and derived rules|(} lcp@310: lcp@105: Definitions are expressed as meta-level equalities. Let us define negation lcp@105: and the if-and-only-if connective: lcp@105: \begin{eqnarray*} lcp@105: \neg \Var{P} & \equiv & \Var{P}\imp\bot \\ lcp@105: \Var{P}\bimp \Var{Q} & \equiv & lcp@105: (\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P}) lcp@105: \end{eqnarray*} lcp@331: \index{meta-rewriting}% lcp@105: Isabelle permits {\bf meta-level rewriting} using definitions such as lcp@105: these. {\bf Unfolding} replaces every instance lcp@331: of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$. For lcp@105: example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to lcp@105: \[ \forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot. \] lcp@105: {\bf Folding} a definition replaces occurrences of the right-hand side by lcp@105: the left. The occurrences need not be free in the entire formula. lcp@105: lcp@105: When you define new concepts, you should derive rules asserting their lcp@105: abstract properties, and then forget their definitions. This supports lcp@331: modularity: if you later change the definitions without affecting their lcp@105: abstract properties, then most of your proofs will carry through without lcp@105: change. Indiscriminate unfolding makes a subgoal grow exponentially, lcp@105: becoming unreadable. lcp@105: lcp@105: Taking this point of view, Isabelle does not unfold definitions lcp@105: automatically during proofs. Rewriting must be explicit and selective. lcp@105: Isabelle provides tactics and meta-rules for rewriting, and a version of lcp@105: the {\tt goal} command that unfolds the conclusion and premises of the rule lcp@105: being derived. lcp@105: lcp@105: For example, the intuitionistic definition of negation given above may seem lcp@105: peculiar. Using Isabelle, we shall derive pleasanter negation rules: lcp@105: \[ \infer[({\neg}I)]{\neg P}{\infer*{\bot}{[P]}} \qquad lcp@105: \infer[({\neg}E)]{Q}{\neg P & P} \] lcp@296: This requires proving the following meta-formulae: wenzelm@3103: $$ (P\Imp\bot) \Imp \neg P \eqno(\neg I) $$ wenzelm@3103: $$ \List{\neg P; P} \Imp Q. \eqno(\neg E) $$ lcp@105: lcp@105: lcp@296: \subsection{Deriving the $\neg$ introduction rule} lcp@310: To derive $(\neg I)$, we may call {\tt goal} with the appropriate lcp@105: formula. Again, {\tt goal} returns a list consisting of the rule's lcp@296: premises. We bind this one-element list to the \ML\ identifier {\tt lcp@296: prems}. lcp@105: \begin{ttbox} lcp@105: val prems = goal FOL.thy "(P ==> False) ==> ~P"; lcp@105: {\out Level 0} lcp@105: {\out ~P} lcp@105: {\out 1. ~P} lcp@105: {\out val prems = ["P ==> False [P ==> False]"] : thm list} lcp@105: \end{ttbox} lcp@310: Calling \ttindex{rewrite_goals_tac} with \tdx{not_def}, which is the lcp@105: definition of negation, unfolds that definition in the subgoals. It leaves lcp@105: the main goal alone. lcp@105: \begin{ttbox} lcp@105: not_def; lcp@105: {\out val it = "~?P == ?P --> False" : thm} lcp@105: by (rewrite_goals_tac [not_def]); lcp@105: {\out Level 1} lcp@105: {\out ~P} lcp@105: {\out 1. P --> False} lcp@105: \end{ttbox} lcp@310: Using \tdx{impI} and the premise, we reduce subgoal~1 to a triviality: lcp@105: \begin{ttbox} lcp@105: by (resolve_tac [impI] 1); lcp@105: {\out Level 2} lcp@105: {\out ~P} lcp@105: {\out 1. P ==> False} lcp@105: \ttbreak lcp@105: by (resolve_tac prems 1); lcp@105: {\out Level 3} lcp@105: {\out ~P} lcp@105: {\out 1. P ==> P} lcp@105: \end{ttbox} lcp@296: The rest of the proof is routine. Note the form of the final result. lcp@105: \begin{ttbox} lcp@105: by (assume_tac 1); lcp@105: {\out Level 4} lcp@105: {\out ~P} lcp@105: {\out No subgoals!} lcp@296: \ttbreak wenzelm@3103: qed "notI"; lcp@105: {\out val notI = "(?P ==> False) ==> ~?P" : thm} lcp@105: \end{ttbox} lcp@310: \indexbold{*notI theorem} lcp@105: lcp@105: There is a simpler way of conducting this proof. The \ttindex{goalw} lcp@310: command starts a backward proof, as does {\tt goal}, but it also lcp@296: unfolds definitions. Thus there is no need to call lcp@296: \ttindex{rewrite_goals_tac}: lcp@105: \begin{ttbox} lcp@105: val prems = goalw FOL.thy [not_def] lcp@105: "(P ==> False) ==> ~P"; lcp@105: {\out Level 0} lcp@105: {\out ~P} lcp@105: {\out 1. P --> False} lcp@105: {\out val prems = ["P ==> False [P ==> False]"] : thm list} lcp@105: \end{ttbox} lcp@105: lcp@105: lcp@296: \subsection{Deriving the $\neg$ elimination rule} lcp@284: Let us derive the rule $(\neg E)$. The proof follows that of~{\tt conjE} lcp@296: above, with an additional step to unfold negation in the major premise. lcp@296: Although the {\tt goalw} command is best for this, let us lcp@310: try~{\tt goal} to see another way of unfolding definitions. After lcp@310: binding the premises to \ML\ identifiers, we apply \tdx{FalseE}: lcp@105: \begin{ttbox} lcp@105: val [major,minor] = goal FOL.thy "[| ~P; P |] ==> R"; lcp@105: {\out Level 0} lcp@105: {\out R} lcp@105: {\out 1. R} lcp@105: {\out val major = "~ P [~ P]" : thm} lcp@105: {\out val minor = "P [P]" : thm} lcp@105: \ttbreak lcp@105: by (resolve_tac [FalseE] 1); lcp@105: {\out Level 1} lcp@105: {\out R} lcp@105: {\out 1. False} lcp@284: \end{ttbox} lcp@284: Everything follows from falsity. And we can prove falsity using the lcp@284: premises and Modus Ponens: lcp@284: \begin{ttbox} lcp@105: by (resolve_tac [mp] 1); lcp@105: {\out Level 2} lcp@105: {\out R} lcp@105: {\out 1. ?P1 --> False} lcp@105: {\out 2. ?P1} lcp@105: \end{ttbox} lcp@105: For subgoal~1, we transform the major premise from~$\neg P$ lcp@105: to~${P\imp\bot}$. The function \ttindex{rewrite_rule}, given a list of lcp@296: definitions, unfolds them in a theorem. Rewriting does not lcp@105: affect the theorem's hypothesis, which remains~$\neg P$: lcp@105: \begin{ttbox} lcp@105: rewrite_rule [not_def] major; lcp@105: {\out val it = "P --> False [~P]" : thm} lcp@105: by (resolve_tac [it] 1); lcp@105: {\out Level 3} lcp@105: {\out R} lcp@105: {\out 1. P} lcp@105: \end{ttbox} lcp@296: The subgoal {\tt?P1} has been instantiated to~{\tt P}, which we can prove lcp@284: using the minor premise: lcp@105: \begin{ttbox} lcp@105: by (resolve_tac [minor] 1); lcp@105: {\out Level 4} lcp@105: {\out R} lcp@105: {\out No subgoals!} wenzelm@3103: qed "notE"; lcp@105: {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm} lcp@105: \end{ttbox} lcp@310: \indexbold{*notE theorem} lcp@105: lcp@105: \medskip lcp@284: Again, there is a simpler way of conducting this proof. Recall that lcp@284: the \ttindex{goalw} command unfolds definitions the conclusion; it also lcp@284: unfolds definitions in the premises: lcp@105: \begin{ttbox} lcp@105: val [major,minor] = goalw FOL.thy [not_def] lcp@105: "[| ~P; P |] ==> R"; lcp@105: {\out val major = "P --> False [~ P]" : thm} lcp@105: {\out val minor = "P [P]" : thm} lcp@105: \end{ttbox} lcp@296: Observe the difference in {\tt major}; the premises are unfolded without lcp@296: calling~\ttindex{rewrite_rule}. Incidentally, the four calls to lcp@296: \ttindex{resolve_tac} above can be collapsed to one, with the help lcp@284: of~\ttindex{RS}; this is a typical example of forward reasoning from a lcp@284: complex premise. lcp@105: \begin{ttbox} lcp@105: minor RS (major RS mp RS FalseE); lcp@105: {\out val it = "?P [P, ~P]" : thm} lcp@105: by (resolve_tac [it] 1); lcp@105: {\out Level 1} lcp@105: {\out R} lcp@105: {\out No subgoals!} lcp@105: \end{ttbox} lcp@310: \index{definitions!and derived rules|)} lcp@105: lcp@310: \goodbreak\medskip\index{*"!"! symbol!in main goal} lcp@284: Finally, here is a trick that is sometimes useful. If the goal lcp@105: has an outermost meta-quantifier, then \ttindex{goal} and \ttindex{goalw} lcp@284: do not return the rule's premises in the list of theorems; instead, the lcp@284: premises become assumptions in subgoal~1. lcp@284: %%%It does not matter which variables are quantified over. lcp@105: \begin{ttbox} lcp@105: goalw FOL.thy [not_def] "!!P R. [| ~P; P |] ==> R"; lcp@105: {\out Level 0} lcp@105: {\out !!P R. [| ~ P; P |] ==> R} lcp@105: {\out 1. !!P R. [| P --> False; P |] ==> R} lcp@105: val it = [] : thm list lcp@105: \end{ttbox} lcp@105: The proof continues as before. But instead of referring to \ML\ lcp@310: identifiers, we refer to assumptions using {\tt eresolve_tac} or lcp@310: {\tt assume_tac}: lcp@105: \begin{ttbox} lcp@105: by (resolve_tac [FalseE] 1); lcp@105: {\out Level 1} lcp@105: {\out !!P R. [| ~ P; P |] ==> R} lcp@105: {\out 1. !!P R. [| P --> False; P |] ==> False} lcp@105: \ttbreak lcp@105: by (eresolve_tac [mp] 1); lcp@105: {\out Level 2} lcp@105: {\out !!P R. [| ~ P; P |] ==> R} lcp@105: {\out 1. !!P R. P ==> P} lcp@105: \ttbreak lcp@105: by (assume_tac 1); lcp@105: {\out Level 3} lcp@105: {\out !!P R. [| ~ P; P |] ==> R} lcp@105: {\out No subgoals!} lcp@105: \end{ttbox} wenzelm@3103: Calling \ttindex{qed} strips the meta-quantifiers, so the resulting lcp@105: theorem is the same as before. lcp@105: \begin{ttbox} wenzelm@3103: qed "notE"; lcp@105: {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm} lcp@105: \end{ttbox} lcp@105: Do not use the {\tt!!}\ trick if the premises contain meta-level lcp@105: connectives, because \ttindex{eresolve_tac} and \ttindex{assume_tac} would lcp@105: not be able to handle the resulting assumptions. The trick is not suitable lcp@105: for deriving the introduction rule~$(\neg I)$. lcp@105: lcp@105: lcp@284: \section{Defining theories}\label{sec:defining-theories} lcp@105: \index{theories!defining|(} lcp@310: wenzelm@3103: Isabelle makes no distinction between simple extensions of a logic --- wenzelm@3103: like specifying a type~$bool$ with constants~$true$ and~$false$ --- wenzelm@3103: and defining an entire logic. A theory definition has a form like lcp@105: \begin{ttbox} lcp@105: \(T\) = \(S@1\) + \(\cdots\) + \(S@n\) + lcp@105: classes {\it class declarations} lcp@105: default {\it sort} lcp@331: types {\it type declarations and synonyms} wenzelm@3103: arities {\it type arity declarations} lcp@105: consts {\it constant declarations} wenzelm@3103: syntax {\it syntactic constant declarations} wenzelm@3103: translations {\it ast translation rules} wenzelm@3103: defs {\it meta-logical definitions} lcp@105: rules {\it rule declarations} lcp@105: end lcp@105: ML {\it ML code} lcp@105: \end{ttbox} lcp@105: This declares the theory $T$ to extend the existing theories wenzelm@3103: $S@1$,~\ldots,~$S@n$. It may introduce new classes, types, arities wenzelm@3103: (of existing types), constants and rules; it can specify the default wenzelm@3103: sort for type variables. A constant declaration can specify an wenzelm@3103: associated concrete syntax. The translations section specifies wenzelm@3103: rewrite rules on abstract syntax trees, handling notations and wenzelm@3103: abbreviations. \index{*ML section} The {\tt ML} section may contain wenzelm@3103: code to perform arbitrary syntactic transformations. The main wenzelm@3212: declaration forms are discussed below. There are some more sections wenzelm@3212: not presented here, the full syntax can be found in wenzelm@3212: \iflabelundefined{app:TheorySyntax}{an appendix of the {\it Reference wenzelm@3212: Manual}}{App.\ts\ref{app:TheorySyntax}}. Also note that wenzelm@3212: object-logics may add further theory sections, for example wenzelm@3212: \texttt{typedef}, \texttt{datatype} in \HOL. lcp@105: wenzelm@3103: All the declaration parts can be omitted or repeated and may appear in wenzelm@3103: any order, except that the {\ML} section must be last (after the {\tt wenzelm@3103: end} keyword). In the simplest case, $T$ is just the union of wenzelm@3103: $S@1$,~\ldots,~$S@n$. New theories always extend one or more other wenzelm@3103: theories, inheriting their types, constants, syntax, etc. The theory paulson@3485: \thydx{Pure} contains nothing but Isabelle's meta-logic. The variant wenzelm@3103: \thydx{CPure} offers the more usual higher-order function application wenzelm@3106: syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in \Pure. lcp@105: wenzelm@3103: Each theory definition must reside in a separate file, whose name is wenzelm@3103: the theory's with {\tt.thy} appended. Calling wenzelm@3103: \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads the definition from {\it wenzelm@3103: T}{\tt.thy}, writes a corresponding file of {\ML} code {\tt.{\it wenzelm@3103: T}.thy.ML}, reads the latter file, and deletes it if no errors wenzelm@3103: occurred. This declares the {\ML} structure~$T$, which contains a wenzelm@3103: component {\tt thy} denoting the new theory, a component for each wenzelm@3103: rule, and everything declared in {\it ML code}. lcp@105: wenzelm@3103: Errors may arise during the translation to {\ML} (say, a misspelled wenzelm@3103: keyword) or during creation of the new theory (say, a type error in a wenzelm@3103: rule). But if all goes well, {\tt use_thy} will finally read the file wenzelm@3103: {\it T}{\tt.ML} (if it exists). This file typically contains proofs paulson@3485: that refer to the components of~$T$. The structure is automatically wenzelm@3103: opened, so its components may be referred to by unqualified names, wenzelm@3103: e.g.\ just {\tt thy} instead of $T${\tt .thy}. lcp@105: wenzelm@3103: \ttindexbold{use_thy} automatically loads a theory's parents before wenzelm@3103: loading the theory itself. When a theory file is modified, many wenzelm@3103: theories may have to be reloaded. Isabelle records the modification wenzelm@3103: times and dependencies of theory files. See lcp@331: \iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}% lcp@331: {\S\ref{sec:reloading-theories}} lcp@296: for more details. lcp@296: lcp@105: lcp@1084: \subsection{Declaring constants, definitions and rules} lcp@310: \indexbold{constants!declaring}\index{rules!declaring} lcp@310: lcp@1084: Most theories simply declare constants, definitions and rules. The {\bf lcp@1084: constant declaration part} has the form lcp@105: \begin{ttbox} clasohm@1387: consts \(c@1\) :: \(\tau@1\) lcp@105: \vdots clasohm@1387: \(c@n\) :: \(\tau@n\) lcp@105: \end{ttbox} lcp@105: where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are clasohm@1387: types. The types must be enclosed in quotation marks if they contain clasohm@1387: user-declared infix type constructors like {\tt *}. Each lcp@105: constant must be enclosed in quotation marks unless it is a valid lcp@105: identifier. To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$, lcp@105: the $n$ declarations may be abbreviated to a single line: lcp@105: \begin{ttbox} clasohm@1387: \(c@1\), \ldots, \(c@n\) :: \(\tau\) lcp@105: \end{ttbox} lcp@105: The {\bf rule declaration part} has the form lcp@105: \begin{ttbox} lcp@105: rules \(id@1\) "\(rule@1\)" lcp@105: \vdots lcp@105: \(id@n\) "\(rule@n\)" lcp@105: \end{ttbox} lcp@105: where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots, lcp@284: $rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be lcp@284: enclosed in quotation marks. lcp@284: wenzelm@3103: \indexbold{definitions} The {\bf definition part} is similar, but with wenzelm@3103: the keyword {\tt defs} instead of {\tt rules}. {\bf Definitions} are wenzelm@3103: rules of the form $s \equiv t$, and should serve only as paulson@3485: abbreviations. The simplest form of a definition is $f \equiv t$, paulson@3485: where $f$ is a constant. Also allowed are $\eta$-equivalent forms of wenzelm@3106: this, where the arguments of~$f$ appear applied on the left-hand side wenzelm@3106: of the equation instead of abstracted on the right-hand side. lcp@1084: wenzelm@3103: Isabelle checks for common errors in definitions, such as extra wenzelm@3103: variables on the right-hand side, but currently does not a complete paulson@3485: test of well-formedness. Thus determined users can write wenzelm@3103: non-conservative `definitions' by using mutual recursion, for example; wenzelm@3103: the consequences of such actions are their responsibility. wenzelm@3103: wenzelm@3103: \index{examples!of theories} This example theory extends first-order wenzelm@3103: logic by declaring and defining two constants, {\em nand} and {\em wenzelm@3103: xor}: lcp@284: \begin{ttbox} lcp@105: Gate = FOL + clasohm@1387: consts nand,xor :: [o,o] => o lcp@1084: defs nand_def "nand(P,Q) == ~(P & Q)" lcp@105: xor_def "xor(P,Q) == P & ~Q | ~P & Q" lcp@105: end lcp@105: \end{ttbox} lcp@105: nipkow@1649: Declaring and defining constants can be combined: nipkow@1649: \begin{ttbox} nipkow@1649: Gate = FOL + nipkow@1649: constdefs nand :: [o,o] => o nipkow@1649: "nand(P,Q) == ~(P & Q)" nipkow@1649: xor :: [o,o] => o nipkow@1649: "xor(P,Q) == P & ~Q | ~P & Q" nipkow@1649: end nipkow@1649: \end{ttbox} nipkow@1649: {\tt constdefs} generates the names {\tt nand_def} and {\tt xor_def} paulson@3485: automatically, which is why it is restricted to alphanumeric identifiers. In nipkow@1649: general it has the form nipkow@1649: \begin{ttbox} nipkow@1649: constdefs \(id@1\) :: \(\tau@1\) nipkow@1649: "\(id@1 \equiv \dots\)" nipkow@1649: \vdots nipkow@1649: \(id@n\) :: \(\tau@n\) nipkow@1649: "\(id@n \equiv \dots\)" nipkow@1649: \end{ttbox} nipkow@1649: nipkow@1649: nipkow@1366: \begin{warn} nipkow@1366: A common mistake when writing definitions is to introduce extra free variables nipkow@1468: on the right-hand side as in the following fictitious definition: nipkow@1366: \begin{ttbox} nipkow@1366: defs prime_def "prime(p) == (m divides p) --> (m=1 | m=p)" nipkow@1366: \end{ttbox} nipkow@1366: Isabelle rejects this ``definition'' because of the extra {\tt m} on the paulson@3485: right-hand side, which would introduce an inconsistency. What you should have nipkow@1366: written is nipkow@1366: \begin{ttbox} nipkow@1366: defs prime_def "prime(p) == ALL m. (m divides p) --> (m=1 | m=p)" nipkow@1366: \end{ttbox} nipkow@1366: \end{warn} lcp@105: lcp@105: \subsection{Declaring type constructors} nipkow@303: \indexbold{types!declaring}\indexbold{arities!declaring} lcp@284: % lcp@105: Types are composed of type variables and {\bf type constructors}. Each lcp@284: type constructor takes a fixed number of arguments. They are declared lcp@284: with an \ML-like syntax. If $list$ takes one type argument, $tree$ takes lcp@284: two arguments and $nat$ takes no arguments, then these type constructors lcp@284: can be declared by lcp@284: \begin{ttbox} lcp@284: types 'a list lcp@284: ('a,'b) tree lcp@284: nat lcp@284: \end{ttbox} lcp@105: lcp@284: The {\bf type declaration part} has the general form lcp@105: \begin{ttbox} lcp@284: types \(tids@1\) \(id@1\) lcp@105: \vdots wenzelm@841: \(tids@n\) \(id@n\) lcp@105: \end{ttbox} lcp@284: where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$ lcp@284: are type argument lists as shown in the example above. It declares each lcp@284: $id@i$ as a type constructor with the specified number of argument places. lcp@105: lcp@105: The {\bf arity declaration part} has the form lcp@105: \begin{ttbox} lcp@105: arities \(tycon@1\) :: \(arity@1\) lcp@105: \vdots lcp@105: \(tycon@n\) :: \(arity@n\) lcp@105: \end{ttbox} lcp@105: where $tycon@1$, \ldots, $tycon@n$ are identifiers and $arity@1$, \ldots, lcp@105: $arity@n$ are arities. Arity declarations add arities to existing lcp@296: types; they do not declare the types themselves. lcp@105: In the simplest case, for an 0-place type constructor, an arity is simply lcp@105: the type's class. Let us declare a type~$bool$ of class $term$, with lcp@284: constants $tt$ and~$ff$. (In first-order logic, booleans are lcp@284: distinct from formulae, which have type $o::logic$.) lcp@105: \index{examples!of theories} lcp@284: \begin{ttbox} lcp@105: Bool = FOL + lcp@284: types bool lcp@105: arities bool :: term clasohm@1387: consts tt,ff :: bool lcp@105: end lcp@105: \end{ttbox} lcp@296: A $k$-place type constructor may have arities of the form lcp@296: $(s@1,\ldots,s@k)c$, where $s@1,\ldots,s@n$ are sorts and $c$ is a class. lcp@296: Each sort specifies a type argument; it has the form $\{c@1,\ldots,c@m\}$, lcp@296: where $c@1$, \dots,~$c@m$ are classes. Mostly we deal with singleton lcp@296: sorts, and may abbreviate them by dropping the braces. The arity lcp@296: $(term)term$ is short for $(\{term\})term$. Recall the discussion in lcp@296: \S\ref{polymorphic}. lcp@105: lcp@105: A type constructor may be overloaded (subject to certain conditions) by lcp@296: appearing in several arity declarations. For instance, the function type lcp@331: constructor~$fun$ has the arity $(logic,logic)logic$; in higher-order lcp@105: logic, it is declared also to have arity $(term,term)term$. lcp@105: lcp@105: Theory {\tt List} declares the 1-place type constructor $list$, gives lcp@284: it arity $(term)term$, and declares constants $Nil$ and $Cons$ with lcp@296: polymorphic types:% lcp@296: \footnote{In the {\tt consts} part, type variable {\tt'a} has the default lcp@296: sort, which is {\tt term}. See the {\em Reference Manual\/} lcp@296: \iflabelundefined{sec:ref-defining-theories}{}% lcp@296: {(\S\ref{sec:ref-defining-theories})} for more information.} lcp@105: \index{examples!of theories} lcp@284: \begin{ttbox} lcp@105: List = FOL + lcp@284: types 'a list lcp@105: arities list :: (term)term clasohm@1387: consts Nil :: 'a list clasohm@1387: Cons :: ['a, 'a list] => 'a list lcp@105: end lcp@105: \end{ttbox} lcp@284: Multiple arity declarations may be abbreviated to a single line: lcp@105: \begin{ttbox} lcp@105: arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\) lcp@105: \end{ttbox} lcp@105: wenzelm@3103: %\begin{warn} wenzelm@3103: %Arity declarations resemble constant declarations, but there are {\it no\/} wenzelm@3103: %quotation marks! Types and rules must be quoted because the theory wenzelm@3103: %translator passes them verbatim to the {\ML} output file. wenzelm@3103: %\end{warn} lcp@105: lcp@331: \subsection{Type synonyms}\indexbold{type synonyms} nipkow@303: Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar lcp@307: to those found in \ML. Such synonyms are defined in the type declaration part nipkow@303: and are fairly self explanatory: nipkow@303: \begin{ttbox} clasohm@1387: types gate = [o,o] => o clasohm@1387: 'a pred = 'a => o clasohm@1387: ('a,'b)nuf = 'b => 'a nipkow@303: \end{ttbox} nipkow@303: Type declarations and synonyms can be mixed arbitrarily: nipkow@303: \begin{ttbox} nipkow@303: types nat clasohm@1387: 'a stream = nat => 'a clasohm@1387: signal = nat stream nipkow@303: 'a list nipkow@303: \end{ttbox} wenzelm@3103: A synonym is merely an abbreviation for some existing type expression. wenzelm@3103: Hence synonyms may not be recursive! Internally all synonyms are wenzelm@3103: fully expanded. As a consequence Isabelle output never contains wenzelm@3103: synonyms. Their main purpose is to improve the readability of theory wenzelm@3103: definitions. Synonyms can be used just like any other type: nipkow@303: \begin{ttbox} clasohm@1387: consts and,or :: gate clasohm@1387: negate :: signal => signal nipkow@303: \end{ttbox} nipkow@303: lcp@348: \subsection{Infix and mixfix operators} lcp@310: \index{infixes}\index{examples!of theories} lcp@310: lcp@310: Infix or mixfix syntax may be attached to constants. Consider the lcp@310: following theory: lcp@284: \begin{ttbox} lcp@105: Gate2 = FOL + clasohm@1387: consts "~&" :: [o,o] => o (infixl 35) clasohm@1387: "#" :: [o,o] => o (infixl 30) lcp@1084: defs nand_def "P ~& Q == ~(P & Q)" lcp@105: xor_def "P # Q == P & ~Q | ~P & Q" lcp@105: end lcp@105: \end{ttbox} lcp@310: The constant declaration part declares two left-associating infix operators lcp@310: with their priorities, or precedences; they are $\nand$ of priority~35 and lcp@310: $\xor$ of priority~30. Hence $P \xor Q \xor R$ is parsed as $(P\xor Q) lcp@310: \xor R$ and $P \xor Q \nand R$ as $P \xor (Q \nand R)$. Note the quotation lcp@310: marks in \verb|"~&"| and \verb|"#"|. lcp@105: lcp@105: The constants \hbox{\verb|op ~&|} and \hbox{\verb|op #|} are declared lcp@105: automatically, just as in \ML. Hence you may write propositions like lcp@105: \verb|op #(True) == op ~&(True)|, which asserts that the functions $\lambda lcp@105: Q.True \xor Q$ and $\lambda Q.True \nand Q$ are identical. lcp@105: wenzelm@3212: \medskip Infix syntax and constant names may be also specified paulson@3485: independently. For example, consider this version of $\nand$: wenzelm@3212: \begin{ttbox} wenzelm@3212: consts nand :: [o,o] => o (infixl "~&" 35) wenzelm@3212: \end{ttbox} wenzelm@3212: lcp@310: \bigskip\index{mixfix declarations} lcp@310: {\bf Mixfix} operators may have arbitrary context-free syntaxes. Let us lcp@310: add a line to the constant declaration part: lcp@284: \begin{ttbox} clasohm@1387: If :: [o,o,o] => o ("if _ then _ else _") lcp@105: \end{ttbox} lcp@310: This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt lcp@296: if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}. Underscores lcp@310: denote argument positions. lcp@105: wenzelm@3103: The declaration above does not allow the {\tt if}-{\tt then}-{\tt wenzelm@3103: else} construct to be printed split across several lines, even if it wenzelm@3103: is too long to fit on one line. Pretty-printing information can be wenzelm@3103: added to specify the layout of mixfix operators. For details, see lcp@310: \iflabelundefined{Defining-Logics}% lcp@310: {the {\it Reference Manual}, chapter `Defining Logics'}% lcp@310: {Chap.\ts\ref{Defining-Logics}}. lcp@310: lcp@310: Mixfix declarations can be annotated with priorities, just like lcp@105: infixes. The example above is just a shorthand for lcp@284: \begin{ttbox} clasohm@1387: If :: [o,o,o] => o ("if _ then _ else _" [0,0,0] 1000) lcp@105: \end{ttbox} lcp@310: The numeric components determine priorities. The list of integers lcp@310: defines, for each argument position, the minimal priority an expression lcp@310: at that position must have. The final integer is the priority of the lcp@105: construct itself. In the example above, any argument expression is lcp@310: acceptable because priorities are non-negative, and conditionals may lcp@310: appear everywhere because 1000 is the highest priority. On the other lcp@310: hand, the declaration lcp@284: \begin{ttbox} clasohm@1387: If :: [o,o,o] => o ("if _ then _ else _" [100,0,0] 99) lcp@105: \end{ttbox} lcp@284: defines concrete syntax for a conditional whose first argument cannot have lcp@310: the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a priority lcp@310: of at least~100. We may of course write lcp@284: \begin{quote}\tt lcp@284: if (if $P$ then $Q$ else $R$) then $S$ else $T$ lcp@156: \end{quote} lcp@310: because expressions in parentheses have maximal priority. lcp@105: lcp@105: Binary type constructors, like products and sums, may also be declared as lcp@105: infixes. The type declaration below introduces a type constructor~$*$ with lcp@105: infix notation $\alpha*\beta$, together with the mixfix notation lcp@1084: ${<}\_,\_{>}$ for pairs. We also see a rule declaration part. lcp@310: \index{examples!of theories}\index{mixfix declarations} lcp@105: \begin{ttbox} lcp@105: Prod = FOL + lcp@284: types ('a,'b) "*" (infixl 20) lcp@105: arities "*" :: (term,term)term lcp@105: consts fst :: "'a * 'b => 'a" lcp@105: snd :: "'a * 'b => 'b" lcp@105: Pair :: "['a,'b] => 'a * 'b" ("(1<_,/_>)") lcp@105: rules fst "fst() = a" lcp@105: snd "snd() = b" lcp@105: end lcp@105: \end{ttbox} lcp@105: lcp@105: \begin{warn} wenzelm@3103: The name of the type constructor is~{\tt *} and not {\tt op~*}, as wenzelm@3103: it would be in the case of an infix constant. Only infix type wenzelm@3103: constructors can have symbolic names like~{\tt *}. General mixfix wenzelm@3103: syntax for types may be introduced via appropriate {\tt syntax} wenzelm@3103: declarations. lcp@105: \end{warn} lcp@105: lcp@105: lcp@105: \subsection{Overloading} lcp@105: \index{overloading}\index{examples!of theories} lcp@105: The {\bf class declaration part} has the form lcp@105: \begin{ttbox} lcp@105: classes \(id@1\) < \(c@1\) lcp@105: \vdots lcp@105: \(id@n\) < \(c@n\) lcp@105: \end{ttbox} lcp@105: where $id@1$, \ldots, $id@n$ are identifiers and $c@1$, \ldots, $c@n$ are lcp@105: existing classes. It declares each $id@i$ as a new class, a subclass lcp@105: of~$c@i$. In the general case, an identifier may be declared to be a lcp@105: subclass of $k$ existing classes: lcp@105: \begin{ttbox} lcp@105: \(id\) < \(c@1\), \ldots, \(c@k\) lcp@105: \end{ttbox} lcp@296: Type classes allow constants to be overloaded. As suggested in lcp@307: \S\ref{polymorphic}, let us define the class $arith$ of arithmetic lcp@296: types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::} lcp@296: \alpha$, for $\alpha{::}arith$. We introduce $arith$ as a subclass of lcp@296: $term$ and add the three polymorphic constants of this class. lcp@310: \index{examples!of theories}\index{constants!overloaded} lcp@105: \begin{ttbox} lcp@105: Arith = FOL + lcp@105: classes arith < term clasohm@1387: consts "0" :: 'a::arith ("0") clasohm@1387: "1" :: 'a::arith ("1") clasohm@1387: "+" :: ['a::arith,'a] => 'a (infixl 60) lcp@105: end lcp@105: \end{ttbox} lcp@105: No rules are declared for these constants: we merely introduce their lcp@105: names without specifying properties. On the other hand, classes lcp@105: with rules make it possible to prove {\bf generic} theorems. Such lcp@105: theorems hold for all instances, all types in that class. lcp@105: lcp@105: We can now obtain distinct versions of the constants of $arith$ by lcp@105: declaring certain types to be of class $arith$. For example, let us lcp@105: declare the 0-place type constructors $bool$ and $nat$: lcp@105: \index{examples!of theories} lcp@105: \begin{ttbox} lcp@105: BoolNat = Arith + lcp@348: types bool nat lcp@348: arities bool, nat :: arith clasohm@1387: consts Suc :: nat=>nat lcp@284: \ttbreak lcp@105: rules add0 "0 + n = n::nat" lcp@105: addS "Suc(m)+n = Suc(m+n)" lcp@105: nat1 "1 = Suc(0)" lcp@105: or0l "0 + x = x::bool" lcp@105: or0r "x + 0 = x::bool" lcp@105: or1l "1 + x = 1::bool" lcp@105: or1r "x + 1 = 1::bool" lcp@105: end lcp@105: \end{ttbox} lcp@105: Because $nat$ and $bool$ have class $arith$, we can use $0$, $1$ and $+$ at lcp@105: either type. The type constraints in the axioms are vital. Without lcp@105: constraints, the $x$ in $1+x = x$ would have type $\alpha{::}arith$ lcp@105: and the axiom would hold for any type of class $arith$. This would lcp@284: collapse $nat$ to a trivial type: lcp@105: \[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \] lcp@105: lcp@296: lcp@296: \section{Theory example: the natural numbers} lcp@296: lcp@296: We shall now work through a small example of formalized mathematics lcp@105: demonstrating many of the theory extension features. lcp@105: lcp@105: lcp@105: \subsection{Extending first-order logic with the natural numbers} lcp@105: \index{examples!of theories} lcp@105: lcp@284: Section\ts\ref{sec:logical-syntax} has formalized a first-order logic, lcp@284: including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$. lcp@284: Let us introduce the Peano axioms for mathematical induction and the lcp@310: freeness of $0$ and~$Suc$:\index{axioms!Peano} lcp@307: \[ \vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}} lcp@105: \qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$} lcp@105: \] lcp@105: \[ \infer[(Suc\_inject)]{m=n}{Suc(m)=Suc(n)} \qquad lcp@105: \infer[(Suc\_neq\_0)]{R}{Suc(m)=0} lcp@105: \] lcp@105: Mathematical induction asserts that $P(n)$ is true, for any $n::nat$, lcp@105: provided $P(0)$ holds and that $P(x)$ implies $P(Suc(x))$ for all~$x$. lcp@105: Some authors express the induction step as $\forall x. P(x)\imp P(Suc(x))$. lcp@105: To avoid making induction require the presence of other connectives, we lcp@105: formalize mathematical induction as lcp@105: $$ \List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n). \eqno(induct) $$ lcp@105: lcp@105: \noindent lcp@105: Similarly, to avoid expressing the other rules using~$\forall$, $\imp$ lcp@105: and~$\neg$, we take advantage of the meta-logic;\footnote lcp@105: {On the other hand, the axioms $Suc(m)=Suc(n) \bimp m=n$ lcp@105: and $\neg(Suc(m)=0)$ are logically equivalent to those given, and work lcp@105: better with Isabelle's simplifier.} lcp@105: $(Suc\_neq\_0)$ is lcp@105: an elimination rule for $Suc(m)=0$: lcp@105: $$ Suc(m)=Suc(n) \Imp m=n \eqno(Suc\_inject) $$ lcp@105: $$ Suc(m)=0 \Imp R \eqno(Suc\_neq\_0) $$ lcp@105: lcp@105: \noindent lcp@105: We shall also define a primitive recursion operator, $rec$. Traditionally, lcp@105: primitive recursion takes a natural number~$a$ and a 2-place function~$f$, lcp@105: and obeys the equations lcp@105: \begin{eqnarray*} lcp@105: rec(0,a,f) & = & a \\ lcp@105: rec(Suc(m),a,f) & = & f(m, rec(m,a,f)) lcp@105: \end{eqnarray*} lcp@105: Addition, defined by $m+n \equiv rec(m,n,\lambda x\,y.Suc(y))$, lcp@105: should satisfy lcp@105: \begin{eqnarray*} lcp@105: 0+n & = & n \\ lcp@105: Suc(m)+n & = & Suc(m+n) lcp@105: \end{eqnarray*} lcp@296: Primitive recursion appears to pose difficulties: first-order logic has no lcp@296: function-valued expressions. We again take advantage of the meta-logic, lcp@296: which does have functions. We also generalise primitive recursion to be lcp@105: polymorphic over any type of class~$term$, and declare the addition lcp@105: function: lcp@105: \begin{eqnarray*} lcp@105: rec & :: & [nat, \alpha{::}term, [nat,\alpha]\To\alpha] \To\alpha \\ lcp@105: + & :: & [nat,nat]\To nat lcp@105: \end{eqnarray*} lcp@105: lcp@105: lcp@105: \subsection{Declaring the theory to Isabelle} lcp@105: \index{examples!of theories} lcp@310: Let us create the theory \thydx{Nat} starting from theory~\verb$FOL$, lcp@105: which contains only classical logic with no natural numbers. We declare lcp@307: the 0-place type constructor $nat$ and the associated constants. Note that lcp@307: the constant~0 requires a mixfix annotation because~0 is not a legal lcp@307: identifier, and could not otherwise be written in terms: lcp@310: \begin{ttbox}\index{mixfix declarations} lcp@105: Nat = FOL + lcp@284: types nat lcp@105: arities nat :: term clasohm@1387: consts "0" :: nat ("0") clasohm@1387: Suc :: nat=>nat clasohm@1387: rec :: [nat, 'a, [nat,'a]=>'a] => 'a clasohm@1387: "+" :: [nat, nat] => nat (infixl 60) lcp@296: rules Suc_inject "Suc(m)=Suc(n) ==> m=n" lcp@105: Suc_neq_0 "Suc(m)=0 ==> R" lcp@296: induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)" lcp@105: rec_0 "rec(0,a,f) = a" lcp@105: rec_Suc "rec(Suc(m), a, f) = f(m, rec(m,a,f))" lcp@296: add_def "m+n == rec(m, n, \%x y. Suc(y))" lcp@105: end lcp@105: \end{ttbox} lcp@105: In axiom {\tt add_def}, recall that \verb|%| stands for~$\lambda$. lcp@296: Loading this theory file creates the \ML\ structure {\tt Nat}, which wenzelm@3103: contains the theory and axioms. lcp@296: lcp@296: \subsection{Proving some recursion equations} lcp@331: File {\tt FOL/ex/Nat.ML} contains proofs involving this theory of the lcp@105: natural numbers. As a trivial example, let us derive recursion equations lcp@105: for \verb$+$. Here is the zero case: lcp@284: \begin{ttbox} lcp@105: goalw Nat.thy [add_def] "0+n = n"; lcp@105: {\out Level 0} lcp@105: {\out 0 + n = n} lcp@284: {\out 1. rec(0,n,\%x y. Suc(y)) = n} lcp@105: \ttbreak lcp@105: by (resolve_tac [rec_0] 1); lcp@105: {\out Level 1} lcp@105: {\out 0 + n = n} lcp@105: {\out No subgoals!} wenzelm@3103: qed "add_0"; lcp@284: \end{ttbox} lcp@105: And here is the successor case: lcp@284: \begin{ttbox} lcp@105: goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)"; lcp@105: {\out Level 0} lcp@105: {\out Suc(m) + n = Suc(m + n)} lcp@284: {\out 1. rec(Suc(m),n,\%x y. Suc(y)) = Suc(rec(m,n,\%x y. Suc(y)))} lcp@105: \ttbreak lcp@105: by (resolve_tac [rec_Suc] 1); lcp@105: {\out Level 1} lcp@105: {\out Suc(m) + n = Suc(m + n)} lcp@105: {\out No subgoals!} wenzelm@3103: qed "add_Suc"; lcp@284: \end{ttbox} lcp@105: The induction rule raises some complications, which are discussed next. lcp@105: \index{theories!defining|)} lcp@105: lcp@105: lcp@105: \section{Refinement with explicit instantiation} lcp@310: \index{resolution!with instantiation} lcp@310: \index{instantiation|(} lcp@310: lcp@105: In order to employ mathematical induction, we need to refine a subgoal by lcp@105: the rule~$(induct)$. The conclusion of this rule is $\Var{P}(\Var{n})$, lcp@105: which is highly ambiguous in higher-order unification. It matches every lcp@105: way that a formula can be regarded as depending on a subterm of type~$nat$. lcp@105: To get round this problem, we could make the induction rule conclude lcp@105: $\forall n.\Var{P}(n)$ --- but putting a subgoal into this form requires lcp@105: refinement by~$(\forall E)$, which is equally hard! lcp@105: lcp@105: The tactic {\tt res_inst_tac}, like {\tt resolve_tac}, refines a subgoal by lcp@105: a rule. But it also accepts explicit instantiations for the rule's lcp@105: schematic variables. lcp@105: \begin{description} lcp@310: \item[\ttindex{res_inst_tac} {\it insts} {\it thm} {\it i}] lcp@105: instantiates the rule {\it thm} with the instantiations {\it insts}, and lcp@105: then performs resolution on subgoal~$i$. lcp@105: lcp@310: \item[\ttindex{eres_inst_tac}] lcp@310: and \ttindex{dres_inst_tac} are similar, but perform elim-resolution lcp@105: and destruct-resolution, respectively. lcp@105: \end{description} lcp@105: The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$, lcp@105: where $v@1$, \ldots, $v@n$ are names of schematic variables in the rule --- lcp@307: with no leading question marks! --- and $e@1$, \ldots, $e@n$ are lcp@105: expressions giving their instantiations. The expressions are type-checked lcp@105: in the context of a particular subgoal: free variables receive the same lcp@105: types as they have in the subgoal, and parameters may appear. Type lcp@105: variable instantiations may appear in~{\it insts}, but they are seldom lcp@105: required: {\tt res_inst_tac} instantiates type variables automatically lcp@105: whenever the type of~$e@i$ is an instance of the type of~$\Var{v@i}$. lcp@105: lcp@105: \subsection{A simple proof by induction} lcp@310: \index{examples!of induction} lcp@105: Let us prove that no natural number~$k$ equals its own successor. To lcp@105: use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good lcp@105: instantiation for~$\Var{P}$. lcp@284: \begin{ttbox} lcp@105: goal Nat.thy "~ (Suc(k) = k)"; lcp@105: {\out Level 0} lcp@459: {\out Suc(k) ~= k} lcp@459: {\out 1. Suc(k) ~= k} lcp@105: \ttbreak lcp@105: by (res_inst_tac [("n","k")] induct 1); lcp@105: {\out Level 1} lcp@459: {\out Suc(k) ~= k} lcp@459: {\out 1. Suc(0) ~= 0} lcp@459: {\out 2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)} lcp@284: \end{ttbox} lcp@105: We should check that Isabelle has correctly applied induction. Subgoal~1 lcp@105: is the base case, with $k$ replaced by~0. Subgoal~2 is the inductive step, lcp@105: with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$. lcp@310: The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the lcp@310: other rules of theory {\tt Nat}. The base case holds by~\ttindex{Suc_neq_0}: lcp@284: \begin{ttbox} lcp@105: by (resolve_tac [notI] 1); lcp@105: {\out Level 2} lcp@459: {\out Suc(k) ~= k} lcp@105: {\out 1. Suc(0) = 0 ==> False} lcp@459: {\out 2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)} lcp@105: \ttbreak lcp@105: by (eresolve_tac [Suc_neq_0] 1); lcp@105: {\out Level 3} lcp@459: {\out Suc(k) ~= k} lcp@459: {\out 1. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)} lcp@284: \end{ttbox} lcp@105: The inductive step holds by the contrapositive of~\ttindex{Suc_inject}. lcp@284: Negation rules transform the subgoal into that of proving $Suc(x)=x$ from lcp@284: $Suc(Suc(x)) = Suc(x)$: lcp@284: \begin{ttbox} lcp@105: by (resolve_tac [notI] 1); lcp@105: {\out Level 4} lcp@459: {\out Suc(k) ~= k} lcp@459: {\out 1. !!x. [| Suc(x) ~= x; Suc(Suc(x)) = Suc(x) |] ==> False} lcp@105: \ttbreak lcp@105: by (eresolve_tac [notE] 1); lcp@105: {\out Level 5} lcp@459: {\out Suc(k) ~= k} lcp@105: {\out 1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x} lcp@105: \ttbreak lcp@105: by (eresolve_tac [Suc_inject] 1); lcp@105: {\out Level 6} lcp@459: {\out Suc(k) ~= k} lcp@105: {\out No subgoals!} lcp@284: \end{ttbox} lcp@105: lcp@105: lcp@105: \subsection{An example of ambiguity in {\tt resolve_tac}} lcp@105: \index{examples!of induction}\index{unification!higher-order} lcp@105: If you try the example above, you may observe that {\tt res_inst_tac} is lcp@105: not actually needed. Almost by chance, \ttindex{resolve_tac} finds the right lcp@105: instantiation for~$(induct)$ to yield the desired next state. With more lcp@105: complex formulae, our luck fails. lcp@284: \begin{ttbox} lcp@105: goal Nat.thy "(k+m)+n = k+(m+n)"; lcp@105: {\out Level 0} lcp@105: {\out k + m + n = k + (m + n)} lcp@105: {\out 1. k + m + n = k + (m + n)} lcp@105: \ttbreak lcp@105: by (resolve_tac [induct] 1); lcp@105: {\out Level 1} lcp@105: {\out k + m + n = k + (m + n)} lcp@105: {\out 1. k + m + n = 0} lcp@105: {\out 2. !!x. k + m + n = x ==> k + m + n = Suc(x)} lcp@284: \end{ttbox} lcp@284: This proof requires induction on~$k$. The occurrence of~0 in subgoal~1 lcp@284: indicates that induction has been applied to the term~$k+(m+n)$; this lcp@284: application is sound but will not lead to a proof here. Fortunately, lcp@284: Isabelle can (lazily!) generate all the valid applications of induction. lcp@284: The \ttindex{back} command causes backtracking to an alternative outcome of lcp@284: the tactic. lcp@284: \begin{ttbox} lcp@105: back(); lcp@105: {\out Level 1} lcp@105: {\out k + m + n = k + (m + n)} lcp@105: {\out 1. k + m + n = k + 0} lcp@105: {\out 2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)} lcp@284: \end{ttbox} lcp@284: Now induction has been applied to~$m+n$. This is equally useless. Let us lcp@284: call \ttindex{back} again. lcp@284: \begin{ttbox} lcp@105: back(); lcp@105: {\out Level 1} lcp@105: {\out k + m + n = k + (m + n)} lcp@105: {\out 1. k + m + 0 = k + (m + 0)} lcp@284: {\out 2. !!x. k + m + x = k + (m + x) ==>} lcp@284: {\out k + m + Suc(x) = k + (m + Suc(x))} lcp@284: \end{ttbox} lcp@105: Now induction has been applied to~$n$. What is the next alternative? lcp@284: \begin{ttbox} lcp@105: back(); lcp@105: {\out Level 1} lcp@105: {\out k + m + n = k + (m + n)} lcp@105: {\out 1. k + m + n = k + (m + 0)} lcp@105: {\out 2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))} lcp@284: \end{ttbox} lcp@105: Inspecting subgoal~1 reveals that induction has been applied to just the lcp@105: second occurrence of~$n$. This perfectly legitimate induction is useless lcp@310: here. lcp@310: lcp@310: The main goal admits fourteen different applications of induction. The lcp@310: number is exponential in the size of the formula. lcp@105: lcp@105: \subsection{Proving that addition is associative} lcp@331: Let us invoke the induction rule properly, using~{\tt lcp@310: res_inst_tac}. At the same time, we shall have a glimpse at Isabelle's lcp@310: simplification tactics, which are described in lcp@310: \iflabelundefined{simp-chap}% lcp@310: {the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}. lcp@105: lcp@310: \index{simplification}\index{examples!of simplification} lcp@284: wenzelm@3114: Isabelle's simplification tactics repeatedly apply equations to a wenzelm@3114: subgoal, perhaps proving it. For efficiency, the rewrite rules must wenzelm@3114: be packaged into a {\bf simplification set},\index{simplification wenzelm@3114: sets} or {\bf simpset}. We augment the implicit simpset of {\FOL} wenzelm@3114: with the equations proved in the previous section, namely $0+n=n$ and wenzelm@3114: ${\tt Suc}(m)+n={\tt Suc}(m+n)$: lcp@284: \begin{ttbox} wenzelm@3114: Addsimps [add_0, add_Suc]; lcp@284: \end{ttbox} lcp@105: We state the goal for associativity of addition, and lcp@105: use \ttindex{res_inst_tac} to invoke induction on~$k$: lcp@284: \begin{ttbox} lcp@105: goal Nat.thy "(k+m)+n = k+(m+n)"; lcp@105: {\out Level 0} lcp@105: {\out k + m + n = k + (m + n)} lcp@105: {\out 1. k + m + n = k + (m + n)} lcp@105: \ttbreak lcp@105: by (res_inst_tac [("n","k")] induct 1); lcp@105: {\out Level 1} lcp@105: {\out k + m + n = k + (m + n)} lcp@105: {\out 1. 0 + m + n = 0 + (m + n)} lcp@284: {\out 2. !!x. x + m + n = x + (m + n) ==>} lcp@284: {\out Suc(x) + m + n = Suc(x) + (m + n)} lcp@284: \end{ttbox} lcp@105: The base case holds easily; both sides reduce to $m+n$. The wenzelm@3114: tactic~\ttindex{Simp_tac} rewrites with respect to the current wenzelm@3114: simplification set, applying the rewrite rules for addition: lcp@284: \begin{ttbox} wenzelm@3114: by (Simp_tac 1); lcp@105: {\out Level 2} lcp@105: {\out k + m + n = k + (m + n)} lcp@284: {\out 1. !!x. x + m + n = x + (m + n) ==>} lcp@284: {\out Suc(x) + m + n = Suc(x) + (m + n)} lcp@284: \end{ttbox} lcp@331: The inductive step requires rewriting by the equations for addition lcp@105: together the induction hypothesis, which is also an equation. The wenzelm@3114: tactic~\ttindex{Asm_simp_tac} rewrites using the implicit wenzelm@3114: simplification set and any useful assumptions: lcp@284: \begin{ttbox} wenzelm@3114: by (Asm_simp_tac 1); lcp@105: {\out Level 3} lcp@105: {\out k + m + n = k + (m + n)} lcp@105: {\out No subgoals!} lcp@284: \end{ttbox} lcp@310: \index{instantiation|)} lcp@105: lcp@105: lcp@284: \section{A Prolog interpreter} lcp@105: \index{Prolog interpreter|bold} lcp@284: To demonstrate the power of tacticals, let us construct a Prolog lcp@105: interpreter and execute programs involving lists.\footnote{To run these lcp@331: examples, see the file {\tt FOL/ex/Prolog.ML}.} The Prolog program lcp@105: consists of a theory. We declare a type constructor for lists, with an lcp@105: arity declaration to say that $(\tau)list$ is of class~$term$ lcp@105: provided~$\tau$ is: lcp@105: \begin{eqnarray*} lcp@105: list & :: & (term)term lcp@105: \end{eqnarray*} lcp@105: We declare four constants: the empty list~$Nil$; the infix list lcp@105: constructor~{:}; the list concatenation predicate~$app$; the list reverse lcp@284: predicate~$rev$. (In Prolog, functions on lists are expressed as lcp@105: predicates.) lcp@105: \begin{eqnarray*} lcp@105: Nil & :: & \alpha list \\ lcp@105: {:} & :: & [\alpha,\alpha list] \To \alpha list \\ lcp@105: app & :: & [\alpha list,\alpha list,\alpha list] \To o \\ lcp@105: rev & :: & [\alpha list,\alpha list] \To o lcp@105: \end{eqnarray*} lcp@284: The predicate $app$ should satisfy the Prolog-style rules lcp@105: \[ {app(Nil,ys,ys)} \qquad lcp@105: {app(xs,ys,zs) \over app(x:xs, ys, x:zs)} \] lcp@105: We define the naive version of $rev$, which calls~$app$: lcp@105: \[ {rev(Nil,Nil)} \qquad lcp@105: {rev(xs,ys)\quad app(ys, x:Nil, zs) \over lcp@105: rev(x:xs, zs)} lcp@105: \] lcp@105: lcp@105: \index{examples!of theories} lcp@310: Theory \thydx{Prolog} extends first-order logic in order to make use lcp@105: of the class~$term$ and the type~$o$. The interpreter does not use the lcp@310: rules of~{\tt FOL}. lcp@105: \begin{ttbox} lcp@105: Prolog = FOL + lcp@296: types 'a list lcp@105: arities list :: (term)term clasohm@1387: consts Nil :: 'a list clasohm@1387: ":" :: ['a, 'a list]=> 'a list (infixr 60) clasohm@1387: app :: ['a list, 'a list, 'a list] => o clasohm@1387: rev :: ['a list, 'a list] => o lcp@105: rules appNil "app(Nil,ys,ys)" lcp@105: appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" lcp@105: revNil "rev(Nil,Nil)" lcp@105: revCons "[| rev(xs,ys); app(ys,x:Nil,zs) |] ==> rev(x:xs,zs)" lcp@105: end lcp@105: \end{ttbox} lcp@105: \subsection{Simple executions} lcp@284: Repeated application of the rules solves Prolog goals. Let us lcp@105: append the lists $[a,b,c]$ and~$[d,e]$. As the rules are applied, the lcp@105: answer builds up in~{\tt ?x}. lcp@105: \begin{ttbox} lcp@105: goal Prolog.thy "app(a:b:c:Nil, d:e:Nil, ?x)"; lcp@105: {\out Level 0} lcp@105: {\out app(a : b : c : Nil, d : e : Nil, ?x)} lcp@105: {\out 1. app(a : b : c : Nil, d : e : Nil, ?x)} lcp@105: \ttbreak lcp@105: by (resolve_tac [appNil,appCons] 1); lcp@105: {\out Level 1} lcp@105: {\out app(a : b : c : Nil, d : e : Nil, a : ?zs1)} lcp@105: {\out 1. app(b : c : Nil, d : e : Nil, ?zs1)} lcp@105: \ttbreak lcp@105: by (resolve_tac [appNil,appCons] 1); lcp@105: {\out Level 2} lcp@105: {\out app(a : b : c : Nil, d : e : Nil, a : b : ?zs2)} lcp@105: {\out 1. app(c : Nil, d : e : Nil, ?zs2)} lcp@105: \end{ttbox} lcp@105: At this point, the first two elements of the result are~$a$ and~$b$. lcp@105: \begin{ttbox} lcp@105: by (resolve_tac [appNil,appCons] 1); lcp@105: {\out Level 3} lcp@105: {\out app(a : b : c : Nil, d : e : Nil, a : b : c : ?zs3)} lcp@105: {\out 1. app(Nil, d : e : Nil, ?zs3)} lcp@105: \ttbreak lcp@105: by (resolve_tac [appNil,appCons] 1); lcp@105: {\out Level 4} lcp@105: {\out app(a : b : c : Nil, d : e : Nil, a : b : c : d : e : Nil)} lcp@105: {\out No subgoals!} lcp@105: \end{ttbox} lcp@105: lcp@284: Prolog can run functions backwards. Which list can be appended lcp@105: with $[c,d]$ to produce $[a,b,c,d]$? lcp@105: Using \ttindex{REPEAT}, we find the answer at once, $[a,b]$: lcp@105: \begin{ttbox} lcp@105: goal Prolog.thy "app(?x, c:d:Nil, a:b:c:d:Nil)"; lcp@105: {\out Level 0} lcp@105: {\out app(?x, c : d : Nil, a : b : c : d : Nil)} lcp@105: {\out 1. app(?x, c : d : Nil, a : b : c : d : Nil)} lcp@105: \ttbreak lcp@105: by (REPEAT (resolve_tac [appNil,appCons] 1)); lcp@105: {\out Level 1} lcp@105: {\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)} lcp@105: {\out No subgoals!} lcp@105: \end{ttbox} lcp@105: lcp@105: lcp@310: \subsection{Backtracking}\index{backtracking!Prolog style} lcp@296: Prolog backtracking can answer questions that have multiple solutions. lcp@296: Which lists $x$ and $y$ can be appended to form the list $[a,b,c,d]$? This lcp@296: question has five solutions. Using \ttindex{REPEAT} to apply the rules, we lcp@296: quickly find the first solution, namely $x=[]$ and $y=[a,b,c,d]$: lcp@105: \begin{ttbox} lcp@105: goal Prolog.thy "app(?x, ?y, a:b:c:d:Nil)"; lcp@105: {\out Level 0} lcp@105: {\out app(?x, ?y, a : b : c : d : Nil)} lcp@105: {\out 1. app(?x, ?y, a : b : c : d : Nil)} lcp@105: \ttbreak lcp@105: by (REPEAT (resolve_tac [appNil,appCons] 1)); lcp@105: {\out Level 1} lcp@105: {\out app(Nil, a : b : c : d : Nil, a : b : c : d : Nil)} lcp@105: {\out No subgoals!} lcp@105: \end{ttbox} lcp@284: Isabelle can lazily generate all the possibilities. The \ttindex{back} lcp@284: command returns the tactic's next outcome, namely $x=[a]$ and $y=[b,c,d]$: lcp@105: \begin{ttbox} lcp@105: back(); lcp@105: {\out Level 1} lcp@105: {\out app(a : Nil, b : c : d : Nil, a : b : c : d : Nil)} lcp@105: {\out No subgoals!} lcp@105: \end{ttbox} lcp@105: The other solutions are generated similarly. lcp@105: \begin{ttbox} lcp@105: back(); lcp@105: {\out Level 1} lcp@105: {\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)} lcp@105: {\out No subgoals!} lcp@105: \ttbreak lcp@105: back(); lcp@105: {\out Level 1} lcp@105: {\out app(a : b : c : Nil, d : Nil, a : b : c : d : Nil)} lcp@105: {\out No subgoals!} lcp@105: \ttbreak lcp@105: back(); lcp@105: {\out Level 1} lcp@105: {\out app(a : b : c : d : Nil, Nil, a : b : c : d : Nil)} lcp@105: {\out No subgoals!} lcp@105: \end{ttbox} lcp@105: lcp@105: lcp@105: \subsection{Depth-first search} lcp@105: \index{search!depth-first} lcp@105: Now let us try $rev$, reversing a list. lcp@105: Bundle the rules together as the \ML{} identifier {\tt rules}. Naive lcp@105: reverse requires 120 inferences for this 14-element list, but the tactic lcp@105: terminates in a few seconds. lcp@105: \begin{ttbox} lcp@105: goal Prolog.thy "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"; lcp@105: {\out Level 0} lcp@105: {\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)} lcp@284: {\out 1. rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,} lcp@284: {\out ?w)} lcp@284: \ttbreak lcp@105: val rules = [appNil,appCons,revNil,revCons]; lcp@105: \ttbreak lcp@105: by (REPEAT (resolve_tac rules 1)); lcp@105: {\out Level 1} lcp@105: {\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,} lcp@105: {\out n : m : l : k : j : i : h : g : f : e : d : c : b : a : Nil)} lcp@105: {\out No subgoals!} lcp@105: \end{ttbox} lcp@105: We may execute $rev$ backwards. This, too, should reverse a list. What lcp@105: is the reverse of $[a,b,c]$? lcp@105: \begin{ttbox} lcp@105: goal Prolog.thy "rev(?x, a:b:c:Nil)"; lcp@105: {\out Level 0} lcp@105: {\out rev(?x, a : b : c : Nil)} lcp@105: {\out 1. rev(?x, a : b : c : Nil)} lcp@105: \ttbreak lcp@105: by (REPEAT (resolve_tac rules 1)); lcp@105: {\out Level 1} lcp@105: {\out rev(?x1 : Nil, a : b : c : Nil)} lcp@105: {\out 1. app(Nil, ?x1 : Nil, a : b : c : Nil)} lcp@105: \end{ttbox} lcp@105: The tactic has failed to find a solution! It reached a dead end at lcp@331: subgoal~1: there is no~$\Var{x@1}$ such that [] appended with~$[\Var{x@1}]$ lcp@105: equals~$[a,b,c]$. Backtracking explores other outcomes. lcp@105: \begin{ttbox} lcp@105: back(); lcp@105: {\out Level 1} lcp@105: {\out rev(?x1 : a : Nil, a : b : c : Nil)} lcp@105: {\out 1. app(Nil, ?x1 : Nil, b : c : Nil)} lcp@105: \end{ttbox} lcp@105: This too is a dead end, but the next outcome is successful. lcp@105: \begin{ttbox} lcp@105: back(); lcp@105: {\out Level 1} lcp@105: {\out rev(c : b : a : Nil, a : b : c : Nil)} lcp@105: {\out No subgoals!} lcp@105: \end{ttbox} lcp@310: \ttindex{REPEAT} goes wrong because it is only a repetition tactical, not a lcp@310: search tactical. {\tt REPEAT} stops when it cannot continue, regardless of lcp@310: which state is reached. The tactical \ttindex{DEPTH_FIRST} searches for a lcp@310: satisfactory state, as specified by an \ML{} predicate. Below, lcp@105: \ttindex{has_fewer_prems} specifies that the proof state should have no lcp@310: subgoals. lcp@105: \begin{ttbox} lcp@105: val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) lcp@105: (resolve_tac rules 1); lcp@105: \end{ttbox} lcp@284: Since Prolog uses depth-first search, this tactic is a (slow!) lcp@296: Prolog interpreter. We return to the start of the proof using lcp@296: \ttindex{choplev}, and apply {\tt prolog_tac}: lcp@105: \begin{ttbox} lcp@105: choplev 0; lcp@105: {\out Level 0} lcp@105: {\out rev(?x, a : b : c : Nil)} lcp@105: {\out 1. rev(?x, a : b : c : Nil)} lcp@105: \ttbreak lcp@105: by (DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1)); lcp@105: {\out Level 1} lcp@105: {\out rev(c : b : a : Nil, a : b : c : Nil)} lcp@105: {\out No subgoals!} lcp@105: \end{ttbox} lcp@105: Let us try {\tt prolog_tac} on one more example, containing four unknowns: lcp@105: \begin{ttbox} lcp@105: goal Prolog.thy "rev(a:?x:c:?y:Nil, d:?z:b:?u)"; lcp@105: {\out Level 0} lcp@105: {\out rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)} lcp@105: {\out 1. rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)} lcp@105: \ttbreak lcp@105: by prolog_tac; lcp@105: {\out Level 1} lcp@105: {\out rev(a : b : c : d : Nil, d : c : b : a : Nil)} lcp@105: {\out No subgoals!} lcp@105: \end{ttbox} lcp@284: Although Isabelle is much slower than a Prolog system, Isabelle lcp@156: tactics can exploit logic programming techniques. lcp@156: