more stuff;
authorwenzelm
Tue Mar 05 18:55:46 2002 +0100 (2002-03-05)
changeset 130240461b281c2b5
parent 13023 f869b6822006
child 13025 433c57d09d53
more stuff;
doc-src/IsarRef/conversion.tex
doc-src/IsarRef/generic.tex
doc-src/IsarRef/logics.tex
doc-src/IsarRef/pure.tex
doc-src/IsarRef/refcard.tex
     1.1 --- a/doc-src/IsarRef/conversion.tex	Tue Mar 05 18:54:55 2002 +0100
     1.2 +++ b/doc-src/IsarRef/conversion.tex	Tue Mar 05 18:55:46 2002 +0100
     1.3 @@ -221,7 +221,7 @@
     1.4  $simp$, $blast$, or $auto$.  This would work as follows:
     1.5  \begin{matharray}{l}
     1.6    \LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\
     1.7 -  \quad \APPLY{unfold~defs} \quad \CMT{or ``$\APPLY{insert~facts}$''} \\
     1.8 +  \quad \APPLY{unfold~defs} \\
     1.9    \quad \APPLY{blast} \\
    1.10    \quad \DONE \\
    1.11  \end{matharray}
     2.1 --- a/doc-src/IsarRef/generic.tex	Tue Mar 05 18:54:55 2002 +0100
     2.2 +++ b/doc-src/IsarRef/generic.tex	Tue Mar 05 18:55:46 2002 +0100
     2.3 @@ -16,7 +16,7 @@
     2.4  interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic
     2.5  may make use of this light-weight mechanism of abstract theories
     2.6  \cite{Wenzel:1997:TPHOL}.  There is also a tutorial on using axiomatic type
     2.7 -classes in isabelle \cite{isabelle-axclass} that is part of the standard
     2.8 +classes in Isabelle \cite{isabelle-axclass} that is part of the standard
     2.9  Isabelle documentation.
    2.10  
    2.11  \begin{rail}
    2.12 @@ -27,7 +27,7 @@
    2.13  \end{rail}
    2.14  
    2.15  \begin{descr}
    2.16 -\item [$\AXCLASS~c \subseteq \vec c~axms$] defines an axiomatic type class as
    2.17 +\item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as
    2.18    the intersection of existing classes, with additional axioms holding.  Class
    2.19    axioms may not contain more than one type variable.  The class axioms (with
    2.20    implicit sort constraints added) are bound to the given names.  Furthermore
    2.21 @@ -37,7 +37,7 @@
    2.22    
    2.23    The ``axioms'' are stored as theorems according to the given name
    2.24    specifications, adding the class name $c$ as name space prefix; these facts
    2.25 -  are stored collectively as $c.axioms$, too.
    2.26 +  are stored collectively as $c{\dtt}axioms$, too.
    2.27    
    2.28  \item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a
    2.29    goal stating a class relation or type arity.  The proof would usually
    2.30 @@ -132,8 +132,8 @@
    2.31  \item [$\LOCALE~loc~=~import~+~body$] defines new locale $loc$ as a context
    2.32    consisting of a certain view of existing locales ($import$) plus some
    2.33    additional elements ($body$).  Both $import$ and $body$ are optional; the
    2.34 -  trivial $\LOCALE~loc$ defines an empty locale, which may still be useful to
    2.35 -  collect declarations of facts later on.  Type-inference on locale
    2.36 +  degenerate form $\LOCALE~loc$ defines an empty locale, which may still be
    2.37 +  useful to collect declarations of facts later on.  Type-inference on locale
    2.38    expressions automatically takes care of the most general typing that the
    2.39    combined context elements may acquire.
    2.40    
    2.41 @@ -299,16 +299,14 @@
    2.42  \end{matharray}
    2.43  
    2.44  \begin{rail}
    2.45 -  ('also' | 'finally') transrules?
    2.46 +  ('also' | 'finally') ('(' thmrefs ')')?
    2.47    ;
    2.48    'trans' (() | 'add' | 'del')
    2.49    ;
    2.50 -
    2.51 -  transrules: '(' thmrefs ')'
    2.52 -  ;
    2.53  \end{rail}
    2.54  
    2.55  \begin{descr}
    2.56 +  
    2.57  \item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as
    2.58    follows.  The first occurrence of $\ALSO$ in some calculational thread
    2.59    initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
    2.60 @@ -328,22 +326,23 @@
    2.61  \item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
    2.62    but collect results only, without applying rules.
    2.63    
    2.64 -\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity (and
    2.65 -  symmetry) rules declared in the current context.
    2.66 -
    2.67 +\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity
    2.68 +  rules (for calculational commands $\ALSO$ and $\FINALLY$) and symmetry rules
    2.69 +  (for the $symmetric$ operation and single step elimination patters) of the
    2.70 +  current context.
    2.71 +  
    2.72  \item [$trans$] declares theorems as transitivity rules.
    2.73    
    2.74 -\item [$sym$] declares symmetry rules, to be used either with the $symmetric$
    2.75 -  operation (see below), or in canonical single-step eliminations (such as
    2.76 -  ``$\ASSUME{}{x = y}~\HENCE{}{y = x}~\DDOT$'').
    2.77 -  
    2.78 -  Isabelle/Pure declares symmetry of $\equiv$, common object-logics add
    2.79 -  further standard rules, such as symmetry of $=$ and $\not=$.
    2.80 +\item [$sym$] declares symmetry rules.
    2.81    
    2.82  \item [$symmetric$] resolves a theorem with some rule declared as $sym$ in the
    2.83    current context.  For example, ``$\ASSUME{[symmetric]}{x = y}$'' produces a
    2.84    swapped fact derived from that assumption.
    2.85 -
    2.86 +  
    2.87 +  In structured proof texts it is often more appropriate to use an explicit
    2.88 +  single-step elimination proof, such as ``$\ASSUME{}{x = y}~\HENCE{}{y =
    2.89 +    x}~\DDOT$''.  Note that the very same rules known to $symmetric$ are
    2.90 +  declared as $elim$ at the same time.
    2.91  \end{descr}
    2.92  
    2.93  
    2.94 @@ -360,7 +359,7 @@
    2.95    insert & : & \isarmeth \\[0.5ex]
    2.96    erule^* & : & \isarmeth \\
    2.97    drule^* & : & \isarmeth \\
    2.98 -  frule^* & : & \isarmeth \\[0.5ex]
    2.99 +  frule^* & : & \isarmeth \\
   2.100    succeed & : & \isarmeth \\
   2.101    fail & : & \isarmeth \\
   2.102  \end{matharray}
   2.103 @@ -373,11 +372,14 @@
   2.104  \end{rail}
   2.105  
   2.106  \begin{descr}
   2.107 -\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
   2.108 -  meta-level definitions throughout all goals; any facts provided are inserted
   2.109 -  into the goal and subject to rewriting as well.
   2.110 +  
   2.111 +\item [$unfold~\vec a$ and $fold~\vec a$] expand (or fold back again) the
   2.112 +  given meta-level definitions throughout all goals; any chained facts
   2.113 +  provided are inserted into the goal and subject to rewriting as well.
   2.114 +  
   2.115  \item [$insert~\vec a$] inserts theorems as facts into all goals of the proof
   2.116    state.  Note that current facts indicated for forward chaining are ignored.
   2.117 +
   2.118  \item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the
   2.119    basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by
   2.120    elim-resolution, destruct-resolution, and forward-resolution, respectively
   2.121 @@ -390,17 +392,20 @@
   2.122    rather than via implicit proof state manipulations.  For example, a proper
   2.123    single-step elimination would be done using the basic $rule$ method, with
   2.124    forward chaining of current facts.
   2.125 +
   2.126  \item [$succeed$] yields a single (unchanged) result; it is the identity of
   2.127    the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
   2.128 +
   2.129  \item [$fail$] yields an empty result sequence; it is the identity of the
   2.130    ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
   2.131 +
   2.132  \end{descr}
   2.133  
   2.134  \indexisaratt{tagged}\indexisaratt{untagged}
   2.135  \indexisaratt{THEN}\indexisaratt{COMP}
   2.136  \indexisaratt{where}\indexisaratt{unfolded}\indexisaratt{folded}
   2.137  \indexisaratt{standard}\indexisaratt{elim-format}
   2.138 -\indexisaratt{no-vars}\indexisaratt{exported}
   2.139 +\indexisaratt{no-vars}
   2.140  \begin{matharray}{rcl}
   2.141    tagged & : & \isaratt \\
   2.142    untagged & : & \isaratt \\[0.5ex]
   2.143 @@ -412,7 +417,6 @@
   2.144    standard & : & \isaratt \\
   2.145    elim_format & : & \isaratt \\
   2.146    no_vars^* & : & \isaratt \\
   2.147 -  exported^* & : & \isaratt \\
   2.148  \end{matharray}
   2.149  
   2.150  \begin{rail}
   2.151 @@ -450,10 +454,6 @@
   2.152    see also the ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
   2.153  \item [$no_vars$] replaces schematic variables by free ones; this is mainly
   2.154    for tuning output of pretty printed theorems.
   2.155 -\item [$exported$] lifts a local result out of the current proof context,
   2.156 -  generalizing all fixed variables and discharging all assumptions.  Note that
   2.157 -  proper incremental export is already done as part of the basic Isar
   2.158 -  machinery.  This attribute is mainly for experimentation.
   2.159  \end{descr}
   2.160  
   2.161  
   2.162 @@ -547,7 +547,7 @@
   2.163    \cite[\S3]{isabelle-ref}).
   2.164  \item [$cut_tac$] inserts facts into the proof state as assumption of a
   2.165    subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}.  Note
   2.166 -  that the scope of schmatic variables is spread over the main goal statement.
   2.167 +  that the scope of schematic variables is spread over the main goal statement.
   2.168    Instantiations may be given as well, see also ML tactic
   2.169    \texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.
   2.170  \item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note
   2.171 @@ -567,7 +567,6 @@
   2.172    implicit theory context, the ML code may refer to the following locally
   2.173    bound values:
   2.174  
   2.175 -%%FIXME ttbox produces too much trailing space (why?)
   2.176  {\footnotesize\begin{verbatim}
   2.177  val ctxt  : Proof.context
   2.178  val facts : thm list
   2.179 @@ -637,7 +636,7 @@
   2.180  
   2.181  By default the Simplifier methods take local assumptions fully into account,
   2.182  using equational assumptions in the subsequent normalization process, or
   2.183 -simplifying assumptions themselvess (cf.\ \texttt{asm_full_simp_tac} in
   2.184 +simplifying assumptions themselves (cf.\ \texttt{asm_full_simp_tac} in
   2.185  \cite[\S10]{isabelle-ref}).  In structured proofs this is usually quite well
   2.186  behaved in practice: just the local premises of the actual goal are involved,
   2.187  additional facts may inserted via explicit forward-chaining (using $\THEN$,
   2.188 @@ -665,7 +664,7 @@
   2.189  \indexisarcmd{print-simpset}
   2.190  \indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
   2.191  \begin{matharray}{rcl}
   2.192 -  print_simpset^* & : & \isarkeep{theory~|~proof} \\
   2.193 +  \isarcmd{print_simpset}^* & : & \isarkeep{theory~|~proof} \\
   2.194    simp & : & \isaratt \\
   2.195    cong & : & \isaratt \\
   2.196    split & : & \isaratt \\
   2.197 @@ -677,12 +676,17 @@
   2.198  \end{rail}
   2.199  
   2.200  \begin{descr}
   2.201 -\item [$print_simpset$] prints the collection of rules declared to the
   2.202 -  Simplifier, which is also known as ``simpset'' internally
   2.203 +
   2.204 +\item [$\isarcmd{print_simpset}$] prints the collection of rules declared to
   2.205 +  the Simplifier, which is also known as ``simpset'' internally
   2.206    \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
   2.207 +
   2.208  \item [$simp$] declares simplification rules.
   2.209 +
   2.210  \item [$cong$] declares congruence rules.
   2.211 +
   2.212  \item [$split$] declares case split rules.
   2.213 +
   2.214  \end{descr}
   2.215  
   2.216  
   2.217 @@ -762,13 +766,13 @@
   2.218  
   2.219  \subsubsection{Basic methods}\label{sec:classical-basic}
   2.220  
   2.221 -\indexisarmeth{rule}\indexisarmeth{intro}
   2.222 -\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}
   2.223 +\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
   2.224 +\indexisarmeth{intro}\indexisarmeth{elim}
   2.225  \begin{matharray}{rcl}
   2.226    rule & : & \isarmeth \\
   2.227 +  contradiction & : & \isarmeth \\
   2.228    intro & : & \isarmeth \\
   2.229    elim & : & \isarmeth \\
   2.230 -  contradiction & : & \isarmeth \\
   2.231  \end{matharray}
   2.232  
   2.233  \begin{rail}
   2.234 @@ -777,13 +781,20 @@
   2.235  \end{rail}
   2.236  
   2.237  \begin{descr}
   2.238 +  
   2.239  \item [$rule$] as offered by the classical reasoner is a refinement over the
   2.240 -  primitive one (see \S\ref{sec:pure-meth-att}).  In case that no rules are
   2.241 -  provided as arguments, it automatically determines elimination and
   2.242 -  introduction rules from the context (see also \S\ref{sec:classical-mod}).
   2.243 -  This is made the default method for basic proof steps, such as $\PROOFNAME$
   2.244 -  and ``$\DDOT$'' (two dots), see also \S\ref{sec:proof-steps} and
   2.245 -  \S\ref{sec:pure-meth-att}.
   2.246 +  primitive one (see \S\ref{sec:pure-meth-att}).  Both versions essentially
   2.247 +  work the same, but the classical version observes the classical rule context
   2.248 +  in addition to the Isabelle/Pure one.
   2.249 +  
   2.250 +  The library of common object logics (HOL, ZF, etc.) usually declare a rich
   2.251 +  collection of classical rules (even if these perfectly OK from the
   2.252 +  intuitionistic viewpoint), but only few declarations to the rule context of
   2.253 +  Isabelle/Pure (\S\ref{sec:pure-meth-att}).
   2.254 +  
   2.255 +\item [$contradiction$] solves some goal by contradiction, deriving any result
   2.256 +  from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may
   2.257 +  appear in either order.
   2.258  
   2.259  \item [$intro$ and $elim$] repeatedly refine some goal by intro- or
   2.260    elim-resolution, after having inserted any facts.  Omitting the arguments
   2.261 @@ -792,10 +803,7 @@
   2.262    of what actually happens, thus it is very appropriate as an initial method
   2.263    for $\PROOFNAME$ that splits up certain connectives of the goal, before
   2.264    entering the actual sub-proof.
   2.265 -
   2.266 -\item [$contradiction$] solves some goal by contradiction, deriving any result
   2.267 -  from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may
   2.268 -  appear in either order.
   2.269 +  
   2.270  \end{descr}
   2.271  
   2.272  
   2.273 @@ -891,7 +899,7 @@
   2.274  \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
   2.275  \indexisaratt{iff}\indexisaratt{rule}
   2.276  \begin{matharray}{rcl}
   2.277 -  print_claset^* & : & \isarkeep{theory~|~proof} \\
   2.278 +  \isarcmd{print_claset}^* & : & \isarkeep{theory~|~proof} \\
   2.279    intro & : & \isaratt \\
   2.280    elim & : & \isaratt \\
   2.281    dest & : & \isaratt \\
   2.282 @@ -909,31 +917,31 @@
   2.283  \end{rail}
   2.284  
   2.285  \begin{descr}
   2.286 -\item [$print_claset$] prints the collection of rules declared to the
   2.287 -  Classical Reasoner, which is also known as ``simpset'' internally
   2.288 +
   2.289 +\item [$\isarcmd{print_claset}$] prints the collection of rules declared to
   2.290 +  the Classical Reasoner, which is also known as ``simpset'' internally
   2.291    \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
   2.292 +
   2.293  \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
   2.294    destruction rules, respectively.  By default, rules are considered as
   2.295    \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
   2.296    single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not
   2.297    applied in the search-oriented automated methods, but only in single-step
   2.298    methods such as $rule$).
   2.299 +
   2.300  \item [$rule~del$] deletes introduction, elimination, or destruction rules from
   2.301    the context.
   2.302 -\item [$iff$] declares a (possibly conditional) ``safe'' rule to the context in
   2.303 -  several ways.   The rule is declared as a rewrite rule to the Simplifier. 
   2.304 -  Furthermore, it is 
   2.305 -  declared in several ways (depending on its structure) to the Classical 
   2.306 -  Reasoner for aggressive use, which would normally be indicated by ``!'').
   2.307 -  If the rule is an equivalence, the two corresponding implications are 
   2.308 -  declared as introduction and destruction rules. Otherwise, 
   2.309 -  if the rule is an inequality, the corresponding negation elimination rule
   2.310 -  is declared, else the rule itself is declared as an introduction rule.
   2.311    
   2.312 -  The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only,
   2.313 -  and omits the Simplifier declaration.  Thus the declaration does not have
   2.314 -  any effect on automated proof tools, but only on simple methods such as
   2.315 -  $rule$ (see \S\ref{sec:misc-meth-att}).
   2.316 +\item [$iff$] declares a logical equivalences to the Simplifier and the
   2.317 +  Classical reasoner at the same time.  Non-conditional rules result in a
   2.318 +  ``safe'' introduction and elimination pair; conditional ones are considered
   2.319 +  ``unsafe''.  Rules with negative conclusion are automatically inverted
   2.320 +  (using $\neg$-elimination).
   2.321 +  
   2.322 +  The ``?'' version of $iff$ declares rules to the Pure context only, and
   2.323 +  omits the Simplifier declaration.  Thus the declaration does not have any
   2.324 +  effect on automated proof tools, but only on the single-step $rule$ method
   2.325 +  (see \S\ref{sec:misc-meth-att}).
   2.326  \end{descr}
   2.327  
   2.328  
   2.329 @@ -986,8 +994,11 @@
   2.330  \railterm{casenames}
   2.331  
   2.332  \begin{rail}
   2.333 -  'case' nameref attributes?
   2.334 +  'case' caseref | ('(' caseref ((name | underscore) +) ')')
   2.335    ;
   2.336 +  caseref: nameref attributes?
   2.337 +  ;
   2.338 +
   2.339    casenames (name + )
   2.340    ;
   2.341    'params' ((name * ) + 'and')
   2.342 @@ -1189,17 +1200,24 @@
   2.343    ;
   2.344  \end{rail}
   2.345  
   2.346 -The $cases$ and $induct$ attributes augment the corresponding context of rules
   2.347 -for reasoning about inductive sets and types.  The standard rules are already
   2.348 -declared by advanced definitional packages.  For special applications, these
   2.349 -may be replaced manually by variant versions.
   2.350 +\begin{descr}
   2.351 +  
   2.352 +\item [$\isarkeyword{print_induct_rules}$] prints cases and induct rules for
   2.353 +  sets and types of the current context.
   2.354  
   2.355 -Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:rule-cases}) to
   2.356 -adjust names of cases and parameters of a rule.
   2.357 -
   2.358 -The $consumes$ declaration (cf.\ \S\ref{sec:rule-cases}) is taken care of
   2.359 -automatically (if none had been given already): $consumes~0$ is specified for
   2.360 -``type'' rules and $consumes~1$ for ``set'' rules.
   2.361 +\item [$cases$ and $induct$] (as attributes) augment the corresponding context
   2.362 +  of rules for reasoning about inductive sets and types, using the
   2.363 +  corresponding methods of the same name.  Certain definitional packages of
   2.364 +  object-logics usually declare emerging cases and induction rules as
   2.365 +  expected, so users rarely need to intervene.
   2.366 +  
   2.367 +  Manual rule declarations usually include the the $case_names$ and $ps$
   2.368 +  attributes to adjust names of cases and parameters of a rule (see
   2.369 +  \S\ref{sec:rule-cases}); the $consumes$ declaration is taken care of
   2.370 +  automatically: $consumes~0$ is specified for ``type'' rules and $consumes~1$
   2.371 +  for ``set'' rules.
   2.372 +  
   2.373 +\end{descr}
   2.374  
   2.375  %%% Local Variables:
   2.376  %%% mode: latex
     3.1 --- a/doc-src/IsarRef/logics.tex	Tue Mar 05 18:54:55 2002 +0100
     3.2 +++ b/doc-src/IsarRef/logics.tex	Tue Mar 05 18:55:46 2002 +0100
     3.3 @@ -149,7 +149,7 @@
     3.4  \railterm{complete}
     3.5  
     3.6  \begin{rail}
     3.7 -  splitformat (((name * ) + 'and') | ('(' complete ')'))
     3.8 +  splitformat (((name *) + 'and') | ('(' complete ')'))
     3.9    ;
    3.10  \end{rail}
    3.11  
    3.12 @@ -396,12 +396,12 @@
    3.13  \begin{rail}
    3.14    'datatype' (dtspec + 'and')
    3.15    ;
    3.16 -  repdatatype (name * ) dtrules
    3.17 +  repdatatype (name *) dtrules
    3.18    ;
    3.19  
    3.20    dtspec: parname? typespec infix? '=' (cons + '|')
    3.21    ;
    3.22 -  cons: name (type * ) mixfix?
    3.23 +  cons: name (type *) mixfix?
    3.24    ;
    3.25    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
    3.26  \end{rail}
    3.27 @@ -421,8 +421,9 @@
    3.28  old-style theory syntax being used there!  Apart from proper proof methods for
    3.29  case-analysis and induction, there are also emulations of ML tactics
    3.30  \texttt{case_tac} and \texttt{induct_tac} available, see
    3.31 -\S\ref{sec:induct_tac}; these admit to refer directly to the internal
    3.32 -structure of subgoals (including internally bound parameters).
    3.33 +\S\ref{sec:hol-induct-tac} or \S\ref{sec:zf-induct-tac}; these admit to refer
    3.34 +directly to the internal structure of subgoals (including internally bound
    3.35 +parameters).
    3.36  
    3.37  
    3.38  \subsection{Recursive functions}\label{sec:recursion}
    3.39 @@ -432,8 +433,7 @@
    3.40    \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
    3.41    \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
    3.42    \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
    3.43 -%FIXME
    3.44 -%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
    3.45 +%  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\  %FIXME
    3.46  \end{matharray}
    3.47  
    3.48  \railalias{recdefsimp}{recdef\_simp}
    3.49 @@ -449,16 +449,16 @@
    3.50  \railterm{recdeftc}
    3.51  
    3.52  \begin{rail}
    3.53 -  'primrec' parname? (equation + )
    3.54 +  'primrec' parname? (equation +)
    3.55    ;
    3.56 -  'recdef' ('(' 'permissive' ')')? \\ name term (prop + ) hints?
    3.57 +  'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
    3.58    ;
    3.59    recdeftc thmdecl? tc
    3.60    ;
    3.61  
    3.62    equation: thmdecl? prop
    3.63    ;
    3.64 -  hints: '(' 'hints' (recdefmod * ) ')'
    3.65 +  hints: '(' 'hints' (recdefmod *) ')'
    3.66    ;
    3.67    recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
    3.68    ;
    3.69 @@ -467,23 +467,27 @@
    3.70  \end{rail}
    3.71  
    3.72  \begin{descr}
    3.73 +  
    3.74  \item [$\isarkeyword{primrec}$] defines primitive recursive functions over
    3.75 -  datatypes, see also \cite{isabelle-HOL} FIXME.
    3.76 +  datatypes, see also \cite{isabelle-HOL}.
    3.77 +  
    3.78  \item [$\isarkeyword{recdef}$] defines general well-founded recursive
    3.79 -  functions (using the TFL package), see also \cite{isabelle-HOL} FIXME.  The
    3.80 +  functions (using the TFL package), see also \cite{isabelle-HOL}.  The
    3.81    $(permissive)$ option tells TFL to recover from failed proof attempts,
    3.82    returning unfinished results.  The $recdef_simp$, $recdef_cong$, and
    3.83    $recdef_wf$ hints refer to auxiliary rules to be used in the internal
    3.84 -  automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\
    3.85 +  automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\ 
    3.86    \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier
    3.87 -  (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\
    3.88 +  (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ 
    3.89    \S\ref{sec:classical}).
    3.90 +  
    3.91  \item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
    3.92    termination condition number $i$ (default $1$) as generated by a
    3.93    $\isarkeyword{recdef}$ definition of constant $c$.
    3.94 -
    3.95 +  
    3.96    Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
    3.97    internal proofs without manual intervention.
    3.98 +
    3.99  \end{descr}
   3.100  
   3.101  Both kinds of recursive definitions accommodate reasoning by induction (cf.\
   3.102 @@ -533,9 +537,6 @@
   3.103    mono & : & \isaratt \\
   3.104  \end{matharray}
   3.105  
   3.106 -\railalias{condefs}{con\_defs}
   3.107 -\railterm{condefs}
   3.108 -
   3.109  \begin{rail}
   3.110    ('inductive' | 'coinductive') sets intros monos?
   3.111    ;
   3.112 @@ -557,8 +558,8 @@
   3.113    automated monotonicity proof of $\isarkeyword{inductive}$.
   3.114  \end{descr}
   3.115  
   3.116 -See \cite{isabelle-HOL} FIXME for further information on inductive definitions
   3.117 -in HOL.
   3.118 +See \cite{isabelle-HOL} for further information on inductive definitions in
   3.119 +HOL, but note that this covers the old-style theory format.
   3.120  
   3.121  
   3.122  \subsection{Arithmetic proof support}
   3.123 @@ -584,7 +585,7 @@
   3.124  performed by the Simplifier.
   3.125  
   3.126  
   3.127 -\subsection{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
   3.128 +\subsection{Cases and induction: emulating tactic scripts}\label{sec:hol-induct-tac}
   3.129  
   3.130  The following important tactical tools of Isabelle/HOL have been ported to
   3.131  Isar.  These should be never used in proper proof texts!
   3.132 @@ -681,7 +682,7 @@
   3.133  
   3.134    dmspec: typespec '=' (cons + '|')
   3.135    ;
   3.136 -  cons: name (type * ) mixfix?
   3.137 +  cons: name (type *) mixfix?
   3.138    ;
   3.139    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
   3.140  \end{rail}
   3.141 @@ -698,11 +699,142 @@
   3.142  
   3.143  \subsection{Type checking}
   3.144  
   3.145 -FIXME
   3.146 +The ZF logic is essentially untyped, so the concept of ``type checking'' is
   3.147 +performed as logical reasoning about set-membership statements.  A special
   3.148 +method assists users in this task; a version of this is already declared as a
   3.149 +``solver'' in the default Simplifier context.
   3.150 +
   3.151 +\indexisarcmd{print-tcset}\indexisaratt{typecheck}\indexisaratt{TC}
   3.152 +
   3.153 +\begin{matharray}{rcl}
   3.154 +  \isarcmd{print_tcset}^* & : & \isarkeep{theory~|~proof} \\
   3.155 +  typecheck & : & \isarmeth \\
   3.156 +  TC & : & \isaratt \\
   3.157 +\end{matharray}
   3.158 +
   3.159 +\begin{rail}
   3.160 +  'TC' (() | 'add' | 'del')
   3.161 +  ;
   3.162 +\end{rail}
   3.163 +
   3.164 +\begin{descr}
   3.165 +  
   3.166 +\item [$\isarcmd{print_tcset}$] prints the collection of typechecking rules of
   3.167 +  the current context.
   3.168 +  
   3.169 +  Note that the component built into the Simplifier only knows about those
   3.170 +  rules being declared globally in the theory!
   3.171 +  
   3.172 +\item [$typecheck$] attempts to solve any pending type-checking problems in
   3.173 +  subgoals.
   3.174 +  
   3.175 +\item [$TC$] adds or deletes type-checking rules from the context.
   3.176 +
   3.177 +\end{descr}
   3.178 +
   3.179 +
   3.180 +\subsection{(Co)Inductive sets and datatypes}
   3.181 +
   3.182 +\subsubsection{Set definitions}
   3.183 +
   3.184 +In ZF everything is a set.  The generic inductive package also provides a
   3.185 +specific view for ``datatype'' specifications.  Coinductive definitions are
   3.186 +available as well.
   3.187 +
   3.188 +\indexisarcmdof{ZF}{inductive}\indexisarcmdof{ZF}{coinductive}
   3.189 +\indexisarcmdof{ZF}{datatype}\indexisarcmdof{ZF}{codatatype}
   3.190 +\begin{matharray}{rcl}
   3.191 +  \isarcmd{inductive} & : & \isartrans{theory}{theory} \\
   3.192 +  \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\
   3.193 +  \isarcmd{datatype} & : & \isartrans{theory}{theory} \\
   3.194 +  \isarcmd{codatatype} & : & \isartrans{theory}{theory} \\
   3.195 +\end{matharray}
   3.196 +
   3.197 +\railalias{CONDEFS}{con\_defs}
   3.198 +\railterm{CONDEFS}
   3.199 +
   3.200 +\railalias{TYPEINTROS}{type\_intros}
   3.201 +\railterm{TYPEINTROS}
   3.202 +
   3.203 +\railalias{TYPEELIMS}{type\_elims}
   3.204 +\railterm{TYPEELIMS}
   3.205 +
   3.206 +\begin{rail}
   3.207 +  ('inductive' | 'coinductive') domains intros hints
   3.208 +  ;
   3.209  
   3.210 -\subsection{Inductive sets and datatypes}
   3.211 +  domains: 'domains' (term + '+') ('<=' | subseteq) term
   3.212 +  ;
   3.213 +  intros: 'intros' (thmdecl? prop +)
   3.214 +  ;
   3.215 +  hints: monos? condefs? typeintros? typeelims?
   3.216 +  ;
   3.217 +  monos: ('monos' thmrefs)?
   3.218 +  ;
   3.219 +  condefs: (CONDEFS thmrefs)?
   3.220 +  ;
   3.221 +  typeintros: (TYPEINTROS thmrefs)?
   3.222 +  ;
   3.223 +  typeelims: (TYPEELIMS thmrefs)?
   3.224 +  ;
   3.225 +\end{rail}
   3.226 +
   3.227 +In the following diagram $monos$, $typeintros$, and $typeelims$ are the same
   3.228 +as above.
   3.229 +
   3.230 +\begin{rail}
   3.231 +  ('datatype' | 'codatatype') domain? (dtspec + 'and') hints
   3.232 +  ;
   3.233 +
   3.234 +  domain: ('<=' | subseteq) term
   3.235 +  ;
   3.236 +  dtspec: term '=' (con + '|')
   3.237 +  ;
   3.238 +  con: name ('(' (term ',' +) ')')?  
   3.239 +  ;
   3.240 +  hints: monos? typeintros? typeelims?
   3.241 +  ;
   3.242 +\end{rail}
   3.243 +
   3.244 +See \cite{isabelle-ZF} for further information on inductive definitions in
   3.245 +HOL, but note that this covers the old-style theory format.
   3.246  
   3.247 -FIXME
   3.248 +
   3.249 +\subsubsection{Primitive recursive functions}
   3.250 +
   3.251 +\indexisarcmdof{ZF}{primrec}
   3.252 +\begin{matharray}{rcl}
   3.253 +  \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
   3.254 +\end{matharray}
   3.255 +
   3.256 +\begin{rail}
   3.257 +  'primrec' (thmdecl? prop +)
   3.258 +  ;
   3.259 +\end{rail}
   3.260 +
   3.261 +
   3.262 +\subsubsection{Cases and induction: emulating tactic scripts}\label{sec:zf-induct-tac}
   3.263 +
   3.264 +The following important tactical tools of Isabelle/ZF have been ported to
   3.265 +Isar.  These should be never used in proper proof texts!
   3.266 +
   3.267 +\indexisarmethof{ZF}{case-tac}\indexisarmethof{ZF}{induct-tac}
   3.268 +\indexisarmethof{ZF}{ind-cases}\indexisarcmdof{ZF}{inductive-cases}
   3.269 +\begin{matharray}{rcl}
   3.270 +  case_tac^* & : & \isarmeth \\
   3.271 +  induct_tac^* & : & \isarmeth \\
   3.272 +  ind_cases^* & : & \isarmeth \\
   3.273 +  \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\
   3.274 +\end{matharray}
   3.275 +
   3.276 +\begin{rail}
   3.277 +  (casetac | inducttac) goalspec? name
   3.278 +  ;
   3.279 +  indcases (prop +)
   3.280 +  ;
   3.281 +  inductivecases (thmdecl? (prop +) + 'and')
   3.282 +  ;
   3.283 +\end{rail}
   3.284  
   3.285  
   3.286  %%% Local Variables:
     4.1 --- a/doc-src/IsarRef/pure.tex	Tue Mar 05 18:54:55 2002 +0100
     4.2 +++ b/doc-src/IsarRef/pure.tex	Tue Mar 05 18:55:46 2002 +0100
     4.3 @@ -291,19 +291,20 @@
     4.4  \end{rail}
     4.5  
     4.6  \begin{descr}
     4.7 +  
     4.8  \item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,
     4.9    except that the actual logical signature extension is omitted.  Thus the
    4.10    context free grammar of Isabelle's inner syntax may be augmented in
    4.11    arbitrary ways, independently of the logic.  The $mode$ argument refers to
    4.12 -  the print mode that the grammar rules belong; unless the \texttt{output}
    4.13 -  flag is given, all productions are added both to the input and output
    4.14 -  grammar.
    4.15 +  the print mode that the grammar rules belong; unless the
    4.16 +  $\isarkeyword{output}$ indicator is given, all productions are added both to
    4.17 +  the input and output grammar.
    4.18 +  
    4.19  \item [$\isarkeyword{translations}~rules$] specifies syntactic translation
    4.20 -  rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==} or
    4.21 -  \isasymrightleftharpoons), parse rules (\texttt{=>} or
    4.22 -  \isasymrightharpoonup), or print rules (\texttt{<=} or
    4.23 -  \isasymleftharpoondown).  Translation patterns may be prefixed by the
    4.24 -  syntactic category to be used for parsing; the default is \texttt{logic}.
    4.25 +  rules (i.e.\ macros): parse~/ print rules (\isasymrightleftharpoons), parse
    4.26 +  rules (\isasymrightharpoonup), or print rules (\isasymleftharpoondown).
    4.27 +  Translation patterns may be prefixed by the syntactic category to be used
    4.28 +  for parsing; the default is $logic$.
    4.29  \end{descr}
    4.30  
    4.31  
    4.32 @@ -333,7 +334,7 @@
    4.33    Everyday work is typically done the hard way, with proper definitions and
    4.34    actual proven theorems.
    4.35    
    4.36 -\item [$\isarkeyword{lemmas}~a = \vec b$] restrieves and stores existing facts
    4.37 +\item [$\isarkeyword{lemmas}~a = \vec b$] retrieves and stores existing facts
    4.38    in the theory context, or the specified locale (see also
    4.39    \S\ref{sec:locale}).  Typical applications would also involve attributes, to
    4.40    declare Simplifier rules, for example.
    4.41 @@ -933,43 +934,59 @@
    4.42  object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and
    4.43  \ref{ch:logics}).
    4.44  
    4.45 -\indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$-$}
    4.46 -\indexisaratt{OF}\indexisaratt{of}
    4.47 +\indexisarmeth{$-$}\indexisarmeth{assumption}
    4.48 +\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{rules}
    4.49  \indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
    4.50  \indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
    4.51 +\indexisaratt{OF}\indexisaratt{of}
    4.52  \begin{matharray}{rcl}
    4.53 +  - & : & \isarmeth \\
    4.54    assumption & : & \isarmeth \\
    4.55    this & : & \isarmeth \\
    4.56    rule & : & \isarmeth \\
    4.57 -  - & : & \isarmeth \\
    4.58 -  OF & : & \isaratt \\
    4.59 -  of & : & \isaratt \\
    4.60 +  rules & : & \isarmeth \\[0.5ex]
    4.61    intro & : & \isaratt \\
    4.62    elim & : & \isaratt \\
    4.63    dest & : & \isaratt \\
    4.64 -  rule & : & \isaratt \\
    4.65 +  rule & : & \isaratt \\[0.5ex]
    4.66 +  OF & : & \isaratt \\
    4.67 +  of & : & \isaratt \\
    4.68  \end{matharray}
    4.69  
    4.70 -%FIXME intro!, intro, intro?
    4.71 -
    4.72  \begin{rail}
    4.73    'rule' thmrefs?
    4.74    ;
    4.75 +  'rules' ('!' ?) (rulemod *)
    4.76 +  ;
    4.77 +  rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
    4.78 +  ;
    4.79 +  ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
    4.80 +  ;
    4.81 +  'rule' 'del'
    4.82 +  ;
    4.83    'OF' thmrefs
    4.84    ;
    4.85    'of' insts ('concl' ':' insts)?
    4.86    ;
    4.87 -  'rule' 'del'
    4.88 -  ;
    4.89  \end{rail}
    4.90  
    4.91  \begin{descr}
    4.92 +  
    4.93 +\item [``$-$''] does nothing but insert the forward chaining facts as premises
    4.94 +  into the goal.  Note that command $\PROOFNAME$ without any method actually
    4.95 +  performs a single reduction step using the $rule$ method; thus a plain
    4.96 +  \emph{do-nothing} proof step would be $\PROOF{-}$ rather than $\PROOFNAME$
    4.97 +  alone.
    4.98 +  
    4.99  \item [$assumption$] solves some goal by a single assumption step.  Any facts
   4.100    given (${} \le 1$) are guaranteed to participate in the refinement.  Recall
   4.101    that $\QEDNAME$ (see \S\ref{sec:proof-steps}) already concludes any
   4.102 -  remaining sub-goals by assumption.
   4.103 +  remaining sub-goals by assumption, so structured proofs usually need not
   4.104 +  quote the $assumption$ method at all.
   4.105 +  
   4.106  \item [$this$] applies all of the current facts directly as rules.  Recall
   4.107    that ``$\DOT$'' (dot) abbreviates $\BY{this}$.
   4.108 +  
   4.109  \item [$rule~\vec a$] applies some rule given as argument in backward manner;
   4.110    facts are used to reduce the rule before applying it to the goal.  Thus
   4.111    $rule$ without facts is plain \emph{introduction}, while with facts it
   4.112 @@ -980,27 +997,41 @@
   4.113    $elim$, $dest$ attributes (see below).  This is the default behavior of
   4.114    $\PROOFNAME$ and ``$\DDOT$'' (double-dot) steps (see
   4.115    \S\ref{sec:proof-steps}).
   4.116 -\item [``$-$''] does nothing but insert the forward chaining facts as premises
   4.117 -  into the goal.  Note that command $\PROOFNAME$ without any method actually
   4.118 -  performs a single reduction step using the $rule$ method; thus a plain
   4.119 -  \emph{do-nothing} proof step would be $\PROOF{-}$ rather than $\PROOFNAME$
   4.120 -  alone.
   4.121 +  
   4.122 +\item [$rules$] performs intuitionistic proof search, depending on
   4.123 +  specifically declared rules from the context, or given as explicit
   4.124 +  arguments.  Chained facts are inserted into the goal before commencing proof
   4.125 +  search; $rules!$ means to include the current $prems$ as well.
   4.126 +  
   4.127 +  Rules need to be classified as $intro$, $elim$, or $dest$; here the ``$!$''
   4.128 +  indicator refers to ``safe'' rules, which may be applied aggressively
   4.129 +  (without considering back-tracking later).  Rules declared with ``$?$'' are
   4.130 +  ignored in proof search (the single-step $rule$ method still observes
   4.131 +  these).  An explicit weight annotation may be given as well; otherwise the
   4.132 +  number of rule premises will be taken into account.
   4.133 +
   4.134 +\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
   4.135 +  destruct rules, to be used with the $rule$ and $rules$ methods.  Note that
   4.136 +  the latter will ignore rules declare with ``$?$'', while ``$!$'' are used
   4.137 +  most aggressively.
   4.138 +  
   4.139 +  The classical reasoner (see \S\ref{sec:classical-basic}) introduces its own
   4.140 +  variants of these attributes; use qualified names to access the present
   4.141 +  versions of Isabelle/Pure, i.e.\ $Pure{\dtt}intro$ or $CPure{\dtt}intro$.
   4.142 +  
   4.143 +\item [$rule~del$] undeclares introduction, elimination, or destruct rules.
   4.144 +  
   4.145  \item [$OF~\vec a$] applies some theorem to given rules $\vec a$ (in
   4.146    parallel).  This corresponds to the \texttt{MRS} operator in ML
   4.147    \cite[\S5]{isabelle-ref}, but note the reversed order.  Positions may be
   4.148    skipped by including ``$\_$'' (underscore) as argument.
   4.149 +  
   4.150  \item [$of~\vec t$] performs positional instantiation.  The terms $\vec t$ are
   4.151    substituted for any schematic variables occurring in a theorem from left to
   4.152    right; ``\texttt{_}'' (underscore) indicates to skip a position.  Arguments
   4.153    following a ``$concl\colon$'' specification refer to positions of the
   4.154    conclusion of a rule.
   4.155 -\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
   4.156 -  destruct rules, respectively.  Note that the classical reasoner (see
   4.157 -  \S\ref{sec:classical-basic}) introduces different versions of these
   4.158 -  attributes, and the $rule$ method, too.  In object-logics with classical
   4.159 -  reasoning enabled, the latter version should be used all the time to avoid
   4.160 -  confusion!
   4.161 -\item [$rule~del$] undeclares introduction, elimination, or destruct rules.
   4.162 +  
   4.163  \end{descr}
   4.164  
   4.165  
     5.1 --- a/doc-src/IsarRef/refcard.tex	Tue Mar 05 18:54:55 2002 +0100
     5.2 +++ b/doc-src/IsarRef/refcard.tex	Tue Mar 05 18:55:46 2002 +0100
     5.3 @@ -23,7 +23,9 @@
     5.4    theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\
     5.5    & \Or & \LEMMA{name}{prop}~proof \\
     5.6    & \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex]
     5.7 -  proof & = & \PROOF{method}~stmt^*~\QED{method} \\[1ex]
     5.8 +  proof & = & prfx^*~\PROOF{method}~stmt^*~\QED{method} \\[1ex]
     5.9 +  prfx & = & \APPLY{method} \\
    5.10 +  & \Or & \USING{name^+} \\
    5.11    stmt & = & \BG~stmt^*~\EN \\
    5.12    & \Or & \NEXT \\
    5.13    & \Or & \NOTE{name}{name^+} \\
    5.14 @@ -31,8 +33,8 @@
    5.15    & \Or & \FIX{var^+} \\
    5.16    & \Or & \ASSUME{name}{prop^+}\\
    5.17    & \Or & \THEN~goal{\dsh}stmt \\
    5.18 -  & \Or & goal{\dsh}stmt \\
    5.19 -  goal{\dsh}stmt & = & \HAVE{name}{prop}~proof \\
    5.20 +  & \Or & goal \\
    5.21 +  goal & = & \HAVE{name}{prop}~proof \\
    5.22    & \Or & \SHOW{name}{prop}~proof \\
    5.23  \end{matharray}
    5.24  
    5.25 @@ -104,6 +106,7 @@
    5.26    $unfold~\vec a$ & \Text{definitions} \\[2ex]
    5.27  
    5.28    \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
    5.29 +  $rules$ & \Text{intuitionistic proof search} \\
    5.30    $simp$, $simp_all$ & Simplifier (+ Splitter) \\
    5.31    $blast$, $fast$ & Classical Reasoner \\
    5.32    $auto$, $force$ & Simplifier + Classical Reasoner \\