(* Title: HOL/Decision_Procs/Cooper.thy
Author: Amine Chaieb
*)
section \<open>Presburger arithmetic based on Cooper's algorithm\<close>
theory Cooper
imports
Complex_Main
"HOL-Library.Code_Target_Numeral"
begin
subsection \<open>Basic formulae\<close>
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 \<open>Boundedness and substitution\<close>
primrec numbound0 :: "num \ bool" \ \a \num\ is \<^emph>\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 \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) 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 \<open>Simplification\<close>
text \<open>Algebraic simplifications for nums\<close>
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 \<le> 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 \<or> 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 \<or> 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 \<or> 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 \<or> 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 \<bar>i\<bar> = 1 then T
else let a' = simpnum a in case a' of C v \<Rightarrow> if i dvd v then T else F | _ \<Rightarrow> Dvd i a')"
| "simpfm (NDvd i a) =
(if i = 0 then simpfm (NEq a)
else if \<bar>i\<bar> = 1 then F
else let a' = simpnum a in case a' of C v \<Rightarrow> if \<not>( i dvd v) then T else F | _ \<Rightarrow> 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 \<open>Generic quantifier elimination\<close>
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 \<open>Linearity for fm where Bound 0 ranges over \<open>\<int>\<close>\<close>
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) \<and> 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) \
(\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> 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) \
(\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> 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)) \ c > 0 \ i > 0 \ numbound0 e"
| "iszlfm p \ isatom p \ bound0 p"
lemma zlin_qfree: "iszlfm p \ qfree p"
by (induct p rule: iszlfm.induct) auto
fun zlfm :: "fm \ fm" \ \linearity transformation for fm\
where
"zlfm (And p q) = And (zlfm p) (zlfm q)"
| "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
| "zlfm (Imp p q) = Or (zlfm (NOT p)) (zlfm q)"
| "zlfm (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))"
| "zlfm (Lt a) =
(let (c, r) = zsplit0 a in
if c = 0 then Lt r else
if c > 0 then (Lt (CN 0 c r))
else Gt (CN 0 (- c) (Neg r)))"
| "zlfm (Le a) =
(let (c, r) = zsplit0 a in
if c = 0 then Le r
else if c > 0 then Le (CN 0 c r)
else Ge (CN 0 (- c) (Neg r)))"
| "zlfm (Gt a) =
(let (c, r) = zsplit0 a in
if c = 0 then Gt r else
if c > 0 then Gt (CN 0 c r)
else Lt (CN 0 (- c) (Neg r)))"
| "zlfm (Ge a) =
(let (c, r) = zsplit0 a in
if c = 0 then Ge r
else if c > 0 then Ge (CN 0 c r)
else Le (CN 0 (- c) (Neg r)))"
| "zlfm (Eq a) =
(let (c, r) = zsplit0 a in
if c = 0 then Eq r
else if c > 0 then Eq (CN 0 c r)
else Eq (CN 0 (- c) (Neg r)))"
| "zlfm (NEq a) =
(let (c, r) = zsplit0 a in
if c = 0 then NEq r
else if c > 0 then NEq (CN 0 c r)
else NEq (CN 0 (- c) (Neg r)))"
| "zlfm (Dvd i a) =
(if i = 0 then zlfm (Eq a)
else
let (c, r) = zsplit0 a in
if c = 0 then Dvd \<bar>i\<bar> r
else if c > 0 then Dvd \<bar>i\<bar> (CN 0 c r)
else Dvd \<bar>i\<bar> (CN 0 (- c) (Neg r)))"
| "zlfm (NDvd i a) =
(if i = 0 then zlfm (NEq a)
else
let (c, r) = zsplit0 a in
if c = 0 then NDvd \<bar>i\<bar> r
else if c > 0 then NDvd \<bar>i\<bar> (CN 0 c r)
else NDvd \<bar>i\<bar> (CN 0 (- c) (Neg r)))"
| "zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))"
| "zlfm (NOT (Or p q)) = And (zlfm (NOT p)) (zlfm (NOT q))"
| "zlfm (NOT (Imp p q)) = And (zlfm p) (zlfm (NOT q))"
| "zlfm (NOT (Iff p q)) = Or (And(zlfm p) (zlfm(NOT q))) (And (zlfm(NOT p)) (zlfm q))"
| "zlfm (NOT (NOT p)) = zlfm p"
| "zlfm (NOT T) = F"
| "zlfm (NOT F) = T"
| "zlfm (NOT (Lt a)) = zlfm (Ge a)"
| "zlfm (NOT (Le a)) = zlfm (Gt a)"
| "zlfm (NOT (Gt a)) = zlfm (Le a)"
| "zlfm (NOT (Ge a)) = zlfm (Lt a)"
| "zlfm (NOT (Eq a)) = zlfm (NEq a)"
| "zlfm (NOT (NEq a)) = zlfm (Eq a)"
| "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"
| "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"
| "zlfm (NOT (Closed P)) = NClosed P"
| "zlfm (NOT (NClosed P)) = Closed P"
| "zlfm p = p"
lemma zlfm_I:
assumes qfp: "qfree p"
shows "Ifm bbs (i # bs) (zlfm p) = Ifm bbs (i # bs) p \ iszlfm (zlfm p)"
(is "?I (?l p) = ?I p \ ?L (?l p)")
using qfp
proof (induct p rule: zlfm.induct)
case (5 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c, ?r)"
by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
let ?N = "\t. Inum (i # bs) t"
from 5 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r")
apply auto
subgoal for nat a b by (cases nat) auto
done
next
case (6 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c, ?r)"
by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
let ?N = "\t. Inum (i # bs) t"
from 6 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r")
apply auto
subgoal for nat a b by (cases nat) auto
done
next
case (7 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c, ?r)"
by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
let ?N = "\t. Inum (i # bs) t"
from 7 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r")
apply auto
subgoal for nat a b by (cases nat) auto
done
next
case (8 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c, ?r)"
by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
let ?N = "\t. Inum (i # bs) t"
from 8 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r")
apply auto
subgoal for nat a b by (cases nat) auto
done
next
case (9 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c, ?r)"
by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
let ?N = "\t. Inum (i # bs) t"
from 9 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r")
apply auto
subgoal for nat a b by (cases nat) auto
done
next
case (10 a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c, ?r)"
by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
let ?N = "\t. Inum (i # bs) t"
from 10 Ia nb show ?case
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r")
apply auto
subgoal for nat a b by (cases nat) auto
done
next
case (11 j a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c,?r)"
by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
let ?N = "\t. Inum (i#bs) t"
consider "j = 0" | "j \ 0" "?c = 0" | "j \ 0" "?c > 0" | "j \ 0" "?c < 0"
by arith
then show ?case
proof cases
case 1
then have z: "zlfm (Dvd j a) = (zlfm (Eq a))"
by (simp add: Let_def)
with 11 \<open>j = 0\<close> show ?thesis
by (simp del: zlfm.simps)
next
case 2
with zsplit0_I[OF spl, where x="i" and bs="bs"] show ?thesis
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r")
apply auto
subgoal for nat a b by (cases nat) auto
done
next
case 3
then have l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
with Ia 3 show ?thesis
by (simp add: Let_def split_def)
next
case 4
then have l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
with Ia 4 dvd_minus_iff[of "\j\" "?c*i + ?N ?r"] show ?thesis
by (simp add: Let_def split_def)
qed
next
case (12 j a)
let ?c = "fst (zsplit0 a)"
let ?r = "snd (zsplit0 a)"
have spl: "zsplit0 a = (?c, ?r)"
by simp
from zsplit0_I[OF spl, where x="i" and bs="bs"]
have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
by auto
let ?N = "\t. Inum (i # bs) t"
consider "j = 0" | "j \ 0" "?c = 0" | "j \ 0" "?c > 0" | "j \ 0" "?c < 0"
by arith
then show ?case
proof cases
case 1
then have z: "zlfm (NDvd j a) = zlfm (NEq a)"
by (simp add: Let_def)
with assms 12 \<open>j = 0\<close> show ?thesis
by (simp del: zlfm.simps)
next
case 2
with zsplit0_I[OF spl, where x="i" and bs="bs"] show ?thesis
apply (auto simp add: Let_def split_def algebra_simps)
apply (cases "?r")
apply auto
subgoal for nat a b by (cases nat) auto
done
next
case 3
then have l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
with Ia 3 show ?thesis
by (simp add: Let_def split_def)
next
case 4
then have l: "?L (?l (Dvd j a))"
by (simp add: nb Let_def split_def)
with Ia 4 dvd_minus_iff[of "\j\" "?c*i + ?N ?r"] show ?thesis
by (simp add: Let_def split_def)
qed
qed auto
fun minusinf :: "fm \ fm" \ \virtual substitution of \-\\\
where
"minusinf (And p q) = And (minusinf p) (minusinf q)"
| "minusinf (Or p q) = Or (minusinf p) (minusinf q)"
| "minusinf (Eq (CN 0 c e)) = F"
| "minusinf (NEq (CN 0 c e)) = T"
| "minusinf (Lt (CN 0 c e)) = T"
| "minusinf (Le (CN 0 c e)) = T"
| "minusinf (Gt (CN 0 c e)) = F"
| "minusinf (Ge (CN 0 c e)) = F"
| "minusinf p = p"
lemma minusinf_qfree: "qfree p \ qfree (minusinf p)"
by (induct p rule: minusinf.induct) auto
fun plusinf :: "fm \ fm" \ \virtual substitution of \+\\\
where
"plusinf (And p q) = And (plusinf p) (plusinf q)"
| "plusinf (Or p q) = Or (plusinf p) (plusinf q)"
| "plusinf (Eq (CN 0 c e)) = F"
| "plusinf (NEq (CN 0 c e)) = T"
| "plusinf (Lt (CN 0 c e)) = F"
| "plusinf (Le (CN 0 c e)) = F"
| "plusinf (Gt (CN 0 c e)) = T"
| "plusinf (Ge (CN 0 c e)) = T"
| "plusinf p = p"
fun \<delta> :: "fm \<Rightarrow> int" \<comment> \<open>compute \<open>lcm {d| N\<^sup>? Dvd c*x+t \<in> p}\<close>\<close>
where
"\ (And p q) = lcm (\ p) (\ q)"
| "\ (Or p q) = lcm (\ p) (\ q)"
| "\ (Dvd i (CN 0 c e)) = i"
| "\ (NDvd i (CN 0 c e)) = i"
| "\ p = 1"
fun d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" \<comment> \<open>check if a given \<open>l\<close> divides all the \<open>ds\<close> above\<close>
where
"d_\ (And p q) d \ d_\ p d \ d_\ q d"
| "d_\ (Or p q) d \ d_\ p d \ d_\ q d"
| "d_\ (Dvd i (CN 0 c e)) d \ i dvd d"
| "d_\ (NDvd i (CN 0 c e)) d \ i dvd d"
| "d_\ p d \ True"
lemma delta_mono:
assumes lin: "iszlfm p"
and d: "d dvd d'"
and ad: "d_\ p d"
shows "d_\ p d'"
using lin ad
proof (induct p rule: iszlfm.induct)
case (9 i c e)
then show ?case using d
by (simp add: dvd_trans[of "i" "d" "d'"])
next
case (10 i c e)
then show ?case using d
by (simp add: dvd_trans[of "i" "d" "d'"])
qed simp_all
lemma \<delta>:
assumes lin: "iszlfm p"
shows "d_\ p (\ p) \ \ p >0"
using lin
by (induct p rule: iszlfm.induct) (auto intro: delta_mono simp add: lcm_pos_int)
fun a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" \<comment> \<open>adjust the coefficients of a formula\<close>
where
"a_\ (And p q) k = And (a_\ p k) (a_\ q k)"
| "a_\ (Or p q) k = Or (a_\ p k) (a_\ q k)"
| "a_\ (Eq (CN 0 c e)) k = Eq (CN 0 1 (Mul (k div c) e))"
| "a_\ (NEq (CN 0 c e)) k = NEq (CN 0 1 (Mul (k div c) e))"
| "a_\ (Lt (CN 0 c e)) k = Lt (CN 0 1 (Mul (k div c) e))"
| "a_\ (Le (CN 0 c e)) k = Le (CN 0 1 (Mul (k div c) e))"
| "a_\ (Gt (CN 0 c e)) k = Gt (CN 0 1 (Mul (k div c) e))"
| "a_\ (Ge (CN 0 c e)) k = Ge (CN 0 1 (Mul (k div c) e))"
| "a_\ (Dvd i (CN 0 c e)) k = Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e))"
| "a_\ (NDvd i (CN 0 c e)) k = NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e))"
| "a_\ p k = p"
fun d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" \<comment> \<open>test if all coeffs of \<open>c\<close> divide a given \<open>l\<close>\<close>
where
"d_\ (And p q) k \ d_\ p k \ d_\ q k"
| "d_\ (Or p q) k \ d_\ p k \ d_\ q k"
| "d_\ (Eq (CN 0 c e)) k \ c dvd k"
| "d_\ (NEq (CN 0 c e)) k \ c dvd k"
| "d_\ (Lt (CN 0 c e)) k \ c dvd k"
| "d_\ (Le (CN 0 c e)) k \ c dvd k"
| "d_\ (Gt (CN 0 c e)) k \ c dvd k"
| "d_\ (Ge (CN 0 c e)) k \ c dvd k"
| "d_\ (Dvd i (CN 0 c e)) k \ c dvd k"
| "d_\ (NDvd i (CN 0 c e)) k \ c dvd k"
| "d_\ p k \ True"
fun \<zeta> :: "fm \<Rightarrow> int" \<comment> \<open>computes the lcm of all coefficients of \<open>x\<close>\<close>
where
"\ (And p q) = lcm (\ p) (\ q)"
| "\ (Or p q) = lcm (\ p) (\ q)"
| "\ (Eq (CN 0 c e)) = c"
| "\ (NEq (CN 0 c e)) = c"
| "\ (Lt (CN 0 c e)) = c"
| "\ (Le (CN 0 c e)) = c"
| "\ (Gt (CN 0 c e)) = c"
| "\ (Ge (CN 0 c e)) = c"
| "\ (Dvd i (CN 0 c e)) = c"
| "\ (NDvd i (CN 0 c e))= c"
| "\ p = 1"
fun \<beta> :: "fm \<Rightarrow> num list"
where
"\ (And p q) = (\ p @ \ q)"
| "\ (Or p q) = (\ p @ \ q)"
| "\ (Eq (CN 0 c e)) = [Sub (C (- 1)) e]"
| "\ (NEq (CN 0 c e)) = [Neg e]"
| "\ (Lt (CN 0 c e)) = []"
| "\ (Le (CN 0 c e)) = []"
| "\ (Gt (CN 0 c e)) = [Neg e]"
| "\ (Ge (CN 0 c e)) = [Sub (C (- 1)) e]"
| "\ p = []"
fun \<alpha> :: "fm \<Rightarrow> num list"
where
"\ (And p q) = \ p @ \ q"
| "\ (Or p q) = \ p @ \ q"
| "\ (Eq (CN 0 c e)) = [Add (C (- 1)) e]"
| "\ (NEq (CN 0 c e)) = [e]"
| "\ (Lt (CN 0 c e)) = [e]"
| "\ (Le (CN 0 c e)) = [Add (C (- 1)) e]"
| "\ (Gt (CN 0 c e)) = []"
| "\ (Ge (CN 0 c e)) = []"
| "\ p = []"
fun mirror :: "fm \ fm"
where
"mirror (And p q) = And (mirror p) (mirror q)"
| "mirror (Or p q) = Or (mirror p) (mirror q)"
| "mirror (Eq (CN 0 c e)) = Eq (CN 0 c (Neg e))"
| "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"
| "mirror (Lt (CN 0 c e)) = Gt (CN 0 c (Neg e))"
| "mirror (Le (CN 0 c e)) = Ge (CN 0 c (Neg e))"
| "mirror (Gt (CN 0 c e)) = Lt (CN 0 c (Neg e))"
| "mirror (Ge (CN 0 c e)) = Le (CN 0 c (Neg e))"
| "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
| "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
| "mirror p = p"
text \<open>Lemmas for the correctness of \<open>\<sigma>_\<rho>\<close>\<close>
lemma dvd1_eq1: "x > 0 \ x dvd 1 \ x = 1"
for x :: int
by simp
lemma minusinf_inf:
assumes linp: "iszlfm p"
and u: "d_\ p 1"
shows "\z::int. \x < z. Ifm bbs (x # bs) (minusinf p) = Ifm bbs (x # bs) p"
(is "?P p" is "\(z::int). \x < z. ?I x (?M p) = ?I x p")
using linp u
proof (induct p rule: minusinf.induct)
case (1 p q)
then show ?case
apply auto
subgoal for z z' by (rule exI [where x = "min z z'"]) simp
done
next
case (2 p q)
then show ?case
apply auto
subgoal for z z' by (rule exI [where x = "min z z'"]) simp
done
next
case (3 c e)
then have c1: "c = 1" and nb: "numbound0 e"
by simp_all
fix a
from 3 have "\x<(- Inum (a # bs) e). c * x + Inum (x # bs) e \ 0"
proof clarsimp
fix x
assume "x < (- Inum (a # bs) e)" and "x + Inum (x # bs) e = 0"
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
show False by simp
qed
then show ?case by auto
next
case (4 c e)
then have c1: "c = 1" and nb: "numbound0 e"
by simp_all
fix a
from 4 have "\x < (- Inum (a # bs) e). c * x + Inum (x # bs) e \ 0"
proof clarsimp
fix x
assume "x < (- Inum (a # bs) e)" and "x + Inum (x # bs) e = 0"
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
show "False" by simp
qed
then show ?case by auto
next
case (5 c e)
then have c1: "c = 1" and nb: "numbound0 e"
by simp_all
fix a
from 5 have "\x<(- Inum (a # bs) e). c * x + Inum (x # bs) e < 0"
proof clarsimp
fix x
assume "x < (- Inum (a # bs) e)"
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
show "x + Inum (x # bs) e < 0"
by simp
qed
then show ?case by auto
next
case (6 c e)
then have c1: "c = 1" and nb: "numbound0 e"
by simp_all
fix a
from 6 have "\x<(- Inum (a # bs) e). c * x + Inum (x # bs) e \ 0"
proof clarsimp
fix x
assume "x < (- Inum (a # bs) e)"
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
show "x + Inum (x # bs) e \ 0" by simp
qed
then show ?case by auto
next
case (7 c e)
then have c1: "c = 1" and nb: "numbound0 e"
by simp_all
fix a
from 7 have "\x<(- Inum (a # bs) e). \ (c * x + Inum (x # bs) e > 0)"
proof clarsimp
fix x
assume "x < - Inum (a # bs) e" and "x + Inum (x # bs) e > 0"
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
show False by simp
qed
then show ?case by auto
next
case (8 c e)
then have c1: "c = 1" and nb: "numbound0 e"
by simp_all
fix a
from 8 have "\x<(- Inum (a # bs) e). \ c * x + Inum (x # bs) e \ 0"
proof clarsimp
fix x
assume "x < (- Inum (a # bs) e)" and "x + Inum (x # bs) e \ 0"
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
show False by simp
qed
then show ?case by auto
qed auto
lemma minusinf_repeats:
assumes d: "d_\ p d"
and linp: "iszlfm p"
shows "Ifm bbs ((x - k * d) # bs) (minusinf p) = Ifm bbs (x # bs) (minusinf p)"
using linp d
proof (induct p rule: iszlfm.induct)
case (9 i c e)
then have nbe: "numbound0 e" and id: "i dvd d"
by simp_all
then have "\k. d = i * k"
by (simp add: dvd_def)
then obtain "di" where di_def: "d = i * di"
by blast
show ?case
proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib,
rule iffI)
assume "i dvd c * x - c * (k * d) + Inum (x # bs) e"
(is "?ri dvd ?rc * ?rx - ?rc * (?rk * ?rd) + ?I x e" is "?ri dvd ?rt")
then have "\l::int. ?rt = i * l"
by (simp add: dvd_def)
then have "\l::int. c * x + ?I x e = i * l + c * (k * i * di)"
by (simp add: algebra_simps di_def)
then have "\l::int. c * x + ?I x e = i* (l + c * k * di)"
by (simp add: algebra_simps)
then have "\l::int. c * x + ?I x e = i * l"
by blast
then show "i dvd c * x + Inum (x # bs) e"
by (simp add: dvd_def)
next
assume "i dvd c * x + Inum (x # bs) e" (is "?ri dvd ?rc * ?rx + ?e")
then have "\l::int. c * x + ?e = i * l"
by (simp add: dvd_def)
then have "\l::int. c * x - c * (k * d) + ?e = i * l - c * (k * d)"
by simp
then have "\l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)"
by (simp add: di_def)
then have "\l::int. c * x - c * (k * d) + ?e = i * (l - c * k * di)"
by (simp add: algebra_simps)
then have "\l::int. c * x - c * (k * d) + ?e = i * l"
by blast
then show "i dvd c * x - c * (k * d) + Inum (x # bs) e"
by (simp add: dvd_def)
qed
next
case (10 i c e)
then have nbe: "numbound0 e" and id: "i dvd d"
by simp_all
then have "\k. d = i * k"
by (simp add: dvd_def)
then obtain di where di_def: "d = i * di"
by blast
show ?case
proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib,
rule iffI)
assume "i dvd c * x - c * (k * d) + Inum (x # bs) e"
(is "?ri dvd ?rc * ?rx - ?rc * (?rk * ?rd) + ?I x e" is "?ri dvd ?rt")
then have "\l::int. ?rt = i * l"
by (simp add: dvd_def)
then have "\l::int. c * x + ?I x e = i * l + c * (k * i * di)"
by (simp add: algebra_simps di_def)
then have "\l::int. c * x+ ?I x e = i * (l + c * k * di)"
by (simp add: algebra_simps)
then have "\l::int. c * x + ?I x e = i * l"
by blast
then show "i dvd c * x + Inum (x # bs) e"
by (simp add: dvd_def)
next
assume "i dvd c * x + Inum (x # bs) e" (is "?ri dvd ?rc * ?rx + ?e")
then have "\l::int. c * x + ?e = i * l"
by (simp add: dvd_def)
then have "\l::int. c * x - c * (k * d) + ?e = i * l - c * (k * d)"
by simp
then have "\l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)"
by (simp add: di_def)
then have "\l::int. c * x - c * (k * d) + ?e = i * (l - c * k * di)"
by (simp add: algebra_simps)
then have "\l::int. c * x - c * (k * d) + ?e = i * l"
by blast
then show "i dvd c * x - c * (k * d) + Inum (x # bs) e"
by (simp add: dvd_def)
qed
qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"])
lemma mirror_\<alpha>_\<beta>:
assumes lp: "iszlfm p"
shows "Inum (i # bs) ` set (\ p) = Inum (i # bs) ` set (\ (mirror p))"
using lp by (induct p rule: mirror.induct) auto
lemma mirror:
assumes lp: "iszlfm p"
shows "Ifm bbs (x # bs) (mirror p) = Ifm bbs ((- x) # bs) p"
using lp
proof (induct p rule: iszlfm.induct)
case (9 j c e)
then have nb: "numbound0 e"
by simp
have "Ifm bbs (x # bs) (mirror (Dvd j (CN 0 c e))) \ j dvd c * x - Inum (x # bs) e"
(is "_ = (j dvd c*x - ?e)") by simp
also have "\ \ j dvd (- (c * x - ?e))"
by (simp only: dvd_minus_iff)
also have "\ \ j dvd (c * (- x)) + ?e"
by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] ac_simps minus_add_distrib)
(simp add: algebra_simps)
also have "\ = Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
finally show ?case .
next
case (10 j c e)
then have nb: "numbound0 e"
by simp
have "Ifm bbs (x # bs) (mirror (Dvd j (CN 0 c e))) \ j dvd c * x - Inum (x # bs) e"
(is "_ = (j dvd c * x - ?e)") by simp
also have "\ \ j dvd (- (c * x - ?e))"
by (simp only: dvd_minus_iff)
also have "\ \ j dvd (c * (- x)) + ?e"
by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] ac_simps minus_add_distrib)
(simp add: algebra_simps)
also have "\ \ Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
finally show ?case by simp
qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] gr0_conv_Suc)
lemma mirror_l: "iszlfm p \ d_\ p 1 \ iszlfm (mirror p) \ d_\ (mirror p) 1"
by (induct p rule: mirror.induct) auto
lemma mirror_\<delta>: "iszlfm p \<Longrightarrow> \<delta> (mirror p) = \<delta> p"
by (induct p rule: mirror.induct) auto
lemma \<beta>_numbound0:
assumes lp: "iszlfm p"
shows "\b \ set (\ p). numbound0 b"
using lp by (induct p rule: \<beta>.induct) auto
lemma d_\<beta>_mono:
assumes linp: "iszlfm p"
and dr: "d_\ p l"
and d: "l dvd l'"
shows "d_\ p l'"
using dr linp dvd_trans[of _ "l" "l'", simplified d]
by (induct p rule: iszlfm.induct) simp_all
lemma \<alpha>_l:
assumes "iszlfm p"
shows "\b \ set (\ p). numbound0 b"
using assms by (induct p rule: \<alpha>.induct) auto
lemma \<zeta>:
assumes "iszlfm p"
shows "\ p > 0 \ d_\ p (\ p)"
using assms
proof (induct p rule: iszlfm.induct)
case (1 p q)
from 1 have dl1: "\ p dvd lcm (\ p) (\ q)"
by simp
from 1 have dl2: "\ q dvd lcm (\ p) (\ q)"
by simp
from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
dl1 dl2
show ?case
by (auto simp add: lcm_pos_int)
next
case (2 p q)
from 2 have dl1: "\ p dvd lcm (\ p) (\ q)"
by simp
from 2 have dl2: "\ q dvd lcm (\ p) (\ q)"
by simp
from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
dl1 dl2
show ?case
by (auto simp add: lcm_pos_int)
qed (auto simp add: lcm_pos_int)
lemma a_\<beta>:
assumes linp: "iszlfm p"
and d: "d_\ p l"
and lp: "l > 0"
shows "iszlfm (a_\ p l) \ d_\ (a_\ p l) 1 \ Ifm bbs (l * x # bs) (a_\ p l) = Ifm bbs (x # bs) p"
using linp d
proof (induct p rule: iszlfm.induct)
case (5 c e)
then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
by simp_all
from lp cp have clel: "c \ l"
by (simp add: zdvd_imp_le [OF d' lp])
from cp have cnz: "c \ 0"
by simp
have "c div c \ l div c"
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp: "0 < l div c"
by (simp add: div_self[OF cnz])
have "c * (l div c) = c * (l div c) + l mod c"
using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
then have cl: "c * (l div c) =l"
using mult_div_mod_eq [where a="l" and b="c"] by simp
then have "(l * x + (l div c) * Inum (x # bs) e < 0) \
((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
by simp
also have "\ \ (l div c) * (c * x + Inum (x # bs) e) < (l div c) * 0"
by (simp add: algebra_simps)
also have "\ \ c * x + Inum (x # bs) e < 0"
using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp
by simp
finally show ?case
using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be
by simp
next
case (6 c e)
then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
by simp_all
from lp cp have clel: "c \ l"
by (simp add: zdvd_imp_le [OF d' lp])
from cp have cnz: "c \ 0"
by simp
have "c div c \ l div c"
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp:"0 < l div c"
by (simp add: div_self[OF cnz])
have "c * (l div c) = c * (l div c) + l mod c"
using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
then have cl: "c * (l div c) = l"
using mult_div_mod_eq [where a="l" and b="c"] by simp
then have "l * x + (l div c) * Inum (x # bs) e \ 0 \
(c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0"
by simp
also have "\ \ (l div c) * (c * x + Inum (x # bs) e) \ (l div c) * 0"
by (simp add: algebra_simps)
also have "\ \ c * x + Inum (x # bs) e \ 0"
using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
finally show ?case
using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
next
case (7 c e)
then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
by simp_all
from lp cp have clel: "c \ l"
by (simp add: zdvd_imp_le [OF d' lp])
from cp have cnz: "c \ 0"
by simp
have "c div c \ l div c"
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp: "0 < l div c"
by (simp add: div_self[OF cnz])
have "c * (l div c) = c * (l div c) + l mod c"
using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
then have cl: "c * (l div c) = l"
using mult_div_mod_eq [where a="l" and b="c"] by simp
then have "l * x + (l div c) * Inum (x # bs) e > 0 \
(c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0"
by simp
also have "\ \ (l div c) * (c * x + Inum (x # bs) e) > (l div c) * 0"
by (simp add: algebra_simps)
also have "\ \ c * x + Inum (x # bs) e > 0"
using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
by simp
finally show ?case
using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
by simp
next
case (8 c e)
then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
by simp_all
from lp cp have clel: "c \ l"
by (simp add: zdvd_imp_le [OF d' lp])
from cp have cnz: "c \ 0"
by simp
have "c div c \ l div c"
by (simp add: zdiv_mono1[OF clel cp])
then have ldcp: "0 < l div c"
by (simp add: div_self[OF cnz])
have "c * (l div c) = c * (l div c) + l mod c"
using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
then have cl: "c * (l div c) =l"
using mult_div_mod_eq [where a="l" and b="c"]
by simp
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.83 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
