# Theory QEdlo_inf

Up to index of Isabelle/HOL/LinearQuantifierElim

theory QEdlo_inf
imports DLO
(*  Author:     Tobias Nipkow, 2007  *)theory QEdlo_infimports DLObeginsubsection "Quantifier elimination with infinitesimals"text{* This section presents a new quantifier elimination procedurefor dense linear orders based on (the simulation of) infinitesimals.It is a fairly straightforward adaptation of the analogous algorithmby 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 blastdonelemma 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 blastdonedeclare[[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  qednext  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_alldeclare[[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])qedlemma 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    donenext  case Or thus ?case by forceqed simp_alldefinition"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 blastnext  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 blastqedlemma qfree_asubst_peps: "qfree (asubst⇣+ k a)"by(cases "(k,a)" rule:asubst_peps.cases) simp_alllemma 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)donedefinition "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