Session LinearQuantifierElim

Theory Logic

(*  Author:     Tobias Nipkow, 2007  *)

section‹Logic›

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

text‹\noindent
We start with a generic formalization of quantified logical formulae
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 ("mapfm")

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" ("amapfm") where
"amapfm h TrueF = TrueF" |
"amapfm h FalseF = FalseF" |
"amapfm h (Atom a) = h a" |
"amapfm h (And φ1 φ2) = and (amapfm h φ1) (amapfm h φ2)" |
"amapfm h (Or φ1 φ2) = or (amapfm h φ1) (amapfm h φ2)" |
"amapfm h (Neg φ) = neg (amapfm h φ)"

lemma amap_fm_list_disj:
  "amapfm h (list_disj fs) = list_disj (map (amapfm 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)"
by(simp add:and_def)

lemma qfree_or[simp]: " qfree φ1; qfree φ2   qfree(or φ1 φ2)"
by(simp add:or_def)

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

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 (mapfm f φ) = qfree φ"
by (induct φ) simp_all

lemma atoms_list_disjE:
  "a  atoms(list_disj fs)  a  (φ  set fs. atoms φ)"
apply(induct fs)
 apply (simp add:list_disj_def)
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 (simp add:list_conj_def)
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 (mapfm 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  batoms(aneg a). anormal b"

fixes Ia :: "'a  'b list  bool"
assumes Ia_aneg: "interpret Ia (aneg a) xs = (¬ Ia a xs)"

fixes depends0 :: "'a  bool"
and decr :: "'a  'a" 
assumes not_dep_decr: "¬depends0 a  Ia a (x#xs) = Ia (decr a) xs"
assumes anormal_decr: "¬ depends0 a  anormal a  anormal(decr a)"

begin

fun atoms0 :: "'a fm  'a list" where
"atoms0 TrueF = []" |
"atoms0 FalseF = []" |
"atoms0 (Atom a) = (if depends0 a then [a] else [])" |
"atoms0 (And φ1 φ2) = atoms0 φ1 @ atoms0 φ2" |
"atoms0 (Or φ1 φ2) = atoms0 φ1 @ atoms0 φ2" |
"atoms0 (Neg φ) = atoms0 φ"

abbreviation I where "I  interpret Ia"

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)
  (simp_all add: nqfree_aneg and_def or_def)

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"
by(simp add:neg_def)

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

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
  } thus ?thesis by(simp add:list_conj_def)
qed

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

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
  } thus ?thesis by(simp add:list_disj_def)
qed

lemma I_nnf: "I (nnf φ) xs = I φ xs"
by(induct rule:nnf.induct)(simp_all add: Ia_aneg)

lemma I_dnf:
"nqfree φ  (asset (dnf φ). aset as. Ia 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)"
by (simp add:anormal_aneg normal_def)

lemma normal_and[simp]:
  "normal φ1  normal φ2  normal (and φ1 φ2)"
by (simp add:Logic.and_def)

lemma normal_or[simp]:
  "normal φ1  normal φ2  normal (or φ1 φ2)"
by (simp add:Logic.or_def)

lemma normal_list_disj[simp]:
  "φset fs. normal φ  normal (list_disj fs)"
apply(induct fs)
 apply (simp add:list_disj_def)
apply (simp add:list_disj_def)
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 (mapfm f φ) = normal φ"
by(induct φ) auto


lemma anormal_nnf:
  "qfree φ  normal φ  aatoms(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(simp_all add: normal_def)
    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 [aas. depends0 a];
      indep = [Atom(decr a). aas, ¬ depends0 a]
  in and qf (list_conj indep))"

abbreviation is_dnf_qe :: "('a list  'a fm)  'a list  bool" where
"is_dnf_qe qe as  xs. I(qe as) xs = (x.aset as. Ia a (x#xs))"

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

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

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

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

lemma qfree_lift_dnf_qe: "(as. (aset as. depends0 a)  qfree(qe as))
  qfree(lift_dnf_qe qe φ)"
by (induct φ) (simp_all add:qelim_def)

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

lemma lem: "P A. (xA. y. P x y) = (y. xA. P x y)" by blast

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

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

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

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

context notes [[simp_depth_limit = 5]]
begin

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

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

end

context notes [[simp_depth_limit = 9]]
begin

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

end

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


subsubsection‹NNF-based›

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

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

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

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

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

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

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

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

end


subsection‹With equality›

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

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

begin

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

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

definition "lift_dnfeq_qe = lift_dnf_qe  lift_eq_qe"

lemma qfree_lift_eq_qe:
  "(as. aset as. depends0 a  qfree (qe as)) 
   aset as. depends0 a  qfree(lift_eq_qe qe as)"
by(simp add:lift_eq_qe_def ball_Un split:list.split)

lemma qfree_lift_dnfeq_qe: "(as. (aset as. depends0 a)  qfree(qe as))
   qfree(lift_dnfeq_qe qe φ)"
by(simp add: lift_dnfeq_qe_def qfree_lift_dnf_qe qfree_lift_eq_qe)

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

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

end

end

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 negdlo :: "atom  atom fm" where
"negdlo (Less i j) = Or (Atom(Less j i)) (Atom(Eq i j))" |
"negdlo (Eq i j) = Or (Atom(Less i j)) (Atom(Less j i))"

fun Idlo :: "atom  'a::dlo list  bool" where
"Idlo (Eq i j) xs = (xs!i = xs!j)" |
"Idlo (Less i j) xs = (xs!i < xs!j)"

fun dependsdlo :: "atom  bool" where
"dependsdlo(Eq i j) = (i=0 | j=0)" |
"dependsdlo(Less i j) = (i=0 | j=0)"

fun decrdlo :: "atom  atom" where
"decrdlo (Less i j) = Less (i - 1) (j - 1)" |
"decrdlo (Eq i j) = Eq (i - 1) (j - 1)"

(* needed for code generation *)
definition [code del]: "nnf = ATOM.nnf negdlo"
definition [code del]: "qelim = ATOM.qelim dependsdlo decrdlo"
definition [code del]: "lift_dnf_qe = ATOM.lift_dnf_qe negdlo dependsdlo decrdlo"
definition [code del]: "lift_nnf_qe = ATOM.lift_nnf_qe negdlo"

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 negdlo "(λa. True)" Idlo dependsdlo decrdlo
apply(unfold_locales)
apply(case_tac a)
apply simp_all
apply(case_tac a)
apply (simp_all add:linorder_class.not_less_iff_gr_or_eq
                    linorder_not_less linorder_neq_iff)
apply(case_tac a)
apply(simp_all add:nth_Cons')
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.atoms0 f)}"
abbreviation "UB f xs  {xs!i|i. Less 0 (Suc i)  set(DLO.atoms0 f)}"
definition "EQ f xs = {xs!k|k.
  Eq (Suc k) 0  set(DLO.atoms0 f)  Eq 0 (Suc k)  set(DLO.atoms0 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 = (eset(ebounds(DLO.atoms0 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  mapfm (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)
apply(simp_all add:nth.simps split:nat.splits)
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-  amapfm 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+  amapfm aplus_inf"

lemma min_inf:
  "nqfree f  x. yx. 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
      by(simp add:nth_Cons') (metis no_lb linorder_not_less)
  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.yx. DLO.I (inf+ f) xs = DLO.I f (y # xs)"
  (is "_  x. ?P f x")
proof (induct f)
  have dlo_bound: "z::'a. x. yx. y > z"
  proof -
    fix z
    from no_ub obtain w :: 'a where "w > z" ..
    then have "yw. 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.atoms0 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.atoms0 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- φ)"
by(induct φ)(simp_all add:qfree_amin_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+ φ)"
by(induct φ)(simp_all add:qfree_aplus_inf)

end

Theory QEdlo

(*  Author:     Tobias Nipkow, 2007  *)

theory QEdlo
imports DLO
begin

subsection "DNF-based quantifier elimination"

definition qe_dlo1 :: "atom list  atom fm" where
"qe_dlo1 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_dlo1:
assumes less: "a  set as. is_Less a" and dep: "a  set as. dependsdlo a"
shows "DLO.I (qe_dlo1 as) xs = (x. a  set as. Idlo 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 dependsdlo.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_dlo1_def)
  with qe1 have 1: "x?Ls. y?Us. xs ! x < xs ! y"
    by (fastforce simp:qe_dlo1_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. Idlo 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. Idlo 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. Idlo 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. Idlo 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_dlo1_def is_Less_iff split:atom.splits nat.splits)
qed

lemma I_qe_dlo1_pretty:
  "a  set as. is_Less a  dependsdlo a  DLO.is_dnf_qe _ qe_dlo1 as"
by(metis I_qe_dlo1)

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 subst0 :: "atom  atom  atom" where
"subst0 (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 subst0_pretty:
  "subst0 (Eq i j) (Less m n) = Less (subst i j m) (subst i j n)"
  "subst0 (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 negdlo dependsdlo decrdlo (λEq i j  i=0  j=0 | a  False)
          (λEq i j  i=j | a  False) subst0"
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) subst0"

lemmas DLOe_code_lemmas = DLO_code_lemmas lift_dnfeq_qe_def lift_eq_qe_def

hide_const lift_dnfeq_qe lift_eq_qe
(*>*)

interpretation DLOe:
  ATOM_EQ negdlo "(λa. True)" Idlo dependsdlo decrdlo
          "(λEq i j  i=0  j=0 | a  False)"
          "(λEq i j  i=j | a  False)" subst0
apply(unfold_locales)
apply(fastforce simp:subst_def nth_Cons' split:atom.splits if_split_asm)
apply(simp add:subst_def split:atom.splits)
apply(fastforce simp:subst_def nth_Cons' split:atom.splits)
apply(fastforce simp add:subst_def split:atom.splits)
done

(*<*)
lemmas [folded DLOe_code_lemmas, code] =
  DLOe.lift_dnfeq_qe_def DLOe.lift_eq_qe_def
(*>*)

setup ‹Sign.revert_abbrev "" @{const_abbrev DLOe.lift_dnfeq_qe}

definition "qe_dlo = DLOe.lift_dnfeq_qe qe_dlo1"
(*<*)
lemmas [folded DLOe_code_lemmas, code] = qe_dlo_def 
(*>*)

lemma qfree_qe_dlo1: "qfree (qe_dlo1 as)"
by(auto simp:qe_dlo1_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_dlo1 qfree_qe_dlo1 DLOe.I_lift_dnfeq_qe
        simp: is_Less_iff not_is_Eq_iff split:atom.splits cong:conj_cong)

theorem qfree_qe_dlo: "qfree (qe_dlo φ)"
by(simp add:qe_dlo_def DLOe.qfree_lift_dnfeq_qe qfree_qe_dlo1)

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 Idlo"

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

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)"
by(simp_all add:interpret_def)

lemmas reify_eqs =
  Logic.interpret.simps(1,2,4-7)[of Idlo, 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 Idlo.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 asubst2 :: "nat  nat  atom  atom fm" where
"asubst2 l u (Less 0 0) = FalseF" |
"asubst2 l u (Less 0 (Suc j)) = Or (Atom(Less u j)) (Atom(Eq u j))" |
"asubst2 l u (Less (Suc i) 0) = Or (Atom(Less i l)) (Atom(Eq i l))" |
"asubst2 l u (Less (Suc i) (Suc j)) = Atom(Less i j)" |
"asubst2 l u (Eq 0 0) = TrueF" |
"asubst2 l u (Eq 0 _) = FalseF" |
"asubst2 l u (Eq _ 0) = FalseF" |
"asubst2 l u (Eq (Suc i) (Suc j)) = Atom(Eq i j)"

abbreviation "subst2 l u  amapfm (asubst2 l u)"

lemma I_subst21:
 "nqfree f  xs!l < xs!u  DLO.I (subst2 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: asubst2.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_subst22:
 "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 (subst2 l u f) xs"
proof (induct f)
  case (Atom a) show ?case
    apply (cases "(l,u,a)" rule: asubst2.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_interior1 φ =
(let as = DLO.atoms0 φ; lbs = lbounds as; ubs = ubounds as; ebs = ebounds as;
     intrs = [And (Atom(Less l u)) (subst2 l u φ). llbs, uubs]
 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 "lL.uU. l<x  x<u  (y{l<..<x}. yL)  (y{x<..<u}. yU)
             (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_interior1 φ) 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 φ
      by(auto simp add:qe_interior1_def amap_fm_list_disj)
  } moreover
  { assume  "DLO.I (inf+ φ) xs"
    hence ?EX using ?QE plus_inf[of φ xs] ‹nqfree φ
      by(auto simp add:qe_interior1_def amap_fm_list_disj)
  } moreover
  { assume "¬DLO.I (inf- φ) xs  ¬DLO.I (inf+ φ) xs 
            (xEQ φ xs. ¬DLO.I φ (x#xs))"
    with ?QE ‹nqfree φ obtain l u
      where "DLO.I (subst2 l u φ) xs" and "xs!l < xs!u"
      by(fastforce simp: qe_interior1_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_subst21[OF ‹nqfree φ xs!l < xs!u] by simp
    hence ?EX .. }
  ultimately show ?EX by blast
next
  let ?as = "DLO.atoms0 φ" 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_interior1_def)
  } moreover
  { assume "k  ?E. DLO.I (subst φ k) xs"
    hence ?QE by(force simp:qe_interior1_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 "lLB φ xs. uUB φ 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]
      by (simp add:nolub_def)
    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 (subst2 m n φ) xs" using noE
      by(force intro!: I_subst22[OF ‹nqfree φ])
    ultimately have ?QE
      by(fastforce simp add:qe_interior1_def bex_Un set_lbounds set_ubounds)
  } ultimately show ?QE by blast
qed

lemma qfree_asubst2: "qfree (asubst2 l u a)"
by(cases "(l,u,a)" rule:asubst2.cases) simp_all

lemma qfree_subst2: "nqfree φ  qfree (subst2 l u φ)"
by(induct φ) (simp_all add:qfree_asubst2)

lemma qfree_interior1: "nqfree φ  qfree(qe_interior1 φ)"
apply(simp add:qe_interior1_def)
apply(rule qfree_list_disj)
apply (auto simp:qfree_min_inf qfree_plus_inf qfree_subst2 qfree_map_fm)
done


definition "qe_interior = DLO.lift_nnf_qe qe_interior1"

lemma qfree_qe_interior: "qfree(qe_interior φ)"
by(simp add: qe_interior_def DLO.qfree_lift_nnf_qe qfree_interior1)

lemma I_qe_interior: "DLO.I (qe_interior φ) xs = DLO.I φ xs"
by(simp add:qe_interior_def DLO.I_lift_nnf_qe qfree_interior1 I_interior1)

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  amapfm (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 "i0  j0") apply simp
      apply(case_tac "i=0  j0") apply (fastforce split:if_split_asm)
      apply(case_tac "i0  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; yx   P y"
shows "lL. l<x  (y{l<..<x}. y  L)  (y. l<y  yx  P y)"
proof -
  let ?L = "{lL. 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_eps1(φ) =
(let as = DLO.atoms0 φ; 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_eps1 φ) xs = (x. DLO.I φ (x#xs))"
  (is "?QE = ?EX")
proof
  let ?as = "DLO.atoms0 φ" let ?ebs = "ebounds ?as"
  assume ?QE
  { assume "DLO.I (inf- φ) xs"
    hence ?EX using ?QE min_inf[of φ xs] ‹nqfree φ
      by(auto simp add:qe_eps1_def amap_fm_list_disj)
  } 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_eps1_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.atoms0 φ" 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_eps1_def)
  } moreover
  { assume "k  set ?ebs. DLO.I (subst φ k) xs"
    hence ?QE by(auto simp:qe_eps1_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 "lLB φ 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 lLB φ xs l<x x] x innermost_intvl[OF ‹nqfree φ _ _ x  EQ φ xs]
      by (simp add:nolb_def)
    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_eps1_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)"
by(induct φ) (simp_all add:qfree_asubst_peps)

lemma qfree_qe_eps1: "nqfree φ  qfree(qe_eps1 φ)"
apply(simp add:qe_eps1_def)
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_eps1"

lemma qfree_qe_eps: "qfree(qe_eps φ)"
by(simp add: qe_eps_def DLO.qfree_lift_nnf_qe qfree_qe_eps1)

lemma I_qe_eps: "DLO.I (qe_eps φ) xs = DLO.I φ xs"
by(simp add:qe_eps_def DLO.I_lift_nnf_qe qfree_qe_eps1 I_qe_eps1)

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 negR :: "atom  atom fm" where
"negR (Less r t) = Or (Atom(Less (-r) (-t))) (Atom(Eq r t))" |
"negR (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 "dependsR a = (hd_coeff a  0)"

fun decrR :: "atom  atom" where
"decrR (Less r rs) = Less r (tl rs)" |
"decrR (Eq r rs) = Eq r (tl rs)"

fun IR :: "atom  real list  bool" where
"IR (Less r cs) xs = (r < cs,xs)" |
"IR (Eq r cs) xs = (r = cs,xs)"

definition "atoms0 = ATOM.atoms0 dependsR"
(* FIXME !!! (incl: display should hide params)*)

interpretation R: ATOM negR "(λa. True)" IR dependsR decrR
  rewrites "ATOM.atoms0 dependsR = atoms0"
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)
    apply(simp_all add:dependsR_def split:list.splits)
    done
next
  case 2
  thus ?case by(simp add:atoms0_def)
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 (r1,cs1) (r2,cs2) = Less (r1-r2) (cs2 - cs1)"

(* 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, c0]"

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  c0}"
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.atoms0 f)  c0}"
abbreviation LB where
"LB f xs  {(r - cs,xs)/c|r c cs. Less r (c#cs)  set(R.atoms0 f)  c>0}"
abbreviation UB where
"UB f xs  {(r - cs,xs)/c|r c cs. Less r (c#cs)  set(R.atoms0 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  mapfm (asubst rcs) φ"

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

lemma I_asubst:
 "IR (asubst t a) xs = IR a (eval t xs # xs)"
proof(cases a)
  case (Less r cs)
  thus ?thesis by(cases t, cases cs,
    simp_all add:eval_def distrib_left iprod_left_add_distrib)
    arith
next
  case (Eq r cs)
  thus ?thesis
    by(cases t, cases cs, simp_all add:eval_def distrib_left iprod_left_add_distrib)
      arith
qed

lemma I_subst:
  "qfree φ  R.I (subst φ t) xs = R.I φ (eval t xs # xs)"
by(induct φ)(simp_all add:I_asubst)
lemma I_subst_pretty:
  "qfree φ  R.I (subst φ (r,cs)) xs = R.I φ ((r + cs,xs) # xs)"
by(simp add:I_subst eval_def)


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. yx. 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
          by(auto simp add: field_simps)
        hence ?thesis .. }
      moreover
      { assume "c>0"
        hence "?P (Atom a) ((r - cs,xs - 1)/c)" using Less Cons
          by(auto simp add: field_simps)
        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
          by(auto simp add: field_simps)
        hence ?thesis .. }
      moreover
      { assume "c>0"
        hence "?P (Atom a) ((r - cs,xs - 1)/c)" using Eq Cons
          by(auto simp add: field_simps)
        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. yx. 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
          by(auto simp add: field_simps)
        hence ?thesis .. }
      moreover
      { assume "c>0"
        hence "?P (Atom a) ((r - cs,xs + 1)/c)" using Less Cons
          by(auto simp add: field_simps)
        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
          by(auto simp add: field_simps)
        hence ?thesis .. }
      moreover
      { assume "c>0"
        hence "?P (Atom a) ((r - cs,xs + 1)/c)" using Eq Cons
          by(auto simp add: field_simps)
        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: dependsR_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: dependsR_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.atoms0 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.atoms0 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_FM1 :: "atom list  atom fm" where
"qe_FM1 as = list_conj [Atom(combine p q). plbounds as, qubounds as]"

theorem I_qe_FM1:
assumes less: "a  set as. is_Less a" and dep: "a  set as. dependsR a"
shows "R.I (qe_FM1 as) xs = (x. a  set as. IR 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 dependsR_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_FM1_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. IR 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. IR 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])
          (force simp add:field_simps)
      ultimately show "IR a ((Max ?lbs + 1) # xs)" by (simp add: field_simps)
    qed
    hence ?R .. }
  moreover
  { assume asm: "?lbs = {}  ?ubs  {}"
    have "a  set as. IR 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])
          (force simp add:field_simps)
      ultimately show "IR 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. IR 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_FM1_def iprod_left_diff_distrib less field_simps set_lbounds set_ubounds)
qed

corollary I_qe_FM1_pretty:
  "a  set as. is_Less a  dependsR a  R.is_dnf_qe qe_FM1 as"
by(metis I_qe_FM1)


fun subst0 :: "atom  atom  atom" where
"subst0 (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 subst0_pretty:
 "subst0 (Eq r (c#cs)) (Less s (d#ds)) = Less (s - (r*d)/c) (ds - (d/c) *s cs)"
 "subst0 (Eq r (c#cs)) (Eq s (d#ds)) = Eq (s - (r*d)/c) (ds - (d/c) *s cs)"
by auto

lemma I_subst0: "dependsR a  c  0 
       IR (subst0 (Eq r (c#cs)) a) xs = IR a ((r - cs,xs)/c # xs)"
apply(cases a)
by (auto simp add: dependsR_def iprod_left_diff_distrib algebra_simps diff_divide_distrib split:list.splits)

interpretation Re:
  ATOM_EQ negR "(λa. True)" IR dependsR decrR
          "(λEq _ (c#_)  c  0 | _  False)"
          "(λEq r cs  r=0  (c set cs. c=0) | _  False)" subst0
apply(unfold_locales)
   apply(simp del:subst0.simps add:I_subst0 split:atom.splits list.splits)
  apply(simp add: iprod0_if_coeffs0 split:atom.splits)
 apply(simp split:atom.splits list.splits)
 apply(rename_tac r ds c cs)
 apply(rule_tac x= "(r - cs,xs)/c" in exI)
 apply (simp add: algebra_simps diff_divide_distrib)
apply(simp add: self_list_diff set_replicate_conv_if
        split:atom.splits list.splits)
done

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

definition "qe_FM = Re.lift_dnfeq_qe qe_FM1"

lemma qfree_qe_FM1: "qfree (qe_FM1 as)"
by(auto simp:qe_FM1_def intro!:qfree_list_conj)

corollary I_qe_FM: "R.I (qe_FM φ) xs = R.I φ xs"
unfolding qe_FM_def
apply(rule Re.I_lift_dnfeq_qe)
 apply(rule qfree_qe_FM1)
apply(rule allI)
apply(rule I_qe_FM1)
 prefer 2 apply blast
apply(clarify)
apply(drule_tac x=a in bspec) apply simp
apply(simp add: dependsR_def split:atom.splits list.splits)
done

theorem qfree_qe_FM: "qfree (qe_FM f)"
by(simp add:qe_FM_def Re.qfree_lift_dnfeq_qe qfree_qe_FM1)

subsubsection‹Tests›

lemmas qesimps = qe_FM_def Re.lift_dnfeq_qe_def Re.lift_eq_qe_def R.qelim_def qe_FM1_def lbounds_def ubounds_def list_conj_def list_disj_def and_def or_def dependsR_def

lemma "qe_FM(TrueF) = TrueF"
by(simp add:qesimps)

lemma
  "qe_FM(ExQ (And (Atom(Less 0 [1])) (Atom(Less 0 [-1])))) = Atom(Less 0 [])"
by(simp add:qesimps)

lemma
 "qe_FM(ExQ (And (Atom(Less 0 [1])) (Atom(Less (- 1) [-1])))) = Atom(Less (- 1) [])"
by(simp add:qesimps)

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_FMo1 :: "atom list  atom fm" where
"qe_FMo1 as = list_conj [asimp(combine p q). plbounds as, qubounds as]"

lemma I_asimp: "R.I (asimp a) xs = IR a xs"
by(simp add:asimp_def iprod0_if_coeffs0 split:atom.split)

lemma I_qe_FMo1: "R.I (qe_FMo1 as) xs = R.I (qe_FM1 as) xs"
by(simp add:qe_FM1_def qe_FMo1_def I_asimp)

definition "qe_FMo = Re.lift_dnfeq_qe qe_FMo1"

lemma qfree_qe_FMo1: "qfree (qe_FMo1 as)"
by(auto simp:qe_FM1_def qe_FMo1_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 Re.I_lift_dnfeq_qe)
 apply(rule qfree_qe_FMo1)
apply(rule allI)
apply(subst I_qe_FMo1)
apply(rule I_qe_FM1)
 prefer 2 apply blast
apply(clarify)
apply(drule_tac x=a in bspec) apply simp
apply(simp add: dependsR_def split:atom.splits list.splits)
done

theorem qfree_qe_FMo: "qfree (qe_FMo f)"
by(simp add:qe_FMo_def Re.qfree_lift_dnfeq_qe qfree_qe_FMo1)

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 FR1 :: "atom fm  atom fm" where
"FR1 φ =
(let as = R.atoms0 φ; 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 "lL.uU. 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:dependsR_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
          by (simp add: field_simps)
        have ?thesis
        proof (rule ccontr)
          assume "¬ R.I (Atom a) (y#xs)"
          hence "?u  y" using Atom Less Cons c<0
            by (auto simp add: field_simps)
          hence "?u < u" using y<u by simp
          with x<?u show False using Atom Less Cons c<0
            by(auto simp:dependsR_def)
        qed } moreover
      { assume "c>0"
        hence "x > (r - cs,xs)/c" (is "_ > ?l") using r < c*x + cs,xs
          by (simp add: field_simps)
        have ?thesis
        proof (rule ccontr)
          assume "¬ R.I (Atom a) (y#xs)"
          hence "?l  y" using Atom Less Cons c>0
            by (auto simp add: field_simps)
          hence "?l > l" using y>l by simp
          with ?l<x show False using Atom Less Cons c>0
            by (auto simp:dependsR_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:dependsR_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 "c0"
        hence ?thesis using r = c*x + cs,xs Atom Eq Cons l<y y<u
          by (auto simp: dependsR_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_FR1:
assumes "nqfree φ" shows "R.I (FR1 φ) 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]
      by(auto simp add:FR1_def)
  } moreover
  { assume "R.I (inf+ φ) xs"
    hence ?EX using ?FR plus_inf[OF ‹nqfree φ, where xs=xs]
      by(auto simp add:FR1_def)
  } moreover
  { assume "x  EQ φ xs. R.I φ (x#xs)"
    hence ?EX using ?FR by(auto simp add:FR1_def)
  } moreover
  { assume "¬R.I (inf- φ) xs  ¬R.I (inf+ φ) xs 
            (xEQ φ 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: FR1_def eval_def
        diff_divide_distrib set_ebounds I_subst ‹nqfree φ) blast
    hence "R.I φ (eval (between (r,cs) (s,ds)) xs # xs)"
      by(simp add:I_subst ‹nqfree φ)
    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:FR1_def)
  } moreover
  { assume "x  EQ φ xs"
    then obtain r cs
      where "(r,cs)  set(ebounds(R.atoms0 φ))  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:FR1_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 "lLB φ xs. uUB φ 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.atoms0 φ)" "Less s (d # ds)  set (R.atoms0 φ)"
          "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"
        by (simp add: algebra_split_simps)
      from * have "c * s + d * cs,xs < d * r + c * ds,xs"
        by (simp add: field_simps)
      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: FR1_def bex_Un set_lbounds set_ubounds set_ebounds I_subst ‹nqfree φ)
  } ultimately show ?FR by blast
qed


definition "FR = R.lift_nnf_qe FR1"


lemma qfree_FR1: "nqfree φ  qfree (FR1 φ)"
apply(simp add:FR1_def)
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"
by(simp add:I_FR1 FR_def R.I_lift_nnf_qe qfree_FR1)

theorem qfree_FR: "qfree (FR φ)"
by(simp add:FR_def R.qfree_lift_nnf_qe qfree_FR1)

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  amapfm (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:dependsR_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
          by (simp add: field_simps)
        have ?thesis
        proof (rule ccontr)
          assume "¬ R.I (Atom a) (y#xs)"
          hence "?u  y" using Atom c<0
            by (auto simp add: field_simps)
          with x<?u show False using Atom c<0
            by(auto simp:dependsR_def)
        qed } moreover
      { assume "c>0"
        hence "x > (r - cs,xs)/c" (is "_ > ?l") using r < c*x + cs,xs
          by (simp add: field_simps)
        then have "?l < y" using Atom c>0
            by (auto simp:dependsR_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:dependsR_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 "c0"
        hence ?thesis using r = c*x + cs,xs Atom
          by (auto simp: dependsR_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
        by (simp add: mult_strict_left_mono_neg)
      ultimately have "s < d * (r + cs,xs) + ds,xs" by(simp add:algebra_simps)
      hence ?thesis using 1
        by (auto simp add: iprod_left_add_distrib algebra_simps)
    } 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
        by(simp_all add:nolb_def dependsR_def Ball_def field_simps)
      hence "?L < ?U  ?L = ?U"
        by (metis linorder_neqE_linordered_idom order_refl)
      hence ?thesis using Atom 1 d>0
        by (simp add: iprod_left_add_distrib field_simps)
    } ultimately show ?thesis by force
  next
    case 2 thus ?thesis using Atom
      by (fastforce simp: nolb_def EQ2_def dependsR_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")
        by(simp add:field_simps iprod_left_add_distrib)
      then obtain x where "?a < x" "x < ?b" by(metis dense)
      hence " y. ?a < y  y  x  s < d*y + ds,xs"
        using d<0 by (simp add:field_simps)
      (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
          by(simp add:field_simps iprod_left_add_distrib)
            (metis add_0_left add_less_cancel_right distrib_left mult.commute mult_strict_left_mono)
      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
            by (simp add:algebra_simps iprod_left_add_distrib)
        }
        thus ?thesis using 1 d>0
          by(force simp: iprod_left_add_distrib)
      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; yx   P y"
shows "lL. l<x  (y{l<..<x}. y  L)  (y. l<y  yx  P y)"
proof -
  let ?L = "{lL. 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_eps1(f) =
(let as = R.atoms0 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_eps1 f) xs = (x. R.I f (x#xs))"
  (is "?QE = ?EX")
proof
  let ?as = "R.atoms0 f" let ?ebs = "ebounds ?as"
  assume ?QE
  { assume "R.I (inf- f) xs"
    hence ?EX using ?QE min_inf[of f xs] ‹nqfree f
      by(auto simp add:qe_eps1_def amap_fm_list_disj)
  } 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_eps1_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.atoms0 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_eps1_def)
  } moreover
  { assume "rcs  set ?ebs. R.I (subst f rcs) xs"
    hence ?QE by(auto simp:qe_eps1_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 "lLB 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 lLB f xs l<x x] x innermost_intvl[OF ‹nqfree f _ _ x  EQ f xs]
      by (simp add:nolb_def)
    then obtain r c cs
      where *: "Less r (c#cs)  set(R.atoms0 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
      by(simp add:qe_eps1_def bex_Un set_lbounds) metis
  } 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)"
by(induct φ) (simp_all add:qfree_asubst_peps)

lemma qfree_qe_eps1: "nqfree φ  qfree(qe_eps1 φ)"
apply(simp add:qe_eps1_def)
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_eps1"

lemma qfree_qe_eps: "qfree(qe_eps φ)"
by(simp add: qe_eps_def R.qfree_lift_nnf_qe qfree_qe_eps1)

lemma I_qe_eps: "R.I (qe_eps φ) xs = R.I φ xs"
by(simp add:qe_eps_def R.I_lift_nnf_qe qfree_qe_eps1 I_eps1)

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 negZ :: "atom  atom fm" where
"negZ (Le i ks) = Atom(Le (1-i) (-ks))" |
"negZ (Dvd d i ks) = Atom(NDvd d i ks)" |
"negZ (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 decrZ :: "atom  atom" where
"decrZ (Le i ks) = Le i (tl ks)" |
"decrZ (Dvd d i ks) = Dvd d i (tl ks)" |
"decrZ (NDvd d i ks) = NDvd d i (tl ks)"

fun IZ :: "atom  int list  bool" where
"IZ (Le i ks) xs = (i  ks,xs)" |
"IZ (Dvd d i ks) xs = (d dvd i+ks,xs)" |
"IZ (NDvd d i ks) xs = (¬ d dvd i+ks,xs)"

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

interpretation Z:
  ATOM negZ "(λa. divisor a  0)" IZ "(λa. hd_coeff a  0)" decrZ
  rewrites "ATOM.atoms0 (λa. hd_coeff a  0) = atoms0"
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(simp_all add: split: list.splits)
    apply(case_tac a)
    apply simp_all
    done
next
  case 2
  thus ?case by(simp add:atoms0_def)
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  mapfm (asubst i ks)"

lemma IZ_asubst: "IZ (asubst i ks a) xs = IZ a ((i + ks,xs) # xs)"
apply (cases a)
apply (rename_tac list)
apply (case_tac list)
apply (simp_all add:algebra_simps iprod_left_add_distrib)
apply (rename_tac list)
apply (case_tac list)
apply (simp_all add:algebra_simps iprod_left_add_distrib)
apply (rename_tac list)
apply (case_tac list)
apply (simp_all add:algebra_simps iprod_left_add_distrib)
done

lemma I_subst:
  "qfree φ  Z.I φ ((i + ks,xs) # xs) = Z.I (subst i ks φ) xs"
by (induct φ) (simp_all add:IZ_asubst)

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"
by(simp add:lbounds_def)


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. i0  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  
  IZ (hd_coeff1 m (Dvd d i (k#ks))) (x#e) = (let m' = m div (abs k) in
  IZ (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 (metis diff_conv_add_uminus add.left_commute dvd_minus_iff minus_add_distrib)
apply(simp add: zdiv_zminus2_eq_if dvd_eq_mod_eq_0[THEN iffD1] algebra_simps)
apply (metis diff_conv_add_uminus add.left_commute dvd_minus_iff minus_add_distrib)
done


lemma I_hd_coeff1_mult_a: assumes "m>0"
shows "hd_coeff a dvd m | hd_coeff a = 0  IZ (hd_coeff1 m a) (m*x#xs) = IZ 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 "k0"
      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 k0
        by(simp add:zdvd_imp_le)
      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 "IZ (hd_coeff1 m (Le i ks)) (m*x#xs) 
            (i*?m'  sgn k * m*x + ?m' * ks',xs)"
        using k0 by(simp add: algebra_simps)
      also have "  ?m'*i  ?m' * (k*x + ks',xs)" using 1
        by(simp (no_asm_simp) add:algebra_simps)
      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 "k0"
      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 k0
        by(simp add:linorder_not_less zdvd_imp_le)
      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]
          by(simp add:algebra_simps)
        finally show ?thesis .
      qed
      have "IZ (hd_coeff1 m (Dvd d i ks)) (m*x#xs) 
            (?m'*d dvd ?m'*i + m*x + ?m' * ks',xs)"
        using k0 by(simp add: algebra_simps)
      also have "  ?m'*d dvd ?m' * (i + k*x + ks',xs)" using 1
        by(simp (no_asm_simp) add:algebra_simps)
      also have "  d dvd i + k*x + ks',xs" using ?m'0 by(simp)
      finally show ?thesis by(simp add:algebra_simps)
    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 "k0"
      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 k0
        by(simp add:linorder_not_less zdvd_imp_le)
      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]
          by(simp add:algebra_simps)
        finally show ?thesis .
      qed
      have "IZ (hd_coeff1 m (NDvd d i ks)) (m*x#xs) 
            ¬(?m'*d dvd ?m'*i + m*x + ?m' * ks',xs)"
        using k0 by(simp add: algebra_simps)
      also have "  ¬ ?m'*d dvd ?m' * (i + k*x + ks',xs)" using 1
        by(simp (no_asm_simp) add:algebra_simps)
      also have "  ¬ d dvd i + k*x + ks',xs" using ?m'0 by(simp)
      finally show ?thesis by(simp add:algebra_simps)
    qed
  qed
qed


lemma I_hd_coeff1_mult: assumes "m>0"
shows "qfree φ   a  set(Z.atoms0 φ). hd_coeff a dvd m 
 Z.I (mapfm (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: "aset as. hd_coeff a  0" shows
  "(x. a  set(hd_coeffs1 as). IZ a (x#xs)) =
   (x. a  set as. IZ 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. IZ (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. IZ (hd_coeff1 ?m a) (x#xs)))"
    by(rule unity_coeff_ex[THEN meta_eq_to_obj_eq])
  finally show ?thesis by(simp add:hd_coeffs1_def)
qed


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

definition
"qe_pres1 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 "IZ a (i#e) = IZ 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"
      by (simp add: mod_add_eq)
    also have "(i + ks',e) mod d = (i mod d + ks',e mod d) mod d"
      by (simp add: mod_add_eq)
    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"
      by(rule mod_add_eq)
    also have "(l mod d + (j + ks',e) mod d) mod d = ?r"
      by(rule mod_add_eq)
    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"
      by (simp add: mod_add_eq)
    also have "(i + ks',e) mod d = (i mod d + ks',e mod d) mod d"
      by (simp add: mod_add_eq)
    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"
      by(rule mod_add_eq)
    also have "(l mod d + (j + ks',e) mod d) mod d = ?r"
      by(rule mod_add_eq)
    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_pres1:
assumes norm: "a  set as. divisor a  0"
and hd: "a  set as. hd_coeff_is1 a"
shows "Z.I (qe_pres1 as) xs = (x. a set as. IZ 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. IZ a (n#xs)" using 1
        by(auto simp:IZ_asubst qe_pres1_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) `
                         {aset 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. IZ 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"
              by (simp add: mod_diff_eq)
            also have "(?k * ?lcm) mod ?d = 0"
              by(simp add: dvd_eq_mod_eq_0[symmetric] dvd_mult[OF 2])
            finally show ?thesis by simp
          qed
          thus "IZ a (?x#xs)" using A I_cyclic[of a n ?x] a  ?Ds 1 by auto
        qed
        moreover
        have "a ?Us. IZ 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"
            by(simp add: pos_mod_bound[OF zlcms_pos] norm)
          ultimately show "IZ a (?x#xs)"
            by(simp add:minus_mod_eq_mult_div [symmetric] algebra_simps)
        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 "aset as. IZ (asubst (il + m) ksl a) xs"
        by(auto simp:qe_pres1_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. IZ a (x # xs))"
        (is "x. ?P x")
      proof
        { fix a assume "a  ?Ds"
          hence "IZ a ((x mod ?lcm) # xs) = IZ 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_pres1_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 "IZ a (x # xs)" by blast
        have "IZ 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"
              using lm by(simp add: zmod_le_nonneg_dividend)
            hence ?thesis using ‹IZ a (x # xs) lm by auto }
          moreover
          { assume "a  ?Ds"
            have ?thesis
            proof(rule I_cyclic[THEN iffD2, OF _ _ _ ‹IZ 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"
                by (simp add: mod_add_eq)
              also have
        " = (?lm mod divisor a + (x-?lm) mod divisor a) mod divisor a"
                using ‹is_dvd a a set as
                by(simp add: mod_mod_cancel dvd_zlcms)
              also have " = (?lm + (x-?lm)) mod divisor a"
                by(rule mod_add_eq)
              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_pres1_def IZ_asubst split_def)
           (force simp del:int_nat_eq)
    qed
  qed
qed

lemma  divisors_hd_coeffs1:
assumes div0: "aset as. divisor a  0" and hd0: "aset as. hd_coeff a  0"
and a: "aset (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]
        by(auto simp add:dvd_def)
      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]
        by(auto simp add:dvd_def)
      thus ?thesis using b by (simp)
    qed
  qed
qed

lemma hd_coeff_is1_hd_coeffs1:
assumes hd0: "aset as. hd_coeff a  0"
and a: "aset (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_pres1_o:
 " a  set as. divisor a  0; aset as. hd_coeff a  0  
  Z.I ((qe_pres1  hd_coeffs1) as) e = (x. a set as. IZ a (x#e))"
apply(simp)
apply(subst I_qe_pres1)
  apply(simp add: divisors_hd_coeffs1)
 apply(simp add: hd_coeff_is1_hd_coeffs1)
using I_hd_coeffs1 apply(simp)
done

definition "qe_pres = Z.lift_dnf_qe (qe_pres1  hd_coeffs1)"

lemma qfree_qe_pres_o: "qfree ((qe_pres1  hd_coeffs1) as)"
by(auto simp:qe_pres1_def intro!:qfree_list_disj)


lemma normal_qe_pres1_o:
  "a  set as. hd_coeff a  0  divisor a  0 
   Z.normal ((qe_pres1  hd_coeffs1) as)"
  supply image_cong_simp [cong del]
apply(auto simp:qe_pres1_def Z.normal_def
   dest!:atoms_list_disjE atoms_list_conjE)

apply(simp add: hd_coeffs1_def)
 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(simp add:zdiv_eq_0_iff)
 apply(subgoal_tac "a  set(map hd_coeff as)")
  prefer 2 apply force
 apply(subgoal_tac "i set(map hd_coeff as). i  0")
  prefer 2 apply simp
 apply (metis elem_le_zlcms linorder_not_le zlcms_pos)
apply(rename_tac list) apply(case_tac list) apply fastforce
apply (