Theory FRE

(*  Author:     Tobias Nipkow, 2007  *)

theory FRE
imports LinArith
begin

subsection‹Ferrante-Rackoff \label{sec:FRE}›

text‹This section formalizes a slight variant of Ferrante and
Rackoff's algorithm~\<^cite>‹"FerranteR-SIAM75"›. We consider equalities
separately, which improves performance.›

fun between :: "real * real list ⇒ real * real list ⇒ real * real list"
where "between (r,cs) (s,ds) = ((r+s)/2, (1/2) *⇩s (cs+ds))"

definition FR⇩1 :: "atom fm ⇒ atom fm" where
"FR⇩1 φ =
(let as = R.atoms⇩0 φ; lbs = lbounds as; ubs = ubounds as; ebs = ebounds as;
     intrs = [subst φ (between l u) . l ← lbs, u ← ubs]
 in list_disj (inf⇩- φ # inf⇩+ φ # intrs @ map (subst φ) ebs))"


lemma dense_interval:
assumes "finite L" "finite U" "l ∈ L" "u ∈ U" "l < x" "x < u" "P(x::real)"
and dense: "⋀y l u. ⟦ ∀y∈{l<..<x}. y ∉ L;  ∀y∈{x<..<u}. y ∉ U;
                       l<x;x<u; l<y;y<u ⟧ ⟹ P y"
shows "∃l∈L.∃u∈U. l<u ∧ (∀y. l<y ∧ y<u ⟶ P y)"
proof -
  let ?L = "{l:L. l < x}" let ?U = "{u:U. x < u}"
  let ?ll = "Max ?L" let ?uu = "Min ?U"
  have "?L ≠ {}" using ‹l ∈ L› ‹l<x› by (blast intro:order_less_imp_le)
  moreover have "?U ≠ {}" using ‹u:U› ‹x<u› by (blast intro:order_less_imp_le)
  ultimately have "∀y. ?ll<y ∧ y<x ⟶ y ∉ L" "∀y. x<y ∧ y<?uu ⟶ y ∉ U"
    using ‹finite L› ‹finite U› by force+
  moreover have "?ll ∈ L"
  proof
    show "?ll ∈ ?L" using ‹finite L› Max_in[OF _ ‹?L ≠ {}›] by simp
    show "?L ⊆ L" by blast
  qed
  moreover have "?uu ∈ U"
  proof
    show "?uu ∈ ?U" using ‹finite U› Min_in[OF _ ‹?U ≠ {}›] by simp
    show "?U ⊆ U" by blast
  qed
  moreover have "?ll < x" using ‹finite L› ‹?L ≠ {}› by simp
  moreover have "x < ?uu" using ‹finite U› ‹?U ≠ {}› by simp
  moreover have "?ll < ?uu" using ‹?ll<x› ‹x<?uu› by arith
  ultimately show ?thesis using ‹l < x› ‹x < u› ‹?L ≠ {}› ‹?U ≠ {}›
    by(blast intro!:dense greaterThanLessThan_iff[THEN iffD1])
qed

lemma dense:
  "⟦ nqfree f; ∀y∈{l<..<x}. y ∉ LB f xs; ∀y∈{x<..<u}. y ∉ UB f xs;
     l < x; x < u; x ∉ EQ f xs;  R.I f (x#xs); l < y; y < u⟧
   ⟹ R.I f (y#xs)"
proof(induct f)
  case (Atom a)
  show ?case
  proof (cases a)
    case (Less r cs)
    show ?thesis
    proof (cases cs)
      case Nil thus ?thesis using Atom Less by (simp add:depends⇩R_def)
    next
      case (Cons c cs)
      hence "r < c*x + ⟨cs,xs⟩" using Atom Less by simp
      { assume "c=0" hence ?thesis using Atom Less Cons by simp }
      moreover
      { assume "c<0"
        hence "x < (r - ⟨cs,xs⟩)/c" (is "_ < ?u") using ‹r < c*x + ⟨cs,xs⟩›
          by (simp add: field_simps)
        have ?thesis
        proof (rule ccontr)
          assume "¬ R.I (Atom a) (y#xs)"
          hence "?u ≤ y" using Atom Less Cons ‹c<0›
            by (auto simp add: field_simps)
          hence "?u < u" using ‹y<u› by simp
          with ‹x<?u› show False using Atom Less Cons ‹c<0›
            by(auto simp:depends⇩R_def)
        qed } moreover
      { assume "c>0"
        hence "x > (r - ⟨cs,xs⟩)/c" (is "_ > ?l") using ‹r < c*x + ⟨cs,xs⟩›
          by (simp add: field_simps)
        have ?thesis
        proof (rule ccontr)
          assume "¬ R.I (Atom a) (y#xs)"
          hence "?l ≥ y" using Atom Less Cons ‹c>0›
            by (auto simp add: field_simps)
          hence "?l > l" using ‹y>l› by simp
          with ‹?l<x› show False using Atom Less Cons ‹c>0›
            by (auto simp:depends⇩R_def)
        qed }
      ultimately show ?thesis by force
    qed
  next
    case (Eq r cs)
    show ?thesis
    proof (cases cs)
      case Nil thus ?thesis using Atom Eq by (simp add:depends⇩R_def)
    next
      case (Cons c cs)
      hence "r = c*x + ⟨cs,xs⟩" using Atom Eq by simp
      { assume "c=0" hence ?thesis using Atom Eq Cons by simp }
      moreover
      { assume "c≠0"
        hence ?thesis using ‹r = c*x + ⟨cs,xs⟩› Atom Eq Cons ‹l<y› ‹y<u›
          by (auto simp: depends⇩R_def split: if_splits) }
      ultimately show ?thesis by force
    qed
  qed
next
  case (And f1 f2) thus ?case
    by auto (metis (no_types, opaque_lifting))+
next
  case (Or f1 f2) thus ?case
    by auto (metis (no_types, opaque_lifting))+
qed fastforce+

theorem I_FR⇩1:
assumes "nqfree φ" shows "R.I (FR⇩1 φ) xs = (∃x. R.I φ (x#xs))"
  (is "?FR = ?EX")
proof
  assume ?FR
  { assume "R.I (inf⇩- φ) xs"
    hence ?EX using ‹?FR› min_inf[OF ‹nqfree φ›, where xs=xs]
      by(auto simp add:FR⇩1_def)
  } moreover
  { assume "R.I (inf⇩+ φ) xs"
    hence ?EX using ‹?FR› plus_inf[OF ‹nqfree φ›, where xs=xs]
      by(auto simp add:FR⇩1_def)
  } moreover
  { assume "∃x ∈ EQ φ xs. R.I φ (x#xs)"
    hence ?EX using ‹?FR› by(auto simp add:FR⇩1_def)
  } moreover
  { assume "¬R.I (inf⇩- φ) xs ∧ ¬R.I (inf⇩+ φ) xs ∧
            (∀x∈EQ φ xs. ¬R.I φ (x#xs))"
    with ‹?FR› obtain r cs s ds
      where "R.I (subst φ (between (r,cs) (s,ds))) xs"
      by(auto simp: FR⇩1_def eval_def
        diff_divide_distrib set_ebounds I_subst ‹nqfree φ›) blast
    hence "R.I φ (eval (between (r,cs) (s,ds)) xs # xs)"
      by(simp add:I_subst ‹nqfree φ›)
    hence ?EX .. }
  ultimately show ?EX by blast
next
  assume ?EX
  then obtain x where x: "R.I φ (x#xs)" ..
  { assume "R.I (inf⇩- φ) xs ∨ R.I (inf⇩+ φ) xs"
    hence ?FR by(auto simp:FR⇩1_def)
  } moreover
  { assume "x ∈ EQ φ xs"
    then obtain r cs
      where "(r,cs) ∈ set(ebounds(R.atoms⇩0 φ)) ∧ x = r + ⟨cs,xs⟩"
      by(force simp:set_ebounds field_simps)
    moreover hence "R.I (subst φ (r,cs)) xs" using x
      by(auto simp: I_subst ‹nqfree φ› eval_def)
    ultimately have ?FR by(force simp:FR⇩1_def) } moreover
  { assume "¬ R.I (inf⇩- φ) xs" and "¬ R.I (inf⇩+ φ) xs" and "x ∉ EQ φ xs"
    obtain l where "l ∈ LB φ xs" "l < x"
      using LBex[OF ‹nqfree φ› x ‹¬ R.I (inf⇩- φ) xs› ‹x ∉ EQ φ xs›] ..
    obtain u where "u ∈ UB φ xs" "x < u"
      using UBex[OF ‹nqfree φ› x ‹¬ R.I (inf⇩+ φ) xs› ‹x ∉ EQ φ xs›] ..
    have "∃l∈LB φ xs. ∃u∈UB φ xs. l<u ∧ (∀y. l < y ∧ y < u ⟶ R.I φ (y#xs))"
      using dense_interval[where P = "λx. R.I φ (x#xs)", OF finite_LB finite_UB ‹l:LB φ xs› ‹u:UB φ xs› ‹l<x› ‹x<u› x] x dense[OF ‹nqfree φ› _ _ _ _ ‹x ∉ EQ φ xs›] by simp
    then obtain r c cs s d ds
      where "Less r (c # cs) ∈ set (R.atoms⇩0 φ)" "Less s (d # ds) ∈ set (R.atoms⇩0 φ)"
          "⋀y. (r - ⟨cs,xs⟩) / c < y ⟹ y < (s - ⟨ds,xs⟩) / d ⟹ R.I φ (y # xs)"
        and *: "c > 0" "d < 0" "(r - ⟨cs,xs⟩) / c < (s - ⟨ds,xs⟩) / d"
      by blast
    moreover
      have "(r - ⟨cs,xs⟩) / c < eval (between (r / c, (-1 / c) *⇩s cs) (s / d, (-1 / d) *⇩s ds)) xs" (is ?P)
        and "eval (between (r / c, (-1 / c) *⇩s cs) (s / d, (-1 / d) *⇩s ds)) xs < (s - ⟨ds,xs⟩) / d" (is ?Q)
    proof -
      from * have [simp]: "c * (c * (d * (d * 4))) > 0"
        by (simp add: algebra_split_simps)
      from * have "c * s + d * ⟨cs,xs⟩ < d * r + c * ⟨ds,xs⟩"
        by (simp add: field_simps)
      with * have "(2 * c * c * d) * (d * r + c * ⟨ds,xs⟩)
        < (2 * c * c * d) * (c * s + d * ⟨cs,xs⟩)"
        and "(2 * c * d * d) * (c * s + d * ⟨cs,xs⟩)
        < (2 * c * d * d) * (d * r + c * ⟨ds,xs⟩)" by simp_all
      with * show ?P and ?Q by (auto simp add: field_simps eval_def iprod_left_add_distrib)
    qed
    ultimately have ?FR
      by (fastforce simp: FR⇩1_def bex_Un set_lbounds set_ubounds set_ebounds I_subst ‹nqfree φ›)
  } ultimately show ?FR by blast
qed


definition "FR = R.lift_nnf_qe FR⇩1"


lemma qfree_FR⇩1: "nqfree φ ⟹ qfree (FR⇩1 φ)"
apply(simp add:FR⇩1_def)
apply(rule qfree_list_disj)
apply(auto simp:qfree_min_inf qfree_plus_inf set_ubounds set_lbounds set_ebounds image_def qfree_map_fm)
done

theorem I_FR: "R.I (FR φ) xs = R.I φ xs"
by(simp add:I_FR⇩1 FR_def R.I_lift_nnf_qe qfree_FR⇩1)

theorem qfree_FR: "qfree (FR φ)"
by(simp add:FR_def R.qfree_lift_nnf_qe qfree_FR⇩1)

end