# Theory PresArith

Up to index of Isabelle/HOL/LinearQuantifierElim

theory PresArith
imports GCD QE ListVector
`(*  Author:     Tobias Nipkow, 2007  *)header{* Presburger arithmetic *}theory PresArithimports GCD QE "~~/src/HOL/Library/ListVector"begindeclare iprod_assoc[simp]subsection{*Syntax*}datatype atom =  Le int "int list" | Dvd int int "int list" | NDvd int int "int list"fun divisor :: "atom => int" where"divisor (Le i ks) = 1" |"divisor (Dvd d i ks) = d" |"divisor (NDvd d i ks) = d"fun neg⇣Z :: "atom => atom fm" where"neg⇣Z (Le i ks) = Atom(Le (1-i) (-ks))" |"neg⇣Z (Dvd d i ks) = Atom(NDvd d i ks)" |"neg⇣Z (NDvd d i ks) = Atom(Dvd d i ks)"fun hd_coeff :: "atom => int" where"hd_coeff (Le i ks) = (case ks of [] => 0 | k#_ => k)" |"hd_coeff (Dvd d i ks) = (case ks of [] => 0 | k#_ => k)" |"hd_coeff (NDvd d i ks) = (case ks of [] => 0 | k#_ => k)"fun decr⇣Z :: "atom => atom" where"decr⇣Z (Le i ks) = Le i (tl ks)" |"decr⇣Z (Dvd d i ks) = Dvd d i (tl ks)" |"decr⇣Z (NDvd d i ks) = NDvd d i (tl ks)"fun I⇣Z :: "atom => int list => bool" where"I⇣Z (Le i ks) xs = (i ≤ ⟨ks,xs⟩)" |"I⇣Z (Dvd d i ks) xs = (d dvd i+⟨ks,xs⟩)" |"I⇣Z (NDvd d i ks) xs = (¬ d dvd i+⟨ks,xs⟩)"definition "atoms⇣0 = ATOM.atoms⇣0 (λa. hd_coeff a ≠ 0)"(* FIXME !!! (incl: display should hide params)*)interpretation Z!:  ATOM neg⇣Z "(λa. divisor a ≠ 0)" I⇣Z "(λa. hd_coeff a ≠ 0)" decr⇣Z  where "ATOM.atoms⇣0 (λa. hd_coeff a ≠ 0) = atoms⇣0"proof-  case goal1  thus ?caseapply(unfold_locales)apply(case_tac a)apply simp_allapply(case_tac a)apply simp_allapply(case_tac a)apply (simp_all)apply arithapply(case_tac a)apply(simp_all add: split: list.splits)apply(case_tac a)apply simp_alldonenext  case goal2 thus ?case by(simp add:atoms⇣0_def)qedsetup {* Sign.revert_abbrev "" @{const_abbrev Z.I} *}setup {* Sign.revert_abbrev "" @{const_abbrev Z.lift_dnf_qe} *}(* FIXME doesn't work*)(* FIXME does not helpsetup {* Sign.revert_abbrev "" @{const_abbrev Z.normal} *}*)abbreviation"hd_coeff_is1 a ≡  (case a of Le _ _ => hd_coeff a : {1,-1} | _ => hd_coeff a = 1)"fun asubst :: "int => int list => atom => atom" where"asubst i' ks' (Le i (k#ks)) = Le (i - k*i') (k *⇩s ks' + ks)" |"asubst i' ks' (Dvd d i (k#ks)) = Dvd d (i + k*i') (k *⇩s ks' + ks)" |"asubst i' ks' (NDvd d i (k#ks)) = NDvd d (i + k*i') (k *⇩s ks' + ks)" |"asubst i' ks' a = a"abbreviation subst :: "int => int list => atom fm => atom fm"where "subst i ks ≡ map⇘fm⇙ (asubst i ks)"lemma IZ_asubst: "I⇣Z (asubst i ks a) xs = I⇣Z a ((i + ⟨ks,xs⟩) # xs)"apply (cases a)apply (case_tac list)apply (simp_all add:algebra_simps iprod_left_add_distrib)apply (case_tac list)apply (simp_all add:algebra_simps iprod_left_add_distrib)apply (case_tac list)apply (simp_all add:algebra_simps iprod_left_add_distrib)donelemma I_subst:  "qfree φ ==> Z.I φ ((i + ⟨ks,xs⟩) # xs) = Z.I (subst i ks φ) xs"by (induct φ) (simp_all add:IZ_asubst)lemma divisor_asubst[simp]: "divisor (asubst i ks a) = divisor a"by(induct i ks a rule:asubst.induct) autodefinition "lbounds as = [(i,ks). Le i (k#ks) \<leftarrow> as, k>0]"definition "ubounds as = [(i,ks). Le i (k#ks) \<leftarrow> as, k<0]"lemma set_lbounds:  "set(lbounds as) = {(i,ks)|i k ks. Le i (k#ks) : set as ∧ k>0}"by(auto simp: lbounds_def split:list.splits atom.splits if_splits)lemma set_ubounds:  "set(ubounds as) = {(i,ks)|i k ks. Le i (k#ks) : set as ∧ k<0}"by(auto simp: ubounds_def split:list.splits atom.splits if_splits)lemma lbounds_append[simp]: "lbounds(as @ bs) = lbounds as @ lbounds bs"by(simp add:lbounds_def)subsection{*LCM and lemmas*}fun zlcms :: "int list => int" where"zlcms [] = 1" |"zlcms (i#is) = lcm i (zlcms is)"lemma dvd_zlcms: "i : set is ==> i dvd zlcms is"by(induct "is") autolemma zlcms_pos: "∀i ∈ set is. i≠0 ==> zlcms is > 0"by(induct "is")(auto simp:lcm_pos_int)lemma zlcms0_iff[simp]: "(zlcms is = 0) = (0 : set is)"by (metis mod_by_0 dvd_eq_mod_eq_0 dvd_zlcms zlcms_pos less_le)lemma elem_le_zlcms: "∀i ∈ set is. i ≠ 0 ==> i : set is ==> i ≤ zlcms is"by (metis dvd_zlcms zdvd_imp_le zlcms_pos)subsection{* Setting coeffiencients to 1 or -1 *}fun hd_coeff1 :: "int => atom => atom" where"hd_coeff1 m (Le i (k#ks)) =   (if k=0 then Le i (k#ks)    else let m' = m div (abs k) in Le (m'*i) (sgn k # (m' *⇩s ks)))" |"hd_coeff1 m (Dvd d i (k#ks)) =   (if k=0 then Dvd d i (k#ks)    else let m' = m div k in Dvd (m'*d) (m'*i) (1 # (m' *⇩s ks)))" |"hd_coeff1 m (NDvd d i (k#ks)) =   (if k=0 then NDvd d i (k#ks)    else let m' = m div k in NDvd (m'*d) (m'*i) (1 # (m' *⇩s ks)))" |"hd_coeff1 _ a = a"text{* The def of @{const hd_coeff1} on @{const Dvd} and @{const NDvd} isdifferent from the @{const Le} because it allows the resulting headcoefficient to be 1 rather than 1 or -1. We show that the other version hasthe same semantics: *}lemma "[| k ≠ 0; k dvd m |] ==>  I⇣Z (hd_coeff1 m (Dvd d i (k#ks))) (x#e) = (let m' = m div (abs k) in  I⇣Z (Dvd (m'*d) (m'*i) (sgn k # (m' *⇩s ks))) (x#e))"apply(auto simp:algebra_simps abs_if sgn_if) apply(simp add: zdiv_zminus2_eq_if dvd_eq_mod_eq_0[THEN iffD1] algebra_simps) apply (metis diff_minus add_left_commute dvd_minus_iff minus_add_distrib)apply(simp add: zdiv_zminus2_eq_if dvd_eq_mod_eq_0[THEN iffD1] algebra_simps)apply (metis diff_minus add_left_commute dvd_minus_iff minus_add_distrib)donelemma I_hd_coeff1_mult_a: assumes "m>0"shows "hd_coeff a dvd m | hd_coeff a = 0 ==> I⇣Z (hd_coeff1 m a) (m*x#xs) = I⇣Z a (x#xs)"proof(induct a)  case (Le i ks)[simp]  show ?case  proof(cases ks)    case Nil thus ?thesis by simp  next    case (Cons k ks')[simp]    show ?thesis    proof cases      assume "k=0" thus ?thesis by simp    next      assume "k≠0"      with Le have "¦k¦ dvd m" by simp      let ?m' = "m div ¦k¦"      have "?m' > 0" using `¦k¦ dvd m` pos_imp_zdiv_pos_iff `m>0` `k≠0`        by(simp add:zdvd_imp_le)      have 1: "k*(x*?m') = sgn k * x * m"      proof -        have "k*(x*?m') = (sgn k * abs k) * (x * ?m')"          by(simp only: mult_sgn_abs)        also have "… = sgn k * x * (abs k * ?m')" by simp        also have "… = sgn k * x * m"          using dvd_mult_div_cancel[OF `¦k¦ dvd m`] by(simp add:algebra_simps)        finally show ?thesis .      qed      have "I⇣Z (hd_coeff1 m (Le i ks)) (m*x#xs) <->            (i*?m' ≤ sgn k * m*x + ?m' * ⟨ks',xs⟩)"        using `k≠0` by(simp add: algebra_simps)      also have "… <-> ?m'*i ≤ ?m' * (k*x + ⟨ks',xs⟩)" using 1        by(simp (no_asm_simp) add:algebra_simps)      also have "… <-> i ≤ k*x + ⟨ks',xs⟩" using `?m'>0`        by simp      finally show ?thesis by(simp)    qed  qednext  case (Dvd d i ks)[simp]  show ?case  proof(cases ks)    case Nil thus ?thesis by simp  next    case (Cons k ks')[simp]    show ?thesis    proof cases      assume "k=0" thus ?thesis by simp    next      assume "k≠0"      with Dvd have "k dvd m" by simp      let ?m' = "m div k"      have "?m' ≠ 0" using `k dvd m` zdiv_eq_0_iff `m>0` `k≠0`        by(simp add:linorder_not_less zdvd_imp_le)      have 1: "k*(x*?m') = x * m"      proof -        have "k*(x*?m') = x*(k*?m')" by(simp add:algebra_simps)        also have "… = x*m" using dvd_mult_div_cancel[OF `k dvd m`]          by(simp add:algebra_simps)        finally show ?thesis .      qed      have "I⇣Z (hd_coeff1 m (Dvd d i ks)) (m*x#xs) <->            (?m'*d dvd ?m'*i + m*x + ?m' * ⟨ks',xs⟩)"        using `k≠0` by(simp add: algebra_simps)      also have "… <-> ?m'*d dvd ?m' * (i + k*x + ⟨ks',xs⟩)" using 1        by(simp (no_asm_simp) add:algebra_simps)      also have "… <-> d dvd i + k*x + ⟨ks',xs⟩" using `?m'≠0` by(simp)      finally show ?thesis by(simp add:algebra_simps)    qed  qednext  case (NDvd d i ks)[simp]  show ?case  proof(cases ks)    case Nil thus ?thesis by simp  next    case (Cons k ks')[simp]    show ?thesis    proof cases      assume "k=0" thus ?thesis by simp    next      assume "k≠0"      with NDvd have "k dvd m" by simp      let ?m' = "m div k"      have "?m' ≠ 0" using `k dvd m` zdiv_eq_0_iff `m>0` `k≠0`        by(simp add:linorder_not_less zdvd_imp_le)      have 1: "k*(x*?m') = x * m"      proof -        have "k*(x*?m') = x*(k*?m')" by(simp add:algebra_simps)        also have "… = x*m" using dvd_mult_div_cancel[OF `k dvd m`]          by(simp add:algebra_simps)        finally show ?thesis .      qed      have "I⇣Z (hd_coeff1 m (NDvd d i ks)) (m*x#xs) <->            ¬(?m'*d dvd ?m'*i + m*x + ?m' * ⟨ks',xs⟩)"        using `k≠0` by(simp add: algebra_simps)      also have "… <-> ¬ ?m'*d dvd ?m' * (i + k*x + ⟨ks',xs⟩)" using 1        by(simp (no_asm_simp) add:algebra_simps)      also have "… <-> ¬ d dvd i + k*x + ⟨ks',xs⟩" using `?m'≠0` by(simp)      finally show ?thesis by(simp add:algebra_simps)    qed  qedqedlemma I_hd_coeff1_mult: assumes "m>0"shows "qfree φ ==> ∀ a ∈ set(Z.atoms⇣0 φ). hd_coeff a dvd m ==> Z.I (map⇘fm⇙ (hd_coeff1 m) φ) (m*x#xs) = Z.I φ (x#xs)"proof(induct φ)  case (Atom a)  thus ?case using I_hd_coeff1_mult_a[OF `m>0`] by autoqed simp_allend`