updated; Isabelle99
authorwenzelm
Sun Oct 31 20:11:23 1999 +0100 (1999-10-31)
changeset 79900a604b2fc2b1
parent 7989 50ca726466c6
child 7991 966efa3bb851
updated;
doc-src/IsarRef/generic.tex
doc-src/IsarRef/hol.tex
doc-src/Ref/classical.tex
doc-src/Ref/goals.tex
doc-src/Ref/introduction.tex
doc-src/Ref/simplifier.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Sun Oct 31 15:26:37 1999 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sun Oct 31 20:11:23 1999 +0100
     1.3 @@ -61,6 +61,7 @@
     1.4  \indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
     1.5  \indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
     1.6  \indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
     1.7 +\indexisaratt{unfold}\indexisaratt{fold}
     1.8  \begin{matharray}{rcl}
     1.9    tag & : & \isaratt \\
    1.10    untag & : & \isaratt \\[0.5ex]
    1.11 @@ -69,10 +70,12 @@
    1.12    COMP & : & \isaratt \\[0.5ex]
    1.13    of & : & \isaratt \\
    1.14    where & : & \isaratt \\[0.5ex]
    1.15 +  unfold & : & \isaratt \\
    1.16 +  fold & : & \isaratt \\[0.5ex]
    1.17    standard & : & \isaratt \\
    1.18    elimify & : & \isaratt \\
    1.19    export^* & : & \isaratt \\
    1.20 -  transfer & : & \isaratt \\
    1.21 +  transfer & : & \isaratt \\[0.5ex]
    1.22  \end{matharray}
    1.23  
    1.24  \begin{rail}
    1.25 @@ -86,6 +89,8 @@
    1.26    ;
    1.27    'where' (name '=' term * 'and')
    1.28    ;
    1.29 +  ('unfold' | 'fold') thmrefs
    1.30 +  ;
    1.31  
    1.32    inst: underscore | term
    1.33    ;
    1.34 @@ -108,7 +113,12 @@
    1.35  \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
    1.36    instantiation, respectively.  The terms given in $of$ are substituted for
    1.37    any schematic variables occurring in a theorem from left to right;
    1.38 -  ``\texttt{_}'' (underscore) indicates to skip a position.
    1.39 +  ``\texttt{_}'' (underscore) indicates to skip a position.  Arguments
    1.40 +  following a ``$concl\colon$'' specification refer to positions of the
    1.41 +  conclusion of a rule.
    1.42 +  
    1.43 +\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
    1.44 +  meta-level definitions throughout a rule.
    1.45   
    1.46  \item [$standard$] puts a theorem into the standard form of object-rules, just
    1.47    as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
    1.48 @@ -447,7 +457,8 @@
    1.49  \item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
    1.50    respectively.  By default, rules are considered as \emph{safe}, while a
    1.51    single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\ 
    1.52 -  not applied in the search-oriented automated methods, but only $rule$).
    1.53 +  not applied in the search-oriented automated methods, but only in
    1.54 +  single-step methods such as $rule$).
    1.55    
    1.56  \item [$iff$] declares equations both as rewrite rules for the simplifier and
    1.57    classical reasoning rules.
     2.1 --- a/doc-src/IsarRef/hol.tex	Sun Oct 31 15:26:37 1999 +0100
     2.2 +++ b/doc-src/IsarRef/hol.tex	Sun Oct 31 20:11:23 1999 +0100
     2.3 @@ -1,6 +1,27 @@
     2.4  
     2.5  \chapter{Isabelle/HOL Tools and Packages}\label{ch:hol-tools}
     2.6  
     2.7 +\section{Miscellaneous attributes}
     2.8 +
     2.9 +\indexisaratt{rulify}\indexisaratt{rulify-prems}
    2.10 +\begin{matharray}{rcl}
    2.11 +  rulify & : & \isaratt \\
    2.12 +  rulify_prems & : & \isaratt \\
    2.13 +\end{matharray}
    2.14 +
    2.15 +\begin{descr}
    2.16 +
    2.17 +\item [$rulify$] puts a theorem into object-rule form, replacing implication
    2.18 +  and universal quantification of HOL by the corresponding meta-logical
    2.19 +  connectives.  This is the same operation as performed by the
    2.20 +  \texttt{qed_spec_mp} ML function.
    2.21 +  
    2.22 +\item [$rulify_prems$] is similar to $rulify$, but acts on the premises of a
    2.23 +  rule.
    2.24 +
    2.25 +\end{descr}
    2.26 +
    2.27 +
    2.28  \section{Primitive types}
    2.29  
    2.30  \indexisarcmd{typedecl}\indexisarcmd{typedef}
    2.31 @@ -119,9 +140,11 @@
    2.32  \section{(Co)Inductive sets}
    2.33  
    2.34  \indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive-cases}
    2.35 +\indexisaratt{mono}
    2.36  \begin{matharray}{rcl}
    2.37    \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
    2.38    \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
    2.39 +  mono & : & \isaratt \\
    2.40    \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
    2.41  \end{matharray}
    2.42  
    2.43 @@ -136,11 +159,16 @@
    2.44    ;
    2.45    indcases thmdef? nameref ':' \\ (prop +) comment?
    2.46    ;
    2.47 +  'mono' (() | 'add' | 'del')
    2.48 +  ;
    2.49  \end{rail}
    2.50  
    2.51  \begin{descr}
    2.52  \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define
    2.53    (co)inductive sets from the given introduction rules.
    2.54 +\item [$mono$] adds or deletes monotonicity rules from the theory or proof
    2.55 +  context (the default is to add).  These rule are involved in the automated
    2.56 +  monotonicity proof of $\isarkeyword{inductive}$.
    2.57  \item [$\isarkeyword{inductive_cases}$] creates simplified instances of
    2.58    elimination rules of (co)inductive sets.
    2.59  \end{descr}
     3.1 --- a/doc-src/Ref/classical.tex	Sun Oct 31 15:26:37 1999 +0100
     3.2 +++ b/doc-src/Ref/classical.tex	Sun Oct 31 20:11:23 1999 +0100
     3.3 @@ -670,6 +670,17 @@
     3.4  \end{ttbox}
     3.5  deletes rules from the current claset. 
     3.6  
     3.7 +\medskip A few further functions are available as uppercase versions only:
     3.8 +\begin{ttbox}
     3.9 +AddXIs, AddXEs, AddXDs: thm list -> unit
    3.10 +\end{ttbox}
    3.11 +\indexbold{*AddXIs} \indexbold{*AddXEs} \indexbold{*AddXDs} augment the
    3.12 +current claset by \emph{extra} introduction, elimination, or destruct rules.
    3.13 +These provide additional hints for the basic non-automated proof methods of
    3.14 +Isabelle/Isar \cite{isabelle-isar-ref}.  The corresponding Isar attributes are
    3.15 +``$intro!!$'', ``$elim!!$'', and ``$dest!!$''.  Note that these extra rules do
    3.16 +not have any effect on classic Isabelle tactics.
    3.17 +
    3.18  
    3.19  \subsection{Accessing the current claset}
    3.20  \label{sec:access-current-claset}
     4.1 --- a/doc-src/Ref/goals.tex	Sun Oct 31 15:26:37 1999 +0100
     4.2 +++ b/doc-src/Ref/goals.tex	Sun Oct 31 20:11:23 1999 +0100
     4.3 @@ -186,14 +186,14 @@
     4.4    stores $thm$ in the theorem database associated with its theory and
     4.5    returns that theorem.
     4.6    
     4.7 -\item[\ttindexbold{bind_thms} and \ttindexbold{store_thms}] are similar to
     4.8 +\item[\ttindexbold{bind_thms} \textrm{and} \ttindexbold{store_thms}] are similar to
     4.9    \texttt{bind_thm} and \texttt{store_thm}, but store lists of theorems.
    4.10  
    4.11  \end{ttdescription}
    4.12  
    4.13 -The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be empty
    4.14 -(\texttt{""}) as well; in that case the result is \emph{not} stored, but
    4.15 -proper checks and presentation of the result still apply.
    4.16 +The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be the empty
    4.17 +string as well; in that case the result is \emph{not} stored, but proper
    4.18 +checks and presentation of the result still apply.
    4.19  
    4.20  
    4.21  \subsection{Extracting axioms and stored theorems}
     5.1 --- a/doc-src/Ref/introduction.tex	Sun Oct 31 15:26:37 1999 +0100
     5.2 +++ b/doc-src/Ref/introduction.tex	Sun Oct 31 20:11:23 1999 +0100
     5.3 @@ -39,10 +39,10 @@
     5.4  Subsequently, we assume that the \texttt{isabelle} executable is determined
     5.5  automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome
     5.6    \rangle\)/bin} to your search path.\footnote{Depending on your installation,
     5.7 -  there might be also stand-alone binaries located in some global directory
     5.8 -  such as \texttt{/usr/bin}.  Do not attempt to copy {\tt \(\langle
     5.9 -    isabellehome \rangle\)/bin/isabelle}, though!  See \texttt{isatool
    5.10 -    install} in \emph{The Isabelle System Manual} of how to do this properly.}
    5.11 +  there may be stand-alone binaries located in some global directory such as
    5.12 +  \texttt{/usr/bin}.  Do not attempt to copy {\tt \(\langle isabellehome
    5.13 +    \rangle\)/bin/isabelle}, though!  See \texttt{isatool install} in
    5.14 +  \emph{The Isabelle System Manual} of how to do this properly.}
    5.15  
    5.16  \medskip
    5.17  
     6.1 --- a/doc-src/Ref/simplifier.tex	Sun Oct 31 15:26:37 1999 +0100
     6.2 +++ b/doc-src/Ref/simplifier.tex	Sun Oct 31 20:11:23 1999 +0100
     6.3 @@ -502,7 +502,8 @@
     6.4  
     6.5  \subsection{*The subgoaler}\label{sec:simp-subgoaler}
     6.6  \begin{ttbox}
     6.7 -setsubgoaler : simpset *  (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
     6.8 +setsubgoaler :
     6.9 +  simpset *  (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
    6.10  prems_of_ss  : simpset -> thm list
    6.11  \end{ttbox}
    6.12  
    6.13 @@ -794,7 +795,7 @@
    6.14  \end{warn}
    6.15  
    6.16  
    6.17 -\section{Examples of using the simplifier}
    6.18 +\section{Examples of using the Simplifier}
    6.19  \index{examples!of simplification} Assume we are working within {\tt
    6.20    FOL} (see the file \texttt{FOL/ex/Nat}) and that
    6.21  \begin{ttdescription}
    6.22 @@ -1239,7 +1240,7 @@
    6.23  prove particular theorems depending on the current redex.
    6.24  
    6.25  
    6.26 -\section{*Setting up the simplifier}\label{sec:setting-up-simp}
    6.27 +\section{*Setting up the Simplifier}\label{sec:setting-up-simp}
    6.28  \index{simplification!setting up}
    6.29  
    6.30  Setting up the simplifier for new logics is complicated.  This section