如何使用word_rsplit

Question

~~/src/HOL/Word/Word.thy中有一個稱爲word_rsplit的功能。

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 S，可以作如下規定：

word_rsplit :: 32 word => 8 word list" 

例子：

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

產生

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