isabelle - word_rsplitの使い方

Question

と呼ばれる関数がありword_rsplitます~~/src/HOL/Word/Word.thy。

definition word_rsplit :: "'a :: len0 word => 'b :: len word list" where
  "word_rsplit w = 
  map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"

32 wordaを fourに分割したいのですが8 word、この機能は完璧のようです。

そしてレンマword_rcat (word_rsplit w) = wは私にとっても役に立ちます。

なので、 の使い方、 = 32 と= 8のword_rsplit指定方法を知る必要があります。'a'b

Answer 1

特定の単語型のバリアントを取得するにはword_rsplit、明示的な型制約を与えるだけです。たとえば、 a32 wordを複数8 wordの s に分割する例は、次のように指定できます。

word_rsplit :: 32 word => 8 word list"

例：

value "(word_rsplit :: 32 word ⇒ 8 word list) 1024"

生産する

"[0, 0, 4, 0]"
  :: "8 word list"