doc-src/IsarRef/hol.tex
changeset 11691 fc9bd420162c
parent 11662 744399c9dd6a
child 12618 43a97a2155d0
     1.1 --- a/doc-src/IsarRef/hol.tex	Thu Oct 04 16:07:43 2001 +0200
     1.2 +++ b/doc-src/IsarRef/hol.tex	Thu Oct 04 16:09:12 2001 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4  \end{descr}
     1.5  
     1.6  
     1.7 -\section{Primitive types}
     1.8 +\section{Primitive types}\label{sec:typedef}
     1.9  
    1.10  \indexisarcmd{typedecl}\indexisarcmd{typedef}
    1.11  \begin{matharray}{rcl}
    1.12 @@ -140,7 +140,7 @@
    1.13  \S\ref{sec:induct_tac}.
    1.14  
    1.15  
    1.16 -\section{Recursive functions}
    1.17 +\section{Recursive functions}\label{sec:recursion}
    1.18  
    1.19  \indexisarcmd{primrec}\indexisarcmd{recdef}\indexisarcmd{recdef-tc}
    1.20  \begin{matharray}{rcl}
    1.21 @@ -278,190 +278,33 @@
    1.22  HOL.
    1.23  
    1.24  
    1.25 -\section{Proof by cases and induction}\label{sec:induct-method}
    1.26 -%FIXME move to generic.tex
    1.27 -
    1.28 -\subsection{Proof methods}\label{sec:induct-method-proper}
    1.29 +\section{Arithmetic}
    1.30  
    1.31 -\indexisarmeth{cases}\indexisarmeth{induct}
    1.32 +\indexisarmeth{arith}\indexisaratt{arith-split}
    1.33  \begin{matharray}{rcl}
    1.34 -  cases & : & \isarmeth \\
    1.35 -  induct & : & \isarmeth \\
    1.36 +  arith & : & \isarmeth \\
    1.37 +  arith_split & : & \isaratt \\
    1.38  \end{matharray}
    1.39  
    1.40 -The $cases$ and $induct$ methods provide a uniform interface to case analysis
    1.41 -and induction over datatypes, inductive sets, and recursive functions.  The
    1.42 -corresponding rules may be specified and instantiated in a casual manner.
    1.43 -Furthermore, these methods provide named local contexts that may be invoked
    1.44 -via the $\CASENAME$ proof command within the subsequent proof text (cf.\ 
    1.45 -\S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
    1.46 -about large specifications.
    1.47 -
    1.48  \begin{rail}
    1.49 -  'cases' ('(' 'simplified' ')')? spec
    1.50 -  ;
    1.51 -  'induct' ('(' 'stripped' ')')? spec
    1.52 -  ;
    1.53 -
    1.54 -  spec: open? args rule? params?
    1.55 -  ;
    1.56 -  open: '(' 'open' ')'
    1.57 -  ;
    1.58 -  args: (insts * 'and') 
    1.59 -  ;
    1.60 -  rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
    1.61 -  ;
    1.62 -  params: 'of' ':' insts
    1.63 +  'arith' '!'?
    1.64    ;
    1.65  \end{rail}
    1.66  
    1.67 -\begin{descr}
    1.68 -\item [$cases~insts~R~ps$] applies method $rule$ with an appropriate case
    1.69 -  distinction theorem, instantiated to the subjects $insts$.  Symbolic case
    1.70 -  names are bound according to the rule's local contexts.
    1.71 -  
    1.72 -  The rule is determined as follows, according to the facts and arguments
    1.73 -  passed to the $cases$ method:
    1.74 -  \begin{matharray}{llll}
    1.75 -    \Text{facts}    &       & \Text{arguments} & \Text{rule} \\\hline
    1.76 -                    & cases &           & \Text{classical case split} \\
    1.77 -                    & cases & t         & \Text{datatype exhaustion (type of $t$)} \\
    1.78 -    \edrv a \in A   & cases & \dots     & \Text{inductive set elimination (of $A$)} \\
    1.79 -    \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
    1.80 -  \end{matharray}
    1.81 -  
    1.82 -  Several instantiations may be given, referring to the \emph{suffix} of
    1.83 -  premises of the case rule; within each premise, the \emph{prefix} of
    1.84 -  variables is instantiated.  In most situations, only a single term needs to
    1.85 -  be specified; this refers to the first variable of the last premise (it is
    1.86 -  usually the same for all cases).
    1.87 -  
    1.88 -  Additional parameters may be specified as $ps$; these are applied after the
    1.89 -  primary instantiation in the same manner as by the $of$ attribute (cf.\ 
    1.90 -  \S\ref{sec:pure-meth-att}).  This feature is rarely needed in practice; a
    1.91 -  typical application would be to specify additional arguments for rules
    1.92 -  stemming from parameterized inductive definitions (see also
    1.93 -  \S\ref{sec:inductive}).
    1.94 +The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
    1.95 +$real$).  Any current facts are inserted into the goal before running the
    1.96 +procedure.  The ``!''~argument causes the full context of assumptions to be
    1.97 +included.  The $arith_split$ attribute declares case split rules to be
    1.98 +expanded before the arithmetic procedure is invoked.
    1.99  
   1.100 -  The $simplified$ option causes ``obvious cases'' of the rule to be solved
   1.101 -  beforehand, while the others are left unscathed.
   1.102 -  
   1.103 -  The $open$ option causes the parameters of the new local contexts to be
   1.104 -  exposed to the current proof context.  Thus local variables stemming from
   1.105 -  distant parts of the theory development may be introduced in an implicit
   1.106 -  manner, which can be quite confusing to the reader.  Furthermore, this
   1.107 -  option may cause unwanted hiding of existing local variables, resulting in
   1.108 -  less robust proof texts.
   1.109 -  
   1.110 -\item [$induct~insts~R~ps$] is analogous to the $cases$ method, but refers to
   1.111 -  induction rules, which are determined as follows:
   1.112 -  \begin{matharray}{llll}
   1.113 -    \Text{facts}    &        & \Text{arguments} & \Text{rule} \\\hline
   1.114 -                    & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
   1.115 -    \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\
   1.116 -    \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
   1.117 -  \end{matharray}
   1.118 -  
   1.119 -  Several instantiations may be given, each referring to some part of a mutual
   1.120 -  inductive definition or datatype --- only related partial induction rules
   1.121 -  may be used together, though.  Any of the lists of terms $P, x, \dots$
   1.122 -  refers to the \emph{suffix} of variables present in the induction rule.
   1.123 -  This enables the writer to specify only induction variables, or both
   1.124 -  predicates and variables, for example.
   1.125 -  
   1.126 -  Additional parameters may be given in the same way as for $cases$.
   1.127 -  
   1.128 -  The $stripped$ option causes implications and (bounded) universal
   1.129 -  quantifiers to be removed from each new subgoal emerging from the
   1.130 -  application of the induction rule.  This accommodates special applications
   1.131 -  of ``strengthened induction predicates''.  This option is rarely needed, the
   1.132 -  $induct$ method already handles proper rules appropriately by default.
   1.133 -  
   1.134 -  The $open$ option has the same effect as for the $cases$ method, see above.
   1.135 -\end{descr}
   1.136 -
   1.137 -Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
   1.138 -determined by the instantiated rule \emph{before} it has been applied to the
   1.139 -internal proof state.\footnote{As a general principle, Isar proof text may
   1.140 -  never refer to parts of proof states directly.} Thus proper use of symbolic
   1.141 -cases usually require the rule to be instantiated fully, as far as the
   1.142 -emerging local contexts and subgoals are concerned.  In particular, for
   1.143 -induction both the predicates and variables have to be specified.  Otherwise
   1.144 -the $\CASENAME$ command would refuse to invoke cases containing schematic
   1.145 -variables.  Furthermore the resulting local goal statement is bound to the
   1.146 -term variable $\Var{case}$\indexisarvar{case} --- for each case where it is
   1.147 -fully specified.
   1.148 -
   1.149 -The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named
   1.150 -cases present in the current proof state.
   1.151 -
   1.152 -\medskip
   1.153 -
   1.154 -It is important to note that there is a fundamental difference of the $cases$
   1.155 -and $induct$ methods in handling of non-atomic goal statements: $cases$ just
   1.156 -applies a certain rule in backward fashion, splitting the result into new
   1.157 -goals with the local contexts being augmented in a purely monotonic manner.
   1.158 -
   1.159 -In contrast, $induct$ passes the full goal statement through the ``recursive''
   1.160 -course involved in the induction.  Thus the original statement is basically
   1.161 -replaced by separate copies, corresponding to the induction hypotheses and
   1.162 -conclusion; the original goal context is no longer available.  This behavior
   1.163 -allows \emph{strengthened induction predicates} to be expressed concisely as
   1.164 -meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp \psi$ to
   1.165 -indicate ``variable'' parameters $\vec x$ and ``recursive'' assumptions
   1.166 -$\vec\phi$.  Also note that local definitions may be expressed as $\All{\vec
   1.167 -  x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
   1.168 -
   1.169 -\medskip
   1.170 -
   1.171 -Facts presented to either method are consumed according to the number of
   1.172 -``major premises'' of the rule involved (see also \S\ref{sec:induct-att} and
   1.173 -\S\ref{sec:cases}), which is usually $0$ for plain cases and induction rules
   1.174 -of datatypes etc.\ and $1$ for rules of inductive sets and the like.  The
   1.175 -remaining facts are inserted into the goal verbatim before the actual $cases$
   1.176 -or $induct$ rule is applied (thus facts may be even passed through an
   1.177 -induction).
   1.178 -
   1.179 -Note that whenever facts are present, the default rule selection scheme would
   1.180 -provide a ``set'' rule only, with the first fact consumed and the rest
   1.181 -inserted into the goal.  In order to pass all facts into a ``type'' rule
   1.182 -instead, one would have to specify this explicitly, e.g.\ by appending
   1.183 -``$type: name$'' to the method argument.
   1.184 +Note that a simpler (but faster) version of arithmetic reasoning is already
   1.185 +performed by the Simplifier.
   1.186  
   1.187  
   1.188 -\subsection{Declaring rules}\label{sec:induct-att}
   1.189 -
   1.190 -\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
   1.191 -\begin{matharray}{rcl}
   1.192 -  \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\
   1.193 -  cases & : & \isaratt \\
   1.194 -  induct & : & \isaratt \\
   1.195 -\end{matharray}
   1.196 -
   1.197 -\begin{rail}
   1.198 -  'cases' spec
   1.199 -  ;
   1.200 -  'induct' spec
   1.201 -  ;
   1.202 +\section{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
   1.203  
   1.204 -  spec: ('type' | 'set') ':' nameref
   1.205 -  ;
   1.206 -\end{rail}
   1.207 -
   1.208 -The $cases$ and $induct$ attributes augment the corresponding context of rules
   1.209 -for reasoning about inductive sets and types.  The standard rules are already
   1.210 -declared by HOL definitional packages.  For special applications, these may be
   1.211 -replaced manually by variant versions.
   1.212 -
   1.213 -Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:cases}) to
   1.214 -adjust names of cases and parameters of a rule.
   1.215 -
   1.216 -The $consumes$ declaration (cf.\ \S\ref{sec:cases}) is taken care of
   1.217 -automatically (if none had been given already): $consumes~0$ is specified for
   1.218 -``type'' rules and $consumes~1$ for ``set'' rules.
   1.219 -
   1.220 -
   1.221 -\subsection{Emulating tactic scripts}\label{sec:induct_tac}
   1.222 +The following important tactical tools of Isabelle/HOL have been ported to
   1.223 +Isar.  These should be never used in proper proof texts!
   1.224  
   1.225  \indexisarmeth{case-tac}\indexisarmeth{induct-tac}
   1.226  \indexisarmeth{ind-cases}\indexisarcmd{inductive-cases}
   1.227 @@ -510,9 +353,7 @@
   1.228    
   1.229  \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
   1.230    to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
   1.231 -  forward manner, unlike the proper $cases$ method (see
   1.232 -  \S\ref{sec:induct-method-proper}) which requires simplified cases to be
   1.233 -  solved completely.
   1.234 +  forward manner.
   1.235    
   1.236    While $ind_cases$ is a proof method to apply the result immediately as
   1.237    elimination rules, $\isarkeyword{inductive_cases}$ provides case split
   1.238 @@ -520,29 +361,6 @@
   1.239  \end{descr}
   1.240  
   1.241  
   1.242 -\section{Arithmetic}
   1.243 -
   1.244 -\indexisarmeth{arith}\indexisaratt{arith-split}
   1.245 -\begin{matharray}{rcl}
   1.246 -  arith & : & \isarmeth \\
   1.247 -  arith_split & : & \isaratt \\
   1.248 -\end{matharray}
   1.249 -
   1.250 -\begin{rail}
   1.251 -  'arith' '!'?
   1.252 -  ;
   1.253 -\end{rail}
   1.254 -
   1.255 -The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
   1.256 -$real$).  Any current facts are inserted into the goal before running the
   1.257 -procedure.  The ``!''~argument causes the full context of assumptions to be
   1.258 -included.  The $arith_split$ attribute declares case split rules to be
   1.259 -expanded before the arithmetic procedure is invoked.
   1.260 -
   1.261 -Note that a simpler (but faster) version of arithmetic reasoning is already
   1.262 -performed by the Simplifier.
   1.263 -
   1.264 -
   1.265  %%% Local Variables: 
   1.266  %%% mode: latex
   1.267  %%% TeX-master: "isar-ref"