Theory PresArith (Isabelle2009-1: December 2009)

(*  ID:         $Id: PresArith.thy,v 1.13 2009-07-15 09:26:53 makarius Exp $
    Author:     Tobias Nipkow, 2007
*)

header{* Presburger arithmetic *}

theory PresArith
imports GCD QE ListVector
begin

declare 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₀ = ATOM.atoms₀ (λ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₀ (λa. hd_coeff a ≠ 0) = atoms₀"
proof-
  case goal1
  thus ?case
apply(unfold_locales)
apply(case_tac a)
apply simp_all
apply(case_tac a)
apply simp_all
apply(case_tac a)
apply (simp_all)
apply arith
apply(case_tac a)
apply(simp_all add: split: list.splits)
apply(case_tac a)
apply simp_all
done
next
  case goal2 thus ?case by(simp add:atoms₀_def)
qed

setup {* Sign.revert_abbrev "" @{const_name Z.I} *}
setup {* Sign.revert_abbrev "" @{const_name Z.lift_dnf_qe} *}
(* FIXME doesn't work*)
(* FIXME does not help
setup {* Sign.revert_abbrev "" @{const_name 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)
done

lemma 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) auto


definition "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*}

(* FIXME move into Library *)

lemma zdiv_eq_0_iff:
 "(i::int) div k = 0 <-> k=0 ∨ 0≤i ∧ i<k ∨ i≤0 ∧ k<i"
apply(auto simp: div_pos_pos_trivial div_neg_neg_trivial)
  apply (metis int_0_neq_1 linorder_not_less neg_imp_zdiv_nonneg_iff zdiv_mono1 zdiv_self zero_le_one zle_antisym zle_refl zless_linear)
  apply (metis int_0_neq_1 linorder_not_less pos_imp_zdiv_nonneg_iff zdiv_mono1_neg zdiv_self zero_le_one zle_antisym zle_refl zless_linear)
apply (metis int_0_neq_1 zdiv_self zless_linear)
done

lemma pos_imp_zdiv_pos_iff:
  "0<k ==> 0 < (i::int) div k <-> k ≤ i"
using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k]
by arith

lemma zmod_le_nonneg_dividend: "(m::int) ≥ 0 ==> m mod k ≤ m"
apply(cases "k=0") apply simp
by(metis linorder_not_le mod_pos_pos_trivial neg_mod_conj pos_mod_conj zle_refl zle_trans zless_le)

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") auto

lemma 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 DIVISION_BY_ZERO dvd_eq_mod_eq_0 dvd_zlcms zlcms_pos zless_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} is
different from the @{const Le} because it allows the resulting head
coefficient to be 1 rather than 1 or -1. We show that the other version has
the 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 comm_monoid_add.mult_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 comm_monoid_add.mult_left_commute dvd_minus_iff minus_add_distrib)
done


lemma 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 zdvd_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 add: mult_compare_simps)
      finally show ?thesis by(simp)
    qed
  qed
next
  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 zdvd_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
  qed
next
  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 zdvd_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
  qed
qed


lemma I_hd_coeff1_mult: assumes "m>0"
shows "qfree φ ==> ∀ a ∈ set(Z.atoms₀ φ). 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(simp split:split_if_asm)
qed simp_all

end