Как использовать 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 word на четыре 8 word, эта функция, кажется идеальным.

И лемма word_rcat (word_rsplit w) = w полезна для меня.

Так что мне нужно знать, как использовать word_rsplit, как указать 'a = 32 и 'b = 8.

Answer 1

Чтобы получить вариант word_rsplit для конкретных типов слов, вы можете просто дать явные ограничения типа. Например, ваш пример, где вы хотите разделить 32 word на несколько 8 word с, может быть определена следующим образом:

word_rsplit :: 32 word => 8 word list" 

Пример:

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

производит

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