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⟩`
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:dependsR_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: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 (fastsimp simp:Ball_def)
next
case (Or f1 f2) thus ?case by (fastsimp simp:Ball_def)
qed fastsimp+
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]
by(auto simp add:FR1_def)
} moreover
{ assume "R.I (inf+ φ) xs"
hence ?EX using `?FR` plus_inf[OF `nqfree φ`, where xs=xs]
by(auto simp add:FR1_def)
} 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(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(fastsimp 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 φ)"
apply(simp add:FR1_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_FR1 FR_def R.I_lift_nnf_qe qfree_FR1)
theorem qfree_FR: "qfree (FR φ)"
by(simp add:FR_def R.qfree_lift_nnf_qe qfree_FR1)
end