# Theory QEdlo

Up to index of Isabelle/HOL/LinearQuantifierElim

theory QEdlo
imports DLO Reflection
`(*  Author:     Tobias Nipkow, 2007  *)theory QEdloimports DLO "~~/src/HOL/Library/Reflection"beginsubsection "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 blastnext  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)qedlemma 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_defhide_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⇣0apply(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_defby(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`