Theory PresArith

(*  Author:     Tobias Nipkow, 2007  *)

section‹Presburger arithmetic›

theory PresArith
imports QE "HOL-Library.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⇩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
  rewrites "ATOM.atoms⇩0 (λa. hd_coeff a ≠ 0) = atoms⇩0"
proof goal_cases
  case 1
  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 2
  thus ?case by(simp add:atoms⇩0_def)
qed

setup ‹Sign.revert_abbrev "" @{const_abbrev Z.I}›
setup ‹Sign.revert_abbrev "" @{const_abbrev Z.lift_dnf_qe}›
(* FIXME doesn't work*)
(* FIXME does not help
setup {* 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⇩f⇩m (asubst i ks)"

lemma IZ_asubst: "I⇩Z (asubst i ks a) xs = I⇩Z a ((i + ⟨ks,xs⟩) # xs)"
apply (cases a)
apply (rename_tac list)
apply (case_tac list)
apply (simp_all add:algebra_simps iprod_left_add_distrib)
apply (rename_tac list)
apply (case_tac list)
apply (simp_all add:algebra_simps iprod_left_add_distrib)
apply (rename_tac list)
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) ← as, k>0]"
definition "ubounds as = [(i,ks). Le i (k#ks) ← 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") 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 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} 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_conv_add_uminus 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_conv_add_uminus add.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 [simp]: (Le i ks)
  show ?case
  proof(cases ks)
    case Nil thus ?thesis by simp
  next
    case [simp]: (Cons k ks')
    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
  qed
next
  case [simp]: (Dvd d i ks)
  show ?case
  proof(cases ks)
    case Nil thus ?thesis by simp
  next
    case [simp]: (Cons k ks')
    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
  qed
next
  case [simp]: (NDvd d i ks)
  show ?case
  proof(cases ks)
    case Nil thus ?thesis by simp
  next
    case [simp]: (Cons k ks')
    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
  qed
qed


lemma I_hd_coeff1_mult: assumes "m>0"
shows "qfree φ ⟹ ∀ a ∈ set(Z.atoms⇩0 φ). hd_coeff a dvd m ⟹
 Z.I (map⇩f⇩m (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 auto
qed simp_all

end