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
89
90
91
92
93
94
95
96
97
98
99
100
101
|
\DOC INDUCT_THEN
\TYPE {INDUCT_THEN : (thm -> thm_tactic -> tactic)}
\SYNOPSIS
Structural induction tactic for automatically-defined concrete types.
\KEYWORDS
theorem-tactic, induction.
\DESCRIBE
The function {INDUCT_THEN} implements structural induction tactics for
arbitrary concrete recursive types of the kind definable by {define_type}. The
first argument to {INDUCT_THEN} is a structural induction theorem for the
concrete type in question. This theorem must have the form of an induction
theorem of the kind returned by {prove_induction_thm}. When applied to such a
theorem, the function {INDUCT_THEN} constructs specialized tactic for
doing structural induction on the concrete type in question.
The second argument to {INDUCT_THEN} is a function that determines what is be
done with the induction hypotheses in the goal-directed proof by structural
induction. Suppose that {th} is a structural induction theorem for a concrete
data type {ty}, and that {A ?- !x.P} is a universally-quantified goal in which
the variable {x} ranges over values of type {ty}. If the type {ty} has {n}
constructors {C1}, ..., {Cn} and `{Ci(vs)}' represents a (curried) application
of the {i}th constructor to a sequence of variables, then if {ttac} is a
function that maps the induction hypotheses {hypi} of the {i}th subgoal
to the tactic:
{
A ?- P[Ci(vs)/x]
====================== MAP_EVERY ttac hypi
A1 ?- Gi
}
\noindent then {INDUCT_THEN th ttac} is an induction tactic that decomposes
the goal {A ?- !x.P} into a set of {n} subgoals, one for each constructor,
as follows:
{
A ?- !x.P
================================ INDUCT_THEN th ttac
A1 ?- G1 ... An ?- Gn
}
\noindent The resulting subgoals correspond to the cases in a structural
induction on the variable {x} of type {ty}, with induction hypotheses treated
as determined by {ttac}.
\FAILURE
{INDUCT_THEN th ttac g} fails if {th} is not a structural induction theorem of
the form returned by {prove_induction_thm}, or if the goal does not have the
form {A ?- !x:ty.P} where {ty} is the type for which {th} is the induction
theorem, or if {ttac} fails for any subgoal in the induction.
\EXAMPLE
The built-in structural induction theorem for lists is:
{
|- !P. P[] /\ (!t. P t ==> (!h. P(CONS h t))) ==> (!l. P l)
}
\noindent When {INDUCT_THEN} is applied to this theorem, it constructs
and returns a specialized induction tactic (parameterized by a theorem-tactic)
for doing induction on lists:
{
#let LIST_INDUCT_THEN = INDUCT_THEN list_INDUCT;;
LIST_INDUCT_THEN = - : (thm_tactic -> tactic)
}
\noindent The resulting function, when supplied with the thm-tactic
{ASSUME_TAC}, returns a tactic that decomposes a goal {?- !l.P[l]} into the
base case {?- P[NIL]} and a step case {P[l] ?- !h. P[CONS h l]}, where the
induction hypothesis {P[l]} in the step case has been put on the assumption
list. That is, the tactic:
{
LIST_INDUCT_THEN ASSUME_TAC
}
\noindent does structural induction on lists, putting any induction hypotheses
that arise onto the assumption list:
{
A ?- !l. P
=======================================================
A |- P[NIL/l] A u {{P[l'/l]}} ?- !h. P[(CONS h l')/l]
}
\noindent Likewise {LIST_INDUCT_THEN STRIP_ASSUME_TAC} will also do induction
on lists, but will strip induction hypotheses apart before adding them to the
assumptions (this may be useful if P is a conjunction or a disjunction, or is
existentially quantified). By contrast, the tactic:
{
LIST_INDUCT_THEN MP_TAC
}
\noindent will decompose the goal as follows:
{
A ?- !l. P
=====================================================
A |- P[NIL/l] A ?- P[l'/l] ==> !h. P[CONS h l'/l]
}
\noindent That is, the induction hypothesis becomes the antecedent of an
implication expressing the step case in the induction, rather than an
assumption of the step-case subgoal.
\SEEALSO
define_type, new_recursive_definition, prove_cases_thm,
prove_constructors_distinct, prove_constructors_one_one, prove_induction_thm,
prove_rec_fn_exists.
\ENDDOC
|
