Theory QElin

(*  Author:     Tobias Nipkow, 2007  *)

theory QElin
imports LinArith
begin

subsection‹Fourier›

definition qe_FM1 :: "atom list ⇒ atom fm" where
"qe_FM1 as = list_conj [Atom(combine p q). p←lbounds as, q←ubounds as]"

theorem I_qe_FM1:
assumes less: "∀a ∈ set as. is_Less a" and dep: "∀a ∈ set as. dependsR a"
shows "R.I (qe_FM1 as) xs = (∃x. ∀a ∈ set as. IR 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 dependsR_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_FM1_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. IR a (m#xs)" using 2 nonempty
      apply (auto simp: Ball_def)
      apply (auto simp: Bex_def)
      apply (fastforce simp: field_simps)
      done
    hence ?R .. }
  moreover
  { assume asm: "?lbs ≠ {} ∧ ?ubs = {}"
    have "∀a ∈ set as. IR 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 simp: field_simps)
      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 "IR a ((Max ?lbs + 1) # xs)" by (simp add: field_simps)
    qed
    hence ?R .. }
  moreover
  { assume asm: "?lbs = {} ∧ ?ubs ≠ {}"
    have "∀a ∈ set as. IR 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 "IR 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. IR 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_FM1_def iprod_left_diff_distrib less field_simps set_lbounds set_ubounds)
qed

corollary I_qe_FM1_pretty:
  "∀a ∈ set as. is_Less a ∧ dependsR a ⟹ R.is_dnf_qe qe_FM1 as"
by(metis I_qe_FM1)


fun subst0 :: "atom ⇒ atom ⇒ atom" where
"subst0 (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 subst0_pretty:
 "subst0 (Eq r (c#cs)) (Less s (d#ds)) = Less (s - (r*d)/c) (ds - (d/c) *s cs)"
 "subst0 (Eq r (c#cs)) (Eq s (d#ds)) = Eq (s - (r*d)/c) (ds - (d/c) *s cs)"
by auto

lemma I_subst0: "dependsR a ⟹ c ≠ 0 ⟹
       IR (subst0 (Eq r (c#cs)) a) xs = IR a ((r - ⟨cs,xs⟩)/c # xs)"
apply(cases a)
by (auto simp add: dependsR_def iprod_left_diff_distrib algebra_simps diff_divide_distrib split:list.splits)

interpretation Re:
  ATOM_EQ negR "(λa. True)" IR dependsR decrR
          "(λEq _ (c#_) ⇒ c ≠ 0 | _ ⇒ False)"
          "(λEq r cs ⇒ r=0 ∧ (∀c∈ set cs. c=0) | _ ⇒ False)" subst0
apply(unfold_locales)
   apply(simp del:subst0.simps add:I_subst0 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 Re.lift_dnfeq_qe} *}
*)

definition "qe_FM = Re.lift_dnfeq_qe qe_FM1"

lemma qfree_qe_FM1: "qfree (qe_FM1 as)"
by(auto simp:qe_FM1_def intro!:qfree_list_conj)

corollary I_qe_FM: "R.I (qe_FM φ) xs = R.I φ xs"
unfolding qe_FM_def
apply(rule Re.I_lift_dnfeq_qe)
 apply(rule qfree_qe_FM1)
apply(rule allI)
apply(rule I_qe_FM1)
 prefer 2 apply blast
apply(clarify)
apply(drule_tac x=a in bspec) apply simp
apply(simp add: dependsR_def split:atom.splits list.splits)
done

theorem qfree_qe_FM: "qfree (qe_FM f)"
by(simp add:qe_FM_def Re.qfree_lift_dnfeq_qe qfree_qe_FM1)

subsubsection‹Tests›

lemmas qesimps = qe_FM_def Re.lift_dnfeq_qe_def Re.lift_eq_qe_def R.qelim_def qe_FM1_def lbounds_def ubounds_def list_conj_def list_disj_def and_def or_def dependsR_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