如何在Isabelle中定义含非固定大小word类型的datatype？

Isabelle的datatype命令本身不支持(overloaded)修饰符，而's word类型依赖len_of('s)类型类约束，普通datatype定义无法处理这种带开放依赖的类型。要实现需求，需要手动通过typedef (overloaded)来模拟datatype的结构，步骤如下：

1. 导入Word库并定义重载类型 #

首先导入HOL-Library.Word，然后用typedef (overloaded)定义底层类型，基于sum类型承载两种构造器的内容：

theory Foo_Word_Datatype
imports HOL-Library.Word
begin

typedef (overloaded) 's Foo = "UNIV :: ('s word + 's word) set" ..

或者也可以通过启用上下文配置typedef_overloaded来替代(overloaded)修饰符：

context notes [[typedef_overloaded]] begin
typedef 's Foo = "UNIV :: ('s word + 's word) set" ..
end

2. 定义构造器 #

手动实现Foo1和Foo2构造器，对应sum类型的Inl和Inr：

definition Foo1 :: "'s word ⇒ 's Foo" where
  "Foo1 x = Abs_Foo (Inl x)"

definition Foo2 :: "'s word ⇒ 's Foo" where
  "Foo2 x = Abs_Foo (Inr x)"

3. 定义case分析函数 #

实现类似datatype的case分析逻辑，方便模式匹配：

definition case_Foo :: "('s word ⇒ 'a) ⇒ ('s word ⇒ 'a) ⇒ 's Foo ⇒ 'a" where
  "case_Foo f g x = (case Rep_Foo x of Inl y ⇒ f y | Inr y ⇒ g y)"

4. 注册case语法（可选） #

为了让Isabelle支持原生的case ... of模式匹配语法，需要注册case分析规则：

setup {*
  Sign.add_path (Long_Name.base_name "Foo1") #>
  Sign.add_path (Long_Name.base_name "Foo2") #>
  Context.theory_map (
    Datatype_Case.add_case "Foo"
      (fn c => fn _ => fn _ =>
         case c of
           "Foo1" => SOME ("case_Foo", fn f => "λx. " ^ f ^ " x")
         | "Foo2" => SOME ("case_Foo", fn f => "λx. " ^ f ^ " x")
         | _ => NONE)
  )
*}

5. 添加基础定理（可选） #

为构造器和case分析添加基本的正确性定理，方便后续推理：

lemma Foo1_inj: "Foo1 x = Foo1 y ⟷ x = y"
  unfolding Foo1_def by (simp add: Abs_Foo_inject)

lemma Foo2_inj: "Foo2 x = Foo2 y ⟷ x = y"
  unfolding Foo2_def by (simp add: Abs_Foo_inject)

lemma Foo1_neq_Foo2: "Foo1 x ≠ Foo2 y"
  unfolding Foo1_def Foo2_def by (simp add: Abs_Foo_inject sum.distinct)

lemma case_Foo_Foo1: "case_Foo f g (Foo1 x) = f x"
  unfolding case_Foo_def Foo1_def by simp

lemma case_Foo_Foo2: "case_Foo f g (Foo2 x) = g x"
  unfolding case_Foo_def Foo2_def by simp

完成以上步骤后，你就可以像使用普通datatype一样使用's Foo，支持任意满足len_of约束的s类型，比如32 word、64 word等。

内容的提问来源于stack exchange，提问作者Proof-By-Sledgehammer