1.1 --- a/doc-src/Intro/advanced.tex Mon May 05 12:15:53 1997 +0200
1.2 +++ b/doc-src/Intro/advanced.tex Mon May 05 13:24:11 1997 +0200
1.3 @@ -3,14 +3,15 @@
1.4 Before continuing, it might be wise to try some of your own examples in
1.5 Isabelle, reinforcing your knowledge of the basic functions.
1.6
1.7 -Look through {\em Isabelle's Object-Logics\/} and try proving some simple
1.8 -theorems. You probably should begin with first-order logic ({\tt FOL}
1.9 -or~{\tt LK}). Try working some of the examples provided, and others from
1.10 -the literature. Set theory~({\tt ZF}) and Constructive Type Theory~({\tt
1.11 - CTT}) form a richer world for mathematical reasoning and, again, many
1.12 -examples are in the literature. Higher-order logic~({\tt HOL}) is
1.13 -Isabelle's most sophisticated logic because its types and functions are
1.14 -identified with those of the meta-logic.
1.15 +Look through {\em Isabelle's Object-Logics\/} and try proving some
1.16 +simple theorems. You probably should begin with first-order logic
1.17 +({\tt FOL} or~{\tt LK}). Try working some of the examples provided,
1.18 +and others from the literature. Set theory~({\tt ZF}) and
1.19 +Constructive Type Theory~({\tt CTT}) form a richer world for
1.20 +mathematical reasoning and, again, many examples are in the
1.21 +literature. Higher-order logic~({\tt HOL}) is Isabelle's most
1.22 +elaborate logic. Its types and functions are identified with those of
1.23 +the meta-logic.
1.24
1.25 Choose a logic that you already understand. Isabelle is a proof
1.26 tool, not a teaching tool; if you do not know how to do a particular proof
1.27 @@ -36,11 +37,12 @@
1.28 \index{examples!of deriving rules}\index{assumptions!of main goal}
1.29
1.30 The subgoal module supports the derivation of rules, as discussed in
1.31 -\S\ref{deriving}. The \ttindex{goal} command, when supplied a goal of the
1.32 -form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates $\phi\Imp\phi$
1.33 -as the initial proof state and returns a list consisting of the theorems
1.34 -${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$. These meta-assumptions
1.35 -are also recorded internally, allowing {\tt result} to discharge them
1.36 +\S\ref{deriving}. The \ttindex{goal} command, when supplied a goal of
1.37 +the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates
1.38 +$\phi\Imp\phi$ as the initial proof state and returns a list
1.39 +consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$,
1.40 +\ldots,~$k$. These meta-assumptions are also recorded internally,
1.41 +allowing {\tt result} (which is called by {\tt qed}) to discharge them
1.42 in the original order.
1.43
1.44 Let us derive $\conj$ elimination using Isabelle.
1.45 @@ -91,13 +93,13 @@
1.46 {\out No subgoals!}
1.47 \end{ttbox}
1.48 Calling \ttindex{topthm} returns the current proof state as a theorem.
1.49 -Note that it contains assumptions. Calling \ttindex{result} discharges the
1.50 -assumptions --- both occurrences of $P\conj Q$ are discharged as one ---
1.51 -and makes the variables schematic.
1.52 +Note that it contains assumptions. Calling \ttindex{qed} discharges
1.53 +the assumptions --- both occurrences of $P\conj Q$ are discharged as
1.54 +one --- and makes the variables schematic.
1.55 \begin{ttbox}
1.56 topthm();
1.57 {\out val it = "R [P & Q, P & Q, [| P; Q |] ==> R]" : thm}
1.58 -val conjE = result();
1.59 +qed "conjE";
1.60 {\out val conjE = "[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R" : thm}
1.61 \end{ttbox}
1.62
1.63 @@ -139,8 +141,8 @@
1.64 \[ \infer[({\neg}I)]{\neg P}{\infer*{\bot}{[P]}} \qquad
1.65 \infer[({\neg}E)]{Q}{\neg P & P} \]
1.66 This requires proving the following meta-formulae:
1.67 -$$ (P\Imp\bot) \Imp \neg P \eqno(\neg I)$$
1.68 -$$ \List{\neg P; P} \Imp Q. \eqno(\neg E)$$
1.69 +$$ (P\Imp\bot) \Imp \neg P \eqno(\neg I) $$
1.70 +$$ \List{\neg P; P} \Imp Q. \eqno(\neg E) $$
1.71
1.72
1.73 \subsection{Deriving the $\neg$ introduction rule}
1.74 @@ -185,7 +187,7 @@
1.75 {\out ~P}
1.76 {\out No subgoals!}
1.77 \ttbreak
1.78 -val notI = result();
1.79 +qed "notI";
1.80 {\out val notI = "(?P ==> False) ==> ~?P" : thm}
1.81 \end{ttbox}
1.82 \indexbold{*notI theorem}
1.83 @@ -251,7 +253,7 @@
1.84 {\out Level 4}
1.85 {\out R}
1.86 {\out No subgoals!}
1.87 -val notE = result();
1.88 +qed "notE";
1.89 {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
1.90 \end{ttbox}
1.91 \indexbold{*notE theorem}
1.92 @@ -313,10 +315,10 @@
1.93 {\out !!P R. [| ~ P; P |] ==> R}
1.94 {\out No subgoals!}
1.95 \end{ttbox}
1.96 -Calling \ttindex{result} strips the meta-quantifiers, so the resulting
1.97 +Calling \ttindex{qed} strips the meta-quantifiers, so the resulting
1.98 theorem is the same as before.
1.99 \begin{ttbox}
1.100 -val notE = result();
1.101 +qed "notE";
1.102 {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
1.103 \end{ttbox}
1.104 Do not use the {\tt!!}\ trick if the premises contain meta-level
1.105 @@ -328,62 +330,67 @@
1.106 \section{Defining theories}\label{sec:defining-theories}
1.107 \index{theories!defining|(}
1.108
1.109 -Isabelle makes no distinction between simple extensions of a logic --- like
1.110 -defining a type~$bool$ with constants~$true$ and~$false$ --- and defining
1.111 -an entire logic. A theory definition has the form
1.112 +Isabelle makes no distinction between simple extensions of a logic ---
1.113 +like specifying a type~$bool$ with constants~$true$ and~$false$ ---
1.114 +and defining an entire logic. A theory definition has a form like
1.115 \begin{ttbox}
1.116 \(T\) = \(S@1\) + \(\cdots\) + \(S@n\) +
1.117 classes {\it class declarations}
1.118 default {\it sort}
1.119 types {\it type declarations and synonyms}
1.120 -arities {\it arity declarations}
1.121 +arities {\it type arity declarations}
1.122 consts {\it constant declarations}
1.123 -translations {\it translation declarations}
1.124 -defs {\it definitions}
1.125 +syntax {\it syntactic constant declarations}
1.126 +translations {\it ast translation rules}
1.127 +defs {\it meta-logical definitions}
1.128 rules {\it rule declarations}
1.129 end
1.130 ML {\it ML code}
1.131 \end{ttbox}
1.132 This declares the theory $T$ to extend the existing theories
1.133 -$S@1$,~\ldots,~$S@n$. It may declare new classes, types, arities
1.134 -(overloadings of existing types), constants and rules; it can specify the
1.135 -default sort for type variables. A constant declaration can specify an
1.136 -associated concrete syntax. The translations section specifies rewrite
1.137 -rules on abstract syntax trees, for defining notations and abbreviations.
1.138 -\index{*ML section}
1.139 -The {\tt ML} section contains code to perform arbitrary syntactic
1.140 -transformations. The main declaration forms are discussed below.
1.141 -The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the
1.142 - appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.
1.143 +$S@1$,~\ldots,~$S@n$. It may introduce new classes, types, arities
1.144 +(of existing types), constants and rules; it can specify the default
1.145 +sort for type variables. A constant declaration can specify an
1.146 +associated concrete syntax. The translations section specifies
1.147 +rewrite rules on abstract syntax trees, handling notations and
1.148 +abbreviations. \index{*ML section} The {\tt ML} section may contain
1.149 +code to perform arbitrary syntactic transformations. The main
1.150 +declaration forms are discussed below. The full syntax can be found
1.151 +in \iflabelundefined{app:TheorySyntax}{an appendix of the {\it
1.152 + Reference Manual}}{App.\ts\ref{app:TheorySyntax}}. Also note that
1.153 +object-logics may add further theory sections, for example {\tt
1.154 + typedef}, {\tt datatype} in \HOL.
1.155
1.156 -All the declaration parts can be omitted or repeated and may appear in any
1.157 -order, except that the {\ML} section must be last. In the simplest case, $T$
1.158 -is just the union of $S@1$,~\ldots,~$S@n$. New theories always extend one or
1.159 -more other theories, inheriting their types, constants, syntax, etc. The
1.160 -theory \thydx{Pure} contains nothing but Isabelle's meta-logic.
1.161 +All the declaration parts can be omitted or repeated and may appear in
1.162 +any order, except that the {\ML} section must be last (after the {\tt
1.163 + end} keyword). In the simplest case, $T$ is just the union of
1.164 +$S@1$,~\ldots,~$S@n$. New theories always extend one or more other
1.165 +theories, inheriting their types, constants, syntax, etc. The theory
1.166 +\thydx{Pure} contains nothing but Isabelle's meta-logic. The variant
1.167 +\thydx{CPure} offers the more usual higher-order function application
1.168 +syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$.
1.169
1.170 -Each theory definition must reside in a separate file, whose name is the
1.171 -theory's with {\tt.thy} appended. For example, theory {\tt ListFn} resides
1.172 -on a file named {\tt ListFn.thy}. Isabelle uses this convention to locate the
1.173 -file containing a given theory; \ttindexbold{use_thy} automatically loads a
1.174 -theory's parents before loading the theory itself.
1.175 +Each theory definition must reside in a separate file, whose name is
1.176 +the theory's with {\tt.thy} appended. Calling
1.177 +\ttindexbold{use_thy}~{\tt"{\it T\/}"} reads the definition from {\it
1.178 + T}{\tt.thy}, writes a corresponding file of {\ML} code {\tt.{\it
1.179 + T}.thy.ML}, reads the latter file, and deletes it if no errors
1.180 +occurred. This declares the {\ML} structure~$T$, which contains a
1.181 +component {\tt thy} denoting the new theory, a component for each
1.182 +rule, and everything declared in {\it ML code}.
1.183
1.184 -Calling \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads a theory from the
1.185 -file {\it T}{\tt.thy}, writes the corresponding {\ML} code to the file
1.186 -{\tt.{\it T}.thy.ML}, reads the latter file, and deletes it if no errors
1.187 -occurred. This declares the {\ML} structure~$T$, which contains a component
1.188 -{\tt thy} denoting the new theory, a component for each rule, and everything
1.189 -declared in {\it ML code}.
1.190 +Errors may arise during the translation to {\ML} (say, a misspelled
1.191 +keyword) or during creation of the new theory (say, a type error in a
1.192 +rule). But if all goes well, {\tt use_thy} will finally read the file
1.193 +{\it T}{\tt.ML} (if it exists). This file typically contains proofs
1.194 +that refer to the components of~$T$. The structure is automatically
1.195 +opened, so its components may be referred to by unqualified names,
1.196 +e.g.\ just {\tt thy} instead of $T${\tt .thy}.
1.197
1.198 -Errors may arise during the translation to {\ML} (say, a misspelled keyword)
1.199 -or during creation of the new theory (say, a type error in a rule). But if
1.200 -all goes well, {\tt use_thy} will finally read the file {\it T}{\tt.ML}, if
1.201 -it exists. This file typically begins with the {\ML} declaration {\tt
1.202 -open}~$T$ and contains proofs that refer to the components of~$T$.
1.203 -
1.204 -When a theory file is modified, many theories may have to be reloaded.
1.205 -Isabelle records the modification times and dependencies of theory files.
1.206 -See
1.207 +\ttindexbold{use_thy} automatically loads a theory's parents before
1.208 +loading the theory itself. When a theory file is modified, many
1.209 +theories may have to be reloaded. Isabelle records the modification
1.210 +times and dependencies of theory files. See
1.211 \iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%
1.212 {\S\ref{sec:reloading-theories}}
1.213 for more details.
1.214 @@ -418,23 +425,23 @@
1.215 $rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be
1.216 enclosed in quotation marks.
1.217
1.218 -\indexbold{definitions} The {\bf definition part} is similar, but with the
1.219 -keyword {\tt defs} instead of {\tt rules}. {\bf Definitions} are rules of the
1.220 -form $s \equiv t$, and should serve only as abbreviations. The simplest form
1.221 -of a definition is $f \equiv t$, where $f$ is a constant. Isabelle also
1.222 -allows a derived form where the arguments of~$f$ appear on the left:
1.223 -\begin{itemize}
1.224 -\item In uncurried syntax: $f(x@1,\dots,x@n) \equiv u$ (\FOL, \ZF, \dots)
1.225 -\item In curried syntax: $f~x@1~\dots~x@n \equiv u$ (\HOL, \HOLCF)
1.226 -\end{itemize}
1.227 -Isabelle checks for common errors in definitions, such as extra variables on
1.228 -the right-hand side. Determined users can write non-conservative
1.229 -`definitions' by using mutual recursion, for example; the consequences of
1.230 -such actions are their responsibility.
1.231 +\indexbold{definitions} The {\bf definition part} is similar, but with
1.232 +the keyword {\tt defs} instead of {\tt rules}. {\bf Definitions} are
1.233 +rules of the form $s \equiv t$, and should serve only as
1.234 +abbreviations. The simplest form of a definition is $f \equiv t$,
1.235 +where $f$ is a constant. Also allowed are $\eta$-equivalent forms,
1.236 +where the arguments of~$f$ appear applied on the left-hand side of the
1.237 +equation instead of abstracted on the right-hand side.
1.238
1.239 -\index{examples!of theories}
1.240 -This theory extends first-order logic by declaring and defining two constants,
1.241 -{\em nand} and {\em xor}:
1.242 +Isabelle checks for common errors in definitions, such as extra
1.243 +variables on the right-hand side, but currently does not a complete
1.244 +test of well-formedness. Thus determined users can write
1.245 +non-conservative `definitions' by using mutual recursion, for example;
1.246 +the consequences of such actions are their responsibility.
1.247 +
1.248 +\index{examples!of theories} This example theory extends first-order
1.249 +logic by declaring and defining two constants, {\em nand} and {\em
1.250 + xor}:
1.251 \begin{ttbox}
1.252 Gate = FOL +
1.253 consts nand,xor :: [o,o] => o
1.254 @@ -557,11 +564,11 @@
1.255 arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\)
1.256 \end{ttbox}
1.257
1.258 -\begin{warn}
1.259 -Arity declarations resemble constant declarations, but there are {\it no\/}
1.260 -quotation marks! Types and rules must be quoted because the theory
1.261 -translator passes them verbatim to the {\ML} output file.
1.262 -\end{warn}
1.263 +%\begin{warn}
1.264 +%Arity declarations resemble constant declarations, but there are {\it no\/}
1.265 +%quotation marks! Types and rules must be quoted because the theory
1.266 +%translator passes them verbatim to the {\ML} output file.
1.267 +%\end{warn}
1.268
1.269 \subsection{Type synonyms}\indexbold{type synonyms}
1.270 Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
1.271 @@ -579,11 +586,11 @@
1.272 signal = nat stream
1.273 'a list
1.274 \end{ttbox}
1.275 -A synonym is merely an abbreviation for some existing type expression. Hence
1.276 -synonyms may not be recursive! Internally all synonyms are fully expanded. As
1.277 -a consequence Isabelle output never contains synonyms. Their main purpose is
1.278 -to improve the readability of theories. Synonyms can be used just like any
1.279 -other type:
1.280 +A synonym is merely an abbreviation for some existing type expression.
1.281 +Hence synonyms may not be recursive! Internally all synonyms are
1.282 +fully expanded. As a consequence Isabelle output never contains
1.283 +synonyms. Their main purpose is to improve the readability of theory
1.284 +definitions. Synonyms can be used just like any other type:
1.285 \begin{ttbox}
1.286 consts and,or :: gate
1.287 negate :: signal => signal
1.288 @@ -623,10 +630,10 @@
1.289 if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}. Underscores
1.290 denote argument positions.
1.291
1.292 -The declaration above does not allow the {\tt if}-{\tt then}-{\tt else}
1.293 -construct to be split across several lines, even if it is too long to fit
1.294 -on one line. Pretty-printing information can be added to specify the
1.295 -layout of mixfix operators. For details, see
1.296 +The declaration above does not allow the {\tt if}-{\tt then}-{\tt
1.297 + else} construct to be printed split across several lines, even if it
1.298 +is too long to fit on one line. Pretty-printing information can be
1.299 +added to specify the layout of mixfix operators. For details, see
1.300 \iflabelundefined{Defining-Logics}%
1.301 {the {\it Reference Manual}, chapter `Defining Logics'}%
1.302 {Chap.\ts\ref{Defining-Logics}}.
1.303 @@ -672,9 +679,11 @@
1.304 \end{ttbox}
1.305
1.306 \begin{warn}
1.307 -The name of the type constructor is~{\tt *} and not {\tt op~*}, as it would
1.308 -be in the case of an infix constant. Only infix type constructors can have
1.309 -symbolic names like~{\tt *}. There is no general mixfix syntax for types.
1.310 + The name of the type constructor is~{\tt *} and not {\tt op~*}, as
1.311 + it would be in the case of an infix constant. Only infix type
1.312 + constructors can have symbolic names like~{\tt *}. General mixfix
1.313 + syntax for types may be introduced via appropriate {\tt syntax}
1.314 + declarations.
1.315 \end{warn}
1.316
1.317
1.318 @@ -826,11 +835,7 @@
1.319 \end{ttbox}
1.320 In axiom {\tt add_def}, recall that \verb|%| stands for~$\lambda$.
1.321 Loading this theory file creates the \ML\ structure {\tt Nat}, which
1.322 -contains the theory and axioms. Opening structure {\tt Nat} lets us write
1.323 -{\tt induct} instead of {\tt Nat.induct}, and so forth.
1.324 -\begin{ttbox}
1.325 -open Nat;
1.326 -\end{ttbox}
1.327 +contains the theory and axioms.
1.328
1.329 \subsection{Proving some recursion equations}
1.330 File {\tt FOL/ex/Nat.ML} contains proofs involving this theory of the
1.331 @@ -846,7 +851,7 @@
1.332 {\out Level 1}
1.333 {\out 0 + n = n}
1.334 {\out No subgoals!}
1.335 -val add_0 = result();
1.336 +qed "add_0";
1.337 \end{ttbox}
1.338 And here is the successor case:
1.339 \begin{ttbox}
1.340 @@ -859,7 +864,7 @@
1.341 {\out Level 1}
1.342 {\out Suc(m) + n = Suc(m + n)}
1.343 {\out No subgoals!}
1.344 -val add_Suc = result();
1.345 +qed "add_Suc";
1.346 \end{ttbox}
1.347 The induction rule raises some complications, which are discussed next.
1.348 \index{theories!defining|)}