Theory QElin

(*  Author:     Tobias Nipkow, 2007  *)

theory QElin
imports LinArith
begin

subsection{* Fourier *}

definition qe_FM⇣1 :: "atom list => atom fm" where
"qe_FM⇣1 as = list_conj [Atom(combine p q). p\<leftarrow>lbounds as, q\<leftarrow>ubounds as]"

theorem I_qe_FM⇣1:
assumes less: "∀a ∈ set as. is_Less a" and dep: "∀a ∈ set as. depends⇣R a"
shows "R.I (qe_FM⇣1 as) xs = (∃x. ∀a ∈ set as. I⇣R a (x#xs))"  (is "?L = ?R")
proof
  let ?Ls = "set(lbounds as)" let ?Us = "set(ubounds as)"
  let ?lbs = "UN (r,cs):?Ls. {r + ⟨cs,xs⟩}"
  let ?ubs = "UN (r,cs):?Us. {r + ⟨cs,xs⟩}"
  have fins: "finite ?lbs ∧ finite ?ubs" by auto
  have 2: "∀f∈ set as. ∃r c cs. f = Less r (c#cs) ∧
          (c>0 ∧ (r/c,(-1/c)*⇩s cs) ∈ ?Ls ∨ c<0 ∧ (r/c,(-1/c)*⇩s cs) ∈ ?Us)"
    using dep less
    by(fastforce simp:set_lbounds set_ubounds is_Less_iff depends⇣R_def
                split:list.splits)
  assume ?L
  have 1: "∀x∈?lbs. ∀y∈?ubs. x < y"
  proof (rule ballI)+
    fix x y assume "x∈?lbs" "y∈?ubs"
    then obtain r cs
      where "(r,cs) ∈ ?Ls ∧ x = r + ⟨cs,xs⟩" by fastforce
    moreover from `y∈?ubs` obtain s ds
      where "(s,ds) ∈ ?Us ∧ y = s + ⟨ds,xs⟩" by fastforce
    ultimately show "x<y" using `?L`
      by(fastforce simp:qe_FM⇣1_def algebra_simps iprod_left_diff_distrib)
  qed
  { assume nonempty: "?lbs ≠ {} ∧ ?ubs ≠ {}"
    hence "Max ?lbs < Min ?ubs" using fins 1
      by(blast intro: Max_less_iff[THEN iffD2] Min_gr_iff[THEN iffD2])
    then obtain m where "Max ?lbs < m ∧ m < Min ?ubs"
      using dense[where 'a = real] by blast
    hence "∀a ∈ set as. I⇣R a (m#xs)" using 2 nonempty
      by (auto simp:Ball_def Bex_def)(fastforce simp:field_simps)
    hence ?R .. }
  moreover
  { assume asm: "?lbs ≠ {} ∧ ?ubs = {}"
    have "∀a ∈ set as. I⇣R a ((Max ?lbs + 1) # xs)"
    proof
      fix a assume "a ∈ set as"
      then obtain r c cs
        where "a = Less r (c#cs)" "c>0" "(r/c,(-1/c)*⇩s cs) ∈ ?Ls"
        using asm 2 by fastforce
      moreover hence "(r - ⟨cs,xs⟩)/c ≤ Max ?lbs"
        using asm fins
        by(auto intro!: Max_ge_iff[THEN iffD2])
          (force simp add:field_simps)
      ultimately show "I⇣R a ((Max ?lbs + 1) # xs)" by (simp add: field_simps)
    qed
    hence ?R .. }
  moreover
  { assume asm: "?lbs = {} ∧ ?ubs ≠ {}"
    have "∀a ∈ set as. I⇣R a ((Min ?ubs - 1) # xs)"
    proof
      fix a assume "a ∈ set as"
      then obtain r c cs
        where "a = Less r (c#cs)" "c<0" "(r/c,(-1/c)*⇩s cs) ∈ ?Us"
        using asm 2 by fastforce
      moreover hence "Min ?ubs ≤ (r - ⟨cs,xs⟩)/c"
        using asm fins
        by(auto intro!: Min_le_iff[THEN iffD2])
          (force simp add:field_simps)
      ultimately show "I⇣R a ((Min ?ubs - 1) # xs)" by (simp add: field_simps)
    qed
    hence ?R .. }
  moreover
  { assume "?lbs = {} ∧ ?ubs = {}"
    hence ?R using 2 less by auto (rule, fast)
  }
  ultimately show ?R by blast
next
  let ?Ls = "set(lbounds as)" let ?Us = "set(ubounds as)"
  assume ?R
  then obtain x where 1: "∀a∈ set as. I⇣R a (x#xs)" ..
  { fix r c cs s d ds
    assume "Less r (c#cs) ∈ set as" "0 < c" "Less s (d#ds) ∈ set as" "d < 0"
    hence "r < c*x + ⟨cs,xs⟩" "s < d*x + ⟨ds,xs⟩" "c > 0" "d < 0"
      using 1 by auto
    hence "(r - ⟨cs,xs⟩)/c < x" "x < (s - ⟨ds,xs⟩)/d" by(simp add:field_simps)+
    hence "(r - ⟨cs,xs⟩)/c < (s - ⟨ds,xs⟩)/d" by arith
  }
  thus ?L by (auto simp: qe_FM⇣1_def iprod_left_diff_distrib less field_simps set_lbounds set_ubounds)
qed

corollary I_qe_FM⇣1_pretty:
  "∀a ∈ set as. is_Less a ∧ depends⇣R a ==> R.is_dnf_qe qe_FM⇣1 as"
by(metis I_qe_FM⇣1)


fun subst⇣0 :: "atom => atom => atom" where
"subst⇣0 (Eq r (c#cs)) a = (case a of
   Less s (d#ds) => Less (s - (r*d)/c) (ds - (d/c) *⇩s cs)
 | Eq s (d#ds) => Eq (s - (r*d)/c) (ds - (d/c) *⇩s cs))"

lemma subst⇣0_pretty:
 "subst⇣0 (Eq r (c#cs)) (Less s (d#ds)) = Less (s - (r*d)/c) (ds - (d/c) *⇩s cs)"
 "subst⇣0 (Eq r (c#cs)) (Eq s (d#ds)) = Eq (s - (r*d)/c) (ds - (d/c) *⇩s cs)"
by auto

lemma I_subst⇣0: "depends⇣R a ==> c ≠ 0 ==>
       I⇣R (subst⇣0 (Eq r (c#cs)) a) xs = I⇣R a ((r - ⟨cs,xs⟩)/c # xs)"
apply(cases a)
by (auto simp add: depends⇣R_def iprod_left_diff_distrib algebra_simps diff_divide_distrib split:list.splits)

interpretation R⇣e!:
  ATOM_EQ neg⇣R "(λa. True)" I⇣R depends⇣R decr⇣R
          "(λEq _ (c#_) => c ≠ 0 | _ => False)"
          "(λEq r cs => r=0 ∧ (∀c∈ set cs. c=0) | _ => False)" subst⇣0
apply(unfold_locales)
   apply(simp del:subst⇣0.simps add:I_subst⇣0 split:atom.splits list.splits)
  apply(simp add: iprod0_if_coeffs0 split:atom.splits)
 apply(simp split:atom.splits list.splits)
 apply(rename_tac r ds c cs)
 apply(rule_tac x= "(r - ⟨cs,xs⟩)/c" in exI)
 apply (simp add: algebra_simps diff_divide_distrib)
apply(simp add: self_list_diff set_replicate_conv_if
        split:atom.splits list.splits)
done

(* FIXME does not help
setup {* Sign.revert_abbrev "" @{const_name R⇣e.lift_dnfeq_qe} *}
*)

definition "qe_FM = R⇣e.lift_dnfeq_qe qe_FM⇣1"

lemma qfree_qe_FM⇣1: "qfree (qe_FM⇣1 as)"
by(auto simp:qe_FM⇣1_def intro!:qfree_list_conj)

corollary I_qe_FM: "R.I (qe_FM φ) xs = R.I φ xs"
unfolding qe_FM_def
apply(rule R⇣e.I_lift_dnfeq_qe)
 apply(rule qfree_qe_FM⇣1)
apply(rule allI)
apply(rule I_qe_FM⇣1)
 prefer 2 apply blast
apply(clarify)
apply(drule_tac x=a in bspec) apply simp
apply(simp add: depends⇣R_def split:atom.splits list.splits)
done

theorem qfree_qe_FM: "qfree (qe_FM f)"
by(simp add:qe_FM_def R⇣e.qfree_lift_dnfeq_qe qfree_qe_FM⇣1)

subsubsection{* Tests *}

lemmas qesimps = qe_FM_def R⇣e.lift_dnfeq_qe_def R⇣e.lift_eq_qe_def R.qelim_def qe_FM⇣1_def lbounds_def ubounds_def list_conj_def list_disj_def and_def or_def depends⇣R_def

lemma "qe_FM(TrueF) = TrueF"
by(simp add:qesimps)

lemma
  "qe_FM(ExQ (And (Atom(Less 0 [1])) (Atom(Less 0 [-1])))) = Atom(Less 0 [])"
by(simp add:qesimps)

lemma
 "qe_FM(ExQ (And (Atom(Less 0 [1])) (Atom(Less -1 [-1])))) = Atom(Less -1 [])"
by(simp add:qesimps)

end