Induct_word

wordsLib.Induct_word : tactic

Initiate an induction on the value of a word.

The tactic Induct_word makes use of the tactic bossLib.recInduct wordsTheory.WORD_INDUCT.

Example

Given the goal

?- !w:word8. P w

one can apply Induct_word to begin a proof by induction.

> e wordsLib.Induct_word
Exception- OK..
HOL_ERR (at Induction.ndest_forall: too few quantified variables in goal) raised

This results in the base and step cases of the induction as new goals.

?- P 0w

[SUC n < 256, P (n2w n)] ?- P (n2w (SUC n))

See also

bossLib.recInduct