# HG changeset patch # User wenzelm # Date 966271516 -7200 # Node ID 900df8e67fcf56afc3b09cd2c1bf3e47d079c1ef # Parent 69d2fb3dc4c6fe636a8faffd17ca94f3263b8c6b renamed 'intrs' to 'intros'; updated 'inductive_cases', added 'mk_cases_tac'; 'cases' method: admit multiple insts; added 'arith_split' att; diff -r 69d2fb3dc4c6 -r 900df8e67fcf doc-src/IsarRef/hol.tex --- a/doc-src/IsarRef/hol.tex Mon Aug 14 18:43:57 2000 +0200 +++ b/doc-src/IsarRef/hol.tex Mon Aug 14 18:45:16 2000 +0200 @@ -165,26 +165,21 @@ \section{(Co)Inductive sets} -\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive-cases} -\indexisaratt{mono} +\indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisaratt{mono} \begin{matharray}{rcl} \isarcmd{inductive} & : & \isartrans{theory}{theory} \\ - \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\ + \isarcmd{coinductive}^* & : & \isartrans{theory}{theory} \\ mono & : & \isaratt \\ - \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ \end{matharray} \railalias{condefs}{con\_defs} -\railalias{indcases}{inductive\_cases} -\railterm{condefs,indcases} +\railterm{condefs} \begin{rail} ('inductive' | 'coinductive') (term comment? +) \\ - 'intrs' attributes? (thmdecl? prop comment? +) \\ + 'intros' attributes? (thmdecl? prop comment? +) \\ 'monos' thmrefs comment? \\ condefs thmrefs comment? ; - indcases thmdef? nameref ':' \\ (prop +) comment? - ; 'mono' (() | 'add' | 'del') ; \end{rail} @@ -194,18 +189,6 @@ (co)inductive sets from the given introduction rules. \item [$mono$] declares monotonicity rules. These rule are involved in the automated monotonicity proof of $\isarkeyword{inductive}$. -\item [$\isarkeyword{inductive_cases}$] creates instances of elimination rules - of (co)inductive sets, solving obvious cases by simplification. - - The $cases$ proof method (see \S\ref{sec:induct-method}) provides a more - direct way for reasoning by cases (including optional simplification). - - Unlike the \texttt{mk_cases} ML function exported with any inductive - definition \cite{isabelle-HOL}, $\isarkeyword{inductive_cases}$ it does - \emph{not} modify cases by simplification that are not solved completely - anyway (e.g.\ due to contradictory assumptions). Thus - $\isarkeyword{inductive_cases}$ conforms to the way Isar proofs are - conducted, rather than old-style tactic scripts. \end{descr} See \cite{isabelle-HOL} for further information on inductive definitions in @@ -231,7 +214,7 @@ about large specifications. \begin{rail} - 'cases' ('(simplified)')? ('(opaque)')? \\ term? rule? ; + 'cases' ('(simplified)')? ('(opaque)')? \\ (insts * 'and') rule? ; 'induct' ('(stripped)')? ('(opaque)')? \\ (insts * 'and') rule? ; @@ -241,9 +224,9 @@ \end{rail} \begin{descr} -\item [$cases~t~R$] applies method $rule$ with an appropriate case distinction - theorem, instantiated to the subject $t$. Symbolic case names are bound - according to the rule's local contexts. +\item [$cases~insts~R$] applies method $rule$ with an appropriate case + distinction theorem, instantiated to the subjects $insts$. Symbolic case + names are bound according to the rule's local contexts. The rule is determined as follows, according to the facts and arguments passed to the $cases$ method: @@ -254,6 +237,12 @@ \edrv a \in A & cases & \dots & \text{inductive set elimination (of $A$)} \\ \dots & cases & \dots ~ R & \text{explicit rule $R$} \\ \end{matharray} + + Several instantiations may be given, referring to the \emph{suffix} of + premises of the case rule; within each premise, the \emph{prefix} of + variables is instantiated. In most situations, only a single term needs to + be specified; this refers to the first variable of the last premise (it is + usually the same for all cases). The $simplified$ option causes ``obvious cases'' of the rule to be solved beforehand, while the others are left unscathed. @@ -301,7 +290,7 @@ the $\CASENAME$ command would refuse to invoke cases containing schematic variables. -The $\isarkeyword{print_cases}$ command (\S\ref{sec:diag}) prints all named +The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named cases present in the current proof state. @@ -335,44 +324,68 @@ \subsection{Emulating tactic scripts}\label{sec:induct_tac} \indexisarmeth{case-tac}\indexisarmeth{induct-tac} +\indexisarmeth{mk-cases-tac}\indexisarcmd{inductive-cases} \begin{matharray}{rcl} case_tac & : & \isarmeth \\ induct_tac & : & \isarmeth \\ + mk_cases_tac & : & \isarmeth \\ + \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ \end{matharray} -These proof methods directly correspond to the ML tactics of the same name -\cite{isabelle-HOL}. In particular, the instantiation given refers to the -\emph{dynamic} proof state, rather than the current proof text. This enables -proof scripts to refer to parameters of some subgoal, for example. - \railalias{casetac}{case\_tac} \railterm{casetac} + \railalias{inducttac}{induct\_tac} \railterm{inducttac} +\railalias{mkcasestac}{mk\_cases\_tac} +\railterm{mkcasestac} + +\railalias{indcases}{inductive\_cases} +\railterm{indcases} + \begin{rail} casetac goalspec? term rule? ; inducttac goalspec? (insts * 'and') rule? ; + mkcasestac (prop +) + ; + indcases thmdef? (prop +) comment? + ; rule: ('rule' ':' thmref) ; \end{rail} -By default, $case_tac$ and $induct_tac$ admit to reason about inductive -datatypes only, unless an alternative rule is given explicitly. Furthermore, -$case_tac$ does a classical case split on booleans; $induct_tac$ allows only -variables to be given as instantiation. Also note that named local contexts -(see \S\ref{sec:cases}) are not provided as would be by the proper $induct$ -and $cases$ proof methods (see \S\ref{sec:induct-method-proper}). +\begin{descr} +\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes + only (unless an alternative rule is given explicitly). Furthermore, + $case_tac$ does a classical case split on booleans; $induct_tac$ allows only + variables to be given as instantiation. These tactic emulations feature + both goal addressing and dynamic instantiation. Note that named local + contexts (see \S\ref{sec:cases}) are \emph{not} provided as would be by the + proper $induct$ and $cases$ proof methods (see + \S\ref{sec:induct-method-proper}). + +\item [$mk_cases_tac$ and $\isarkeyword{inductive_cases}$] provide an + interface to the \texttt{mk_cases} operation. Rules are simplified in an + unrestricted forward manner, unlike the proper $cases$ method (see + \S\ref{sec:induct-method-proper}) which requires simplified cases to be + solved completely. + + While $mk_cases_tac$ is a proof method to apply the result immediately as + elimination rules, $\isarkeyword{inductive_cases}$ provides case split + theorems at the theory level for later use, +\end{descr} \section{Arithmetic} -\indexisarmeth{arith} +\indexisarmeth{arith}\indexisaratt{arith_split} \begin{matharray}{rcl} arith & : & \isarmeth \\ + arith_split & : & \isaratt \\ \end{matharray} \begin{rail} @@ -383,7 +396,8 @@ The $arith$ method decides linear arithmetic problems (on types $nat$, $int$, $real$). Any current facts are inserted into the goal before running the procedure. The ``!''~argument causes the full context of assumptions to be -included. +included. The $arith_split$ attribute declares case split rules to be +expanded before the arithmetic procedure is invoked. Note that a simpler (but faster) version of arithmetic reasoning is already performed by the Simplifier.