|
1 \begin{isabelle}% |
|
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}% |
|
12 \isacommand{constdefs}~exor~::~{"}bool~{\isasymRightarrow}~bool~{\isasymRightarrow}~bool{"}\isanewline |
|
13 ~~~~~~~~~{"}exor~A~B~{\isasymequiv}~(A~{\isasymand}~{\isasymnot}B)~{\isasymor}~({\isasymnot}A~{\isasymand}~B){"}% |
|
14 \begin{isamarkuptext}% |
|
15 \noindent |
|
16 we may want to prove% |
|
17 \end{isamarkuptext}% |
|
18 \isacommand{lemma}~{"}exor~A~({\isasymnot}A){"}% |
|
19 \begin{isamarkuptxt}% |
|
20 \noindent |
|
21 There is a special method for \emph{unfolding} definitions, which we need to |
|
22 get started:\indexbold{*unfold}\indexbold{definition!unfolding}% |
|
23 \end{isamarkuptxt}% |
|
24 \isacommand{apply}(unfold~exor\_def)% |
|
25 \begin{isamarkuptxt}% |
|
26 \noindent |
|
27 It unfolds the given list of definitions (here merely one) in all subgoals: |
|
28 \begin{isabellepar}% |
|
29 ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A% |
|
30 \end{isabellepar}% |
|
31 The resulting goal can be proved by simplification. |
|
32 |
|
33 In case we want to expand a definition in the middle of a proof, we can |
|
34 simply include it locally:% |
|
35 \end{isamarkuptxt}% |
|
36 \isacommand{apply}(simp~add:~exor\_def)% |
|
37 \begin{isamarkuptext}% |
|
38 \noindent |
|
39 In fact, this one command proves the above lemma directly. |
|
40 |
|
41 You should normally not turn a definition permanently into a simplification |
|
42 rule because this defeats the whole purpose of an abbreviation.% |
|
43 \end{isamarkuptext}% |
|
44 \end{isabelle}% |