Theory Experiments

theory Experiments
  imports Taylor_Models
    Affine_Arithmetic.Affine_Arithmetic
begin

instantiation interval::("{show, preorder}") "show" begin

context includes interval.lifting begin
lift_definition shows_prec_interval::
  "nat ⇒ 'a interval ⇒ char list ⇒ char list"
  is "λp ivl s. (shows_string ''Interval'' o shows ivl) s" .


lift_definition shows_list_interval::
  "'a interval list ⇒ char list ⇒ char list"
  is "λivls s. shows_list ivls s" .

instance
  apply standard
  subgoal by transfer (auto simp: show_law_simps)
  subgoal by transfer (auto simp: show_law_simps)
  done
end

end

definition  split_largest_interval :: "float interval list ⇒ float interval list × float interval list" where
"split_largest_interval xs = (case sort_key (uminus o snd) (zip [0..<length xs] (map (λx. upper x - lower x) xs)) of Nil ⇒ ([], [])
  | (i, _)#_ ⇒ let x = xs! i in (xs[i:=Ivl (lower x) ((upper x + lower x)*Float 1 (-1))],
                 xs[i:=Ivl ((upper x + lower x)*Float 1 (-1)) (upper x)]))"

definition "Inf_tm p params tm =
  lower (compute_bound_tm p (replicate params (Ivl (-1) (1))) (replicate params (Ivl 0 0)) tm)"

primrec prove_pos::"bool ⇒ nat ⇒ nat ⇒ nat ⇒
    (nat ⇒ nat ⇒ taylor_model list ⇒ taylor_model option) ⇒ float interval list list ⇒ bool" where
  "prove_pos prnt 0 p ord F X = (let _ = if prnt then print (STR ''# depth limit exceeded⏎'') else () in False)"
| "prove_pos prnt (Suc i) p ord F XXS =
    (case XXS of [] ⇒ True | (X#XS) ⇒
    let
       params = length X;
       R = F p ord (tms_of_ivls X);
       _ = if prnt  then print (String.implode ((shows ''# '' o shows (map (λivl. (lower ivl, upper ivl)) X)) ''⏎'')) else ()
    in
    if R ≠ None ∧ 0 < Inf_tm p params (the R)
    then let _ = if prnt then print (STR ''# Success⏎'') else () in prove_pos prnt i p ord F XS
    else let _ = if prnt then print (String.implode ((shows ''# Split ('' o shows ((map_option (Inf_tm p params)) R) o shows '')'') ''⏎'')) else () in case split_largest_interval X of (a, b) ⇒
      prove_pos prnt i p ord F (a#b#XS))"

hide_const (open) prove_pos_slp

definition "prove_pos_slp prnt prec ord fa i xs = (let slp = slp_of_fas [fa] in prove_pos prnt i prec ord (λp ord xs.
  case approx_slp prec ord 1 slp xs of None ⇒ None | Some [x] ⇒ Some x | Some _ ⇒ None) xs)"

experiment begin

unbundle floatarith_syntax

abbreviation "schwefel ≡
  (5.8806 / 10 ^ 10) + (Var 0 - (Var 1)^⇩e2)^⇩e2 + (Var 1 - 1)^⇩e2 + (Var 0 - (Var 2)^⇩e2)^⇩e2 + (Var 2 - 1)^⇩e2"

lemma "prove_pos_slp True 30 0 schwefel 100000 [replicate 3 (Ivl (-10) 10)]"
  by eval

abbreviation "delta6 ≡ (Var 0 * Var 3 * (-Var 0 + Var 1 + Var 2 - Var 3 + Var 4 + Var 5) +
    Var 1 * Var 4 * ( Var 0 - Var 1 + Var 2 + Var 3 - Var 4 + Var 5) +
    Var 2 * Var 5 * ( Var 0 + Var 1 - Var 2 + Var 3 + Var 4 - Var 5)
   - Var 1 * Var 2 * Var 3
   - Var 0 * Var 2 * Var 4
   - Var 0 * Var 1 * Var 5
   - Var 3 * Var 4 * Var 5)"

lemma "prove_pos_slp True 30 3 delta6 10000 [replicate 6 (Ivl 4 (Float 104045 (-14)))]"
  by eval

abbreviation "caprasse ≡ (3.1801 + - Var 0 * (Var 2) ^⇩e 3 + 4 * Var 1 * (Var 2)^⇩e2 * Var 3 +
    4 * Var 0 * Var 2 * (Var 3)^⇩e2 + 2 * Var 1 * (Var 3)^⇩e3 + 4 * Var 0 * Var 2 + 4 * (Var 2)^⇩e2 - 10 * Var 1 * Var 3 +
    -10 * (Var 3)^⇩e2 + 2)"

lemma "prove_pos_slp True 30 2 caprasse 10000 [replicate 4 (Ivl (-Float 1 (-1)) (Float 1 (-1)))]"
  by eval

abbreviation "magnetism ≡
  0.25001 + (Var 0)^⇩e2 + 2 * (Var 1)^⇩e2 + 2 * (Var 2)^⇩e2 + 2 * (Var 3)^⇩e2 + 2 * (Var 4)^⇩e2 + 2 * (Var 5)^⇩e2 +
    2 * (Var 6)^⇩e2 - Var 0"

end

end