measureInduct_on : term quotation -> tactic
STRUCTURE
SYNOPSIS
Perform complete induction with a supplied measure function.
DESCRIPTION
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
HOL  Kananaskis-13