# Theory QElin

Up to index of Isabelle/HOL/LinearQuantifierElim

theory QElin
imports LinArith
`(*  Author:     Tobias Nipkow, 2007  *)theory QElinimports LinArithbeginsubsection{* Fourier *}definition qe_FM⇣1 :: "atom list => atom fm" where"qe_FM⇣1 as = list_conj [Atom(combine p q). p\<leftarrow>lbounds as, q\<leftarrow>ubounds as]"theorem I_qe_FM⇣1:assumes less: "∀a ∈ set as. is_Less a" and dep: "∀a ∈ set as. depends⇣R a"shows "R.I (qe_FM⇣1 as) xs = (∃x. ∀a ∈ set as. I⇣R a (x#xs))"  (is "?L = ?R")proof  let ?Ls = "set(lbounds as)" let ?Us = "set(ubounds as)"  let ?lbs = "UN (r,cs):?Ls. {r + ⟨cs,xs⟩}"  let ?ubs = "UN (r,cs):?Us. {r + ⟨cs,xs⟩}"  have fins: "finite ?lbs ∧ finite ?ubs" by auto  have 2: "∀f∈ set as. ∃r c cs. f = Less r (c#cs) ∧          (c>0 ∧ (r/c,(-1/c)*⇩s cs) ∈ ?Ls ∨ c<0 ∧ (r/c,(-1/c)*⇩s cs) ∈ ?Us)"    using dep less    by(fastforce simp:set_lbounds set_ubounds is_Less_iff depends⇣R_def                split:list.splits)  assume ?L  have 1: "∀x∈?lbs. ∀y∈?ubs. x < y"  proof (rule ballI)+    fix x y assume "x∈?lbs" "y∈?ubs"    then obtain r cs      where "(r,cs) ∈ ?Ls ∧ x = r + ⟨cs,xs⟩" by fastforce    moreover from `y∈?ubs` obtain s ds      where "(s,ds) ∈ ?Us ∧ y = s + ⟨ds,xs⟩" by fastforce    ultimately show "x<y" using `?L`      by(fastforce simp:qe_FM⇣1_def algebra_simps iprod_left_diff_distrib)  qed  { assume nonempty: "?lbs ≠ {} ∧ ?ubs ≠ {}"    hence "Max ?lbs < Min ?ubs" using fins 1      by(blast intro: Max_less_iff[THEN iffD2] Min_gr_iff[THEN iffD2])    then obtain m where "Max ?lbs < m ∧ m < Min ?ubs"      using dense[where 'a = real] by blast    hence "∀a ∈ set as. I⇣R a (m#xs)" using 2 nonempty      by (auto simp:Ball_def Bex_def)(fastforce simp:field_simps)    hence ?R .. }  moreover  { assume asm: "?lbs ≠ {} ∧ ?ubs = {}"    have "∀a ∈ set as. I⇣R a ((Max ?lbs + 1) # xs)"    proof      fix a assume "a ∈ set as"      then obtain r c cs        where "a = Less r (c#cs)" "c>0" "(r/c,(-1/c)*⇩s cs) ∈ ?Ls"        using asm 2 by fastforce      moreover hence "(r - ⟨cs,xs⟩)/c ≤ Max ?lbs"        using asm fins        by(auto intro!: Max_ge_iff[THEN iffD2])          (force simp add:field_simps)      ultimately show "I⇣R a ((Max ?lbs + 1) # xs)" by (simp add: field_simps)    qed    hence ?R .. }  moreover  { assume asm: "?lbs = {} ∧ ?ubs ≠ {}"    have "∀a ∈ set as. I⇣R a ((Min ?ubs - 1) # xs)"    proof      fix a assume "a ∈ set as"      then obtain r c cs        where "a = Less r (c#cs)" "c<0" "(r/c,(-1/c)*⇩s cs) ∈ ?Us"        using asm 2 by fastforce      moreover hence "Min ?ubs ≤ (r - ⟨cs,xs⟩)/c"        using asm fins        by(auto intro!: Min_le_iff[THEN iffD2])          (force simp add:field_simps)      ultimately show "I⇣R a ((Min ?ubs - 1) # xs)" by (simp add: field_simps)    qed    hence ?R .. }  moreover  { assume "?lbs = {} ∧ ?ubs = {}"    hence ?R using 2 less by auto (rule, fast)  }  ultimately show ?R by blastnext  let ?Ls = "set(lbounds as)" let ?Us = "set(ubounds as)"  assume ?R  then obtain x where 1: "∀a∈ set as. I⇣R a (x#xs)" ..  { fix r c cs s d ds    assume "Less r (c#cs) ∈ set as" "0 < c" "Less s (d#ds) ∈ set as" "d < 0"    hence "r < c*x + ⟨cs,xs⟩" "s < d*x + ⟨ds,xs⟩" "c > 0" "d < 0"      using 1 by auto    hence "(r - ⟨cs,xs⟩)/c < x" "x < (s - ⟨ds,xs⟩)/d" by(simp add:field_simps)+    hence "(r - ⟨cs,xs⟩)/c < (s - ⟨ds,xs⟩)/d" by arith  }  thus ?L by (auto simp: qe_FM⇣1_def iprod_left_diff_distrib less field_simps set_lbounds set_ubounds)qedcorollary I_qe_FM⇣1_pretty:  "∀a ∈ set as. is_Less a ∧ depends⇣R a ==> R.is_dnf_qe qe_FM⇣1 as"by(metis I_qe_FM⇣1)fun subst⇣0 :: "atom => atom => atom" where"subst⇣0 (Eq r (c#cs)) a = (case a of   Less s (d#ds) => Less (s - (r*d)/c) (ds - (d/c) *⇩s cs) | Eq s (d#ds) => Eq (s - (r*d)/c) (ds - (d/c) *⇩s cs))"lemma subst⇣0_pretty: "subst⇣0 (Eq r (c#cs)) (Less s (d#ds)) = Less (s - (r*d)/c) (ds - (d/c) *⇩s cs)" "subst⇣0 (Eq r (c#cs)) (Eq s (d#ds)) = Eq (s - (r*d)/c) (ds - (d/c) *⇩s cs)"by autolemma I_subst⇣0: "depends⇣R a ==> c ≠ 0 ==>       I⇣R (subst⇣0 (Eq r (c#cs)) a) xs = I⇣R a ((r - ⟨cs,xs⟩)/c # xs)"apply(cases a)by (auto simp add: depends⇣R_def iprod_left_diff_distrib algebra_simps diff_divide_distrib split:list.splits)interpretation R⇣e!:  ATOM_EQ neg⇣R "(λa. True)" I⇣R depends⇣R decr⇣R          "(λEq _ (c#_) => c ≠ 0 | _ => False)"          "(λEq r cs => r=0 ∧ (∀c∈ set cs. c=0) | _ => False)" subst⇣0apply(unfold_locales)   apply(simp del:subst⇣0.simps add:I_subst⇣0 split:atom.splits list.splits)  apply(simp add: iprod0_if_coeffs0 split:atom.splits) apply(simp split:atom.splits list.splits) apply(rename_tac r ds c cs) apply(rule_tac x= "(r - ⟨cs,xs⟩)/c" in exI) apply (simp add: algebra_simps diff_divide_distrib)apply(simp add: self_list_diff set_replicate_conv_if        split:atom.splits list.splits)done(* FIXME does not helpsetup {* Sign.revert_abbrev "" @{const_name R⇣e.lift_dnfeq_qe} *}*)definition "qe_FM = R⇣e.lift_dnfeq_qe qe_FM⇣1"lemma qfree_qe_FM⇣1: "qfree (qe_FM⇣1 as)"by(auto simp:qe_FM⇣1_def intro!:qfree_list_conj)corollary I_qe_FM: "R.I (qe_FM φ) xs = R.I φ xs"unfolding qe_FM_defapply(rule R⇣e.I_lift_dnfeq_qe) apply(rule qfree_qe_FM⇣1)apply(rule allI)apply(rule I_qe_FM⇣1) prefer 2 apply blastapply(clarify)apply(drule_tac x=a in bspec) apply simpapply(simp add: depends⇣R_def split:atom.splits list.splits)donetheorem qfree_qe_FM: "qfree (qe_FM f)"by(simp add:qe_FM_def R⇣e.qfree_lift_dnfeq_qe qfree_qe_FM⇣1)subsubsection{* Tests *}lemmas qesimps = qe_FM_def R⇣e.lift_dnfeq_qe_def R⇣e.lift_eq_qe_def R.qelim_def qe_FM⇣1_def lbounds_def ubounds_def list_conj_def list_disj_def and_def or_def depends⇣R_deflemma "qe_FM(TrueF) = TrueF"by(simp add:qesimps)lemma  "qe_FM(ExQ (And (Atom(Less 0 [1])) (Atom(Less 0 [-1])))) = Atom(Less 0 [])"by(simp add:qesimps)lemma "qe_FM(ExQ (And (Atom(Less 0 [1])) (Atom(Less -1 [-1])))) = Atom(Less -1 [])"by(simp add:qesimps)end`