----------------------------------------------------------------------
measureInduct_on                                             (bossLib)
----------------------------------------------------------------------
measureInduct_on : term quotation -> tactic

SYNOPSIS
Perform complete induction with a supplied measure function.

KEYWORDS
induction, measure.

DESCRIBE
If {q} parses into a well-typed term {M N}, an invocation
{measureInduct_on q} begins a proof by induction, using {M} to map
{N} into a number. The term {N} should occur free in the current goal.

FAILURE
If {M N} does not parse into a term or if {N} does not occur free in the
current goal.

EXAMPLE
Suppose we wish to prove {P (APPEND l1 l2)} by induction on the length of
{l1}. Then {measureInduct_on `LENGTH ll`} yields the goal

   { !y. LENGTH y < LENGTH l1 ==> P (APPEND y l2) } ?- P (APPEND l1 l2)


SEEALSO
bossLib.completeInduct_on, bossLib.Induct, bossLib.Induct_on.

----------------------------------------------------------------------