《伊莎贝尔》中的浮动和区间算术

Question

我在Isabelle中使用Descision_Procs文件中的近似.thy进行区间运算。该文件为您提供了一种在实数上证明不等式的策略，例如：

theorem "3 ≤ x ∧ x ≤ 6 ⟹ sin ( pi / x) > 0.4" by (approximation 10)

现在，我有兴趣尝试实现的核心功能，它似乎是近似函数。这在Isabelle/HOL中通过计算证明实值不等式的第4.5.2节中有描述。以下是我所做的一些陈述：

value "Float 3 (-1)"
value "approx 1 (Num (Float 3 (-2))) [Some (Float 1 0,Float 4 0)]"
value "approx 1 (Add (Num (Float 3 (-2))) (Num (Float 4 (-8)))) [Some (Float 1 0,Float 4 0)]"
value "approx 1 (Add (Var 1) (Num (Float 4 (-8)))) [Some (Float 1 0,Float 4 0)]"

首先，我想问您是否知道一种更方便的方法来编写浮点(可能有一个real_to_float r类型的函数，而不是浮点a b(。然后，您可以看到，在给定一定精度(我将其理解为正确小数的数量(的情况下，该函数计算作为第二个参数给出的运算的上界和下界。

现在，主要问题如下：

• 最后一个参数的用途是什么？我猜它们是第二个参数中变量的置信区间？

• 文本声称此函数还实现了区间算术。你能举一个例子吗？例如，我可以看到这个函数是如何执行区间加法的？([a，b]+[c，d]=[a+c，b+d](

Answer 1

这些东西都不是直接使用的；这就是为什么Approximation方法在它们上面提供了一个方便层。

有一个类似real_to_float的函数。它的名字是float_of，但它没有任何代码方程，所以你不能真正使用它。可以为它证明一个代码方程，但这会有点乏味。

至于你的其他问题：是的，最后一个参数是一个列表，其中第i个元素是已知第i个变量值所在的区间。

是的，approx执行区间运算；事实上，这是它所做工作的核心。它完全按间隔运行。你提到的例子可以观察到，例如，当进行x + y时，其中x在[1;2]中，y在[-1;2]中：

value "approx 10 (Add (Var 0) (Var 1))
[Some (Float 1 0, Float 1 1), Some (Float (-1) 0, Float 1 1)]"

返回区间CCD_ 10:

"Some (Float 0 0, Float 2 1)"
:: "(float × float) option"

或者更直接地说：

lemma "(x :: real) ∈ {1..2} ⟹ y ∈ {-1..2} ⟹ x + y ∈ {0..4}"
by (approximation 10)