theory QEdlo_inf
imports DLO
begin
subsection "Quantifier elimination with infinitesimals"
text{* This section presents a new quantifier elimination procedure
for dense linear orders based on (the simulation of) infinitesimals.
It is a fairly straightforward adaptation of the analogous algorithm
by Loos and Weispfenning for linear arithmetic described in
\S\ref{sec:lin-inf}. *}
fun asubst_peps :: "nat => atom => atom fm" ("asubst+") where
"asubst_peps k (Less 0 0) = FalseF" |
"asubst_peps k (Less 0 (Suc j)) = Atom(Less k j)" |
"asubst_peps k (Less (Suc i) 0) = (if i=k then TrueF
else Or (Atom(Less i k)) (Atom(Eq i k)))" |
"asubst_peps k (Less (Suc i) (Suc j)) = Atom(Less i j)" |
"asubst_peps k (Eq 0 0) = TrueF" |
"asubst_peps k (Eq 0 _) = FalseF" |
"asubst_peps k (Eq _ 0) = FalseF" |
"asubst_peps k (Eq (Suc i) (Suc j)) = Atom(Eq i j)"
abbreviation subst_peps :: "atom fm => nat => atom fm" ("subst+") where
"subst+ φ k ≡ amapfm (asubst+ k) φ"
definition "nolb φ xs l x = (∀y∈{l<..<x}. y ∉ LB φ xs)"
lemma nolb_And[simp]:
"nolb (And φ1 φ2) xs l x = (nolb φ1 xs l x ∧ nolb φ2 xs l x)"
apply(clarsimp simp:nolb_def)
apply blast
done
lemma nolb_Or[simp]:
"nolb (Or φ1 φ2) xs l x = (nolb φ1 xs l x ∧ nolb φ2 xs l x)"
apply(clarsimp simp:nolb_def)
apply blast
done
declare[[simp_depth_limit=3]]
lemma innermost_intvl:
"[| nqfree φ; nolb φ xs l x; l < x; x ∉ EQ φ xs; DLO.I φ (x#xs); l < y; y ≤ x|]
==> DLO.I φ (y#xs)"
proof(induct φ)
case (Atom a)
show ?case
proof (cases a)
case (Less i j)
then show ?thesis using Atom
unfolding nolb_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) thus ?thesis using Atom
apply(clarsimp simp:EQ_def nolb_def nth_Cons')
apply(case_tac "i=0 ∧ j=0") apply simp
apply(case_tac "i≠0 ∧ j≠0") apply simp
apply(case_tac "i=0 ∧ j≠0") apply (fastsimp split:split_if_asm)
apply(case_tac "i≠0 ∧ j=0") apply (fastsimp split:split_if_asm)
apply arith
done
qed
next
case And thus ?case by (fastsimp)
next
case Or thus ?case by (fastsimp)
qed simp+
lemma I_subst_peps2:
"nqfree φ ==> xs!l < x ==> nolb φ xs (xs!l) x ==> x ∉ EQ φ xs
==> ∀y ∈ {xs!l <.. x}. DLO.I φ (y#xs)
==> DLO.I (subst+ φ l) xs"
proof(induct φ)
case FalseF thus ?case
by simp (metis linorder_antisym_conv1 linorder_neq_iff)
next
case (Atom a)
show ?case
proof(cases "(l,a)" rule:asubst_peps.cases)
case 3 thus ?thesis using Atom
by (auto simp: nolb_def EQ_def Ball_def)
(metis One_nat_def linorder_antisym_conv1 not_less_iff_gr_or_eq)
qed (insert Atom, auto simp: nolb_def EQ_def Ball_def)
next
case Or thus ?case by(simp add: Ball_def)(metis order_refl innermost_intvl)
qed simp_all
declare[[simp_depth_limit=50]]
lemma dense_interval:
assumes "finite L" "l ∈ L" "l < x" "P(x::'a::dlo)"
and dense: "!!y l. [| ∀y∈{l<..<x}. y ∉ L; l<x; l<y; y≤x |] ==> P y"
shows "∃l∈L. l<x ∧ (∀y∈{l<..<x}. y ∉ L) ∧ (∀y. l<y ∧ y≤x --> P y)"
proof -
let ?L = "{l∈L. l < x}"
let ?ll = "Max ?L"
have "?L ≠ {}" using `l ∈ L` `l<x` by (blast intro:order_less_imp_le)
hence "∀y. ?ll<y ∧ y<x --> y ∉ L" using `finite L` 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 "?ll < x" using `finite L` `?L ≠ {}` by simp
ultimately show ?thesis using `l < x` `?L ≠ {}`
by(blast intro!:dense greaterThanLessThan_iff[THEN iffD1])
qed
lemma I_subst_peps:
"nqfree φ ==> DLO.I (subst+ φ l) xs -->
(∃leps>xs!l. ∀x. xs!l < x ∧ x ≤ leps --> DLO.I φ (x#xs))"
proof(induct φ)
case TrueF thus ?case by simp (metis no_ub)
next
case (Atom a)
show ?case
proof (cases "(l,a)" rule: asubst_peps.cases)
case 2 thus ?thesis using Atom
apply(auto)
apply(drule dense)
apply(metis One_nat_def xt1(7))
done
next
case 3 thus ?thesis using Atom
apply(auto)
apply (metis no_ub)
apply (metis no_ub less_trans)
apply (metis no_ub)
done
next
case 4 thus ?thesis using Atom by(auto)(metis no_ub)
next
case 5 thus ?thesis using Atom by(auto)(metis no_ub)
next
case 8 thus ?thesis using Atom by(auto)(metis no_ub)
qed (insert Atom, auto)
next
case And thus ?case
apply clarsimp
apply(rule_tac x="min leps lepsa" in exI)
apply simp
done
next
case Or thus ?case by force
qed simp_all
definition
"qe_eps1(φ) =
(let as = DLO.atoms0 φ; lbs = lbounds as; ebs = ebounds as
in list_disj (inf- φ # map (subst+ φ) lbs @ map (subst φ) ebs))"
theorem I_qe_eps1:
assumes "nqfree φ" shows "DLO.I (qe_eps1 φ) xs = (∃x. DLO.I φ (x#xs))"
(is "?QE = ?EX")
proof
let ?as = "DLO.atoms0 φ" let ?ebs = "ebounds ?as"
assume ?QE
{ assume "DLO.I (inf- φ) xs"
hence ?EX using `?QE` min_inf[of φ xs] `nqfree φ`
by(auto simp add:qe_eps1_def amap_fm_list_disj)
} moreover
{ assume "∀i ∈ set ?ebs. ¬DLO.I φ (xs!i # xs)"
"¬ DLO.I (inf- φ) xs"
with `?QE` `nqfree φ` obtain l where "DLO.I (subst+ φ l) xs"
by(fastsimp simp: I_subst qe_eps1_def set_ebounds set_lbounds)
then obtain leps where "DLO.I φ (leps#xs)"
using I_subst_peps[OF `nqfree φ`] by fastsimp
hence ?EX .. }
ultimately show ?EX by blast
next
let ?as = "DLO.atoms0 φ" let ?ebs = "ebounds ?as"
assume ?EX
then obtain x where x: "DLO.I φ (x#xs)" ..
{ assume "DLO.I (inf- φ) xs"
hence ?QE using `nqfree φ` by(auto simp:qe_eps1_def)
} moreover
{ assume "∃k ∈ set ?ebs. DLO.I (subst φ k) xs"
hence ?QE by(auto simp:qe_eps1_def) } moreover
{ assume "¬ DLO.I (inf- φ) xs"
and "∀k ∈ set ?ebs. ¬ DLO.I (subst φ k) xs"
hence noE: "∀e ∈ EQ φ xs. ¬ DLO.I φ (e#xs)" using `nqfree φ`
by (auto simp:set_ebounds EQ_def I_subst nth_Cons' split:split_if_asm)
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`] ..
have "∃l∈LB φ xs. l<x ∧ nolb φ xs l x ∧
(∀y. l < y ∧ y ≤ x --> DLO.I φ (y#xs))"
using dense_interval[where P = "λx. DLO.I φ (x#xs)", OF finite_LB `l∈LB φ xs` `l<x` x] x innermost_intvl[OF `nqfree φ` _ _ `x ∉ EQ φ xs`]
by (simp add:nolb_def)
then obtain m
where "Less (Suc m) 0 ∈ set ?as ∧ xs!m < x ∧ nolb φ xs (xs!m) x
∧ (∀y. xs!m < y ∧ y ≤ x --> DLO.I φ (y#xs))"
by blast
then moreover have "DLO.I (subst+ φ m) xs"
using noE by(auto intro!: I_subst_peps2[OF `nqfree φ`])
ultimately have ?QE
by(simp add:qe_eps1_def bex_Un set_lbounds set_ebounds) metis
} ultimately show ?QE by blast
qed
lemma qfree_asubst_peps: "qfree (asubst+ k a)"
by(cases "(k,a)" rule:asubst_peps.cases) simp_all
lemma qfree_subst_peps: "nqfree φ ==> qfree (subst+ φ k)"
by(induct φ) (simp_all add:qfree_asubst_peps)
lemma qfree_qe_eps1: "nqfree φ ==> qfree(qe_eps1 φ)"
apply(simp add:qe_eps1_def)
apply(rule qfree_list_disj)
apply (auto simp:qfree_min_inf qfree_subst_peps qfree_map_fm)
done
definition "qe_eps = DLO.lift_nnf_qe qe_eps1"
lemma qfree_qe_eps: "qfree(qe_eps φ)"
by(simp add: qe_eps_def DLO.qfree_lift_nnf_qe qfree_qe_eps1)
lemma I_qe_eps: "DLO.I (qe_eps φ) xs = DLO.I φ xs"
by(simp add:qe_eps_def DLO.I_lift_nnf_qe qfree_qe_eps1 I_qe_eps1)
end