(* Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2009 *)

theory Approximation_Ex
imports Complex_Main "../Approximation"
begin

text ‹

  are some examples how to use the approximation method.

  approximation method has the following syntax:

  "prec" (splitting: "x" = "depth" and "y" = "depth" ...)? (taylor: "z" = "derivates")?

  "prec" specifies the precision used in all computations, it is specified as
  of bits to calculate. In the proposition to prove an arbitrary amount of
  can be used, but each one need to be bounded by an upper and lower
 .

  specify the bounds either term‹l₁ ≤ x ∧ x ≤ u₁›,
 term‹x ∈ { l₁ .. u₁ }› or term‹x = bnd› can be used. Where the
  specification are again arithmetic formulas containing variables. They can
  connected using either meta level or HOL equivalence.

  use interval splitting add for each variable whos interval should be splitted
  the "splitting:" parameter. The parameter specifies how often each interval
  be divided, e.g. when x = 16 is specified, there will be term‹65536 = 2^16›
  to be calculated.

  use taylor series expansion specify the variable to derive. You need to
  the amount of derivations to compute. When using taylor series expansion
  one variable can be used.

 ›

section "Compute some transcendental values"

lemma "∣ ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 ∣ < (inverse (2^51) :: real)"
  by (approximation 60)

lemma "∣ exp 1.626 - 5.083499996273 ∣ < (inverse 10 ^ 10 :: real)"
  by (approximation 40)

lemma "∣ sqrt 2 - 1.4142135623730951 ∣ < inverse 10 ^ 16"
  by (approximation 60)

lemma "∣ pi - 3.1415926535897932385 ∣ < inverse 10 ^ 18"
  by (approximation 70)

lemma "∣ sin 100 + 0.50636564110975879 ∣ < (inverse 10 ^ 17 :: real)"
  by (approximation 70)

section "Use variable ranges"

lemma "0.5 ≤ x ∧ x ≤ 4.5 ==> ∣ arctan x - 0.91 ∣ < 0.455"
  by (approximation 10)

lemma "x ∈ {0.5 .. 4.5} ⟶ ∣ arctan x - 0.91 ∣ < 0.455"
  by (approximation 10)

lemma "0.49 ≤ x ∧ x ≤ 4.49 ==> ∣ arctan x - 0.91 ∣ < 0.455"
  by (approximation 20)

lemma "1 / 2^1 ≤ x ∧ x ≤ 9 / 2^1 ==> ∣ arctan x - 0.91 ∣ < 0.455"
  by (approximation 10)

lemma "3.2 ≤ (x::real) ∧ x ≤ 6.2 ==> sin x ≤ 0"
  by (approximation 10)

lemma "3.2 ≤ (x::real) ∧ x ≤ 3.9 ==> real_of_int (ceiling x) ∈ {4 .. 4}"
  by (approximation 10)

lemma
  defines "g ≡ 9.80665" and "v ≡ 128.61" and "d ≡ pi / 180"
  shows "g / v * tan (35 * d) ∈ { 3 * d .. 3.1 * d }"
  using assms by (approximation 20)

lemma "x ∈ { 0 .. 1 :: real } ⟶ x² ≤ x"
  by (approximation 30 splitting: x=1 taylor: x = 3)

lemma "(n::real) ∈ {32 .. 62} ==> ⌈log 2 (2 * (⌊n⌋ div 2) + 1)⌉ = ⌈log 2 (⌊n⌋ + 1)⌉"
  unfolding eq_iff
  by (approximation 20)

approximate 10

end