Theory QE

(*  Author:     Tobias Nipkow, 2007  *)

section‹Quantifier elimination›

theory QE
imports Logic
begin

text‹\noindent
The generic, i.e.\ theory-independent part of quantifier elimination.
Both DNF and an NNF-based procedures are defined and proved correct.›

notation (input) Collect (‹|_|›)

subsection‹No Equality›

context ATOM
begin

subsubsection‹DNF-based›

text‹\noindent Taking care of atoms independent of variable 0:›

definition
"qelim qe as =
 (let qf = qe [a←as. depends0 a];
      indep = [Atom(decr a). a←as, ¬ depends0 a]
  in and qf (list_conj indep))"

abbreviation is_dnf_qe :: "('a list ⇒ 'a fm) ⇒ 'a list ⇒ bool" where
"is_dnf_qe qe as ≡ ∀xs. I(qe as) xs = (∃x.∀a∈set as. Ia a (x#xs))"

text‹\noindent
Note that the exported abbreviation will have as a first parameter
the type @{typ"'b"} of values ‹xs› ranges over.›

lemma I_qelim:
assumes qe: "⋀as. (∀a ∈ set as. depends0 a) ⟹ is_dnf_qe qe as"
shows "is_dnf_qe (qelim qe) as" (is "∀xs. ?P xs")
proof
  fix  xs
  let ?as0 = "filter depends0 as"
  let ?as1 = "filter (Not ∘ depends0) as"
  have "I (qelim qe as) xs =
        (I (qe ?as0) xs ∧ (∀a∈set(map decr ?as1). Ia a xs))"
    (is "_ = (_ ∧ ?B)") by(force simp add:qelim_def)
  also have "… = ((∃x. ∀a ∈ set ?as0. Ia a (x#xs)) ∧ ?B)"
    by(simp add:qe not_dep_decr)
  also have "… = (∃x. (∀a ∈ set ?as0. Ia a (x#xs)) ∧ ?B)" by blast
  also have "?B = (∀a ∈ set ?as1. Ia (decr a) xs)" by simp
  also have "(∃x. (∀a ∈ set ?as0. Ia a (x#xs)) ∧ …) =
             (∃x. (∀a ∈ set ?as0. Ia a (x#xs)) ∧
                  (∀a ∈ set ?as1. Ia a (x#xs)))"
    by(simp add: not_dep_decr)
  also have "… = (∃x. ∀a ∈ set(?as0 @ ?as1). Ia a (x#xs))"
    by (simp add:ball_Un)
  also have "… = (∃x. ∀a ∈ set(as). Ia a (x#xs))"
    by simp blast
  finally show "?P xs" .
qed

text‹\noindent The generic DNF-based quantifier elimination procedure:›

fun lift_dnf_qe :: "('a list ⇒ 'a fm) ⇒ 'a fm ⇒ 'a fm" where
"lift_dnf_qe qe (And φ1 φ2) = and (lift_dnf_qe qe φ1) (lift_dnf_qe qe φ2)" |
"lift_dnf_qe qe (Or φ1 φ2) = or (lift_dnf_qe qe φ1) (lift_dnf_qe qe φ2)" |
"lift_dnf_qe qe (Neg φ) = neg(lift_dnf_qe qe φ)" |
"lift_dnf_qe qe (ExQ φ) = Disj (dnf(nnf(lift_dnf_qe qe φ))) (qelim qe)" |
"lift_dnf_qe qe φ = φ"

lemma qfree_lift_dnf_qe: "(⋀as. (∀a∈set as. depends0 a) ⟹ qfree(qe as))
 ⟹ qfree(lift_dnf_qe qe φ)"
by (induct φ) (simp_all add:qelim_def)

lemma qfree_lift_dnf_qe2: "qe ∈ lists |depends0| → |qfree|
 ⟹ qfree(lift_dnf_qe qe φ)"
using in_lists_conv_set[where ?'a = 'a]
by (simp add:Pi_def qfree_lift_dnf_qe)

lemma lem: "∀P A. (∃x∈A. ∃y. P x y) = (∃y. ∃x∈A. P x y)" by blast

lemma I_lift_dnf_qe:
assumes  "⋀as. (∀a ∈ set as. depends0 a) ⟹ qfree(qe as)"
and "⋀as. (∀a ∈ set as. depends0 a) ⟹ is_dnf_qe qe as"
shows "I (lift_dnf_qe qe φ) xs = I φ xs"
proof(induct φ arbitrary:xs)
  case ExQ thus ?case
    by (simp add: assms I_qelim lem I_dnf nqfree_nnf qfree_lift_dnf_qe
                  I_nnf)
qed simp_all

lemma I_lift_dnf_qe2:
assumes  "qe ∈ lists |depends0| → |qfree|"
and "∀as ∈ lists |depends0|. is_dnf_qe qe as"
shows "I (lift_dnf_qe qe φ) xs = I φ xs"
using assms in_lists_conv_set[where ?'a = 'a]
by(simp add:Pi_def I_lift_dnf_qe)

text‹\noindent Quantifier elimination with invariant (needed for Presburger):›

lemma I_qelim_anormal:
assumes qe: "⋀xs as. ∀a ∈ set as. depends0 a ∧ anormal a ⟹ is_dnf_qe qe as"
and nm: "∀a ∈ set as. anormal a"
shows "I (qelim qe as) xs = (∃x. ∀a∈set as. Ia a (x#xs))"
proof -
  let ?as0 = "filter depends0 as"
  let ?as1 = "filter (Not ∘ depends0) as"
  have "I (qelim qe as) xs =
        (I (qe ?as0) xs ∧ (∀a∈set(map decr ?as1). Ia a xs))"
    (is "_ = (_ ∧ ?B)") by(force simp add:qelim_def)
  also have "… = ((∃x. ∀a ∈ set ?as0. Ia a (x#xs)) ∧ ?B)"
    by(simp add:qe nm not_dep_decr)
  also have "… = (∃x. (∀a ∈ set ?as0. Ia a (x#xs)) ∧ ?B)" by blast
  also have "?B = (∀a ∈ set ?as1. Ia (decr a) xs)" by simp
  also have "(∃x. (∀a ∈ set ?as0. Ia a (x#xs)) ∧ …) =
             (∃x. (∀a ∈ set ?as0. Ia a (x#xs)) ∧
                  (∀a ∈ set ?as1. Ia a (x#xs)))"
    by(simp add: not_dep_decr)
  also have "… = (∃x. ∀a ∈ set(?as0 @ ?as1). Ia a (x#xs))"
    by (simp add:ball_Un)
  also have "… = (∃x. ∀a ∈ set(as). Ia a (x#xs))"
    by simp blast
  finally show ?thesis .
qed

context notes [[simp_depth_limit = 5]]
begin

lemma anormal_atoms_qelim:
  "(⋀as. ∀a ∈ set as. depends0 a ∧ anormal a ⟹ normal(qe as)) ⟹
   ∀a ∈ set as. anormal a ⟹ a ∈ atoms(qelim qe as) ⟹ anormal a"
apply(auto simp add:qelim_def and_def normal_def split:if_split_asm)
apply(auto simp add:anormal_decr dest!: atoms_list_conjE)
 apply(erule_tac x = "filter depends0 as" in meta_allE)
 apply(simp)
apply(erule_tac x = "filter depends0 as" in meta_allE)
apply(simp)
done

lemma normal_lift_dnf_qe:
assumes "⋀as. ∀a ∈ set as. depends0 a ⟹ qfree(qe as)"
and "⋀as. ∀a ∈ set as. depends0 a ∧ anormal a ⟹ normal(qe as)"
shows  "normal φ ⟹ normal(lift_dnf_qe qe φ)"
proof(simp add:normal_def, induct φ)
  case ExQ thus ?case
    apply (auto dest!: atoms_list_disjE)
    apply(rule anormal_atoms_qelim)
      prefer 3 apply assumption
     apply(simp add:assms)
    apply (simp add:normal_def qfree_lift_dnf_qe anormal_dnf_nnf assms)
    done
qed (simp_all add:and_def or_def neg_def Ball_def)

end

context notes [[simp_depth_limit = 9]]
begin

lemma I_lift_dnf_qe_anormal:
assumes "⋀as. ∀a ∈ set as. depends0 a ⟹ qfree(qe as)"
and "⋀as. ∀a ∈ set as. depends0 a ∧ anormal a ⟹ normal(qe as)"
and "⋀xs as. ∀a ∈ set as. depends0 a ∧ anormal a ⟹ is_dnf_qe qe as"
shows "normal f ⟹ I (lift_dnf_qe qe f) xs = I f xs"
proof(induct f arbitrary:xs)
  case ExQ thus ?case using normal_lift_dnf_qe[of qe]
    by (simp add: assms[simplified normal_def] anormal_dnf_nnf I_qelim_anormal lem I_dnf nqfree_nnf qfree_lift_dnf_qe I_nnf normal_def)
qed (simp_all add:normal_def)

end

lemma I_lift_dnf_qe_anormal2:
assumes "qe ∈ lists |depends0| → |qfree|"
and "qe ∈ lists ( |depends0| ∩ |anormal| ) → |normal|"
and "∀as ∈ lists( |depends0| ∩ |anormal| ). is_dnf_qe qe as"
shows "normal f ⟹ I (lift_dnf_qe qe f) xs = I f xs"
using assms in_lists_conv_set[where ?'a = 'a]
by(simp add:Pi_def I_lift_dnf_qe_anormal Int_def)


subsubsection‹NNF-based›

fun lift_nnf_qe :: "('a fm ⇒ 'a fm) ⇒ 'a fm ⇒ 'a fm" where
"lift_nnf_qe qe (And φ1 φ2) = and (lift_nnf_qe qe φ1) (lift_nnf_qe qe φ2)" |
"lift_nnf_qe qe (Or φ1 φ2) = or (lift_nnf_qe qe φ1) (lift_nnf_qe qe φ2)" |
"lift_nnf_qe qe (Neg φ) = neg(lift_nnf_qe qe φ)" |
"lift_nnf_qe qe (ExQ φ) = qe(nnf(lift_nnf_qe qe φ))" |
"lift_nnf_qe qe φ = φ"

lemma qfree_lift_nnf_qe: "(⋀φ. nqfree φ ⟹ qfree(qe φ))
 ⟹ qfree(lift_nnf_qe qe φ)"
by (induct φ) (simp_all add:nqfree_nnf)

lemma qfree_lift_nnf_qe2:
  "qe ∈ |nqfree| → |qfree| ⟹ qfree(lift_nnf_qe qe φ)"
by(simp add:Pi_def qfree_lift_nnf_qe)

lemma I_lift_nnf_qe:
assumes  "⋀φ. nqfree φ ⟹ qfree(qe φ)"
and "⋀xs φ. nqfree φ ⟹ I (qe φ) xs = (∃x. I φ (x#xs))"
shows "I (lift_nnf_qe qe φ) xs = I φ xs"
proof(induct "φ" arbitrary:xs)
  case ExQ thus ?case
    by (simp add: assms nqfree_nnf qfree_lift_nnf_qe I_nnf)
qed simp_all

lemma I_lift_nnf_qe2:
assumes  "qe ∈ |nqfree| → |qfree|"
and "∀φ ∈ |nqfree|. ∀xs. I (qe φ) xs = (∃x. I φ (x#xs))"
shows "I (lift_nnf_qe qe φ) xs = I φ xs"
using assms by(simp add:Pi_def I_lift_nnf_qe)

lemma normal_lift_nnf_qe:
assumes "⋀φ. nqfree φ ⟹ qfree(qe φ)"
and     "⋀φ. nqfree φ ⟹ normal φ ⟹ normal(qe φ)"
shows "normal φ ⟹ normal(lift_nnf_qe qe φ)"
by (induct φ)
   (simp_all add: assms Logic.neg_def normal_nnf
                  nqfree_nnf qfree_lift_nnf_qe)

lemma I_lift_nnf_qe_normal:
assumes  "⋀φ. nqfree φ ⟹ qfree(qe φ)"
and "⋀φ. nqfree φ ⟹ normal φ ⟹ normal(qe φ)"
and "⋀xs φ. normal φ ⟹ nqfree φ ⟹ I (qe φ) xs = (∃x. I φ (x#xs))"
shows "normal φ ⟹ I (lift_nnf_qe qe φ) xs = I φ xs"
proof(induct "φ" arbitrary:xs)
  case ExQ thus ?case
    by (simp add: assms nqfree_nnf qfree_lift_nnf_qe I_nnf
                  normal_lift_nnf_qe normal_nnf)
qed auto

lemma I_lift_nnf_qe_normal2:
assumes  "qe ∈ |nqfree| → |qfree|"
and "qe ∈ |nqfree| ∩ |normal| → |normal|"
and "∀φ ∈ |normal| ∩ |nqfree|. ∀xs. I (qe φ) xs = (∃x. I φ (x#xs))"
shows "normal φ ⟹ I (lift_nnf_qe qe φ) xs = I φ xs"
using assms by(simp add:Pi_def I_lift_nnf_qe_normal Int_def)

end


subsection‹With equality›

text‹DNF-based quantifier elimination can accommodate equality atoms
in a generic fashion.›

locale ATOM_EQ = ATOM +
fixes solvable0 :: "'a ⇒ bool"
and trivial :: "'a ⇒ bool" 
and subst0 :: "'a ⇒ 'a ⇒ 'a"
assumes subst0:
  "⟦ solvable0 eq;  ¬trivial eq;  Ia eq (x#xs);  depends0 a ⟧
   ⟹ Ia (subst0 eq a) xs = Ia a (x#xs)"
and trivial: "trivial eq ⟹ Ia eq xs"
and solvable: "solvable0 eq ⟹ ∃x. Ia eq (x#xs)"
and is_triv_self_subst: "solvable0 eq ⟹ trivial (subst0 eq eq)"

begin

definition lift_eq_qe :: "('a list ⇒ 'a fm) ⇒ 'a list ⇒ 'a fm" where
"lift_eq_qe qe as =
 (let as = [a←as. ¬ trivial a]
  in case [a←as. solvable0 a] of
    [] ⇒ qe as
  | eq # eqs ⇒
        (let ineqs = [a←as. ¬ solvable0 a]
         in list_conj (map (Atom ∘ (subst0 eq)) (eqs @ ineqs))))"

theorem I_lift_eq_qe:
assumes dep: "∀a∈set as. depends0 a"
assumes qe: "⋀as. (∀a ∈ set as. depends0 a ∧ ¬ solvable0 a) ⟹
   I (qe as) xs = (∃x. ∀a ∈ set as. Ia a (x#xs))"
shows "I (lift_eq_qe qe as) xs = (∃x. ∀a ∈ set as. Ia a (x#xs))"
  (is "?L = ?R")
proof -
  let ?as = "[a←as. ¬ trivial a]"
  show ?thesis
  proof (cases "[a←?as. solvable0 a]")
    case Nil
    hence "∀a∈set as. ¬ trivial a ⟶ ¬ solvable0 a"
      by(auto simp: filter_empty_conv)
    thus "?L = ?R"
      by(simp add:lift_eq_qe_def dep qe cong:conj_cong) (metis trivial)
  next
    case (Cons eq _)
    then have "eq ∈ set as" "solvable0 eq" "¬ trivial eq"
      by (auto simp: filter_eq_Cons_iff)
    then obtain e where "Ia eq (e#xs)" by(metis solvable)
    have "∀a ∈ set as. Ia a (e # xs) = Ia (subst0 eq a) xs"
      by(simp add: subst0[OF ‹solvable0 eq› ‹¬ trivial eq› ‹Ia eq (e#xs)›] dep)
    thus ?thesis using Cons dep
      apply(simp add: lift_eq_qe_def,
            clarsimp simp: filter_eq_Cons_iff ball_Un)
      apply(rule iffI)
      apply(fastforce intro!:exI[of _ e] simp: trivial is_triv_self_subst)
      apply (metis subst0)
      done
  qed
qed

definition "lift_dnfeq_qe = lift_dnf_qe ∘ lift_eq_qe"

lemma qfree_lift_eq_qe:
  "(⋀as. ∀a∈set as. depends0 a ⟹ qfree (qe as)) ⟹
   ∀a∈set as. depends0 a ⟹ qfree(lift_eq_qe qe as)"
by(simp add:lift_eq_qe_def ball_Un split:list.split)

lemma qfree_lift_dnfeq_qe: "(⋀as. (∀a∈set as. depends0 a) ⟹ qfree(qe as))
  ⟹ qfree(lift_dnfeq_qe qe φ)"
by(simp add: lift_dnfeq_qe_def qfree_lift_dnf_qe qfree_lift_eq_qe)

lemma I_lift_dnfeq_qe:
  "(⋀as. (∀a ∈ set as. depends0 a) ⟹ qfree(qe as)) ⟹
   (⋀as. (∀a ∈ set as. depends0 a ∧ ¬ solvable0 a) ⟹ is_dnf_qe qe as) ⟹
   I (lift_dnfeq_qe qe φ) xs = I φ xs"
by(simp add:lift_dnfeq_qe_def I_lift_dnf_qe qfree_lift_eq_qe I_lift_eq_qe)

lemma I_lift_dnfeq_qe2:
  "qe ∈ lists |depends0| → |qfree| ⟹
   (∀as ∈ lists( |depends0| ∩ - |solvable0| ). is_dnf_qe qe as) ⟹
   I (lift_dnfeq_qe qe φ) xs = I φ xs"
using in_lists_conv_set[where ?'a = 'a]
by(simp add:Pi_def I_lift_dnfeq_qe Int_def Compl_eq)

end

end