Theory QEdlo

(*  Author:     Tobias Nipkow, 2007  *)

theory QEdlo
imports DLO "~~/src/HOL/Library/Reflection"
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 \<leftarrow> as]; ubs = [j. Less 0 (Suc j) \<leftarrow> as];
      pairs = [Atom(Less i j). i \<leftarrow> lbs, j \<leftarrow> 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 \<leftarrow> as]"
  let ?ubs = "[j. Less 0 (Suc j) \<leftarrow> as]"
  let ?Ls = "set ?lbs" let ?Us = "set ?ubs"
  let ?lb = "Max (\<Union>x∈?Ls. {xs!x})"
  let ?ub = "Min (\<Union>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 (\<Union>x∈?Ls. {xs!x}) < Min (\<Union>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 split_if_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