# 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 (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))"
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)"
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))"
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)"

lemma numadd_nb: "numbound0 t ⟹ numbound0 s ⟹ numbound0 (numadd t s)"

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

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 (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 (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 (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))"
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
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
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))"
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))<```