Theory Cooper

(*  Title:      HOL/Decision_Procs/Cooper.thy
    Author:     Amine Chaieb
*)

section ‹Presburger arithmetic based on Cooper's algorithm›

theory Cooper
imports
  Complex_Main
  "HOL-Library.Code_Target_Numeral"
begin

subsection ‹Basic formulae›

datatype (plugins del: size) num = C int | Bound nat | CN nat int num
  | Neg num | Add num num | Sub num num
  | Mul int num

instantiation num :: size
begin

primrec size_num :: "num  nat"
  where
    "size_num (C c) = 1"
  | "size_num (Bound n) = 1"
  | "size_num (Neg a) = 1 + size_num a"
  | "size_num (Add a b) = 1 + size_num a + size_num b"
  | "size_num (Sub a b) = 3 + size_num a + size_num b"
  | "size_num (CN n c a) = 4 + size_num a"
  | "size_num (Mul c a) = 1 + size_num a"

instance ..

end

primrec Inum :: "int list  num  int"
  where
    "Inum bs (C c) = c"
  | "Inum bs (Bound n) = bs ! n"
  | "Inum bs (CN n c a) = c * (bs ! n) + Inum bs a"
  | "Inum bs (Neg a) = - Inum bs a"
  | "Inum bs (Add a b) = Inum bs a + Inum bs b"
  | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
  | "Inum bs (Mul c a) = c * Inum bs a"

datatype (plugins del: size) fm = T | F
  | Lt num | Le num | Gt num | Ge num | Eq num | NEq num
  | Dvd int num | NDvd int num
  | Not fm | And fm fm | Or fm fm | Imp fm fm | Iff fm fm
  | E fm | A fm | Closed nat | NClosed nat

instantiation fm :: size
begin

primrec size_fm :: "fm  nat"
  where
    "size_fm (Not p) = 1 + size_fm p"
  | "size_fm (And p q) = 1 + size_fm p + size_fm q"
  | "size_fm (Or p q) = 1 + size_fm p + size_fm q"
  | "size_fm (Imp p q) = 3 + size_fm p + size_fm q"
  | "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)"
  | "size_fm (E p) = 1 + size_fm p"
  | "size_fm (A p) = 4 + size_fm p"
  | "size_fm (Dvd i t) = 2"
  | "size_fm (NDvd i t) = 2"
  | "size_fm T = 1"
  | "size_fm F = 1"
  | "size_fm (Lt _) = 1"
  | "size_fm (Le _) = 1"
  | "size_fm (Gt _) = 1"
  | "size_fm (Ge _) = 1"
  | "size_fm (Eq _) = 1"
  | "size_fm (NEq _) = 1"
  | "size_fm (Closed _) = 1"
  | "size_fm (NClosed _) = 1"

instance ..

end

lemma fmsize_pos [simp]: "size p > 0"
  for p :: fm
  by (induct p) simp_all

primrec Ifm :: "bool list  int list  fm  bool"  ― ‹Semantics of formulae (fm›)›
  where
    "Ifm bbs bs T  True"
  | "Ifm bbs bs F  False"
  | "Ifm bbs bs (Lt a)  Inum bs a < 0"
  | "Ifm bbs bs (Gt a)  Inum bs a > 0"
  | "Ifm bbs bs (Le a)  Inum bs a  0"
  | "Ifm bbs bs (Ge a)  Inum bs a  0"
  | "Ifm bbs bs (Eq a)  Inum bs a = 0"
  | "Ifm bbs bs (NEq a)  Inum bs a  0"
  | "Ifm bbs bs (Dvd i b)  i dvd Inum bs b"
  | "Ifm bbs bs (NDvd i b)  ¬ i dvd Inum bs b"
  | "Ifm bbs bs (Not p)  ¬ Ifm bbs bs p"
  | "Ifm bbs bs (And p q)  Ifm bbs bs p  Ifm bbs bs q"
  | "Ifm bbs bs (Or p q)  Ifm bbs bs p  Ifm bbs bs q"
  | "Ifm bbs bs (Imp p q)  (Ifm bbs bs p  Ifm bbs bs q)"
  | "Ifm bbs bs (Iff p q)  Ifm bbs bs p = Ifm bbs bs q"
  | "Ifm bbs bs (E p)  (x. Ifm bbs (x # bs) p)"
  | "Ifm bbs bs (A p)  (x. Ifm bbs (x # bs) p)"
  | "Ifm bbs bs (Closed n)  bbs ! n"
  | "Ifm bbs bs (NClosed n)  ¬ bbs ! n"

fun prep :: "fm  fm"
  where
    "prep (E T) = T"
  | "prep (E F) = F"
  | "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
  | "prep (E (Imp p q)) = Or (prep (E (Not p))) (prep (E q))"
  | "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (Not p) (Not q))))"
  | "prep (E (Not (And p q))) = Or (prep (E (Not p))) (prep (E(Not q)))"
  | "prep (E (Not (Imp p q))) = prep (E (And p (Not q)))"
  | "prep (E (Not (Iff p q))) = Or (prep (E (And p (Not q)))) (prep (E(And (Not p) q)))"
  | "prep (E p) = E (prep p)"
  | "prep (A (And p q)) = And (prep (A p)) (prep (A q))"
  | "prep (A p) = prep (Not (E (Not p)))"
  | "prep (Not (Not p)) = prep p"
  | "prep (Not (And p q)) = Or (prep (Not p)) (prep (Not q))"
  | "prep (Not (A p)) = prep (E (Not p))"
  | "prep (Not (Or p q)) = And (prep (Not p)) (prep (Not q))"
  | "prep (Not (Imp p q)) = And (prep p) (prep (Not q))"
  | "prep (Not (Iff p q)) = Or (prep (And p (Not q))) (prep (And (Not p) q))"
  | "prep (Not p) = Not (prep p)"
  | "prep (Or p q) = Or (prep p) (prep q)"
  | "prep (And p q) = And (prep p) (prep q)"
  | "prep (Imp p q) = prep (Or (Not p) q)"
  | "prep (Iff p q) = Or (prep (And p q)) (prep (And (Not p) (Not q)))"
  | "prep p = p"

lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
  by (induct p arbitrary: bs rule: prep.induct) auto


fun qfree :: "fm  bool"  ― ‹Quantifier freeness›
  where
    "qfree (E p)  False"
  | "qfree (A p)  False"
  | "qfree (Not p)  qfree p"
  | "qfree (And p q)  qfree p  qfree q"
  | "qfree (Or  p q)  qfree p  qfree q"
  | "qfree (Imp p q)  qfree p  qfree q"
  | "qfree (Iff p q)  qfree p  qfree q"
  | "qfree p  True"


subsection ‹Boundedness and substitution›

primrec numbound0 :: "num  bool"  ― ‹a num› is ‹independent› of Bound 0›
  where
    "numbound0 (C c)  True"
  | "numbound0 (Bound n)  n > 0"
  | "numbound0 (CN n i a)  n > 0  numbound0 a"
  | "numbound0 (Neg a)  numbound0 a"
  | "numbound0 (Add a b)  numbound0 a  numbound0 b"
  | "numbound0 (Sub a b)  numbound0 a  numbound0 b"
  | "numbound0 (Mul i a)  numbound0 a"

lemma numbound0_I:
  assumes "numbound0 a"
  shows "Inum (b # bs) a = Inum (b' # bs) a"
  using assms by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)

primrec bound0 :: "fm  bool" ― ‹a formula is independent of Bound 0›
  where
    "bound0 T  True"
  | "bound0 F  True"
  | "bound0 (Lt a)  numbound0 a"
  | "bound0 (Le a)  numbound0 a"
  | "bound0 (Gt a)  numbound0 a"
  | "bound0 (Ge a)  numbound0 a"
  | "bound0 (Eq a)  numbound0 a"
  | "bound0 (NEq a)  numbound0 a"
  | "bound0 (Dvd i a)  numbound0 a"
  | "bound0 (NDvd i a)  numbound0 a"
  | "bound0 (Not p)  bound0 p"
  | "bound0 (And p q)  bound0 p  bound0 q"
  | "bound0 (Or p q)  bound0 p  bound0 q"
  | "bound0 (Imp p q)  bound0 p  bound0 q"
  | "bound0 (Iff p q)  bound0 p  bound0 q"
  | "bound0 (E p)  False"
  | "bound0 (A p)  False"
  | "bound0 (Closed P)  True"
  | "bound0 (NClosed P)  True"

lemma bound0_I:
  assumes "bound0 p"
  shows "Ifm bbs (b # bs) p = Ifm bbs (b' # bs) p"
  using assms numbound0_I[where b="b" and bs="bs" and b'="b'"]
  by (induct p rule: fm.induct) (auto simp add: gr0_conv_Suc)

fun numsubst0 :: "num  num  num"
  where
    "numsubst0 t (C c) = (C c)"
  | "numsubst0 t (Bound n) = (if n = 0 then t else Bound n)"
  | "numsubst0 t (CN 0 i a) = Add (Mul i t) (numsubst0 t a)"
  | "numsubst0 t (CN n i a) = CN n i (numsubst0 t a)"
  | "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
  | "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
  | "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)"
  | "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"

lemma numsubst0_I: "Inum (b # bs) (numsubst0 a t) = Inum ((Inum (b # bs) a) # bs) t"
  by (induct t rule: numsubst0.induct) (auto simp: nth_Cons')

lemma numsubst0_I': "numbound0 a  Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
  by (induct t rule: numsubst0.induct) (auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])

primrec subst0:: "num  fm  fm"  ― ‹substitute a num› into a formula for Bound 0›
  where
    "subst0 t T = T"
  | "subst0 t F = F"
  | "subst0 t (Lt a) = Lt (numsubst0 t a)"
  | "subst0 t (Le a) = Le (numsubst0 t a)"
  | "subst0 t (Gt a) = Gt (numsubst0 t a)"
  | "subst0 t (Ge a) = Ge (numsubst0 t a)"
  | "subst0 t (Eq a) = Eq (numsubst0 t a)"
  | "subst0 t (NEq a) = NEq (numsubst0 t a)"
  | "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
  | "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
  | "subst0 t (Not p) = Not (subst0 t p)"
  | "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
  | "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
  | "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
  | "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
  | "subst0 t (Closed P) = (Closed P)"
  | "subst0 t (NClosed P) = (NClosed P)"

lemma subst0_I:
  assumes "qfree p"
  shows "Ifm bbs (b # bs) (subst0 a p) = Ifm bbs (Inum (b # bs) a # bs) p"
  using assms numsubst0_I[where b="b" and bs="bs" and a="a"]
  by (induct p) (simp_all add: gr0_conv_Suc)

fun decrnum:: "num  num"
  where
    "decrnum (Bound n) = Bound (n - 1)"
  | "decrnum (Neg a) = Neg (decrnum a)"
  | "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
  | "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"
  | "decrnum (Mul c a) = Mul c (decrnum a)"
  | "decrnum (CN n i a) = (CN (n - 1) i (decrnum a))"
  | "decrnum a = a"

fun decr :: "fm  fm"
  where
    "decr (Lt a) = Lt (decrnum a)"
  | "decr (Le a) = Le (decrnum a)"
  | "decr (Gt a) = Gt (decrnum a)"
  | "decr (Ge a) = Ge (decrnum a)"
  | "decr (Eq a) = Eq (decrnum a)"
  | "decr (NEq a) = NEq (decrnum a)"
  | "decr (Dvd i a) = Dvd i (decrnum a)"
  | "decr (NDvd i a) = NDvd i (decrnum a)"
  | "decr (Not p) = Not (decr p)"
  | "decr (And p q) = And (decr p) (decr q)"
  | "decr (Or p q) = Or (decr p) (decr q)"
  | "decr (Imp p q) = Imp (decr p) (decr q)"
  | "decr (Iff p q) = Iff (decr p) (decr q)"
  | "decr p = p"

lemma decrnum:
  assumes "numbound0 t"
  shows "Inum (x # bs) t = Inum bs (decrnum t)"
  using assms by (induct t rule: decrnum.induct) (auto simp add: gr0_conv_Suc)

lemma decr:
  assumes assms: "bound0 p"
  shows "Ifm bbs (x # bs) p = Ifm bbs bs (decr p)"
  using assms by (induct p rule: decr.induct) (simp_all add: gr0_conv_Suc decrnum)

lemma decr_qf: "bound0 p  qfree (decr p)"
  by (induct p) simp_all

fun isatom :: "fm  bool"  ― ‹test for atomicity›
  where
    "isatom T  True"
  | "isatom F  True"
  | "isatom (Lt a)  True"
  | "isatom (Le a)  True"
  | "isatom (Gt a)  True"
  | "isatom (Ge a)  True"
  | "isatom (Eq a)  True"
  | "isatom (NEq a)  True"
  | "isatom (Dvd i b)  True"
  | "isatom (NDvd i b)  True"
  | "isatom (Closed P)  True"
  | "isatom (NClosed P)  True"
  | "isatom p  False"

lemma numsubst0_numbound0:
  assumes "numbound0 t"
  shows "numbound0 (numsubst0 t a)"
  using assms
proof (induct a)
  case (CN n)
  then show ?case by (cases n) simp_all
qed simp_all

lemma subst0_bound0:
  assumes qf: "qfree p"
    and nb: "numbound0 t"
  shows "bound0 (subst0 t p)"
  using qf numsubst0_numbound0[OF nb] by (induct p) auto

lemma bound0_qf: "bound0 p  qfree p"
  by (induct p) simp_all


definition djf :: "('a  fm)  'a  fm  fm"
where
  "djf f p q =
   (if q = T then T
    else if q = F then f p
    else
      let fp = f p
      in case fp of T  T | F  q | _  Or fp q)"

definition evaldjf :: "('a  fm)  'a list  fm"
  where "evaldjf f ps = foldr (djf f) ps F"

lemma djf_Or: "Ifm bbs bs (djf f p q) = Ifm bbs bs (Or (f p) q)"
  by (cases "q=T", simp add: djf_def, cases "q = F", simp add: djf_def)
    (cases "f p", simp_all add: Let_def djf_def)

lemma evaldjf_ex: "Ifm bbs bs (evaldjf f ps)  (p  set ps. Ifm bbs bs (f p))"
  by (induct ps) (simp_all add: evaldjf_def djf_Or)

lemma evaldjf_bound0:
  assumes nb: "x set xs. bound0 (f x)"
  shows "bound0 (evaldjf f xs)"
  using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)

lemma evaldjf_qf:
  assumes nb: "x set xs. qfree (f x)"
  shows "qfree (evaldjf f xs)"
  using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)

fun disjuncts :: "fm  fm list"
  where
    "disjuncts (Or p q) = disjuncts p @ disjuncts q"
  | "disjuncts F = []"
  | "disjuncts p = [p]"

lemma disjuncts: "(q  set (disjuncts p). Ifm bbs bs q)  Ifm bbs bs p"
  by (induct p rule: disjuncts.induct) auto

lemma disjuncts_nb:
  assumes "bound0 p"
  shows "q  set (disjuncts p). bound0 q"
proof -
  from assms have "list_all bound0 (disjuncts p)"
    by (induct p rule: disjuncts.induct) auto
  then show ?thesis
    by (simp only: list_all_iff)
qed

lemma disjuncts_qf:
  assumes "qfree p"
  shows "q  set (disjuncts p). qfree q"
proof -
  from assms have "list_all qfree (disjuncts p)"
    by (induct p rule: disjuncts.induct) auto
  then show ?thesis by (simp only: list_all_iff)
qed

definition DJ :: "(fm  fm)  fm  fm"
  where "DJ f p = evaldjf f (disjuncts p)"

lemma DJ:
  assumes "p q. f (Or p q) = Or (f p) (f q)"
    and "f F = F"
  shows "Ifm bbs bs (DJ f p) = Ifm bbs bs (f p)"
proof -
  have "Ifm bbs bs (DJ f p)  (q  set (disjuncts p). Ifm bbs bs (f q))"
    by (simp add: DJ_def evaldjf_ex)
  also from assms have " = Ifm bbs bs (f p)"
    by (induct p rule: disjuncts.induct) auto
  finally show ?thesis .
qed

lemma DJ_qf:
  assumes "p. qfree p  qfree (f p)"
  shows "p. qfree p  qfree (DJ f p) "
proof clarify
  fix p
  assume qf: "qfree p"
  have th: "DJ f p = evaldjf f (disjuncts p)"
    by (simp add: DJ_def)
  from disjuncts_qf[OF qf] have "q  set (disjuncts p). qfree q" .
  with assms have th': "q  set (disjuncts p). qfree (f q)"
    by blast
  from evaldjf_qf[OF th'] th show "qfree (DJ f p)"
    by simp
qed

lemma DJ_qe:
  assumes qe: "bs p. qfree p  qfree (qe p)  Ifm bbs bs (qe p) = Ifm bbs bs (E p)"
  shows "bs p. qfree p  qfree (DJ qe p)  Ifm bbs bs ((DJ qe p)) = Ifm bbs bs (E p)"
proof clarify
  fix p :: fm
  fix bs
  assume qf: "qfree p"
  from qe have qth: "p. qfree p  qfree (qe p)"
    by blast
  from DJ_qf[OF qth] qf have qfth: "qfree (DJ qe p)"
    by auto
  have "Ifm bbs bs (DJ qe p) = (q set (disjuncts p). Ifm bbs bs (qe q))"
    by (simp add: DJ_def evaldjf_ex)
  also have "  (q  set (disjuncts p). Ifm bbs bs (E q))"
    using qe disjuncts_qf[OF qf] by auto
  also have "  Ifm bbs bs (E p)"
    by (induct p rule: disjuncts.induct) auto
  finally show "qfree (DJ qe p)  Ifm bbs bs (DJ qe p) = Ifm bbs bs (E p)"
    using qfth by blast
qed


subsection ‹Simplification›

text ‹Algebraic simplifications for nums›

fun bnds :: "num  nat list"
  where
    "bnds (Bound n) = [n]"
  | "bnds (CN n c a) = n # bnds a"
  | "bnds (Neg a) = bnds a"
  | "bnds (Add a b) = bnds a @ bnds b"
  | "bnds (Sub a b) = bnds a @ bnds b"
  | "bnds (Mul i a) = bnds a"
  | "bnds a = []"

fun lex_ns:: "nat list  nat list  bool"
  where
    "lex_ns [] ms  True"
  | "lex_ns ns []  False"
  | "lex_ns (n # ns) (m # ms)  n < m  (n = m  lex_ns ns ms)"

definition lex_bnd :: "num  num  bool"
  where "lex_bnd t s = lex_ns (bnds t) (bnds s)"

fun numadd:: "num  num  num"
  where
    "numadd (CN n1 c1 r1) (CN n2 c2 r2) =
      (if n1 = n2 then
         let c = c1 + c2
         in if c = 0 then numadd r1 r2 else CN n1 c (numadd r1 r2)
       else if n1  n2 then CN n1 c1 (numadd r1 (Add (Mul c2 (Bound n2)) r2))
       else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1) r2))"
  | "numadd (CN n1 c1 r1) t = CN n1 c1 (numadd r1 t)"
  | "numadd t (CN n2 c2 r2) = CN n2 c2 (numadd t r2)"
  | "numadd (C b1) (C b2) = C (b1 + b2)"
  | "numadd a b = Add a b"

lemma numadd: "Inum bs (numadd t s) = Inum bs (Add t s)"
  by (induct t s rule: numadd.induct) (simp_all add: Let_def algebra_simps add_eq_0_iff)

lemma numadd_nb: "numbound0 t  numbound0 s  numbound0 (numadd t s)"
  by (induct t s rule: numadd.induct) (simp_all add: Let_def)

fun nummul :: "int  num  num"
  where
    "nummul i (C j) = C (i * j)"
  | "nummul i (CN n c t) = CN n (c * i) (nummul i t)"
  | "nummul i t = Mul i t"

lemma nummul: "Inum bs (nummul i t) = Inum bs (Mul i t)"
  by (induct t arbitrary: i rule: nummul.induct) (simp_all add: algebra_simps)

lemma nummul_nb: "numbound0 t  numbound0 (nummul i t)"
  by (induct t arbitrary: i rule: nummul.induct) (simp_all add: numadd_nb)

definition numneg :: "num  num"
  where "numneg t = nummul (- 1) t"

definition numsub :: "num  num  num"
  where "numsub s t = (if s = t then C 0 else numadd s (numneg t))"

lemma numneg: "Inum bs (numneg t) = Inum bs (Neg t)"
  using numneg_def nummul by simp

lemma numneg_nb: "numbound0 t  numbound0 (numneg t)"
  using numneg_def nummul_nb by simp

lemma numsub: "Inum bs (numsub a b) = Inum bs (Sub a b)"
  using numneg numadd numsub_def by simp

lemma numsub_nb: "numbound0 t  numbound0 s  numbound0 (numsub t s)"
  using numsub_def numadd_nb numneg_nb by simp

fun simpnum :: "num  num"
  where
    "simpnum (C j) = C j"
  | "simpnum (Bound n) = CN n 1 (C 0)"
  | "simpnum (Neg t) = numneg (simpnum t)"
  | "simpnum (Add t s) = numadd (simpnum t) (simpnum s)"
  | "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
  | "simpnum (Mul i t) = (if i = 0 then C 0 else nummul i (simpnum t))"
  | "simpnum t = t"

lemma simpnum_ci: "Inum bs (simpnum t) = Inum bs t"
  by (induct t rule: simpnum.induct) (auto simp add: numneg numadd numsub nummul)

lemma simpnum_numbound0: "numbound0 t  numbound0 (simpnum t)"
  by (induct t rule: simpnum.induct) (auto simp add: numadd_nb numsub_nb nummul_nb numneg_nb)

fun not :: "fm  fm"
  where
    "not (Not p) = p"
  | "not T = F"
  | "not F = T"
  | "not p = Not p"

lemma not: "Ifm bbs bs (not p) = Ifm bbs bs (Not p)"
  by (cases p) auto

lemma not_qf: "qfree p  qfree (not p)"
  by (cases p) auto

lemma not_bn: "bound0 p  bound0 (not p)"
  by (cases p) auto

definition conj :: "fm  fm  fm"
  where "conj p q =
    (if p = F  q = F then F
     else if p = T then q
     else if q = T then p
     else And p q)"

lemma conj: "Ifm bbs bs (conj p q) = Ifm bbs bs (And p q)"
  by (cases "p = F  q = F", simp_all add: conj_def) (cases p, simp_all)

lemma conj_qf: "qfree p  qfree q  qfree (conj p q)"
  using conj_def by auto

lemma conj_nb: "bound0 p  bound0 q  bound0 (conj p q)"
  using conj_def by auto

definition disj :: "fm  fm  fm"
  where "disj p q =
    (if p = T  q = T then T
     else if p = F then q
     else if q = F then p
     else Or p q)"

lemma disj: "Ifm bbs bs (disj p q) = Ifm bbs bs (Or p q)"
  by (cases "p = T  q = T", simp_all add: disj_def) (cases p, simp_all)

lemma disj_qf: "qfree p  qfree q  qfree (disj p q)"
  using disj_def by auto

lemma disj_nb: "bound0 p  bound0 q  bound0 (disj p q)"
  using disj_def by auto

definition imp :: "fm  fm  fm"
  where "imp p q =
    (if p = F  q = T then T
     else if p = T then q
     else if q = F then not p
     else Imp p q)"

lemma imp: "Ifm bbs bs (imp p q) = Ifm bbs bs (Imp p q)"
  by (cases "p = F  q = T", simp_all add: imp_def, cases p) (simp_all add: not)

lemma imp_qf: "qfree p  qfree q  qfree (imp p q)"
  using imp_def by (cases "p = F  q = T", simp_all add: imp_def, cases p) (simp_all add: not_qf)

lemma imp_nb: "bound0 p  bound0 q  bound0 (imp p q)"
  using imp_def by (cases "p = F  q = T", simp_all add: imp_def, cases p) simp_all

definition iff :: "fm  fm  fm"
  where "iff p q =
    (if p = q then T
     else if p = not q  not p = q then F
     else if p = F then not q
     else if q = F then not p
     else if p = T then q
     else if q = T then p
     else Iff p q)"

lemma iff: "Ifm bbs bs (iff p q) = Ifm bbs bs (Iff p q)"
  by (unfold iff_def, cases "p = q", simp, cases "p = not q", simp add: not)
    (cases "not p = q", auto simp add: not)

lemma iff_qf: "qfree p  qfree q  qfree (iff p q)"
  by (unfold iff_def, cases "p = q", auto simp add: not_qf)

lemma iff_nb: "bound0 p  bound0 q  bound0 (iff p q)"
  using iff_def by (unfold iff_def, cases "p = q", auto simp add: not_bn)

fun simpfm :: "fm  fm"
  where
    "simpfm (And p q) = conj (simpfm p) (simpfm q)"
  | "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
  | "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
  | "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
  | "simpfm (Not p) = not (simpfm p)"
  | "simpfm (Lt a) = (let a' = simpnum a in case a' of C v  if v < 0 then T else F | _  Lt a')"
  | "simpfm (Le a) = (let a' = simpnum a in case a' of C v  if v  0 then T else F | _  Le a')"
  | "simpfm (Gt a) = (let a' = simpnum a in case a' of C v  if v > 0 then T else F | _  Gt a')"
  | "simpfm (Ge a) = (let a' = simpnum a in case a' of C v  if v  0 then T else F | _  Ge a')"
  | "simpfm (Eq a) = (let a' = simpnum a in case a' of C v  if v = 0 then T else F | _  Eq a')"
  | "simpfm (NEq a) = (let a' = simpnum a in case a' of C v  if v  0 then T else F | _  NEq a')"
  | "simpfm (Dvd i a) =
      (if i = 0 then simpfm (Eq a)
       else if ¦i¦ = 1 then T
       else let a' = simpnum a in case a' of C v  if i dvd v then T else F | _  Dvd i a')"
  | "simpfm (NDvd i a) =
      (if i = 0 then simpfm (NEq a)
       else if ¦i¦ = 1 then F
       else let a' = simpnum a in case a' of C v  if ¬( i dvd v) then T else F | _  NDvd i a')"
  | "simpfm p = p"

lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p"
proof (induct p rule: simpfm.induct)
  case (6 a)
  let ?sa = "simpnum a"
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
    by simp
  consider v where "?sa = C v" | "¬ (v. ?sa = C v)" by blast
  then show ?case
  proof cases
    case 1
    with sa show ?thesis by simp
  next
    case 2
    with sa show ?thesis by (cases ?sa) (simp_all add: Let_def)
  qed
next
  case (7 a)
  let ?sa = "simpnum a"
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
    by simp
  consider v where "?sa = C v" | "¬ (v. ?sa = C v)" by blast
  then show ?case
  proof cases
    case 1
    with sa show ?thesis by simp
  next
    case 2
    with sa show ?thesis by (cases ?sa) (simp_all add: Let_def)
  qed
next
  case (8 a)
  let ?sa = "simpnum a"
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
    by simp
  consider v where "?sa = C v" | "¬ (v. ?sa = C v)" by blast
  then show ?case
  proof cases
    case 1
    with sa show ?thesis by simp
  next
    case 2
    with sa show ?thesis by (cases ?sa) (simp_all add: Let_def)
  qed
next
  case (9 a)
  let ?sa = "simpnum a"
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
    by simp
  consider v where "?sa = C v" | "¬ (v. ?sa = C v)" by blast
  then show ?case
  proof cases
    case 1
    with sa show ?thesis by simp
  next
    case 2
    with sa show ?thesis by (cases ?sa) (simp_all add: Let_def)
  qed
next
  case (10 a)
  let ?sa = "simpnum a"
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
    by simp
  consider v where "?sa = C v" | "¬ (v. ?sa = C v)" by blast
  then show ?case
  proof cases
    case 1
    with sa show ?thesis by simp
  next
    case 2
    with sa show ?thesis by (cases ?sa) (simp_all add: Let_def)
  qed
next
  case (11 a)
  let ?sa = "simpnum a"
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
    by simp
  consider v where "?sa = C v" | "¬ (v. ?sa = C v)" by blast
  then show ?case
  proof cases
    case 1
    with sa show ?thesis by simp
  next
    case 2
    with sa show ?thesis by (cases ?sa) (simp_all add: Let_def)
  qed
next
  case (12 i a)
  let ?sa = "simpnum a"
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
    by simp
  consider "i = 0" | "¦i¦ = 1" | "i  0" "¦i¦  1" by blast
  then show ?case
  proof cases
    case 1
    then show ?thesis
      using "12.hyps" by (simp add: dvd_def Let_def)
  next
    case 2
    with one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
    show ?thesis
      apply (cases "i = 0")
      apply (simp_all add: Let_def)
      apply (cases "i > 0")
      apply simp_all
      done
  next
    case i: 3
    consider v where "?sa = C v" | "¬ (v. ?sa = C v)" by blast
    then show ?thesis
    proof cases
      case 1
      with sa[symmetric] i show ?thesis
        by (cases "¦i¦ = 1") auto
    next
      case 2
      then have "simpfm (Dvd i a) = Dvd i ?sa"
        using i by (cases ?sa) (auto simp add: Let_def)
      with sa show ?thesis by simp
    qed
  qed
next
  case (13 i a)
  let ?sa = "simpnum a"
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
    by simp
  consider "i = 0" | "¦i¦ = 1" | "i  0" "¦i¦  1" by blast
  then show ?case
  proof cases
    case 1
    then show ?thesis
      using "13.hyps" by (simp add: dvd_def Let_def)
  next
    case 2
    with one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
    show ?thesis
      apply (cases "i = 0")
      apply (simp_all add: Let_def)
      apply (cases "i > 0")
      apply simp_all
      done
  next
    case i: 3
    consider v where "?sa = C v" | "¬ (v. ?sa = C v)" by blast
    then show ?thesis
    proof cases
      case 1
      with sa[symmetric] i show ?thesis
        by (cases "¦i¦ = 1") auto
    next
      case 2
      then have "simpfm (NDvd i a) = NDvd i ?sa"
        using i by (cases ?sa) (auto simp add: Let_def)
      with sa show ?thesis by simp
    qed
  qed
qed (simp_all add: conj disj imp iff not)

lemma simpfm_bound0: "bound0 p  bound0 (simpfm p)"
proof (induct p rule: simpfm.induct)
  case (6 a)
  then have nb: "numbound0 a" by simp
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
next
  case (7 a)
  then have nb: "numbound0 a" by simp
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
next
  case (8 a)
  then have nb: "numbound0 a" by simp
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
next
  case (9 a)
  then have nb: "numbound0 a" by simp
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
next
  case (10 a)
  then have nb: "numbound0 a" by simp
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
next
  case (11 a)
  then have nb: "numbound0 a" by simp
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
next
  case (12 i a)
  then have nb: "numbound0 a" by simp
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
next
  case (13 i a)
  then have nb: "numbound0 a" by simp
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
qed (auto simp add: disj_def imp_def iff_def conj_def not_bn)

lemma simpfm_qf: "qfree p  qfree (simpfm p)"
  apply (induct p rule: simpfm.induct)
  apply (auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def)
  apply (case_tac "simpnum a", auto)+
  done


subsection ‹Generic quantifier elimination›

fun qelim :: "fm  (fm  fm)  fm"
  where
    "qelim (E p) = (λqe. DJ qe (qelim p qe))"
  | "qelim (A p) = (λqe. not (qe ((qelim (Not p) qe))))"
  | "qelim (Not p) = (λqe. not (qelim p qe))"
  | "qelim (And p q) = (λqe. conj (qelim p qe) (qelim q qe))"
  | "qelim (Or  p q) = (λqe. disj (qelim p qe) (qelim q qe))"
  | "qelim (Imp p q) = (λqe. imp (qelim p qe) (qelim q qe))"
  | "qelim (Iff p q) = (λqe. iff (qelim p qe) (qelim q qe))"
  | "qelim p = (λy. simpfm p)"

lemma qelim_ci:
  assumes qe_inv: "bs p. qfree p  qfree (qe p)  Ifm bbs bs (qe p) = Ifm bbs bs (E p)"
  shows "bs. qfree (qelim p qe)  Ifm bbs bs (qelim p qe) = Ifm bbs bs p"
  using qe_inv DJ_qe[OF qe_inv]
  by (induct p rule: qelim.induct)
    (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
      simpfm simpfm_qf simp del: simpfm.simps)

text ‹Linearity for fm where Bound 0 ranges over ℤ›

fun zsplit0 :: "num  int × num"  ― ‹splits the bounded from the unbounded part›
  where
    "zsplit0 (C c) = (0, C c)"
  | "zsplit0 (Bound n) = (if n = 0 then (1, C 0) else (0, Bound n))"
  | "zsplit0 (CN n i a) =
      (let (i', a') =  zsplit0 a
       in if n = 0 then (i + i', a') else (i', CN n i a'))"
  | "zsplit0 (Neg a) = (let (i', a') = zsplit0 a in (-i', Neg a'))"
  | "zsplit0 (Add a b) =
      (let
        (ia, a') = zsplit0 a;
        (ib, b') = zsplit0 b
       in (ia + ib, Add a' b'))"
  | "zsplit0 (Sub a b) =
      (let
        (ia, a') = zsplit0 a;
        (ib, b') = zsplit0 b
       in (ia - ib, Sub a' b'))"
  | "zsplit0 (Mul i a) = (let (i', a') = zsplit0 a in (i*i', Mul i a'))"

lemma zsplit0_I:
  "n a. zsplit0 t = (n, a) 
    (Inum ((x::int) # bs) (CN 0 n a) = Inum (x # bs) t)  numbound0 a"
  (is "n a. ?S t = (n,a)  (?I x (CN 0 n a) = ?I x t)  ?N a")
proof (induct t rule: zsplit0.induct)
  case (1 c n a)
  then show ?case by auto
next
  case (2 m n a)
  then show ?case by (cases "m = 0") auto
next
  case (3 m i a n a')
  let ?j = "fst (zsplit0 a)"
  let ?b = "snd (zsplit0 a)"
  have abj: "zsplit0 a = (?j, ?b)" by simp
  show ?case
  proof (cases "m = 0")
    case False
    with 3(1)[OF abj] 3(2) show ?thesis
      by (auto simp add: Let_def split_def)
  next
    case m: True
    with abj have th: "a' = ?b  n = i + ?j"
      using 3 by (simp add: Let_def split_def)
    from abj 3 m have th2: "(?I x (CN 0 ?j ?b) = ?I x a)  ?N ?b"
      by blast
    from th have "?I x (CN 0 n a') = ?I x (CN 0 (i + ?j) ?b)"
      by simp
    also from th2 have " = ?I x (CN 0 i (CN 0 ?j ?b))"
      by (simp add: distrib_right)
    finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)"
      using th2 by simp
    with th2 th m show ?thesis
      by blast
  qed
next
  case (4 t n a)
  let ?nt = "fst (zsplit0 t)"
  let ?at = "snd (zsplit0 t)"
  have abj: "zsplit0 t = (?nt, ?at)"
    by simp
  then have th: "a = Neg ?at  n = - ?nt"
    using 4 by (simp add: Let_def split_def)
  from abj 4 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t)  ?N ?at"
    by blast
  from th2[simplified] th[simplified] show ?case
    by simp
next
  case (5 s t n a)
  let ?ns = "fst (zsplit0 s)"
  let ?as = "snd (zsplit0 s)"
  let ?nt = "fst (zsplit0 t)"
  let ?at = "snd (zsplit0 t)"
  have abjs: "zsplit0 s = (?ns, ?as)"
    by simp
  moreover have abjt: "zsplit0 t = (?nt, ?at)"
    by simp
  ultimately have th: "a = Add ?as ?at  n = ?ns + ?nt"
    using 5 by (simp add: Let_def split_def)
  from abjs[symmetric] have bluddy: "x y. (x, y) = zsplit0 s"
    by blast
  from 5 have "(x y. (x, y) = zsplit0 s) 
    (xa xb. zsplit0 t = (xa, xb)  Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t  numbound0 xb)"
    by auto
  with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t)  ?N ?at"
    by blast
  from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s)  ?N ?as"
    by blast
  from th3[simplified] th2[simplified] th[simplified] show ?case
    by (simp add: distrib_right)
next
  case (6 s t n a)
  let ?ns = "fst (zsplit0 s)"
  let ?as = "snd (zsplit0 s)"
  let ?nt = "fst (zsplit0 t)"
  let ?at = "snd (zsplit0 t)"
  have abjs: "zsplit0 s = (?ns, ?as)"
    by simp
  moreover have abjt: "zsplit0 t = (?nt, ?at)"
    by simp
  ultimately have th: "a = Sub ?as ?at  n = ?ns - ?nt"
    using 6 by (simp add: Let_def split_def)
  from abjs[symmetric] have bluddy: "x y. (x, y) = zsplit0 s"
    by blast
  from 6 have "(x y. (x,y) = zsplit0 s) 
    (xa xb. zsplit0 t = (xa, xb)  Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t  numbound0 xb)"
    by auto
  with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t)  ?N ?at"
    by blast
  from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s)  ?N ?as"
    by blast
  from th3[simplified] th2[simplified] th[simplified] show ?case
    by (simp add: left_diff_distrib)
next
  case (7 i t n a)
  let ?nt = "fst (zsplit0 t)"
  let ?at = "snd (zsplit0 t)"
  have abj: "zsplit0 t = (?nt,?at)"
    by simp
  then have th: "a = Mul i ?at  n = i * ?nt"
    using 7 by (simp add: Let_def split_def)
  from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t)  ?N ?at"
    by blast
  then have "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)"
    by simp
  also have " = ?I x (CN 0 (i*?nt) (Mul i ?at))"
    by (simp add: distrib_left)
  finally show ?case using th th2
    by simp
qed

fun iszlfm :: "fm  bool"  ― ‹linearity test for fm›
  where
    "iszlfm (And p q)  iszlfm p  iszlfm q"
  | "iszlfm (Or p q)  iszlfm p  iszlfm q"
  | "iszlfm (Eq  (CN 0 c e))  c > 0  numbound0 e"
  | "iszlfm (NEq (CN 0 c e))  c > 0  numbound0 e"
  | "iszlfm (Lt  (CN 0 c e))  c > 0  numbound0 e"
  | "iszlfm (Le  (CN 0 c e))  c > 0  numbound0 e"
  | "iszlfm (Gt  (CN 0 c e))  c > 0  numbound0 e"
  | "iszlfm (Ge  (CN 0 c e))  c > 0  numbound0 e"
  | "iszlfm (Dvd i (CN 0 c e))  c > 0  i > 0  numbound0 e"
  | "iszlfm (NDvd i (CN 0 c e))<