我研究了Coq及其相关类型。我对这一切只有最模糊的想法，但是现在我想将一个矢量作为a bool list，其中矢量的长度是该类型的一部分。

（这个问题可能是另一个问题的前身。在下一个问题中，如果我提出这个问题，我将问我在使用typedef以下方法时是否可以弥补损失的钱。）

（对于这个问题，这个问题在底部）

这是我想要的类型的要求：

• 它必须使用bool list，以便我可以直接或间接在列表上进行模式匹配和递归，并且
• 向量的长度必须在类型中指定。

这是我所拥有的：

typedef bitvec_4 = "{bl::bool list. length bl = 4}"
  by(auto, metis Ex_list_of_length)

列表的长度必须是类型的一部分，这一点很重要，因为我想将类型与a一起使用definition，其中所有列表的大小都相同，例如以下示例所示：

definition two_bv4_to_bv4 :: "bitvec_4 => bitvec_4 => bitvec_4" where
  "two_bv4_to_bv4 x y = x"

在一个定理中，我不需要指定列表的长度。类型类最终将以某种方式发挥作用，但是正如我所说的，我想在类型定义中指定长度。

定义和类型签名。我在哪里放n = 4!! （具有最小幽默价值的技术笑话）

现在，我尝试用typedef这样的概括，其中长度是一个变量：

typedef bitvec_n = "{(bl::bool list, n::nat). length bl = n}"
  by(auto)

不好 在下一个这样的定义中，我的类型不能保证所有列表的长度都相同：

definition two_bvn_to_bvn :: "bitvec_n => bitvec_n => bitvec_n" where
  "two_bvn_to_bvn x y = x"

有问题吗 （我想是这样）

我已经对bitvec_4上述类型进行了一些试验。如果我没有遇到大障碍，我可能会尝试充分利用它们。

我可以为2的幂定义上述类型，最多1024个位，以及反映它们共同属性的类型类。

但是，还有更好的方法吗？我认为，使用一定要简单明了bool list。

更新（了解实际的答案）

根据Manuel的回答，我在这里包括一个独立的理论。

它主要是Manuel资料的重复，但是最后，我的功能swap_bl和swap_2bv以及最终使用value展示了我试图完成的工作的最终结果。我的评论强调了我心中的问题，也许我的最终应用程序表明了为什么我没有将其HOL/Word作为解决方案。

对于typedef类型，要进行间接模式匹配，类似于使用swap_bl和2 bitvec，我将Abs和Rep函数一起用作反函数。正如曼努埃尔指出的那样，一个问题是我可以输入错误长度的Abs函数a bool list，并且不会出错。另一个大问题是由于使用该Abs函数而导致抽象冲突。

这些问题，想知道我是否可以恢复value对我的typedef类型的使用，这将是我下一个问题的一部分，但此处已回答了所有问题。

theory i141210ac__testing_out_manuels_answer
imports Main "~~/src/HOL/Library/Numeral_Type"
begin
(*Basic type definition.*)
  typedef ('n::finite) bitvec = "{bs :: bool list. length bs = CARD('n)}"
    morphisms bitvec_to_list Abs_bitvec
    by (simp add: Ex_list_of_length)

  setup_lifting type_definition_bitvec

  lift_definition nth :: "('n::finite) bitvec => nat => bool" (infixl "$" 90) 
    is List.nth .

(*Can't use 'value' yet for 'nth', or I get an abstraction violation.*)
  term "(Abs_bitvec [True,False] :: 2 bitvec) $ 1"

(*Truncate or fill the list: needed to set things up for 'value'.*)
  definition set_length :: "nat => bool list => bool list" where
    "set_length n xs = (if length xs < n 
                        then xs @ replicate (n - length xs) False 
                        else take n xs)"              
  lemma length_set_length [simp]: "length (set_length n xs) = n"
    unfolding set_length_def by auto

  definition list_to_bitvec :: "bool list => ('n::finite) bitvec" where
    "list_to_bitvec xs = Abs_bitvec (set_length CARD('n) xs)"
  
(*Finishing the magic needed for 'value'.*)
  lemma list_to_bitvec_code [code abstract]:
    "bitvec_to_list (list_to_bitvec xs :: ('n::finite) bitvec) 
      = set_length CARD('n) xs"
    unfolding list_to_bitvec_def by(simp add: Abs_bitvec_inverse)
  
(*Inverses for lists of length 2: no abstraction violations.*)
  value "list_to_bitvec (bitvec_to_list x) :: 2 bitvec"
  value "bitvec_to_list (list_to_bitvec x :: 2 bitvec)"

(*The magic now kicks in for 'value' and 'nth'. Understanding is optional.*)
  value "(list_to_bitvec [True,False] :: 2 bitvec) $ 1" (*OUTPUT: False.*)

(*For my use, the primary context of all this is pattern matching on lists.
  I can't pattern match on a 'typedef' type directly with 'fun', because 
  it's not a 'datatype'. I do it indirectly.*)
  
fun swap_bl :: "bool list => bool list" where
  "swap_bl [a,b] = [b,a]"
 |"swap_bl _ = undefined"
 
definition swap_2bv :: "2 bitvec => 2 bitvec" where
  "swap_2bv bv = list_to_bitvec (swap_bl (bitvec_to_list bv))"

value "swap_2bv (list_to_bitvec [a,b] :: 2 bitvec)" (*
  OUTPUT: "Abs_bitvec [b, a]" :: "2 bitvec" *)

(*Whether that's all a good idea, that's about the future, but it appears the 
  hard work, recovering the use of 'value', along with generalizing length,
  has been done by Manuel, and the authors of Numeral_Type and its imports.*)
end