INDUCT_THEN : (thm -> thm_tactic -> tactic)

- STRUCTURE
- SYNOPSIS
- Structural induction tactic for automatically-defined concrete types.
- DESCRIPTION
- 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 ith constructor to a sequence of variables, then if ttac is a function that maps the induction hypotheses hypi of the ith subgoal to the tactic:

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 ?- P[Ci(vs)/x] ====================== MAP_EVERY ttac hypi A1 ?- Gi

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.A ?- !x.P ================================ INDUCT_THEN th ttac A1 ?- G1 ... An ?- Gn

- 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: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:
|- !P. P[] /\ (!t. P t ==> (!h. P(CONS h t))) ==> (!l. P l)

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:- val LIST_INDUCT_THEN = INDUCT_THEN listTheory.list_INDUCT;

does structural induction on lists, putting any induction hypotheses that arise onto the assumption list:LIST_INDUCT_THEN ASSUME_TAC

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:A ?- !l. P ======================================================= A |- P[NIL/l] A u {P[l'/l]} ?- !h. P[(CONS h l')/l]

will decompose the goal as follows:LIST_INDUCT_THEN MP_TAC

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.A ?- !l. P ===================================================== A |- P[NIL/l] A ?- P[l'/l] ==> !h. P[CONS h l'/l]

- SEEALSO

HOL Kananaskis-14