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