equal
deleted
inserted
replaced
18 text {* |
18 text {* |
19 Using \commdx{inductive\protect\_set}, we declare the constant @{text even} to be |
19 Using \commdx{inductive\protect\_set}, we declare the constant @{text even} to be |
20 a set of natural numbers with the desired properties. |
20 a set of natural numbers with the desired properties. |
21 *} |
21 *} |
22 |
22 |
23 inductive_set even :: "nat set" |
23 inductive_set even :: "nat set" where |
24 where |
24 zero[intro!]: "0 \<in> even" | |
25 zero[intro!]: "0 \<in> even" |
25 step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even" |
26 | step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even" |
|
27 |
26 |
28 text {* |
27 text {* |
29 An inductive definition consists of introduction rules. The first one |
28 An inductive definition consists of introduction rules. The first one |
30 above states that 0 is even; the second states that if $n$ is even, then so |
29 above states that 0 is even; the second states that if $n$ is even, then so |
31 is~$n+2$. Given this declaration, Isabelle generates a fixed point |
30 is~$n+2$. Given this declaration, Isabelle generates a fixed point |