如何在Isabelle中评估自定义类型t的Rep_t操作？

我在Isabelle中定义了如下类型t：

typedef t = "{(0::nat)..10}" by auto

为了能评估t类型的项，我将Abs_t设置为构造器：

lemma [code abstype]: "Abs_t (Rep_t x) = x" by (rule Rep_t_inverse)
code_datatype Abs_t

这样就能通过value "Abs_t 4"这类语句正常求值。

现在我希望让Rep_t x形式的项能映射回自然数，但Rep_t (Abs_t x) = x仅在x属于集合{(0::nat)..10}时成立，无法直接作为通用的代码方程。

目前我只能给定义域内的每个元素单独编写代码方程：

lemma[code]:
 "Rep_t (Abs_t 0) = 0"
 "Rep_t (Abs_t 1) = 1"
 (* ... 中间省略7个元素的方程 *)
 "Rep_t (Abs_t 10) = 10"
 by(auto simp add: Abs_t_inverse) 

但这种方式在定义域范围更大时完全不可行。

我尝试过两种方案都失败了：

• 直接使用lemma [code abstype]: "Rep_t (Abs_t x) = x"，因前提条件不满足无法通过
• 尝试编写带条件的方程：lemma [code abstype]: "Rep_t (Abs_t x) = (if x ∈ {(0::nat)..10} then x else undefined)"，但无法完成证明

请问如何正确定义代码方程，使得value "(Rep_t (Abs_t x))"对定义域内的所有x都能求值为x::nat？

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