# Theory Logic

(*  Author:     Tobias Nipkow, 2007  *)

section‹Logic›

theory Logic
imports Main "HOL-Library.FuncSet"
begin

text‹\noindent
using de Bruijn notation. The syntax is parametric in the type of atoms.›

declare Let_def[simp]

datatype (atoms: 'a) fm =
TrueF | FalseF | Atom 'a | And "'a fm" "'a fm" | Or "'a fm" "'a fm" |
Neg "'a fm" | ExQ "'a fm"

notation map_fm ("map⇩f⇩m")

abbreviation Imp where "Imp φ⇩1 φ⇩2 ≡ Or (Neg φ⇩1) φ⇩2"
abbreviation AllQ where "AllQ φ ≡ Neg(ExQ(Neg φ))"

definition neg where
"neg φ = (if φ=TrueF then FalseF else if φ=FalseF then TrueF else Neg φ)"

definition "and" :: "'a fm ⇒ 'a fm ⇒ 'a fm" where
"and φ⇩1 φ⇩2 =
(if φ⇩1=TrueF then φ⇩2 else if φ⇩2=TrueF then φ⇩1 else
if φ⇩1=FalseF ∨ φ⇩2=FalseF then FalseF else And φ⇩1 φ⇩2)"

definition or :: "'a fm ⇒ 'a fm ⇒ 'a fm" where
"or φ⇩1 φ⇩2 =
(if φ⇩1=FalseF then φ⇩2 else if φ⇩2=FalseF then φ⇩1 else
if φ⇩1=TrueF ∨ φ⇩2=TrueF then TrueF else Or φ⇩1 φ⇩2)"

definition list_conj :: "'a fm list ⇒ 'a fm" where
"list_conj fs = foldr and fs TrueF"

definition list_disj :: "'a fm list ⇒ 'a fm" where
"list_disj fs = foldr or fs FalseF"

abbreviation "Disj is f ≡ list_disj (map f is)"

lemmas atoms_map_fm[simp] = fm.set_map

fun amap_fm :: "('a ⇒ 'b fm) ⇒ 'a fm ⇒ 'b fm" ("amap⇩f⇩m") where
"amap⇩f⇩m h TrueF = TrueF" |
"amap⇩f⇩m h FalseF = FalseF" |
"amap⇩f⇩m h (Atom a) = h a" |
"amap⇩f⇩m h (And φ⇩1 φ⇩2) = and (amap⇩f⇩m h φ⇩1) (amap⇩f⇩m h φ⇩2)" |
"amap⇩f⇩m h (Or φ⇩1 φ⇩2) = or (amap⇩f⇩m h φ⇩1) (amap⇩f⇩m h φ⇩2)" |
"amap⇩f⇩m h (Neg φ) = neg (amap⇩f⇩m h φ)"

lemma amap_fm_list_disj:
"amap⇩f⇩m h (list_disj fs) = list_disj (map (amap⇩f⇩m h) fs)"
by(induct fs) (auto simp:list_disj_def or_def)

fun qfree :: "'a fm ⇒ bool" where
"qfree(ExQ f) = False" |
"qfree(And φ⇩1 φ⇩2) = (qfree φ⇩1 ∧ qfree φ⇩2)" |
"qfree(Or φ⇩1 φ⇩2) = (qfree φ⇩1 ∧ qfree φ⇩2)" |
"qfree(Neg φ) = (qfree φ)" |
"qfree φ = True"

lemma qfree_and[simp]: "⟦ qfree φ⇩1; qfree φ⇩2 ⟧ ⟹ qfree(and φ⇩1 φ⇩2)"

lemma qfree_or[simp]: "⟦ qfree φ⇩1; qfree φ⇩2 ⟧ ⟹ qfree(or φ⇩1 φ⇩2)"

lemma qfree_neg[simp]: "qfree(neg φ) = qfree φ"

lemma qfree_foldr_Or[simp]:
"qfree(foldr Or fs φ) = (qfree φ ∧ (∀φ ∈ set fs. qfree φ))"
by (induct fs) auto

lemma qfree_list_conj[simp]:
assumes "∀φ ∈ set fs. qfree φ" shows "qfree(list_conj fs)"
proof -
{ fix fs φ
have "⟦ ∀φ ∈ set fs. qfree φ; qfree φ ⟧ ⟹ qfree(foldr and fs φ)"
by (induct fs) auto
} thus ?thesis using assms by (fastforce simp add:list_conj_def)
qed

lemma qfree_list_disj[simp]:
assumes "∀φ ∈ set fs. qfree φ" shows "qfree(list_disj fs)"
proof -
{ fix fs φ
have "⟦ ∀φ ∈ set fs. qfree φ; qfree φ ⟧ ⟹ qfree(foldr or fs φ)"
by (induct fs) auto
} thus ?thesis using assms by (fastforce simp add:list_disj_def)
qed

lemma qfree_map_fm: "qfree (map⇩f⇩m f φ) = qfree φ"
by (induct φ) simp_all

lemma atoms_list_disjE:
"a ∈ atoms(list_disj fs) ⟹ a ∈ (⋃φ ∈ set fs. atoms φ)"
apply(induct fs)
apply (auto simp add:list_disj_def Logic.or_def split:if_split_asm)
done

lemma atoms_list_conjE:
"a ∈ atoms(list_conj fs) ⟹ a ∈ (⋃φ ∈ set fs. atoms φ)"
apply(induct fs)
apply (auto simp add:list_conj_def Logic.and_def split:if_split_asm)
done

fun dnf :: "'a fm ⇒ 'a list list" where
"dnf TrueF = [[]]" |
"dnf FalseF = []" |
"dnf (Atom φ) = [[φ]]" |
"dnf (And φ⇩1 φ⇩2) = [d1 @ d2. d1 ← dnf φ⇩1, d2 ← dnf φ⇩2]" |
"dnf (Or φ⇩1 φ⇩2) = dnf φ⇩1 @ dnf φ⇩2"

fun nqfree :: "'a fm ⇒ bool" where
"nqfree(Atom a) = True" |
"nqfree TrueF = True" |
"nqfree FalseF = True" |
"nqfree (And φ⇩1 φ⇩2) = (nqfree φ⇩1 ∧ nqfree φ⇩2)" |
"nqfree (Or φ⇩1 φ⇩2) = (nqfree φ⇩1 ∧ nqfree φ⇩2)" |
"nqfree φ = False"

lemma nqfree_qfree[simp]: "nqfree φ ⟹ qfree φ"
by (induct φ) simp_all

lemma nqfree_map_fm: "nqfree (map⇩f⇩m f φ) = nqfree φ"
by (induct φ) simp_all

fun "interpret" :: "('a ⇒ 'b list ⇒ bool) ⇒ 'a fm ⇒ 'b list ⇒ bool" where
"interpret h TrueF xs = True" |
"interpret h FalseF xs = False" |
"interpret h (Atom a) xs = h a xs" |
"interpret h (And φ⇩1 φ⇩2) xs = (interpret h φ⇩1 xs ∧ interpret h φ⇩2 xs)" |
"interpret h (Or φ⇩1 φ⇩2) xs = (interpret h φ⇩1 xs ∨ interpret h φ⇩2 xs)" |
"interpret h (Neg φ) xs = (¬ interpret h φ xs)" |
"interpret h (ExQ φ) xs = (∃x. interpret h φ (x#xs))"

subsection‹Atoms›

text‹The locale ATOM of atoms provides a minimal framework for the
generic formulation of theory-independent algorithms, in particular
quantifier elimination.›

locale ATOM =
fixes aneg :: "'a ⇒ 'a fm"
fixes anormal :: "'a ⇒ bool"
assumes nqfree_aneg: "nqfree(aneg a)"
assumes anormal_aneg: "anormal a ⟹ ∀b∈atoms(aneg a). anormal b"

fixes I⇩a :: "'a ⇒ 'b list ⇒ bool"
assumes I⇩a_aneg: "interpret I⇩a (aneg a) xs = (¬ I⇩a a xs)"

fixes depends⇩0 :: "'a ⇒ bool"
and decr :: "'a ⇒ 'a"
assumes not_dep_decr: "¬depends⇩0 a ⟹ I⇩a a (x#xs) = I⇩a (decr a) xs"
assumes anormal_decr: "¬ depends⇩0 a ⟹ anormal a ⟹ anormal(decr a)"

begin

fun atoms⇩0 :: "'a fm ⇒ 'a list" where
"atoms⇩0 TrueF = []" |
"atoms⇩0 FalseF = []" |
"atoms⇩0 (Atom a) = (if depends⇩0 a then [a] else [])" |
"atoms⇩0 (And φ⇩1 φ⇩2) = atoms⇩0 φ⇩1 @ atoms⇩0 φ⇩2" |
"atoms⇩0 (Or φ⇩1 φ⇩2) = atoms⇩0 φ⇩1 @ atoms⇩0 φ⇩2" |
"atoms⇩0 (Neg φ) = atoms⇩0 φ"

abbreviation I where "I ≡ interpret I⇩a"

fun nnf :: "'a fm ⇒ 'a fm" where
"nnf (And φ⇩1 φ⇩2) = And (nnf φ⇩1) (nnf φ⇩2)" |
"nnf (Or φ⇩1 φ⇩2) = Or (nnf φ⇩1) (nnf φ⇩2)" |
"nnf (Neg TrueF) = FalseF" |
"nnf (Neg FalseF) = TrueF" |
"nnf (Neg (Neg φ)) = (nnf φ)" |
"nnf (Neg (And φ⇩1 φ⇩2)) = (Or (nnf (Neg φ⇩1)) (nnf (Neg φ⇩2)))" |
"nnf (Neg (Or φ⇩1 φ⇩2)) = (And (nnf (Neg φ⇩1)) (nnf (Neg φ⇩2)))" |
"nnf (Neg (Atom a)) = aneg a" |
"nnf φ = φ"

lemma nqfree_nnf: "qfree φ ⟹ nqfree(nnf φ)"
by(induct φ rule:nnf.induct)

lemma qfree_nnf[simp]: "qfree(nnf φ) = qfree φ"
by (induct φ rule:nnf.induct)(simp_all add: nqfree_aneg)

lemma I_neg[simp]: "I (neg φ) xs = I (Neg φ) xs"

lemma I_and[simp]: "I (and φ⇩1 φ⇩2) xs = I (And φ⇩1 φ⇩2) xs"

lemma I_list_conj[simp]:
"I (list_conj fs) xs = (∀φ ∈ set fs. I φ xs)"
proof -
{ fix fs φ
have "I (foldr and fs φ) xs = (I φ xs ∧ (∀φ ∈ set fs. I φ xs))"
by (induct fs) auto
qed

lemma I_or[simp]: "I (or φ⇩1 φ⇩2) xs = I (Or φ⇩1 φ⇩2) xs"

lemma I_list_disj[simp]:
"I (list_disj fs) xs = (∃φ ∈ set fs. I φ xs)"
proof -
{ fix fs φ
have "I (foldr or fs φ) xs = (I φ xs ∨ (∃φ ∈ set fs. I φ xs))"
by (induct fs) auto
qed

lemma I_nnf: "I (nnf φ) xs = I φ xs"

lemma I_dnf:
"nqfree φ ⟹ (∃as∈set (dnf φ). ∀a∈set as. I⇩a a xs) = I φ xs"
by (induct φ) (fastforce)+

definition "normal φ = (∀a ∈ atoms φ. anormal a)"

lemma normal_simps[simp]:
"normal TrueF"
"normal FalseF"
"normal (Atom a) ⟷ anormal a"
"normal (And φ⇩1 φ⇩2) ⟷ normal φ⇩1 ∧ normal φ⇩2"
"normal (Or φ⇩1 φ⇩2) ⟷ normal φ⇩1 ∧ normal φ⇩2"
"normal (Neg φ) ⟷ normal φ"
"normal (ExQ φ) ⟷ normal φ"
by(auto simp:normal_def)

lemma normal_aneg[simp]: "anormal a ⟹ normal (aneg a)"

lemma normal_and[simp]:
"normal φ⇩1 ⟹ normal φ⇩2 ⟹ normal (and φ⇩1 φ⇩2)"

lemma normal_or[simp]:
"normal φ⇩1 ⟹ normal φ⇩2 ⟹ normal (or φ⇩1 φ⇩2)"

lemma normal_list_disj[simp]:
"∀φ∈set fs. normal φ ⟹ normal (list_disj fs)"
apply(induct fs)
done

lemma normal_nnf: "normal φ ⟹ normal(nnf φ)"
by(induct φ rule:nnf.induct) simp_all

lemma normal_map_fm:
"∀a. anormal(f a) = anormal(a) ⟹ normal (map⇩f⇩m f φ) = normal φ"
by(induct φ) auto

lemma anormal_nnf:
"qfree φ ⟹ normal φ ⟹ ∀a∈atoms(nnf φ). anormal a"
apply(induct φ rule:nnf.induct)
apply(unfold normal_def)
apply(simp_all)
apply (blast dest:anormal_aneg)+
done

lemma atoms_dnf: "nqfree φ ⟹ as ∈ set(dnf φ) ⟹ a ∈ set as ⟹ a ∈ atoms φ"
by(induct φ arbitrary: as a rule:nqfree.induct)(auto)

lemma anormal_dnf_nnf:
"as ∈ set(dnf(nnf φ)) ⟹ qfree φ ⟹ normal φ ⟹ a ∈ set as ⟹ anormal a"
apply(induct φ arbitrary: a as rule:nnf.induct)
apply clarify
apply (metis UnE set_append)
apply metis
apply metis
apply fastforce
apply (metis anormal_aneg atoms_dnf nqfree_aneg)
done

end

end


# 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. depends⇩0 a];
indep = [Atom(decr a). a←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 ‹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 ∘ 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)"
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)))"
also have "… = (∃x. ∀a ∈ set(?as0 @ ?as1). I⇩a a (x#xs))"
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 φ)"

lemma qfree_lift_dnf_qe2: "qe ∈ lists |depends⇩0| → |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. 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]

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

end

context notes [[simp_depth_limit = 9]]
begin

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)

end

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]

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 "∀φ ∈ |nqfree|. ∀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 "∀φ ∈ |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 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←as. ¬ trivial a]
in case [a←as. solvable⇩0 a] of
[] ⇒ qe as
| eq # eqs ⇒
(let ineqs = [a←as. ¬ solvable⇩0 a]
in list_conj (map (Atom ∘ (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←as. ¬ trivial a]"
show ?thesis
proof (cases "[a←?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
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 ∘ 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)"

lemma qfree_lift_dnfeq_qe: "(⋀as. (∀a∈set as. depends⇩0 a) ⟹ qfree(qe as))
⟹ qfree(lift_dnfeq_qe 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"

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]

end

end


# Theory DLO

(*  Author:     Tobias Nipkow, 2007  *)

section "DLO"

theory DLO
imports QE Complex_Main
begin

subsection "Basics"

class dlo = linorder +
assumes dense: "x < z ⟹ ∃y. x < y ∧ y < z"
and no_ub: "∃u. x < u" and no_lb: "∃l. l < x"

instance real :: dlo
proof
fix r s :: real
let ?v = "(r + s) / 2"
assume "r < s"
hence "r < ?v ∧ ?v < s" by simp
thus "∃v. r < v ∧ v < s" ..
next
fix r :: real
have "r < r + 1" by arith
thus "∃s. r < s" ..
next
fix r :: real
have "r - 1 < r" by arith
thus "∃s. s < r" ..
qed

datatype atom = Less nat nat | Eq nat nat

fun is_Less :: "atom ⇒ bool" where
"is_Less (Less i j) = True" |
"is_Less f = False"

abbreviation "is_Eq ≡ Not ∘ is_Less"

lemma is_Less_iff: "is_Less a = (∃i j. a = Less i j)"
by(cases a) auto
lemma is_Eq_iff: "(∀i j. a ≠ Less i j) = (∃i j. a = Eq i j)"
by(cases a) auto
lemma not_is_Eq_iff: "(∀i j. a ≠ Eq i j) = (∃i j. a = Less i j)"
by(cases a) auto

fun neg⇩d⇩l⇩o :: "atom ⇒ atom fm" where
"neg⇩d⇩l⇩o (Less i j) = Or (Atom(Less j i)) (Atom(Eq i j))" |
"neg⇩d⇩l⇩o (Eq i j) = Or (Atom(Less i j)) (Atom(Less j i))"

fun I⇩d⇩l⇩o :: "atom ⇒ 'a::dlo list ⇒ bool" where
"I⇩d⇩l⇩o (Eq i j) xs = (xs!i = xs!j)" |
"I⇩d⇩l⇩o (Less i j) xs = (xs!i < xs!j)"

fun depends⇩d⇩l⇩o :: "atom ⇒ bool" where
"depends⇩d⇩l⇩o(Eq i j) = (i=0 | j=0)" |
"depends⇩d⇩l⇩o(Less i j) = (i=0 | j=0)"

fun decr⇩d⇩l⇩o :: "atom ⇒ atom" where
"decr⇩d⇩l⇩o (Less i j) = Less (i - 1) (j - 1)" |
"decr⇩d⇩l⇩o (Eq i j) = Eq (i - 1) (j - 1)"

(* needed for code generation *)
definition [code del]: "nnf = ATOM.nnf neg⇩d⇩l⇩o"
definition [code del]: "qelim = ATOM.qelim depends⇩d⇩l⇩o decr⇩d⇩l⇩o"
definition [code del]: "lift_dnf_qe = ATOM.lift_dnf_qe neg⇩d⇩l⇩o depends⇩d⇩l⇩o decr⇩d⇩l⇩o"
definition [code del]: "lift_nnf_qe = ATOM.lift_nnf_qe neg⇩d⇩l⇩o"

hide_const nnf qelim lift_dnf_qe lift_nnf_qe

lemmas DLO_code_lemmas = nnf_def qelim_def lift_dnf_qe_def lift_nnf_qe_def

interpretation DLO:
ATOM neg⇩d⇩l⇩o "(λa. True)" I⇩d⇩l⇩o depends⇩d⇩l⇩o decr⇩d⇩l⇩o
apply(unfold_locales)
apply(case_tac a)
apply simp_all
apply(case_tac a)
linorder_not_less linorder_neq_iff)
apply(case_tac a)
done

lemmas [folded DLO_code_lemmas, code] =
DLO.nnf.simps DLO.qelim_def DLO.lift_dnf_qe.simps DLO.lift_dnf_qe.simps

setup ‹Sign.revert_abbrev "" @{const_abbrev DLO.I}›

definition lbounds where "lbounds as = [i. Less (Suc i) 0 ← as]"
definition ubounds where "ubounds as = [i. Less 0 (Suc i) ← as]"
definition ebounds where
"ebounds as = [i. Eq (Suc i) 0 ← as] @ [i. Eq 0 (Suc i) ← as]"

lemma set_lbounds: "set(lbounds as) = {i. Less (Suc i) 0 ∈ set as}"
by(auto simp: lbounds_def split:nat.splits atom.splits)
lemma set_ubounds: "set(ubounds as) = {i. Less 0 (Suc i) ∈ set as}"
by(auto simp: ubounds_def split:nat.splits atom.splits)
lemma set_ebounds:
"set(ebounds as) = {k. Eq (Suc k) 0 ∈ set as ∨ Eq 0 (Suc k) ∈ set as}"
by(auto simp: ebounds_def split: atom.splits nat.splits)

abbreviation "LB f xs ≡ {xs!i|i. Less (Suc i) 0 ∈ set(DLO.atoms⇩0 f)}"
abbreviation "UB f xs ≡ {xs!i|i. Less 0 (Suc i) ∈ set(DLO.atoms⇩0 f)}"
definition "EQ f xs = {xs!k|k.
Eq (Suc k) 0 ∈ set(DLO.atoms⇩0 f) ∨ Eq 0 (Suc k) ∈ set(DLO.atoms⇩0 f)}"

lemma EQ_And[simp]: "EQ (And f g) xs = (EQ f xs ∪ EQ g xs)"
by(auto simp:EQ_def)

lemma EQ_Or[simp]: "EQ (Or f g) xs = (EQ f xs ∪ EQ g xs)"
by(auto simp:EQ_def)

lemma EQ_conv_set_ebounds:
"x ∈ EQ f xs = (∃e∈set(ebounds(DLO.atoms⇩0 f)). x = xs!e)"
by(auto simp: EQ_def set_ebounds)

fun isubst where "isubst k 0 = k" | "isubst k (Suc i) = i"

fun asubst :: "nat ⇒ atom ⇒ atom" where
"asubst k (Less i j) = Less (isubst k i) (isubst k j)"|
"asubst k (Eq i j) = Eq (isubst k i) (isubst k j)"

abbreviation "subst φ k ≡ map⇩f⇩m (asubst k) φ"

lemma I_subst:
"qfree f ⟹ DLO.I (subst f k) xs = DLO.I f (xs!k # xs)"
apply(induct f)
apply(simp_all)
apply(rename_tac a)
apply(case_tac a)
done

fun amin_inf :: "atom ⇒ atom fm" where
"amin_inf (Less _ 0) = FalseF" |
"amin_inf (Less 0 _) = TrueF" |
"amin_inf (Less (Suc i) (Suc j)) = Atom(Less i j)" |
"amin_inf (Eq 0 0) = TrueF" |
"amin_inf (Eq 0 _) = FalseF" |
"amin_inf (Eq _ 0) = FalseF" |
"amin_inf (Eq (Suc i) (Suc j)) = Atom(Eq i j)"

abbreviation min_inf :: "atom fm ⇒ atom fm" ("inf⇩-") where
"inf⇩- ≡ amap⇩f⇩m amin_inf"

fun aplus_inf :: "atom ⇒ atom fm" where
"aplus_inf (Less 0 _) = FalseF" |
"aplus_inf (Less _ 0) = TrueF" |
"aplus_inf (Less (Suc i) (Suc j)) = Atom(Less i j)" |
"aplus_inf (Eq 0 0) = TrueF" |
"aplus_inf (Eq 0 _) = FalseF" |
"aplus_inf (Eq _ 0) = FalseF" |
"aplus_inf (Eq (Suc i) (Suc j)) = Atom(Eq i j)"

abbreviation plus_inf :: "atom fm ⇒ atom fm" ("inf⇩+") where
"inf⇩+ ≡ amap⇩f⇩m aplus_inf"

lemma min_inf:
"nqfree f ⟹ ∃x. ∀y≤x. DLO.I (inf⇩- f) xs = DLO.I f (y # xs)"
(is "_ ⟹ ∃x. ?P f x")
proof(induct f)
case (Atom a)
show ?case
proof (cases a rule: amin_inf.cases)
case 1 thus ?thesis by(auto simp add:nth_Cons' linorder_not_less)
next
case 2 thus ?thesis
by (simp) (metis no_lb linorder_not_less order_less_le_trans)
next
case 5 thus ?thesis
next
case 6 thus ?thesis by simp (metis no_lb linorder_not_less)
qed simp_all
next
case (And f1 f2)
then obtain x1 x2 where "?P f1 x1" "?P f2 x2" by fastforce+
hence "?P (And f1 f2) (min x1 x2)" by(force simp:and_def)
thus ?case ..
next
case (Or f1 f2)
then obtain x1 x2 where "?P f1 x1" "?P f2 x2" by fastforce+
hence "?P (Or f1 f2) (min x1 x2)" by(force simp:or_def)
thus ?case ..
qed simp_all

lemma plus_inf:
"nqfree f ⟹ ∃x.∀y≥x. DLO.I (inf⇩+ f) xs = DLO.I f (y # xs)"
(is "_ ⟹ ∃x. ?P f x")
proof (induct f)
have dlo_bound: "⋀z::'a. ∃x. ∀y≥x. y > z"
proof -
fix z
from no_ub obtain w :: 'a where "w > z" ..
then have "∀y≥w. y > z" by auto
then show "?thesis z" ..
qed
case (Atom a)
show ?case
proof (cases a rule: aplus_inf.cases)
case 1 thus ?thesis
by (simp add: nth_Cons') (metis linorder_not_less)
next
case 2 thus ?thesis by (auto intro: dlo_bound)
next
case 5 thus ?thesis
by simp (metis dlo_bound less_imp_neq)
next
case 6 thus ?thesis
by simp (metis dlo_bound less_imp_neq)
qed simp_all
next
case (And f1 f2)
then obtain x1 x2 where "?P f1 x1" "?P f2 x2" by fastforce+
hence "?P (And f1 f2) (max x1 x2)" by(force simp:and_def)
thus ?case ..
next
case (Or f1 f2)
then obtain x1 x2 where "?P f1 x1" "?P f2 x2" by fastforce+
hence "?P (Or f1 f2) (max x1 x2)" by(force simp:or_def)
thus ?case ..
qed simp_all

context notes [[simp_depth_limit=2]]
begin

lemma LBex:
"⟦ nqfree f; DLO.I f (x#xs); ¬DLO.I (inf⇩- f) xs; x ∉ EQ f xs ⟧
⟹ ∃l∈ LB f xs. l < x"
proof(induct f)
case (Atom a) thus ?case
by (cases a rule: amin_inf.cases)
(simp_all add: nth.simps EQ_def split: nat.splits)
qed auto

lemma UBex:
"⟦ nqfree f; DLO.I f (x#xs); ¬DLO.I (inf⇩+ f) xs; x ∉ EQ f xs ⟧
⟹ ∃u ∈ UB f xs. x < u"
proof(induct f)
case (Atom a) thus ?case
by (cases a rule: aplus_inf.cases)
(simp_all add: nth.simps EQ_def split: nat.splits)
qed auto

end

lemma finite_LB: "finite(LB f xs)"
proof -
have "LB f xs = (λk. xs!k)  set(lbounds(DLO.atoms⇩0 f))"
by (auto simp:set_lbounds image_def)
thus ?thesis by simp
qed

lemma finite_UB: "finite(UB f xs)"
proof -
have "UB f xs = (λk.  xs!k)  set(ubounds(DLO.atoms⇩0 f))"
by (auto simp:set_ubounds image_def)
thus ?thesis by simp
qed

lemma qfree_amin_inf: "qfree (amin_inf a)"
by(cases a rule:amin_inf.cases) simp_all

lemma qfree_min_inf: "nqfree φ ⟹ qfree(inf⇩- φ)"

lemma qfree_aplus_inf: "qfree (aplus_inf a)"
by(cases a rule:aplus_inf.cases) simp_all

lemma qfree_plus_inf: "nqfree φ ⟹ qfree(inf⇩+ φ)"

end


# Theory QEdlo

(*  Author:     Tobias Nipkow, 2007  *)

theory QEdlo
imports DLO
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 ← as]; ubs = [j. Less 0 (Suc j) ← as];
pairs = [Atom(Less i j). i ← lbs, j ← 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 ← as]"
let ?ubs = "[j. Less 0 (Suc j) ← as]"
let ?Ls = "set ?lbs" let ?Us = "set ?ubs"
let ?lb = "Max (⋃x∈?Ls. {xs!x})"
let ?ub = "Min (⋃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 (⋃x∈?Ls. {xs!x}) < Min (⋃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 if_split_asm)
apply(fastforce simp:subst_def nth_Cons' 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 φ)"

end


# Theory QEdlo_ex

(*  Author:     Tobias Nipkow, 2007  *)

theory QEdlo_ex imports QEdlo
begin

(* tweaking the reflection setup *)

definition "interpret" :: "atom fm ⇒ 'a::dlo list ⇒ bool" where
"interpret = Logic.interpret I⇩d⇩l⇩o"

lemma interpret_Atoms:
"interpret (Atom (Eq i j)) xs = (xs!i = xs!j)"
"interpret (Atom (Less i j)) xs = (xs!i < xs!j)"

lemma interpret_others:
"interpret (Neg(ExQ (Neg f))) xs = (∀x. interpret f (x#xs))"
"interpret (Or (Neg f1) f2) xs = (interpret f1 xs ⟶ interpret f2 xs)"

lemmas reify_eqs =
Logic.interpret.simps(1,2,4-7)[of I⇩d⇩l⇩o, folded interpret_def]
interpret_others interpret_Atoms

method_setup dlo_reify = ‹
Scan.succeed
(fn ctxt =>
Method.SIMPLE_METHOD' (Reification.tac ctxt @{thms reify_eqs} NONE
THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm"interpret_def"}])))
› "dlo reification"

(* leave just enough equations in to convert back to True/False by eval *)
declare I⇩d⇩l⇩o.simps(1)[code]
declare Logic.interpret.simps[code del]
declare Logic.interpret.simps(1-2)[code]

subsection‹Examples›

lemma "∀x::real. ¬ x < x"
apply dlo_reify
apply (subst I_qe_dlo [symmetric])
by eval

lemma "∀x y::real. ∃z. x < y ⟶ x < z ∧ z < y"
apply dlo_reify
apply (subst I_qe_dlo [symmetric])
by eval

lemma "∃ x::real. a+b < x ∧ x < c*d"
apply dlo_reify
apply (subst I_qe_dlo [symmetric])
apply normalization
oops

lemma "∀x::real. ¬ x < x"
apply dlo_reify
apply (subst I_qe_dlo [symmetric])
by eval

lemma "∀x y::real. ∃z. x < y ⟶ x < z ∧ z < y"
apply dlo_reify
apply (subst I_qe_dlo [symmetric])
by eval

(* 160 secs *)
lemma "¬(∃x y z. ∀u::real. x < x ∨ ¬ x<u ∨ x<y ∧ y<z ∧ ¬ x<z)"
apply dlo_reify
apply (subst I_qe_dlo [symmetric])
by eval

lemma "qe_dlo(AllQ (Imp (Atom(Less 0 1)) (Atom(Less 1 0)))) = FalseF"
by eval

lemma "qe_dlo(AllQ(AllQ (Imp (Atom(Less 0 1)) (Atom(Less 0 1))))) = TrueF"
by eval

lemma
"qe_dlo(AllQ(ExQ(AllQ (And (Atom(Less 2 1)) (Atom(Less 1 0)))))) = FalseF"
by eval

lemma "qe_dlo(AllQ(ExQ(ExQ (And (Atom(Less 1 2)) (Atom(Less 2 0)))))) = TrueF"
by eval

lemma
"qe_dlo(AllQ(AllQ(ExQ (And (Atom(Less 1 0)) (Atom(Less 0 2)))))) = FalseF"
by eval

lemma "qe_dlo(AllQ(AllQ(ExQ (Imp (Atom(Less 1 2)) (And (Atom(Less 1 0)) (Atom(Less 0 2))))))) = TrueF"
by eval

value "qe_dlo(AllQ (Imp (Atom(Less 0 1)) (Atom(Less 0 2))))"

end


# Theory QEdlo_fr

(*  Author:     Tobias Nipkow, 2007  *)

theory QEdlo_fr
imports DLO
begin

subsection "Interior Point Method"

text‹This section formalizes a new quantifier elimination procedure
based on the idea of Ferrante and Rackoff~\cite{FerranteR-SIAM75} (see
also \S\ref{sec:FRE}) of taking a point between each lower and upper
bound as a test point. For dense linear orders it is not obvious how
to realize this because we cannot name any intermediate point
directly.›

fun asubst⇩2 :: "nat ⇒ nat ⇒ atom ⇒ atom fm" where
"asubst⇩2 l u (Less 0 0) = FalseF" |
"asubst⇩2 l u (Less 0 (Suc j)) = Or (Atom(Less u j)) (Atom(Eq u j))" |
"asubst⇩2 l u (Less (Suc i) 0) = Or (Atom(Less i l)) (Atom(Eq i l))" |
"asubst⇩2 l u (Less (Suc i) (Suc j)) = Atom(Less i j)" |
"asubst⇩2 l u (Eq 0 0) = TrueF" |
"asubst⇩2 l u (Eq 0 _) = FalseF" |
"asubst⇩2 l u (Eq _ 0) = FalseF" |
"asubst⇩2 l u (Eq (Suc i) (Suc j)) = Atom(Eq i j)"

abbreviation "subst⇩2 l u ≡ amap⇩f⇩m (asubst⇩2 l u)"

lemma I_subst⇩21:
"nqfree f ⟹ xs!l < xs!u ⟹ DLO.I (subst⇩2 l u f) xs
⟹ xs!l < x ⟹ x < xs!u ⟹ DLO.I f (x#xs)"
proof(induct f arbitrary: x)
case (Atom a) thus ?case
by (cases "(l,u,a)" rule: asubst⇩2.cases) auto
qed auto

definition
"nolub f xs l x u ⟷ (∀y∈{l<..<x}. y ∉ LB f xs) ∧ (∀y∈{x<..<u}. y ∉ UB f xs)"

lemma nolub_And[simp]:
"nolub (And f g) xs l x u = (nolub f xs l x u ∧ nolub g xs l x u)"
by(auto simp:nolub_def)

lemma nolub_Or[simp]:
"nolub (Or f g) xs l x u = (nolub f xs l x u ∧ nolub g xs l x u)"
by(auto simp:nolub_def)

context notes [[simp_depth_limit=3]]
begin

lemma innermost_intvl:
"⟦ nqfree f; nolub f xs l x u; l < x; x < u; x ∉ EQ f xs;
DLO.I f (x#xs); l < y; y < u⟧
⟹ DLO.I f (y#xs)"
proof(induct f)
case (Atom a)
show ?case
proof (cases a)
case (Less i j)
then show ?thesis using Atom
unfolding nolub_def
by (clarsimp simp: nth.simps Ball_def split:if_split_asm nat.splits)
(metis not_le_imp_less order_antisym order_less_trans)+
next
case [simp]: (Eq i j)
show ?thesis
proof (cases i)
case [simp]: 0
show ?thesis
proof (cases j)
case 0 thus ?thesis using Atom by simp
next
case Suc thus ?thesis using Atom by(simp add:EQ_def)
qed
next
case [simp]: Suc
show ?thesis
proof (cases j)
case 0 thus ?thesis using Atom by(simp add:EQ_def)
next
case Suc thus ?thesis using Atom by simp
qed
qed
qed
next
case (And f1 f2) thus ?case by (fastforce)
next
case (Or f1 f2) thus ?case by (fastforce)
qed simp+

lemma I_subst⇩22:
"nqfree f ⟹ xs!l < x ∧ x < xs!u ⟹ nolub f xs (xs!l) x (xs!u)
⟹ ∀x∈{xs!l <..< xs!u}. DLO.I f (x#xs) ∧ x ∉ EQ f xs
⟹ DLO.I (subst⇩2 l u f) xs"
proof (induct f)
case (Atom a) show ?case
apply (cases "(l,u,a)" rule: asubst⇩2.cases)
apply(insert Atom, auto simp: EQ_def nolub_def split:if_split_asm)
done
next
case Or thus ?case by (simp add: Ball_def)(metis innermost_intvl)
qed auto

end

definition
"qe_interior⇩1 φ =
(let as = DLO.atoms⇩0 φ; lbs = lbounds as; ubs = ubounds as; ebs = ebounds as;
intrs = [And (Atom(Less l u)) (subst⇩2 l u φ). l←lbs, u←ubs]
in list_disj (inf⇩- φ # inf⇩+ φ # intrs @ map (subst φ) ebs))"

lemma dense_interval:
assumes "finite L" "finite U" "l ∈ L" "u ∈ U" "l < x" "x < u" "P(x::'a::dlo)"
and dense: "⋀y l u. ⟦ ∀y∈{l<..<x}. y ∉ L;  ∀y∈{x<..<u}. y ∉ U;
l<x;x<u; l<y;y<u ⟧ ⟹ P y"
shows "∃l∈L.∃u∈U. l<x ∧ x<u ∧ (∀y∈{l<..<x}. y∉L) ∧ (∀y∈{x<..<u}. y∉U)
∧ (∀y. l<y ∧ y<u ⟶ P y)"
proof -
let ?L = "{l:L. l < x}" let ?U = "{u:U. x < u}"
let ?ll = "Max ?L" let ?uu = "Min ?U"
have "?L ≠ {}" using ‹l ∈ L› ‹l<x› by (blast intro:order_less_imp_le)
moreover have "?U ≠ {}" using ‹u:U› ‹x<u› by (blast intro:order_less_imp_le)
ultimately have "∀y. ?ll<y ∧ y<x ⟶ y ∉ L" "∀y. x<y ∧ y<?uu ⟶ y ∉ U"
using ‹finite L› ‹finite U› by force+
moreover have "?ll ∈ L"
proof
show "?ll ∈ ?L" using ‹finite L› Max_in[OF _ ‹?L ≠ {}›] by simp
show "?L ⊆ L" by blast
qed
moreover have "?uu ∈ U"
proof
show "?uu ∈ ?U" using ‹finite U› Min_in[OF _ ‹?U ≠ {}›] by simp
show "?U ⊆ U" by blast
qed
moreover have "?ll < x" using ‹finite L› ‹?L ≠ {}› by simp
moreover have "x < ?uu" using ‹finite U› ‹?U ≠ {}› by simp
moreover have "?ll < ?uu" using ‹?ll<x› ‹x<?uu› by simp
ultimately show ?thesis using ‹l < x› ‹x < u› ‹?L ≠ {}› ‹?U ≠ {}›
by(blast intro!:dense greaterThanLessThan_iff[THEN iffD1])
qed

theorem I_interior1:
assumes "nqfree φ" shows "DLO.I (qe_interior⇩1 φ) xs = (∃x. DLO.I φ (x#xs))"
(is "?QE = ?EX")
proof
assume ?QE
{ assume "DLO.I (inf⇩- φ) xs"
hence ?EX using ‹?QE› min_inf[of φ xs] ‹nqfree φ›
} moreover
{ assume  "DLO.I (inf⇩+ φ) xs"
hence ?EX using ‹?QE› plus_inf[of φ xs] ‹nqfree φ›
} moreover
{ assume "¬DLO.I (inf⇩- φ) xs ∧ ¬DLO.I (inf⇩+ φ) xs ∧
(∀x∈EQ φ xs. ¬DLO.I φ (x#xs))"
with ‹?QE› ‹nqfree φ› obtain l u
where "DLO.I (subst⇩2 l u φ) xs" and "xs!l < xs!u"
by(fastforce simp: qe_interior⇩1_def set_lbounds set_ubounds I_subst EQ_conv_set_ebounds)
moreover then obtain x where "xs!l < x ∧ x < xs!u" by(metis dense)
ultimately have "DLO.I φ (x # xs)"
using ‹nqfree φ› I_subst⇩21[OF ‹nqfree φ› ‹xs!l < xs!u›] by simp
hence ?EX .. }
ultimately show ?EX by blast
next
let ?as = "DLO.atoms⇩0 φ" let ?E = "set(ebounds ?as)"
assume ?EX
then obtain x where x: "DLO.I φ (x#xs)" ..
{ assume "DLO.I (inf⇩- φ) xs ∨ DLO.I (inf⇩+ φ) xs"
hence ?QE using ‹nqfree φ› by(auto simp:qe_interior⇩1_def)
} moreover
{ assume "∃k ∈ ?E. DLO.I (subst φ k) xs"
hence ?QE by(force simp:qe_interior⇩1_def) } moreover
{ assume "¬ DLO.I (inf⇩- φ) xs" and "¬ DLO.I (inf⇩+ φ) xs"
and "∀k ∈ ?E. ¬ DLO.I (subst φ k) xs"
hence noE: "∀e ∈ EQ φ xs. ¬ DLO.I φ (e#xs)"
using ‹nqfree φ› by (force simp:set_ebounds EQ_def I_subst)
hence "x ∉ EQ φ xs" using x by fastforce
obtain l where "l ∈ LB φ xs" "l < x"
using LBex[OF ‹nqfree φ› x ‹¬ DLO.I(inf⇩- φ) xs› ‹x ∉ EQ φ xs›] ..
obtain u where "u ∈ UB φ xs" "x < u"
using UBex[OF ‹nqfree φ› x ‹¬ DLO.I(inf⇩+ φ) xs› ‹x ∉ EQ φ xs›] ..
have "∃l∈LB φ xs. ∃u∈UB φ xs. l<x ∧ x<u ∧ nolub φ xs l x u ∧ (∀y. l < y ∧ y < u ⟶ DLO.I φ (y#xs))"
using dense_interval[where P = "λx. DLO.I φ (x#xs)", OF finite_LB finite_UB ‹l:LB φ xs› ‹u:UB φ xs› ‹l<x› ‹x<u› x] x innermost_intvl[OF ‹nqfree φ› _ _ _ ‹x ∉ EQ φ xs›]
then obtain m n where
"Less (Suc m) 0 ∈ set ?as" "Less 0 (Suc n) ∈ set ?as"
"xs!m < x ∧ x < xs!n"
"nolub φ xs (xs!m) x (xs!n)"
"∀y. xs!m < y ∧ y < xs!n ⟶ DLO.I φ (y#xs)"
by blast
moreover
hence "DLO.I (subst⇩2 m n φ) xs" using noE
by(force intro!: I_subst⇩22[OF ‹nqfree φ›])
ultimately have ?QE
by(fastforce simp add:qe_interior⇩1_def bex_Un set_lbounds set_ubounds)
} ultimately show ?QE by blast
qed

lemma qfree_asubst⇩2: "qfree (asubst⇩2 l u a)"
by(cases "(l,u,a)" rule:asubst⇩2.cases) simp_all

lemma qfree_subst⇩2: "nqfree φ ⟹ qfree (subst⇩2 l u φ)"

lemma qfree_interior1: "nqfree φ ⟹ qfree(qe_interior⇩1 φ)"
apply(rule qfree_list_disj)
apply (auto simp:qfree_min_inf qfree_plus_inf qfree_subst⇩2 qfree_map_fm)
done

definition "qe_interior = DLO.lift_nnf_qe qe_interior⇩1"

lemma qfree_qe_interior: "qfree(qe_interior φ)"

lemma I_qe_interior: "DLO.I (qe_interior φ) xs = DLO.I φ xs"

end


# Theory QEdlo_inf

(*  Author:     Tobias Nipkow, 2007  *)

theory QEdlo_inf
imports DLO
begin

subsection "Quantifier elimination with infinitesimals"

text‹This section presents a new quantifier elimination procedure
for dense linear orders based on (the simulation of) infinitesimals.
It is a fairly straightforward adaptation of the analogous algorithm
by Loos and Weispfenning for linear arithmetic described in
\S\ref{sec:lin-inf}.›

fun asubst_peps :: "nat ⇒ atom ⇒ atom fm" ("asubst⇩+") where
"asubst_peps k (Less 0 0) = FalseF" |
"asubst_peps k (Less 0 (Suc j)) = Atom(Less k j)" |
"asubst_peps k (Less (Suc i) 0) = (if i=k then TrueF
else Or (Atom(Less i k)) (Atom(Eq i k)))" |
"asubst_peps k (Less (Suc i) (Suc j)) = Atom(Less i j)" |
"asubst_peps k (Eq 0 0) = TrueF" |
"asubst_peps k (Eq 0 _) = FalseF" |
"asubst_peps k (Eq _ 0) = FalseF" |
"asubst_peps k (Eq (Suc i) (Suc j)) = Atom(Eq i j)"

abbreviation subst_peps :: "atom fm ⇒ nat ⇒ atom fm" ("subst⇩+") where
"subst⇩+ φ k ≡ amap⇩f⇩m (asubst⇩+ k) φ"

definition "nolb φ xs l x = (∀y∈{l<..<x}. y ∉ LB φ xs)"

lemma nolb_And[simp]:
"nolb (And φ⇩1 φ⇩2) xs l x = (nolb φ⇩1 xs l x ∧ nolb φ⇩2 xs l x)"
apply(clarsimp simp:nolb_def)
apply blast
done

lemma nolb_Or[simp]:
"nolb (Or φ⇩1 φ⇩2) xs l x = (nolb φ⇩1 xs l x ∧ nolb φ⇩2 xs l x)"
apply(clarsimp simp:nolb_def)
apply blast
done

context notes [[simp_depth_limit=3]]
begin

lemma innermost_intvl:
"⟦ nqfree φ; nolb φ xs l x; l < x; x ∉ EQ φ xs; DLO.I φ (x#xs); l < y; y ≤ x⟧
⟹ DLO.I φ (y#xs)"
proof(induct φ)
case (Atom a)
show ?case
proof (cases a)
case (Less i j)
then show ?thesis using Atom
unfolding nolb_def
by (clarsimp simp: nth.simps Ball_def split:if_split_asm nat.splits)
(metis not_le_imp_less order_antisym order_less_trans)+
next
case (Eq i j) thus ?thesis using Atom
apply(clarsimp simp:EQ_def nolb_def nth_Cons')
apply(case_tac "i=0 ∧ j=0") apply simp
apply(case_tac "i≠0 ∧ j≠0") apply simp
apply(case_tac "i=0 ∧ j≠0") apply (fastforce split:if_split_asm)
apply(case_tac "i≠0 ∧ j=0") apply (fastforce split:if_split_asm)
apply arith
done
qed
next
case And thus ?case by (fastforce)
next
case Or thus ?case by (fastforce)
qed simp+

lemma I_subst_peps2:
"nqfree φ ⟹ xs!l < x ⟹ nolb φ xs (xs!l) x ⟹ x ∉ EQ φ xs
⟹ ∀y ∈ {xs!l <.. x}. DLO.I φ (y#xs)
⟹ DLO.I (subst⇩+ φ l) xs"
proof(induct φ)
case FalseF thus ?case
by simp (metis antisym_conv1 linorder_neq_iff)
next
case (Atom a)
show ?case
proof(cases "(l,a)" rule:asubst_peps.cases)
case 3 thus ?thesis using Atom
by (auto simp: nolb_def EQ_def Ball_def)
(metis One_nat_def antisym_conv1 not_less_iff_gr_or_eq)
qed (insert Atom, auto simp: nolb_def EQ_def Ball_def)
next
case Or thus ?case by(simp add: Ball_def)(metis order_refl innermost_intvl)
qed simp_all

end

lemma dense_interval:
assumes "finite L" "l ∈ L" "l < x" "P(x::'a::dlo)"
and dense: "⋀y l. ⟦ ∀y∈{l<..<x}. y ∉ L; l<x; l<y; y≤x ⟧ ⟹ P y"
shows "∃l∈L. l<x ∧ (∀y∈{l<..<x}. y ∉ L) ∧ (∀y. l<y ∧ y≤x ⟶ P y)"
proof -
let ?L = "{l∈L. l < x}"
let ?ll = "Max ?L"
have "?L ≠ {}" using ‹l ∈ L› ‹l<x› by (blast intro:order_less_imp_le)
hence "∀y. ?ll<y ∧ y<x ⟶ y ∉ L" using ‹finite L› by force
moreover have "?ll ∈ L"
proof
show "?ll ∈ ?L" using ‹finite L› Max_in[OF _ ‹?L ≠ {}›] by simp
show "?L ⊆ L" by blast
qed
moreover have "?ll < x" using ‹finite L› ‹?L ≠ {}› by simp
ultimately show ?thesis using ‹l < x› ‹?L ≠ {}›
by(blast intro!:dense greaterThanLessThan_iff[THEN iffD1])
qed

lemma I_subst_peps:
"nqfree φ ⟹ DLO.I (subst⇩+ φ l) xs ⟶
(∃leps>xs!l. ∀x. xs!l < x ∧ x ≤ leps ⟶ DLO.I φ (x#xs))"
proof(induct φ)
case TrueF thus ?case by simp (metis no_ub)
next
case (Atom a)
show ?case
proof (cases "(l,a)" rule: asubst_peps.cases)
case 2 thus ?thesis using Atom
apply(auto)
apply(drule dense)
apply(metis One_nat_def xt1(7))
done
next
case 3 thus ?thesis using Atom
apply(auto)
apply (metis no_ub)
apply (metis no_ub less_trans)
apply (metis no_ub)
done
next
case 4 thus ?thesis using Atom by(auto)(metis no_ub)
next
case 5 thus ?thesis using Atom by(auto)(metis no_ub)
next
case 8 thus ?thesis using Atom by(auto)(metis no_ub)
qed (insert Atom, auto)
next
case And thus ?case
apply clarsimp
apply(rule_tac x="min leps lepsa" in exI)
apply simp
done
next
case Or thus ?case by force
qed simp_all

definition
"qe_eps⇩1(φ) =
(let as = DLO.atoms⇩0 φ; lbs = lbounds as; ebs = ebounds as
in list_disj (inf⇩- φ # map (subst⇩+ φ) lbs @ map (subst φ) ebs))"

theorem I_qe_eps1:
assumes "nqfree φ" shows "DLO.I (qe_eps⇩1 φ) xs = (∃x. DLO.I φ (x#xs))"
(is "?QE = ?EX")
proof
let ?as = "DLO.atoms⇩0 φ" let ?ebs = "ebounds ?as"
assume ?QE
{ assume "DLO.I (inf⇩- φ) xs"
hence ?EX using ‹?QE› min_inf[of φ xs] ‹nqfree φ›
} moreover
{ assume "∀i ∈ set ?ebs. ¬DLO.I φ (xs!i # xs)"
"¬ DLO.I (inf⇩- φ) xs"
with ‹?QE› ‹nqfree φ› obtain l where "DLO.I (subst⇩+ φ l) xs"
by(fastforce simp: I_subst qe_eps⇩1_def set_ebounds set_lbounds)
then obtain leps where "DLO.I φ (leps#xs)"
using I_subst_peps[OF ‹nqfree φ›] by fastforce
hence ?EX .. }
ultimately show ?EX by blast
next
let ?as = "DLO.atoms⇩0 φ" let ?ebs = "ebounds ?as"
assume ?EX
then obtain x where x: "DLO.I φ (x#xs)" ..
{ assume "DLO.I (inf⇩- φ) xs"
hence ?QE using ‹nqfree φ› by(auto simp:qe_eps⇩1_def)
} moreover
{ assume "∃k ∈ set ?ebs. DLO.I (subst φ k) xs"
hence ?QE by(auto simp:qe_eps⇩1_def) } moreover
{ assume "¬ DLO.I (inf⇩- φ) xs"
and "∀k ∈ set ?ebs. ¬ DLO.I (subst φ k) xs"
hence noE: "∀e ∈ EQ φ xs. ¬ DLO.I φ (e#xs)" using ‹nqfree φ›
by (auto simp:set_ebounds EQ_def I_subst nth_Cons' split:if_split_asm)
hence "x ∉ EQ φ xs" using x by fastforce
obtain l where "l ∈ LB φ xs" "l < x"
using LBex[OF ‹nqfree φ› x ‹¬ DLO.I(inf⇩- φ) xs› ‹x ∉ EQ φ xs›] ..
have "∃l∈LB φ xs. l<x ∧ nolb φ xs l x ∧
(∀y. l < y ∧ y ≤ x ⟶ DLO.I φ (y#xs))"
using dense_interval[where P = "λx. DLO.I φ (x#xs)", OF finite_LB ‹l∈LB φ xs› ‹l<x› x] x innermost_intvl[OF ‹nqfree φ› _ _ ‹x ∉ EQ φ xs›]
then obtain m
where *: "Less (Suc m) 0 ∈ set ?as ∧ xs!m < x ∧ nolb φ xs (xs!m) x
∧ (∀y. xs!m < y ∧ y ≤ x ⟶ DLO.I φ (y#xs))"
by blast
then have "DLO.I (subst⇩+ φ m) xs"
using noE by(auto intro!: I_subst_peps2[OF ‹nqfree φ›])
with * have ?QE
by(simp add:qe_eps⇩1_def bex_Un set_lbounds set_ebounds) metis
} ultimately show ?QE by blast
qed

lemma qfree_asubst_peps: "qfree (asubst⇩+ k a)"
by(cases "(k,a)" rule:asubst_peps.cases) simp_all

lemma qfree_subst_peps: "nqfree φ ⟹ qfree (subst⇩+ φ k)"

lemma qfree_qe_eps⇩1: "nqfree φ ⟹ qfree(qe_eps⇩1 φ)"
apply(rule qfree_list_disj)
apply (auto simp:qfree_min_inf qfree_subst_peps qfree_map_fm)
done

definition "qe_eps = DLO.lift_nnf_qe qe_eps⇩1"

lemma qfree_qe_eps: "qfree(qe_eps φ)"

lemma I_qe_eps: "DLO.I (qe_eps φ) xs = DLO.I φ xs"

end


# Theory LinArith

(*  Author:     Tobias Nipkow, 2007  *)

section‹Linear real arithmetic›

theory LinArith
imports QE "HOL-Library.ListVector" Complex_Main
begin

declare iprod_assoc[simp]

subsection‹Basics›

subsubsection‹Syntax and Semantics›

datatype atom = Less real "real list" | Eq real "real list"

fun is_Less :: "atom ⇒ bool" where
"is_Less (Less r rs) = True" |
"is_Less f = False"

abbreviation "is_Eq ≡ Not ∘ is_Less"

lemma is_Less_iff: "is_Less f = (∃r rs. f = Less r rs)"
by(induct f) auto

lemma is_Eq_iff: "(∀i j. a ≠ Less i j) = (∃i j. a = Eq i j)"
by(cases a) auto

fun neg⇩R :: "atom ⇒ atom fm" where
"neg⇩R (Less r t) = Or (Atom(Less (-r) (-t))) (Atom(Eq r t))" |
"neg⇩R (Eq r t) = Or (Atom(Less r t)) (Atom(Less (-r) (-t)))"

fun hd_coeff :: "atom ⇒ real" where
"hd_coeff (Less r cs) = (case cs of [] ⇒ 0 | c#_ ⇒ c)" |
"hd_coeff (Eq r cs) = (case cs of [] ⇒ 0 | c#_ ⇒ c)"

definition "depends⇩R a = (hd_coeff a ≠ 0)"

fun decr⇩R :: "atom ⇒ atom" where
"decr⇩R (Less r rs) = Less r (tl rs)" |
"decr⇩R (Eq r rs) = Eq r (tl rs)"

fun I⇩R :: "atom ⇒ real list ⇒ bool" where
"I⇩R (Less r cs) xs = (r < ⟨cs,xs⟩)" |
"I⇩R (Eq r cs) xs = (r = ⟨cs,xs⟩)"

definition "atoms⇩0 = ATOM.atoms⇩0 depends⇩R"
(* FIXME !!! (incl: display should hide params)*)

interpretation R: ATOM neg⇩R "(λa. True)" I⇩R depends⇩R decr⇩R
rewrites "ATOM.atoms⇩0 depends⇩R = atoms⇩0"
proof goal_cases
case 1
thus ?case
apply(unfold_locales)
apply(case_tac a)
apply simp_all
apply(case_tac a)
apply simp_all
apply arith
apply arith
apply(case_tac a)
done
next
case 2
qed

setup ‹Sign.revert_abbrev "" @{const_abbrev R.I}›
setup ‹Sign.revert_abbrev "" @{const_abbrev R.lift_nnf_qe}›

subsubsection‹Shared constructions›

fun combine :: "(real * real list) ⇒ (real * real list) ⇒ atom" where
"combine (r⇩1,cs⇩1) (r⇩2,cs⇩2) = Less (r⇩1-r⇩2) (cs⇩2 - cs⇩1)"

(* More efficient combination than rhs of combine_conv below; unused
lemma combine_code:
"combine (r1,c1,cs1) (r2,c2,cs2) =
Less (c1*r2-c2*r1) (zipwith0 (%x y. c1*y-c2*x) cs1 cs2)"
apply(rule sym)
apply(simp)
apply(induct cs1 arbitrary:cs2)
apply simp
apply(case_tac cs2)
apply simp
apply simp
done*)

definition "lbounds as = [(r/c, (-1/c) *⇩s cs). Less r (c#cs) ← as, c>0]"
definition "ubounds as = [(r/c, (-1/c) *⇩s cs). Less r (c#cs) ← as, c<0]"
definition "ebounds as = [(r/c, (-1/c) *⇩s cs). Eq r (c#cs) ← as, c≠0]"

lemma set_lbounds:
"set(lbounds as) = {(r/c, (-1/c) *⇩s cs)|r c cs. Less r (c#cs) ∈ set as ∧ c>0}"
by(force simp: lbounds_def split:list.splits atom.splits if_splits)
lemma set_ubounds:
"set(ubounds as) = {(r/c, (-1/c) *⇩s cs)|r c cs. Less r (c#cs) ∈ set as ∧ c<0}"
by(force simp: ubounds_def split:list.splits atom.splits if_splits)
lemma set_ebounds:
"set(ebounds as) = {(r/c, (-1/c) *⇩s cs)|r c cs. Eq r (c#cs) ∈ set as ∧ c≠0}"
by(force simp: ebounds_def split:list.splits atom.splits if_splits)

abbreviation EQ where
"EQ f xs ≡ {(r - ⟨cs,xs⟩)/c|r c cs. Eq r (c#cs) ∈ set(R.atoms⇩0 f) ∧ c≠0}"
abbreviation LB where
"LB f xs ≡ {(r - ⟨cs,xs⟩)/c|r c cs. Less r (c#cs) ∈ set(R.atoms⇩0 f) ∧ c>0}"
abbreviation UB where
"UB f xs ≡ {(r - ⟨cs,xs⟩)/c|r c cs. Less r (c#cs) ∈ set(R.atoms⇩0 f) ∧ c<0}"

fun asubst :: "real * real list ⇒ atom ⇒ atom" where
"asubst (r,cs) (Less s (d#ds)) = Less (s - d*r) (d *⇩s cs + ds)" |
"asubst (r,cs) (Eq s (d#ds)) = Eq (s - d*r) (d *⇩s cs + ds)" |
"asubst (r,cs) (Less s []) = Less s []" |
"asubst (r,cs) (Eq s []) = Eq s []"

abbreviation "subst φ rcs ≡ map⇩f⇩m (asubst rcs) φ"

definition eval :: "real * real list ⇒ real list ⇒ real" where
"eval rcs xs = fst rcs + ⟨snd rcs,xs⟩"

lemma I_asubst:
"I⇩R (asubst t a) xs = I⇩R a (eval t xs # xs)"
proof(cases a)
case (Less r cs)
thus ?thesis by(cases t, cases cs,
arith
next
case (Eq r cs)
thus ?thesis
arith
qed

lemma I_subst:
"qfree φ ⟹ R.I (subst φ t) xs = R.I φ (eval t xs # xs)"
lemma I_subst_pretty:
"qfree φ ⟹ R.I (subst φ (r,cs)) xs = R.I φ ((r + ⟨cs,xs⟩) # xs)"

fun min_inf :: "atom fm ⇒ atom fm" ("inf⇩-") where
"inf⇩- (And φ⇩1 φ⇩2) = and (inf⇩- φ⇩1) (inf⇩- φ⇩2)" |
"inf⇩- (Or φ⇩1 φ⇩2) = or (inf⇩- φ⇩1) (inf⇩- φ⇩2)" |
"inf⇩- (Atom(Less r (c#cs))) =
(if c<0 then TrueF else if c>0 then FalseF else Atom(Less r cs))" |
"inf⇩- (Atom(Eq r (c#cs))) = (if c=0 then Atom(Eq r cs) else FalseF)" |
"inf⇩- φ = φ"

fun plus_inf :: "atom fm ⇒ atom fm" ("inf⇩+") where
"inf⇩+ (And φ⇩1 φ⇩2) = and (inf⇩+ φ⇩1) (inf⇩+ φ⇩2)" |
"inf⇩+ (Or φ⇩1 φ⇩2) = or (inf⇩+ φ⇩1) (inf⇩+ φ⇩2)" |
"inf⇩+ (Atom(Less r (c#cs))) =
(if c>0 then TrueF else if c<0 then FalseF else Atom(Less r cs))" |
"inf⇩+ (Atom(Eq r (c#cs))) = (if c=0 then Atom(Eq r cs) else FalseF)" |
"inf⇩+ φ = φ"

lemma qfree_min_inf: "qfree φ ⟹ qfree(inf⇩- φ)"
by(induct φ rule:min_inf.induct) simp_all

lemma qfree_plus_inf: "qfree φ ⟹ qfree(inf⇩+ φ)"
by(induct φ rule:plus_inf.induct) simp_all

lemma min_inf:
"nqfree f ⟹ ∃x. ∀y≤x. R.I (inf⇩- f) xs = R.I f (y # xs)"
(is "_ ⟹ ∃x. ?P f x")
proof(induct f)
case (Atom a)
show ?case
proof (cases a)
case (Less r cs)
show ?thesis
proof(cases cs)
case Nil thus ?thesis using Less by simp
next
case (Cons c cs)
{ assume "c=0" hence ?thesis using Less Cons by simp }
moreover
{ assume "c<0"
hence "?P (Atom a) ((r - ⟨cs,xs⟩ + 1)/c)" using Less Cons
hence ?thesis .. }
moreover
{ assume "c>0"
hence "?P (Atom a) ((r - ⟨cs,xs⟩ - 1)/c)" using Less Cons
hence ?thesis .. }
ultimately show ?thesis by force
qed
next
case (Eq r cs)
show ?thesis
proof(cases cs)
case Nil thus ?thesis using Eq by simp
next
case (Cons c cs)
{ assume "c=0" hence ?thesis using Eq Cons by simp }
moreover
{ assume "c<0"
hence "?P (Atom a) ((r - ⟨cs,xs⟩ + 1)/c)" using Eq Cons
hence ?thesis .. }
moreover
{ assume "c>0"
hence "?P (Atom a) ((r - ⟨cs,xs⟩ - 1)/c)" using Eq Cons
hence ?thesis .. }
ultimately show ?thesis by force
qed
qed
next
case (And f1 f2)
then obtain x1 x2 where "?P f1 x1" "?P f2 x2" by fastforce+
hence "?P (And f1 f2) (min x1 x2)" by(force simp:and_def)
thus ?case ..
next
case (Or f1 f2)
then obtain x1 x2 where "?P f1 x1" "?P f2 x2" by fastforce+
hence "?P (Or f1 f2) (min x1 x2)" by(force simp:or_def)
thus ?case ..
qed simp_all

lemma plus_inf:
"nqfree f ⟹ ∃x. ∀y≥x. R.I (inf⇩+ f) xs = R.I f (y # xs)"
(is "_ ⟹ ∃x. ?P f x")
proof(induct f)
case (Atom a)
show ?case
proof (cases a)
case (Less r cs)
show ?thesis
proof(cases cs)
case Nil thus ?thesis using Less by simp
next
case (Cons c cs)
{ assume "c=0" hence ?thesis using Less Cons by simp }
moreover
{ assume "c<0"
hence "?P (Atom a) ((r - ⟨cs,xs⟩ - 1)/c)" using Less Cons
hence ?thesis .. }
moreover
{ assume "c>0"
hence "?P (Atom a) ((r - ⟨cs,xs⟩ + 1)/c)" using Less Cons
hence ?thesis .. }
ultimately show ?thesis by force
qed
next
case (Eq r cs)
show ?thesis
proof(cases cs)
case Nil thus ?thesis using Eq by simp
next
case (Cons c cs)
{ assume "c=0" hence ?thesis using Eq Cons by simp }
moreover
{ assume "c<0"
hence "?P (Atom a) ((r - ⟨cs,xs⟩ - 1)/c)" using Eq Cons
hence ?thesis .. }
moreover
{ assume "c>0"
hence "?P (Atom a) ((r - ⟨cs,xs⟩ + 1)/c)" using Eq Cons
hence ?thesis .. }
ultimately show ?thesis by force
qed
qed
next
case (And f1 f2)
then obtain x1 x2 where "?P f1 x1" "?P f2 x2" by fastforce+
hence "?P (And f1 f2) (max x1 x2)" by(force simp:and_def)
thus ?case ..
next
case (Or f1 f2)
then obtain x1 x2 where "?P f1 x1" "?P f2 x2" by fastforce+
hence "?P (Or f1 f2) (max x1 x2)" by(force simp:or_def)
thus ?case ..
qed simp_all

context notes [[simp_depth_limit = 4]]
begin

lemma LBex:
"⟦ nqfree f; R.I f (x#xs); ¬R.I (inf⇩- f) xs; x ∉ EQ f xs ⟧
⟹ ∃l∈ LB f xs. l < x"
apply(induct f)
apply simp
apply simp
apply(rename_tac a)
apply(case_tac a)
apply(auto simp add: depends⇩R_def field_simps split:if_splits list.splits)
apply fastforce+
done

lemma UBex:
"⟦ nqfree f; R.I f (x#xs); ¬R.I (inf⇩+ f) xs; x ∉ EQ f xs ⟧
⟹ ∃u∈ UB f xs. x < u"
apply(induct f)
apply simp
apply simp
apply(rename_tac a)
apply(case_tac a)
apply(auto simp add: depends⇩R_def field_simps split:if_splits list.splits)
apply fastforce+
done

end

lemma finite_LB: "finite(LB f xs)"
proof -
have "LB f xs = (λ(r,cs). r + ⟨cs,xs⟩)  set(lbounds(R.atoms⇩0 f))"
by (force simp:set_lbounds image_def field_simps)
thus ?thesis by simp
qed

lemma finite_UB: "finite(UB f xs)"
proof -
have "UB f xs = (λ(r,cs). r + ⟨cs,xs⟩)  set(ubounds(R.atoms⇩0 f))"
by (force simp:set_ubounds image_def field_simps)
thus ?thesis by simp
qed

end


# Theory QElin

(*  Author:     Tobias Nipkow, 2007  *)

theory QElin
imports LinArith
begin

subsection‹Fourier›

definition qe_FM⇩1 :: "atom list ⇒ atom fm" where
"qe_FM⇩1 as = list_conj [Atom(combine p q). p←lbounds as, q←ubounds as]"

theorem I_qe_FM⇩1:
assumes less: "∀a ∈ set as. is_Less a" and dep: "∀a ∈ set as. depends⇩R a"
shows "R.I (qe_FM⇩1 as) xs = (∃x. ∀a ∈ set as. I⇩R a (x#xs))"  (is "?L = ?R")
proof
let ?Ls = "set(lbounds as)" let ?Us = "set(ubounds as)"
let ?lbs = "UN (r,cs):?Ls. {r + ⟨cs,xs⟩}"
let ?ubs = "UN (r,cs):?Us. {r + ⟨cs,xs⟩}"
have fins: "finite ?lbs ∧ finite ?ubs" by auto
have 2: "∀f∈ set as. ∃r c cs. f = Less r (c#cs) ∧
(c>0 ∧ (r/c,(-1/c)*⇩s cs) ∈ ?Ls ∨ c<0 ∧ (r/c,(-1/c)*⇩s cs) ∈ ?Us)"
using dep less
by(fastforce simp:set_lbounds set_ubounds is_Less_iff depends⇩R_def
split:list.splits)
assume ?L
have 1: "∀x∈?lbs. ∀y∈?ubs. x < y"
proof (rule ballI)+
fix x y assume "x∈?lbs" "y∈?ubs"
then obtain r cs
where "(r,cs) ∈ ?Ls ∧ x = r + ⟨cs,xs⟩" by fastforce
moreover from ‹y∈?ubs› obtain s ds
where "(s,ds) ∈ ?Us ∧ y = s + ⟨ds,xs⟩" by fastforce
ultimately show "x<y" using ‹?L›
by(fastforce simp:qe_FM⇩1_def algebra_simps iprod_left_diff_distrib)
qed
{ assume nonempty: "?lbs ≠ {} ∧ ?ubs ≠ {}"
hence "Max ?lbs < Min ?ubs" using fins 1
by(blast intro: Max_less_iff[THEN iffD2] Min_gr_iff[THEN iffD2])
then obtain m where "Max ?lbs < m ∧ m < Min ?ubs"
using dense[where 'a = real] by blast
hence "∀a ∈ set as. I⇩R a (m#xs)" using 2 nonempty
apply (auto simp: Ball_def)
apply (auto simp: Bex_def)
apply (fastforce simp: field_simps)
done
hence ?R .. }
moreover
{ assume asm: "?lbs ≠ {} ∧ ?ubs = {}"
have "∀a ∈ set as. I⇩R a ((Max ?lbs + 1) # xs)"
proof
fix a assume "a ∈ set as"
then obtain r c cs
where "a = Less r (c#cs)" "c>0" "(r/c,(-1/c)*⇩s cs) ∈ ?Ls"
using asm 2
by (fastforce simp: field_simps)
moreover hence "(r - ⟨cs,xs⟩)/c ≤ Max ?lbs"
using asm fins
by(auto intro!: Max_ge_iff[THEN iffD2])
ultimately show "I⇩R a ((Max ?lbs + 1) # xs)" by (simp add: field_simps)
qed
hence ?R .. }
moreover
{ assume asm: "?lbs = {} ∧ ?ubs ≠ {}"
have "∀a ∈ set as. I⇩R a ((Min ?ubs - 1) # xs)"
proof
fix a assume "a ∈ set as"
then obtain r c cs
where "a = Less r (c#cs)" "c<0" "(r/c,(-1/c)*⇩s cs) ∈ ?Us"
using asm 2 by fastforce
moreover hence "Min ?ubs ≤ (r - ⟨cs,xs⟩)/c"
using asm fins
by(auto intro!: Min_le_iff[THEN iffD2])
ultimately show "I⇩R a ((Min ?ubs - 1) # xs)" by (simp add: field_simps)
qed
hence ?R .. }
moreover
{ assume "?lbs = {} ∧ ?ubs = {}"
hence ?R using 2 less by auto (rule, fast)
}
ultimately show ?R by blast
next
let ?Ls = "set(lbounds as)" let ?Us = "set(ubounds as)"
assume ?R
then obtain x where 1: "∀a∈ set as. I⇩R a (x#xs)" ..
{ fix r c cs s d ds
assume "Less r (c#cs) ∈ set as" "0 < c" "Less s (d#ds) ∈ set as" "d < 0"
hence "r < c*x + ⟨cs,xs⟩" "s < d*x + ⟨ds,xs⟩" "c > 0" "d < 0"
using 1 by auto
hence "(r - ⟨cs,xs⟩)/c < x" "x < (s - ⟨ds,xs⟩)/d" by(simp add:field_simps)+
hence "(r - ⟨cs,xs⟩)/c < (s - ⟨ds,xs⟩)/d" by arith
}
thus ?L by (auto simp: qe_FM⇩1_def iprod_left_diff_distrib less field_simps set_lbounds set_ubounds)
qed

corollary I_qe_FM⇩1_pretty:
"∀a ∈ set as. is_Less a ∧ depends⇩R a ⟹ R.is_dnf_qe qe_FM⇩1 as"
by(metis I_qe_FM⇩1)

fun subst⇩0 :: "atom ⇒ atom ⇒ atom" where
"subst⇩0 (Eq r (c#cs)) a = (case a of
Less s (d#ds) ⇒ Less (s - (r*d)/c) (ds - (d/c) *⇩s cs)
| Eq s (d#ds) ⇒ Eq (s - (r*d)/c) (ds - (d/c) *⇩s cs))"

lemma subst⇩0_pretty:
"subst⇩0 (Eq r (c#cs)) (Less s (d#ds)) = Less (s - (r*d)/c) (ds - (d/c) *⇩s cs)"
"subst⇩0 (Eq r (c#cs)) (Eq s (d#ds)) = Eq (s - (r*d)/c) (ds - (d/c) *⇩s cs)"
by auto

lemma I_subst⇩0: "depends⇩R a ⟹ c ≠ 0 ⟹
I⇩R (subst⇩0 (Eq r (c#cs)) a) xs = I⇩R a ((r - ⟨cs,xs⟩)/c # xs)"
apply(cases a)
by (auto simp add: depends⇩R_def iprod_left_diff_distrib algebra_simps diff_divide_distrib split:list.splits)

interpretation R⇩e:
ATOM_EQ neg⇩R "(λa. True)" I⇩R depends⇩R decr⇩R
"(λEq _ (c#_) ⇒ c ≠ 0 | _ ⇒ False)"
"(λEq r cs ⇒ r=0 ∧ (∀c∈ set cs. c=0) | _ ⇒ False)" subst⇩0
apply(unfold_locales)
apply(simp split:atom.splits list.splits)
apply(rename_tac r ds c cs)
apply(rule_tac x= "(r - ⟨cs,xs⟩)/c" in exI)
split:atom.splits list.splits)
done

(* FIXME does not help
setup {* Sign.revert_abbrev "" @{const_name R⇩e.lift_dnfeq_qe} *}
*)

definition "qe_FM = R⇩e.lift_dnfeq_qe qe_FM⇩1"

lemma qfree_qe_FM⇩1: "qfree (qe_FM⇩1 as)"
by(auto simp:qe_FM⇩1_def intro!:qfree_list_conj)

corollary I_qe_FM: "R.I (qe_FM φ) xs = R.I φ xs"
unfolding qe_FM_def
apply(rule R⇩e.I_lift_dnfeq_qe)
apply(rule qfree_qe_FM⇩1)
apply(rule allI)
apply(rule I_qe_FM⇩1)
prefer 2 apply blast
apply(clarify)
apply(drule_tac x=a in bspec) apply simp
done

theorem qfree_qe_FM: "qfree (qe_FM f)"

subsubsection‹Tests›

lemmas qesimps = qe_FM_def R⇩e.lift_dnfeq_qe_def R⇩e.lift_eq_qe_def R.qelim_def qe_FM⇩1_def lbounds_def ubounds_def list_conj_def list_disj_def and_def or_def depends⇩R_def

lemma "qe_FM(TrueF) = TrueF"

lemma
"qe_FM(ExQ (And (Atom(Less 0 [1])) (Atom(Less 0 [-1])))) = Atom(Less 0 [])"

lemma
"qe_FM(ExQ (And (Atom(Less 0 [1])) (Atom(Less (- 1) [-1])))) = Atom(Less (- 1) [])"

end


# Theory QElin_opt

(*  Author:     Tobias Nipkow, 2007  *)

theory QElin_opt
imports QElin
begin

subsubsection‹An optimization›

text‹Atoms are simplified asap.›

definition
"asimp a = (case a of
Less r cs ⇒ (if ∀c∈ set cs. c = 0
then if r<0 then TrueF else FalseF
else Atom a) |
Eq r cs ⇒ (if ∀c∈ set cs. c = 0
then if r=0 then TrueF else FalseF else Atom a))"

lemma asimp_pretty:
"asimp (Less r cs) =
(if ∀c∈ set cs. c = 0
then if r<0 then TrueF else FalseF
else Atom(Less r cs))"
"asimp (Eq r cs) =
(if ∀c∈ set cs. c = 0
then if r=0 then TrueF else FalseF
else Atom(Eq r cs))"
by(auto simp:asimp_def)

definition qe_FMo⇩1 :: "atom list ⇒ atom fm" where
"qe_FMo⇩1 as = list_conj [asimp(combine p q). p←lbounds as, q←ubounds as]"

lemma I_asimp: "R.I (asimp a) xs = I⇩R a xs"

lemma I_qe_FMo⇩1: "R.I (qe_FMo⇩1 as) xs = R.I (qe_FM⇩1 as) xs"

definition "qe_FMo = R⇩e.lift_dnfeq_qe qe_FMo⇩1"

lemma qfree_qe_FMo⇩1: "qfree (qe_FMo⇩1 as)"
by(auto simp:qe_FM⇩1_def qe_FMo⇩1_def asimp_def intro!:qfree_list_conj
split:atom.split)

corollary I_qe_FMo: "R.I (qe_FMo φ) xs = R.I φ xs"
unfolding qe_FMo_def
apply(rule R⇩e.I_lift_dnfeq_qe)
apply(rule qfree_qe_FMo⇩1)
apply(rule allI)
apply(subst I_qe_FMo⇩1)
apply(rule I_qe_FM⇩1)
prefer 2 apply blast
apply(clarify)
apply(drule_tac x=a in bspec) apply simp
done

theorem qfree_qe_FMo: "qfree (qe_FMo f)"

end


# Theory FRE

(*  Author:     Tobias Nipkow, 2007  *)

theory FRE
imports LinArith
begin

subsection‹Ferrante-Rackoff \label{sec:FRE}›

text‹This section formalizes a slight variant of Ferrante and
Rackoff's algorithm~\cite{FerranteR-SIAM75}. We consider equalities
separately, which improves performance.›

fun between :: "real * real list ⇒ real * real list ⇒ real * real list"
where "between (r,cs) (s,ds) = ((r+s)/2, (1/2) *⇩s (cs+ds))"

definition FR⇩1 :: "atom fm ⇒ atom fm" where
"FR⇩1 φ =
(let as = R.atoms⇩0 φ; lbs = lbounds as; ubs = ubounds as; ebs = ebounds as;
intrs = [subst φ (between l u) . l ← lbs, u ← ubs]
in list_disj (inf⇩- φ # inf⇩+ φ # intrs @ map (subst φ) ebs))"

lemma dense_interval:
assumes "finite L" "finite U" "l ∈ L" "u ∈ U" "l < x" "x < u" "P(x::real)"
and dense: "⋀y l u. ⟦ ∀y∈{l<..<x}. y ∉ L;  ∀y∈{x<..<u}. y ∉ U;
l<x;x<u; l<y;y<u ⟧ ⟹ P y"
shows "∃l∈L.∃u∈U. l<u ∧ (∀y. l<y ∧ y<u ⟶ P y)"
proof -
let ?L = "{l:L. l < x}" let ?U = "{u:U. x < u}"
let ?ll = "Max ?L" let ?uu = "Min ?U"
have "?L ≠ {}" using ‹l ∈ L› ‹l<x› by (blast intro:order_less_imp_le)
moreover have "?U ≠ {}" using ‹u:U› ‹x<u› by (blast intro:order_less_imp_le)
ultimately have "∀y. ?ll<y ∧ y<x ⟶ y ∉ L" "∀y. x<y ∧ y<?uu ⟶ y ∉ U"
using ‹finite L› ‹finite U› by force+
moreover have "?ll ∈ L"
proof
show "?ll ∈ ?L" using ‹finite L› Max_in[OF _ ‹?L ≠ {}›] by simp
show "?L ⊆ L" by blast
qed
moreover have "?uu ∈ U"
proof
show "?uu ∈ ?U" using ‹finite U› Min_in[OF _ ‹?U ≠ {}›] by simp
show "?U ⊆ U" by blast
qed
moreover have "?ll < x" using ‹finite L› ‹?L ≠ {}› by simp
moreover have "x < ?uu" using ‹finite U› ‹?U ≠ {}› by simp
moreover have "?ll < ?uu" using ‹?ll<x› ‹x<?uu› by arith
ultimately show ?thesis using ‹l < x› ‹x < u› ‹?L ≠ {}› ‹?U ≠ {}›
by(blast intro!:dense greaterThanLessThan_iff[THEN iffD1])
qed

lemma dense:
"⟦ nqfree f; ∀y∈{l<..<x}. y ∉ LB f xs; ∀y∈{x<..<u}. y ∉ UB f xs;
l < x; x < u; x ∉ EQ f xs;  R.I f (x#xs); l < y; y < u⟧
⟹ R.I f (y#xs)"
proof(induct f)
case (Atom a)
show ?case
proof (cases a)
case (Less r cs)
show ?thesis
proof (cases cs)
case Nil thus ?thesis using Atom Less by (simp add:depends⇩R_def)
next
case (Cons c cs)
hence "r < c*x + ⟨cs,xs⟩" using Atom Less by simp
{ assume "c=0" hence ?thesis using Atom Less Cons by simp }
moreover
{ assume "c<0"
hence "x < (r - ⟨cs,xs⟩)/c" (is "_ < ?u") using ‹r < c*x + ⟨cs,xs⟩›
have ?thesis
proof (rule ccontr)
assume "¬ R.I (Atom a) (y#xs)"
hence "?u ≤ y" using Atom Less Cons ‹c<0›
hence "?u < u" using ‹y<u› by simp
with ‹x<?u› show False using Atom Less Cons ‹c<0›
by(auto simp:depends⇩R_def)
qed } moreover
{ assume "c>0"
hence "x > (r - ⟨cs,xs⟩)/c" (is "_ > ?l") using ‹r < c*x + ⟨cs,xs⟩›
have ?thesis
proof (rule ccontr)
assume "¬ R.I (Atom a) (y#xs)"
hence "?l ≥ y" using Atom Less Cons ‹c>0›
hence "?l > l" using ‹y>l› by simp
with ‹?l<x› show False using Atom Less Cons ‹c>0›
by (auto simp:depends⇩R_def)
qed }
ultimately show ?thesis by force
qed
next
case (Eq r cs)
show ?thesis
proof (cases cs)
case Nil thus ?thesis using Atom Eq by (simp add:depends⇩R_def)
next
case (Cons c cs)
hence "r = c*x + ⟨cs,xs⟩" using Atom Eq by simp
{ assume "c=0" hence ?thesis using Atom Eq Cons by simp }
moreover
{ assume "c≠0"
hence ?thesis using ‹r = c*x + ⟨cs,xs⟩› Atom Eq Cons ‹l<y› ‹y<u›
by (auto simp: depends⇩R_def split: if_splits) }
ultimately show ?thesis by force
qed
qed
next
case (And f1 f2) thus ?case
by auto (metis (no_types, hide_lams))+
next
case (Or f1 f2) thus ?case
by auto (metis (no_types, hide_lams))+
qed fastforce+

theorem I_FR⇩1:
assumes "nqfree φ" shows "R.I (FR⇩1 φ) xs = (∃x. R.I φ (x#xs))"
(is "?FR = ?EX")
proof
assume ?FR
{ assume "R.I (inf⇩- φ) xs"
hence ?EX using ‹?FR› min_inf[OF ‹nqfree φ›, where xs=xs]
} moreover
{ assume "R.I (inf⇩+ φ) xs"
hence ?EX using ‹?FR› plus_inf[OF ‹nqfree φ›, where xs=xs]
} moreover
{ assume "∃x ∈ EQ φ xs. R.I φ (x#xs)"
hence ?EX using ‹?FR› by(auto simp add:FR⇩1_def)
} moreover
{ assume "¬R.I (inf⇩- φ) xs ∧ ¬R.I (inf⇩+ φ) xs ∧
(∀x∈EQ φ xs. ¬R.I φ (x#xs))"
with ‹?FR› obtain r cs s ds
where "R.I (subst φ (between (r,cs) (s,ds))) xs"
by(auto simp: FR⇩1_def eval_def
diff_divide_distrib set_ebounds I_subst ‹nqfree φ›) blast
hence "R.I φ (eval (between (r,cs) (s,ds)) xs # xs)"
hence ?EX .. }
ultimately show ?EX by blast
next
assume ?EX
then obtain x where x: "R.I φ (x#xs)" ..
{ assume "R.I (inf⇩- φ) xs ∨ R.I (inf⇩+ φ) xs"
hence ?FR by(auto simp:FR⇩1_def)
} moreover
{ assume "x ∈ EQ φ xs"
then obtain r cs
where "(r,cs) ∈ set(ebounds(R.atoms⇩0 φ)) ∧ x = r + ⟨cs,xs⟩"
by(force simp:set_ebounds field_simps)
moreover hence "R.I (subst φ (r,cs)) xs" using x
by(auto simp: I_subst ‹nqfree φ› eval_def)
ultimately have ?FR by(force simp:FR⇩1_def) } moreover
{ assume "¬ R.I (inf⇩- φ) xs" and "¬ R.I (inf⇩+ φ) xs" and "x ∉ EQ φ xs"
obtain l where "l ∈ LB φ xs" "l < x"
using LBex[OF ‹nqfree φ› x ‹¬ R.I (inf⇩- φ) xs› ‹x ∉ EQ φ xs›] ..
obtain u where "u ∈ UB φ xs" "x < u"
using UBex[OF ‹nqfree φ› x ‹¬ R.I (inf⇩+ φ) xs› ‹x ∉ EQ φ xs›] ..
have "∃l∈LB φ xs. ∃u∈UB φ xs. l<u ∧ (∀y. l < y ∧ y < u ⟶ R.I φ (y#xs))"
using dense_interval[where P = "λx. R.I φ (x#xs)", OF finite_LB finite_UB ‹l:LB φ xs› ‹u:UB φ xs› ‹l<x› ‹x<u› x] x dense[OF ‹nqfree φ› _ _ _ _ ‹x ∉ EQ φ xs›] by simp
then obtain r c cs s d ds
where "Less r (c # cs) ∈ set (R.atoms⇩0 φ)" "Less s (d # ds) ∈ set (R.atoms⇩0 φ)"
"⋀y. (r - ⟨cs,xs⟩) / c < y ⟹ y < (s - ⟨ds,xs⟩) / d ⟹ R.I φ (y # xs)"
and *: "c > 0" "d < 0" "(r - ⟨cs,xs⟩) / c < (s - ⟨ds,xs⟩) / d"
by blast
moreover
have "(r - ⟨cs,xs⟩) / c < eval (between (r / c, (-1 / c) *⇩s cs) (s / d, (-1 / d) *⇩s ds)) xs" (is ?P)
and "eval (between (r / c, (-1 / c) *⇩s cs) (s / d, (-1 / d) *⇩s ds)) xs < (s - ⟨ds,xs⟩) / d" (is ?Q)
proof -
from * have [simp]: "c * (c * (d * (d * 4))) > 0"
from * have "c * s + d * ⟨cs,xs⟩ < d * r + c * ⟨ds,xs⟩"
with * have "(2 * c * c * d) * (d * r + c * ⟨ds,xs⟩)
< (2 * c * c * d) * (c * s + d * ⟨cs,xs⟩)"
and "(2 * c * d * d) * (c * s + d * ⟨cs,xs⟩)
< (2 * c * d * d) * (d * r + c * ⟨ds,xs⟩)" by simp_all
with * show ?P and ?Q by (auto simp add: field_simps eval_def iprod_left_add_distrib)
qed
ultimately have ?FR
by (fastforce simp: FR⇩1_def bex_Un set_lbounds set_ubounds set_ebounds I_subst ‹nqfree φ›)
} ultimately show ?FR by blast
qed

definition "FR = R.lift_nnf_qe FR⇩1"

lemma qfree_FR⇩1: "nqfree φ ⟹ qfree (FR⇩1 φ)"
apply(rule qfree_list_disj)
apply(auto simp:qfree_min_inf qfree_plus_inf set_ubounds set_lbounds set_ebounds image_def qfree_map_fm)
done

theorem I_FR: "R.I (FR φ) xs = R.I φ xs"

theorem qfree_FR: "qfree (FR φ)"

end


# Theory QElin_inf

(*  Author:     Tobias Nipkow, 2007  *)

theory QElin_inf
imports LinArith
begin

subsection ‹Quantifier elimination with infinitesimals \label{sec:lin-inf}›

text‹This section formalizes Loos and Weispfenning's quantifier
elimination procedure based on (the simulation of)
infinitesimals~\cite{LoosW93}.›

fun asubst_peps :: "real * real list ⇒ atom ⇒ atom fm" ("asubst⇩+") where
"asubst_peps (r,cs) (Less s (d#ds)) =
(if d=0 then Atom(Less s ds) else
let u = s - d*r; v = d *⇩s cs + ds; less = Atom(Less u v)
in if d<0 then less else Or less (Atom(Eq u v)))" |
"asubst_peps rcs (Eq r (d#ds)) = (if d=0 then Atom(Eq r ds) else FalseF)" |
"asubst_peps rcs a = Atom a"

abbreviation subst_peps :: "atom fm ⇒ real * real list ⇒ atom fm" ("subst⇩+")
where "subst⇩+ φ rcs ≡ amap⇩f⇩m (asubst⇩+ rcs) φ"

definition "nolb f xs l x = (∀y∈{l<..<x}. y ∉ LB f xs)"

lemma nolb_And[simp]:
"nolb (And f g) xs l x = (nolb f xs l x ∧ nolb g xs l x)"
apply(clarsimp simp:nolb_def)
apply blast
done

lemma nolb_Or[simp]:
"nolb (Or f g) xs l x = (nolb f xs l x ∧ nolb g xs l x)"
apply(clarsimp simp:nolb_def)
apply blast
done

context notes [[simp_depth_limit=4]]
begin

lemma innermost_intvl:
"⟦ nqfree f; nolb f xs l x; l < x; x ∉ EQ f xs; R.I f (x#xs); l < y; y ≤ x⟧
⟹ R.I f (y#xs)"
proof(induct f)
case (Atom a)
show ?case
proof (cases a)
case [simp]: (Less r cs)
show ?thesis
proof (cases cs)
case Nil thus ?thesis using Atom by (simp add:depends⇩R_def)
next
case [simp]: (Cons c cs)
hence "r < c*x + ⟨cs,xs⟩" using Atom by simp
{ assume "c=0" hence ?thesis using Atom by simp }
moreover
{ assume "c<0"
hence "x < (r - ⟨cs,xs⟩)/c" (is "_ < ?u") using ‹r < c*x + ⟨cs,xs⟩›
have ?thesis
proof (rule ccontr)
assume "¬ R.I (Atom a) (y#xs)"
hence "?u ≤ y" using Atom ‹c<0›
with ‹x<?u› show False using Atom ‹c<0›
by(auto simp:depends⇩R_def)
qed } moreover
{ assume "c>0"
hence "x > (r - ⟨cs,xs⟩)/c" (is "_ > ?l") using ‹r < c*x + ⟨cs,xs⟩›
then have "?l < y" using Atom ‹c>0›
by (auto simp:depends⇩R_def Ball_def nolb_def)
(metis linorder_not_le antisym order_less_trans)
hence ?thesis using ‹c>0› by (simp add: field_simps)
} ultimately show ?thesis by force
qed
next
case [simp]: (Eq r cs)
show ?thesis
proof (cases cs)
case Nil thus ?thesis using Atom by (simp add:depends⇩R_def)
next
case [simp]: (Cons c cs)
hence "r = c*x + ⟨cs,xs⟩" using Atom by simp
{ assume "c=0" hence ?thesis using Atom by simp }
moreover
{ assume "c≠0"
hence ?thesis using ‹r = c*x + ⟨cs,xs⟩› Atom
by (auto simp: depends⇩R_def split: if_splits) }
ultimately show ?thesis by force
qed
qed
next
case (And f1 f2) thus ?case by (fastforce)
next
case (Or f1 f2) thus ?case by (fastforce)
qed simp+

definition "EQ2 = EQ"

lemma EQ2_Or[simp]: "EQ2 (Or f g) xs = (EQ2 f xs ∪ EQ2 g xs)"
by(auto simp:EQ2_def)

lemma EQ2_And[simp]: "EQ2 (And f g) xs = (EQ2 f xs ∪ EQ2 g xs)"
by(auto simp:EQ2_def)

lemma innermost_intvl2:
"⟦ nqfree f; nolb f xs l x; l < x; x ∉ EQ2 f xs; R.I f (x#xs); l < y; y ≤ x⟧
⟹ R.I f (y#xs)"
unfolding EQ2_def by(blast intro:innermost_intvl)

lemma I_subst_peps2:
"nqfree f ⟹ r+⟨cs,xs⟩ < x ⟹ nolb f xs (r+⟨cs,xs⟩) x
⟹ ∀y ∈ {r+⟨cs,xs⟩ <.. x}. R.I f (y#xs) ∧ y ∉ EQ2 f xs
⟹ R.I (subst⇩+ f (r,cs)) xs"
proof(induct f)
case FalseF thus ?case
by simp (metis antisym_conv1 linorder_neq_iff)
next
case (Atom a)
show ?case
proof(cases "((r,cs),a)" rule:asubst_peps.cases)
case (1 r cs s d ds)
{ assume "d=0" hence ?thesis using Atom 1 by auto }
moreover
{ assume "d<0"
have "s < d*x + ⟨ds,xs⟩" using Atom 1 by simp
moreover have "d*x < d*(r + ⟨cs,xs⟩)" using ‹d<0› Atom 1
ultimately have "s < d * (r + ⟨cs,xs⟩) + ⟨ds,xs⟩" by(simp add:algebra_simps)
hence ?thesis using 1
} moreover
{ let ?L = "(s - ⟨ds,xs⟩) / d" let ?U = "r + ⟨cs,xs⟩"
assume "d>0"
hence "?U < x" and "∀y. ?U < y ∧ y < x ⟶ y ≠ ?L"
and "∀y. ?U < y ∧ y ≤ x ⟶ ?L < y" using Atom 1
hence "?L < ?U ∨ ?L = ?U"
by (metis linorder_neqE_linordered_idom order_refl)
hence ?thesis using Atom 1 ‹d>0›
} ultimately show ?thesis by force
next
case 2 thus ?thesis using Atom
by (fastforce simp: nolb_def EQ2_def depends⇩R_def field_simps split: if_split_asm)
qed (insert Atom, auto)
next
case Or thus ?case by(simp add:Ball_def)(metis order_refl innermost_intvl2)
qed simp_all

end

lemma I_subst_peps:
"nqfree f ⟹ R.I (subst⇩+ f (r,cs)) xs ⟹
(∃leps>r+⟨cs,xs⟩. ∀x. r+⟨cs,xs⟩ < x ∧ x ≤ leps ⟶ R.I f (x#xs))"
proof(induct f)
case TrueF thus ?case by simp (metis less_add_one)
next
case (Atom a)
show ?case
proof (cases "((r,cs),a)" rule: asubst_peps.cases)
case (1 r cs s d ds)
{ assume "d=0" hence ?thesis using Atom 1 by auto (metis less_add_one) }
moreover
{ assume "d<0"
with Atom 1 have "r + ⟨cs,xs⟩ < (s - ⟨ds,xs⟩)/d" (is "?a < ?b")
then obtain x where "?a < x" "x < ?b" by(metis dense)
hence " ∀y. ?a < y ∧ y ≤ x ⟶ s < d*y + ⟨ds,xs⟩"
(metis add_le_cancel_right mult_le_cancel_left order_antisym linear mult.commute xt1(8))
hence ?thesis using 1 ‹?a<x› by auto
} moreover
{ let ?a = "s - d * r" let ?b = "⟨d *⇩s cs + ds,xs⟩"
assume "d>0"
with Atom 1 have "?a < ?b ∨ ?a = ?b" by auto
hence ?thesis
proof
assume "?a = ?b"
thus ?thesis using ‹d>0› Atom 1
next
assume "?a < ?b"
{ fix x assume "r+⟨cs,xs⟩ < x ∧ x ≤ r+⟨cs,xs⟩ + 1"
hence "d*(r + ⟨cs,xs⟩) < d*x"
using ‹d>0› by(metis mult_strict_left_mono)
hence "s < d*x + ⟨ds,xs⟩" using ‹d>0› ‹?a < ?b›
}
thus ?thesis using 1 ‹d>0›
qed
} ultimately show ?thesis by (metis less_linear)
qed (insert Atom, auto split:if_split_asm intro: less_add_one)
next
case And thus ?case
apply clarsimp
apply(rule_tac x="min leps lepsa" in exI)
apply simp
done
next
case Or thus ?case by force
qed simp_all

lemma dense_interval:
assumes "finite L" "l ∈ L" "l < x" "P(x::real)"
and dense: "⋀y l. ⟦ ∀y∈{l<..<x}. y ∉ L; l<x; l<y; y≤x ⟧ ⟹ P y"
shows "∃l∈L. l<x ∧ (∀y∈{l<..<x}. y ∉ L) ∧ (∀y. l<y ∧ y≤x ⟶ P y)"
proof -
let ?L = "{l∈L. l < x}"
let ?ll = "Max ?L"
have "?L ≠ {}" using ‹l ∈ L› ‹l<x› by (blast intro:order_less_imp_le)
hence "∀y. ?ll<y ∧ y<x ⟶ y ∉ L" using ‹finite L› by force
moreover have "?ll ∈ L"
proof
show "?ll ∈ ?L" using ‹finite L› Max_in[OF _ ‹?L ≠ {}›] by simp
show "?L ⊆ L" by blast
qed
moreover have "?ll < x" using ‹finite L› ‹?L ≠ {}› by simp
ultimately show ?thesis using ‹l < x› ‹?L ≠ {}›
by(blast intro!:dense greaterThanLessThan_iff[THEN iffD1])
qed

definition
"qe_eps⇩1(f) =
(let as = R.atoms⇩0 f; lbs = lbounds as; ebs = ebounds as
in list_disj (inf⇩- f # map (subst⇩+ f) lbs @ map (subst f) ebs))"

theorem I_eps1:
assumes "nqfree f" shows "R.I (qe_eps⇩1 f) xs = (∃x. R.I f (x#xs))"
(is "?QE = ?EX")
proof
let ?as = "R.atoms⇩0 f" let ?ebs = "ebounds ?as"
assume ?QE
{ assume "R.I (inf⇩- f) xs"
hence ?EX using ‹?QE› min_inf[of f xs] ‹nqfree f›
} moreover
{ assume "∀x ∈ EQ f xs. ¬R.I f (x#xs)"
"¬ R.I (inf⇩- f) xs"
with ‹?QE› ‹nqfree f› obtain r cs where "R.I (subst⇩+ f (r,cs)) xs"
by (fastforce simp: qe_eps⇩1_def set_ebounds diff_divide_distrib eval_def I_subst ‹nqfree f›)
then obtain leps where "R.I f (leps#xs)"
using I_subst_peps[OF ‹nqfree f›] by fastforce
hence ?EX .. }
ultimately show ?EX by blast
next
let ?as = "R.atoms⇩0 f" let ?ebs = "ebounds ?as"
assume ?EX
then obtain x where x: "R.I f (x#xs)" ..
{ assume "R.I (inf⇩- f) xs"
hence ?QE using ‹nqfree f› by(auto simp:qe_eps⇩1_def)
} moreover
{ assume "∃rcs ∈ set ?ebs. R.I (subst f rcs) xs"
hence ?QE by(auto simp:qe_eps⇩1_def) } moreover
{ assume "¬ R.I (inf⇩- f) xs"
and "∀rcs ∈ set ?ebs. ¬ R.I (subst f rcs) xs"
hence noE: "∀e ∈ EQ f xs. ¬ R.I f (e#xs)" using ‹nqfree f›
by (force simp:set_ebounds I_subst diff_divide_distrib eval_def split:if_split_asm)
hence "x ∉ EQ f xs" using x by fastforce
obtain l where "l ∈ LB f xs" "l < x"
using LBex[OF ‹nqfree f› x ‹¬ R.I(inf⇩- f) xs› ‹x ∉ EQ f xs›] ..
have "∃l∈LB f xs. l<x ∧ nolb f xs l x ∧
(∀y. l < y ∧ y ≤ x ⟶ R.I f (y#xs))"
using dense_interval[where P = "λx. R.I f (x#xs)", OF finite_LB ‹l∈LB f xs› ‹l<x› x] x innermost_intvl[OF ‹nqfree f› _ _ ‹x ∉ EQ f xs›]
then obtain r c cs
where *: "Less r (c#cs) ∈ set(R.atoms⇩0 f) ∧ c>0 ∧
(r - ⟨cs,xs⟩)/c < x ∧ nolb f xs ((r - ⟨cs,xs⟩)/c) x
∧ (∀y. (r - ⟨cs,xs⟩)/c < y ∧ y ≤ x ⟶ R.I f (y#xs))"
by blast
then have "R.I (subst⇩+ f (r/c, (-1/c) *⇩s cs)) xs" using noE
by(auto intro!: I_subst_peps2[OF ‹nqfree f›]
simp:EQ2_def diff_divide_distrib algebra_simps)
with * have ?QE
} ultimately show ?QE by blast
qed

lemma qfree_asubst_peps: "qfree (asubst⇩+ rcs a)"
by(cases "(rcs,a)" rule:asubst_peps.cases) simp_all

lemma qfree_subst_peps: "nqfree φ ⟹ qfree (subst⇩+ φ rcs)"

lemma qfree_qe_eps⇩1: "nqfree φ ⟹ qfree(qe_eps⇩1 φ)"
apply(rule qfree_list_disj)
apply (auto simp:qfree_min_inf qfree_subst_peps qfree_map_fm)
done

definition "qe_eps = R.lift_nnf_qe qe_eps⇩1"

lemma qfree_qe_eps: "qfree(qe_eps φ)"

lemma I_qe_eps: "R.I (qe_eps φ) xs = R.I φ xs"

end


# Theory PresArith

(*  Author:     Tobias Nipkow, 2007  *)

section‹Presburger arithmetic›

theory PresArith
imports QE "HOL-Library.ListVector"
begin

declare iprod_assoc[simp]

subsection‹Syntax›

datatype atom =
Le int "int list" | Dvd int int "int list" | NDvd int int "int list"

fun divisor :: "atom ⇒ int" where
"divisor (Le i ks) = 1" |
"divisor (Dvd d i ks) = d" |
"divisor (NDvd d i ks) = d"

fun neg⇩Z :: "atom ⇒ atom fm" where
"neg⇩Z (Le i ks) = Atom(Le (1-i) (-ks))" |
"neg⇩Z (Dvd d i ks) = Atom(NDvd d i ks)" |
"neg⇩Z (NDvd d i ks) = Atom(Dvd d i ks)"

fun hd_coeff :: "atom ⇒ int" where
"hd_coeff (Le i ks) = (case ks of [] ⇒ 0 | k#_ ⇒ k)" |
"hd_coeff (Dvd d i ks) = (case ks of [] ⇒ 0 | k#_ ⇒ k)" |
"hd_coeff (NDvd d i ks) = (case ks of [] ⇒ 0 | k#_ ⇒ k)"

fun decr⇩Z :: "atom ⇒ atom" where
"decr⇩Z (Le i ks) = Le i (tl ks)" |
"decr⇩Z (Dvd d i ks) = Dvd d i (tl ks)" |
"decr⇩Z (NDvd d i ks) = NDvd d i (tl ks)"

fun I⇩Z :: "atom ⇒ int list ⇒ bool" where
"I⇩Z (Le i ks) xs = (i ≤ ⟨ks,xs⟩)" |
"I⇩Z (Dvd d i ks) xs = (d dvd i+⟨ks,xs⟩)" |
"I⇩Z (NDvd d i ks) xs = (¬ d dvd i+⟨ks,xs⟩)"

definition "atoms⇩0 = ATOM.atoms⇩0 (λa. hd_coeff a ≠ 0)"
(* FIXME !!! (incl: display should hide params)*)

interpretation Z:
ATOM neg⇩Z "(λa. divisor a ≠ 0)" I⇩Z "(λa. hd_coeff a ≠ 0)" decr⇩Z
rewrites "ATOM.atoms⇩0 (λa. hd_coeff a ≠ 0) = atoms⇩0"
proof goal_cases
case 1
thus ?case
apply(unfold_locales)
apply(case_tac a)
apply simp_all
apply(case_tac a)
apply simp_all
apply(case_tac a)
apply (simp_all)
apply arith
apply(case_tac a)
apply(case_tac a)
apply simp_all
done
next
case 2
qed

setup ‹Sign.revert_abbrev "" @{const_abbrev Z.I}›
setup ‹Sign.revert_abbrev "" @{const_abbrev Z.lift_dnf_qe}›
(* FIXME doesn't work*)
(* FIXME does not help
setup {* Sign.revert_abbrev "" @{const_abbrev Z.normal} *}
*)

abbreviation
"hd_coeff_is1 a ≡
(case a of Le _ _ ⇒ hd_coeff a ∈ {1,-1} | _ ⇒ hd_coeff a = 1)"

fun asubst :: "int ⇒ int list ⇒ atom ⇒ atom" where
"asubst i' ks' (Le i (k#ks)) = Le (i - k*i') (k *⇩s ks' + ks)" |
"asubst i' ks' (Dvd d i (k#ks)) = Dvd d (i + k*i') (k *⇩s ks' + ks)" |
"asubst i' ks' (NDvd d i (k#ks)) = NDvd d (i + k*i') (k *⇩s ks' + ks)" |
"asubst i' ks' a = a"

abbreviation subst :: "int ⇒ int list ⇒ atom fm ⇒ atom fm"
where "subst i ks ≡ map⇩f⇩m (asubst i ks)"

lemma IZ_asubst: "I⇩Z (asubst i ks a) xs = I⇩Z a ((i + ⟨ks,xs⟩) # xs)"
apply (cases a)
apply (rename_tac list)
apply (case_tac list)
apply (rename_tac list)
apply (case_tac list)
apply (rename_tac list)
apply (case_tac list)
done

lemma I_subst:
"qfree φ ⟹ Z.I φ ((i + ⟨ks,xs⟩) # xs) = Z.I (subst i ks φ) xs"

lemma divisor_asubst[simp]: "divisor (asubst i ks a) = divisor a"
by(induct i ks a rule:asubst.induct) auto

definition "lbounds as = [(i,ks). Le i (k#ks) ← as, k>0]"
definition "ubounds as = [(i,ks). Le i (k#ks) ← as, k<0]"
lemma set_lbounds:
"set(lbounds as) = {(i,ks)|i k ks. Le i (k#ks) ∈ set as ∧ k>0}"
by(auto simp: lbounds_def split:list.splits atom.splits if_splits)
lemma set_ubounds:
"set(ubounds as) = {(i,ks)|i k ks. Le i (k#ks) ∈ set as ∧ k<0}"
by(auto simp: ubounds_def split:list.splits atom.splits if_splits)

lemma lbounds_append[simp]: "lbounds(as @ bs) = lbounds as @ lbounds bs"

subsection‹LCM and lemmas›

fun zlcms :: "int list ⇒ int" where
"zlcms [] = 1" |
"zlcms (i#is) = lcm i (zlcms is)"

lemma dvd_zlcms: "i ∈ set is ⟹ i dvd zlcms is"
by(induct "is") auto

lemma zlcms_pos: "∀i ∈ set is. i≠0 ⟹ zlcms is > 0"
by(induct "is")(auto simp:lcm_pos_int)

lemma zlcms0_iff[simp]: "(zlcms is = 0) = (0 ∈ set is)"
by (metis mod_by_0 dvd_eq_mod_eq_0 dvd_zlcms zlcms_pos less_le)

lemma elem_le_zlcms: "∀i ∈ set is. i ≠ 0 ⟹ i ∈ set is ⟹ i ≤ zlcms is"
by (metis dvd_zlcms zdvd_imp_le zlcms_pos)

subsection‹Setting coeffiencients to 1 or -1›

fun hd_coeff1 :: "int ⇒ atom ⇒ atom" where
"hd_coeff1 m (Le i (k#ks)) =
(if k=0 then Le i (k#ks)
else let m' = m div (abs k) in Le (m'*i) (sgn k # (m' *⇩s ks)))" |
"hd_coeff1 m (Dvd d i (k#ks)) =
(if k=0 then Dvd d i (k#ks)
else let m' = m div k in Dvd (m'*d) (m'*i) (1 # (m' *⇩s ks)))" |
"hd_coeff1 m (NDvd d i (k#ks)) =
(if k=0 then NDvd d i (k#ks)
else let m' = m div k in NDvd (m'*d) (m'*i) (1 # (m' *⇩s ks)))" |
"hd_coeff1 _ a = a"

text‹The def of @{const hd_coeff1} on @{const Dvd} and @{const NDvd} is
different from the @{const Le} because it allows the resulting head
coefficient to be 1 rather than 1 or -1. We show that the other version has
the same semantics:›

lemma "⟦ k ≠ 0; k dvd m ⟧ ⟹
I⇩Z (hd_coeff1 m (Dvd d i (k#ks))) (x#e) = (let m' = m div (abs k) in
I⇩Z (Dvd (m'*d) (m'*i) (sgn k # (m' *⇩s ks))) (x#e))"
apply(auto simp:algebra_simps abs_if sgn_if)
apply(simp add: zdiv_zminus2_eq_if dvd_eq_mod_eq_0[THEN iffD1] algebra_simps)
apply(simp add: zdiv_zminus2_eq_if dvd_eq_mod_eq_0[THEN iffD1] algebra_simps)
done

lemma I_hd_coeff1_mult_a: assumes "m>0"
shows "hd_coeff a dvd m | hd_coeff a = 0 ⟹ I⇩Z (hd_coeff1 m a) (m*x#xs) = I⇩Z a (x#xs)"
proof(induct a)
case [simp]: (Le i ks)
show ?case
proof(cases ks)
case Nil thus ?thesis by simp
next
case [simp]: (Cons k ks')
show ?thesis
proof cases
assume "k=0" thus ?thesis by simp
next
assume "k≠0"
with Le have "¦k¦ dvd m" by simp
let ?m' = "m div ¦k¦"
have "?m' > 0" using ‹¦k¦ dvd m› pos_imp_zdiv_pos_iff ‹m>0› ‹k≠0›
have 1: "k*(x*?m') = sgn k * x * m"
proof -
have "k*(x*?m') = (sgn k * abs k) * (x * ?m')"
by(simp only: mult_sgn_abs)
also have "… = sgn k * x * (abs k * ?m')" by simp
also have "… = sgn k * x * m"
using dvd_mult_div_cancel[OF ‹¦k¦ dvd m›] by(simp add:algebra_simps)
finally show ?thesis .
qed
have "I⇩Z (hd_coeff1 m (Le i ks)) (m*x#xs) ⟷
(i*?m' ≤ sgn k * m*x + ?m' * ⟨ks',xs⟩)"
also have "… ⟷ ?m'*i ≤ ?m' * (k*x + ⟨ks',xs⟩)" using 1
also have "… ⟷ i ≤ k*x + ⟨ks',xs⟩" using ‹?m'>0›
by simp
finally show ?thesis by(simp)
qed
qed
next
case [simp]: (Dvd d i ks)
show ?case
proof(cases ks)
case Nil thus ?thesis by simp
next
case [simp]: (Cons k ks')
show ?thesis
proof cases
assume "k=0" thus ?thesis by simp
next
assume "k≠0"
with Dvd have "k dvd m" by simp
let ?m' = "m div k"
have "?m' ≠ 0" using ‹k dvd m› zdiv_eq_0_iff ‹m>0› ‹k≠0›
have 1: "k*(x*?m') = x * m"
proof -
have "k*(x*?m') = x*(k*?m')" by(simp add:algebra_simps)
also have "… = x*m" using dvd_mult_div_cancel[OF ‹k dvd m›]
finally show ?thesis .
qed
have "I⇩Z (hd_coeff1 m (Dvd d i ks)) (m*x#xs) ⟷
(?m'*d dvd ?m'*i + m*x + ?m' * ⟨ks',xs⟩)"
also have "… ⟷ ?m'*d dvd ?m' * (i + k*x + ⟨ks',xs⟩)" using 1
also have "… ⟷ d dvd i + k*x + ⟨ks',xs⟩" using ‹?m'≠0› by(simp)
qed
qed
next
case [simp]: (NDvd d i ks)
show ?case
proof(cases ks)
case Nil thus ?thesis by simp
next
case [simp]: (Cons k ks')
show ?thesis
proof cases
assume "k=0" thus ?thesis by simp
next
assume "k≠0"
with NDvd have "k dvd m" by simp
let ?m' = "m div k"
have "?m' ≠ 0" using ‹k dvd m› zdiv_eq_0_iff ‹m>0› ‹k≠0›
have 1: "k*(x*?m') = x * m"
proof -
have "k*(x*?m') = x*(k*?m')" by(simp add:algebra_simps)
also have "… = x*m" using dvd_mult_div_cancel[OF ‹k dvd m›]
finally show ?thesis .
qed
have "I⇩Z (hd_coeff1 m (NDvd d i ks)) (m*x#xs) ⟷
¬(?m'*d dvd ?m'*i + m*x + ?m' * ⟨ks',xs⟩)"
also have "… ⟷ ¬ ?m'*d dvd ?m' * (i + k*x + ⟨ks',xs⟩)" using 1
also have "… ⟷ ¬ d dvd i + k*x + ⟨ks',xs⟩" using ‹?m'≠0› by(simp)
qed
qed
qed

lemma I_hd_coeff1_mult: assumes "m>0"
shows "qfree φ ⟹ ∀ a ∈ set(Z.atoms⇩0 φ). hd_coeff a dvd m ⟹
Z.I (map⇩f⇩m (hd_coeff1 m) φ) (m*x#xs) = Z.I φ (x#xs)"
proof(induct φ)
case (Atom a)
thus ?case using I_hd_coeff1_mult_a[OF ‹m>0›] by auto
qed simp_all

end


# Theory QEpres

(*  Author:     Tobias Nipkow, 2007  *)

theory QEpres
imports PresArith
begin

subsection‹DNF-based quantifier elimination›

(* all hd-coeffs are nonzero! *)
definition
"hd_coeffs1 as =
(let m = zlcms(map hd_coeff as)
in Dvd m 0 [1] # map (hd_coeff1 m) as)"

lemma I_hd_coeffs1:
assumes 0: "∀a∈set as. hd_coeff a ≠ 0" shows
"(∃x. ∀a ∈ set(hd_coeffs1 as). I⇩Z a (x#xs)) =
(∃x. ∀a ∈ set as. I⇩Z a (x#xs))" (is "?B = ?A")
proof -
let ?m = "zlcms(map hd_coeff as)"
have "?m>0" using 0 by(simp add:zlcms_pos)
have "?A = (∃x. ∀a ∈ set as. I⇩Z (hd_coeff1 ?m a) (?m*x#xs))"
by (simp add:I_hd_coeff1_mult_a[OF ‹?m>0›] dvd_zlcms 0)
also have "… = (∃x. ?m dvd x+0 ∧ (∀a ∈ set as. I⇩Z (hd_coeff1 ?m a) (x#xs)))"
by(rule unity_coeff_ex[THEN meta_eq_to_obj_eq])
qed

abbreviation "is_dvd a ≡ case a of Le _ _ ⇒ False | _ ⇒ True"

definition
"qe_pres⇩1 as =
(let ds = filter is_dvd as; (d::int) = zlcms(map divisor ds); ls = lbounds as
in if ls = []
then Disj [0..d - 1] (λn. list_conj(map (Atom ∘ asubst n []) ds))
else
Disj ls (λ(li,lks).
Disj [0..d - 1] (λn.
list_conj(map (Atom ∘ asubst (li + n) (-lks)) as))))"
text‹\noindent Note the optimization in the case @{prop"ls = []"}: only the
divisibility atoms are tested, not the inequalities. This complicates
the proof.›

lemma I_cyclic:
assumes "is_dvd a" and "hd_coeff a = 1" and "i mod divisor a = j mod divisor a"
shows "I⇩Z a (i#e) = I⇩Z a (j#e)"
proof (cases a)
case (Dvd d l ks)
with ‹hd_coeff a = 1› obtain ks' where [simp]: "ks = 1#ks'"
by(simp split:list.splits)
have "(l + (i + ⟨ks',e⟩)) mod d = (l + (j + ⟨ks',e⟩)) mod d" (is "?l=?r")
proof -
have "?l = (l mod d + (i + ⟨ks',e⟩) mod d) mod d"
also have "(i + ⟨ks',e⟩) mod d = (i mod d + ⟨ks',e⟩ mod d) mod d"
also have "i mod d = j mod d"
using ‹i mod divisor a = j mod divisor a› Dvd by simp
also have "(j mod d + ⟨ks',e⟩ mod d) mod d = (j + ⟨ks',e⟩) mod d"
also have "(l mod d + (j + ⟨ks',e⟩) mod d) mod d = ?r"
finally show ?thesis .
qed
thus ?thesis using Dvd by (simp add:dvd_eq_mod_eq_0)
next
case (NDvd d l ks)
with ‹hd_coeff a = 1› obtain ks' where [simp]: "ks = 1#ks'"
by(simp split:list.splits)
have "(l + (i + ⟨ks',e⟩)) mod d = (l + (j + ⟨ks',e⟩)) mod d" (is "?l=?r")
proof -
have "?l = (l mod d + (i + ⟨ks',e⟩) mod d) mod d"
also have "(i + ⟨ks',e⟩) mod d = (i mod d + ⟨ks',e⟩ mod d) mod d"
also have "i mod d = j mod d"
using ‹i mod divisor a = j mod divisor a› NDvd by simp
also have "(j mod d + ⟨ks',e⟩ mod d) mod d = (j + ⟨ks',e⟩) mod d"
also have "(l mod d + (j + ⟨ks',e⟩) mod d) mod d = ?r"
finally show ?thesis .
qed
thus ?thesis using NDvd by (simp add:dvd_eq_mod_eq_0)
next
case Le thus ?thesis using ‹is_dvd a› by simp
qed

lemma I_qe_pres⇩1:
assumes norm: "∀a ∈ set as. divisor a ≠ 0"
and hd: "∀a ∈ set as. hd_coeff_is1 a"
shows "Z.I (qe_pres⇩1 as) xs = (∃x. ∀a∈ set as. I⇩Z a (x#xs))"
proof -
let ?lbs = "lbounds as"
let ?ds = "filter is_dvd as"
let ?lcm = "zlcms(map divisor ?ds)"
let ?Ds = "{a ∈ set as. is_dvd a}"
let ?Us = "{a ∈ set as. case a of Le _ (k#_) ⇒ k < 0 | _ ⇒ False}"
let ?Ls = "{a ∈ set as. case a of Le _ (k#_) ⇒ k > 0 | _ ⇒ False}"
have as: "set as = ?Ds ∪ ?Ls ∪ ?Us" (is "_ = ?S")
proof -
{ fix x assume "x ∈ set as"
hence "x ∈ ?S" using hd by (cases x rule: atom.exhaust)(auto split:list.splits) }
moreover
{ fix x assume "x ∈ ?S"
hence "x ∈ set as" by auto }
ultimately show ?thesis by blast
qed
have 1: "∀a ∈ ?Ds. hd_coeff a = 1" using hd by(fastforce split:atom.splits)
show ?thesis  (is "?QE = (∃x. ?P x)")
proof
assume "?QE"
{ assume "?lbs = []"
with ‹?QE› obtain n where "n < ?lcm" and
A: "∀a ∈ ?Ds. I⇩Z a (n#xs)" using 1
by(auto simp:IZ_asubst qe_pres⇩1_def)
have "?Ls = {}" using ‹?lbs = []› set_lbounds[of as]
by (auto simp add:filter_empty_conv split:atom.split list.split)
have "∃x. ?P x"
proof cases
assume "?Us = {}"
with ‹?Ls = {}› have "set as = ?Ds" using as by(simp (no_asm_use))blast
hence "?P n" using A by auto
thus ?thesis ..
next
assume "?Us ≠ {}"
let ?M = "{⟨tl ks, xs⟩ - i|ks i. Le i ks ∈ ?Us}" let ?m = "Min ?M"
have "finite ?M"
proof -
have "finite ( (λLe i ks ⇒ ⟨tl ks, xs⟩ - i)
{a∈set as. ∃i k ks. k<0 ∧ a = Le i (k#ks)} )"
(is "finite ?B")
by simp
also have "?B = ?M" using hd
by(fastforce simp:image_def neq_Nil_conv split:atom.splits list.splits)
finally show ?thesis by auto
qed
have "?M ≠ {}"
proof -
from ‹?Us ≠ {}› obtain i k ks where "Le i (k#ks) ∈ ?Us ∧ k<0"
by (fastforce split:atom.splits list.splits)
thus ?thesis by auto
qed
let ?k = "(n - ?m) div ?lcm + 1" let ?x = "n - ?k * ?lcm"
have "∀a ∈ ?Ds. I⇩Z a (?x # xs)"
proof (intro allI ballI)
fix a assume "a ∈ ?Ds"
let ?d = "divisor a"
have 2: "?d dvd ?lcm" using ‹a ∈ ?Ds› by(simp add:dvd_zlcms)
have "?x mod ?d = n mod ?d" (is "?l = ?r")
proof -
have "?l = (?r - ((?k * ?lcm) mod ?d)) mod ?d"
also have "(?k * ?lcm) mod ?d = 0"
finally show ?thesis by simp
qed
thus "I⇩Z a (?x#xs)" using A I_cyclic[of a n ?x] ‹a ∈ ?Ds› 1 by auto
qed
moreover
have "∀a∈ ?Us. I⇩Z a (?x#xs)"
proof
fix a assume "a ∈ ?Us"
then obtain l ks where [simp]: "a = Le l (-1#ks)" using hd
by(fastforce split:atom.splits list.splits)
have "?m ≤ ⟨ks,xs⟩ - l"
using Min_le_iff[OF ‹finite ?M› ‹?M ≠ {}›] ‹a ∈ ?Us› by fastforce
moreover have "(n - ?m) mod ?lcm < ?lcm"
ultimately show "I⇩Z a (?x#xs)"
qed
moreover
have "set as = ?Ds ∪ ?Us" using as ‹?Ls = {}›
by (simp (no_asm_use)) blast
ultimately have "?P(?x)" by auto
thus ?thesis ..
qed }
moreover
{ assume "?lbs ≠ []"
with ‹?QE› obtain il ksl m
where "∀a∈set as. I⇩Z (asubst (il + m) ksl a) xs"
by(auto simp:qe_pres⇩1_def)
hence "?P(il + m + ⟨ksl,xs⟩)" by(simp add:IZ_asubst)
hence "∃x. ?P x" .. }
ultimately show "∃x. ?P x" by blast
next
assume "∃x. ?P x" then obtain x where x: "?P x" ..
show ?QE
proof cases
assume "?lbs = []"
moreover
have "∃x. 0 ≤ x ∧ x < ?lcm ∧ (∀a ∈ ?Ds. I⇩Z a (x # xs))"
(is "∃x. ?P x")
proof
{ fix a assume "a ∈ ?Ds"
hence "I⇩Z a ((x mod ?lcm) # xs) = I⇩Z a (x # xs)" using 1
by (fastforce del:iffI intro: I_cyclic
simp: mod_mod_cancel dvd_zlcms) }
thus "?P(x mod ?lcm)" using x norm by(simp add: zlcms_pos)
qed
ultimately show ?thesis by (auto simp:qe_pres⇩1_def IZ_asubst)
next
assume "?lbs ≠ []"
let ?L = "{i - ⟨ks,xs⟩ |ks i. (i,ks) ∈ set(lbounds as)}"
let ?lm = "Max ?L"
let ?n = "(x - ?lm) mod ?lcm"
have "finite ?L"
proof -
have "finite((λ(i,ks). i-⟨ks,xs⟩)  set(lbounds as) )" (is "finite ?B")
by simp
also have "?B = ?L" by auto
finally show ?thesis by auto
qed
moreover have "?L ≠ {}" using ‹?lbs ≠ []›
by(fastforce simp:neq_Nil_conv)
ultimately have "?lm ∈ ?L" by(rule Max_in)
then obtain li lks where "(li,lks)∈ set ?lbs" and lm: "?lm = li-⟨lks,xs⟩"
by blast
moreover
have n: "0 ≤ ?n ∧ ?n < ?lcm" using norm by(simp add:zlcms_pos)
moreover
{ fix a assume "a ∈ set as"
with x have "I⇩Z a (x # xs)" by blast
have "I⇩Z a ((li + ?n - ⟨lks,xs⟩) # xs)"
proof -
{ assume "a ∈ ?Ls"
then obtain i ks where [simp]: "a = Le i (1#ks)" using hd
by(fastforce split:atom.splits list.splits)
from ‹a ∈ ?Ls› have "i-⟨ks,xs⟩ ∈ ?L" by(fastforce simp:set_lbounds)
hence "i-⟨ks,xs⟩ ≤ li - ⟨lks,xs⟩"
using lm[symmetric] ‹finite ?L› ‹?L ≠ {}› by auto
hence ?thesis using n by simp }
moreover
{ assume "a ∈ ?Us"
then obtain i ks where [simp]: "a = Le i (-1#ks)" using hd
by(fastforce split:atom.splits list.splits)
have "Le li (1#lks) ∈ set as" using ‹(li,lks) ∈ set ?lbs› hd
by(auto simp:set_lbounds)
hence "li - ⟨lks,xs⟩ ≤ x" using x by auto
hence "(x - ?lm) mod ?lcm ≤ x - ?lm"
hence ?thesis using ‹I⇩Z a (x # xs)› lm by auto }
moreover
{ assume "a ∈ ?Ds"
have ?thesis
proof(rule I_cyclic[THEN iffD2, OF _ _ _ ‹I⇩Z a (x # xs)›])
show "is_dvd a" using ‹a ∈ ?Ds› by simp
show "hd_coeff a = 1" using ‹a ∈ ?Ds› hd
by(fastforce split:atom.splits list.splits)
have "li + (x-?lm) mod ?lcm - ⟨lks,xs⟩ = ?lm + (x-?lm) mod ?lcm"
using lm by arith
hence "(li + (x-?lm) mod ?lcm - ⟨lks,xs⟩) mod divisor a =
(?lm + (x-?lm) mod ?lcm) mod divisor a" by (simp only:)
also have "… =
(?lm mod divisor a + (x-?lm) mod ?lcm mod divisor a) mod divisor a"
also have
"… = (?lm mod divisor a + (x-?lm) mod divisor a) mod divisor a"
using ‹is_dvd a› ‹a∈ set as›
also have "… = (?lm + (x-?lm)) mod divisor a"
also have "… = x mod divisor a" by simp
finally
show "(li + ?n - ⟨lks,xs⟩) mod divisor a = x mod divisor a"
using norm by(auto simp: zlcms_pos)
qed }
ultimately show ?thesis using ‹a ∈ set as› as by blast
qed
}
ultimately show ?thesis using ‹?lbs ≠ []›
by (simp (no_asm_simp) add:qe_pres⇩1_def IZ_asubst split_def)
(force simp del:int_nat_eq)
qed
qed
qed

lemma  divisors_hd_coeffs1:
assumes div0: "∀a∈set as. divisor a ≠ 0" and hd0: "∀a∈set as. hd_coeff a ≠ 0"
and a: "a∈set (hd_coeffs1 as)" shows "divisor a ≠ 0"
proof -
let ?m = "zlcms(map hd_coeff as)"
from a have "a = Dvd ?m 0 [1] ∨ (∃b ∈ set as. a = hd_coeff1 ?m b)"
(is "?A ∨ ?B")
by(auto simp:hd_coeffs1_def)
thus ?thesis
proof
assume ?A thus ?thesis using hd0 by(auto)
next
assume ?B
then obtain b where "b ∈ set as" and [simp]: "a = hd_coeff1 ?m b" ..
hence b: "hd_coeff b ≠ 0" "divisor b ≠ 0" using div0 hd0 by auto
show ?thesis
proof (cases b)
case (Le i ks) thus ?thesis using b by(auto split:list.splits)
next
case [simp]: (Dvd d i ks)
then obtain k ks' where [simp]: "ks = k#ks'" using b
by(auto split:list.splits)
have k: "k ∈ set(map hd_coeff as)" using ‹b ∈ set as› by force
have "zlcms (map hd_coeff as) div k ≠ 0"
using b hd0 dvd_zlcms[OF k]
thus ?thesis using b by (simp)
next
case [simp]: (NDvd d i ks)
then obtain k ks' where [simp]: "ks = k#ks'" using b
by(auto split:list.splits)
have k: "k ∈ set(map hd_coeff as)" using ‹b ∈ set as› by force
have "zlcms (map hd_coeff as) div k ≠ 0"
using b hd0 dvd_zlcms[OF k]
thus ?thesis using b by (simp)
qed
qed
qed

lemma hd_coeff_is1_hd_coeffs1:
assumes hd0: "∀a∈set as. hd_coeff a ≠ 0"
and a: "a∈set (hd_coeffs1 as)" shows "hd_coeff_is1 a"
proof -
let ?m = "zlcms(map hd_coeff as)"
from a have "a = Dvd ?m 0 [1] ∨ (∃b ∈ set as. a = hd_coeff1 ?m b)"
(is "?A ∨ ?B")
by(auto simp:hd_coeffs1_def)
thus ?thesis
proof
assume ?A thus ?thesis using hd0 by simp
next
assume ?B
then obtain b where "b ∈ set as" and [simp]: "a = hd_coeff1 ?m b" ..
hence b: "hd_coeff b ≠ 0" using hd0 by auto
show ?thesis using b
by (cases b) (auto simp: sgn_if split:list.splits)
qed
qed

lemma I_qe_pres⇩1_o:
"⟦ ∀a ∈ set as. divisor a ≠ 0; ∀a∈set as. hd_coeff a ≠ 0 ⟧ ⟹
Z.I ((qe_pres⇩1 ∘ hd_coeffs1) as) e = (∃x. ∀a∈ set as. I⇩Z a (x#e))"
apply(simp)
apply(subst I_qe_pres⇩1)
using I_hd_coeffs1 apply(simp)
done

definition "qe_pres = Z.lift_dnf_qe (qe_pres⇩1 ∘ hd_coeffs1)"

lemma qfree_qe_pres_o: "qfree ((qe_pres⇩1 ∘ hd_coeffs1) as)"
by(auto simp:qe_pres⇩1_def intro!:qfree_list_disj)

lemma normal_qe_pres⇩1_o:
"∀a ∈ set as. hd_coeff a ≠ 0 ∧ divisor a ≠ 0 ⟹
Z.normal ((qe_pres⇩1 ∘ hd_coeffs1) as)"
supply image_cong_simp [cong del]
apply(auto simp:qe_pres⇩1_def Z.normal_def
dest!:atoms_list_disjE atoms_list_conjE)

apply(erule disjE) apply fastforce
apply (clarsimp)
apply(case_tac xa)
apply(rename_tac list) apply(case_tac list) apply fastforce apply (simp split:if_split_asm)
apply(rename_tac list) apply(case_tac list) apply fastforce
apply (simp split:if_split_asm) apply fastforce
apply(erule disjE) prefer 2 apply fastforce
apply (