doc-src/Ref/simplifier.tex
 changeset 9695 ec7d7f877712 parent 9445 6c93b1eb11f8 child 9712 e33422a2eb9c
     1.1 --- a/doc-src/Ref/simplifier.tex	Mon Aug 28 13:50:24 2000 +0200
1.2 +++ b/doc-src/Ref/simplifier.tex	Mon Aug 28 13:52:38 2000 +0200
1.3 @@ -3,12 +3,11 @@
1.4  \label{chap:simplification}
1.5  \index{simplification|(}
1.6
1.7 -This chapter describes Isabelle's generic simplification package.  It
1.8 -performs conditional and unconditional rewriting and uses contextual
1.9 -information (local assumptions').  It provides several general hooks,
1.10 -which can provide automatic case splits during rewriting, for example.
1.11 -The simplifier is already set up for many of Isabelle's logics: \FOL,
1.12 -\ZF, \HOL, \HOLCF.
1.13 +This chapter describes Isabelle's generic simplification package.  It performs
1.14 +conditional and unconditional rewriting and uses contextual information
1.15 +(local assumptions').  It provides several general hooks, which can provide
1.16 +automatic case splits during rewriting, for example.  The simplifier is
1.17 +already set up for many of Isabelle's logics: FOL, ZF, HOL, HOLCF.
1.18
1.19  The first section is a quick introduction to the simplifier that
1.20  should be sufficient to get started.  The later sections explain more
1.21 @@ -71,9 +70,9 @@
1.22
1.23  \medskip
1.24
1.25 -As an example, consider the theory of arithmetic in \HOL.  The (rather
1.26 -trivial) goal $0 + (x + 0) = x + 0 + 0$ can be solved by a single call
1.27 -of \texttt{Simp_tac} as follows:
1.28 +As an example, consider the theory of arithmetic in HOL.  The (rather trivial)
1.29 +goal $0 + (x + 0) = x + 0 + 0$ can be solved by a single call of
1.30 +\texttt{Simp_tac} as follows:
1.31  \begin{ttbox}
1.32  context Arith.thy;
1.33  Goal "0 + (x + 0) = x + 0 + 0";
1.34 @@ -181,11 +180,11 @@
1.35
1.36  \end{ttdescription}
1.37
1.38 -When a new theory is built, its implicit simpset is initialized by the
1.39 -union of the respective simpsets of its parent theories.  In addition,
1.40 -certain theory definition constructs (e.g.\ \ttindex{datatype} and
1.41 -\ttindex{primrec} in \HOL) implicitly augment the current simpset.
1.42 -Ordinary definitions are not added automatically!
1.43 +When a new theory is built, its implicit simpset is initialized by the union
1.44 +of the respective simpsets of its parent theories.  In addition, certain
1.45 +theory definition constructs (e.g.\ \ttindex{datatype} and \ttindex{primrec}
1.46 +in HOL) implicitly augment the current simpset.  Ordinary definitions are not
1.48
1.49  It is up the user to manipulate the current simpset further by
1.50  explicitly adding or deleting theorems and simplification procedures.
1.51 @@ -253,12 +252,11 @@
1.52  \end{ttbox}
1.53  \begin{ttdescription}
1.54
1.55 -\item[\ttindexbold{empty_ss}] is the empty simpset.  This is not very
1.56 -  useful under normal circumstances because it doesn't contain
1.57 -  suitable tactics (subgoaler etc.).  When setting up the simplifier
1.58 -  for a particular object-logic, one will typically define a more
1.59 -  appropriate almost empty'' simpset.  For example, in \HOL\ this is
1.60 -  called \ttindexbold{HOL_basic_ss}.
1.61 +\item[\ttindexbold{empty_ss}] is the empty simpset.  This is not very useful
1.62 +  under normal circumstances because it doesn't contain suitable tactics
1.63 +  (subgoaler etc.).  When setting up the simplifier for a particular
1.64 +  object-logic, one will typically define a more appropriate almost empty''
1.65 +  simpset.  For example, in HOL this is called \ttindexbold{HOL_basic_ss}.
1.66
1.67  \item[\ttindexbold{merge_ss} ($ss@1$, $ss@2$)] merges simpsets $ss@1$
1.68    and $ss@2$ by building the union of their respective rewrite rules,
1.69 @@ -1077,12 +1075,11 @@
1.70
1.71  \subsection{Example: sums of natural numbers}
1.72
1.73 -This example is again set in \HOL\ (see \texttt{HOL/ex/NatSum}).
1.74 -Theory \thydx{Arith} contains natural numbers arithmetic.  Its
1.75 -associated simpset contains many arithmetic laws including
1.76 -distributivity of~$\times$ over~$+$, while \texttt{add_ac} is a list
1.77 -consisting of the A, C and LC laws for~$+$ on type \texttt{nat}.  Let
1.78 -us prove the theorem
1.79 +This example is again set in HOL (see \texttt{HOL/ex/NatSum}).  Theory
1.80 +\thydx{Arith} contains natural numbers arithmetic.  Its associated simpset
1.81 +contains many arithmetic laws including distributivity of~$\times$ over~$+$,
1.82 +while \texttt{add_ac} is a list consisting of the A, C and LC laws for~$+$ on
1.83 +type \texttt{nat}.  Let us prove the theorem
1.84  $\sum@{i=1}^n i = n\times(n+1)/2.$
1.85  %
1.86  A functional~\texttt{sum} represents the summation operator under the
1.87 @@ -1216,12 +1213,11 @@
1.88  \texttt{HOL/Modelcheck/MCSyn} where this is used to provide external
1.89  model checker syntax).
1.90
1.91 -The {\HOL} theory of tuples (see \texttt{HOL/Prod}) provides an
1.92 -operator \texttt{split} together with some concrete syntax supporting
1.93 -$\lambda\,(x,y).b$ abstractions.  Assume that we would like to offer a
1.94 -tactic that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of
1.95 -some pair type) to $\lambda\,(x,y).f\,(x,y)$.  The corresponding rule
1.96 -is:
1.97 +The HOL theory of tuples (see \texttt{HOL/Prod}) provides an operator
1.98 +\texttt{split} together with some concrete syntax supporting
1.99 +$\lambda\,(x,y).b$ abstractions.  Assume that we would like to offer a tactic
1.100 +that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of some pair type)
1.101 +to $\lambda\,(x,y).f\,(x,y)$.  The corresponding rule is:
1.102  \begin{ttbox}
1.103  pair_eta_expand:  (f::'a*'b=>'c) = (\%(x, y). f (x, y))
1.104  \end{ttbox}
1.105 @@ -1298,7 +1294,7 @@
1.106  We first prove lots of standard rewrite rules about the logical
1.107  connectives.  These include cancellation and associative laws.  We
1.108  define a function that echoes the desired law and then supplies it the
1.109 -prover for intuitionistic \FOL:
1.110 +prover for intuitionistic FOL:
1.111  \begin{ttbox}
1.112  fun int_prove_fun s =
1.113   (writeln s;
1.114 @@ -1437,12 +1433,11 @@
1.115  val triv_rls = [TrueI,refl,iff_refl,notFalseI];
1.116  \end{ttbox}
1.117  %
1.118 -The basic simpset for intuitionistic \FOL{} is
1.119 -\ttindexbold{FOL_basic_ss}.  It preprocess rewrites using {\tt
1.120 -  gen_all}, \texttt{atomize} and \texttt{mk_eq}.  It solves simplified
1.121 -subgoals using \texttt{triv_rls} and assumptions, and by detecting
1.122 -contradictions.  It uses \ttindex{asm_simp_tac} to tackle subgoals of
1.123 -conditional rewrites.
1.124 +The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}.  It
1.125 +preprocess rewrites using {\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}.
1.126 +It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by
1.127 +detecting contradictions.  It uses \ttindex{asm_simp_tac} to tackle subgoals
1.128 +of conditional rewrites.
1.129
1.130  Other simpsets built from \texttt{FOL_basic_ss} will inherit these items.
1.131  In particular, \ttindexbold{IFOL_ss}, which introduces {\tt