261 \isacom{from} \ \textit{facts} \ (\isacom{have}$\mid$\isacom{show}) \ \textit{prop}\\ |
261 \isacom{from} \ \textit{facts} \ (\isacom{have}$\mid$\isacom{show}) \ \textit{prop}\\ |
262 \isacom{with} \ \textit{facts} &=& \isacom{from} \ \textit{facts} \isa{this} |
262 \isacom{with} \ \textit{facts} &=& \isacom{from} \ \textit{facts} \isa{this} |
263 \end{tabular} |
263 \end{tabular} |
264 \medskip |
264 \medskip |
265 |
265 |
266 \noindent The \isacom{using} idiom de-emphasises the used facts by moving them |
266 \noindent The \isacom{using} idiom de-emphasizes the used facts by moving them |
267 behind the proposition. |
267 behind the proposition. |
268 |
268 |
269 \subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}} |
269 \subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}} |
270 |
270 |
271 Lemmas can also be stated in a more structured fashion. To demonstrate this |
271 Lemmas can also be stated in a more structured fashion. To demonstrate this |
337 We show a number of important basic proof patterns. Many of them arise from |
337 We show a number of important basic proof patterns. Many of them arise from |
338 the rules of natural deduction that are applied by \isacom{proof} by |
338 the rules of natural deduction that are applied by \isacom{proof} by |
339 default. The patterns are phrased in terms of \isacom{show} but work for |
339 default. The patterns are phrased in terms of \isacom{show} but work for |
340 \isacom{have} and \isacom{lemma}, too. |
340 \isacom{have} and \isacom{lemma}, too. |
341 |
341 |
342 We start with two forms of \concept{case distinction}: |
342 We start with two forms of \concept{case analysis}: |
343 starting from a formula \isa{P} we have the two cases \isa{P} and |
343 starting from a formula \isa{P} we have the two cases \isa{P} and |
344 \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P}, and starting from a fact \isa{P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q} |
344 \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P}, and starting from a fact \isa{P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q} |
345 we have the two cases \isa{P} and \isa{Q}:% |
345 we have the two cases \isa{P} and \isa{Q}:% |
346 \end{isamarkuptext}% |
346 \end{isamarkuptext}% |
347 \isamarkuptrue% |
347 \isamarkuptrue% |
944 |
944 |
945 \subsection{Raw proof blocks} |
945 \subsection{Raw proof blocks} |
946 |
946 |
947 Sometimes one would like to prove some lemma locally within a proof. |
947 Sometimes one would like to prove some lemma locally within a proof. |
948 A lemma that shares the current context of assumptions but that |
948 A lemma that shares the current context of assumptions but that |
949 has its own assumptions and is generalised over its locally fixed |
949 has its own assumptions and is generalized over its locally fixed |
950 variables at the end. This is what a \concept{raw proof block} does: |
950 variables at the end. This is what a \concept{raw proof block} does: |
951 \begin{quote} |
951 \begin{quote} |
952 \isa{{\isaliteral{7B}{\isacharbraceleft}}} \isacom{fix} \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n}\\ |
952 \isa{{\isaliteral{7B}{\isacharbraceleft}}} \isacom{fix} \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n}\\ |
953 \mbox{}\ \ \ \isacom{assume} \isa{A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub m}\\ |
953 \mbox{}\ \ \ \isacom{assume} \isa{A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub m}\\ |
954 \mbox{}\ \ \ $\vdots$\\ |
954 \mbox{}\ \ \ $\vdots$\\ |
1014 \end{quote} |
1014 \end{quote} |
1015 This introduces a new name \isa{name} that refers to \isa{this}, |
1015 This introduces a new name \isa{name} that refers to \isa{this}, |
1016 the fact just proved, in this case the preceding block. In general, |
1016 the fact just proved, in this case the preceding block. In general, |
1017 \isacom{note} introduces a new name for one or more facts. |
1017 \isacom{note} introduces a new name for one or more facts. |
1018 |
1018 |
1019 \section{Case distinction and induction} |
1019 \section{Case analysis and induction} |
1020 |
1020 |
1021 \subsection{Datatype case distinction} |
1021 \subsection{Datatype case analysis} |
1022 |
1022 |
1023 We have seen case distinction on formulas. Now we want to distinguish |
1023 We have seen case analysis on formulas. Now we want to distinguish |
1024 which form some term takes: is it \isa{{\isadigit{0}}} or of the form \isa{Suc\ n}, |
1024 which form some term takes: is it \isa{{\isadigit{0}}} or of the form \isa{Suc\ n}, |
1025 is it \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} or of the form \isa{x\ {\isaliteral{23}{\isacharhash}}\ xs}, etc. Here is a typical example |
1025 is it \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} or of the form \isa{x\ {\isaliteral{23}{\isacharhash}}\ xs}, etc. Here is a typical example |
1026 proof by case distinction on the form of \isa{xs}:% |
1026 proof by case analysis on the form of \isa{xs}:% |
1027 \end{isamarkuptext}% |
1027 \end{isamarkuptext}% |
1028 \isamarkuptrue% |
1028 \isamarkuptrue% |
1029 \isacommand{lemma}\isamarkupfalse% |
1029 \isacommand{lemma}\isamarkupfalse% |
1030 \ {\isaliteral{22}{\isachardoublequoteopen}}length{\isaliteral{28}{\isacharparenleft}}tl\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ length\ xs\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
1030 \ {\isaliteral{22}{\isachardoublequoteopen}}length{\isaliteral{28}{\isacharparenleft}}tl\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ length\ xs\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
1031 % |
1031 % |
1121 (\isa{{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}}) is equal to \mbox{\isa{n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}}}. |
1121 (\isa{{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}}) is equal to \mbox{\isa{n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}}}. |
1122 Never mind the details, just focus on the pattern:% |
1122 Never mind the details, just focus on the pattern:% |
1123 \end{isamarkuptext}% |
1123 \end{isamarkuptext}% |
1124 \isamarkuptrue% |
1124 \isamarkuptrue% |
1125 \isacommand{lemma}\isamarkupfalse% |
1125 \isacommand{lemma}\isamarkupfalse% |
1126 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{is}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline |
1126 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
1127 % |
1127 % |
1128 \isadelimproof |
1128 \isadelimproof |
1129 % |
1129 % |
1130 \endisadelimproof |
1130 \endisadelimproof |
1131 % |
1131 % |
1139 \isanewline |
1139 \isanewline |
1140 \ \ \isacommand{fix}\isamarkupfalse% |
1140 \ \ \isacommand{fix}\isamarkupfalse% |
1141 \ n\ \isacommand{assume}\isamarkupfalse% |
1141 \ n\ \isacommand{assume}\isamarkupfalse% |
1142 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
1142 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
1143 \ \ \isacommand{thus}\isamarkupfalse% |
1143 \ \ \isacommand{thus}\isamarkupfalse% |
1144 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}Suc\ n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
1144 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{7B}{\isacharbraceleft}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}Suc\ n{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% |
1145 \ simp\isanewline |
1145 \ simp\isanewline |
1146 \isacommand{qed}\isamarkupfalse% |
1146 \isacommand{qed}\isamarkupfalse% |
1147 % |
1147 % |
1148 \endisatagproof |
1148 \endisatagproof |
1149 {\isafoldproof}% |
1149 {\isafoldproof}% |
1546 This is where the indexing of fact lists comes in handy, e.g.\ |
1546 This is where the indexing of fact lists comes in handy, e.g.\ |
1547 \isa{name{\isaliteral{2E}{\isachardot}}IH{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} or \isa{name{\isaliteral{2E}{\isachardot}}prems{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2D}{\isacharminus}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}. |
1547 \isa{name{\isaliteral{2E}{\isachardot}}IH{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} or \isa{name{\isaliteral{2E}{\isachardot}}prems{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2D}{\isacharminus}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}. |
1548 |
1548 |
1549 \subsection{Rule inversion} |
1549 \subsection{Rule inversion} |
1550 |
1550 |
1551 Rule inversion is case distinction on which rule could have been used to |
1551 Rule inversion is case analysis of which rule could have been used to |
1552 derive some fact. The name \concept{rule inversion} emphasizes that we are |
1552 derive some fact. The name \concept{rule inversion} emphasizes that we are |
1553 reasoning backwards: by which rules could some given fact have been proved? |
1553 reasoning backwards: by which rules could some given fact have been proved? |
1554 For the inductive definition of \isa{ev}, rule inversion can be summarized |
1554 For the inductive definition of \isa{ev}, rule inversion can be summarized |
1555 like this: |
1555 like this: |
1556 \begin{isabelle}% |
1556 \begin{isabelle}% |
1557 ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}k{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ ev\ k{\isaliteral{29}{\isacharparenright}}% |
1557 ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}k{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ ev\ k{\isaliteral{29}{\isacharparenright}}% |
1558 \end{isabelle} |
1558 \end{isabelle} |
1559 The realisation in Isabelle is a case distinction. |
1559 The realisation in Isabelle is a case analysis. |
1560 A simple example is the proof that \isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}. We |
1560 A simple example is the proof that \isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}. We |
1561 already went through the details informally in \autoref{sec:Logic:even}. This |
1561 already went through the details informally in \autoref{sec:Logic:even}. This |
1562 is the Isar proof:% |
1562 is the Isar proof:% |
1563 \end{isamarkuptext}% |
1563 \end{isamarkuptext}% |
1564 \isamarkuptrue% |
1564 \isamarkuptrue% |
1593 \isadelimproof |
1593 \isadelimproof |
1594 % |
1594 % |
1595 \endisadelimproof |
1595 \endisadelimproof |
1596 % |
1596 % |
1597 \begin{isamarkuptext}% |
1597 \begin{isamarkuptext}% |
1598 The key point here is that a case distinction over some inductively |
1598 The key point here is that a case analysis over some inductively |
1599 defined predicate is triggered by piping the given fact |
1599 defined predicate is triggered by piping the given fact |
1600 (here: \isacom{from}~\isa{this}) into a proof by \isa{cases}. |
1600 (here: \isacom{from}~\isa{this}) into a proof by \isa{cases}. |
1601 Let us examine the assumptions available in each case. In case \isa{ev{\isadigit{0}}} |
1601 Let us examine the assumptions available in each case. In case \isa{ev{\isadigit{0}}} |
1602 we have \isa{n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} and in case \isa{evSS} we have \isa{n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ k{\isaliteral{29}{\isacharparenright}}} |
1602 we have \isa{n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} and in case \isa{evSS} we have \isa{n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ k{\isaliteral{29}{\isacharparenright}}} |
1603 and \isa{ev\ k}. In each case the assumptions are available under the name |
1603 and \isa{ev\ k}. In each case the assumptions are available under the name |