如何让选项表达式在 Isabelle 中简化？

Question

我试图理解 Isabelle (2020) 中的选项，但无法理解为什么一些简单的选项表达式不能按预期计算或简化。

例如，我希望这样

value "some (1::nat)"

应该返回一个"nat option" 类型，然而，它返回一个未指定的类型：

"some 1"
  :: "'a

此外，从类型签名来看，我希望 the 函数在选项“内部”返回值，因此“(some (1::nat))”只是 (1::nat)。

然而，

value "the (some (1::nat))"

返回一个看似不是很有用的类型：

"the (some 1)"
  :: "'a"

，这不是nat。那么结果就不是很有用了，例如

 value "the (some (1::nat)) + 2"

返回

"the (some 1) + (1 + 1)"
  :: "'a"

（我预计结果是"3::nat"）

这是设计使然，还是我错过了 the 的某些内容，或者 Isabelle 中的选项如何简化/计算？

（我没有关于 Isabelle 选项的先验知识，我只是假设它类似于 Haskell 的 Maybe。）

Answer 1

A C-click 显示定义是：

datatype 'a option =
    None
  | Some (the: 'a)

是一些，而不是一些。

有提示看到some没有定义：颜色和the中的颜色不一样。