8745
|
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
|
9689
|
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}
|
8745
|
25 |
*}
|
|
26 |
|
9689
|
27 |
apply(simp only:exor_def);
|
8745
|
28 |
|
|
29 |
txt{*\noindent
|
9689
|
30 |
In this particular case, the resulting goal
|
8745
|
31 |
\begin{isabellepar}%
|
|
32 |
~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
|
|
33 |
\end{isabellepar}%
|
9689
|
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)
|
8745
|
37 |
|
|
38 |
text{*\noindent
|
9689
|
39 |
Of course we can also unfold definitions in the middle of a proof.
|
8745
|
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(*>*)
|