# let EO_RULES, EO_INDUCT, EO_CASES = new_inductive_set
`0 IN even_numbers /\
(!n. n IN even_numbers ==> SUC n IN odd_numbers) /\
1 IN odd_numbers /\
(!n. n IN odd_numbers ==> SUC n IN even_numbers)`;;
val EO_RULES : thm =
|- 0 IN even_numbers /\
(!n. n IN even_numbers ==> SUC n IN odd_numbers) /\
1 IN odd_numbers /\
(!n. n IN odd_numbers ==> SUC n IN even_numbers)
val EO_INDUCT : thm =
|- !odd_numbers' even_numbers'.
even_numbers' 0 /\
(!n. even_numbers' n ==> odd_numbers' (SUC n)) /\
odd_numbers' 1 /\
(!n. odd_numbers' n ==> even_numbers' (SUC n))
==> (!a0. a0 IN odd_numbers ==> odd_numbers' a0) /\
(!a1. a1 IN even_numbers ==> even_numbers' a1)
val EO_CASES : thm =
|- (!a0. a0 IN odd_numbers <=>
(?n. a0 = SUC n /\ n IN even_numbers) \/ a0 = 1) /\
(!a1. a1 IN even_numbers <=>
a1 = 0 \/ (?n. a1 = SUC n /\ n IN odd_numbers))
Note that the `rules' theorem corresponds exactly to the input, and says that
indeed the sets do satisfy the rules. The `induction' theorem says that
the sets are the minimal ones satisfying the rules. You can use this to
prove properties by induction, e.g. the relationship with the pre-defined
concepts of odd and even: