Floating and interval arithmetic in Isabelle

Question

I'm using the Approximation.thy from the Descision_Procs file for interval arithmetic in Isabelle. The file gives you a tactic for proving inequalities over the reals, such as:

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

Now, I'm interested in trying out the core function of the implementation which appears to be the approx function. This is described in section 4.5.2 of Proving Real-Valued Inequalities by Computation in Isabelle/HOL. Here are some of the statements that I do:

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)]"

First, I would ask if you know a more convinient way to write floats (instead of Float a b, maybe there is a function of the kind real_to_float r). Then, you see that the function computes, given some precision (which I understand as the number of correct decimals), the upper and lower bounds for the operations given as a second parameter.

Now, the main question is the following:

• What is the purpose of the last parameter? I guess they are confidence intervals for the variables in the second parameter?

• The text claims that this function also implements interval arithmetic. Can you show an example where I can see how this functions performs interval addition for instance? ([a,b]+[c,d]=[a+c,b+d])

Answer 1

None of these things are meant to be used directly; that's why the Approximation method offers a convenience layer above them.

There is a function like real_to_float. Its name is float_of, but it does not have any code equations, so you cannot really use it. One could prove a code equation for it, but that would be a bit tedious.

As for your other questions: Yes, the last parameter is a list where the i-th element is an interval in which the value of the i-th variable is known to lie.

And yes, approx performs interval arithmetic; in fact, that is at the very core of what it does. It operates entirely on intervals. The example you mentioned can be observed e.g. when doing x + y where x is in [1;2] and y is in [-1;2]:

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

which returns the interval [0;4]:

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

or, more directly:

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