author  paulson 
Thu, 20 Nov 1997 11:54:31 +0100  
changeset 4245  b9ce25073cc0 
parent 3950  e9d5bcae8351 
child 4317  7264fa2ff2ec 
permissions  rwrr 
104  1 
%% $Id$ 
3950  2 
\chapter{Simplification} 
3 
\label{chap:simplification} 

104  4 
\index{simplification(} 
5 

6 
This chapter describes Isabelle's generic simplification package, which 

323  7 
provides a suite of simplification tactics. It performs conditional and 
8 
unconditional rewriting and uses contextual information (`local 

9 
assumptions'). It provides a few general hooks, which can provide 

10 
automatic case splits during rewriting, for example. The simplifier is set 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

11 
up for many of Isabelle's logics: \FOL, \ZF, \HOL\ and \HOLCF. 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

12 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

13 
The next section is a quick introduction to the simplifier, the later 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

14 
sections explain advanced features. 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

15 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

16 
\section{Simplification for dummies} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

17 
\label{sec:simpfordummies} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

18 

2479  19 
In some logics (\FOL, {\HOL} and \ZF), the simplifier is particularly easy to 
20 
use because it supports the concept of a {\em current 

21 
simpset}\index{simpset!current}. This is a default set of simplification 

22 
rules. All commands are interpreted relative to the current simpset. For 

23 
example, in the theory of arithmetic the goal 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

24 
\begin{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

25 
{\out 1. 0 + (x + 0) = x + 0 + 0} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

26 
\end{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

27 
can be solved by a single 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

28 
\begin{ttbox} 
2479  29 
by (Simp_tac 1); 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

30 
\end{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

31 
The simplifier uses the current simpset, which in the case of arithmetic 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

32 
contains the required theorems $\Var{n}+0 = \Var{n}$ and $0+\Var{n} = 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

33 
\Var{n}$. 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

34 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

35 
If assumptions of the subgoal are also needed in the simplification 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

36 
process, as in 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

37 
\begin{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

38 
{\out 1. x = 0 ==> x + x = 0} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

39 
\end{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

40 
then there is the more powerful 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

41 
\begin{ttbox} 
2479  42 
by (Asm_simp_tac 1); 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

43 
\end{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

44 
which solves the above goal. 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

45 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

46 
There are four basic simplification tactics: 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

47 
\begin{ttdescription} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

48 
\item[\ttindexbold{Simp_tac} $i$] simplifies subgoal~$i$ using the current 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

49 
simpset. It may solve the subgoal completely if it has become trivial, 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

50 
using the solver. 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

51 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

52 
\item[\ttindexbold{Asm_simp_tac}]\index{assumptions!in simplification} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

53 
is like \verb$Simp_tac$, but extracts additional rewrite rules from the 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

54 
assumptions. 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

55 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

56 
\item[\ttindexbold{Full_simp_tac}] is like \verb$Simp_tac$, but also 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

57 
simplifies the assumptions (but without using the assumptions to simplify 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

58 
each other or the actual goal.) 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

59 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

60 
\item[\ttindexbold{Asm_full_simp_tac}] 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

61 
is like \verb$Asm_simp_tac$, but also simplifies the assumptions one by 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

62 
one. {\em Working from left to right, it uses each assumption in the 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

63 
simplification of those following.} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

64 
\end{ttdescription} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

65 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

66 
{\tt Asm_full_simp_tac} is the most powerful of this quartet but may also 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

67 
loop where some of the others terminate. For example, 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

68 
\begin{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

69 
{\out 1. ALL x. f(x) = g(f(g(x))) ==> f(0) = f(0)+0} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

70 
\end{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

71 
is solved by {\tt Simp_tac}, but {\tt Asm_simp_tac} and {\tt Asm_simp_tac} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

72 
loop because the rewrite rule $f(\Var{x}) = f(g(f(\Var{x})))$ extracted from 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

73 
the assumption does not terminate. Isabelle notices certain simple forms of 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

74 
nontermination, but not this one. 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

75 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

76 
\begin{warn} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

77 
Since \verb$Asm_full_simp_tac$ works from left to right, it sometimes 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

78 
misses opportunities for simplification: given the subgoal 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

79 
\begin{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

80 
{\out [ P(f(a)); f(a) = t ] ==> ...} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

81 
\end{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

82 
\verb$Asm_full_simp_tac$ will not simplify the first assumption using the 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

83 
second but will leave the assumptions unchanged. See 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

84 
\S\ref{sec:reorderingasms} for ways around this problem. 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

85 
\end{warn} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

86 

3108  87 
Using the simplifier effectively may take a bit of experimentation. 
88 
\index{tracing!of simplification}\index{*trace_simp} The tactics can 

89 
be traced by setting \verb$trace_simp := true$. 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

90 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

91 
There is not just one global current simpset, but one associated with each 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

92 
theory as well. How are these simpset built up? 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

93 
\begin{enumerate} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

94 
\item When loading {\tt T.thy}, the current simpset is initialized with the 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

95 
union of the simpsets associated with all the ancestors of {\tt T}. In 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

96 
addition, certain constructs in {\tt T} may add new rules to the simpset, 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

97 
e.g.\ \ttindex{datatype} and \ttindex{primrec} in \HOL. Definitions are not 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

98 
added automatically! 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

99 
\item The script in {\tt T.ML} may manipulate the current simpset further by 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

100 
explicitly adding/deleting theorems to/from it (see below). 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

101 
\item After {\tt T.ML} has been read, the current simpset is associated with 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

102 
theory {\tt T}. 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

103 
\end{enumerate} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

104 
The current simpset is manipulated by 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

105 
\begin{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

106 
Addsimps, Delsimps: thm list > unit 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

107 
\end{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

108 
\begin{ttdescription} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

109 
\item[\ttindexbold{Addsimps} $thms$] adds $thms$ to the current simpset 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

110 
\item[\ttindexbold{Delsimps} $thms$] deletes $thms$ from the current simpset 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

111 
\end{ttdescription} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

112 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

113 
Generally useful simplification rules $\Var{n}+0 = \Var{n}$ should be added 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

114 
to the current simpset right after they have been proved. Those of a more 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

115 
specific nature (e.g.\ the laws of de~Morgan, which alter the structure of a 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

116 
formula) should only be added for specific proofs and deleted again 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

117 
afterwards. Conversely, it may also happen that a generally useful rule needs 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

118 
to be removed for a certain proof and is added again afterwards. Well 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

119 
designed simpsets need few temporary additions or deletions. 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

120 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

121 
\begin{warn} 
2479  122 
The union of the ancestor simpsets (as described above) is not always a good 
123 
simpset for the new theory. If some ancestors have deleted simplification 

124 
rules because they are no longer wanted, while others have left those rules 

125 
in, then the union will contain the unwanted rules. If the ancestor 

126 
simpsets differ in other components (the subgoaler, solver, looper or rule 

127 
preprocessor: see below), then you cannot be sure which version of that 

128 
component will be inherited. You may have to set the component explicitly 

129 
for the new theory's simpset by an assignment of the form 

130 
{\tt simpset := \dots}. 

131 
\end{warn} 

132 

133 
\begin{warn} 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

134 
If you execute proofs interactively, or load them from an ML file without 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

135 
associated {\tt .thy} file, you must set the current simpset by calling 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

136 
\ttindex{set_current_thy}~{\tt"}$T${\tt"}, where $T$ is the name of the 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

137 
theory you want to work in. If you have just loaded $T$, this is not 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

138 
necessary. 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

139 
\end{warn} 
104  140 

141 

286  142 
\section{Simplification sets}\index{simplification sets} 
3134  143 
The simplification tactics are controlled by {\bf simpsets}. These 
144 
consist of several components, including rewrite rules, congruence 

145 
rules, the subgoaler, the solver and the looper. The simplifier 

146 
should be set up with sensible defaults so that most simplifier calls 

147 
specify only rewrite rules. Experienced users can exploit the other 

148 
components to streamline proofs. 

323  149 

3108  150 
Logics like \HOL, which support a current 
151 
simpset\index{simpset!current}, store its value in an ML reference 

152 
variable called {\tt simpset}\index{simpset@{\tt simpset} ML value}. 

104  153 

332  154 
\subsection{Rewrite rules} 
155 
\index{rewrite rules(} 

323  156 
Rewrite rules are theorems expressing some form of equality: 
157 
\begin{eqnarray*} 

158 
Suc(\Var{m}) + \Var{n} &=& \Var{m} + Suc(\Var{n}) \\ 

159 
\Var{P}\conj\Var{P} &\bimp& \Var{P} \\ 

714  160 
\Var{A} \un \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\} 
323  161 
\end{eqnarray*} 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

162 
Conditional rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} = 
3108  163 
0$ are permitted; the conditions can be arbitrary formulas. 
104  164 

323  165 
Internally, all rewrite rules are translated into metaequalities, theorems 
166 
with conclusion $lhs \equiv rhs$. Each simpset contains a function for 

167 
extracting equalities from arbitrary theorems. For example, 

168 
$\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\} \equiv 

169 
False$. This function can be installed using \ttindex{setmksimps} but only 

170 
the definer of a logic should need to do this; see \S\ref{sec:setmksimps}. 

171 
The function processes theorems added by \ttindex{addsimps} as well as 

172 
local assumptions. 

104  173 

174 

332  175 
\begin{warn} 
1101  176 
The simplifier will accept all standard rewrite rules: those 
177 
where all unknowns are of base type. Hence ${\Var{i}+(\Var{j}+\Var{k})} = 

714  178 
{(\Var{i}+\Var{j})+\Var{k}}$ is ok. 
179 

180 
It will also deal gracefully with all rules whose lefthand sides are 

3950  181 
socalled {\em higherorder patterns}~\cite{nipkowpatterns}. 
182 
\indexbold{higherorder pattern}\indexbold{pattern, higherorder} 

183 
These are terms in $\beta$normal form (this will always be the case unless 

184 
you have done something strange) where each occurrence of an unknown is of 

185 
the form $\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are distinct bound 

186 
variables. Hence $(\forall x.\Var{P}(x) \land \Var{Q}(x)) \bimp (\forall 

187 
x.\Var{P}(x)) \land (\forall x.\Var{Q}(x))$ is also ok, in both directions. 

714  188 

189 
In some rare cases the rewriter will even deal with quite general rules: for 

190 
example ${\Var{f}(\Var{x})\in range(\Var{f})} = True$ rewrites $g(a) \in 

191 
range(g)$ to $True$, but will fail to match $g(h(b)) \in range(\lambda 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

192 
x.g(h(x)))$. However, you can replace the offending subterms (in our case 
714  193 
$\Var{f}(\Var{x})$, which is not a pattern) by adding new variables and 
194 
conditions: $\Var{y} = \Var{f}(\Var{x}) \Imp \Var{y}\in range(\Var{f}) 

195 
= True$ is acceptable as a conditional rewrite rule since conditions can 

196 
be arbitrary terms. 

197 

198 
There is no restriction on the form of the righthand sides. 

104  199 
\end{warn} 
200 

332  201 
\index{rewrite rules)} 
202 

203 
\subsection{*Congruence rules}\index{congruence rules} 

104  204 
Congruence rules are metaequalities of the form 
3108  205 
\[ \dots \Imp 
104  206 
f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}). 
207 
\] 

323  208 
This governs the simplification of the arguments of~$f$. For 
104  209 
example, some arguments can be simplified under additional assumptions: 
210 
\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}} 

211 
\Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2}) 

212 
\] 

323  213 
Given this rule, the simplifier assumes $Q@1$ and extracts rewrite rules 
214 
from it when simplifying~$P@2$. Such local assumptions are effective for 

698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

215 
rewriting formulae such as $x=0\imp y+x=y$. The local assumptions are also 
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

216 
provided as theorems to the solver; see page~\pageref{sec:simpsolver} below. 
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

217 

23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

218 
Here are some more examples. The congruence rule for bounded quantifiers 
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

219 
also supplies contextual information, this time about the bound variable: 
286  220 
\begin{eqnarray*} 
221 
&&\List{\Var{A}=\Var{B};\; 

222 
\Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\ 

223 
&&\qquad\qquad 

224 
(\forall x\in \Var{A}.\Var{P}(x)) = (\forall x\in \Var{B}.\Var{Q}(x)) 

225 
\end{eqnarray*} 

323  226 
The congruence rule for conditional expressions can supply contextual 
227 
information for simplifying the arms: 

104  228 
\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~ 
229 
\neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp 

230 
if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d}) 

231 
\] 

698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

232 
A congruence rule can also {\em prevent\/} simplification of some arguments. 
104  233 
Here is an alternative congruence rule for conditional expressions: 
234 
\[ \Var{p}=\Var{q} \Imp 

235 
if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b}) 

236 
\] 

237 
Only the first argument is simplified; the others remain unchanged. 

238 
This can make simplification much faster, but may require an extra case split 

239 
to prove the goal. 

240 

2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

241 
Congruence rules are added/deleted using 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

242 
\ttindexbold{addeqcongs}/\ttindex{deleqcongs}. 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

243 
Their conclusion must be a metaequality, as in the examples above. It is more 
104  244 
natural to derive the rules with objectlogic equality, for example 
245 
\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}} 

246 
\Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2}), 

247 
\] 

2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

248 
Each objectlogic should define operators called \ttindex{addcongs} and 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

249 
\ttindex{delcongs} that expects objectequalities and translates them into 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

250 
metaequalities. 
104  251 

323  252 
\subsection{*The subgoaler} 
104  253 
The subgoaler is the tactic used to solve subgoals arising out of 
254 
conditional rewrite rules or congruence rules. The default should be 

255 
simplification itself. Occasionally this strategy needs to be changed. For 

256 
example, if the premise of a conditional rule is an instance of its 

257 
conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m} < \Var{n}$, the 

258 
default strategy could loop. 

259 

260 
The subgoaler can be set explicitly with \ttindex{setsubgoaler}. For 

261 
example, the subgoaler 

262 
\begin{ttbox} 

332  263 
fun subgoal_tac ss = assume_tac ORELSE' 
264 
resolve_tac (prems_of_ss ss) ORELSE' 

104  265 
asm_simp_tac ss; 
266 
\end{ttbox} 

332  267 
tries to solve the subgoal by assumption or with one of the premises, calling 
104  268 
simplification only if that fails; here {\tt prems_of_ss} extracts the 
269 
current premises from a simpset. 

270 

698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset

271 
\subsection{*The solver}\label{sec:simpsolver} 
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

272 
The solver is a pair of tactics that attempt to solve a subgoal after 
286  273 
simplification. Typically it just proves trivial subgoals such as {\tt 
323  274 
True} and $t=t$. It could use sophisticated means such as {\tt 
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3112
diff
changeset

275 
blast_tac}, though that could make simplification expensive. 
286  276 

3108  277 
Rewriting does not instantiate unknowns. For example, rewriting 
278 
cannot prove $a\in \Var{A}$ since this requires 

279 
instantiating~$\Var{A}$. The solver, however, is an arbitrary tactic 

280 
and may instantiate unknowns as it pleases. This is the only way the 

281 
simplifier can handle a conditional rewrite rule whose condition 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

282 
contains extra variables. When a simplification tactic is to be 
3108  283 
combined with other provers, especially with the classical reasoner, 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

284 
it is important whether it can be considered safe or not. Therefore, 
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

285 
the solver is split into a safe and an unsafe part. Both parts can be 
3108  286 
set independently, using either \ttindex{setSSolver} with a safe 
287 
tactic as argument, or \ttindex{setSolver} with an unsafe tactic. 

288 
Additional solvers, which are tried after the already set solvers, may 

289 
be added using \ttindex{addSSolver} and \ttindex{addSolver}. 

2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

290 

3108  291 
The standard simplification strategy solely uses the unsafe solver, 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

292 
which is appropriate in most cases. But for special applications where 
3108  293 
the simplification process is not allowed to instantiate unknowns 
294 
within the goal, the tactic \ttindexbold{safe_asm_full_simp_tac} is 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

295 
provided. It uses the \emph{safe} solver for the current subgoal, but 
3108  296 
applies ordinary unsafe {\tt asm_full_simp_tac} for recursive internal 
297 
simplifications (for conditional rules or congruences). 

323  298 

299 
\index{assumptions!in simplification} 

286  300 
The tactic is presented with the full goal, including the asssumptions. 
301 
Hence it can use those assumptions (say by calling {\tt assume_tac}) even 

302 
inside {\tt simp_tac}, which otherwise does not use assumptions. The 

303 
solver is also supplied a list of theorems, namely assumptions that hold in 

304 
the local context. 

104  305 

323  306 
The subgoaler is also used to solve the premises of congruence rules, which 
307 
are usually of the form $s = \Var{x}$, where $s$ needs to be simplified and 

308 
$\Var{x}$ needs to be instantiated with the result. Hence the subgoaler 

309 
should call the simplifier at some point. The simplifier will then call the 

310 
solver, which must therefore be prepared to solve goals of the form $t = 

311 
\Var{x}$, usually by reflexivity. In particular, reflexivity should be 

3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3112
diff
changeset

312 
tried before any of the fancy tactics like {\tt blast_tac}. 
323  313 

3108  314 
It may even happen that due to simplification the subgoal is no longer 
315 
an equality. For example $False \bimp \Var{Q}$ could be rewritten to 

316 
$\neg\Var{Q}$. To cover this case, the solver could try resolving 

317 
with the theorem $\neg False$. 

104  318 

319 
\begin{warn} 

3108  320 
If the simplifier aborts with the message {\tt Failed congruence 
321 
proof!}, then the subgoaler or solver has failed to prove a 

322 
premise of a congruence rule. This should never occur under normal 

323 
circumstances; it indicates that some congruence rule, or possibly 

324 
the subgoaler or solver, is faulty. 

104  325 
\end{warn} 
326 

323  327 

328 
\subsection{*The looper} 

104  329 
The looper is a tactic that is applied after simplification, in case the 
330 
solver failed to solve the simplified goal. If the looper succeeds, the 

331 
simplification process is started all over again. Each of the subgoals 

332 
generated by the looper is attacked in turn, in reverse order. A 

333 
typical looper is case splitting: the expansion of a conditional. Another 

334 
possibility is to apply an elimination rule on the assumptions. More 

335 
adventurous loopers could start an induction. The looper is set with 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

336 
\ttindex{setloop}. Additional loopers, which are tried after the already set 
2567  337 
looper, may be added with \ttindex{addloop}. 
104  338 

339 

340 
\begin{figure} 

323  341 
\index{*simpset ML type} 
2567  342 
\index{*empty_ss} 
343 
\index{*rep_ss} 

344 
\index{*prems_of_ss} 

345 
\index{*setloop} 

346 
\index{*addloop} 

2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

347 
\index{*setSSolver} 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

348 
\index{*addSSolver} 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

349 
\index{*setSolver} 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

350 
\index{*addSolver} 
2567  351 
\index{*setsubgoaler} 
352 
\index{*setmksimps} 

323  353 
\index{*addsimps} 
354 
\index{*delsimps} 

2567  355 
\index{*addeqcongs} 
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

356 
\index{*deleqcongs} 
323  357 
\index{*merge_ss} 
2567  358 
\index{*simpset} 
359 
\index{*Addsimps} 

360 
\index{*Delsimps} 

361 
\index{*simp_tac} 

362 
\index{*asm_simp_tac} 

363 
\index{*full_simp_tac} 

364 
\index{*asm_full_simp_tac} 

2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

365 
\index{*safe_asm_full_simp_tac} 
2567  366 
\index{*Simp_tac} 
367 
\index{*Asm_simp_tac} 

368 
\index{*Full_simp_tac} 

369 
\index{*Asm_full_simp_tac} 

370 

104  371 
\begin{ttbox} 
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3112
diff
changeset

372 
infix 4 setsubgoaler setloop addloop 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3112
diff
changeset

373 
setSSolver addSSolver setSolver addSolver 
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

374 
setmksimps addsimps delsimps addeqcongs deleqcongs; 
104  375 

376 
signature SIMPLIFIER = 

377 
sig 

378 
type simpset 

2567  379 
val empty_ss: simpset 
3134  380 
val rep_ss: simpset > {\ttlbrace}simps: thm list, procs: string list, 
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3112
diff
changeset

381 
congs: thm list, 
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

382 
subgoal_tac: simpset > int > tactic, 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

383 
loop_tac: int > tactic, 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

384 
finish_tac: thm list > int > tactic, 
3134  385 
unsafe_finish_tac: thm list > int > tactic{\ttrbrace} 
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

386 
val setsubgoaler: simpset * (simpset > int > tactic) > simpset 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

387 
val setloop: simpset * (int > tactic) > simpset 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

388 
val addloop: simpset * (int > tactic) > simpset 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

389 
val setSSolver: simpset * (thm list > int > tactic) > simpset 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

390 
val addSSolver: simpset * (thm list > int > tactic) > simpset 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

391 
val setSolver: simpset * (thm list > int > tactic) > simpset 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

392 
val addSolver: simpset * (thm list > int > tactic) > simpset 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

393 
val setmksimps: simpset * (thm > thm list) > simpset 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

394 
val addsimps: simpset * thm list > simpset 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

395 
val delsimps: simpset * thm list > simpset 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

396 
val addeqcongs: simpset * thm list > simpset 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

397 
val deleqcongs: simpset * thm list > simpset 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

398 
val merge_ss: simpset * simpset > simpset 
2567  399 
val prems_of_ss: simpset > thm list 
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

400 
val simpset: simpset ref 
2567  401 
val Addsimps: thm list > unit 
402 
val Delsimps: thm list > unit 

2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

403 
val simp_tac: simpset > int > tactic 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

404 
val asm_simp_tac: simpset > int > tactic 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

405 
val full_simp_tac: simpset > int > tactic 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

406 
val asm_full_simp_tac: simpset > int > tactic 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

407 
val safe_asm_full_simp_tac: simpset > int > tactic 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

408 
val Simp_tac: int > tactic 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

409 
val Asm_simp_tac: int > tactic 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

410 
val Full_simp_tac: int > tactic 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

411 
val Asm_full_simp_tac: int > tactic 
104  412 
end; 
413 
\end{ttbox} 

323  414 
\caption{The simplifier primitives} \label{SIMPLIFIER} 
104  415 
\end{figure} 
416 

417 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

418 
\section{The simplification tactics} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

419 
\label{simptactics} 
323  420 
\index{simplification!tactics} 
421 
\index{tactics!simplification} 

104  422 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

423 
The actual simplification work is performed by the following basic tactics: 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

424 
\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac}, 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

425 
\ttindexbold{full_simp_tac} and \ttindexbold{asm_full_simp_tac}. They work 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

426 
exactly like their namesakes in \S\ref{sec:simpfordummies}, except that 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

427 
they are explicitly supplied with a simpset. This is because the ones in 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

428 
\S\ref{sec:simpfordummies} are defined in terms of the ones above, e.g. 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

429 
\begin{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

430 
fun Simp_tac i = simp_tac (!simpset) i; 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

431 
\end{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

432 
where \ttindex{!simpset} is the current simpset\index{simpset!current}. 
104  433 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

434 
The rewriting strategy of all four tactics is strictly bottom up, except for 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

435 
congruence rules, which are applied while descending into a term. Conditions 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

436 
in conditional rewrite rules are solved recursively before the rewrite rule 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

437 
is applied. 
104  438 

3108  439 
The infix operation \ttindex{addsimps} adds rewrite rules to a 
440 
simpset, while \ttindex{delsimps} deletes them. They are used to 

441 
implement \ttindex{Addsimps} and \ttindex{Delsimps}, e.g. 

1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

442 
\begin{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

443 
fun Addsimps thms = (simpset := (!simpset addsimps thms)); 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

444 
\end{ttbox} 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

445 
and can also be used directly, even in the presence of a current simpset. For 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

446 
example 
1213  447 
\begin{ttbox} 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

448 
Addsimps \(thms\); 
2479  449 
by (Simp_tac \(i\)); 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

450 
Delsimps \(thms\); 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

451 
\end{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

452 
can be compressed into 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

453 
\begin{ttbox} 
2479  454 
by (simp_tac (!simpset addsimps \(thms\)) \(i\)); 
1213  455 
\end{ttbox} 
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

456 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

457 
The simpset associated with a particular theory can be retrieved via the name 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

458 
of the theory using the function 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

459 
\begin{ttbox} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

460 
simpset_of: string > simpset 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

461 
\end{ttbox}\index{*simpset_of} 
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

462 

71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset

463 
To remind yourself of what is in a simpset, use the function \verb$rep_ss$ to 
104  464 
return its simplification and congruence rules. 
465 

286  466 
\section{Examples using the simplifier} 
3112  467 
\index{examples!of simplification} Assume we are working within {\tt 
468 
FOL} (cf.\ \texttt{FOL/ex/Nat}) and that 

323  469 
\begin{ttdescription} 
470 
\item[Nat.thy] 

471 
is a theory including the constants $0$, $Suc$ and $+$, 

472 
\item[add_0] 

473 
is the rewrite rule $0+\Var{n} = \Var{n}$, 

474 
\item[add_Suc] 

475 
is the rewrite rule $Suc(\Var{m})+\Var{n} = Suc(\Var{m}+\Var{n})$, 

476 
\item[induct] 

477 
is the induction rule $\List{\Var{P}(0);\; \Forall x. \Var{P}(x)\Imp 

478 
\Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$. 

479 
\end{ttdescription} 

3112  480 
We augment the implicit simpset of {\FOL} with the basic rewrite rules 
481 
for natural numbers: 

104  482 
\begin{ttbox} 
3112  483 
Addsimps [add_0, add_Suc]; 
104  484 
\end{ttbox} 
323  485 

486 
\subsection{A trivial example} 

286  487 
Proofs by induction typically involve simplification. Here is a proof 
488 
that~0 is a right identity: 

104  489 
\begin{ttbox} 
490 
goal Nat.thy "m+0 = m"; 

491 
{\out Level 0} 

492 
{\out m + 0 = m} 

493 
{\out 1. m + 0 = m} 

286  494 
\end{ttbox} 
495 
The first step is to perform induction on the variable~$m$. This returns a 

496 
base case and inductive step as two subgoals: 

497 
\begin{ttbox} 

104  498 
by (res_inst_tac [("n","m")] induct 1); 
499 
{\out Level 1} 

500 
{\out m + 0 = m} 

501 
{\out 1. 0 + 0 = 0} 

502 
{\out 2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)} 

503 
\end{ttbox} 

286  504 
Simplification solves the first subgoal trivially: 
104  505 
\begin{ttbox} 
3112  506 
by (Simp_tac 1); 
104  507 
{\out Level 2} 
508 
{\out m + 0 = m} 

509 
{\out 1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)} 

510 
\end{ttbox} 

3112  511 
The remaining subgoal requires \ttindex{Asm_simp_tac} in order to use the 
104  512 
induction hypothesis as a rewrite rule: 
513 
\begin{ttbox} 

3112  514 
by (Asm_simp_tac 1); 
104  515 
{\out Level 3} 
516 
{\out m + 0 = m} 

517 
{\out No subgoals!} 

518 
\end{ttbox} 

519 

323  520 
\subsection{An example of tracing} 
3108  521 
\index{tracing!of simplification(}\index{*trace_simp} 
323  522 
Let us prove a similar result involving more complex terms. The two 
523 
equations together can be used to prove that addition is commutative. 

104  524 
\begin{ttbox} 
525 
goal Nat.thy "m+Suc(n) = Suc(m+n)"; 

526 
{\out Level 0} 

527 
{\out m + Suc(n) = Suc(m + n)} 

528 
{\out 1. m + Suc(n) = Suc(m + n)} 

286  529 
\end{ttbox} 
530 
We again perform induction on~$m$ and get two subgoals: 

531 
\begin{ttbox} 

104  532 
by (res_inst_tac [("n","m")] induct 1); 
533 
{\out Level 1} 

534 
{\out m + Suc(n) = Suc(m + n)} 

535 
{\out 1. 0 + Suc(n) = Suc(0 + n)} 

286  536 
{\out 2. !!x. x + Suc(n) = Suc(x + n) ==>} 
537 
{\out Suc(x) + Suc(n) = Suc(Suc(x) + n)} 

538 
\end{ttbox} 

539 
Simplification solves the first subgoal, this time rewriting two 

540 
occurrences of~0: 

541 
\begin{ttbox} 

3112  542 
by (Simp_tac 1); 
104  543 
{\out Level 2} 
544 
{\out m + Suc(n) = Suc(m + n)} 

286  545 
{\out 1. !!x. x + Suc(n) = Suc(x + n) ==>} 
546 
{\out Suc(x) + Suc(n) = Suc(Suc(x) + n)} 

104  547 
\end{ttbox} 
548 
Switching tracing on illustrates how the simplifier solves the remaining 

549 
subgoal: 

550 
\begin{ttbox} 

551 
trace_simp := true; 

3112  552 
by (Asm_simp_tac 1); 
323  553 
\ttbreak 
3112  554 
{\out Adding rewrite rule:} 
555 
{\out .x + Suc(n) == Suc(.x + n)} 

323  556 
\ttbreak 
104  557 
{\out Rewriting:} 
3112  558 
{\out Suc(.x) + Suc(n) == Suc(.x + Suc(n))} 
323  559 
\ttbreak 
104  560 
{\out Rewriting:} 
3112  561 
{\out .x + Suc(n) == Suc(.x + n)} 
323  562 
\ttbreak 
104  563 
{\out Rewriting:} 
3112  564 
{\out Suc(.x) + n == Suc(.x + n)} 
565 
\ttbreak 

566 
{\out Rewriting:} 

567 
{\out Suc(Suc(.x + n)) = Suc(Suc(.x + n)) == True} 

323  568 
\ttbreak 
104  569 
{\out Level 3} 
570 
{\out m + Suc(n) = Suc(m + n)} 

571 
{\out No subgoals!} 

572 
\end{ttbox} 

286  573 
Many variations are possible. At Level~1 (in either example) we could have 
574 
solved both subgoals at once using the tactical \ttindex{ALLGOALS}: 

104  575 
\begin{ttbox} 
3112  576 
by (ALLGOALS Asm_simp_tac); 
104  577 
{\out Level 2} 
578 
{\out m + Suc(n) = Suc(m + n)} 

579 
{\out No subgoals!} 

580 
\end{ttbox} 

3108  581 
\index{tracing!of simplification)} 
104  582 

323  583 
\subsection{Free variables and simplification} 
104  584 
Here is a conjecture to be proved for an arbitrary function~$f$ satisfying 
323  585 
the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$: 
104  586 
\begin{ttbox} 
587 
val [prem] = goal Nat.thy 

588 
"(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; 

589 
{\out Level 0} 

590 
{\out f(i + j) = i + f(j)} 

591 
{\out 1. f(i + j) = i + f(j)} 

323  592 
\ttbreak 
286  593 
{\out val prem = "f(Suc(?n)) = Suc(f(?n))} 
594 
{\out [!!n. f(Suc(n)) = Suc(f(n))]" : thm} 

323  595 
\end{ttbox} 
596 
In the theorem~{\tt prem}, note that $f$ is a free variable while 

597 
$\Var{n}$ is a schematic variable. 

598 
\begin{ttbox} 

104  599 
by (res_inst_tac [("n","i")] induct 1); 
600 
{\out Level 1} 

601 
{\out f(i + j) = i + f(j)} 

602 
{\out 1. f(0 + j) = 0 + f(j)} 

603 
{\out 2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)} 

604 
\end{ttbox} 

605 
We simplify each subgoal in turn. The first one is trivial: 

606 
\begin{ttbox} 

3112  607 
by (Simp_tac 1); 
104  608 
{\out Level 2} 
609 
{\out f(i + j) = i + f(j)} 

610 
{\out 1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)} 

611 
\end{ttbox} 

3112  612 
The remaining subgoal requires rewriting by the premise, so we add it 
613 
to the current simpset:\footnote{The previous simplifier required 

614 
congruence rules for function variables like~$f$ in order to 

615 
simplify their arguments. It was more general than the current 

616 
simplifier, but harder to use and slower. The present simplifier 

617 
can be given congruence rules to realize nonstandard simplification 

618 
of a function's arguments, but this is seldom necessary.} 

104  619 
\begin{ttbox} 
3112  620 
by (asm_simp_tac (!simpset addsimps [prem]) 1); 
104  621 
{\out Level 3} 
622 
{\out f(i + j) = i + f(j)} 

623 
{\out No subgoals!} 

624 
\end{ttbox} 

625 

1213  626 
\subsection{Reordering assumptions} 
627 
\label{sec:reorderingasms} 

628 
\index{assumptions!reordering} 

629 

630 
As mentioned above, \ttindex{asm_full_simp_tac} may require the assumptions 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

631 
to be permuted to be more effective. Given the subgoal 
1213  632 
\begin{ttbox} 
633 
{\out 1. [ P(f(a)); Q; f(a) = t; R ] ==> S} 

634 
\end{ttbox} 

635 
we can rotate the assumptions two positions to the right 

636 
\begin{ttbox} 

637 
by (rotate_tac ~2 1); 

638 
\end{ttbox} 

639 
to obtain 

640 
\begin{ttbox} 

641 
{\out 1. [ f(a) = t; R; P(f(a)); Q ] ==> S} 

642 
\end{ttbox} 

643 
which enables \verb$asm_full_simp_tac$ to simplify \verb$P(f(a))$ to 

644 
\verb$P(t)$. 

645 

646 
Since rotation alone cannot produce arbitrary permutations, you can also pick 

647 
out a particular assumption which needs to be rewritten and move it the the 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

648 
right end of the assumptions. In the above case rotation can be replaced by 
1213  649 
\begin{ttbox} 
650 
by (dres_inst_tac [("psi","P(f(a))")] asm_rl 1); 

651 
\end{ttbox} 

652 
which is more directed and leads to 

653 
\begin{ttbox} 

654 
{\out 1. [ Q; f(a) = t; R; P(f(a)) ] ==> S} 

655 
\end{ttbox} 

656 

657 
Note that reordering assumptions usually leads to brittle proofs and should 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset

658 
therefore be avoided. Future versions of \verb$asm_full_simp_tac$ may remove 
1213  659 
the need for such manipulations. 
286  660 

332  661 
\section{Permutative rewrite rules} 
323  662 
\index{rewrite rules!permutative(} 
663 

664 
A rewrite rule is {\bf permutative} if the lefthand side and righthand 

665 
side are the same up to renaming of variables. The most common permutative 

666 
rule is commutativity: $x+y = y+x$. Other examples include $(xy)z = 

667 
(xz)y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$ 

668 
for sets. Such rules are common enough to merit special attention. 

669 

670 
Because ordinary rewriting loops given such rules, the simplifier employs a 

671 
special strategy, called {\bf ordered rewriting}\index{rewriting!ordered}. 

3108  672 
There is a standard lexicographic ordering on terms. A permutative rewrite 
323  673 
rule is applied only if it decreases the given term with respect to this 
674 
ordering. For example, commutativity rewrites~$b+a$ to $a+b$, but then 

675 
stops because $a+b$ is strictly less than $b+a$. The BoyerMoore theorem 

676 
prover~\cite{bm88book} also employs ordered rewriting. 

677 

678 
Permutative rewrite rules are added to simpsets just like other rewrite 

679 
rules; the simplifier recognizes their special status automatically. They 

680 
are most effective in the case of associativecommutative operators. 

681 
(Associativity by itself is not permutative.) When dealing with an 

682 
ACoperator~$f$, keep the following points in mind: 

683 
\begin{itemize}\index{associativecommutative operators} 

684 
\item The associative law must always be oriented from left to right, namely 

685 
$f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if used with 

686 
commutativity, leads to looping! Future versions of Isabelle may remove 

687 
this restriction. 

688 

689 
\item To complete your set of rewrite rules, you must add not just 

690 
associativity~(A) and commutativity~(C) but also a derived rule, {\bf 

691 
leftcommutativity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$. 

692 
\end{itemize} 

693 
Ordered rewriting with the combination of A, C, and~LC sorts a term 

694 
lexicographically: 

695 
\[\def\maps#1{\stackrel{#1}{\longmapsto}} 

696 
(b+c)+a \maps{A} b+(c+a) \maps{C} b+(a+c) \maps{LC} a+(b+c) \] 

697 
Martin and Nipkow~\cite{martinnipkow} discuss the theory and give many 

698 
examples; other algebraic structures are amenable to ordered rewriting, 

699 
such as boolean rings. 

700 

3108  701 
\subsection{Example: sums of natural numbers} 
702 
This example is set in \HOL\ (see \texttt{HOL/ex/NatSum}). Theory 

703 
\thydx{Arith} contains natural numbers arithmetic. Its associated 

704 
simpset contains many arithmetic laws including distributivity 

705 
of~$\times$ over~$+$, while {\tt add_ac} is a list consisting of the 

706 
A, C and LC laws for~$+$ on type \texttt{nat}. Let us prove the 

707 
theorem 

323  708 
\[ \sum@{i=1}^n i = n\times(n+1)/2. \] 
709 
% 

710 
A functional~{\tt sum} represents the summation operator under the 

3108  711 
interpretation ${\tt sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We 
712 
extend {\tt Arith} using a theory file: 

323  713 
\begin{ttbox} 
714 
NatSum = Arith + 

1387  715 
consts sum :: [nat=>nat, nat] => nat 
4245  716 
primrec "sum" nat 
717 
"sum f 0 = 0" 

718 
"sum f (Suc n) = f(n) + sum f n" 

323  719 
end 
720 
\end{ttbox} 

4245  721 
The \texttt{primrec} declaration automatically adds rewrite rules for 
722 
\texttt{sum} to the default simpset. We now insert the ACrules for~$+$: 

323  723 
\begin{ttbox} 
4245  724 
Addsimps add_ac; 
323  725 
\end{ttbox} 
3108  726 
Our desired theorem now reads ${\tt sum} \, (\lambda i.i) \, (n+1) = 
323  727 
n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$: 
728 
\begin{ttbox} 

3108  729 
goal NatSum.thy "2 * sum (\%i.i) (Suc n) = n * Suc n"; 
323  730 
{\out Level 0} 
3108  731 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
732 
{\out 1. 2 * sum (\%i. i) (Suc n) = n * Suc n} 

323  733 
\end{ttbox} 
3108  734 
Induction should not be applied until the goal is in the simplest 
735 
form: 

323  736 
\begin{ttbox} 
4245  737 
by (Simp_tac 1); 
323  738 
{\out Level 1} 
3108  739 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
740 
{\out 1. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n} 

323  741 
\end{ttbox} 
3108  742 
Ordered rewriting has sorted the terms in the lefthand side. The 
743 
subgoal is now ready for induction: 

323  744 
\begin{ttbox} 
4245  745 
by (induct_tac "n" 1); 
323  746 
{\out Level 2} 
3108  747 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
748 
{\out 1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0} 

323  749 
\ttbreak 
4245  750 
{\out 2. !!n. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n} 
751 
{\out ==> Suc n + (sum (\%i. i) (Suc n) + sum (\%i. i) (Suc n)) =} 

752 
{\out Suc n * Suc n} 

323  753 
\end{ttbox} 
754 
Simplification proves both subgoals immediately:\index{*ALLGOALS} 

755 
\begin{ttbox} 

4245  756 
by (ALLGOALS Asm_simp_tac); 
323  757 
{\out Level 3} 
3108  758 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 
323  759 
{\out No subgoals!} 
760 
\end{ttbox} 

4245  761 
Simplification cannot prove the induction step if we omit {\tt add_ac} from 
762 
the simpset. Observe that like terms have not been collected: 

323  763 
\begin{ttbox} 
4245  764 
{\out Level 3} 
765 
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} 

766 
{\out 1. !!n. n + sum (\%i. i) n + (n + sum (\%i. i) n) = n + n * n} 

767 
{\out ==> n + (n + sum (\%i. i) n) + (n + (n + sum (\%i. i) n)) =} 

768 
{\out n + (n + (n + n * n))} 

323  769 
\end{ttbox} 
770 
Ordered rewriting proves this by sorting the lefthand side. Proving 

771 
arithmetic theorems without ordered rewriting requires explicit use of 

772 
commutativity. This is tedious; try it and see! 

773 

774 
Ordered rewriting is equally successful in proving 

775 
$\sum@{i=1}^n i^3 = n^2\times(n+1)^2/4$. 

776 

777 

778 
\subsection{Reorienting equalities} 

779 
Ordered rewriting with the derived rule {\tt symmetry} can reverse equality 

780 
signs: 

781 
\begin{ttbox} 

782 
val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" 

3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3112
diff
changeset

783 
(fn _ => [Blast_tac 1]); 
323  784 
\end{ttbox} 
785 
This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs 

786 
in the conclusion but not~$s$, can often be brought into the right form. 

787 
For example, ordered rewriting with {\tt symmetry} can prove the goal 

788 
\[ f(a)=b \conj f(a)=c \imp b=c. \] 

789 
Here {\tt symmetry} reverses both $f(a)=b$ and $f(a)=c$ 

790 
because $f(a)$ is lexicographically greater than $b$ and~$c$. These 

791 
reoriented equations, as rewrite rules, replace $b$ and~$c$ in the 

792 
conclusion by~$f(a)$. 

793 

794 
Another example is the goal $\neg(t=u) \imp \neg(u=t)$. 

795 
The differing orientations make this appear difficult to prove. Ordered 

796 
rewriting with {\tt symmetry} makes the equalities agree. (Without 

797 
knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$ 

798 
or~$u=t$.) Then the simplifier can prove the goal outright. 

799 

800 
\index{rewrite rules!permutative)} 

801 

802 

803 
\section{*Setting up the simplifier}\label{sec:settingupsimp} 

804 
\index{simplification!setting up} 

286  805 

806 
Setting up the simplifier for new logics is complicated. This section 

323  807 
describes how the simplifier is installed for intuitionistic firstorder 
808 
logic; the code is largely taken from {\tt FOL/simpdata.ML}. 

286  809 

323  810 
The simplifier and the case splitting tactic, which reside on separate 
811 
files, are not part of Pure Isabelle. They must be loaded explicitly: 

286  812 
\begin{ttbox} 
813 
use "../Provers/simplifier.ML"; 

814 
use "../Provers/splitter.ML"; 

815 
\end{ttbox} 

816 

817 
Simplification works by reducing various objectequalities to 

323  818 
metaequality. It requires rules stating that equal terms and equivalent 
819 
formulae are also equal at the metalevel. The rule declaration part of 

3108  820 
the file {\tt FOL/IFOL.thy} contains the two lines 
323  821 
\begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem} 
286  822 
eq_reflection "(x=y) ==> (x==y)" 
823 
iff_reflection "(P<>Q) ==> (P==Q)" 

824 
\end{ttbox} 

323  825 
Of course, you should only assert such rules if they are true for your 
286  826 
particular logic. In Constructive Type Theory, equality is a ternary 
827 
relation of the form $a=b\in A$; the type~$A$ determines the meaning of the 

332  828 
equality essentially as a partial equivalence relation. The present 
323  829 
simplifier cannot be used. Rewriting in {\tt CTT} uses another simplifier, 
830 
which resides in the file {\tt typedsimp.ML} and is not documented. Even 

831 
this does not work for later variants of Constructive Type Theory that use 

832 
intensional equality~\cite{nordstrom90}. 

286  833 

834 

835 
\subsection{A collection of standard rewrite rules} 

836 
The file begins by proving lots of standard rewrite rules about the logical 

323  837 
connectives. These include cancellation and associative laws. To prove 
838 
them easily, it defines a function that echoes the desired law and then 

286  839 
supplies it the theorem prover for intuitionistic \FOL: 
840 
\begin{ttbox} 

841 
fun int_prove_fun s = 

842 
(writeln s; 

843 
prove_goal IFOL.thy s 

844 
(fn prems => [ (cut_facts_tac prems 1), 

845 
(Int.fast_tac 1) ])); 

846 
\end{ttbox} 

847 
The following rewrite rules about conjunction are a selection of those 

848 
proved on {\tt FOL/simpdata.ML}. Later, these will be supplied to the 

849 
standard simpset. 

850 
\begin{ttbox} 

851 
val conj_rews = map int_prove_fun 

852 
["P & True <> P", "True & P <> P", 

853 
"P & False <> False", "False & P <> False", 

854 
"P & P <> P", 

855 
"P & ~P <> False", "~P & P <> False", 

856 
"(P & Q) & R <> P & (Q & R)"]; 

857 
\end{ttbox} 

858 
The file also proves some distributive laws. As they can cause exponential 

859 
blowup, they will not be included in the standard simpset. Instead they 

323  860 
are merely bound to an \ML{} identifier, for user reference. 
286  861 
\begin{ttbox} 
862 
val distrib_rews = map int_prove_fun 

863 
["P & (Q  R) <> P&Q  P&R", 

864 
"(Q  R) & P <> Q&P  R&P", 

865 
"(P  Q > R) <> (P > R) & (Q > R)"]; 

866 
\end{ttbox} 

867 

868 

869 
\subsection{Functions for preprocessing the rewrite rules} 

323  870 
\label{sec:setmksimps} 
871 
% 

286  872 
The next step is to define the function for preprocessing rewrite rules. 
873 
This will be installed by calling {\tt setmksimps} below. Preprocessing 

874 
occurs whenever rewrite rules are added, whether by user command or 

875 
automatically. Preprocessing involves extracting atomic rewrites at the 

876 
objectlevel, then reflecting them to the metalevel. 

877 

878 
To start, the function {\tt gen_all} strips any metalevel 

879 
quantifiers from the front of the given theorem. Usually there are none 

880 
anyway. 

881 
\begin{ttbox} 

882 
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; 

883 
\end{ttbox} 

884 
The function {\tt atomize} analyses a theorem in order to extract 

885 
atomic rewrite rules. The head of all the patterns, matched by the 

886 
wildcard~{\tt _}, is the coercion function {\tt Trueprop}. 

887 
\begin{ttbox} 

888 
fun atomize th = case concl_of th of 

889 
_ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) \at 

890 
atomize(th RS conjunct2) 

891 
 _ $ (Const("op >",_) $ _ $ _) => atomize(th RS mp) 

892 
 _ $ (Const("All",_) $ _) => atomize(th RS spec) 

893 
 _ $ (Const("True",_)) => [] 

894 
 _ $ (Const("False",_)) => [] 

895 
 _ => [th]; 

896 
\end{ttbox} 

897 
There are several cases, depending upon the form of the conclusion: 

898 
\begin{itemize} 

899 
\item Conjunction: extract rewrites from both conjuncts. 

900 

901 
\item Implication: convert $P\imp Q$ to the metaimplication $P\Imp Q$ and 

902 
extract rewrites from~$Q$; these will be conditional rewrites with the 

903 
condition~$P$. 

904 

905 
\item Universal quantification: remove the quantifier, replacing the bound 

906 
variable by a schematic variable, and extract rewrites from the body. 

907 

908 
\item {\tt True} and {\tt False} contain no useful rewrites. 

909 

910 
\item Anything else: return the theorem in a singleton list. 

911 
\end{itemize} 

912 
The resulting theorems are not literally atomic  they could be 

323  913 
disjunctive, for example  but are broken down as much as possible. See 
286  914 
the file {\tt ZF/simpdata.ML} for a sophisticated translation of 
915 
settheoretic formulae into rewrite rules. 

104  916 

286  917 
The simplified rewrites must now be converted into metaequalities. The 
323  918 
rule {\tt eq_reflection} converts equality rewrites, while {\tt 
286  919 
iff_reflection} converts ifandonlyif rewrites. The latter possibility 
920 
can arise in two other ways: the negative theorem~$\neg P$ is converted to 

323  921 
$P\equiv{\tt False}$, and any other theorem~$P$ is converted to 
286  922 
$P\equiv{\tt True}$. The rules {\tt iff_reflection_F} and {\tt 
923 
iff_reflection_T} accomplish this conversion. 

924 
\begin{ttbox} 

925 
val P_iff_F = int_prove_fun "~P ==> (P <> False)"; 

926 
val iff_reflection_F = P_iff_F RS iff_reflection; 

927 
\ttbreak 

928 
val P_iff_T = int_prove_fun "P ==> (P <> True)"; 

929 
val iff_reflection_T = P_iff_T RS iff_reflection; 

930 
\end{ttbox} 

931 
The function {\tt mk_meta_eq} converts a theorem to a metaequality 

932 
using the case analysis described above. 

933 
\begin{ttbox} 

934 
fun mk_meta_eq th = case concl_of th of 

935 
_ $ (Const("op =",_)$_$_) => th RS eq_reflection 

936 
 _ $ (Const("op <>",_)$_$_) => th RS iff_reflection 

937 
 _ $ (Const("Not",_)$_) => th RS iff_reflection_F 

938 
 _ => th RS iff_reflection_T; 

939 
\end{ttbox} 

940 
The three functions {\tt gen_all}, {\tt atomize} and {\tt mk_meta_eq} will 

941 
be composed together and supplied below to {\tt setmksimps}. 

942 

943 

944 
\subsection{Making the initial simpset} 

945 
It is time to assemble these items. We open module {\tt Simplifier} to 

323  946 
gain access to its components. We define the infix operator 
947 
\ttindexbold{addcongs} to insert congruence rules; given a list of theorems, 

948 
it converts their conclusions into metaequalities and passes them to 

949 
\ttindex{addeqcongs}. 

286  950 
\begin{ttbox} 
951 
open Simplifier; 

952 
\ttbreak 

953 
infix addcongs; 

954 
fun ss addcongs congs = 

955 
ss addeqcongs (congs RL [eq_reflection,iff_reflection]); 

956 
\end{ttbox} 

957 
The list {\tt IFOL_rews} contains the default rewrite rules for firstorder 

958 
logic. The first of these is the reflexive law expressed as the 

323  959 
equivalence $(a=a)\bimp{\tt True}$; the rewrite rule $a=a$ is clearly useless. 
286  960 
\begin{ttbox} 
961 
val IFOL_rews = 

962 
[refl RS P_iff_T] \at conj_rews \at disj_rews \at not_rews \at 

963 
imp_rews \at iff_rews \at quant_rews; 

964 
\end{ttbox} 

965 
The list {\tt triv_rls} contains trivial theorems for the solver. Any 

966 
subgoal that is simplified to one of these will be removed. 

967 
\begin{ttbox} 

968 
val notFalseI = int_prove_fun "~False"; 

969 
val triv_rls = [TrueI,refl,iff_refl,notFalseI]; 

970 
\end{ttbox} 

323  971 
% 
286  972 
The basic simpset for intuitionistic \FOL{} starts with \ttindex{empty_ss}. 
973 
It preprocess rewrites using {\tt gen_all}, {\tt atomize} and {\tt 

974 
mk_meta_eq}. It solves simplified subgoals using {\tt triv_rls} and 

2613  975 
assumptions, and by detecting contradictions. 
976 
It uses \ttindex{asm_simp_tac} to tackle subgoals of 

286  977 
conditional rewrites. It takes {\tt IFOL_rews} as rewrite rules. 
978 
Other simpsets built from {\tt IFOL_ss} will inherit these items. 

323  979 
In particular, {\tt FOL_ss} extends {\tt IFOL_ss} with classical rewrite 
980 
rules such as $\neg\neg P\bimp P$. 

2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

981 
\index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler} 
286  982 
\index{*addsimps}\index{*addcongs} 
983 
\begin{ttbox} 

2632  984 
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls \at prems), 
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

985 
atac, etac FalseE]; 
2632  986 
fun safe_solver prems = FIRST'[match_tac (triv_rls \at prems), 
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

987 
eq_assume_tac, ematch_tac [FalseE]]; 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

988 
val IFOL_ss = empty_ss setsubgoaler asm_simp_tac 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

989 
setSSolver safe_solver 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

990 
setSolver unsafe_solver 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

991 
setmksimps (map mk_meta_eq o atomize o gen_all) 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

992 
addsimps IFOL_simps 
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset

993 
addcongs [imp_cong]; 
286  994 
\end{ttbox} 
995 
This simpset takes {\tt imp_cong} as a congruence rule in order to use 

996 
contextual information to simplify the conclusions of implications: 

997 
\[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp 

998 
(\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'}) 

999 
\] 

1000 
By adding the congruence rule {\tt conj_cong}, we could obtain a similar 

1001 
effect for conjunctions. 

1002 

1003 

1004 
\subsection{Case splitting} 

323  1005 
To set up case splitting, we must prove the theorem below and pass it to 
1006 
\ttindexbold{mk_case_split_tac}. The tactic \ttindexbold{split_tac} uses 

1007 
{\tt mk_meta_eq}, defined above, to convert the splitting rules to 

1008 
metaequalities. 

286  1009 
\begin{ttbox} 
1010 
val meta_iffD = 

1011 
prove_goal FOL.thy "[ P==Q; Q ] ==> P" 

1012 
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]) 

1013 
\ttbreak 

1014 
fun split_tac splits = 

1015 
mk_case_split_tac meta_iffD (map mk_meta_eq splits); 

1016 
\end{ttbox} 

1017 
% 

323  1018 
The splitter replaces applications of a given function; the righthand side 
1019 
of the replacement can be anything. For example, here is a splitting rule 

1020 
for conditional expressions: 

286  1021 
\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x})) 
1022 
\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y})) 

1023 
\] 

323  1024 
Another example is the elimination operator (which happens to be 
1025 
called~$split$) for Cartesian products: 

286  1026 
\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} = 
1027 
\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) 

1028 
\] 

1029 
Case splits should be allowed only when necessary; they are expensive 

1030 
and hard to control. Here is a typical example of use, where {\tt 

1031 
expand_if} is the first rule above: 

1032 
\begin{ttbox} 

3112  1033 
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); 
286  1034 
\end{ttbox} 
1035 

104  1036 

1037 

1038 
\index{simplification)} 

1039 

286  1040 