# Theory QEpres

Up to index of Isabelle/HOL/LinearQuantifierElim

theory QEpres
imports PresArith
(*  Author:     Tobias Nipkow, 2007  *)theory QEpresimports PresArithbeginsubsection{*DNF-based quantifier elimination*}(* all hd-coeffs are nonzero! *)definition"hd_coeffs1 as = (let m = zlcms(map hd_coeff as)  in Dvd m 0 [1] # map (hd_coeff1 m) as)"lemma I_hd_coeffs1:assumes 0: "∀a∈set as. hd_coeff a ≠ 0" shows  "(∃x. ∀a ∈ set(hd_coeffs1 as). I⇣Z a (x#xs)) =   (∃x. ∀a ∈ set as. I⇣Z a (x#xs))" (is "?B = ?A")proof -  let ?m = "zlcms(map hd_coeff as)"  have "?m>0" using 0 by(simp add:zlcms_pos)  have "?A = (∃x. ∀a ∈ set as. I⇣Z (hd_coeff1 ?m a) (?m*x#xs))"    by (simp add:I_hd_coeff1_mult_a[OF ?m>0] dvd_zlcms 0)  also have "… = (∃x. ?m dvd x+0 ∧ (∀a ∈ set as. I⇣Z (hd_coeff1 ?m a) (x#xs)))"    by(rule unity_coeff_ex[THEN meta_eq_to_obj_eq])  finally show ?thesis by(simp add:hd_coeffs1_def)qedabbreviation "is_dvd a ≡ case a of Le _ _ => False | _ => True"definition"qe_pres⇣1 as = (let ds = filter is_dvd as; (d::int) = zlcms(map divisor ds); ls = lbounds as  in if ls = []     then Disj [0..d - 1] (λn. list_conj(map (Atom o asubst n []) ds))     else     Disj ls (λ(li,lks).       Disj [0..d - 1] (λn.         list_conj(map (Atom o asubst (li + n) (-lks)) as))))"text{* \noindent Note the optimization in the case @{prop"ls = []"}: only thedivisibility atoms are tested, not the inequalities. This complicatesthe proof. *}lemma I_cyclic:assumes "is_dvd a" and "hd_coeff a = 1" and "i mod divisor a = j mod divisor a"shows "I⇣Z a (i#e) = I⇣Z a (j#e)"proof (cases a)  case (Dvd d l ks)  with hd_coeff a = 1 obtain ks' where [simp]: "ks = 1#ks'"    by(simp split:list.splits)  have "(l + (i + ⟨ks',e⟩)) mod d = (l + (j + ⟨ks',e⟩)) mod d" (is "?l=?r")  proof -    have "?l = (l mod d + (i + ⟨ks',e⟩) mod d) mod d"      by(rule mod_add_eq)    also have "(i + ⟨ks',e⟩) mod d = (i mod d + ⟨ks',e⟩ mod d) mod d"      by(rule mod_add_eq)    also have "i mod d = j mod d"      using i mod divisor a = j mod divisor a Dvd by simp    also have "(j mod d + ⟨ks',e⟩ mod d) mod d = (j + ⟨ks',e⟩) mod d"      by(rule mod_add_eq[symmetric])    also have "(l mod d + (j + ⟨ks',e⟩) mod d) mod d = ?r"      by(rule mod_add_eq[symmetric])    finally show ?thesis .  qed                 thus ?thesis using Dvd by (simp add:dvd_eq_mod_eq_0)next  case (NDvd d l ks)  with hd_coeff a = 1 obtain ks' where [simp]: "ks = 1#ks'"    by(simp split:list.splits)  have "(l + (i + ⟨ks',e⟩)) mod d = (l + (j + ⟨ks',e⟩)) mod d" (is "?l=?r")  proof -    have "?l = (l mod d + (i + ⟨ks',e⟩) mod d) mod d"      by(rule mod_add_eq)    also have "(i + ⟨ks',e⟩) mod d = (i mod d + ⟨ks',e⟩ mod d) mod d"      by(rule mod_add_eq)    also have "i mod d = j mod d"      using i mod divisor a = j mod divisor a NDvd by simp    also have "(j mod d + ⟨ks',e⟩ mod d) mod d = (j + ⟨ks',e⟩) mod d"      by(rule mod_add_eq[symmetric])    also have "(l mod d + (j + ⟨ks',e⟩) mod d) mod d = ?r"      by(rule mod_add_eq[symmetric])    finally show ?thesis .  qed  thus ?thesis using NDvd by (simp add:dvd_eq_mod_eq_0)next  case Le thus ?thesis using is_dvd a by simpqedlemma I_qe_pres⇣1:assumes norm: "∀a ∈ set as. divisor a ≠ 0"and hd: "∀a ∈ set as. hd_coeff_is1 a"shows "Z.I (qe_pres⇣1 as) xs = (∃x. ∀a∈ set as. I⇣Z a (x#xs))"proof -  let ?lbs = "lbounds as"  let ?ds = "filter is_dvd as"  let ?lcm = "zlcms(map divisor ?ds)"  let ?Ds = "{a ∈ set as. is_dvd a}"  let ?Us = "{a ∈ set as. case a of Le _ (k#_) => k < 0 | _ => False}"  let ?Ls = "{a ∈ set as. case a of Le _ (k#_) => k > 0 | _ => False}"  have as: "set as = ?Ds ∪ ?Ls ∪ ?Us" (is "_ = ?S")  proof -    { fix x assume "x ∈ set as"      hence "x ∈ ?S" using hd by (cases x)(auto split:list.splits) }    moreover    { fix x assume "x ∈ ?S"      hence "x ∈ set as" by auto }    ultimately show ?thesis by blast  qed  have 1: "∀a ∈ ?Ds. hd_coeff a = 1" using hd by(fastforce split:atom.splits)  show ?thesis  (is "?QE = (∃x. ?P x)")  proof    assume "?QE"    { assume "?lbs = []"      with ?QE obtain n where "n < ?lcm" and        A: "∀a ∈ ?Ds. I⇣Z a (n#xs)" using 1        by(auto simp:IZ_asubst qe_pres⇣1_def)      have "?Ls = {}" using ?lbs = [] set_lbounds[of as]        by (auto simp add:filter_empty_conv split:atom.split list.split)      have "∃x. ?P x"      proof cases        assume "?Us = {}"        with ?Ls = {} have "set as = ?Ds" using as by(simp (no_asm_use))blast        hence "?P n" using A by auto        thus ?thesis ..      next        assume "?Us ≠ {}"        let ?M = "{⟨tl ks, xs⟩ - i|ks i. Le i ks ∈ ?Us}" let ?m = "Min ?M"        have "finite ?M"        proof -          have "finite ( (λLe i ks => ⟨tl ks, xs⟩ - i)                          {a∈set as. ∃i k ks. k<0 ∧ a = Le i (k#ks)} )"            (is "finite ?B")            by simp          also have "?B = ?M" using hd            by(fastforce simp:image_def neq_Nil_conv split:atom.splits list.splits)          finally show ?thesis by auto        qed        have "?M ≠ {}"        proof -          from ?Us ≠ {} obtain i k ks where "Le i (k#ks) ∈ ?Us ∧ k<0"            by (fastforce split:atom.splits list.splits)          thus ?thesis by auto        qed        let ?k = "(n - ?m) div ?lcm + 1" let ?x = "n - ?k * ?lcm"        have "∀a ∈ ?Ds. I⇣Z a (?x # xs)"        proof (intro allI ballI)          fix a assume "a ∈ ?Ds"          let ?d = "divisor a"          have 2: "?d dvd ?lcm" using a ∈ ?Ds by(simp add:dvd_zlcms)          have "?x mod ?d = n mod ?d" (is "?l = ?r")          proof -            have "?l = (?r - ((?k * ?lcm) mod ?d)) mod ?d"              by(rule mod_diff_eq)            also have "(?k * ?lcm) mod ?d = 0"              by(simp add: dvd_eq_mod_eq_0[symmetric] dvd_mult[OF 2])            finally show ?thesis by simp          qed          thus "I⇣Z a (?x#xs)" using A I_cyclic[of a n ?x] a ∈ ?Ds 1 by auto        qed        moreover        have "∀a∈ ?Us. I⇣Z a (?x#xs)"        proof          fix a assume "a ∈ ?Us"          then obtain l ks where [simp]: "a = Le l (-1#ks)" using hd            by(fastforce split:atom.splits list.splits)          have "?m ≤ ⟨ks,xs⟩ - l"            using Min_le_iff[OF finite ?M ?M ≠ {}] a ∈ ?Us by fastforce          moreover have "(n - ?m) mod ?lcm < ?lcm"            by(simp add: pos_mod_bound[OF zlcms_pos] norm)          ultimately show "I⇣Z a (?x#xs)"            by(simp add:zmult_div_cancel algebra_simps)        qed        moreover        have "set as = ?Ds ∪ ?Us" using as ?Ls = {}          by (simp (no_asm_use)) blast        ultimately have "?P(?x)" by auto        thus ?thesis ..      qed }    moreover    { assume "?lbs ≠ []"      with ?QE obtain il ksl m        where "∀a∈set as. I⇣Z (asubst (il + m) ksl a) xs"        by(auto simp:qe_pres⇣1_def)      hence "?P(il + m + ⟨ksl,xs⟩)" by(simp add:IZ_asubst)      hence "∃x. ?P x" .. }    ultimately show "∃x. ?P x" by blast  next    assume "∃x. ?P x" then obtain x where x: "?P x" ..    show ?QE    proof cases      assume "?lbs = []"      moreover      have "∃x. 0 ≤ x ∧ x < ?lcm ∧ (∀a ∈ ?Ds. I⇣Z a (x # xs))"        (is "∃x. ?P x")      proof        { fix a assume "a ∈ ?Ds"          hence "I⇣Z a ((x mod ?lcm) # xs) = I⇣Z a (x # xs)" using 1            by (fastforce del:iffI intro: I_cyclic                simp: mod_mod_cancel dvd_zlcms) }        thus "?P(x mod ?lcm)" using x norm by(simp add: zlcms_pos)      qed      ultimately show ?thesis by (auto simp:qe_pres⇣1_def IZ_asubst)    next      assume "?lbs ≠ []"      let ?L = "{i - ⟨ks,xs⟩ |ks i. (i,ks) ∈ set(lbounds as)}"      let ?lm = "Max ?L"      let ?n = "(x - ?lm) mod ?lcm"      have "finite ?L"      proof -        have "finite((λ(i,ks). i-⟨ks,xs⟩)  set(lbounds as) )" (is "finite ?B")          by simp        also have "?B = ?L" by auto        finally show ?thesis by auto      qed      moreover have "?L ≠ {}" using ?lbs ≠ []        by(fastforce simp:neq_Nil_conv)      ultimately have "?lm ∈ ?L" by(rule Max_in)      then obtain li lks where "(li,lks)∈ set ?lbs" and lm: "?lm = li-⟨lks,xs⟩"        by blast      moreover      have n: "0 ≤ ?n ∧ ?n < ?lcm" using norm by(simp add:zlcms_pos)      moreover      { fix a assume "a ∈ set as"        with x have "I⇣Z a (x # xs)" by blast        have "I⇣Z a ((li + ?n - ⟨lks,xs⟩) # xs)"        proof -          { assume "a ∈ ?Ls"            then obtain i ks where [simp]: "a = Le i (1#ks)" using hd              by(fastforce split:atom.splits list.splits)            from a ∈ ?Ls have "i-⟨ks,xs⟩ ∈ ?L" by(fastforce simp:set_lbounds)            hence "i-⟨ks,xs⟩ ≤ li - ⟨lks,xs⟩"              using lm[symmetric] finite ?L ?L ≠ {} by auto            hence ?thesis using n by simp }          moreover          { assume "a ∈ ?Us"            then obtain i ks where [simp]: "a = Le i (-1#ks)" using hd              by(fastforce split:atom.splits list.splits)            have "Le li (1#lks) ∈ set as" using (li,lks) ∈ set ?lbs hd              by(auto simp:set_lbounds)            hence "li - ⟨lks,xs⟩ ≤ x" using x by auto            hence "(x - ?lm) mod ?lcm ≤ x - ?lm"              using lm by(simp add: zmod_le_nonneg_dividend)            hence ?thesis using I⇣Z a (x # xs) lm by auto }          moreover          { assume "a ∈ ?Ds"            have ?thesis            proof(rule I_cyclic[THEN iffD2, OF _ _ _ I⇣Z a (x # xs)])              show "is_dvd a" using a ∈ ?Ds by simp              show "hd_coeff a = 1" using a ∈ ?Ds hd                by(fastforce split:atom.splits list.splits)              have "li + (x-?lm) mod ?lcm - ⟨lks,xs⟩ = ?lm + (x-?lm) mod ?lcm"                using lm by arith              hence "(li + (x-?lm) mod ?lcm - ⟨lks,xs⟩) mod divisor a =                     (?lm + (x-?lm) mod ?lcm) mod divisor a" by (simp only:)              also have "… =        (?lm mod divisor a + (x-?lm) mod ?lcm mod divisor a) mod divisor a"                by(rule mod_add_eq)              also have        "… = (?lm mod divisor a + (x-?lm) mod divisor a) mod divisor a"                using is_dvd a a∈ set as                by(simp add: mod_mod_cancel dvd_zlcms)              also have "… = (?lm + (x-?lm)) mod divisor a"                by(rule mod_add_eq[symmetric])              also have "… = x mod divisor a" by simp              finally              show "(li + ?n - ⟨lks,xs⟩) mod divisor a = x mod divisor a"                using norm by(auto simp: zlcms_pos)            qed }          ultimately show ?thesis using a ∈ set as as by blast        qed      }      ultimately show ?thesis using ?lbs ≠ []        by (simp (no_asm_simp) add:qe_pres⇣1_def IZ_asubst split_def)           (force simp del:int_nat_eq)    qed  qedqedlemma  divisors_hd_coeffs1:assumes div0: "∀a∈set as. divisor a ≠ 0" and hd0: "∀a∈set as. hd_coeff a ≠ 0"and a: "a∈set (hd_coeffs1 as)" shows "divisor a ≠ 0"proof -  let ?m = "zlcms(map hd_coeff as)"  from a have "a = Dvd ?m 0 [1] ∨ (∃b ∈ set as. a = hd_coeff1 ?m b)"    (is "?A ∨ ?B")    by(auto simp:hd_coeffs1_def)  thus ?thesis  proof    assume ?A thus ?thesis using hd0 by(auto)  next    assume ?B    then obtain b where "b ∈ set as" and [simp]: "a = hd_coeff1 ?m b" ..    hence b: "hd_coeff b ≠ 0" "divisor b ≠ 0" using div0 hd0 by auto    show ?thesis    proof (cases b)      case (Le i ks) thus ?thesis using b by(auto split:list.splits)    next      case (Dvd d i ks)[simp]      then obtain k ks' where [simp]: "ks = k#ks'" using b        by(auto split:list.splits)      have k: "k ∈ set(map hd_coeff as)" using b ∈ set as by force      have "zlcms (map hd_coeff as) div k ≠ 0"        using b hd0 dvd_zlcms[OF k]        by(auto simp add:dvd_def)      thus ?thesis using b by (simp)    next      case (NDvd d i ks)[simp]      then obtain k ks' where [simp]: "ks = k#ks'" using b        by(auto split:list.splits)      have k: "k ∈ set(map hd_coeff as)" using b ∈ set as by force      have "zlcms (map hd_coeff as) div k ≠ 0"        using b hd0 dvd_zlcms[OF k]        by(auto simp add:dvd_def)      thus ?thesis using b by (simp)    qed  qedqedlemma hd_coeff_is1_hd_coeffs1:assumes hd0: "∀a∈set as. hd_coeff a ≠ 0"and a: "a∈set (hd_coeffs1 as)" shows "hd_coeff_is1 a"proof -  let ?m = "zlcms(map hd_coeff as)"  from a have "a = Dvd ?m 0 [1] ∨ (∃b ∈ set as. a = hd_coeff1 ?m b)"    (is "?A ∨ ?B")    by(auto simp:hd_coeffs1_def)  thus ?thesis  proof    assume ?A thus ?thesis using hd0 by simp  next    assume ?B    then obtain b where "b ∈ set as" and [simp]: "a = hd_coeff1 ?m b" ..    hence b: "hd_coeff b ≠ 0" using hd0 by auto    show ?thesis using b      by (cases b) (auto simp: sgn_if split:list.splits)  qedqedlemma I_qe_pres⇣1_o: "[| ∀a ∈ set as. divisor a ≠ 0; ∀a∈set as. hd_coeff a ≠ 0 |] ==>  Z.I ((qe_pres⇣1 o hd_coeffs1) as) e = (∃x. ∀a∈ set as. I⇣Z a (x#e))"apply(simp)apply(subst I_qe_pres⇣1)  apply(simp add: divisors_hd_coeffs1) apply(simp add: hd_coeff_is1_hd_coeffs1)using I_hd_coeffs1 apply(simp)donedefinition "qe_pres = Z.lift_dnf_qe (qe_pres⇣1 o hd_coeffs1)"lemma qfree_qe_pres_o: "qfree ((qe_pres⇣1 o hd_coeffs1) as)"by(auto simp:qe_pres⇣1_def intro!:qfree_list_disj)lemma normal_qe_pres⇣1_o:  "∀a ∈ set as. hd_coeff a ≠ 0 ∧ divisor a ≠ 0 ==>   Z.normal ((qe_pres⇣1 o hd_coeffs1) as)"apply(auto simp:qe_pres⇣1_def Z.normal_def   dest!:atoms_list_disjE atoms_list_conjE)apply(simp add: hd_coeffs1_def) apply(erule disjE) apply fastforceapply (clarsimp)apply(case_tac xa)  apply(case_tac list) apply fastforce apply (simp split:split_if_asm) apply(case_tac list) apply fastforce apply (simp split:split_if_asm) apply fastforce apply(erule disjE) prefer 2 apply fastforce apply(simp add:zdiv_eq_0_iff) apply(subgoal_tac "a ∈ set(map hd_coeff as)")  prefer 2 apply force apply(subgoal_tac "∀i∈ set(map hd_coeff as). i ≠ 0")  prefer 2 apply simp apply (metis elem_le_zlcms linorder_not_le zlcms_pos)apply(case_tac list) apply fastforceapply (simp split:split_if_asm) apply fastforceapply(simp add:zdiv_eq_0_iff)apply(subgoal_tac "∀i∈ set(map hd_coeff as). i ≠ 0") prefer 2 apply simpapply(subgoal_tac "a ∈ set(map hd_coeff as)") prefer 2 apply forceapply(erule disjE) apply (metis elem_le_zlcms linorder_not_le)apply(erule disjE) apply (metis linorder_not_le zlcms_pos)apply fastforceapply(simp add: hd_coeffs1_def) apply(erule disjE) apply fastforceapply (clarsimp)apply(case_tac xa)  apply(case_tac list) apply fastforce apply (simp split:split_if_asm) apply(case_tac list) apply fastforce apply (simp split:split_if_asm) apply fastforce apply(erule disjE) prefer 2 apply fastforce apply(simp add:zdiv_eq_0_iff) apply(subgoal_tac "a ∈ set(map hd_coeff as)")  prefer 2 apply force apply(subgoal_tac "∀i∈ set(map hd_coeff as). i ≠ 0")  prefer 2 apply simp apply (metis elem_le_zlcms linorder_not_le zlcms_pos)apply(case_tac list) apply fastforceapply (simp split:split_if_asm) apply fastforceapply(simp add:zdiv_eq_0_iff)apply(subgoal_tac "∀i∈ set(map hd_coeff as). i ≠ 0") prefer 2 apply simpapply(subgoal_tac "a ∈ set(map hd_coeff as)") prefer 2 apply forceapply(erule disjE) apply (metis elem_le_zlcms linorder_not_le)apply(erule disjE) apply (metis linorder_not_le zlcms_pos)apply fastforcedonetheorem I_pres_qe: "Z.normal φ ==>  Z.I (qe_pres φ) xs = Z.I φ xs"by(simp add:qe_pres_def Z.I_lift_dnf_qe_anormal I_qe_pres⇣1_o qfree_qe_pres_o normal_qe_pres⇣1_o del:o_apply)theorem qfree_pres_qe: "qfree (qe_pres f)"by(simp add:qe_pres_def Z.qfree_lift_dnf_qe qfree_qe_pres_o del:o_apply)end