--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Reflected_Presburger.thy Wed Sep 14 17:25:52 2005 +0200
@@ -0,0 +1,5726 @@
+(* A formalization of quantifier elimination for Presburger arithmetic*)
+(* based on a generic quantifier elimination algorithm and
+ cooper's methos to eliminate on \<exists> *)
+
+theory Reflected_Presburger
+imports Main
+uses ("rcooper.ML") ("rpresbtac.ML")
+begin
+
+(* Shadow syntax for integer terms *)
+datatype intterm =
+ Cst int
+ | Var nat
+ | Neg intterm
+ | Add intterm intterm
+ | Sub intterm intterm
+ | Mult intterm intterm
+
+(* interpretatation of intterms , takes bound variables and free variables *)
+consts I_intterm :: "int list \<Rightarrow> intterm \<Rightarrow> 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 \<Rightarrow> QF \<Rightarrow> 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 \<le> I_intterm ats it2)"
+"qinterp ats (Ge it1 it2) = (I_intterm ats it1 \<ge> 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) = (\<not>(qinterp ats p))"
+"qinterp ats (And p q) = (qinterp ats p \<and> qinterp ats q)"
+"qinterp ats (Or p q) = (qinterp ats p \<or> qinterp ats q)"
+"qinterp ats (Imp p q) = (qinterp ats p \<longrightarrow> qinterp ats q)"
+"qinterp ats (Equ p q) = (qinterp ats p = qinterp ats q)"
+"qinterp ats (QAll p) = (\<forall>x. qinterp (x#ats) p)"
+"qinterp ats (QEx p) = (\<exists>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 reult is of type QF option *)
+
+consts lift_bin:: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<times> 'a option \<times> 'a option \<Rightarrow> 'b option"
+recdef lift_bin "measure (\<lambda>(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 "(\<exists>a. x = Some a) \<and> (\<exists>b. y = Some b)"
+ using ls
+ by (cases "x", auto) (cases "y", auto)+
+
+consts lift_un:: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
+primrec
+"lift_un c None = None"
+"lift_un c (Some p) = Some (c p)"
+
+consts lift_qe:: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a option \<Rightarrow> 'b option"
+primrec
+"lift_qe qe None = None"
+"lift_qe qe (Some p) = qe p"
+
+(* generic quantifier elimination *)
+consts qelim :: "(QF \<Rightarrow> QF option) \<times> QF \<Rightarrow> QF option"
+recdef qelim "measure (\<lambda>(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 \<Rightarrow> bool"
+recdef isqfree "measure size"
+"isqfree (QAll p) = False"
+"isqfree (QEx p) = False"
+"isqfree (And p q) = (isqfree p \<and> isqfree q)"
+"isqfree (Or p q) = (isqfree p \<and> isqfree q)"
+"isqfree (Imp p q) = (isqfree p \<and> isqfree q)"
+"isqfree (Equ p q) = (isqfree p \<and> isqfree q)"
+"isqfree (NOT p) = isqfree p"
+"isqfree p = True"
+
+(* qelim lifts quantifierfreeness*)
+lemma qelim_qfree:
+ assumes qeqf: "(\<And> q q'. \<lbrakk>isqfree q ; qe q = Some q'\<rbrakk> \<Longrightarrow> isqfree q')"
+ shows qff:"\<And> p'. qelim (qe, p) = Some p' \<Longrightarrow> 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 "\<exists> 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 "\<And>q q'. \<lbrakk>isqfree q; qe q = Some q'\<rbrakk> \<Longrightarrow> 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: "(\<exists>p1. qelim(qe,p) = Some p1) \<and>
+ (\<exists>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: "(\<exists>p1. qelim(qe,p) = Some p1) \<and>
+ (\<exists>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: "(\<exists>p1. qelim(qe,p) = Some p1) \<and>
+ (\<exists>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: "(\<exists>p1. qelim(qe,p) = Some p1) \<and>
+ (\<exists>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 "\<exists> 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 "\<And>q q'. \<lbrakk>isqfree q; qe q = Some q'\<rbrakk> \<Longrightarrow> 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 "\<exists> 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 "\<exists> 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 "\<exists> 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: "(\<And> q q' ats. \<lbrakk>isqfree q ; qe q = Some q'\<rbrakk> \<Longrightarrow> (qinterp ats (QEx q)) = (qinterp ats q'))"
+ and qeqf: "(\<And> q q'. \<lbrakk>isqfree q ; qe q = Some q'\<rbrakk> \<Longrightarrow> isqfree q')"
+ shows qff:"\<And> p' ats. qelim (qe, p) = Some p' \<Longrightarrow> (qinterp ats p = qinterp ats p')" (is "\<And> p' ats. ?Qe p p' \<Longrightarrow> (?F ats p = ?F ats p')")
+ using qeqf qecorr
+proof (induct p)
+ case (NOT f)
+ from "NOT.prems" have "\<exists>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: "(\<exists>f1. qelim(qe,f) = Some f1) \<and>
+ (\<exists>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: "(\<exists>f1. qelim(qe,f) = Some f1) \<and>
+ (\<exists>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: "(\<exists>f1. qelim(qe,f) = Some f1) \<and>
+ (\<exists>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: "(\<exists>f1. qelim(qe,f) = Some f1) \<and>
+ (\<exists>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 "\<exists> 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: "\<forall> 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 "\<exists> 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 "\<exists> 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 "\<exists> 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 "\<exists> 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 "\<exists> 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: "\<forall> 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: "\<forall> 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) = (\<forall>x. ?F (x#ats) f)" by simp
+ also have "\<dots> = (\<not> (\<exists> x. ?F (x#ats) (NOT f)))" by simp
+ also have "\<dots> = (\<not> (\<exists> x. ?F (x#ats) (NOT (NOT f2))))" using feqf2
+ by auto
+ also have "\<dots> = (\<not> (\<exists> x. ?F (x#ats) f2))" by simp
+ also have "\<dots> = (\<not> (?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 \<Rightarrow> nat"
+ nnf :: "QF \<Rightarrow> 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 (\<lambda>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 \<Rightarrow> bool"
+recdef isnnf "measure (\<lambda>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 \<and> isnnf q)"
+ "isnnf (Or p q) = (isnnf p \<and> 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 \<Longrightarrow> 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 \<Longrightarrow> isnnf (nnf p)"
+by (induct p rule: nnf.induct, auto)
+
+lemma nnf_isqfree: "isnnf p \<Longrightarrow> isqfree p"
+by (induct p rule: isnnf.induct) auto
+
+(* nnf preserves quantifier freeness *)
+lemma nnf_qfree: "isqfree p \<Longrightarrow> isqfree(nnf p)"
+ using nnf_isqfree nnf_isnnf by simp
+
+(* Linearization and normalization of formulae *)
+(* Definition of linearity of an intterm *)
+
+consts islinintterm :: "intterm \<Rightarrow> bool"
+recdef islinintterm "measure size"
+"islinintterm (Cst i) = True"
+"islinintterm (Add (Mult (Cst i) (Var n)) (Cst i')) = (i \<noteq> 0)"
+"islinintterm (Add (Mult (Cst i) (Var n)) (Add (Mult (Cst i') (Var n')) r)) = ( i \<noteq> 0 \<and> i' \<noteq> 0 \<and> n < n' \<and> 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 \<noteq> 0 for linear term c.n + r*)
+lemma islinintterm_cnz:
+ assumes lr: "islinintterm (Add (Mult (Cst i) (Var n)) r)"
+ shows "i \<noteq> 0"
+using lr
+by (induct r rule: islinintterm.induct) auto
+
+lemma islininttermc0r: "islinintterm (Add (Mult (Cst c) (Var n)) r) \<Longrightarrow> (c \<noteq> 0 \<and> islinintterm r)"
+by (induct r rule: islinintterm.induct, simp_all)
+
+(* An alternative linearity definition *)
+consts islintn :: "(nat \<times> intterm) \<Rightarrow> bool"
+recdef islintn "measure (\<lambda> (n,t). (size t))"
+"islintn (n0, Cst i) = True"
+"islintn (n0, Add (Mult (Cst i) (Var n)) r) = (i \<noteq> 0 \<and> n0 \<le> n \<and> islintn (n+1,r))"
+"islintn (n0, t) = False"
+
+constdefs islint :: "intterm \<Rightarrow> bool"
+ "islint t \<equiv> 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 \<le> 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 \<longrightarrow> (x#xs) ! n = (y#xs) ! n"
+using Nat.gr0_conv_Suc
+by clarsimp
+
+lemma nth_pos2: "0 < n \<Longrightarrow> (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 doese not depend
+ on the first variable if it doese 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 "\<forall>x.\<forall>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 \<times> intterm \<Rightarrow> intterm"
+recdef lin_add "measure (\<lambda>(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 \<le> 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: "\<And> n01 n02. \<lbrakk> islintn (n01,a) ; islintn (n02,b)\<rbrakk>
+ \<Longrightarrow> 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 \<and> i+j = 0) \<or> (n = m \<and> i+j \<noteq> 0) \<or> n < m \<or> m < n " by arith
+ moreover
+ {assume "n=m\<and>i+j=0" hence ?case using prems by (auto simp add: sym[OF zadd_zmult_distrib]) }
+ moreover
+ {assume "n=m\<and>i+j\<noteq>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: "\<And> n0 n01 n02. \<lbrakk> islintn (n01,a) ; islintn (n02,b); n0 \<le> min n01 n02 \<rbrakk>
+ \<Longrightarrow> 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 \<and> i + j = 0) \<or> (n = m \<and> i+j \<noteq> 0) \<or> n <m \<or> 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 \<noteq> 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 \<times> intterm \<Rightarrow> intterm"
+recdef lin_mul "measure (\<lambda>(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:
+ "\<And> m. islintn(m,t) \<Longrightarrow> 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 \<Rightarrow> 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 \<or> n1 < n2 \<or> 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 \<Rightarrow> intterm option"
+recdef linearize "measure (\<lambda>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(\<lambda> x. \<lambda> y. lin_add(x,y), linearize i, linearize j)"
+"linearize (Sub i j) =
+ lift_bin(\<lambda> x. \<lambda> y. lin_add(x,lin_neg y), linearize i, linearize j)"
+"linearize (Mult i j) =
+ (case linearize i of
+ None \<Rightarrow> None
+ | Some li \<Rightarrow> (case li of
+ Cst b \<Rightarrow> (case linearize j of
+ None \<Rightarrow> None
+ | (Some lj) \<Rightarrow> Some (lin_mul(b,lj)))
+ | _ \<Rightarrow> (case linearize j of
+ None \<Rightarrow> None
+ | (Some lj) \<Rightarrow> (case lj of
+ Cst b \<Rightarrow> Some (lin_mul (b,li))
+ | _ \<Rightarrow> None))))"
+
+lemma linearize_linear1:
+ assumes lin: "linearize t \<noteq> 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) \<or> (\<exists>li. linearize i = Some li)" by auto
+ moreover
+ { assume "linearize i = None" with prems have ?thesis by auto}
+ moreover
+ { assume lini: "\<exists>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) \<or> ((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or> ((\<exists> li. linearize i = Some li) \<and> (\<exists> 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: "\<exists> 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: "\<exists>li. linearize i = Some li"
+ and linj: "\<exists>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) \<or> ((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or> ((\<exists> li. linearize i = Some li) \<and> (\<exists> 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: "\<exists> 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: "\<exists>li. linearize i = Some li"
+ and linj: "\<exists>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) \<or>
+ ((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or>
+ ((\<exists> li. linearize i = Some li) \<and> (\<exists> bj. linearize j = Some (Cst bj)))
+ \<or> ((\<exists> bi. linearize i = Some (Cst bi)) \<and> (\<exists> lj. linearize j = Some lj))
+ \<or> ((\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)) \<and> (\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> 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: "\<exists> 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: "\<exists>li. linearize i = Some li"
+ and linj: "\<exists>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: "\<exists>bi. linearize i = Some (Cst bi)"
+ and linj: "\<exists>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: "\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)"
+ and ljnc: "\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)"
+ from linc obtain "li" where "linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)" by blast
+ moreover
+ from ljnc obtain "lj" where "linearize j = Some lj \<and> \<not> (\<exists> 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: "\<And> t'. linearize t = Some t' \<Longrightarrow> islinintterm t'"
+proof-
+ fix t'
+ assume lint: "linearize t = Some t'"
+ from lint have lt: "linearize t \<noteq> 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 \<noteq> 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) \<or> (\<exists>li. linearize i = Some li)" by auto
+ moreover
+ {
+ assume "linearize i = None"
+ have ?thesis using prems by simp
+ }
+ moreover
+ {
+ assume lini: "\<exists>li. linearize i = Some li"
+ from lini have lini2: "linearize i \<noteq> 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) \<or> ((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or> ((\<exists> li. linearize i = Some li) \<and> (\<exists> 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: "\<exists> 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: "\<exists>li. linearize i = Some li"
+ and linj: "\<exists>lj. linearize j = Some lj"
+ from lini have lini2: "linearize i \<noteq> None" by simp
+ from linj have linj2: "linearize j \<noteq> 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) \<or> ((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or> ((\<exists> li. linearize i = Some li) \<and> (\<exists> 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: "\<exists> 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: "\<exists>li. linearize i = Some li"
+ and linj: "\<exists>lj. linearize j = Some lj"
+ from lini have lini2: "linearize i \<noteq> None" by simp
+ from linj have linj2: "linearize j \<noteq> 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) \<or>
+ ((\<exists> li. linearize i = Some li) \<and> linearize j = None) \<or>
+ ((\<exists> li. linearize i = Some li) \<and> (\<exists> bj. linearize j = Some (Cst bj)))
+ \<or> ((\<exists> bi. linearize i = Some (Cst bi)) \<and> (\<exists> lj. linearize j = Some lj))
+ \<or> ((\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)) \<and> (\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> 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: "\<exists> 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: "\<exists>li. linearize i = Some li"
+ and linj: "\<exists>bj. linearize j = Some (Cst bj)"
+ from lini have lini2: "linearize i \<noteq> None" by simp
+ from linj have linj2: "linearize j \<noteq> 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: "\<exists>bi. linearize i = Some (Cst bi)"
+ and linj: "\<exists>lj. linearize j = Some lj"
+ from lini have lini2 : "linearize i \<noteq> None" by auto
+ from linj have linj2 : "linearize j \<noteq> 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: "\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)"
+ and ljnc: "\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)"
+ from linc obtain "li" where "\<exists> li. linearize i = Some li \<and> \<not> (\<exists> bi. li = Cst bi)" by blast
+ moreover
+ from ljnc obtain "lj" where "\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> 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: "\<And> t'. linearize t = Some t' \<Longrightarrow> 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 \<noteq> 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 \<Rightarrow> QF option"
+primrec
+"linform (Le it1 it2) =
+ lift_bin(\<lambda>x. \<lambda>y. Le (lin_add(x,lin_neg y)) (Cst 0),linearize it1, linearize it2)"
+"linform (Eq it1 it2) =
+ lift_bin(\<lambda>x. \<lambda>y. Eq (lin_add(x,lin_neg y)) (Cst 0),linearize it1, linearize it2)"
+"linform (Divides d t) =
+ (case linearize d of
+ None \<Rightarrow> None
+ | Some ld \<Rightarrow> (case ld of
+ Cst b \<Rightarrow>
+ (if (b=0) then None
+ else
+ (case linearize t of
+ None \<Rightarrow> None
+ | Some lt \<Rightarrow> Some (Divides ld lt)))
+ | _ \<Rightarrow> None))"
+"linform T = Some T"
+"linform F = Some F"
+"linform (NOT p) = lift_un NOT (linform p)"
+"linform (And p q)= lift_bin(\<lambda>f. \<lambda>g. And f g, linform p, linform q)"
+"linform (Or p q) = lift_bin(\<lambda>f. \<lambda>g. Or f g, linform p, linform q)"
+
+(* linearity of formulae *)
+consts islinform :: "QF \<Rightarrow> bool"
+recdef islinform "measure size"
+"islinform (Le it (Cst i)) = (i=0 \<and> islinintterm it )"
+"islinform (Eq it (Cst i)) = (i=0 \<and> islinintterm it)"
+"islinform (Divides (Cst d) t) = (d \<noteq> 0 \<and> islinintterm t)"
+"islinform T = True"
+"islinform F = True"
+"islinform (NOT (Divides (Cst d) t)) = (d \<noteq> 0 \<and> islinintterm t)"
+"islinform (NOT (Eq it (Cst i))) = (i=0 \<and> islinintterm it)"
+"islinform (And p q)= ((islinform p) \<and> (islinform q))"
+"islinform (Or p q) = ((islinform p) \<and> (islinform q))"
+"islinform p = False"
+
+(* linform preserves nnf, if successful *)
+lemma linform_nnf:
+ assumes nnfp: "isnnf p"
+ shows "\<And> p'. \<lbrakk>linform p = Some p'\<rbrakk> \<Longrightarrow> 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: "\<And> lp. \<lbrakk> isnnf p ; linform p = Some lp \<rbrakk> \<Longrightarrow>
+ (qinterp ats p = qinterp ats lp)"
+proof (induct p rule: linform.induct)
+ case (Le x y)
+ show ?case
+ using "Le.prems"
+ proof-
+ have "(\<exists> lx ly. linearize x = Some lx \<and> linearize y = Some ly) \<or>
+ (linearize x = None) \<or> (linearize y = None)"by auto
+ moreover
+ {
+ assume linxy: "\<exists> lx ly. linearize x = Some lx \<and> linearize y = Some ly"
+ from linxy obtain "lx" "ly"
+ where lxly:"linearize x = Some lx \<and> 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 "(\<exists> lx ly. linearize x = Some lx \<and> linearize y = Some ly) \<or>
+ (linearize x = None) \<or> (linearize y = None)"by auto
+ moreover
+ {
+ assume linxy: "\<exists> lx ly. linearize x = Some lx \<and> linearize y = Some ly"
+ from linxy obtain "lx" "ly"
+ where lxly:"linearize x = Some lx \<and> 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 "(\<exists> lf. linform f = Some lf) \<or> (linform f = None)" by auto
+ moreover
+ {
+ assume linf: "\<exists> 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 "((\<exists> lf. linform f = Some lf ) \<and> (\<exists> lg. linform g = Some lg)) \<or>
+ (linform f = None) \<or> (linform g = None)" by auto
+ moreover
+ {
+ assume linf: "\<exists> lf. linform f = Some lf"
+ and ling: "\<exists> 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 "((\<exists> lf. linform f = Some lf ) \<and> (\<exists> lg. linform g = Some lg)) \<or>
+ (linform f = None) \<or> (linform g = None)" by auto
+ moreover
+ {
+ assume linf: "\<exists> lf. linform f = Some lf"
+ and ling: "\<exists> 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: "\<And> lp. \<lbrakk> isnnf p ; linform p = Some lp\<rbrakk> \<Longrightarrow> islinform lp"
+proof (induct p rule: linform.induct)
+ case (Le x y)
+ have "((\<exists> lx. linearize x = Some lx) \<and> (\<exists> ly. linearize y = Some ly)) \<or>
+ (linearize x = None) \<or> (linearize y = None) " by clarsimp
+ moreover
+ {
+ assume linx: "\<exists> lx. linearize x = Some lx"
+ and liny: "\<exists> 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 "((\<exists> lx. linearize x = Some lx) \<and> (\<exists> ly. linearize y = Some ly)) \<or>
+ (linearize x = None) \<or> (linearize y = None) " by clarsimp
+ moreover
+ {
+ assume linx: "\<exists> lx. linearize x = Some lx"
+ and liny: "\<exists> 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 "((\<exists> lf. linform f = Some lf ) \<and> (\<exists> lg. linform g = Some lg)) \<or>
+ (linform f = None) \<or> (linform g = None)" by auto
+ moreover
+ {
+ assume linf: "\<exists> lf. linform f = Some lf"
+ and ling: "\<exists> 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 "((\<exists> lf. linform f = Some lf ) \<and> (\<exists> lg. linform g = Some lg)) \<or>
+ (linform f = None) \<or> (linform g = None)" by auto
+ moreover
+ {
+ assume linf: "\<exists> lf. linform f = Some lf"
+ and ling: "\<exists> 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 "(\<exists> lf. linform f = Some lf) \<or> (linform f = None)" by auto
+ moreover
+ {
+ assume linf: "\<exists> 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 \<Longrightarrow> isnnf p"
+by (induct p rule: islinform.induct) auto
+
+lemma linform_isqfree: "islinform p \<Longrightarrow> isqfree p"
+using linform_isnnf nnf_isqfree by simp
+
+lemma linform_qfree: "\<And> p'. \<lbrakk> isnnf p ; linform p = Some p'\<rbrakk> \<Longrightarrow> isqfree p'"
+using linform_isqfree linform_lin
+by simp
+
+(* Definitions and lemmas about gcd and lcm *)
+constdefs lcm :: "nat \<times> nat \<Rightarrow> nat"
+ "lcm \<equiv> (\<lambda>(m,n). m*n div gcd(m,n))"
+
+constdefs ilcm :: "int \<Rightarrow> int \<Rightarrow> int"
+ "ilcm \<equiv> \<lambda>i.\<lambda>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 "\<dots> = 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 "\<dots> = n*k" using mpos npos gcd_zero by simp
+ finally show ?thesis by (simp add: lcm_def)
+qed
+
+lemma ilcm_dvd1:
+assumes anz: "a \<noteq> 0"
+ and bnz: "b \<noteq> 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 \<noteq> 0"
+ and bnz: "b \<noteq> 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) \<noteq> 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) \<le> m" by simp
+ with npos have t1:"gcd(m,n)*n \<le> m*n" by simp
+ have "gcd(m,n) \<le> gcd(m,n)*n" using npos by simp
+ with t1 have "gcd(m,n) \<le> 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 \<Rightarrow> 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 \<times> QF \<Rightarrow> bool"
+recdef divideallc "measure (\<lambda>(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) \<and> divideallc (l,q))"
+"divideallc (l,Or p q) = (divideallc (l,p) \<and> 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 \<or> i \<noteq> 0" by simp
+ moreover
+ {
+ assume "i \<noteq> 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\<noteq>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 \<or> i \<noteq> 0" by simp
+ moreover
+ {
+ assume "i \<noteq> 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\<noteq>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: "\<And> c. \<lbrakk> divideallc(c,p) ; c dvd d\<rbrakk> \<Longrightarrow> 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 \<noteq> 0" by simp
+ moreover have "formlcm g > 0" using formlcm_pos prems by simp
+ hence "formlcm g \<noteq> 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 \<noteq> 0" by simp
+ moreover have "formlcm g > 0" using formlcm_pos prems by simp
+ hence "formlcm g \<noteq> 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 \<times> QF \<Rightarrow> QF"
+recdef adjustcoeff "measure (\<lambda>(l,p). size p)"
+"adjustcoeff (l,(Le (Add (Mult (Cst c) (Var 0)) r) (Cst i))) =
+ (if c\<le>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 \<Rightarrow> 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 \<Rightarrow> bool"
+recdef isunified "measure size"
+"isunified (Le (Add (Mult (Cst i) (Var 0)) r) (Cst z)) =
+ ((abs i) = 1 \<and> (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 \<and> (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 \<and> (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 \<and> (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 \<and> (islinform(NOT(Divides (Cst d) (Add (Mult (Cst i) (Var 0)) r)))))"
+"isunified (And p q) = (isunified p \<and> isunified q)"
+"isunified (Or p q) = (isunified p \<and> isunified q)"
+"isunified p = islinform p"
+
+lemma unified_islinform: "isunified p \<Longrightarrow> islinform p"
+by (induct p rule: isunified.induct) auto
+
+lemma adjustcoeff_lenpos:
+ "0 < n \<Longrightarrow> 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 \<Longrightarrow> 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) \<le> j \<Longrightarrow> 0 \<le> k \<Longrightarrow> k * i \<le> 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) \<le> j) = (k*i \<le> k*j)" (is "?P = ?Q")
+proof
+ assume P: ?P
+ from kpos have kge0: "0 \<le> k" by simp
+ show ?Q
+ by (rule zmult_zle_mono[OF P kge0])
+next
+ assume ?Q
+ then have "k*i - k*j \<le> 0" by simp
+ then have le1: "k*(i-j) \<le> k*0"
+ by (simp add: zdiff_zmult_distrib2)
+ have "i -j \<le> 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 \<le> 0) = (l*x + ((l div i)*r) \<le> 0)"
+proof-
+ from lpos ipos have ilel: "i\<le>l" by (simp add: zdvd_imp_le [OF dvd lpos])
+ from ipos have inz: "i \<noteq> 0" by simp
+ have "i div i\<le> 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 "\<exists>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 \<le> 0) = (l div i * (i * x + r) \<le> 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) \<le> l div i * 0) = ((l div i * i) * x + ((l div i)*r) \<le> 0)"
+ by (simp add: mult_ac)
+ also have "((l div i * i) * x + ((l div i)*r) \<le> 0) = (l*x + ((l div i)*r) \<le> 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 \<le> 0) = ((-l)*x + ((-(l div i))*r) \<le> 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\<le>l" by (simp add: zdvd_imp_le [OF midvdl lpos])
+ from ineg have inz: "i \<noteq> 0" by simp
+ have "l div i\<le> -i div i"
+ by (simp add: zdiv_mono1_neg[OF milel ineg])
+ then have "l div i \<le> -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 "\<exists>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 \<le> 0) = (- (l div i) * (i * x + r) \<le> - (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) \<le> - (l div i) * 0) = (-((l div i) * i) * x \<le> (l div i)*r)"
+ by (simp add: mult_ac)
+ also have " (-((l div i) * i) * x \<le> (l div i)*r) = (- (l*x) \<le> (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\<noteq>0"
+ and dvd: "a dvd b"
+ shows "(b div a)*a = b"
+proof-
+ from anz have "0 < a \<or> a < 0" by arith
+ moreover
+ {
+ assume apos: "0 < a"
+ from bpos apos have aleb: "a\<le>b" by (simp add: zdvd_imp_le [OF dvd bpos])
+ have "a div a\<le> 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 "\<exists>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\<le>b" by (simp add: zdvd_imp_le [OF midvdb bpos])
+ from aneg have anz: "a \<noteq> 0" by simp
+ have "b div a\<le> -a div a"
+ by (simp add: zdiv_mono1_neg[OF maleb aneg])
+ then have "b div a \<le> -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 "\<exists>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 \<noteq> 0"
+ and dvd: "i dvd l"
+ shows "(i*x + r = 0) = (l*x + ((l div i)*r) = 0)"
+proof-
+ thm dvd_div_pos[OF lpos inz dvd]
+ have ldvdii: "(l div i)*i = l" by (rule dvd_div_pos[OF lpos inz dvd])
+ have ldivinz: "l div i \<noteq> 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 "\<dots> = (((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\<noteq>0" by simp
+ then
+ have "(n=0 \<and> i < 0) \<or> (n=0 \<and> i > 0) \<or> n\<noteq>0" by arith
+ moreover
+ {
+ assume "n\<noteq>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' \<le> 0) = (l*a+ ((l div i)*i') \<le> 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' \<le> 0) = (-l*a + (-(l div i) * i') \<le> 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\<noteq>0" by simp
+ then
+ have "(n=0 \<and> i < 0) \<or> (n=0 \<and> i > 0) \<or> n\<noteq>0" by arith
+ moreover
+ {
+ assume nnz: "n\<noteq>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) \<le> 0) =
+ (l * a + l div i * (i' * (a # ats) ! n' + I_intterm (a # ats) r) \<le> 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) \<le> 0) =
+ (- l * a + - (l div i) * (i' * (a # ats) ! n' + I_intterm (a # ats) r) \<le> 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\<noteq>0" by simp
+ then
+ have "n=0 \<or> n\<noteq>0" by arith
+ moreover
+ {
+ assume "n\<noteq>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\<noteq>0" by simp
+ then
+ have "n=0 \<or> n\<noteq>0" by arith
+ moreover
+ {
+ assume nnz: "n\<noteq>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 \<noteq> 0" by auto
+ from prems nz have idvdl: "i dvd l" by simp
+ thm adjustcoeff_eq_corr[OF lpos inz idvdl]
+ 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 \<or> (\<exists>m. (n = Suc m))" by arith
+ moreover
+ {
+ assume "\<exists>m. n = Suc m"
+ then have ?case using prems by auto
+ }
+ moreover
+ {
+ assume nz: "n=0"
+ from prems have inz: "i\<noteq>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 \<noteq> 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\<noteq>0" by simp
+
+ have "n=0 \<or> (\<exists>m. (n = Suc m))" by arith
+ moreover
+ {
+ assume "\<exists>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 \<noteq> 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 \<or> (\<exists>m. (n = Suc m))" by arith
+ moreover
+ {
+ assume "\<exists>m. n = Suc m"
+ then have ?case using prems by auto
+ }
+ moreover
+ {
+ assume nz: "n=0"
+ from prems have inz: "i\<noteq>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 \<noteq> 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\<noteq>0" by simp
+
+ have "n=0 \<or> (\<exists>m. (n = Suc m))" by arith
+ moreover
+ {
+ assume "\<exists>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 \<noteq> 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\<noteq>0" by simp
+ then
+ have "n=0 \<or> n\<noteq>0" by arith
+ moreover
+ {
+ assume "n\<noteq>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\<noteq>0" by simp
+ then
+ have "n=0 \<or> n\<noteq>0" by arith
+ moreover
+ {
+ assume nnz: "n\<noteq>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 \<noteq> 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 "(\<exists>x. qinterp (x * formlcm p # ats) (adjustcoeff (formlcm p, p))) =
+ (\<exists>x. formlcm p dvd x \<and>
+ qinterp (x # ats) (adjustcoeff (formlcm p, p)))"
+ (is "(\<exists>x. ?P(x* (formlcm p))) = (\<exists>x. formlcm p dvd x \<and> ?P x)")
+ proof-
+ have "(\<exists>x. ?P(x* (formlcm p))) = (\<exists>x. ?P((formlcm p)*x))"
+ by (simp add: mult_commute)
+ also have "(\<exists>x. ?P((formlcm p)*x)) = (\<exists>x. (formlcm p dvd x) \<and> ?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 \<or> 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 \<le> l" by (rule zdvd_imp_le[OF cdvdl lp])
+ have "c div c \<le> 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 \<noteq> 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 \<le> l" by (rule zdvd_imp_le[OF mcdvdl lp])
+ have "l div c = (-l div -c)" by simp
+ also have "\<dots> = - (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 \<le> 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 \<or> 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 \<le> l" by (rule zdvd_imp_le[OF cdvdl lp])
+ have "c div c \<le> 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 \<noteq> 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 \<le> l" by (rule zdvd_imp_le[OF mcdvdl lp])
+ have "l div c = (-l div -c)" by simp
+ also have "\<dots> = - (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 \<le> 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\<Longrightarrow> isqfree p"
+using unified_islinform linform_isqfree
+by auto
+
+(* Plus/Minus infinity , B and A set definitions *)
+
+consts minusinf :: "QF \<Rightarrow> QF"
+ plusinf :: "QF \<Rightarrow> QF"
+ aset :: "QF \<Rightarrow> intterm list"
+ bset :: "QF \<Rightarrow> 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 \<delta> = lcm d , where d | x +t occurs in p *)
+consts divlcm :: "QF \<Rightarrow> 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 \<delta> *)
+consts alldivide :: "int \<times> QF \<Rightarrow> 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) \<and> alldivide (d,q))"
+"alldivide (d,(Or p q)) = ((alldivide (d,p)) \<and> (alldivide (d,q)))"
+"alldivide (d,p) = True"
+
+(* alldivide is monotone *)
+lemma alldivide_mono: "\<And> d'. \<lbrakk> alldivide (d,p) ; d dvd d'\<rbrakk> \<Longrightarrow> 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 \<or> d' \<ge> 0" by arith
+ moreover
+ {
+ assume dn': "d' < 0"
+ then have "abs d' = - d'" by simp
+ then
+ have ?thesis by (simp)
+ }
+ moreover
+ {
+ assume dp': "d' \<ge> 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
+
+(* \<delta> > 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 \<Longrightarrow> x \<noteq> 0" by auto
+(* divlcm is correct *)
+lemma divlcm_corr:
+ assumes
+ linp: "islinform p"
+ shows "alldivide (divlcm p,p)"
+thm nz_le[OF divlcm_pos[OF linp]]
+ 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 \<dots> *)
+lemma minusinf_eq:
+ assumes unifp: "isunified p"
+ shows "\<exists> z. \<forall> x. x < z \<longrightarrow> (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 \<or> 0 \<le> 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 \<longrightarrow> \<not> - x + I_intterm (x # ats) r \<le> 0"
+ by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"])
+ qed
+ qed
+ }
+ moreover
+ {
+ assume cpos: "0 \<le> 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 \<longrightarrow> x + I_intterm (x # ats) r \<le> 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 \<or> 0 \<le> 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 \<longrightarrow> \<not> - 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 \<le> 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 \<longrightarrow> x + I_intterm (x # ats) r \<noteq> 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 \<or> 0 \<le> 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 \<longrightarrow> \<not> - 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 \<le> 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 \<longrightarrow> x + I_intterm (x # ats) r \<noteq> 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:"\<forall>x<zf. qinterp (x # ats) f = qinterp (x # ats) (minusinf f)" by auto
+ from prems obtain "zg" where
+ zg:"\<forall>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:"\<forall>x<zf. qinterp (x # ats) f = qinterp (x # ats) (minusinf f)" by auto
+ from prems obtain "zg" where
+ zg:"\<forall>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) \<and> i \<noteq> 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 \<or> 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 \<and> i\<noteq>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 \<and> i\<noteq>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 \<or> 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 \<and> i\<noteq>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 "\<forall> x k. (qinterp (x#ats) (minusinf p) = qinterp ((x - k*d)#ats) (minusinf p))"
+ (is "\<forall> 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: "\<exists> j \<in> {1 ..d}. qinterp (j#ats) (minusinf p)" (is "\<exists> j \<in> {1 .. d}. ?P1 j")
+ shows "\<exists> x. qinterp (x#ats) p" (is "\<exists> x. ?P x")
+proof-
+ from exminf obtain "j" where P1j: "?P1 j" by blast
+ have ePeqP1: "\<exists>z. \<forall> x. x < z \<longrightarrow> (?P x = ?P1 x)"
+ by (rule minusinf_eq[OF unifp])
+ then obtain "z" where P1eqP : "\<forall> x. x < z \<longrightarrow> (?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 : "\<forall> x k. ?P1 x = ?P1 (x - k*(?d))"
+ by (rule minusinf_repeats2[OF alldvd unifp])
+ let ?w = "j - (abs (j-z) +1)* ?d"
+ show "\<exists> 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 "\<dots> = ?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 "(\<exists> x. qinterp (x#ats) (minusinf p)) =
+ (\<exists> j \<in> { 1.. divlcm p}. qinterp (j#ats) (minusinf p))"
+ (is "(\<exists> x. ?P x) = (\<exists> j \<in> { 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 "\<exists> j\<in> {1 .. ?d}. ?P j"
+ then show "\<exists> x. ?P x" using dpos by auto
+ next
+ assume "\<exists> x. ?P x"
+ then obtain "x" where P: "?P x" by blast
+ have modd: "\<forall>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 "\<exists> j\<in> {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 \<in> {1 .. ?d}" using dpos
+ by (simp add:atLeastAtMost_iff)
+ ultimately show "\<exists> j\<in> {1 .. ?d}. ?P j" ..
+ next
+ assume not0: "x mod ?d \<noteq> 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 \<le> 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 "\<exists> j\<in> {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 "\<forall> b \<in> 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) \<and> \<not>(\<exists>j\<in> {1 .. d}. \<exists> b \<in> set (bset p). (qinterp (((I_intterm (a#ats) b) + j)#ats) q)) \<and>(qinterp (x#ats) p)"
+ (is "?Q x \<and> \<not>(\<exists> j\<in> {1.. d}. \<exists> b\<in> ?B. ?Q (?I a b + j)) \<and> ?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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 \<or> 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 \<or> 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 \<le> 0"
+ then show "- x + d + ?I x r \<le> 0" .
+ next
+ assume np: "\<not> - x + d + ?I x r \<le> 0"
+ then have ltd:"x - ?I x r \<le> d - 1" by simp
+ from prems have "-x + ?I x r \<le> 0" by simp
+ then have ge0: "x - ?I x r \<ge> 0"
+ by simp
+ from ltd ge0 have "x - ?I x r = 0 \<or> (1 \<le> x - ?I x r \<and> x - ?I x r \<le> 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 "\<forall>j\<in>{1..d}. \<not> ?Q (?I a r + -1 + j)"
+ using linr by (auto simp add: lin_add_corr)
+ moreover from dpos have "1 \<in> {1..d}" by simp
+ ultimately have " \<not> ?Q (?I a r + -1 + 1)" by blast
+ with dpos linr have "\<not> ?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 \<le> 0" by simp
+ }
+ moreover
+ {
+ assume gt0: "1 \<le> x - ?I x r \<and> x - ?I x r \<le> d - 1"
+ then have "\<exists> j\<in> {1 .. d - 1}. x - ?I x r = j" by simp
+ then have "\<exists> j\<in> {1 .. d}. x - ?I x r = j" by auto
+ then obtain "j" where con: "1\<le>j \<and> j \<le> d \<and> 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: "\<exists> j\<in> {1 .. d}. ?Q (?I x r + j)" by auto
+ from prems have "\<forall>j\<in>{1..d}. \<not> ?Q (?I a r + j)" by auto
+ then have "\<not> (\<exists> j\<in>{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 \<le> 0" by simp
+
+ }
+ ultimately show "- x + d + ?I x r \<le> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 \<or> 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 \<or> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 \<or> 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 \<or> i = -1" by arith
+ from nz prems have advdixr: "\<not> (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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 \<or> 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 \<or> 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 "\<not> (?Q ((?I a (lin_add(lin_neg r, Cst -1))) + 1))"
+ by auto
+ hence "\<not> (?Q ((- ?I a r - 1) + 1))"
+ using lin_add_corr lin_neg_corr linr lin_neg_lin
+ by simp
+ hence "\<not> (?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 "\<not> (?Q ((?I a (lin_add(r, Cst -1))) + 1))"
+ by auto
+ hence "\<not> (?Q (?I a r))"
+ using lin_add_corr lin_neg_corr linr lin_neg_lin
+ by simp
+ hence "\<not> (?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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 \<or> 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 \<or> 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 "\<not> (?Q ((?I a (lin_neg r)) + d))"
+ by auto
+ hence "\<not> (?Q (- ?I a r + d))"
+ using lin_neg_corr linr by simp
+ hence "\<not> (?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 "\<not> (?Q ((?I a r) + d))"
+ by auto
+ hence "\<not> (?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 "\<forall> x. \<not>(\<exists>j\<in> {1 .. (divlcm p)}. \<exists> b \<in> set (bset p).
+ (qinterp (((I_intterm (a#ats) b) + j)#ats) p))
+ \<longrightarrow> (qinterp (x#ats) p) \<longrightarrow> (qinterp ((x - (divlcm p))#ats) p)"
+ (is "\<forall> x. \<not>(\<exists> j\<in> {1 .. ?d}. \<exists> b\<in> ?B. ?P (?I a b + j)) \<longrightarrow> ?P x \<longrightarrow> ?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 "\<not>(\<exists> j\<in> {1 .. ?d}. \<exists> b\<in> ?B. ?P (?I a b + j)) \<longrightarrow> ?P x \<longrightarrow> ?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 "(\<exists> x. qinterp (x#ats) p) =
+ ((\<exists> j \<in> {1 .. (divlcm p)}. qinterp (j#ats) (minusinf p)) \<or>
+ (\<exists> j \<in> {1 .. (divlcm p)}. \<exists> b \<in> set (bset p).
+ qinterp (((I_intterm (a#ats) b) + j)#ats) p))"
+ (is "(\<exists> x. ?P x) = ((\<exists> j\<in> {1 .. ?d}. ?MP j) \<or> (\<exists> j \<in> ?D. \<exists> b\<in> ?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: "(\<exists>j \<in> ?D. ?MP j) \<longrightarrow> (\<exists>x. ?P x)"
+ by (simp add: minusinf_lemma[OF unifp, where d="?d" and ats="ats"])
+ have ePimpeP: "(\<exists> j \<in> ?D. \<exists> b\<in> ?B. ?P (?I a b + j)) \<longrightarrow> (\<exists> x. ?P x)"
+ by blast
+ have bst_rep: "\<forall> x. \<not> (\<exists> j \<in> ?D. \<exists> b \<in> ?B. ?P (?I a b + j)) \<longrightarrow> ?P x \<longrightarrow> ?P (x - ?d)"
+ by (rule bset_disj_repeat2[OF unifp])
+ have MPrep: "\<forall> x k. ?MP x = ?MP (x- k*?d)"
+ by (rule minusinf_repeats2[OF alldvd unifp])
+ have MPeqP: "\<exists> z. \<forall> x < z. ?P x = ?MP x"
+ by (rule minusinf_eq[OF unifp])
+ let ?B'= "{?I a b| b. b\<in> ?B}"
+ from bst_rep have bst_rep2: "\<forall>x. \<not> (\<exists>j\<in>?D. \<exists>b\<in> ?B'. ?P (b+j)) \<longrightarrow> ?P x \<longrightarrow> ?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 \<Rightarrow> 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 \<or> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> i n r. t = Add (Mult (Cst i) (Var n) ) r) \<or> (\<exists> i. t = Cst i)"
+ by (induct t rule: islinintterm.induct) auto
+ moreover{ assume "\<exists> i. t = Cst i" then have ?case using prems by auto }
+ moreover
+ { assume "\<exists> 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 "(\<exists> x. (qinterp (x#ats) p)) = (\<exists> y. (qinterp (y#ats) (mirror p)))"
+ (is "(\<exists> x. ?P x) = (\<exists> y. ?MP y)")
+proof
+ assume "\<exists> 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 "\<exists> y. ?MP y" by blast
+next
+ assume "\<exists> 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 "\<exists> 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 "(\<exists> x. qinterp (x#ats) p) =
+ ((\<exists> j \<in> {1 .. (divlcm p)}. qinterp (-j#ats) (plusinf p)) \<or>
+ (\<exists> j \<in> {1 .. (divlcm p)}. \<exists> b \<in> set (aset p).
+ qinterp (((I_intterm (a#ats) b) - j)#ats) p))"
+ (is "(\<exists> x. ?P x) = ((\<exists> j\<in> {1 .. ?d}. ?PP (-j)) \<or> (\<exists> j \<in> ?D. \<exists> b\<in> ?A. ?P (?I a b - j)))")
+proof-
+ have unifmp: "isunified (mirror p)" by (rule mirror_unified[OF unifp])
+ have th1:
+ "(\<exists> j\<in> {1 .. ?d}. ?PP (-j)) = (\<exists> j\<in> {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 "(\<exists> j \<in> ?D. \<exists> b\<in> ?A. ?P (?I a b - j)) =
+ (\<exists> j\<in> ?D. \<exists> b \<in> set (map lin_neg (bset (mirror p))). ?P (?I a b - j))"
+ by (simp only: aset_eq_bset_mirror[OF unifp])
+ also have "\<dots> = (\<exists> j\<in> ?D. \<exists> b \<in> set (bset (mirror p)). ?P (?I a (lin_neg b) - j))"
+ by simp
+ also have "\<dots> = (\<exists> j\<in> ?D. \<exists> b \<in> set (bset (mirror p)). ?P (-(?I a b + j)))"
+ proof
+ assume "\<exists>j\<in>{1..divlcm p}.
+ \<exists>b\<in>set (bset (mirror p)). qinterp ((I_intterm (a # ats) (lin_neg b) - j) # ats) p"
+ then
+ obtain "j" and "b" where
+ pbmj: "j\<in> ?D \<and> b\<in> set (bset (mirror p)) \<and> ?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 "\<exists> j\<in> ?D. \<exists> b \<in> set (bset (mirror p)). ?P (-(?I a b + j))"
+ using pbmj
+ by auto
+ next
+ assume "\<exists> j\<in> ?D. \<exists> b \<in> set (bset (mirror p)). ?P (-(?I a b + j))"
+ then obtain "j" and "b" where
+ pbmj: "j\<in> ?D \<and> b\<in> set (bset (mirror p)) \<and> ?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 "\<exists> j\<in> ?D. \<exists> b \<in> set (bset (mirror p)). ?P (?I a (lin_neg b) - j)"
+ using pbmj by auto
+ qed
+ finally
+ have bth: "(\<exists> j\<in> ?D. \<exists> b\<in> ?A. ?P (?I a b - j)) =
+ (\<exists>j\<in> ?D. \<exists> b\<in>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 "(\<exists> x. ?P x) = (\<exists> x. qinterp (x#ats) (mirror p))"
+ by (simp add: mirror_ex[OF unifp])
+ also have "\<dots> = ((\<exists>j\<in>{1..divlcm (mirror p)}. qinterp (j # ats) (minusinf (mirror p))) \<or>
+ (\<exists>j\<in>{1..divlcm (mirror p)}.
+ \<exists>b\<in>set (bset (mirror p)). qinterp ((I_intterm (a # ats) b + j) # ats) (mirror p)))"
+ (is "(\<exists> x. ?MP x) = ((\<exists> j\<in> ?DM. ?MPM j) \<or> (\<exists> j \<in> ?DM. \<exists> b\<in> ?BM. ?MP (?I a b + j)))")
+ by (rule cooper_mi_eq[OF unifmp])
+ also
+ have "\<dots> = ((\<exists> j\<in> ?D. ?PP (-j)) \<or> (\<exists> j \<in> ?D. \<exists> b\<in> ?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 \<Rightarrow> intterm \<Rightarrow> 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 \<Rightarrow> QF \<Rightarrow> 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 \<Rightarrow> bool"
+primrec
+"novar0I (Cst i) = True"
+"novar0I (Var n) = (n > 0)"
+"novar0I (Neg a) = (novar0I a)"
+"novar0I (Add a b) = (novar0I a \<and> novar0I b)"
+"novar0I (Sub a b) = (novar0I a \<and> novar0I b)"
+"novar0I (Mult a b) = (novar0I a \<and> novar0I b)"
+
+consts novar0:: "QF \<Rightarrow> bool"
+recdef novar0 "measure size"
+"novar0 (Lt a b) = (novar0I a \<and> novar0I b)"
+"novar0 (Gt a b) = (novar0I a \<and> novar0I b)"
+"novar0 (Le a b) = (novar0I a \<and> novar0I b)"
+"novar0 (Ge a b) = (novar0I a \<and> novar0I b)"
+"novar0 (Eq a b) = (novar0I a \<and> novar0I b)"
+"novar0 (Divides a b) = (novar0I a \<and> novar0I b)"
+"novar0 T = True"
+"novar0 F = True"
+"novar0 (NOT p) = novar0 p"
+"novar0 (And p q) = (novar0 p \<and> novar0 q)"
+"novar0 (Or p q) = (novar0 p \<and> novar0 q)"
+"novar0 (Imp p q) = (novar0 p \<and> novar0 q)"
+"novar0 (Equ p q) = (novar0 p \<and> 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 "\<exists> 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 "\<exists> na > 0. islintn(na, a)" by (rule lin_novar0[OF lina nov0a])
+ then obtain "na" where na: "na > 0 \<and> islintn(na,a)" by blast
+ have "\<exists> nb > 0. islintn(nb, b)" by (rule lin_novar0[OF linb nov0b])
+ then obtain "nb" where nb: "nb > 0 \<and> 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 \<le> 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 \<noteq> 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 \<Rightarrow> 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 \<Rightarrow> 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 \<Longrightarrow> isqfree (decrvars p)"
+by (induct p rule: isqfree.induct, auto)
+
+lemma novar0_qfree: "novar0 p \<Longrightarrow> 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 "\<forall> b\<in> 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 \<or> 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 \<or> 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 \<or> 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 "\<And> t'. linearize t = Some t' \<Longrightarrow> novar0I t'"
+using nov0t
+proof(induct t rule: novar0I.induct)
+ case (Neg a)
+ let ?la = "linearize a"
+ from prems have "\<exists> 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 "\<exists> 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 "\<exists> 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 "\<exists> 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 "\<exists> 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 "\<exists> 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 "\<exists> 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 \<Rightarrow> QF"
+recdef psimpl "measure size"
+"psimpl (Le l r) =
+ (case (linearize (Sub l r)) of
+ None \<Rightarrow> Le l r
+ | Some x \<Rightarrow> (case x of
+ Cst i \<Rightarrow> (if i \<le> 0 then T else F)
+ | _ \<Rightarrow> (Le x (Cst 0))))"
+"psimpl (Eq l r) =
+ (case (linearize (Sub l r)) of
+ None \<Rightarrow> Eq l r
+ | Some x \<Rightarrow> (case x of
+ Cst i \<Rightarrow> (if i = 0 then T else F)
+ | _ \<Rightarrow> (Eq x (Cst 0))))"
+
+"psimpl (Divides (Cst d) t) =
+ (case (linearize t) of
+ None \<Rightarrow> (Divides (Cst d) t)
+ | Some c \<Rightarrow> (case c of
+ Cst i \<Rightarrow> (if d dvd i then T else F)
+ | _ \<Rightarrow> (Divides (Cst d) c)))"
+
+"psimpl (And p q) =
+ (let p'= psimpl p
+ in (case p' of
+ F \<Rightarrow> F
+ |T \<Rightarrow> psimpl q
+ | _ \<Rightarrow> let q' = psimpl q
+ in (case q' of
+ F \<Rightarrow> F
+ | T \<Rightarrow> p'
+ | _ \<Rightarrow> (And p' q'))))"
+
+"psimpl (Or p q) =
+ (let p'= psimpl p
+ in (case p' of
+ T \<Rightarrow> T
+ | F \<Rightarrow> psimpl q
+ | _ \<Rightarrow> let q' = psimpl q
+ in (case q' of
+ T \<Rightarrow> T
+ | F \<Rightarrow> p'
+ | _ \<Rightarrow> (Or p' q'))))"
+
+"psimpl (Imp p q) =
+ (let p'= psimpl p
+ in (case p' of
+ F \<Rightarrow> T
+ |T \<Rightarrow> psimpl q
+ | NOT p1 \<Rightarrow> let q' = psimpl q
+ in (case q' of
+ F \<Rightarrow> p1
+ | T \<Rightarrow> T
+ | _ \<Rightarrow> (Or p1 q'))
+ | _ \<Rightarrow> let q' = psimpl q
+ in (case q' of
+ F \<Rightarrow> NOT p'
+ | T \<Rightarrow> T
+ | _ \<Rightarrow> (Imp p' q'))))"
+
+"psimpl (Equ p q) =
+ (let p'= psimpl p ; q' = psimpl q
+ in (case p' of
+ T \<Rightarrow> q'
+ | F \<Rightarrow> (case q' of
+ T \<Rightarrow> F
+ | F \<Rightarrow> T
+ | NOT q1 \<Rightarrow> q1
+ | _ \<Rightarrow> NOT q')
+ | NOT p1 \<Rightarrow> (case q' of
+ T \<Rightarrow> p'
+ | F \<Rightarrow> p1
+ | NOT q1 \<Rightarrow> (Equ p1 q1)
+ | _ \<Rightarrow> (Equ p' q'))
+ | _ \<Rightarrow> (case q' of
+ T \<Rightarrow> p'
+ | F \<Rightarrow> NOT p'
+ | _ \<Rightarrow> (Equ p' q'))))"
+
+"psimpl (NOT p) =
+ (let p' = psimpl p
+ in ( case p' of
+ F \<Rightarrow> T
+ | T \<Rightarrow> F
+ | NOT p1 \<Rightarrow> p1
+ | _ \<Rightarrow> (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 "(\<exists> lx. linearize (Sub l r) = Some lx) \<or> (linearize (Sub l r) = None)" by auto
+ moreover
+ {
+ assume lin: "\<exists> 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 "(\<exists> i. lx = Cst i) \<or> (\<not> (\<exists> i. lx = Cst i))" by blast
+ moreover
+ {
+ assume lxcst: "\<exists> i. lx = Cst i"
+ from lxcst obtain "i" where lxi: "lx = Cst i" by blast
+ with feq have "qinterp ats (Le l r) = (i \<le> 0)" by simp
+ then have ?case using prems by (simp add: measure_def inv_image_def)
+ }
+ moreover
+ {
+ assume "(\<not> (\<exists> i. lx = Cst i))"
+ then have "(case lx of
+ Cst i \<Rightarrow> (if i \<le> 0 then T else F)
+ | _ \<Rightarrow> (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 "(\<exists> lx. linearize (Sub l r) = Some lx) \<or> (linearize (Sub l r) = None)" by auto
+ moreover
+ {
+ assume lin: "\<exists> 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 "(\<exists> i. lx = Cst i) \<or> (\<not> (\<exists> i. lx = Cst i))" by blast
+ moreover
+ {
+ assume lxcst: "\<exists> 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 "(\<not> (\<exists> i. lx = Cst i))"
+ then have "(case lx of
+ Cst i \<Rightarrow> (if i = 0 then T else F)
+ | _ \<Rightarrow> (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 "(\<exists> lt. linearize t = Some lt) \<or> (linearize t = None)" by auto
+ moreover
+ {
+ assume lin: "\<exists> 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 \<or> (\<exists> 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 "\<exists> 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 \<or> (\<exists> 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 "\<exists> 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 \<or> (\<exists> x. ?lt = Some x)" by auto
+ moreover
+ { assume "?lt = None" then have ?case using prems by simp }
+ moreover {
+ assume "\<exists>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 \<times> QF) \<Rightarrow> QF"
+recdef explode_disj "measure (\<lambda>(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 \<Rightarrow> T
+ | F \<Rightarrow> explode_disj (is,p)
+ | _ \<Rightarrow> (let r = explode_disj (is,p)
+ in (case r of
+ T \<Rightarrow> T
+ | F \<Rightarrow> pi
+ | _ \<Rightarrow> 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) \<or> (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 \<or> ?pi = F"
+ then show ?thesis using pi by (case_tac "?pi::QF", auto)
+
+ next
+ assume notTF: "\<not> (?pi = T \<or> ?pi = F)"
+ let ?dp = "explode_disj(is,p)"
+ have dp_cases: "explode_disj(i#is,p) =
+ (case (explode_disj(is,p)) of
+ T \<Rightarrow> T
+ | F \<Rightarrow> psimpl (subst_p i p)
+ | _ \<Rightarrow> 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 \<or> ?dp = F"
+ then show ?thesis
+ using pi dp_cases
+ by (cases "?dp") auto
+ next
+ assume "\<not> (?dp = T \<or> ?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 "(\<exists> x \<in> set xs. qinterp (a#ats) (subst_p x p)) =
+ (qinterp (a#ats) (explode_disj(xs,p)))" (is "(\<exists> x \<in> set xs. ?P x) = (?DP a xs )")
+ using qfp
+ proof (induct xs)
+ case Nil show ?case by simp
+ next
+ case (Cons y ys)
+ have "(\<exists> x \<in> set (y#ys). ?P x) = (?P y \<or> (\<exists> x\<in> set ys. ?P x))"
+ by auto
+ also have "\<dots> = (?P y \<or> ?DP a ys)" using "Cons.hyps" qfp by auto
+ also have "\<dots> = ?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: "\<forall>x \<in> 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 \<or> ?qs = F \<or> (?qs \<noteq> T \<or> ?qs \<noteq> 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 \<noteq> T \<and> ?qs \<noteq> 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 \<or> ?r = F \<or> (?r \<noteq> T \<or> ?r \<noteq> 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 \<noteq> T \<and> ?r \<noteq> 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 \<Rightarrow> T
+ | F \<Rightarrow> g
+ | _ \<Rightarrow> (case g of
+ T \<Rightarrow> T
+ | F \<Rightarrow> f
+ | _ \<Rightarrow> Or f g)) = (qinterp (a#ats) f \<or> qinterp (a#ats) g)"
+proof-
+ let ?result = "
+ (case f of
+ T \<Rightarrow> T
+ | F \<Rightarrow> g
+ | _ \<Rightarrow> (case g of
+ T \<Rightarrow> T
+ | F \<Rightarrow> f
+ | _ \<Rightarrow> Or f g))"
+ have "f = T \<or> f = F \<or> (f \<noteq> T \<and> f\<noteq> 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\<noteq>T"
+ and fnF: "f\<noteq>F"
+ have "g = T \<or> g = F \<or> (g \<noteq> T \<and> g\<noteq> 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\<noteq>T"
+ and gnF: "g\<noteq>F"
+ then have "?result = (case g of
+ T \<Rightarrow> T
+ | F \<Rightarrow> f
+ | _ \<Rightarrow> Or f g)"
+ using fnT fnF
+ by (cases f, auto)
+ also have "\<dots> = 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 \<noteq> T \<and> f \<noteq> F"
+ and gnTF: "g \<noteq> T \<and> g \<noteq> F"
+ and f0: "novar0 f"
+ and g0: "novar0 g"
+ shows "novar0
+ (case f of T \<Rightarrow> T | F \<Rightarrow> g
+ | _ \<Rightarrow> (case g of T \<Rightarrow> T | F \<Rightarrow> f | _ \<Rightarrow> 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 \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ "list_insert x xs \<equiv> (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 \<times> 'a list) \<Rightarrow> 'a list"
+
+recdef list_union "measure (\<lambda>(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 \<Rightarrow> '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 \<times> int \<Rightarrow> int list"
+recdef iupto "measure (\<lambda> (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 \<times> intterm list \<Rightarrow> intterm list"
+recdef all_sums "measure (\<lambda>(i,is). length is)"
+"all_sums (j,[]) = []"
+"all_sums (j,i#is) = (map (\<lambda>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: "\<forall> x\<in> set xs. novar0I x"
+ and linxs: "\<forall> x\<in> set xs. islinintterm x "
+ shows "\<forall> x\<in> 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 (\<lambda>x. lin_add (a,(Cst x))) (iupto(1,j))"
+ have nov0ys: "\<forall> y\<in> set ?ys. novar0I y"
+ proof-
+ have linx: "\<forall> x \<in> set (iupto(1,j)). islinintterm (Cst x)" by simp
+ have nov0x: "\<forall> x \<in> set (iupto(1,j)). novar0I (Cst x)" by simp
+ with nov0a lina linx have "\<forall> x\<in> 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: "\<forall>u\<in>set as. islinintterm u" by auto
+ from "2.prems" have nov0as: "\<forall>u\<in>set as. novar0I u" by auto
+ from "2.hyps" linas nov0as have nov0alls: "\<forall>u\<in>set (all_sums (j, as)). novar0I u" by simp
+ from nov0alls nov0ys have
+ cs: "(\<forall> u\<in> 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 = (\<forall> x\<in> 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:
+ "(\<exists> j\<in> {1..d}. \<exists> b\<in> (set xs). P (lin_add(b,Cst j))) =
+ (\<exists> x\<in> 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 "(\<exists> x\<in> set (map (\<lambda>x. lin_add (y,(Cst x))) (iupto(1,a))) . P x) =
+ (\<exists> j\<in> set (iupto(1,a)). P (lin_add(y,Cst j)))"
+ by auto
+ also have "\<dots> = (\<exists> j\<in> {1..a}. P (lin_add(y,Cst j)))"
+ by (simp only : iupto_set)
+ finally
+ have dsj1:"(\<exists>j\<in>{1..a}. P (lin_add (y, Cst j))) = (\<exists>x\<in>set (map (\<lambda>x. lin_add (y, Cst x)) (iupto (1, a))). P x)" by simp
+
+ from prems have "(\<exists> j\<in> {1..a}. \<exists> b\<in> (set (y#ys)). P (lin_add(b,Cst j))) =
+ ((\<exists> j\<in> {1..a}. P (lin_add(y,Cst j))) \<or> (\<exists> j\<in> {1..a}. \<exists> b \<in> set ys. P (lin_add(b,Cst j))))" by auto
+ also
+ have " \<dots> = ((\<exists> j\<in> {1..a}. P (lin_add(y,Cst j))) \<or> (\<exists> x\<in> set (all_sums(a, ys)). P x))" using prems by simp
+ also have "\<dots> = ((\<exists>x\<in>set (map (\<lambda>x. lin_add (y, Cst x)) (iupto (1, a))). P x) \<or> (\<exists>x\<in>set (all_sums (a, ys)). P x))" using dsj1 by simp
+ also have "\<dots> = (\<exists> x\<in> (set (map (\<lambda>x. lin_add (y, Cst x)) (iupto (1, a)))) \<union> (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 \<times> intterm list) \<Rightarrow> 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 \<Rightarrow> T
+ | F \<Rightarrow> explode_disj (all_sums (d,B),q)
+ | _ \<Rightarrow> (let dj2 = explode_disj (all_sums (d,B),q)
+ in ( case dj2 of
+ T \<Rightarrow> T
+ | F \<Rightarrow> dj1
+ | _ \<Rightarrow> 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 "\<forall> x\<in> 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: "\<forall>b\<in>set B. islinintterm b"
+ using bset_lin[OF unifp] bst
+ by simp
+
+ have bstnov0: "\<forall>b\<in>set B. novar0I b"
+ using bst bset_novar0[OF unifp] by simp
+ have allsnov0: "\<forall>x\<in>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 \<or> ?dj1 = F \<or> (?dj1 \<noteq> T \<and> ?dj1 \<noteq> 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 \<noteq> T \<and> ?dj1 \<noteq> F"
+
+ have "?dj2 = T \<or> ?dj2 = F \<or> (?dj2 \<noteq> T \<and> ?dj2 \<noteq> 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 \<noteq> T \<and> ?dj2 \<noteq> F"
+ let ?res = "\<lambda>f. \<lambda>g. (case f of T \<Rightarrow> T | F \<Rightarrow> g
+ | _ \<Rightarrow> (case g of T \<Rightarrow> T| F \<Rightarrow> f| _ \<Rightarrow> 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 "(\<exists> x . qinterp (x#ats) p) = (qinterp (a#ats) (explode_minf (p,B)))"
+ (is "(\<exists> 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 "(\<exists>j\<in>{1..?d}. qinterp (j # ats) (minusinf p))
+ = (\<exists>j\<in> set (iupto(1,?d)). qinterp (j#ats) (minusinf p))"
+ (is "(\<exists> j\<in> {1..?d}. ?QM j) = \<dots>")
+ by (simp add: sym[OF iupto_set] )
+ also
+ have "\<dots> =(\<exists>j\<in> set (iupto(1,?d)). qinterp ((I_intterm (a#ats) (Cst j))#ats) (minusinf p))"
+ by simp
+ also have
+ "\<dots> = (\<exists>j\<in> set (map Cst (iupto(1,?d))). qinterp ((I_intterm (a#ats) j)#ats) (minusinf p))" by simp
+ also have
+ "\<dots> =
+ (\<exists>j\<in> 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:
+ "(\<exists> j\<in> {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: "\<forall>b\<in>set B. islinintterm b"
+ using bst by (simp add: bset_lin[OF unifp])
+ have bstnov0: "\<forall>b\<in>set B. novar0I b"
+ using bst by (simp add: bset_novar0[OF unifp])
+ have allsnov0: "\<forall>x\<in>set (all_sums(?d,B)). novar0I x "
+ by (simp add:all_sums_novar0[OF bstnov0 bstlin] )
+ have "(\<exists> j\<in> {1..?d}. \<exists> b\<in> set B. ?P (I_intterm (a#ats) b + j)) =
+ (\<exists> j\<in> {1..?d}. \<exists> b\<in> 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 "\<dots> = (\<exists> x \<in> set (all_sums (?d, B)). ?P (I_intterm (a#ats) x))"
+ by (simp add: all_sums_ex[where P="\<lambda> t. ?P (I_intterm (a#ats) t)"])
+ finally
+ have "(\<exists> j\<in> {1..?d}. \<exists> b\<in> set B. ?P (I_intterm (a#ats) b + j)) =
+ (\<exists> x \<in> 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 "\<dots> = (qinterp (a#ats) ?dj2)"
+ using linform_isqfree unified_islinform[OF unifp]
+ by (simp add: explode_disj_corr)
+ finally have dj2th:
+ "(\<exists> j\<in> {1..?d}. \<exists> b\<in> set B. ?P (I_intterm (a#ats) b + j)) =
+ (qinterp (a#ats) ?dj2)" by simp
+ let ?result = "\<lambda>f. \<lambda>g.
+ (case f of
+ T \<Rightarrow> T
+ | F \<Rightarrow> g
+ | _ \<Rightarrow> (case g of
+ T \<Rightarrow> T
+ | F \<Rightarrow> f
+ | _ \<Rightarrow> Or f g))"
+ have "?EXP a p = qinterp (a#ats) (?result ?dj1 ?dj2)"
+ by (simp only: explode_minf.simps Let_def)
+ also
+ have "\<dots> = (qinterp (a#ats) ?dj1 \<or> qinterp (a#ats) ?dj2)"
+ by (rule eval_Or_cases[where f="?dj1" and g="?dj2" and a="a" and ats="ats"])
+ also
+ have "\<dots> = ((\<exists> j\<in> {1..?d}. ?QM j) \<or>
+ (\<exists> j\<in> {1..?d}. \<exists> b\<in> set B. ?P (I_intterm (a#ats) b + j)))"
+ by (simp add: dj1_thm dj2th)
+ also
+ have "\<dots> = (\<exists> 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 = (\<exists>x. qinterp (x#ats) p)" by simp
+ also have "\<dots> = (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 \<Rightarrow> (QF \<times> intterm list)"
+ "unify p \<equiv>
+ (let q = unitycoeff p;
+ B = list_set(bset q);
+ A = list_set (aset q)
+ in
+ if (length B \<le> 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))) \<le> length (list_set (aset (unitycoeff p))) \<or> length (list_set(bset (unitycoeff p))) > length (list_set (aset (unitycoeff p)))" by arith
+ moreover
+ {
+ assume "length (list_set(bset (unitycoeff p))) \<le> 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 \<le> length ?la \<or> length ?lb > length ?la" by arith
+ moreover
+ {
+ assume "length ?lb \<le> 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: "\<forall> x\<in> 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 "\<dots> = set (map (\<lambda>x. lin_neg (lin_neg x)) (bset (mirror (unitycoeff p))))"
+ by auto
+ also have "\<dots> = 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 "\<exists> 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 "\<exists> 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 \<Rightarrow> QF option"
+"cooper p \<equiv> lift_un (\<lambda>q. decrvars(explode_minf (unify q))) (linform (nnf p))"
+
+(* cooper eliminates quantifiers *)
+lemma cooper_qfree: "(\<And> q q'. \<lbrakk>isqfree q ; cooper q = Some q'\<rbrakk> \<Longrightarrow> isqfree q')"
+proof-
+ fix "q" "q'"
+ assume qfq: "isqfree q"
+ and qeq: "cooper q = Some q'"
+ from qeq have "\<exists>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: "(\<And> q q' ats. \<lbrakk>isqfree q ; cooper q = Some q'\<rbrakk> \<Longrightarrow> (qinterp ats (QEx q)) = (qinterp ats q'))" (is "\<And> q q' ats. \<lbrakk> _ ; _ \<rbrakk> \<Longrightarrow> (?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 "\<exists>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 "\<forall> ats. ?P ats q = ?P ats (nnf q)" using nnf_corr qfq by auto
+ then have qeqp: "\<forall> 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 \<Rightarrow> QF option"
+"pa p \<equiv> lift_un psimpl (qelim(cooper, p))"
+
+lemma psimpl_qfree: "isqfree p \<Longrightarrow> 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 (\<lambda>x y. lin_add (x, lin_neg y), linearize y,
+ linearize z)", auto)
+apply (case_tac "a",auto)
+apply (case_tac "lift_bin (\<lambda>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: "\<And> p'. pa p = Some p' \<Longrightarrow> isqfree p'"
+proof(simp only: pa_def)
+fix "p'"
+assume qep: "lift_un psimpl (qelim (cooper, p)) = Some p'"
+then have "\<exists> 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 "\<And>q q'. \<lbrakk>isqfree q; cooper q = Some q'\<rbrakk> \<Longrightarrow> 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:
+ "\<And> p'. pa p = Some p' \<Longrightarrow> (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 "\<exists> 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:"\<And>q q' ats.
+ \<lbrakk>isqfree q; cooper q = Some q'\<rbrakk> \<Longrightarrow> qinterp ats (QEx q) = qinterp ats q'"
+ using cooper_corr by blast
+ moreover have cp2: "\<And>q q'. \<lbrakk>isqfree q; cooper q = Some q'\<rbrakk> \<Longrightarrow> 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 \<Rightarrow> None
+ | Some li \<Rightarrow> (case li of
+ Cst b \<Rightarrow> (case linearize j of
+ None \<Rightarrow> None
+ | (Some lj) \<Rightarrow> Some (lin_mul(b,lj)))
+ | _ \<Rightarrow> (case linearize j of
+ None \<Rightarrow> None
+ | (Some lj) \<Rightarrow> (case lj of
+ Cst b \<Rightarrow> Some (lin_mul (b,li))
+ | _ \<Rightarrow> None))))"
+by (simp add: measure_def inv_image_def)
+
+lemma [code]: "psimpl (And p q) =
+ (let p'= psimpl p
+ in (case p' of
+ F \<Rightarrow> F
+ |T \<Rightarrow> psimpl q
+ | _ \<Rightarrow> let q' = psimpl q
+ in (case q' of
+ F \<Rightarrow> F
+ | T \<Rightarrow> p'
+ | _ \<Rightarrow> (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 \<Rightarrow> T
+ | F \<Rightarrow> psimpl q
+ | _ \<Rightarrow> let q' = psimpl q
+ in (case q' of
+ T \<Rightarrow> T
+ | F \<Rightarrow> p'
+ | _ \<Rightarrow> (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 \<Rightarrow> T
+ |T \<Rightarrow> psimpl q
+ | NOT p1 \<Rightarrow> let q' = psimpl q
+ in (case q' of
+ F \<Rightarrow> p1
+ | T \<Rightarrow> T
+ | _ \<Rightarrow> (Or p1 q'))
+ | _ \<Rightarrow> let q' = psimpl q
+ in (case q' of
+ F \<Rightarrow> NOT p'
+ | T \<Rightarrow> T
+ | _ \<Rightarrow> (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