(* Title: HOL/Decision_Procs/Cooper.thy Author: Amine Chaieb *) theory Cooper imports Complex_Main "HOL-Library.Code_Target_Numeral" begin section ‹Periodicity of ‹dvd›› subsection ‹Shadow syntax and semantics› 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" text ‹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 (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 text ‹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 text ‹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)) ⟷ 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 ¦i¦ r else if c > 0 then Dvd ¦i¦ (CN 0 c r) else Dvd ¦i¦ (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 ¦i¦ r else if c > 0 then NDvd ¦i¦ (CN 0 c r) else NDvd ¦i¦ (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 ‹j = 0› 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 ‹j = 0› 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 δ :: "fm ⇒ int" ― ‹compute ‹lcm {d| N⇧^{?}Dvd c*x+t ∈ p}›› 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_δ :: "fm ⇒ int ⇒ bool" ― ‹check if a given ‹l› divides all the ‹ds› above› 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 δ: 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_β :: "fm ⇒ int ⇒ fm" ― ‹adjust the coefficients of a formula› 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_β :: "fm ⇒ int ⇒ bool" ― ‹test if all coeffs of ‹c› divide a given ‹l›› 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 ζ :: "fm ⇒ int" ― ‹computes the lcm of all coefficients of ‹x›› 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 β :: "fm ⇒ 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 α :: "fm ⇒ 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 ‹Lemmas for the correctness of ‹σ_ρ›› 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_α_β: 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_δ: "iszlfm p ⟹ δ (mirror p) = δ p" by (induct p rule: mirror.induct) auto lemma β_numbound0: assumes lp: "iszlfm p" shows "∀b ∈ set (β p). numbound0 b" using lp by (induct p rule: β.induct) auto lemma d_β_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 α_l: assumes "iszlfm p" shows "∀b ∈ set (α p). numbound0 b" using assms by (induct p rule: α.induct) auto lemma ζ: 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_β_mono[where p = "p" and l="ζ p" and l'="lcm (ζ p) (ζ q)"] d_β_mono[where p = "q" and l="ζ q" and l'="lcm (ζ p) (ζ 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_β_mono[where p = "p" and l="ζ p" and l'="lcm (ζ p) (ζ q)"] d_β_mono[where p = "q" and l="ζ q" and l'="lcm (ζ p) (ζ q)"] dl1 dl2 show ?case by (auto simp add: lcm_pos_int) qed (auto simp add: lcm_pos_int) lemma a_β: 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 ≤ 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 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 ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"] by simp finally show ?case using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] by simp next case (3 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_eq_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 (4 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_le_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 (9 j c e) then have cp: "c > 0" and be: "numbound0 e" and jp: "j > 0" 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 "(∃k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) ⟷ (∃k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp also have "… ⟷ (∃k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)" by (simp add: algebra_simps) also have "… ⟷ (∃k::int. c * x + Inum (x # bs) e - j * k = 0)" using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k" for k] ldcp by simp also have "… ⟷ (∃k::int. c * x + Inum (x # bs) e = j * k)" by simp finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be mult_strict_mono[OF ldcp jp ldcp ] by (simp add: dvd_def) next case (10 j c e) then have cp: "c > 0" and be: "numbound0 e" and jp: "j > 0" 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 "(∃k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) ⟷ (∃k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp also have "… ⟷ (∃k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)" by (simp add: algebra_simps) also have "… ⟷ (∃k::int. c * x + Inum (x # bs) e - j * k = 0)" using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k" for k] ldcp by simp also have "… ⟷ (∃k::int. c * x + Inum (x # bs) e = j * k)" by simp finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be mult_strict_mono[OF ldcp jp ldcp ] by (simp add: dvd_def) qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="(l * x)" and b'="x"]) lemma a_β_ex: assumes linp: "iszlfm p" and d: "d_β p l" and lp: "l > 0" shows "(∃x. l dvd x ∧ Ifm bbs (x #bs) (a_β p l)) ⟷ (∃x::int. Ifm bbs (x#bs) p)" (is "(∃x. l dvd x ∧ ?P x) ⟷ (∃x. ?P' x)") proof- have "(∃x. l dvd x ∧ ?P x) ⟷ (∃x::int. ?P (l * x))" using unity_coeff_ex[where l="l" and P="?P", simplified] by simp also have "… = (∃x::int. ?P' x)" using a_β[OF linp d lp] by simp finally show ?thesis . qed lemma β: assumes "iszlfm p" and "d_β p 1" and "d_δ p d" and dp: "d > 0" and "¬ (∃j::int ∈ {1 .. d}. ∃b ∈ Inum (a # bs) ` set (β p). x = b + j)" and p: "Ifm bbs (x # bs) p" (is "?P x") shows "?P (x - d)" using assms proof (induct p rule: iszlfm.induct) case (5 c e) then have c1: "c = 1" and bn: "numbound0 e" by simp_all with dp p c1 numbound0_I[OF bn,where b = "(x - d)" and b' = "x" and bs = "bs"] 5 show ?case by simp next case (6 c e) then have c1: "c = 1" and bn: "numbound0 e" by simp_all with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 6 show ?case by simp next case (7 c e) then have p: "Ifm bbs (x # bs) (Gt (CN 0 c e))" and c1: "c=1" and bn: "numbound0 e" by simp_all let ?e = "Inum (x # bs) e" show ?case proof (cases "(x - d) + ?e > 0") case True then show ?thesis using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp next case False let ?v = "Neg e" have vb: "?v ∈ set (β (Gt (CN 0 c e)))" by simp from 7(5)[simplified simp_thms Inum.simps β.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] have nob: "¬ (∃j∈ {1 ..d}. x = - ?e + j)" by auto from False p have "x + ?e > 0 ∧ x + ?e ≤ d" by (simp add: c1) then have "x + ?e ≥ 1 ∧ x + ?e ≤ d" by simp then have "∃j::int ∈ {1 .. d}. j = x + ?e" by simp then have "∃j::int ∈ {1 .. d}. x = (- ?e + j)" by (simp add: algebra_simps) with nob show ?thesis by auto qed next case (8 c e) then have p: "Ifm bbs (x # bs) (Ge (CN 0 c e))" and c1: "c = 1" and bn: "numbound0 e" by simp_all let ?e = "Inum (x # bs) e" show ?case proof (cases "(x - d) + ?e ≥ 0") case True then show ?thesis using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp next case False let ?v = "Sub (C (- 1)) e" have vb: "?v ∈ set (β (Ge (CN 0 c e)))" by simp from 8(5)[simplified simp_thms Inum.simps β.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] have nob: "¬ (∃j∈ {1 ..d}. x = - ?e - 1 + j)" by auto from False p have "x + ?e ≥ 0 ∧ x + ?e < d" by (simp add: c1) then have "x + ?e +1 ≥ 1 ∧ x + ?e + 1 ≤ d" by simp then have "∃j::int ∈ {1 .. d}. j = x + ?e + 1" by simp then have "∃j::int ∈ {1 .. d}. x= - ?e - 1 + j" by (simp add: algebra_simps) with nob show ?thesis by simp qed next case (3 c e) then have p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c = 1" and bn: "numbound0 e" by simp_all let ?e = "Inum (x # bs) e" let ?v="(Sub (C (- 1)) e)" have vb: "?v ∈ set (β (Eq (CN 0 c e)))" by simp from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case using dp apply simp apply (erule ballE[where x="1"]) apply (simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"]) done next case (4 c e) then have p: "Ifm bbs (x # bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c = 1" and bn: "numbound0 e" by simp_all let ?e = "Inum (x # bs) e" let ?v="Neg e" have vb: "?v ∈ set (β (NEq (CN 0 c e)))" by simp show ?case proof (cases "x - d + Inum ((x - d) # bs) e = 0") case False then show ?thesis by (simp add: c1) next case True then have "x = - Inum ((x - d) # bs) e + d" by simp then have "x = - Inum (a # bs) e + d" by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"]) with 4(5) show ?thesis using dp by simp qed next case (9 j c e) then have p: "Ifm bbs (x # bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c = 1" and bn: "numbound0 e" by simp_all let ?e = "Inum (x # bs) e" from 9 have id: "j dvd d" by simp from c1 have "?p x ⟷ j dvd (x + ?e)" by simp also have "… ⟷ j dvd x - d + ?e" using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp finally show ?case using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp next case (10 j c e) then have p: "Ifm bbs (x # bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c = 1" and bn: "numbound0 e" by simp_all let ?e = "Inum (x # bs) e" from 10 have id: "j dvd d" by simp from c1 have "?p x ⟷ ¬ j dvd (x + ?e)" by simp also have "… ⟷ ¬ j dvd x - d + ?e" using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp finally show ?case using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp qed (auto simp add: numbound0_I[where bs="bs" and b="(x - d)" and b'="x"] gr0_conv_Suc) lemma β': assumes lp: "iszlfm p" and u: "d_β p 1" and d: "d_δ p d" and dp: "d > 0" shows "∀x. ¬ (∃j::int ∈ {1 .. d}. ∃b ∈ set(β p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) ⟶ Ifm bbs (x # bs) p ⟶ Ifm bbs ((x - d) # bs) p" (is "∀x. ?b ⟶ ?P x ⟶ ?P (x - d)") proof clarify fix x assume nb: "?b" and px: "?P x" then have nb2: "¬ (∃j::int ∈ {1 .. d}. ∃b ∈ Inum (a # bs) ` set (β p). x = b + j)" by auto show "?P (x - d)" by (rule β[OF lp u d dp nb2 px]) qed lemma cpmi_eq: fixes P P1 :: "int ⇒ bool" assumes "0 < D" and "∃z. ∀x. x < z ⟶ P x = P1 x" and "∀x. ¬ (∃j ∈ {1..D}. ∃b ∈ B. P (b + j)) ⟶ P x ⟶ P (x - D)" and "∀x k. P1 x = P1 (x - k * D)" shows "(∃x. P x) ⟷ (∃j ∈ {1..D}. P1 j) ∨ (∃j ∈ {1..D}. ∃b ∈ B. P (b + j))" apply (insert assms) apply (rule iffI) prefer 2 apply (drule minusinfinity) apply assumption+ apply fastforce apply clarsimp apply (subgoal_tac "⋀k. 0 ≤ k ⟹ ∀x. P x ⟶ P (x - k * D)") apply (frule_tac x = x and z=z in decr_lemma) apply (subgoal_tac "P1 (x - (¦x - z¦ + 1) * D)") prefer 2 apply (subgoal_tac "0 ≤ ¦x - z¦ + 1") prefer 2 apply arith apply fastforce apply (drule (1) periodic_finite_ex) apply blast apply (blast dest: decr_mult_lemma) done theorem cp_thm: assumes lp: "iszlfm p" and u: "d_β p 1" and d: "d_δ p d" and dp: "d > 0" shows "(∃x. Ifm bbs (x # bs) p) ⟷ (∃j ∈ {1.. d}. Ifm bbs (j # bs) (minusinf p) ∨ (∃b ∈ set (β p). Ifm bbs ((Inum (i # bs) b + j) # bs) p))" (is "(∃x. ?P x) ⟷ (∃j ∈ ?D. ?M j ∨ (∃b ∈ ?B. ?P (?I b + j)))") proof - from minusinf_inf[OF lp u] have th: "∃z. ∀x<z. ?P x = ?M x" by blast let ?B' = "{?I b | b. b ∈ ?B}" have BB': "(∃j∈?D. ∃b ∈ ?B. ?P (?I b + j)) ⟷ (∃j ∈ ?D. ∃b ∈ ?B'. ?P (b + j))" by auto then have th2: "∀x. ¬ (∃j ∈ ?D. ∃b ∈ ?B'. ?P (b + j)) ⟶ ?P x ⟶ ?P (x - d)" using β'[OF lp u d dp, where a="i" and bbs = "bbs"] by blast from minusinf_repeats[OF d lp] have th3: "∀x k. ?M x = ?M (x-k*d)" by simp from cpmi_eq[OF dp th th2 th3] BB' show ?thesis by blast qed text ‹Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff.› lemma mirror_ex: assumes "iszlfm p" shows "(∃x. Ifm bbs (x#bs) (mirror p)) ⟷ (∃x. Ifm bbs (x#bs) p)" (is "(∃x. ?I x ?mp) = (∃x. ?I x p)") proof auto fix x assume "?I x ?mp" then have "?I (- x) p" using mirror[OF assms] by blast then show "∃x. ?I x p" by blast next fix x assume "?I x p" then have "?I (- x) ?mp" using mirror[OF assms, where x="- x", symmetric] by auto then show "∃x. ?I x ?mp" by blast qed lemma cp_thm': assumes "iszlfm p" and "d_β p 1" and "d_δ p d" and "d > 0" shows "(∃x. Ifm bbs (x # bs) p) ⟷ ((∃j∈ {1 .. d}. Ifm bbs (j#bs) (minusinf p)) ∨ (∃j∈ {1.. d}. ∃b∈ (Inum (i#bs)) ` set (β p). Ifm bbs ((b + j) # bs) p))" using cp_thm[OF assms,where i="i"] by auto definition unit :: "fm ⇒ fm × num list × int" where "unit p = (let p' = zlfm p; l = ζ p'; q = And (Dvd l (CN 0 1 (C 0))) (a_β p' l); d = δ q; B = remdups (map simpnum (β q)); a = remdups (map simpnum (α q)) in if length B ≤ length a then (q, B, d) else (mirror q, a, d))" lemma unit: assumes qf: "qfree p" fixes q B d assumes qBd: "unit p = (q, B, d)" shows "((∃x. Ifm bbs (x # bs) p) ⟷ (∃x. Ifm bbs (x # bs) q)) ∧ (Inum (i # bs)) ` set B = (Inum (i # bs)) ` set (β q) ∧ d_β q 1 ∧ d_δ q d ∧ d > 0 ∧ iszlfm q ∧ (∀b∈ set B. numbound0 b)" proof - let ?I = "λx p. Ifm bbs (x#bs) p" let ?p' = "zlfm p" let ?l = "ζ ?p'" let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a_β ?p' ?l)" let ?d = "δ ?q" let ?B = "set (β ?q)" let ?B'= "remdups (map simpnum (β ?q))" let ?A = "set (α ?q)" let ?A'= "remdups (map simpnum (α ?q))" from conjunct1[OF zlfm_I[OF qf, where bs="bs"]] have pp': "∀i. ?I i ?p' = ?I i p" by auto from conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]] have lp': "iszlfm ?p'" . from lp' ζ[where p="?p'"] have lp: "?l >0" and dl: "d_β ?p' ?l" by auto from a_β_ex[where p="?p'" and l="?l" and bs="bs", OF lp' dl lp] pp' have pq_ex:"(∃(x::int). ?I x p) = (∃x. ?I x ?q)" by simp from lp' lp a_β[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d_β ?q 1" by auto from δ[OF lq] have dp:"?d >0" and dd: "d_δ ?q ?d" by blast+ let ?N = "λt. Inum (i#bs) t" have "?N ` set ?B' = ((?N ∘ simpnum) ` ?B)" by auto also have "… = ?N ` ?B" using simpnum_ci[where bs="i#bs"] by auto finally have BB': "?N ` set ?B' = ?N ` ?B" . have "?N ` set ?A' = ((?N ∘ simpnum) ` ?A)" by auto also have "… = ?N ` ?A" using simpnum_ci[where bs="i#bs"] by auto finally have AA': "?N ` set ?A' = ?N ` ?A" . from β_numbound0[OF lq] have B_nb:"∀b∈ set ?B'. numbound0 b" by (simp add: simpnum_numbound0) from α_l[OF lq] have A_nb: "∀b∈ set ?A'. numbound0 b" by (simp add: simpnum_numbound0) show ?thesis proof (cases "length ?B' ≤ length ?A'") case True then have q: "q = ?q" and "B = ?B'" and d: "d = ?d" using qBd by (auto simp add: Let_def unit_def) with BB' B_nb have b: "?N ` (set B) = ?N ` set (β q)" and bn: "∀b∈ set B. numbound0 b" by simp_all with pq_ex dp uq dd lq q d show ?thesis by simp next case False then have q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d" using qBd by (auto simp add: Let_def unit_def) with AA' mirror_α_β[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (β q)" and bn: "∀b∈ set B. numbound0 b" by simp_all from mirror_ex[OF lq] pq_ex q have pqm_eq:"(∃(x::int). ?I x p) = (∃(x::int). ?I x q)" by simp from lq uq q mirror_l[where p="?q"] have lq': "iszlfm q" and uq: "d_β q 1" by auto from δ[OF lq'] mirror_δ[OF lq] q d have dq: "d_δ q d" by auto from pqm_eq b bn uq lq' dp dq q dp d show ?thesis by simp qed qed text ‹Cooper's Algorithm› definition cooper :: "fm ⇒ fm" where "cooper p = (let (q, B, d) = unit p; js = [1..d]; mq = simpfm (minusinf q); md = evaldjf (λj. simpfm (subst0 (C j) mq)) js in if md = T then T else (let qd = evaldjf (λ(b, j). simpfm (subst0 (Add b (C j)) q)) [(b, j). b ← B, j ← js] in decr (disj md qd)))" lemma cooper: assumes qf: "qfree p" shows "(∃x. Ifm bbs (x#bs) p) = Ifm bbs bs (cooper p) ∧ qfree (cooper p)" (is "?lhs = ?rhs ∧ _") proof - let ?I = "λx p. Ifm bbs (x#bs) p" let ?q = "fst (unit p)" let ?B = "fst (snd(unit p))" let ?d = "snd (snd (unit p))" let ?js = "[1..?d]" let ?mq = "minusinf ?q" let ?smq = "simpfm ?mq" let ?md = "evaldjf (λj. simpfm (subst0 (C j) ?smq)) ?js" fix i let ?N = "λt. Inum (i#bs) t" let ?Bjs = "[(b,j). b←?B,j←?js]" let ?qd = "evaldjf (λ(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs" have qbf:"unit p = (?q,?B,?d)" by simp from unit[OF qf qbf] have pq_ex: "(∃(x::int). ?I x p) ⟷ (∃(x::int). ?I x ?q)" and B: "?N ` set ?B = ?N ` set (β ?q)" and uq: "d_β ?q 1" and dd: "d_δ ?q ?d" and dp: "?d > 0" and lq: "iszlfm ?q" and Bn: "∀b∈ set ?B. numbound0 b" by auto from zlin_qfree[OF lq] have qfq: "qfree ?q" . from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq" . have jsnb: "∀j ∈ set ?js. numbound0 (C j)" by simp then have "∀j∈ set ?js. bound0 (subst0 (C j) ?smq)" by (auto simp only: subst0_bound0[OF qfmq]) then have th: "∀j∈ set ?js. bound0 (simpfm (subst0 (C j) ?smq))" by (auto simp add: simpfm_bound0) from evaldjf_bound0[OF th] have mdb: "bound0 ?md" by simp from Bn jsnb have "∀(b,j) ∈ set ?Bjs. numbound0 (Add b (C j))" by simp then have "∀(b,j) ∈ set ?Bjs. bound0 (subst0 (Add b (C j)) ?q)" using subst0_bound0[OF qfq] by blast then have "∀(b,j) ∈ set ?Bjs. bound0 (simpfm (subst0 (Add b (C j)) ?q))" using simpfm_bound0 by blast then have th': "∀x ∈ set ?Bjs. bound0 ((λ(b,j). simpfm (subst0 (Add b (C j)) ?q)) x)" by auto from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd" by simp from mdb qdb have mdqdb: "bound0 (disj ?md ?qd)" unfolding disj_def by (cases "?md = T ∨ ?qd = T") simp_all from trans [OF pq_ex cp_thm'[OF lq uq dd dp,where i="i"]] B have "?lhs ⟷ (∃j ∈ {1.. ?d}. ?I j ?mq ∨ (∃b ∈ ?N ` set ?B. Ifm bbs ((b + j) # bs) ?q))" by auto also have "… ⟷ (∃j ∈ {1.. ?d}. ?I j ?mq ∨ (∃b ∈ set ?B. Ifm bbs ((?N b + j) # bs) ?q))" by simp also have "… ⟷ (∃j ∈ {1.. ?d}. ?I j ?mq ) ∨ (∃j∈ {1.. ?d}. ∃b ∈ set ?B. Ifm bbs ((?N (Add b (C j))) # bs) ?q)" by (simp only: Inum.simps) blast also have "… ⟷ (∃j ∈ {1.. ?d}. ?I j ?smq) ∨ (∃j ∈ {1.. ?d}. ∃b ∈ set ?B. Ifm bbs ((?N (Add b (C j))) # bs) ?q)" by (simp add: simpfm) also have "… ⟷ (∃j∈ set ?js. (λj. ?I i (simpfm (subst0 (C j) ?smq))) j) ∨ (∃j∈ set ?js. ∃b∈ set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q)" by (simp only: simpfm subst0_I[OF qfmq] set_upto) auto also have "… ⟷ ?I i (evaldjf (λj. simpfm (subst0 (C j) ?smq)) ?js) ∨ (∃j∈ set ?js. ∃b∈ set ?B. ?I i (subst0 (Add b (C j)) ?q))" by (simp only: evaldjf_ex subst0_I[OF qfq]) also have "… ⟷ ?I i ?md ∨ (∃(b,j) ∈ set ?Bjs. (λ(b,j). ?I i (simpfm (subst0 (Add b (C j)) ?q))) (b,j))" by (simp only: simpfm set_concat set_map concat_map_singleton UN_simps) blast also have "… ⟷ ?I i ?md ∨ ?I i (evaldjf (λ(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)" by (simp only: evaldjf_ex[where bs="i#bs" and f="λ(b,j). simpfm (subst0 (Add b (C j)) ?q)" and ps="?Bjs"]) (auto simp add: split_def) finally have mdqd: "?lhs ⟷ ?I i ?md ∨ ?I i ?qd" by simp also have "… ⟷ ?I i (disj ?md ?qd)" by (simp add: disj) also have "… ⟷ Ifm bbs bs (decr (disj ?md ?qd))" by (simp only: decr [OF mdqdb]) finally have mdqd2: "?lhs ⟷ Ifm bbs bs (decr (disj ?md ?qd))" . show ?thesis proof (cases "?md = T") case True then have cT: "cooper p = T" by (simp only: cooper_def unit_def split_def Let_def if_True) simp from True have lhs: "?lhs" using mdqd by simp from True have "?rhs" by (simp add: cooper_def unit_def split_def) with lhs cT show ?thesis by simp next case False then have "cooper p = decr (disj ?md ?qd)" by (simp only: cooper_def unit_def split_def Let_def if_False) with mdqd2 decr_qf[OF mdqdb] show ?thesis by simp qed qed definition pa :: "fm ⇒ fm" where "pa p = qelim (prep p) cooper" theorem mirqe: "Ifm bbs bs (pa p) = Ifm bbs bs p ∧ qfree (pa p)" using qelim_ci cooper prep by (auto simp add: pa_def) definition cooper_test :: "unit ⇒ fm" where "cooper_test u = pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1))) (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) (Bound 2))))))))" ML_val ‹@{code cooper_test} ()› (*code_reflect Cooper_Procedure functions pa T Bound nat_of_integer integer_of_nat int_of_integer integer_of_int file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML"*) oracle linzqe_oracle = ‹ let fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (=) vs t of NONE => error "Variable not found in the list!" | SOME n => @{code Bound} (@{code nat_of_integer} n)) | num_of_term vs @{term "0::int"} = @{code C} (@{code int_of_integer} 0) | num_of_term vs @{term "1::int"} = @{code C} (@{code int_of_integer} 1) | num_of_term vs @{term "- 1::int"} = @{code C} (@{code int_of_integer} (~ 1)) | num_of_term vs (@{term "numeral :: _ ⇒ int"} $ t) = @{code C} (@{code int_of_integer} (HOLogic.dest_numeral t)) | num_of_term vs (@{term "- numeral :: _ ⇒ int"} $ t) = @{code C} (@{code int_of_integer} (~(HOLogic.dest_numeral t))) | num_of_term vs (Bound i) = @{code Bound} (@{code nat_of_integer} i) | num_of_term vs (@{term "uminus :: int ⇒ int"} $ t') = @{code Neg} (num_of_term vs t') | num_of_term vs (@{term "(+) :: int ⇒ int ⇒ int"} $ t1 $ t2) = @{code Add} (num_of_term vs t1, num_of_term vs t2) | num_of_term vs (@{term "(-) :: int ⇒ int ⇒ int"} $ t1 $ t2) = @{code Sub} (num_of_term vs t1, num_of_term vs t2) | num_of_term vs (@{term "( * ) :: int ⇒ int ⇒ int"} $ t1 $ t2) = (case try HOLogic.dest_number t1 of SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t2) | NONE => (case try HOLogic.dest_number t2 of SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t1) | NONE => error "num_of_term: unsupported multiplication")) | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t); fun fm_of_term ps vs @{term True} = @{code T} | fm_of_term ps vs @{term False} = @{code F} | fm_of_term ps vs (@{term "(<) :: int ⇒ int ⇒ bool"} $ t1 $ t2) = @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) | fm_of_term ps vs (@{term "(≤) :: int ⇒ int ⇒ bool"} $ t1 $ t2) = @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) | fm_of_term ps vs (@{term "(=) :: int ⇒ int ⇒ bool"} $ t1 $ t2) = @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) | fm_of_term ps vs (@{term "(dvd) :: int ⇒ int ⇒ bool"} $ t1 $ t2) = (case try HOLogic.dest_number t1 of SOME (_, i) => @{code Dvd} (@{code int_of_integer} i, num_of_term vs t2) | NONE => error "num_of_term: unsupported dvd") | fm_of_term ps vs (@{term "(=) :: bool ⇒ bool ⇒ bool"} $ t1 $ t2) = @{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2) | fm_of_term ps vs (@{term HOL.conj} $ t1 $ t2) = @{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2) | fm_of_term ps vs (@{term HOL.disj} $ t1 $ t2) = @{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2) | fm_of_term ps vs (@{term HOL.implies} $ t1 $ t2) = @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2) | fm_of_term ps vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term ps vs t') | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) = let val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p); (* FIXME !? *) val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs; in @{code E} (fm_of_term ps vs' p) end | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) = let val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p); (* FIXME !? *) val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs; in @{code A} (fm_of_term ps vs' p) end | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t); fun term_of_num vs (@{code C} i) = HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i) | term_of_num vs (@{code Bound} n) = let val q = @{code integer_of_nat} n in fst (the (find_first (fn (_, m) => q = m) vs)) end | term_of_num vs (@{code Neg} t') = @{term "uminus :: int ⇒ int"} $ term_of_num vs t' | term_of_num vs (@{code Add} (t1, t2)) = @{term "(+) :: int ⇒ int ⇒ int"} $ term_of_num vs t1 $ term_of_num vs t2 | term_of_num vs (@{code Sub} (t1, t2)) = @{term "(-) :: int ⇒ int ⇒ int"} $ term_of_num vs t1 $ term_of_num vs t2 | term_of_num vs (@{code Mul} (i, t2)) = @{term "( * ) :: int ⇒ int ⇒ int"} $ term_of_num vs (@{code C} i) $ term_of_num vs t2 | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t)); fun term_of_fm ps vs @{code T} = @{term True} | term_of_fm ps vs @{code F} = @{term False} | term_of_fm ps vs (@{code Lt} t) = @{term "(<) :: int ⇒ int ⇒ bool"} $ term_of_num vs t $ @{term "0::int"} | term_of_fm ps vs (@{code Le} t) = @{term "(≤) :: int ⇒ int ⇒ bool"} $ term_of_num vs t $ @{term "0::int"} | term_of_fm ps vs (@{code Gt} t) = @{term "(<) :: int ⇒ int ⇒ bool"} $ @{term "0::int"} $ term_of_num vs t | term_of_fm ps vs (@{code Ge} t) = @{term "(≤) :: int ⇒ int ⇒ bool"} $ @{term "0::int"} $ term_of_num vs t | term_of_fm ps vs (@{code Eq} t) = @{term "(=) :: int ⇒ int ⇒ bool"} $ term_of_num vs t $ @{term "0::int"} | term_of_fm ps vs (@{code NEq} t) = term_of_fm ps vs (@{code NOT} (@{code Eq} t)) | term_of_fm ps vs (@{code Dvd} (i, t)) = @{term "(dvd) :: int ⇒ int ⇒ bool"} $ term_of_num vs (@{code C} i) $ term_of_num vs t | term_of_fm ps vs (@{code NDvd} (i, t)) = term_of_fm ps vs (@{code NOT} (@{code Dvd} (i, t))) | term_of_fm ps vs (@{code NOT} t') = HOLogic.Not $ term_of_fm ps vs t' | term_of_fm ps vs (@{code And} (t1, t2)) = HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 | term_of_fm ps vs (@{code Or} (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 | term_of_fm ps vs (@{code Imp} (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 | term_of_fm ps vs (@{code Iff} (t1, t2)) = @{term "(=) :: bool ⇒ bool ⇒ bool"} $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 | term_of_fm ps vs (@{code Closed} n) = let val q = @{code integer_of_nat} n in (fst o the) (find_first (fn (_, m) => m = q) ps) end | term_of_fm ps vs (@{code NClosed} n) = term_of_fm ps vs (@{code NOT} (@{code Closed} n)); fun term_bools acc t = let val is_op = member (=) [@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "(=) :: bool ⇒ _"}, @{term "(=) :: int ⇒ _"}, @{term "(<) :: int ⇒ _"}, @{term "(≤) :: int ⇒ _"}, @{term "Not"}, @{term "All :: (int ⇒ _) ⇒ _"}, @{term "Ex :: (int ⇒ _) ⇒ _"}, @{term "True"}, @{term "False"}] fun is_ty t = not (fastype_of t = HOLogic.boolT) in (case t of (l as f $ a) $ b => if is_ty t orelse is_op t then term_bools (term_bools acc l) b else insert (aconv) t acc | f $ a => if is_ty t orelse is_op t then term_bools (term_bools acc f) a else insert (aconv) t acc | Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p)) (* FIXME !? *) | _ => if is_ty t orelse is_op t then acc else insert (aconv) t acc) end; in fn (ctxt, t) => let val fs = Misc_Legacy.term_frees t; val bs = term_bools [] t; val vs = map_index swap fs; val ps = map_index swap bs; val t' = term_of_fm ps vs (@{code pa} (fm_of_term ps vs t)); in Thm.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end end; › ML_file "cooper_tac.ML" method_setup cooper = ‹ Scan.lift (Args.mode "no_quantify") >> (fn q => fn ctxt => SIMPLE_METHOD' (Cooper_Tac.linz_tac ctxt (not q))) › "decision procedure for linear integer arithmetic" text ‹Tests› lemma "∃(j::int). ∀x≥j. ∃a b. x = 3*a+5*b" by cooper lemma "∀(x::int) ≥ 8. ∃i j. 5*i + 3*j = x" by cooper theorem "(∀(y::int). 3 dvd y) ⟹ ∀(x::int). b < x ⟶ a ≤ x" by cooper theorem "⋀(y::int) (z::int) (n::int). 3 dvd z ⟹ 2 dvd (y::int) ⟹ (∃(x::int). 2*x = y) ∧ (∃(k::int). 3*k = z)" by cooper theorem "⋀(y::int) (z::int) n. Suc n < 6 ⟹ 3 dvd z ⟹ 2 dvd (y::int) ⟹ (∃(x::int). 2*x = y) ∧ (∃(k::int). 3*k = z)" by cooper theorem "∀(x::nat). ∃(y::nat). (0::nat) ≤ 5 ⟶ y = 5 + x" by cooper lemma "∀(x::int) ≥ 8. ∃i j. 5*i + 3*j = x" by cooper lemma "∀(y::int) (z::int) (n::int). 3 dvd z ⟶ 2 dvd (y::int) ⟶ (∃(x::int). 2*x = y) ∧ (∃(k::int). 3*k = z)" by cooper lemma "∀(x::int) y. x < y ⟶ 2 * x + 1 < 2 * y" by cooper lemma "∀(x::int) y. 2 * x + 1 ≠ 2 * y" by cooper lemma "∃(x::int) y. 0 < x ∧ 0 ≤ y ∧ 3 * x - 5 * y = 1" by cooper lemma "¬ (∃(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" by cooper lemma "∀(x::int). 2 dvd x ⟶ (∃(y::int). x = 2*y)" by cooper lemma "∀(x::int). 2 dvd x ⟷ (∃(y::int). x = 2*y)" by cooper lemma "∀(x::int). 2 dvd x ⟷ (∀(y::int). x ≠ 2*y + 1)" by cooper lemma "¬ (∀(x::int). (2 dvd x ⟷ (∀(y::int). x ≠ 2*y+1) ∨ (∃(q::int) (u::int) i. 3*i + 2*q - u < 17) ⟶ 0 < x ∨ (¬ 3 dvd x ∧ x + 8 = 0)))" by cooper lemma "¬ (∀(i::int). 4 ≤ i ⟶ (∃x y. 0 ≤ x ∧ 0 ≤ y ∧ 3 * x + 5 * y = i))" by cooper lemma "∃j. ∀(x::int) ≥ j. ∃i j. 5*i + 3*j = x" by cooper theorem "(∀(y::int). 3 dvd y) ⟹ ∀(x::int). b < x ⟶ a ≤ x" by cooper theorem "⋀(y::int) (z::int) (n::int). 3 dvd z ⟹ 2 dvd (y::int) ⟹ (∃(x::int). 2*x = y) ∧ (∃(k::int). 3*k = z)" by cooper theorem "⋀(y::int) (z::int) n. Suc n < 6 ⟹ 3 dvd z ⟹ 2 dvd (y::int) ⟹ (∃(x::int). 2*x = y) ∧ (∃(k::int). 3*k = z)" by cooper theorem "∀(x::nat). ∃(y::nat). (0::nat) ≤ 5 ⟶ y = 5 + x" by cooper theorem "∀(x::nat). ∃(y::nat). y = 5 + x ∨ x div 6 + 1 = 2" by cooper theorem "∃(x::int). 0 < x" by cooper theorem "∀(x::int) y. x < y ⟶ 2 * x + 1 < 2 * y" by cooper theorem "∀(x::int) y. 2 * x + 1 ≠ 2 * y" by cooper theorem "∃(x::int) y. 0 < x ∧ 0 ≤ y ∧ 3 * x - 5 * y = 1" by cooper theorem "¬ (∃(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" by cooper theorem "¬ (∃(x::int). False)" by cooper theorem "∀(x::int). 2 dvd x ⟶ (∃(y::int). x = 2*y)" by cooper theorem "∀(x::int). 2 dvd x ⟶ (∃(y::int). x = 2*y)" by cooper theorem "∀(x::int). 2 dvd x ⟷ (∃(y::int). x = 2*y)" by cooper theorem "∀(x::int). 2 dvd x ⟷ (∀(y::int). x ≠ 2*y + 1)" by cooper theorem "¬ (∀(x::int). (2 dvd x ⟷ (∀(y::int). x ≠ 2*y+1) ∨ (∃(q::int) (u::int) i. 3*i + 2*q - u < 17) ⟶ 0 < x ∨ (¬ 3 dvd x ∧ x + 8 = 0)))" by cooper theorem "¬ (∀(i::int). 4 ≤ i ⟶ (∃x y. 0 ≤ x ∧ 0 ≤ y ∧ 3 * x + 5 * y = i))" by cooper theorem "∀(i::int). 8 ≤ i ⟶ (∃x y. 0 ≤ x ∧ 0 ≤ y ∧ 3 * x + 5 * y = i)" by cooper theorem "∃(j::int). ∀i. j ≤ i ⟶ (∃x y. 0 ≤ x ∧ 0 ≤ y ∧ 3 * x + 5 * y = i)" by cooper theorem "¬ (∀j (i::int). j ≤ i ⟶ (∃x y. 0 ≤ x ∧ 0 ≤ y ∧ 3 * x + 5 * y = i))" by cooper theorem "(∃m::nat. n = 2 * m) ⟶ (n + 1) div 2 = n div 2" by cooper end