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⇘fm⇙ (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 (fastforce split:split_if_asm)
      apply(case_tac "i≠0 ∧ j=0") apply (fastforce split:split_if_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 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_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:split_if_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