Theory QEpres

(*  Author:     Tobias Nipkow, 2007  *)

theory QEpres
imports PresArith
begin

subsection‹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)
qed


abbreviation "is_dvd a ≡ case a of Le _ _ ⇒ False | _ ⇒ True"

definition
"qe_pres⇩₁ 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 ∘ asubst n []) ds))
     else
     Disj ls (λ(li,lks).
       Disj [0..d - 1] (λn.
         list_conj(map (Atom ∘ asubst (li + n) (-lks)) as))))"
text‹\noindent Note the optimization in the case @{prop"ls = []"}: only the
divisibility atoms are tested, not the inequalities. This complicates
the 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 (simp add: mod_add_eq)
    also have "(i + ⟨ks',e⟩) mod d = (i mod d + ⟨ks',e⟩ mod d) mod d"
      by (simp add: 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)
    also have "(l mod d + (j + ⟨ks',e⟩) mod d) mod d = ?r"
      by(rule mod_add_eq)
    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 (simp add: mod_add_eq)
    also have "(i + ⟨ks',e⟩) mod d = (i mod d + ⟨ks',e⟩ mod d) mod d"
      by (simp add: 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)
    also have "(l mod d + (j + ⟨ks',e⟩) mod d) mod d = ?r"
      by(rule mod_add_eq)
    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 simp
qed

lemma I_qe_pres⇩₁:
assumes norm: "∀a ∈ set as. divisor a ≠ 0"
and hd: "∀a ∈ set as. hd_coeff_is1 a"
shows "Z.I (qe_pres⇩₁ 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 rule: atom.exhaust)(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⇩₁_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 (simp add: 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:minus_mod_eq_mult_div [symmetric] 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⇩₁_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⇩₁_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 (simp add: 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)
              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⇩₁_def IZ_asubst split_def)
           (force simp del:int_nat_eq)
    qed
  qed
qed

lemma  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 [simp]: (Dvd d i ks)
      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 [simp]: (NDvd d i ks)
      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
  qed
qed

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


lemma I_qe_pres⇩₁_o:
 "⟦ ∀a ∈ set as. divisor a ≠ 0; ∀a∈set as. hd_coeff a ≠ 0 ⟧ ⟹
  Z.I ((qe_pres⇩₁ ∘ hd_coeffs1) as) e = (∃x. ∀a∈ set as. I⇩_Z a (x#e))"
apply(simp)
apply(subst I_qe_pres⇩₁)
  apply(simp add: divisors_hd_coeffs1)
 apply(simp add: hd_coeff_is1_hd_coeffs1)
using I_hd_coeffs1 apply(simp)
done

definition "qe_pres = Z.lift_dnf_qe (qe_pres⇩₁ ∘ hd_coeffs1)"

lemma qfree_qe_pres_o: "qfree ((qe_pres⇩₁ ∘ hd_coeffs1) as)"
by(auto simp:qe_pres⇩₁_def intro!:qfree_list_disj)


lemma normal_qe_pres⇩₁_o:
  "∀a ∈ set as. hd_coeff a ≠ 0 ∧ divisor a ≠ 0 ⟹
   Z.normal ((qe_pres⇩₁ ∘ hd_coeffs1) as)"
  supply image_cong_simp [cong del]
apply(auto simp:qe_pres⇩₁_def Z.normal_def
   dest!:atoms_list_disjE atoms_list_conjE)

apply(simp add: hd_coeffs1_def)
 apply(erule disjE) apply fastforce
apply (clarsimp)
apply(case_tac xa)
  apply(rename_tac list) apply(case_tac list) apply fastforce apply (simp split:if_split_asm)
 apply(rename_tac list) apply(case_tac list) apply fastforce
 apply (simp split:if_split_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(rename_tac list) apply(case_tac list) apply fastforce
apply (simp split:if_split_asm) apply fastforce
apply(simp add:zdiv_eq_0_iff)
apply(subgoal_tac "∀i∈ set(map hd_coeff as). i ≠ 0")
 prefer 2 apply simp
apply(subgoal_tac "a ∈ set(map hd_coeff as)")
 prefer 2 apply force
apply(erule disjE)
 apply (metis elem_le_zlcms linorder_not_le)
apply(erule disjE)
 apply (metis linorder_not_le zlcms_pos)
apply fastforce

apply(simp add: hd_coeffs1_def)
 apply(erule disjE) apply fastforce
apply (clarsimp)
apply(case_tac xa)
  apply(rename_tac list) apply(case_tac list) apply fastforce apply (simp split:if_split_asm)
 apply(rename_tac list) apply(case_tac list) apply fastforce
 apply (simp split:if_split_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(rename_tac list) apply(case_tac list) apply fastforce
apply (simp split:if_split_asm) apply fastforce
apply(simp add:zdiv_eq_0_iff)
apply(subgoal_tac "∀i∈ set(map hd_coeff as). i ≠ 0")
 prefer 2 apply simp
apply(subgoal_tac "a ∈ set(map hd_coeff as)")
 prefer 2 apply force
apply(erule disjE)
 apply (metis elem_le_zlcms linorder_not_le)
apply(erule disjE)
 apply (metis linorder_not_le zlcms_pos)
apply fastforce
done

theorem 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⇩₁_o qfree_qe_pres_o normal_qe_pres⇩₁_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