Theory QEdlo_inf

(*  Author:     Tobias Nipkow, 2007  *)

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 ≡ amap⇩f⇩m (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

context notes [[simp_depth_limit=3]]
begin

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:if_split_asm nat.splits)
         (metis not_le_imp_less 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 (fastforce split:if_split_asm)
      apply(case_tac "i≠0 ∧ j=0") apply (fastforce split:if_split_asm)
      apply arith
      done
  qed
next
  case And thus ?case by (fastforce)
next
  case Or thus ?case by (fastforce)
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 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 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

end

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_eps⇩1(φ) =
(let as = DLO.atoms⇩0 φ; 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_eps⇩1 φ) xs = (∃x. DLO.I φ (x#xs))"
  (is "?QE = ?EX")
proof
  let ?as = "DLO.atoms⇩0 φ" 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_eps⇩1_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(fastforce simp: I_subst qe_eps⇩1_def set_ebounds set_lbounds)
    then obtain leps where "DLO.I φ (leps#xs)"
      using I_subst_peps[OF ‹nqfree φ›] by fastforce
    hence ?EX .. }
  ultimately show ?EX by blast
next
  let ?as = "DLO.atoms⇩0 φ" 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_eps⇩1_def)
  } moreover
  { assume "∃k ∈ set ?ebs. DLO.I (subst φ k) xs"
    hence ?QE by(auto simp:qe_eps⇩1_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:if_split_asm)
    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›] ..
    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 have "DLO.I (subst⇩+ φ m) xs"
      using noE by(auto intro!: I_subst_peps2[OF ‹nqfree φ›])
    with * have ?QE
      by(simp add:qe_eps⇩1_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_eps⇩1: "nqfree φ ⟹ qfree(qe_eps⇩1 φ)"
apply(simp add:qe_eps⇩1_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_eps⇩1"

lemma qfree_qe_eps: "qfree(qe_eps φ)"
by(simp add: qe_eps_def DLO.qfree_lift_nnf_qe qfree_qe_eps⇩1)

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_eps⇩1 I_qe_eps1)

end