Prim_rec.INDUCT

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:

      A  ?- P[Ci(vs)/x]
   ======================  MAP_EVERY ttac hypi
         A1 ?- Gi

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

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)

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:

   - val LIST_INDUCT_THEN = INDUCT_THEN listTheory.list_INDUCT;

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

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]

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

will decompose the goal as follows:

                      A ?- !l. P
   =====================================================
    A |- P[NIL/l]   A ?- P[l'/l] ==> !h. P[CONS h l'/l]

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

new_recursive_definition, prove_cases_thm, prove_constructors_distinct, prove_constructors_one_one, prove_induction_thm, prove_rec_fn_exists