summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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