如何在Isabelle中定义满足约束规则的合法aset类型？

方法1：使用谓词定义合法性约束 #

由于type_synonym只是现有类型的别名，无法直接添加约束，最直接的方式是定义一个谓词来描述合法aset需满足的条件：

datatype akind = k1 | k2 | k3
record apair =
  kind :: akind
  val :: nat

type_synonym aset = "apair set"

(* 定义合法aset的谓词 *)
definition is_valid_aset :: "aset ⇒ bool" where
  "is_valid_aset s = (
    finite s ∧                  (* 约束1：集合有限 *)
    s ≠ {} ∧                    (* 约束2：非空 *)
    inj_on kind s               (* 约束3：每种kind仅对应一个记录（kind函数在集合上是单射） *)
  )"

(* 定义示例集合 *)
define s1 :: aset where "s1 = {}"
define s2 :: aset where "s2 = {⦇ kind = k1, val = 1 ⦈, ⦇ kind = k1, val = 2 ⦈}"
define s3 :: aset where "s3 = {⦇ kind = k1, val = 1 ⦈, ⦇ kind = k3, val = 3 ⦈}"

(* 验证合法性 *)
lemma "¬is_valid_aset s1" by (simp add: is_valid_aset_def s1_def)
lemma "¬is_valid_aset s2" by (simp add: is_valid_aset_def s2_def)
lemma "is_valid_aset s3" by (simp add: is_valid_aset_def s3_def)

这个方法灵活易用，你可以在需要验证合法性的场景中直接调用is_valid_aset谓词。

方法2：使用typedef创建带约束的新类型 #

如果你希望所有该类型的元素自动满足约束，可以用typedef基于合法子集创建严格的新类型：

datatype akind = k1 | k2 | k3
record apair =
  kind :: akind
  val :: nat

type_synonym aset = "apair set"

(* 先定义合法集合的谓词 *)
definition valid_aset_pred :: "aset ⇒ bool" where
  "valid_aset_pred s = (finite s ∧ s ≠ {} ∧ inj_on kind s)"

(* 证明存在至少一个合法集合（typedef的必要前置条件） *)
lemma exists_valid_aset: "∃s. valid_aset_pred s"
  using s3_def valid_aset_pred_def by auto

(* 创建带约束的新类型ValidAset *)
typedef ValidAset = "{s :: aset. valid_aset_pred s}"
  using exists_valid_aset by blast

(* 定义新类型到原始aset的转换函数 *)
definition valid_aset_to_set :: "ValidAset ⇒ aset" where
  "valid_aset_to_set = Rep_ValidAset"

(* 验证新类型元素天然满足所有约束 *)
lemma valid_aset_properties:
  fixes v :: ValidAset
  shows "finite (valid_aset_to_set v)"
    and "valid_aset_to_set v ≠ {}"
    and "inj_on kind (valid_aset_to_set v)"
  using Rep_ValidAset [of v] valid_aset_pred_def valid_aset_to_set_def by auto

使用typedef后，ValidAset类型的所有实例都自动符合你要求的三条约束，无需每次手动验证。

补充说明 #

• 约束3用inj_on kind s等价于原描述的“每种kind仅对应一个记录”，写法更简洁且符合Isabelle的惯用法；
• 示例中集合元素需用record的标准语法⦇ kind = k1, val = 1 ⦈，而非元组形式，因为你定义的是record而非tuple。

内容的提问来源于stack exchange，提问作者Alicia M.