9721
|
1 |
\begin{isabelle}%
|
8749
|
2 |
%
|
|
3 |
\begin{isamarkuptext}%
|
|
4 |
\noindent Constant definitions (\S\ref{sec:ConstDefinitions}) can
|
|
5 |
be used as simplification rules, but by default they are not. Hence the
|
|
6 |
simplifier does not expand them automatically, just as it should be:
|
|
7 |
definitions are introduced for the purpose of abbreviating complex
|
|
8 |
concepts. Of course we need to expand the definitions initially to derive
|
|
9 |
enough lemmas that characterize the concept sufficiently for us to forget the
|
|
10 |
original definition. For example, given%
|
|
11 |
\end{isamarkuptext}%
|
9673
|
12 |
\isacommand{constdefs}\ exor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
|
|
13 |
\ \ \ \ \ \ \ \ \ {\isachardoublequote}exor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}%
|
8749
|
14 |
\begin{isamarkuptext}%
|
|
15 |
\noindent
|
|
16 |
we may want to prove%
|
|
17 |
\end{isamarkuptext}%
|
9673
|
18 |
\isacommand{lemma}\ {\isachardoublequote}exor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}%
|
8749
|
19 |
\begin{isamarkuptxt}%
|
|
20 |
\noindent
|
9698
|
21 |
Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
|
|
22 |
get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}%
|
8749
|
23 |
\end{isamarkuptxt}%
|
9698
|
24 |
\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}exor{\isacharunderscore}def{\isacharparenright}%
|
8749
|
25 |
\begin{isamarkuptxt}%
|
|
26 |
\noindent
|
9698
|
27 |
In this particular case, the resulting goal
|
8749
|
28 |
\begin{isabellepar}%
|
|
29 |
~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
|
|
30 |
\end{isabellepar}%
|
9698
|
31 |
can be proved by simplification. Thus we could have proved the lemma outright%
|
8749
|
32 |
\end{isamarkuptxt}%
|
9698
|
33 |
\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%
|
8749
|
34 |
\begin{isamarkuptext}%
|
|
35 |
\noindent
|
9698
|
36 |
Of course we can also unfold definitions in the middle of a proof.
|
8749
|
37 |
|
|
38 |
You should normally not turn a definition permanently into a simplification
|
|
39 |
rule because this defeats the whole purpose of an abbreviation.%
|
|
40 |
\end{isamarkuptext}%
|
9721
|
41 |
\end{isabelle}%
|
9145
|
42 |
%%% Local Variables:
|
|
43 |
%%% mode: latex
|
|
44 |
%%% TeX-master: "root"
|
|
45 |
%%% End:
|