# Theory QE

Up to index of Isabelle/HOL/LinearQuantifierElim

theory QE
imports Logic
(*  Author:     Tobias Nipkow, 2007  *)

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. depends0 a];
indep = [Atom(decr a). a\<leftarrow>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 @{text 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 o 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)"
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)))"

also have "… = (∃x. ∀a ∈ set(?as0 @ ?as1). Ia a (x#xs))"
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 φ)"

lemma qfree_lift_dnf_qe2: "qe : lists |depends0| -> |qfree|
==> qfree(lift_dnf_qe qe φ)"

using in_lists_conv_set[where ?'a = 'a]

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]

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 o 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)"
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)))"

also have "… = (∃x. ∀a ∈ set(?as0 @ ?as1). Ia a (x#xs))"
also have "… = (∃x. ∀a ∈ set(as). Ia a (x#xs))"
by simp blast
finally show ?thesis .
qed

declare [[simp_depth_limit = 5]]

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:split_if_asm)
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 φ)"
case ExQ thus ?case
apply (auto dest!: atoms_list_disjE)
apply(rule anormal_atoms_qelim)
prefer 3 apply assumption
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. 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)
declare [[simp_depth_limit = 50]]

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]

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 φ)"

lemma qfree_lift_nnf_qe2:
"qe : |nqfree| -> |qfree| ==> qfree(lift_nnf_qe 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"

lemma normal_lift_nnf_qe:
assumes "!!φ. nqfree φ ==> qfree(qe φ)"
and "!!φ. nqfree φ ==> normal φ ==> normal(qe φ)"
shows "normal φ ==> normal(lift_nnf_qe qe φ)"
by (induct φ)
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 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\<leftarrow>as. ¬ trivial a]
in case [a\<leftarrow>as. solvable0 a] of
[] => qe as
| eq # eqs =>
(let ineqs = [a\<leftarrow>as. ¬ solvable0 a]
in list_conj (map (Atom o (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\<leftarrow>as. ¬ trivial a]"
show ?thesis
proof (cases "[a\<leftarrow>?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
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 o 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)"

lemma qfree_lift_dnfeq_qe: "(!!as. (∀a∈set as. depends0 a) ==> qfree(qe as))
==> qfree(lift_dnfeq_qe 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"