doc-src/TutorialI/Misc/simp.thy
author nipkow
Wed Dec 13 09:39:53 2000 +0100 (2000-12-13)
changeset 10654 458068404143
parent 10362 c6b197ccf1f1
child 10788 ea48dd8b0232
permissions -rw-r--r--
*** empty log message ***
nipkow@9932
     1
(*<*)
wenzelm@9922
     2
theory simp = Main:
nipkow@9932
     3
(*>*)
wenzelm@9922
     4
nipkow@9932
     5
subsubsection{*Simplification rules*}
nipkow@9932
     6
nipkow@9932
     7
text{*\indexbold{simplification rule}
nipkow@9932
     8
To facilitate simplification, theorems can be declared to be simplification
nipkow@9932
     9
rules (with the help of the attribute @{text"[simp]"}\index{*simp
nipkow@9932
    10
  (attribute)}), in which case proofs by simplification make use of these
nipkow@9932
    11
rules automatically. In addition the constructs \isacommand{datatype} and
nipkow@9932
    12
\isacommand{primrec} (and a few others) invisibly declare useful
nipkow@9932
    13
simplification rules. Explicit definitions are \emph{not} declared
nipkow@9932
    14
simplification rules automatically!
nipkow@9932
    15
nipkow@9932
    16
Not merely equations but pretty much any theorem can become a simplification
nipkow@9932
    17
rule. The simplifier will try to make sense of it.  For example, a theorem
nipkow@9932
    18
@{prop"~P"} is automatically turned into @{prop"P = False"}. The details
nipkow@9932
    19
are explained in \S\ref{sec:SimpHow}.
nipkow@9932
    20
nipkow@9932
    21
The simplification attribute of theorems can be turned on and off as follows:
nipkow@9932
    22
\begin{quote}
nipkow@9932
    23
\isacommand{declare} \textit{theorem-name}@{text"[simp]"}\\
nipkow@9932
    24
\isacommand{declare} \textit{theorem-name}@{text"[simp del]"}
nipkow@9932
    25
\end{quote}
nipkow@9932
    26
As a rule of thumb, equations that really simplify (like @{prop"rev(rev xs) =
nipkow@9932
    27
 xs"} and @{prop"xs @ [] = xs"}) should be made simplification
nipkow@9932
    28
rules.  Those of a more specific nature (e.g.\ distributivity laws, which
nipkow@9932
    29
alter the structure of terms considerably) should only be used selectively,
nipkow@9932
    30
i.e.\ they should not be default simplification rules.  Conversely, it may
nipkow@9932
    31
also happen that a simplification rule needs to be disabled in certain
nipkow@9932
    32
proofs.  Frequent changes in the simplification status of a theorem may
nipkow@9932
    33
indicate a badly designed theory.
nipkow@9932
    34
\begin{warn}
nipkow@9932
    35
  Simplification may not terminate, for example if both $f(x) = g(x)$ and
nipkow@9932
    36
  $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
nipkow@9932
    37
  to include simplification rules that can lead to nontermination, either on
nipkow@9932
    38
  their own or in combination with other simplification rules.
nipkow@9932
    39
\end{warn}
nipkow@9932
    40
*}
nipkow@9932
    41
nipkow@9932
    42
subsubsection{*The simplification method*}
nipkow@9932
    43
nipkow@9932
    44
text{*\index{*simp (method)|bold}
nipkow@9932
    45
The general format of the simplification method is
nipkow@9932
    46
\begin{quote}
nipkow@9932
    47
@{text simp} \textit{list of modifiers}
nipkow@9932
    48
\end{quote}
nipkow@9932
    49
where the list of \emph{modifiers} helps to fine tune the behaviour and may
nipkow@9932
    50
be empty. Most if not all of the proofs seen so far could have been performed
nipkow@9932
    51
with @{text simp} instead of \isa{auto}, except that @{text simp} attacks
nipkow@9932
    52
only the first subgoal and may thus need to be repeated---use
nipkow@9932
    53
\isaindex{simp_all} to simplify all subgoals.
nipkow@9932
    54
Note that @{text simp} fails if nothing changes.
nipkow@9932
    55
*}
nipkow@9932
    56
nipkow@9932
    57
subsubsection{*Adding and deleting simplification rules*}
nipkow@9932
    58
nipkow@9932
    59
text{*
nipkow@9932
    60
If a certain theorem is merely needed in a few proofs by simplification,
nipkow@9932
    61
we do not need to make it a global simplification rule. Instead we can modify
nipkow@9932
    62
the set of simplification rules used in a simplification step by adding rules
nipkow@9932
    63
to it and/or deleting rules from it. The two modifiers for this are
nipkow@9932
    64
\begin{quote}
nipkow@9932
    65
@{text"add:"} \textit{list of theorem names}\\
nipkow@9932
    66
@{text"del:"} \textit{list of theorem names}
nipkow@9932
    67
\end{quote}
nipkow@9932
    68
In case you want to use only a specific list of theorems and ignore all
nipkow@9932
    69
others:
nipkow@9932
    70
\begin{quote}
nipkow@9932
    71
@{text"only:"} \textit{list of theorem names}
nipkow@9932
    72
\end{quote}
nipkow@9932
    73
*}
nipkow@9932
    74
nipkow@9932
    75
subsubsection{*Assumptions*}
nipkow@9932
    76
nipkow@9932
    77
text{*\index{simplification!with/of assumptions}
nipkow@9932
    78
By default, assumptions are part of the simplification process: they are used
nipkow@9932
    79
as simplification rules and are simplified themselves. For example:
nipkow@9932
    80
*}
nipkow@9932
    81
nipkow@10171
    82
lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs";
nipkow@10171
    83
apply simp;
nipkow@10171
    84
done
nipkow@9932
    85
nipkow@9932
    86
text{*\noindent
nipkow@9932
    87
The second assumption simplifies to @{term"xs = []"}, which in turn
nipkow@9932
    88
simplifies the first assumption to @{term"zs = ys"}, thus reducing the
nipkow@9932
    89
conclusion to @{term"ys = ys"} and hence to @{term"True"}.
nipkow@9932
    90
nipkow@9932
    91
In some cases this may be too much of a good thing and may lead to
nipkow@9932
    92
nontermination:
nipkow@9932
    93
*}
nipkow@9932
    94
nipkow@10171
    95
lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []";
nipkow@9932
    96
nipkow@9932
    97
txt{*\noindent
nipkow@9932
    98
cannot be solved by an unmodified application of @{text"simp"} because the
nipkow@9932
    99
simplification rule @{term"f x = g (f (g x))"} extracted from the assumption
nipkow@9932
   100
does not terminate. Isabelle notices certain simple forms of
nipkow@9932
   101
nontermination but not this one. The problem can be circumvented by
nipkow@9932
   102
explicitly telling the simplifier to ignore the assumptions:
nipkow@9932
   103
*}
nipkow@9932
   104
nipkow@10171
   105
apply(simp (no_asm));
nipkow@10171
   106
done
nipkow@9932
   107
nipkow@9932
   108
text{*\noindent
nipkow@9932
   109
There are three options that influence the treatment of assumptions:
nipkow@9932
   110
\begin{description}
nipkow@9932
   111
\item[@{text"(no_asm)"}]\indexbold{*no_asm}
nipkow@9932
   112
 means that assumptions are completely ignored.
nipkow@9932
   113
\item[@{text"(no_asm_simp)"}]\indexbold{*no_asm_simp}
nipkow@9932
   114
 means that the assumptions are not simplified but
nipkow@9932
   115
  are used in the simplification of the conclusion.
nipkow@9932
   116
\item[@{text"(no_asm_use)"}]\indexbold{*no_asm_use}
nipkow@9932
   117
 means that the assumptions are simplified but are not
nipkow@9932
   118
  used in the simplification of each other or the conclusion.
nipkow@9932
   119
\end{description}
nipkow@9932
   120
Neither @{text"(no_asm_simp)"} nor @{text"(no_asm_use)"} allow to simplify
nipkow@9932
   121
the above problematic subgoal.
nipkow@9932
   122
nipkow@9932
   123
Note that only one of the above options is allowed, and it must precede all
nipkow@9932
   124
other arguments.
nipkow@9932
   125
*}
nipkow@9932
   126
nipkow@9932
   127
subsubsection{*Rewriting with definitions*}
nipkow@9932
   128
nipkow@9932
   129
text{*\index{simplification!with definitions}
nipkow@9932
   130
Constant definitions (\S\ref{sec:ConstDefinitions}) can
nipkow@9932
   131
be used as simplification rules, but by default they are not.  Hence the
nipkow@9932
   132
simplifier does not expand them automatically, just as it should be:
nipkow@9932
   133
definitions are introduced for the purpose of abbreviating complex
nipkow@9932
   134
concepts. Of course we need to expand the definitions initially to derive
nipkow@9932
   135
enough lemmas that characterize the concept sufficiently for us to forget the
nipkow@9932
   136
original definition. For example, given
nipkow@9932
   137
*}
nipkow@9932
   138
nipkow@10171
   139
constdefs exor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
nipkow@10171
   140
         "exor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)";
nipkow@9932
   141
nipkow@9932
   142
text{*\noindent
nipkow@9932
   143
we may want to prove
nipkow@9932
   144
*}
nipkow@9932
   145
nipkow@10171
   146
lemma "exor A (\<not>A)";
nipkow@9932
   147
nipkow@9932
   148
txt{*\noindent
nipkow@9932
   149
Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
nipkow@9932
   150
get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}
nipkow@9932
   151
*}
nipkow@9932
   152
nipkow@9932
   153
apply(simp only:exor_def);
nipkow@9932
   154
nipkow@9932
   155
txt{*\noindent
nipkow@9932
   156
In this particular case, the resulting goal
nipkow@10362
   157
@{subgoals[display,indent=0]}
nipkow@10171
   158
can be proved by simplification. Thus we could have proved the lemma outright by
nipkow@10171
   159
*}(*<*)oops;lemma "exor A (\<not>A)";(*>*)
nipkow@10171
   160
apply(simp add: exor_def)
nipkow@10171
   161
(*<*)done(*>*)
nipkow@9932
   162
text{*\noindent
nipkow@9932
   163
Of course we can also unfold definitions in the middle of a proof.
nipkow@9932
   164
nipkow@9932
   165
You should normally not turn a definition permanently into a simplification
nipkow@9932
   166
rule because this defeats the whole purpose of an abbreviation.
nipkow@9932
   167
nipkow@9932
   168
\begin{warn}
nipkow@9932
   169
  If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
nipkow@9932
   170
  occurrences of $f$ with at least two arguments. Thus it is safer to define
nipkow@9932
   171
  $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
nipkow@9932
   172
\end{warn}
nipkow@9932
   173
*}
nipkow@9932
   174
nipkow@9932
   175
subsubsection{*Simplifying let-expressions*}
nipkow@9932
   176
nipkow@9932
   177
text{*\index{simplification!of let-expressions}
nipkow@9932
   178
Proving a goal containing \isaindex{let}-expressions almost invariably
nipkow@9932
   179
requires the @{text"let"}-con\-structs to be expanded at some point. Since
nipkow@9932
   180
@{text"let"}-@{text"in"} is just syntactic sugar for a predefined constant
nipkow@9932
   181
(called @{term"Let"}), expanding @{text"let"}-constructs means rewriting with
nipkow@9932
   182
@{thm[source]Let_def}:
nipkow@9932
   183
*}
nipkow@9932
   184
nipkow@9932
   185
lemma "(let xs = [] in xs@ys@xs) = ys";
nipkow@10171
   186
apply(simp add: Let_def);
nipkow@10171
   187
done
nipkow@9932
   188
nipkow@9932
   189
text{*
nipkow@9932
   190
If, in a particular context, there is no danger of a combinatorial explosion
nipkow@9932
   191
of nested @{text"let"}s one could even simlify with @{thm[source]Let_def} by
nipkow@9932
   192
default:
nipkow@9932
   193
*}
nipkow@9932
   194
declare Let_def [simp]
nipkow@9932
   195
nipkow@9932
   196
subsubsection{*Conditional equations*}
nipkow@9932
   197
nipkow@9932
   198
text{*
nipkow@9932
   199
So far all examples of rewrite rules were equations. The simplifier also
nipkow@9932
   200
accepts \emph{conditional} equations, for example
nipkow@9932
   201
*}
nipkow@9932
   202
nipkow@10171
   203
lemma hd_Cons_tl[simp]: "xs \<noteq> []  \<Longrightarrow>  hd xs # tl xs = xs";
nipkow@10171
   204
apply(case_tac xs, simp, simp);
nipkow@10171
   205
done
nipkow@9932
   206
nipkow@9932
   207
text{*\noindent
nipkow@9932
   208
Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
nipkow@9932
   209
sequence of methods. Assuming that the simplification rule
nipkow@9932
   210
@{term"(rev xs = []) = (xs = [])"}
nipkow@9932
   211
is present as well,
nipkow@9932
   212
*}
nipkow@9932
   213
nipkow@10171
   214
lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
nipkow@9932
   215
(*<*)
nipkow@9932
   216
by(simp);
nipkow@9932
   217
(*>*)
nipkow@9932
   218
text{*\noindent
nipkow@9932
   219
is proved by plain simplification:
nipkow@9932
   220
the conditional equation @{thm[source]hd_Cons_tl} above
nipkow@9932
   221
can simplify @{term"hd(rev xs) # tl(rev xs)"} to @{term"rev xs"}
nipkow@9932
   222
because the corresponding precondition @{term"rev xs ~= []"}
nipkow@9932
   223
simplifies to @{term"xs ~= []"}, which is exactly the local
nipkow@9932
   224
assumption of the subgoal.
nipkow@9932
   225
*}
nipkow@9932
   226
nipkow@9932
   227
nipkow@9932
   228
subsubsection{*Automatic case splits*}
nipkow@9932
   229
nipkow@10654
   230
text{*\indexbold{case splits}\index{*split (method, attr.)|(}
nipkow@9932
   231
Goals containing @{text"if"}-expressions are usually proved by case
nipkow@9932
   232
distinction on the condition of the @{text"if"}. For example the goal
nipkow@9932
   233
*}
nipkow@9932
   234
nipkow@10171
   235
lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []";
nipkow@9932
   236
nipkow@9932
   237
txt{*\noindent
nipkow@10654
   238
can be split by a special method @{text split}:
nipkow@9932
   239
*}
nipkow@9932
   240
nipkow@10654
   241
apply(split split_if)
nipkow@9932
   242
nipkow@10362
   243
txt{*\noindent
nipkow@10362
   244
@{subgoals[display,indent=0]}
nipkow@10654
   245
where \isaindexbold{split_if} is a theorem that expresses splitting of
nipkow@10654
   246
@{text"if"}s. Because
nipkow@9932
   247
case-splitting on @{text"if"}s is almost always the right proof strategy, the
nipkow@9932
   248
simplifier performs it automatically. Try \isacommand{apply}@{text"(simp)"}
nipkow@9932
   249
on the initial goal above.
nipkow@9932
   250
nipkow@9932
   251
This splitting idea generalizes from @{text"if"} to \isaindex{case}:
nipkow@10654
   252
*}(*<*)by simp(*>*)
nipkow@10171
   253
lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
nipkow@10654
   254
apply(split list.split);
nipkow@9932
   255
nipkow@10362
   256
txt{*
nipkow@10362
   257
@{subgoals[display,indent=0]}
nipkow@9932
   258
In contrast to @{text"if"}-expressions, the simplifier does not split
nipkow@9932
   259
@{text"case"}-expressions by default because this can lead to nontermination
nipkow@10654
   260
in case of recursive datatypes. Therefore the simplifier has a modifier
nipkow@10654
   261
@{text split} for adding further splitting rules explicitly. This means the
nipkow@10654
   262
above lemma can be proved in one step by
nipkow@9932
   263
*}
nipkow@10362
   264
(*<*)oops;
nipkow@10171
   265
lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
nipkow@9932
   266
(*>*)
nipkow@10171
   267
apply(simp split: list.split);
nipkow@10171
   268
(*<*)done(*>*)
nipkow@10654
   269
text{*\noindent
nipkow@10654
   270
whereas \isacommand{apply}@{text"(simp)"} alone will not succeed.
nipkow@9932
   271
nipkow@9932
   272
In general, every datatype $t$ comes with a theorem
nipkow@9932
   273
$t$@{text".split"} which can be declared to be a \bfindex{split rule} either
nipkow@9932
   274
locally as above, or by giving it the @{text"split"} attribute globally:
nipkow@9932
   275
*}
nipkow@9932
   276
nipkow@9932
   277
declare list.split [split]
nipkow@9932
   278
nipkow@9932
   279
text{*\noindent
nipkow@9932
   280
The @{text"split"} attribute can be removed with the @{text"del"} modifier,
nipkow@9932
   281
either locally
nipkow@9932
   282
*}
nipkow@9932
   283
(*<*)
nipkow@9932
   284
lemma "dummy=dummy";
nipkow@9932
   285
(*>*)
nipkow@9932
   286
apply(simp split del: split_if);
nipkow@9932
   287
(*<*)
nipkow@9932
   288
oops;
nipkow@9932
   289
(*>*)
nipkow@9932
   290
text{*\noindent
nipkow@9932
   291
or globally:
nipkow@9932
   292
*}
nipkow@9932
   293
declare list.split [split del]
nipkow@9932
   294
nipkow@9932
   295
text{*
nipkow@10654
   296
In polished proofs the @{text split} method is rarely used on its own
nipkow@10654
   297
but always as part of the simplifier. However, if a goal contains
nipkow@10654
   298
multiple splittable constructs, the @{text split} method can be
nipkow@10654
   299
helpful in selectively exploring the effects of splitting.
nipkow@10654
   300
nipkow@9932
   301
The above split rules intentionally only affect the conclusion of a
nipkow@9932
   302
subgoal.  If you want to split an @{text"if"} or @{text"case"}-expression in
nipkow@9932
   303
the assumptions, you have to apply @{thm[source]split_if_asm} or
nipkow@9932
   304
$t$@{text".split_asm"}:
nipkow@9932
   305
*}
nipkow@9932
   306
nipkow@10654
   307
lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []"
nipkow@10654
   308
apply(split split_if_asm)
nipkow@9932
   309
nipkow@10362
   310
txt{*\noindent
nipkow@9932
   311
In contrast to splitting the conclusion, this actually creates two
nipkow@9932
   312
separate subgoals (which are solved by @{text"simp_all"}):
nipkow@10362
   313
@{subgoals[display,indent=0]}
nipkow@9932
   314
If you need to split both in the assumptions and the conclusion,
nipkow@9932
   315
use $t$@{text".splits"} which subsumes $t$@{text".split"} and
nipkow@9932
   316
$t$@{text".split_asm"}. Analogously, there is @{thm[source]if_splits}.
nipkow@9932
   317
nipkow@9932
   318
\begin{warn}
nipkow@9932
   319
  The simplifier merely simplifies the condition of an \isa{if} but not the
nipkow@9932
   320
  \isa{then} or \isa{else} parts. The latter are simplified only after the
nipkow@9932
   321
  condition reduces to \isa{True} or \isa{False}, or after splitting. The
nipkow@9932
   322
  same is true for \isaindex{case}-expressions: only the selector is
nipkow@9932
   323
  simplified at first, until either the expression reduces to one of the
nipkow@9932
   324
  cases or it is split.
nipkow@10654
   325
\end{warn}\index{*split (method, attr.)|)}
nipkow@9932
   326
*}
nipkow@10362
   327
(*<*)
nipkow@10362
   328
by(simp_all)
nipkow@10362
   329
(*>*)
nipkow@9932
   330
nipkow@9932
   331
subsubsection{*Arithmetic*}
nipkow@9932
   332
nipkow@9932
   333
text{*\index{arithmetic}
nipkow@9932
   334
The simplifier routinely solves a small class of linear arithmetic formulae
nipkow@9932
   335
(over type \isa{nat} and other numeric types): it only takes into account
nipkow@9932
   336
assumptions and conclusions that are (possibly negated) (in)equalities
nipkow@9932
   337
(@{text"="}, \isasymle, @{text"<"}) and it only knows about addition. Thus
nipkow@9932
   338
*}
nipkow@9932
   339
nipkow@10171
   340
lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
nipkow@9932
   341
(*<*)by(auto)(*>*)
nipkow@9932
   342
nipkow@9932
   343
text{*\noindent
nipkow@9932
   344
is proved by simplification, whereas the only slightly more complex
nipkow@9932
   345
*}
nipkow@9932
   346
nipkow@10171
   347
lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n";
nipkow@9932
   348
(*<*)by(arith)(*>*)
nipkow@9932
   349
nipkow@9932
   350
text{*\noindent
nipkow@9932
   351
is not proved by simplification and requires @{text arith}.
nipkow@9932
   352
*}
nipkow@9932
   353
nipkow@9932
   354
nipkow@9932
   355
subsubsection{*Tracing*}
nipkow@9932
   356
text{*\indexbold{tracing the simplifier}
nipkow@9932
   357
Using the simplifier effectively may take a bit of experimentation.  Set the
nipkow@9932
   358
\isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
nipkow@9932
   359
on:
nipkow@9932
   360
*}
nipkow@9932
   361
nipkow@9932
   362
ML "set trace_simp";
nipkow@9932
   363
lemma "rev [a] = []";
nipkow@9932
   364
apply(simp);
nipkow@9932
   365
(*<*)oops(*>*)
nipkow@9932
   366
nipkow@9932
   367
text{*\noindent
nipkow@9932
   368
produces the trace
nipkow@9932
   369
nipkow@9932
   370
\begin{ttbox}\makeatother
nipkow@9932
   371
Applying instance of rewrite rule:
nipkow@9932
   372
rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
nipkow@9932
   373
Rewriting:
nipkow@9932
   374
rev [x] == rev [] @ [x]
nipkow@9932
   375
Applying instance of rewrite rule:
nipkow@9932
   376
rev [] == []
nipkow@9932
   377
Rewriting:
nipkow@9932
   378
rev [] == []
nipkow@9932
   379
Applying instance of rewrite rule:
nipkow@9932
   380
[] @ ?y == ?y
nipkow@9932
   381
Rewriting:
nipkow@9932
   382
[] @ [x] == [x]
nipkow@9932
   383
Applying instance of rewrite rule:
nipkow@9932
   384
?x3 \# ?t3 = ?t3 == False
nipkow@9932
   385
Rewriting:
nipkow@9932
   386
[x] = [] == False
nipkow@9932
   387
\end{ttbox}
nipkow@9932
   388
nipkow@9932
   389
In more complicated cases, the trace can be quite lenghty, especially since
nipkow@9932
   390
invocations of the simplifier are often nested (e.g.\ when solving conditions
nipkow@9932
   391
of rewrite rules). Thus it is advisable to reset it:
nipkow@9932
   392
*}
nipkow@9932
   393
nipkow@9932
   394
ML "reset trace_simp";
nipkow@9932
   395
nipkow@9932
   396
(*<*)
wenzelm@9922
   397
end
nipkow@9932
   398
(*>*)