# HG changeset patch # User nipkow # Date 877341222 -7200 # Node ID e9d5bcae8351789413d575a8d242aa0a75abea1f # Parent c60ff6d0a6b8295a09ea02c876a3318f110fd5a4 \label{simp-chap} -> chap:simplification Indexed "higher-order pattern" diff -r c60ff6d0a6b8 -r e9d5bcae8351 doc-src/Ref/ref.ind --- a/doc-src/Ref/ref.ind Mon Oct 20 11:47:04 1997 +0200 +++ b/doc-src/Ref/ref.ind Mon Oct 20 11:53:42 1997 +0200 @@ -313,6 +313,7 @@ \indexspace \item {\tt has_fewer_prems}, \bold{32} + \item higher-order pattern, \bold{102} \item {\tt hyp_subst_tac}, \bold{96} \item {\tt hyp_subst_tacs}, \bold{130} \item {\tt HypsubstFun}, 97, 130 @@ -427,6 +428,7 @@ \item {\tt parse_ast_translation}, 91 \item {\tt parse_rules}, 86 \item {\tt parse_translation}, 91 + \item pattern, higher-order, \bold{102} \item {\tt pause_tac}, \bold{25} \item Poly/{\ML} compiler, 5 \item {\tt pop_proof}, \bold{14} diff -r c60ff6d0a6b8 -r e9d5bcae8351 doc-src/Ref/ref.tex --- a/doc-src/Ref/ref.tex Mon Oct 20 11:47:04 1997 +0200 +++ b/doc-src/Ref/ref.tex Mon Oct 20 11:53:42 1997 +0200 @@ -21,7 +21,8 @@ \texttt{lcp@cl.cam.ac.uk}\\[3ex] With Contributions by Tobias Nipkow and Markus Wenzel% \thanks{Tobias Nipkow, of T. U. Munich, wrote most of - Chapters~\protect\ref{Defining-Logics} and~\protect\ref{simp-chap}, and part of + Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification}, + and part of Chapter~\protect\ref{theories}. Carsten Clasohm also contributed to Chapter~\protect\ref{theories}. Markus Wenzel contributed to Chapter~\protect\ref{chap:syntax}. Sara Kalvala, Martin Simons and others diff -r c60ff6d0a6b8 -r e9d5bcae8351 doc-src/Ref/simplifier.tex --- a/doc-src/Ref/simplifier.tex Mon Oct 20 11:47:04 1997 +0200 +++ b/doc-src/Ref/simplifier.tex Mon Oct 20 11:53:42 1997 +0200 @@ -1,5 +1,6 @@ %% $Id$ -\chapter{Simplification} \label{simp-chap} +\chapter{Simplification} +\label{chap:simplification} \index{simplification|(} This chapter describes Isabelle's generic simplification package, which @@ -177,12 +178,13 @@ {(\Var{i}+\Var{j})+\Var{k}}$ is ok. It will also deal gracefully with all rules whose left-hand sides are -so-called {\em higher-order patterns}~\cite{nipkow-patterns}. These are terms -in $\beta$-normal form (this will always be the case unless you have done -something strange) where each occurrence of an unknown is of the form -$\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are distinct bound variables. -Hence $(\forall x.\Var{P}(x) \land \Var{Q}(x)) \bimp (\forall x.\Var{P}(x)) -\land (\forall x.\Var{Q}(x))$ is also ok, in both directions. +so-called {\em higher-order patterns}~\cite{nipkow-patterns}. +\indexbold{higher-order pattern}\indexbold{pattern, higher-order} +These are terms in $\beta$-normal form (this will always be the case unless +you have done something strange) where each occurrence of an unknown is of +the form $\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are distinct bound +variables. Hence $(\forall x.\Var{P}(x) \land \Var{Q}(x)) \bimp (\forall +x.\Var{P}(x)) \land (\forall x.\Var{Q}(x))$ is also ok, in both directions. In some rare cases the rewriter will even deal with quite general rules: for example ${\Var{f}(\Var{x})\in range(\Var{f})} = True$ rewrites $g(a) \in diff -r c60ff6d0a6b8 -r e9d5bcae8351 doc-src/Ref/substitution.tex --- a/doc-src/Ref/substitution.tex Mon Oct 20 11:47:04 1997 +0200 +++ b/doc-src/Ref/substitution.tex Mon Oct 20 11:53:42 1997 +0200 @@ -15,7 +15,7 @@ corresponding instances of~$u$, and continues until it reaches a normal form. Substitution handles `one-off' replacements by particular equalities while rewriting handles general equations. -Chapter~\ref{simp-chap} discusses Isabelle's rewriting tactics. +Chapter~\ref{chap:simplification} discusses Isabelle's rewriting tactics. \section{Substitution rules} @@ -136,7 +136,7 @@ Thus, the functor requires the following items: \begin{ttdescription} \item[Simplifier] should be an instance of the simplifier (see - Chapter~\ref{simp-chap}). + Chapter~\ref{chap:simplification}). \item[\ttindexbold{dest_eq}] should return the pair~$(t,u)$ when applied to the \ML{} term that represents~$t=u$. For other terms, it diff -r c60ff6d0a6b8 -r e9d5bcae8351 doc-src/Ref/tactic.tex --- a/doc-src/Ref/tactic.tex Mon Oct 20 11:47:04 1997 +0200 +++ b/doc-src/Ref/tactic.tex Mon Oct 20 11:53:42 1997 +0200 @@ -7,8 +7,8 @@ expressed using basic tactics and tacticals. This chapter only presents the primitive tactics. Substantial proofs require -the power of simplification (Chapter~\ref{simp-chap}) and classical reasoning -(Chapter~\ref{chap:classical}). +the power of simplification (Chapter~\ref{chap:simplification}) and classical +reasoning (Chapter~\ref{chap:classical}). \section{Resolution and assumption tactics} {\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using