header{* 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\<leftarrow>as. depends⇣0 a];
indep = [Atom(decr a). a\<leftarrow>as, ¬ depends⇣0 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. I⇣a a (x#xs))"
text{*\noindent
Note that the exported abbreviation will have as a first parameter
the type @{typ"'b"} of values @{text xs} ranges over. *}
lemma I_qelim:
assumes qe: "!!as. (∀a ∈ set as. depends⇣0 a) ==> is_dnf_qe qe as"
shows "is_dnf_qe (qelim qe) as" (is "∀xs. ?P xs")
proof
fix xs
let ?as0 = "filter depends⇣0 as"
let ?as1 = "filter (Not o depends⇣0) as"
have "I (qelim qe as) xs =
(I (qe ?as0) xs ∧ (∀a∈set(map decr ?as1). I⇣a a xs))"
(is "_ = (_ ∧ ?B)") by(force simp add:qelim_def)
also have "… = ((∃x. ∀a ∈ set ?as0. I⇣a a (x#xs)) ∧ ?B)"
by(simp add:qe not_dep_decr)
also have "… = (∃x. (∀a ∈ set ?as0. I⇣a a (x#xs)) ∧ ?B)" by blast
also have "?B = (∀a ∈ set ?as1. I⇣a (decr a) xs)" by simp
also have "(∃x. (∀a ∈ set ?as0. I⇣a a (x#xs)) ∧ …) =
(∃x. (∀a ∈ set ?as0. I⇣a a (x#xs)) ∧
(∀a ∈ set ?as1. I⇣a a (x#xs)))"
by(simp add: not_dep_decr)
also have "… = (∃x. ∀a ∈ set(?as0 @ ?as1). I⇣a a (x#xs))"
by (simp add:ball_Un)
also have "… = (∃x. ∀a ∈ set(as). I⇣a 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. depends⇣0 a) ==> qfree(qe as))
==> qfree(lift_dnf_qe qe φ)"
by (induct φ) (simp_all add:qelim_def)
lemma qfree_lift_dnf_qe2: "qe : lists |depends⇣0| -> |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. depends⇣0 a) ==> qfree(qe as)"
and "!!as. (∀a ∈ set as. depends⇣0 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 |depends⇣0| -> |qfree|"
and "∀as ∈ lists |depends⇣0|. 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. depends⇣0 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. I⇣a a (x#xs))"
proof -
let ?as0 = "filter depends⇣0 as"
let ?as1 = "filter (Not o depends⇣0) as"
have "I (qelim qe as) xs =
(I (qe ?as0) xs ∧ (∀a∈set(map decr ?as1). I⇣a a xs))"
(is "_ = (_ ∧ ?B)") by(force simp add:qelim_def)
also have "… = ((∃x. ∀a ∈ set ?as0. I⇣a a (x#xs)) ∧ ?B)"
by(simp add:qe nm not_dep_decr)
also have "… = (∃x. (∀a ∈ set ?as0. I⇣a a (x#xs)) ∧ ?B)" by blast
also have "?B = (∀a ∈ set ?as1. I⇣a (decr a) xs)" by simp
also have "(∃x. (∀a ∈ set ?as0. I⇣a a (x#xs)) ∧ …) =
(∃x. (∀a ∈ set ?as0. I⇣a a (x#xs)) ∧
(∀a ∈ set ?as1. I⇣a a (x#xs)))"
by(simp add: not_dep_decr)
also have "… = (∃x. ∀a ∈ set(?as0 @ ?as1). I⇣a a (x#xs))"
by (simp add:ball_Un)
also have "… = (∃x. ∀a ∈ set(as). I⇣a a (x#xs))"
by simp blast
finally show ?thesis .
qed
declare [[simp_depth_limit = 5]]
lemma anormal_atoms_qelim:
"(!!as. ∀a ∈ set as. depends⇣0 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:split_if_asm)
apply(auto simp add:anormal_decr dest!: atoms_list_conjE)
apply(erule_tac x = "filter depends⇣0 as" in meta_allE)
apply(simp)
apply(erule_tac x = "filter depends⇣0 as" in meta_allE)
apply(simp)
done
lemma normal_lift_dnf_qe:
assumes "!!as. ∀a ∈ set as. depends⇣0 a ==> qfree(qe as)"
and "!!as. ∀a ∈ set as. depends⇣0 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)
declare [[simp_depth_limit = 9]]
lemma I_lift_dnf_qe_anormal:
assumes "!!as. ∀a ∈ set as. depends⇣0 a ==> qfree(qe as)"
and "!!as. ∀a ∈ set as. depends⇣0 a ∧ anormal a ==> normal(qe as)"
and "!!xs as. ∀a ∈ set as. depends⇣0 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)
declare [[simp_depth_limit = 50]]
lemma I_lift_dnf_qe_anormal2:
assumes "qe : lists |depends⇣0| -> |qfree|"
and "qe : lists ( |depends⇣0| ∩ |anormal| ) -> |normal|"
and "∀as ∈ lists( |depends⇣0| ∩ |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 "ALL φ : |nqfree|. ALL 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 "ALL φ : |normal| Int |nqfree|. ALL 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 solvable⇣0 :: "'a => bool"
and trivial :: "'a => bool"
and subst⇣0 :: "'a => 'a => 'a"
assumes subst⇣0:
"[| solvable⇣0 eq; ¬trivial eq; I⇣a eq (x#xs); depends⇣0 a |]
==> I⇣a (subst⇣0 eq a) xs = I⇣a a (x#xs)"
and trivial: "trivial eq ==> I⇣a eq xs"
and solvable: "solvable⇣0 eq ==> ∃x. I⇣a eq (x#xs)"
and is_triv_self_subst: "solvable⇣0 eq ==> trivial (subst⇣0 eq eq)"
begin
definition lift_eq_qe :: "('a list => 'a fm) => 'a list => 'a fm" where
"lift_eq_qe qe as =
(let as = [a\<leftarrow>as. ¬ trivial a]
in case [a\<leftarrow>as. solvable⇣0 a] of
[] => qe as
| eq # eqs =>
(let ineqs = [a\<leftarrow>as. ¬ solvable⇣0 a]
in list_conj (map (Atom o (subst⇣0 eq)) (eqs @ ineqs))))"
theorem I_lift_eq_qe:
assumes dep: "∀a∈set as. depends⇣0 a"
assumes qe: "!!as. (∀a ∈ set as. depends⇣0 a ∧ ¬ solvable⇣0 a) ==>
I (qe as) xs = (∃x. ∀a ∈ set as. I⇣a a (x#xs))"
shows "I (lift_eq_qe qe as) xs = (∃x. ∀a ∈ set as. I⇣a a (x#xs))"
(is "?L = ?R")
proof -
let ?as = "[a\<leftarrow>as. ¬ trivial a]"
show ?thesis
proof (cases "[a\<leftarrow>?as. solvable⇣0 a]")
case Nil
hence "∀a∈set as. ¬ trivial a --> ¬ solvable⇣0 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" "solvable⇣0 eq" "¬ trivial eq"
by (auto simp: filter_eq_Cons_iff)
then obtain e where "I⇣a eq (e#xs)" by(metis solvable)
have "∀a ∈ set as. I⇣a a (e # xs) = I⇣a (subst⇣0 eq a) xs"
by(simp add: subst⇣0[OF `solvable⇣0 eq` `¬ trivial eq` `I⇣a 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 subst⇣0)
done
qed
qed;
definition "lift_dnfeq_qe = lift_dnf_qe o lift_eq_qe"
lemma qfree_lift_eq_qe:
"(!!as. ∀a∈set as. depends⇣0 a ==> qfree (qe as)) ==>
∀a∈set as. depends⇣0 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. depends⇣0 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. depends⇣0 a) ==> qfree(qe as)) ==>
(!!as. (∀a ∈ set as. depends⇣0 a ∧ ¬ solvable⇣0 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 |depends⇣0| -> |qfree| ==>
(∀as ∈ lists( |depends⇣0| ∩ - |solvable⇣0| ). 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