Up to index of Isabelle/HOL/ex
theory Reflected_Presburger(* Title: HOL/ex/PresburgerEx.thy ID: $Id: Reflected_Presburger.thy,v 1.4 2005/09/23 19:02:13 webertj Exp $ Author: Amine Chaieb, TU Muenchen A formalization of quantifier elimination for Presburger arithmetic based on a generic quantifier elimination algorithm and Cooper's method to eliminate on ∃. *) header {* Quantifier elimination for Presburger arithmetic *} theory Reflected_Presburger imports Main begin (* Shadow syntax for integer terms *) datatype intterm = Cst int | Var nat | Neg intterm | Add intterm intterm | Sub intterm intterm | Mult intterm intterm (* interpretation of intterms, takes bound variables and free variables *) consts I_intterm :: "int list => intterm => int" primrec "I_intterm ats (Cst b) = b" "I_intterm ats (Var n) = (ats!n)" "I_intterm ats (Neg it) = -(I_intterm ats it)" "I_intterm ats (Add it1 it2) = (I_intterm ats it1) + (I_intterm ats it2)" "I_intterm ats (Sub it1 it2) = (I_intterm ats it1) - (I_intterm ats it2)" "I_intterm ats (Mult it1 it2) = (I_intterm ats it1) * (I_intterm ats it2)" (* Shadow syntax for Presburger formulae *) datatype QF = Lt intterm intterm |Gt intterm intterm |Le intterm intterm |Ge intterm intterm |Eq intterm intterm |Divides intterm intterm |T |F |NOT QF |And QF QF |Or QF QF |Imp QF QF |Equ QF QF |QAll QF |QEx QF (* Interpretation of Presburger formulae *) consts qinterp :: "int list => QF => bool" primrec "qinterp ats (Lt it1 it2) = (I_intterm ats it1 < I_intterm ats it2)" "qinterp ats (Gt it1 it2) = (I_intterm ats it1 > I_intterm ats it2)" "qinterp ats (Le it1 it2) = (I_intterm ats it1 ≤ I_intterm ats it2)" "qinterp ats (Ge it1 it2) = (I_intterm ats it1 ≥ I_intterm ats it2)" "qinterp ats (Divides it1 it2) = (I_intterm ats it1 dvd I_intterm ats it2)" "qinterp ats (Eq it1 it2) = (I_intterm ats it1 = I_intterm ats it2)" "qinterp ats T = True" "qinterp ats F = False" "qinterp ats (NOT p) = (¬(qinterp ats p))" "qinterp ats (And p q) = (qinterp ats p ∧ qinterp ats q)" "qinterp ats (Or p q) = (qinterp ats p ∨ qinterp ats q)" "qinterp ats (Imp p q) = (qinterp ats p --> qinterp ats q)" "qinterp ats (Equ p q) = (qinterp ats p = qinterp ats q)" "qinterp ats (QAll p) = (∀x. qinterp (x#ats) p)" "qinterp ats (QEx p) = (∃x. qinterp (x#ats) p)" (* quantifier elimination based on qe, quantifier elimination for an existential formula, with quantifier free body Since quantifier elimination for one formula is allowed to fail, the result is of type QF option *) consts lift_bin:: "('a => 'a => 'b) × 'a option × 'a option => 'b option" recdef lift_bin "measure (λ(c,a,b). size a)" "lift_bin (c,Some a,Some b) = Some (c a b)" "lift_bin (c,x, y) = None" lemma lift_bin_Some: assumes ls: "lift_bin (c,x,y) = Some t" shows "(∃a. x = Some a) ∧ (∃b. y = Some b)" using ls by (cases "x", auto) (cases "y", auto)+ consts lift_un:: "('a => 'b) => 'a option => 'b option" primrec "lift_un c None = None" "lift_un c (Some p) = Some (c p)" consts lift_qe:: "('a => 'b option) => 'a option => 'b option" primrec "lift_qe qe None = None" "lift_qe qe (Some p) = qe p" (* generic quantifier elimination *) consts qelim :: "(QF => QF option) × QF => QF option" recdef qelim "measure (λ(qe,p). size p)" "qelim (qe, (QAll p)) = lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,p))))" "qelim (qe, (QEx p)) = lift_qe qe (qelim (qe,p))" "qelim (qe, (And p q)) = lift_bin (And, (qelim (qe, p)), (qelim (qe, q)))" "qelim (qe, (Or p q)) = lift_bin (Or, (qelim (qe, p)), (qelim (qe, q)))" "qelim (qe, (Imp p q)) = lift_bin (Imp, (qelim (qe, p)), (qelim (qe, q)))" "qelim (qe, (Equ p q)) = lift_bin (Equ, (qelim (qe, p)), (qelim (qe, q)))" "qelim (qe,NOT p) = lift_un NOT (qelim (qe,p))" "qelim (qe, p) = Some p" (* quantifier free-ness *) consts isqfree :: "QF => bool" recdef isqfree "measure size" "isqfree (QAll p) = False" "isqfree (QEx p) = False" "isqfree (And p q) = (isqfree p ∧ isqfree q)" "isqfree (Or p q) = (isqfree p ∧ isqfree q)" "isqfree (Imp p q) = (isqfree p ∧ isqfree q)" "isqfree (Equ p q) = (isqfree p ∧ isqfree q)" "isqfree (NOT p) = isqfree p" "isqfree p = True" (* qelim lifts quantifierfreeness*) lemma qelim_qfree: assumes qeqf: "(!! q q'. [|isqfree q ; qe q = Some q'|] ==> isqfree q')" shows qff:"!! p'. qelim (qe, p) = Some p' ==> isqfree p'" using qeqf proof (induct p) case (Lt a b) have "qelim (qe, Lt a b) = Some (Lt a b)" by simp moreover have "qelim (qe,Lt a b) = Some p'" . ultimately have "p' = Lt a b" by simp moreover have "isqfree (Lt a b)" by simp ultimately show ?case by simp next case (Gt a b) have "qelim (qe, Gt a b) = Some (Gt a b)" by simp moreover have "qelim (qe,Gt a b) = Some p'" . ultimately have "p' = Gt a b" by simp moreover have "isqfree (Gt a b)" by simp ultimately show ?case by simp next case (Le a b) have "qelim (qe, Le a b) = Some (Le a b)" by simp moreover have "qelim (qe,Le a b) = Some p'" . ultimately have "p' = Le a b" by simp moreover have "isqfree (Le a b)" by simp ultimately show ?case by simp next case (Ge a b) have "qelim (qe, Ge a b) = Some (Ge a b)" by simp moreover have "qelim (qe,Ge a b) = Some p'" . ultimately have "p' = Ge a b" by simp moreover have "isqfree (Ge a b)" by simp ultimately show ?case by simp next case (Eq a b) have "qelim (qe, Eq a b) = Some (Eq a b)" by simp moreover have "qelim (qe,Eq a b) = Some p'" . ultimately have "p' = Eq a b" by simp moreover have "isqfree (Eq a b)" by simp ultimately show ?case by simp next case (Divides a b) have "qelim (qe, Divides a b) = Some (Divides a b)" by simp moreover have "qelim (qe,Divides a b) = Some p'" . ultimately have "p' = Divides a b" by simp moreover have "isqfree (Divides a b)" by simp ultimately show ?case by simp next case T have "qelim(qe,T) = Some T" by simp moreover have "qelim(qe,T) = Some p'" . ultimately have "p' = T" by simp moreover have "isqfree T" by simp ultimately show ?case by simp next case F have "qelim(qe,F) = Some F" by simp moreover have "qelim(qe,F) = Some p'" . ultimately have "p' = F" by simp moreover have "isqfree F" by simp ultimately show ?case by simp next case (NOT p) from "NOT.prems" have "∃ p1. qelim(qe,p) = Some p1" by (cases "qelim(qe,p)") simp_all then obtain "p1" where p1_def: "qelim(qe,p) = Some p1" by blast from "NOT.prems" have "!!q q'. [|isqfree q; qe q = Some q'|] ==> isqfree q'" by blast with "NOT.hyps" p1_def have p1qf: "isqfree p1" by blast then have "p' = NOT p1" using "NOT.prems" p1_def by (cases "qelim(qe,NOT p)") simp_all then show ?case using p1qf by simp next case (And p q) from "And.prems" have p1q1: "(∃p1. qelim(qe,p) = Some p1) ∧ (∃q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="And"] by simp from p1q1 obtain "p1" and "q1" where p1_def: "qelim(qe,p) = Some p1" and q1_def: "qelim(qe,q) = Some q1" by blast from prems have qf1:"isqfree p1" using p1_def by blast from prems have qf2:"isqfree q1" using q1_def by blast from "And.prems" have "qelim(qe,And p q) = Some p'" by blast then have "p' = And p1 q1" using p1_def q1_def by simp then show ?case using qf1 qf2 by simp next case (Or p q) from "Or.prems" have p1q1: "(∃p1. qelim(qe,p) = Some p1) ∧ (∃q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="Or"] by simp from p1q1 obtain "p1" and "q1" where p1_def: "qelim(qe,p) = Some p1" and q1_def: "qelim(qe,q) = Some q1" by blast from prems have qf1:"isqfree p1" using p1_def by blast from prems have qf2:"isqfree q1" using q1_def by blast from "Or.prems" have "qelim(qe,Or p q) = Some p'" by blast then have "p' = Or p1 q1" using p1_def q1_def by simp then show ?case using qf1 qf2 by simp next case (Imp p q) from "Imp.prems" have p1q1: "(∃p1. qelim(qe,p) = Some p1) ∧ (∃q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="Imp"] by simp from p1q1 obtain "p1" and "q1" where p1_def: "qelim(qe,p) = Some p1" and q1_def: "qelim(qe,q) = Some q1" by blast from prems have qf1:"isqfree p1" using p1_def by blast from prems have qf2:"isqfree q1" using q1_def by blast from "Imp.prems" have "qelim(qe,Imp p q) = Some p'" by blast then have "p' = Imp p1 q1" using p1_def q1_def by simp then show ?case using qf1 qf2 by simp next case (Equ p q) from "Equ.prems" have p1q1: "(∃p1. qelim(qe,p) = Some p1) ∧ (∃q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="Equ"] by simp from p1q1 obtain "p1" and "q1" where p1_def: "qelim(qe,p) = Some p1" and q1_def: "qelim(qe,q) = Some q1" by blast from prems have qf1:"isqfree p1" using p1_def by blast from prems have qf2:"isqfree q1" using q1_def by blast from "Equ.prems" have "qelim(qe,Equ p q) = Some p'" by blast then have "p' = Equ p1 q1" using p1_def q1_def by simp then show ?case using qf1 qf2 by simp next case (QEx p) from "QEx.prems" have "∃ p1. qelim(qe,p) = Some p1" by (cases "qelim(qe,p)") simp_all then obtain "p1" where p1_def: "qelim(qe,p) = Some p1" by blast from "QEx.prems" have "!!q q'. [|isqfree q; qe q = Some q'|] ==> isqfree q'" by blast with "QEx.hyps" p1_def have p1qf: "isqfree p1" by blast from "QEx.prems" have "qe p1 = Some p'" using p1_def by simp with "QEx.prems" show ?case using p1qf by simp next case (QAll p) from "QAll.prems" have "∃ p1. lift_qe qe (lift_un NOT (qelim (qe ,p))) = Some p1" by (cases "lift_qe qe (lift_un NOT (qelim (qe ,p)))") simp_all then obtain "p1" where p1_def:"lift_qe qe (lift_un NOT (qelim (qe ,p))) = Some p1" by blast then have "∃ p2. lift_un NOT (qelim (qe ,p)) = Some p2" by (cases "qelim (qe ,p)") simp_all then obtain "p2" where p2_def:"lift_un NOT (qelim (qe ,p)) = Some p2" by blast then have "∃ p3. qelim(qe,p) = Some p3" by (cases "qelim(qe,p)") simp_all then obtain "p3" where p3_def: "qelim(qe,p) = Some p3" by blast with prems have qf3: "isqfree p3" by blast have p2_def2: "p2 = NOT p3" using p2_def p3_def by simp then have qf2: "isqfree p2" using qf3 by simp have p1_edf2: "qe p2 = Some p1" using p1_def p2_def by simp with "QAll.prems" have qf1: "isqfree p1" using qf2 by blast from "QAll.prems" have "p' = NOT p1" using p1_def by simp with qf1 show ?case by simp qed (* qelim lifts semantical equivalence *) lemma qelim_corr: assumes qecorr: "(!! q q' ats. [|isqfree q ; qe q = Some q'|] ==> (qinterp ats (QEx q)) = (qinterp ats q'))" and qeqf: "(!! q q'. [|isqfree q ; qe q = Some q'|] ==> isqfree q')" shows qff:"!! p' ats. qelim (qe, p) = Some p' ==> (qinterp ats p = qinterp ats p')" (is "!! p' ats. ?Qe p p' ==> (?F ats p = ?F ats p')") using qeqf qecorr proof (induct p) case (NOT f) from "NOT.prems" have "∃f'. ?Qe f f' " by (cases "qelim(qe,f)") simp_all then obtain "f'" where df': "?Qe f f'" by blast with prems have feqf': "?F ats f = ?F ats f'" by blast from "NOT.prems" df' have "p' = NOT f'" by simp with feqf' show ?case by simp next case (And f g) from "And.prems" have f1g1: "(∃f1. qelim(qe,f) = Some f1) ∧ (∃g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="And"] by simp from f1g1 obtain "f1" and "g1" where f1_def: "qelim(qe, f) = Some f1" and g1_def: "qelim(qe,g) = Some g1" by blast from prems f1_def have feqf1: "?F ats f = ?F ats f1" by blast from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast from "And.prems" f1_def g1_def have "p' = And f1 g1" by simp with feqf1 geqg1 show ?case by simp next case (Or f g) from "Or.prems" have f1g1: "(∃f1. qelim(qe,f) = Some f1) ∧ (∃g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="Or"] by simp from f1g1 obtain "f1" and "g1" where f1_def: "qelim(qe, f) = Some f1" and g1_def: "qelim(qe,g) = Some g1" by blast from prems f1_def have feqf1: "?F ats f = ?F ats f1" by blast from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast from "Or.prems" f1_def g1_def have "p' = Or f1 g1" by simp with feqf1 geqg1 show ?case by simp next case (Imp f g) from "Imp.prems" have f1g1: "(∃f1. qelim(qe,f) = Some f1) ∧ (∃g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="Imp"] by simp from f1g1 obtain "f1" and "g1" where f1_def: "qelim(qe, f) = Some f1" and g1_def: "qelim(qe,g) = Some g1" by blast from prems f1_def have feqf1: "?F ats f = ?F ats f1" by blast from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast from "Imp.prems" f1_def g1_def have "p' = Imp f1 g1" by simp with feqf1 geqg1 show ?case by simp next case (Equ f g) from "Equ.prems" have f1g1: "(∃f1. qelim(qe,f) = Some f1) ∧ (∃g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="Equ"] by simp from f1g1 obtain "f1" and "g1" where f1_def: "qelim(qe, f) = Some f1" and g1_def: "qelim(qe,g) = Some g1" by blast from prems f1_def have feqf1: "?F ats f = ?F ats f1" by blast from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast from "Equ.prems" f1_def g1_def have "p' = Equ f1 g1" by simp with feqf1 geqg1 show ?case by simp next case (QEx f) from "QEx.prems" have "∃ f1. ?Qe f f1" by (cases "qelim(qe,f)") simp_all then obtain "f1" where f1_def: "qelim(qe,f) = Some f1" by blast from prems have qf1:"isqfree f1" using qelim_qfree by blast from prems have feqf1: "∀ ats. qinterp ats f = qinterp ats f1" using f1_def qf1 by blast then have "?F ats (QEx f) = ?F ats (QEx f1)" by simp from prems have "qelim (qe,QEx f) = Some p'" by blast then have "∃ f'. qe f1 = Some f'" using f1_def by simp then obtain "f'" where fdef': "qe f1 = Some f'" by blast with prems have exf1: "?F ats (QEx f1) = ?F ats f'" using qf1 by blast have fp: "?Qe (QEx f) f'" using f1_def fdef' by simp from prems have "?Qe (QEx f) p'" by blast then have "p' = f'" using fp by simp then show ?case using feqf1 exf1 by simp next case (QAll f) from "QAll.prems" have "∃ f0. lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,f)))) = Some f0" by (cases "lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,f))))") simp_all then obtain "f0" where f0_def: "lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,f)))) = Some f0" by blast then have "∃ f1. lift_qe qe (lift_un NOT (qelim (qe ,f))) = Some f1" by (cases "lift_qe qe (lift_un NOT (qelim (qe ,f)))") simp_all then obtain "f1" where f1_def:"lift_qe qe (lift_un NOT (qelim (qe ,f))) = Some f1" by blast then have "∃ f2. lift_un NOT (qelim (qe ,f)) = Some f2" by (cases "qelim (qe ,f)") simp_all then obtain "f2" where f2_def:"lift_un NOT (qelim (qe ,f)) = Some f2" by blast then have "∃ f3. qelim(qe,f) = Some f3" by (cases "qelim(qe,f)") simp_all then obtain "f3" where f3_def: "qelim(qe,f) = Some f3" by blast from prems have qf3:"isqfree f3" using qelim_qfree by blast from prems have feqf3: "∀ ats. qinterp ats f = qinterp ats f3" using f3_def qf3 by blast have f23:"f2 = NOT f3" using f2_def f3_def by simp then have feqf2: "∀ ats. qinterp ats f = qinterp ats (NOT f2)" using feqf3 by simp have qf2: "isqfree f2" using f23 qf3 by simp have "qe f2 = Some f1" using f1_def f2_def f23 by simp with prems have exf2eqf1: "?F ats (QEx f2) = ?F ats f1" using qf2 by blast have "f0 = NOT f1" using f0_def f1_def by simp then have f0eqf1: "?F ats f0 = ?F ats (NOT f1)" by simp from prems have "qelim (qe, QAll f) = Some p'" by blast then have f0eqp': "p' = f0" using f0_def by simp have "?F ats (QAll f) = (∀x. ?F (x#ats) f)" by simp also have "… = (¬ (∃ x. ?F (x#ats) (NOT f)))" by simp also have "… = (¬ (∃ x. ?F (x#ats) (NOT (NOT f2))))" using feqf2 by auto also have "… = (¬ (∃ x. ?F (x#ats) f2))" by simp also have "… = (¬ (?F ats f1))" using exf2eqf1 by simp finally show ?case using f0eqp' f0eqf1 by simp qed simp_all (* Cooper's algorithm *) (* Transform an intform into NNF *) consts lgth :: "QF => nat" nnf :: "QF => QF" primrec "lgth (Lt it1 it2) = 1" "lgth (Gt it1 it2) = 1" "lgth (Le it1 it2) = 1" "lgth (Ge it1 it2) = 1" "lgth (Eq it1 it2) = 1" "lgth (Divides it1 it2) = 1" "lgth T = 1" "lgth F = 1" "lgth (NOT p) = 1 + lgth p" "lgth (And p q) = 1 + lgth p + lgth q" "lgth (Or p q) = 1 + lgth p + lgth q" "lgth (Imp p q) = 1 + lgth p + lgth q" "lgth (Equ p q) = 1 + lgth p + lgth q" "lgth (QAll p) = 1 + lgth p" "lgth (QEx p) = 1 + lgth p" lemma [simp] :"0 < lgth q" apply (induct_tac q) apply(auto) done (* NNF *) recdef nnf "measure (λp. lgth p)" "nnf (Lt it1 it2) = Le (Sub it1 it2) (Cst (- 1))" "nnf (Gt it1 it2) = Le (Sub it2 it1) (Cst (- 1))" "nnf (Le it1 it2) = Le it1 it2 " "nnf (Ge it1 it2) = Le it2 it1" "nnf (Eq it1 it2) = Eq it2 it1" "nnf (Divides d t) = Divides d t" "nnf T = T" "nnf F = F" "nnf (And p q) = And (nnf p) (nnf q)" "nnf (Or p q) = Or (nnf p) (nnf q)" "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)" "nnf (Equ p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))" "nnf (NOT (Lt it1 it2)) = (Le it2 it1)" "nnf (NOT (Gt it1 it2)) = (Le it1 it2)" "nnf (NOT (Le it1 it2)) = (Le (Sub it2 it1) (Cst (- 1)))" "nnf (NOT (Ge it1 it2)) = (Le (Sub it1 it2) (Cst (- 1)))" "nnf (NOT (Eq it1 it2)) = (NOT (Eq it1 it2))" "nnf (NOT (Divides d t)) = (NOT (Divides d t))" "nnf (NOT T) = F" "nnf (NOT F) = T" "nnf (NOT (NOT p)) = (nnf p)" "nnf (NOT (And p q)) = (Or (nnf (NOT p)) (nnf (NOT q)))" "nnf (NOT (Or p q)) = (And (nnf (NOT p)) (nnf (NOT q)))" "nnf (NOT (Imp p q)) = (And (nnf p) (nnf (NOT q)))" "nnf (NOT (Equ p q)) = (Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q)))" consts isnnf :: "QF => bool" recdef isnnf "measure (λp. lgth p)" "isnnf (Le it1 it2) = True" "isnnf (Eq it1 it2) = True" "isnnf (Divides d t) = True" "isnnf T = True" "isnnf F = True" "isnnf (And p q) = (isnnf p ∧ isnnf q)" "isnnf (Or p q) = (isnnf p ∧ isnnf q)" "isnnf (NOT (Divides d t)) = True" "isnnf (NOT (Eq it1 it2)) = True" "isnnf p = False" (* nnf preserves semantics *) lemma nnf_corr: "isqfree p ==> qinterp ats p = qinterp ats (nnf p)" by (induct p rule: nnf.induct,simp_all) (arith, arith, arith, arith, arith, arith, arith, arith, arith, blast) (* the result of nnf is in NNF *) lemma nnf_isnnf : "isqfree p ==> isnnf (nnf p)" by (induct p rule: nnf.induct, auto) lemma nnf_isqfree: "isnnf p ==> isqfree p" by (induct p rule: isnnf.induct) auto (* nnf preserves quantifier freeness *) lemma nnf_qfree: "isqfree p ==> isqfree(nnf p)" using nnf_isqfree nnf_isnnf by simp (* Linearization and normalization of formulae *) (* Definition of linearity of an intterm *) consts islinintterm :: "intterm => bool" recdef islinintterm "measure size" "islinintterm (Cst i) = True" "islinintterm (Add (Mult (Cst i) (Var n)) (Cst i')) = (i ≠ 0)" "islinintterm (Add (Mult (Cst i) (Var n)) (Add (Mult (Cst i') (Var n')) r)) = ( i ≠ 0 ∧ i' ≠ 0 ∧ n < n' ∧ islinintterm (Add (Mult (Cst i') (Var n')) r))" "islinintterm i = False" (* subterms of linear terms are linear *) lemma islinintterm_subt: assumes lr: "islinintterm (Add (Mult (Cst i) (Var n)) r)" shows "islinintterm r" using lr by (induct r rule: islinintterm.induct) auto (* c ≠ 0 for linear term c.n + r*) lemma islinintterm_cnz: assumes lr: "islinintterm (Add (Mult (Cst i) (Var n)) r)" shows "i ≠ 0" using lr by (induct r rule: islinintterm.induct) auto lemma islininttermc0r: "islinintterm (Add (Mult (Cst c) (Var n)) r) ==> (c ≠ 0 ∧ islinintterm r)" by (induct r rule: islinintterm.induct, simp_all) (* An alternative linearity definition *) consts islintn :: "(nat × intterm) => bool" recdef islintn "measure (λ (n,t). (size t))" "islintn (n0, Cst i) = True" "islintn (n0, Add (Mult (Cst i) (Var n)) r) = (i ≠ 0 ∧ n0 ≤ n ∧ islintn (n+1,r))" "islintn (n0, t) = False" constdefs islint :: "intterm => bool" "islint t ≡ islintn(0,t)" (* And the equivalence to the first definition *) lemma islinintterm_eq_islint: "islinintterm t = islint t" using islint_def by (induct t rule: islinintterm.induct) auto (* monotony *) lemma islintn_mon: assumes lin: "islintn (n,t)" and mgen: "m ≤ n" shows "islintn(m,t)" using lin mgen by (induct t rule: islintn.induct) auto lemma islintn_subt: assumes lint: "islintn(n,Add (Mult (Cst i) (Var m)) r)" shows "islintn (m+1,r)" using lint by auto (* List indexin for n > 0 *) lemma nth_pos: "0 < n --> (x#xs) ! n = (y#xs) ! n" using Nat.gr0_conv_Suc by clarsimp lemma nth_pos2: "0 < n ==> (x#xs) ! n = xs ! (n - 1)" using Nat.gr0_conv_Suc by clarsimp lemma intterm_novar0: assumes lin: "islinintterm (Add (Mult (Cst i) (Var n)) r)" shows "I_intterm (x#ats) r = I_intterm (y#ats) r" using lin by (induct r rule: islinintterm.induct) (simp_all add: nth_pos2) (* a simple version of a general theorem: Interpretation does not depend on the first variable if it does not occur in the term *) lemma linterm_novar0: assumes lin: "islintn (n,t)" and npos: "0 < n" shows "I_intterm (x#ats) t = I_intterm (y#ats) t" using lin npos by (induct n t rule: islintn.induct) (simp_all add: nth_pos2) (* Periodicity of dvd *) lemma dvd_period: assumes advdd: "(a::int) dvd d" shows "(a dvd (x + t)) = (a dvd ((x+ c*d) + t))" using advdd proof- from advdd have "∀x.∀k. (((a::int) dvd (x + t)) = (a dvd (x+k*d + t)))" by (rule dvd_modd_pinf) then show ?thesis by simp qed (* lin_ad adds two linear terms*) consts lin_add :: "intterm × intterm => intterm" recdef lin_add "measure (λ(x,y). ((size x) + (size y)))" "lin_add (Add (Mult (Cst c1) (Var n1)) (r1),Add (Mult (Cst c2) (Var n2)) (r2)) = (if n1=n2 then (let c = Cst (c1 + c2) in (if c1+c2=0 then lin_add(r1,r2) else Add (Mult c (Var n1)) (lin_add (r1,r2)))) else if n1 ≤ n2 then (Add (Mult (Cst c1) (Var n1)) (lin_add (r1,Add (Mult (Cst c2) (Var n2)) (r2)))) else (Add (Mult (Cst c2) (Var n2)) (lin_add (Add (Mult (Cst c1) (Var n1)) r1,r2))))" "lin_add (Add (Mult (Cst c1) (Var n1)) (r1),Cst b) = (Add (Mult (Cst c1) (Var n1)) (lin_add (r1, Cst b)))" "lin_add (Cst x,Add (Mult (Cst c2) (Var n2)) (r2)) = Add (Mult (Cst c2) (Var n2)) (lin_add (Cst x,r2))" "lin_add (Cst b1, Cst b2) = Cst (b1+b2)" lemma lin_add_cst_corr: assumes blin : "islintn(n0,b)" shows "I_intterm ats (lin_add (Cst a,b)) = (I_intterm ats (Add (Cst a) b))" using blin by (induct n0 b rule: islintn.induct) auto lemma lin_add_cst_corr2: assumes blin : "islintn(n0,b)" shows "I_intterm ats (lin_add (b,Cst a)) = (I_intterm ats (Add b (Cst a)))" using blin by (induct n0 b rule: islintn.induct) auto lemma lin_add_corrh: "!! n01 n02. [| islintn (n01,a) ; islintn (n02,b)|] ==> I_intterm ats (lin_add(a,b)) = I_intterm ats (Add a b)" proof(induct a b rule: lin_add.induct) case (58 i n r j m s) have "(n = m ∧ i+j = 0) ∨ (n = m ∧ i+j ≠ 0) ∨ n < m ∨ m < n " by arith moreover {assume "n=m∧i+j=0" hence ?case using prems by (auto simp add: sym[OF zadd_zmult_distrib]) } moreover {assume "n=m∧i+j≠0" hence ?case using prems by (auto simp add: Let_def zadd_zmult_distrib)} moreover {assume "n < m" hence ?case using prems by auto } moreover {assume "n > m" hence ?case using prems by auto } ultimately show ?case by blast qed (auto simp add: lin_add_cst_corr lin_add_cst_corr2 Let_def) (* lin_add has the semantics of Add*) lemma lin_add_corr: assumes lina: "islinintterm a" and linb: "islinintterm b" shows "I_intterm ats (lin_add (a,b)) = (I_intterm ats (Add a b))" using lina linb islinintterm_eq_islint islint_def lin_add_corrh by blast lemma lin_add_cst_lint: assumes lin: "islintn (n0,b)" shows "islintn (n0, lin_add (Cst i, b))" using lin by (induct n0 b rule: islintn.induct) auto lemma lin_add_cst_lint2: assumes lin: "islintn (n0,b)" shows "islintn (n0, lin_add (b,Cst i))" using lin by (induct n0 b rule: islintn.induct) auto (* lin_add preserves linearity..*) lemma lin_add_lint: "!! n0 n01 n02. [| islintn (n01,a) ; islintn (n02,b); n0 ≤ min n01 n02 |] ==> islintn (n0, lin_add (a,b))" proof (induct a b rule: lin_add.induct) case (58 i n r j m s) have "(n =m ∧ i + j = 0) ∨ (n = m ∧ i+j ≠ 0) ∨ n <m ∨ m < n" by arith moreover { assume "n = m" and "i+j = 0" hence ?case using "58" islintn_mon[where m = "n01" and n = "Suc m"] islintn_mon[where m = "n02" and n = "Suc m"] by auto } moreover { assume "n = m" and "i+j ≠ 0" hence ?case using "58" islintn_mon[where m = "n01" and n = "Suc m"] islintn_mon[where m = "n02" and n = "Suc m"] by (auto simp add: Let_def) } moreover { assume "n < m" hence ?case using 58 by force } moreover { assume "m < n" hence ?case using 58 apply (auto simp add: Let_def) apply (erule allE[where x = "Suc m" ] ) by (erule allE[where x = "Suc m" ] ) simp } ultimately show ?case by blast qed(simp_all add: Let_def lin_add_cst_lint lin_add_cst_lint2) lemma lin_add_lin: assumes lina: "islinintterm a" and linb: "islinintterm b" shows "islinintterm (lin_add (a,b))" using islinintterm_eq_islint islint_def lin_add_lint lina linb by auto (* lin_mul multiplies a linear term by a constant *) consts lin_mul :: "int × intterm => intterm" recdef lin_mul "measure (λ(c,t). size t)" "lin_mul (c,Cst i) = (Cst (c*i))" "lin_mul (c,Add (Mult (Cst c') (Var n)) r) = (if c = 0 then (Cst 0) else (Add (Mult (Cst (c*c')) (Var n)) (lin_mul (c,r))))" lemma zmult_zadd_distrib[simp]: "(a::int) * (b+c) = a*b + a*c" proof- have "a*(b+c) = (b+c)*a" by simp moreover have "(b+c)*a = b*a + c*a" by (simp add: zadd_zmult_distrib) ultimately show ?thesis by simp qed (* lin_mul has the semantics of Mult *) lemma lin_mul_corr: assumes lint: "islinintterm t" shows "I_intterm ats (lin_mul (c,t)) = I_intterm ats (Mult (Cst c) t)" using lint proof (induct c t rule: lin_mul.induct) case (21 c c' n r) have "islinintterm (Add (Mult (Cst c') (Var n)) r)" . then have "islinintterm r" by (rule islinintterm_subt[of "c'" "n" "r"]) then show ?case using "21.hyps" "21.prems" by simp qed(auto) (* lin_mul preserves linearity *) lemma lin_mul_lin: assumes lint: "islinintterm t" shows "islinintterm (lin_mul(c,t))" using lint by (induct t rule: islinintterm.induct) auto lemma lin_mul0: assumes lint: "islinintterm t" shows "lin_mul(0,t) = Cst 0" using lint by (induct t rule: islinintterm.induct) auto lemma lin_mul_lintn: "!! m. islintn(m,t) ==> islintn(m,lin_mul(l,t))" by (induct l t rule: lin_mul.induct) simp_all (* lin_neg neagtes a linear term *) constdefs lin_neg :: "intterm => intterm" "lin_neg i == lin_mul ((-1::int),i)" (* lin_neg has the semantics of Neg *) lemma lin_neg_corr: assumes lint: "islinintterm t" shows "I_intterm ats (lin_neg t) = I_intterm ats (Neg t)" using lint lin_mul_corr by (simp add: lin_neg_def lin_mul_corr) (* lin_neg preserves linearity *) lemma lin_neg_lin: assumes lint: "islinintterm t" shows "islinintterm (lin_neg t)" using lint by (simp add: lin_mul_lin lin_neg_def) (* Some properties about lin_add and lin-neg should be moved above *) lemma lin_neg_idemp: assumes lini: "islinintterm i" shows "lin_neg (lin_neg i) = i" using lini by (induct i rule: islinintterm.induct) (auto simp add: lin_neg_def) lemma lin_neg_lin_add_distrib: assumes lina : "islinintterm a" and linb :"islinintterm b" shows "lin_neg (lin_add(a,b)) = lin_add (lin_neg a, lin_neg b)" using lina linb proof (induct a b rule: lin_add.induct) case (58 c1 n1 r1 c2 n2 r2) from prems have lincnr1:"islinintterm (Add (Mult (Cst c1) (Var n1)) r1)" by simp have linr1: "islinintterm r1" by (rule islinintterm_subt[OF lincnr1]) from prems have lincnr2: "islinintterm (Add (Mult (Cst c2) (Var n2)) r2)" by simp have linr2: "islinintterm r2" by (rule islinintterm_subt[OF lincnr2]) have "n1 = n2 ∨ n1 < n2 ∨ n1 > n2" by arith show ?case using prems linr1 linr2 by (simp_all add: lin_neg_def Let_def) next case (59 c n r b) from prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var n)) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) show ?case using prems linr by (simp add: lin_neg_def Let_def) next case (60 b c n r) from prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var n)) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) show ?case using prems linr by (simp add: lin_neg_def Let_def) qed (simp_all add: lin_neg_def) (* linearize tries to linearize a term *) consts linearize :: "intterm => intterm option" recdef linearize "measure (λt. size t)" "linearize (Cst b) = Some (Cst b)" "linearize (Var n) = Some (Add (Mult (Cst 1) (Var n)) (Cst 0))" "linearize (Neg i) = lift_un lin_neg (linearize i)" "linearize (Add i j) = lift_bin(λ x. λ y. lin_add(x,y), linearize i, linearize j)" "linearize (Sub i j) = lift_bin(λ x. λ y. lin_add(x,lin_neg y), linearize i, linearize j)" "linearize (Mult i j) = (case linearize i of None => None | Some li => (case li of Cst b => (case linearize j of None => None | (Some lj) => Some (lin_mul(b,lj))) | _ => (case linearize j of None => None | (Some lj) => (case lj of Cst b => Some (lin_mul (b,li)) | _ => None))))" lemma linearize_linear1: assumes lin: "linearize t ≠ None" shows "islinintterm (the (linearize t))" using lin proof (induct t rule: linearize.induct) case (1 b) show ?case by simp next case (2 n) show ?case by simp next case (3 i) show ?case proof- have "(linearize i = None) ∨ (∃li. linearize i = Some li)" by auto moreover { assume "linearize i = None" with prems have ?thesis by auto} moreover { assume lini: "∃li. linearize i = Some li" from lini obtain "li" where "linearize i = Some li" by blast have linli: "islinintterm li" by (simp!) moreover have "linearize (Neg i) = Some (lin_neg li)" using prems by simp moreover from linli have "islinintterm(lin_neg li)" by (simp add: lin_neg_lin) ultimately have ?thesis by simp } ultimately show ?thesis by blast qed next case (4 i j) show ?case proof- have "(linearize i = None) ∨ ((∃ li. linearize i = Some li) ∧ linearize j = None) ∨ ((∃ li. linearize i = Some li) ∧ (∃ lj. linearize j = Some lj))" by auto moreover { assume nlini: "linearize i = None" from nlini have "linearize (Add i j) = None" by (simp add: Let_def measure_def inv_image_def) then have ?thesis using prems by auto} moreover { assume nlinj: "linearize j = None" and lini: "∃ li. linearize i = Some li" from nlinj lini have "linearize (Add i j) = None" by (simp add: Let_def measure_def inv_image_def, auto) with prems have ?thesis by auto} moreover { assume lini: "∃li. linearize i = Some li" and linj: "∃lj. linearize j = Some lj" from lini obtain "li" where "linearize i = Some li" by blast have linli: "islinintterm li" by (simp!) from linj obtain "lj" where "linearize j = Some lj" by blast have linlj: "islinintterm lj" by (simp!) moreover from lini linj have "linearize (Add i j) = Some (lin_add (li,lj))" by (simp add: measure_def inv_image_def, auto!) moreover from linli linlj have "islinintterm(lin_add (li,lj))" by (simp add: lin_add_lin) ultimately have ?thesis by simp } ultimately show ?thesis by blast qed next case (5 i j)show ?case proof- have "(linearize i = None) ∨ ((∃ li. linearize i = Some li) ∧ linearize j = None) ∨ ((∃ li. linearize i = Some li) ∧ (∃ lj. linearize j = Some lj))" by auto moreover { assume nlini: "linearize i = None" from nlini have "linearize (Sub i j) = None" by (simp add: Let_def measure_def inv_image_def) then have ?thesis by (auto!) } moreover { assume lini: "∃ li. linearize i = Some li" and nlinj: "linearize j = None" from nlinj lini have "linearize (Sub i j) = None" by (simp add: Let_def measure_def inv_image_def, auto) then have ?thesis by (auto!) } moreover { assume lini: "∃li. linearize i = Some li" and linj: "∃lj. linearize j = Some lj" from lini obtain "li" where "linearize i = Some li" by blast have linli: "islinintterm li" by (simp!) from linj obtain "lj" where "linearize j = Some lj" by blast have linlj: "islinintterm lj" by (simp!) moreover from lini linj have "linearize (Sub i j) = Some (lin_add (li,lin_neg lj))" by (simp add: measure_def inv_image_def, auto!) moreover from linli linlj have "islinintterm(lin_add (li,lin_neg lj))" by (simp add: lin_add_lin lin_neg_lin) ultimately have ?thesis by simp } ultimately show ?thesis by blast qed next case (6 i j)show ?case proof- have cses: "(linearize i = None) ∨ ((∃ li. linearize i = Some li) ∧ linearize j = None) ∨ ((∃ li. linearize i = Some li) ∧ (∃ bj. linearize j = Some (Cst bj))) ∨ ((∃ bi. linearize i = Some (Cst bi)) ∧ (∃ lj. linearize j = Some lj)) ∨ ((∃ li. linearize i = Some li ∧ ¬ (∃ bi. li = Cst bi)) ∧ (∃ lj. linearize j = Some lj ∧ ¬ (∃ bj. lj = Cst bj)))" by auto moreover { assume nlini: "linearize i = None" from nlini have "linearize (Mult i j) = None" by (simp add: Let_def measure_def inv_image_def) with prems have ?thesis by auto } moreover { assume lini: "∃ li. linearize i = Some li" and nlinj: "linearize j = None" from lini obtain "li" where "linearize i = Some li" by blast moreover from nlinj lini have "linearize (Mult i j) = None" using prems by (cases li ) (auto simp add: Let_def measure_def inv_image_def) with prems have ?thesis by auto} moreover { assume lini: "∃li. linearize i = Some li" and linj: "∃bj. linearize j = Some (Cst bj)" from lini obtain "li" where li_def: "linearize i = Some li" by blast from prems have linli: "islinintterm li" by simp moreover from linj obtain "bj" where bj_def: "linearize j = Some (Cst bj)" by blast have linlj: "islinintterm (Cst bj)" by simp moreover from lini linj prems have "linearize (Mult i j) = Some (lin_mul (bj,li))" by (cases li) (auto simp add: measure_def inv_image_def) moreover from linli linlj have "islinintterm(lin_mul (bj,li))" by (simp add: lin_mul_lin) ultimately have ?thesis by simp } moreover { assume lini: "∃bi. linearize i = Some (Cst bi)" and linj: "∃lj. linearize j = Some lj" from lini obtain "bi" where "linearize i = Some (Cst bi)" by blast from prems have linli: "islinintterm (Cst bi)" by simp moreover from linj obtain "lj" where "linearize j = Some lj" by blast from prems have linlj: "islinintterm lj" by simp moreover from lini linj prems have "linearize (Mult i j) = Some (lin_mul (bi,lj))" by (simp add: measure_def inv_image_def) moreover from linli linlj have "islinintterm(lin_mul (bi,lj))" by (simp add: lin_mul_lin) ultimately have ?thesis by simp } moreover { assume linc: "∃ li. linearize i = Some li ∧ ¬ (∃ bi. li = Cst bi)" and ljnc: "∃ lj. linearize j = Some lj ∧ ¬ (∃ bj. lj = Cst bj)" from linc obtain "li" where "linearize i = Some li ∧ ¬ (∃ bi. li = Cst bi)" by blast moreover from ljnc obtain "lj" where "linearize j = Some lj ∧ ¬ (∃ bj. lj = Cst bj)" by blast ultimately have "linearize (Mult i j) = None" by (cases li, auto simp add: measure_def inv_image_def) (cases lj, auto)+ with prems have ?thesis by simp } ultimately show ?thesis by blast qed qed (* the result of linearize, when successful, is a linear term*) lemma linearize_linear: "!! t'. linearize t = Some t' ==> islinintterm t'" proof- fix t' assume lint: "linearize t = Some t'" from lint have lt: "linearize t ≠ None" by auto then have "islinintterm (the (linearize t))" by (rule_tac linearize_linear1[OF lt]) with lint show "islinintterm t'" by simp qed lemma linearize_corr1: assumes lin: "linearize t ≠ None" shows "I_intterm ats t = I_intterm ats (the (linearize t))" using lin proof (induct t rule: linearize.induct) case (3 i) show ?case proof- have "(linearize i = None) ∨ (∃li. linearize i = Some li)" by auto moreover { assume "linearize i = None" have ?thesis using prems by simp } moreover { assume lini: "∃li. linearize i = Some li" from lini have lini2: "linearize i ≠ None" by simp from lini obtain "li" where "linearize i = Some li" by blast from lini2 lini have "islinintterm (the (linearize i))" by (simp add: linearize_linear1[OF lini2]) then have linli: "islinintterm li" using prems by simp have ieqli: "I_intterm ats i = I_intterm ats li" using prems by simp moreover have "linearize (Neg i) = Some (lin_neg li)" using prems by simp moreover from ieqli linli have "I_intterm ats (Neg i) = I_intterm ats (lin_neg li)" by (simp add: lin_neg_corr[OF linli]) ultimately have ?thesis using prems by (simp add: lin_neg_corr) } ultimately show ?thesis by blast qed next case (4 i j) show ?case proof- have "(linearize i = None) ∨ ((∃ li. linearize i = Some li) ∧ linearize j = None) ∨ ((∃ li. linearize i = Some li) ∧ (∃ lj. linearize j = Some lj))" by auto moreover { assume nlini: "linearize i = None" from nlini have "linearize (Add i j) = None" by (simp add: Let_def measure_def inv_image_def) then have ?thesis using prems by auto } moreover { assume nlinj: "linearize j = None" and lini: "∃ li. linearize i = Some li" from nlinj lini have "linearize (Add i j) = None" by (simp add: Let_def measure_def inv_image_def, auto) then have ?thesis using prems by auto } moreover { assume lini: "∃li. linearize i = Some li" and linj: "∃lj. linearize j = Some lj" from lini have lini2: "linearize i ≠ None" by simp from linj have linj2: "linearize j ≠ None" by simp from lini obtain "li" where "linearize i = Some li" by blast from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1) then have linli: "islinintterm li" using prems by simp from linj obtain "lj" where "linearize j = Some lj" by blast from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1) then have linlj: "islinintterm lj" using prems by simp moreover from lini linj have "linearize (Add i j) = Some (lin_add (li,lj))" using prems by (simp add: measure_def inv_image_def) moreover from linli linlj have "I_intterm ats (lin_add (li,lj)) = I_intterm ats (Add li lj)" by (simp add: lin_add_corr) ultimately have ?thesis using prems by simp } ultimately show ?thesis by blast qed next case (5 i j)show ?case proof- have "(linearize i = None) ∨ ((∃ li. linearize i = Some li) ∧ linearize j = None) ∨ ((∃ li. linearize i = Some li) ∧ (∃ lj. linearize j = Some lj))" by auto moreover { assume nlini: "linearize i = None" from nlini have "linearize (Sub i j) = None" by (simp add: Let_def measure_def inv_image_def) then have ?thesis using prems by auto } moreover { assume lini: "∃ li. linearize i = Some li" and nlinj: "linearize j = None" from nlinj lini have "linearize (Sub i j) = None" by (simp add: Let_def measure_def inv_image_def, auto) with prems have ?thesis by auto } moreover { assume lini: "∃li. linearize i = Some li" and linj: "∃lj. linearize j = Some lj" from lini have lini2: "linearize i ≠ None" by simp from linj have linj2: "linearize j ≠ None" by simp from lini obtain "li" where "linearize i = Some li" by blast from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1) with prems have linli: "islinintterm li" by simp from linj obtain "lj" where "linearize j = Some lj" by blast from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1) with prems have linlj: "islinintterm lj" by simp moreover from prems have "linearize (Sub i j) = Some (lin_add (li,lin_neg lj))" by (simp add: measure_def inv_image_def) moreover from linlj have linnlj:"islinintterm (lin_neg lj)" by (simp add: lin_neg_lin) moreover from linli linnlj have "I_intterm ats (lin_add (li,lin_neg lj)) = I_intterm ats (Add li (lin_neg lj))" by (simp only: lin_add_corr[OF linli linnlj]) moreover from linli linlj linnlj have "I_intterm ats (Add li (lin_neg lj)) = I_intterm ats (Sub li lj)" by (simp add: lin_neg_corr) ultimately have ?thesis using prems by simp } ultimately show ?thesis by blast qed next case (6 i j)show ?case proof- have cses: "(linearize i = None) ∨ ((∃ li. linearize i = Some li) ∧ linearize j = None) ∨ ((∃ li. linearize i = Some li) ∧ (∃ bj. linearize j = Some (Cst bj))) ∨ ((∃ bi. linearize i = Some (Cst bi)) ∧ (∃ lj. linearize j = Some lj)) ∨ ((∃ li. linearize i = Some li ∧ ¬ (∃ bi. li = Cst bi)) ∧ (∃ lj. linearize j = Some lj ∧ ¬ (∃ bj. lj = Cst bj)))" by auto moreover { assume nlini: "linearize i = None" from nlini have "linearize (Mult i j) = None" by (simp add: Let_def measure_def inv_image_def) with prems have ?thesis by auto } moreover { assume lini: "∃ li. linearize i = Some li" and nlinj: "linearize j = None" from lini obtain "li" where "linearize i = Some li" by blast moreover from prems have "linearize (Mult i j) = None" by (cases li) (simp_all add: Let_def measure_def inv_image_def) with prems have ?thesis by auto } moreover { assume lini: "∃li. linearize i = Some li" and linj: "∃bj. linearize j = Some (Cst bj)" from lini have lini2: "linearize i ≠ None" by simp from linj have linj2: "linearize j ≠ None" by auto from lini obtain "li" where "linearize i = Some li" by blast from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1) with prems have linli: "islinintterm li" by simp moreover from linj obtain "bj" where "linearize j = Some (Cst bj)" by blast have linlj: "islinintterm (Cst bj)" by simp moreover from prems have "linearize (Mult i j) = Some (lin_mul (bj,li))" by (cases li) (auto simp add: measure_def inv_image_def) then have lm1: "I_intterm ats (the(linearize (Mult i j))) = I_intterm ats (lin_mul (bj,li))" by simp moreover from linli linlj have "I_intterm ats (lin_mul(bj,li)) = I_intterm ats (Mult li (Cst bj))" by (simp add: lin_mul_corr) with prems have "I_intterm ats (lin_mul(bj,li)) = I_intterm ats (Mult li (the (linearize j)))" by auto moreover have "I_intterm ats (Mult li (the (linearize j))) = I_intterm ats (Mult i (the (linearize j)))" using prems by simp moreover have "I_intterm ats i = I_intterm ats (the (linearize i))" using lini2 lini "6.hyps" by simp moreover have "I_intterm ats j = I_intterm ats (the (linearize j))" using prems by (cases li) (auto simp add: measure_def inv_image_def) ultimately have ?thesis by auto } moreover { assume lini: "∃bi. linearize i = Some (Cst bi)" and linj: "∃lj. linearize j = Some lj" from lini have lini2 : "linearize i ≠ None" by auto from linj have linj2 : "linearize j ≠ None" by auto from lini obtain "bi" where "linearize i = Some (Cst bi)" by blast have linli: "islinintterm (Cst bi)" using prems by simp moreover from linj obtain "lj" where "linearize j = Some lj" by blast from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1) then have linlj: "islinintterm lj" by (simp!) moreover from linli lini linj have "linearize (Mult i j) = Some (lin_mul (bi,lj))" apply (simp add: measure_def inv_image_def) apply auto by (case_tac "li::intterm",auto!) then have lm1: "I_intterm ats (the(linearize (Mult i j))) = I_intterm ats (lin_mul (bi,lj))" by simp moreover from linli linlj have "I_intterm ats (lin_mul(bi,lj)) = I_intterm ats (Mult (Cst bi) lj)" by (simp add: lin_mul_corr) then have "I_intterm ats (lin_mul(bi,lj)) = I_intterm ats (Mult (the (linearize i)) lj)" by (auto!) moreover have "I_intterm ats (Mult (the (linearize i)) lj) = I_intterm ats (Mult (the (linearize i)) j)" using lini lini2 by (simp!) moreover have "I_intterm ats i = I_intterm ats (the (linearize i))" using lini2 lini "6.hyps" by simp moreover have "I_intterm ats j = I_intterm ats (the (linearize j))" using linj linj2 lini lini2 linli linlj "6.hyps" by (auto!) ultimately have ?thesis by auto } moreover { assume linc: "∃ li. linearize i = Some li ∧ ¬ (∃ bi. li = Cst bi)" and ljnc: "∃ lj. linearize j = Some lj ∧ ¬ (∃ bj. lj = Cst bj)" from linc obtain "li" where "∃ li. linearize i = Some li ∧ ¬ (∃ bi. li = Cst bi)" by blast moreover from ljnc obtain "lj" where "∃ lj. linearize j = Some lj ∧ ¬ (∃ bj. lj = Cst bj)" by blast ultimately have "linearize (Mult i j) = None" apply (simp add: measure_def inv_image_def) apply (case_tac "linearize i", auto) apply (case_tac a) apply (auto!) by (case_tac "lj",auto)+ then have ?thesis by (simp!) } ultimately show ?thesis by blast qed qed simp_all (* linearize, when successfull, preserves semantics *) lemma linearize_corr: "!! t'. linearize t = Some t' ==> I_intterm ats t = I_intterm ats t' " proof- fix t' assume lint: "linearize t = Some t'" show "I_intterm ats t = I_intterm ats t'" proof- from lint have lt: "linearize t ≠ None" by simp then have "I_intterm ats t = I_intterm ats (the (linearize t))" by (rule_tac linearize_corr1[OF lt]) with lint show ?thesis by simp qed qed (* tries to linearize a formula *) consts linform :: "QF => QF option" primrec "linform (Le it1 it2) = lift_bin(λx. λy. Le (lin_add(x,lin_neg y)) (Cst 0),linearize it1, linearize it2)" "linform (Eq it1 it2) = lift_bin(λx. λy. Eq (lin_add(x,lin_neg y)) (Cst 0),linearize it1, linearize it2)" "linform (Divides d t) = (case linearize d of None => None | Some ld => (case ld of Cst b => (if (b=0) then None else (case linearize t of None => None | Some lt => Some (Divides ld lt))) | _ => None))" "linform T = Some T" "linform F = Some F" "linform (NOT p) = lift_un NOT (linform p)" "linform (And p q)= lift_bin(λf. λg. And f g, linform p, linform q)" "linform (Or p q) = lift_bin(λf. λg. Or f g, linform p, linform q)" (* linearity of formulae *) consts islinform :: "QF => bool" recdef islinform "measure size" "islinform (Le it (Cst i)) = (i=0 ∧ islinintterm it )" "islinform (Eq it (Cst i)) = (i=0 ∧ islinintterm it)" "islinform (Divides (Cst d) t) = (d ≠ 0 ∧ islinintterm t)" "islinform T = True" "islinform F = True" "islinform (NOT (Divides (Cst d) t)) = (d ≠ 0 ∧ islinintterm t)" "islinform (NOT (Eq it (Cst i))) = (i=0 ∧ islinintterm it)" "islinform (And p q)= ((islinform p) ∧ (islinform q))" "islinform (Or p q) = ((islinform p) ∧ (islinform q))" "islinform p = False" (* linform preserves nnf, if successful *) lemma linform_nnf: assumes nnfp: "isnnf p" shows "!! p'. [|linform p = Some p'|] ==> isnnf p'" using nnfp proof (induct p rule: isnnf.induct, simp_all) case (goal1 a b p') show ?case using prems by (cases "linearize a", auto) (cases "linearize b", auto) next case (goal2 a b p') show ?case using prems by (cases "linearize a", auto) (cases "linearize b", auto) next case (goal3 d t p') show ?case using prems apply (cases "linearize d", auto) apply (case_tac "a",auto) apply (case_tac "int=0",auto) by (cases "linearize t",auto) next case (goal4 f g p') show ?case using prems by (cases "linform f", auto) (cases "linform g", auto) next case (goal5 f g p') show ?case using prems by (cases "linform f", auto) (cases "linform g", auto) next case (goal6 d t p') show ?case using prems apply (cases "linearize d", auto) apply (case_tac "a", auto) apply (case_tac "int = 0",auto) by (cases "linearize t", auto) next case (goal7 a b p') show ?case using prems by (cases "linearize a", auto) (cases "linearize b", auto) qed lemma linform_corr: "!! lp. [| isnnf p ; linform p = Some lp |] ==> (qinterp ats p = qinterp ats lp)" proof (induct p rule: linform.induct) case (Le x y) show ?case using "Le.prems" proof- have "(∃ lx ly. linearize x = Some lx ∧ linearize y = Some ly) ∨ (linearize x = None) ∨ (linearize y = None)"by auto moreover { assume linxy: "∃ lx ly. linearize x = Some lx ∧ linearize y = Some ly" from linxy obtain "lx" "ly" where lxly:"linearize x = Some lx ∧ linearize y = Some ly" by blast then have lxeqx: "I_intterm ats x = I_intterm ats lx" by (simp add: linearize_corr) from lxly have lxlin: "islinintterm lx" by (auto simp add: linearize_linear) from lxly have lyeqy: "I_intterm ats y = I_intterm ats ly" by (simp add: linearize_corr) from lxly have lylin: "islinintterm ly" by (auto simp add: linearize_linear) from "prems" have lpeqle: "lp = (Le (lin_add(lx,lin_neg ly)) (Cst 0))" by auto moreover have lin1: "islinintterm (Cst 1)" by simp then have ?thesis using lxlin lylin lin1 lin_add_lin lin_neg_lin "prems" lxly lpeqle by (simp add: lin_add_corr lin_neg_corr lxeqx lyeqy) } moreover { assume "linearize x = None" have ?thesis using "prems" by simp } moreover { assume "linearize y = None" then have ?thesis using "prems" by (case_tac "linearize x", auto) } ultimately show ?thesis by blast qed next case (Eq x y) show ?case using "Eq.prems" proof- have "(∃ lx ly. linearize x = Some lx ∧ linearize y = Some ly) ∨ (linearize x = None) ∨ (linearize y = None)"by auto moreover { assume linxy: "∃ lx ly. linearize x = Some lx ∧ linearize y = Some ly" from linxy obtain "lx" "ly" where lxly:"linearize x = Some lx ∧ linearize y = Some ly" by blast then have lxeqx: "I_intterm ats x = I_intterm ats lx" by (simp add: linearize_corr) from lxly have lxlin: "islinintterm lx" by (auto simp add: linearize_linear) from lxly have lyeqy: "I_intterm ats y = I_intterm ats ly" by (simp add: linearize_corr) from lxly have lylin: "islinintterm ly" by (auto simp add: linearize_linear) from "prems" have lpeqle: "lp = (Eq (lin_add(lx,lin_neg ly)) (Cst 0))" by auto moreover have lin1: "islinintterm (Cst 1)" by simp then have ?thesis using lxlin lylin lin1 lin_add_lin lin_neg_lin "prems" lxly lpeqle by (simp add: lin_add_corr lin_neg_corr lxeqx lyeqy) } moreover { assume "linearize x = None" have ?thesis using "prems" by simp } moreover { assume "linearize y = None" then have ?thesis using "prems" by (case_tac "linearize x", auto) } ultimately show ?thesis by blast qed next case (Divides d t) show ?case using "Divides.prems" apply (case_tac "linearize d",auto) apply (case_tac a, auto) apply (case_tac "int = 0", auto) apply (case_tac "linearize t", auto) apply (simp add: linearize_corr) apply (case_tac a, auto) apply (case_tac "int = 0", auto) by (case_tac "linearize t", auto simp add: linearize_corr) next case (NOT f) show ?case using "prems" proof- have "(∃ lf. linform f = Some lf) ∨ (linform f = None)" by auto moreover { assume linf: "∃ lf. linform f = Some lf" from prems have "isnnf (NOT f)" by simp then have fnnf: "isnnf f" by (cases f) auto from linf obtain "lf" where lf: "linform f = Some lf" by blast then have "lp = NOT lf" using "prems" by auto with "NOT.prems" "NOT.hyps" lf fnnf have ?case by simp } moreover { assume "linform f = None" then have "linform (NOT f) = None" by simp then have ?thesis using "NOT.prems" by simp } ultimately show ?thesis by blast qed next case (Or f g) show ?case using "Or.hyps" proof - have "((∃ lf. linform f = Some lf ) ∧ (∃ lg. linform g = Some lg)) ∨ (linform f = None) ∨ (linform g = None)" by auto moreover { assume linf: "∃ lf. linform f = Some lf" and ling: "∃ lg. linform g = Some lg" from linf obtain "lf" where lf: "linform f = Some lf" by blast from ling obtain "lg" where lg: "linform g = Some lg" by blast from lf lg have "linform (Or f g) = Some (Or lf lg)" by simp then have "lp = Or lf lg" using lf lg "prems" by simp with lf lg "prems" have ?thesis by simp } moreover { assume "linform f = None" then have ?thesis using "Or.prems" by auto } moreover { assume "linform g = None" then have ?thesis using "Or.prems" by (case_tac "linform f", auto) } ultimately show ?thesis by blast qed next case (And f g) show ?case using "And.hyps" proof - have "((∃ lf. linform f = Some lf ) ∧ (∃ lg. linform g = Some lg)) ∨ (linform f = None) ∨ (linform g = None)" by auto moreover { assume linf: "∃ lf. linform f = Some lf" and ling: "∃ lg. linform g = Some lg" from linf obtain "lf" where lf: "linform f = Some lf" by blast from ling obtain "lg" where lg: "linform g = Some lg" by blast from lf lg have "linform (And f g) = Some (And lf lg)" by simp then have "lp = And lf lg" using lf lg "prems" by simp with lf lg "prems" have ?thesis by simp } moreover { assume "linform f = None" then have ?thesis using "And.prems" by auto } moreover { assume "linform g = None" then have ?thesis using "And.prems" by (case_tac "linform f", auto) } ultimately show ?thesis by blast qed qed simp_all (* the result of linform is a linear formula *) lemma linform_lin: "!! lp. [| isnnf p ; linform p = Some lp|] ==> islinform lp" proof (induct p rule: linform.induct) case (Le x y) have "((∃ lx. linearize x = Some lx) ∧ (∃ ly. linearize y = Some ly)) ∨ (linearize x = None) ∨ (linearize y = None) " by clarsimp moreover { assume linx: "∃ lx. linearize x = Some lx" and liny: "∃ ly. linearize y = Some ly" from linx obtain "lx" where lx: "linearize x = Some lx" by blast from liny obtain "ly" where ly: "linearize y = Some ly" by blast from lx have lxlin: "islinintterm lx" by (simp add: linearize_linear) from ly have lylin: "islinintterm ly" by (simp add: linearize_linear) have lin1:"islinintterm (Cst 1)" by simp have lin0: "islinintterm (Cst 0)" by simp from "prems" have "lp = Le (lin_add(lx,lin_neg ly)) (Cst 0)" by auto with lin0 lin1 lxlin lylin "prems" have ?case by (simp add: lin_add_lin lin_neg_lin) } moreover { assume "linearize x = None" then have ?case using "prems" by simp } moreover { assume "linearize y = None" then have ?case using "prems" by (case_tac "linearize x",simp_all) } ultimately show ?case by blast next case (Eq x y) have "((∃ lx. linearize x = Some lx) ∧ (∃ ly. linearize y = Some ly)) ∨ (linearize x = None) ∨ (linearize y = None) " by clarsimp moreover { assume linx: "∃ lx. linearize x = Some lx" and liny: "∃ ly. linearize y = Some ly" from linx obtain "lx" where lx: "linearize x = Some lx" by blast from liny obtain "ly" where ly: "linearize y = Some ly" by blast from lx have lxlin: "islinintterm lx" by (simp add: linearize_linear) from ly have lylin: "islinintterm ly" by (simp add: linearize_linear) have lin1:"islinintterm (Cst 1)" by simp have lin0: "islinintterm (Cst 0)" by simp from "prems" have "lp = Eq (lin_add(lx,lin_neg ly)) (Cst 0)" by auto with lin0 lin1 lxlin lylin "prems" have ?case by (simp add: lin_add_lin lin_neg_lin) } moreover { assume "linearize x = None" then have ?case using "prems" by simp } moreover { assume "linearize y = None" then have ?case using "prems" by (case_tac "linearize x",simp_all) } ultimately show ?case by blast next case (Divides d t) show ?case using prems apply (case_tac "linearize d", auto) apply (case_tac a, auto) apply (case_tac "int = 0", auto) by (case_tac "linearize t",auto simp add: linearize_linear) next case (Or f g) show ?case using "Or.hyps" proof - have "((∃ lf. linform f = Some lf ) ∧ (∃ lg. linform g = Some lg)) ∨ (linform f = None) ∨ (linform g = None)" by auto moreover { assume linf: "∃ lf. linform f = Some lf" and ling: "∃ lg. linform g = Some lg" from linf obtain "lf" where lf: "linform f = Some lf" by blast from ling obtain "lg" where lg: "linform g = Some lg" by blast from lf lg have "linform (Or f g) = Some (Or lf lg)" by simp then have "lp = Or lf lg" using lf lg "prems" by simp with lf lg "prems" have ?thesis by simp } moreover { assume "linform f = None" then have ?thesis using "Or.prems" by auto } moreover { assume "linform g = None" then have ?thesis using "Or.prems" by (case_tac "linform f", auto) } ultimately show ?thesis by blast qed next case (And f g) show ?case using "And.hyps" proof - have "((∃ lf. linform f = Some lf ) ∧ (∃ lg. linform g = Some lg)) ∨ (linform f = None) ∨ (linform g = None)" by auto moreover { assume linf: "∃ lf. linform f = Some lf" and ling: "∃ lg. linform g = Some lg" from linf obtain "lf" where lf: "linform f = Some lf" by blast from ling obtain "lg" where lg: "linform g = Some lg" by blast from lf lg have "linform (And f g) = Some (And lf lg)" by simp then have "lp = And lf lg" using lf lg "prems" by simp with lf lg "prems" have ?thesis by simp } moreover { assume "linform f = None" then have ?thesis using "And.prems" by auto } moreover { assume "linform g = None" then have ?thesis using "And.prems" by (case_tac "linform f", auto) } ultimately show ?thesis by blast qed next case (NOT f) show ?case using "prems" proof- have "(∃ lf. linform f = Some lf) ∨ (linform f = None)" by auto moreover { assume linf: "∃ lf. linform f = Some lf" from prems have "isnnf (NOT f)" by simp then have fnnf: "isnnf f" by (cases f) auto from linf obtain "lf" where lf: "linform f = Some lf" by blast then have "lp = NOT lf" using "prems" by auto with "NOT.prems" "NOT.hyps" lf fnnf have ?thesis using fnnf apply (cases f, auto) prefer 2 apply (case_tac "linearize intterm1",auto) apply (case_tac a, auto) apply (case_tac "int = 0", auto) apply (case_tac "linearize intterm2") apply (auto simp add: linearize_linear) apply (case_tac "linearize intterm1",auto) by (case_tac "linearize intterm2") (auto simp add: linearize_linear lin_add_lin lin_neg_lin) } moreover { assume "linform f = None" then have "linform (NOT f) = None" by simp then have ?thesis using "NOT.prems" by simp } ultimately show ?thesis by blast qed qed (simp_all) (* linform, if successfull, preserves quantifier freeness *) lemma linform_isnnf: "islinform p ==> isnnf p" by (induct p rule: islinform.induct) auto lemma linform_isqfree: "islinform p ==> isqfree p" using linform_isnnf nnf_isqfree by simp lemma linform_qfree: "!! p'. [| isnnf p ; linform p = Some p'|] ==> isqfree p'" using linform_isqfree linform_lin by simp (* Definitions and lemmas about gcd and lcm *) constdefs lcm :: "nat × nat => nat" "lcm ≡ (λ(m,n). m*n div gcd(m,n))" constdefs ilcm :: "int => int => int" "ilcm ≡ λi.λj. int (lcm(nat(abs i),nat(abs j)))" (* ilcm_dvd12 are needed later *) lemma lcm_dvd1: assumes mpos: " m >0" and npos: "n>0" shows "m dvd (lcm(m,n))" proof- have "gcd(m,n) dvd n" by simp then obtain "k" where "n = gcd(m,n) * k" using dvd_def by auto then have "m*n div gcd(m,n) = m*(gcd(m,n)*k) div gcd(m,n)" by (simp add: mult_ac) also have "… = m*k" using mpos npos gcd_zero by simp finally show ?thesis by (simp add: lcm_def) qed lemma lcm_dvd2: assumes mpos: " m >0" and npos: "n>0" shows "n dvd (lcm(m,n))" proof- have "gcd(m,n) dvd m" by simp then obtain "k" where "m = gcd(m,n) * k" using dvd_def by auto then have "m*n div gcd(m,n) = (gcd(m,n)*k)*n div gcd(m,n)" by (simp add: mult_ac) also have "… = n*k" using mpos npos gcd_zero by simp finally show ?thesis by (simp add: lcm_def) qed lemma ilcm_dvd1: assumes anz: "a ≠ 0" and bnz: "b ≠ 0" shows "a dvd (ilcm a b)" proof- let ?na = "nat (abs a)" let ?nb = "nat (abs b)" have nap: "?na >0" using anz by simp have nbp: "?nb >0" using bnz by simp from nap nbp have "?na dvd lcm(?na,?nb)" using lcm_dvd1 by simp thus ?thesis by (simp add: ilcm_def dvd_int_iff) qed lemma ilcm_dvd2: assumes anz: "a ≠ 0" and bnz: "b ≠ 0" shows "b dvd (ilcm a b)" proof- let ?na = "nat (abs a)" let ?nb = "nat (abs b)" have nap: "?na >0" using anz by simp have nbp: "?nb >0" using bnz by simp from nap nbp have "?nb dvd lcm(?na,?nb)" using lcm_dvd2 by simp thus ?thesis by (simp add: ilcm_def dvd_int_iff) qed lemma zdvd_self_abs1: "(d::int) dvd (abs d)" by (case_tac "d <0", simp_all) lemma zdvd_self_abs2: "(abs (d::int)) dvd d" by (case_tac "d<0", simp_all) (* lcm a b is positive for positive a and b *) lemma lcm_pos: assumes mpos: "m > 0" and npos: "n>0" shows "lcm (m,n) > 0" proof(rule ccontr, simp add: lcm_def gcd_zero) assume h:"m*n div gcd(m,n) = 0" from mpos npos have "gcd (m,n) ≠ 0" using gcd_zero by simp hence gcdp: "gcd(m,n) > 0" by simp with h have "m*n < gcd(m,n)" by (cases "m * n < gcd (m, n)") (auto simp add: div_if[OF gcdp, where m="m*n"]) moreover have "gcd(m,n) dvd m" by simp with mpos dvd_imp_le have t1:"gcd(m,n) ≤ m" by simp with npos have t1:"gcd(m,n)*n ≤ m*n" by simp have "gcd(m,n) ≤ gcd(m,n)*n" using npos by simp with t1 have "gcd(m,n) ≤ m*n" by arith ultimately show "False" by simp qed lemma ilcm_pos: assumes apos: " 0 < a" and bpos: "0 < b" shows "0 < ilcm a b" proof- let ?na = "nat (abs a)" let ?nb = "nat (abs b)" have nap: "?na >0" using apos by simp have nbp: "?nb >0" using bpos by simp have "0 < lcm (?na,?nb)" by (rule lcm_pos[OF nap nbp]) thus ?thesis by (simp add: ilcm_def) qed (* fomlcm computes the lcm of all c, where c is the coeffitient of Var 0 *) consts formlcm :: "QF => int" recdef formlcm "measure size" "formlcm (Le (Add (Mult (Cst c) (Var 0)) r) (Cst i)) = abs c " "formlcm (Eq (Add (Mult (Cst c) (Var 0)) r) (Cst i)) = abs c " "formlcm (Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) = abs c" "formlcm (NOT p) = formlcm p" "formlcm (And p q)= ilcm (formlcm p) (formlcm q)" "formlcm (Or p q) = ilcm (formlcm p) (formlcm q)" "formlcm p = 1" (* the property that formlcm should fullfill *) consts divideallc:: "int × QF => bool" recdef divideallc "measure (λ(i,p). size p)" "divideallc (l,Le (Add (Mult (Cst c) (Var 0)) r) (Cst i)) = (c dvd l)" "divideallc (l,Eq (Add (Mult (Cst c) (Var 0)) r) (Cst i)) = (c dvd l)" "divideallc(l,Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) = (c dvd l)" "divideallc (l,NOT p) = divideallc(l,p)" "divideallc (l,And p q) = (divideallc (l,p) ∧ divideallc (l,q))" "divideallc (l,Or p q) = (divideallc (l,p) ∧ divideallc (l,q))" "divideallc p = True" (* formlcm retuns a positive integer *) lemma formlcm_pos: assumes linp: "islinform p" shows "0 < formlcm p" using linp proof (induct p rule: formlcm.induct, simp_all add: ilcm_pos) case (goal1 c r i) have "i=0 ∨ i ≠ 0" by simp moreover { assume "i ≠ 0" then have ?case using prems by simp } moreover { assume iz: "i = 0" then have "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp then have "c≠0" using prems by (simp add: islininttermc0r[where c="c" and n="0" and r="r"]) then have ?case by simp } ultimately show ?case by blast next case (goal2 c r i) have "i=0 ∨ i ≠ 0" by simp moreover { assume "i ≠ 0" then have ?case using prems by simp } moreover { assume iz: "i = 0" then have "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp then have "c≠0" using prems by (simp add: islininttermc0r[where c="c" and n="0" and r="r"]) then have ?case by simp } ultimately show ?case by blast next case (goal3 d c r) show ?case using prems by (simp add: islininttermc0r[where c="c" and n="0" and r="r"]) next case (goal4 f) show ?case using prems by (cases f,auto) (case_tac "intterm2", auto,case_tac "intterm1", auto) qed lemma divideallc_mono: "!! c. [| divideallc(c,p) ; c dvd d|] ==> divideallc (d,p)" proof (induct d p rule: divideallc.induct, simp_all) case (goal1 l a b) show ?case by ( rule zdvd_trans [where m="a" and n="b" and k="l"]) next case (goal2 l a b) show ?case by ( rule zdvd_trans [where m="a" and n="b" and k="l"]) next case (goal3 l a b) show ?case by ( rule zdvd_trans [where m="a" and n="b" and k="l"]) next case (goal4 l f g k) have "divideallc (l,g)" using prems by clarsimp moreover have "divideallc (l,f)" using prems by clarsimp ultimately show ?case by simp next case (goal5 l f g k) have "divideallc (l,g)" using prems by clarsimp moreover have "divideallc (l,f)" using prems by clarsimp ultimately show ?case by simp qed (* fomlcm retuns a number all coeffitients of Var 0 divide *) lemma formlcm_divideallc: assumes linp: "islinform p" shows "divideallc(formlcm p, p)" using linp proof (induct p rule: formlcm.induct, simp_all add: zdvd_self_abs1) case (goal1 f) show ?case using prems by (cases f,auto) (case_tac "intterm2", auto, case_tac "intterm1",auto) next case (goal2 f g) have "formlcm f >0" using formlcm_pos prems by simp hence "formlcm f ≠ 0" by simp moreover have "formlcm g > 0" using formlcm_pos prems by simp hence "formlcm g ≠ 0" by simp ultimately show ?case using prems formlcm_pos by (simp add: ilcm_dvd1 ilcm_dvd2 divideallc_mono[where c="formlcm f" and d="ilcm (formlcm f) (formlcm g)"] divideallc_mono[where c="formlcm g" and d="ilcm (formlcm f) (formlcm g)"]) next case (goal3 f g) have "formlcm f >0" using formlcm_pos prems by simp hence "formlcm f ≠ 0" by simp moreover have "formlcm g > 0" using formlcm_pos prems by simp hence "formlcm g ≠ 0" by simp ultimately show ?case using prems by (simp add: ilcm_dvd1 ilcm_dvd2 divideallc_mono[where c="formlcm f" and d="ilcm (formlcm f) (formlcm g)"] divideallc_mono[where c="formlcm g" and d="ilcm (formlcm f) (formlcm g)"]) qed (* adjustcoeff transforms the formula given an l , look at correctness thm*) consts adjustcoeff :: "int × QF => QF" recdef adjustcoeff "measure (λ(l,p). size p)" "adjustcoeff (l,(Le (Add (Mult (Cst c) (Var 0)) r) (Cst i))) = (if c≤0 then Le (Add (Mult (Cst -1) (Var 0)) (lin_mul (- (l div c), r))) (Cst (0::int)) else Le (Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r))) (Cst (0::int)))" "adjustcoeff (l,(Eq (Add (Mult (Cst c) (Var 0)) r) (Cst i))) = (Eq (Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r))) (Cst (0::int)))" "adjustcoeff (l,Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) = Divides (Cst ((l div c) * d)) (Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r)))" "adjustcoeff (l,NOT (Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r))) = NOT (Divides (Cst ((l div c) * d)) (Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r))))" "adjustcoeff (l,(NOT(Eq (Add (Mult (Cst c) (Var 0)) r) (Cst i)))) = (NOT(Eq (Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r))) (Cst (0::int))))" "adjustcoeff (l,And p q) = And (adjustcoeff (l,p)) (adjustcoeff(l,q))" "adjustcoeff (l,Or p q) = Or (adjustcoeff (l,p)) (adjustcoeff(l,q))" "adjustcoeff (l,p) = p" (* unitycoeff expects a quantifier free formula an transforms it to an equivalent formula where the bound variable occurs only with coeffitient 1 or -1 *) constdefs unitycoeff :: "QF => QF" "unitycoeff p == (let l = formlcm p; p' = adjustcoeff (l,p) in (if l=1 then p' else (And (Divides (Cst l) (Add (Mult (Cst 1) (Var 0)) (Cst 0))) p')))" (* what is a unified formula *) consts isunified :: "QF => bool" recdef isunified "measure size" "isunified (Le (Add (Mult (Cst i) (Var 0)) r) (Cst z)) = ((abs i) = 1 ∧ (islinform(Le (Add (Mult (Cst i) (Var 0)) r) (Cst z))))" "isunified (Eq (Add (Mult (Cst i) (Var 0)) r) (Cst z)) = ((abs i) = 1 ∧ (islinform(Le (Add (Mult (Cst i) (Var 0)) r) (Cst z))))" "isunified (NOT(Eq (Add (Mult (Cst i) (Var 0)) r) (Cst z))) = ((abs i) = 1 ∧ (islinform(Le (Add (Mult (Cst i) (Var 0)) r) (Cst z))))" "isunified (Divides (Cst d) (Add (Mult (Cst i) (Var 0)) r)) = ((abs i) = 1 ∧ (islinform(Divides (Cst d) (Add (Mult (Cst i) (Var 0)) r))))" "isunified (NOT(Divides (Cst d) (Add (Mult (Cst i) (Var 0)) r))) = ((abs i) = 1 ∧ (islinform(NOT(Divides (Cst d) (Add (Mult (Cst i) (Var 0)) r)))))" "isunified (And p q) = (isunified p ∧ isunified q)" "isunified (Or p q) = (isunified p ∧ isunified q)" "isunified p = islinform p" lemma unified_islinform: "isunified p ==> islinform p" by (induct p rule: isunified.induct) auto lemma adjustcoeff_lenpos: "0 < n ==> adjustcoeff (l, Le (Add (Mult (Cst i) (Var n)) r) (Cst c)) = Le (Add (Mult (Cst i) (Var n)) r) (Cst c)" by (cases n, auto) lemma adjustcoeff_eqnpos: "0 < n ==> adjustcoeff (l, Eq (Add (Mult (Cst i) (Var n)) r) (Cst c)) = Eq (Add (Mult (Cst i) (Var n)) r) (Cst c)" by (cases n, auto) (* Properties of adjustcoeff and unitycoeff *) (* Some simple lemmas used afterwards *) lemma zmult_zle_mono: "(i::int) ≤ j ==> 0 ≤ k ==> k * i ≤ k * j" apply (erule order_le_less [THEN iffD1, THEN disjE, of "0::int"]) apply (erule order_le_less [THEN iffD1, THEN disjE]) apply (rule order_less_imp_le) apply (rule zmult_zless_mono2) apply simp_all done lemma zmult_zle_mono_eq: assumes kpos: "0 < k" shows "((i::int) ≤ j) = (k*i ≤ k*j)" (is "?P = ?Q") proof assume P: ?P from kpos have kge0: "0 ≤ k" by simp show ?Q by (rule zmult_zle_mono[OF P kge0]) next assume ?Q then have "k*i - k*j ≤ 0" by simp then have le1: "k*(i-j) ≤ k*0" by (simp add: zdiff_zmult_distrib2) have "i -j ≤ 0" by (rule mult_left_le_imp_le[OF le1 kpos]) then show ?P by simp qed lemma adjustcoeff_le_corr: assumes lpos: "0 < l" and ipos: "0 < (i::int)" and dvd: "i dvd l" shows "(i*x + r ≤ 0) = (l*x + ((l div i)*r) ≤ 0)" proof- from lpos ipos have ilel: "i≤l" by (simp add: zdvd_imp_le [OF dvd lpos]) from ipos have inz: "i ≠ 0" by simp have "i div i≤ l div i" by (simp add: zdiv_mono1[OF ilel ipos]) then have ldivipos:"0 < l div i" by (simp add: zdiv_self[OF inz]) from dvd have "∃i'. i*i' = l" by (auto simp add: dvd_def) then obtain "i'" where ii'eql: "i*i' = l" by blast have "(i * x + r ≤ 0) = (l div i * (i * x + r) ≤ l div i * 0)" by (rule zmult_zle_mono_eq[OF ldivipos, where i="i*x + r" and j="0"]) also have "(l div i * (i * x + r) ≤ l div i * 0) = ((l div i * i) * x + ((l div i)*r) ≤ 0)" by (simp add: mult_ac) also have "((l div i * i) * x + ((l div i)*r) ≤ 0) = (l*x + ((l div i)*r) ≤ 0)" using sym[OF ii'eql] inz by (simp add: zmult_ac) finally show ?thesis by simp qed lemma adjustcoeff_le_corr2: assumes lpos: "0 < l" and ineg: "(i::int) < 0" and dvd: "i dvd l" shows "(i*x + r ≤ 0) = ((-l)*x + ((-(l div i))*r) ≤ 0)" proof- from dvd have midvdl: "-i dvd l" by simp from ineg have mipos: "0 < -i" by simp from lpos ineg have milel: "-i≤l" by (simp add: zdvd_imp_le [OF midvdl lpos]) from ineg have inz: "i ≠ 0" by simp have "l div i≤ -i div i" by (simp add: zdiv_mono1_neg[OF milel ineg]) then have "l div i ≤ -1" apply (simp add: zdiv_zminus1_eq_if[OF inz, where a="i"]) by (simp add: zdiv_self[OF inz]) then have ldivineg: "l div i < 0" by simp then have mldivipos: "0 < - (l div i)" by simp from dvd have "∃i'. i*i' = l" by (auto simp add: dvd_def) then obtain "i'" where ii'eql: "i*i' = l" by blast have "(i * x + r ≤ 0) = (- (l div i) * (i * x + r) ≤ - (l div i) * 0)" by (rule zmult_zle_mono_eq[OF mldivipos, where i="i*x + r" and j="0"]) also have "(- (l div i) * (i * x + r) ≤ - (l div i) * 0) = (-((l div i) * i) * x ≤ (l div i)*r)" by (simp add: mult_ac) also have " (-((l div i) * i) * x ≤ (l div i)*r) = (- (l*x) ≤ (l div i)*r)" using sym[OF ii'eql] inz by (simp add: zmult_ac) finally show ?thesis by simp qed (* FIXME : Move this theorem above, it simplifies the 2 theorems above : adjustcoeff_le_corr1,2 *) lemma dvd_div_pos: assumes bpos: "0 < (b::int)" and anz: "a≠0" and dvd: "a dvd b" shows "(b div a)*a = b" proof- from anz have "0 < a ∨ a < 0" by arith moreover { assume apos: "0 < a" from bpos apos have aleb: "a≤b" by (simp add: zdvd_imp_le [OF dvd bpos]) have "a div a≤ b div a" by (simp add: zdiv_mono1[OF aleb apos]) then have bdivapos:"0 < b div a" by (simp add: zdiv_self[OF anz]) from dvd have "∃a'. a*a' = b" by (auto simp add: dvd_def) then obtain "a'" where aa'eqb: "a*a' = b" by blast then have ?thesis using anz sym[OF aa'eqb] by simp } moreover { assume aneg: "a < 0" from dvd have midvdb: "-a dvd b" by simp from aneg have mapos: "0 < -a" by simp from bpos aneg have maleb: "-a≤b" by (simp add: zdvd_imp_le [OF midvdb bpos]) from aneg have anz: "a ≠ 0" by simp have "b div a≤ -a div a" by (simp add: zdiv_mono1_neg[OF maleb aneg]) then have "b div a ≤ -1" apply (simp add: zdiv_zminus1_eq_if[OF anz, where a="a"]) by (simp add: zdiv_self[OF anz]) then have bdivaneg: "b div a < 0" by simp then have mbdivapos: "0 < - (b div a)" by simp from dvd have "∃a'. a*a' = b" by (auto simp add: dvd_def) then obtain "a'" where aa'eqb: "a*a' = b" by blast then have ?thesis using anz sym[OF aa'eqb] by (simp) } ultimately show ?thesis by blast qed lemma adjustcoeff_eq_corr: assumes lpos: "(0::int) < l" and inz: "i ≠ 0" and dvd: "i dvd l" shows "(i*x + r = 0) = (l*x + ((l div i)*r) = 0)" proof- have ldvdii: "(l div i)*i = l" by (rule dvd_div_pos[OF lpos inz dvd]) have ldivinz: "l div i ≠ 0" using inz ldvdii lpos by auto have "(i*x + r = 0) = ((l div i)*(i*x + r) = (l div i)*0)" using ldivinz by arith also have "… = (((l div i)*i)*x + (l div i)*r = 0)" by (simp add: zmult_ac) finally show ?thesis using ldvdii by simp qed (* Correctness theorem for adjustcoeff *) lemma adjustcoeff_corr: assumes linp: "islinform p" and alldvd: "divideallc (l,p)" and lpos: "0 < l" shows "qinterp (a#ats) p = qinterp ((a*l)#ats) (adjustcoeff(l, p))" using linp alldvd proof (induct p rule: islinform.induct,simp_all) case (goal1 t c) from prems have cz: "c=0" by simp then have ?case using prems proof(induct t rule: islinintterm.induct) case (2 i n i') show ?case using prems proof- from prems have "i≠0" by simp then have "(n=0 ∧ i < 0) ∨ (n=0 ∧ i > 0) ∨ n≠0" by arith moreover { assume "n≠0" then have ?thesis by (simp add: nth_pos2 adjustcoeff_lenpos) } moreover { assume nz: "n=0" and ipos: "0 < i" from prems nz have idvdl: "i dvd l" by simp have "(i*a + i' ≤ 0) = (l*a+ ((l div i)*i') ≤ 0)" by (rule adjustcoeff_le_corr[OF lpos ipos idvdl]) then have ?thesis using prems by (simp add: mult_ac) } moreover { assume nz: "n=0" and ineg: "i < 0" from prems nz have idvdl: "i dvd l" by simp have "(i*a+i' ≤ 0) = (-l*a + (-(l div i) * i') ≤ 0)" by (rule adjustcoeff_le_corr2[OF lpos ineg idvdl]) then have ?thesis using prems by (simp add: zmult_ac) } ultimately show ?thesis by blast qed next case (3 i n i' n' r) show ?case using prems proof- from prems have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp then have "islint (Add (Mult (Cst i') (Var n')) (r))" by (simp add: islinintterm_eq_islint) then have linr: "islintn(Suc n',r)" by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def) from lininrp have linr2: "islinintterm r" by (simp add: islinintterm_subt[OF lininrp]) from prems have "n < n'" by simp then have nppos: "0 < n'" by simp from prems have "i≠0" by simp then have "(n=0 ∧ i < 0) ∨ (n=0 ∧ i > 0) ∨ n≠0" by arith moreover { assume nnz: "n≠0" from linr have ?thesis using nppos nnz intterm_novar0[OF lininrp] prems apply (simp add: adjustcoeff_lenpos linterm_novar0[OF linr, where x="a" and y="a*l"]) by (simp add: nth_pos2) } moreover { assume nz: "n=0" and ipos: "0 < i" from prems nz have idvdl: "i dvd l" by simp have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) ≤ 0) = (l * a + l div i * (i' * (a # ats) ! n' + I_intterm (a # ats) r) ≤ 0)" by (rule adjustcoeff_le_corr[OF lpos ipos idvdl]) then have ?thesis using prems linr linr2 by (simp add: mult_ac nth_pos2 lin_mul_corr linterm_novar0[OF linr, where x="a" and y="a*l"]) } moreover { assume nz: "n=0" and ineg: "i < 0" from prems nz have idvdl: "i dvd l" by simp have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) ≤ 0) = (- l * a + - (l div i) * (i' * (a # ats) ! n' + I_intterm (a # ats) r) ≤ 0)" by (rule adjustcoeff_le_corr2[OF lpos ineg idvdl, where x="a" and r="(i'* (a#ats) ! n' + I_intterm (a#ats) r )"]) then have ?thesis using prems linr linr2 by (simp add: zmult_ac nth_pos2 lin_mul_corr linterm_novar0[OF linr, where x="a" and y="a*l"] ) } ultimately show ?thesis by blast qed qed simp_all then show ?case by simp next case (goal2 t c) from prems have cz: "c=0" by simp then have ?case using prems proof(induct t rule: islinintterm.induct) case (2 i n i') show ?case using prems proof- from prems have inz: "i≠0" by simp then have "n=0 ∨ n≠0" by arith moreover { assume "n≠0" then have ?thesis by (simp add: nth_pos2 adjustcoeff_eqnpos) } moreover { assume nz: "n=0" from prems nz have idvdl: "i dvd l" by simp have "(i*a + i' = 0) = (l*a+ ((l div i)*i') = 0)" by (rule adjustcoeff_eq_corr[OF lpos inz idvdl]) then have ?thesis using prems by (simp add: mult_ac) } ultimately show ?thesis by blast qed next case (3 i n i' n' r) show ?case using prems proof- from prems have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp then have "islint (Add (Mult (Cst i') (Var n')) (r))" by (simp add: islinintterm_eq_islint) then have linr: "islintn(Suc n',r)" by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def) from lininrp have linr2: "islinintterm r" by (simp add: islinintterm_subt[OF lininrp]) from prems have "n < n'" by simp then have nppos: "0 < n'" by simp from prems have "i≠0" by simp then have "n=0 ∨ n≠0" by arith moreover { assume nnz: "n≠0" from linr have ?thesis using nppos nnz intterm_novar0[OF lininrp] prems apply (simp add: adjustcoeff_eqnpos linterm_novar0[OF linr, where x="a" and y="a*l"]) by (simp add: nth_pos2) } moreover { assume nz: "n=0" from prems have inz: "i ≠ 0" by auto from prems nz have idvdl: "i dvd l" by simp have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0) = (l * a + l div i * (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0)" by (rule adjustcoeff_eq_corr[OF lpos inz idvdl]) then have ?thesis using prems linr linr2 by (simp add: mult_ac nth_pos2 lin_mul_corr linterm_novar0[OF linr, where x="a" and y="a*l"]) } ultimately show ?thesis by blast qed qed simp_all then show ?case by simp next case (goal3 d t) show ?case using prems proof (induct t rule: islinintterm.induct) case (2 i n i') have "n=0 ∨ (∃m. (n = Suc m))" by arith moreover { assume "∃m. n = Suc m" then have ?case using prems by auto } moreover { assume nz: "n=0" from prems have inz: "i≠0" by simp from prems have idvdl: "i dvd l" by simp have ldiviieql: "l div i * i = l" by (rule dvd_div_pos[OF lpos inz idvdl]) with lpos have ldivinz: "0 ≠ l div i" by auto then have ?case using prems apply simp apply (simp add: ac_dvd_eq[OF ldivinz, where m="d" and c="i" and n="a" and t="i'"] ldiviieql) by (simp add: zmult_commute) } ultimately show ?case by blast next case (3 i n i' n' r) from prems have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp then have "islint (Add (Mult (Cst i') (Var n')) (r))" by (simp add: islinintterm_eq_islint) then have linr: "islintn(Suc n',r)" by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def) from lininrp have linr2: "islinintterm r" by (simp add: islinintterm_subt[OF lininrp]) from prems have "n < n'" by simp then have nppos: "0 < n'" by simp from prems have inz: "i≠0" by simp have "n=0 ∨ (∃m. (n = Suc m))" by arith moreover { assume "∃m. n = Suc m" then have npos: "0 < n" by arith have ?case using nppos intterm_novar0[OF lininrp] prems apply (auto simp add: linterm_novar0[OF linr, where x="a" and y="a*l"]) by (simp_all add: nth_pos2) } moreover { assume nz: "n=0" from prems have idvdl: "i dvd l" by simp have ldiviieql: "l div i * i = l" by (rule dvd_div_pos[OF lpos inz idvdl]) with lpos have ldivinz: "0 ≠ l div i" by auto then have ?case using prems linr2 linr apply (simp add: nth_pos2 lin_mul_corr linterm_novar0) apply (simp add: ac_dvd_eq[OF ldivinz, where m="d" and c="i" and n="a" and t="(i' * ats ! (n' - Suc 0) + I_intterm (a # ats) r)"] ldiviieql) by (simp add: zmult_ac linterm_novar0[OF linr, where x="a" and y="a*l"]) } ultimately show ?case by blast qed simp_all next case (goal4 d t) show ?case using prems proof (induct t rule: islinintterm.induct) case (2 i n i') have "n=0 ∨ (∃m. (n = Suc m))" by arith moreover { assume "∃m. n = Suc m" then have ?case using prems by auto } moreover { assume nz: "n=0" from prems have inz: "i≠0" by simp from prems have idvdl: "i dvd l" by simp have ldiviieql: "l div i * i = l" by (rule dvd_div_pos[OF lpos inz idvdl]) with lpos have ldivinz: "0 ≠ l div i" by auto then have ?case using prems apply simp apply (simp add: ac_dvd_eq[OF ldivinz, where m="d" and c="i" and n="a" and t="i'"] ldiviieql) by (simp add: zmult_commute) } ultimately show ?case by blast next case (3 i n i' n' r) from prems have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp then have "islint (Add (Mult (Cst i') (Var n')) (r))" by (simp add: islinintterm_eq_islint) then have linr: "islintn(Suc n',r)" by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def) from lininrp have linr2: "islinintterm r" by (simp add: islinintterm_subt[OF lininrp]) from prems have "n < n'" by simp then have nppos: "0 < n'" by simp from prems have inz: "i≠0" by simp have "n=0 ∨ (∃m. (n = Suc m))" by arith moreover { assume "∃m. n = Suc m" then have npos: "0 < n" by arith have ?case using nppos intterm_novar0[OF lininrp] prems apply (auto simp add: linterm_novar0[OF linr, where x="a" and y="a*l"]) by (simp_all add: nth_pos2) } moreover { assume nz: "n=0" from prems have idvdl: "i dvd l" by simp have ldiviieql: "l div i * i = l" by (rule dvd_div_pos[OF lpos inz idvdl]) with lpos have ldivinz: "0 ≠ l div i" by auto then have ?case using prems linr2 linr apply (simp add: nth_pos2 lin_mul_corr linterm_novar0) apply (simp add: ac_dvd_eq[OF ldivinz, where m="d" and c="i" and n="a" and t="(i' * ats ! (n' - Suc 0) + I_intterm (a # ats) r)"] ldiviieql) by (simp add: zmult_ac linterm_novar0[OF linr, where x="a" and y="a*l"]) } ultimately show ?case by blast qed simp_all next case (goal5 t c) from prems have cz: "c=0" by simp then have ?case using prems proof(induct t rule: islinintterm.induct) case (2 i n i') show ?case using prems proof- from prems have inz: "i≠0" by simp then have "n=0 ∨ n≠0" by arith moreover { assume "n≠0" then have ?thesis using prems by (cases n, simp_all) } moreover { assume nz: "n=0" from prems nz have idvdl: "i dvd l" by simp have "(i*a + i' = 0) = (l*a+ ((l div i)*i') = 0)" by (rule adjustcoeff_eq_corr[OF lpos inz idvdl]) then have ?thesis using prems by (simp add: mult_ac) } ultimately show ?thesis by blast qed next case (3 i n i' n' r) show ?case using prems proof- from prems have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp then have "islint (Add (Mult (Cst i') (Var n')) (r))" by (simp add: islinintterm_eq_islint) then have linr: "islintn(Suc n',r)" by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def) from lininrp have linr2: "islinintterm r" by (simp add: islinintterm_subt[OF lininrp]) from prems have "n < n'" by simp then have nppos: "0 < n'" by simp from prems have "i≠0" by simp then have "n=0 ∨ n≠0" by arith moreover { assume nnz: "n≠0" then have ?thesis using prems linr nppos nnz intterm_novar0[OF lininrp] by (cases n, simp_all) (simp add: nth_pos2 linterm_novar0[OF linr, where x="a" and y="a*l"]) } moreover { assume nz: "n=0" from prems have inz: "i ≠ 0" by auto from prems nz have idvdl: "i dvd l" by simp have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0) = (l * a + l div i * (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0)" by (rule adjustcoeff_eq_corr[OF lpos inz idvdl]) then have ?thesis using prems linr linr2 by (simp add: mult_ac nth_pos2 lin_mul_corr linterm_novar0[OF linr, where x="a" and y="a*l"]) } ultimately show ?thesis by blast qed qed simp_all then show ?case by simp qed (* unitycoeff preserves semantics *) lemma unitycoeff_corr: assumes linp: "islinform p" shows "qinterp ats (QEx p) = qinterp ats (QEx (unitycoeff p))" proof- have lpos: "0 < formlcm p" by (rule formlcm_pos[OF linp]) have dvd : "divideallc (formlcm p, p)" by (rule formlcm_divideallc[OF linp]) show ?thesis using prems lpos dvd proof (simp add: unitycoeff_def Let_def,case_tac "formlcm p = 1", simp_all add: adjustcoeff_corr) show "(∃x. qinterp (x * formlcm p # ats) (adjustcoeff (formlcm p, p))) = (∃x. formlcm p dvd x ∧ qinterp (x # ats) (adjustcoeff (formlcm p, p)))" (is "(∃x. ?P(x* (formlcm p))) = (∃x. formlcm p dvd x ∧ ?P x)") proof- have "(∃x. ?P(x* (formlcm p))) = (∃x. ?P((formlcm p)*x))" by (simp add: mult_commute) also have "(∃x. ?P((formlcm p)*x)) = (∃x. (formlcm p dvd x) ∧ ?P x)" by (simp add: unity_coeff_ex[where P="?P"]) finally show ?thesis by simp qed qed qed (* the resul of adjustcoeff is unified for all l with divideallc (l,p) *) lemma adjustcoeff_unified: assumes linp: "islinform p" and dvdc: "divideallc(l,p)" and lpos: "l > 0" shows "isunified (adjustcoeff(l, p))" using linp dvdc lpos proof(induct l p rule: adjustcoeff.induct,simp_all add: lin_mul_lintn islinintterm_eq_islint islint_def) case (goal1 l d c r) from prems have "c >0 ∨ c < 0" by auto moreover { assume cpos: "c > 0 " from prems have lp: "l > 0" by simp from prems have cdvdl: "c dvd l" by simp have clel: "c ≤ l" by (rule zdvd_imp_le[OF cdvdl lp]) have "c div c ≤ l div c" by (rule zdiv_mono1[OF clel cpos]) then have ?case using cpos by (simp add: zdiv_self) } moreover { assume cneg: "c < 0" have mcpos: "-c > 0" by simp then have mcnz: "-c ≠ 0" by simp from prems have mcdvdl: "-c dvd l" by simp then have l1:"l mod -c = 0" by (simp add: zdvd_iff_zmod_eq_0) from prems have lp: "l >0" by simp have mclel: "-c ≤ l" by (rule zdvd_imp_le[OF mcdvdl lp]) have "l div c = (-l div -c)" by simp also have "… = - (l div -c)" using l1 by (simp only: zdiv_zminus1_eq_if[OF mcnz, where a="l"]) simp finally have diveq: "l div c = - (l div -c)" by simp have "-c div -c ≤ l div -c" by (rule zdiv_mono1[OF mclel mcpos]) then have "0 < l div -c" using cneg by (simp add: zdiv_self) then have ?case using diveq by simp } ultimately show ?case by blast next case (goal2 l p) from prems have "c >0 ∨ c < 0" by auto moreover { assume cpos: "c > 0 " from prems have lp: "l > 0" by simp from prems have cdvdl: "c dvd l" by simp have clel: "c ≤ l" by (rule zdvd_imp_le[OF cdvdl lp]) have "c div c ≤ l div c" by (rule zdiv_mono1[OF clel cpos]) then have ?case using cpos by (simp add: zdiv_self) } moreover { assume cneg: "c < 0" have mcpos: "-c > 0" by simp then have mcnz: "-c ≠ 0" by simp from prems have mcdvdl: "-c dvd l" by simp then have l1:"l mod -c = 0" by (simp add: zdvd_iff_zmod_eq_0) from prems have lp: "l >0" by simp have mclel: "-c ≤ l" by (rule zdvd_imp_le[OF mcdvdl lp]) have "l div c = (-l div -c)" by simp also have "… = - (l div -c)" using l1 by (simp only: zdiv_zminus1_eq_if[OF mcnz, where a="l"]) simp finally have diveq: "l div c = - (l div -c)" by simp have "-c div -c ≤ l div -c" by (rule zdiv_mono1[OF mclel mcpos]) then have "0 < l div -c" using cneg by (simp add: zdiv_self) then have ?case using diveq by simp } ultimately show ?case by blast qed lemma adjustcoeff_lcm_unified: assumes linp: "islinform p" shows "isunified (adjustcoeff(formlcm p, p))" using linp adjustcoeff_unified formlcm_pos formlcm_divideallc by simp (* the result of unitycoeff is unified *) lemma unitycoeff_unified: assumes linp: "islinform p" shows "isunified (unitycoeff p)" using linp formlcm_pos[OF linp] proof (auto simp add: unitycoeff_def Let_def adjustcoeff_lcm_unified) assume f1: "formlcm p = 1" have "isunified (adjustcoeff(formlcm p, p))" by (rule adjustcoeff_lcm_unified[OF linp]) with f1 show "isunified (adjustcoeff(1,p))" by simp qed lemma unified_isnnf: assumes unifp: "isunified p" shows "isnnf p" using unified_islinform[OF unifp] linform_isnnf by simp lemma unified_isqfree: "isunified p==> isqfree p" using unified_islinform linform_isqfree by auto (* Plus/Minus infinity , B and A set definitions *) consts minusinf :: "QF => QF" plusinf :: "QF => QF" aset :: "QF => intterm list" bset :: "QF => intterm list" recdef minusinf "measure size" "minusinf (Le (Add (Mult (Cst c) (Var 0)) r) z) = (if c < 0 then F else T)" "minusinf (Eq (Add (Mult (Cst c) (Var 0)) r) z) = F" "minusinf (NOT(Eq (Add (Mult (Cst c) (Var 0)) r) z)) = T" "minusinf (And p q) = And (minusinf p) (minusinf q)" "minusinf (Or p q) = Or (minusinf p) (minusinf q)" "minusinf p = p" recdef plusinf "measure size" "plusinf (Le (Add (Mult (Cst c) (Var 0)) r) z) = (if c < 0 then T else F)" "plusinf (Eq (Add (Mult (Cst c) (Var 0)) r) z) = F" "plusinf (NOT (Eq (Add (Mult (Cst c) (Var 0)) r) z)) = T" "plusinf (And p q) = And (plusinf p) (plusinf q)" "plusinf (Or p q) = Or (plusinf p) (plusinf q)" "plusinf p = p" recdef bset "measure size" "bset (Le (Add (Mult (Cst c) (Var 0)) r) z) = (if c < 0 then [lin_add(r,(Cst -1)), r] else [lin_add(lin_neg r,(Cst -1))])" "bset (Eq (Add (Mult (Cst c) (Var 0)) r) z) = (if c < 0 then [lin_add(r,(Cst -1))] else [lin_add(lin_neg r,(Cst -1))])" "bset (NOT(Eq (Add (Mult (Cst c) (Var 0)) r) z)) = (if c < 0 then [r] else [lin_neg r])" "bset (And p q) = (bset p) @ (bset q)" "bset (Or p q) = (bset p) @ (bset q)" "bset p = []" recdef aset "measure size" "aset (Le (Add (Mult (Cst c) (Var 0)) r) z) = (if c < 0 then [lin_add (r, Cst 1)] else [lin_add (lin_neg r, Cst 1), lin_neg r])" "aset (Eq (Add (Mult (Cst c) (Var 0)) r) z) = (if c < 0 then [lin_add(r,(Cst 1))] else [lin_add(lin_neg r,(Cst 1))])" "aset (NOT(Eq (Add (Mult (Cst c) (Var 0)) r) z)) = (if c < 0 then [r] else [lin_neg r])" "aset (And p q) = (aset p) @ (aset q)" "aset (Or p q) = (aset p) @ (aset q)" "aset p = []" (* divlcm computes δ = lcm d , where d | x +t occurs in p *) consts divlcm :: "QF => int" recdef divlcm "measure size" "divlcm (Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) = (abs d)" "divlcm (NOT p) = divlcm p" "divlcm (And p q)= ilcm (divlcm p) (divlcm q)" "divlcm (Or p q) = ilcm (divlcm p) (divlcm q)" "divlcm p = 1" (* the preoperty of δ *) consts alldivide :: "int × QF => bool" recdef alldivide "measure (%(d,p). size p)" "alldivide (d,(Divides (Cst d') (Add (Mult (Cst c) (Var 0)) r))) = (d' dvd d)" "alldivide (d,(NOT p)) = alldivide (d,p)" "alldivide (d,(And p q)) = (alldivide (d,p) ∧ alldivide (d,q))" "alldivide (d,(Or p q)) = ((alldivide (d,p)) ∧ (alldivide (d,q)))" "alldivide (d,p) = True" (* alldivide is monotone *) lemma alldivide_mono: "!! d'. [| alldivide (d,p) ; d dvd d'|] ==> alldivide (d',p)" proof(induct d p rule: alldivide.induct, simp_all add: ilcm_dvd1 ilcm_dvd2) fix "d1" "d2" "d3" assume th1:"d2 dvd (d1::int)" and th2: "d1 dvd d3" show "d2 dvd d3" by (rule zdvd_trans[OF th1 th2]) qed (* Some simple lemmas *) lemma zdvd_eq_zdvd_abs: " (d::int) dvd d' = (d dvd (abs d')) " proof- have "d' < 0 ∨ d' ≥ 0" by arith moreover { assume dn': "d' < 0" then have "abs d' = - d'" by simp then have ?thesis by (simp) } moreover { assume dp': "d' ≥ 0" then have "abs d' = d'" by simp then have ?thesis by simp } ultimately show ?thesis by blast qed lemma zdvd_refl_abs: "(d::int) dvd (abs d)" proof- have "d dvd d" by simp then show ?thesis by (simp add: iffD1 [OF zdvd_eq_zdvd_abs [where d = "d" and d'="d"]]) qed (* δ > 0*) lemma divlcm_pos: assumes linp: "islinform p" shows "0 < divlcm p" using linp proof (induct p rule: divlcm.induct,simp_all add: ilcm_pos) case (goal1 f) show ?case using prems by (cases f, auto) (case_tac "intterm1", auto) qed lemma nz_le: "(x::int) > 0 ==> x ≠ 0" by auto (* divlcm is correct *) lemma divlcm_corr: assumes linp: "islinform p" shows "alldivide (divlcm p,p)" using linp divlcm_pos proof (induct p rule: divlcm.induct,simp_all add: zdvd_refl_abs,clarsimp simp add: Nat.gr0_conv_Suc) case (goal1 f) have "islinform f" using prems by (cases f, auto) (case_tac "intterm2", auto,case_tac "intterm1", auto) then have "alldivide (divlcm f, f)" using prems by simp moreover have "divlcm (NOT f) = divlcm f" by simp moreover have "alldivide (x,f) = alldivide (x,NOT f)" by simp ultimately show ?case by simp next case (goal2 f g) have dvd1: "(divlcm f) dvd (ilcm (divlcm f) (divlcm g))" using prems by(simp add: ilcm_dvd1 nz_le) have dvd2: "(divlcm g) dvd (ilcm (divlcm f) (divlcm g))" using prems by (simp add: ilcm_dvd2 nz_le) from dvd1 prems have "alldivide (ilcm (divlcm f) (divlcm g), f)" by (simp add: alldivide_mono[where d= "divlcm f" and p="f" and d' ="ilcm (divlcm f) (divlcm g)"]) moreover from dvd2 prems have "alldivide (ilcm (divlcm f) (divlcm g), g)" by (simp add: alldivide_mono[where d= "divlcm g" and p="g" and d' ="ilcm (divlcm f) (divlcm g)"]) ultimately show ?case by simp next case (goal3 f g) have dvd1: "(divlcm f) dvd (ilcm (divlcm f) (divlcm g))" using prems by (simp add: nz_le ilcm_dvd1) have dvd2: "(divlcm g) dvd (ilcm (divlcm f) (divlcm g))" using prems by (simp add: nz_le ilcm_dvd2) from dvd1 prems have "alldivide (ilcm (divlcm f) (divlcm g), f)" by (simp add: alldivide_mono[where d= "divlcm f" and p="f" and d' ="ilcm (divlcm f) (divlcm g)"]) moreover from dvd2 prems have "alldivide (ilcm (divlcm f) (divlcm g), g)" by (simp add: alldivide_mono[where d= "divlcm g" and p="g" and d' ="ilcm (divlcm f) (divlcm g)"]) ultimately show ?case by simp qed (* Properties of minusinf and plusinf*) (* minusinf p and p are the same for minusinfity … *) lemma minusinf_eq: assumes unifp: "isunified p" shows "∃ z. ∀ x. x < z --> (qinterp (x#ats) p = qinterp (x#ats) (minusinf p))" using unifp unified_islinform[OF unifp] proof (induct p rule: minusinf.induct) case (1 c r z) have "c <0 ∨ 0 ≤ c" by arith moreover { assume cneg: " c < 0" from prems have z0: "z= Cst 0" by (cases z,auto) with prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp from prems z0 have ?case proof- show ?thesis using prems z0 apply auto apply (rule exI[where x="I_intterm (a # ats) r"]) apply (rule allI) proof- fix x show "x < I_intterm (a # ats) r --> ¬ - x + I_intterm (x # ats) r ≤ 0" by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"]) qed qed } moreover { assume cpos: "0 ≤ c" from prems have z0: "z= Cst 0" by (cases z) auto with prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp from prems z0 have ?case proof- show ?thesis using prems z0 apply auto apply (rule exI[where x="-(I_intterm (a # ats) r)"]) apply (rule allI) proof- fix x show "x < - I_intterm (a # ats) r --> x + I_intterm (x # ats) r ≤ 0" by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"]) qed qed } ultimately show ?case by blast next case (2 c r z) from prems have z0: "z= Cst 0" by (cases z,auto) with prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp have "c <0 ∨ 0 ≤ c" by arith moreover { assume cneg: " c < 0" from prems z0 have ?case proof- show ?thesis using prems z0 apply auto apply (rule exI[where x="I_intterm (a # ats) r"]) apply (rule allI) proof- fix x show "x < I_intterm (a # ats) r --> ¬ - x + I_intterm (x # ats) r = 0" by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"]) qed qed } moreover { assume cpos: "0 ≤ c" from prems z0 have ?case proof- show ?thesis using prems z0 apply auto apply (rule exI[where x="-(I_intterm (a # ats) r)"]) apply (rule allI) proof- fix x show "x < - I_intterm (a # ats) r --> x + I_intterm (x # ats) r ≠ 0" by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"]) qed qed } ultimately show ?case by blast next case (3 c r z) from prems have z0: "z= Cst 0" by (cases z,auto) with prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp have "c <0 ∨ 0 ≤ c" by arith moreover { assume cneg: " c < 0" from prems z0 have ?case proof- show ?thesis using prems z0 apply auto apply (rule exI[where x="I_intterm (a # ats) r"]) apply (rule allI) proof- fix x show "x < I_intterm (a # ats) r --> ¬ - x + I_intterm (x # ats) r = 0" by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"]) qed qed } moreover { assume cpos: "0 ≤ c" from prems z0 have ?case proof- show ?thesis using prems z0 apply auto apply (rule exI[where x="-(I_intterm (a # ats) r)"]) apply (rule allI) proof- fix x show "x < - I_intterm (a # ats) r --> x + I_intterm (x # ats) r ≠ 0" by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"]) qed qed } ultimately show ?case by blast next case (4 f g) from prems obtain "zf" where zf:"∀x<zf. qinterp (x # ats) f = qinterp (x # ats) (minusinf f)" by auto from prems obtain "zg" where zg:"∀x<zg. qinterp (x # ats) g = qinterp (x # ats) (minusinf g)" by auto from zf zg show ?case apply auto apply (rule exI[where x="min zf zg"]) by simp next case (5 f g) from prems obtain "zf" where zf:"∀x<zf. qinterp (x # ats) f = qinterp (x # ats) (minusinf f)" by auto from prems obtain "zg" where zg:"∀x<zg. qinterp (x # ats) g = qinterp (x # ats) (minusinf g)" by auto from zf zg show ?case apply auto apply (rule exI[where x="min zf zg"]) by simp qed simp_all (* miusinf p behaves periodically*) lemma minusinf_repeats: assumes alldvd: "alldivide (d,p)" and unity: "isunified p" shows "qinterp (x#ats) (minusinf p) = qinterp ((x + c*d)#ats) (minusinf p)" using alldvd unity unified_islinform[OF unity] proof(induct p rule: islinform.induct, simp_all) case (goal1 t a) show ?case using prems apply (cases t, simp_all add: nth_pos2) apply (case_tac "intterm1", simp_all) apply (case_tac "intterm1a",simp_all) by (case_tac "intterm2a",simp_all) (case_tac "nat",simp_all add: nth_pos2 intterm_novar0[where x="x" and y="x+c*d"]) next case (goal2 t a) show ?case using prems apply (cases t, simp_all add: nth_pos2) apply (case_tac "intterm1", simp_all) apply (case_tac "intterm1a",simp_all) by (case_tac "intterm2a",simp_all) (case_tac "nat",simp_all add: nth_pos2 intterm_novar0[where x="x" and y="x+c*d"]) next case (goal3 a t) show ?case using prems proof(induct t rule: islinintterm.induct, simp_all add: nth_pos2) case (goal1 i n i') show ?case using prems proof(cases n, simp_all, case_tac "i=1", simp, simp add: dvd_period[where a="a" and d="d" and x="x" and c="c"]) case goal1 from prems have "(abs i = 1) ∧ i ≠ 1" by auto then have im1: "i=-1" by arith then have "(a dvd i*x + i') = (a dvd x + (-i'))" by (simp add: uminus_dvd_conv'[where d="a" and t="-x +i'"]) moreover from im1 have "(a dvd i*x + (i*(c * d)) + i') = (a dvd (x + c*d - i'))" apply simp apply (simp add: uminus_dvd_conv'[where d="a" and t="-x - c * d + i'"]) by (simp add: zadd_ac) ultimately have eq1:"((a dvd i*x + i') = (a dvd i*x + (i*(c * d)) + i')) = ((a dvd x + (-i')) = (a dvd (x + c*d - i')))" by simp moreover have dvd2: "(a dvd x + (-i')) = (a dvd x + c * d + (-i'))" by (rule dvd_period[where a="a" and d="d" and x="x" and c="c"], assumption) ultimately show ?case by simp qed next case (goal2 i n i' n' r) have "n = 0 ∨ 0 < n" by arith moreover { assume npos: "0 < n" from prems have "n < n'" by simp then have "0 < n'" by simp moreover from prems have linr: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp ultimately have ?case using prems npos by (simp add: nth_pos2 intterm_novar0[OF linr,where x="x" and y="x + c*d"]) } moreover { assume n0: "n=0" from prems have lin2: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp from prems have "n < n'" by simp then have npos': "0 < n'" by simp with prems have ?case proof(simp add: intterm_novar0[OF lin2, where x="x" and y="x+c*d"] nth_pos2 dvd_period,case_tac "i=1", simp add: dvd_period[where a="a" and d="d" and x="x" and c="c"], simp) case goal1 from prems have "abs i = 1 ∧ i≠1" by auto then have mi: "i = -1" by arith have "(a dvd -x + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r)) = (a dvd x + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r))" by (simp add: uminus_dvd_conv'[where d="a" and t="-x + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r)"]) also have "(a dvd x + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)) = (a dvd x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r))" by (rule dvd_period[where a="a" and d="d" and x="x" and c="c"], assumption) also have "(a dvd x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)) = (a dvd -(x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)))" by (rule uminus_dvd_conv'[where d="a" and t="x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)"]) also have "(a dvd -(x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r))) = (a dvd - x - c * d + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r))" by (auto,simp_all add: zadd_ac) finally show ?case using mi by auto qed } ultimately show ?case by blast qed next case (goal4 a t) show ?case using prems proof(induct t rule: islinintterm.induct, simp_all,case_tac "n=0", simp_all add: nth_pos2) case (goal1 i n i') show ?case using prems proof(case_tac "i=1", simp, simp add: dvd_period[where a="a" and d="d" and x="x" and c="c"]) case goal1 from prems have "abs i = 1 ∧ i≠1" by auto then have im1: "i=-1" by arith then have "(a dvd i*x + i') = (a dvd x + (-i'))" by (simp add: uminus_dvd_conv'[where d="a" and t="-x +i'"]) moreover from im1 have "(a dvd i*x + (i*(c * d)) + i') = (a dvd (x + c*d - i'))" apply simp apply (simp add: uminus_dvd_conv'[where d="a" and t="-x - c * d + i'"]) by (simp add: zadd_ac) ultimately have eq1:"((a dvd i*x + i') = (a dvd i*x + (i*(c * d)) + i')) = ((a dvd x + (-i')) = (a dvd (x + c*d - i')))" by simp moreover have dvd2: "(a dvd x + (-i')) = (a dvd x + c * d + (-i'))" by (rule dvd_period[where a="a" and d="d" and x="x" and c="c"], assumption) ultimately show ?thesis by simp qed next case (goal2 i n i' n' r) have "n = 0 ∨ 0 < n" by arith moreover { assume npos: "0 < n" from prems have "n < n'" by simp then have "0 < n'" by simp moreover from prems have linr: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp ultimately have ?case using prems npos by (simp add: nth_pos2 intterm_novar0[OF linr,where x="x" and y="x + c*d"]) } moreover { assume n0: "n=0" from prems have lin2: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp from prems have "n < n'" by simp then have npos': "0 < n'" by simp with prems have ?case proof(simp add: intterm_novar0[OF lin2, where x="x" and y="x+c*d"] nth_pos2 dvd_period,case_tac "i=1", simp add: dvd_period[where a="a" and d="d" and x="x" and c="c"], simp) case goal1 from prems have "abs i = 1 ∧ i≠1" by auto then have mi: "i = -1" by arith have "(a dvd -x + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r)) = (a dvd x + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r))" by (simp add: uminus_dvd_conv'[where d="a" and t="-x + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r)"]) also have "(a dvd x + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)) = (a dvd x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r))" by (rule dvd_period[where a="a" and d="d" and x="x" and c="c"], assumption) also have "(a dvd x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)) = (a dvd -(x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)))" by (rule uminus_dvd_conv'[where d="a" and t="x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)"]) also have "(a dvd -(x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r))) = (a dvd - x - c * d + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r))" by (auto,simp_all add: zadd_ac) finally show ?case using mi by auto qed } ultimately show ?case by blast qed next case (goal5 t a) show ?case using prems apply (cases t, simp_all add: nth_pos2) apply (case_tac "intterm1", simp_all) apply (case_tac "intterm1a",simp_all) by (case_tac "intterm2a",simp_all) (case_tac "nat",simp_all add: nth_pos2 intterm_novar0[where x="x" and y="x+c*d"]) qed lemma minusinf_repeats2: assumes alldvd: "alldivide (d,p)" and unity: "isunified p" shows "∀ x k. (qinterp (x#ats) (minusinf p) = qinterp ((x - k*d)#ats) (minusinf p))" (is "∀ x k. ?P x = ?P (x - k*d)") proof(rule allI, rule allI) fix x k show "?P x = ?P (x - k*d)" proof- have "?P x = ?P (x + (-k)*d)" by (rule minusinf_repeats[OF alldvd unity]) then have "?P x = ?P (x - (k*d))" by simp then show ?thesis by blast qed qed (* existence for minusinf p is existence for p *) lemma minusinf_lemma: assumes unifp: "isunified p" and exminf: "∃ j ∈ {1 ..d}. qinterp (j#ats) (minusinf p)" (is "∃ j ∈ {1 .. d}. ?P1 j") shows "∃ x. qinterp (x#ats) p" (is "∃ x. ?P x") proof- from exminf obtain "j" where P1j: "?P1 j" by blast have ePeqP1: "∃z. ∀ x. x < z --> (?P x = ?P1 x)" by (rule minusinf_eq[OF unifp]) then obtain "z" where P1eqP : "∀ x. x < z --> (?P x = ?P1 x)" by blast let ?d = "divlcm p" have alldvd: "alldivide (?d,p)" using unified_islinform[OF unifp] divlcm_corr by auto have dpos: "0 < ?d" using unified_islinform[OF unifp] divlcm_pos by simp have P1eqP1 : "∀ x k. ?P1 x = ?P1 (x - k*(?d))" by (rule minusinf_repeats2[OF alldvd unifp]) let ?w = "j - (abs (j-z) +1)* ?d" show "∃ x. ?P x" proof have w: "?w < z" by (rule decr_lemma[OF dpos]) have "?P1 j = ?P1 ?w" using P1eqP1 by blast also have "… = ?P ?w" using w P1eqP by blast finally show "?P ?w" using P1j by blast qed qed (* limited search for the withness for minusinf p, due to peridicity *) lemma minusinf_disj: assumes unifp: "isunified p" shows "(∃ x. qinterp (x#ats) (minusinf p)) = (∃ j ∈ { 1.. divlcm p}. qinterp (j#ats) (minusinf p))" (is "(∃ x. ?P x) = (∃ j ∈ { 1.. ?d}. ?P j)") proof have linp: "islinform p" by (rule unified_islinform[OF unifp]) have dpos: "0 < ?d" by (rule divlcm_pos[OF linp]) have alldvd: "alldivide(?d,p)" by (rule divlcm_corr[OF linp]) { assume "∃ j∈ {1 .. ?d}. ?P j" then show "∃ x. ?P x" using dpos by auto next assume "∃ x. ?P x" then obtain "x" where P: "?P x" by blast have modd: "∀x k. ?P x = ?P (x - k*?d)" by (rule minusinf_repeats2[OF alldvd unifp]) have "x mod ?d = x - (x div ?d)*?d" by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq) hence Pmod: "?P x = ?P (x mod ?d)" using modd by simp show "∃ j∈ {1 .. ?d}. ?P j" proof (cases) assume "x mod ?d = 0" hence "?P 0" using P Pmod by simp moreover have "?P 0 = ?P (0 - (-1)*?d)" using modd by blast ultimately have "?P ?d" by simp moreover have "?d ∈ {1 .. ?d}" using dpos by (simp add:atLeastAtMost_iff) ultimately show "∃ j∈ {1 .. ?d}. ?P j" .. next assume not0: "x mod ?d ≠ 0" have "?P(x mod ?d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound) moreover have "x mod ?d : {1 .. ?d}" proof - have "0 ≤ x mod ?d" by(rule pos_mod_sign[OF dpos]) moreover have "x mod ?d < ?d" by(rule pos_mod_bound[OF dpos]) ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff) qed ultimately show "∃ j∈ {1 .. ?d}. ?P j" .. qed } qed lemma minusinf_qfree: assumes linp : "islinform p" shows "isqfree (minusinf p)" using linp by (induct p rule: minusinf.induct) auto (* Properties of bset and a set *) (* The elements of a bset are linear *) lemma bset_lin: assumes unifp: "isunified p" shows "∀ b ∈ set (bset p). islinintterm b" using unifp unified_islinform[OF unifp] proof (induct p rule: bset.induct, auto) case (goal1 c r z) from prems have "z = Cst 0" by (cases z, simp_all) then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have "islinintterm (Cst -1)" by simp then show ?case using linr lin_add_lin by simp next case (goal2 c r z) from prems have "z = Cst 0" by (cases z, simp_all) then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) show ?case by (rule linr) next case (goal3 c r z) from prems have "z = Cst 0" by (cases z, simp_all) then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have "islinintterm (Cst -1)" by simp then show ?case using linr lin_add_lin lin_neg_lin by simp next case (goal4 c r z) from prems have "z = Cst 0" by (cases z, simp_all) then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have "islinintterm (Cst -1)" by simp then show ?case using linr lin_add_lin lin_neg_lin by simp next case (goal5 c r z) from prems have "z = Cst 0" by (cases z, simp_all) then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have "islinintterm (Cst -1)" by simp then show ?case using linr lin_add_lin lin_neg_lin by simp next case (goal6 c r z) from prems have "z = Cst 0" by (cases z, simp_all) then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have "islinintterm (Cst -1)" by simp then show ?case using linr lin_add_lin lin_neg_lin by simp next case (goal7 c r z) from prems have "z = Cst 0" by (cases z, simp_all) then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have "islinintterm (Cst -1)" by simp then show ?case using linr lin_add_lin lin_neg_lin by simp qed (* The third lemma in Norrisch's Paper *) lemma bset_disj_repeat: assumes unifp: "isunified p" and alldvd: "alldivide (d,p)" and dpos: "0 < d" and nob: "(qinterp (x#ats) q) ∧ ¬(∃j∈ {1 .. d}. ∃ b ∈ set (bset p). (qinterp (((I_intterm (a#ats) b) + j)#ats) q)) ∧(qinterp (x#ats) p)" (is "?Q x ∧ ¬(∃ j∈ {1.. d}. ∃ b∈ ?B. ?Q (?I a b + j)) ∧ ?P x") shows "?P (x -d)" using unifp nob alldvd unified_islinform[OF unifp] proof (induct p rule: islinform.induct,auto) case (goal1 t) from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have "n=0 ∨ n>0" by arith moreover {assume "n>0" then have ?case using prems by (simp add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="x-d"]) } moreover {assume nz: "n = 0" from prems have "abs i = 1" by auto then have "i = -1 ∨ i =1" by arith moreover { assume i1: "i=1" have ?case using dpos prems by (auto simp add: intterm_novar0[OF lininr, where x="x" and y="x - d"]) } moreover { assume im1: "i = -1" have ?case using prems proof(auto simp add: intterm_novar0[OF lininr, where x="x - d" and y="x"], cases) assume "- x + d + ?I x r ≤ 0" then show "- x + d + ?I x r ≤ 0" . next assume np: "¬ - x + d + ?I x r ≤ 0" then have ltd:"x - ?I x r ≤ d - 1" by simp from prems have "-x + ?I x r ≤ 0" by simp then have ge0: "x - ?I x r ≥ 0" by simp from ltd ge0 have "x - ?I x r = 0 ∨ (1 ≤ x - ?I x r ∧ x - ?I x r ≤ d - 1) " by arith moreover { assume "x - ?I x r = 0" then have xeqr: "x = ?I x r" by simp from prems have "?Q x" by simp with xeqr have qr:"?Q (?I x r)" by simp from prems have lininr: "islinintterm (Add (Mult (Cst i) (Var 0)) r)" by simp have "islinintterm r" by (rule islinintterm_subt[OF lininr]) from prems have "∀j∈{1..d}. ¬ ?Q (?I a r + -1 + j)" using linr by (auto simp add: lin_add_corr) moreover from dpos have "1 ∈ {1..d}" by simp ultimately have " ¬ ?Q (?I a r + -1 + 1)" by blast with dpos linr have "¬ ?Q (?I x r)" by (simp add: intterm_novar0[OF lininr, where x="x" and y="a"] lin_add_corr) with qr have "- x + d + ?I x r ≤ 0" by simp } moreover { assume gt0: "1 ≤ x - ?I x r ∧ x - ?I x r ≤ d - 1" then have "∃ j∈ {1 .. d - 1}. x - ?I x r = j" by simp then have "∃ j∈ {1 .. d}. x - ?I x r = j" by auto then obtain "j" where con: "1≤j ∧ j ≤ d ∧ x - ?I x r = j" by auto then have xeqr: "x = ?I x r + j" by auto with prems have "?Q (?I x r + j)" by simp with con have qrpj: "∃ j∈ {1 .. d}. ?Q (?I x r + j)" by auto from prems have "∀j∈{1..d}. ¬ ?Q (?I a r + j)" by auto then have "¬ (∃ j∈{1..d}. ?Q (?I x r + j))" by (simp add: intterm_novar0[OF lininr, where x="x" and y="a"]) with qrpj prems have "- x + d + ?I x r ≤ 0" by simp } ultimately show "- x + d + ?I x r ≤ 0" by blast qed } ultimately have ?case by blast } ultimately have ?case by blast } ultimately show ?case by blast next case (goal3 a t) from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have "n=0 ∨ n>0" by arith moreover {assume "n>0" then have ?case using prems by (simp add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="x-d"]) } moreover { assume nz: "n=0" from prems have "abs i = 1" by auto then have ipm: "i=1 ∨ i = -1" by arith from nz prems have advdixr: "a dvd (i * x) + I_intterm (x # ats) r" by simp from prems have "a dvd d" by simp then have advdid: "a dvd i*d" using ipm by auto have ?case using prems ipm by (auto simp add: intterm_novar0[OF lininr, where x="x-d" and y="x"] dvd_period[OF advdid, where x="i*x" and c="-1"]) } ultimately have ?case by blast } ultimately show ?case by blast next case (goal4 a t) from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have "n=0 ∨ n>0" by arith moreover {assume "n>0" then have ?case using prems by (simp add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="x-d"]) } moreover { assume nz: "n=0" from prems have "abs i = 1" by auto then have ipm: "i =1 ∨ i = -1" by arith from nz prems have advdixr: "¬ (a dvd (i * x) + I_intterm (x # ats) r)" by simp from prems have "a dvd d" by simp then have advdid: "a dvd i*d" using ipm by auto have ?case using prems ipm by (auto simp add: intterm_novar0[OF lininr, where x="x-d" and y="x"] dvd_period[OF advdid, where x="i*x" and c="-1"]) } ultimately have ?case by blast } ultimately show ?case by blast next case (goal2 t) from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have "n=0 ∨ n>0" by arith moreover {assume "n>0" then have ?case using prems by (simp add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="x-d"]) } moreover {assume nz: "n = 0" from prems have "abs i = 1" by auto then have "i = -1 ∨ i =1" by arith moreover { assume i1: "i=1" with prems have px: "x + ?I x r = 0" by simp then have "x = (- ?I x r - 1) + 1" by simp hence q1: "?Q ((- ?I x r - 1) + 1)" by simp from prems have "¬ (?Q ((?I a (lin_add(lin_neg r, Cst -1))) + 1))" by auto hence "¬ (?Q ((- ?I a r - 1) + 1))" using lin_add_corr lin_neg_corr linr lin_neg_lin by simp hence "¬ (?Q ((- ?I x r - 1) + 1))" using intterm_novar0[OF lininr, where x="x" and y="a"] by simp with q1 have ?case by simp } moreover { assume im1: "i = -1" with prems have px: "-x + ?I x r = 0" by simp then have "x = ?I x r" by simp hence q1: "?Q (?I x r)" by simp from prems have "¬ (?Q ((?I a (lin_add(r, Cst -1))) + 1))" by auto hence "¬ (?Q (?I a r))" using lin_add_corr lin_neg_corr linr lin_neg_lin by simp hence "¬ (?Q (?I x r ))" using intterm_novar0[OF lininr, where x="x" and y="a"] by simp with q1 have ?case by simp } ultimately have ?case by blast } ultimately have ?case by blast } ultimately show ?case by blast next case (goal5 t) from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have "n=0 ∨ n>0" by arith moreover {assume "n>0" then have ?case using prems by (simp add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="x-d"]) } moreover {assume nz: "n = 0" from prems have "abs i = 1" by auto then have "i = -1 ∨ i =1" by arith moreover { assume i1: "i=1" with prems have px: "x -d + ?I (x-d) r = 0" by simp hence "x = (- ?I x r) + d" using intterm_novar0[OF lininr, where x="x" and y="x-d"] by simp hence q1: "?Q (- ?I x r + d)" by simp from prems have "¬ (?Q ((?I a (lin_neg r)) + d))" by auto hence "¬ (?Q (- ?I a r + d))" using lin_neg_corr linr by simp hence "¬ (?Q ((- ?I x r + d)))" using intterm_novar0[OF lininr, where x="x" and y="a"] by simp with q1 have ?case by simp } moreover { assume im1: "i = -1" with prems have px: "- (x -d) + ?I (x - d) r = 0" by simp then have "x = ?I x r + d " using intterm_novar0[OF lininr, where x="x" and y="x-d"] by simp hence q1: "?Q (?I x r + d)" by simp from prems have "¬ (?Q ((?I a r) + d))" by auto hence "¬ (?Q (?I x r + d))" using intterm_novar0[OF lininr, where x="x" and y="a"] by simp with q1 have ?case by simp } ultimately have ?case by blast } ultimately have ?case by blast } ultimately show ?case by blast qed lemma bset_disj_repeat2: assumes unifp: "isunified p" shows "∀ x. ¬(∃j∈ {1 .. (divlcm p)}. ∃ b ∈ set (bset p). (qinterp (((I_intterm (a#ats) b) + j)#ats) p)) --> (qinterp (x#ats) p) --> (qinterp ((x - (divlcm p))#ats) p)" (is "∀ x. ¬(∃ j∈ {1 .. ?d}. ∃ b∈ ?B. ?P (?I a b + j)) --> ?P x --> ?P (x - ?d)") proof fix x have linp: "islinform p" by (rule unified_islinform[OF unifp]) have dpos: "?d > 0" by (rule divlcm_pos[OF linp]) have alldvd: "alldivide(?d,p)" by (rule divlcm_corr[OF linp]) show "¬(∃ j∈ {1 .. ?d}. ∃ b∈ ?B. ?P (?I a b + j)) --> ?P x --> ?P (x - ?d)" using prems bset_disj_repeat[OF unifp alldvd dpos] by blast qed (* Cooper's theorem in the minusinfinity version *) lemma cooper_mi_eq: assumes unifp : "isunified p" shows "(∃ x. qinterp (x#ats) p) = ((∃ j ∈ {1 .. (divlcm p)}. qinterp (j#ats) (minusinf p)) ∨ (∃ j ∈ {1 .. (divlcm p)}. ∃ b ∈ set (bset p). qinterp (((I_intterm (a#ats) b) + j)#ats) p))" (is "(∃ x. ?P x) = ((∃ j∈ {1 .. ?d}. ?MP j) ∨ (∃ j ∈ ?D. ∃ b∈ ?B. ?P (?I a b + j)))") proof- have linp :"islinform p" by (rule unified_islinform[OF unifp]) have dpos: "?d > 0" by (rule divlcm_pos[OF linp]) have alldvd: "alldivide(?d,p)" by (rule divlcm_corr[OF linp]) have eMPimpeP: "(∃j ∈ ?D. ?MP j) --> (∃x. ?P x)" by (simp add: minusinf_lemma[OF unifp, where d="?d" and ats="ats"]) have ePimpeP: "(∃ j ∈ ?D. ∃ b∈ ?B. ?P (?I a b + j)) --> (∃ x. ?P x)" by blast have bst_rep: "∀ x. ¬ (∃ j ∈ ?D. ∃ b ∈ ?B. ?P (?I a b + j)) --> ?P x --> ?P (x - ?d)" by (rule bset_disj_repeat2[OF unifp]) have MPrep: "∀ x k. ?MP x = ?MP (x- k*?d)" by (rule minusinf_repeats2[OF alldvd unifp]) have MPeqP: "∃ z. ∀ x < z. ?P x = ?MP x" by (rule minusinf_eq[OF unifp]) let ?B'= "{?I a b| b. b∈ ?B}" from bst_rep have bst_rep2: "∀x. ¬ (∃j∈?D. ∃b∈ ?B'. ?P (b+j)) --> ?P x --> ?P (x - ?d)" by auto show ?thesis using cpmi_eq[OF dpos MPeqP bst_rep2 MPrep] by auto qed (* A formalized analogy between aset, bset, plusinfinity and minusinfinity *) consts mirror:: "QF => QF" recdef mirror "measure size" "mirror (Le (Add (Mult (Cst c) (Var 0)) r) z) = (Le (Add (Mult (Cst (- c)) (Var 0)) r) z)" "mirror (Eq (Add (Mult (Cst c) (Var 0)) r) z) = (Eq (Add (Mult (Cst (- c)) (Var 0)) r) z)" "mirror (Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) = (Divides (Cst d) (Add (Mult (Cst (- c)) (Var 0)) r))" "mirror (NOT(Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r))) = (NOT(Divides (Cst d) (Add (Mult (Cst (- c)) (Var 0)) r)))" "mirror (NOT(Eq (Add (Mult (Cst c) (Var 0)) r) z)) = (NOT(Eq (Add (Mult (Cst (- c)) (Var 0)) r) z))" "mirror (And p q) = And (mirror p) (mirror q)" "mirror (Or p q) = Or (mirror p) (mirror q)" "mirror p = p" (* mirror preserves unifiedness *) lemma[simp]: "(abs (i::int) = 1) = (i =1 ∨ i = -1)" by arith lemma mirror_unified: assumes unif: "isunified p" shows "isunified (mirror p)" using unif proof (induct p rule: mirror.induct, simp_all) case (goal1 c r z) from prems have zz: "z = Cst 0" by (cases z, simp_all) then show ?case using prems by (auto simp add: islinintterm_eq_islint islint_def) next case (goal2 c r z) from prems have zz: "z = Cst 0" by (cases z, simp_all) then show ?case using prems by (auto simp add: islinintterm_eq_islint islint_def) next case (goal3 d c r) show ?case using prems by (auto simp add: islinintterm_eq_islint islint_def) next case (goal4 d c r) show ?case using prems by (auto simp add: islinintterm_eq_islint islint_def) next case (goal5 c r z) from prems have zz: "z = Cst 0" by (cases z, simp_all) then show ?case using prems by (auto simp add: islinintterm_eq_islint islint_def) qed (* relationship between plusinf and minusinf *) lemma plusinf_eq_minusinf_mirror: assumes unifp: "isunified p" shows "(qinterp (x#ats) (plusinf p)) = (qinterp ((- x)#ats) (minusinf (mirror p)))" using unifp unified_islinform[OF unifp] proof (induct p rule: islinform.induct, simp_all) case (goal1 t z) from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems by (cases n, auto simp add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"] )} ultimately show ?case by blast next case (goal2 t z) from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems by (cases n, auto simp add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"] )} ultimately show ?case by blast next case (goal3 d t) from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems by (cases n, simp_all add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"] )} ultimately show ?case by blast next case (goal4 d t) from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems by (cases n, simp_all add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"] )} ultimately show ?case by blast next case (goal5 t z) from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems by (cases n, auto simp add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"] )} ultimately show ?case by blast qed (* relationship between aset abd bset *) lemma aset_eq_bset_mirror: assumes unifp: "isunified p" shows "set (aset p) = set (map lin_neg (bset (mirror p)))" using unifp proof(induct p rule: mirror.induct) case (1 c r z) from prems have zz: "z = Cst 0" by (cases z, auto) from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def) have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def) show ?case using prems linr zz apply (auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1) by (simp add: negm1eq1 lin_neg_idemp sym[OF lin_neg_lin_add_distrib] lin_add_lin) next case (2 c r z) from prems have zz: "z = Cst 0" by (cases z, auto) from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def) have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def) show ?case using prems linr zz by (auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1) (simp add: negm1eq1 lin_neg_idemp sym[OF lin_neg_lin_add_distrib] lin_add_lin lin_neg_lin) next case (5 c r z) from prems have zz: "z = Cst 0" by (cases z, auto) from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def) have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def) show ?case using prems linr zz by(auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1) qed simp_all (* relationship between aset abd bset 2*) lemma aset_eq_bset_mirror2: assumes unifp: "isunified p" shows "aset p = map lin_neg (bset (mirror p))" using unifp proof(induct p rule: mirror.induct) case (1 c r z) from prems have zz: "z = Cst 0" by (cases z, auto) from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def) have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def) show ?case using prems linr zz apply (simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1) apply (simp add: negm1eq1 lin_neg_idemp sym[OF lin_neg_lin_add_distrib] lin_add_lin) by arith next case (2 c r z) from prems have zz: "z = Cst 0" by (cases z, auto) from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def) have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def) show ?case using prems linr zz by(auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1) (simp add: negm1eq1 lin_neg_idemp sym[OF lin_neg_lin_add_distrib] lin_add_lin lin_neg_lin) next case (5 c r z) from prems have zz: "z = Cst 0" by (cases z, auto) from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def) have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def) show ?case using prems linr zz by(auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1) qed simp_all (* mirror preserves divlcm *) lemma divlcm_mirror_eq: assumes unifp: "isunified p" shows "divlcm p = divlcm (mirror p)" using unifp by (induct p rule: mirror.induct) auto (* mirror almost preserves semantics *) lemma mirror_interp: assumes unifp: "isunified p" shows "(qinterp (x#ats) p) = (qinterp ((- x)#ats) (mirror p))" (is "?P x = ?MP (-x)") using unifp unified_islinform[OF unifp] proof (induct p rule: islinform.induct) case (1 t z) from prems have zz: "z = 0" by simp from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems zz by (cases n) (simp_all add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"]) } ultimately show ?case by blast next case (2 t z) from prems have zz: "z = 0" by simp from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems zz by (cases n) (simp_all add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"]) } ultimately show ?case by blast next case (3 d t) from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems linr by (cases n) (simp_all add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"]) } ultimately show ?case by blast next case (6 d t) from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems linr by (cases n) (simp_all add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"]) } ultimately show ?case by blast next case (7 t z) from prems have zz: "z = 0" by simp from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems zz by (cases n) (simp_all add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"]) } ultimately show ?case by blast qed simp_all lemma mirror_interp2: assumes unifp: "islinform p" shows "(qinterp (x#ats) p) = (qinterp ((- x)#ats) (mirror p))" (is "?P x = ?MP (-x)") using unifp proof (induct p rule: islinform.induct) case (1 t z) from prems have zz: "z = 0" by simp from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems zz by (cases n) (simp_all add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"]) } ultimately show ?case by blast next case (2 t z) from prems have zz: "z = 0" by simp from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems zz by (cases n) (simp_all add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"]) } ultimately show ?case by blast next case (3 d t) from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems linr by (cases n) (simp_all add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"]) } ultimately show ?case by blast next case (6 d t) from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems linr by (cases n) (simp_all add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"]) } ultimately show ?case by blast next case (7 t z) from prems have zz: "z = 0" by simp from prems have lint: "islinintterm t" by simp then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)" by (induct t rule: islinintterm.induct) auto moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto } moreover { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r" then obtain "i" "n" "r" where inr_def: "t = Add (Mult (Cst i) (Var n) ) r" by blast with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lininr]) have ?case using prems zz by (cases n) (simp_all add: nth_pos2 intterm_novar0[OF lininr, where x="x" and y="-x"]) } ultimately show ?case by blast qed simp_all (* mirror preserves existence *) lemma mirror_ex: assumes unifp: "isunified p" shows "(∃ x. (qinterp (x#ats) p)) = (∃ y. (qinterp (y#ats) (mirror p)))" (is "(∃ x. ?P x) = (∃ y. ?MP y)") proof assume "∃ x. ?P x" then obtain "x" where px:"?P x" by blast have "?MP (-x)" using px by(simp add: mirror_interp[OF unifp, where x="x"]) then show "∃ y. ?MP y" by blast next assume "∃ y. ?MP y" then obtain "y" where mpy: "?MP y" by blast have "?P (-y)" using mpy by (simp add: mirror_interp[OF unifp, where x="-y"]) then show "∃ x. ?P x" by blast qed lemma mirror_ex2: assumes unifp: "isunified p" shows "qinterp ats (QEx p) = qinterp ats (QEx (mirror p))" using mirror_ex[OF unifp] by simp (* Cooper's theorem in its plusinfinity version *) lemma cooper_pi_eq: assumes unifp : "isunified p" shows "(∃ x. qinterp (x#ats) p) = ((∃ j ∈ {1 .. (divlcm p)}. qinterp (-j#ats) (plusinf p)) ∨ (∃ j ∈ {1 .. (divlcm p)}. ∃ b ∈ set (aset p). qinterp (((I_intterm (a#ats) b) - j)#ats) p))" (is "(∃ x. ?P x) = ((∃ j∈ {1 .. ?d}. ?PP (-j)) ∨ (∃ j ∈ ?D. ∃ b∈ ?A. ?P (?I a b - j)))") proof- have unifmp: "isunified (mirror p)" by (rule mirror_unified[OF unifp]) have th1: "(∃ j∈ {1 .. ?d}. ?PP (-j)) = (∃ j∈ {1..?d}. qinterp (j # ats) (minusinf (mirror p)))" by (simp add: plusinf_eq_minusinf_mirror[OF unifp]) have dth: "?d = divlcm (mirror p)" by (rule divlcm_mirror_eq[OF unifp]) have "(∃ j ∈ ?D. ∃ b∈ ?A. ?P (?I a b - j)) = (∃ j∈ ?D. ∃ b ∈ set (map lin_neg (bset (mirror p))). ?P (?I a b - j))" by (simp only: aset_eq_bset_mirror[OF unifp]) also have "… = (∃ j∈ ?D. ∃ b ∈ set (bset (mirror p)). ?P (?I a (lin_neg b) - j))" by simp also have "… = (∃ j∈ ?D. ∃ b ∈ set (bset (mirror p)). ?P (-(?I a b + j)))" proof assume "∃j∈{1..divlcm p}. ∃b∈set (bset (mirror p)). qinterp ((I_intterm (a # ats) (lin_neg b) - j) # ats) p" then obtain "j" and "b" where pbmj: "j∈ ?D ∧ b∈ set (bset (mirror p)) ∧ ?P (?I a (lin_neg b) - j)" by blast then have linb: "islinintterm b" by (auto simp add:bset_lin[OF unifmp]) from linb pbmj have "?P (-(?I a b + j))" by (simp add: lin_neg_corr) then show "∃ j∈ ?D. ∃ b ∈ set (bset (mirror p)). ?P (-(?I a b + j))" using pbmj by auto next assume "∃ j∈ ?D. ∃ b ∈ set (bset (mirror p)). ?P (-(?I a b + j))" then obtain "j" and "b" where pbmj: "j∈ ?D ∧ b∈ set (bset (mirror p)) ∧ ?P (-(?I a b + j))" by blast then have linb: "islinintterm b" by (auto simp add:bset_lin[OF unifmp]) from linb pbmj have "?P (?I a (lin_neg b) - j)" by (simp add: lin_neg_corr) then show "∃ j∈ ?D. ∃ b ∈ set (bset (mirror p)). ?P (?I a (lin_neg b) - j)" using pbmj by auto qed finally have bth: "(∃ j∈ ?D. ∃ b∈ ?A. ?P (?I a b - j)) = (∃j∈ ?D. ∃ b∈set (bset (mirror p)). qinterp ((I_intterm (a # ats) b + j) # ats) (mirror p))" by (simp add: mirror_interp[OF unifp] zadd_ac) from bth dth th1 have "(∃ x. ?P x) = (∃ x. qinterp (x#ats) (mirror p))" by (simp add: mirror_ex[OF unifp]) also have "… = ((∃j∈{1..divlcm (mirror p)}. qinterp (j # ats) (minusinf (mirror p))) ∨ (∃j∈{1..divlcm (mirror p)}. ∃b∈set (bset (mirror p)). qinterp ((I_intterm (a # ats) b + j) # ats) (mirror p)))" (is "(∃ x. ?MP x) = ((∃ j∈ ?DM. ?MPM j) ∨ (∃ j ∈ ?DM. ∃ b∈ ?BM. ?MP (?I a b + j)))") by (rule cooper_mi_eq[OF unifmp]) also have "… = ((∃ j∈ ?D. ?PP (-j)) ∨ (∃ j ∈ ?D. ∃ b∈ ?BM. ?MP (?I a b + j)))" using bth th1 dth by simp finally show ?thesis using sym[OF bth] by simp qed (* substitution of a term into a Qfree formula, substitution of Bound 0 by i*) consts subst_it:: "intterm => intterm => intterm" primrec "subst_it i (Cst b) = Cst b" "subst_it i (Var n) = (if n = 0 then i else Var n)" "subst_it i (Neg it) = Neg (subst_it i it)" "subst_it i (Add it1 it2) = Add (subst_it i it1) (subst_it i it2)" "subst_it i (Sub it1 it2) = Sub (subst_it i it1) (subst_it i it2)" "subst_it i (Mult it1 it2) = Mult (subst_it i it1) (subst_it i it2)" (* subst_it preserves semantics *) lemma subst_it_corr: "I_intterm (a#ats) (subst_it i t) = I_intterm ((I_intterm (a#ats) i)#ats) t" by (induct t rule: subst_it.induct, simp_all add: nth_pos2) consts subst_p:: "intterm => QF => QF" primrec "subst_p i (Le it1 it2) = Le (subst_it i it1) (subst_it i it2)" "subst_p i (Lt it1 it2) = Lt (subst_it i it1) (subst_it i it2)" "subst_p i (Ge it1 it2) = Ge (subst_it i it1) (subst_it i it2)" "subst_p i (Gt it1 it2) = Gt (subst_it i it1) (subst_it i it2)" "subst_p i (Eq it1 it2) = Eq (subst_it i it1) (subst_it i it2)" "subst_p i (Divides d t) = Divides (subst_it i d) (subst_it i t)" "subst_p i T = T" "subst_p i F = F" "subst_p i (And p q) = And (subst_p i p) (subst_p i q)" "subst_p i (Or p q) = Or (subst_p i p) (subst_p i q)" "subst_p i (Imp p q) = Imp (subst_p i p) (subst_p i q)" "subst_p i (Equ p q) = Equ (subst_p i p) (subst_p i q)" "subst_p i (NOT p) = (NOT (subst_p i p))" (* subs_p preserves correctness *) lemma subst_p_corr: assumes qf: "isqfree p" shows "qinterp (a # ats) (subst_p i p) = qinterp ((I_intterm (a#ats) i)#ats) p " using qf by (induct p rule: subst_p.induct) (simp_all add: subst_it_corr) (* novar0 p is true if the fomula doese not depend on the quantified variable*) consts novar0I:: "intterm => bool" primrec "novar0I (Cst i) = True" "novar0I (Var n) = (n > 0)" "novar0I (Neg a) = (novar0I a)" "novar0I (Add a b) = (novar0I a ∧ novar0I b)" "novar0I (Sub a b) = (novar0I a ∧ novar0I b)" "novar0I (Mult a b) = (novar0I a ∧ novar0I b)" consts novar0:: "QF => bool" recdef novar0 "measure size" "novar0 (Lt a b) = (novar0I a ∧ novar0I b)" "novar0 (Gt a b) = (novar0I a ∧ novar0I b)" "novar0 (Le a b) = (novar0I a ∧ novar0I b)" "novar0 (Ge a b) = (novar0I a ∧ novar0I b)" "novar0 (Eq a b) = (novar0I a ∧ novar0I b)" "novar0 (Divides a b) = (novar0I a ∧ novar0I b)" "novar0 T = True" "novar0 F = True" "novar0 (NOT p) = novar0 p" "novar0 (And p q) = (novar0 p ∧ novar0 q)" "novar0 (Or p q) = (novar0 p ∧ novar0 q)" "novar0 (Imp p q) = (novar0 p ∧ novar0 q)" "novar0 (Equ p q) = (novar0 p ∧ novar0 q)" "novar0 p = False" (* Interpretation of terms, that doese not depend on Var 0 *) lemma I_intterm_novar0: assumes nov0: "novar0I x" shows "I_intterm (a#ats) x = I_intterm (b#ats) x" using nov0 by (induct x) (auto simp add: nth_pos2) (* substition is meaningless for term independent of Var 0*) lemma subst_p_novar0_corr: assumes qfp: "isqfree p" and nov0: "novar0I i" shows "qinterp (a#ats) (subst_p i p) = qinterp (I_intterm (b#ats) i#ats) p" proof- have "qinterp (a#ats) (subst_p i p) = qinterp (I_intterm (a#ats) i#ats) p" by (rule subst_p_corr[OF qfp]) moreover have "I_intterm (a#ats) i#ats = I_intterm (b#ats) i#ats" by (simp add: I_intterm_novar0[OF nov0, where a="a" and b="b"]) ultimately show ?thesis by simp qed (* linearity and independence on Var 0*) lemma lin_novar0: assumes linx: "islinintterm x" and nov0: "novar0I x" shows "∃ n > 0. islintn(n,x)" using linx nov0 by (induct x rule: islinintterm.induct) auto lemma lintnpos_novar0: assumes npos: "n > 0" and linx: "islintn(n,x)" shows "novar0I x" using npos linx by (induct n x rule: islintn.induct) auto (* lin_add preserves independence on Var 0*) lemma lin_add_novar0: assumes nov0a: "novar0I a" and nov0b : "novar0I b" and lina : "islinintterm a" and linb: "islinintterm b" shows "novar0I (lin_add (a,b))" proof- have "∃ na > 0. islintn(na, a)" by (rule lin_novar0[OF lina nov0a]) then obtain "na" where na: "na > 0 ∧ islintn(na,a)" by blast have "∃ nb > 0. islintn(nb, b)" by (rule lin_novar0[OF linb nov0b]) then obtain "nb" where nb: "nb > 0 ∧ islintn(nb,b)" by blast from na have napos: "na > 0" by simp from na have linna: "islintn(na,a)" by simp from nb have nbpos: "nb > 0" by simp from nb have linnb: "islintn(nb,b)" by simp have "min na nb ≤ min na nb" by simp then have "islintn (min na nb, lin_add(a,b))" by (simp add: lin_add_lint[OF linna linnb]) moreover have "min na nb > 0" using napos nbpos by (simp add: min_def) ultimately show ?thesis by (simp only: lintnpos_novar0) qed (* lin__mul preserves independence on Var 0*) lemma lin_mul_novar0: assumes linx: "islinintterm x" and nov0: "novar0I x" shows "novar0I (lin_mul(i,x))" using linx nov0 proof (induct i x rule: lin_mul.induct, auto) case (goal1 c c' n r) from prems have lincnr: "islinintterm (Add (Mult (Cst c') (Var n)) r)" by simp have "islinintterm r" by (rule islinintterm_subt[OF lincnr]) then show ?case using prems by simp qed (* lin_neg preserves indepenednce on Var 0*) lemma lin_neg_novar0: assumes linx: "islinintterm x" and nov0: "novar0I x" shows "novar0I (lin_neg x)" by (auto simp add: lin_mul_novar0 linx nov0 lin_neg_def) (* subterms of linear terms are independent on Var 0*) lemma intterm_subt_novar0: assumes lincnr: "islinintterm (Add (Mult (Cst c) (Var n)) r)" shows "novar0I r" proof- have cnz: "c ≠ 0" by (rule islinintterm_cnz[OF lincnr]) have "islintn(0,Add (Mult (Cst c) (Var n)) r)" using lincnr by (simp only: islinintterm_eq_islint islint_def) then have "islintn (n+1,r)" by auto moreover have "n+1 >0 " by arith ultimately show ?thesis using lintnpos_novar0 by auto qed (* decrease the De-Bruijn indices*) consts decrvarsI:: "intterm => intterm" primrec "decrvarsI (Cst i) = (Cst i)" "decrvarsI (Var n) = (Var (n - 1))" "decrvarsI (Neg a) = (Neg (decrvarsI a))" "decrvarsI (Add a b) = (Add (decrvarsI a) (decrvarsI b))" "decrvarsI (Sub a b) = (Sub (decrvarsI a) (decrvarsI b))" "decrvarsI (Mult a b) = (Mult (decrvarsI a) (decrvarsI b))" (* One can decrease the indics for terms and formulae independent on Var 0*) lemma intterm_decrvarsI: assumes nov0: "novar0I t" shows "I_intterm (a#ats) t = I_intterm ats (decrvarsI t)" using nov0 by (induct t) (auto simp add: nth_pos2) consts decrvars:: "QF => QF" primrec "decrvars (Lt a b) = (Lt (decrvarsI a) (decrvarsI b))" "decrvars (Gt a b) = (Gt (decrvarsI a) (decrvarsI b))" "decrvars (Le a b) = (Le (decrvarsI a) (decrvarsI b))" "decrvars (Ge a b) = (Ge (decrvarsI a) (decrvarsI b))" "decrvars (Eq a b) = (Eq (decrvarsI a) (decrvarsI b))" "decrvars (Divides a b) = (Divides (decrvarsI a) (decrvarsI b))" "decrvars T = T" "decrvars F = F" "decrvars (NOT p) = (NOT (decrvars p))" "decrvars (And p q) = (And (decrvars p) (decrvars q))" "decrvars (Or p q) = (Or (decrvars p) (decrvars q))" "decrvars (Imp p q) = (Imp (decrvars p) (decrvars q))" "decrvars (Equ p q) = (Equ (decrvars p) (decrvars q))" (* decrvars preserves quantifier freeness*) lemma decrvars_qfree: "isqfree p ==> isqfree (decrvars p)" by (induct p rule: isqfree.induct, auto) lemma novar0_qfree: "novar0 p ==> isqfree p" by (induct p) auto lemma qinterp_novar0: assumes nov0: "novar0 p" shows "qinterp (a#ats) p = qinterp ats (decrvars p)" using nov0 by(induct p) (simp_all add: intterm_decrvarsI) (* All elements of bset p doese not depend on Var 0*) lemma bset_novar0: assumes unifp: "isunified p" shows "∀ b∈ set (bset p). novar0I b " using unifp proof(induct p rule: bset.induct) case (1 c r z) from prems have zz: "z = Cst 0" by (cases "z", auto) from prems zz have lincnr: "islinintterm(Add (Mult (Cst c) (Var 0)) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have novar0r: "novar0I r" by (rule intterm_subt_novar0[OF lincnr]) from prems zz have "c = 1 ∨ c = -1" by auto moreover { assume c1: "c=1" have lin1: "islinintterm (Cst 1)" by simp have novar01: "novar0I (Cst 1)" by simp then have ?case using prems zz novar0r lin1 novar01 by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin) } moreover { assume c1: "c= -1" have lin1: "islinintterm (Cst -1)" by simp have novar01: "novar0I (Cst -1)" by simp then have ?case using prems zz novar0r lin1 novar01 by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin) } ultimately show ?case by blast next case (2 c r z) from prems have zz: "z = Cst 0" by (cases "z", auto) from prems zz have lincnr: "islinintterm(Add (Mult (Cst c) (Var 0)) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have novar0r: "novar0I r" by (rule intterm_subt_novar0[OF lincnr]) from prems zz have "c = 1 ∨ c = -1" by auto moreover { assume c1: "c=1" have lin1: "islinintterm (Cst 1)" by simp have novar01: "novar0I (Cst 1)" by simp then have ?case using prems zz novar0r lin1 novar01 by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin) } moreover { assume c1: "c= -1" have lin1: "islinintterm (Cst -1)" by simp have novar01: "novar0I (Cst -1)" by simp then have ?case using prems zz novar0r lin1 novar01 by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin) } ultimately show ?case by blast next case (3 c r z) from prems have zz: "z = Cst 0" by (cases "z", auto) from prems zz have lincnr: "islinintterm(Add (Mult (Cst c) (Var 0)) r)" by simp have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr]) have novar0r: "novar0I r" by (rule intterm_subt_novar0[OF lincnr]) from prems zz have "c = 1 ∨ c = -1" by auto moreover { assume c1: "c=1" have lin1: "islinintterm (Cst 1)" by simp have novar01: "novar0I (Cst 1)" by simp then have ?case using prems zz novar0r lin1 novar01 by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin) } moreover { assume c1: "c= -1" have lin1: "islinintterm (Cst -1)" by simp have novar01: "novar0I (Cst -1)" by simp then have ?case using prems zz novar0r lin1 novar01 by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin) } ultimately show ?case by blast qed auto (* substitution preserves independence on Var 0*) lemma subst_it_novar0: assumes nov0x: "novar0I x" shows "novar0I (subst_it x t)" using nov0x by (induct t) auto lemma subst_p_novar0: assumes nov0x:"novar0I x" and qfp: "isqfree p" shows "novar0 (subst_p x p)" using nov0x qfp by (induct p rule: novar0.induct) (simp_all add: subst_it_novar0) (* linearize preserves independence on Var 0 *) lemma linearize_novar0: assumes nov0t: "novar0I t " shows "!! t'. linearize t = Some t' ==> novar0I t'" using nov0t proof(induct t rule: novar0I.induct) case (Neg a) let ?la = "linearize a" from prems have "∃ a'. ?la = Some a'" by (cases ?la, auto) then obtain "a'" where "?la = Some a'" by blast with prems have nv0a':"novar0I a'" by simp have "islinintterm a'" using prems by (simp add: linearize_linear) with nv0a' have "novar0I (lin_neg a')" by (simp add: lin_neg_novar0) then show ?case using prems by simp next case (Add a b) let ?la = "linearize a" let ?lb = "linearize b" from prems have linab: "linearize (Add a b) = Some t'" by simp then have "∃ a'. ?la = Some a'" by (cases ?la) auto then obtain "a'" where "?la = Some a'" by blast with prems have nv0a':"novar0I a'" by simp have lina': "islinintterm a'" using prems by (simp add: linearize_linear) from linab have "∃ b'. ?lb = Some b'" by (cases ?la, auto simp add: measure_def inv_image_def) (cases ?lb, auto) then obtain "b'" where "?lb = Some b'" by blast with prems have nv0b':"novar0I b'" by simp have linb': "islinintterm b'" using prems by (simp add: linearize_linear) then show ?case using prems lina' linb' nv0a' nv0b' by (auto simp add: measure_def inv_image_def lin_add_novar0) next case (Sub a b) let ?la = "linearize a" let ?lb = "linearize b" from prems have linab: "linearize (Sub a b) = Some t'" by simp then have "∃ a'. ?la = Some a'" by (cases ?la) auto then obtain "a'" where "?la = Some a'" by blast with prems have nv0a':"novar0I a'" by simp have lina': "islinintterm a'" using prems by (simp add: linearize_linear) from linab have "∃ b'. ?lb = Some b'" by (cases ?la, auto simp add: measure_def inv_image_def) (cases ?lb, auto) then obtain "b'" where "?lb = Some b'" by blast with prems have nv0b':"novar0I b'" by simp have linb': "islinintterm b'" using prems by (simp add: linearize_linear) then show ?case using prems lina' linb' nv0a' nv0b' by (auto simp add: measure_def inv_image_def lin_add_novar0 lin_neg_novar0 lin_neg_lin) next case (Mult a b) let ?la = "linearize a" let ?lb = "linearize b" from prems have linab: "linearize (Mult a b) = Some t'" by simp then have "∃ a'. ?la = Some a'" by (cases ?la, auto simp add: measure_def inv_image_def) then obtain "a'" where "?la = Some a'" by blast with prems have nv0a':"novar0I a'" by simp have lina': "islinintterm a'" using prems by (simp add: linearize_linear) from prems linab have "∃ b'. ?lb = Some b'" apply (cases ?la, auto simp add: measure_def inv_image_def) by (cases "a'",auto simp add: measure_def inv_image_def) (cases ?lb, auto)+ then obtain "b'" where "?lb = Some b'" by blast with prems have nv0b':"novar0I b'" by simp have linb': "islinintterm b'" using prems by (simp add: linearize_linear) then show ?case using prems lina' linb' nv0a' nv0b' by (cases "a'",auto simp add: measure_def inv_image_def lin_mul_novar0) (cases "b'",auto simp add: measure_def inv_image_def lin_mul_novar0) qed auto (* simplification of formulae *) consts psimpl :: "QF => QF" recdef psimpl "measure size" "psimpl (Le l r) = (case (linearize (Sub l r)) of None => Le l r | Some x => (case x of Cst i => (if i ≤ 0 then T else F) | _ => (Le x (Cst 0))))" "psimpl (Eq l r) = (case (linearize (Sub l r)) of None => Eq l r | Some x => (case x of Cst i => (if i = 0 then T else F) | _ => (Eq x (Cst 0))))" "psimpl (Divides (Cst d) t) = (case (linearize t) of None => (Divides (Cst d) t) | Some c => (case c of Cst i => (if d dvd i then T else F) | _ => (Divides (Cst d) c)))" "psimpl (And p q) = (let p'= psimpl p in (case p' of F => F |T => psimpl q | _ => let q' = psimpl q in (case q' of F => F | T => p' | _ => (And p' q'))))" "psimpl (Or p q) = (let p'= psimpl p in (case p' of T => T | F => psimpl q | _ => let q' = psimpl q in (case q' of T => T | F => p' | _ => (Or p' q'))))" "psimpl (Imp p q) = (let p'= psimpl p in (case p' of F => T |T => psimpl q | NOT p1 => let q' = psimpl q in (case q' of F => p1 | T => T | _ => (Or p1 q')) | _ => let q' = psimpl q in (case q' of F => NOT p' | T => T | _ => (Imp p' q'))))" "psimpl (Equ p q) = (let p'= psimpl p ; q' = psimpl q in (case p' of T => q' | F => (case q' of T => F | F => T | NOT q1 => q1 | _ => NOT q') | NOT p1 => (case q' of T => p' | F => p1 | NOT q1 => (Equ p1 q1) | _ => (Equ p' q')) | _ => (case q' of T => p' | F => NOT p' | _ => (Equ p' q'))))" "psimpl (NOT p) = (let p' = psimpl p in ( case p' of F => T | T => F | NOT p1 => p1 | _ => (NOT p')))" "psimpl p = p" (* psimpl preserves semantics *) lemma psimpl_corr: "qinterp ats p = qinterp ats (psimpl p)" proof(induct p rule: psimpl.induct) case (1 l r) have "(∃ lx. linearize (Sub l r) = Some lx) ∨ (linearize (Sub l r) = None)" by auto moreover { assume lin: "∃ lx. linearize (Sub l r) = Some lx" from lin obtain "lx" where lx: "linearize (Sub l r) = Some lx" by blast from lx have "I_intterm ats (Sub l r) = I_intterm ats lx" by (rule linearize_corr[where t="Sub l r" and t'= "lx"]) then have feq: "qinterp ats (Le l r) = qinterp ats (Le lx (Cst 0))" by (simp , arith) from lx have lxlin: "islinintterm lx" by (rule linearize_linear) from lxlin feq have ?case proof- have "(∃ i. lx = Cst i) ∨ (¬ (∃ i. lx = Cst i))" by blast moreover { assume lxcst: "∃ i. lx = Cst i" from lxcst obtain "i" where lxi: "lx = Cst i" by blast with feq have "qinterp ats (Le l r) = (i ≤ 0)" by simp then have ?case using prems by (simp add: measure_def inv_image_def) } moreover { assume "(¬ (∃ i. lx = Cst i))" then have "(case lx of Cst i => (if i ≤ 0 then T else F) | _ => (Le lx (Cst 0))) = (Le lx (Cst 0))" by (case_tac "lx::intterm", auto) with prems lxlin feq have ?case by (auto simp add: measure_def inv_image_def) } ultimately show ?thesis by blast qed } moreover { assume "linearize (Sub l r) = None" then have ?case using prems by simp } ultimately show ?case by blast next case (2 l r) have "(∃ lx. linearize (Sub l r) = Some lx) ∨ (linearize (Sub l r) = None)" by auto moreover { assume lin: "∃ lx. linearize (Sub l r) = Some lx" from lin obtain "lx" where lx: "linearize (Sub l r) = Some lx" by blast from lx have "I_intterm ats (Sub l r) = I_intterm ats lx" by (rule linearize_corr[where t="Sub l r" and t'= "lx"]) then have feq: "qinterp ats (Eq l r) = qinterp ats (Eq lx (Cst 0))" by (simp , arith) from lx have lxlin: "islinintterm lx" by (rule linearize_linear) from lxlin feq have ?case proof- have "(∃ i. lx = Cst i) ∨ (¬ (∃ i. lx = Cst i))" by blast moreover { assume lxcst: "∃ i. lx = Cst i" from lxcst obtain "i" where lxi: "lx = Cst i" by blast with feq have "qinterp ats (Eq l r) = (i = 0)" by simp then have ?case using prems by (simp add: measure_def inv_image_def) } moreover { assume "(¬ (∃ i. lx = Cst i))" then have "(case lx of Cst i => (if i = 0 then T else F) | _ => (Eq lx (Cst 0))) = (Eq lx (Cst 0))" by (case_tac "lx::intterm", auto) with prems lxlin feq have ?case by (auto simp add: measure_def inv_image_def) } ultimately show ?thesis by blast qed } moreover { assume "linearize (Sub l r) = None" then have ?case using prems by simp } ultimately show ?case by blast next case (3 d t) have "(∃ lt. linearize t = Some lt) ∨ (linearize t = None)" by auto moreover { assume lin: "∃ lt. linearize t = Some lt" from lin obtain "lt" where lt: "linearize t = Some lt" by blast from lt have "I_intterm ats t = I_intterm ats lt" by (rule linearize_corr[where t="t" and t'= "lt"]) then have feq: "qinterp ats (Divides (Cst d) t) = qinterp ats (Divides (Cst d) lt)" by (simp) from lt have ltlin: "islinintterm lt" by (rule linearize_linear) from ltlin feq have ?case using prems apply simp by (case_tac "lt::intterm", simp_all) } moreover { assume "linearize t = None" then have ?case using prems by simp } ultimately show ?case by blast next case (4 f g) let ?sf = "psimpl f" let ?sg = "psimpl g" show ?case using prems by (cases ?sf, simp_all add: Let_def measure_def inv_image_def) (cases ?sg, simp_all)+ next case (5 f g) let ?sf = "psimpl f" let ?sg = "psimpl g" show ?case using prems apply (cases ?sf, simp_all add: Let_def measure_def inv_image_def) apply (cases ?sg, simp_all) apply (cases ?sg, simp_all) apply (cases ?sg, simp_all) apply (cases ?sg, simp_all) apply (cases ?sg, simp_all) apply (cases ?sg, simp_all) apply (cases ?sg, simp_all) apply blast apply (cases ?sg, simp_all) apply (cases ?sg, simp_all) apply (cases ?sg, simp_all) apply blast apply (cases ?sg, simp_all) by (cases ?sg, simp_all) (cases ?sg, simp_all) next case (6 f g) let ?sf = "psimpl f" let ?sg = "psimpl g" show ?case using prems apply(simp add: Let_def measure_def inv_image_def) apply(cases ?sf,simp_all) apply (simp_all add: Let_def measure_def inv_image_def) apply(cases ?sg, simp_all) apply(cases ?sg, simp_all) apply(cases ?sg, simp_all) apply(cases ?sg, simp_all) apply(cases ?sg, simp_all) apply(cases ?sg, simp_all) apply(cases ?sg, simp_all) apply blast apply blast apply blast apply blast apply blast apply blast apply blast apply blast apply blast apply blast apply blast apply blast apply blast apply(cases ?sg, simp_all) apply(cases ?sg, simp_all) apply(cases ?sg, simp_all) apply(cases ?sg, simp_all) apply(cases ?sg, simp_all) apply(cases ?sg, simp_all) done next case (7 f g) let ?sf = "psimpl f" let ?sg = "psimpl g" show ?case using prems by (cases ?sf, simp_all add: Let_def) (cases ?sg, simp_all)+ next case (8 f) show ?case using prems apply (simp add: Let_def) by (case_tac "psimpl f", simp_all) qed simp_all (* psimpl preserves independence on Var 0*) lemma psimpl_novar0: assumes nov0p: "novar0 p" shows "novar0 (psimpl p)" using nov0p proof (induct p rule: psimpl.induct) case (1 l r) let ?ls = "linearize (Sub l r)" have "?ls = None ∨ (∃ x. ?ls = Some x)" by auto moreover { assume "?ls = None" then have ?case using prems by (simp add: measure_def inv_image_def) } moreover { assume "∃ x. ?ls = Some x" then obtain "x" where ls_d: "?ls = Some x" by blast from prems have "novar0I l" by simp moreover from prems have "novar0I r" by simp ultimately have nv0s: "novar0I (Sub l r)" by simp from prems have "novar0I x" by (simp add: linearize_novar0[OF nv0s, where t'="x"]) then have ?case using prems by (cases "x") (auto simp add: measure_def inv_image_def) } ultimately show ?case by blast next case (2 l r) let ?ls = "linearize (Sub l r)" have "?ls = None ∨ (∃ x. ?ls = Some x)" by auto moreover { assume "?ls = None" then have ?case using prems by (simp add: measure_def inv_image_def) } moreover { assume "∃ x. ?ls = Some x" then obtain "x" where ls_d: "?ls = Some x" by blast from prems have "novar0I l" by simp moreover from prems have "novar0I r" by simp ultimately have nv0s: "novar0I (Sub l r)" by simp from prems have "novar0I x" by (simp add: linearize_novar0[OF nv0s, where t'="x"]) then have ?case using prems by (cases "x") (auto simp add: measure_def inv_image_def) } ultimately show ?case by blast next case (3 d t) let ?lt = "linearize t" have "?lt = None ∨ (∃ x. ?lt = Some x)" by auto moreover { assume "?lt = None" then have ?case using prems by simp } moreover { assume "∃x. ?lt = Some x" then obtain "x" where x_d: "?lt = Some x" by blast from prems have nv0t: "novar0I t" by simp with x_d have "novar0I x" by (simp add: linearize_novar0[OF nv0t]) with prems have ?case by (cases "x") simp_all } ultimately show ?case by blast next case (4 f g) let ?sf = "psimpl f" let ?sg = "psimpl g" show ?case using prems by (cases ?sf, simp_all add: Let_def measure_def inv_image_def) (cases ?sg,simp_all)+ next case (5 f g) let ?sf = "psimpl f" let ?sg = "psimpl g" show ?case using prems by (cases ?sf, simp_all add: Let_def measure_def inv_image_def) (cases ?sg,simp_all)+ next case (6 f g) let ?sf = "psimpl f" let ?sg = "psimpl g" show ?case using prems by (cases ?sf, simp_all add: Let_def measure_def inv_image_def) (cases ?sg,simp_all)+ next case (7 f g) let ?sf = "psimpl f" let ?sg = "psimpl g" show ?case using prems by (cases ?sf, simp_all add: Let_def measure_def inv_image_def) (cases ?sg,simp_all)+ next case (8 f) let ?sf = "psimpl f" from prems have nv0sf:"novar0 ?sf" by simp show ?case using prems nv0sf by (cases ?sf, auto simp add: Let_def measure_def inv_image_def) qed simp_all (* implements a disj of p applied to all elements of the list*) consts explode_disj :: "(intterm list × QF) => QF" recdef explode_disj "measure (λ(is,p). length is)" "explode_disj ([],p) = F" "explode_disj (i#is,p) = (let pi = psimpl (subst_p i p) in ( case pi of T => T | F => explode_disj (is,p) | _ => (let r = explode_disj (is,p) in (case r of T => T | F => pi | _ => Or pi r))))" (* correctness theorem for one iteration of explode_disj *) lemma explode_disj_disj: assumes qfp: "isqfree p" shows "(qinterp (x#xs) (explode_disj(i#is,p))) = (qinterp (x#xs) (subst_p i p) ∨ (qinterp (x#xs) (explode_disj(is,p))))" using qfp proof- let ?pi = "psimpl (subst_p i p)" have pi: "qinterp (x#xs) ?pi = qinterp (x#xs) (subst_p i p)" by (simp add: psimpl_corr[where p="(subst_p i p)"]) let ?dp = "explode_disj(is,p)" show ?thesis using pi proof (cases) assume "?pi= T ∨ ?pi = F" then show ?thesis using pi by (case_tac "?pi::QF", auto) next assume notTF: "¬ (?pi = T ∨ ?pi = F)" let ?dp = "explode_disj(is,p)" have dp_cases: "explode_disj(i#is,p) = (case (explode_disj(is,p)) of T => T | F => psimpl (subst_p i p) | _ => Or (psimpl (subst_p i p)) (explode_disj(is,p)))" using notTF by (cases "?pi") (simp_all add: Let_def cong del: QF.weak_case_cong) show ?thesis using pi dp_cases notTF proof(cases) assume "?dp = T ∨ ?dp = F" then show ?thesis using pi dp_cases by (cases "?dp") auto next assume "¬ (?dp = T ∨ ?dp = F)" then show ?thesis using pi dp_cases notTF by (cases ?dp) auto qed qed qed (* correctness theorem for explode_disj *) lemma explode_disj_corr: assumes qfp: "isqfree p" shows "(∃ x ∈ set xs. qinterp (a#ats) (subst_p x p)) = (qinterp (a#ats) (explode_disj(xs,p)))" (is "(∃ x ∈ set xs. ?P x) = (?DP a xs )") using qfp proof (induct xs) case Nil show ?case by simp next case (Cons y ys) have "(∃ x ∈ set (y#ys). ?P x) = (?P y ∨ (∃ x∈ set ys. ?P x))" by auto also have "… = (?P y ∨ ?DP a ys)" using "Cons.hyps" qfp by auto also have "… = ?DP a (y#ys)" using explode_disj_disj[OF qfp] by auto finally show ?case by simp qed (* explode_disj preserves independence on Var 0*) lemma explode_disj_novar0: assumes nov0xs: "∀x ∈ set xs. novar0I x" and qfp: "isqfree p" shows "novar0 (explode_disj (xs,p))" using nov0xs qfp proof (induct xs, auto simp add: Let_def) case (goal1 a as) let ?q = "subst_p a p" let ?qs = "psimpl ?q" have "?qs = T ∨ ?qs = F ∨ (?qs ≠ T ∨ ?qs ≠ F)" by simp moreover { assume "?qs = T" then have ?case by simp } moreover { assume "?qs = F" then have ?case by simp } moreover { assume qsnTF: "?qs ≠ T ∧ ?qs ≠ F" let ?r = "explode_disj (as,p)" have nov0qs: "novar0 ?qs" using prems by (auto simp add: psimpl_novar0 subst_p_novar0) have "?r = T ∨ ?r = F ∨ (?r ≠ T ∨ ?r ≠ F)" by simp moreover { assume "?r = T" then have ?case by (cases ?qs) auto } moreover { assume "?r = F" then have ?case using nov0qs by (cases ?qs, auto) } moreover { assume "?r ≠ T ∧ ?r ≠ F" then have ?case using nov0qs prems qsnTF by (cases ?qs, auto simp add: Let_def) (cases ?r,auto)+ } ultimately have ?case by blast } ultimately show ?case by blast qed (* Some simple lemmas used for technical reasons *) lemma eval_Or_cases: "qinterp (a#ats) (case f of T => T | F => g | _ => (case g of T => T | F => f | _ => Or f g)) = (qinterp (a#ats) f ∨ qinterp (a#ats) g)" proof- let ?result = " (case f of T => T | F => g | _ => (case g of T => T | F => f | _ => Or f g))" have "f = T ∨ f = F ∨ (f ≠ T ∧ f≠ F)" by auto moreover { assume fT: "f = T" then have ?thesis by auto } moreover { assume "f=F" then have ?thesis by auto } moreover { assume fnT: "f≠T" and fnF: "f≠F" have "g = T ∨ g = F ∨ (g ≠ T ∧ g≠ F)" by auto moreover { assume "g=T" then have ?thesis using fnT fnF by (cases f, auto) } moreover { assume "g=F" then have ?thesis using fnT fnF by (cases f, auto) } moreover { assume gnT: "g≠T" and gnF: "g≠F" then have "?result = (case g of T => T | F => f | _ => Or f g)" using fnT fnF by (cases f, auto) also have "… = Or f g" using gnT gnF by (cases g, auto) finally have "?result = Or f g" by simp then have ?thesis by simp } ultimately have ?thesis by blast } ultimately show ?thesis by blast qed lemma or_case_novar0: assumes fnTF: "f ≠ T ∧ f ≠ F" and gnTF: "g ≠ T ∧ g ≠ F" and f0: "novar0 f" and g0: "novar0 g" shows "novar0 (case f of T => T | F => g | _ => (case g of T => T | F => f | _ => Or f g))" using fnTF gnTF f0 g0 by (cases f, auto) (cases g, auto)+ (* An implementation of sets trough lists *) constdefs list_insert :: "'a => 'a list => 'a list" "list_insert x xs ≡ (if x mem xs then xs else x#xs)" lemma list_insert_set: "set (list_insert x xs) = set (x#xs)" by(induct xs) (auto simp add: list_insert_def) consts list_union :: "('a list × 'a list) => 'a list" recdef list_union "measure (λ(xs,ys). length xs)" "list_union ([], ys) = ys" "list_union (xs, []) = xs" "list_union (x#xs,ys) = list_insert x (list_union (xs,ys))" lemma list_union_set: "set (list_union(xs,ys)) = set (xs@ys)" by(induct xs ys rule: list_union.induct, auto simp add:list_insert_set) consts list_set ::"'a list => 'a list" primrec "list_set [] = []" "list_set (x#xs) = list_insert x (list_set xs)" lemma list_set_set: "set xs = set (list_set xs)" by (induct xs) (auto simp add: list_insert_set) consts iupto :: "int × int => int list" recdef iupto "measure (λ (i,j). nat (j - i +1))" "iupto(i,j) = (if j<i then [] else (i#(iupto(i+1,j))))" (* correctness theorem for iupto *) lemma iupto_set: "set (iupto(i,j)) = {i .. j}" proof(induct rule: iupto.induct) case (1 a b) show ?case using prems by (simp add: simp_from_to) qed consts all_sums :: "int × intterm list => intterm list" recdef all_sums "measure (λ(i,is). length is)" "all_sums (j,[]) = []" "all_sums (j,i#is) = (map (λx. lin_add (i,(Cst x))) (iupto(1,j))@(all_sums (j,is)))" (* all_sums preserves independence on Var 0*) lemma all_sums_novar0: assumes nov0xs: "∀ x∈ set xs. novar0I x" and linxs: "∀ x∈ set xs. islinintterm x " shows "∀ x∈ set (all_sums (d,xs)). novar0I x" using nov0xs linxs proof(induct d xs rule: all_sums.induct) case 1 show ?case by simp next case (2 j a as) have lina: "islinintterm a" using "2.prems" by auto have nov0a: "novar0I a" using "2.prems" by auto let ?ys = "map (λx. lin_add (a,(Cst x))) (iupto(1,j))" have nov0ys: "∀ y∈ set ?ys. novar0I y" proof- have linx: "∀ x ∈ set (iupto(1,j)). islinintterm (Cst x)" by simp have nov0x: "∀ x ∈ set (iupto(1,j)). novar0I (Cst x)" by simp with nov0a lina linx have "∀ x∈ set (iupto(1,j)). novar0I (lin_add (a,Cst x))" by (simp add: lin_add_novar0) then show ?thesis by auto qed from "2.prems" have linas: "∀u∈set as. islinintterm u" by auto from "2.prems" have nov0as: "∀u∈set as. novar0I u" by auto from "2.hyps" linas nov0as have nov0alls: "∀u∈set (all_sums (j, as)). novar0I u" by simp from nov0alls nov0ys have cs: "(∀ u∈ set (?ys@ (all_sums (j,as))). novar0I u)" by (simp only: sym[OF list_all_iff]) auto have "all_sums(j,a#as) = ?ys@(all_sums(j,as))" by simp then have "?case = (∀ x∈ set (?ys@ (all_sums (j,as))). novar0I x)" by auto with cs show ?case by blast qed (* correctness theorem for all_sums*) lemma all_sums_ex: "(∃ j∈ {1..d}. ∃ b∈ (set xs). P (lin_add(b,Cst j))) = (∃ x∈ set (all_sums (d,xs)). P x)" proof(induct d xs rule: all_sums.induct) case (1 a) show ?case by simp next case (2 a y ys) have "(∃ x∈ set (map (λx. lin_add (y,(Cst x))) (iupto(1,a))) . P x) = (∃ j∈ set (iupto(1,a)). P (lin_add(y,Cst j)))" by auto also have "… = (∃ j∈ {1..a}. P (lin_add(y,Cst j)))" by (simp only : iupto_set) finally have dsj1:"(∃j∈{1..a}. P (lin_add (y, Cst j))) = (∃x∈set (map (λx. lin_add (y, Cst x)) (iupto (1, a))). P x)" by simp from prems have "(∃ j∈ {1..a}. ∃ b∈ (set (y#ys)). P (lin_add(b,Cst j))) = ((∃ j∈ {1..a}. P (lin_add(y,Cst j))) ∨ (∃ j∈ {1..a}. ∃ b ∈ set ys. P (lin_add(b,Cst j))))" by auto also have " … = ((∃ j∈ {1..a}. P (lin_add(y,Cst j))) ∨ (∃ x∈ set (all_sums(a, ys)). P x))" using prems by simp also have "… = ((∃x∈set (map (λx. lin_add (y, Cst x)) (iupto (1, a))). P x) ∨ (∃x∈set (all_sums (a, ys)). P x))" using dsj1 by simp also have "… = (∃ x∈ (set (map (λx. lin_add (y, Cst x)) (iupto (1, a)))) ∪ (set (all_sums(a, ys))). P x)" by blast finally show ?case by simp qed (* explode_minf (p,B) assumes that p is unified and B = bset p, it computes the rhs of cooper_mi_eq*) consts explode_minf :: "(QF × intterm list) => QF" recdef explode_minf "measure size" "explode_minf (q,B) = (let d = divlcm q; pm = minusinf q; dj1 = explode_disj ((map Cst (iupto (1, d))),pm) in (case dj1 of T => T | F => explode_disj (all_sums (d,B),q) | _ => (let dj2 = explode_disj (all_sums (d,B),q) in ( case dj2 of T => T | F => dj1 | _ => Or dj1 dj2))))" (* The result of the rhs of cooper's theorem doese not depend on Var 0*) lemma explode_minf_novar0: assumes unifp : "isunified p" and bst: "set (bset p) = set B" shows "novar0 (explode_minf (p,B))" proof- let ?d = "divlcm p" let ?pm = "minusinf p" let ?dj1 = "explode_disj (map Cst (iupto(1,?d)),?pm)" have qfpm: "isqfree ?pm" using unified_islinform[OF unifp] minusinf_qfree by simp have dpos: "?d >0" using unified_islinform[OF unifp] divlcm_pos by simp have "∀ x∈ set (map Cst (iupto(1,?d))). novar0I x" by auto then have dj1_nov0: "novar0 ?dj1" using qfpm explode_disj_novar0 by simp let ?dj2 = "explode_disj (all_sums (?d,B),p)" have bstlin: "∀b∈set B. islinintterm b" using bset_lin[OF unifp] bst by simp have bstnov0: "∀b∈set B. novar0I b" using bst bset_novar0[OF unifp] by simp have allsnov0: "∀x∈set (all_sums(?d,B)). novar0I x " by (simp add:all_sums_novar0[OF bstnov0 bstlin] ) then have dj2_nov0: "novar0 ?dj2" using explode_disj_novar0 unified_isqfree[OF unifp] bst by simp have "?dj1 = T ∨ ?dj1 = F ∨ (?dj1 ≠ T ∧ ?dj1 ≠ F)" by auto moreover { assume "?dj1 = T" then have ?thesis by simp } moreover { assume "?dj1 = F" then have ?thesis using bst dj2_nov0 by (simp add: Let_def)} moreover { assume dj1nFT:"?dj1 ≠ T ∧ ?dj1 ≠ F" have "?dj2 = T ∨ ?dj2 = F ∨ (?dj2 ≠ T ∧ ?dj2 ≠ F)" by auto moreover { assume "?dj2 = T" then have ?thesis by (cases ?dj1) simp_all } moreover { assume "?dj2 = F" then have ?thesis using dj1_nov0 bst by (cases ?dj1) (simp_all add: Let_def)} moreover { assume dj2_nTF:"?dj2 ≠ T ∧ ?dj2 ≠ F" let ?res = "λf. λg. (case f of T => T | F => g | _ => (case g of T => T| F => f| _ => Or f g))" have expth: "explode_minf (p,B) = ?res ?dj1 ?dj2" by (simp add: Let_def del: iupto.simps split del: split_if cong del: QF.weak_case_cong) then have ?thesis using prems or_case_novar0 [OF dj1nFT dj2_nTF dj1_nov0 dj2_nov0] by (simp add: Let_def del: iupto.simps cong del: QF.weak_case_cong) } ultimately have ?thesis by blast } ultimately show ?thesis by blast qed (* explode_minf computes the rhs of cooper's thm*) lemma explode_minf_corr: assumes unifp : "isunified p" and bst: "set (bset p) = set B" shows "(∃ x . qinterp (x#ats) p) = (qinterp (a#ats) (explode_minf (p,B)))" (is "(∃ x. ?P x) = (?EXP a p)") proof- let ?d = "divlcm p" let ?pm = "minusinf p" let ?dj1 = "explode_disj (map Cst (iupto(1,?d)),?pm)" have qfpm: "isqfree ?pm" using unified_islinform[OF unifp] minusinf_qfree by simp have nnfp: "isnnf p" by (rule unified_isnnf[OF unifp]) have "(∃j∈{1..?d}. qinterp (j # ats) (minusinf p)) = (∃j∈ set (iupto(1,?d)). qinterp (j#ats) (minusinf p))" (is "(∃ j∈ {1..?d}. ?QM j) = …") by (simp add: sym[OF iupto_set] ) also have "… =(∃j∈ set (iupto(1,?d)). qinterp ((I_intterm (a#ats) (Cst j))#ats) (minusinf p))" by simp also have "… = (∃j∈ set (map Cst (iupto(1,?d))). qinterp ((I_intterm (a#ats) j)#ats) (minusinf p))" by simp also have "… = (∃j∈ set (map Cst (iupto(1,?d))). qinterp (a#ats) (subst_p j (minusinf p)))" by (simp add: subst_p_corr[OF qfpm]) finally have dj1_thm: "(∃ j∈ {1..?d}. ?QM j) = (qinterp (a#ats) ?dj1)" by (simp only: explode_disj_corr[OF qfpm]) let ?dj2 = "explode_disj (all_sums (?d,B),p)" have bstlin: "∀b∈set B. islinintterm b" using bst by (simp add: bset_lin[OF unifp]) have bstnov0: "∀b∈set B. novar0I b" using bst by (simp add: bset_novar0[OF unifp]) have allsnov0: "∀x∈set (all_sums(?d,B)). novar0I x " by (simp add:all_sums_novar0[OF bstnov0 bstlin] ) have "(∃ j∈ {1..?d}. ∃ b∈ set B. ?P (I_intterm (a#ats) b + j)) = (∃ j∈ {1..?d}. ∃ b∈ set B. ?P (I_intterm (a#ats) (lin_add(b,Cst j))))" using bst by (auto simp add: lin_add_corr bset_lin[OF unifp]) also have "… = (∃ x ∈ set (all_sums (?d, B)). ?P (I_intterm (a#ats) x))" by (simp add: all_sums_ex[where P="λ t. ?P (I_intterm (a#ats) t)"]) finally have "(∃ j∈ {1..?d}. ∃ b∈ set B. ?P (I_intterm (a#ats) b + j)) = (∃ x ∈ set (all_sums (?d, B)). qinterp (a#ats) (subst_p x p))" using allsnov0 prems linform_isqfree unified_islinform[OF unifp] by (simp add: all_sums_ex subst_p_corr) also have "… = (qinterp (a#ats) ?dj2)" using linform_isqfree unified_islinform[OF unifp] by (simp add: explode_disj_corr) finally have dj2th: "(∃ j∈ {1..?d}. ∃ b∈ set B. ?P (I_intterm (a#ats) b + j)) = (qinterp (a#ats) ?dj2)" by simp let ?result = "λf. λg. (case f of T => T | F => g | _ => (case g of T => T | F => f | _ => Or f g))" have "?EXP a p = qinterp (a#ats) (?result ?dj1 ?dj2)" by (simp only: explode_minf.simps Let_def) also have "… = (qinterp (a#ats) ?dj1 ∨ qinterp (a#ats) ?dj2)" by (rule eval_Or_cases[where f="?dj1" and g="?dj2" and a="a" and ats="ats"]) also have "… = ((∃ j∈ {1..?d}. ?QM j) ∨ (∃ j∈ {1..?d}. ∃ b∈ set B. ?P (I_intterm (a#ats) b + j)))" by (simp add: dj1_thm dj2th) also have "… = (∃ x. ?P x)" using bst sym[OF cooper_mi_eq[OF unifp]] by simp finally show ?thesis by simp qed lemma explode_minf_corr2: assumes unifp : "isunified p" and bst: "set (bset p) = set B" shows "(qinterp ats (QEx p)) = (qinterp ats (decrvars(explode_minf (p,B))))" (is "?P = (?Qe p)") proof- have "?P = (∃x. qinterp (x#ats) p)" by simp also have "… = (qinterp (a # ats) (explode_minf (p,B)))" using unifp bst explode_minf_corr by simp finally have ex: "?P = (qinterp (a # ats) (explode_minf (p,B)))" . have nv0: "novar0 (explode_minf (p,B))" by (rule explode_minf_novar0[OF unifp]) show ?thesis using qinterp_novar0[OF nv0] ex by simp qed (* An implementation of cooper's method for both plus/minus/infinity *) (* unify the formula *) constdefs unify:: "QF => (QF × intterm list)" "unify p ≡ (let q = unitycoeff p; B = list_set(bset q); A = list_set (aset q) in if (length B ≤ length A) then (q,B) else (mirror q, map lin_neg A))" (* unify behaves like unitycoeff *) lemma unify_ex: assumes linp: "islinform p" shows "qinterp ats (QEx p) = qinterp ats (QEx (fst (unify p)))" proof- have "length (list_set(bset (unitycoeff p))) ≤ length (list_set (aset (unitycoeff p))) ∨ length (list_set(bset (unitycoeff p))) > length (list_set (aset (unitycoeff p)))" by arith moreover { assume "length (list_set(bset (unitycoeff p))) ≤ length (list_set (aset (unitycoeff p)))" then have "fst (unify p) = unitycoeff p" using unify_def by (simp add: Let_def) then have ?thesis using unitycoeff_corr[OF linp] by simp } moreover { assume "length (list_set(bset (unitycoeff p))) > length (list_set (aset (unitycoeff p)))" then have unif: "fst(unify p) = mirror (unitycoeff p)" using unify_def by (simp add: Let_def) let ?q ="unitycoeff p" have unifq: "isunified ?q" by(rule unitycoeff_unified[OF linp]) have linq: "islinform ?q" by (rule unified_islinform[OF unifq]) have "qinterp ats (QEx ?q) = qinterp ats (QEx (mirror ?q))" by (rule mirror_ex2[OF unifq]) moreover have "qinterp ats (QEx p) = qinterp ats (QEx ?q)" using unitycoeff_corr linp by simp ultimately have ?thesis using prems unif by simp } ultimately show ?thesis by blast qed (* unify's result is a unified formula *) lemma unify_unified: assumes linp: "islinform p" shows "isunified (fst (unify p))" using linp unitycoeff_unified mirror_unified unify_def unified_islinform by (auto simp add: Let_def) (* unify preserves quantifier-freeness*) lemma unify_qfree: assumes linp: "islinform p" shows "isqfree (fst(unify p))" using linp unify_unified unified_isqfree by simp lemma unify_bst: assumes linp: " islinform p" and unif: "unify p = (q,B)" shows "set B = set (bset q)" proof- let ?q = "unitycoeff p" let ?a = "aset ?q" let ?b = "bset ?q" let ?la = "list_set ?a" let ?lb = "list_set ?b" have " length ?lb ≤ length ?la ∨ length ?lb > length ?la" by arith moreover { assume "length ?lb ≤ length ?la" then have "unify p = (?q,?lb)"using unify_def prems by (simp add: Let_def) then have ?thesis using prems by (simp add: sym[OF list_set_set]) } moreover { assume "length ?lb > length ?la" have r: "unify p = (mirror ?q,map lin_neg ?la)"using unify_def prems by (simp add: Let_def) have lin: "∀ x∈ set (bset (mirror ?q)). islinintterm x" using bset_lin mirror_unified unitycoeff_unified[OF linp] by auto with r prems aset_eq_bset_mirror lin_neg_idemp unitycoeff_unified linp have "set B = set (map lin_neg (map lin_neg (bset (mirror (unitycoeff p)))))" by (simp add: sym[OF list_set_set]) also have "… = set (map (λx. lin_neg (lin_neg x)) (bset (mirror (unitycoeff p))))" by auto also have "… = set (bset (mirror (unitycoeff p)))" using lin lin_neg_idemp by (auto simp add: map_idI) finally have ?thesis using r prems aset_eq_bset_mirror lin_neg_idemp unitycoeff_unified linp by (simp add: sym[OF list_set_set])} ultimately show ?thesis by blast qed lemma explode_minf_unify_novar0: assumes linp: "islinform p" shows "novar0 (explode_minf (unify p))" proof- have "∃ q B. unify p = (q,B)" by simp then obtain "q" "B" where qB_def: "unify p = (q,B)" by blast have unifq: "isunified q" using unify_unified[OF linp] qB_def by simp have bst: "set B = set (bset q)" using unify_bst linp qB_def by simp from unifq bst explode_minf_novar0 show ?thesis using qB_def by simp qed lemma explode_minf_unify_corr2: assumes linp: "islinform p" shows "qinterp ats (QEx p) = qinterp ats (decrvars(explode_minf(unify p)))" proof- have "∃ q B. unify p = (q,B)" by simp then obtain "q" "B" where qB_def: "unify p = (q,B)" by blast have unifq: "isunified q" using unify_unified[OF linp] qB_def by simp have bst: "set (bset q) = set B" using unify_bst linp qB_def by simp from explode_minf_corr2[OF unifq bst] unify_ex[OF linp] show ?thesis using qB_def by simp qed (* An implementation of cooper's method *) constdefs cooper:: "QF => QF option" "cooper p ≡ lift_un (λq. decrvars(explode_minf (unify q))) (linform (nnf p))" (* cooper eliminates quantifiers *) lemma cooper_qfree: "(!! q q'. [|isqfree q ; cooper q = Some q'|] ==> isqfree q')" proof- fix "q" "q'" assume qfq: "isqfree q" and qeq: "cooper q = Some q'" from qeq have "∃p. linform (nnf q) = Some p" by (cases "linform (nnf q)") (simp_all add: cooper_def) then obtain "p" where p_def: "linform (nnf q) = Some p" by blast have linp: "islinform p" using p_def linform_lin nnf_isnnf qfq by auto have nnfq: "isnnf (nnf q)" using nnf_isnnf qfq by simp then have nnfp: "isnnf p" using linform_nnf[OF nnfq] p_def by auto have qfp: "isqfree p" using linp linform_isqfree by simp have "cooper q = Some (decrvars(explode_minf (unify p)))" using p_def by (simp add: cooper_def del: explode_minf.simps) then have "q' = decrvars (explode_minf (unify p))" using qeq by simp with linp qfp nnfp unify_unified unify_qfree unified_islinform show "isqfree q'" using novar0_qfree explode_minf_unify_novar0 decrvars_qfree by simp qed (* cooper preserves semantics *) lemma cooper_corr: "(!! q q' ats. [|isqfree q ; cooper q = Some q'|] ==> (qinterp ats (QEx q)) = (qinterp ats q'))" (is "!! q q' ats. [| _ ; _ |] ==> (?P ats (QEx q) = ?P ats q')") proof- fix "q" "q'" "ats" assume qfq: "isqfree q" and qeq: "cooper q = Some q'" from qeq have "∃p. linform (nnf q) = Some p" by (cases "linform (nnf q)") (simp_all add: cooper_def) then obtain "p" where p_def: "linform (nnf q) = Some p" by blast have linp: "islinform p" using p_def linform_lin nnf_isnnf qfq by auto have qfp: "isqfree p" using linp linform_isqfree by simp have nnfq: "isnnf (nnf q)" using nnf_isnnf qfq by simp then have nnfp: "isnnf p" using linform_nnf[OF nnfq] p_def by auto have "∀ ats. ?P ats q = ?P ats (nnf q)" using nnf_corr qfq by auto then have qeqp: "∀ ats. ?P ats q = ?P ats p" using linform_corr p_def nnf_isnnf qfq by auto have "cooper q = Some (decrvars (explode_minf (unify p)))" using p_def by (simp add: cooper_def del: explode_minf.simps) then have decr: "q' = decrvars(explode_minf (unify p))" using qeq by simp have eqq:"?P ats (QEx q) = ?P ats (QEx p)" using qeqp by auto with decr explode_minf_unify_corr2 unified_islinform unify_unified linp show "?P ats (QEx q) = ?P ats q'" by simp qed (* A decision procedure for Presburger Arithmetics *) constdefs pa:: "QF => QF option" "pa p ≡ lift_un psimpl (qelim(cooper, p))" lemma psimpl_qfree: "isqfree p ==> isqfree (psimpl p)" apply(induct p rule: isqfree.induct) apply(auto simp add: Let_def measure_def inv_image_def) apply (simp_all cong del: QF.weak_case_cong add: Let_def) apply (case_tac "psimpl p", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl p", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl p", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl p", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl q", auto) apply (case_tac "psimpl p", auto) apply (case_tac "lift_bin (λx y. lin_add (x, lin_neg y), linearize y, linearize z)", auto) apply (case_tac "a",auto) apply (case_tac "lift_bin (λx y. lin_add (x, lin_neg y), linearize ac, linearize ad)", auto) apply (case_tac "a",auto) apply (case_tac "ae", auto) apply (case_tac "linearize af", auto) by (case_tac "a", auto) (* pa eliminates quantifiers *) theorem pa_qfree: "!! p'. pa p = Some p' ==> isqfree p'" proof(simp only: pa_def) fix "p'" assume qep: "lift_un psimpl (qelim (cooper, p)) = Some p'" then have "∃ q. qelim (cooper, p) = Some q" by (cases "qelim(cooper, p)") auto then obtain "q" where q_def: "qelim (cooper, p) = Some q" by blast have "!!q q'. [|isqfree q; cooper q = Some q'|] ==> isqfree q'" using cooper_qfree by blast with q_def have "isqfree q" using qelim_qfree by blast then have "isqfree (psimpl q)" using psimpl_qfree by auto then show "isqfree p'" using prems by simp qed (* pa preserves semantics *) theorem pa_corr: "!! p'. pa p = Some p' ==> (qinterp ats p = qinterp ats p')" proof(simp only: pa_def) fix "p'" assume qep: "lift_un psimpl (qelim(cooper, p)) = Some p'" then have "∃ q. qelim (cooper, p) = Some q" by (cases "qelim(cooper, p)") auto then obtain "q" where q_def: "qelim (cooper, p) = Some q" by blast have cp1:"!!q q' ats. [|isqfree q; cooper q = Some q'|] ==> qinterp ats (QEx q) = qinterp ats q'" using cooper_corr by blast moreover have cp2: "!!q q'. [|isqfree q; cooper q = Some q'|] ==> isqfree q'" using cooper_qfree by blast ultimately have "qinterp ats p = qinterp ats q" using qelim_corr qep psimpl_corr q_def by blast then have "qinterp ats p = qinterp ats (psimpl q)" using psimpl_corr q_def by auto then show "qinterp ats p = qinterp ats p'" using prems by simp qed lemma [code]: "linearize (Mult i j) = (case linearize i of None => None | Some li => (case li of Cst b => (case linearize j of None => None | (Some lj) => Some (lin_mul(b,lj))) | _ => (case linearize j of None => None | (Some lj) => (case lj of Cst b => Some (lin_mul (b,li)) | _ => None))))" by (simp add: measure_def inv_image_def) lemma [code]: "psimpl (And p q) = (let p'= psimpl p in (case p' of F => F |T => psimpl q | _ => let q' = psimpl q in (case q' of F => F | T => p' | _ => (And p' q'))))" by (simp add: measure_def inv_image_def) lemma [code]: "psimpl (Or p q) = (let p'= psimpl p in (case p' of T => T | F => psimpl q | _ => let q' = psimpl q in (case q' of T => T | F => p' | _ => (Or p' q'))))" by (simp add: measure_def inv_image_def) lemma [code]: "psimpl (Imp p q) = (let p'= psimpl p in (case p' of F => T |T => psimpl q | NOT p1 => let q' = psimpl q in (case q' of F => p1 | T => T | _ => (Or p1 q')) | _ => let q' = psimpl q in (case q' of F => NOT p' | T => T | _ => (Imp p' q'))))" by (simp add: measure_def inv_image_def) declare zdvd_iff_zmod_eq_0 [code] (* generate_code ("presburger.ML") test = "pa" use "rcooper.ML" oracle rpresburger_oracle ("term") = RCooper.rpresburger_oracle use "rpresbtac.ML" setup RPresburger.setup *) end
lemma lift_bin_Some:
lift_bin (c, x, y) = Some t ==> (∃a. x = Some a) ∧ (∃b. y = Some b)
lemma qff:
[| !!q q'. [| isqfree q; qe q = Some q' |] ==> isqfree q'; qelim (qe, p) = Some p' |] ==> isqfree p'
lemma qff:
[| !!q q' ats. [| isqfree q; qe q = Some q' |] ==> qinterp ats (QEx q) = qinterp ats q'; !!q q'. [| isqfree q; qe q = Some q' |] ==> isqfree q'; qelim (qe, p) = Some p' |] ==> qinterp ats p = qinterp ats p'
lemma
0 < lgth q
lemma nnf_corr:
isqfree p ==> qinterp ats p = qinterp ats (nnf p)
lemma nnf_isnnf:
isqfree p ==> isnnf (nnf p)
lemma nnf_isqfree:
isnnf p ==> isqfree p
lemma nnf_qfree:
isqfree p ==> isqfree (nnf p)
lemma islinintterm_subt:
islinintterm (Add (Mult (Cst i) (Var n)) r) ==> islinintterm r
lemma islinintterm_cnz:
islinintterm (Add (Mult (Cst i) (Var n)) r) ==> i ≠ 0
lemma islininttermc0r:
islinintterm (Add (Mult (Cst c) (Var n)) r) ==> c ≠ 0 ∧ islinintterm r
lemma islinintterm_eq_islint:
islinintterm t = islint t
lemma islintn_mon:
[| islintn (n, t); m ≤ n |] ==> islintn (m, t)
lemma islintn_subt:
islintn (n, Add (Mult (Cst i) (Var m)) r) ==> islintn (m + 1, r)
lemma nth_pos:
0 < n --> (x # xs) ! n = (y # xs) ! n
lemma nth_pos2:
0 < n ==> (x # xs) ! n = xs ! (n - 1)
lemma intterm_novar0:
islinintterm (Add (Mult (Cst i) (Var n)) r) ==> I_intterm (x # ats) r = I_intterm (y # ats) r
lemma linterm_novar0:
[| islintn (n, t); 0 < n |] ==> I_intterm (x # ats) t = I_intterm (y # ats) t
lemma dvd_period:
a dvd d ==> (a dvd x + t) = (a dvd x + c * d + t)
lemma lin_add_cst_corr:
islintn (n0.0, b) ==> I_intterm ats (lin_add (Cst a, b)) = I_intterm ats (Add (Cst a) b)
lemma lin_add_cst_corr2:
islintn (n0.0, b) ==> I_intterm ats (lin_add (b, Cst a)) = I_intterm ats (Add b (Cst a))
lemma lin_add_corrh:
[| islintn (n01.0, a); islintn (n02.0, b) |] ==> I_intterm ats (lin_add (a, b)) = I_intterm ats (Add a b)
lemma lin_add_corr:
[| islinintterm a; islinintterm b |] ==> I_intterm ats (lin_add (a, b)) = I_intterm ats (Add a b)
lemma lin_add_cst_lint:
islintn (n0.0, b) ==> islintn (n0.0, lin_add (Cst i, b))
lemma lin_add_cst_lint2:
islintn (n0.0, b) ==> islintn (n0.0, lin_add (b, Cst i))
lemma lin_add_lint:
[| islintn (n01.0, a); islintn (n02.0, b); n0.0 ≤ min n01.0 n02.0 |] ==> islintn (n0.0, lin_add (a, b))
lemma lin_add_lin:
[| islinintterm a; islinintterm b |] ==> islinintterm (lin_add (a, b))
lemma zmult_zadd_distrib:
a * (b + c) = a * b + a * c
lemma lin_mul_corr:
islinintterm t ==> I_intterm ats (lin_mul (c, t)) = I_intterm ats (Mult (Cst c) t)
lemma lin_mul_lin:
islinintterm t ==> islinintterm (lin_mul (c, t))
lemma lin_mul0:
islinintterm t ==> lin_mul (0, t) = Cst 0
lemma lin_mul_lintn:
islintn (m, t) ==> islintn (m, lin_mul (l, t))
lemma lin_neg_corr:
islinintterm t ==> I_intterm ats (lin_neg t) = I_intterm ats (Neg t)
lemma lin_neg_lin:
islinintterm t ==> islinintterm (lin_neg t)
lemma lin_neg_idemp:
islinintterm i ==> lin_neg (lin_neg i) = i
lemma lin_neg_lin_add_distrib:
[| islinintterm a; islinintterm b |] ==> lin_neg (lin_add (a, b)) = lin_add (lin_neg a, lin_neg b)
lemma linearize_linear1:
linearize t ≠ None ==> islinintterm (the (linearize t))
lemma linearize_linear:
linearize t = Some t' ==> islinintterm t'
lemma linearize_corr1:
linearize t ≠ None ==> I_intterm ats t = I_intterm ats (the (linearize t))
lemma linearize_corr:
linearize t = Some t' ==> I_intterm ats t = I_intterm ats t'
lemma linform_nnf:
[| isnnf p; linform p = Some p' |] ==> isnnf p'
lemma linform_corr:
[| isnnf p; linform p = Some lp |] ==> qinterp ats p = qinterp ats lp
lemma linform_lin:
[| isnnf p; linform p = Some lp |] ==> islinform lp
lemma linform_isnnf:
islinform p ==> isnnf p
lemma linform_isqfree:
islinform p ==> isqfree p
lemma linform_qfree:
[| isnnf p; linform p = Some p' |] ==> isqfree p'
lemma lcm_dvd1:
[| 0 < m; 0 < n |] ==> m dvd lcm (m, n)
lemma lcm_dvd2:
[| 0 < m; 0 < n |] ==> n dvd lcm (m, n)
lemma ilcm_dvd1:
[| a ≠ 0; b ≠ 0 |] ==> a dvd ilcm a b
lemma ilcm_dvd2:
[| a ≠ 0; b ≠ 0 |] ==> b dvd ilcm a b
lemma zdvd_self_abs1:
d dvd ¦d¦
lemma zdvd_self_abs2:
¦d¦ dvd d
lemma lcm_pos:
[| 0 < m; 0 < n |] ==> 0 < lcm (m, n)
lemma ilcm_pos:
[| 0 < a; 0 < b |] ==> 0 < ilcm a b
lemma formlcm_pos:
islinform p ==> 0 < formlcm p
lemma divideallc_mono:
[| divideallc (c, p); c dvd d |] ==> divideallc (d, p)
lemma formlcm_divideallc:
islinform p ==> divideallc (formlcm p, p)
lemma unified_islinform:
isunified p ==> islinform p
lemma adjustcoeff_lenpos:
0 < n ==> adjustcoeff (l, Le (Add (Mult (Cst i) (Var n)) r) (Cst c)) = Le (Add (Mult (Cst i) (Var n)) r) (Cst c)
lemma adjustcoeff_eqnpos:
0 < n ==> adjustcoeff (l, Eq (Add (Mult (Cst i) (Var n)) r) (Cst c)) = Eq (Add (Mult (Cst i) (Var n)) r) (Cst c)
lemma zmult_zle_mono:
[| i ≤ j; 0 ≤ k |] ==> k * i ≤ k * j
lemma zmult_zle_mono_eq:
0 < k ==> (i ≤ j) = (k * i ≤ k * j)
lemma adjustcoeff_le_corr:
[| 0 < l; 0 < i; i dvd l |] ==> (i * x + r ≤ 0) = (l * x + l div i * r ≤ 0)
lemma adjustcoeff_le_corr2:
[| 0 < l; i < 0; i dvd l |] ==> (i * x + r ≤ 0) = (- l * x + - (l div i) * r ≤ 0)
lemma dvd_div_pos:
[| 0 < b; a ≠ 0; a dvd b |] ==> b div a * a = b
lemma adjustcoeff_eq_corr:
[| 0 < l; i ≠ 0; i dvd l |] ==> (i * x + r = 0) = (l * x + l div i * r = 0)
lemma adjustcoeff_corr:
[| islinform p; divideallc (l, p); 0 < l |] ==> qinterp (a # ats) p = qinterp (a * l # ats) (adjustcoeff (l, p))
lemma unitycoeff_corr:
islinform p ==> qinterp ats (QEx p) = qinterp ats (QEx (unitycoeff p))
lemma adjustcoeff_unified:
[| islinform p; divideallc (l, p); 0 < l |] ==> isunified (adjustcoeff (l, p))
lemma adjustcoeff_lcm_unified:
islinform p ==> isunified (adjustcoeff (formlcm p, p))
lemma unitycoeff_unified:
islinform p ==> isunified (unitycoeff p)
lemma unified_isnnf:
isunified p ==> isnnf p
lemma unified_isqfree:
isunified p ==> isqfree p
lemma alldivide_mono:
[| alldivide (d, p); d dvd d' |] ==> alldivide (d', p)
lemma zdvd_eq_zdvd_abs:
(d dvd d') = (d dvd ¦d'¦)
lemma zdvd_refl_abs:
d dvd ¦d¦
lemma divlcm_pos:
islinform p ==> 0 < divlcm p
lemma nz_le:
0 < x ==> x ≠ 0
lemma divlcm_corr:
islinform p ==> alldivide (divlcm p, p)
lemma minusinf_eq:
isunified p ==> ∃z. ∀x<z. qinterp (x # ats) p = qinterp (x # ats) (minusinf p)
lemma minusinf_repeats:
[| alldivide (d, p); isunified p |] ==> qinterp (x # ats) (minusinf p) = qinterp ((x + c * d) # ats) (minusinf p)
lemma minusinf_repeats2:
[| alldivide (d, p); isunified p |] ==> ∀x k. qinterp (x # ats) (minusinf p) = qinterp ((x - k * d) # ats) (minusinf p)
lemma minusinf_lemma:
[| isunified p; ∃j∈{1..d}. qinterp (j # ats) (minusinf p) |] ==> ∃x. qinterp (x # ats) p
lemma minusinf_disj:
isunified p ==> (∃x. qinterp (x # ats) (minusinf p)) = (∃j∈{1..divlcm p}. qinterp (j # ats) (minusinf p))
lemma minusinf_qfree:
islinform p ==> isqfree (minusinf p)
lemma bset_lin:
isunified p ==> ∀b∈set (bset p). islinintterm b
lemma bset_disj_repeat:
[| isunified p; alldivide (d, p); 0 < d; qinterp (x # ats) q ∧ ¬ (∃j∈{1..d}. ∃b∈set (bset p). qinterp ((I_intterm (a # ats) b + j) # ats) q) ∧ qinterp (x # ats) p |] ==> qinterp ((x - d) # ats) p
lemma bset_disj_repeat2:
isunified p ==> ∀x. ¬ (∃j∈{1..divlcm p}. ∃b∈set (bset p). qinterp ((I_intterm (a # ats) b + j) # ats) p) --> qinterp (x # ats) p --> qinterp ((x - divlcm p) # ats) p
lemma cooper_mi_eq:
isunified p ==> (∃x. qinterp (x # ats) p) = ((∃j∈{1..divlcm p}. qinterp (j # ats) (minusinf p)) ∨ (∃j∈{1..divlcm p}. ∃b∈set (bset p). qinterp ((I_intterm (a # ats) b + j) # ats) p))
lemma
(¦i¦ = 1) = (i = 1 ∨ i = -1)
lemma mirror_unified:
isunified p ==> isunified (mirror p)
lemma plusinf_eq_minusinf_mirror:
isunified p ==> qinterp (x # ats) (plusinf p) = qinterp (- x # ats) (minusinf (mirror p))
lemma aset_eq_bset_mirror:
isunified p ==> set (aset p) = set (map lin_neg (bset (mirror p)))
lemma aset_eq_bset_mirror2:
isunified p ==> aset p = map lin_neg (bset (mirror p))
lemma divlcm_mirror_eq:
isunified p ==> divlcm p = divlcm (mirror p)
lemma mirror_interp:
isunified p ==> qinterp (x # ats) p = qinterp (- x # ats) (mirror p)
lemma mirror_interp2:
islinform p ==> qinterp (x # ats) p = qinterp (- x # ats) (mirror p)
lemma mirror_ex:
isunified p ==> (∃x. qinterp (x # ats) p) = (∃y. qinterp (y # ats) (mirror p))
lemma mirror_ex2:
isunified p ==> qinterp ats (QEx p) = qinterp ats (QEx (mirror p))
lemma cooper_pi_eq:
isunified p ==> (∃x. qinterp (x # ats) p) = ((∃j∈{1..divlcm p}. qinterp (- j # ats) (plusinf p)) ∨ (∃j∈{1..divlcm p}. ∃b∈set (aset p). qinterp ((I_intterm (a # ats) b - j) # ats) p))
lemma subst_it_corr:
I_intterm (a # ats) (subst_it i t) = I_intterm (I_intterm (a # ats) i # ats) t
lemma subst_p_corr:
isqfree p ==> qinterp (a # ats) (subst_p i p) = qinterp (I_intterm (a # ats) i # ats) p
lemma I_intterm_novar0:
novar0I x ==> I_intterm (a # ats) x = I_intterm (b # ats) x
lemma subst_p_novar0_corr:
[| isqfree p; novar0I i |] ==> qinterp (a # ats) (subst_p i p) = qinterp (I_intterm (b # ats) i # ats) p
lemma lin_novar0:
[| islinintterm x; novar0I x |] ==> ∃n>0. islintn (n, x)
lemma lintnpos_novar0:
[| 0 < n; islintn (n, x) |] ==> novar0I x
lemma lin_add_novar0:
[| novar0I a; novar0I b; islinintterm a; islinintterm b |] ==> novar0I (lin_add (a, b))
lemma lin_mul_novar0:
[| islinintterm x; novar0I x |] ==> novar0I (lin_mul (i, x))
lemma lin_neg_novar0:
[| islinintterm x; novar0I x |] ==> novar0I (lin_neg x)
lemma intterm_subt_novar0:
islinintterm (Add (Mult (Cst c) (Var n)) r) ==> novar0I r
lemma intterm_decrvarsI:
novar0I t ==> I_intterm (a # ats) t = I_intterm ats (decrvarsI t)
lemma decrvars_qfree:
isqfree p ==> isqfree (decrvars p)
lemma novar0_qfree:
novar0 p ==> isqfree p
lemma qinterp_novar0:
novar0 p ==> qinterp (a # ats) p = qinterp ats (decrvars p)
lemma bset_novar0:
isunified p ==> ∀b∈set (bset p). novar0I b
lemma subst_it_novar0:
novar0I x ==> novar0I (subst_it x t)
lemma subst_p_novar0:
[| novar0I x; isqfree p |] ==> novar0 (subst_p x p)
lemma linearize_novar0:
[| novar0I t; linearize t = Some t' |] ==> novar0I t'
lemma psimpl_corr:
qinterp ats p = qinterp ats (psimpl p)
lemma psimpl_novar0:
novar0 p ==> novar0 (psimpl p)
lemma explode_disj_disj:
isqfree p ==> qinterp (x # xs) (explode_disj (i # is, p)) = (qinterp (x # xs) (subst_p i p) ∨ qinterp (x # xs) (explode_disj (is, p)))
lemma explode_disj_corr:
isqfree p ==> (∃x∈set xs. qinterp (a # ats) (subst_p x p)) = qinterp (a # ats) (explode_disj (xs, p))
lemma explode_disj_novar0:
[| ∀x∈set xs. novar0I x; isqfree p |] ==> novar0 (explode_disj (xs, p))
lemma eval_Or_cases:
qinterp (a # ats) (case f of T => T | F => g | _ => case g of T => T | F => f | _ => Or f g) = (qinterp (a # ats) f ∨ qinterp (a # ats) g)
lemma or_case_novar0:
[| f ≠ T ∧ f ≠ F; g ≠ T ∧ g ≠ F; novar0 f; novar0 g |] ==> novar0 (case f of T => T | F => g | _ => case g of T => T | F => f | _ => Or f g)
lemma list_insert_set:
set (list_insert x xs) = set (x # xs)
lemma list_union_set:
set (list_union (xs, ys)) = set (xs @ ys)
lemma list_set_set:
set xs = set (list_set xs)
lemma iupto_set:
set (iupto (i, j)) = {i..j}
lemma all_sums_novar0:
[| ∀x∈set xs. novar0I x; ∀x∈set xs. islinintterm x |] ==> ∀x∈set (all_sums (d, xs)). novar0I x
lemma all_sums_ex:
(∃j∈{1..d}. ∃b∈set xs. P (lin_add (b, Cst j))) = (∃x∈set (all_sums (d, xs)). P x)
lemma explode_minf_novar0:
[| isunified p; set (bset p) = set B |] ==> novar0 (explode_minf (p, B))
lemma explode_minf_corr:
[| isunified p; set (bset p) = set B |] ==> (∃x. qinterp (x # ats) p) = qinterp (a # ats) (explode_minf (p, B))
lemma explode_minf_corr2:
[| isunified p; set (bset p) = set B |] ==> qinterp ats (QEx p) = qinterp ats (decrvars (explode_minf (p, B)))
lemma unify_ex:
islinform p ==> qinterp ats (QEx p) = qinterp ats (QEx (fst (unify p)))
lemma unify_unified:
islinform p ==> isunified (fst (unify p))
lemma unify_qfree:
islinform p ==> isqfree (fst (unify p))
lemma unify_bst:
[| islinform p; unify p = (q, B) |] ==> set B = set (bset q)
lemma explode_minf_unify_novar0:
islinform p ==> novar0 (explode_minf (unify p))
lemma explode_minf_unify_corr2:
islinform p ==> qinterp ats (QEx p) = qinterp ats (decrvars (explode_minf (unify p)))
lemma cooper_qfree:
[| isqfree q; cooper q = Some q' |] ==> isqfree q'
lemma cooper_corr:
[| isqfree q; cooper q = Some q' |] ==> qinterp ats (QEx q) = qinterp ats q'
lemma psimpl_qfree:
isqfree p ==> isqfree (psimpl p)
theorem pa_qfree:
pa p = Some p' ==> isqfree p'
theorem pa_corr:
pa p = Some p' ==> qinterp ats p = qinterp ats p'
lemma
linearize (Mult i j) = (case linearize i of None => None | Some li => case li of Cst b => case linearize j of None => None | Some lj => Some (lin_mul (b, lj)) | _ => case linearize j of None => None | Some lj => case lj of Cst b => Some (lin_mul (b, li)) | _ => None)
lemma
psimpl (And p q) = (let p' = psimpl p in case p' of T => psimpl q | F => F | _ => let q' = psimpl q in case q' of T => p' | F => F | _ => And p' q')
lemma
psimpl (Or p q) = (let p' = psimpl p in case p' of T => T | F => psimpl q | _ => let q' = psimpl q in case q' of T => T | F => p' | _ => Or p' q')
lemma
psimpl (Imp p q) = (let p' = psimpl p in case p' of T => psimpl q | F => T | NOT p1 => let q' = psimpl q in case q' of T => T | F => p1 | _ => Or p1 q' | _ => let q' = psimpl q in case q' of T => T | F => NOT p' | _ => Imp p' q')