equal
deleted
inserted
replaced
125 % |
125 % |
126 \begin{isamarkuptext}% |
126 \begin{isamarkuptext}% |
127 We start with an inductive proof where both cases are proved automatically:% |
127 We start with an inductive proof where both cases are proved automatically:% |
128 \end{isamarkuptext}% |
128 \end{isamarkuptext}% |
129 \isamarkuptrue% |
129 \isamarkuptrue% |
130 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
130 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat{\isasymle}n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
131 \isamarkupfalse% |
131 \isamarkupfalse% |
132 \isacommand{by}\ {\isacharparenleft}induct\ n{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% |
132 \isacommand{by}\ {\isacharparenleft}induct\ n{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% |
133 % |
133 % |
134 \begin{isamarkuptext}% |
134 \begin{isamarkuptext}% |
135 \noindent The constraint \isa{{\isacharcolon}{\isacharcolon}nat} is needed because all of |
135 \noindent The constraint \isa{{\isacharcolon}{\isacharcolon}nat} is needed because all of |
138 If we want to expose more of the structure of the |
138 If we want to expose more of the structure of the |
139 proof, we can use pattern matching to avoid having to repeat the goal |
139 proof, we can use pattern matching to avoid having to repeat the goal |
140 statement:% |
140 statement:% |
141 \end{isamarkuptext}% |
141 \end{isamarkuptext}% |
142 \isamarkuptrue% |
142 \isamarkuptrue% |
143 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline |
143 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat{\isasymle}n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline |
144 \isamarkupfalse% |
144 \isamarkupfalse% |
145 \isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline |
145 \isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline |
146 \ \ \isamarkupfalse% |
146 \ \ \isamarkupfalse% |
147 \isacommand{show}\ {\isachardoublequote}{\isacharquery}P\ {\isadigit{0}}{\isachardoublequote}\ \isamarkupfalse% |
147 \isacommand{show}\ {\isachardoublequote}{\isacharquery}P\ {\isadigit{0}}{\isachardoublequote}\ \isamarkupfalse% |
148 \isacommand{by}\ simp\isanewline |
148 \isacommand{by}\ simp\isanewline |
161 \noindent We could refine this further to show more of the equational |
161 \noindent We could refine this further to show more of the equational |
162 proof. Instead we explore the same avenue as for case distinctions: |
162 proof. Instead we explore the same avenue as for case distinctions: |
163 introducing context via the \isakeyword{case} command:% |
163 introducing context via the \isakeyword{case} command:% |
164 \end{isamarkuptext}% |
164 \end{isamarkuptext}% |
165 \isamarkuptrue% |
165 \isamarkuptrue% |
166 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
166 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isasymle}\ n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
167 \isamarkupfalse% |
167 \isamarkupfalse% |
168 \isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline |
168 \isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline |
169 \ \ \isamarkupfalse% |
169 \ \ \isamarkupfalse% |
170 \isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse% |
170 \isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse% |
171 \isacommand{show}\ {\isacharquery}case\ \isamarkupfalse% |
171 \isacommand{show}\ {\isacharquery}case\ \isamarkupfalse% |