--- a/doc-src/IsarRef/generic.tex Sun Oct 31 15:26:37 1999 +0100
+++ b/doc-src/IsarRef/generic.tex Sun Oct 31 20:11:23 1999 +0100
@@ -61,6 +61,7 @@
\indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
\indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
\indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
+\indexisaratt{unfold}\indexisaratt{fold}
\begin{matharray}{rcl}
tag & : & \isaratt \\
untag & : & \isaratt \\[0.5ex]
@@ -69,10 +70,12 @@
COMP & : & \isaratt \\[0.5ex]
of & : & \isaratt \\
where & : & \isaratt \\[0.5ex]
+ unfold & : & \isaratt \\
+ fold & : & \isaratt \\[0.5ex]
standard & : & \isaratt \\
elimify & : & \isaratt \\
export^* & : & \isaratt \\
- transfer & : & \isaratt \\
+ transfer & : & \isaratt \\[0.5ex]
\end{matharray}
\begin{rail}
@@ -86,6 +89,8 @@
;
'where' (name '=' term * 'and')
;
+ ('unfold' | 'fold') thmrefs
+ ;
inst: underscore | term
;
@@ -108,7 +113,12 @@
\item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
instantiation, respectively. The terms given in $of$ are substituted for
any schematic variables occurring in a theorem from left to right;
- ``\texttt{_}'' (underscore) indicates to skip a position.
+ ``\texttt{_}'' (underscore) indicates to skip a position. Arguments
+ following a ``$concl\colon$'' specification refer to positions of the
+ conclusion of a rule.
+
+\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
+ meta-level definitions throughout a rule.
\item [$standard$] puts a theorem into the standard form of object-rules, just
as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
@@ -447,7 +457,8 @@
\item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
respectively. By default, rules are considered as \emph{safe}, while a
single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\
- not applied in the search-oriented automated methods, but only $rule$).
+ not applied in the search-oriented automated methods, but only in
+ single-step methods such as $rule$).
\item [$iff$] declares equations both as rewrite rules for the simplifier and
classical reasoning rules.
--- a/doc-src/IsarRef/hol.tex Sun Oct 31 15:26:37 1999 +0100
+++ b/doc-src/IsarRef/hol.tex Sun Oct 31 20:11:23 1999 +0100
@@ -1,6 +1,27 @@
\chapter{Isabelle/HOL Tools and Packages}\label{ch:hol-tools}
+\section{Miscellaneous attributes}
+
+\indexisaratt{rulify}\indexisaratt{rulify-prems}
+\begin{matharray}{rcl}
+ rulify & : & \isaratt \\
+ rulify_prems & : & \isaratt \\
+\end{matharray}
+
+\begin{descr}
+
+\item [$rulify$] puts a theorem into object-rule form, replacing implication
+ and universal quantification of HOL by the corresponding meta-logical
+ connectives. This is the same operation as performed by the
+ \texttt{qed_spec_mp} ML function.
+
+\item [$rulify_prems$] is similar to $rulify$, but acts on the premises of a
+ rule.
+
+\end{descr}
+
+
\section{Primitive types}
\indexisarcmd{typedecl}\indexisarcmd{typedef}
@@ -119,9 +140,11 @@
\section{(Co)Inductive sets}
\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive-cases}
+\indexisaratt{mono}
\begin{matharray}{rcl}
\isarcmd{inductive} & : & \isartrans{theory}{theory} \\
\isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
+ mono & : & \isaratt \\
\isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
\end{matharray}
@@ -136,11 +159,16 @@
;
indcases thmdef? nameref ':' \\ (prop +) comment?
;
+ 'mono' (() | 'add' | 'del')
+ ;
\end{rail}
\begin{descr}
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
(co)inductive sets from the given introduction rules.
+\item [$mono$] adds or deletes monotonicity rules from the theory or proof
+ context (the default is to add). These rule are involved in the automated
+ monotonicity proof of $\isarkeyword{inductive}$.
\item [$\isarkeyword{inductive_cases}$] creates simplified instances of
elimination rules of (co)inductive sets.
\end{descr}
--- a/doc-src/Ref/classical.tex Sun Oct 31 15:26:37 1999 +0100
+++ b/doc-src/Ref/classical.tex Sun Oct 31 20:11:23 1999 +0100
@@ -670,6 +670,17 @@
\end{ttbox}
deletes rules from the current claset.
+\medskip A few further functions are available as uppercase versions only:
+\begin{ttbox}
+AddXIs, AddXEs, AddXDs: thm list -> unit
+\end{ttbox}
+\indexbold{*AddXIs} \indexbold{*AddXEs} \indexbold{*AddXDs} augment the
+current claset by \emph{extra} introduction, elimination, or destruct rules.
+These provide additional hints for the basic non-automated proof methods of
+Isabelle/Isar \cite{isabelle-isar-ref}. The corresponding Isar attributes are
+``$intro!!$'', ``$elim!!$'', and ``$dest!!$''. Note that these extra rules do
+not have any effect on classic Isabelle tactics.
+
\subsection{Accessing the current claset}
\label{sec:access-current-claset}
--- a/doc-src/Ref/goals.tex Sun Oct 31 15:26:37 1999 +0100
+++ b/doc-src/Ref/goals.tex Sun Oct 31 20:11:23 1999 +0100
@@ -186,14 +186,14 @@
stores $thm$ in the theorem database associated with its theory and
returns that theorem.
-\item[\ttindexbold{bind_thms} and \ttindexbold{store_thms}] are similar to
+\item[\ttindexbold{bind_thms} \textrm{and} \ttindexbold{store_thms}] are similar to
\texttt{bind_thm} and \texttt{store_thm}, but store lists of theorems.
\end{ttdescription}
-The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be empty
-(\texttt{""}) as well; in that case the result is \emph{not} stored, but
-proper checks and presentation of the result still apply.
+The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be the empty
+string as well; in that case the result is \emph{not} stored, but proper
+checks and presentation of the result still apply.
\subsection{Extracting axioms and stored theorems}
--- a/doc-src/Ref/introduction.tex Sun Oct 31 15:26:37 1999 +0100
+++ b/doc-src/Ref/introduction.tex Sun Oct 31 20:11:23 1999 +0100
@@ -39,10 +39,10 @@
Subsequently, we assume that the \texttt{isabelle} executable is determined
automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome
\rangle\)/bin} to your search path.\footnote{Depending on your installation,
- there might be also stand-alone binaries located in some global directory
- such as \texttt{/usr/bin}. Do not attempt to copy {\tt \(\langle
- isabellehome \rangle\)/bin/isabelle}, though! See \texttt{isatool
- install} in \emph{The Isabelle System Manual} of how to do this properly.}
+ there may be stand-alone binaries located in some global directory such as
+ \texttt{/usr/bin}. Do not attempt to copy {\tt \(\langle isabellehome
+ \rangle\)/bin/isabelle}, though! See \texttt{isatool install} in
+ \emph{The Isabelle System Manual} of how to do this properly.}
\medskip
--- a/doc-src/Ref/simplifier.tex Sun Oct 31 15:26:37 1999 +0100
+++ b/doc-src/Ref/simplifier.tex Sun Oct 31 20:11:23 1999 +0100
@@ -502,7 +502,8 @@
\subsection{*The subgoaler}\label{sec:simp-subgoaler}
\begin{ttbox}
-setsubgoaler : simpset * (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
+setsubgoaler :
+ simpset * (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
prems_of_ss : simpset -> thm list
\end{ttbox}
@@ -794,7 +795,7 @@
\end{warn}
-\section{Examples of using the simplifier}
+\section{Examples of using the Simplifier}
\index{examples!of simplification} Assume we are working within {\tt
FOL} (see the file \texttt{FOL/ex/Nat}) and that
\begin{ttdescription}
@@ -1239,7 +1240,7 @@
prove particular theorems depending on the current redex.
-\section{*Setting up the simplifier}\label{sec:setting-up-simp}
+\section{*Setting up the Simplifier}\label{sec:setting-up-simp}
\index{simplification!setting up}
Setting up the simplifier for new logics is complicated. This section