Isabelle2021中如何优雅解构datatype定义函数？

问题背景 #

首先定义了如下自定义类型：

datatype 'a foo = Foo 'a

我希望编写一个函数，能够解构Foo a并访问其中的a，尝试了以下代码：

definition do_foo :: "'a foo ⇒ 'a" where
  "do_foo (Foo a) ≡ if True then a else a"

但在Isabelle2021中报错：Bad arguments on lhs: "Foo a"。

已尝试的非优雅方案 #

右侧通过case语句解构 #

definition do_foo :: "'a foo ⇒ 'a" where
  "do_foo fooa ≡ case fooa of Foo a ⇒ if True then a else a"

缺点：case语句写法过于冗长。

为datatype内置getter #

datatype 'a foo = Foo (a: 'a)

definition do_foo :: "'a foo ⇒ 'a" where
  "do_foo fooa ≡ if True then a fooa else a fooa"

缺点：getter名称a会污染命名空间，且a fooa的调用写法不够直观美观。

用fun替代definition（无效尝试） #

fun do_foo :: "'a foo ⇒ 'a" where
  "do_foo (Foo a) ≡ if True then a else a"

报错：Not an equation，原因是fun不支持使用≡定义等式。

用fun替代definition（有效但繁琐） #

fun do_foo :: "'a foo ⇒ 'a" where
  "do_foo (Foo a) = (if True then a else a)"

缺点：if语句必须额外加括号，且要模拟definition的特性，还需要执行declare do_foo.simps[simp del]，操作步骤繁琐。

求助 #

现寻求实现该需求的最优雅方式。

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