1.1 --- a/doc-src/HOL/HOL.tex Mon Sep 06 17:03:19 1999 +0200
1.2 +++ b/doc-src/HOL/HOL.tex Mon Sep 06 18:17:48 1999 +0200
1.3 @@ -10,7 +10,7 @@
1.4 Church-style higher-order logic. Experience with the {\sc hol} system
1.5 has demonstrated that higher-order logic is widely applicable in many
1.6 areas of mathematics and computer science, not just hardware
1.7 -verification, {\sc hol}'s original \textit{raison d'\^etre\/}. It is
1.8 +verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}. It is
1.9 weaker than {\ZF} set theory but for most applications this does not
1.10 matter. If you prefer {\ML} to Lisp, you will probably prefer \HOL\
1.11 to~{\ZF}.
1.12 @@ -46,7 +46,7 @@
1.13 \begin{constants}
1.14 \it name &\it meta-type & \it description \\
1.15 \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\
1.16 - \cdx{Not} & $bool\To bool$ & negation ($\neg$) \\
1.17 + \cdx{Not} & $bool\To bool$ & negation ($\lnot$) \\
1.18 \cdx{True} & $bool$ & tautology ($\top$) \\
1.19 \cdx{False} & $bool$ & absurdity ($\bot$) \\
1.20 \cdx{If} & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\
1.21 @@ -132,13 +132,13 @@
1.22 Figure~\ref{hol-constants} lists the constants (including infixes and
1.23 binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
1.24 higher-order logic. Note that $a$\verb|~=|$b$ is translated to
1.25 -$\neg(a=b)$.
1.26 +$\lnot(a=b)$.
1.27
1.28 \begin{warn}
1.29 \HOL\ has no if-and-only-if connective; logical equivalence is expressed
1.30 using equality. But equality has a high priority, as befitting a
1.31 relation, while if-and-only-if typically has the lowest priority. Thus,
1.32 - $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
1.33 + $\lnot\lnot P=P$ abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$.
1.34 When using $=$ to mean logical equivalence, enclose both operands in
1.35 parentheses.
1.36 \end{warn}
1.37 @@ -157,14 +157,14 @@
1.38 functions.
1.39
1.40 \HOL\ offers various methods for introducing new types.
1.41 -See~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}.
1.42 +See~{\S}\ref{sec:HOL:Types} and~{\S}\ref{sec:HOL:datatype}.
1.43
1.44 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order
1.45 signatures; the relations $<$ and $\leq$ are polymorphic over this
1.46 class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and
1.47 the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass
1.48 \cldx{order} of \cldx{ord} which axiomatizes partially ordered types
1.49 -(w.r.t.\ $\le$).
1.50 +(w.r.t.\ $\leq$).
1.51
1.52 Three other syntactic type classes --- \cldx{plus}, \cldx{minus} and
1.53 \cldx{times} --- permit overloading of the operators {\tt+},\index{*"+
1.54 @@ -175,10 +175,10 @@
1.55 If you state a goal containing overloaded functions, you may need to include
1.56 type constraints. Type inference may otherwise make the goal more
1.57 polymorphic than you intended, with confusing results. For example, the
1.58 -variables $i$, $j$ and $k$ in the goal $i \le j \Imp i \le j+k$ have type
1.59 +variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type
1.60 $\alpha::\{ord,plus\}$, although you may have expected them to have some
1.61 numeric type, e.g. $nat$. Instead you should have stated the goal as
1.62 -$(i::nat) \le j \Imp i \le j+k$, which causes all three variables to have
1.63 +$(i::nat) \leq j \Imp i \leq j+k$, which causes all three variables to have
1.64 type $nat$.
1.65
1.66 \begin{warn}
1.67 @@ -231,12 +231,12 @@
1.68
1.69 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a
1.70 variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined
1.71 -to be the least (w.r.t.\ $\le$) $x$ such that $P~x$ holds (see
1.72 +to be the least (w.r.t.\ $\leq$) $x$ such that $P~x$ holds (see
1.73 Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$
1.74 choice operator, so \texttt{Least} is always meaningful, but may yield
1.75 nothing useful in case there is not a unique least element satisfying
1.76 $P$.\footnote{Class $ord$ does not require much of its instances, so
1.77 - $\le$ need not be a well-ordering, not even an order at all!}
1.78 + $\leq$ need not be a well-ordering, not even an order at all!}
1.79
1.80 \medskip All these binders have priority 10.
1.81
1.82 @@ -260,7 +260,7 @@
1.83 logical meaning. By declaring translations, you can cause instances of the
1.84 \texttt{case} construct to denote applications of particular case operators.
1.85 This is what happens automatically for each \texttt{datatype} definition
1.86 -(see~\S\ref{sec:HOL:datatype}).
1.87 +(see~{\S}\ref{sec:HOL:datatype}).
1.88
1.89 \begin{warn}
1.90 Both \texttt{if} and \texttt{case} constructs have as low a priority as
1.91 @@ -335,7 +335,7 @@
1.92 The definitions above should never be expanded and are shown for completeness
1.93 only. Instead users should reason in terms of the derived rules shown below
1.94 or, better still, using high-level tactics
1.95 -(see~\S\ref{sec:HOL:generic-packages}).
1.96 +(see~{\S}\ref{sec:HOL:generic-packages}).
1.97 \end{warn}
1.98
1.99 Some of the rules mention type variables; for example, \texttt{refl}
1.100 @@ -441,7 +441,14 @@
1.101 from subgoal $i$.
1.102 \item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction
1.103 on $P$ for subgoal $i$: the latter is replaced by two identical subgoals
1.104 - with the added assumptions $P$ and $\neg P$, respectively.
1.105 + with the added assumptions $P$ and $\lnot P$, respectively.
1.106 +\item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then
1.107 + \texttt{mp} in subgoal $i$, which is typically useful when forward-chaining
1.108 + from an induction hypothesis. As a generalization of \texttt{mp_tac},
1.109 + if there are assumptions $\forall \vec{x}. P \vec{x} \imp Q \vec{x}$ and
1.110 + $P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables)
1.111 + then it replaces the universally quantified implication by $Q \vec{a}$.
1.112 + It may instantiate unknowns. It fails if it can do nothing.
1.113 \end{ttdescription}
1.114
1.115
1.116 @@ -592,7 +599,7 @@
1.117 constructs. Infix operators include union and intersection ($A\un B$
1.118 and $A\int B$), the subset and membership relations, and the image
1.119 operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to
1.120 -$\neg(a\in b)$.
1.121 +$\lnot(a\in b)$.
1.122
1.123 The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in
1.124 the obvious manner using~\texttt{insert} and~$\{\}$:
1.125 @@ -955,7 +962,7 @@
1.126 expressed by the theorem \tdx{split_if}:
1.127 $$
1.128 \Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~
1.129 -((\Var{b} \to \Var{P}(\Var{x})) \land (\neg \Var{b} \to \Var{P}(\Var{y})))
1.130 +((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y})))
1.131 \eqno{(*)}
1.132 $$
1.133 For example, a simple instance of $(*)$ is
1.134 @@ -992,8 +999,8 @@
1.135 where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the
1.136 right form because internally the left-hand side is
1.137 $\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples
1.138 -are splitting rules for \texttt{case} expressions (see~\S\ref{subsec:list}
1.139 -and~\S\ref{subsec:datatype:basics}).
1.140 +are splitting rules for \texttt{case} expressions (see~{\S}\ref{subsec:list}
1.141 +and~{\S}\ref{subsec:datatype:basics}).
1.142
1.143 Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also
1.144 imperative versions of \texttt{addsplits} and \texttt{delsplits}
1.145 @@ -1117,7 +1124,7 @@
1.146 \beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for
1.147 introducing new types in general. The most important type
1.148 construction, the \texttt{datatype}, is treated separately in
1.149 -\S\ref{sec:HOL:datatype}.
1.150 +{\S}\ref{sec:HOL:datatype}.
1.151
1.152
1.153 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}
1.154 @@ -1225,7 +1232,7 @@
1.155 shown. The constructions are fairly standard and can be found in the
1.156 respective theory files. Although the sum and product types are
1.157 constructed manually for foundational reasons, they are represented as
1.158 -actual datatypes later (see \S\ref{subsec:datatype:rep_datatype}).
1.159 +actual datatypes later (see {\S}\ref{subsec:datatype:rep_datatype}).
1.160 Therefore, the theory \texttt{Datatype} should be used instead of
1.161 \texttt{Sum} or \texttt{Prod}.
1.162
1.163 @@ -1335,7 +1342,7 @@
1.164 \texttt{nat} are part of the default simpset.
1.165
1.166 Functions on \tydx{nat} can be defined by primitive or well-founded recursion;
1.167 -see \S\ref{sec:HOL:recursive}. A simple example is addition.
1.168 +see {\S}\ref{sec:HOL:recursive}. A simple example is addition.
1.169 Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following
1.170 the standard convention.
1.171 \begin{ttbox}
1.172 @@ -1352,7 +1359,7 @@
1.173 the order of the two cases.
1.174 Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
1.175 \cdx{nat_rec}, which is available because \textit{nat} is represented as
1.176 -a datatype (see \S\ref{subsec:datatype:rep_datatype}).
1.177 +a datatype (see {\S}\ref{subsec:datatype:rep_datatype}).
1.178
1.179 %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
1.180 %Recursion along this relation resembles primitive recursion, but is
1.181 @@ -1513,7 +1520,7 @@
1.182 \begin{center}\tt
1.183 case $e$ of [] => $a$ | \(x\)\#\(xs\) => b
1.184 \end{center}
1.185 -is defined by translation. For details see~\S\ref{sec:HOL:datatype}. There
1.186 +is defined by translation. For details see~{\S}\ref{sec:HOL:datatype}. There
1.187 is also a case splitting rule \tdx{split_list_case}
1.188 \[
1.189 \begin{array}{l}
1.190 @@ -1524,10 +1531,10 @@
1.191 \end{array}
1.192 \]
1.193 which can be fed to \ttindex{addsplits} just like
1.194 -\texttt{split_if} (see~\S\ref{subsec:HOL:case:splitting}).
1.195 +\texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}).
1.196
1.197 \texttt{List} provides a basic library of list processing functions defined by
1.198 -primitive recursion (see~\S\ref{sec:HOL:primrec}). The recursion equations
1.199 +primitive recursion (see~{\S}\ref{sec:HOL:primrec}). The recursion equations
1.200 are shown in Fig.\ts\ref{fig:HOL:list-simps}.
1.201
1.202 \index{list@{\textit{list}} type|)}
1.203 @@ -1543,7 +1550,7 @@
1.204
1.205 \begin{warn}
1.206 Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
1.207 - unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}.
1.208 + unsound, because $\exists x. x=x$ is a theorem \cite[{\S}7]{paulson-COLOG}.
1.209 \end{warn}
1.210 A \bfindex{type definition} identifies the new type with a subset of
1.211 an existing type. More precisely, the new type is defined by
1.212 @@ -1699,11 +1706,11 @@
1.213
1.214 In Isabelle/HOL record types have to be defined explicitly, fixing their field
1.215 names and types, and their (optional) parent record (see
1.216 -\S\ref{sec:HOL:record-def}). Afterwards, records may be formed using above
1.217 +{\S}\ref{sec:HOL:record-def}). Afterwards, records may be formed using above
1.218 syntax, while obeying the canonical order of fields as given by their
1.219 declaration. The record package also provides several operations like
1.220 -selectors and updates (see \S\ref{sec:HOL:record-ops}), together with
1.221 -characteristic properties (see \S\ref{sec:HOL:record-thms}).
1.222 +selectors and updates (see {\S}\ref{sec:HOL:record-ops}), together with
1.223 +characteristic properties (see {\S}\ref{sec:HOL:record-thms}).
1.224
1.225 There is an example theory demonstrating most basic aspects of extensible
1.226 records (see theory \texttt{HOL/ex/Points} in the Isabelle sources).
1.227 @@ -1891,7 +1898,7 @@
1.228
1.229 Inductive datatypes, similar to those of \ML, frequently appear in
1.230 applications of Isabelle/HOL. In principle, such types could be defined by
1.231 -hand via \texttt{typedef} (see \S\ref{sec:typedef}), but this would be far too
1.232 +hand via \texttt{typedef} (see {\S}\ref{sec:typedef}), but this would be far too
1.233 tedious. The \ttindex{datatype} definition package of Isabelle/HOL (cf.\
1.234 \cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores. It generates an
1.235 appropriate \texttt{typedef} based on a least fixed-point construction, and
1.236 @@ -1931,7 +1938,7 @@
1.237 \item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is
1.238 the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$
1.239 are admissible types.
1.240 -\item $\tau = \sigma \rightarrow \tau'$, where $\tau'$ is an admissible
1.241 +\item $\tau = \sigma \to \tau'$, where $\tau'$ is an admissible
1.242 type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined
1.243 types are {\em strictly positive})
1.244 \end{itemize}
1.245 @@ -1972,7 +1979,7 @@
1.246 \medskip
1.247
1.248 Types in HOL must be non-empty. Each of the new datatypes
1.249 -$(\alpha@1,\ldots,\alpha@h)t@j$ with $1 \le j \le n$ is non-empty iff it has a
1.250 +$(\alpha@1,\ldots,\alpha@h)t@j$ with $1 \leq j \leq n$ is non-empty iff it has a
1.251 constructor $C^j@i$ with the following property: for all argument types
1.252 $\tau^j@{i,i'}$ of the form $(\alpha@1,\ldots,\alpha@h)t@{j'}$ the datatype
1.253 $(\alpha@1,\ldots,\alpha@h)t@{j'}$ is non-empty.
1.254 @@ -2014,7 +2021,7 @@
1.255 The datatype package also provides structural induction rules. For
1.256 datatypes without nested recursion, this is of the following form:
1.257 \[
1.258 -\infer{P@1~x@1 \wedge \dots \wedge P@n~x@n}
1.259 +\infer{P@1~x@1 \land \dots \land P@n~x@n}
1.260 {\begin{array}{lcl}
1.261 \Forall x@1 \dots x@{m^1@1}.
1.262 \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots;
1.263 @@ -2044,7 +2051,7 @@
1.264 \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,
1.265 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex]
1.266 && \left\{(i',i'')~\left|~
1.267 - 1\leq i' \leq m^j@i \wedge 1 \leq i'' \leq n \wedge
1.268 + 1\leq i' \leq m^j@i \land 1 \leq i'' \leq n \land
1.269 \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\}
1.270 \end{array}
1.271 \]
1.272 @@ -2070,7 +2077,7 @@
1.273 constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for
1.274 \texttt{term} gets the form
1.275 \[
1.276 -\infer{P@1~x@1 \wedge P@2~x@2}
1.277 +\infer{P@1~x@1 \land P@2~x@2}
1.278 {\begin{array}{l}
1.279 \Forall x.~P@1~(\mathtt{Var}~x) \\
1.280 \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\
1.281 @@ -2105,7 +2112,7 @@
1.282 \end{array}
1.283 \]
1.284 where the $x@{i,j}$ are either identifiers or nested tuple patterns as in
1.285 -\S\ref{subsec:prod-sum}.
1.286 +{\S}\ref{subsec:prod-sum}.
1.287 \begin{warn}
1.288 All constructors must be present, their order is fixed, and nested patterns
1.289 are not supported (with the exception of tuples). Violating this
1.290 @@ -2126,7 +2133,7 @@
1.291 \]
1.292 where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct.
1.293 This theorem can be added to a simpset via \ttindex{addsplits}
1.294 -(see~\S\ref{subsec:HOL:case:splitting}).
1.295 +(see~{\S}\ref{subsec:HOL:case:splitting}).
1.296
1.297 \subsubsection{The function \cdx{size}}\label{sec:HOL:size}
1.298
1.299 @@ -2456,7 +2463,7 @@
1.300 \subsubsection{Example: Evaluation of expressions}
1.301 Using mutual primitive recursion, we can define evaluation functions \texttt{evala}
1.302 and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in
1.303 -\S\ref{subsec:datatype:basics}:
1.304 +{\S}\ref{subsec:datatype:basics}:
1.305 \begin{ttbox}
1.306 consts
1.307 evala :: "['a => nat, 'a aexp] => nat"
1.308 @@ -2516,7 +2523,7 @@
1.309
1.310 \subsubsection{Example: A substitution function for terms}
1.311 Functions on datatypes with nested recursion, such as the type
1.312 -\texttt{term} mentioned in \S\ref{subsec:datatype:basics}, are
1.313 +\texttt{term} mentioned in {\S}\ref{subsec:datatype:basics}, are
1.314 also defined by mutual primitive recursion. A substitution
1.315 function \texttt{subst_term} on type \texttt{term}, similar to the functions
1.316 \texttt{substa} and \texttt{substb} described above, can
1.317 @@ -2536,7 +2543,7 @@
1.318 subst_term f t # subst_term_list f ts"
1.319 \end{ttbox}
1.320 The recursion scheme follows the structure of the unfolded definition of type
1.321 -\texttt{term} shown in \S\ref{subsec:datatype:basics}. To prove properties of
1.322 +\texttt{term} shown in {\S}\ref{subsec:datatype:basics}. To prove properties of
1.323 this substitution function, mutual induction is needed:
1.324 \begin{ttbox}
1.325 Goal
1.326 @@ -2625,7 +2632,7 @@
1.327 Typically, $f$ takes the recursive function's arguments (as a tuple) and
1.328 returns a result expressed in terms of the function \texttt{size}. It is
1.329 called a \textbf{measure function}. Recall that \texttt{size} is overloaded
1.330 - and is defined on all datatypes (see \S\ref{sec:HOL:size}).
1.331 + and is defined on all datatypes (see {\S}\ref{sec:HOL:size}).
1.332
1.333 \item $\mathop{\mathtt{inv_image}} f\;R$ is a generalisation of
1.334 \texttt{measure}. It specifies a relation such that $x\prec y$ iff $f(x)$
1.335 @@ -2989,7 +2996,7 @@
1.336 procedure. These are mostly taken from Pelletier \cite{pelletier86}.
1.337
1.338 \item File \texttt{set.ML} proves Cantor's Theorem, which is presented in
1.339 - \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
1.340 + {\S}\ref{sec:hol-cantor} below, and the Schr{\"o}der-Bernstein Theorem.
1.341
1.342 \item Theory \texttt{MT} contains Jacob Frost's formalization~\cite{frost93} of
1.343 Milner and Tofte's coinduction example~\cite{milner-coind}. This
2.1 --- a/src/HOL/HOL_lemmas.ML Mon Sep 06 17:03:19 1999 +0200
2.2 +++ b/src/HOL/HOL_lemmas.ML Mon Sep 06 18:17:48 1999 +0200
2.3 @@ -424,9 +424,22 @@
2.4 in CHANGED_GOAL (rtac (th' RS ssubst))
2.5 end;
2.6
2.7 +(* combination of (spec RS spec RS ...(j times) ... spec RS mp *)
2.8 +local
2.9 + fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
2.10 + | wrong_prem (Bound _) = true
2.11 + | wrong_prem _ = false;
2.12 + fun wrong (Const ("==>", _) $ (Const ("Trueprop", _) $ t) $ _) = wrong_prem t
2.13 + | wrong _ = true;
2.14 + val filter_right = filter (fn t => not (wrong (#prop (rep_thm t))));
2.15 +in
2.16 + fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
2.17 + fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]
2.18 +end;
2.19 +
2.20 +
2.21 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
2.22
2.23 -
2.24 (** strip ! and --> from proved goal while preserving !-bound var names **)
2.25
2.26 local