# let eo_RULES,eo_INDUCT, eo_CASES = new_inductive_definition
`even(0) /\ odd(1) /\
(!n. even(n) ==> odd(n + 1)) /\
(!n. odd(n) ==> even(n + 1))`;;
val eo_RULES : thm =
|- even 0 /\
odd 1 /\
(!n. even n ==> odd (n + 1)) /\
(!n. odd n ==> even (n + 1))
val eo_INDUCT : thm =
|- !odd' even'.
even' 0 /\
odd' 1 /\
(!n. even' n ==> odd' (n + 1)) /\
(!n. odd' n ==> even' (n + 1))
==> (!a0. odd a0 ==> odd' a0) /\ (!a1. even a1 ==> even' a1)
val eo_CASES : thm =
|- (!a0. odd a0 <=> a0 = 1 \/ (?n. a0 = n + 1 /\ even n)) /\
(!a1. even a1 <=> a1 = 0 \/ (?n. a1 = n + 1 /\ odd n))
Note that the `rules' theorem corresponds exactly to the input, and says that
indeed the relations do satisfy the rules. The `induction' theorem says that
the relations 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:
# parse_as_infix("-->",(13,"right"));;
val it : unit = ()
# let form_tybij = define_type "form = False | --> form form";;
val form_tybij : thm * thm =
(|- !P. P False /\ (!a0 a1. P a0 /\ P a1 ==> P (a0 --> a1)) ==> (!x. P x),
|- !f0 f1.
?fn. fn False = f0 /\
(!a0 a1. fn (a0 --> a1) = f1 a0 a1 (fn a0) (fn a1)))
and making an inductive definition of the provability relation:
# parse_as_infix("|--",(11,"right"));;
val it : unit = ()
# let provable_RULES,provable_INDUCT,provable_CASES = new_inductive_definition
`(!p. p IN A ==> A |-- p) /\
(!p q. A |-- p --> (q --> p)) /\
(!p q r. A |-- (p --> q --> r) --> (p --> q) --> (p --> r)) /\
(!p. A |-- ((p --> False) --> False) --> p) /\
(!p q. A |-- p --> q /\ A |-- p ==> A |-- q)`;;
val provable_RULES : thm =
|- !A. (!p. p IN A ==> A |-- p) /\
(!p q. A |-- p --> q --> p) /\
(!p q r. A |-- (p --> q --> r) --> (p --> q) --> p --> r) /\
(!p. A |-- ((p --> False) --> False) --> p) /\
(!p q. A |-- p --> q /\ A |-- p ==> A |-- q)
val provable_INDUCT : thm =
|- !A |--'.
(!p. p IN A ==> |--' p) /\
(!p q. |--' (p --> q --> p)) /\
(!p q r. |--' ((p --> q --> r) --> (p --> q) --> p --> r)) /\
(!p. |--' (((p --> False) --> False) --> p)) /\
(!p q. |--' (p --> q) /\ |--' p ==> |--' q)
==> (!a. A |-- a ==> |--' a)
val provable_CASES : thm =
|- !A a.
A |-- a <=>
a IN A \/
(?p q. a = p --> q --> p) \/
(?p q r. a = (p --> q --> r) --> (p --> q) --> p --> r) \/
(?p. a = ((p --> False) --> False) --> p) \/
(?p. A |-- p --> a /\ A |-- p)
Note that