# Theory FRE

Up to index of Isabelle/HOL/LinearQuantifierElim

theory FRE
imports LinArith
(*  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 FR1 :: "atom fm => atom fm" where
"FR1 φ =
(let as = R.atoms0 φ; 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:dependsR_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⟩
have ?thesis
proof (rule ccontr)
assume "¬ R.I (Atom a) (y#xs)"
hence "?u ≤ y" using Atom Less Cons c<0
hence "?u < u" using y<u by simp
with x<?u show False using Atom Less Cons c<0
by(auto simp:dependsR_def)
qed } moreover
{ assume "c>0"
hence "x > (r - ⟨cs,xs⟩)/c" (is "_ > ?l") using r < c*x + ⟨cs,xs⟩
have ?thesis
proof (rule ccontr)
assume "¬ R.I (Atom a) (y#xs)"
hence "?l ≥ y" using Atom Less Cons c>0
hence "?l > l" using y>l by simp
with ?l<x show False using Atom Less Cons c>0
by (auto simp:dependsR_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:dependsR_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 dependsR_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_FR1:
assumes "nqfree φ" shows "R.I (FR1 φ) 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]
} moreover
{ assume "R.I (inf+ φ) xs"
hence ?EX using ?FR plus_inf[OF nqfree φ, where xs=xs]
} moreover
{ assume "∃x ∈ EQ φ xs. R.I φ (x#xs)"
hence ?EX using ?FR by(auto simp add:FR1_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: FR1_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:FR1_def)
} moreover
{ assume "x : EQ φ xs"
then obtain r cs
where "(r,cs) : set(ebounds(R.atoms0 φ)) ∧ 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:FR1_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.atoms0 φ) ∧ c>0 ∧
Less s (d#ds) : set(R.atoms0 φ) ∧ 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(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(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
done
ultimately have ?FR
by(fastforce simp:FR1_def bex_Un set_lbounds set_ubounds set_ebounds I_subst nqfree φ)
} ultimately show ?FR by blast
qed

definition "FR = R.lift_nnf_qe FR1"

lemma qfree_FR1: "nqfree φ ==> qfree (FR1 φ)"