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.47 +added automatically!
    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