1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
\DOC new_inductive_set
\TYPE {new_inductive_set : term -> thm * thm * thm}
\SYNOPSIS
Define a set or family of sets inductively.
\DESCRIBE
The function {new_inductive_set} is applied to a conjunction of ``rules'', each
of the form {!x1...xn. Pi ==> ti IN Sk}. This conjunction is interpreted as an
inductive definition of a family of sets {Sk} (however many appear in the
consequents of the rules). That is, the sets are defined to be the smallest
ones closed under the rules. The function {new_inductive_set} will convert this
into explicit definitions, define a new constant for each {Sk}, and return a
triple of theorems. The first one will be the ``rule'' theorem, which
essentially matches the input clauses except that the {Si} are now the new
constants; this simply says that the new sets are indeed closed under the
rules. The second theorem is an induction theorem, asserting that the sets are
the least ones closed under the rules. Finally, the cases theorem gives a case
analysis theorem showing how each set of values satisfying the set may be
composed.
\FAILURE
Fails if the clauses are malformed, if the constants are already in use, or if
there are unproven monotonicity hypotheses. See {new_inductive_definition} for
more detailed discussion in the similar case of indunctive relations.
\EXAMPLE
A classic example where we have mutual induction is the set of even and odd
numbers:
{
# 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:
{
# g `(!n. n IN odd_numbers ==> ODD(n)) /\
(!n. n IN even_numbers ==> EVEN(n))`;;
}
\noindent applying the induction theorem:
{
# e(MATCH_MP_TAC EO_INDUCT);;
val it : goalstack = 1 subgoal (1 total)
`EVEN 0 /\
(!n. EVEN n ==> ODD (SUC n)) /\
ODD 1 /\
(!n. ODD n ==> EVEN (SUC n))`
}
\noindent This is easily finished off by, for example:
{
# e(REWRITE_TAC[GSYM NOT_EVEN; EVEN; ARITH]);;
val it : goalstack = No subgoals
}
This function uses {new_inductive_relation} internally, and the documentation
for that function gives additional information and other relevant examples.
\SEEALSO
derive_strong_induction, new_inductive_definition,
prove_inductive_relations_exist, prove_monotonicity_hyps.
\ENDDOC
|
