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: lcp@105: Look through {\em Isabelle's Object-Logics\/} and try proving some simple lcp@105: theorems. You probably should begin with first-order logic ({\tt FOL} lcp@105: or~{\tt LK}). Try working some of the examples provided, and others from lcp@105: the literature. Set theory~({\tt ZF}) and Constructive Type Theory~({\tt lcp@105: CTT}) form a richer world for mathematical reasoning and, again, many lcp@105: examples are in the literature. Higher-order logic~({\tt HOL}) is lcp@331: Isabelle's most sophisticated logic because its types and functions are lcp@331: identified with those of 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 lcp@307: \S\ref{deriving}. The \ttindex{goal} command, when supplied a goal of the lcp@307: form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates $\phi\Imp\phi$ lcp@307: as the initial proof state and returns a list consisting of the theorems lcp@307: ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$. These meta-assumptions lcp@310: are also recorded internally, allowing {\tt result} 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. lcp@105: Note that it contains assumptions. Calling \ttindex{result} discharges the lcp@105: assumptions --- both occurrences of $P\conj Q$ are discharged as one --- lcp@105: 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} lcp@105: val conjE = result(); 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: lcp@105: $$ (P\Imp\bot) \Imp \neg P \eqno(\neg I)$$ lcp@105: $$ \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 lcp@105: val notI = result(); 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!} lcp@105: val notE = result(); 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} lcp@105: Calling \ttindex{result} strips the meta-quantifiers, so the resulting lcp@105: theorem is the same as before. lcp@105: \begin{ttbox} lcp@105: val notE = result(); 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: lcp@105: Isabelle makes no distinction between simple extensions of a logic --- like lcp@105: defining a type~$bool$ with constants~$true$ and~$false$ --- and defining lcp@105: an entire logic. A theory definition has the form 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} lcp@105: arities {\it arity declarations} lcp@105: consts {\it constant declarations} lcp@105: rules {\it rule declarations} lcp@105: translations {\it translation 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 lcp@105: $S@1$,~\ldots,~$S@n$. It may declare new classes, types, arities lcp@105: (overloadings of existing types), constants and rules; it can specify the lcp@105: default sort for type variables. A constant declaration can specify an lcp@105: associated concrete syntax. The translations section specifies rewrite lcp@105: rules on abstract syntax trees, for defining notations and abbreviations. lcp@310: \index{*ML section} lcp@310: The {\tt ML} section contains code to perform arbitrary syntactic lcp@284: transformations. The main declaration forms are discussed below. nipkow@303: The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the lcp@307: appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}. lcp@105: lcp@105: All the declaration parts can be omitted. In the simplest case, $T$ is lcp@105: just the union of $S@1$,~\ldots,~$S@n$. New theories always extend one lcp@105: or more other theories, inheriting their types, constants, syntax, etc. lcp@310: The theory \thydx{Pure} contains nothing but Isabelle's meta-logic. lcp@105: lcp@331: Each theory definition must reside in a separate file, whose name is the lcp@331: theory's with {\tt.thy} appended. For example, theory {\tt ListFn} resides lcp@331: on a file named {\tt ListFn.thy}. Isabelle uses this convention to locate the lcp@331: file containing a given theory; \ttindexbold{use_thy} automatically loads a lcp@331: theory's parents before loading the theory itself. lcp@105: lcp@331: Calling \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads a theory from the lcp@331: file {\it T}{\tt.thy}, writes the corresponding {\ML} code to the file lcp@331: {\tt.{\it T}.thy.ML}, reads the latter file, and deletes it if no errors lcp@331: occurred. This declares the {\ML} structure~$T$, which contains a component clasohm@109: {\tt thy} denoting the new theory, a component for each rule, and everything clasohm@109: declared in {\it ML code}. lcp@105: lcp@105: Errors may arise during the translation to {\ML} (say, a misspelled keyword) lcp@105: or during creation of the new theory (say, a type error in a rule). But if lcp@331: all goes well, {\tt use_thy} will finally read the file {\it T}{\tt.ML}, if lcp@105: it exists. This file typically begins with the {\ML} declaration {\tt lcp@105: open}~$T$ and contains proofs that refer to the components of~$T$. lcp@105: lcp@296: When a theory file is modified, many theories may have to be reloaded. lcp@296: Isabelle records the modification times and dependencies of theory files. lcp@331: 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@105: \subsection{Declaring constants and rules} lcp@310: \indexbold{constants!declaring}\index{rules!declaring} lcp@310: lcp@296: Most theories simply declare constants and rules. The {\bf constant lcp@105: declaration part} has the form lcp@105: \begin{ttbox} lcp@105: consts \(c@1\) :: "\(\tau@1\)" lcp@105: \vdots lcp@105: \(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 lcp@105: types. Each type {\em must\/} be enclosed in quotation marks. 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} lcp@105: \(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: lcp@310: \indexbold{definitions} lcp@284: {\bf Definitions} are rules of the form $t\equiv u$. Normally definitions lcp@284: should be conservative, serving only as abbreviations. As of this writing, lcp@284: Isabelle does not provide a separate declaration part for definitions; it lcp@284: is your responsibility to ensure that your definitions are conservative. lcp@284: However, Isabelle's rewriting primitives will reject $t\equiv u$ unless all lcp@284: variables free in~$u$ are also free in~$t$. lcp@105: lcp@105: \index{examples!of theories} lcp@105: This theory extends first-order logic with two constants {\em nand} and lcp@284: {\em xor}, and declares rules to define them: lcp@284: \begin{ttbox} lcp@105: Gate = FOL + lcp@105: consts nand,xor :: "[o,o] => o" lcp@105: rules 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: 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 lcp@284: \(tids@1\) \(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 lcp@105: 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 lcp@105: consts Nil :: "'a list" lcp@105: 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: lcp@105: \begin{warn} lcp@105: Arity declarations resemble constant declarations, but there are {\it no\/} lcp@105: quotation marks! Types and rules must be quoted because the theory lcp@105: translator passes them verbatim to the {\ML} output file. lcp@105: \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} lcp@307: types gate = "[o,o] => o" lcp@307: 'a pred = "'a => o" nipkow@303: ('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 nipkow@303: 'a stream = "nat => 'a" lcp@307: signal = "nat stream" nipkow@303: 'a list nipkow@303: \end{ttbox} lcp@307: A synonym is merely an abbreviation for some existing type expression. Hence lcp@307: synonyms may not be recursive! Internally all synonyms are fully expanded. As lcp@307: a consequence Isabelle output never contains synonyms. Their main purpose is lcp@307: to improve the readability of theories. Synonyms can be used just like any nipkow@303: other type: nipkow@303: \begin{ttbox} nipkow@303: consts and,or :: "gate" nipkow@303: 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 + lcp@105: consts "~&" :: "[o,o] => o" (infixl 35) lcp@105: "#" :: "[o,o] => o" (infixl 30) lcp@105: rules 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: 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} lcp@284: 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: lcp@310: The declaration above does not allow the {\tt if}-{\tt then}-{\tt else} lcp@310: construct to be split across several lines, even if it is too long to fit lcp@310: on one line. Pretty-printing information can be added to specify the lcp@310: 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} lcp@284: 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} lcp@284: 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@105: ${<}\_,\_{>}$ for pairs. 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} lcp@105: The name of the type constructor is~{\tt *} and not {\tt op~*}, as it would lcp@105: be in the case of an infix constant. Only infix type constructors can have lcp@105: symbolic names like~{\tt *}. There is no general mixfix syntax for types. 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 lcp@105: consts "0" :: "'a::arith" ("0") lcp@105: "1" :: "'a::arith" ("1") lcp@105: "+" :: "['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 lcp@105: 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 lcp@296: consts "0" :: "nat" ("0") lcp@105: Suc :: "nat=>nat" lcp@105: rec :: "[nat, 'a, [nat,'a]=>'a] => 'a" lcp@296: "+" :: "[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 lcp@296: contains the theory and axioms. Opening structure {\tt Nat} lets us write lcp@296: {\tt induct} instead of {\tt Nat.induct}, and so forth. lcp@105: \begin{ttbox} lcp@105: open Nat; lcp@105: \end{ttbox} 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!} lcp@105: val add_0 = result(); 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!} lcp@105: val add_Suc = result(); 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@105: {\out ~Suc(k) = k} lcp@105: {\out 1. ~Suc(k) = k} lcp@105: \ttbreak lcp@105: by (res_inst_tac [("n","k")] induct 1); lcp@105: {\out Level 1} lcp@105: {\out ~Suc(k) = k} lcp@105: {\out 1. ~Suc(0) = 0} lcp@105: {\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@105: {\out ~Suc(k) = k} lcp@105: {\out 1. Suc(0) = 0 ==> False} lcp@105: {\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@105: {\out ~Suc(k) = k} lcp@105: {\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@105: {\out ~Suc(k) = k} lcp@105: {\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@105: {\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@105: {\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: lcp@310: Isabelle's simplification tactics repeatedly apply equations to a subgoal, lcp@310: perhaps proving it. For efficiency, the rewrite rules must be lcp@310: packaged into a {\bf simplification set},\index{simplification sets} lcp@310: or {\bf simpset}. We take the standard simpset for first-order logic and lcp@331: insert the equations proved in the previous section, namely lcp@310: $0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$: lcp@284: \begin{ttbox} lcp@105: val add_ss = FOL_ss addrews [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 lcp@105: tactic~\ttindex{simp_tac} rewrites with respect to the given simplification lcp@331: set, applying the rewrite rules for addition: lcp@284: \begin{ttbox} lcp@105: by (simp_tac add_ss 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 lcp@105: tactic~\ttindex{asm_simp_tac} rewrites using a simplification set and any lcp@105: useful assumptions: lcp@284: \begin{ttbox} lcp@105: by (asm_simp_tac add_ss 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 lcp@105: consts Nil :: "'a list" lcp@105: ":" :: "['a, 'a list]=> 'a list" (infixr 60) lcp@105: app :: "['a list, 'a list, 'a list] => o" lcp@105: 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: