# Theory QElin_inf

Up to index of Isabelle/HOL/LinearQuantifierElim

theory QElin_inf
imports LinArith
(*  Author:     Tobias Nipkow, 2007  *)theory QElin_infimports LinArithbeginsubsection {*Quantifier elimination with infinitesimals \label{sec:lin-inf}*}text{* This section formalizes Loos and Weispfenning's quantifierelimination procedure based on (the simulation of)infinitesimals~\cite{LoosW93}. *}fun asubst_peps :: "real * real list => atom => atom fm" ("asubst⇣+") where"asubst_peps (r,cs) (Less s (d#ds)) =  (if d=0 then Atom(Less s ds) else   let u = s - d*r; v = d *⇩s cs + ds; less = Atom(Less u v)   in if d<0 then less else Or less (Atom(Eq u v)))" |"asubst_peps rcs (Eq r (d#ds)) = (if d=0 then Atom(Eq r ds) else FalseF)" |"asubst_peps rcs a = Atom a"abbreviation subst_peps :: "atom fm => real * real list => atom fm" ("subst⇣+")where "subst⇣+ φ rcs ≡ amap⇘fm⇙ (asubst⇣+ rcs) φ"definition "nolb f xs l x = (∀y∈{l<..<x}. y ∉ LB f xs)"lemma nolb_And[simp]:  "nolb (And f g) xs l x = (nolb f xs l x ∧ nolb g xs l x)"apply(clarsimp simp:nolb_def)apply blastdonelemma nolb_Or[simp]:  "nolb (Or f g) xs l x = (nolb f xs l x ∧ nolb g xs l x)"apply(clarsimp simp:nolb_def)apply blastdonedeclare[[simp_depth_limit=4]]lemma innermost_intvl:  "[| nqfree f; nolb f xs l x; l < x; x ∉ EQ f xs; R.I f (x#xs); l < y; y ≤ x|]  ==> R.I f (y#xs)"proof(induct f)  case (Atom a)  show ?case  proof (cases a)    case (Less r cs)[simp]    show ?thesis    proof (cases cs)      case Nil thus ?thesis using Atom by (simp add:depends⇣R_def)    next      case (Cons c cs)[simp]      hence "r < c*x + ⟨cs,xs⟩" using Atom by simp      { assume "c=0" hence ?thesis using Atom by simp }      moreover      { assume "c<0"        hence "x < (r - ⟨cs,xs⟩)/c" (is "_ < ?u") using r < c*x + ⟨cs,xs⟩          by (simp add: field_simps)        have ?thesis        proof (rule ccontr)          assume "¬ R.I (Atom a) (y#xs)"          hence "?u ≤ y" using Atom c<0            by (auto simp add: field_simps)          with x<?u show False using Atom c<0            by(auto simp:depends⇣R_def)        qed } moreover      { assume "c>0"        hence "x > (r - ⟨cs,xs⟩)/c" (is "_ > ?l") using r < c*x + ⟨cs,xs⟩          by (simp add: field_simps)        then have "?l < y" using Atom c>0            by (auto simp:depends⇣R_def Ball_def nolb_def)               (metis linorder_not_le antisym order_less_trans)        hence ?thesis using c>0 by (simp add: field_simps)      } ultimately show ?thesis by force    qed  next    case (Eq r cs)[simp]    show ?thesis    proof (cases cs)      case Nil thus ?thesis using Atom by (simp add:depends⇣R_def)    next      case (Cons c cs)[simp]      hence "r = c*x + ⟨cs,xs⟩" using Atom by simp      { assume "c=0" hence ?thesis using Atom by simp }      moreover      { assume "c≠0"        hence ?thesis using r = c*x + ⟨cs,xs⟩ Atom          by(auto simp: mult_ac depends⇣R_def split:if_splits) }      ultimately show ?thesis by force    qed  qednext  case (And f1 f2) thus ?case by (fastforce)next  case (Or f1 f2) thus ?case by (fastforce)qed simp+definition "EQ2 = EQ"lemma EQ2_Or[simp]: "EQ2 (Or f g) xs = (EQ2 f xs Un EQ2 g xs)"by(auto simp:EQ2_def)lemma EQ2_And[simp]: "EQ2 (And f g) xs = (EQ2 f xs Un EQ2 g xs)"by(auto simp:EQ2_def)lemma innermost_intvl2:  "[| nqfree f; nolb f xs l x; l < x; x ∉ EQ2 f xs; R.I f (x#xs); l < y; y ≤ x|]  ==> R.I f (y#xs)"unfolding EQ2_def by(blast intro:innermost_intvl)lemma I_subst_peps2: "nqfree f ==> r+⟨cs,xs⟩ < x ==> nolb f xs (r+⟨cs,xs⟩) x ==> ∀y ∈ {r+⟨cs,xs⟩ <.. x}. R.I f (y#xs) ∧ y ∉ EQ2 f xs ==> R.I (subst⇣+ f (r,cs)) xs"proof(induct f)  case FalseF thus ?case    by simp (metis linorder_antisym_conv1 linorder_neq_iff)next  case (Atom a)  show ?case  proof(cases "((r,cs),a)" rule:asubst_peps.cases)    case (1 r cs s d ds)    { assume "d=0" hence ?thesis using Atom 1 by auto }    moreover    { assume "d<0"      have "s < d*x + ⟨ds,xs⟩" using Atom 1 by simp      moreover have "d*x < d*(r + ⟨cs,xs⟩)" using d<0 Atom 1        by (simp add: mult_strict_left_mono_neg)      ultimately have "s < d * (r + ⟨cs,xs⟩) + ⟨ds,xs⟩" by(simp add:algebra_simps)      hence ?thesis using 1        by (auto simp add: iprod_left_add_distrib algebra_simps)    } moreover    { let ?L = "(s - ⟨ds,xs⟩) / d" let ?U = "r + ⟨cs,xs⟩"      assume "d>0"      hence "?U < x" and "∀y. ?U < y ∧ y < x --> y ≠ ?L"        and "∀y. ?U < y ∧ y ≤ x --> ?L < y" using Atom 1        by(simp_all add:nolb_def depends⇣R_def Ball_def field_simps)      hence "?L < ?U ∨ ?L = ?U"        by (metis linorder_neqE_linordered_idom order_refl)      hence ?thesis using Atom 1 d>0        by (simp add: iprod_left_add_distrib field_simps)    } ultimately show ?thesis by force  next    case 2 thus ?thesis using Atom      by(fastforce simp:nolb_def EQ2_def depends⇣R_def field_simps split:split_if_asm)  qed (insert Atom, auto)next  case Or thus ?case by(simp add:Ball_def)(metis order_refl innermost_intvl2)qed simp_alldeclare[[simp_depth_limit=50]]lemma I_subst_peps:  "nqfree f ==> R.I (subst⇣+ f (r,cs)) xs ==>  (∃leps>r+⟨cs,xs⟩. ∀x. r+⟨cs,xs⟩ < x ∧ x ≤ leps --> R.I f (x#xs))"proof(induct f)  case TrueF thus ?case by simp (metis less_add_one)next  case (Atom a)  show ?case  proof (cases "((r,cs),a)" rule: asubst_peps.cases)    case (1 r cs s d ds)    { assume "d=0" hence ?thesis using Atom 1 by auto (metis less_add_one) }    moreover    { assume "d<0"      with Atom 1 have "r + ⟨cs,xs⟩ < (s - ⟨ds,xs⟩)/d" (is "?a < ?b")        by(simp add:field_simps iprod_left_add_distrib)      then obtain x where "?a < x" "x < ?b" by(metis dense)      hence " ∀y. ?a < y ∧ y ≤ x --> s < d*y + ⟨ds,xs⟩"        using d<0 by (simp add:field_simps)      (metis add_le_cancel_right mult_le_cancel_left order_antisym linear mult_commute xt1(8))      hence ?thesis using 1 ?a<x by auto    } moreover    { let ?a = "s - d * r" let ?b = "⟨d *⇩s cs + ds,xs⟩"      assume "d>0"      with Atom 1 have "?a < ?b ∨ ?a = ?b" by auto      hence ?thesis      proof        assume "?a = ?b"        thus ?thesis using d>0 Atom 1          by(simp add:field_simps iprod_left_add_distrib)            (metis add_0_left add_less_cancel_right distrib_left mult_commute mult_strict_left_mono)      next        assume "?a < ?b"        { fix x assume "r+⟨cs,xs⟩ < x ∧ x ≤ r+⟨cs,xs⟩ + 1"          hence "d*(r + ⟨cs,xs⟩) < d*x"            using d>0 by(metis mult_strict_left_mono)          hence "s < d*x + ⟨ds,xs⟩" using d>0 ?a < ?b            by (simp add:algebra_simps iprod_left_add_distrib)        }        thus ?thesis using 1 d>0          by(force simp: iprod_left_add_distrib)      qed    } ultimately show ?thesis by (metis less_linear)  qed (insert Atom, auto split:split_if_asm intro: less_add_one)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_alllemma dense_interval:assumes "finite L" "l ∈ L" "l < x" "P(x::real)"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])qeddefinition"qe_eps⇣1(f) =(let as = R.atoms⇣0 f; lbs = lbounds as; ebs = ebounds as in list_disj (inf⇣- f # map (subst⇣+ f) lbs @ map (subst f) ebs))"theorem I_eps1:assumes "nqfree f" shows "R.I (qe_eps⇣1 f) xs = (∃x. R.I f (x#xs))"  (is "?QE = ?EX")proof  let ?as = "R.atoms⇣0 f" let ?ebs = "ebounds ?as"  assume ?QE  { assume "R.I (inf⇣- f) xs"    hence ?EX using ?QE min_inf[of f xs] nqfree f      by(auto simp add:qe_eps⇣1_def amap_fm_list_disj)  } moreover  { assume "∀x ∈ EQ f xs. ¬R.I f (x#xs)"           "¬ R.I (inf⇣- f) xs"    with ?QE nqfree f obtain r cs where "R.I (subst⇣+ f (r,cs)) xs"      by(fastforce simp:qe_eps⇣1_def set_ebounds diff_divide_distrib eval_def        diff_minus[symmetric] I_subst nqfree f)    then obtain leps where "R.I f (leps#xs)"      using I_subst_peps[OF nqfree f] by fastforce    hence ?EX .. }  ultimately show ?EX by blastnext  let ?as = "R.atoms⇣0 f" let ?ebs = "ebounds ?as"  assume ?EX  then obtain x where x: "R.I f (x#xs)" ..  { assume "R.I (inf⇣- f) xs"    hence ?QE using nqfree f by(auto simp:qe_eps⇣1_def)  } moreover  { assume "∃rcs ∈ set ?ebs. R.I (subst f rcs) xs"    hence ?QE by(auto simp:qe_eps⇣1_def) } moreover  { assume "¬ R.I (inf⇣- f) xs"    and "∀rcs ∈ set ?ebs. ¬ R.I (subst f rcs) xs"    hence noE: "∀e ∈ EQ f xs. ¬ R.I f (e#xs)" using nqfree f      by (force simp:set_ebounds I_subst diff_divide_distrib eval_def        diff_minus[symmetric] split:split_if_asm)    hence "x ∉ EQ f xs" using x by fastforce    obtain l where "l ∈ LB f xs" "l < x"      using LBex[OF nqfree f x ¬ R.I(inf⇣- f) xs x ∉ EQ f xs] ..    have "∃l∈LB f xs. l<x ∧ nolb f xs l x ∧            (∀y. l < y ∧ y ≤ x --> R.I f (y#xs))"      using dense_interval[where P = "λx. R.I f (x#xs)", OF finite_LB l∈LB f xs l<x x] x innermost_intvl[OF nqfree f _ _ x ∉ EQ f xs]      by (simp add:nolb_def)    then obtain r c cs      where *: "Less r (c#cs) ∈ set(R.atoms⇣0 f) ∧ c>0 ∧            (r - ⟨cs,xs⟩)/c < x ∧ nolb f xs ((r - ⟨cs,xs⟩)/c) x            ∧ (∀y. (r - ⟨cs,xs⟩)/c < y ∧ y ≤ x --> R.I f (y#xs))"      by blast    then have "R.I (subst⇣+ f (r/c, (-1/c) *⇩s cs)) xs" using noE      by(auto intro!: I_subst_peps2[OF nqfree f]        simp:EQ2_def diff_divide_distrib algebra_simps)    with * have ?QE      by(simp add:qe_eps⇣1_def bex_Un set_lbounds) metis  } ultimately show ?QE by blastqedlemma qfree_asubst_peps: "qfree (asubst⇣+ rcs a)"by(cases "(rcs,a)" rule:asubst_peps.cases) simp_alllemma qfree_subst_peps: "nqfree φ ==> qfree (subst⇣+ φ rcs)"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 = R.lift_nnf_qe qe_eps⇣1"lemma qfree_qe_eps: "qfree(qe_eps φ)"by(simp add: qe_eps_def R.qfree_lift_nnf_qe qfree_qe_eps⇣1)lemma I_qe_eps: "R.I (qe_eps φ) xs = R.I φ xs"by(simp add:qe_eps_def R.I_lift_nnf_qe qfree_qe_eps⇣1 I_eps1)end