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
|
\DOC derive_nonschematic_inductive_relations
\TYPE {derive_nonschematic_inductive_relations : term -> thm}
\SYNOPSIS
Deduce inductive definitions properties from an explicit assignment.
\DESCRIBE
Given a set of clauses as given to {new_inductive_definitions}, the call
{derive_nonschematic_inductive_relations} will introduce explicit equational
constraints (``definitions'', though only assumptions of the theorem, not
actually constant definitions) that allow it to deduce those clauses. It will
in general have additional `monotonicity' hypotheses, but these may be
removable by {prove_monotonicity_hyps}. None of the arguments are treated as
schematic.
\FAILURE
Fails if the format of the clauses is wrong.
\EXAMPLE
Here we try one of the classic examples of a mutually inductive definition,
defining odd-ness and even-ness of natural numbers:
{
# (prove_monotonicity_hyps o derive_nonschematic_inductive_relations)
`even(0) /\ odd(1) /\
(!n. even(n) ==> odd(n + 1)) /\ (!n. odd(n) ==> even(n + 1))`;;
val it : thm =
odd =
(\a0. !odd' even'.
(!a0. a0 = 1 \/ (?n. a0 = n + 1 /\ even' n) ==> odd' a0) /\
(!a1. a1 = 0 \/ (?n. a1 = n + 1 /\ odd' n) ==> even' a1)
==> odd' a0),
even =
(\a1. !odd' even'.
(!a0. a0 = 1 \/ (?n. a0 = n + 1 /\ even' n) ==> odd' a0) /\
(!a1. a1 = 0 \/ (?n. a1 = n + 1 /\ odd' n) ==> even' a1)
==> even' a1)
|- (even 0 /\
odd 1 /\
(!n. even n ==> odd (n + 1)) /\
(!n. odd n ==> even (n + 1))) /\
(!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)) /\
(!a0. odd a0 <=> a0 = 1 \/ (?n. a0 = n + 1 /\ even n)) /\
(!a1. even a1 <=> a1 = 0 \/ (?n. a1 = n + 1 /\ odd n))
}
\noindent Note that the final theorem has two assumptions that one can think of
as the appropriate explicit definitions of these relations, and the conclusion
gives the rule, induction and cases theorems.
\COMMENTS
Normally, use {prove_inductive_relations_exist} or {new_inductive_definition}.
This function is only needed for a very fine level of control.
\SEEALSO
new_inductive_definition, prove_inductive_relations_exist,
prove_monotonicity_hyps.
\ENDDOC
|
