Theory QEdlo

(*  Author:     Tobias Nipkow, 2007  *)

theory QEdlo
imports DLO
begin

subsection "DNF-based quantifier elimination"

definition qe_dlo⇩1 :: "atom list ⇒ atom fm" where
"qe_dlo⇩1 as =
 (if Less 0 0 ∈ set as then FalseF else
  let lbs = [i. Less (Suc i) 0 ← as]; ubs = [j. Less 0 (Suc j) ← as];
      pairs = [Atom(Less i j). i ← lbs, j ← ubs]
  in list_conj pairs)"

theorem I_qe_dlo⇩1:
assumes less: "∀a ∈ set as. is_Less a" and dep: "∀a ∈ set as. depends⇩d⇩l⇩o a"
shows "DLO.I (qe_dlo⇩1 as) xs = (∃x. ∀a ∈ set as. I⇩d⇩l⇩o a (x#xs))"
  (is "?L = ?R")
proof
  let ?lbs = "[i. Less (Suc i) 0 ← as]"
  let ?ubs = "[j. Less 0 (Suc j) ← as]"
  let ?Ls = "set ?lbs" let ?Us = "set ?ubs"
  let ?lb = "Max (⋃x∈?Ls. {xs!x})"
  let ?ub = "Min (⋃x∈?Us. {xs!x})"
  have 2: "Less 0 0 ∉ set as ⟹ ∀a ∈ set as.
      (∃i ∈ ?Ls. a = Less (Suc i) 0) ∨ (∃i ∈ ?Us. a = Less 0 (Suc i))"
  proof
    fix a assume "Less 0 0 ∉ set as" "a ∈ set as"
    then obtain i j where [simp]: "a = Less i j"
      using less by (force simp:is_Less_iff)
    with dep obtain k where "i = 0 ∧ j = Suc k ∨ i = Suc k ∧ j = 0"
      using ‹Less 0 0 ∉ set as› ‹a ∈ set as›
      by auto (metis Nat.nat.nchotomy depends⇩d⇩l⇩o.simps(2))
    moreover hence "i=0 ∧ k ∈ ?Us ∨ j=0 ∧ k ∈ ?Ls"
      using ‹a ∈ set as› by force
    ultimately show "(∃i∈?Ls. a=Less (Suc i) 0) ∨ (∃i∈?Us. a=Less 0 (Suc i))"
      by force
  qed
  assume qe1: ?L
  hence 0: "Less 0 0 ∉ set as" by (auto simp:qe_dlo⇩1_def)
  with qe1 have 1: "∀x∈?Ls. ∀y∈?Us. xs ! x < xs ! y"
    by (fastforce simp:qe_dlo⇩1_def)
  have finite: "finite ?Ls" "finite ?Us" by (rule finite_set)+
  { fix i x
    assume "Less i 0 ∈ set as | Less 0 i ∈ set as"
    moreover hence "i ≠ 0" using 0 by iprover
    ultimately have "(x#xs) ! i = xs!(i - 1)" by (simp add: nth_Cons')
  } note this[simp]
  { assume nonempty: "?Ls ≠ {} ∧ ?Us ≠ {}"
    hence "Max (⋃x∈?Ls. {xs!x}) < Min (⋃x∈?Us. {xs!x})"
      using 1 finite by auto
    then obtain m where "?lb < m ∧ m < ?ub" using dense by blast
    hence "∀i∈?Ls. xs!i < m" and "∀j∈?Us. m < xs!j"
      using nonempty finite by auto
    hence "∀a ∈ set as. I⇩d⇩l⇩o a (m # xs)" using 2[OF 0] by(auto simp:less)
    hence ?R .. }
  moreover
  { assume asm: "?Ls ≠ {} ∧ ?Us = {}"
    then obtain m where "?lb < m" using no_ub by blast
    hence "∀a∈ set as. I⇩d⇩l⇩o a (m # xs)" using 2[OF 0] asm finite by auto
    hence ?R .. }
  moreover
  { assume asm: "?Ls = {} ∧ ?Us ≠ {}"
    then obtain m where "m < ?ub" using no_lb by blast
    hence "∀a∈ set as. I⇩d⇩l⇩o a (m # xs)" using 2[OF 0] asm finite by auto
    hence ?R .. }
  moreover
  { assume "?Ls = {} ∧ ?Us = {}"
    hence ?R using 2[OF 0] by (auto simp add:less)
  }
  ultimately show ?R by blast
next
  assume ?R
  then obtain x where 1: "∀a∈ set as. I⇩d⇩l⇩o a (x # xs)" ..
  hence 0: "Less 0 0 ∉ set as" by auto
  { fix i j
    assume asm: "Less i 0 ∈ set as" "Less 0 j ∈ set as"
    hence "(x#xs)!i < x" "x < (x#xs)!j" using 1 by auto+
    hence "(x#xs)!i < (x#xs)!j" by(rule order_less_trans)
    moreover have "¬(i = 0 | j = 0)" using 0 asm by blast
    ultimately have "xs ! (i - 1) < xs ! (j - 1)" by (simp add: nth_Cons')
  }
  thus ?L using 0 less
    by (fastforce simp: qe_dlo⇩1_def is_Less_iff split:atom.splits nat.splits)
qed

lemma I_qe_dlo⇩1_pretty:
  "∀a ∈ set as. is_Less a ∧ depends⇩d⇩l⇩o a ⟹ DLO.is_dnf_qe _ qe_dlo⇩1 as"
by(metis I_qe_dlo⇩1)

definition subst :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"subst i j k = (if k=0 then if i=0 then j else i else k) - 1"
fun subst⇩0 :: "atom ⇒ atom ⇒ atom" where
"subst⇩0 (Eq i j) a = (case a of
   Less m n ⇒ Less (subst i j m) (subst i j n)
 | Eq m n ⇒ Eq (subst i j m) (subst i j n))"

lemma subst⇩0_pretty:
  "subst⇩0 (Eq i j) (Less m n) = Less (subst i j m) (subst i j n)"
  "subst⇩0 (Eq i j) (Eq m n) = Eq (subst i j m) (subst i j n)"
by auto

(*<*)
(* needed for code generation *)
definition [code del]: "lift_dnfeq_qe = ATOM_EQ.lift_dnfeq_qe neg⇩d⇩l⇩o depends⇩d⇩l⇩o decr⇩d⇩l⇩o (λEq i j ⇒ i=0 ∨ j=0 | a ⇒ False)
          (λEq i j ⇒ i=j | a ⇒ False) subst⇩0"
definition [code del]:
  "lift_eq_qe = ATOM_EQ.lift_eq_qe (λEq i j ⇒ i=0 ∨ j=0 | a ⇒ False)
                                   (λEq i j ⇒ i=j | a ⇒ False) subst⇩0"

lemmas DLOe_code_lemmas = DLO_code_lemmas lift_dnfeq_qe_def lift_eq_qe_def

hide_const lift_dnfeq_qe lift_eq_qe
(*>*)

interpretation DLO⇩e:
  ATOM_EQ neg⇩d⇩l⇩o "(λa. True)" I⇩d⇩l⇩o depends⇩d⇩l⇩o decr⇩d⇩l⇩o
          "(λEq i j ⇒ i=0 ∨ j=0 | a ⇒ False)"
          "(λEq i j ⇒ i=j | a ⇒ False)" subst⇩0
apply(unfold_locales)
apply(fastforce simp:subst_def nth_Cons' split:atom.splits if_split_asm)
apply(simp add:subst_def split:atom.splits)
apply(fastforce simp:subst_def nth_Cons' split:atom.splits)
apply(fastforce simp add:subst_def split:atom.splits)
done

(*<*)
lemmas [folded DLOe_code_lemmas, code] =
  DLO⇩e.lift_dnfeq_qe_def DLO⇩e.lift_eq_qe_def
(*>*)

setup ‹Sign.revert_abbrev "" @{const_abbrev DLO⇩e.lift_dnfeq_qe}›

definition "qe_dlo = DLO⇩e.lift_dnfeq_qe qe_dlo⇩1"
(*<*)
lemmas [folded DLOe_code_lemmas, code] = qe_dlo_def 
(*>*)

lemma qfree_qe_dlo⇩1: "qfree (qe_dlo⇩1 as)"
by(auto simp:qe_dlo⇩1_def intro!:qfree_list_conj)

theorem I_qe_dlo: "DLO.I (qe_dlo φ) xs = DLO.I φ xs"
unfolding qe_dlo_def
by(fastforce intro!: I_qe_dlo⇩1 qfree_qe_dlo⇩1 DLO⇩e.I_lift_dnfeq_qe
        simp: is_Less_iff not_is_Eq_iff split:atom.splits cong:conj_cong)

theorem qfree_qe_dlo: "qfree (qe_dlo φ)"
by(simp add:qe_dlo_def DLO⇩e.qfree_lift_dnfeq_qe qfree_qe_dlo⇩1)

end