28 step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}% |
28 step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}% |
29 \begin{isamarkuptext}% |
29 \begin{isamarkuptext}% |
30 An inductive definition consists of introduction rules. |
30 An inductive definition consists of introduction rules. |
31 |
31 |
32 \begin{isabelle}% |
32 \begin{isabelle}% |
33 \ \ \ \ \ n\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ Even{\isachardot}even% |
33 \ \ \ \ \ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even% |
34 \end{isabelle} |
34 \end{isabelle} |
35 \rulename{even.step} |
35 \rulename{even.step} |
36 |
36 |
37 \begin{isabelle}% |
37 \begin{isabelle}% |
38 \ \ \ \ \ {\isasymlbrakk}xa\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ P\ {\isadigit{0}}{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ P\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\isanewline |
38 \ \ \ \ \ {\isasymlbrakk}xa\ {\isasymin}\ even{\isacharsemicolon}\ P\ {\isadigit{0}}{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ P\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ xa% |
39 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ P\ xa% |
|
40 \end{isabelle} |
39 \end{isabelle} |
41 \rulename{even.induct} |
40 \rulename{even.induct} |
42 |
41 |
43 Attributes can be given to the introduction rules. Here both rules are |
42 Attributes can be given to the introduction rules. Here both rules are |
44 specified as \isa{intro!} |
43 specified as \isa{intro!} |
58 \ {\isacharparenleft}induct{\isacharunderscore}tac\ k{\isacharparenright}% |
57 \ {\isacharparenleft}induct{\isacharunderscore}tac\ k{\isacharparenright}% |
59 \begin{isamarkuptxt}% |
58 \begin{isamarkuptxt}% |
60 The first step is induction on the natural number \isa{k}, which leaves |
59 The first step is induction on the natural number \isa{k}, which leaves |
61 two subgoals: |
60 two subgoals: |
62 \begin{isabelle}% |
61 \begin{isabelle}% |
63 \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ Even{\isachardot}even\isanewline |
62 \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ even\isanewline |
64 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ {\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ Even{\isachardot}even% |
63 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ even% |
65 \end{isabelle} |
64 \end{isabelle} |
66 Here \isa{auto} simplifies both subgoals so that they match the introduction |
65 Here \isa{auto} simplifies both subgoals so that they match the introduction |
67 rules, which then are applied automatically.% |
66 rules, which then are applied automatically.% |
68 \end{isamarkuptxt}% |
67 \end{isamarkuptxt}% |
69 \isamarkuptrue% |
68 \isamarkuptrue% |
117 \isacommand{apply}\isamarkupfalse% |
116 \isacommand{apply}\isamarkupfalse% |
118 \ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}% |
117 \ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}% |
119 \begin{isamarkuptxt}% |
118 \begin{isamarkuptxt}% |
120 \begin{isabelle}% |
119 \begin{isabelle}% |
121 \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline |
120 \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline |
122 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% |
121 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% |
123 \end{isabelle}% |
122 \end{isabelle}% |
124 \end{isamarkuptxt}% |
123 \end{isamarkuptxt}% |
125 \isamarkuptrue% |
124 \isamarkuptrue% |
126 \isacommand{apply}\isamarkupfalse% |
125 \isacommand{apply}\isamarkupfalse% |
127 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}% |
126 \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}% |
128 \begin{isamarkuptxt}% |
127 \begin{isamarkuptxt}% |
129 \begin{isabelle}% |
128 \begin{isabelle}% |
130 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ {\isasymexists}k{\isachardot}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}k{\isachardot}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k% |
129 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isasymexists}k{\isachardot}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}k{\isachardot}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k% |
131 \end{isabelle}% |
130 \end{isabelle}% |
132 \end{isamarkuptxt}% |
131 \end{isamarkuptxt}% |
133 \isamarkuptrue% |
132 \isamarkuptrue% |
134 \isacommand{apply}\isamarkupfalse% |
133 \isacommand{apply}\isamarkupfalse% |
135 \ clarify% |
134 \ clarify% |
136 \begin{isamarkuptxt}% |
135 \begin{isamarkuptxt}% |
137 \begin{isabelle}% |
136 \begin{isabelle}% |
138 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ k{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ {\isasymexists}ka{\isachardot}\ Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ ka% |
137 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ k{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isasymexists}ka{\isachardot}\ Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ ka% |
139 \end{isabelle}% |
138 \end{isabelle}% |
140 \end{isamarkuptxt}% |
139 \end{isamarkuptxt}% |
141 \isamarkuptrue% |
140 \isamarkuptrue% |
142 \isacommand{apply}\isamarkupfalse% |
141 \isacommand{apply}\isamarkupfalse% |
143 \ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}Suc\ k{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ simp{\isacharparenright}\isanewline |
142 \ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}Suc\ k{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharcomma}\ simp{\isacharparenright}\isanewline |
185 \isatagproof |
184 \isatagproof |
186 \isacommand{apply}\isamarkupfalse% |
185 \isacommand{apply}\isamarkupfalse% |
187 \ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}% |
186 \ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}% |
188 \begin{isamarkuptxt}% |
187 \begin{isamarkuptxt}% |
189 \begin{isabelle}% |
188 \begin{isabelle}% |
190 \ {\isadigit{1}}{\isachardot}\ n\ {\isasymin}\ Even{\isachardot}even\isanewline |
189 \ {\isadigit{1}}{\isachardot}\ n\ {\isasymin}\ even\isanewline |
191 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}na{\isachardot}\ {\isasymlbrakk}na\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ n\ {\isasymin}\ Even{\isachardot}even{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ Even{\isachardot}even% |
190 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}na{\isachardot}\ {\isasymlbrakk}na\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even% |
192 \end{isabelle}% |
191 \end{isabelle}% |
193 \end{isamarkuptxt}% |
192 \end{isamarkuptxt}% |
194 \isamarkuptrue% |
193 \isamarkuptrue% |
195 \isacommand{oops}\isamarkupfalse% |
194 \isacommand{oops}\isamarkupfalse% |
196 % |
195 % |
215 \isatagproof |
214 \isatagproof |
216 \isacommand{apply}\isamarkupfalse% |
215 \isacommand{apply}\isamarkupfalse% |
217 \ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}% |
216 \ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}% |
218 \begin{isamarkuptxt}% |
217 \begin{isamarkuptxt}% |
219 \begin{isabelle}% |
218 \begin{isabelle}% |
220 \ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ Even{\isachardot}even\isanewline |
219 \ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even\isanewline |
221 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ n\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ Even{\isachardot}even{\isasymrbrakk}\isanewline |
220 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even% |
222 \isaindent{\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ }{\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ Even{\isachardot}even% |
|
223 \end{isabelle}% |
221 \end{isabelle}% |
224 \end{isamarkuptxt}% |
222 \end{isamarkuptxt}% |
225 \isamarkuptrue% |
223 \isamarkuptrue% |
226 \isacommand{apply}\isamarkupfalse% |
224 \isacommand{apply}\isamarkupfalse% |
227 \ auto\isanewline |
225 \ auto\isanewline |