Isabelle中同构类型的运算符重载与定理继承问题

核心思路：基于类型同构与Lifting包 #

你提到的通过同构函数复用nat的定义和定理完全可行，Isabelle的Lifting包就是专门解决这类问题的——它能依托类型同构关系，自动将nat上的运算符、定理“迁移”到自定义类型中，无需手动重复实现所有逻辑。

具体实现步骤 #

1. 定义类型并证明同构性 #

你的seconds和minutes本质是nat的包装类型，先明确它们与nat的同构函数，并证明二者互为逆函数：

datatype seconds = Seconds (secs: nat)
datatype minutes = Minutes (mins: nat)

(* 证明seconds与nat的同构关系 *)
lemma secs_inverse: "secs (Seconds n) = n" by simp
lemma Seconds_inverse: "Seconds (secs s) = s" by (cases s) simp_all

(* 证明minutes与nat的同构关系 *)
lemma mins_inverse: "mins (Minutes n) = n" by simp
lemma Minutes_inverse: "Minutes (mins m) = m" by (cases m) simp_all

2. 提升nat的运算符到自定义类型 #

使用lift_definition命令将nat上的运算符（如+、*、≤等）迁移到自定义类型，以加法为例：

(* 为seconds提升加法运算 *)
lift_definition plus_seconds :: "seconds ⇒ seconds ⇒ seconds" is "(+) :: nat ⇒ nat ⇒ nat"
  by (auto simp: secs_inverse Seconds_inverse)

(* 重载加号，让Seconds可以直接使用+ *)
notation plus_seconds (infixl "+" 60)

(* 同理为minutes提升加法 *)
lift_definition plus_minutes :: "minutes ⇒ minutes ⇒ minutes" is "(+) :: nat ⇒ nat ⇒ nat"
  by (auto simp: mins_inverse Minutes_inverse)
notation plus_minutes (infixl "+" 60)

3. 自动继承nat的定理 #

Lifting包支持通过transfer属性将nat的定理直接转移到自定义类型，比如加法结合律：

(* 转移nat的加法结合律到seconds *)
lemma plus_seconds_assoc: "(s1 + s2) + s3 = s1 + (s2 + s3)"
  by (transfer, rule add.assoc)

(* 你的目标语句可直接通过transfer+simp验证 *)
lemma "Seconds 1 + Seconds 2 + Seconds 3 = Seconds 6"
  by (transfer, simp)

若想让auto自动调用这些迁移后的定理，可将其加入simp集合：

declare plus_seconds_assoc [simp]
declare plus_seconds_comm [simp]  (* 转移交换律后同样加入 *)

简化方案：用typedef替代datatype #

使用typedef定义类型可自动生成同构相关的核心定理，省去手动编写case分析证明的步骤：

typedef seconds = "{n :: nat. True}" by auto
typedef minutes = "{n :: nat. True}" by auto

(* 自动生成的同构函数：Abs_seconds、Rep_seconds *)
lemma Rep_Abs_seconds: "Rep_seconds (Abs_seconds n) = n" by (rule Rep_Abs)
lemma Abs_Rep_seconds: "Abs_seconds (Rep_seconds s) = s" by (rule Abs_Rep)

(* 提升运算符的过程更简洁 *)
lift_definition plus_seconds :: "seconds ⇒ seconds ⇒ seconds" is "(+)" .
notation plus_seconds (infixl "+" 60)

关键注意点 #

• 每个需要的运算符或关系（+、-、*、≤等）都需通过lift_definition单独提升，Lifting包支持绝大多数常见的nat上的定义。
• 自定义定理可通过transfer属性直接从nat的对应定理迁移，无需手动重新证明。
• 类型安全的目标完全保留：尝试将seconds与minutes相加时，类型系统会直接报错，避免类型混淆。

内容的提问来源于stack exchange，提问作者Mathieu Paturel