doc-src/TutorialI/Misc/simp.thy
author nipkow
Wed, 12 Dec 2001 09:04:20 +0100
changeset 12473 f41e477576b9
parent 12332 aea72a834c85
child 12489 c92e38c3cbaa
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
     1
(*<*)
9922
wenzelm
parents:
diff changeset
     2
theory simp = Main:
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
     3
(*>*)
9922
wenzelm
parents:
diff changeset
     4
11214
3b3cc0cf533f *** empty log message ***
nipkow
parents: 11206
diff changeset
     5
subsection{*Simplification Rules*}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
     6
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
     7
text{*\index{simplification rules}
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
     8
To facilitate simplification,  
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
     9
the attribute @{text"[simp]"}\index{*simp (attribute)}
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    10
declares theorems to be simplification rules, which the simplifier
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    11
will use automatically.  In addition, \isacommand{datatype} and
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    12
\isacommand{primrec} declarations (and a few others) 
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    13
implicitly declare some simplification rules.  
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    14
Explicit definitions are \emph{not} declared as 
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    15
simplification rules automatically!
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    16
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    17
Nearly any theorem can become a simplification
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    18
rule. The simplifier will try to transform it into an equation.  
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    19
For example, the theorem
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    20
@{prop"~P"} is turned into @{prop"P = False"}. The details
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    21
are explained in \S\ref{sec:SimpHow}.
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    22
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    23
The simplification attribute of theorems can be turned on and off:%
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    24
\index{*simp del (attribute)}\REMARK{need to index attributes!switching off??}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    25
\begin{quote}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    26
\isacommand{declare} \textit{theorem-name}@{text"[simp]"}\\
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    27
\isacommand{declare} \textit{theorem-name}@{text"[simp del]"}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    28
\end{quote}
11309
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    29
Only equations that really simplify, like \isa{rev\
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    30
{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs} and
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    31
\isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    32
{\isacharequal}\ xs}, should be declared as default simplification rules. 
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    33
More specific ones should only be used selectively and should
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    34
not be made default.  Distributivity laws, for example, alter
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    35
the structure of terms and can produce an exponential blow-up instead of
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    36
simplification.  A default simplification rule may
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    37
need to be disabled in certain proofs.  Frequent changes in the simplification
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    38
status of a theorem may indicate an unwise use of defaults.
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    39
\begin{warn}
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    40
  Simplification can run forever, for example if both $f(x) = g(x)$ and
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    41
  $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    42
  to include simplification rules that can lead to nontermination, either on
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    43
  their own or in combination with other simplification rules.
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    44
\end{warn}
12332
aea72a834c85 *** empty log message ***
nipkow
parents: 11494
diff changeset
    45
\begin{warn}
aea72a834c85 *** empty log message ***
nipkow
parents: 11494
diff changeset
    46
  It is inadvisable to toggle the simplification attribute of a
aea72a834c85 *** empty log message ***
nipkow
parents: 11494
diff changeset
    47
  theorem from a parent theory $A$ in a child theory $B$ for good.
aea72a834c85 *** empty log message ***
nipkow
parents: 11494
diff changeset
    48
  The reason is that if some theory $C$ is based both on $B$ and (via a
aea72a834c85 *** empty log message ***
nipkow
parents: 11494
diff changeset
    49
  differnt path) on $A$, it is not defined what the simplification attribute
aea72a834c85 *** empty log message ***
nipkow
parents: 11494
diff changeset
    50
  of that theorem will be in $C$: it could be either.
aea72a834c85 *** empty log message ***
nipkow
parents: 11494
diff changeset
    51
\end{warn}
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    52
*} 
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    53
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    54
subsection{*The {\tt\slshape simp}  Method*}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    55
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    56
text{*\index{*simp (method)|bold}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    57
The general format of the simplification method is
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    58
\begin{quote}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    59
@{text simp} \textit{list of modifiers}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    60
\end{quote}
10795
9e888d60d3e5 minor edits to Chapters 1-3
paulson
parents: 10788
diff changeset
    61
where the list of \emph{modifiers} fine tunes the behaviour and may
11309
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    62
be empty. Specific modifiers are discussed below.  Most if not all of the
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    63
proofs seen so far could have been performed
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    64
with @{text simp} instead of \isa{auto}, except that @{text simp} attacks
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 10885
diff changeset
    65
only the first subgoal and may thus need to be repeated --- use
11428
332347b9b942 tidying the index
paulson
parents: 11309
diff changeset
    66
\methdx{simp_all} to simplify all subgoals.
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    67
If nothing changes, @{text simp} fails.
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    68
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    69
11214
3b3cc0cf533f *** empty log message ***
nipkow
parents: 11206
diff changeset
    70
subsection{*Adding and Deleting Simplification Rules*}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    71
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    72
text{*
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    73
\index{simplification rules!adding and deleting}%
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    74
If a certain theorem is merely needed in a few proofs by simplification,
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    75
we do not need to make it a global simplification rule. Instead we can modify
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    76
the set of simplification rules used in a simplification step by adding rules
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    77
to it and/or deleting rules from it. The two modifiers for this are
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    78
\begin{quote}
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    79
@{text"add:"} \textit{list of theorem names}\index{*add (modifier)}\\
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    80
@{text"del:"} \textit{list of theorem names}\index{*del (modifier)}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    81
\end{quote}
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    82
Or you can use a specific list of theorems and omit all others:
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    83
\begin{quote}
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
    84
@{text"only:"} \textit{list of theorem names}\index{*only (modifier)}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    85
\end{quote}
11309
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    86
In this example, we invoke the simplifier, adding two distributive
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    87
laws:
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    88
\begin{quote}
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    89
\isacommand{apply}@{text"(simp add: mod_mult_distrib add_mult_distrib)"}
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
    90
\end{quote}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    91
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    92
11214
3b3cc0cf533f *** empty log message ***
nipkow
parents: 11206
diff changeset
    93
subsection{*Assumptions*}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    94
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    95
text{*\index{simplification!with/of assumptions}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    96
By default, assumptions are part of the simplification process: they are used
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    97
as simplification rules and are simplified themselves. For example:
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    98
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
    99
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   100
lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs";
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   101
apply simp;
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   102
done
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   103
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   104
text{*\noindent
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   105
The second assumption simplifies to @{term"xs = []"}, which in turn
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   106
simplifies the first assumption to @{term"zs = ys"}, thus reducing the
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   107
conclusion to @{term"ys = ys"} and hence to @{term"True"}.
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   108
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   109
In some cases, using the assumptions can lead to nontermination:
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   110
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   111
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   112
lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []";
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   113
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   114
txt{*\noindent
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   115
An unmodified application of @{text"simp"} loops.  The culprit is the
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   116
simplification rule @{term"f x = g (f (g x))"}, which is extracted from
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   117
the assumption.  (Isabelle notices certain simple forms of
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   118
nontermination but not this one.)  The problem can be circumvented by
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   119
telling the simplifier to ignore the assumptions:
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   120
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   121
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   122
apply(simp (no_asm));
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   123
done
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   124
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   125
text{*\noindent
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   126
Three modifiers influence the treatment of assumptions:
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   127
\begin{description}
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   128
\item[@{text"(no_asm)"}]\index{*no_asm (modifier)}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   129
 means that assumptions are completely ignored.
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   130
\item[@{text"(no_asm_simp)"}]\index{*no_asm_simp (modifier)}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   131
 means that the assumptions are not simplified but
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   132
  are used in the simplification of the conclusion.
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   133
\item[@{text"(no_asm_use)"}]\index{*no_asm_use (modifier)}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   134
 means that the assumptions are simplified but are not
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   135
  used in the simplification of each other or the conclusion.
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   136
\end{description}
10795
9e888d60d3e5 minor edits to Chapters 1-3
paulson
parents: 10788
diff changeset
   137
Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on
9e888d60d3e5 minor edits to Chapters 1-3
paulson
parents: 10788
diff changeset
   138
the problematic subgoal above.
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   139
Only one of the modifiers is allowed, and it must precede all
11309
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
   140
other modifiers.
11206
5bea3a8abdc3 *** empty log message ***
nipkow
parents: 10983
diff changeset
   141
5bea3a8abdc3 *** empty log message ***
nipkow
parents: 10983
diff changeset
   142
\begin{warn}
5bea3a8abdc3 *** empty log message ***
nipkow
parents: 10983
diff changeset
   143
Assumptions are simplified in a left-to-right fashion. If an
5bea3a8abdc3 *** empty log message ***
nipkow
parents: 10983
diff changeset
   144
assumption can help in simplifying one to the left of it, this may get
5bea3a8abdc3 *** empty log message ***
nipkow
parents: 10983
diff changeset
   145
overlooked. In such cases you have to rotate the assumptions explicitly:
11428
332347b9b942 tidying the index
paulson
parents: 11309
diff changeset
   146
\isacommand{apply}@{text"("}\methdx{rotate_tac}~$n$@{text")"}
11206
5bea3a8abdc3 *** empty log message ***
nipkow
parents: 10983
diff changeset
   147
causes a cyclic shift by $n$ positions from right to left, if $n$ is
5bea3a8abdc3 *** empty log message ***
nipkow
parents: 10983
diff changeset
   148
positive, and from left to right, if $n$ is negative.
5bea3a8abdc3 *** empty log message ***
nipkow
parents: 10983
diff changeset
   149
Beware that such rotations make proofs quite brittle.
5bea3a8abdc3 *** empty log message ***
nipkow
parents: 10983
diff changeset
   150
\end{warn}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   151
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   152
11214
3b3cc0cf533f *** empty log message ***
nipkow
parents: 11206
diff changeset
   153
subsection{*Rewriting with Definitions*}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   154
11215
b44ad7e4c4d2 *** empty log message ***
nipkow
parents: 11214
diff changeset
   155
text{*\label{sec:Simp-with-Defs}\index{simplification!with definitions}
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   156
Constant definitions (\S\ref{sec:ConstDefinitions}) can be used as
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   157
simplification rules, but by default they are not: the simplifier does not
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   158
expand them automatically.  Definitions are intended for introducing abstract
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   159
concepts and not merely as abbreviations.  (Contrast with syntax
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   160
translations, \S\ref{sec:def-translations}.)  Of course, we need to expand
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   161
the definition initially, but once we have proved enough abstract properties
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   162
of the new constant, we can forget its original definition.  This style makes
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   163
proofs more robust: if the definition has to be changed,
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   164
only the proofs of the abstract properties will be affected.
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   165
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   166
For example, given *}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   167
10788
ea48dd8b0232 *** empty log message ***
nipkow
parents: 10654
diff changeset
   168
constdefs xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
ea48dd8b0232 *** empty log message ***
nipkow
parents: 10654
diff changeset
   169
         "xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)";
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   170
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   171
text{*\noindent
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   172
we may want to prove
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   173
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   174
10788
ea48dd8b0232 *** empty log message ***
nipkow
parents: 10654
diff changeset
   175
lemma "xor A (\<not>A)";
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   176
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   177
txt{*\noindent
11428
332347b9b942 tidying the index
paulson
parents: 11309
diff changeset
   178
Typically, we begin by unfolding some definitions:
332347b9b942 tidying the index
paulson
parents: 11309
diff changeset
   179
\indexbold{definitions!unfolding}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   180
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   181
10788
ea48dd8b0232 *** empty log message ***
nipkow
parents: 10654
diff changeset
   182
apply(simp only:xor_def);
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   183
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   184
txt{*\noindent
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   185
In this particular case, the resulting goal
10362
c6b197ccf1f1 *** empty log message ***
nipkow
parents: 10171
diff changeset
   186
@{subgoals[display,indent=0]}
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   187
can be proved by simplification. Thus we could have proved the lemma outright by
10788
ea48dd8b0232 *** empty log message ***
nipkow
parents: 10654
diff changeset
   188
*}(*<*)oops;lemma "xor A (\<not>A)";(*>*)
ea48dd8b0232 *** empty log message ***
nipkow
parents: 10654
diff changeset
   189
apply(simp add: xor_def)
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   190
(*<*)done(*>*)
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   191
text{*\noindent
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   192
Of course we can also unfold definitions in the middle of a proof.
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   193
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   194
\begin{warn}
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 10885
diff changeset
   195
  If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
6852682eaf16 *** empty log message ***
nipkow
parents: 10885
diff changeset
   196
  occurrences of $f$ with at least two arguments. This may be helpful for unfolding
6852682eaf16 *** empty log message ***
nipkow
parents: 10885
diff changeset
   197
  $f$ selectively, but it may also get in the way. Defining
6852682eaf16 *** empty log message ***
nipkow
parents: 10885
diff changeset
   198
  $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   199
\end{warn}
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12332
diff changeset
   200
f41e477576b9 *** empty log message ***
nipkow
parents: 12332
diff changeset
   201
There is also the special method \isa{unfold}\index{*unfold (method)|bold}
f41e477576b9 *** empty log message ***
nipkow
parents: 12332
diff changeset
   202
which merely unfolds
f41e477576b9 *** empty log message ***
nipkow
parents: 12332
diff changeset
   203
one or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}.
f41e477576b9 *** empty log message ***
nipkow
parents: 12332
diff changeset
   204
This is can be useful in situations where \isa{simp} does too much.
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   205
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   206
11214
3b3cc0cf533f *** empty log message ***
nipkow
parents: 11206
diff changeset
   207
subsection{*Simplifying {\tt\slshape let}-Expressions*}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   208
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   209
text{*\index{simplification!of \isa{let}-expressions}\index{*let expressions}%
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   210
Proving a goal containing \isa{let}-expressions almost invariably requires the
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   211
@{text"let"}-con\-structs to be expanded at some point. Since
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   212
@{text"let"}\ldots\isa{=}\ldots@{text"in"}{\ldots} is just syntactic sugar for
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   213
the predefined constant @{term"Let"}, expanding @{text"let"}-constructs
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   214
means rewriting with \tdx{Let_def}: *}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   215
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   216
lemma "(let xs = [] in xs@ys@xs) = ys";
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   217
apply(simp add: Let_def);
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   218
done
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   219
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   220
text{*
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   221
If, in a particular context, there is no danger of a combinatorial explosion
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   222
of nested @{text"let"}s, you could even simplify with @{thm[source]Let_def} by
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   223
default:
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   224
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   225
declare Let_def [simp]
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   226
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   227
subsection{*Conditional Simplification Rules*}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   228
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   229
text{*
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   230
\index{conditional simplification rules}%
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   231
So far all examples of rewrite rules were equations. The simplifier also
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   232
accepts \emph{conditional} equations, for example
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   233
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   234
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   235
lemma hd_Cons_tl[simp]: "xs \<noteq> []  \<Longrightarrow>  hd xs # tl xs = xs";
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   236
apply(case_tac xs, simp, simp);
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   237
done
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   238
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   239
text{*\noindent
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   240
Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   241
sequence of methods. Assuming that the simplification rule
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   242
@{term"(rev xs = []) = (xs = [])"}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   243
is present as well,
10795
9e888d60d3e5 minor edits to Chapters 1-3
paulson
parents: 10788
diff changeset
   244
the lemma below is proved by plain simplification:
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   245
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   246
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   247
lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   248
(*<*)
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   249
by(simp);
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   250
(*>*)
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   251
text{*\noindent
10795
9e888d60d3e5 minor edits to Chapters 1-3
paulson
parents: 10788
diff changeset
   252
The conditional equation @{thm[source]hd_Cons_tl} above
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   253
can simplify @{term"hd(rev xs) # tl(rev xs)"} to @{term"rev xs"}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   254
because the corresponding precondition @{term"rev xs ~= []"}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   255
simplifies to @{term"xs ~= []"}, which is exactly the local
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   256
assumption of the subgoal.
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   257
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   258
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   259
11214
3b3cc0cf533f *** empty log message ***
nipkow
parents: 11206
diff changeset
   260
subsection{*Automatic Case Splits*}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   261
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   262
text{*\label{sec:AutoCaseSplits}\indexbold{case splits}%
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   263
Goals containing @{text"if"}-expressions\index{*if expressions!splitting of}
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   264
are usually proved by case
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   265
distinction on the boolean condition.  Here is an example:
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   266
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   267
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   268
lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []";
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   269
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   270
txt{*\noindent
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   271
The goal can be split by a special method, \methdx{split}:
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   272
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   273
10654
458068404143 *** empty log message ***
nipkow
parents: 10362
diff changeset
   274
apply(split split_if)
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   275
10362
c6b197ccf1f1 *** empty log message ***
nipkow
parents: 10171
diff changeset
   276
txt{*\noindent
c6b197ccf1f1 *** empty log message ***
nipkow
parents: 10171
diff changeset
   277
@{subgoals[display,indent=0]}
11428
332347b9b942 tidying the index
paulson
parents: 11309
diff changeset
   278
where \tdx{split_if} is a theorem that expresses splitting of
10654
458068404143 *** empty log message ***
nipkow
parents: 10362
diff changeset
   279
@{text"if"}s. Because
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   280
splitting the @{text"if"}s is usually the right proof strategy, the
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   281
simplifier does it automatically.  Try \isacommand{apply}@{text"(simp)"}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   282
on the initial goal above.
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   283
11428
332347b9b942 tidying the index
paulson
parents: 11309
diff changeset
   284
This splitting idea generalizes from @{text"if"} to \sdx{case}.
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   285
Let us simplify a case analysis over lists:\index{*list.split (theorem)}
10654
458068404143 *** empty log message ***
nipkow
parents: 10362
diff changeset
   286
*}(*<*)by simp(*>*)
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   287
lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
10654
458068404143 *** empty log message ***
nipkow
parents: 10362
diff changeset
   288
apply(split list.split);
11309
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
   289
 
10362
c6b197ccf1f1 *** empty log message ***
nipkow
parents: 10171
diff changeset
   290
txt{*
c6b197ccf1f1 *** empty log message ***
nipkow
parents: 10171
diff changeset
   291
@{subgoals[display,indent=0]}
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   292
The simplifier does not split
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   293
@{text"case"}-expressions, as it does @{text"if"}-expressions, 
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   294
because with recursive datatypes it could lead to nontermination.
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   295
Instead, the simplifier has a modifier
11494
23a118849801 revisions and indexing
paulson
parents: 11458
diff changeset
   296
@{text split}\index{*split (modifier)} 
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   297
for adding splitting rules explicitly.  The
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   298
lemma above can be proved in one step by
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   299
*}
10362
c6b197ccf1f1 *** empty log message ***
nipkow
parents: 10171
diff changeset
   300
(*<*)oops;
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   301
lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   302
(*>*)
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   303
apply(simp split: list.split);
59d6633835fa *** empty log message ***
nipkow
parents: 9932
diff changeset
   304
(*<*)done(*>*)
10654
458068404143 *** empty log message ***
nipkow
parents: 10362
diff changeset
   305
text{*\noindent
458068404143 *** empty log message ***
nipkow
parents: 10362
diff changeset
   306
whereas \isacommand{apply}@{text"(simp)"} alone will not succeed.
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   307
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   308
Every datatype $t$ comes with a theorem
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   309
$t$@{text".split"} which can be declared to be a \bfindex{split rule} either
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   310
locally as above, or by giving it the \attrdx{split} attribute globally:
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   311
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   312
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   313
declare list.split [split]
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   314
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   315
text{*\noindent
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   316
The @{text"split"} attribute can be removed with the @{text"del"} modifier,
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   317
either locally
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   318
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   319
(*<*)
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   320
lemma "dummy=dummy";
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   321
(*>*)
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   322
apply(simp split del: split_if);
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   323
(*<*)
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   324
oops;
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   325
(*>*)
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   326
text{*\noindent
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   327
or globally:
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   328
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   329
declare list.split [split del]
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   330
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   331
text{*
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   332
Polished proofs typically perform splitting within @{text simp} rather than 
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   333
invoking the @{text split} method.  However, if a goal contains
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   334
several @{text if} and @{text case} expressions, 
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   335
the @{text split} method can be
10654
458068404143 *** empty log message ***
nipkow
parents: 10362
diff changeset
   336
helpful in selectively exploring the effects of splitting.
458068404143 *** empty log message ***
nipkow
parents: 10362
diff changeset
   337
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   338
The split rules shown above are intended to affect only the subgoal's
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   339
conclusion.  If you want to split an @{text"if"} or @{text"case"}-expression
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   340
in the assumptions, you have to apply \tdx{split_if_asm} or
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   341
$t$@{text".split_asm"}: *}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   342
10654
458068404143 *** empty log message ***
nipkow
parents: 10362
diff changeset
   343
lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []"
458068404143 *** empty log message ***
nipkow
parents: 10362
diff changeset
   344
apply(split split_if_asm)
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   345
10362
c6b197ccf1f1 *** empty log message ***
nipkow
parents: 10171
diff changeset
   346
txt{*\noindent
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   347
Unlike splitting the conclusion, this step creates two
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   348
separate subgoals, which here can be solved by @{text"simp_all"}:
10362
c6b197ccf1f1 *** empty log message ***
nipkow
parents: 10171
diff changeset
   349
@{subgoals[display,indent=0]}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   350
If you need to split both in the assumptions and the conclusion,
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   351
use $t$@{text".splits"} which subsumes $t$@{text".split"} and
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   352
$t$@{text".split_asm"}. Analogously, there is @{thm[source]if_splits}.
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   353
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   354
\begin{warn}
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   355
  The simplifier merely simplifies the condition of an 
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   356
  \isa{if}\index{*if expressions!simplification of} but not the
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   357
  \isa{then} or \isa{else} parts. The latter are simplified only after the
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   358
  condition reduces to \isa{True} or \isa{False}, or after splitting. The
11428
332347b9b942 tidying the index
paulson
parents: 11309
diff changeset
   359
  same is true for \sdx{case}-expressions: only the selector is
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   360
  simplified at first, until either the expression reduces to one of the
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   361
  cases or it is split.
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   362
\end{warn}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   363
*}
10362
c6b197ccf1f1 *** empty log message ***
nipkow
parents: 10171
diff changeset
   364
(*<*)
c6b197ccf1f1 *** empty log message ***
nipkow
parents: 10171
diff changeset
   365
by(simp_all)
c6b197ccf1f1 *** empty log message ***
nipkow
parents: 10171
diff changeset
   366
(*>*)
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   367
11214
3b3cc0cf533f *** empty log message ***
nipkow
parents: 11206
diff changeset
   368
subsection{*Tracing*}
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   369
text{*\indexbold{tracing the simplifier}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   370
Using the simplifier effectively may take a bit of experimentation.  Set the
11428
332347b9b942 tidying the index
paulson
parents: 11309
diff changeset
   371
\isa{trace_simp}\index{*trace_simp (flag)} flag\index{flags} 
332347b9b942 tidying the index
paulson
parents: 11309
diff changeset
   372
to get a better idea of what is going
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   373
on:
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   374
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   375
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   376
ML "set trace_simp";
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   377
lemma "rev [a] = []";
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   378
apply(simp);
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   379
(*<*)oops(*>*)
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   380
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   381
text{*\noindent
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   382
produces the trace
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   383
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   384
\begin{ttbox}\makeatother
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   385
Applying instance of rewrite rule:
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   386
rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   387
Rewriting:
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 10885
diff changeset
   388
rev [a] == rev [] @ [a]
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   389
Applying instance of rewrite rule:
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   390
rev [] == []
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   391
Rewriting:
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   392
rev [] == []
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   393
Applying instance of rewrite rule:
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   394
[] @ ?y == ?y
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   395
Rewriting:
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 10885
diff changeset
   396
[] @ [a] == [a]
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   397
Applying instance of rewrite rule:
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   398
?x3 \# ?t3 = ?t3 == False
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   399
Rewriting:
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 10885
diff changeset
   400
[a] = [] == False
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   401
\end{ttbox}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   402
11309
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
   403
The trace lists each rule being applied, both in its general form and the 
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
   404
instance being used.  For conditional rules, the trace lists the rule
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
   405
it is trying to rewrite and gives the result of attempting to prove
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
   406
each of the rule's conditions.  Many other hints about the simplifier's
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
   407
actions will appear.
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11215
diff changeset
   408
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   409
In more complicated cases, the trace can be quite lengthy.  Invocations of the
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   410
simplifier are often nested, for instance when solving conditions of rewrite
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11428
diff changeset
   411
rules.  Thus it is advisable to reset it:
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   412
*}
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   413
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   414
ML "reset trace_simp";
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   415
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   416
(*<*)
9922
wenzelm
parents:
diff changeset
   417
end
9932
5b6305cab436 *** empty log message ***
nipkow
parents: 9922
diff changeset
   418
(*>*)