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))"

我想将 a 拆分32 word为四个8 word，这个功能似乎很完美。

引理word_rcat (word_rsplit w) = w对我也很有用。

所以我需要知道如何使用word_rsplit，如何指定'a= 32 和'b= 8。

Answer 1

要获得word_rsplit特定单词类型的变体，您只需给出明确的类型约束即可。例如，您要将 a 拆分32 word为多个8 words 的示例可以指定如下：

word_rsplit :: 32 word => 8 word list"

例子：

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

生产

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