1 (*<*) |
|
2 theory def_rewr = Main:; |
|
3 |
|
4 (*>*)text{*\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 *} |
|
12 |
|
13 constdefs exor :: "bool \\<Rightarrow> bool \\<Rightarrow> bool" |
|
14 "exor A B \\<equiv> (A \\<and> \\<not>B) \\<or> (\\<not>A \\<and> B)"; |
|
15 |
|
16 text{*\noindent |
|
17 we may want to prove |
|
18 *} |
|
19 |
|
20 lemma "exor A (\\<not>A)"; |
|
21 |
|
22 txt{*\noindent |
|
23 Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to |
|
24 get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding} |
|
25 *} |
|
26 |
|
27 apply(simp only:exor_def); |
|
28 |
|
29 txt{*\noindent |
|
30 In this particular case, the resulting goal |
|
31 \begin{isabelle} |
|
32 ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A% |
|
33 \end{isabelle} |
|
34 can be proved by simplification. Thus we could have proved the lemma outright |
|
35 *}(*<*)oops;lemma "exor A (\\<not>A)";(*>*) |
|
36 by(simp add: exor_def) |
|
37 |
|
38 text{*\noindent |
|
39 Of course we can also unfold definitions in the middle of a proof. |
|
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 *} |
|
44 (*<*)end(*>*) |
|