author | paulson |
Mon, 19 Aug 1996 11:15:44 +0200 | |
changeset 1909 | f535276171d1 |
parent 1860 | 71bfeecfa96c |
child 2020 | 586f3c075b05 |
permissions | -rw-r--r-- |
104 | 1 |
%% $Id$ |
2 |
\chapter{Simplification} \label{simp-chap} |
|
3 |
\index{simplification|(} |
|
4 |
||
5 |
This chapter describes Isabelle's generic simplification package, which |
|
323 | 6 |
provides a suite of simplification tactics. It performs conditional and |
7 |
unconditional rewriting and uses contextual information (`local |
|
8 |
assumptions'). It provides a few general hooks, which can provide |
|
9 |
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
|
10 |
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
|
11 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
12 |
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
|
13 |
sections explain advanced features. |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
14 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
15 |
\section{Simplification for dummies} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
16 |
\label{sec:simp-for-dummies} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
17 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
18 |
In some logics (e.g.\ \HOL), the simplifier is particularly easy to |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
19 |
use because it supports the concept of a {\em current set of simplification |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
20 |
rules}, also called the {\em current simpset}\index{simpset!current}. All |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
21 |
commands are interpreted relative to the current simpset. For example, in the |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
22 |
theory of arithmetic the goal |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
23 |
\begin{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
24 |
{\out 1. 0 + (x + 0) = x + 0 + 0} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
25 |
\end{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
26 |
can be solved by a single |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
27 |
\begin{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
28 |
by(Simp_tac 1); |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
29 |
\end{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
30 |
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
|
31 |
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
|
32 |
\Var{n}$. |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
33 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
34 |
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
|
35 |
process, as in |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
36 |
\begin{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
37 |
{\out 1. x = 0 ==> x + x = 0} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
38 |
\end{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
39 |
then there is the more powerful |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
40 |
\begin{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
41 |
by(Asm_simp_tac 1); |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
42 |
\end{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
43 |
which solves the above goal. |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
44 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
45 |
There are four basic simplification tactics: |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
46 |
\begin{ttdescription} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
47 |
\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
|
48 |
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
|
49 |
using the solver. |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
50 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
51 |
\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
|
52 |
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
|
53 |
assumptions. |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
54 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
55 |
\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
|
56 |
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
|
57 |
each other or the actual goal.) |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
58 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
59 |
\item[\ttindexbold{Asm_full_simp_tac}] |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
60 |
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
|
61 |
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
|
62 |
simplification of those following.} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
63 |
\end{ttdescription} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
64 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
65 |
{\tt Asm_full_simp_tac} is the most powerful of this quartet but may also |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
66 |
loop where some of the others terminate. For example, |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
67 |
\begin{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
68 |
{\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
|
69 |
\end{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
70 |
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
|
71 |
loop because the rewrite rule $f(\Var{x}) = f(g(f(\Var{x})))$ extracted from |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
72 |
the assumption does not terminate. Isabelle notices certain simple forms of |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
73 |
nontermination, but not this one. |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
74 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
75 |
\begin{warn} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
76 |
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
|
77 |
misses opportunities for simplification: given the subgoal |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
78 |
\begin{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
79 |
{\out [| P(f(a)); f(a) = t |] ==> ...} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
80 |
\end{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
81 |
\verb$Asm_full_simp_tac$ will not simplify the first assumption using the |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
82 |
second but will leave the assumptions unchanged. See |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
83 |
\S\ref{sec:reordering-asms} for ways around this problem. |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
84 |
\end{warn} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
85 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
86 |
Using the simplifier effectively may take a bit of experimentation. The |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
87 |
tactics can be traced with the ML command \verb$trace_simp := true$. |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
88 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
89 |
There is not just one global current simpset, but one associated with each |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
90 |
theory as well. How are these simpset built up? |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
91 |
\begin{enumerate} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
92 |
\item When loading {\tt T.thy}, the current simpset is initialized with the |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
93 |
union of the simpsets associated with all the ancestors of {\tt T}. In |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
94 |
addition, certain constructs in {\tt T} may add new rules to the simpset, |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
95 |
e.g.\ \ttindex{datatype} and \ttindex{primrec} in \HOL. Definitions are not |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
96 |
added automatically! |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
97 |
\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
|
98 |
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
|
99 |
\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
|
100 |
theory {\tt T}. |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
101 |
\end{enumerate} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
102 |
The current simpset is manipulated by |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
103 |
\begin{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
104 |
Addsimps, Delsimps: thm list -> unit |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
105 |
\end{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
106 |
\begin{ttdescription} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
107 |
\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
|
108 |
\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
|
109 |
\end{ttdescription} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
110 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
111 |
Generally useful simplification rules $\Var{n}+0 = \Var{n}$ should be added |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
112 |
to the current simpset right after they have been proved. Those of a more |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
113 |
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
|
114 |
formula) should only be added for specific proofs and deleted again |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
115 |
afterwards. Conversely, it may also happen that a generally useful rule needs |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
116 |
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
|
117 |
designed simpsets need few temporary additions or deletions. |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
118 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
119 |
\begin{warn} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
120 |
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
|
121 |
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
|
122 |
\ttindex{set_current_thy}~{\tt"}$T${\tt"}, where $T$ is the name of the |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
123 |
theory you want to work in. If you have just loaded $T$, this is not |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
124 |
necessary. |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
125 |
\end{warn} |
104 | 126 |
|
127 |
||
286 | 128 |
\section{Simplification sets}\index{simplification sets} |
104 | 129 |
The simplification tactics are controlled by {\bf simpsets}. These consist |
130 |
of five components: rewrite rules, congruence rules, the subgoaler, the |
|
323 | 131 |
solver and the looper. The simplifier should be set up with sensible |
132 |
defaults so that most simplifier calls specify only rewrite rules. |
|
133 |
Experienced users can exploit the other components to streamline proofs. |
|
134 |
||
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
135 |
Logics like \HOL, which support a current simpset\index{simpset!current}, |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
136 |
store its value in an ML reference variable usually called {\tt |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
137 |
simpset}\index{simpset@{\tt simpset} ML value}. It can be accessed via |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
138 |
{\tt!simpset} and updated via {\tt simpset := \dots}. |
104 | 139 |
|
332 | 140 |
\subsection{Rewrite rules} |
141 |
\index{rewrite rules|(} |
|
323 | 142 |
Rewrite rules are theorems expressing some form of equality: |
143 |
\begin{eqnarray*} |
|
144 |
Suc(\Var{m}) + \Var{n} &=& \Var{m} + Suc(\Var{n}) \\ |
|
145 |
\Var{P}\conj\Var{P} &\bimp& \Var{P} \\ |
|
714 | 146 |
\Var{A} \un \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\} |
323 | 147 |
\end{eqnarray*} |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
148 |
Conditional rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} = |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
149 |
0$ are permitted; the conditions can be arbitrary terms. |
104 | 150 |
|
323 | 151 |
Internally, all rewrite rules are translated into meta-equalities, theorems |
152 |
with conclusion $lhs \equiv rhs$. Each simpset contains a function for |
|
153 |
extracting equalities from arbitrary theorems. For example, |
|
154 |
$\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\} \equiv |
|
155 |
False$. This function can be installed using \ttindex{setmksimps} but only |
|
156 |
the definer of a logic should need to do this; see \S\ref{sec:setmksimps}. |
|
157 |
The function processes theorems added by \ttindex{addsimps} as well as |
|
158 |
local assumptions. |
|
104 | 159 |
|
160 |
||
332 | 161 |
\begin{warn} |
1101 | 162 |
The simplifier will accept all standard rewrite rules: those |
163 |
where all unknowns are of base type. Hence ${\Var{i}+(\Var{j}+\Var{k})} = |
|
714 | 164 |
{(\Var{i}+\Var{j})+\Var{k}}$ is ok. |
165 |
||
166 |
It will also deal gracefully with all rules whose left-hand sides are |
|
167 |
so-called {\em higher-order patterns}~\cite{Nipkow-LICS-93}. These are terms |
|
168 |
in $\beta$-normal form (this will always be the case unless you have done |
|
169 |
something strange) where each occurrence of an unknown is of the form |
|
170 |
$\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are distinct bound variables. |
|
171 |
Hence $(\forall x.\Var{P}(x) \land \Var{Q}(x)) \bimp (\forall x.\Var{P}(x)) |
|
172 |
\land (\forall x.\Var{Q}(x))$ is also ok, in both directions. |
|
173 |
||
174 |
In some rare cases the rewriter will even deal with quite general rules: for |
|
175 |
example ${\Var{f}(\Var{x})\in range(\Var{f})} = True$ rewrites $g(a) \in |
|
176 |
range(g)$ to $True$, but will fail to match $g(h(b)) \in range(\lambda |
|
177 |
x.g(h(x)))$. However, you can replace the offending subterms (in our case |
|
178 |
$\Var{f}(\Var{x})$, which is not a pattern) by adding new variables and |
|
179 |
conditions: $\Var{y} = \Var{f}(\Var{x}) \Imp \Var{y}\in range(\Var{f}) |
|
180 |
= True$ is acceptable as a conditional rewrite rule since conditions can |
|
181 |
be arbitrary terms. |
|
182 |
||
183 |
There is no restriction on the form of the right-hand sides. |
|
104 | 184 |
\end{warn} |
185 |
||
332 | 186 |
\index{rewrite rules|)} |
187 |
||
188 |
\subsection{*Congruence rules}\index{congruence rules} |
|
104 | 189 |
Congruence rules are meta-equalities of the form |
190 |
\[ \List{\dots} \Imp |
|
191 |
f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}). |
|
192 |
\] |
|
323 | 193 |
This governs the simplification of the arguments of~$f$. For |
104 | 194 |
example, some arguments can be simplified under additional assumptions: |
195 |
\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}} |
|
196 |
\Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2}) |
|
197 |
\] |
|
323 | 198 |
Given this rule, the simplifier assumes $Q@1$ and extracts rewrite rules |
199 |
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
|
200 |
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
|
201 |
provided as theorems to the solver; see page~\pageref{sec:simp-solver} below. |
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset
|
202 |
|
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset
|
203 |
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
|
204 |
also supplies contextual information, this time about the bound variable: |
286 | 205 |
\begin{eqnarray*} |
206 |
&&\List{\Var{A}=\Var{B};\; |
|
207 |
\Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\ |
|
208 |
&&\qquad\qquad |
|
209 |
(\forall x\in \Var{A}.\Var{P}(x)) = (\forall x\in \Var{B}.\Var{Q}(x)) |
|
210 |
\end{eqnarray*} |
|
323 | 211 |
The congruence rule for conditional expressions can supply contextual |
212 |
information for simplifying the arms: |
|
104 | 213 |
\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~ |
214 |
\neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp |
|
215 |
if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d}) |
|
216 |
\] |
|
698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset
|
217 |
A congruence rule can also {\em prevent\/} simplification of some arguments. |
104 | 218 |
Here is an alternative congruence rule for conditional expressions: |
219 |
\[ \Var{p}=\Var{q} \Imp |
|
220 |
if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b}) |
|
221 |
\] |
|
222 |
Only the first argument is simplified; the others remain unchanged. |
|
223 |
This can make simplification much faster, but may require an extra case split |
|
224 |
to prove the goal. |
|
225 |
||
286 | 226 |
Congruence rules are added using \ttindexbold{addeqcongs}. Their conclusion |
104 | 227 |
must be a meta-equality, as in the examples above. It is more |
228 |
natural to derive the rules with object-logic equality, for example |
|
229 |
\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}} |
|
230 |
\Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2}), |
|
231 |
\] |
|
286 | 232 |
Each object-logic should define an operator called \ttindex{addcongs} that |
233 |
expects object-equalities and translates them into meta-equalities. |
|
104 | 234 |
|
323 | 235 |
\subsection{*The subgoaler} |
104 | 236 |
The subgoaler is the tactic used to solve subgoals arising out of |
237 |
conditional rewrite rules or congruence rules. The default should be |
|
238 |
simplification itself. Occasionally this strategy needs to be changed. For |
|
239 |
example, if the premise of a conditional rule is an instance of its |
|
240 |
conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m} < \Var{n}$, the |
|
241 |
default strategy could loop. |
|
242 |
||
243 |
The subgoaler can be set explicitly with \ttindex{setsubgoaler}. For |
|
244 |
example, the subgoaler |
|
245 |
\begin{ttbox} |
|
332 | 246 |
fun subgoal_tac ss = assume_tac ORELSE' |
247 |
resolve_tac (prems_of_ss ss) ORELSE' |
|
104 | 248 |
asm_simp_tac ss; |
249 |
\end{ttbox} |
|
332 | 250 |
tries to solve the subgoal by assumption or with one of the premises, calling |
104 | 251 |
simplification only if that fails; here {\tt prems_of_ss} extracts the |
252 |
current premises from a simpset. |
|
253 |
||
698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset
|
254 |
\subsection{*The solver}\label{sec:simp-solver} |
286 | 255 |
The solver is a tactic that attempts to solve a subgoal after |
256 |
simplification. Typically it just proves trivial subgoals such as {\tt |
|
323 | 257 |
True} and $t=t$. It could use sophisticated means such as {\tt |
258 |
fast_tac}, though that could make simplification expensive. The solver |
|
259 |
is set using \ttindex{setsolver}. |
|
286 | 260 |
|
323 | 261 |
Rewriting does not instantiate unknowns. For example, rewriting cannot |
262 |
prove $a\in \Var{A}$ since this requires instantiating~$\Var{A}$. The |
|
263 |
solver, however, is an arbitrary tactic and may instantiate unknowns as it |
|
264 |
pleases. This is the only way the simplifier can handle a conditional |
|
265 |
rewrite rule whose condition contains extra variables. |
|
266 |
||
267 |
\index{assumptions!in simplification} |
|
286 | 268 |
The tactic is presented with the full goal, including the asssumptions. |
269 |
Hence it can use those assumptions (say by calling {\tt assume_tac}) even |
|
270 |
inside {\tt simp_tac}, which otherwise does not use assumptions. The |
|
271 |
solver is also supplied a list of theorems, namely assumptions that hold in |
|
272 |
the local context. |
|
104 | 273 |
|
323 | 274 |
The subgoaler is also used to solve the premises of congruence rules, which |
275 |
are usually of the form $s = \Var{x}$, where $s$ needs to be simplified and |
|
276 |
$\Var{x}$ needs to be instantiated with the result. Hence the subgoaler |
|
277 |
should call the simplifier at some point. The simplifier will then call the |
|
278 |
solver, which must therefore be prepared to solve goals of the form $t = |
|
279 |
\Var{x}$, usually by reflexivity. In particular, reflexivity should be |
|
280 |
tried before any of the fancy tactics like {\tt fast_tac}. |
|
281 |
||
282 |
It may even happen that, due to simplification, the subgoal is no longer an |
|
283 |
equality. For example $False \bimp \Var{Q}$ could be rewritten to |
|
284 |
$\neg\Var{Q}$. To cover this case, the solver could try resolving with the |
|
285 |
theorem $\neg False$. |
|
104 | 286 |
|
287 |
\begin{warn} |
|
288 |
If the simplifier aborts with the message {\tt Failed congruence proof!}, |
|
323 | 289 |
then the subgoaler or solver has failed to prove a premise of a |
698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset
|
290 |
congruence rule. This should never occur; it indicates that some |
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset
|
291 |
congruence rule, or possibly the subgoaler or solver, is faulty. |
104 | 292 |
\end{warn} |
293 |
||
323 | 294 |
|
295 |
\subsection{*The looper} |
|
104 | 296 |
The looper is a tactic that is applied after simplification, in case the |
297 |
solver failed to solve the simplified goal. If the looper succeeds, the |
|
298 |
simplification process is started all over again. Each of the subgoals |
|
299 |
generated by the looper is attacked in turn, in reverse order. A |
|
300 |
typical looper is case splitting: the expansion of a conditional. Another |
|
301 |
possibility is to apply an elimination rule on the assumptions. More |
|
302 |
adventurous loopers could start an induction. The looper is set with |
|
303 |
\ttindex{setloop}. |
|
304 |
||
305 |
||
306 |
\begin{figure} |
|
323 | 307 |
\index{*simpset ML type} |
308 |
\index{*simp_tac} |
|
309 |
\index{*asm_simp_tac} |
|
310 |
\index{*asm_full_simp_tac} |
|
311 |
\index{*addeqcongs} |
|
312 |
\index{*addsimps} |
|
313 |
\index{*delsimps} |
|
314 |
\index{*empty_ss} |
|
315 |
\index{*merge_ss} |
|
316 |
\index{*setsubgoaler} |
|
317 |
\index{*setsolver} |
|
318 |
\index{*setloop} |
|
319 |
\index{*setmksimps} |
|
320 |
\index{*prems_of_ss} |
|
321 |
\index{*rep_ss} |
|
104 | 322 |
\begin{ttbox} |
323 |
infix addsimps addeqcongs delsimps |
|
324 |
setsubgoaler setsolver setloop setmksimps; |
|
325 |
||
326 |
signature SIMPLIFIER = |
|
327 |
sig |
|
328 |
type simpset |
|
329 |
val simp_tac: simpset -> int -> tactic |
|
330 |
val asm_simp_tac: simpset -> int -> tactic |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
331 |
val full_simp_tac: simpset -> int -> tactic |
133 | 332 |
val asm_full_simp_tac: simpset -> int -> tactic\smallskip |
333 |
val addeqcongs: simpset * thm list -> simpset |
|
334 |
val addsimps: simpset * thm list -> simpset |
|
335 |
val delsimps: simpset * thm list -> simpset |
|
104 | 336 |
val empty_ss: simpset |
337 |
val merge_ss: simpset * simpset -> simpset |
|
338 |
val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset |
|
339 |
val setsolver: simpset * (thm list -> int -> tactic) -> simpset |
|
340 |
val setloop: simpset * (int -> tactic) -> simpset |
|
341 |
val setmksimps: simpset * (thm -> thm list) -> simpset |
|
342 |
val prems_of_ss: simpset -> thm list |
|
343 |
val rep_ss: simpset -> \{simps: thm list, congs: thm list\} |
|
344 |
end; |
|
345 |
\end{ttbox} |
|
323 | 346 |
\caption{The simplifier primitives} \label{SIMPLIFIER} |
104 | 347 |
\end{figure} |
348 |
||
349 |
||
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
350 |
\section{The simplification tactics} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
351 |
\label{simp-tactics} |
323 | 352 |
\index{simplification!tactics} |
353 |
\index{tactics!simplification} |
|
104 | 354 |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
355 |
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
|
356 |
\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac}, |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
357 |
\ttindexbold{full_simp_tac} and \ttindexbold{asm_full_simp_tac}. They work |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
358 |
exactly like their namesakes in \S\ref{sec:simp-for-dummies}, except that |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
359 |
they are explicitly supplied with a simpset. This is because the ones in |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
360 |
\S\ref{sec:simp-for-dummies} 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
|
361 |
\begin{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
362 |
fun Simp_tac i = simp_tac (!simpset) i; |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
363 |
\end{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
364 |
where \ttindex{!simpset} is the current simpset\index{simpset!current}. |
104 | 365 |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
366 |
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
|
367 |
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
|
368 |
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
|
369 |
is applied. |
104 | 370 |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
371 |
The infix operations \ttindex{addsimps}/\ttindex{delsimps} add/delete rewrite |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
372 |
rules to/from a simpset. They are used to implement \ttindex{Addsimps} and |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
373 |
\ttindex{Delsimps}, e.g. |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
374 |
\begin{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
375 |
fun Addsimps thms = (simpset := (!simpset addsimps thms)); |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
376 |
\end{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
377 |
and can also be used directly, even in the presence of a current simpset. For |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
378 |
example |
1213 | 379 |
\begin{ttbox} |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
380 |
Addsimps \(thms\); |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
381 |
by(Simp_tac \(i\)); |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
382 |
Delsimps \(thms\); |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
383 |
\end{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
384 |
can be compressed into |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
385 |
\begin{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
386 |
by(simp_tac (!simpset addsimps \(thms\)) \(i\)); |
1213 | 387 |
\end{ttbox} |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
388 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
389 |
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
|
390 |
of the theory using the function |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
391 |
\begin{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
392 |
simpset_of: string -> simpset |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
393 |
\end{ttbox}\index{*simpset_of} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
394 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
395 |
To remind yourself of what is in a simpset, use the function \verb$rep_ss$ to |
104 | 396 |
return its simplification and congruence rules. |
397 |
||
286 | 398 |
\section{Examples using the simplifier} |
323 | 399 |
\index{examples!of simplification} |
104 | 400 |
Assume we are working within {\tt FOL} and that |
323 | 401 |
\begin{ttdescription} |
402 |
\item[Nat.thy] |
|
403 |
is a theory including the constants $0$, $Suc$ and $+$, |
|
404 |
\item[add_0] |
|
405 |
is the rewrite rule $0+\Var{n} = \Var{n}$, |
|
406 |
\item[add_Suc] |
|
407 |
is the rewrite rule $Suc(\Var{m})+\Var{n} = Suc(\Var{m}+\Var{n})$, |
|
408 |
\item[induct] |
|
409 |
is the induction rule $\List{\Var{P}(0);\; \Forall x. \Var{P}(x)\Imp |
|
410 |
\Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$. |
|
411 |
\item[FOL_ss] |
|
412 |
is a basic simpset for {\tt FOL}.% |
|
332 | 413 |
\footnote{These examples reside on the file {\tt FOL/ex/Nat.ML}.} |
323 | 414 |
\end{ttdescription} |
104 | 415 |
|
416 |
We create a simpset for natural numbers by extending~{\tt FOL_ss}: |
|
417 |
\begin{ttbox} |
|
418 |
val add_ss = FOL_ss addsimps [add_0, add_Suc]; |
|
419 |
\end{ttbox} |
|
323 | 420 |
|
421 |
\subsection{A trivial example} |
|
286 | 422 |
Proofs by induction typically involve simplification. Here is a proof |
423 |
that~0 is a right identity: |
|
104 | 424 |
\begin{ttbox} |
425 |
goal Nat.thy "m+0 = m"; |
|
426 |
{\out Level 0} |
|
427 |
{\out m + 0 = m} |
|
428 |
{\out 1. m + 0 = m} |
|
286 | 429 |
\end{ttbox} |
430 |
The first step is to perform induction on the variable~$m$. This returns a |
|
431 |
base case and inductive step as two subgoals: |
|
432 |
\begin{ttbox} |
|
104 | 433 |
by (res_inst_tac [("n","m")] induct 1); |
434 |
{\out Level 1} |
|
435 |
{\out m + 0 = m} |
|
436 |
{\out 1. 0 + 0 = 0} |
|
437 |
{\out 2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)} |
|
438 |
\end{ttbox} |
|
286 | 439 |
Simplification solves the first subgoal trivially: |
104 | 440 |
\begin{ttbox} |
441 |
by (simp_tac add_ss 1); |
|
442 |
{\out Level 2} |
|
443 |
{\out m + 0 = m} |
|
444 |
{\out 1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)} |
|
445 |
\end{ttbox} |
|
446 |
The remaining subgoal requires \ttindex{asm_simp_tac} in order to use the |
|
447 |
induction hypothesis as a rewrite rule: |
|
448 |
\begin{ttbox} |
|
449 |
by (asm_simp_tac add_ss 1); |
|
450 |
{\out Level 3} |
|
451 |
{\out m + 0 = m} |
|
452 |
{\out No subgoals!} |
|
453 |
\end{ttbox} |
|
454 |
||
323 | 455 |
\subsection{An example of tracing} |
456 |
Let us prove a similar result involving more complex terms. The two |
|
457 |
equations together can be used to prove that addition is commutative. |
|
104 | 458 |
\begin{ttbox} |
459 |
goal Nat.thy "m+Suc(n) = Suc(m+n)"; |
|
460 |
{\out Level 0} |
|
461 |
{\out m + Suc(n) = Suc(m + n)} |
|
462 |
{\out 1. m + Suc(n) = Suc(m + n)} |
|
286 | 463 |
\end{ttbox} |
464 |
We again perform induction on~$m$ and get two subgoals: |
|
465 |
\begin{ttbox} |
|
104 | 466 |
by (res_inst_tac [("n","m")] induct 1); |
467 |
{\out Level 1} |
|
468 |
{\out m + Suc(n) = Suc(m + n)} |
|
469 |
{\out 1. 0 + Suc(n) = Suc(0 + n)} |
|
286 | 470 |
{\out 2. !!x. x + Suc(n) = Suc(x + n) ==>} |
471 |
{\out Suc(x) + Suc(n) = Suc(Suc(x) + n)} |
|
472 |
\end{ttbox} |
|
473 |
Simplification solves the first subgoal, this time rewriting two |
|
474 |
occurrences of~0: |
|
475 |
\begin{ttbox} |
|
104 | 476 |
by (simp_tac add_ss 1); |
477 |
{\out Level 2} |
|
478 |
{\out m + Suc(n) = Suc(m + n)} |
|
286 | 479 |
{\out 1. !!x. x + Suc(n) = Suc(x + n) ==>} |
480 |
{\out Suc(x) + Suc(n) = Suc(Suc(x) + n)} |
|
104 | 481 |
\end{ttbox} |
482 |
Switching tracing on illustrates how the simplifier solves the remaining |
|
483 |
subgoal: |
|
484 |
\begin{ttbox} |
|
485 |
trace_simp := true; |
|
486 |
by (asm_simp_tac add_ss 1); |
|
323 | 487 |
\ttbreak |
104 | 488 |
{\out Rewriting:} |
489 |
{\out Suc(x) + Suc(n) == Suc(x + Suc(n))} |
|
323 | 490 |
\ttbreak |
104 | 491 |
{\out Rewriting:} |
492 |
{\out x + Suc(n) == Suc(x + n)} |
|
323 | 493 |
\ttbreak |
104 | 494 |
{\out Rewriting:} |
495 |
{\out Suc(x) + n == Suc(x + n)} |
|
323 | 496 |
\ttbreak |
104 | 497 |
{\out Rewriting:} |
498 |
{\out Suc(Suc(x + n)) = Suc(Suc(x + n)) == True} |
|
323 | 499 |
\ttbreak |
104 | 500 |
{\out Level 3} |
501 |
{\out m + Suc(n) = Suc(m + n)} |
|
502 |
{\out No subgoals!} |
|
503 |
\end{ttbox} |
|
286 | 504 |
Many variations are possible. At Level~1 (in either example) we could have |
505 |
solved both subgoals at once using the tactical \ttindex{ALLGOALS}: |
|
104 | 506 |
\begin{ttbox} |
507 |
by (ALLGOALS (asm_simp_tac add_ss)); |
|
508 |
{\out Level 2} |
|
509 |
{\out m + Suc(n) = Suc(m + n)} |
|
510 |
{\out No subgoals!} |
|
511 |
\end{ttbox} |
|
512 |
||
323 | 513 |
\subsection{Free variables and simplification} |
104 | 514 |
Here is a conjecture to be proved for an arbitrary function~$f$ satisfying |
323 | 515 |
the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$: |
104 | 516 |
\begin{ttbox} |
517 |
val [prem] = goal Nat.thy |
|
518 |
"(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; |
|
519 |
{\out Level 0} |
|
520 |
{\out f(i + j) = i + f(j)} |
|
521 |
{\out 1. f(i + j) = i + f(j)} |
|
323 | 522 |
\ttbreak |
286 | 523 |
{\out val prem = "f(Suc(?n)) = Suc(f(?n))} |
524 |
{\out [!!n. f(Suc(n)) = Suc(f(n))]" : thm} |
|
323 | 525 |
\end{ttbox} |
526 |
In the theorem~{\tt prem}, note that $f$ is a free variable while |
|
527 |
$\Var{n}$ is a schematic variable. |
|
528 |
\begin{ttbox} |
|
104 | 529 |
by (res_inst_tac [("n","i")] induct 1); |
530 |
{\out Level 1} |
|
531 |
{\out f(i + j) = i + f(j)} |
|
532 |
{\out 1. f(0 + j) = 0 + f(j)} |
|
533 |
{\out 2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)} |
|
534 |
\end{ttbox} |
|
535 |
We simplify each subgoal in turn. The first one is trivial: |
|
536 |
\begin{ttbox} |
|
537 |
by (simp_tac add_ss 1); |
|
538 |
{\out Level 2} |
|
539 |
{\out f(i + j) = i + f(j)} |
|
540 |
{\out 1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)} |
|
541 |
\end{ttbox} |
|
542 |
The remaining subgoal requires rewriting by the premise, so we add it to |
|
323 | 543 |
{\tt add_ss}:% |
544 |
\footnote{The previous simplifier required congruence rules for function |
|
545 |
variables like~$f$ in order to simplify their arguments. It was more |
|
546 |
general than the current simplifier, but harder to use and slower. The |
|
547 |
present simplifier can be given congruence rules to realize non-standard |
|
548 |
simplification of a function's arguments, but this is seldom necessary.} |
|
104 | 549 |
\begin{ttbox} |
550 |
by (asm_simp_tac (add_ss addsimps [prem]) 1); |
|
551 |
{\out Level 3} |
|
552 |
{\out f(i + j) = i + f(j)} |
|
553 |
{\out No subgoals!} |
|
554 |
\end{ttbox} |
|
555 |
||
1213 | 556 |
\subsection{Reordering assumptions} |
557 |
\label{sec:reordering-asms} |
|
558 |
\index{assumptions!reordering} |
|
559 |
||
560 |
As mentioned above, \ttindex{asm_full_simp_tac} may require the assumptions |
|
561 |
to be permuted to be more effective. Given the subgoal |
|
562 |
\begin{ttbox} |
|
563 |
{\out 1. [| P(f(a)); Q; f(a) = t; R |] ==> S} |
|
564 |
\end{ttbox} |
|
565 |
we can rotate the assumptions two positions to the right |
|
566 |
\begin{ttbox} |
|
567 |
by (rotate_tac ~2 1); |
|
568 |
\end{ttbox} |
|
569 |
to obtain |
|
570 |
\begin{ttbox} |
|
571 |
{\out 1. [| f(a) = t; R; P(f(a)); Q |] ==> S} |
|
572 |
\end{ttbox} |
|
573 |
which enables \verb$asm_full_simp_tac$ to simplify \verb$P(f(a))$ to |
|
574 |
\verb$P(t)$. |
|
575 |
||
576 |
Since rotation alone cannot produce arbitrary permutations, you can also pick |
|
577 |
out a particular assumption which needs to be rewritten and move it the the |
|
578 |
right end of the assumptions. In the above case rotation can be replaced by |
|
579 |
\begin{ttbox} |
|
580 |
by (dres_inst_tac [("psi","P(f(a))")] asm_rl 1); |
|
581 |
\end{ttbox} |
|
582 |
which is more directed and leads to |
|
583 |
\begin{ttbox} |
|
584 |
{\out 1. [| Q; f(a) = t; R; P(f(a)) |] ==> S} |
|
585 |
\end{ttbox} |
|
586 |
||
587 |
Note that reordering assumptions usually leads to brittle proofs and should |
|
588 |
therefore be avoided. Future versions of \verb$asm_full_simp_tac$ may remove |
|
589 |
the need for such manipulations. |
|
286 | 590 |
|
332 | 591 |
\section{Permutative rewrite rules} |
323 | 592 |
\index{rewrite rules!permutative|(} |
593 |
||
594 |
A rewrite rule is {\bf permutative} if the left-hand side and right-hand |
|
595 |
side are the same up to renaming of variables. The most common permutative |
|
596 |
rule is commutativity: $x+y = y+x$. Other examples include $(x-y)-z = |
|
597 |
(x-z)-y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$ |
|
598 |
for sets. Such rules are common enough to merit special attention. |
|
599 |
||
600 |
Because ordinary rewriting loops given such rules, the simplifier employs a |
|
601 |
special strategy, called {\bf ordered rewriting}\index{rewriting!ordered}. |
|
602 |
There is a built-in lexicographic ordering on terms. A permutative rewrite |
|
603 |
rule is applied only if it decreases the given term with respect to this |
|
604 |
ordering. For example, commutativity rewrites~$b+a$ to $a+b$, but then |
|
605 |
stops because $a+b$ is strictly less than $b+a$. The Boyer-Moore theorem |
|
606 |
prover~\cite{bm88book} also employs ordered rewriting. |
|
607 |
||
608 |
Permutative rewrite rules are added to simpsets just like other rewrite |
|
609 |
rules; the simplifier recognizes their special status automatically. They |
|
610 |
are most effective in the case of associative-commutative operators. |
|
611 |
(Associativity by itself is not permutative.) When dealing with an |
|
612 |
AC-operator~$f$, keep the following points in mind: |
|
613 |
\begin{itemize}\index{associative-commutative operators} |
|
614 |
\item The associative law must always be oriented from left to right, namely |
|
615 |
$f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if used with |
|
616 |
commutativity, leads to looping! Future versions of Isabelle may remove |
|
617 |
this restriction. |
|
618 |
||
619 |
\item To complete your set of rewrite rules, you must add not just |
|
620 |
associativity~(A) and commutativity~(C) but also a derived rule, {\bf |
|
621 |
left-commutativity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$. |
|
622 |
\end{itemize} |
|
623 |
Ordered rewriting with the combination of A, C, and~LC sorts a term |
|
624 |
lexicographically: |
|
625 |
\[\def\maps#1{\stackrel{#1}{\longmapsto}} |
|
626 |
(b+c)+a \maps{A} b+(c+a) \maps{C} b+(a+c) \maps{LC} a+(b+c) \] |
|
627 |
Martin and Nipkow~\cite{martin-nipkow} discuss the theory and give many |
|
628 |
examples; other algebraic structures are amenable to ordered rewriting, |
|
629 |
such as boolean rings. |
|
630 |
||
631 |
\subsection{Example: sums of integers} |
|
632 |
This example is set in Isabelle's higher-order logic. Theory |
|
633 |
\thydx{Arith} contains the theory of arithmetic. The simpset {\tt |
|
634 |
arith_ss} contains many arithmetic laws including distributivity |
|
635 |
of~$\times$ over~$+$, while {\tt add_ac} is a list consisting of the A, C |
|
636 |
and LC laws for~$+$. Let us prove the theorem |
|
637 |
\[ \sum@{i=1}^n i = n\times(n+1)/2. \] |
|
638 |
% |
|
639 |
A functional~{\tt sum} represents the summation operator under the |
|
640 |
interpretation ${\tt sum}(f,n+1) = \sum@{i=0}^n f(i)$. We extend {\tt |
|
641 |
Arith} using a theory file: |
|
642 |
\begin{ttbox} |
|
643 |
NatSum = Arith + |
|
1387 | 644 |
consts sum :: [nat=>nat, nat] => nat |
323 | 645 |
rules sum_0 "sum(f,0) = 0" |
646 |
sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)" |
|
647 |
end |
|
648 |
\end{ttbox} |
|
332 | 649 |
After declaring {\tt open NatSum}, we make the required simpset by adding |
323 | 650 |
the AC-rules for~$+$ and the axioms for~{\tt sum}: |
651 |
\begin{ttbox} |
|
652 |
val natsum_ss = arith_ss addsimps ([sum_0,sum_Suc] \at add_ac); |
|
653 |
{\out val natsum_ss = SS \{\ldots\} : simpset} |
|
654 |
\end{ttbox} |
|
655 |
Our desired theorem now reads ${\tt sum}(\lambda i.i,n+1) = |
|
656 |
n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$: |
|
657 |
\begin{ttbox} |
|
658 |
goal NatSum.thy "Suc(Suc(0))*sum(\%i.i,Suc(n)) = n*Suc(n)"; |
|
659 |
{\out Level 0} |
|
660 |
{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)} |
|
661 |
{\out 1. Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)} |
|
662 |
\end{ttbox} |
|
663 |
Induction should not be applied until the goal is in the simplest form: |
|
664 |
\begin{ttbox} |
|
665 |
by (simp_tac natsum_ss 1); |
|
666 |
{\out Level 1} |
|
667 |
{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)} |
|
668 |
{\out 1. n + (n + (sum(\%i. i, n) + sum(\%i. i, n))) = n + n * n} |
|
669 |
\end{ttbox} |
|
670 |
Ordered rewriting has sorted the terms in the left-hand side. |
|
671 |
The subgoal is now ready for induction: |
|
672 |
\begin{ttbox} |
|
673 |
by (nat_ind_tac "n" 1); |
|
674 |
{\out Level 2} |
|
675 |
{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)} |
|
676 |
{\out 1. 0 + (0 + (sum(\%i. i, 0) + sum(\%i. i, 0))) = 0 + 0 * 0} |
|
677 |
\ttbreak |
|
678 |
{\out 2. !!n1. n1 + (n1 + (sum(\%i. i, n1) + sum(\%i. i, n1))) =} |
|
679 |
{\out n1 + n1 * n1 ==>} |
|
680 |
{\out Suc(n1) +} |
|
681 |
{\out (Suc(n1) + (sum(\%i. i, Suc(n1)) + sum(\%i. i, Suc(n1)))) =} |
|
682 |
{\out Suc(n1) + Suc(n1) * Suc(n1)} |
|
683 |
\end{ttbox} |
|
684 |
Simplification proves both subgoals immediately:\index{*ALLGOALS} |
|
685 |
\begin{ttbox} |
|
686 |
by (ALLGOALS (asm_simp_tac natsum_ss)); |
|
687 |
{\out Level 3} |
|
688 |
{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)} |
|
689 |
{\out No subgoals!} |
|
690 |
\end{ttbox} |
|
691 |
If we had omitted {\tt add_ac} from the simpset, simplification would have |
|
692 |
failed to prove the induction step: |
|
693 |
\begin{ttbox} |
|
694 |
Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n) |
|
695 |
1. !!n1. n1 + (n1 + (sum(\%i. i, n1) + sum(\%i. i, n1))) = |
|
696 |
n1 + n1 * n1 ==> |
|
697 |
n1 + (n1 + (n1 + sum(\%i. i, n1) + (n1 + sum(\%i. i, n1)))) = |
|
698 |
n1 + (n1 + (n1 + n1 * n1)) |
|
699 |
\end{ttbox} |
|
700 |
Ordered rewriting proves this by sorting the left-hand side. Proving |
|
701 |
arithmetic theorems without ordered rewriting requires explicit use of |
|
702 |
commutativity. This is tedious; try it and see! |
|
703 |
||
704 |
Ordered rewriting is equally successful in proving |
|
705 |
$\sum@{i=1}^n i^3 = n^2\times(n+1)^2/4$. |
|
706 |
||
707 |
||
708 |
\subsection{Re-orienting equalities} |
|
709 |
Ordered rewriting with the derived rule {\tt symmetry} can reverse equality |
|
710 |
signs: |
|
711 |
\begin{ttbox} |
|
712 |
val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" |
|
713 |
(fn _ => [fast_tac HOL_cs 1]); |
|
714 |
\end{ttbox} |
|
715 |
This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs |
|
716 |
in the conclusion but not~$s$, can often be brought into the right form. |
|
717 |
For example, ordered rewriting with {\tt symmetry} can prove the goal |
|
718 |
\[ f(a)=b \conj f(a)=c \imp b=c. \] |
|
719 |
Here {\tt symmetry} reverses both $f(a)=b$ and $f(a)=c$ |
|
720 |
because $f(a)$ is lexicographically greater than $b$ and~$c$. These |
|
721 |
re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the |
|
722 |
conclusion by~$f(a)$. |
|
723 |
||
724 |
Another example is the goal $\neg(t=u) \imp \neg(u=t)$. |
|
725 |
The differing orientations make this appear difficult to prove. Ordered |
|
726 |
rewriting with {\tt symmetry} makes the equalities agree. (Without |
|
727 |
knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$ |
|
728 |
or~$u=t$.) Then the simplifier can prove the goal outright. |
|
729 |
||
730 |
\index{rewrite rules!permutative|)} |
|
731 |
||
732 |
||
733 |
\section{*Setting up the simplifier}\label{sec:setting-up-simp} |
|
734 |
\index{simplification!setting up} |
|
286 | 735 |
|
736 |
Setting up the simplifier for new logics is complicated. This section |
|
323 | 737 |
describes how the simplifier is installed for intuitionistic first-order |
738 |
logic; the code is largely taken from {\tt FOL/simpdata.ML}. |
|
286 | 739 |
|
323 | 740 |
The simplifier and the case splitting tactic, which reside on separate |
741 |
files, are not part of Pure Isabelle. They must be loaded explicitly: |
|
286 | 742 |
\begin{ttbox} |
743 |
use "../Provers/simplifier.ML"; |
|
744 |
use "../Provers/splitter.ML"; |
|
745 |
\end{ttbox} |
|
746 |
||
747 |
Simplification works by reducing various object-equalities to |
|
323 | 748 |
meta-equality. It requires rules stating that equal terms and equivalent |
749 |
formulae are also equal at the meta-level. The rule declaration part of |
|
750 |
the file {\tt FOL/ifol.thy} contains the two lines |
|
751 |
\begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem} |
|
286 | 752 |
eq_reflection "(x=y) ==> (x==y)" |
753 |
iff_reflection "(P<->Q) ==> (P==Q)" |
|
754 |
\end{ttbox} |
|
323 | 755 |
Of course, you should only assert such rules if they are true for your |
286 | 756 |
particular logic. In Constructive Type Theory, equality is a ternary |
757 |
relation of the form $a=b\in A$; the type~$A$ determines the meaning of the |
|
332 | 758 |
equality essentially as a partial equivalence relation. The present |
323 | 759 |
simplifier cannot be used. Rewriting in {\tt CTT} uses another simplifier, |
760 |
which resides in the file {\tt typedsimp.ML} and is not documented. Even |
|
761 |
this does not work for later variants of Constructive Type Theory that use |
|
762 |
intensional equality~\cite{nordstrom90}. |
|
286 | 763 |
|
764 |
||
765 |
\subsection{A collection of standard rewrite rules} |
|
766 |
The file begins by proving lots of standard rewrite rules about the logical |
|
323 | 767 |
connectives. These include cancellation and associative laws. To prove |
768 |
them easily, it defines a function that echoes the desired law and then |
|
286 | 769 |
supplies it the theorem prover for intuitionistic \FOL: |
770 |
\begin{ttbox} |
|
771 |
fun int_prove_fun s = |
|
772 |
(writeln s; |
|
773 |
prove_goal IFOL.thy s |
|
774 |
(fn prems => [ (cut_facts_tac prems 1), |
|
775 |
(Int.fast_tac 1) ])); |
|
776 |
\end{ttbox} |
|
777 |
The following rewrite rules about conjunction are a selection of those |
|
778 |
proved on {\tt FOL/simpdata.ML}. Later, these will be supplied to the |
|
779 |
standard simpset. |
|
780 |
\begin{ttbox} |
|
781 |
val conj_rews = map int_prove_fun |
|
782 |
["P & True <-> P", "True & P <-> P", |
|
783 |
"P & False <-> False", "False & P <-> False", |
|
784 |
"P & P <-> P", |
|
785 |
"P & ~P <-> False", "~P & P <-> False", |
|
786 |
"(P & Q) & R <-> P & (Q & R)"]; |
|
787 |
\end{ttbox} |
|
788 |
The file also proves some distributive laws. As they can cause exponential |
|
789 |
blowup, they will not be included in the standard simpset. Instead they |
|
323 | 790 |
are merely bound to an \ML{} identifier, for user reference. |
286 | 791 |
\begin{ttbox} |
792 |
val distrib_rews = map int_prove_fun |
|
793 |
["P & (Q | R) <-> P&Q | P&R", |
|
794 |
"(Q | R) & P <-> Q&P | R&P", |
|
795 |
"(P | Q --> R) <-> (P --> R) & (Q --> R)"]; |
|
796 |
\end{ttbox} |
|
797 |
||
798 |
||
799 |
\subsection{Functions for preprocessing the rewrite rules} |
|
323 | 800 |
\label{sec:setmksimps} |
801 |
% |
|
286 | 802 |
The next step is to define the function for preprocessing rewrite rules. |
803 |
This will be installed by calling {\tt setmksimps} below. Preprocessing |
|
804 |
occurs whenever rewrite rules are added, whether by user command or |
|
805 |
automatically. Preprocessing involves extracting atomic rewrites at the |
|
806 |
object-level, then reflecting them to the meta-level. |
|
807 |
||
808 |
To start, the function {\tt gen_all} strips any meta-level |
|
809 |
quantifiers from the front of the given theorem. Usually there are none |
|
810 |
anyway. |
|
811 |
\begin{ttbox} |
|
812 |
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; |
|
813 |
\end{ttbox} |
|
814 |
The function {\tt atomize} analyses a theorem in order to extract |
|
815 |
atomic rewrite rules. The head of all the patterns, matched by the |
|
816 |
wildcard~{\tt _}, is the coercion function {\tt Trueprop}. |
|
817 |
\begin{ttbox} |
|
818 |
fun atomize th = case concl_of th of |
|
819 |
_ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) \at |
|
820 |
atomize(th RS conjunct2) |
|
821 |
| _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp) |
|
822 |
| _ $ (Const("All",_) $ _) => atomize(th RS spec) |
|
823 |
| _ $ (Const("True",_)) => [] |
|
824 |
| _ $ (Const("False",_)) => [] |
|
825 |
| _ => [th]; |
|
826 |
\end{ttbox} |
|
827 |
There are several cases, depending upon the form of the conclusion: |
|
828 |
\begin{itemize} |
|
829 |
\item Conjunction: extract rewrites from both conjuncts. |
|
830 |
||
831 |
\item Implication: convert $P\imp Q$ to the meta-implication $P\Imp Q$ and |
|
832 |
extract rewrites from~$Q$; these will be conditional rewrites with the |
|
833 |
condition~$P$. |
|
834 |
||
835 |
\item Universal quantification: remove the quantifier, replacing the bound |
|
836 |
variable by a schematic variable, and extract rewrites from the body. |
|
837 |
||
838 |
\item {\tt True} and {\tt False} contain no useful rewrites. |
|
839 |
||
840 |
\item Anything else: return the theorem in a singleton list. |
|
841 |
\end{itemize} |
|
842 |
The resulting theorems are not literally atomic --- they could be |
|
323 | 843 |
disjunctive, for example --- but are broken down as much as possible. See |
286 | 844 |
the file {\tt ZF/simpdata.ML} for a sophisticated translation of |
845 |
set-theoretic formulae into rewrite rules. |
|
104 | 846 |
|
286 | 847 |
The simplified rewrites must now be converted into meta-equalities. The |
323 | 848 |
rule {\tt eq_reflection} converts equality rewrites, while {\tt |
286 | 849 |
iff_reflection} converts if-and-only-if rewrites. The latter possibility |
850 |
can arise in two other ways: the negative theorem~$\neg P$ is converted to |
|
323 | 851 |
$P\equiv{\tt False}$, and any other theorem~$P$ is converted to |
286 | 852 |
$P\equiv{\tt True}$. The rules {\tt iff_reflection_F} and {\tt |
853 |
iff_reflection_T} accomplish this conversion. |
|
854 |
\begin{ttbox} |
|
855 |
val P_iff_F = int_prove_fun "~P ==> (P <-> False)"; |
|
856 |
val iff_reflection_F = P_iff_F RS iff_reflection; |
|
857 |
\ttbreak |
|
858 |
val P_iff_T = int_prove_fun "P ==> (P <-> True)"; |
|
859 |
val iff_reflection_T = P_iff_T RS iff_reflection; |
|
860 |
\end{ttbox} |
|
861 |
The function {\tt mk_meta_eq} converts a theorem to a meta-equality |
|
862 |
using the case analysis described above. |
|
863 |
\begin{ttbox} |
|
864 |
fun mk_meta_eq th = case concl_of th of |
|
865 |
_ $ (Const("op =",_)$_$_) => th RS eq_reflection |
|
866 |
| _ $ (Const("op <->",_)$_$_) => th RS iff_reflection |
|
867 |
| _ $ (Const("Not",_)$_) => th RS iff_reflection_F |
|
868 |
| _ => th RS iff_reflection_T; |
|
869 |
\end{ttbox} |
|
870 |
The three functions {\tt gen_all}, {\tt atomize} and {\tt mk_meta_eq} will |
|
871 |
be composed together and supplied below to {\tt setmksimps}. |
|
872 |
||
873 |
||
874 |
\subsection{Making the initial simpset} |
|
875 |
It is time to assemble these items. We open module {\tt Simplifier} to |
|
323 | 876 |
gain access to its components. We define the infix operator |
877 |
\ttindexbold{addcongs} to insert congruence rules; given a list of theorems, |
|
878 |
it converts their conclusions into meta-equalities and passes them to |
|
879 |
\ttindex{addeqcongs}. |
|
286 | 880 |
\begin{ttbox} |
881 |
open Simplifier; |
|
882 |
\ttbreak |
|
883 |
infix addcongs; |
|
884 |
fun ss addcongs congs = |
|
885 |
ss addeqcongs (congs RL [eq_reflection,iff_reflection]); |
|
886 |
\end{ttbox} |
|
887 |
The list {\tt IFOL_rews} contains the default rewrite rules for first-order |
|
888 |
logic. The first of these is the reflexive law expressed as the |
|
323 | 889 |
equivalence $(a=a)\bimp{\tt True}$; the rewrite rule $a=a$ is clearly useless. |
286 | 890 |
\begin{ttbox} |
891 |
val IFOL_rews = |
|
892 |
[refl RS P_iff_T] \at conj_rews \at disj_rews \at not_rews \at |
|
893 |
imp_rews \at iff_rews \at quant_rews; |
|
894 |
\end{ttbox} |
|
895 |
The list {\tt triv_rls} contains trivial theorems for the solver. Any |
|
896 |
subgoal that is simplified to one of these will be removed. |
|
897 |
\begin{ttbox} |
|
898 |
val notFalseI = int_prove_fun "~False"; |
|
899 |
val triv_rls = [TrueI,refl,iff_refl,notFalseI]; |
|
900 |
\end{ttbox} |
|
323 | 901 |
% |
286 | 902 |
The basic simpset for intuitionistic \FOL{} starts with \ttindex{empty_ss}. |
903 |
It preprocess rewrites using {\tt gen_all}, {\tt atomize} and {\tt |
|
904 |
mk_meta_eq}. It solves simplified subgoals using {\tt triv_rls} and |
|
905 |
assumptions. It uses \ttindex{asm_simp_tac} to tackle subgoals of |
|
906 |
conditional rewrites. It takes {\tt IFOL_rews} as rewrite rules. |
|
907 |
Other simpsets built from {\tt IFOL_ss} will inherit these items. |
|
323 | 908 |
In particular, {\tt FOL_ss} extends {\tt IFOL_ss} with classical rewrite |
909 |
rules such as $\neg\neg P\bimp P$. |
|
286 | 910 |
\index{*setmksimps}\index{*setsolver}\index{*setsubgoaler} |
911 |
\index{*addsimps}\index{*addcongs} |
|
912 |
\begin{ttbox} |
|
913 |
val IFOL_ss = |
|
914 |
empty_ss |
|
915 |
setmksimps (map mk_meta_eq o atomize o gen_all) |
|
916 |
setsolver (fn prems => resolve_tac (triv_rls \at prems) ORELSE' |
|
917 |
assume_tac) |
|
918 |
setsubgoaler asm_simp_tac |
|
919 |
addsimps IFOL_rews |
|
920 |
addcongs [imp_cong]; |
|
921 |
\end{ttbox} |
|
922 |
This simpset takes {\tt imp_cong} as a congruence rule in order to use |
|
923 |
contextual information to simplify the conclusions of implications: |
|
924 |
\[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp |
|
925 |
(\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'}) |
|
926 |
\] |
|
927 |
By adding the congruence rule {\tt conj_cong}, we could obtain a similar |
|
928 |
effect for conjunctions. |
|
929 |
||
930 |
||
931 |
\subsection{Case splitting} |
|
323 | 932 |
To set up case splitting, we must prove the theorem below and pass it to |
933 |
\ttindexbold{mk_case_split_tac}. The tactic \ttindexbold{split_tac} uses |
|
934 |
{\tt mk_meta_eq}, defined above, to convert the splitting rules to |
|
935 |
meta-equalities. |
|
286 | 936 |
\begin{ttbox} |
937 |
val meta_iffD = |
|
938 |
prove_goal FOL.thy "[| P==Q; Q |] ==> P" |
|
939 |
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]) |
|
940 |
\ttbreak |
|
941 |
fun split_tac splits = |
|
942 |
mk_case_split_tac meta_iffD (map mk_meta_eq splits); |
|
943 |
\end{ttbox} |
|
944 |
% |
|
323 | 945 |
The splitter replaces applications of a given function; the right-hand side |
946 |
of the replacement can be anything. For example, here is a splitting rule |
|
947 |
for conditional expressions: |
|
286 | 948 |
\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x})) |
949 |
\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y})) |
|
950 |
\] |
|
323 | 951 |
Another example is the elimination operator (which happens to be |
952 |
called~$split$) for Cartesian products: |
|
286 | 953 |
\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} = |
954 |
\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) |
|
955 |
\] |
|
956 |
Case splits should be allowed only when necessary; they are expensive |
|
957 |
and hard to control. Here is a typical example of use, where {\tt |
|
958 |
expand_if} is the first rule above: |
|
959 |
\begin{ttbox} |
|
960 |
by (simp_tac (prop_rec_ss setloop (split_tac [expand_if])) 1); |
|
961 |
\end{ttbox} |
|
962 |
||
104 | 963 |
|
964 |
||
965 |
\index{simplification|)} |
|
966 |
||
286 | 967 |