theory QEdlo_fr
imports DLO
begin
subsection "Interior Point Method"
text{* This section formalizes a new quantifier elimination procedure
based on the idea of Ferrante and Rackoff~\cite{FerranteR-SIAM75} (see
also \S\ref{sec:FRE}) of taking a point between each lower and upper
bound as a test point. For dense linear orders it is not obvious how
to realize this because we cannot name any intermediate point
directly. *}
fun asubst2 :: "nat => nat => atom => atom fm" where
"asubst2 l u (Less 0 0) = FalseF" |
"asubst2 l u (Less 0 (Suc j)) = Or (Atom(Less u j)) (Atom(Eq u j))" |
"asubst2 l u (Less (Suc i) 0) = Or (Atom(Less i l)) (Atom(Eq i l))" |
"asubst2 l u (Less (Suc i) (Suc j)) = Atom(Less i j)" |
"asubst2 l u (Eq 0 0) = TrueF" |
"asubst2 l u (Eq 0 _) = FalseF" |
"asubst2 l u (Eq _ 0) = FalseF" |
"asubst2 l u (Eq (Suc i) (Suc j)) = Atom(Eq i j)"
abbreviation "subst2 l u ≡ amapfm (asubst2 l u)"
lemma I_subst21:
"nqfree f ==> xs!l < xs!u ==> DLO.I (subst2 l u f) xs
==> xs!l < x ==> x < xs!u ==> DLO.I f (x#xs)"
proof(induct f arbitrary: x)
case (Atom a) thus ?case
by (cases "(l,u,a)" rule: asubst2.cases) auto
qed auto
definition
"nolub f xs l x u <-> (∀y∈{l<..<x}. y ∉ LB f xs) ∧ (∀y∈{x<..<u}. y ∉ UB f xs)"
lemma nolub_And[simp]:
"nolub (And f g) xs l x u = (nolub f xs l x u ∧ nolub g xs l x u)"
by(auto simp:nolub_def)
lemma nolub_Or[simp]:
"nolub (Or f g) xs l x u = (nolub f xs l x u ∧ nolub g xs l x u)"
by(auto simp:nolub_def)
declare[[simp_depth_limit=3]]
lemma innermost_intvl:
"[| nqfree f; nolub f xs l x u; l < x; x < u; x ∉ EQ f xs;
DLO.I f (x#xs); l < y; y < u|]
==> DLO.I f (y#xs)"
proof(induct f)
case (Atom a)
show ?case
proof (cases a)
case (Less i j)
then show ?thesis using Atom
unfolding nolub_def
by (clarsimp simp: nth.simps Ball_def split:split_if_asm nat.splits)
(metis not_leE order_antisym order_less_trans)+
next
case (Eq i j)[simp]
show ?thesis
proof (cases i)
case 0[simp]
show ?thesis
proof (cases j)
case 0 thus ?thesis using Atom by simp
next
case Suc thus ?thesis using Atom by(simp add:EQ_def)
qed
next
case Suc[simp]
show ?thesis
proof (cases j)
case 0 thus ?thesis using Atom by(simp add:EQ_def)
next
case Suc thus ?thesis using Atom by simp
qed
qed
qed
next
case (And f1 f2) thus ?case by (fastsimp)
next
case (Or f1 f2) thus ?case by (fastsimp)
qed simp+
lemma I_subst22:
"nqfree f ==> xs!l < x ∧ x < xs!u ==> nolub f xs (xs!l) x (xs!u)
==> ∀x∈{xs!l <..< xs!u}. DLO.I f (x#xs) ∧ x ∉ EQ f xs
==> DLO.I (subst2 l u f) xs"
proof (induct f)
case (Atom a) show ?case
apply (cases "(l,u,a)" rule: asubst2.cases)
apply(insert Atom, auto simp: EQ_def nolub_def split:split_if_asm)
done
next
case Or thus ?case by (simp add: Ball_def)(metis innermost_intvl)
qed auto
declare[[simp_depth_limit=50]]
definition
"qe_interior1 φ =
(let as = DLO.atoms0 φ; lbs = lbounds as; ubs = ubounds as; ebs = ebounds as;
intrs = [And (Atom(Less l u)) (subst2 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::'a::dlo)"
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<x ∧ x<u ∧ (∀y∈{l<..<x}. y∉L) ∧ (∀y∈{x<..<u}. y∉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 simp
ultimately show ?thesis using `l < x` `x < u` `?L ≠ {}` `?U ≠ {}`
by(blast intro!:dense greaterThanLessThan_iff[THEN iffD1])
qed
theorem I_interior1:
assumes "nqfree φ" shows "DLO.I (qe_interior1 φ) xs = (EX x. DLO.I φ (x#xs))"
(is "?QE = ?EX")
proof
assume ?QE
{ assume "DLO.I (inf- φ) xs"
hence ?EX using `?QE` min_inf[of φ xs] `nqfree φ`
by(auto simp add:qe_interior1_def amap_fm_list_disj)
} moreover
{ assume "DLO.I (inf+ φ) xs"
hence ?EX using `?QE` plus_inf[of φ xs] `nqfree φ`
by(auto simp add:qe_interior1_def amap_fm_list_disj)
} moreover
{ assume "¬DLO.I (inf- φ) xs ∧ ¬DLO.I (inf+ φ) xs ∧
(∀x∈EQ φ xs. ¬DLO.I φ (x#xs))"
with `?QE` `nqfree φ` obtain l u
where "DLO.I (subst2 l u φ) xs" and "xs!l < xs!u"
by(fastsimp simp: qe_interior1_def set_lbounds set_ubounds I_subst EQ_conv_set_ebounds)
moreover then obtain x where "xs!l < x ∧ x < xs!u" by(metis dense)
ultimately have "DLO.I φ (x # xs)"
using `nqfree φ` I_subst21[OF `nqfree φ` `xs!l < xs!u`] by simp
hence ?EX .. }
ultimately show ?EX by blast
next
let ?as = "DLO.atoms0 φ" let ?E = "set(ebounds ?as)"
assume ?EX
then obtain x where x: "DLO.I φ (x#xs)" ..
{ assume "DLO.I (inf- φ) xs ∨ DLO.I (inf+ φ) xs"
hence ?QE using `nqfree φ` by(auto simp:qe_interior1_def)
} moreover
{ assume "EX k : ?E. DLO.I (subst φ k) xs"
hence ?QE by(force simp:qe_interior1_def) } moreover
{ assume "¬ DLO.I (inf- φ) xs" and "¬ DLO.I (inf+ φ) xs"
and "∀k ∈ ?E. ¬ DLO.I (subst φ k) xs"
hence noE: "∀e ∈ EQ φ xs. ¬ DLO.I φ (e#xs)"
using `nqfree φ` by (force simp:set_ebounds EQ_def I_subst)
hence "x ∉ EQ φ xs" using x by fastsimp
obtain l where "l : LB φ xs" "l < x"
using LBex[OF `nqfree φ` x `¬ DLO.I(inf- φ) xs` `x ∉ EQ φ xs`] ..
obtain u where "u : UB φ xs" "x < u"
using UBex[OF `nqfree φ` x `¬ DLO.I(inf+ φ) xs` `x ∉ EQ φ xs`] ..
have "∃l∈LB φ xs. ∃u∈UB φ xs. l<x ∧ x<u ∧ nolub φ xs l x u ∧ (∀y. l < y ∧ y < u --> DLO.I φ (y#xs))"
using dense_interval[where P = "λx. DLO.I φ (x#xs)", OF finite_LB finite_UB `l:LB φ xs` `u:UB φ xs` `l<x` `x<u` x] x innermost_intvl[OF `nqfree φ` _ _ _ `x ∉ EQ φ xs`]
by (simp add:nolub_def) fastsimp
then obtain m n where
"Less (Suc m) 0 : set ?as" "Less 0 (Suc n) : set ?as"
"xs!m < x ∧ x < xs!n"
"nolub φ xs (xs!m) x (xs!n)"
"∀y. xs!m < y ∧ y < xs!n --> DLO.I φ (y#xs)"
by blast
moreover
hence "DLO.I (subst2 m n φ) xs" using noE
by(force intro!: I_subst22[OF `nqfree φ`])
ultimately have ?QE
by(fastsimp simp add:qe_interior1_def bex_Un set_lbounds set_ubounds)
} ultimately show ?QE by blast
qed
lemma qfree_asubst2: "qfree (asubst2 l u a)"
by(cases "(l,u,a)" rule:asubst2.cases) simp_all
lemma qfree_subst2: "nqfree φ ==> qfree (subst2 l u φ)"
by(induct φ) (simp_all add:qfree_asubst2)
lemma qfree_interior1: "nqfree φ ==> qfree(qe_interior1 φ)"
apply(simp add:qe_interior1_def)
apply(rule qfree_list_disj)
apply (auto simp:qfree_min_inf qfree_plus_inf qfree_subst2 qfree_map_fm)
done
definition "qe_interior = DLO.lift_nnf_qe qe_interior1"
lemma qfree_qe_interior: "qfree(qe_interior φ)"
by(simp add: qe_interior_def DLO.qfree_lift_nnf_qe qfree_interior1)
lemma I_qe_interior: "DLO.I (qe_interior φ) xs = DLO.I φ xs"
by(simp add:qe_interior_def DLO.I_lift_nnf_qe qfree_interior1 I_interior1)
end