completeInduct_on : term quotation -> tactic
STRUCTURE
SYNOPSIS
Perform complete induction.
DESCRIPTION
If q parses into a well-typed term M, an invocation completeInduct_on q begins a proof by complete (also known as ‘course-of-values’) induction on M. The term M should occur free in the current goal.
FAILURE
If M does not parse into a term or does not occur free in the current goal.
EXAMPLE
Suppose we wish to prove that every number not equal to one has a prime factor:
   !n. ~(n = 1) ==> ?p. prime p /\ p divides n
A natural way to prove this is by complete induction. Invoking completeInduct_on `n` yields the goal
      { !m. m < n ==> ~(m = 1) ==> ?p. prime p /\ p divides m }
      ?-
      ~(n = 1) ==> ?p. prime p /\ p divides n
SEEALSO
HOL  Kananaskis-14