Theory QEdlo_fr

(*  Author:     Tobias Nipkow, 2007  *)

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 asubst⇩2 :: "nat ⇒ nat ⇒ atom ⇒ atom fm" where
"asubst⇩2 l u (Less 0 0) = FalseF" |
"asubst⇩2 l u (Less 0 (Suc j)) = Or (Atom(Less u j)) (Atom(Eq u j))" |
"asubst⇩2 l u (Less (Suc i) 0) = Or (Atom(Less i l)) (Atom(Eq i l))" |
"asubst⇩2 l u (Less (Suc i) (Suc j)) = Atom(Less i j)" |
"asubst⇩2 l u (Eq 0 0) = TrueF" |
"asubst⇩2 l u (Eq 0 _) = FalseF" |
"asubst⇩2 l u (Eq _ 0) = FalseF" |
"asubst⇩2 l u (Eq (Suc i) (Suc j)) = Atom(Eq i j)"

abbreviation "subst⇩2 l u ≡ amap⇩f⇩m (asubst⇩2 l u)"

lemma I_subst⇩21:
 "nqfree f ⟹ xs!l < xs!u ⟹ DLO.I (subst⇩2 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: asubst⇩2.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)

context notes [[simp_depth_limit=3]]
begin

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:if_split_asm nat.splits)
         (metis not_le_imp_less order_antisym order_less_trans)+
  next
    case [simp]: (Eq i j)
    show ?thesis
    proof (cases i)
      case [simp]: 0
      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 [simp]: Suc
      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 (fastforce)
next
  case (Or f1 f2) thus ?case by (fastforce)
qed simp+

lemma I_subst⇩22:
 "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 (subst⇩2 l u f) xs"
proof (induct f)
  case (Atom a) show ?case
    apply (cases "(l,u,a)" rule: asubst⇩2.cases)
    apply(insert Atom, auto simp: EQ_def nolub_def split:if_split_asm)
    done
next
  case Or thus ?case by (simp add: Ball_def)(metis innermost_intvl)
qed auto

end

definition
"qe_interior⇩1 φ =
(let as = DLO.atoms⇩0 φ; lbs = lbounds as; ubs = ubounds as; ebs = ebounds as;
     intrs = [And (Atom(Less l u)) (subst⇩2 l u φ). l←lbs, u←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_interior⇩1 φ) xs = (∃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_interior⇩1_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_interior⇩1_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 (subst⇩2 l u φ) xs" and "xs!l < xs!u"
      by(fastforce simp: qe_interior⇩1_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_subst⇩21[OF ‹nqfree φ› ‹xs!l < xs!u›] by simp
    hence ?EX .. }
  ultimately show ?EX by blast
next
  let ?as = "DLO.atoms⇩0 φ" 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_interior⇩1_def)
  } moreover
  { assume "∃k ∈ ?E. DLO.I (subst φ k) xs"
    hence ?QE by(force simp:qe_interior⇩1_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 fastforce
    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)
    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 (subst⇩2 m n φ) xs" using noE
      by(force intro!: I_subst⇩22[OF ‹nqfree φ›])
    ultimately have ?QE
      by(fastforce simp add:qe_interior⇩1_def bex_Un set_lbounds set_ubounds)
  } ultimately show ?QE by blast
qed

lemma qfree_asubst⇩2: "qfree (asubst⇩2 l u a)"
by(cases "(l,u,a)" rule:asubst⇩2.cases) simp_all

lemma qfree_subst⇩2: "nqfree φ ⟹ qfree (subst⇩2 l u φ)"
by(induct φ) (simp_all add:qfree_asubst⇩2)

lemma qfree_interior1: "nqfree φ ⟹ qfree(qe_interior⇩1 φ)"
apply(simp add:qe_interior⇩1_def)
apply(rule qfree_list_disj)
apply (auto simp:qfree_min_inf qfree_plus_inf qfree_subst⇩2 qfree_map_fm)
done


definition "qe_interior = DLO.lift_nnf_qe qe_interior⇩1"

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