54 \end{isamarkuptext}% |
54 \end{isamarkuptext}% |
55 \isamarkuptrue% |
55 \isamarkuptrue% |
56 % |
56 % |
57 \begin{isamarkuptext}% |
57 \begin{isamarkuptext}% |
58 It proves $\mathit{formula}_0 \Longrightarrow \mathit{formula}_{n+1}$ |
58 It proves $\mathit{formula}_0 \Longrightarrow \mathit{formula}_{n+1}$ |
59 (provided provided each proof step succeeds). |
59 (provided each proof step succeeds). |
60 The intermediate \isacom{have} statements are merely stepping stones |
60 The intermediate \isacom{have} statements are merely stepping stones |
61 on the way towards the \isacom{show} statement that proves the actual |
61 on the way towards the \isacom{show} statement that proves the actual |
62 goal. In more detail, this is the Isar core syntax: |
62 goal. In more detail, this is the Isar core syntax: |
63 \medskip |
63 \medskip |
64 |
64 |
113 writing \isa{f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}, whole sublists by \isa{f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2D}{\isacharminus}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}}. |
113 writing \isa{f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}, whole sublists by \isa{f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2D}{\isacharminus}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}}. |
114 |
114 |
115 |
115 |
116 \section{Isar by example} |
116 \section{Isar by example} |
117 |
117 |
118 We show a number of proofs of Cantors theorem that a function from a set to |
118 We show a number of proofs of Cantor's theorem that a function from a set to |
119 its powerset cannot be surjective, illustrating various features of Isar. The |
119 its powerset cannot be surjective, illustrating various features of Isar. The |
120 constant \isa{surj} is predefined.% |
120 constant \isa{surj} is predefined.% |
121 \end{isamarkuptext}% |
121 \end{isamarkuptext}% |
122 \isamarkuptrue% |
122 \isamarkuptrue% |
123 \isacommand{lemma}\isamarkupfalse% |
123 \isacommand{lemma}\isamarkupfalse% |
325 command. It is the null method that does nothing to the goal. Leaving it out |
325 command. It is the null method that does nothing to the goal. Leaving it out |
326 would ask Isabelle to try some suitable introduction rule on the goal \isa{False}---but there is no suitable introduction rule and \isacom{proof} |
326 would ask Isabelle to try some suitable introduction rule on the goal \isa{False}---but there is no suitable introduction rule and \isacom{proof} |
327 would fail. |
327 would fail. |
328 \end{warn} |
328 \end{warn} |
329 |
329 |
330 Stating a lemmas with \isacom{assumes}-\isacom{shows} implicitly introduces the |
330 Stating a lemma with \isacom{assumes}-\isacom{shows} implicitly introduces the |
331 name \isa{assms} that stands for the list of all assumptions. You can refer |
331 name \isa{assms} that stands for the list of all assumptions. You can refer |
332 to individual assumptions by \isa{assms{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}}, \isa{assms{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} etc, |
332 to individual assumptions by \isa{assms{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}}, \isa{assms{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} etc, |
333 thus obviating the need to name them individually. |
333 thus obviating the need to name them individually. |
334 |
334 |
335 \section{Proof patterns} |
335 \section{Proof patterns} |
597 \end{minipage} |
597 \end{minipage} |
598 \end{tabular} |
598 \end{tabular} |
599 \medskip |
599 \medskip |
600 \begin{isamarkuptext}% |
600 \begin{isamarkuptext}% |
601 In the proof of \noquotes{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}}, |
601 In the proof of \noquotes{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}}, |
602 the step \isacom{fix}~\isa{x} introduces a locale fixed variable \isa{x} |
602 the step \isacom{fix}~\isa{x} introduces a locally fixed variable \isa{x} |
603 into the subproof, the proverbial ``arbitrary but fixed value''. |
603 into the subproof, the proverbial ``arbitrary but fixed value''. |
604 Instead of \isa{x} we could have chosen any name in the subproof. |
604 Instead of \isa{x} we could have chosen any name in the subproof. |
605 In the proof of \noquotes{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}}, |
605 In the proof of \noquotes{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}}, |
606 \isa{witness} is some arbitrary |
606 \isa{witness} is some arbitrary |
607 term for which we can prove that it satisfies \isa{P}. |
607 term for which we can prove that it satisfies \isa{P}. |
837 \end{warn} |
837 \end{warn} |
838 |
838 |
839 Although abbreviations shorten the text, the reader needs to remember what |
839 Although abbreviations shorten the text, the reader needs to remember what |
840 they stand for. Similarly for names of facts. Names like \isa{{\isadigit{1}}}, \isa{{\isadigit{2}}} |
840 they stand for. Similarly for names of facts. Names like \isa{{\isadigit{1}}}, \isa{{\isadigit{2}}} |
841 and \isa{{\isadigit{3}}} are not helpful and should only be used in short proofs. For |
841 and \isa{{\isadigit{3}}} are not helpful and should only be used in short proofs. For |
842 longer proof, descriptive names are better. But look at this example: |
842 longer proofs, descriptive names are better. But look at this example: |
843 \begin{quote} |
843 \begin{quote} |
844 \isacom{have} \ \isa{x{\isaliteral{5F}{\isacharunderscore}}gr{\isaliteral{5F}{\isacharunderscore}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}}\\ |
844 \isacom{have} \ \isa{x{\isaliteral{5F}{\isacharunderscore}}gr{\isaliteral{5F}{\isacharunderscore}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}}\\ |
845 $\vdots$\\ |
845 $\vdots$\\ |
846 \isacom{from} \isa{x{\isaliteral{5F}{\isacharunderscore}}gr{\isaliteral{5F}{\isacharunderscore}}{\isadigit{0}}} \dots |
846 \isacom{from} \isa{x{\isaliteral{5F}{\isacharunderscore}}gr{\isaliteral{5F}{\isacharunderscore}}{\isadigit{0}}} \dots |
847 \end{quote} |
847 \end{quote} |
1071 Each case can be written in a more compact form by means of the \isacom{case} |
1071 Each case can be written in a more compact form by means of the \isacom{case} |
1072 command: |
1072 command: |
1073 \begin{quote} |
1073 \begin{quote} |
1074 \isacom{case} \isa{{\isaliteral{28}{\isacharparenleft}}C\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} |
1074 \isacom{case} \isa{{\isaliteral{28}{\isacharparenleft}}C\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} |
1075 \end{quote} |
1075 \end{quote} |
1076 This is equivalent to the explicit \isacom{fix}-\isacom{assumen} line |
1076 This is equivalent to the explicit \isacom{fix}-\isacom{assume} line |
1077 but also gives the assumption \isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3D}{\isacharequal}}\ C\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} a name: \isa{C}, |
1077 but also gives the assumption \isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{3D}{\isacharequal}}\ C\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} a name: \isa{C}, |
1078 like the constructor. |
1078 like the constructor. |
1079 Here is the \isacom{case} version of the proof above:% |
1079 Here is the \isacom{case} version of the proof above:% |
1080 \end{isamarkuptext}% |
1080 \end{isamarkuptext}% |
1081 \isamarkuptrue% |
1081 \isamarkuptrue% |
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 |
1604 of the case; there is no fine grained naming schema like for induction. |
1604 of the case; there is no fine grained naming schema like for induction. |
1605 |
1605 |
1606 Sometimes some rules could not have beed used to derive the given fact |
1606 Sometimes some rules could not have been used to derive the given fact |
1607 because constructors clash. As an extreme example consider |
1607 because constructors clash. As an extreme example consider |
1608 rule inversion applied to \isa{ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}}: neither rule \isa{ev{\isadigit{0}}} nor |
1608 rule inversion applied to \isa{ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}}: neither rule \isa{ev{\isadigit{0}}} nor |
1609 rule \isa{evSS} can yield \isa{ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}} because \isa{Suc\ {\isadigit{0}}} unifies |
1609 rule \isa{evSS} can yield \isa{ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}} because \isa{Suc\ {\isadigit{0}}} unifies |
1610 neither with \isa{{\isadigit{0}}} nor with \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}}. Impossible cases do not |
1610 neither with \isa{{\isadigit{0}}} nor with \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}}. Impossible cases do not |
1611 have to be proved. Hence we can prove anything from \isa{ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}}:% |
1611 have to be proved. Hence we can prove anything from \isa{ev\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}}:% |