Induct_word : tactic

- STRUCTURE
- SYNOPSIS
- Initiate an induction on the value of a word.
- DESCRIPTION
- The tactic Induct_word makes use of the tactic bossLib.recInduct wordsTheory.WORD_INDUCT.
- EXAMPLE
- Given the goalone can apply Induct_word to begin a proof by induction.
?- !w:word8. P w

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

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

- SEEALSO

HOL Kananaskis-14