问如何让选项表达式在伊莎贝尔中简单化？

EN

我正在尝试理解Isabelle (2020)中的选项，并且无法理解为什么某些简单的选项表达式不像预期的那样计算或简化。

例如，我希望

value "some (1::nat)"

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

"some 1"
  :: "'a

更重要的是，从类型签名中，我希望the函数返回"inside“选项中的值，因此”(一些(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__的东西，或者选项如何简化/计算在伊莎贝尔中？

(我之前不知道伊莎贝尔的选择，我只是假设它和哈斯克尔的类似。)