38 Using \commdx{inductive\protect\_set}, we declare the constant \isa{even} to be |
38 Using \commdx{inductive\protect\_set}, we declare the constant \isa{even} to be |
39 a set of natural numbers with the desired properties.% |
39 a set of natural numbers with the desired properties.% |
40 \end{isamarkuptext}% |
40 \end{isamarkuptext}% |
41 \isamarkuptrue% |
41 \isamarkuptrue% |
42 \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% |
42 \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% |
43 \ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline |
43 \ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
44 \isakeyword{where}\isanewline |
44 zero{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
45 \ \ zero{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline |
45 step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}% |
46 {\isacharbar}\ step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}% |
|
47 \begin{isamarkuptext}% |
46 \begin{isamarkuptext}% |
48 An inductive definition consists of introduction rules. The first one |
47 An inductive definition consists of introduction rules. The first one |
49 above states that 0 is even; the second states that if $n$ is even, then so |
48 above states that 0 is even; the second states that if $n$ is even, then so |
50 is~$n+2$. Given this declaration, Isabelle generates a fixed point |
49 is~$n+2$. Given this declaration, Isabelle generates a fixed point |
51 definition for \isa{even} and proves theorems about it, |
50 definition for \isa{even} and proves theorems about it, |