induct/cases made generic, removed simplified/stripped options;
authorwenzelm
Thu Oct 04 16:09:12 2001 +0200 (2001-10-04)
changeset 11691fc9bd420162c
parent 11690 cb64368fb405
child 11692 6d15ae4b1123
induct/cases made generic, removed simplified/stripped options;
doc-src/IsarRef/generic.tex
doc-src/IsarRef/hol.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Thu Oct 04 16:07:43 2001 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Thu Oct 04 16:09:12 2001 +0200
     1.3 @@ -854,6 +854,182 @@
     1.4  \end{descr}
     1.5  
     1.6  
     1.7 +\section{Proof by cases and induction}\label{sec:induct-method}
     1.8 +
     1.9 +\subsection{Proof methods}\label{sec:induct-method-proper}
    1.10 +
    1.11 +\indexisarmeth{cases}\indexisarmeth{induct}
    1.12 +\begin{matharray}{rcl}
    1.13 +  cases & : & \isarmeth \\
    1.14 +  induct & : & \isarmeth \\
    1.15 +\end{matharray}
    1.16 +
    1.17 +The $cases$ and $induct$ methods provide a uniform interface to case analysis
    1.18 +and induction over datatypes, inductive sets, and recursive functions.  The
    1.19 +corresponding rules may be specified and instantiated in a casual manner.
    1.20 +Furthermore, these methods provide named local contexts that may be invoked
    1.21 +via the $\CASENAME$ proof command within the subsequent proof text (cf.\ 
    1.22 +\S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
    1.23 +about large specifications.
    1.24 +
    1.25 +Note that the full spectrum of this generic functionality is currently only
    1.26 +supported by Isabelle/HOL, when used in conjunction with advanced definitional
    1.27 +packages (see especially \S\ref{sec:datatype} and \S\ref{sec:inductive}).
    1.28 +
    1.29 +\begin{rail}
    1.30 +  'cases' spec
    1.31 +  ;
    1.32 +  'induct' spec
    1.33 +  ;
    1.34 +
    1.35 +  spec: open? args rule? params?
    1.36 +  ;
    1.37 +  open: '(' 'open' ')'
    1.38 +  ;
    1.39 +  args: (insts * 'and') 
    1.40 +  ;
    1.41 +  rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
    1.42 +  ;
    1.43 +  params: 'of' ':' insts
    1.44 +  ;
    1.45 +\end{rail}
    1.46 +
    1.47 +\begin{descr}
    1.48 +\item [$cases~insts~R~ps$] applies method $rule$ with an appropriate case
    1.49 +  distinction theorem, instantiated to the subjects $insts$.  Symbolic case
    1.50 +  names are bound according to the rule's local contexts.
    1.51 +  
    1.52 +  The rule is determined as follows, according to the facts and arguments
    1.53 +  passed to the $cases$ method:
    1.54 +  \begin{matharray}{llll}
    1.55 +    \Text{facts}    &       & \Text{arguments} & \Text{rule} \\\hline
    1.56 +                    & cases &           & \Text{classical case split} \\
    1.57 +                    & cases & t         & \Text{datatype exhaustion (type of $t$)} \\
    1.58 +    \edrv a \in A   & cases & \dots     & \Text{inductive set elimination (of $A$)} \\
    1.59 +    \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
    1.60 +  \end{matharray}
    1.61 +  
    1.62 +  Several instantiations may be given, referring to the \emph{suffix} of
    1.63 +  premises of the case rule; within each premise, the \emph{prefix} of
    1.64 +  variables is instantiated.  In most situations, only a single term needs to
    1.65 +  be specified; this refers to the first variable of the last premise (it is
    1.66 +  usually the same for all cases).
    1.67 +  
    1.68 +  Additional parameters may be specified as $ps$; these are applied after the
    1.69 +  primary instantiation in the same manner as by the $of$ attribute (cf.\ 
    1.70 +  \S\ref{sec:pure-meth-att}).  This feature is rarely needed in practice; a
    1.71 +  typical application would be to specify additional arguments for rules
    1.72 +  stemming from parameterized inductive definitions (see also
    1.73 +  \S\ref{sec:inductive}).
    1.74 +  
    1.75 +  The $open$ option causes the parameters of the new local contexts to be
    1.76 +  exposed to the current proof context.  Thus local variables stemming from
    1.77 +  distant parts of the theory development may be introduced in an implicit
    1.78 +  manner, which can be quite confusing to the reader.  Furthermore, this
    1.79 +  option may cause unwanted hiding of existing local variables, resulting in
    1.80 +  less robust proof texts.
    1.81 +  
    1.82 +\item [$induct~insts~R~ps$] is analogous to the $cases$ method, but refers to
    1.83 +  induction rules, which are determined as follows:
    1.84 +  \begin{matharray}{llll}
    1.85 +    \Text{facts}    &        & \Text{arguments} & \Text{rule} \\\hline
    1.86 +                    & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
    1.87 +    \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\
    1.88 +    \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
    1.89 +  \end{matharray}
    1.90 +  
    1.91 +  Several instantiations may be given, each referring to some part of a mutual
    1.92 +  inductive definition or datatype --- only related partial induction rules
    1.93 +  may be used together, though.  Any of the lists of terms $P, x, \dots$
    1.94 +  refers to the \emph{suffix} of variables present in the induction rule.
    1.95 +  This enables the writer to specify only induction variables, or both
    1.96 +  predicates and variables, for example.
    1.97 +  
    1.98 +  Additional parameters (including the $open$ option) may be given in the same
    1.99 +  way as for $cases$, see above.
   1.100 +\end{descr}
   1.101 +
   1.102 +Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
   1.103 +determined by the instantiated rule \emph{before} it has been applied to the
   1.104 +internal proof state.\footnote{As a general principle, Isar proof text may
   1.105 +  never refer to parts of proof states directly.} Thus proper use of symbolic
   1.106 +cases usually require the rule to be instantiated fully, as far as the
   1.107 +emerging local contexts and subgoals are concerned.  In particular, for
   1.108 +induction both the predicates and variables have to be specified.  Otherwise
   1.109 +the $\CASENAME$ command would refuse to invoke cases containing schematic
   1.110 +variables.  Furthermore the resulting local goal statement is bound to the
   1.111 +term variable $\Var{case}$\indexisarvar{case} --- for each case where it is
   1.112 +fully specified.
   1.113 +
   1.114 +The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named
   1.115 +cases present in the current proof state.
   1.116 +
   1.117 +\medskip
   1.118 +
   1.119 +It is important to note that there is a fundamental difference of the $cases$
   1.120 +and $induct$ methods in handling of non-atomic goal statements: $cases$ just
   1.121 +applies a certain rule in backward fashion, splitting the result into new
   1.122 +goals with the local contexts being augmented in a purely monotonic manner.
   1.123 +
   1.124 +In contrast, $induct$ passes the full goal statement through the ``recursive''
   1.125 +course involved in the induction.  Thus the original statement is basically
   1.126 +replaced by separate copies, corresponding to the induction hypotheses and
   1.127 +conclusion; the original goal context is no longer available.  This behavior
   1.128 +allows \emph{strengthened induction predicates} to be expressed concisely as
   1.129 +meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp \psi$ to
   1.130 +indicate ``variable'' parameters $\vec x$ and ``recursive'' assumptions
   1.131 +$\vec\phi$.  Also note that local definitions may be expressed as $\All{\vec
   1.132 +  x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
   1.133 +
   1.134 +\medskip
   1.135 +
   1.136 +Facts presented to either method are consumed according to the number of
   1.137 +``major premises'' of the rule involved (see also \S\ref{sec:induct-att} and
   1.138 +\S\ref{sec:cases}), which is usually $0$ for plain cases and induction rules
   1.139 +of datatypes etc.\ and $1$ for rules of inductive sets and the like.  The
   1.140 +remaining facts are inserted into the goal verbatim before the actual $cases$
   1.141 +or $induct$ rule is applied (thus facts may be even passed through an
   1.142 +induction).
   1.143 +
   1.144 +Note that whenever facts are present, the default rule selection scheme would
   1.145 +provide a ``set'' rule only, with the first fact consumed and the rest
   1.146 +inserted into the goal.  In order to pass all facts into a ``type'' rule
   1.147 +instead, one would have to specify this explicitly, e.g.\ by appending
   1.148 +``$type: name$'' to the method argument.
   1.149 +
   1.150 +
   1.151 +\subsection{Declaring rules}\label{sec:induct-att}
   1.152 +
   1.153 +\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
   1.154 +\begin{matharray}{rcl}
   1.155 +  \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\
   1.156 +  cases & : & \isaratt \\
   1.157 +  induct & : & \isaratt \\
   1.158 +\end{matharray}
   1.159 +
   1.160 +\begin{rail}
   1.161 +  'cases' spec
   1.162 +  ;
   1.163 +  'induct' spec
   1.164 +  ;
   1.165 +
   1.166 +  spec: ('type' | 'set') ':' nameref
   1.167 +  ;
   1.168 +\end{rail}
   1.169 +
   1.170 +The $cases$ and $induct$ attributes augment the corresponding context of rules
   1.171 +for reasoning about inductive sets and types.  The standard rules are already
   1.172 +declared by advanced definitional packages.  For special applications, these
   1.173 +may be replaced manually by variant versions.
   1.174 +
   1.175 +Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:cases}) to
   1.176 +adjust names of cases and parameters of a rule.
   1.177 +
   1.178 +The $consumes$ declaration (cf.\ \S\ref{sec:cases}) is taken care of
   1.179 +automatically (if none had been given already): $consumes~0$ is specified for
   1.180 +``type'' rules and $consumes~1$ for ``set'' rules.
   1.181 +
   1.182 +
   1.183  %%% Local Variables:
   1.184  %%% mode: latex
   1.185  %%% TeX-master: "isar-ref"
     2.1 --- a/doc-src/IsarRef/hol.tex	Thu Oct 04 16:07:43 2001 +0200
     2.2 +++ b/doc-src/IsarRef/hol.tex	Thu Oct 04 16:09:12 2001 +0200
     2.3 @@ -43,7 +43,7 @@
     2.4  \end{descr}
     2.5  
     2.6  
     2.7 -\section{Primitive types}
     2.8 +\section{Primitive types}\label{sec:typedef}
     2.9  
    2.10  \indexisarcmd{typedecl}\indexisarcmd{typedef}
    2.11  \begin{matharray}{rcl}
    2.12 @@ -140,7 +140,7 @@
    2.13  \S\ref{sec:induct_tac}.
    2.14  
    2.15  
    2.16 -\section{Recursive functions}
    2.17 +\section{Recursive functions}\label{sec:recursion}
    2.18  
    2.19  \indexisarcmd{primrec}\indexisarcmd{recdef}\indexisarcmd{recdef-tc}
    2.20  \begin{matharray}{rcl}
    2.21 @@ -278,190 +278,33 @@
    2.22  HOL.
    2.23  
    2.24  
    2.25 -\section{Proof by cases and induction}\label{sec:induct-method}
    2.26 -%FIXME move to generic.tex
    2.27 -
    2.28 -\subsection{Proof methods}\label{sec:induct-method-proper}
    2.29 +\section{Arithmetic}
    2.30  
    2.31 -\indexisarmeth{cases}\indexisarmeth{induct}
    2.32 +\indexisarmeth{arith}\indexisaratt{arith-split}
    2.33  \begin{matharray}{rcl}
    2.34 -  cases & : & \isarmeth \\
    2.35 -  induct & : & \isarmeth \\
    2.36 +  arith & : & \isarmeth \\
    2.37 +  arith_split & : & \isaratt \\
    2.38  \end{matharray}
    2.39  
    2.40 -The $cases$ and $induct$ methods provide a uniform interface to case analysis
    2.41 -and induction over datatypes, inductive sets, and recursive functions.  The
    2.42 -corresponding rules may be specified and instantiated in a casual manner.
    2.43 -Furthermore, these methods provide named local contexts that may be invoked
    2.44 -via the $\CASENAME$ proof command within the subsequent proof text (cf.\ 
    2.45 -\S\ref{sec:cases}).  This accommodates compact proof texts even when reasoning
    2.46 -about large specifications.
    2.47 -
    2.48  \begin{rail}
    2.49 -  'cases' ('(' 'simplified' ')')? spec
    2.50 -  ;
    2.51 -  'induct' ('(' 'stripped' ')')? spec
    2.52 -  ;
    2.53 -
    2.54 -  spec: open? args rule? params?
    2.55 -  ;
    2.56 -  open: '(' 'open' ')'
    2.57 -  ;
    2.58 -  args: (insts * 'and') 
    2.59 -  ;
    2.60 -  rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
    2.61 -  ;
    2.62 -  params: 'of' ':' insts
    2.63 +  'arith' '!'?
    2.64    ;
    2.65  \end{rail}
    2.66  
    2.67 -\begin{descr}
    2.68 -\item [$cases~insts~R~ps$] applies method $rule$ with an appropriate case
    2.69 -  distinction theorem, instantiated to the subjects $insts$.  Symbolic case
    2.70 -  names are bound according to the rule's local contexts.
    2.71 -  
    2.72 -  The rule is determined as follows, according to the facts and arguments
    2.73 -  passed to the $cases$ method:
    2.74 -  \begin{matharray}{llll}
    2.75 -    \Text{facts}    &       & \Text{arguments} & \Text{rule} \\\hline
    2.76 -                    & cases &           & \Text{classical case split} \\
    2.77 -                    & cases & t         & \Text{datatype exhaustion (type of $t$)} \\
    2.78 -    \edrv a \in A   & cases & \dots     & \Text{inductive set elimination (of $A$)} \\
    2.79 -    \dots           & cases & \dots ~ R & \Text{explicit rule $R$} \\
    2.80 -  \end{matharray}
    2.81 -  
    2.82 -  Several instantiations may be given, referring to the \emph{suffix} of
    2.83 -  premises of the case rule; within each premise, the \emph{prefix} of
    2.84 -  variables is instantiated.  In most situations, only a single term needs to
    2.85 -  be specified; this refers to the first variable of the last premise (it is
    2.86 -  usually the same for all cases).
    2.87 -  
    2.88 -  Additional parameters may be specified as $ps$; these are applied after the
    2.89 -  primary instantiation in the same manner as by the $of$ attribute (cf.\ 
    2.90 -  \S\ref{sec:pure-meth-att}).  This feature is rarely needed in practice; a
    2.91 -  typical application would be to specify additional arguments for rules
    2.92 -  stemming from parameterized inductive definitions (see also
    2.93 -  \S\ref{sec:inductive}).
    2.94 +The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
    2.95 +$real$).  Any current facts are inserted into the goal before running the
    2.96 +procedure.  The ``!''~argument causes the full context of assumptions to be
    2.97 +included.  The $arith_split$ attribute declares case split rules to be
    2.98 +expanded before the arithmetic procedure is invoked.
    2.99  
   2.100 -  The $simplified$ option causes ``obvious cases'' of the rule to be solved
   2.101 -  beforehand, while the others are left unscathed.
   2.102 -  
   2.103 -  The $open$ option causes the parameters of the new local contexts to be
   2.104 -  exposed to the current proof context.  Thus local variables stemming from
   2.105 -  distant parts of the theory development may be introduced in an implicit
   2.106 -  manner, which can be quite confusing to the reader.  Furthermore, this
   2.107 -  option may cause unwanted hiding of existing local variables, resulting in
   2.108 -  less robust proof texts.
   2.109 -  
   2.110 -\item [$induct~insts~R~ps$] is analogous to the $cases$ method, but refers to
   2.111 -  induction rules, which are determined as follows:
   2.112 -  \begin{matharray}{llll}
   2.113 -    \Text{facts}    &        & \Text{arguments} & \Text{rule} \\\hline
   2.114 -                    & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
   2.115 -    \edrv x \in A   & induct & \dots         & \Text{set induction (of $A$)} \\
   2.116 -    \dots           & induct & \dots ~ R     & \Text{explicit rule $R$} \\
   2.117 -  \end{matharray}
   2.118 -  
   2.119 -  Several instantiations may be given, each referring to some part of a mutual
   2.120 -  inductive definition or datatype --- only related partial induction rules
   2.121 -  may be used together, though.  Any of the lists of terms $P, x, \dots$
   2.122 -  refers to the \emph{suffix} of variables present in the induction rule.
   2.123 -  This enables the writer to specify only induction variables, or both
   2.124 -  predicates and variables, for example.
   2.125 -  
   2.126 -  Additional parameters may be given in the same way as for $cases$.
   2.127 -  
   2.128 -  The $stripped$ option causes implications and (bounded) universal
   2.129 -  quantifiers to be removed from each new subgoal emerging from the
   2.130 -  application of the induction rule.  This accommodates special applications
   2.131 -  of ``strengthened induction predicates''.  This option is rarely needed, the
   2.132 -  $induct$ method already handles proper rules appropriately by default.
   2.133 -  
   2.134 -  The $open$ option has the same effect as for the $cases$ method, see above.
   2.135 -\end{descr}
   2.136 -
   2.137 -Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as
   2.138 -determined by the instantiated rule \emph{before} it has been applied to the
   2.139 -internal proof state.\footnote{As a general principle, Isar proof text may
   2.140 -  never refer to parts of proof states directly.} Thus proper use of symbolic
   2.141 -cases usually require the rule to be instantiated fully, as far as the
   2.142 -emerging local contexts and subgoals are concerned.  In particular, for
   2.143 -induction both the predicates and variables have to be specified.  Otherwise
   2.144 -the $\CASENAME$ command would refuse to invoke cases containing schematic
   2.145 -variables.  Furthermore the resulting local goal statement is bound to the
   2.146 -term variable $\Var{case}$\indexisarvar{case} --- for each case where it is
   2.147 -fully specified.
   2.148 -
   2.149 -The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named
   2.150 -cases present in the current proof state.
   2.151 -
   2.152 -\medskip
   2.153 -
   2.154 -It is important to note that there is a fundamental difference of the $cases$
   2.155 -and $induct$ methods in handling of non-atomic goal statements: $cases$ just
   2.156 -applies a certain rule in backward fashion, splitting the result into new
   2.157 -goals with the local contexts being augmented in a purely monotonic manner.
   2.158 -
   2.159 -In contrast, $induct$ passes the full goal statement through the ``recursive''
   2.160 -course involved in the induction.  Thus the original statement is basically
   2.161 -replaced by separate copies, corresponding to the induction hypotheses and
   2.162 -conclusion; the original goal context is no longer available.  This behavior
   2.163 -allows \emph{strengthened induction predicates} to be expressed concisely as
   2.164 -meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp \psi$ to
   2.165 -indicate ``variable'' parameters $\vec x$ and ``recursive'' assumptions
   2.166 -$\vec\phi$.  Also note that local definitions may be expressed as $\All{\vec
   2.167 -  x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
   2.168 -
   2.169 -\medskip
   2.170 -
   2.171 -Facts presented to either method are consumed according to the number of
   2.172 -``major premises'' of the rule involved (see also \S\ref{sec:induct-att} and
   2.173 -\S\ref{sec:cases}), which is usually $0$ for plain cases and induction rules
   2.174 -of datatypes etc.\ and $1$ for rules of inductive sets and the like.  The
   2.175 -remaining facts are inserted into the goal verbatim before the actual $cases$
   2.176 -or $induct$ rule is applied (thus facts may be even passed through an
   2.177 -induction).
   2.178 -
   2.179 -Note that whenever facts are present, the default rule selection scheme would
   2.180 -provide a ``set'' rule only, with the first fact consumed and the rest
   2.181 -inserted into the goal.  In order to pass all facts into a ``type'' rule
   2.182 -instead, one would have to specify this explicitly, e.g.\ by appending
   2.183 -``$type: name$'' to the method argument.
   2.184 +Note that a simpler (but faster) version of arithmetic reasoning is already
   2.185 +performed by the Simplifier.
   2.186  
   2.187  
   2.188 -\subsection{Declaring rules}\label{sec:induct-att}
   2.189 -
   2.190 -\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
   2.191 -\begin{matharray}{rcl}
   2.192 -  \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\
   2.193 -  cases & : & \isaratt \\
   2.194 -  induct & : & \isaratt \\
   2.195 -\end{matharray}
   2.196 -
   2.197 -\begin{rail}
   2.198 -  'cases' spec
   2.199 -  ;
   2.200 -  'induct' spec
   2.201 -  ;
   2.202 +\section{Cases and induction: emulating tactic scripts}\label{sec:induct_tac}
   2.203  
   2.204 -  spec: ('type' | 'set') ':' nameref
   2.205 -  ;
   2.206 -\end{rail}
   2.207 -
   2.208 -The $cases$ and $induct$ attributes augment the corresponding context of rules
   2.209 -for reasoning about inductive sets and types.  The standard rules are already
   2.210 -declared by HOL definitional packages.  For special applications, these may be
   2.211 -replaced manually by variant versions.
   2.212 -
   2.213 -Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:cases}) to
   2.214 -adjust names of cases and parameters of a rule.
   2.215 -
   2.216 -The $consumes$ declaration (cf.\ \S\ref{sec:cases}) is taken care of
   2.217 -automatically (if none had been given already): $consumes~0$ is specified for
   2.218 -``type'' rules and $consumes~1$ for ``set'' rules.
   2.219 -
   2.220 -
   2.221 -\subsection{Emulating tactic scripts}\label{sec:induct_tac}
   2.222 +The following important tactical tools of Isabelle/HOL have been ported to
   2.223 +Isar.  These should be never used in proper proof texts!
   2.224  
   2.225  \indexisarmeth{case-tac}\indexisarmeth{induct-tac}
   2.226  \indexisarmeth{ind-cases}\indexisarcmd{inductive-cases}
   2.227 @@ -510,9 +353,7 @@
   2.228    
   2.229  \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
   2.230    to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
   2.231 -  forward manner, unlike the proper $cases$ method (see
   2.232 -  \S\ref{sec:induct-method-proper}) which requires simplified cases to be
   2.233 -  solved completely.
   2.234 +  forward manner.
   2.235    
   2.236    While $ind_cases$ is a proof method to apply the result immediately as
   2.237    elimination rules, $\isarkeyword{inductive_cases}$ provides case split
   2.238 @@ -520,29 +361,6 @@
   2.239  \end{descr}
   2.240  
   2.241  
   2.242 -\section{Arithmetic}
   2.243 -
   2.244 -\indexisarmeth{arith}\indexisaratt{arith-split}
   2.245 -\begin{matharray}{rcl}
   2.246 -  arith & : & \isarmeth \\
   2.247 -  arith_split & : & \isaratt \\
   2.248 -\end{matharray}
   2.249 -
   2.250 -\begin{rail}
   2.251 -  'arith' '!'?
   2.252 -  ;
   2.253 -\end{rail}
   2.254 -
   2.255 -The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
   2.256 -$real$).  Any current facts are inserted into the goal before running the
   2.257 -procedure.  The ``!''~argument causes the full context of assumptions to be
   2.258 -included.  The $arith_split$ attribute declares case split rules to be
   2.259 -expanded before the arithmetic procedure is invoked.
   2.260 -
   2.261 -Note that a simpler (but faster) version of arithmetic reasoning is already
   2.262 -performed by the Simplifier.
   2.263 -
   2.264 -
   2.265  %%% Local Variables: 
   2.266  %%% mode: latex
   2.267  %%% TeX-master: "isar-ref"