18 *} |
18 *} |
19 |
19 |
20 lemma "exor A (\\<not>A)"; |
20 lemma "exor A (\\<not>A)"; |
21 |
21 |
22 txt{*\noindent |
22 txt{*\noindent |
23 There is a special method for \emph{unfolding} definitions, which we need to |
23 Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to |
24 get started:\indexbold{*unfold}\indexbold{definition!unfolding} |
24 get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding} |
25 *} |
25 *} |
26 |
26 |
27 apply(unfold exor_def); |
27 apply(simp only:exor_def); |
28 |
28 |
29 txt{*\noindent |
29 txt{*\noindent |
30 It unfolds the given list of definitions (here merely one) in all subgoals: |
30 In this particular case, the resulting goal |
31 \begin{isabellepar}% |
31 \begin{isabellepar}% |
32 ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A% |
32 ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A% |
33 \end{isabellepar}% |
33 \end{isabellepar}% |
34 The resulting goal can be proved by simplification. |
34 can be proved by simplification. Thus we could have proved the lemma outright |
35 |
35 *}(*<*)oops;lemma "exor A (\\<not>A)";(*>*) |
36 In case we want to expand a definition in the middle of a proof, we can |
36 by(simp add: exor_def) |
37 simply include it locally:*}(*<*)oops;lemma "exor A (\\<not>A)";(*>*) |
|
38 apply(simp add: exor_def);(*<*).(*>*) |
|
39 |
37 |
40 text{*\noindent |
38 text{*\noindent |
41 In fact, this one command proves the above lemma directly. |
39 Of course we can also unfold definitions in the middle of a proof. |
42 |
40 |
43 You should normally not turn a definition permanently into a simplification |
41 You should normally not turn a definition permanently into a simplification |
44 rule because this defeats the whole purpose of an abbreviation. |
42 rule because this defeats the whole purpose of an abbreviation. |
45 *} |
43 *} |
46 (*<*)end(*>*) |
44 (*<*)end(*>*) |