tuned;
authorwenzelm
Mon Aug 23 15:27:27 1999 +0200 (1999-08-23)
changeset 7321b4dcc32310fb
parent 7320 e89fd7d0a624
child 7322 d16d7ddcc842
tuned;
doc-src/IsarRef/generic.tex
doc-src/IsarRef/pure.tex
doc-src/IsarRef/syntax.tex
doc-src/iman.sty
doc-src/isar.sty
     1.1 --- a/doc-src/IsarRef/generic.tex	Mon Aug 23 15:24:00 1999 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Mon Aug 23 15:27:27 1999 +0200
     1.3 @@ -7,15 +7,15 @@
     1.4  \indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}
     1.5  \indexisarmeth{rule}\indexisarmeth{erule}
     1.6  \begin{matharray}{rcl}
     1.7 -  fail & : & \isarmeth \\
     1.8 -  succeed & : & \isarmeth \\
     1.9    - & : & \isarmeth \\
    1.10    assumption & : & \isarmeth \\
    1.11 -  finish & : & \isarmeth \\
    1.12 +  finish & : & \isarmeth \\[0.5ex]
    1.13 +  rule & : & \isarmeth \\
    1.14 +  erule^* & : & \isarmeth \\[0.5ex]
    1.15    fold & : & \isarmeth \\
    1.16 -  unfold & : & \isarmeth \\
    1.17 -  rule & : & \isarmeth \\
    1.18 -  erule^* & : & \isarmeth \\
    1.19 +  unfold & : & \isarmeth \\[0.5ex]
    1.20 +  fail & : & \isarmeth \\
    1.21 +  succeed & : & \isarmeth \\
    1.22  \end{matharray}
    1.23  
    1.24  \begin{rail}
    1.25 @@ -24,14 +24,42 @@
    1.26  \end{rail}
    1.27  
    1.28  \begin{descr}
    1.29 -\item [$ $]
    1.30 -\end{descr}
    1.31 +\item [``$-$''] does nothing but insert the forward chaining facts as premises
    1.32 +  into the goal.  Note that command $\PROOFNAME$ without any method given
    1.33 +  actually performs a single reduction step using the $rule$ method (see
    1.34 +  below); thus a plain \emph{do-nothing} proof step would be $\PROOF{-}$
    1.35 +  rather than $\PROOFNAME$ alone.
    1.36 +\item [$assumption$] solves some goal by assumption (after inserting the
    1.37 +  goal's facts).
    1.38 +\item [$finish$] solves all remaining goals by assumption; this is the default
    1.39 +  terminal proof method for $\QEDNAME$, i.e.\ it usually does not have to be
    1.40 +  spelled out explicitly.
    1.41 +\item [$rule~thms$] applies some rule given as argument in backward manner;
    1.42 +  facts are used to reduce the rule before applying it to the goal.  Thus
    1.43 +  $rule$ without facts is plain \emph{introduction}, while with facts it
    1.44 +  becomes an \emph{elimination}.
    1.45 +  
    1.46 +  Note that the classical reasoner introduces another version of $rule$ that
    1.47 +  is able to pick appropriate rules automatically, whenever explicit $thms$
    1.48 +  are omitted (see \S\ref{sec:classical-basic}) .  That method is the default
    1.49 +  one for proof steps such as $\PROOFNAME$ and ``$\DDOT$'' (two dots).
    1.50 +  
    1.51 +\item [$erule~thms$] is similar to $rule$, but applies rules by
    1.52 +  elim-resolution.  This is an improper method, mainly for experimentation and
    1.53 +  porting of old script.  Actual elimination proofs are usually done with
    1.54 +  $rule$ (single step) or $elim$ (multiple steps, see
    1.55 +  \S\ref{sec:classical-basic}).
    1.56 +  
    1.57 +\item [$unfold~thms$ and $fold~thms$] expand and fold back again meta-level
    1.58 +  definitions $thms$ throughout all goals; facts may not be given.
    1.59  
    1.60 -FIXME
    1.61 -
    1.62 -%FIXME sort
    1.63 -%FIXME thmref (single)
    1.64 -%FIXME var vs. term
    1.65 +\item [$fail$] yields an empty result sequence; it is the identify of the
    1.66 +  ``\texttt{|}'' method combinator.
    1.67 +  
    1.68 +\item [$succeed$] yields a singleton result, which is unchanged except for the
    1.69 +  change from $prove$ mode back to $state$; it is the identify of the
    1.70 +  ``\texttt{,}'' method combinator.
    1.71 +\end{descr}
    1.72  
    1.73  
    1.74  \section{Miscellaneous attributes}
    1.75 @@ -41,46 +69,68 @@
    1.76  \indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
    1.77  \begin{matharray}{rcl}
    1.78    tag & : & \isaratt \\
    1.79 -  untag & : & \isaratt \\
    1.80 -  COMP & : & \isaratt \\
    1.81 +  untag & : & \isaratt \\[0.5ex]
    1.82 +  OF & : & \isaratt \\
    1.83    RS & : & \isaratt \\
    1.84 -  OF & : & \isaratt \\
    1.85 +  COMP & : & \isaratt \\[0.5ex]
    1.86    where & : & \isaratt \\
    1.87 -  of & : & \isaratt \\
    1.88 +  of & : & \isaratt \\[0.5ex]
    1.89    standard & : & \isaratt \\
    1.90    elimify & : & \isaratt \\
    1.91 +  export & : & \isaratt \\
    1.92    transfer & : & \isaratt \\
    1.93 -  export & : & \isaratt \\
    1.94  \end{matharray}
    1.95  
    1.96  \begin{rail}
    1.97    ('tag' | 'untag') (nameref+)
    1.98    ;
    1.99 -\end{rail}
   1.100 -
   1.101 -\begin{rail}
   1.102 -  ('COMP' | 'RS') nat? thmref
   1.103 -  ;
   1.104    'OF' thmrefs
   1.105    ;
   1.106 -\end{rail}
   1.107 -
   1.108 -\begin{rail}
   1.109 -  'where' (name '=' term * 'and')
   1.110 +  ('RS' | 'COMP') nat? thmref
   1.111    ;
   1.112    'of' (inst * ) ('concl' ':' (inst * ))?
   1.113    ;
   1.114 +  'where' (name '=' term * 'and')
   1.115 +  ;
   1.116  
   1.117    inst: underscore | term
   1.118    ;
   1.119  \end{rail}
   1.120  
   1.121  \begin{descr}
   1.122 -\item [$ $]
   1.123 +\item [$tag~tags$ and $untag~tags$] add and remove $tags$ to the theorem,
   1.124 +  respectively.  Tags may be any list of strings that serve as comment for
   1.125 +  some tools (e.g.\ $\LEMMANAME$ causes tag ``$lemma$'' to be added to the
   1.126 +  result).
   1.127 +\item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
   1.128 +  $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
   1.129 +  the reversed order).  $RS$ resolves with the $n$-th premise of $thm$; $COMP$
   1.130 +  is a version of $RS$ that does not include the automatic lifting process
   1.131 +  that is normally desired (see \texttt{RS} and \texttt{COMP} in
   1.132 +  \cite[\S5]{isabelle-ref}).
   1.133 +  
   1.134 +\item [$of~ts$ and $where~insts$] perform positional and named instantiation,
   1.135 +  respectively.  The terms given in $of$ are substituted for any variables
   1.136 +  occurring in a theorem from left to right; ``\texttt{_}'' (underscore)
   1.137 +  indicates to skip a position.
   1.138 + 
   1.139 +\item [$standard$] puts a theorem into the standard form of object-rules, just
   1.140 +  as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
   1.141 +  
   1.142 +\item [$elimify$] turns an destruction rule (such as projection $conjunct@1$
   1.143 +  into an elimination.
   1.144 +  
   1.145 +\item [$export$] lifts a local result out of the current proof context,
   1.146 +  generalizing all fixed variables and discharging all assumptions.  Export is
   1.147 +  usually done automatically behind the scenes.  This attribute is mainly for
   1.148 +  experimentation.
   1.149 +  
   1.150 +\item [$transfer$] promotes a theorem to the current theory context, which has
   1.151 +  to enclose the former one.  Normally, this is done automatically when rules
   1.152 +  are joined by inference.
   1.153 +
   1.154  \end{descr}
   1.155  
   1.156 -FIXME
   1.157 -
   1.158  
   1.159  \section{Calculational proof}\label{sec:calculation}
   1.160  
   1.161 @@ -172,7 +222,13 @@
   1.162  \end{rail}
   1.163  
   1.164  \begin{descr}
   1.165 -\item [$\isarkeyword{axclass}~$] FIXME
   1.166 +\item [$\isarkeyword{axclass}~$] defines an axiomatic type class as the
   1.167 +  intersection of existing classes, with additional axioms holding.  Class
   1.168 +  axioms may not contain more than one type variable.  The class axioms (with
   1.169 +  implicit sort constraints added) are bound to the given names.  Furthermore
   1.170 +  a class introduction rule is generated, which is employed by method
   1.171 +  $expand_classes$ in support instantiation proofs of this class.
   1.172 +
   1.173  \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
   1.174    c@2$] setup up a goal stating the class relation or type arity.  The proof
   1.175    would usually proceed by the $expand_classes$ method, and then establish the
   1.176 @@ -189,13 +245,12 @@
   1.177  
   1.178  \section{The Simplifier}
   1.179  
   1.180 -\subsection{Simplification methods}
   1.181 +\subsection{Simplification methods}\label{sec:simp}
   1.182  
   1.183 -\indexisarmeth{simp}\indexisarmeth{asm_simp}\indexisaratt{simp}
   1.184 +\indexisarmeth{simp}\indexisarmeth{asm_simp}
   1.185  \begin{matharray}{rcl}
   1.186    simp & : & \isarmeth \\
   1.187    asm_simp & : & \isarmeth \\
   1.188 -  simp & : & \isaratt \\
   1.189  \end{matharray}
   1.190  
   1.191  \begin{rail}
   1.192 @@ -206,7 +261,35 @@
   1.193    ;
   1.194  \end{rail}
   1.195  
   1.196 -FIXME
   1.197 +\begin{descr}
   1.198 +\item [Methods $simp$ and $asm_simp$] invoke Isabelle's simplifier, after
   1.199 +  modifying the context as follows adding or deleting given rules.  The
   1.200 +  \railtoken{only} modifier first removes all other rewrite rules and
   1.201 +  congruences, and then is like \railtoken{add}.  In contrast,
   1.202 +  \railtoken{other} ignores its arguments; nevertheless there may be
   1.203 +  side-effects on the context via attributes.  This provides a back door for
   1.204 +  arbitrary manipulation of the context.
   1.205 +  
   1.206 +  Both of these methods are based on \texttt{asm_full_simp_tac}, see
   1.207 +  \cite[\S10]{isabelle-ref}.
   1.208 +\end{descr}
   1.209 +
   1.210 +\subsection{Modifying the context}
   1.211 +
   1.212 +\indexisaratt{simp}
   1.213 +\begin{matharray}{rcl}
   1.214 +  simp & : & \isaratt \\
   1.215 +\end{matharray}
   1.216 +
   1.217 +\begin{rail}
   1.218 +  'simp' (() | 'add' | 'del')
   1.219 +  ;
   1.220 +\end{rail}
   1.221 +
   1.222 +\begin{descr}
   1.223 +\item [Attribute $simp$] adds or deletes rules from the theory or proof
   1.224 +  context.  The default is to add rules.
   1.225 +\end{descr}
   1.226  
   1.227  
   1.228  \subsection{Forward simplification}
   1.229 @@ -219,33 +302,135 @@
   1.230    asm_full_simplify & : & \isaratt \\
   1.231  \end{matharray}
   1.232  
   1.233 -FIXME
   1.234 +These attributes provide forward rules for simplification, which should be
   1.235 +used very rarely.  See the ML function of the same name in
   1.236 +\cite[\S10]{isabelle-ref} for more information.
   1.237  
   1.238  
   1.239  \section{The Classical Reasoner}
   1.240  
   1.241 -\subsection{Single step methods}
   1.242 +\subsection{Basic step methods}\label{sec:classical-basic}
   1.243 +
   1.244 +\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
   1.245 +\begin{matharray}{rcl}
   1.246 +  rule & : & \isarmeth \\
   1.247 +  intro & : & \isarmeth \\
   1.248 +  elim & : & \isarmeth \\
   1.249 +  contradiction & : & \isarmeth \\
   1.250 +\end{matharray}
   1.251 +
   1.252 +\begin{rail}
   1.253 +  ('rule' | 'intro' | 'elim') thmrefs
   1.254 +  ;
   1.255 +\end{rail}
   1.256 +
   1.257 +\begin{descr}
   1.258 +\item [Method $rule$] as offered by the classical reasoner is a refinement
   1.259 +  over the primitive one (see \S\ref{sec:pure-meth}).  In the case that no
   1.260 +  rules are provided as arguments, it automatically determines elimination and
   1.261 +  introduction rules from the context (see also \S\ref{sec:classical-mod}).
   1.262 +  In that form it is the default method for basic proof steps.
   1.263 +  
   1.264 +\item [Methods $intro$ and $elim$] repeatedly refine some goal by intro- or
   1.265 +  elim-resolution, after having inserted the facts.  Omitting the arguments
   1.266 +  refers to any suitable rules from the context, otherwise only the explicitly
   1.267 +  given ones may be applied.  The latter form admits better control of what is
   1.268 +  actually happening, thus it is appropriate as an initial proof method that
   1.269 +  splits up certain connectives of the goal, before entering the sub-proof.
   1.270 +
   1.271 +\item [Method $contradiction$] solves some goal by contradiction: both $A$ and
   1.272 +  $\neg A$ have to be present in the assumptions.
   1.273 +\end{descr}
   1.274 +
   1.275 +
   1.276 +\subsection{Automatic methods}\label{sec:classical-auto}
   1.277  
   1.278 -\subsection{Automatic methods}
   1.279 +\indexisarmeth{blast}
   1.280 +\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow_best}
   1.281 +\begin{matharray}{rcl}
   1.282 + blast & : & \isarmeth \\
   1.283 + fast & : & \isarmeth \\
   1.284 + best & : & \isarmeth \\
   1.285 + slow & : & \isarmeth \\
   1.286 + slow_best & : & \isarmeth \\
   1.287 +\end{matharray}
   1.288 +
   1.289 +\railalias{slowbest}{slow\_best}
   1.290 +\railterm{slowbest}
   1.291 +
   1.292 +\begin{rail}
   1.293 +  'blast' nat? (clamod * )
   1.294 +  ;
   1.295 +  ('fast' | 'best' | 'slow' | slowbest) (clamod * )
   1.296 +  ;
   1.297 +
   1.298 +  clamod: (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del') ':' thmrefs
   1.299 +  ;
   1.300 +\end{rail}
   1.301 +
   1.302 +\begin{descr}
   1.303 +\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
   1.304 +  in \cite[\S11]{isabelle-ref}).  The optional argument specifies a applies a
   1.305 +  user-supplied search bound (default 20).
   1.306 +\item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical
   1.307 +  reasoner (see the corresponding tactics \texttt{fast_tac} etc.\ in
   1.308 +  \cite[\S11]{isabelle-ref}).
   1.309 +\end{descr}
   1.310 +
   1.311 +Any of above methods support additional modifiers of the context of classical
   1.312 +rules.  There semantics is analogous to the attributes given in
   1.313 +\S\ref{sec:classical-mod}.
   1.314 +
   1.315  
   1.316  \subsection{Combined automatic methods}
   1.317  
   1.318 -\subsection{Modifying the context}
   1.319 +\indexisarmeth{auto}\indexisarmeth{force}
   1.320 +\begin{matharray}{rcl}
   1.321 +  force & : & \isarmeth \\
   1.322 +  auto & : & \isarmeth \\
   1.323 +\end{matharray}
   1.324 +
   1.325 +\begin{rail}
   1.326 +  ('force' | 'auto') (clasimpmod * )
   1.327 +  ;
   1.328  
   1.329 +  clasimpmod: ('simp' ('add' | 'del' | 'only') | other |
   1.330 +    (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs
   1.331 +\end{rail}
   1.332  
   1.333 +\begin{descr}
   1.334 +\item [$force$ and $auto$] provide access to Isabelle's combined
   1.335 +  simplification and classical reasoning tactics.  See \texttt{force_tac} and
   1.336 +  \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The
   1.337 +  modifier arguments correspond to those given in \S\ref{sec:simp} and
   1.338 +  \S\ref{sec:classical-auto}.
   1.339 +\end{descr}
   1.340 +
   1.341 +\subsection{Modifying the context}\label{sec:classical-mod}
   1.342  
   1.343 -%\indexisarcmd{}
   1.344 -%\begin{matharray}{rcl}
   1.345 -%  \isarcmd{} & : & \isartrans{}{} \\
   1.346 -%\end{matharray}
   1.347 +\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{delrule}
   1.348 +\begin{matharray}{rcl}
   1.349 +  intro & : & \isaratt \\
   1.350 +  elim & : & \isaratt \\
   1.351 +  dest & : & \isaratt \\
   1.352 +  delrule & : & \isaratt \\
   1.353 +\end{matharray}
   1.354  
   1.355 -%\begin{rail}
   1.356 -  
   1.357 -%\end{rail}
   1.358 +\begin{rail}
   1.359 +  ('intro' | 'elim' | 'dest') (() | '!' | '!!')
   1.360 +  ;
   1.361 +\end{rail}
   1.362  
   1.363 -%\begin{descr}
   1.364 -%\item [$ $]
   1.365 -%\end{descr}
   1.366 +\begin{descr}
   1.367 +\item [Attributes $intro$, $elim$, and $dest$] add introduction, elimination,
   1.368 +  and destruct rules, respectively.  By default, rules are considered as
   1.369 +  \emph{safe}, while a single ``!'' classifies as \emph{unsafe}, and ``!!'' as
   1.370 +  \emph{extra} (i.e.\ not applied in the search-oriented automatic methods).
   1.371 +
   1.372 +\item [Attribute $delrule$] deletes introduction or elimination rules from the
   1.373 +  context.  Destruction rules would have to be turned into elimination rules
   1.374 +  first, e.g.\ by using the $elimify$ attribute.
   1.375 +\end{descr}
   1.376  
   1.377  
   1.378  %%% Local Variables: 
     2.1 --- a/doc-src/IsarRef/pure.tex	Mon Aug 23 15:24:00 1999 +0200
     2.2 +++ b/doc-src/IsarRef/pure.tex	Mon Aug 23 15:27:27 1999 +0200
     2.3 @@ -659,8 +659,8 @@
     2.4    Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done by simply
     2.5    expanding the abbreviation by hand; note that $\PROOF{m@1}$ is usually
     2.6    sufficient to see what is going wrong.
     2.7 -\item [$\DDOT$] is a \emph{default proof}; it abbreviates $\BY{default}$.
     2.8 -\item [$\DOT$] is a \emph{trivial proof}, it abbreviates $\BY{-}$, where
     2.9 +\item [``$\DDOT$''] is a \emph{default proof}; it abbreviates $\BY{default}$.
    2.10 +\item [``$\DOT$''] is a \emph{trivial proof}, it abbreviates $\BY{-}$, where
    2.11    method ``$-$'' does nothing except inserting any facts into the proof state.
    2.12  \item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that
    2.13    \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve
     3.1 --- a/doc-src/IsarRef/syntax.tex	Mon Aug 23 15:24:00 1999 +0200
     3.2 +++ b/doc-src/IsarRef/syntax.tex	Mon Aug 23 15:27:27 1999 +0200
     3.3 @@ -134,7 +134,7 @@
     3.4  \indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
     3.5  \indexouternonterm{classdecl}
     3.6  \begin{rail}
     3.7 -  classdecl: name ('<' (nameref ',' +))?
     3.8 +  classdecl: name ('<' (nameref + ','))?
     3.9    ;
    3.10    sort: nameref | lbrace (nameref * ',') rbrace
    3.11    ;
     4.1 --- a/doc-src/iman.sty	Mon Aug 23 15:24:00 1999 +0200
     4.2 +++ b/doc-src/iman.sty	Mon Aug 23 15:27:27 1999 +0200
     4.3 @@ -36,8 +36,6 @@
     4.4  
     4.5  \newcommand\tooldx[1]{{\tt#1}\index{#1@{\tt#1} tool}}
     4.6  \newcommand\settdx[1]{{\tt#1}\index{#1@{\tt#1} setting}}
     4.7 -\newcommand\attdx[1]{$#1$\index{#1@$#1$ attribute}}
     4.8 -\newcommand\methdx[1]{$#1$\index{#1@$#1$ proof method}}
     4.9  
    4.10  %for cross-references: 2nd argument (page number) is ignored
    4.11  \newcommand\see[2]{{\it see \/}{#1}}
     5.1 --- a/doc-src/isar.sty	Mon Aug 23 15:24:00 1999 +0200
     5.2 +++ b/doc-src/isar.sty	Mon Aug 23 15:27:27 1999 +0200
     5.3 @@ -57,7 +57,7 @@
     5.4  \newcommand{\DEFS}{\isarkeyword{defs}}
     5.5  \newcommand{\TEXT}{\isarkeyword{text}}
     5.6  \newcommand{\TXT}{\isarkeyword{txt}}
     5.7 -\newcommand{\NOTE}[2]{\NOTENAME\ifthenelse{\equal{}{#1}}{}{~#1=}#2}
     5.8 +\newcommand{\NOTE}[2]{\NOTENAME~\ifthenelse{\equal{}{#1}}{}{#1=}#2}
     5.9  \newcommand{\FROM}[1]{\FROMNAME~#1}
    5.10  \newcommand{\WITH}[1]{\WITHNAME~#1}
    5.11  \newcommand{\FIX}[1]{\FIXNAME~#1}