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 \<leftarrow> lbs, u \<leftarrow> 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

declare [[simp_depth_limit = 50]]

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: mult_ac depends⇣R_def split:if_splits) }
      ultimately show ?thesis by force
    qed
  qed
next
  case (And f1 f2) thus ?case by (fastforce simp:Ball_def)
next
  case (Or f1 f2) thus ?case by (fastforce simp:Ball_def)
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_minus[symmetric]
        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 φ) ∧ c>0 ∧
             Less s (d#ds) : set(R.atoms⇣0 φ) ∧ d<0 ∧
            (r - ⟨cs,xs⟩)/c < (s - ⟨ds,xs⟩)/d ∧
            (∀y. (r - ⟨cs,xs⟩)/c < y ∧ y < (s - ⟨ds,xs⟩)/d --> R.I φ (y#xs))"
      by blast
    moreover hence "(r - ⟨cs,xs⟩) / c < eval (between (r/c,(-1/c) *⇩s cs) (s/d,(-1/d) *⇩s ds)) xs ∧ eval (between (r/c,(-1/c) *⇩s cs) (s/d,(-1/d) *⇩s ds)) xs < (s - ⟨ds,xs⟩) / d"
      apply(auto simp add: field_simps eval_def iprod_left_add_distrib)
       apply(rule real_mult_less_iff1[of 2, THEN iffD1]) apply simp
       apply simp
       apply(rule real_mult_less_iff1[of "-d", THEN iffD1]) apply simp
       apply (simp add:ring_distribs add_divide_distrib mult_ac)
      apply(rule real_mult_less_iff1[of 2, THEN iffD1]) apply simp
      apply simp
      apply(rule real_mult_less_iff1[of "c", THEN iffD1]) apply simp
      apply (simp add:algebra_simps add_divide_distrib diff_divide_distrib)
      done
    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