7 definitions are introduced for the purpose of abbreviating complex |
7 definitions are introduced for the purpose of abbreviating complex |
8 concepts. Of course we need to expand the definitions initially to derive |
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 |
9 enough lemmas that characterize the concept sufficiently for us to forget the |
10 original definition. For example, given% |
10 original definition. For example, given% |
11 \end{isamarkuptext}% |
11 \end{isamarkuptext}% |
12 \isacommand{constdefs}~exor~::~{"}bool~{\isasymRightarrow}~bool~{\isasymRightarrow}~bool{"}\isanewline |
12 \isacommand{constdefs}\ exor\ ::\ {"}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{"}\isanewline |
13 ~~~~~~~~~{"}exor~A~B~{\isasymequiv}~(A~{\isasymand}~{\isasymnot}B)~{\isasymor}~({\isasymnot}A~{\isasymand}~B){"}% |
13 \ \ \ \ \ \ \ \ \ {"}exor\ A\ B\ {\isasymequiv}\ (A\ {\isasymand}\ {\isasymnot}B)\ {\isasymor}\ ({\isasymnot}A\ {\isasymand}\ B){"}% |
14 \begin{isamarkuptext}% |
14 \begin{isamarkuptext}% |
15 \noindent |
15 \noindent |
16 we may want to prove% |
16 we may want to prove% |
17 \end{isamarkuptext}% |
17 \end{isamarkuptext}% |
18 \isacommand{lemma}~{"}exor~A~({\isasymnot}A){"}% |
18 \isacommand{lemma}\ {"}exor\ A\ ({\isasymnot}A){"}% |
19 \begin{isamarkuptxt}% |
19 \begin{isamarkuptxt}% |
20 \noindent |
20 \noindent |
21 There is a special method for \emph{unfolding} definitions, which we need to |
21 There is a special method for \emph{unfolding} definitions, which we need to |
22 get started:\indexbold{*unfold}\indexbold{definition!unfolding}% |
22 get started:\indexbold{*unfold}\indexbold{definition!unfolding}% |
23 \end{isamarkuptxt}% |
23 \end{isamarkuptxt}% |
24 \isacommand{apply}(unfold~exor\_def)% |
24 \isacommand{apply}(unfold\ exor\_def)% |
25 \begin{isamarkuptxt}% |
25 \begin{isamarkuptxt}% |
26 \noindent |
26 \noindent |
27 It unfolds the given list of definitions (here merely one) in all subgoals: |
27 It unfolds the given list of definitions (here merely one) in all subgoals: |
28 \begin{isabellepar}% |
28 \begin{isabellepar}% |
29 ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A% |
29 ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A% |
31 The resulting goal can be proved by simplification. |
31 The resulting goal can be proved by simplification. |
32 |
32 |
33 In case we want to expand a definition in the middle of a proof, we can |
33 In case we want to expand a definition in the middle of a proof, we can |
34 simply include it locally:% |
34 simply include it locally:% |
35 \end{isamarkuptxt}% |
35 \end{isamarkuptxt}% |
36 \isacommand{apply}(simp~add:~exor\_def)% |
36 \isacommand{apply}(simp\ add:\ exor\_def)% |
37 \begin{isamarkuptext}% |
37 \begin{isamarkuptext}% |
38 \noindent |
38 \noindent |
39 In fact, this one command proves the above lemma directly. |
39 In fact, this one command proves the above lemma directly. |
40 |
40 |
41 You should normally not turn a definition permanently into a simplification |
41 You should normally not turn a definition permanently into a simplification |