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
|
\DOC derive_strong_induction
\TYPE {derive_strong_induction : thm * thm -> thm}
\SYNOPSIS
Derive stronger induction theorem from inductive definition.
\DESCRIBE
The function {derive_strong_induction} is applied to a pair of theorems as
returned by {new_inductive_definition}. The first theorem is the `rule'
theorem, the second the `induction' theorem; the `case' theorem returned by
{new_inductive_definition} is not needed. It returns a stronger induction
theorem where instances of each inductive predicate occurring in hypotheses
is conjoined with the corresponding inductive relation too.
\FAILURE
Fails if the two input theorems are not of the correct form for rule and
induction theorems returned by {new_inductive_definition}.
\EXAMPLE
A simple example of a mutually inductive definition is:
{
# 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))
}
The stronger induction theorem can be derived as follows. Note that it is
similar in form to {eo_INDUCT} but has stronger hypotheses for two of the
conjuncts in the antecedent.
{
# derive_strong_induction(eo_RULES,eo_INDUCT);;
val it : thm =
|- !odd' even'.
even' 0 /\
odd' 1 /\
(!n. even n /\ even' n ==> odd' (n + 1)) /\
(!n. odd n /\ odd' n ==> even' (n + 1))
==> (!a0. odd a0 ==> odd' a0) /\ (!a1. even a1 ==> even' a1)
}
\COMMENTS
This function needs to discharge monotonicity theorems as part of its internal
working, just as {new_inductive_definition} does when the inductive definition
is made. Usually this is automatic and the user doesn't see it, but in
difficult cases, the theorem returned may have additional monotonicity
hypotheses that are unproven. In such cases, you can either try to prove them
manually or extend {monotonicity_theorems} to make the built-in monotonicity
prover more powerful.
\SEEALSO
new_inductive_definition, prove_inductive_relations_exist,
prove_monotonicity_hyps.
\ENDDOC
|
