# Theory Reflected_Presburger

Up to index of Isabelle/HOL/ex

theory Reflected_Presburger
imports Main
begin

    (*  Title:      HOL/ex/PresburgerEx.thy
        ID:         $Id: Reflected_Presburger.thy,v 1.4 2005/09/23 19:02:13 webertj Exp $
        Author:     Amine Chaieb, TU Muenchen

    A formalization of quantifier elimination for Presburger arithmetic
    based on a generic quantifier elimination algorithm and Cooper's
    method to eliminate on ∃. *)

    header {* Quantifier elimination for Presburger arithmetic *}

    theory Reflected_Presburger
    imports Main
    begin

    (* Shadow syntax for integer terms *)
    datatype intterm =
        Cst int
      | Var nat
      | Neg intterm
      | Add intterm intterm
      | Sub intterm intterm
      | Mult intterm intterm

    (* interpretation of intterms, takes bound variables and free variables *)
    consts I_intterm :: "int list => intterm => int"
    primrec
    "I_intterm ats (Cst b) = b"
    "I_intterm ats (Var n) = (ats!n)"
    "I_intterm ats (Neg it) = -(I_intterm ats it)"
    "I_intterm ats (Add it1 it2) = (I_intterm ats it1) + (I_intterm ats it2)"
    "I_intterm ats (Sub it1 it2) = (I_intterm ats it1) - (I_intterm ats it2)"
    "I_intterm ats (Mult it1 it2) = (I_intterm ats it1) * (I_intterm ats it2)"

    (* Shadow syntax for Presburger formulae *)
    datatype QF =
       Lt intterm intterm
      |Gt intterm intterm
      |Le intterm intterm
      |Ge intterm intterm
      |Eq intterm intterm
      |Divides intterm intterm
      |T
      |F
      |NOT QF
      |And QF QF
      |Or QF QF
      |Imp QF QF
      |Equ QF QF
      |QAll QF
      |QEx QF

    (* Interpretation of Presburger formulae *)
    consts qinterp :: "int list => QF => bool"
    primrec
    "qinterp ats (Lt it1 it2) = (I_intterm ats it1 < I_intterm ats it2)"
    "qinterp ats (Gt it1 it2) = (I_intterm ats it1 > I_intterm ats it2)"
    "qinterp ats (Le it1 it2) = (I_intterm ats it1 ≤ I_intterm ats it2)"
    "qinterp ats (Ge it1 it2) = (I_intterm ats it1 ≥ I_intterm ats it2)"
    "qinterp ats (Divides it1 it2) = (I_intterm ats it1 dvd I_intterm ats it2)"
    "qinterp ats (Eq it1 it2) = (I_intterm ats it1 = I_intterm ats it2)"
    "qinterp ats T = True"
    "qinterp ats F = False"
    "qinterp ats (NOT p) = (¬(qinterp ats p))"
    "qinterp ats (And p q) = (qinterp ats p ∧ qinterp ats q)"
    "qinterp ats (Or p q) = (qinterp ats p ∨ qinterp ats q)"
    "qinterp ats (Imp p q) = (qinterp ats p --> qinterp ats q)"
    "qinterp ats (Equ p q) = (qinterp ats p = qinterp ats q)"
    "qinterp ats (QAll p) = (∀x. qinterp (x#ats) p)"
    "qinterp ats (QEx p) = (∃x. qinterp (x#ats) p)"

    (* quantifier elimination based on qe, quantifier elimination for an
       existential formula, with quantifier free body
       Since quantifier elimination for one formula is allowed to fail,
       the result is of type QF option *)

    consts lift_bin:: "('a => 'a => 'b) × 'a option × 'a option => 'b option"
    recdef lift_bin "measure (λ(c,a,b). size a)"
    "lift_bin (c,Some a,Some b) = Some (c a b)"
    "lift_bin (c,x, y)  = None"

    lemma lift_bin_Some:
      assumes ls: "lift_bin (c,x,y) = Some t"
      shows "(∃a. x = Some a) ∧ (∃b. y = Some b)"
      using ls
      by (cases "x", auto) (cases "y", auto)+

    consts lift_un:: "('a => 'b) => 'a option => 'b option"
    primrec
    "lift_un c None = None"
    "lift_un c (Some p) = Some (c p)"

    consts lift_qe:: "('a => 'b option) => 'a option => 'b option"
    primrec
    "lift_qe qe None = None"
    "lift_qe qe (Some p) = qe p"

    (* generic quantifier elimination *)
    consts qelim :: "(QF => QF option) × QF => QF option"
    recdef qelim "measure (λ(qe,p). size p)"
    "qelim (qe, (QAll p)) = lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,p))))"
    "qelim (qe, (QEx p)) = lift_qe qe (qelim (qe,p))"
    "qelim (qe, (And p q)) = lift_bin (And, (qelim (qe, p)), (qelim (qe, q)))"
    "qelim (qe, (Or p q)) = lift_bin (Or, (qelim (qe, p)), (qelim (qe, q)))"
    "qelim (qe, (Imp p q)) = lift_bin (Imp, (qelim (qe, p)), (qelim (qe, q)))"
    "qelim (qe, (Equ p q)) = lift_bin (Equ, (qelim (qe, p)), (qelim (qe, q)))"
    "qelim (qe,NOT p) = lift_un NOT (qelim (qe,p))"
    "qelim (qe, p) = Some p"

    (* quantifier free-ness *)
    consts isqfree :: "QF => bool"
    recdef isqfree "measure size"
    "isqfree (QAll p) = False"
    "isqfree (QEx p) = False"
    "isqfree (And p q) = (isqfree p ∧ isqfree q)"
    "isqfree (Or p q) = (isqfree p ∧ isqfree q)"
    "isqfree (Imp p q) = (isqfree p ∧ isqfree q)"
    "isqfree (Equ p q) = (isqfree p ∧ isqfree q)"
    "isqfree (NOT p) = isqfree p"
    "isqfree p = True"

    (* qelim lifts quantifierfreeness*)
    lemma qelim_qfree:
      assumes qeqf: "(!! q q'. [|isqfree q ; qe q = Some q'|] ==>  isqfree q')"
      shows qff:"!! p'. qelim (qe, p) = Some p' ==> isqfree p'"
      using qeqf
    proof (induct p)
      case (Lt a b)
      have "qelim (qe, Lt a b) = Some (Lt a b)" by simp
      moreover have "qelim (qe,Lt a b) = Some p'" .
      ultimately have "p' = Lt a b" by simp
      moreover have "isqfree (Lt a b)" by simp
      ultimately
      show ?case  by simp
    next
      case (Gt a b)
      have "qelim (qe, Gt a b) = Some (Gt a b)" by simp
      moreover have "qelim (qe,Gt a b) = Some p'" .
      ultimately have "p' = Gt a b" by simp
      moreover have "isqfree (Gt a b)" by simp
      ultimately
      show ?case  by simp
    next
      case (Le a b)
      have "qelim (qe, Le a b) = Some (Le a b)" by simp
      moreover have "qelim (qe,Le a b) = Some p'" .
      ultimately have "p' = Le a b" by simp
      moreover have "isqfree (Le a b)" by simp
      ultimately
      show ?case  by simp
    next
      case (Ge a b)
      have "qelim (qe, Ge a b) = Some (Ge a b)" by simp
      moreover have "qelim (qe,Ge a b) = Some p'" .
      ultimately have "p' = Ge a b" by simp
      moreover have "isqfree (Ge a b)" by simp
      ultimately
      show ?case  by simp
    next
      case (Eq a b)
      have "qelim (qe, Eq a b) = Some (Eq a b)" by simp
      moreover have "qelim (qe,Eq a b) = Some p'" .
      ultimately have "p' = Eq a b" by simp
      moreover have "isqfree (Eq a b)" by simp
      ultimately
      show ?case  by simp
    next
      case (Divides a b)
      have "qelim (qe, Divides a b) = Some (Divides a b)" by simp
      moreover have "qelim (qe,Divides a b) = Some p'" .
      ultimately have "p' = Divides a b" by simp
      moreover have "isqfree (Divides a b)" by simp
      ultimately
      show ?case  by simp
    next
      case T
      have "qelim(qe,T) = Some T" by simp
      moreover have "qelim(qe,T) = Some p'" .
      ultimately have "p' = T" by simp
      moreover have "isqfree T" by simp
      ultimately show ?case by simp
    next
      case F
      have "qelim(qe,F) = Some F" by simp
      moreover have "qelim(qe,F) = Some p'" .
      ultimately have "p' = F" by simp
      moreover have "isqfree F" by simp
      ultimately show ?case by simp
    next
      case (NOT p)
      from "NOT.prems" have "∃ p1. qelim(qe,p) = Some p1"
        by  (cases "qelim(qe,p)") simp_all
      then obtain "p1" where p1_def: "qelim(qe,p) = Some p1" by blast
      from "NOT.prems" have "!!q q'. [|isqfree q; qe q = Some q'|] ==> isqfree q'"
        by blast
      with "NOT.hyps" p1_def have p1qf: "isqfree p1" by blast
      then have "p' = NOT p1" using "NOT.prems" p1_def
        by (cases "qelim(qe,NOT p)") simp_all
      then show ?case using p1qf by simp
    next
      case (And p q)
      from "And.prems" have p1q1: "(∃p1. qelim(qe,p) = Some p1) ∧
        (∃q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="And"] by simp
      from p1q1 obtain "p1" and "q1"
        where p1_def: "qelim(qe,p) = Some p1"
        and q1_def: "qelim(qe,q) = Some q1" by blast
      from prems have qf1:"isqfree p1"
        using p1_def by blast
      from prems have qf2:"isqfree q1"
        using q1_def by blast
      from "And.prems" have "qelim(qe,And p q) = Some p'" by blast
      then have "p' = And p1 q1" using p1_def q1_def by simp
      then
      show ?case using qf1 qf2 by simp
    next
      case (Or p q)
      from "Or.prems" have p1q1: "(∃p1. qelim(qe,p) = Some p1) ∧
        (∃q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="Or"] by simp
      from p1q1 obtain "p1" and "q1"
        where p1_def: "qelim(qe,p) = Some p1"
        and q1_def: "qelim(qe,q) = Some q1" by blast
      from prems have qf1:"isqfree p1"
        using p1_def by blast
      from prems have qf2:"isqfree q1"
        using q1_def by blast
      from "Or.prems" have "qelim(qe,Or p q) = Some p'" by blast
      then have "p' = Or p1 q1" using p1_def q1_def by simp
      then
      show ?case using qf1 qf2 by simp
    next
      case (Imp p q)
      from "Imp.prems" have p1q1: "(∃p1. qelim(qe,p) = Some p1) ∧
        (∃q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="Imp"] by simp
      from p1q1 obtain "p1" and "q1"
        where p1_def: "qelim(qe,p) = Some p1"
        and q1_def: "qelim(qe,q) = Some q1" by blast
      from prems have qf1:"isqfree p1"
        using p1_def by blast
      from prems have qf2:"isqfree q1"
        using q1_def by blast
      from "Imp.prems" have "qelim(qe,Imp p q) = Some p'" by blast
      then have "p' = Imp p1 q1" using p1_def q1_def by simp
      then
      show ?case using qf1 qf2 by simp
    next
      case (Equ p q)
      from "Equ.prems" have p1q1: "(∃p1. qelim(qe,p) = Some p1) ∧
        (∃q1. qelim(qe,q) = Some q1)" using lift_bin_Some[where c="Equ"] by simp
      from p1q1 obtain "p1" and "q1"
        where p1_def: "qelim(qe,p) = Some p1"
        and q1_def: "qelim(qe,q) = Some q1" by blast
      from prems have qf1:"isqfree p1"
        using p1_def by blast
      from prems have qf2:"isqfree q1"
        using q1_def by blast
      from "Equ.prems" have "qelim(qe,Equ p q) = Some p'" by blast
      then have "p' = Equ p1 q1" using p1_def q1_def by simp
      then
      show ?case using qf1 qf2 by simp
    next
      case (QEx p)
      from "QEx.prems" have "∃ p1. qelim(qe,p) = Some p1"
        by  (cases "qelim(qe,p)") simp_all
      then obtain "p1" where p1_def: "qelim(qe,p) = Some p1" by blast
      from "QEx.prems" have "!!q q'. [|isqfree q; qe q = Some q'|] ==> isqfree q'"
        by blast
      with "QEx.hyps" p1_def have p1qf: "isqfree p1" by blast
      from "QEx.prems" have "qe p1 = Some p'" using p1_def by simp
      with "QEx.prems" show ?case  using p1qf
        by simp
    next
      case (QAll p)
      from "QAll.prems"
      have "∃ p1. lift_qe qe (lift_un NOT (qelim (qe ,p))) = Some p1"
        by (cases "lift_qe qe (lift_un NOT (qelim (qe ,p)))") simp_all
      then obtain "p1" where
        p1_def:"lift_qe qe (lift_un NOT (qelim (qe ,p))) = Some p1" by blast
      then have "∃ p2. lift_un NOT (qelim (qe ,p)) = Some p2"
        by (cases "qelim (qe ,p)") simp_all
      then obtain "p2"
        where p2_def:"lift_un NOT (qelim (qe ,p)) = Some p2" by blast
      then have "∃ p3. qelim(qe,p) = Some p3" by (cases "qelim(qe,p)") simp_all
      then obtain "p3" where p3_def: "qelim(qe,p) = Some p3" by blast
      with prems have qf3: "isqfree p3" by blast
      have p2_def2: "p2 = NOT p3" using p2_def p3_def by simp
      then have qf2: "isqfree p2" using qf3 by simp
      have p1_edf2: "qe p2 = Some p1" using p1_def p2_def by simp
      with "QAll.prems" have qf1: "isqfree p1" using qf2 by blast
      from "QAll.prems" have "p' = NOT p1" using p1_def by simp
      with qf1 show ?case by simp
    qed

    (* qelim lifts semantical equivalence *)
    lemma qelim_corr:
      assumes qecorr: "(!! q q' ats. [|isqfree q ; qe q = Some q'|] ==>  (qinterp ats (QEx q)) = (qinterp ats q'))"
      and qeqf: "(!! q q'. [|isqfree q ; qe q = Some q'|] ==>  isqfree q')"
      shows qff:"!! p' ats. qelim (qe, p) = Some p' ==> (qinterp ats p = qinterp ats p')" (is "!! p' ats. ?Qe p p' ==> (?F ats p = ?F ats p')")
      using qeqf qecorr
    proof (induct p)
      case (NOT f)
      from "NOT.prems" have "∃f'. ?Qe f f' " by (cases "qelim(qe,f)") simp_all
      then obtain "f'" where df': "?Qe f f'" by blast
      with prems have feqf': "?F ats f = ?F ats f'" by blast
      from "NOT.prems" df' have "p' = NOT f'" by simp
      with feqf' show ?case by simp

    next
      case (And f g)
      from "And.prems" have f1g1: "(∃f1. qelim(qe,f) = Some f1) ∧
        (∃g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="And"] by simp
      from f1g1 obtain "f1" and "g1"
        where f1_def: "qelim(qe, f) = Some f1"
        and g1_def: "qelim(qe,g) = Some g1" by blast
      from prems f1_def have feqf1: "?F ats f = ?F ats f1" by blast
      from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast
      from "And.prems" f1_def g1_def have "p' = And f1 g1" by simp
      with feqf1 geqg1 show ?case by simp

    next
      case (Or f g)
      from "Or.prems" have f1g1: "(∃f1. qelim(qe,f) = Some f1) ∧
        (∃g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="Or"] by simp
      from f1g1 obtain "f1" and "g1"
        where f1_def: "qelim(qe, f) = Some f1"
        and g1_def: "qelim(qe,g) = Some g1" by blast
      from prems f1_def have feqf1: "?F ats f = ?F ats  f1" by blast
      from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast
      from "Or.prems" f1_def g1_def have "p' = Or f1 g1" by simp
      with feqf1 geqg1 show ?case by simp
    next
      case (Imp f g)
      from "Imp.prems" have f1g1: "(∃f1. qelim(qe,f) = Some f1) ∧
        (∃g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="Imp"] by simp
      from f1g1 obtain "f1" and "g1"
        where f1_def: "qelim(qe, f) = Some f1"
        and g1_def: "qelim(qe,g) = Some g1" by blast
      from prems f1_def have feqf1: "?F ats f = ?F ats f1" by blast
      from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast
      from "Imp.prems" f1_def g1_def have "p' = Imp f1 g1" by simp
      with feqf1 geqg1 show ?case by simp
    next
      case (Equ f g)
      from "Equ.prems" have f1g1: "(∃f1. qelim(qe,f) = Some f1) ∧
        (∃g1. qelim(qe,g) = Some g1)" using lift_bin_Some[where c="Equ"] by simp
      from f1g1 obtain "f1" and "g1"
        where f1_def: "qelim(qe, f) = Some f1"
        and g1_def: "qelim(qe,g) = Some g1" by blast
      from prems f1_def have feqf1: "?F ats f = ?F ats f1" by blast
      from prems g1_def have geqg1: "?F ats g = ?F ats g1" by blast
      from "Equ.prems" f1_def g1_def have "p' = Equ f1 g1" by simp
      with feqf1 geqg1 show ?case by simp
    next
      case (QEx f)
        from "QEx.prems" have "∃ f1. ?Qe f f1"
        by  (cases "qelim(qe,f)") simp_all
      then obtain "f1" where f1_def: "qelim(qe,f) = Some f1" by blast
      from prems have qf1:"isqfree f1" using qelim_qfree by blast
      from prems have feqf1: "∀ ats. qinterp ats f = qinterp ats f1"
        using f1_def qf1 by blast
      then  have "?F ats (QEx f) = ?F ats (QEx f1)"
        by simp
      from prems have "qelim (qe,QEx f) = Some p'" by blast
      then  have "∃ f'. qe f1 = Some f'" using f1_def by simp
      then obtain "f'" where fdef': "qe f1 = Some f'" by blast
      with prems have exf1: "?F ats (QEx f1) = ?F ats f'" using qf1 by blast
      have fp: "?Qe (QEx f) f'" using f1_def fdef' by simp
      from prems have "?Qe (QEx f) p'" by blast
      then have "p' = f'" using fp by simp
      then show ?case using feqf1 exf1 by simp
    next
      case (QAll f)
      from "QAll.prems"
      have "∃ f0. lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,f)))) =
        Some f0"
        by (cases "lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,f))))")
          simp_all
      then obtain "f0"
        where f0_def: "lift_un NOT (lift_qe qe (lift_un NOT (qelim (qe ,f)))) =
        Some f0" by blast
      then have "∃ f1. lift_qe qe (lift_un NOT (qelim (qe ,f))) = Some f1"
        by (cases "lift_qe qe (lift_un NOT (qelim (qe ,f)))") simp_all
      then obtain "f1" where
        f1_def:"lift_qe qe (lift_un NOT (qelim (qe ,f))) = Some f1" by blast
      then have "∃ f2. lift_un NOT (qelim (qe ,f)) = Some f2"
        by (cases "qelim (qe ,f)") simp_all
      then obtain "f2"
        where f2_def:"lift_un NOT (qelim (qe ,f)) = Some f2" by blast
      then have "∃ f3. qelim(qe,f) = Some f3" by (cases "qelim(qe,f)") simp_all
      then obtain "f3" where f3_def: "qelim(qe,f) = Some f3" by blast
      from prems have qf3:"isqfree f3" using qelim_qfree by blast
      from prems have feqf3: "∀ ats. qinterp ats f = qinterp ats f3"
        using f3_def qf3 by blast
      have f23:"f2 = NOT f3" using f2_def f3_def by simp
      then have feqf2: "∀ ats. qinterp ats f = qinterp ats (NOT f2)"
        using feqf3 by simp
      have qf2: "isqfree f2" using f23 qf3 by simp
      have "qe f2 = Some f1" using f1_def f2_def f23 by simp
      with prems have exf2eqf1: "?F ats (QEx f2) = ?F ats f1" using qf2 by blast
      have "f0 = NOT f1" using f0_def f1_def by simp
      then have f0eqf1: "?F ats f0 = ?F ats (NOT f1)" by simp
      from prems have "qelim (qe, QAll f) = Some p'" by blast
      then have f0eqp': "p' = f0" using f0_def by simp
      have "?F ats (QAll f) = (∀x. ?F (x#ats) f)" by simp
      also have "… = (¬ (∃ x. ?F (x#ats) (NOT f)))" by simp
      also have "… = (¬ (∃ x. ?F (x#ats) (NOT (NOT f2))))" using feqf2
        by auto
      also have "… = (¬ (∃ x. ?F (x#ats) f2))" by simp
      also have "… = (¬ (?F ats f1))" using exf2eqf1 by simp
      finally show ?case using f0eqp' f0eqf1 by simp
    qed simp_all

    (* Cooper's algorithm *)

    (* Transform an intform into NNF *)
    consts lgth :: "QF => nat"
           nnf :: "QF => QF"
    primrec
    "lgth (Lt it1 it2) = 1"
    "lgth (Gt it1 it2) = 1"
    "lgth (Le it1 it2) = 1"
    "lgth (Ge it1 it2) = 1"
    "lgth (Eq it1 it2) = 1"
    "lgth (Divides it1 it2) = 1"
    "lgth T = 1"
    "lgth F = 1"
    "lgth (NOT p) = 1 + lgth p"
    "lgth (And p q) = 1 + lgth p + lgth q"
    "lgth (Or p q) = 1 + lgth p + lgth q"
    "lgth (Imp p q) = 1 + lgth p + lgth q"
    "lgth (Equ p q) = 1 + lgth p + lgth q"
    "lgth (QAll p) = 1 + lgth p"
    "lgth (QEx p) = 1 + lgth p"

    lemma [simp] :"0 < lgth q"
    apply (induct_tac q)
    apply(auto)
    done

    (* NNF *)
    recdef nnf "measure (λp. lgth p)"
      "nnf (Lt it1 it2) = Le (Sub it1 it2) (Cst (- 1))"
      "nnf (Gt it1 it2) = Le (Sub it2 it1) (Cst (- 1))"
      "nnf (Le it1 it2) = Le it1 it2 "
      "nnf (Ge it1 it2) = Le it2 it1"
      "nnf (Eq it1 it2) = Eq it2 it1"
      "nnf (Divides d t) = Divides d t"
      "nnf T = T"
      "nnf F = F"
      "nnf (And p q) = And (nnf p) (nnf q)"
      "nnf (Or p q) = Or (nnf p) (nnf q)"
      "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)"
      "nnf (Equ p q) = Or (And (nnf p) (nnf q))
      (And (nnf (NOT p)) (nnf (NOT q)))"
      "nnf (NOT (Lt it1 it2)) = (Le it2 it1)"
      "nnf (NOT (Gt it1 it2))  = (Le it1 it2)"
      "nnf (NOT (Le it1 it2)) = (Le (Sub it2 it1) (Cst (- 1)))"
      "nnf (NOT (Ge it1 it2)) = (Le (Sub it1 it2) (Cst (- 1)))"
      "nnf (NOT (Eq it1 it2)) = (NOT (Eq it1 it2))"
      "nnf (NOT (Divides d t)) = (NOT (Divides d t))"
      "nnf (NOT T) = F"
      "nnf (NOT F) = T"
      "nnf (NOT (NOT p)) = (nnf p)"
      "nnf (NOT (And p q)) = (Or (nnf (NOT p)) (nnf (NOT q)))"
      "nnf (NOT (Or p q)) = (And (nnf (NOT p)) (nnf (NOT q)))"
      "nnf (NOT (Imp p q)) = (And (nnf p) (nnf (NOT q)))"
      "nnf (NOT (Equ p q)) = (Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q)))"

    consts isnnf :: "QF => bool"
    recdef isnnf "measure (λp. lgth p)"
      "isnnf (Le it1 it2) = True"
      "isnnf (Eq it1 it2) = True"
      "isnnf (Divides d t) = True"
      "isnnf T = True"
      "isnnf F = True"
      "isnnf (And p q) = (isnnf p ∧ isnnf q)"
      "isnnf (Or p q) = (isnnf p ∧ isnnf q)"
      "isnnf (NOT (Divides d t)) = True"
      "isnnf (NOT (Eq it1 it2)) = True"
      "isnnf p = False"

    (* nnf preserves semantics *)
    lemma nnf_corr: "isqfree p ==> qinterp ats p = qinterp ats (nnf p)"
    by (induct p rule: nnf.induct,simp_all)
    (arith, arith, arith, arith, arith, arith, arith, arith, arith, blast)

    (* the result of nnf is in NNF *)
    lemma nnf_isnnf : "isqfree p ==> isnnf (nnf p)"
    by (induct p rule: nnf.induct, auto)

    lemma nnf_isqfree: "isnnf p ==> isqfree p"
    by (induct p rule: isnnf.induct) auto

    (* nnf preserves quantifier freeness *)
    lemma nnf_qfree: "isqfree p ==> isqfree(nnf p)"
      using nnf_isqfree nnf_isnnf by simp

    (* Linearization and normalization of formulae *)
    (* Definition of linearity of an intterm *)

    consts islinintterm :: "intterm => bool"
    recdef islinintterm "measure size"
    "islinintterm (Cst i) = True"
    "islinintterm (Add (Mult (Cst i) (Var n)) (Cst i')) = (i ≠ 0)"
    "islinintterm (Add (Mult (Cst i) (Var n)) (Add (Mult (Cst i') (Var n')) r)) = ( i ≠ 0 ∧ i' ≠ 0 ∧ n < n' ∧ islinintterm  (Add (Mult (Cst i') (Var n')) r))"
    "islinintterm i = False"

    (* subterms of linear terms are linear *)
    lemma islinintterm_subt:
      assumes lr: "islinintterm (Add (Mult (Cst i) (Var n)) r)"
      shows "islinintterm r"
    using lr
    by (induct r rule: islinintterm.induct) auto

    (* c ≠ 0 for linear term c.n + r*)
    lemma islinintterm_cnz:
      assumes lr: "islinintterm (Add (Mult (Cst i) (Var n)) r)"
      shows "i ≠ 0"
    using lr
    by (induct r rule: islinintterm.induct) auto

    lemma islininttermc0r: "islinintterm (Add (Mult (Cst c) (Var n)) r) ==> (c ≠ 0 ∧ islinintterm r)"
    by (induct r rule: islinintterm.induct, simp_all)

    (* An alternative linearity definition *)
    consts islintn :: "(nat × intterm) => bool"
    recdef islintn "measure (λ (n,t). (size t))"
    "islintn (n0, Cst i) = True"
    "islintn (n0, Add (Mult (Cst i) (Var n)) r) = (i ≠ 0 ∧ n0 ≤ n ∧ islintn (n+1,r))"
    "islintn (n0, t) = False"

    constdefs islint :: "intterm => bool"
      "islint t ≡ islintn(0,t)"

    (* And the equivalence to the first definition *)
    lemma islinintterm_eq_islint: "islinintterm t = islint t"
      using islint_def
    by (induct t rule: islinintterm.induct) auto

    (* monotony *)
    lemma islintn_mon:
      assumes lin: "islintn (n,t)"
      and mgen: "m ≤ n"
      shows "islintn(m,t)"
      using lin mgen
    by (induct t rule: islintn.induct) auto

    lemma islintn_subt:
      assumes lint: "islintn(n,Add (Mult (Cst i) (Var m)) r)"
      shows "islintn (m+1,r)"
    using lint
    by auto

    (* List indexin for n > 0 *)
    lemma nth_pos: "0 < n --> (x#xs) ! n = (y#xs) ! n"
    using Nat.gr0_conv_Suc
    by clarsimp

    lemma nth_pos2: "0 < n ==> (x#xs) ! n = xs ! (n - 1)"
    using Nat.gr0_conv_Suc
    by clarsimp

    lemma intterm_novar0:
      assumes lin: "islinintterm (Add (Mult (Cst i) (Var n)) r)"
      shows "I_intterm (x#ats) r = I_intterm (y#ats) r"
    using lin
    by (induct r rule: islinintterm.induct) (simp_all add: nth_pos2)
    (* a simple version of a general theorem: Interpretation does not depend
       on the first variable if it does not occur in the term *)

    lemma linterm_novar0:
      assumes lin: "islintn (n,t)"
      and npos: "0 < n"
      shows "I_intterm (x#ats) t = I_intterm (y#ats) t"
    using lin npos
    by (induct n t rule: islintn.induct) (simp_all add: nth_pos2)

    (* Periodicity of dvd *)
    lemma dvd_period:
      assumes advdd: "(a::int) dvd d"
      shows "(a dvd (x + t)) = (a dvd ((x+ c*d) + t))"
    using advdd
    proof-
      from advdd  have "∀x.∀k. (((a::int) dvd (x + t)) = (a dvd
     (x+k*d + t)))" by (rule dvd_modd_pinf)
      then show ?thesis by simp
    qed

    (* lin_ad adds two linear terms*)
    consts lin_add :: "intterm × intterm => intterm"
    recdef lin_add "measure (λ(x,y). ((size x) + (size y)))"
    "lin_add (Add (Mult (Cst c1) (Var n1)) (r1),Add (Mult (Cst c2) (Var n2)) (r2)) =
      (if n1=n2 then
      (let c = Cst (c1 + c2)
       in (if c1+c2=0 then lin_add(r1,r2) else Add (Mult c (Var n1)) (lin_add (r1,r2))))
      else if n1 ≤ n2 then (Add (Mult (Cst c1) (Var n1)) (lin_add (r1,Add (Mult (Cst c2) (Var n2)) (r2))))
      else (Add (Mult (Cst c2) (Var n2)) (lin_add (Add (Mult (Cst c1) (Var n1)) r1,r2))))"
    "lin_add (Add (Mult (Cst c1) (Var n1)) (r1),Cst b) =
      (Add (Mult (Cst c1) (Var n1)) (lin_add (r1, Cst b)))"
    "lin_add (Cst x,Add (Mult (Cst c2) (Var n2)) (r2)) =
      Add (Mult (Cst c2) (Var n2)) (lin_add (Cst x,r2))"
    "lin_add (Cst b1, Cst b2) = Cst (b1+b2)"

    lemma lin_add_cst_corr:
      assumes blin : "islintn(n0,b)"
      shows "I_intterm ats (lin_add (Cst a,b)) = (I_intterm ats (Add (Cst a) b))"
    using blin
    by (induct n0 b rule: islintn.induct) auto

    lemma lin_add_cst_corr2:
      assumes blin : "islintn(n0,b)"
      shows "I_intterm ats (lin_add (b,Cst a)) = (I_intterm ats (Add b (Cst a)))"
    using blin
    by (induct n0 b rule: islintn.induct) auto

    lemma lin_add_corrh: "!! n01 n02. [| islintn (n01,a) ; islintn (n02,b)|]
      ==> I_intterm ats (lin_add(a,b)) = I_intterm ats (Add a b)"
    proof(induct a b rule: lin_add.induct)
      case (58 i n r j m s)
      have "(n = m ∧ i+j = 0) ∨ (n = m ∧ i+j ≠ 0) ∨ n < m ∨ m < n " by arith
      moreover
      {assume "n=m∧i+j=0" hence ?case using prems by (auto simp add: sym[OF zadd_zmult_distrib]) }
      moreover
      {assume "n=m∧i+j≠0" hence ?case using prems by (auto simp add: Let_def zadd_zmult_distrib)}
      moreover
      {assume "n < m" hence ?case using prems by auto }
      moreover
      {assume "n > m" hence ?case using prems by auto }
      ultimately show ?case by blast
    qed (auto simp add: lin_add_cst_corr lin_add_cst_corr2 Let_def)

    (* lin_add has the semantics of Add*)
    lemma lin_add_corr:
      assumes lina: "islinintterm a"
      and linb: "islinintterm b"
      shows "I_intterm ats (lin_add (a,b)) = (I_intterm ats (Add a b))"
    using lina linb islinintterm_eq_islint islint_def lin_add_corrh
    by blast

    lemma lin_add_cst_lint:
      assumes lin: "islintn (n0,b)"
      shows "islintn (n0, lin_add (Cst i, b))"
    using lin
    by (induct n0 b rule: islintn.induct) auto

    lemma lin_add_cst_lint2:
      assumes lin: "islintn (n0,b)"
      shows "islintn (n0, lin_add (b,Cst i))"
    using lin
    by (induct n0 b rule: islintn.induct) auto

    (* lin_add preserves linearity..*)
    lemma lin_add_lint: "!! n0 n01 n02. [| islintn (n01,a) ; islintn (n02,b); n0 ≤  min n01 n02 |]
      ==> islintn (n0, lin_add (a,b))"
    proof (induct a b rule: lin_add.induct)
      case (58 i n r j m s)
      have "(n =m ∧ i + j = 0) ∨ (n = m ∧ i+j ≠ 0) ∨ n <m ∨ m < n" by arith
      moreover
      { assume "n = m"
          and  "i+j = 0"
        hence ?case using "58" islintn_mon[where m = "n01" and n = "Suc m"]
          islintn_mon[where m = "n02" and n = "Suc m"] by auto }
      moreover
      { assume  "n = m"
          and "i+j ≠ 0"
        hence ?case using "58" islintn_mon[where m = "n01" and n = "Suc m"]
          islintn_mon[where m = "n02" and n = "Suc m"] by (auto simp add: Let_def) }
      moreover
      { assume "n < m" hence ?case using 58 by force }
    moreover
      { assume "m < n"
        hence ?case using 58
          apply (auto simp add: Let_def)
          apply (erule allE[where x = "Suc m" ] )
          by (erule allE[where x = "Suc m" ] ) simp }
      ultimately show ?case by blast
    qed(simp_all add: Let_def lin_add_cst_lint lin_add_cst_lint2)

    lemma lin_add_lin:
      assumes lina: "islinintterm a"
      and linb: "islinintterm b"
      shows "islinintterm (lin_add (a,b))"
    using islinintterm_eq_islint islint_def lin_add_lint lina linb by auto

    (* lin_mul multiplies a linear term by a constant *)
    consts lin_mul :: "int × intterm => intterm"
    recdef lin_mul "measure (λ(c,t). size t)"
    "lin_mul (c,Cst i) = (Cst (c*i))"
    "lin_mul (c,Add (Mult (Cst c') (Var n)) r)  =
      (if c = 0 then (Cst 0) else
      (Add (Mult (Cst (c*c')) (Var n)) (lin_mul (c,r))))"

    lemma zmult_zadd_distrib[simp]: "(a::int) * (b+c) = a*b + a*c"
    proof-
      have "a*(b+c) = (b+c)*a" by simp
      moreover have "(b+c)*a = b*a + c*a" by (simp add: zadd_zmult_distrib)
      ultimately show ?thesis by simp
    qed

    (* lin_mul has the semantics of Mult *)
    lemma lin_mul_corr:
      assumes lint: "islinintterm  t"
      shows "I_intterm ats (lin_mul (c,t)) = I_intterm ats (Mult (Cst c) t)"
    using lint
    proof (induct c t rule: lin_mul.induct)
      case (21 c c' n r)
      have "islinintterm (Add (Mult (Cst c') (Var n)) r)" .
      then have "islinintterm r"
        by (rule islinintterm_subt[of "c'" "n" "r"])
      then show ?case  using "21.hyps" "21.prems" by simp
    qed(auto)

    (* lin_mul preserves linearity *)
    lemma lin_mul_lin:
      assumes lint: "islinintterm t"
      shows "islinintterm (lin_mul(c,t))"
    using lint
    by (induct t rule: islinintterm.induct) auto

    lemma lin_mul0:
      assumes lint: "islinintterm t"
      shows "lin_mul(0,t) = Cst 0"
      using lint
      by (induct t rule: islinintterm.induct) auto

    lemma lin_mul_lintn:
      "!! m. islintn(m,t) ==> islintn(m,lin_mul(l,t))"
      by (induct l t rule: lin_mul.induct) simp_all

    (* lin_neg neagtes a linear term *)
    constdefs lin_neg :: "intterm => intterm"
    "lin_neg i == lin_mul ((-1::int),i)"

    (* lin_neg has the semantics of Neg *)
    lemma lin_neg_corr:
      assumes lint: "islinintterm  t"
      shows "I_intterm ats (lin_neg t) = I_intterm ats (Neg t)"
      using lint lin_mul_corr
      by (simp add: lin_neg_def lin_mul_corr)

    (* lin_neg preserves linearity *)
    lemma lin_neg_lin:
      assumes lint: "islinintterm  t"
      shows "islinintterm (lin_neg t)"
    using lint
    by (simp add: lin_mul_lin lin_neg_def)

    (* Some properties about lin_add and lin-neg should be moved above *)

    lemma lin_neg_idemp:
      assumes lini: "islinintterm i"
      shows "lin_neg (lin_neg i) = i"
    using lini
    by (induct i rule: islinintterm.induct) (auto simp add: lin_neg_def)

    lemma lin_neg_lin_add_distrib:
      assumes lina : "islinintterm a"
      and linb :"islinintterm b"
      shows "lin_neg (lin_add(a,b)) = lin_add (lin_neg a, lin_neg b)"
    using lina linb
    proof (induct a b rule: lin_add.induct)
      case (58 c1 n1 r1 c2 n2 r2)
      from prems have lincnr1:"islinintterm (Add (Mult (Cst c1) (Var n1)) r1)" by simp
      have linr1: "islinintterm r1" by (rule islinintterm_subt[OF lincnr1])
      from prems have lincnr2: "islinintterm (Add (Mult (Cst c2) (Var n2)) r2)" by simp
      have linr2: "islinintterm r2" by (rule islinintterm_subt[OF lincnr2])
      have "n1 = n2 ∨ n1 < n2 ∨ n1 > n2" by arith
      show ?case using prems linr1 linr2 by (simp_all add: lin_neg_def Let_def)
    next
      case (59 c n r b)
      from prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var n)) r)" by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      show ?case using prems linr by (simp add: lin_neg_def Let_def)
    next
      case (60 b c n r)
      from prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var n)) r)" by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      show ?case  using prems linr by (simp add: lin_neg_def Let_def)
    qed (simp_all add: lin_neg_def)

    (* linearize tries to linearize a term *)
    consts linearize :: "intterm => intterm option"
    recdef linearize "measure (λt. size t)"
    "linearize (Cst b) = Some (Cst b)"
    "linearize (Var n) = Some (Add (Mult (Cst 1) (Var n)) (Cst 0))"
    "linearize (Neg i) = lift_un lin_neg (linearize i)"
     "linearize (Add i j) = lift_bin(λ x. λ y. lin_add(x,y), linearize i, linearize j)"
    "linearize (Sub i j) =
      lift_bin(λ x. λ y. lin_add(x,lin_neg y), linearize i, linearize j)"
    "linearize (Mult i j) =
      (case linearize i of
      None => None
      | Some li => (case li of
         Cst b => (case linearize j of
          None => None
         | (Some lj) => Some (lin_mul(b,lj)))
      | _ => (case linearize j of
          None => None
        | (Some lj) => (case lj of
            Cst b => Some (lin_mul (b,li))
          | _ => None))))"

    lemma linearize_linear1:
      assumes lin: "linearize t ≠ None"
      shows "islinintterm (the (linearize t))"
    using lin
    proof (induct t rule: linearize.induct)
      case (1 b) show ?case by simp
    next
      case (2 n) show ?case by simp
    next
      case (3 i) show ?case
        proof-
        have "(linearize i = None) ∨ (∃li. linearize i = Some li)" by auto
        moreover
        { assume "linearize i = None" with prems have ?thesis by auto}
        moreover
        { assume lini: "∃li. linearize i = Some li"
          from lini obtain "li" where  "linearize i = Some li" by blast
          have linli: "islinintterm li" by (simp!)
          moreover have "linearize (Neg i) = Some (lin_neg li)" using prems by simp
          moreover from linli have "islinintterm(lin_neg li)" by (simp add: lin_neg_lin)
          ultimately have ?thesis by simp
        }
        ultimately show ?thesis by blast
      qed
    next
      case (4 i j) show ?case
        proof-
        have "(linearize i = None) ∨ ((∃ li. linearize i = Some li) ∧ linearize j = None) ∨ ((∃ li. linearize i = Some li) ∧ (∃ lj. linearize j = Some lj))" by auto
        moreover
        {
          assume nlini: "linearize i = None"
          from nlini have "linearize (Add i j) = None"
            by (simp add: Let_def measure_def inv_image_def) then have ?thesis using prems by auto}
        moreover
        { assume nlinj: "linearize j = None"
            and lini: "∃ li. linearize i = Some li"
          from nlinj lini have "linearize (Add i j) = None"
            by (simp add: Let_def measure_def inv_image_def, auto) with prems  have ?thesis by auto}
        moreover
        { assume lini: "∃li. linearize i = Some li"
            and linj: "∃lj. linearize j = Some lj"
          from lini obtain "li" where  "linearize i = Some li" by blast
          have linli: "islinintterm li" by (simp!)
          from linj obtain "lj" where  "linearize j = Some lj" by blast
          have linlj: "islinintterm lj" by (simp!)
          moreover from lini linj have "linearize (Add i j) = Some (lin_add (li,lj))"
            by (simp add: measure_def inv_image_def, auto!)
          moreover from linli linlj have "islinintterm(lin_add (li,lj))" by (simp add: lin_add_lin)
          ultimately have ?thesis by simp  }
        ultimately show ?thesis by blast
      qed
    next
      case (5 i j)show ?case
        proof-
        have "(linearize i = None) ∨ ((∃ li. linearize i = Some li) ∧ linearize j = None) ∨ ((∃ li. linearize i = Some li) ∧ (∃ lj. linearize j = Some lj))" by auto
        moreover
        {
          assume nlini: "linearize i = None"
          from nlini have "linearize (Sub i j) = None" by (simp add: Let_def measure_def inv_image_def) then have ?thesis by (auto!)
        }
        moreover
        {
          assume lini: "∃ li. linearize i = Some li"
            and nlinj: "linearize j = None"
          from nlinj lini have "linearize (Sub i j) = None"
            by (simp add: Let_def measure_def inv_image_def, auto) then have ?thesis by (auto!)
        }
        moreover
        {
          assume lini: "∃li. linearize i = Some li"
            and linj: "∃lj. linearize j = Some lj"
          from lini obtain "li" where  "linearize i = Some li" by blast
          have linli: "islinintterm li" by (simp!)
          from linj obtain "lj" where  "linearize j = Some lj" by blast
          have linlj: "islinintterm lj" by (simp!)
          moreover from lini linj have "linearize (Sub i j) = Some (lin_add (li,lin_neg lj))"
            by (simp add: measure_def inv_image_def, auto!)
          moreover from linli linlj have "islinintterm(lin_add (li,lin_neg lj))" by (simp add: lin_add_lin lin_neg_lin)
          ultimately have ?thesis by simp
        }
        ultimately show ?thesis by blast
      qed
    next
      case (6 i j)show ?case
        proof-
          have cses: "(linearize i = None) ∨
            ((∃ li. linearize i = Some li) ∧ linearize j = None) ∨
            ((∃ li. linearize i = Some li) ∧ (∃ bj. linearize j = Some (Cst bj)))
            ∨ ((∃ bi. linearize i = Some (Cst bi)) ∧ (∃ lj. linearize j = Some lj))
            ∨ ((∃ li. linearize i = Some li ∧ ¬ (∃ bi. li = Cst bi)) ∧ (∃ lj. linearize j = Some lj ∧ ¬ (∃ bj. lj = Cst bj)))" by auto
        moreover
        {
          assume nlini: "linearize i = None"
          from nlini have "linearize (Mult i j) = None"
            by (simp add: Let_def measure_def inv_image_def)
          with prems have ?thesis by auto }
        moreover
        {  assume lini: "∃ li. linearize i = Some li"
            and nlinj: "linearize j = None"
          from lini obtain "li" where "linearize i = Some li" by blast
          moreover from nlinj lini have "linearize (Mult i j) = None"
            using prems
            by (cases li ) (auto simp add: Let_def measure_def inv_image_def)
          with prems have ?thesis by auto}
        moreover
        { assume lini: "∃li. linearize i = Some li"
            and linj: "∃bj. linearize j = Some (Cst bj)"
          from lini obtain "li" where  li_def: "linearize i = Some li" by blast
          from prems have linli: "islinintterm li" by simp
          moreover
          from linj  obtain "bj" where  bj_def: "linearize j = Some (Cst bj)" by blast
          have linlj: "islinintterm (Cst bj)" by simp
          moreover from lini linj prems
          have "linearize (Mult i j) = Some (lin_mul (bj,li))"
            by (cases li) (auto simp add: measure_def inv_image_def)
          moreover from linli linlj have "islinintterm(lin_mul (bj,li))" by (simp add: lin_mul_lin)
          ultimately have ?thesis by simp  }
        moreover
        { assume lini: "∃bi. linearize i = Some (Cst bi)"
            and linj: "∃lj. linearize j = Some lj"
          from lini obtain "bi" where  "linearize i = Some (Cst bi)" by blast
          from prems have linli: "islinintterm (Cst bi)" by simp
          moreover
          from linj  obtain "lj" where  "linearize j = Some lj" by blast
          from prems have linlj: "islinintterm lj" by simp
          moreover from lini linj prems have "linearize (Mult i j) = Some (lin_mul (bi,lj))"
            by (simp add: measure_def inv_image_def)
          moreover from linli linlj have "islinintterm(lin_mul (bi,lj))" by (simp add: lin_mul_lin)
          ultimately have ?thesis by simp }
        moreover
        { assume linc: "∃ li. linearize i = Some li ∧ ¬ (∃ bi. li = Cst bi)"
            and ljnc: "∃ lj. linearize j = Some lj ∧ ¬ (∃ bj. lj = Cst bj)"
          from linc obtain "li" where "linearize i = Some li ∧ ¬ (∃ bi. li = Cst bi)" by blast
          moreover
          from ljnc obtain "lj" where "linearize j = Some lj ∧ ¬ (∃ bj. lj = Cst bj)" by blast
          ultimately have "linearize (Mult i j) = None"
            by (cases li, auto simp add: measure_def inv_image_def) (cases lj, auto)+
          with prems have ?thesis by simp }
        ultimately show ?thesis by blast
      qed
    qed

    (* the result of linearize, when successful, is a linear term*)
    lemma linearize_linear: "!! t'. linearize t = Some t' ==> islinintterm t'"
    proof-
      fix t'
      assume lint: "linearize t = Some t'"
      from lint have lt: "linearize t ≠ None" by auto
      then have "islinintterm (the (linearize t))" by (rule_tac  linearize_linear1[OF lt])
      with lint show "islinintterm t'" by simp
    qed

    lemma linearize_corr1:
      assumes lin: "linearize t ≠ None"
      shows "I_intterm ats t = I_intterm ats (the (linearize t))"
    using lin
    proof (induct t rule: linearize.induct)
      case (3 i) show ?case
        proof-
        have "(linearize i = None) ∨ (∃li. linearize i = Some li)" by auto
        moreover
        {
          assume "linearize i = None"
          have ?thesis using prems by simp
        }
        moreover
        {
          assume lini: "∃li. linearize i = Some li"
          from lini have lini2: "linearize i ≠ None" by simp
          from lini obtain "li" where  "linearize i = Some li" by blast
          from lini2 lini have "islinintterm (the (linearize i))"
            by (simp add: linearize_linear1[OF lini2])
          then have linli: "islinintterm li" using prems by simp
          have ieqli: "I_intterm ats i = I_intterm ats li" using prems by simp
          moreover have "linearize (Neg i) = Some (lin_neg li)" using prems by simp
          moreover from ieqli linli have "I_intterm ats (Neg i) = I_intterm ats (lin_neg li)" by (simp add: lin_neg_corr[OF linli])
          ultimately have ?thesis using prems by (simp add: lin_neg_corr)
        }
        ultimately show ?thesis by blast
      qed
    next
      case (4 i j) show ?case
        proof-
        have "(linearize i = None) ∨ ((∃ li. linearize i = Some li) ∧ linearize j = None) ∨ ((∃ li. linearize i = Some li) ∧ (∃ lj. linearize j = Some lj))" by auto
        moreover
        {
          assume nlini: "linearize i = None"
          from nlini have "linearize (Add i j) = None" by (simp add: Let_def measure_def inv_image_def) then have ?thesis using prems by auto
        }
        moreover
        {
          assume nlinj: "linearize j = None"
            and lini: "∃ li. linearize i = Some li"
          from nlinj lini have "linearize (Add i j) = None"
            by (simp add: Let_def measure_def inv_image_def, auto)
          then have ?thesis using prems by auto
        }
        moreover
        {
          assume lini: "∃li. linearize i = Some li"
            and linj: "∃lj. linearize j = Some lj"
          from lini have lini2: "linearize i ≠ None" by simp
          from linj have linj2: "linearize j ≠ None" by simp
          from lini obtain "li" where  "linearize i = Some li" by blast
          from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
          then have linli: "islinintterm li" using prems by simp
          from linj obtain "lj" where  "linearize j = Some lj" by blast
          from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1)
          then have linlj: "islinintterm lj" using prems by simp
          moreover from lini linj have "linearize (Add i j) = Some (lin_add (li,lj))"
            using prems by (simp add: measure_def inv_image_def)
          moreover from linli linlj have "I_intterm ats (lin_add (li,lj)) = I_intterm ats (Add li lj)" by (simp add: lin_add_corr)
          ultimately have ?thesis using prems by simp
        }
        ultimately show ?thesis by blast
      qed
    next
      case (5 i j)show ?case
        proof-
        have "(linearize i = None) ∨ ((∃ li. linearize i = Some li) ∧ linearize j = None) ∨ ((∃ li. linearize i = Some li) ∧ (∃ lj. linearize j = Some lj))" by auto
        moreover
        {
          assume nlini: "linearize i = None"
          from nlini have "linearize (Sub i j) = None" by (simp add: Let_def measure_def inv_image_def) then have ?thesis using prems by auto
        }
        moreover
        {
          assume lini: "∃ li. linearize i = Some li"
            and nlinj: "linearize j = None"
          from nlinj lini have "linearize (Sub i j) = None"
            by (simp add: Let_def measure_def inv_image_def, auto) with prems have ?thesis by auto
        }
        moreover
        {
          assume lini: "∃li. linearize i = Some li"
            and linj: "∃lj. linearize j = Some lj"
          from lini have lini2: "linearize i ≠ None" by simp
          from linj have linj2: "linearize j ≠ None" by simp
          from lini obtain "li" where  "linearize i = Some li" by blast
          from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
          with prems have linli: "islinintterm li" by simp
          from linj obtain "lj" where  "linearize j = Some lj" by blast
          from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1)
          with prems have linlj: "islinintterm lj" by simp
          moreover from prems have "linearize (Sub i j) = Some (lin_add (li,lin_neg lj))"
            by (simp add: measure_def inv_image_def)
          moreover from linlj have linnlj:"islinintterm (lin_neg lj)" by (simp add: lin_neg_lin)
          moreover from linli linnlj have "I_intterm ats (lin_add (li,lin_neg lj)) = I_intterm ats (Add li (lin_neg lj))" by (simp only: lin_add_corr[OF linli linnlj])
          moreover from linli linlj linnlj have "I_intterm ats (Add li (lin_neg lj)) = I_intterm ats (Sub li lj)"
            by (simp add: lin_neg_corr)
          ultimately have ?thesis using prems by simp
        }
        ultimately show ?thesis by blast
      qed
    next
      case (6 i j)show ?case
        proof-
          have cses: "(linearize i = None) ∨
            ((∃ li. linearize i = Some li) ∧ linearize j = None) ∨
            ((∃ li. linearize i = Some li) ∧ (∃ bj. linearize j = Some (Cst bj)))
            ∨ ((∃ bi. linearize i = Some (Cst bi)) ∧ (∃ lj. linearize j = Some lj))
            ∨ ((∃ li. linearize i = Some li ∧ ¬ (∃ bi. li = Cst bi)) ∧ (∃ lj. linearize j = Some lj ∧ ¬ (∃ bj. lj = Cst bj)))" by auto
        moreover
        {
          assume nlini: "linearize i = None"
          from nlini have "linearize (Mult i j) = None" by (simp add: Let_def measure_def inv_image_def) with prems  have ?thesis by auto
        }
        moreover
        {
          assume lini: "∃ li. linearize i = Some li"
            and nlinj: "linearize j = None"

          from lini obtain "li" where "linearize i = Some li" by blast
          moreover from prems have "linearize (Mult i j) = None"
            by (cases li) (simp_all add: Let_def measure_def inv_image_def)
          with prems have ?thesis by auto
        }
        moreover
        {
          assume lini: "∃li. linearize i = Some li"
            and linj: "∃bj. linearize j = Some (Cst bj)"
          from lini have lini2: "linearize i ≠ None" by simp
          from linj have linj2: "linearize j ≠ None" by auto
          from lini obtain "li" where  "linearize i = Some li" by blast
          from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
          with prems  have linli: "islinintterm li" by simp
          moreover
          from linj  obtain "bj" where  "linearize j = Some (Cst bj)" by blast
          have linlj: "islinintterm (Cst bj)" by simp
          moreover from prems have "linearize (Mult i j) = Some (lin_mul (bj,li))"
            by (cases li) (auto simp add: measure_def inv_image_def)
          then have lm1: "I_intterm ats (the(linearize (Mult i j))) = I_intterm ats (lin_mul (bj,li))" by simp
          moreover from linli linlj have "I_intterm ats (lin_mul(bj,li)) = I_intterm ats (Mult li (Cst bj))" by (simp add: lin_mul_corr)
          with prems
          have "I_intterm ats (lin_mul(bj,li)) = I_intterm ats (Mult li (the (linearize j)))"
            by auto
          moreover have "I_intterm ats (Mult li (the (linearize j))) = I_intterm ats (Mult i (the (linearize j)))" using prems  by simp
          moreover have "I_intterm ats i = I_intterm ats (the (linearize i))"
            using lini2 lini "6.hyps" by simp
            moreover have "I_intterm ats j = I_intterm ats (the (linearize j))"
              using prems by (cases li) (auto simp add: measure_def inv_image_def)
          ultimately have ?thesis by auto }
        moreover
        { assume lini: "∃bi. linearize i = Some (Cst bi)"
            and linj: "∃lj. linearize j = Some lj"
          from lini have lini2 : "linearize i ≠ None" by auto
          from linj have linj2 : "linearize j ≠ None" by auto
          from lini obtain "bi" where  "linearize i = Some (Cst bi)" by blast
          have linli: "islinintterm (Cst bi)" using prems by simp
          moreover
          from linj  obtain "lj" where  "linearize j = Some lj" by blast
          from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1)
          then have linlj: "islinintterm lj" by (simp!)
          moreover from linli lini linj have "linearize (Mult i j) = Some (lin_mul (bi,lj))"        apply (simp add: measure_def inv_image_def)
            apply auto by (case_tac "li::intterm",auto!)
          then have lm1: "I_intterm ats (the(linearize (Mult i j))) = I_intterm ats (lin_mul (bi,lj))" by simp
          moreover from linli linlj have "I_intterm ats (lin_mul(bi,lj)) = I_intterm ats (Mult (Cst bi) lj)" by (simp add: lin_mul_corr)
          then have "I_intterm ats (lin_mul(bi,lj)) = I_intterm ats (Mult (the (linearize i)) lj)" by (auto!)
          moreover have "I_intterm ats (Mult (the (linearize i)) lj) = I_intterm ats (Mult (the (linearize i)) j)" using lini lini2  by (simp!)
          moreover have "I_intterm ats i = I_intterm ats (the (linearize i))"
            using lini2 lini "6.hyps" by simp
            moreover have "I_intterm ats j = I_intterm ats (the (linearize j))"
              using linj linj2 lini lini2 linli linlj "6.hyps" by (auto!)

          ultimately have ?thesis by auto }
        moreover
        { assume linc: "∃ li. linearize i = Some li ∧ ¬ (∃ bi. li = Cst bi)"
            and ljnc: "∃ lj. linearize j = Some lj ∧ ¬ (∃ bj. lj = Cst bj)"
          from linc obtain "li" where "∃ li. linearize i = Some li ∧ ¬ (∃ bi. li = Cst bi)" by blast
          moreover
          from ljnc obtain "lj" where "∃ lj. linearize j = Some lj ∧ ¬ (∃ bj. lj = Cst bj)" by blast
          ultimately have "linearize (Mult i j) = None"
            apply (simp add: measure_def inv_image_def)
            apply (case_tac "linearize i", auto)
            apply (case_tac a)
            apply (auto!)
            by (case_tac "lj",auto)+
          then have ?thesis by (simp!) }
        ultimately show ?thesis by blast
      qed
    qed  simp_all

    (* linearize, when successfull, preserves semantics *)
    lemma linearize_corr: "!! t'. linearize t = Some t' ==> I_intterm ats t = I_intterm ats t' "
    proof-
      fix t'
      assume lint: "linearize t = Some t'"
      show  "I_intterm ats t = I_intterm ats t'"
      proof-
        from lint have lt: "linearize t ≠ None" by simp
        then have "I_intterm ats t = I_intterm ats (the (linearize t))"
          by (rule_tac linearize_corr1[OF lt])
        with lint show ?thesis by simp
      qed
    qed

    (* tries to linearize a formula *)
    consts linform :: "QF => QF option"
    primrec
    "linform (Le it1 it2) =
      lift_bin(λx. λy. Le (lin_add(x,lin_neg y)) (Cst 0),linearize it1, linearize it2)"
    "linform (Eq it1 it2) =
      lift_bin(λx. λy. Eq (lin_add(x,lin_neg y)) (Cst 0),linearize it1, linearize it2)"
    "linform (Divides d t) =
      (case linearize d of
        None => None
       | Some ld => (case ld of
              Cst b =>
                   (if (b=0) then None
                   else
                    (case linearize t of
                     None => None
                   | Some lt => Some (Divides ld lt)))
             | _ => None))"
    "linform  T = Some T"
    "linform  F = Some F"
    "linform (NOT p) = lift_un NOT (linform p)"
    "linform (And p q)= lift_bin(λf. λg. And f g, linform p, linform q)"
    "linform (Or p q) = lift_bin(λf. λg. Or f g, linform p, linform q)"

    (* linearity of formulae *)
    consts islinform :: "QF => bool"
    recdef islinform "measure size"
    "islinform (Le it (Cst i)) = (i=0 ∧ islinintterm it )"
    "islinform (Eq it (Cst i)) = (i=0 ∧ islinintterm it)"
    "islinform (Divides (Cst d) t) = (d ≠ 0 ∧ islinintterm t)"
    "islinform  T = True"
    "islinform  F = True"
    "islinform (NOT (Divides (Cst d) t)) = (d ≠ 0 ∧ islinintterm t)"
    "islinform (NOT (Eq it (Cst i))) = (i=0 ∧ islinintterm it)"
    "islinform (And p q)= ((islinform p) ∧ (islinform q))"
    "islinform (Or p q) = ((islinform p) ∧ (islinform q))"
    "islinform p = False"

    (* linform preserves nnf, if successful *)
    lemma linform_nnf:
      assumes nnfp: "isnnf p"
      shows "!! p'. [|linform p = Some p'|] ==> isnnf p'"
    using nnfp
    proof (induct p rule: isnnf.induct, simp_all)
      case (goal1 a b p')
      show ?case
        using prems
        by (cases "linearize a", auto) (cases "linearize b", auto)
    next
      case (goal2 a b p')
      show ?case
        using prems
        by (cases "linearize a", auto) (cases "linearize b", auto)
    next
      case (goal3 d t p')
      show ?case
        using prems
        apply (cases "linearize d", auto)
        apply (case_tac "a",auto)
        apply (case_tac "int=0",auto)
        by (cases "linearize t",auto)
    next
      case (goal4 f g p') show ?case
        using prems
        by (cases "linform f", auto) (cases "linform g", auto)
    next
      case (goal5 f g p') show ?case
        using prems
        by (cases "linform f", auto) (cases "linform g", auto)
    next
      case (goal6 d t p') show ?case
        using prems
        apply (cases "linearize d", auto)
        apply (case_tac "a", auto)
        apply (case_tac "int = 0",auto)
        by (cases "linearize t", auto)
    next
      case (goal7 a b p')
      show ?case
        using prems
        by (cases "linearize a", auto) (cases "linearize b", auto)

    qed

    lemma linform_corr: "!! lp. [| isnnf p ; linform p = Some lp |] ==>
                         (qinterp ats p = qinterp ats lp)"
    proof (induct p rule: linform.induct)
      case (Le x y)
      show ?case
        using "Le.prems"
      proof-
        have "(∃ lx ly. linearize x = Some lx ∧ linearize y = Some ly) ∨
          (linearize x = None) ∨ (linearize y = None)"by auto
        moreover
        {
          assume linxy: "∃ lx ly. linearize x = Some lx ∧ linearize y = Some ly"
          from linxy obtain "lx" "ly"
            where lxly:"linearize x = Some lx ∧ linearize y = Some ly" by blast
          then
          have lxeqx: "I_intterm ats x = I_intterm ats lx"
            by (simp add: linearize_corr)
          from lxly have lxlin: "islinintterm lx"
            by (auto simp add: linearize_linear)
          from lxly have lyeqy: "I_intterm ats y = I_intterm ats ly"
            by (simp add: linearize_corr)
          from lxly have lylin: "islinintterm ly"
            by (auto simp add: linearize_linear)
          from "prems"
          have lpeqle: "lp =  (Le (lin_add(lx,lin_neg ly)) (Cst 0))"
            by auto
          moreover
          have lin1: "islinintterm (Cst 1)" by simp
          then
          have ?thesis
            using lxlin lylin lin1 lin_add_lin lin_neg_lin "prems" lxly lpeqle
            by (simp add: lin_add_corr lin_neg_corr lxeqx lyeqy)

        }

        moreover
        {
          assume "linearize x = None"
          have ?thesis using "prems" by simp
        }

        moreover
        {
          assume "linearize y = None"
          then have ?thesis using "prems"
            by (case_tac "linearize x", auto)
        }
        ultimately show ?thesis by blast
      qed

    next
      case (Eq x y)
      show ?case
        using "Eq.prems"
      proof-
        have "(∃ lx ly. linearize x = Some lx ∧ linearize y = Some ly) ∨
          (linearize x = None) ∨ (linearize y = None)"by auto
        moreover
        {
          assume linxy: "∃ lx ly. linearize x = Some lx ∧ linearize y = Some ly"
          from linxy obtain "lx" "ly"
            where lxly:"linearize x = Some lx ∧ linearize y = Some ly" by blast
          then
          have lxeqx: "I_intterm ats x = I_intterm ats lx"
            by (simp add: linearize_corr)
          from lxly have lxlin: "islinintterm lx"
            by (auto simp add: linearize_linear)
          from lxly have lyeqy: "I_intterm ats y = I_intterm ats ly"
            by (simp add: linearize_corr)
          from lxly have lylin: "islinintterm ly"
            by (auto simp add: linearize_linear)
          from "prems"
          have lpeqle: "lp =  (Eq (lin_add(lx,lin_neg ly)) (Cst 0))"
            by auto
          moreover
          have lin1: "islinintterm (Cst 1)" by simp
          then
          have ?thesis
            using lxlin lylin lin1 lin_add_lin lin_neg_lin "prems" lxly lpeqle
            by (simp add: lin_add_corr lin_neg_corr lxeqx lyeqy)

        }

        moreover
        {
          assume "linearize x = None"
          have ?thesis using "prems" by simp
        }

        moreover
        {
          assume "linearize y = None"
          then have ?thesis using "prems"
            by (case_tac "linearize x", auto)
        }
        ultimately show ?thesis by blast
      qed

    next
      case (Divides d t)
      show ?case
        using "Divides.prems"
        apply (case_tac "linearize d",auto)
        apply (case_tac a, auto)
        apply (case_tac "int = 0", auto)
        apply (case_tac "linearize t", auto)
        apply (simp add: linearize_corr)
        apply (case_tac a, auto)
        apply (case_tac "int = 0", auto)
        by (case_tac "linearize t", auto simp add: linearize_corr)
    next
      case (NOT f) show ?case
        using "prems"
      proof-
        have "(∃ lf. linform f = Some lf) ∨ (linform f = None)" by auto
        moreover
        {
          assume linf: "∃ lf. linform f = Some lf"
          from prems have "isnnf (NOT f)" by simp
          then have fnnf: "isnnf f" by (cases f) auto
          from linf obtain "lf" where lf: "linform f = Some lf" by blast
          then have "lp = NOT lf" using "prems" by auto
          with "NOT.prems" "NOT.hyps" lf fnnf
          have ?case by simp
        }
        moreover
        {
          assume "linform f = None"
          then
          have "linform (NOT f) = None" by simp
          then
          have ?thesis  using "NOT.prems" by simp
        }
        ultimately show ?thesis by blast
      qed
    next
      case (Or f g)
      show ?case using "Or.hyps"
      proof -
        have "((∃ lf. linform f = Some lf ) ∧ (∃ lg. linform g = Some lg)) ∨
          (linform f = None) ∨ (linform g = None)" by auto
        moreover
        {
          assume linf: "∃ lf. linform f = Some lf"
            and ling: "∃ lg. linform g = Some lg"
          from linf obtain "lf" where lf: "linform f = Some lf" by blast
          from ling obtain "lg" where lg: "linform g = Some lg" by blast
          from lf lg have "linform (Or f g) = Some (Or lf lg)" by simp
          then have "lp = Or lf lg" using lf lg "prems"  by simp
          with lf lg "prems" have ?thesis by simp
        }
        moreover
        {
          assume "linform f = None"
          then have ?thesis using "Or.prems"  by auto
        }
        moreover
        {
          assume "linform g = None"
          then have ?thesis using "Or.prems"  by (case_tac "linform f", auto)

        }
        ultimately show ?thesis by blast
      qed
    next
      case (And f g)
      show ?case using "And.hyps"
      proof -
        have "((∃ lf. linform f = Some lf ) ∧ (∃ lg. linform g = Some lg)) ∨
          (linform f = None) ∨ (linform g = None)" by auto
        moreover
        {
          assume linf: "∃ lf. linform f = Some lf"
            and ling: "∃ lg. linform g = Some lg"
          from linf obtain "lf" where lf: "linform f = Some lf" by blast
          from ling obtain "lg" where lg: "linform g = Some lg" by blast
          from lf lg have "linform (And f g) = Some (And lf lg)" by simp
          then have "lp = And lf lg" using lf lg "prems"  by simp
          with lf lg "prems" have ?thesis by simp
        }
        moreover
        {
          assume "linform f = None"
          then have ?thesis using "And.prems"  by auto
        }
        moreover
        {
          assume "linform g = None"
          then have ?thesis using "And.prems"  by (case_tac "linform f", auto)

        }
        ultimately show ?thesis by blast
      qed

    qed simp_all

    (* the result of linform is a linear formula *)
    lemma linform_lin: "!! lp. [| isnnf p ; linform p = Some lp|] ==> islinform lp"
    proof (induct p rule: linform.induct)
       case (Le x y)
      have "((∃ lx. linearize x = Some lx) ∧ (∃ ly. linearize y = Some ly)) ∨
        (linearize x = None) ∨ (linearize y = None) " by clarsimp
      moreover
      {
        assume linx: "∃ lx. linearize x = Some lx"
          and liny: "∃ ly. linearize y = Some ly"
        from linx obtain "lx" where lx: "linearize x = Some lx" by blast
        from liny obtain "ly" where ly: "linearize y = Some ly" by blast
        from lx have lxlin: "islinintterm lx" by (simp add: linearize_linear)
        from ly have lylin: "islinintterm ly" by (simp add: linearize_linear)
        have lin1:"islinintterm (Cst 1)" by simp
        have lin0: "islinintterm (Cst 0)" by simp
        from "prems"  have "lp = Le (lin_add(lx,lin_neg ly)) (Cst 0)"
          by auto
        with lin0 lin1 lxlin lylin "prems"
        have ?case by (simp add: lin_add_lin lin_neg_lin)

      }

      moreover
      {
        assume "linearize x = None"
        then have ?case using "prems" by simp
      }
      moreover
      {
        assume "linearize y = None"
        then have ?case using "prems" by (case_tac "linearize x",simp_all)
      }
      ultimately show ?case by blast
    next
       case (Eq x y)
      have "((∃ lx. linearize x = Some lx) ∧ (∃ ly. linearize y = Some ly)) ∨
        (linearize x = None) ∨ (linearize y = None) " by clarsimp
      moreover
      {
        assume linx: "∃ lx. linearize x = Some lx"
          and liny: "∃ ly. linearize y = Some ly"
        from linx obtain "lx" where lx: "linearize x = Some lx" by blast
        from liny obtain "ly" where ly: "linearize y = Some ly" by blast
        from lx have lxlin: "islinintterm lx" by (simp add: linearize_linear)
        from ly have lylin: "islinintterm ly" by (simp add: linearize_linear)
        have lin1:"islinintterm (Cst 1)" by simp
        have lin0: "islinintterm (Cst 0)" by simp
        from "prems"  have "lp = Eq (lin_add(lx,lin_neg ly)) (Cst 0)"
          by auto
        with lin0 lin1 lxlin lylin "prems"
        have ?case by (simp add: lin_add_lin lin_neg_lin)

      }

      moreover
      {
        assume "linearize x = None"
        then have ?case using "prems" by simp
      }
      moreover
      {
        assume "linearize y = None"
        then have ?case using "prems" by (case_tac "linearize x",simp_all)
      }
      ultimately show ?case by blast
    next
       case (Divides d t)
       show ?case
         using prems
         apply (case_tac "linearize d", auto)
         apply (case_tac a, auto)
         apply (case_tac "int = 0", auto)

         by (case_tac "linearize t",auto simp add: linearize_linear)
    next
      case (Or f g)
     show ?case using "Or.hyps"
      proof -
        have "((∃ lf. linform f = Some lf ) ∧ (∃ lg. linform g = Some lg)) ∨
          (linform f = None) ∨ (linform g = None)" by auto
        moreover
        {
          assume linf: "∃ lf. linform f = Some lf"
            and ling: "∃ lg. linform g = Some lg"
          from linf obtain "lf" where lf: "linform f = Some lf" by blast
          from ling obtain "lg" where lg: "linform g = Some lg" by blast
          from lf lg have "linform (Or f g) = Some (Or lf lg)" by simp
          then have "lp = Or lf lg" using lf lg "prems"  by simp
          with lf lg "prems" have ?thesis by simp
        }
        moreover
        {
          assume "linform f = None"
          then have ?thesis using "Or.prems"  by auto
        }
        moreover
        {
          assume "linform g = None"
          then have ?thesis using "Or.prems"  by (case_tac "linform f", auto)

        }
        ultimately show ?thesis by blast
      qed
    next
      case (And f g)
      show ?case using "And.hyps"
      proof -
        have "((∃ lf. linform f = Some lf ) ∧ (∃ lg. linform g = Some lg)) ∨
          (linform f = None) ∨ (linform g = None)" by auto
        moreover
        {
          assume linf: "∃ lf. linform f = Some lf"
            and ling: "∃ lg. linform g = Some lg"
          from linf obtain "lf" where lf: "linform f = Some lf" by blast
          from ling obtain "lg" where lg: "linform g = Some lg" by blast
          from lf lg have "linform (And f g) = Some (And lf lg)" by simp
          then have "lp = And lf lg" using lf lg "prems"  by simp
          with lf lg "prems" have ?thesis by simp
        }
        moreover
        {
          assume "linform f = None"
          then have ?thesis using "And.prems"  by auto
        }
        moreover
        {
          assume "linform g = None"
          then have ?thesis using "And.prems"  by (case_tac "linform f", auto)

        }
        ultimately show ?thesis by blast
      qed
    next
      case (NOT f) show ?case
        using "prems"
      proof-
        have "(∃ lf. linform f = Some lf) ∨ (linform f = None)" by auto
        moreover
        {
          assume linf: "∃ lf. linform f = Some lf"
          from prems have "isnnf (NOT f)" by simp
          then have fnnf: "isnnf f" by (cases f) auto
          from linf obtain "lf" where lf: "linform f = Some lf" by blast
          then have "lp = NOT lf" using "prems" by auto
          with "NOT.prems" "NOT.hyps" lf fnnf
          have ?thesis
            using fnnf
            apply (cases f, auto)
            prefer 2
            apply (case_tac "linearize intterm1",auto)
            apply (case_tac a, auto)
            apply (case_tac "int = 0", auto)
            apply (case_tac "linearize intterm2")
            apply (auto simp add: linearize_linear)
            apply (case_tac "linearize intterm1",auto)
            by (case_tac "linearize intterm2")
          (auto simp add: linearize_linear lin_add_lin lin_neg_lin)
        }
        moreover
        {
          assume "linform f = None"
          then
          have "linform (NOT f) = None" by simp
          then
          have ?thesis  using "NOT.prems" by simp
        }
        ultimately show ?thesis by blast
      qed
    qed (simp_all)

    (* linform, if successfull, preserves quantifier freeness *)
    lemma linform_isnnf: "islinform p ==> isnnf p"
    by (induct p rule: islinform.induct) auto

    lemma linform_isqfree: "islinform p ==> isqfree p"
    using linform_isnnf nnf_isqfree by simp

    lemma linform_qfree: "!! p'. [| isnnf p ; linform p = Some p'|] ==> isqfree p'"
    using linform_isqfree linform_lin
    by simp

    (* Definitions and lemmas about gcd and lcm *)
    constdefs lcm :: "nat × nat => nat"
      "lcm ≡ (λ(m,n). m*n div gcd(m,n))"

    constdefs ilcm :: "int => int => int"
      "ilcm ≡ λi.λj. int (lcm(nat(abs i),nat(abs j)))"

    (* ilcm_dvd12 are needed later *)
    lemma lcm_dvd1:
      assumes mpos: " m >0"
      and npos: "n>0"
      shows "m dvd (lcm(m,n))"
    proof-
      have "gcd(m,n) dvd n" by simp
      then obtain "k" where "n = gcd(m,n) * k" using dvd_def by auto
      then have "m*n div gcd(m,n) = m*(gcd(m,n)*k) div gcd(m,n)" by (simp add: mult_ac)
      also have "… = m*k" using mpos npos gcd_zero by simp
      finally show ?thesis by (simp add: lcm_def)
    qed

    lemma lcm_dvd2:
      assumes mpos: " m >0"
      and npos: "n>0"
      shows "n dvd (lcm(m,n))"
    proof-
      have "gcd(m,n) dvd m" by simp
      then obtain "k" where "m = gcd(m,n) * k" using dvd_def by auto
      then have "m*n div gcd(m,n) = (gcd(m,n)*k)*n div gcd(m,n)" by (simp add: mult_ac)
      also have "… = n*k" using mpos npos gcd_zero by simp
      finally show ?thesis by (simp add: lcm_def)
    qed

    lemma ilcm_dvd1:
    assumes anz: "a ≠ 0"
      and bnz: "b ≠ 0"
      shows "a dvd (ilcm a b)"
    proof-
      let ?na = "nat (abs a)"
      let ?nb = "nat (abs b)"
      have nap: "?na >0" using anz by simp
      have nbp: "?nb >0" using bnz by simp
      from nap nbp have "?na dvd lcm(?na,?nb)" using lcm_dvd1 by simp
      thus ?thesis by (simp add: ilcm_def dvd_int_iff)
    qed

    lemma ilcm_dvd2:
    assumes anz: "a ≠ 0"
      and bnz: "b ≠ 0"
      shows "b dvd (ilcm a b)"
    proof-
      let ?na = "nat (abs a)"
      let ?nb = "nat (abs b)"
      have nap: "?na >0" using anz by simp
      have nbp: "?nb >0" using bnz by simp
      from nap nbp have "?nb dvd lcm(?na,?nb)" using lcm_dvd2 by simp
      thus ?thesis by (simp add: ilcm_def dvd_int_iff)
    qed

    lemma zdvd_self_abs1: "(d::int) dvd (abs d)"
    by (case_tac "d <0", simp_all)

    lemma zdvd_self_abs2: "(abs (d::int)) dvd d"
    by (case_tac "d<0", simp_all)

    (* lcm a b is positive for positive a and b *)

    lemma lcm_pos:
      assumes mpos: "m > 0"
      and npos: "n>0"
      shows "lcm (m,n) > 0"

    proof(rule ccontr, simp add: lcm_def gcd_zero)
    assume h:"m*n div gcd(m,n) = 0"
    from mpos npos have "gcd (m,n) ≠ 0" using gcd_zero by simp
    hence gcdp: "gcd(m,n) > 0" by simp
    with h
    have "m*n < gcd(m,n)"
      by (cases "m * n < gcd (m, n)") (auto simp add: div_if[OF gcdp, where m="m*n"])
    moreover
    have "gcd(m,n) dvd m" by simp
     with mpos dvd_imp_le have t1:"gcd(m,n) ≤ m" by simp
     with npos have t1:"gcd(m,n)*n ≤ m*n" by simp
     have "gcd(m,n) ≤ gcd(m,n)*n" using npos by simp
     with t1 have "gcd(m,n) ≤ m*n" by arith
    ultimately show "False" by simp
    qed

    lemma ilcm_pos:
      assumes apos: " 0 < a"
      and bpos: "0 < b"
      shows "0 < ilcm  a b"
    proof-
      let ?na = "nat (abs a)"
      let ?nb = "nat (abs b)"
      have nap: "?na >0" using apos by simp
      have nbp: "?nb >0" using bpos by simp
      have "0 < lcm (?na,?nb)" by (rule lcm_pos[OF nap nbp])
      thus ?thesis by (simp add: ilcm_def)
    qed

    (* fomlcm computes the lcm of all c, where c is the coeffitient of Var 0 *)
    consts formlcm :: "QF => int"
    recdef formlcm "measure size"
    "formlcm (Le (Add (Mult (Cst c) (Var 0)) r) (Cst i)) = abs c "
    "formlcm (Eq (Add (Mult (Cst c) (Var 0)) r) (Cst i)) = abs c "
    "formlcm (Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) = abs c"
    "formlcm (NOT p) = formlcm p"
    "formlcm (And p q)= ilcm (formlcm p) (formlcm q)"
    "formlcm (Or p q) = ilcm (formlcm p) (formlcm q)"
    "formlcm p = 1"

    (* the property that formlcm should fullfill *)
    consts divideallc:: "int × QF => bool"
    recdef divideallc "measure (λ(i,p). size p)"
    "divideallc (l,Le (Add (Mult (Cst c) (Var 0)) r) (Cst i)) = (c dvd l)"
    "divideallc (l,Eq (Add (Mult (Cst c) (Var 0)) r) (Cst i)) = (c dvd l)"
    "divideallc(l,Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) = (c dvd l)"
    "divideallc (l,NOT p) = divideallc(l,p)"
    "divideallc (l,And p q) = (divideallc (l,p) ∧ divideallc (l,q))"
    "divideallc (l,Or p q) = (divideallc (l,p) ∧ divideallc (l,q))"
    "divideallc p = True"

    (* formlcm retuns a positive integer *)
    lemma formlcm_pos:
      assumes linp: "islinform p"
      shows "0 < formlcm p"
    using linp
    proof (induct p rule: formlcm.induct, simp_all add: ilcm_pos)
      case (goal1 c r i)
      have "i=0 ∨ i ≠ 0" by simp
      moreover
      {
        assume "i ≠ 0" then have ?case using prems by simp
      }
      moreover
      {
        assume iz: "i = 0"
        then have "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
        then have "c≠0"
          using prems
          by (simp add: islininttermc0r[where c="c" and n="0" and r="r"])
        then have ?case by simp
      }
      ultimately
      show ?case by blast
    next
      case (goal2 c r i)
      have "i=0 ∨ i ≠ 0" by simp
      moreover
      {
        assume "i ≠ 0" then have ?case using prems by simp
      }
      moreover
      {
        assume iz: "i = 0"
        then have "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
        then have "c≠0"
          using prems
          by (simp add: islininttermc0r[where c="c" and n="0" and r="r"])
        then have ?case by simp
      }
      ultimately
      show ?case by blast

    next
      case (goal3 d c r)
      show ?case using prems by (simp add: islininttermc0r[where c="c" and n="0" and r="r"])
    next
      case (goal4 f)
      show ?case using prems
        by (cases f,auto) (case_tac "intterm2", auto,case_tac "intterm1", auto)
    qed

    lemma divideallc_mono: "!! c. [| divideallc(c,p) ; c dvd d|] ==> divideallc (d,p)"
    proof (induct d p rule: divideallc.induct, simp_all)
      case (goal1 l a b) show ?case by ( rule zdvd_trans [where m="a" and n="b" and k="l"])
    next
      case (goal2 l a b) show ?case by ( rule zdvd_trans [where m="a" and n="b" and k="l"])
    next
     case (goal3 l a b) show ?case by ( rule zdvd_trans [where m="a" and n="b" and k="l"])
    next
      case (goal4 l f g k)
      have  "divideallc (l,g)" using prems by clarsimp
      moreover have "divideallc (l,f)" using prems by clarsimp
      ultimately
      show ?case  by simp
    next
      case (goal5 l f g k)
      have  "divideallc (l,g)" using prems by clarsimp
      moreover have "divideallc (l,f)" using prems by clarsimp
      ultimately
      show ?case  by simp

    qed

    (* fomlcm retuns a number all coeffitients of Var 0 divide *)

    lemma formlcm_divideallc:
      assumes linp: "islinform p"
      shows "divideallc(formlcm p, p)"
    using linp
    proof (induct p rule: formlcm.induct, simp_all add: zdvd_self_abs1)
      case (goal1 f)
      show ?case using prems
        by (cases f,auto) (case_tac "intterm2", auto, case_tac "intterm1",auto)
    next
      case (goal2 f g)
      have "formlcm f >0" using formlcm_pos prems by simp
        hence "formlcm f ≠ 0" by simp
      moreover have "formlcm g > 0" using formlcm_pos prems by simp
      hence "formlcm g ≠ 0" by simp
      ultimately
      show ?case using prems formlcm_pos
         by (simp add: ilcm_dvd1 ilcm_dvd2
           divideallc_mono[where c="formlcm f" and d="ilcm (formlcm f) (formlcm g)"]
           divideallc_mono[where c="formlcm g" and d="ilcm (formlcm f) (formlcm g)"])
    next
      case (goal3 f g)
      have "formlcm f >0" using formlcm_pos prems by simp
        hence "formlcm f ≠ 0" by simp
      moreover have "formlcm g > 0" using formlcm_pos prems by simp
      hence "formlcm g ≠ 0" by simp
      ultimately
      show ?case using prems
        by (simp add: ilcm_dvd1 ilcm_dvd2
          divideallc_mono[where c="formlcm f" and d="ilcm (formlcm f) (formlcm g)"]
          divideallc_mono[where c="formlcm g" and d="ilcm (formlcm f) (formlcm g)"])
    qed

    (* adjustcoeff transforms the formula given an l , look at correctness thm*)
    consts adjustcoeff :: "int × QF => QF"
    recdef adjustcoeff "measure (λ(l,p). size p)"
    "adjustcoeff (l,(Le (Add (Mult (Cst c) (Var 0)) r) (Cst i))) =
      (if c≤0 then
      Le (Add (Mult (Cst -1) (Var 0)) (lin_mul (- (l div c), r))) (Cst (0::int))
      else
      Le (Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r))) (Cst (0::int)))"
    "adjustcoeff (l,(Eq (Add (Mult (Cst c) (Var 0)) r) (Cst i))) =
      (Eq (Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r))) (Cst (0::int)))"
    "adjustcoeff (l,Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) =
      Divides (Cst ((l div c) * d))
      (Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r)))"
    "adjustcoeff (l,NOT (Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r))) = NOT (Divides (Cst ((l div c) * d))
      (Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r))))"
    "adjustcoeff (l,(NOT(Eq (Add (Mult (Cst c) (Var 0)) r) (Cst i)))) =
      (NOT(Eq (Add (Mult (Cst 1) (Var 0)) (lin_mul (l div c, r))) (Cst (0::int))))"
    "adjustcoeff (l,And p q) = And (adjustcoeff (l,p)) (adjustcoeff(l,q))"
    "adjustcoeff (l,Or p q) = Or (adjustcoeff (l,p)) (adjustcoeff(l,q))"
    "adjustcoeff (l,p) = p"

    (* unitycoeff expects a quantifier free formula an transforms it to an equivalent formula where the bound variable occurs only with coeffitient 1  or -1 *)
    constdefs unitycoeff :: "QF => QF"
      "unitycoeff p ==
      (let l = formlcm p;
           p' = adjustcoeff (l,p)
       in (if l=1 then p' else
          (And (Divides (Cst l) (Add (Mult (Cst 1) (Var 0)) (Cst 0))) p')))"

    (* what is a unified formula *)
    consts isunified :: "QF => bool"
    recdef isunified "measure size"
    "isunified (Le (Add (Mult (Cst i) (Var 0)) r) (Cst z)) =
      ((abs i) = 1  ∧ (islinform(Le (Add (Mult (Cst i) (Var 0)) r) (Cst z))))"
    "isunified (Eq (Add (Mult (Cst i) (Var 0)) r) (Cst z)) =
      ((abs i) = 1  ∧ (islinform(Le (Add (Mult (Cst i) (Var 0)) r) (Cst z))))"
    "isunified (NOT(Eq (Add (Mult (Cst i) (Var 0)) r) (Cst z))) =
      ((abs i) = 1  ∧ (islinform(Le (Add (Mult (Cst i) (Var 0)) r) (Cst z))))"
    "isunified (Divides (Cst d) (Add (Mult (Cst i) (Var 0)) r)) =
      ((abs i) = 1 ∧ (islinform(Divides (Cst d) (Add (Mult (Cst i) (Var 0)) r))))"
    "isunified (NOT(Divides (Cst d) (Add (Mult (Cst i) (Var 0)) r))) =
      ((abs i) = 1 ∧ (islinform(NOT(Divides (Cst d) (Add (Mult (Cst i) (Var 0)) r)))))"
    "isunified (And p q) = (isunified p ∧ isunified q)"
    "isunified (Or p q) = (isunified p ∧ isunified q)"
    "isunified p = islinform p"

    lemma unified_islinform: "isunified p ==> islinform p"
    by (induct p rule: isunified.induct) auto

    lemma adjustcoeff_lenpos:
      "0 < n ==> adjustcoeff (l, Le (Add (Mult (Cst i) (Var n)) r) (Cst c)) =
        Le (Add (Mult (Cst i) (Var n)) r) (Cst c)"
    by (cases n, auto)

    lemma adjustcoeff_eqnpos:
      "0 < n ==> adjustcoeff (l, Eq (Add (Mult (Cst i) (Var n)) r) (Cst c)) =
        Eq (Add (Mult (Cst i) (Var n)) r) (Cst c)"
    by (cases n, auto)

    (* Properties of adjustcoeff and unitycoeff *)

    (* Some simple lemmas used afterwards *)
    lemma zmult_zle_mono: "(i::int) ≤ j ==> 0 ≤ k ==> k * i ≤ k * j"
      apply (erule order_le_less [THEN iffD1, THEN disjE, of "0::int"])
      apply (erule order_le_less [THEN iffD1, THEN disjE])
      apply (rule order_less_imp_le)
      apply (rule zmult_zless_mono2)
      apply simp_all
      done

    lemma zmult_zle_mono_eq:
      assumes kpos: "0 < k"
      shows "((i::int) ≤ j) = (k*i ≤ k*j)" (is "?P = ?Q")
    proof
      assume P: ?P
      from kpos have kge0: "0 ≤ k" by simp
      show ?Q
        by (rule zmult_zle_mono[OF P kge0])
    next
      assume ?Q
      then have "k*i - k*j ≤ 0" by simp
      then have le1: "k*(i-j) ≤ k*0"
        by (simp add: zdiff_zmult_distrib2)
      have "i -j ≤ 0"
        by (rule mult_left_le_imp_le[OF le1 kpos])
      then
      show ?P by simp
    qed

    lemma adjustcoeff_le_corr:
      assumes lpos: "0 < l"
      and ipos: "0 < (i::int)"
      and dvd: "i dvd l"
      shows "(i*x + r ≤ 0) = (l*x + ((l div i)*r) ≤ 0)"
    proof-
      from lpos ipos have ilel: "i≤l" by (simp add: zdvd_imp_le [OF dvd lpos])
      from ipos have inz: "i ≠ 0" by simp
      have "i div i≤ l div i"
        by (simp add: zdiv_mono1[OF ilel ipos])
      then have ldivipos:"0 < l div i"
        by (simp add: zdiv_self[OF inz])

      from dvd have "∃i'. i*i' = l" by (auto simp add: dvd_def)
      then obtain "i'" where ii'eql: "i*i' = l" by blast
      have "(i * x + r ≤ 0) = (l div i * (i * x + r) ≤ l div i * 0)"
        by (rule zmult_zle_mono_eq[OF ldivipos, where i="i*x + r" and j="0"])
      also
      have "(l div i * (i * x + r) ≤ l div i * 0) = ((l div i * i) * x + ((l div i)*r) ≤ 0)"
        by (simp add: mult_ac)
      also have "((l div i * i) * x + ((l div i)*r) ≤ 0) = (l*x + ((l div i)*r) ≤ 0)"
        using sym[OF ii'eql] inz
        by (simp add: zmult_ac)
      finally
      show ?thesis
        by simp
    qed

    lemma adjustcoeff_le_corr2:
      assumes lpos: "0 < l"
      and ineg: "(i::int) < 0"
      and dvd: "i dvd l"
      shows "(i*x + r ≤ 0) = ((-l)*x + ((-(l div i))*r) ≤ 0)"
    proof-
      from dvd have midvdl: "-i dvd l" by simp
      from ineg have mipos: "0 < -i" by simp
      from lpos ineg have milel: "-i≤l" by (simp add: zdvd_imp_le [OF midvdl lpos])
      from ineg have inz: "i ≠ 0" by simp
      have "l div i≤ -i div i"
        by (simp add: zdiv_mono1_neg[OF milel ineg])
      then have "l div i ≤ -1"
        apply (simp add: zdiv_zminus1_eq_if[OF inz, where a="i"])
        by (simp add: zdiv_self[OF inz])
      then have ldivineg: "l div i < 0" by simp
      then have mldivipos: "0 < - (l div i)" by simp

      from dvd have "∃i'. i*i' = l" by (auto simp add: dvd_def)
      then obtain "i'" where ii'eql: "i*i' = l" by blast
      have "(i * x + r ≤ 0) = (- (l div i) * (i * x + r) ≤ - (l div i) * 0)"
        by (rule zmult_zle_mono_eq[OF mldivipos, where i="i*x + r" and j="0"])
      also
      have "(- (l div i) * (i * x + r) ≤ - (l div i) * 0) = (-((l div i) * i) * x ≤ (l div i)*r)"
        by (simp add: mult_ac)
      also have " (-((l div i) * i) * x ≤ (l div i)*r) = (- (l*x) ≤ (l div i)*r)"
        using sym[OF ii'eql] inz
        by (simp add: zmult_ac)
      finally
      show ?thesis
        by simp
    qed

    (* FIXME : Move this theorem above, it simplifies the 2 theorems above : adjustcoeff_le_corr1,2 *)
    lemma dvd_div_pos:
      assumes bpos: "0 < (b::int)"
      and anz: "a≠0"
      and dvd: "a dvd b"
      shows "(b div a)*a = b"
    proof-
      from anz have "0 < a ∨ a < 0" by arith
      moreover
      {
        assume apos: "0 < a"
        from bpos apos have aleb: "a≤b" by (simp add: zdvd_imp_le [OF dvd bpos])
        have "a div a≤ b div a"
          by (simp add: zdiv_mono1[OF aleb apos])
        then have bdivapos:"0 < b div a"
          by (simp add: zdiv_self[OF anz])

        from dvd have "∃a'. a*a' = b" by (auto simp add: dvd_def)
        then obtain "a'" where aa'eqb: "a*a' = b" by blast
        then have ?thesis  using anz sym[OF aa'eqb] by simp

      }
      moreover
      {
        assume aneg: "a < 0"
        from dvd have midvdb: "-a dvd b" by simp
        from aneg have mapos: "0 < -a" by simp
        from bpos aneg have maleb: "-a≤b" by (simp add: zdvd_imp_le [OF midvdb bpos])
        from aneg have anz: "a ≠ 0" by simp
        have "b div a≤ -a div a"
          by (simp add: zdiv_mono1_neg[OF maleb aneg])
        then have "b div a ≤ -1"
          apply (simp add: zdiv_zminus1_eq_if[OF anz, where a="a"])
          by (simp add: zdiv_self[OF anz])
        then have bdivaneg: "b div a < 0" by simp
        then have mbdivapos: "0 < - (b div a)" by simp

        from dvd have "∃a'. a*a' = b" by (auto simp add: dvd_def)
        then obtain "a'" where aa'eqb: "a*a' = b" by blast
        then have ?thesis using anz sym[OF aa'eqb] by (simp)
      }
      ultimately show ?thesis by blast
    qed

    lemma adjustcoeff_eq_corr:
      assumes lpos: "(0::int) < l"
      and inz: "i ≠ 0"
      and dvd: "i dvd l"
      shows "(i*x + r = 0) = (l*x + ((l div i)*r) = 0)"
    proof-
      have ldvdii: "(l div i)*i = l" by (rule dvd_div_pos[OF lpos inz dvd])
      have ldivinz: "l div i ≠ 0" using inz ldvdii lpos by auto
      have "(i*x + r = 0) = ((l div i)*(i*x + r) = (l div i)*0)"
        using ldivinz by arith
      also have "… = (((l div i)*i)*x + (l div i)*r = 0)"
        by (simp add: zmult_ac)
      finally show ?thesis using ldvdii by simp
    qed

    (* Correctness theorem for adjustcoeff *)
    lemma adjustcoeff_corr:
      assumes linp: "islinform p"
      and alldvd: "divideallc (l,p)"
      and lpos: "0 < l"
      shows "qinterp (a#ats) p = qinterp ((a*l)#ats) (adjustcoeff(l, p))"
    using linp alldvd
    proof (induct p rule: islinform.induct,simp_all)
      case (goal1 t c)
      from prems have cz: "c=0" by simp
        then have ?case
          using prems
        proof(induct t rule: islinintterm.induct)
          case (2 i n i') show ?case using prems
            proof-
              from prems have "i≠0" by simp
              then
              have "(n=0 ∧ i < 0) ∨ (n=0 ∧ i > 0) ∨ n≠0" by arith
              moreover
              {
                assume "n≠0" then have ?thesis
                  by (simp add: nth_pos2 adjustcoeff_lenpos)
              }
              moreover
              {
                assume nz: "n=0"
                  and ipos: "0 < i"
                from prems nz have idvdl: "i dvd l" by simp
                have "(i*a + i' ≤ 0) = (l*a+ ((l div i)*i') ≤ 0)"
                  by (rule adjustcoeff_le_corr[OF lpos ipos idvdl])
                then
                have ?thesis using prems by (simp add: mult_ac)
              }
              moreover
              {
                assume nz: "n=0"
                  and ineg: "i < 0"
                from prems nz have idvdl: "i dvd l" by simp
                have "(i*a+i' ≤ 0) = (-l*a + (-(l div i) * i') ≤ 0)"
                  by (rule adjustcoeff_le_corr2[OF lpos ineg idvdl])
                then
                have ?thesis using prems
                  by (simp add: zmult_ac)
              }
              ultimately show ?thesis by blast
            qed
          next
            case (3 i n i' n' r) show ?case  using prems
            proof-
              from prems
              have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)"
                by simp
              then
              have "islint (Add (Mult (Cst i') (Var n')) (r))"
                by (simp add: islinintterm_eq_islint)
              then have linr: "islintn(Suc n',r)"
                by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def)
              from lininrp have linr2: "islinintterm r"
                by (simp add: islinintterm_subt[OF lininrp])
              from prems have "n < n'" by simp
              then have nppos: "0 < n'" by simp
              from prems have "i≠0" by simp
              then
              have "(n=0 ∧ i < 0) ∨ (n=0 ∧ i > 0) ∨ n≠0" by arith
              moreover
              {
                assume nnz: "n≠0"
                from linr have ?thesis using nppos nnz intterm_novar0[OF lininrp] prems
                  apply (simp add: adjustcoeff_lenpos linterm_novar0[OF linr, where x="a" and y="a*l"])
                  by (simp add: nth_pos2)

              }
              moreover
              {
                assume nz: "n=0"
                  and ipos: "0 < i"
                from prems nz have idvdl: "i dvd l" by simp
                have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) ≤ 0) =
                  (l * a + l div i * (i' * (a # ats) ! n' + I_intterm (a # ats) r) ≤ 0)"
                  by (rule adjustcoeff_le_corr[OF lpos ipos idvdl])
                then
                have ?thesis using prems linr linr2
                  by (simp add: mult_ac nth_pos2 lin_mul_corr
                    linterm_novar0[OF linr, where x="a" and y="a*l"])
              }
              moreover
              {
                assume nz: "n=0"
                  and ineg: "i < 0"
                from prems nz have idvdl: "i dvd l" by simp
                have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) ≤ 0) =
                  (- l * a + - (l div i) * (i' * (a # ats) ! n' + I_intterm (a # ats) r) ≤ 0)"
                  by (rule adjustcoeff_le_corr2[OF lpos ineg idvdl, where  x="a" and r="(i'* (a#ats) ! n' + I_intterm (a#ats) r )"])
                then
                have ?thesis using prems linr linr2
                  by (simp add: zmult_ac nth_pos2 lin_mul_corr
                    linterm_novar0[OF linr, where x="a" and y="a*l"] )
              }
              ultimately show ?thesis by blast
            qed
        qed simp_all
        then show ?case by simp

    next
      case (goal2 t c)
      from prems have cz: "c=0" by simp
        then have ?case
          using prems
        proof(induct t rule: islinintterm.induct)
          case (2 i n i') show ?case using prems
            proof-
              from prems have inz: "i≠0" by simp
              then
              have "n=0 ∨ n≠0" by arith
              moreover
              {
                assume "n≠0" then have ?thesis
                  by (simp add: nth_pos2 adjustcoeff_eqnpos)
              }
              moreover
              {
                assume nz: "n=0"
                from prems nz have idvdl: "i dvd l" by simp
                have "(i*a + i' = 0) = (l*a+ ((l div i)*i') = 0)"
                  by (rule adjustcoeff_eq_corr[OF lpos inz idvdl])
                then
                have ?thesis using prems by (simp add: mult_ac)
              }
              ultimately show ?thesis by blast
            qed
          next
            case (3 i n i' n' r) show ?case  using prems
            proof-
              from prems
              have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)"
                by simp
              then
              have "islint (Add (Mult (Cst i') (Var n')) (r))"
                by (simp add: islinintterm_eq_islint)
              then have linr: "islintn(Suc n',r)"
                by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def)
              from lininrp have linr2: "islinintterm r"
                by (simp add: islinintterm_subt[OF lininrp])
              from prems have "n < n'" by simp
              then have nppos: "0 < n'" by simp
              from prems have "i≠0" by simp
              then
              have "n=0 ∨ n≠0" by arith
              moreover
              {
                assume nnz: "n≠0"
                from linr have ?thesis using nppos nnz intterm_novar0[OF lininrp] prems
                  apply (simp add: adjustcoeff_eqnpos linterm_novar0[OF linr, where x="a" and y="a*l"])
                  by (simp add: nth_pos2)

              }
              moreover
              {
                assume nz: "n=0"
                from prems have inz: "i ≠ 0" by auto
                from prems nz have idvdl: "i dvd l" by simp
                have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0) =
                  (l * a + l div i * (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0)"
                  by (rule adjustcoeff_eq_corr[OF lpos inz idvdl])
                then
                have ?thesis using prems linr linr2
                  by (simp add: mult_ac nth_pos2 lin_mul_corr
                    linterm_novar0[OF linr, where x="a" and y="a*l"])
              }
              ultimately show ?thesis by blast
            qed
        qed simp_all
        then show ?case by simp

    next
      case (goal3 d t) show ?case
        using prems
        proof (induct t rule: islinintterm.induct)
          case (2 i n i')
          have "n=0 ∨ (∃m. (n = Suc m))" by arith
          moreover
          {
            assume "∃m. n = Suc m"
            then have ?case using prems  by auto
          }
          moreover
          {
            assume nz: "n=0"
            from prems have inz: "i≠0" by simp
            from prems have idvdl: "i dvd l" by simp
            have ldiviieql: "l div i * i = l" by (rule dvd_div_pos[OF lpos inz idvdl])
            with lpos have ldivinz: "0 ≠ l div i" by auto

            then have ?case using prems
              apply simp
              apply (simp add:
                ac_dvd_eq[OF ldivinz, where m="d" and c="i" and n="a" and t="i'"]
                ldiviieql)
              by (simp add: zmult_commute)
          }
          ultimately show ?case by blast

        next
          case (3 i n i' n' r)
          from prems
          have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)"
            by simp
          then
          have "islint (Add (Mult (Cst i') (Var n')) (r))"
            by (simp add: islinintterm_eq_islint)
          then have linr: "islintn(Suc n',r)"
            by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def)
          from lininrp have linr2: "islinintterm r"
            by (simp add: islinintterm_subt[OF lininrp])
          from prems have "n < n'" by simp
          then have nppos: "0 < n'" by simp
          from prems have inz: "i≠0" by simp

          have "n=0 ∨ (∃m. (n = Suc m))" by arith
          moreover
          {
            assume "∃m. n = Suc m"
            then have npos: "0 < n" by arith
            have ?case using nppos intterm_novar0[OF lininrp] prems
              apply (auto simp add: linterm_novar0[OF linr, where x="a" and y="a*l"])
              by (simp_all add: nth_pos2)
          }
          moreover
          {
            assume nz: "n=0"
            from prems have idvdl: "i dvd l" by simp
            have ldiviieql: "l div i * i = l" by (rule dvd_div_pos[OF lpos inz idvdl])
            with lpos have ldivinz: "0 ≠ l div i" by auto

            then have ?case using prems linr2 linr
              apply (simp add: nth_pos2 lin_mul_corr linterm_novar0)

              apply (simp add: ac_dvd_eq[OF ldivinz, where m="d" and c="i" and n="a" and t="(i' * ats ! (n' - Suc 0) + I_intterm (a # ats) r)"] ldiviieql)
              by (simp add: zmult_ac linterm_novar0[OF linr, where x="a" and y="a*l"])
          }
          ultimately show ?case by blast

        qed simp_all
    next
      case (goal4 d t) show ?case
        using prems
        proof (induct t rule: islinintterm.induct)
          case (2 i n i')
          have "n=0 ∨ (∃m. (n = Suc m))" by arith
          moreover
          {
            assume "∃m. n = Suc m"
            then have ?case using prems  by auto
          }
          moreover
          {
            assume nz: "n=0"
            from prems have inz: "i≠0" by simp
            from prems have idvdl: "i dvd l" by simp
            have ldiviieql: "l div i * i = l" by (rule dvd_div_pos[OF lpos inz idvdl])
            with lpos have ldivinz: "0 ≠ l div i" by auto

            then have ?case using prems
              apply simp
              apply (simp add:
                ac_dvd_eq[OF ldivinz, where m="d" and c="i" and n="a" and t="i'"]
                ldiviieql)
              by (simp add: zmult_commute)
          }
          ultimately show ?case by blast

        next
          case (3 i n i' n' r)
          from prems
          have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)"
            by simp
          then
          have "islint (Add (Mult (Cst i') (Var n')) (r))"
            by (simp add: islinintterm_eq_islint)
          then have linr: "islintn(Suc n',r)"
            by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def)
          from lininrp have linr2: "islinintterm r"
            by (simp add: islinintterm_subt[OF lininrp])
          from prems have "n < n'" by simp
          then have nppos: "0 < n'" by simp
          from prems have inz: "i≠0" by simp

          have "n=0 ∨ (∃m. (n = Suc m))" by arith
          moreover
          {
            assume "∃m. n = Suc m"
            then have npos: "0 < n" by arith
            have ?case using nppos intterm_novar0[OF lininrp] prems
              apply (auto simp add: linterm_novar0[OF linr, where x="a" and y="a*l"])
              by (simp_all add: nth_pos2)
          }
          moreover
          {
            assume nz: "n=0"
            from prems have idvdl: "i dvd l" by simp
            have ldiviieql: "l div i * i = l" by (rule dvd_div_pos[OF lpos inz idvdl])
            with lpos have ldivinz: "0 ≠ l div i" by auto

            then have ?case using prems linr2 linr
              apply (simp add: nth_pos2 lin_mul_corr linterm_novar0)

              apply (simp add: ac_dvd_eq[OF ldivinz, where m="d" and c="i" and n="a" and t="(i' * ats ! (n' - Suc 0) + I_intterm (a # ats) r)"] ldiviieql)
              by (simp add: zmult_ac linterm_novar0[OF linr, where x="a" and y="a*l"])
          }
          ultimately show ?case by blast

        qed simp_all
    next
        case (goal5 t c)
      from prems have cz: "c=0" by simp
        then have ?case
          using prems
        proof(induct t rule: islinintterm.induct)
          case (2 i n i') show ?case using prems
            proof-
              from prems have inz: "i≠0" by simp
              then
              have "n=0 ∨ n≠0" by arith
              moreover
              {
                assume "n≠0" then have ?thesis
                  using prems
                  by (cases n, simp_all)
              }
              moreover
              {
                assume nz: "n=0"
                from prems nz have idvdl: "i dvd l" by simp
                have "(i*a + i' = 0) = (l*a+ ((l div i)*i') = 0)"
                  by (rule adjustcoeff_eq_corr[OF lpos inz idvdl])
                then
                have ?thesis using prems by (simp add: mult_ac)
              }
              ultimately show ?thesis by blast
            qed
          next
            case (3 i n i' n' r) show ?case  using prems
            proof-
              from prems
              have lininrp: "islinintterm (Add (Mult (Cst i') (Var n')) r)"
                by simp
              then
              have "islint (Add (Mult (Cst i') (Var n')) (r))"
                by (simp add: islinintterm_eq_islint)
              then have linr: "islintn(Suc n',r)"
                by (simp add: islinintterm_subt[OF lininrp] islinintterm_eq_islint islint_def)
              from lininrp have linr2: "islinintterm r"
                by (simp add: islinintterm_subt[OF lininrp])
              from prems have "n < n'" by simp
              then have nppos: "0 < n'" by simp
              from prems have "i≠0" by simp
              then
              have "n=0 ∨ n≠0" by arith
              moreover
              {
                assume nnz: "n≠0"
                then have ?thesis using prems linr nppos nnz intterm_novar0[OF lininrp]
                  by (cases n, simp_all)
                (simp add: nth_pos2 linterm_novar0[OF linr, where x="a" and y="a*l"])
              }
              moreover
              {
                assume nz: "n=0"
                from prems have inz: "i ≠ 0" by auto
                from prems nz have idvdl: "i dvd l" by simp
                have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0) =
                  (l * a + l div i * (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0)"
                  by (rule adjustcoeff_eq_corr[OF lpos inz idvdl])
                then
                have ?thesis using prems linr linr2
                  by (simp add: mult_ac nth_pos2 lin_mul_corr
                    linterm_novar0[OF linr, where x="a" and y="a*l"])
              }
              ultimately show ?thesis by blast
            qed
        qed simp_all
        then show ?case by simp

    qed

    (* unitycoeff preserves semantics *)
    lemma unitycoeff_corr:
      assumes linp: "islinform p"
      shows "qinterp ats (QEx p) = qinterp ats (QEx (unitycoeff p))"
    proof-

      have lpos: "0 < formlcm p" by (rule formlcm_pos[OF linp])
      have dvd : "divideallc (formlcm p, p)" by (rule formlcm_divideallc[OF linp])
      show ?thesis  using prems lpos dvd
      proof (simp add: unitycoeff_def Let_def,case_tac "formlcm p = 1",
          simp_all add: adjustcoeff_corr)
        show "(∃x. qinterp (x * formlcm p # ats) (adjustcoeff (formlcm p, p))) =
          (∃x. formlcm p dvd x ∧
          qinterp (x # ats) (adjustcoeff (formlcm p, p)))"
          (is "(∃x. ?P(x* (formlcm p))) = (∃x. formlcm p dvd x ∧ ?P x)")
        proof-
          have "(∃x. ?P(x* (formlcm p))) = (∃x. ?P((formlcm p)*x))"
            by (simp add: mult_commute)
          also have "(∃x. ?P((formlcm p)*x)) = (∃x. (formlcm p dvd x) ∧ ?P x)"
            by (simp add: unity_coeff_ex[where P="?P"])
          finally show ?thesis by simp
        qed
      qed
    qed

    (* the resul of adjustcoeff is unified for all l with divideallc (l,p) *)
    lemma adjustcoeff_unified:
      assumes linp: "islinform p"
      and dvdc: "divideallc(l,p)"
      and lpos: "l > 0"
      shows "isunified (adjustcoeff(l, p))"
      using linp dvdc lpos
      proof(induct l p rule: adjustcoeff.induct,simp_all add: lin_mul_lintn islinintterm_eq_islint islint_def)
        case (goal1 l d c r)
        from prems have "c >0 ∨ c < 0" by auto
        moreover {
          assume cpos: "c > 0 "
          from prems have lp: "l > 0" by simp
          from prems have cdvdl: "c dvd l" by simp
          have clel: "c ≤ l" by (rule zdvd_imp_le[OF cdvdl lp])
          have "c div c ≤  l div c" by (rule zdiv_mono1[OF clel cpos])
          then have ?case using cpos by (simp add: zdiv_self)
        }
        moreover {
          assume cneg: "c < 0"

         have mcpos: "-c > 0" by simp
          then have mcnz: "-c ≠ 0" by simp
          from prems have mcdvdl: "-c dvd l"
            by simp
          then have l1:"l mod -c = 0" by (simp add: zdvd_iff_zmod_eq_0)
          from prems have lp: "l >0" by simp
          have mclel: "-c ≤ l" by (rule zdvd_imp_le[OF mcdvdl lp])
          have "l div c = (-l div -c)"  by simp
          also have "… = - (l div -c)" using l1
            by (simp only: zdiv_zminus1_eq_if[OF mcnz, where a="l"]) simp
          finally have diveq: "l div c = - (l div -c)" by simp

          have "-c div -c ≤ l div -c" by (rule zdiv_mono1[OF mclel mcpos])
          then have "0 < l div -c" using cneg
            by (simp add: zdiv_self)
          then have ?case using diveq by simp
        }
        ultimately  show ?case by blast
      next
        case (goal2 l p)    from prems have "c >0 ∨ c < 0" by auto
        moreover {
          assume cpos: "c > 0 "
          from prems have lp: "l > 0" by simp
          from prems have cdvdl: "c dvd l" by simp
          have clel: "c ≤ l" by (rule zdvd_imp_le[OF cdvdl lp])
          have "c div c ≤  l div c" by (rule zdiv_mono1[OF clel cpos])
          then have ?case using cpos by (simp add: zdiv_self)
        }
        moreover {
          assume cneg: "c < 0"

         have mcpos: "-c > 0" by simp
          then have mcnz: "-c ≠ 0" by simp
          from prems have mcdvdl: "-c dvd l"
            by simp
          then have l1:"l mod -c = 0" by (simp add: zdvd_iff_zmod_eq_0)
          from prems have lp: "l >0" by simp
          have mclel: "-c ≤ l" by (rule zdvd_imp_le[OF mcdvdl lp])
          have "l div c = (-l div -c)"  by simp
          also have "… = - (l div -c)" using l1
            by (simp only: zdiv_zminus1_eq_if[OF mcnz, where a="l"]) simp
          finally have diveq: "l div c = - (l div -c)" by simp

          have "-c div -c ≤ l div -c" by (rule zdiv_mono1[OF mclel mcpos])
          then have "0 < l div -c" using cneg
            by (simp add: zdiv_self)
          then have ?case using diveq by simp
        }
        ultimately  show ?case by blast
      qed

    lemma adjustcoeff_lcm_unified:
      assumes linp: "islinform p"
      shows "isunified (adjustcoeff(formlcm p, p))"
    using linp adjustcoeff_unified formlcm_pos formlcm_divideallc
    by simp

    (* the result of unitycoeff is unified *)
    lemma unitycoeff_unified:
      assumes linp: "islinform p"
      shows "isunified (unitycoeff p)"
    using linp formlcm_pos[OF linp]
    proof (auto simp add: unitycoeff_def Let_def adjustcoeff_lcm_unified)
      assume f1: "formlcm p = 1"
      have "isunified (adjustcoeff(formlcm p, p))"
        by (rule adjustcoeff_lcm_unified[OF linp])
      with f1
      show "isunified (adjustcoeff(1,p))" by simp
    qed

    lemma unified_isnnf:
      assumes unifp: "isunified p"
      shows "isnnf p"
      using unified_islinform[OF unifp] linform_isnnf
      by simp

    lemma unified_isqfree: "isunified p==> isqfree p"
    using unified_islinform linform_isqfree
    by auto

    (* Plus/Minus infinity , B and A set definitions *)

    consts minusinf :: "QF => QF"
           plusinf  :: "QF => QF"
           aset     :: "QF => intterm list"
           bset     :: "QF => intterm list"

    recdef minusinf "measure size"
    "minusinf (Le (Add (Mult (Cst c) (Var 0)) r) z) =
      (if c < 0 then F else T)"
    "minusinf (Eq (Add (Mult (Cst c) (Var 0)) r) z) = F"
    "minusinf (NOT(Eq (Add (Mult (Cst c) (Var 0)) r) z)) = T"
    "minusinf (And p q) = And (minusinf p) (minusinf q)"
    "minusinf (Or p q) = Or (minusinf p) (minusinf q)"
    "minusinf p = p"

    recdef plusinf "measure size"
    "plusinf (Le (Add (Mult (Cst c) (Var 0)) r) z) =
      (if c < 0 then T else F)"
    "plusinf (Eq (Add (Mult (Cst c) (Var 0)) r) z) = F"
    "plusinf (NOT (Eq (Add (Mult (Cst c) (Var 0)) r) z)) = T"
    "plusinf (And p q) = And (plusinf p) (plusinf q)"
    "plusinf (Or p q) = Or (plusinf p) (plusinf q)"
    "plusinf p = p"

    recdef bset "measure size"
    "bset (Le (Add (Mult (Cst c) (Var 0)) r) z) =
     (if c < 0 then [lin_add(r,(Cst -1)), r]
             else [lin_add(lin_neg r,(Cst -1))])"
    "bset (Eq (Add (Mult (Cst c) (Var 0)) r) z) =
      (if c < 0 then [lin_add(r,(Cst -1))]
             else [lin_add(lin_neg r,(Cst -1))])"
    "bset (NOT(Eq (Add (Mult (Cst c) (Var 0)) r) z)) =
      (if c < 0 then [r]
             else [lin_neg r])"
    "bset (And p q) = (bset p) @ (bset q)"
    "bset (Or p q) = (bset p) @ (bset q)"
    "bset p = []"

    recdef aset "measure size"
    "aset (Le (Add (Mult (Cst c) (Var 0)) r) z) =
      (if c < 0 then [lin_add (r, Cst 1)]
             else [lin_add (lin_neg r, Cst 1), lin_neg r])"
    "aset (Eq (Add (Mult (Cst c) (Var 0)) r) z) =
      (if c < 0 then [lin_add(r,(Cst 1))]
           else [lin_add(lin_neg r,(Cst 1))])"
    "aset (NOT(Eq (Add (Mult (Cst c) (Var 0)) r) z)) =
      (if c < 0 then [r]
          else [lin_neg r])"
    "aset (And p q) = (aset p) @ (aset q)"
    "aset (Or p q) = (aset p) @ (aset q)"
    "aset p = []"

    (* divlcm computes δ = lcm d , where d | x +t occurs in p *)
    consts divlcm :: "QF => int"
    recdef divlcm "measure size"
    "divlcm (Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) = (abs d)"
    "divlcm (NOT p) = divlcm p"
    "divlcm (And p q)= ilcm (divlcm p) (divlcm q)"
    "divlcm (Or p q) = ilcm (divlcm p) (divlcm q)"
    "divlcm p = 1"

    (* the preoperty of δ *)
    consts alldivide :: "int × QF => bool"
    recdef alldivide "measure (%(d,p). size p)"
    "alldivide (d,(Divides (Cst d') (Add (Mult (Cst c) (Var 0)) r))) =
      (d' dvd d)"
    "alldivide (d,(NOT p)) = alldivide (d,p)"
    "alldivide (d,(And p q)) = (alldivide (d,p) ∧ alldivide (d,q))"
    "alldivide (d,(Or p q)) = ((alldivide (d,p)) ∧ (alldivide (d,q)))"
    "alldivide (d,p) = True"

    (* alldivide is monotone *)
    lemma alldivide_mono: "!! d'. [| alldivide (d,p) ; d dvd d'|] ==> alldivide (d',p)"
    proof(induct d p rule: alldivide.induct, simp_all add: ilcm_dvd1 ilcm_dvd2)
      fix "d1" "d2" "d3"
      assume th1:"d2 dvd (d1::int)"
        and th2: "d1 dvd d3"
      show "d2 dvd d3" by (rule zdvd_trans[OF th1 th2])
    qed

    (* Some simple lemmas *)
    lemma zdvd_eq_zdvd_abs: " (d::int) dvd d' = (d dvd (abs d')) "
    proof-
      have "d' < 0 ∨ d' ≥ 0" by arith
      moreover
      {
        assume dn': "d' < 0"
        then have "abs d' = - d'" by simp
        then
        have ?thesis by (simp)
      }
      moreover
      {
        assume dp': "d' ≥ 0"
        then have "abs d' = d'" by simp
        then have ?thesis  by simp
      }
        ultimately show ?thesis by blast
    qed

    lemma zdvd_refl_abs: "(d::int) dvd (abs d)"
    proof-
      have "d dvd d" by simp
      then show ?thesis by (simp add: iffD1 [OF zdvd_eq_zdvd_abs [where d = "d" and d'="d"]])
    qed

    (* δ > 0*)
    lemma divlcm_pos:
      assumes
      linp: "islinform p"
      shows "0 < divlcm p"
    using linp
    proof (induct p rule: divlcm.induct,simp_all add: ilcm_pos)
      case (goal1 f) show ?case
        using prems
        by (cases f, auto) (case_tac "intterm1", auto)
    qed

    lemma nz_le: "(x::int) > 0 ==> x ≠ 0" by auto
    (* divlcm is correct *)
    lemma divlcm_corr:
      assumes
      linp: "islinform p"
      shows "alldivide (divlcm p,p)"
      using linp divlcm_pos
    proof (induct p rule: divlcm.induct,simp_all add: zdvd_refl_abs,clarsimp simp add: Nat.gr0_conv_Suc)
      case (goal1 f)
      have "islinform f" using prems
        by (cases f, auto) (case_tac "intterm2", auto,case_tac "intterm1", auto)
      then have "alldivide (divlcm f, f)"  using prems by simp
      moreover have "divlcm (NOT f) = divlcm f" by simp
      moreover have "alldivide (x,f) = alldivide (x,NOT f)" by simp
      ultimately show ?case by simp
    next
      case (goal2 f g)
      have dvd1: "(divlcm f) dvd (ilcm (divlcm f) (divlcm g))"
        using prems by(simp add: ilcm_dvd1 nz_le)
      have dvd2: "(divlcm g) dvd (ilcm (divlcm f) (divlcm g))"
        using prems by (simp add: ilcm_dvd2 nz_le)
      from dvd1 prems
      have "alldivide (ilcm (divlcm f) (divlcm g), f)"
        by (simp add: alldivide_mono[where d= "divlcm f" and p="f" and d' ="ilcm (divlcm f) (divlcm g)"])
      moreover   from dvd2 prems
       have "alldivide (ilcm (divlcm f) (divlcm g), g)"
        by (simp add: alldivide_mono[where d= "divlcm g" and p="g" and d' ="ilcm (divlcm f) (divlcm g)"])
      ultimately show ?case by simp
    next
      case (goal3 f g)
      have dvd1: "(divlcm f) dvd (ilcm (divlcm f) (divlcm g))"
        using prems by (simp add: nz_le ilcm_dvd1)
      have dvd2: "(divlcm g) dvd (ilcm (divlcm f) (divlcm g))"
        using prems by (simp add: nz_le ilcm_dvd2)
      from dvd1 prems
      have "alldivide (ilcm (divlcm f) (divlcm g), f)"
        by (simp add: alldivide_mono[where d= "divlcm f" and p="f" and d' ="ilcm (divlcm f) (divlcm g)"])
      moreover   from dvd2 prems
       have "alldivide (ilcm (divlcm f) (divlcm g), g)"
        by (simp add: alldivide_mono[where d= "divlcm g" and p="g" and d' ="ilcm (divlcm f) (divlcm g)"])
      ultimately show ?case by simp
    qed

    (* Properties of  minusinf and plusinf*)

    (* minusinf p and p are the same for minusinfity … *)
    lemma minusinf_eq:
      assumes unifp: "isunified p"
      shows "∃ z. ∀ x. x < z --> (qinterp (x#ats) p = qinterp (x#ats) (minusinf p))"
    using unifp unified_islinform[OF unifp]
    proof (induct p rule: minusinf.induct)
      case (1 c r z)
      have "c <0 ∨ 0 ≤ c" by arith
      moreover
      {
        assume cneg: " c < 0"
        from prems have z0: "z= Cst 0"
          by (cases z,auto)
        with prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)"
          by simp

        from prems z0 have ?case
          proof-
            show ?thesis
              using prems z0
          apply auto
          apply (rule exI[where x="I_intterm (a # ats) r"])
          apply (rule allI)
          proof-
            fix x
            show "x < I_intterm (a # ats) r --> ¬ - x + I_intterm (x # ats) r ≤ 0"
              by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"])
          qed
        qed
      }
      moreover
      {
        assume cpos: "0 ≤ c"
        from prems have z0: "z= Cst 0"
          by (cases z) auto
        with prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)"
          by simp

        from prems z0 have ?case
          proof-
            show ?thesis
              using prems z0
          apply auto
          apply (rule exI[where x="-(I_intterm (a # ats) r)"])
          apply (rule allI)
          proof-
            fix x
            show "x < - I_intterm (a # ats) r --> x + I_intterm (x # ats) r ≤ 0"
              by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"])
          qed
        qed
      }

        ultimately show ?case by blast
    next
      case (2 c r z)
      from prems have z0: "z= Cst 0"
        by (cases z,auto)
      with prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)"
        by simp
      have "c <0 ∨ 0 ≤ c" by arith
      moreover
      {
        assume cneg: " c < 0"
        from prems z0 have ?case
          proof-
            show ?thesis
              using prems z0
          apply auto
          apply (rule exI[where x="I_intterm (a # ats) r"])
          apply (rule allI)
          proof-
            fix x
            show "x < I_intterm (a # ats) r --> ¬ - x + I_intterm (x # ats) r = 0"
              by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"])
          qed
        qed
      }
      moreover
      {
        assume cpos: "0 ≤ c"
        from prems z0 have ?case
          proof-
            show ?thesis
              using prems z0
          apply auto
          apply (rule exI[where x="-(I_intterm (a # ats) r)"])
          apply (rule allI)
          proof-
            fix x
            show "x < - I_intterm (a # ats) r --> x + I_intterm (x # ats) r ≠ 0"
              by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"])
          qed
        qed
      }

        ultimately show ?case by blast
    next
      case (3 c r z)
      from prems have z0: "z= Cst 0"
        by (cases z,auto)
      with prems have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)"
        by simp
      have "c <0 ∨ 0 ≤ c" by arith
      moreover
      {
        assume cneg: " c < 0"
        from prems z0 have ?case
          proof-
            show ?thesis
              using prems z0
          apply auto
          apply (rule exI[where x="I_intterm (a # ats) r"])
          apply (rule allI)
          proof-
            fix x
            show "x < I_intterm (a # ats) r --> ¬ - x + I_intterm (x # ats) r = 0"
              by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"])
          qed
        qed
      }
      moreover
      {
        assume cpos: "0 ≤ c"
        from prems z0 have ?case
          proof-
            show ?thesis
              using prems z0
          apply auto
          apply (rule exI[where x="-(I_intterm (a # ats) r)"])
          apply (rule allI)
          proof-
            fix x
            show "x < - I_intterm (a # ats) r --> x + I_intterm (x # ats) r ≠ 0"
              by (simp add: intterm_novar0[OF lincnr, where x="a" and y="x"])
          qed
        qed
      }

        ultimately show ?case by blast
    next

      case (4 f g)
      from prems obtain "zf" where
        zf:"∀x<zf. qinterp (x # ats) f = qinterp (x # ats) (minusinf f)" by auto
      from prems obtain "zg" where
        zg:"∀x<zg. qinterp (x # ats) g = qinterp (x # ats) (minusinf g)" by auto
      from zf zg show ?case
        apply auto
        apply (rule exI[where x="min zf zg"])
        by simp

    next case (5 f g)
      from prems obtain "zf" where
        zf:"∀x<zf. qinterp (x # ats) f = qinterp (x # ats) (minusinf f)" by auto
      from prems obtain "zg" where
        zg:"∀x<zg. qinterp (x # ats) g = qinterp (x # ats) (minusinf g)" by auto
      from zf zg show ?case
        apply auto
        apply (rule exI[where x="min zf zg"])
        by simp

    qed simp_all

    (* miusinf p behaves periodically*)
    lemma minusinf_repeats:
      assumes alldvd: "alldivide (d,p)"
      and unity: "isunified p"
      shows "qinterp (x#ats) (minusinf p) = qinterp ((x + c*d)#ats) (minusinf p)"
      using alldvd unity unified_islinform[OF unity]
    proof(induct p rule: islinform.induct, simp_all)
      case (goal1 t a)
      show ?case
        using prems
        apply (cases t, simp_all add: nth_pos2)
        apply (case_tac "intterm1", simp_all)
        apply (case_tac "intterm1a",simp_all)
        by (case_tac "intterm2a",simp_all)
      (case_tac "nat",simp_all add: nth_pos2 intterm_novar0[where x="x" and y="x+c*d"])
    next
      case (goal2 t a)
      show ?case
        using prems
        apply (cases t, simp_all add: nth_pos2)
        apply (case_tac "intterm1", simp_all)
        apply (case_tac "intterm1a",simp_all)
        by (case_tac "intterm2a",simp_all)
      (case_tac "nat",simp_all add: nth_pos2 intterm_novar0[where x="x" and y="x+c*d"])
    next
      case (goal3 a t)
      show ?case using prems

      proof(induct t rule: islinintterm.induct, simp_all add: nth_pos2)
        case (goal1 i n i')
        show ?case
          using prems
        proof(cases n, simp_all, case_tac "i=1", simp,
            simp add: dvd_period[where a="a" and d="d" and x="x" and c="c"])
          case goal1
          from prems have "(abs i = 1) ∧ i ≠ 1" by auto
          then  have im1: "i=-1" by arith
          then have "(a dvd i*x + i') = (a dvd x + (-i'))"
            by (simp add: uminus_dvd_conv'[where d="a" and t="-x +i'"])
          moreover
          from im1 have "(a dvd i*x + (i*(c * d)) + i') = (a dvd (x + c*d - i'))"
            apply simp
            apply (simp add: uminus_dvd_conv'[where d="a" and t="-x - c * d + i'"])
            by (simp add: zadd_ac)
          ultimately
          have eq1:"((a dvd i*x + i') = (a dvd i*x + (i*(c * d)) + i')) =
            ((a dvd x + (-i'))  = (a dvd (x + c*d - i')))" by simp
          moreover
          have dvd2: "(a dvd x + (-i')) = (a dvd x + c * d + (-i'))"
            by (rule dvd_period[where a="a" and d="d" and x="x" and c="c"], assumption)
          ultimately show ?case by simp
        qed
      next
        case (goal2 i n i' n' r)
        have "n = 0 ∨ 0 < n" by arith
        moreover
        {
          assume npos: "0 < n"
          from prems have "n < n'" by simp then have "0 < n'" by simp
          moreover from prems
          have linr: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp
          ultimately have ?case
            using prems npos
            by (simp add: nth_pos2 intterm_novar0[OF linr,where x="x" and y="x + c*d"])
        }
        moreover
        {
          assume n0: "n=0"
          from prems have lin2: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp
          from prems have "n < n'" by simp then have npos': "0 < n'" by simp
          with prems have ?case
          proof(simp add: intterm_novar0[OF lin2, where x="x" and y="x+c*d"]
              nth_pos2 dvd_period,case_tac "i=1",
              simp add: dvd_period[where a="a" and d="d" and x="x" and c="c"], simp)
            case goal1
            from prems have "abs i = 1 ∧ i≠1" by auto
            then have mi: "i = -1" by arith
            have "(a dvd -x + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r)) =
              (a dvd x + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r))"
              by (simp add:
                uminus_dvd_conv'[where d="a" and
                t="-x + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r)"])
            also
            have "(a dvd x + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)) =
              (a dvd x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r))"
              by (rule dvd_period[where a="a" and d="d" and x="x" and c="c"], assumption)
            also
            have "(a dvd x +c*d +
              (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)) =
              (a dvd -(x +c*d +
              (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)))"
              by (rule uminus_dvd_conv'[where d="a" and
                t="x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)"])
            also
            have "(a dvd -(x +c*d +
              (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)))
              = (a dvd
              - x - c * d + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r))"
              by (auto,simp_all add: zadd_ac)
            finally show ?case using mi by auto
          qed
        }
        ultimately show ?case by blast
      qed
    next
      case (goal4 a t)
      show ?case using prems
      proof(induct t rule: islinintterm.induct, simp_all,case_tac "n=0",
          simp_all add: nth_pos2)
        case (goal1 i n i')
        show ?case
          using prems
        proof(case_tac "i=1", simp,
            simp add: dvd_period[where a="a" and d="d" and x="x" and c="c"])
          case goal1
          from prems have "abs i = 1 ∧ i≠1" by auto
          then have im1: "i=-1" by arith
          then have "(a dvd i*x + i') = (a dvd x + (-i'))"
            by (simp add: uminus_dvd_conv'[where d="a" and t="-x +i'"])
          moreover
          from im1 have "(a dvd i*x + (i*(c * d)) + i') = (a dvd (x + c*d - i'))"
            apply simp
            apply (simp add: uminus_dvd_conv'[where d="a" and t="-x - c * d + i'"])
            by (simp add: zadd_ac)
          ultimately
          have eq1:"((a dvd i*x + i') = (a dvd i*x + (i*(c * d)) + i')) =
            ((a dvd x + (-i'))  = (a dvd (x + c*d - i')))" by simp
          moreover
          have dvd2: "(a dvd x + (-i')) = (a dvd x + c * d + (-i'))"
            by (rule dvd_period[where a="a" and d="d" and x="x" and c="c"], assumption)
          ultimately show ?thesis by simp
        qed
      next
        case (goal2 i n i' n' r)
        have "n = 0 ∨ 0 < n" by arith
        moreover
        {
          assume npos: "0 < n"
          from prems have "n < n'" by simp then have "0 < n'" by simp
          moreover from prems
          have linr: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp
          ultimately have ?case
            using prems npos
            by (simp add: nth_pos2 intterm_novar0[OF linr,where x="x" and y="x + c*d"])
        }
        moreover
        {
          assume n0: "n=0"
          from prems have lin2: "islinintterm (Add (Mult (Cst i') (Var n')) r)" by simp
          from prems have "n < n'" by simp then have npos': "0 < n'" by simp
          with prems have ?case
          proof(simp add: intterm_novar0[OF lin2, where x="x" and y="x+c*d"]
              nth_pos2 dvd_period,case_tac "i=1",
              simp add: dvd_period[where a="a" and d="d" and x="x" and c="c"], simp)
            case goal1
            from prems have "abs i = 1 ∧ i≠1" by auto
            then have mi: "i = -1" by arith
            have "(a dvd -x + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r)) =
              (a dvd x + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r))"
              by (simp add:
                uminus_dvd_conv'[where d="a" and
                t="-x + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r)"])
            also
            have "(a dvd x + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)) =
              (a dvd x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r))"
              by (rule dvd_period[where a="a" and d="d" and x="x" and c="c"], assumption)
            also
            have "(a dvd x +c*d +
              (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)) =
              (a dvd -(x +c*d +
              (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)))"
              by (rule uminus_dvd_conv'[where d="a" and
                t="x +c*d + (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)"])
            also
            have "(a dvd -(x +c*d +
              (-i' * ats ! (n' - Suc 0) - I_intterm ((x + c * d) # ats) r)))
              = (a dvd
              - x - c * d + (i' * ats ! (n' - Suc 0) + I_intterm ((x + c * d) # ats) r))"
              by (auto,simp_all add: zadd_ac)
            finally show ?case using mi by auto
          qed
        }
        ultimately show ?case by blast
      qed
    next
      case (goal5 t a)
      show ?case
        using prems
        apply (cases t, simp_all add: nth_pos2)
        apply (case_tac "intterm1", simp_all)
        apply (case_tac "intterm1a",simp_all)
        by (case_tac "intterm2a",simp_all)
      (case_tac "nat",simp_all add: nth_pos2 intterm_novar0[where x="x" and y="x+c*d"])
    qed

    lemma minusinf_repeats2:
      assumes alldvd: "alldivide (d,p)"
      and unity: "isunified p"
      shows "∀ x k. (qinterp (x#ats) (minusinf p) = qinterp ((x - k*d)#ats) (minusinf p))"
      (is "∀ x k. ?P x = ?P (x - k*d)")
    proof(rule allI, rule allI)
      fix x k
      show "?P x = ?P (x - k*d)"
      proof-
        have "?P x = ?P (x + (-k)*d)" by (rule minusinf_repeats[OF alldvd unity])
        then have "?P x = ?P (x - (k*d))" by simp
        then show ?thesis by blast
      qed
    qed

    (* existence for minusinf p is existence for p *)
    lemma minusinf_lemma:
      assumes unifp: "isunified p"
      and exminf: "∃ j ∈ {1 ..d}. qinterp (j#ats) (minusinf p)" (is "∃ j ∈ {1 .. d}. ?P1 j")
      shows "∃ x. qinterp (x#ats) p" (is "∃ x. ?P x")
    proof-
      from exminf obtain "j" where P1j: "?P1 j" by blast
      have ePeqP1: "∃z. ∀ x. x < z --> (?P x = ?P1 x)"
        by (rule minusinf_eq[OF unifp])
      then obtain "z" where P1eqP : "∀ x. x < z --> (?P x = ?P1 x)" by blast
      let ?d = "divlcm p"
      have alldvd: "alldivide (?d,p)" using unified_islinform[OF unifp] divlcm_corr
        by auto
      have dpos: "0 < ?d" using unified_islinform[OF unifp] divlcm_pos
        by simp
      have P1eqP1 : "∀ x k. ?P1 x = ?P1 (x - k*(?d))"
        by (rule minusinf_repeats2[OF alldvd unifp])
      let ?w = "j - (abs (j-z) +1)* ?d"
      show "∃ x. ?P x"
      proof
        have w: "?w < z"
          by (rule decr_lemma[OF dpos])

        have "?P1 j = ?P1 ?w" using P1eqP1 by blast
        also have "… = ?P ?w"  using w P1eqP by blast
        finally show "?P ?w" using P1j by blast
      qed
    qed

    (* limited search for the withness for minusinf p, due to peridicity *)
    lemma minusinf_disj:
      assumes unifp: "isunified p"
      shows "(∃ x. qinterp (x#ats) (minusinf p)) =
      (∃ j ∈ { 1.. divlcm p}. qinterp (j#ats) (minusinf p))"
      (is "(∃ x. ?P x) = (∃ j ∈ { 1.. ?d}. ?P j)")
    proof
      have linp: "islinform p" by (rule unified_islinform[OF unifp])
      have dpos: "0 < ?d" by (rule divlcm_pos[OF linp])
      have alldvd: "alldivide(?d,p)" by (rule divlcm_corr[OF linp])
      {
        assume "∃ j∈ {1 .. ?d}. ?P j"
        then show "∃ x. ?P x" using dpos  by auto
      next
        assume "∃ x. ?P x"
        then obtain "x" where P: "?P x" by blast
        have modd: "∀x k. ?P x = ?P (x - k*?d)"
          by (rule minusinf_repeats2[OF alldvd unifp])

        have "x mod ?d = x - (x div ?d)*?d"
          by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
        hence Pmod: "?P x = ?P (x mod ?d)" using modd by simp
        show "∃ j∈ {1 .. ?d}. ?P j"
        proof (cases)
          assume "x mod ?d = 0"
          hence "?P 0" using P Pmod by simp
          moreover have "?P 0 = ?P (0 - (-1)*?d)" using modd by blast
          ultimately have "?P ?d" by simp
          moreover have "?d ∈ {1 .. ?d}" using dpos
            by (simp add:atLeastAtMost_iff)
          ultimately show "∃ j∈ {1 .. ?d}. ?P j" ..
        next
          assume not0: "x mod ?d ≠ 0"
          have "?P(x mod ?d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
          moreover have "x mod ?d : {1 .. ?d}"
          proof -
            have "0 ≤ x mod ?d" by(rule pos_mod_sign[OF dpos])
            moreover have "x mod ?d < ?d"  by(rule pos_mod_bound[OF dpos])
            ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
          qed
          ultimately show "∃ j∈ {1 .. ?d}. ?P j" ..
        qed
      }
    qed

    lemma minusinf_qfree:
      assumes linp : "islinform p"
      shows "isqfree (minusinf p)"
      using linp
     by (induct p rule: minusinf.induct) auto

    (* Properties of bset and a set *)

    (* The elements of a bset are linear *)
    lemma bset_lin:
      assumes unifp: "isunified p"
      shows "∀ b ∈ set (bset p). islinintterm b"
    using unifp unified_islinform[OF unifp]
    proof (induct p rule: bset.induct, auto)
      case (goal1 c r z)
      from prems have "z = Cst 0" by (cases z, simp_all)
      then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      have "islinintterm (Cst -1)" by simp
      then show ?case using linr lin_add_lin by simp
    next
      case (goal2 c r z)
      from prems have "z = Cst 0" by (cases z, simp_all)
      then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      show ?case by (rule linr)
    next
      case (goal3 c r z)
      from prems have "z = Cst 0" by (cases z, simp_all)
      then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      have "islinintterm (Cst -1)" by simp
      then show ?case using linr lin_add_lin lin_neg_lin by simp
    next
      case (goal4 c r z)
      from prems have "z = Cst 0" by (cases z, simp_all)
      then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      have "islinintterm (Cst -1)" by simp
      then show ?case using linr lin_add_lin lin_neg_lin by simp
    next
      case (goal5 c r z)
      from prems have "z = Cst 0" by (cases z, simp_all)
      then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      have "islinintterm (Cst -1)" by simp
      then show ?case using linr lin_add_lin lin_neg_lin by simp
    next
      case (goal6 c r z)
      from prems have "z = Cst 0" by (cases z, simp_all)
      then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      have "islinintterm (Cst -1)" by simp
      then show ?case using linr lin_add_lin lin_neg_lin by simp
    next
      case (goal7 c r z)
      from prems have "z = Cst 0" by (cases z, simp_all)
      then have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" using prems by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      have "islinintterm (Cst -1)" by simp
      then show ?case using linr lin_add_lin lin_neg_lin by simp
    qed

    (* The third lemma in Norrisch's Paper *)
    lemma bset_disj_repeat:
      assumes unifp: "isunified p"
      and alldvd: "alldivide (d,p)"
      and dpos: "0 < d"
      and nob: "(qinterp (x#ats) q) ∧ ¬(∃j∈ {1 .. d}. ∃ b ∈ set (bset p). (qinterp (((I_intterm (a#ats) b) + j)#ats) q)) ∧(qinterp (x#ats) p)"
      (is "?Q x ∧ ¬(∃ j∈ {1.. d}. ∃ b∈ ?B. ?Q (?I a b + j)) ∧ ?P x")
        shows "?P (x -d)"
      using unifp nob alldvd unified_islinform[OF unifp]
    proof (induct p rule: islinform.induct,auto)
      case (goal1 t)
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have "n=0 ∨ n>0" by arith
        moreover {assume "n>0" then have ?case
            using prems
            by (simp add: nth_pos2
              intterm_novar0[OF lininr, where x="x" and y="x-d"]) }
        moreover
        {assume nz: "n = 0"
          from prems have "abs i = 1" by auto
          then have "i = -1 ∨ i =1" by arith
          moreover
          {
            assume i1: "i=1"
            have ?case  using dpos prems
              by (auto simp add: intterm_novar0[OF lininr, where x="x" and y="x - d"])
          }
          moreover
          {
            assume im1: "i = -1"
            have ?case
              using prems
            proof(auto simp add: intterm_novar0[OF lininr, where x="x - d" and y="x"], cases)
              assume "- x + d +  ?I x r ≤ 0"
              then show "- x + d + ?I x r ≤ 0" .
            next
              assume np: "¬ - x + d +  ?I x r ≤ 0"
              then have ltd:"x - ?I x r ≤ d - 1" by simp
              from prems have "-x + ?I x r ≤ 0" by simp
              then have ge0: "x - ?I x r ≥ 0"
                by simp
              from ltd ge0 have "x - ?I x r = 0 ∨ (1 ≤ x - ?I x r ∧ x - ?I x r ≤ d - 1) " by arith
              moreover
              {
                assume "x - ?I x r = 0"
                then have xeqr: "x = ?I x r" by simp
                from prems have "?Q x" by simp
                with xeqr have qr:"?Q (?I x r)" by simp
                from prems have lininr: "islinintterm (Add (Mult (Cst i) (Var 0)) r)" by simp
                have "islinintterm r" by (rule islinintterm_subt[OF lininr])
                from prems
                have "∀j∈{1..d}. ¬ ?Q (?I a r + -1 + j)"
                  using linr by (auto simp add: lin_add_corr)
                moreover from dpos have "1 ∈ {1..d}" by simp
                ultimately have " ¬ ?Q (?I a r + -1 + 1)" by blast
                with dpos linr have "¬ ?Q (?I x r)"
                  by (simp add: intterm_novar0[OF lininr, where x="x" and y="a"] lin_add_corr)
                with qr have "- x + d + ?I x r ≤ 0" by simp
              }
              moreover
              {
                assume gt0: "1 ≤ x - ?I x r ∧ x - ?I x r ≤ d - 1"
                then have "∃ j∈ {1 .. d - 1}. x - ?I x r =  j" by simp
                then have "∃ j∈ {1 .. d}. x - ?I x r =  j" by auto
                then obtain  "j" where con: "1≤j ∧ j ≤ d  ∧ x - ?I x r = j" by auto
                then have xeqr: "x = ?I x r + j" by auto
                with prems have "?Q (?I x r + j)" by simp
                with con have qrpj: "∃ j∈ {1 .. d}. ?Q (?I x r + j)" by auto
                from prems have "∀j∈{1..d}. ¬ ?Q (?I a r + j)" by auto
                then have "¬ (∃ j∈{1..d}. ?Q (?I x r + j))"
                  by (simp add: intterm_novar0[OF lininr, where x="x" and y="a"])
                with qrpj prems have "- x + d + ?I x r ≤ 0" by simp

              }
              ultimately show "- x + d + ?I x r ≤ 0" by blast
            qed
          }
          ultimately have ?case by blast
        }
        ultimately have ?case by blast
      }
      ultimately show ?case by blast
    next
      case (goal3 a t)
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have "n=0 ∨ n>0" by arith
        moreover {assume "n>0" then have ?case using prems
            by (simp add: nth_pos2
              intterm_novar0[OF lininr, where x="x" and y="x-d"]) }
        moreover {
          assume nz: "n=0"
          from prems have "abs i = 1" by auto
          then have ipm: "i=1 ∨ i = -1" by arith
          from nz prems have advdixr: "a dvd (i * x) + I_intterm (x # ats) r"
            by simp
          from prems have "a dvd d" by simp
          then have advdid: "a dvd i*d" using ipm by auto
          have ?case
          using prems ipm
          by (auto simp add: intterm_novar0[OF lininr, where x="x-d" and y="x"] dvd_period[OF advdid, where x="i*x" and c="-1"])
      }
      ultimately have ?case by blast
      } ultimately show ?case by blast
    next

      case (goal4 a t)
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])

        have "n=0 ∨ n>0" by arith
        moreover {assume "n>0" then have ?case using prems
            by (simp add: nth_pos2
              intterm_novar0[OF lininr, where x="x" and y="x-d"]) }
        moreover {
          assume nz: "n=0"
          from prems have "abs i = 1" by auto
          then have ipm: "i =1 ∨ i = -1" by arith
          from nz prems have advdixr: "¬ (a dvd (i * x) + I_intterm (x # ats) r)"
            by simp
          from prems have "a dvd d" by simp
          then have advdid: "a dvd i*d" using ipm by auto
          have ?case
          using prems ipm
          by (auto simp add: intterm_novar0[OF lininr, where x="x-d" and y="x"] dvd_period[OF advdid, where x="i*x" and c="-1"])
      }
      ultimately have ?case by blast
      } ultimately show ?case by blast
    next
      case (goal2 t)
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have "n=0 ∨ n>0" by arith
        moreover {assume "n>0" then have ?case
            using prems
            by (simp add: nth_pos2
              intterm_novar0[OF lininr, where x="x" and y="x-d"]) }
        moreover
        {assume nz: "n = 0"
          from prems have "abs i = 1" by auto
          then have "i = -1 ∨ i =1" by arith
          moreover
          {
            assume i1: "i=1"
            with prems have px: "x + ?I x r = 0" by simp
            then have "x = (- ?I x r - 1) + 1" by simp
            hence q1: "?Q ((- ?I x r - 1) + 1)" by simp
            from prems have "¬ (?Q ((?I a (lin_add(lin_neg r, Cst -1))) + 1))"
              by auto
            hence "¬ (?Q ((- ?I a r - 1) + 1))"
              using lin_add_corr lin_neg_corr linr lin_neg_lin
              by simp
            hence "¬ (?Q ((- ?I x r - 1) + 1))"
              using intterm_novar0[OF lininr, where x="x" and y="a"]
              by simp
            with q1 have  ?case by simp
          }
          moreover
          {
            assume im1: "i = -1"
            with prems have px: "-x + ?I x r = 0" by simp
            then have "x = ?I x r" by simp
            hence q1: "?Q (?I x r)" by simp
            from prems have "¬ (?Q ((?I a (lin_add(r, Cst -1))) + 1))"
              by auto
            hence "¬ (?Q (?I a r))"
              using lin_add_corr lin_neg_corr linr lin_neg_lin
              by simp
            hence "¬ (?Q (?I x r ))"
              using intterm_novar0[OF lininr, where x="x" and y="a"]
              by simp
            with q1 have  ?case by simp
          }
          ultimately have ?case by blast
        }
        ultimately have ?case by blast
      }
      ultimately show ?case by blast
    next
      case (goal5 t)
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have "n=0 ∨ n>0" by arith
        moreover {assume "n>0" then have ?case
            using prems
            by (simp add: nth_pos2
              intterm_novar0[OF lininr, where x="x" and y="x-d"]) }
        moreover
        {assume nz: "n = 0"
          from prems have "abs i = 1" by auto
          then have "i = -1 ∨ i =1" by arith
          moreover
          {
            assume i1: "i=1"
            with prems have px: "x -d + ?I (x-d) r = 0" by simp
            hence "x = (- ?I x r) + d"
              using intterm_novar0[OF lininr, where x="x" and y="x-d"]
              by simp
            hence q1: "?Q (- ?I x r + d)" by simp
            from prems have "¬ (?Q ((?I a (lin_neg r)) + d))"
              by auto
            hence "¬ (?Q (- ?I a r + d))"
              using lin_neg_corr linr by simp
            hence "¬ (?Q ((- ?I x r + d)))"
              using intterm_novar0[OF lininr, where x="x" and y="a"]
              by simp
            with q1 have  ?case by simp
          }
          moreover
          {
            assume im1: "i = -1"
            with prems have px: "- (x -d) + ?I (x - d) r = 0" by simp
            then have "x = ?I x r + d "
              using intterm_novar0[OF lininr, where x="x" and y="x-d"]
              by simp
            hence q1: "?Q (?I x r + d)" by simp
            from prems have "¬ (?Q ((?I a r) + d))"
              by auto
            hence "¬ (?Q (?I x r + d))"
              using intterm_novar0[OF lininr, where x="x" and y="a"]
              by simp
            with q1 have  ?case by simp
          }
          ultimately have ?case by blast
        }
        ultimately have ?case by blast
      }
      ultimately show ?case by blast

    qed

    lemma bset_disj_repeat2:
      assumes unifp: "isunified p"

      shows "∀ x. ¬(∃j∈ {1 .. (divlcm p)}. ∃ b ∈ set (bset p).
      (qinterp (((I_intterm (a#ats) b) + j)#ats) p))
      --> (qinterp (x#ats) p) --> (qinterp ((x - (divlcm p))#ats) p)"
      (is "∀ x. ¬(∃ j∈ {1 .. ?d}. ∃ b∈ ?B. ?P (?I a b + j)) --> ?P x --> ?P (x - ?d)")
    proof
      fix x
      have linp: "islinform p" by (rule unified_islinform[OF unifp])
      have dpos: "?d > 0" by (rule divlcm_pos[OF linp])
      have alldvd: "alldivide(?d,p)" by (rule divlcm_corr[OF linp])
        show "¬(∃ j∈ {1 .. ?d}. ∃ b∈ ?B. ?P (?I a b + j)) --> ?P x --> ?P (x - ?d)"
        using prems bset_disj_repeat[OF unifp alldvd dpos]
        by blast
    qed

    (* Cooper's theorem in the minusinfinity version *)
    lemma cooper_mi_eq:
      assumes unifp : "isunified p"
      shows "(∃ x. qinterp (x#ats) p) =
      ((∃ j ∈ {1 .. (divlcm p)}. qinterp (j#ats) (minusinf p)) ∨
      (∃ j ∈ {1 .. (divlcm p)}. ∃ b ∈ set (bset p).
      qinterp (((I_intterm (a#ats) b) + j)#ats) p))"
      (is "(∃ x. ?P x) = ((∃ j∈ {1 .. ?d}. ?MP j) ∨ (∃ j ∈ ?D. ∃ b∈ ?B. ?P (?I a b + j)))")
    proof-
      have linp :"islinform p" by (rule unified_islinform[OF unifp])
      have dpos: "?d > 0" by (rule divlcm_pos[OF linp])
      have alldvd: "alldivide(?d,p)" by (rule divlcm_corr[OF linp])
      have eMPimpeP: "(∃j ∈ ?D. ?MP j) --> (∃x. ?P x)"
        by (simp add: minusinf_lemma[OF unifp, where d="?d" and ats="ats"])
      have ePimpeP: "(∃ j ∈ ?D. ∃ b∈ ?B. ?P (?I a b + j)) --> (∃ x. ?P x)"
        by blast
      have bst_rep: "∀ x. ¬ (∃ j ∈ ?D. ∃ b ∈ ?B. ?P (?I a b + j)) --> ?P x --> ?P (x - ?d)"
        by (rule bset_disj_repeat2[OF unifp])
      have MPrep: "∀ x k. ?MP x = ?MP (x- k*?d)"
        by (rule minusinf_repeats2[OF alldvd unifp])
      have MPeqP: "∃ z. ∀  x < z. ?P x = ?MP x"
        by (rule minusinf_eq[OF unifp])
      let ?B'= "{?I a b| b. b∈ ?B}"
      from bst_rep have bst_rep2: "∀x. ¬ (∃j∈?D. ∃b∈ ?B'. ?P (b+j)) --> ?P x --> ?P (x - ?d)"
        by auto
      show ?thesis
      using cpmi_eq[OF dpos MPeqP bst_rep2 MPrep]
      by auto
    qed

    (* A formalized analogy between aset, bset, plusinfinity and minusinfinity *)

    consts mirror:: "QF => QF"
    recdef mirror "measure size"
    "mirror (Le (Add (Mult (Cst c) (Var 0)) r) z) =
      (Le (Add (Mult (Cst (- c)) (Var 0)) r) z)"
    "mirror (Eq (Add (Mult (Cst c) (Var 0)) r) z) =
      (Eq (Add (Mult (Cst (- c)) (Var 0)) r) z)"
    "mirror (Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r)) =
      (Divides (Cst d) (Add (Mult (Cst (- c)) (Var 0)) r))"
    "mirror (NOT(Divides (Cst d) (Add (Mult (Cst c) (Var 0)) r))) =
      (NOT(Divides (Cst d) (Add (Mult (Cst (- c)) (Var 0)) r)))"
    "mirror (NOT(Eq (Add (Mult (Cst c) (Var 0)) r) z)) =
      (NOT(Eq (Add (Mult (Cst (- c)) (Var 0)) r) z))"
    "mirror (And p q) = And (mirror p) (mirror q)"
    "mirror (Or p q) = Or (mirror p) (mirror q)"
    "mirror p = p"
    (* mirror preserves unifiedness *)

    lemma[simp]: "(abs (i::int) = 1) = (i =1 ∨ i = -1)"  by arith
    lemma mirror_unified:
      assumes unif: "isunified p"
      shows "isunified (mirror p)"
      using unif
    proof (induct p rule: mirror.induct, simp_all)
      case (goal1 c r z)
      from prems have zz: "z = Cst 0" by (cases z, simp_all)
      then show ?case using prems
        by (auto simp add: islinintterm_eq_islint islint_def)
    next
      case (goal2 c r z)
      from prems have zz: "z = Cst 0" by (cases z, simp_all)
      then show ?case using prems
        by (auto simp add: islinintterm_eq_islint islint_def)
    next
      case (goal3 d c r) show ?case using prems by (auto simp add: islinintterm_eq_islint islint_def)
    next
      case (goal4 d c r) show ?case using prems  by (auto simp add: islinintterm_eq_islint islint_def)
    next
     case (goal5 c r z)
      from prems have zz: "z = Cst 0" by (cases z, simp_all)
      then show ?case using prems
        by (auto simp add: islinintterm_eq_islint islint_def)
    qed

    (* relationship between plusinf and minusinf *)
    lemma plusinf_eq_minusinf_mirror:
      assumes unifp: "isunified p"
      shows "(qinterp (x#ats) (plusinf p)) = (qinterp ((- x)#ats) (minusinf (mirror p)))"
    using unifp unified_islinform[OF unifp]
    proof (induct p rule: islinform.induct, simp_all)
      case (goal1 t z)
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have ?case using prems
          by (cases n, auto simp add: nth_pos2
              intterm_novar0[OF lininr, where x="x" and y="-x"] )}
      ultimately show ?case by blast

    next
      case (goal2 t z)
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have ?case using prems
          by (cases n, auto simp add: nth_pos2
              intterm_novar0[OF lininr, where x="x" and y="-x"] )}
      ultimately show ?case by blast
    next
      case (goal3 d t)

     from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])

        have ?case using prems
          by (cases n, simp_all add: nth_pos2
              intterm_novar0[OF lininr, where x="x" and y="-x"] )}
      ultimately show ?case by blast
    next

      case (goal4 d t)

     from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])

        have ?case using prems
          by (cases n, simp_all add: nth_pos2
              intterm_novar0[OF lininr, where x="x" and y="-x"] )}
      ultimately show ?case by blast
    next
      case (goal5 t z)
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have ?case using prems
          by (cases n, auto simp add: nth_pos2
              intterm_novar0[OF lininr, where x="x" and y="-x"] )}
      ultimately show ?case by blast
    qed

    (* relationship between aset abd bset *)
    lemma aset_eq_bset_mirror:
      assumes unifp: "isunified p"
      shows "set (aset p) = set (map lin_neg (bset (mirror p)))"
    using unifp
    proof(induct p rule: mirror.induct)
      case (1 c r z)
      from prems have zz: "z = Cst 0"
        by (cases z, auto)
      from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def)
      have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def)
      show ?case  using prems linr zz apply (auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1)
        by (simp add: negm1eq1 lin_neg_idemp sym[OF lin_neg_lin_add_distrib] lin_add_lin)
    next
      case (2 c r z)   from prems have zz: "z = Cst 0"
        by (cases z, auto)
      from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def)
      have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def)
      show ?case  using prems linr zz
        by (auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1)
      (simp add: negm1eq1 lin_neg_idemp sym[OF lin_neg_lin_add_distrib] lin_add_lin lin_neg_lin)

    next
      case (5 c r z)  from prems have zz: "z = Cst 0"
        by (cases z, auto)
      from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def)
      have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def)
      show ?case  using prems linr zz
        by(auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1)

    qed simp_all

    (* relationship between aset abd bset 2*)
    lemma aset_eq_bset_mirror2:
      assumes unifp: "isunified p"
      shows "aset p = map lin_neg (bset (mirror p))"
    using unifp
    proof(induct p rule: mirror.induct)
      case (1 c r z)
      from prems have zz: "z = Cst 0"
        by (cases z, auto)
      from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def)
      have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def)
      show ?case  using prems linr zz
        apply (simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1)
        apply (simp add: negm1eq1 lin_neg_idemp sym[OF lin_neg_lin_add_distrib] lin_add_lin)
        by arith
    next
      case (2 c r z)   from prems have zz: "z = Cst 0"
        by (cases z, auto)
      from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def)
      have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def)
      show ?case  using prems linr zz
        by(auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1)
        (simp add: negm1eq1 lin_neg_idemp sym[OF lin_neg_lin_add_distrib] lin_add_lin lin_neg_lin)

    next
      case (5 c r z)  from prems have zz: "z = Cst 0"
        by (cases z, auto)
      from prems zz have lincnr: "islinintterm (Add (Mult (Cst c) (Var 0)) r)" by simp
      have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      have neg1eqm1: "Cst 1 = lin_neg (Cst -1)" by (simp add: lin_neg_def)
      have negm1eq1: "Cst -1 = lin_neg (Cst 1)" by (simp add: lin_neg_def)
      show ?case  using prems linr zz
        by(auto simp add: lin_neg_lin_add_distrib lin_neg_idemp neg1eqm1)

    qed simp_all

    (* mirror preserves divlcm *)
    lemma divlcm_mirror_eq:
      assumes unifp: "isunified p"
      shows "divlcm p = divlcm (mirror p)"
      using unifp
    by (induct p rule: mirror.induct) auto

    (* mirror almost preserves semantics *)
    lemma mirror_interp:
      assumes unifp: "isunified p"
      shows "(qinterp (x#ats) p) = (qinterp ((- x)#ats) (mirror p))" (is "?P x = ?MP (-x)")
    using unifp unified_islinform[OF unifp]
    proof (induct p rule: islinform.induct)
      case (1 t z)
      from prems have zz: "z = 0" by simp
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have ?case using prems zz
          by (cases n) (simp_all add: nth_pos2
            intterm_novar0[OF lininr, where x="x" and y="-x"])
      }
      ultimately show ?case by blast
    next
      case (2 t z)
      from prems have zz: "z = 0" by simp
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have ?case using prems zz
          by (cases n) (simp_all add: nth_pos2
            intterm_novar0[OF lininr, where x="x" and y="-x"])
      }
      ultimately show ?case by blast
    next
      case (3 d t)
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have ?case
          using prems linr
          by (cases n) (simp_all add: nth_pos2
            intterm_novar0[OF lininr, where x="x" and y="-x"])
      }
      ultimately show ?case by blast
    next

      case (6 d t)
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have ?case
          using prems linr
          by (cases n) (simp_all add: nth_pos2
            intterm_novar0[OF lininr, where x="x" and y="-x"])
      }
      ultimately show ?case by blast
    next
      case (7 t z)
      from prems have zz: "z = 0" by simp
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have ?case using prems zz
          by (cases n) (simp_all add: nth_pos2
            intterm_novar0[OF lininr, where x="x" and y="-x"])
      }
      ultimately show ?case by blast
    qed simp_all

    lemma mirror_interp2:
      assumes unifp: "islinform p"
      shows "(qinterp (x#ats) p) = (qinterp ((- x)#ats) (mirror p))" (is "?P x = ?MP (-x)")
    using unifp
    proof (induct p rule: islinform.induct)
      case (1 t z)
      from prems have zz: "z = 0" by simp
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have ?case using prems zz
          by (cases n) (simp_all add: nth_pos2
            intterm_novar0[OF lininr, where x="x" and y="-x"])
      }
      ultimately show ?case by blast
    next
      case (2 t z)
      from prems have zz: "z = 0" by simp
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have ?case using prems zz
          by (cases n) (simp_all add: nth_pos2
            intterm_novar0[OF lininr, where x="x" and y="-x"])
      }
      ultimately show ?case by blast
    next
      case (3 d t)
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have ?case
          using prems linr
          by (cases n) (simp_all add: nth_pos2
            intterm_novar0[OF lininr, where x="x" and y="-x"])
      }
      ultimately show ?case by blast
    next

      case (6 d t)
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have ?case
          using prems linr
          by (cases n) (simp_all add: nth_pos2
            intterm_novar0[OF lininr, where x="x" and y="-x"])
      }
      ultimately show ?case by blast
    next
      case (7 t z)
      from prems have zz: "z = 0" by simp
      from prems
      have lint: "islinintterm t" by simp
      then have "(∃ i n r. t = Add (Mult (Cst i) (Var n) ) r) ∨ (∃ i. t = Cst i)"
        by (induct t rule: islinintterm.induct) auto
      moreover{ assume "∃ i. t = Cst i" then have ?case using prems by auto }
      moreover
      { assume "∃ i n r. t = Add (Mult (Cst i) (Var n) ) r"
        then obtain "i" "n" "r" where
          inr_def: "t = Add (Mult (Cst i) (Var n) ) r"
          by blast
        with lint have lininr: "islinintterm (Add (Mult (Cst i) (Var n) ) r)"
          by simp
        have linr: "islinintterm r"
          by (rule islinintterm_subt[OF lininr])
        have ?case using prems zz
          by (cases n) (simp_all add: nth_pos2
            intterm_novar0[OF lininr, where x="x" and y="-x"])
      }
      ultimately show ?case by blast
    qed simp_all

    (* mirror preserves existence *)
    lemma mirror_ex:
      assumes unifp: "isunified p"
      shows "(∃ x. (qinterp (x#ats) p)) = (∃ y. (qinterp (y#ats) (mirror p)))"
      (is "(∃ x. ?P x) = (∃ y. ?MP y)")
    proof
      assume "∃ x. ?P x"
      then obtain "x" where px:"?P x" by blast
      have "?MP (-x)"
        using px
        by(simp add: mirror_interp[OF unifp, where x="x"])
      then show "∃ y. ?MP y" by blast
    next
      assume "∃ y. ?MP y"
      then obtain "y" where mpy: "?MP y" by blast
      have "?P (-y)"
        using mpy
        by (simp add: mirror_interp[OF unifp, where x="-y"])
      then show "∃ x. ?P x" by blast
    qed

    lemma mirror_ex2:
      assumes unifp: "isunified p"
      shows "qinterp ats (QEx p) = qinterp ats (QEx (mirror p))"
    using mirror_ex[OF unifp] by simp

    (* Cooper's theorem in its plusinfinity version *)
    lemma cooper_pi_eq:
      assumes unifp : "isunified p"
      shows "(∃ x. qinterp (x#ats) p) =
      ((∃ j ∈ {1 .. (divlcm p)}. qinterp (-j#ats) (plusinf p)) ∨
      (∃ j ∈ {1 .. (divlcm p)}. ∃ b ∈ set (aset p).
      qinterp (((I_intterm (a#ats) b) - j)#ats) p))"
      (is "(∃ x. ?P x) = ((∃ j∈ {1 .. ?d}. ?PP (-j)) ∨ (∃ j ∈ ?D. ∃ b∈ ?A. ?P (?I a b - j)))")
    proof-
      have unifmp: "isunified (mirror p)" by (rule mirror_unified[OF unifp])
      have th1:
        "(∃ j∈ {1 .. ?d}. ?PP (-j)) = (∃ j∈ {1..?d}.  qinterp (j # ats) (minusinf (mirror p)))"
        by (simp add: plusinf_eq_minusinf_mirror[OF unifp])
      have dth: "?d = divlcm (mirror p)"
        by (rule divlcm_mirror_eq[OF unifp])
      have "(∃ j ∈ ?D. ∃ b∈ ?A. ?P (?I a b - j)) =
        (∃ j∈ ?D. ∃ b ∈ set (map lin_neg (bset (mirror p))). ?P (?I a b - j))"
        by (simp only: aset_eq_bset_mirror[OF unifp])
      also have "… = (∃ j∈ ?D. ∃ b ∈ set (bset (mirror p)). ?P (?I a (lin_neg b) - j))"
        by simp
      also have "… = (∃ j∈ ?D. ∃ b ∈ set (bset (mirror p)). ?P (-(?I a b + j)))"
      proof
        assume "∃j∈{1..divlcm p}.
          ∃b∈set (bset (mirror p)). qinterp ((I_intterm (a # ats) (lin_neg b) - j) # ats) p"
        then
        obtain "j" and "b" where
          pbmj: "j∈ ?D ∧ b∈ set (bset (mirror p)) ∧ ?P (?I a (lin_neg b) - j)" by blast
        then have linb: "islinintterm b"
          by (auto simp add:bset_lin[OF unifmp])
        from linb pbmj have "?P (-(?I a b + j))" by (simp add: lin_neg_corr)
        then show "∃ j∈ ?D. ∃ b ∈ set (bset (mirror p)). ?P (-(?I a b + j))"
          using pbmj
          by auto
      next
        assume "∃ j∈ ?D. ∃ b ∈ set (bset (mirror p)). ?P (-(?I a b + j))"
        then obtain "j" and "b" where
          pbmj: "j∈ ?D ∧ b∈ set (bset (mirror p)) ∧ ?P (-(?I a b + j))"
          by blast
        then have linb: "islinintterm b"
          by (auto simp add:bset_lin[OF unifmp])
        from linb pbmj have "?P (?I a (lin_neg b) - j)"
          by (simp add: lin_neg_corr)
        then show "∃ j∈ ?D. ∃ b ∈ set (bset (mirror p)). ?P (?I a (lin_neg b) - j)"
          using pbmj by auto
      qed
      finally
      have bth: "(∃ j∈ ?D. ∃ b∈ ?A. ?P (?I a b - j)) =
        (∃j∈ ?D. ∃ b∈set (bset (mirror p)).
        qinterp ((I_intterm (a # ats) b + j) # ats) (mirror p))"
        by (simp add: mirror_interp[OF unifp] zadd_ac)
      from bth dth th1
      have "(∃ x. ?P x) = (∃ x. qinterp (x#ats) (mirror p))"
        by (simp add: mirror_ex[OF unifp])
      also have "… = ((∃j∈{1..divlcm (mirror p)}. qinterp (j # ats) (minusinf (mirror p))) ∨
        (∃j∈{1..divlcm (mirror p)}.
        ∃b∈set (bset (mirror p)). qinterp ((I_intterm (a # ats) b + j) # ats) (mirror p)))"
        (is "(∃ x. ?MP x) = ((∃ j∈ ?DM. ?MPM j) ∨ (∃ j ∈ ?DM. ∃ b∈ ?BM. ?MP (?I a b + j)))")
        by (rule cooper_mi_eq[OF unifmp])
      also
      have "… = ((∃ j∈ ?D. ?PP (-j)) ∨ (∃ j ∈ ?D. ∃ b∈ ?BM. ?MP (?I a b + j)))"
        using bth th1 dth by simp
      finally  show ?thesis using sym[OF bth] by simp
    qed

    (* substitution of a term into a Qfree formula, substitution of Bound 0 by i*)

    consts subst_it:: "intterm => intterm => intterm"
    primrec
    "subst_it i (Cst b) = Cst b"
    "subst_it i (Var n) = (if n = 0 then i else Var n)"
    "subst_it i (Neg it) = Neg (subst_it i it)"
    "subst_it i (Add it1 it2) = Add (subst_it i it1) (subst_it i it2)"
    "subst_it i (Sub it1 it2) = Sub (subst_it i it1) (subst_it i it2)"
    "subst_it i (Mult it1 it2) = Mult (subst_it i it1) (subst_it i it2)"

    (* subst_it preserves semantics *)
    lemma subst_it_corr:
    "I_intterm (a#ats) (subst_it i t) = I_intterm ((I_intterm (a#ats) i)#ats) t"
    by (induct t rule: subst_it.induct, simp_all add: nth_pos2)

    consts subst_p:: "intterm => QF => QF"
    primrec
    "subst_p i (Le it1 it2) = Le (subst_it i it1) (subst_it i it2)"
    "subst_p i (Lt it1 it2) = Lt (subst_it i it1) (subst_it i it2)"
    "subst_p i (Ge it1 it2) = Ge (subst_it i it1) (subst_it i it2)"
    "subst_p i (Gt it1 it2) = Gt (subst_it i it1) (subst_it i it2)"
    "subst_p i (Eq it1 it2) = Eq (subst_it i it1) (subst_it i it2)"
    "subst_p i (Divides d t) = Divides (subst_it i d) (subst_it i t)"
    "subst_p i T = T"
    "subst_p i F = F"
    "subst_p i (And p q) = And (subst_p i p) (subst_p i q)"
    "subst_p i (Or p q) = Or (subst_p i p) (subst_p i q)"
    "subst_p i (Imp p q) = Imp (subst_p i p) (subst_p i q)"
    "subst_p i (Equ p q) = Equ (subst_p i p) (subst_p i q)"
    "subst_p i (NOT p) = (NOT (subst_p i p))"

    (* subs_p preserves correctness *)
    lemma subst_p_corr:
      assumes qf: "isqfree p"
      shows "qinterp (a # ats) (subst_p i p) = qinterp ((I_intterm (a#ats) i)#ats) p "
      using qf
    by (induct p rule: subst_p.induct) (simp_all add: subst_it_corr)

    (* novar0 p is true if the fomula doese not depend on the quantified variable*)
    consts novar0I:: "intterm => bool"
    primrec
    "novar0I (Cst i) = True"
    "novar0I (Var n) = (n > 0)"
    "novar0I (Neg a) = (novar0I a)"
    "novar0I (Add a b) = (novar0I a ∧ novar0I b)"
    "novar0I (Sub a b) = (novar0I a ∧ novar0I b)"
    "novar0I (Mult a b) = (novar0I a ∧ novar0I b)"

    consts novar0:: "QF => bool"
    recdef novar0 "measure size"
    "novar0 (Lt a b) = (novar0I a ∧ novar0I b)"
    "novar0 (Gt a b) = (novar0I a ∧ novar0I b)"
    "novar0 (Le a b) = (novar0I a ∧ novar0I b)"
    "novar0 (Ge a b) = (novar0I a ∧ novar0I b)"
    "novar0 (Eq a b) = (novar0I a ∧ novar0I b)"
    "novar0 (Divides a b) = (novar0I a ∧ novar0I b)"
    "novar0 T = True"
    "novar0 F = True"
    "novar0 (NOT p) = novar0 p"
    "novar0 (And p q) = (novar0 p ∧ novar0 q)"
    "novar0 (Or p q)  = (novar0 p ∧ novar0 q)"
    "novar0 (Imp p q) = (novar0 p ∧ novar0 q)"
    "novar0 (Equ p q) = (novar0 p ∧ novar0 q)"
    "novar0 p = False"

    (* Interpretation of terms, that doese not depend on Var 0 *)
    lemma I_intterm_novar0:
      assumes nov0: "novar0I x"
      shows "I_intterm (a#ats) x = I_intterm (b#ats) x"
    using nov0
    by (induct x) (auto simp add: nth_pos2)

    (* substition is meaningless for term independent of Var 0*)
    lemma subst_p_novar0_corr:
    assumes qfp: "isqfree p"
      and nov0: "novar0I i"
      shows "qinterp (a#ats) (subst_p i p) = qinterp (I_intterm (b#ats) i#ats) p"
    proof-
      have "qinterp (a#ats) (subst_p i p) = qinterp (I_intterm (a#ats) i#ats) p"
        by (rule subst_p_corr[OF qfp])
      moreover have "I_intterm (a#ats) i#ats = I_intterm (b#ats) i#ats"
        by (simp add: I_intterm_novar0[OF nov0, where a="a" and b="b"])
      ultimately show ?thesis by simp
    qed

    (* linearity and independence on Var 0*)
    lemma lin_novar0:
      assumes linx: "islinintterm x"
      and nov0: "novar0I x"
      shows "∃ n > 0. islintn(n,x)"
    using linx nov0
    by (induct x rule: islinintterm.induct) auto

    lemma lintnpos_novar0:
     assumes  npos: "n > 0"
      and linx: "islintn(n,x)"
      shows "novar0I x"
    using npos linx
    by (induct n x rule: islintn.induct) auto

    (* lin_add preserves independence on Var 0*)
    lemma lin_add_novar0:
      assumes nov0a: "novar0I a"
      and nov0b : "novar0I b"
      and lina : "islinintterm a"
      and linb: "islinintterm b"
      shows "novar0I (lin_add (a,b))"
    proof-
      have "∃ na > 0. islintn(na, a)" by (rule lin_novar0[OF lina nov0a])
      then obtain "na" where na: "na > 0 ∧ islintn(na,a)" by blast
      have "∃ nb > 0. islintn(nb, b)" by (rule lin_novar0[OF linb nov0b])
      then obtain "nb" where nb: "nb > 0 ∧ islintn(nb,b)" by blast
      from na have napos: "na > 0" by simp
      from na have linna: "islintn(na,a)" by simp
      from nb have nbpos: "nb > 0" by simp
      from nb have linnb: "islintn(nb,b)" by simp
      have "min na nb ≤ min na nb" by simp
      then have "islintn (min na nb, lin_add(a,b))" by (simp add: lin_add_lint[OF linna linnb])
      moreover have "min na nb > 0" using napos nbpos by (simp add: min_def)
      ultimately show ?thesis by (simp only: lintnpos_novar0)
    qed

    (* lin__mul preserves independence on Var 0*)
    lemma lin_mul_novar0:
      assumes linx: "islinintterm x"
      and nov0: "novar0I x"
      shows "novar0I (lin_mul(i,x))"
      using linx nov0
    proof (induct i x rule: lin_mul.induct, auto)
      case (goal1 c c' n r)
      from prems have lincnr: "islinintterm (Add (Mult (Cst c') (Var n)) r)" by simp
      have "islinintterm r" by (rule islinintterm_subt[OF lincnr])
      then show ?case using prems by simp
    qed

    (* lin_neg preserves indepenednce on Var 0*)
    lemma lin_neg_novar0:
      assumes linx: "islinintterm x"
      and nov0: "novar0I x"
      shows "novar0I (lin_neg x)"
    by (auto simp add: lin_mul_novar0 linx nov0 lin_neg_def)

    (* subterms of linear terms are independent on Var 0*)
    lemma intterm_subt_novar0:
      assumes lincnr: "islinintterm (Add (Mult (Cst c) (Var n)) r)"
      shows "novar0I r"
    proof-
      have cnz: "c ≠ 0" by (rule islinintterm_cnz[OF lincnr])
      have "islintn(0,Add (Mult (Cst c) (Var n)) r)" using lincnr
        by (simp only: islinintterm_eq_islint islint_def)
      then have "islintn (n+1,r)" by auto
      moreover have "n+1 >0 " by arith
      ultimately show ?thesis
        using lintnpos_novar0
        by auto
    qed

    (* decrease the De-Bruijn indices*)
    consts decrvarsI:: "intterm => intterm"
    primrec
    "decrvarsI (Cst i) = (Cst i)"
    "decrvarsI (Var n) = (Var (n - 1))"
    "decrvarsI (Neg a) = (Neg (decrvarsI a))"
    "decrvarsI (Add a b) = (Add (decrvarsI a) (decrvarsI b))"
    "decrvarsI (Sub a b) = (Sub (decrvarsI a) (decrvarsI b))"
    "decrvarsI (Mult a b) = (Mult (decrvarsI a) (decrvarsI b))"

    (* One can decrease the indics for terms and formulae independent on Var 0*)
    lemma intterm_decrvarsI:
      assumes nov0: "novar0I t"
      shows "I_intterm (a#ats) t = I_intterm ats (decrvarsI t)"
    using nov0
    by (induct t) (auto simp add: nth_pos2)

    consts decrvars:: "QF => QF"
    primrec
    "decrvars (Lt a b) = (Lt (decrvarsI a) (decrvarsI b))"
    "decrvars (Gt a b) = (Gt (decrvarsI a) (decrvarsI b))"
    "decrvars (Le a b) = (Le (decrvarsI a) (decrvarsI b))"
    "decrvars (Ge a b) = (Ge (decrvarsI a) (decrvarsI b))"
    "decrvars (Eq a b) = (Eq (decrvarsI a) (decrvarsI b))"
    "decrvars (Divides a b) = (Divides (decrvarsI a) (decrvarsI b))"
    "decrvars T = T"
    "decrvars F = F"
    "decrvars (NOT p) = (NOT (decrvars p))"
    "decrvars (And p q) = (And (decrvars p) (decrvars q))"
    "decrvars (Or p q)  = (Or (decrvars p) (decrvars q))"
    "decrvars (Imp p q) = (Imp (decrvars p) (decrvars q))"
    "decrvars (Equ p q) = (Equ (decrvars p) (decrvars q))"

    (* decrvars preserves quantifier freeness*)
    lemma decrvars_qfree: "isqfree p ==> isqfree (decrvars p)"
    by (induct p rule: isqfree.induct, auto)

    lemma novar0_qfree: "novar0 p ==> isqfree p"
    by (induct p) auto

    lemma qinterp_novar0:
      assumes nov0: "novar0 p"
      shows "qinterp (a#ats) p = qinterp ats (decrvars p)"
    using nov0
    by(induct p) (simp_all add: intterm_decrvarsI)

    (* All elements of bset p doese not depend on Var 0*)
    lemma bset_novar0:
      assumes unifp: "isunified p"
      shows "∀ b∈ set (bset p). novar0I b "
      using unifp
    proof(induct p rule: bset.induct)
      case (1 c r z)
      from prems have zz: "z = Cst 0" by (cases "z", auto)
        from prems zz have lincnr: "islinintterm(Add (Mult (Cst c) (Var 0)) r)" by simp
        have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
        have novar0r: "novar0I r" by (rule intterm_subt_novar0[OF lincnr])
        from prems zz have "c = 1 ∨ c = -1" by auto
        moreover
        {
          assume c1: "c=1"
          have lin1: "islinintterm (Cst 1)" by simp
          have novar01: "novar0I (Cst 1)" by simp
          then have ?case
            using prems zz novar0r lin1 novar01
            by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin)
        }
        moreover
        {
          assume c1: "c= -1"
          have lin1: "islinintterm (Cst -1)" by simp
          have novar01: "novar0I (Cst -1)" by simp
          then have ?case
            using prems zz novar0r lin1 novar01
            by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin)
        }
        ultimately show ?case by blast
    next
      case (2 c r z)
      from prems have zz: "z = Cst 0" by (cases "z", auto)
        from prems zz have lincnr: "islinintterm(Add (Mult (Cst c) (Var 0)) r)" by simp
        have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
        have novar0r: "novar0I r" by (rule intterm_subt_novar0[OF lincnr])
        from prems zz have "c = 1 ∨ c = -1" by auto
        moreover
        {
          assume c1: "c=1"
          have lin1: "islinintterm (Cst 1)" by simp
          have novar01: "novar0I (Cst 1)" by simp
          then have ?case
            using prems zz novar0r lin1 novar01
            by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin)
        }
        moreover
        {
          assume c1: "c= -1"
          have lin1: "islinintterm (Cst -1)" by simp
          have novar01: "novar0I (Cst -1)" by simp
          then have ?case
            using prems zz novar0r lin1 novar01
            by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin)
        }
        ultimately show ?case by blast
    next
      case (3 c r z)
      from prems have zz: "z = Cst 0" by (cases "z", auto)
        from prems zz have lincnr: "islinintterm(Add (Mult (Cst c) (Var 0)) r)" by simp
        have linr: "islinintterm r" by (rule islinintterm_subt[OF lincnr])
        have novar0r: "novar0I r" by (rule intterm_subt_novar0[OF lincnr])
        from prems zz have "c = 1 ∨ c = -1" by auto
        moreover
        {
          assume c1: "c=1"
          have lin1: "islinintterm (Cst 1)" by simp
          have novar01: "novar0I (Cst 1)" by simp
          then have ?case
            using prems zz novar0r lin1 novar01
            by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin)
        }
        moreover
        {
          assume c1: "c= -1"
          have lin1: "islinintterm (Cst -1)" by simp
          have novar01: "novar0I (Cst -1)" by simp
          then have ?case
            using prems zz novar0r lin1 novar01
            by (auto simp add: lin_add_novar0 lin_neg_novar0 linr lin_neg_lin)
        }
        ultimately show ?case by blast
    qed auto

    (* substitution preserves independence on Var 0*)
    lemma subst_it_novar0:
      assumes nov0x: "novar0I x"
      shows "novar0I (subst_it x t)"
      using nov0x
      by (induct t) auto

    lemma subst_p_novar0:
      assumes nov0x:"novar0I x"
      and qfp: "isqfree p"
      shows "novar0 (subst_p x p)"
      using nov0x qfp
      by (induct p rule: novar0.induct) (simp_all add: subst_it_novar0)

    (* linearize preserves independence on Var 0 *)
    lemma linearize_novar0:
      assumes nov0t: "novar0I t "
      shows "!! t'. linearize t = Some t' ==> novar0I t'"
    using nov0t
    proof(induct t rule: novar0I.induct)
      case (Neg a)
      let ?la = "linearize a"
      from prems have "∃ a'. ?la = Some a'" by (cases ?la, auto)
      then obtain "a'" where "?la = Some a'" by blast
      with prems have nv0a':"novar0I a'" by simp
      have "islinintterm a'" using prems by (simp add: linearize_linear)
      with nv0a' have "novar0I (lin_neg a')"
        by (simp add: lin_neg_novar0)
      then
      show ?case using prems by simp
    next
      case (Add a b)
      let ?la = "linearize a"
      let ?lb = "linearize b"
      from prems have linab: "linearize (Add a b) = Some t'" by simp
      then have "∃ a'. ?la = Some a'" by (cases ?la) auto
      then obtain "a'" where "?la = Some a'" by blast
      with prems have nv0a':"novar0I a'" by simp
      have lina': "islinintterm a'" using prems by (simp add: linearize_linear)
      from linab have "∃ b'. ?lb = Some b'"
        by (cases ?la, auto simp add: measure_def inv_image_def) (cases ?lb, auto)
      then obtain "b'" where "?lb = Some b'" by blast
      with prems have nv0b':"novar0I b'" by simp
      have linb': "islinintterm b'" using prems by (simp add: linearize_linear)
      then show ?case using prems lina' linb' nv0a' nv0b'
        by (auto simp add: measure_def inv_image_def lin_add_novar0)
    next
      case (Sub a b)
        let ?la = "linearize a"
      let ?lb = "linearize b"
      from prems have linab: "linearize (Sub a b) = Some t'" by simp
      then have "∃ a'. ?la = Some a'" by (cases ?la) auto
      then obtain "a'" where "?la = Some a'" by blast
      with prems have nv0a':"novar0I a'" by simp
      have lina': "islinintterm a'" using prems by (simp add: linearize_linear)
      from linab have "∃ b'. ?lb = Some b'"
        by (cases ?la, auto simp add: measure_def inv_image_def) (cases ?lb, auto)
      then obtain "b'" where "?lb = Some b'" by blast
      with prems have nv0b':"novar0I b'" by simp
      have linb': "islinintterm b'" using prems by (simp add: linearize_linear)
      then show ?case using prems lina' linb' nv0a' nv0b'
        by (auto simp add:
          measure_def inv_image_def lin_add_novar0 lin_neg_novar0 lin_neg_lin)
    next
      case (Mult a b)
      let ?la = "linearize a"
      let ?lb = "linearize b"
      from prems have linab: "linearize (Mult a b) = Some t'" by simp
      then have "∃ a'. ?la = Some a'"
        by (cases ?la, auto simp add: measure_def inv_image_def)
      then obtain "a'" where "?la = Some a'" by blast
      with prems have nv0a':"novar0I a'" by simp
      have lina': "islinintterm a'" using prems by (simp add: linearize_linear)
      from prems linab have "∃ b'. ?lb = Some b'"
        apply (cases ?la, auto simp add: measure_def inv_image_def)
        by (cases "a'",auto simp add: measure_def inv_image_def) (cases ?lb, auto)+
      then obtain "b'" where "?lb = Some b'" by blast
      with prems have nv0b':"novar0I b'" by simp
      have linb': "islinintterm b'" using prems by (simp add: linearize_linear)
      then show ?case using prems lina' linb' nv0a' nv0b'
        by (cases "a'",auto simp add: measure_def inv_image_def lin_mul_novar0)
      (cases "b'",auto simp add: measure_def inv_image_def lin_mul_novar0)
    qed auto

    (* simplification of formulae *)
    consts psimpl :: "QF => QF"
    recdef psimpl "measure size"
    "psimpl (Le l r) =
      (case (linearize (Sub l r)) of
       None => Le l r
     | Some x => (case x of
           Cst i => (if i ≤ 0 then T else F)
         | _ => (Le x (Cst 0))))"
    "psimpl (Eq l r) =
      (case (linearize (Sub l r)) of
       None => Eq l r
     | Some x => (case x of
           Cst i => (if i = 0 then T else F)
         | _ => (Eq x (Cst 0))))"

    "psimpl (Divides (Cst d) t) =
      (case (linearize t) of
      None => (Divides (Cst d) t)
      | Some c => (case c of
         Cst i => (if d dvd i then T else F)
       | _ =>  (Divides (Cst d) c)))"

    "psimpl (And p q) =
      (let p'= psimpl p
      in (case p' of
           F => F
          |T => psimpl q
          | _ => let q' = psimpl q
                 in (case q' of
                         F => F
                       | T => p'
                       | _ => (And p' q'))))"

    "psimpl (Or p q) =
      (let p'= psimpl p
      in (case p' of
            T => T
          | F => psimpl q
          | _ => let q' = psimpl q
                 in (case q' of
                         T => T
                       | F => p'
                       | _ => (Or p' q'))))"

    "psimpl (Imp p q) =
      (let p'= psimpl p
      in (case p' of
           F => T
          |T => psimpl q
          | NOT p1 => let q' = psimpl q
                 in (case q' of
                         F => p1
                       | T => T
                       | _ => (Or p1 q'))
          | _ => let q' = psimpl q
                 in (case q' of
                         F => NOT p'
                       | T => T
                       | _ => (Imp p' q'))))"

    "psimpl (Equ p q) =
      (let p'= psimpl p ; q' = psimpl q
      in (case p' of
            T => q'
          | F => (case q' of
                      T => F
                    | F => T
                    | NOT q1 => q1
                    | _ => NOT q')
          | NOT p1 =>  (case q' of
                      T => p'
                    | F => p1
                    | NOT q1 => (Equ p1 q1)
                    | _ => (Equ p' q'))
          | _ => (case q' of
                      T => p'
                    | F => NOT p'
                    | _ => (Equ p' q'))))"

    "psimpl (NOT p) =
      (let p' = psimpl p
      in ( case p' of
           F => T
         | T => F
         | NOT p1 => p1
         | _ => (NOT p')))"
    "psimpl p = p"

    (* psimpl preserves semantics *)
    lemma psimpl_corr: "qinterp ats p = qinterp ats (psimpl p)"
    proof(induct p rule: psimpl.induct)
      case (1 l r)
      have "(∃ lx. linearize (Sub l r) = Some lx) ∨ (linearize (Sub l r) = None)" by auto
      moreover
      {
        assume lin: "∃ lx. linearize (Sub l r) = Some lx"
        from lin obtain "lx" where lx: "linearize (Sub l r) = Some lx" by blast
        from lx have "I_intterm ats (Sub l r) = I_intterm ats lx"
          by (rule linearize_corr[where t="Sub l r" and t'= "lx"])
        then have feq: "qinterp ats (Le l r) = qinterp ats (Le lx (Cst 0))" by (simp , arith)
        from lx have lxlin: "islinintterm lx" by (rule linearize_linear)
        from lxlin feq have ?case
          proof-
            have "(∃ i. lx = Cst i) ∨ (¬ (∃ i. lx = Cst i))" by blast
            moreover
            {
              assume lxcst: "∃ i. lx = Cst i"
              from lxcst obtain "i" where lxi: "lx = Cst i" by blast
              with feq have "qinterp ats (Le l r) = (i ≤ 0)" by simp
              then have ?case using prems by (simp add: measure_def inv_image_def)
            }
            moreover
            {
              assume "(¬ (∃ i. lx = Cst i))"
              then have "(case lx of
                Cst i => (if i ≤ 0 then T else F)
                | _ => (Le lx (Cst 0))) = (Le lx (Cst 0))"
                by (case_tac "lx::intterm", auto)
              with prems lxlin feq have ?case by (auto simp add: measure_def inv_image_def)
            }
            ultimately show ?thesis  by blast
          qed
      }
      moreover
      {
        assume "linearize (Sub l r) = None"
        then have ?case using prems by simp
      }
      ultimately show ?case by blast

    next
      case (2 l r)
      have "(∃ lx. linearize (Sub l r) = Some lx) ∨ (linearize (Sub l r) = None)" by auto
      moreover
      {
        assume lin: "∃ lx. linearize (Sub l r) = Some lx"
        from lin obtain "lx" where lx: "linearize (Sub l r) = Some lx" by blast
        from lx have "I_intterm ats (Sub l r) = I_intterm ats lx"
          by (rule linearize_corr[where t="Sub l r" and t'= "lx"])
        then have feq: "qinterp ats (Eq l r) = qinterp ats (Eq lx (Cst 0))" by (simp , arith)
        from lx have lxlin: "islinintterm lx" by (rule linearize_linear)
        from lxlin feq have ?case
          proof-
            have "(∃ i. lx = Cst i) ∨ (¬ (∃ i. lx = Cst i))" by blast
            moreover
            {
              assume lxcst: "∃ i. lx = Cst i"
              from lxcst obtain "i" where lxi: "lx = Cst i" by blast
              with feq have "qinterp ats (Eq l r) = (i = 0)" by simp
              then have ?case using prems by (simp add: measure_def inv_image_def)
            }
            moreover
            {
              assume "(¬ (∃ i. lx = Cst i))"
              then have "(case lx of
                Cst i => (if i = 0 then T else F)
                | _ => (Eq lx (Cst 0))) = (Eq lx (Cst 0))"
                by (case_tac "lx::intterm", auto)
              with prems lxlin feq have ?case by (auto simp add: measure_def inv_image_def)
            }
            ultimately show ?thesis  by blast
          qed
      }
      moreover
      {
        assume "linearize (Sub l r) = None"
        then have ?case using prems by simp
      }
      ultimately show ?case by blast

    next

      case (3 d t)
      have "(∃ lt. linearize t = Some lt) ∨ (linearize t = None)" by auto
      moreover
      {
        assume lin: "∃ lt. linearize t  = Some lt"
        from lin obtain "lt" where lt: "linearize t = Some lt" by blast
        from lt have "I_intterm ats t = I_intterm ats lt"
          by (rule linearize_corr[where t="t" and t'= "lt"])
        then have feq: "qinterp ats (Divides (Cst d) t) = qinterp ats (Divides (Cst d) lt)" by (simp)
        from lt have ltlin: "islinintterm lt" by (rule linearize_linear)
        from ltlin feq have ?case using prems  apply simp by (case_tac "lt::intterm", simp_all)
      }
      moreover
      {
        assume "linearize t = None"
        then have ?case using prems by simp
      }
      ultimately show ?case by blast

    next
      case (4 f g)

        let ?sf = "psimpl f"
      let ?sg = "psimpl g"
      show ?case using prems
        by (cases ?sf, simp_all add: Let_def measure_def inv_image_def)
      (cases ?sg, simp_all)+
    next
      case (5 f g)
          let ?sf = "psimpl f"
      let ?sg = "psimpl g"
      show ?case using prems
        apply (cases ?sf, simp_all add: Let_def measure_def inv_image_def)
        apply (cases ?sg, simp_all)
        apply (cases ?sg, simp_all)
        apply (cases ?sg, simp_all)
        apply (cases ?sg, simp_all)
        apply (cases ?sg, simp_all)
        apply (cases ?sg, simp_all)
        apply (cases ?sg, simp_all)
        apply blast
        apply (cases ?sg, simp_all)
        apply (cases ?sg, simp_all)
         apply (cases ?sg, simp_all)
       apply blast
        apply (cases ?sg, simp_all)
        by (cases ?sg, simp_all) (cases ?sg, simp_all)
    next
      case (6 f g)
      let ?sf = "psimpl f"
      let ?sg = "psimpl g"
      show ?case using prems
        apply(simp add: Let_def measure_def inv_image_def)
        apply(cases ?sf,simp_all)
        apply (simp_all add: Let_def measure_def inv_image_def)
        apply(cases ?sg, simp_all)
        apply(cases ?sg, simp_all)
        apply(cases ?sg, simp_all)
        apply(cases ?sg, simp_all)
        apply(cases ?sg, simp_all)
        apply(cases ?sg, simp_all)
        apply(cases ?sg, simp_all)
        apply blast
        apply blast
        apply blast
        apply blast
        apply blast
        apply blast
        apply blast
        apply blast
        apply blast
        apply blast
        apply blast
        apply blast
        apply blast
        apply(cases ?sg, simp_all)
        apply(cases ?sg, simp_all)
        apply(cases ?sg, simp_all)
        apply(cases ?sg, simp_all)
        apply(cases ?sg, simp_all)
        apply(cases ?sg, simp_all)
        done
    next
      case (7 f g)
      let ?sf = "psimpl f"
      let ?sg = "psimpl g"
      show ?case
        using prems
        by (cases ?sf, simp_all add: Let_def) (cases ?sg, simp_all)+
    next
      case (8 f) show ?case
        using prems
        apply (simp add: Let_def)
        by (case_tac "psimpl f", simp_all)
    qed simp_all

    (* psimpl preserves independence on Var 0*)
    lemma psimpl_novar0:
      assumes nov0p: "novar0 p"
      shows "novar0 (psimpl p)"
      using nov0p
    proof (induct p rule: psimpl.induct)
      case (1 l r)
      let ?ls = "linearize (Sub l r)"
      have "?ls = None ∨ (∃ x. ?ls = Some x)" by auto
      moreover
      {
        assume "?ls = None" then have ?case
          using prems by (simp add: measure_def inv_image_def)
      }
      moreover {
        assume "∃ x. ?ls = Some x"
        then obtain "x" where ls_d: "?ls = Some x" by blast
        from prems have "novar0I l" by simp
        moreover from prems have "novar0I r" by simp
        ultimately have nv0s: "novar0I (Sub l r)" by simp
        from prems have "novar0I x"
          by (simp add: linearize_novar0[OF nv0s, where t'="x"])
        then have ?case
          using prems
          by (cases "x") (auto simp add: measure_def inv_image_def)
      }
      ultimately show ?case by blast
    next
      case (2 l r)
      let ?ls = "linearize (Sub l r)"
      have "?ls = None ∨ (∃ x. ?ls = Some x)" by auto
      moreover
      {
        assume "?ls = None" then have ?case
          using prems by (simp add: measure_def inv_image_def)
      }
      moreover {
        assume "∃ x. ?ls = Some x"
        then obtain "x" where ls_d: "?ls = Some x" by blast
        from prems have "novar0I l" by simp
        moreover from prems have "novar0I r" by simp
        ultimately have nv0s: "novar0I (Sub l r)" by simp
        from prems have "novar0I x"
          by (simp add: linearize_novar0[OF nv0s, where t'="x"])
        then have ?case
          using prems
          by (cases "x") (auto simp add: measure_def inv_image_def)
      }
      ultimately show ?case by blast
    next
      case (3 d t)
      let ?lt = "linearize t"
      have "?lt = None ∨ (∃ x. ?lt = Some x)"  by auto
      moreover
      { assume "?lt = None" then have ?case using prems by simp }
      moreover {
        assume "∃x. ?lt = Some x"
        then obtain "x" where x_d: "?lt = Some x" by blast
        from prems have nv0t: "novar0I t" by simp
        with x_d have "novar0I x"
          by (simp add: linearize_novar0[OF nv0t])
        with prems have ?case
          by (cases "x") simp_all
      }
      ultimately show ?case by blast
    next
      case (4 f g)
      let ?sf = "psimpl f"
      let ?sg = "psimpl g"
      show ?case
        using prems
        by (cases ?sf, simp_all add: Let_def measure_def inv_image_def)
      (cases ?sg,simp_all)+
    next
      case (5 f g)
      let ?sf = "psimpl f"
      let ?sg = "psimpl g"
      show ?case
        using prems
        by (cases ?sf, simp_all add: Let_def measure_def inv_image_def)
      (cases ?sg,simp_all)+
    next
      case (6 f g)
      let ?sf = "psimpl f"
      let ?sg = "psimpl g"
      show ?case
        using prems
        by (cases ?sf, simp_all add: Let_def measure_def inv_image_def)
      (cases ?sg,simp_all)+
    next
      case (7 f g)
      let ?sf = "psimpl f"
      let ?sg = "psimpl g"
      show ?case
        using prems
        by (cases ?sf, simp_all add: Let_def measure_def inv_image_def)
      (cases ?sg,simp_all)+

    next
      case (8 f)
      let ?sf = "psimpl f"
      from prems have nv0sf:"novar0 ?sf" by simp
      show ?case using prems nv0sf
        by (cases ?sf, auto simp add: Let_def measure_def inv_image_def)
    qed simp_all

    (* implements a disj of p applied to all elements of the list*)
    consts explode_disj :: "(intterm list × QF) => QF"
    recdef explode_disj "measure (λ(is,p). length is)"
    "explode_disj ([],p) = F"
    "explode_disj (i#is,p) =
      (let pi = psimpl (subst_p i p)
       in ( case pi of
            T => T
           | F => explode_disj (is,p)
           | _ => (let r = explode_disj (is,p)
                   in (case r of
                          T => T
                        | F => pi
                        | _ => Or pi r))))"

    (* correctness theorem for one iteration of explode_disj *)
    lemma explode_disj_disj:
      assumes qfp: "isqfree p"
      shows "(qinterp (x#xs) (explode_disj(i#is,p))) =
      (qinterp (x#xs) (subst_p i p) ∨ (qinterp (x#xs) (explode_disj(is,p))))"
      using qfp
    proof-
      let ?pi = "psimpl (subst_p i p)"
      have pi: "qinterp (x#xs) ?pi = qinterp (x#xs) (subst_p i p)"
        by (simp add: psimpl_corr[where p="(subst_p i p)"])
      let ?dp = "explode_disj(is,p)"
      show ?thesis using pi
      proof (cases)
        assume "?pi= T ∨ ?pi = F"
        then show ?thesis using pi by (case_tac "?pi::QF", auto)

      next
        assume notTF: "¬ (?pi = T ∨ ?pi = F)"
        let ?dp = "explode_disj(is,p)"
        have dp_cases: "explode_disj(i#is,p) =
          (case (explode_disj(is,p)) of
          T => T
          | F => psimpl (subst_p i p)
          | _ => Or (psimpl (subst_p i p)) (explode_disj(is,p)))" using notTF
          by (cases "?pi")
        (simp_all add: Let_def cong del: QF.weak_case_cong)
        show ?thesis using pi dp_cases notTF
        proof(cases)
          assume "?dp = T ∨ ?dp = F"
          then show ?thesis
            using pi dp_cases
            by (cases "?dp") auto
        next
          assume "¬ (?dp = T ∨ ?dp = F)"
          then show ?thesis using pi dp_cases notTF
            by (cases ?dp) auto
        qed
      qed
    qed

    (* correctness theorem for explode_disj *)
    lemma explode_disj_corr:
      assumes qfp: "isqfree p"
      shows "(∃ x ∈ set xs. qinterp (a#ats) (subst_p x p)) =
      (qinterp (a#ats) (explode_disj(xs,p)))" (is "(∃ x ∈ set xs. ?P x) = (?DP a xs )")
      using qfp
      proof (induct xs)
        case Nil show ?case by simp
      next
        case (Cons y ys)
        have "(∃ x ∈ set (y#ys). ?P x) = (?P y ∨ (∃ x∈ set ys. ?P x))"
          by auto
        also have "… = (?P y ∨ ?DP a ys)" using "Cons.hyps" qfp by auto
        also have "… = ?DP a (y#ys)" using explode_disj_disj[OF qfp] by auto
        finally show ?case by simp
    qed

    (* explode_disj preserves independence on Var 0*)
    lemma explode_disj_novar0:
      assumes nov0xs: "∀x ∈ set xs. novar0I x"
      and qfp: "isqfree p"
      shows "novar0 (explode_disj (xs,p))"
      using nov0xs qfp
    proof (induct xs, auto simp add: Let_def)
      case (goal1 a as)
      let ?q = "subst_p a p"
      let ?qs = "psimpl ?q"
      have "?qs = T ∨ ?qs = F ∨ (?qs ≠ T ∨ ?qs ≠ F)" by simp
      moreover
      { assume "?qs = T"  then have ?case  by simp }
      moreover
      { assume "?qs = F"  then have ?case by simp }
      moreover
      {
        assume qsnTF: "?qs ≠ T ∧ ?qs ≠ F"
        let ?r = "explode_disj (as,p)"
        have nov0qs: "novar0 ?qs"
          using prems
          by (auto simp add: psimpl_novar0 subst_p_novar0)
        have "?r = T ∨ ?r = F ∨ (?r ≠ T ∨ ?r ≠ F)" by simp
        moreover
        { assume "?r = T" then have ?case by (cases ?qs) auto  }
        moreover
        { assume "?r = F"  then have ?case  using nov0qs by (cases ?qs, auto)  }
        moreover
        { assume "?r ≠ T ∧ ?r ≠ F"  then have ?case using nov0qs prems qsnTF
            by (cases ?qs, auto simp add: Let_def) (cases ?r,auto)+
        }
        ultimately have ?case by blast
      }
      ultimately show ?case by blast
    qed

    (* Some simple lemmas used for technical reasons *)
    lemma eval_Or_cases:
      "qinterp (a#ats) (case f of
           T => T
           | F => g
           | _ => (case g of
                         T => T
                       | F => f
                       | _ => Or f g)) = (qinterp (a#ats) f ∨ qinterp (a#ats) g)"
    proof-
      let ?result = "
        (case f of
        T => T
        | F => g
        | _ => (case g of
        T => T
        | F => f
        | _ => Or f g))"
      have "f = T ∨ f = F ∨ (f ≠ T ∧ f≠ F)" by auto
      moreover
      {
        assume fT: "f = T"
        then have ?thesis by auto
      }
      moreover
      {
        assume "f=F"
        then have ?thesis by auto
      }
      moreover
      {
        assume fnT: "f≠T"
          and fnF: "f≠F"
        have "g = T ∨ g = F ∨ (g ≠ T ∧ g≠ F)" by auto
        moreover
        {
          assume "g=T"
          then have ?thesis using fnT fnF by (cases f, auto)
        }
        moreover
        {
          assume "g=F"
          then have ?thesis using fnT fnF by (cases f, auto)
        }
        moreover
        {
          assume gnT: "g≠T"
            and gnF: "g≠F"
          then have "?result = (case g of
            T => T
            | F => f
            | _ => Or f g)"
            using fnT fnF
            by (cases f, auto)
          also have "… = Or f g"
            using gnT gnF
            by (cases g, auto)
          finally have "?result = Or f g" by simp
          then
          have  ?thesis by simp
        }
        ultimately have ?thesis by blast

      }

      ultimately show ?thesis by blast
    qed

    lemma or_case_novar0:
      assumes fnTF: "f ≠ T ∧ f ≠ F"
      and gnTF: "g ≠ T ∧ g ≠ F"
      and f0: "novar0 f"
      and g0: "novar0 g"
      shows "novar0
         (case f of T => T | F => g
         | _ => (case g of T => T | F => f | _ => Or f g))"
    using fnTF gnTF f0 g0
    by (cases f, auto) (cases g, auto)+

    (* An implementation of sets trough lists *)
    constdefs list_insert :: "'a => 'a list => 'a list"
      "list_insert x xs ≡ (if x mem xs then xs else x#xs)"

    lemma list_insert_set: "set (list_insert x xs) = set (x#xs)"
    by(induct xs) (auto simp add: list_insert_def)

    consts list_union :: "('a list × 'a list) => 'a list"

    recdef list_union "measure (λ(xs,ys). length xs)"
    "list_union ([], ys) = ys"
    "list_union (xs, []) = xs"
    "list_union (x#xs,ys) = list_insert x (list_union (xs,ys))"

    lemma list_union_set: "set (list_union(xs,ys)) = set (xs@ys)"
      by(induct xs ys rule: list_union.induct, auto simp add:list_insert_set)

    consts list_set ::"'a list => 'a list"
    primrec
      "list_set [] = []"
      "list_set (x#xs) = list_insert x (list_set xs)"

    lemma list_set_set: "set xs = set (list_set xs)"
    by (induct xs) (auto simp add: list_insert_set)

    consts iupto :: "int × int => int list"
    recdef iupto "measure (λ (i,j). nat (j - i +1))"
    "iupto(i,j) = (if j<i then [] else (i#(iupto(i+1,j))))"

    (* correctness theorem for iupto *)
    lemma iupto_set: "set (iupto(i,j)) = {i .. j}"
    proof(induct rule: iupto.induct)
      case (1 a b)
      show ?case
        using prems by (simp add: simp_from_to)
    qed

    consts all_sums :: "int × intterm list => intterm list"
    recdef all_sums "measure (λ(i,is). length is)"
    "all_sums (j,[]) = []"
    "all_sums (j,i#is) = (map (λx. lin_add (i,(Cst x))) (iupto(1,j))@(all_sums (j,is)))"
    (* all_sums preserves independence on Var 0*)
    lemma all_sums_novar0:
      assumes nov0xs: "∀ x∈ set xs. novar0I x"
      and linxs: "∀ x∈ set xs. islinintterm x "
      shows "∀ x∈ set (all_sums (d,xs)). novar0I x"
      using nov0xs linxs
    proof(induct d xs rule: all_sums.induct)
      case 1 show ?case by simp
    next
      case (2 j a as)
      have lina: "islinintterm a" using "2.prems" by auto
      have nov0a: "novar0I a" using "2.prems" by auto
      let ?ys = "map (λx. lin_add (a,(Cst x))) (iupto(1,j))"
      have nov0ys: "∀ y∈ set ?ys. novar0I y"
      proof-
        have linx: "∀ x ∈ set (iupto(1,j)). islinintterm (Cst x)" by simp
        have nov0x: "∀ x ∈ set (iupto(1,j)). novar0I (Cst x)" by simp
        with nov0a lina linx have "∀ x∈ set (iupto(1,j)). novar0I (lin_add (a,Cst x))"
          by (simp add: lin_add_novar0)
        then show ?thesis by auto
      qed
      from "2.prems"
      have linas: "∀u∈set as. islinintterm u" by auto
      from "2.prems" have nov0as: "∀u∈set as. novar0I u" by auto
      from "2.hyps" linas nov0as have nov0alls: "∀u∈set (all_sums (j, as)). novar0I u" by simp
      from nov0alls nov0ys have
        cs: "(∀ u∈ set (?ys@ (all_sums (j,as))). novar0I u)"
        by (simp only: sym[OF list_all_iff]) auto

      have "all_sums(j,a#as) = ?ys@(all_sums(j,as))"
        by simp
      then
      have "?case = (∀ x∈ set (?ys@ (all_sums (j,as))). novar0I x)"
        by auto
      with cs show ?case by blast
    qed

    (* correctness theorem for all_sums*)
    lemma all_sums_ex:
      "(∃ j∈ {1..d}. ∃ b∈ (set xs). P (lin_add(b,Cst j))) =
      (∃ x∈ set (all_sums (d,xs)). P x)"
    proof(induct d xs rule: all_sums.induct)
      case (1 a) show ?case by simp
    next
      case (2 a y ys)
      have "(∃ x∈ set (map (λx. lin_add (y,(Cst x))) (iupto(1,a))) . P x) =
        (∃ j∈ set (iupto(1,a)). P (lin_add(y,Cst j)))"
        by auto
      also have "… = (∃ j∈ {1..a}. P (lin_add(y,Cst j)))"
        by (simp only : iupto_set)
      finally
      have dsj1:"(∃j∈{1..a}. P (lin_add (y, Cst j))) = (∃x∈set (map (λx. lin_add (y, Cst x)) (iupto (1, a))). P x)" by simp

      from prems have "(∃ j∈ {1..a}. ∃ b∈ (set (y#ys)). P (lin_add(b,Cst j))) =
        ((∃ j∈ {1..a}. P (lin_add(y,Cst j))) ∨ (∃ j∈ {1..a}. ∃ b ∈ set ys. P (lin_add(b,Cst j))))" by auto
      also
      have " … = ((∃ j∈ {1..a}. P (lin_add(y,Cst j))) ∨ (∃ x∈ set (all_sums(a, ys)). P x))" using prems by simp
      also have "… = ((∃x∈set (map (λx. lin_add (y, Cst x)) (iupto (1, a))). P x) ∨ (∃x∈set (all_sums (a, ys)). P x))" using dsj1 by simp
      also have "… = (∃ x∈ (set (map (λx. lin_add (y, Cst x)) (iupto (1, a)))) ∪ (set (all_sums(a, ys))). P x)" by blast
      finally show ?case by simp
    qed

    (* explode_minf (p,B)  assumes that p is unified and B = bset p, it computes the rhs of cooper_mi_eq*)

    consts explode_minf :: "(QF × intterm list) => QF"
    recdef explode_minf "measure size"
    "explode_minf (q,B) =
      (let d = divlcm q;
           pm = minusinf q;
            dj1 = explode_disj ((map Cst (iupto (1, d))),pm)
       in (case dj1 of
             T => T
           | F => explode_disj (all_sums (d,B),q)
            | _ => (let dj2 = explode_disj (all_sums (d,B),q)
                  in ( case dj2 of
                         T => T
                       | F => dj1
                       | _ => Or dj1 dj2))))"

    (* The result of the rhs of cooper's theorem doese not depend on Var 0*)
    lemma explode_minf_novar0:
      assumes unifp : "isunified p"
      and bst: "set (bset p) = set B"
      shows "novar0 (explode_minf (p,B))"
    proof-
      let ?d = "divlcm p"
      let ?pm = "minusinf p"
      let ?dj1 = "explode_disj (map Cst (iupto(1,?d)),?pm)"

      have qfpm: "isqfree ?pm"  using unified_islinform[OF unifp] minusinf_qfree by simp
      have dpos: "?d >0" using unified_islinform[OF unifp] divlcm_pos by simp
      have "∀ x∈ set (map Cst (iupto(1,?d))). novar0I x" by auto
      then have dj1_nov0: "novar0 ?dj1" using qfpm explode_disj_novar0 by simp

      let ?dj2 = "explode_disj (all_sums (?d,B),p)"
      have
        bstlin: "∀b∈set B. islinintterm b"
        using bset_lin[OF unifp] bst
        by simp

      have bstnov0: "∀b∈set B. novar0I b"
        using bst bset_novar0[OF unifp] by simp
      have allsnov0: "∀x∈set (all_sums(?d,B)). novar0I x "
        by (simp add:all_sums_novar0[OF bstnov0 bstlin] )
      then have dj2_nov0: "novar0 ?dj2"
        using explode_disj_novar0 unified_isqfree[OF unifp] bst by simp
      have "?dj1 = T ∨ ?dj1 = F ∨ (?dj1 ≠ T ∧ ?dj1 ≠ F)" by auto
      moreover
      { assume "?dj1 = T" then have ?thesis by simp }
      moreover
      { assume "?dj1 = F" then have ?thesis using bst dj2_nov0 by (simp add: Let_def)}
      moreover
      {
        assume dj1nFT:"?dj1 ≠ T ∧ ?dj1 ≠ F"

        have "?dj2 = T ∨ ?dj2 = F ∨ (?dj2 ≠ T ∧ ?dj2 ≠ F)" by auto
        moreover
        { assume "?dj2 = T" then have ?thesis by (cases ?dj1) simp_all }
        moreover
        { assume "?dj2 = F" then have ?thesis using dj1_nov0 bst
            by (cases ?dj1) (simp_all add: Let_def)}
        moreover
        {
          assume dj2_nTF:"?dj2 ≠ T ∧ ?dj2 ≠ F"
          let ?res = "λf. λg. (case f of T => T | F => g
            | _ => (case g of T => T| F => f| _ => Or f g))"
          have expth: "explode_minf (p,B) = ?res ?dj1 ?dj2"
            by (simp add: Let_def del: iupto.simps split del: split_if
              cong del: QF.weak_case_cong)
          then have ?thesis
            using prems or_case_novar0 [OF dj1nFT dj2_nTF dj1_nov0 dj2_nov0]
            by (simp add: Let_def del: iupto.simps cong del: QF.weak_case_cong)
        }
        ultimately have ?thesis by blast
      }
      ultimately show ?thesis by blast
    qed

    (* explode_minf computes the rhs of cooper's thm*)
    lemma explode_minf_corr:
      assumes unifp : "isunified p"
      and bst: "set (bset p) = set B"
      shows "(∃ x . qinterp (x#ats) p) = (qinterp (a#ats) (explode_minf (p,B)))"
      (is "(∃ x. ?P x) = (?EXP a p)")
    proof-
      let ?d = "divlcm p"
      let ?pm = "minusinf p"
      let ?dj1 = "explode_disj (map Cst (iupto(1,?d)),?pm)"
      have qfpm: "isqfree ?pm"  using unified_islinform[OF unifp] minusinf_qfree by simp
      have nnfp: "isnnf p" by (rule unified_isnnf[OF unifp])

      have "(∃j∈{1..?d}. qinterp (j # ats) (minusinf p))
        = (∃j∈ set (iupto(1,?d)). qinterp (j#ats) (minusinf p))"
        (is "(∃ j∈ {1..?d}. ?QM j) = …")
        by (simp add: sym[OF iupto_set] )
      also
      have "… =(∃j∈ set (iupto(1,?d)). qinterp ((I_intterm (a#ats) (Cst j))#ats) (minusinf p))"
        by simp
      also have
        "… = (∃j∈ set (map Cst (iupto(1,?d))). qinterp ((I_intterm (a#ats) j)#ats) (minusinf p))" by simp
      also have
        "… =
        (∃j∈ set (map Cst (iupto(1,?d))). qinterp (a#ats) (subst_p j (minusinf p)))"
        by (simp add: subst_p_corr[OF qfpm])
      finally have dj1_thm:
        "(∃ j∈ {1..?d}. ?QM j) = (qinterp (a#ats) ?dj1)"
        by (simp only: explode_disj_corr[OF qfpm])
      let ?dj2 = "explode_disj (all_sums (?d,B),p)"
      have
        bstlin: "∀b∈set B. islinintterm b"
        using bst by (simp add: bset_lin[OF unifp])
      have bstnov0: "∀b∈set B. novar0I b"
        using bst by (simp add: bset_novar0[OF unifp])
      have allsnov0: "∀x∈set (all_sums(?d,B)). novar0I x "
        by (simp add:all_sums_novar0[OF bstnov0 bstlin] )
      have "(∃ j∈ {1..?d}. ∃ b∈ set B. ?P (I_intterm (a#ats) b + j)) =
       (∃ j∈ {1..?d}. ∃ b∈ set B. ?P (I_intterm (a#ats) (lin_add(b,Cst j))))"
        using bst by (auto simp add: lin_add_corr bset_lin[OF unifp])
      also have "… = (∃ x ∈ set (all_sums (?d, B)). ?P (I_intterm (a#ats) x))"
        by (simp add: all_sums_ex[where P="λ t. ?P (I_intterm (a#ats) t)"])
      finally
      have "(∃ j∈ {1..?d}. ∃ b∈ set B. ?P (I_intterm (a#ats) b + j)) =
        (∃ x ∈ set (all_sums (?d, B)). qinterp (a#ats) (subst_p x p))"
        using allsnov0 prems linform_isqfree unified_islinform[OF unifp]
        by (simp add: all_sums_ex subst_p_corr)
      also have "… = (qinterp (a#ats) ?dj2)"
        using linform_isqfree unified_islinform[OF unifp]
        by (simp add: explode_disj_corr)
      finally have dj2th:
        "(∃ j∈ {1..?d}. ∃ b∈ set B. ?P (I_intterm (a#ats) b + j)) =
        (qinterp (a#ats) ?dj2)" by simp
      let ?result = "λf. λg.
        (case f of
        T => T
        | F => g
        | _ => (case g of
        T => T
        | F => f
        | _ => Or f g))"
      have "?EXP a p =  qinterp (a#ats) (?result ?dj1 ?dj2)"
        by (simp only: explode_minf.simps Let_def)
      also
      have "… = (qinterp (a#ats) ?dj1 ∨ qinterp (a#ats) ?dj2)"
        by (rule eval_Or_cases[where f="?dj1" and g="?dj2" and a="a" and ats="ats"])
      also
      have "… = ((∃ j∈ {1..?d}. ?QM j) ∨
        (∃ j∈ {1..?d}. ∃ b∈ set B. ?P (I_intterm (a#ats) b + j)))"
        by (simp add: dj1_thm dj2th)
      also
      have "… = (∃ x. ?P x)"
        using bst sym[OF cooper_mi_eq[OF unifp]] by simp
      finally show ?thesis by simp
    qed

    lemma explode_minf_corr2:
      assumes unifp : "isunified p"
      and bst: "set (bset p) = set B"
      shows "(qinterp ats (QEx p)) = (qinterp ats (decrvars(explode_minf (p,B))))"
      (is "?P = (?Qe p)")
    proof-
      have "?P = (∃x. qinterp (x#ats) p)" by simp
      also have "…  = (qinterp (a # ats) (explode_minf (p,B)))"
        using unifp bst explode_minf_corr by simp
      finally have ex: "?P = (qinterp (a # ats) (explode_minf (p,B)))" .
      have nv0: "novar0 (explode_minf (p,B))"
        by (rule explode_minf_novar0[OF unifp])
      show ?thesis
        using qinterp_novar0[OF nv0] ex by simp
    qed

    (* An implementation of cooper's method for both plus/minus/infinity *)

    (* unify the formula *)
    constdefs unify:: "QF => (QF × intterm list)"
      "unify p ≡
      (let q = unitycoeff p;
           B = list_set(bset q);
           A = list_set (aset q)
      in
      if (length B ≤ length A)
                 then (q,B)
                 else (mirror q, map lin_neg A))"

    (* unify behaves like unitycoeff *)
    lemma unify_ex:
      assumes linp: "islinform p"
      shows "qinterp ats (QEx p) = qinterp ats (QEx (fst (unify p)))"
    proof-
      have "length (list_set(bset (unitycoeff p))) ≤ length (list_set (aset (unitycoeff p))) ∨ length (list_set(bset (unitycoeff p))) > length (list_set (aset (unitycoeff p)))" by arith
      moreover
      {
        assume "length (list_set(bset (unitycoeff p))) ≤ length (list_set (aset (unitycoeff p)))"
        then have "fst (unify p) = unitycoeff p" using unify_def by (simp add: Let_def)
        then have ?thesis using unitycoeff_corr[OF linp]
          by simp
      }
      moreover
      {
        assume "length (list_set(bset (unitycoeff p))) > length (list_set (aset (unitycoeff p)))"
        then have unif: "fst(unify p) = mirror (unitycoeff p)"
          using unify_def by (simp add: Let_def)
        let ?q ="unitycoeff p"
        have unifq: "isunified ?q" by(rule unitycoeff_unified[OF linp])
        have linq: "islinform ?q" by (rule unified_islinform[OF unifq])
        have "qinterp ats (QEx ?q) = qinterp ats (QEx (mirror ?q))"
          by (rule mirror_ex2[OF unifq])
        moreover have "qinterp ats (QEx p) = qinterp ats (QEx ?q)"
          using unitycoeff_corr linp by simp
        ultimately have ?thesis using prems unif by simp
      }
      ultimately show ?thesis by blast
    qed

    (* unify's result is a unified formula *)
    lemma unify_unified:
      assumes linp: "islinform p"
      shows "isunified (fst (unify p))"
      using linp unitycoeff_unified mirror_unified unify_def unified_islinform
      by (auto simp add: Let_def)

    (* unify preserves quantifier-freeness*)
    lemma unify_qfree:
      assumes linp: "islinform p"
      shows "isqfree (fst(unify p))"
      using linp unify_unified unified_isqfree by simp

    lemma unify_bst:
      assumes linp: " islinform p"
      and unif: "unify p = (q,B)"
      shows "set B = set (bset q)"
    proof-
      let ?q = "unitycoeff p"
      let ?a = "aset ?q"
      let ?b = "bset ?q"
      let ?la = "list_set ?a"
      let ?lb = "list_set ?b"
      have " length ?lb ≤ length ?la ∨ length ?lb > length ?la" by arith
      moreover
      {
        assume "length ?lb ≤ length ?la"
        then
        have "unify p = (?q,?lb)"using unify_def prems by (simp add: Let_def)
        then
        have ?thesis using prems by (simp add: sym[OF list_set_set])
      }
      moreover
      {    assume "length ?lb > length ?la"
        have r: "unify p = (mirror ?q,map lin_neg ?la)"using unify_def prems by (simp add: Let_def)
        have lin: "∀ x∈ set (bset (mirror ?q)). islinintterm x"
          using bset_lin mirror_unified unitycoeff_unified[OF linp] by auto
        with r prems aset_eq_bset_mirror lin_neg_idemp unitycoeff_unified linp
        have "set B = set (map lin_neg (map lin_neg (bset (mirror (unitycoeff p)))))"
           by (simp add: sym[OF list_set_set])
         also have "… = set (map (λx. lin_neg (lin_neg x)) (bset (mirror (unitycoeff p))))"
           by auto
         also have "… = set (bset (mirror (unitycoeff p)))"
           using lin lin_neg_idemp  by (auto simp add: map_idI)
         finally
         have ?thesis using r prems aset_eq_bset_mirror lin_neg_idemp unitycoeff_unified linp
           by (simp add: sym[OF list_set_set])}
      ultimately show ?thesis by blast
    qed

    lemma explode_minf_unify_novar0:
      assumes linp: "islinform p"
      shows "novar0 (explode_minf (unify p))"
    proof-
      have "∃ q B. unify p = (q,B)" by simp
      then obtain "q" "B" where qB_def: "unify p = (q,B)" by blast
      have unifq: "isunified q" using unify_unified[OF linp] qB_def by simp
      have bst: "set B = set (bset q)" using unify_bst linp qB_def by simp
      from unifq bst explode_minf_novar0 show ?thesis
        using qB_def by simp
    qed

    lemma explode_minf_unify_corr2:
      assumes linp: "islinform p"
      shows "qinterp ats (QEx p) = qinterp ats (decrvars(explode_minf(unify p)))"
    proof-
      have "∃ q B. unify p = (q,B)" by simp
      then obtain "q" "B" where qB_def: "unify p = (q,B)" by blast
      have unifq: "isunified q" using unify_unified[OF linp] qB_def by simp
      have bst: "set (bset q) = set B" using unify_bst linp qB_def by simp
      from explode_minf_corr2[OF unifq bst] unify_ex[OF linp] show ?thesis
        using qB_def by simp
    qed
    (* An implementation of cooper's method *)
    constdefs cooper:: "QF => QF option"
    "cooper p ≡ lift_un (λq. decrvars(explode_minf (unify q))) (linform (nnf p))"

    (* cooper eliminates quantifiers *)
    lemma cooper_qfree: "(!! q q'. [|isqfree q ; cooper q = Some q'|] ==>  isqfree q')"
    proof-
      fix "q" "q'"
      assume qfq: "isqfree q"
        and qeq: "cooper q = Some q'"
      from qeq have "∃p. linform (nnf q) = Some p"
        by (cases "linform (nnf q)") (simp_all add: cooper_def)
      then obtain "p" where p_def: "linform (nnf q) = Some p" by blast
      have linp: "islinform p" using p_def linform_lin nnf_isnnf qfq
        by auto
      have nnfq: "isnnf (nnf q)" using nnf_isnnf qfq by simp
      then have nnfp: "isnnf p" using linform_nnf[OF nnfq] p_def by auto
      have qfp: "isqfree p" using linp linform_isqfree by simp
      have "cooper q = Some (decrvars(explode_minf (unify p)))" using p_def
        by (simp add: cooper_def del: explode_minf.simps)
      then have "q' = decrvars (explode_minf (unify p))" using qeq by simp
      with linp qfp nnfp  unify_unified unify_qfree unified_islinform
      show "isqfree q'"
        using novar0_qfree explode_minf_unify_novar0 decrvars_qfree
        by simp
    qed

    (* cooper preserves semantics *)
    lemma cooper_corr: "(!! q q' ats. [|isqfree q ; cooper q = Some q'|] ==>  (qinterp ats (QEx q)) = (qinterp ats q'))"  (is "!! q q' ats. [| _ ; _ |] ==> (?P ats (QEx q) = ?P ats q')")
    proof-
      fix "q" "q'" "ats"
      assume qfq: "isqfree q"
        and qeq: "cooper q = Some q'"
      from qeq have "∃p. linform (nnf q) = Some p"
        by (cases "linform (nnf q)") (simp_all add: cooper_def)
      then obtain "p" where p_def: "linform (nnf q) = Some p" by blast
      have linp: "islinform p" using p_def linform_lin nnf_isnnf qfq by auto
      have qfp: "isqfree p" using linp linform_isqfree by simp
      have nnfq: "isnnf (nnf q)" using nnf_isnnf qfq by simp
      then have nnfp: "isnnf p" using linform_nnf[OF nnfq] p_def by auto
      have "∀ ats. ?P ats q = ?P ats (nnf q)" using nnf_corr qfq by auto
      then have qeqp: "∀ ats. ?P ats q = ?P ats p"
        using linform_corr p_def nnf_isnnf qfq
        by auto

      have "cooper q = Some (decrvars (explode_minf (unify p)))" using p_def
        by (simp add: cooper_def del: explode_minf.simps)
      then have decr: "q' = decrvars(explode_minf (unify p))" using qeq by simp
      have eqq:"?P ats (QEx q) = ?P ats (QEx p)" using qeqp by auto
      with decr explode_minf_unify_corr2 unified_islinform unify_unified linp
      show "?P ats (QEx q) = ?P ats q'" by simp
    qed

    (* A decision procedure for Presburger Arithmetics *)
    constdefs pa:: "QF => QF option"
    "pa p ≡ lift_un psimpl (qelim(cooper, p))"

    lemma psimpl_qfree: "isqfree p ==> isqfree (psimpl p)"
    apply(induct p rule: isqfree.induct)
    apply(auto simp add: Let_def measure_def inv_image_def)
    apply (simp_all cong del: QF.weak_case_cong add: Let_def)
    apply (case_tac "psimpl p", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl p", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl p", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl p", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)
    apply (case_tac "psimpl q", auto)

    apply (case_tac "psimpl p", auto)
    apply (case_tac "lift_bin (λx y. lin_add (x, lin_neg y), linearize y,
                       linearize z)", auto)
    apply (case_tac "a",auto)
    apply (case_tac "lift_bin (λx y. lin_add (x, lin_neg y), linearize ac,
                       linearize ad)", auto)
    apply (case_tac "a",auto)
    apply (case_tac "ae", auto)
    apply (case_tac "linearize af", auto)
    by (case_tac "a", auto)

    (* pa eliminates quantifiers *)
    theorem pa_qfree: "!! p'. pa p = Some p' ==> isqfree p'"
    proof(simp only: pa_def)
    fix "p'"
    assume qep: "lift_un psimpl (qelim (cooper, p)) = Some p'"
    then have "∃ q. qelim (cooper, p) = Some q"
      by (cases "qelim(cooper, p)") auto
    then obtain "q" where q_def: "qelim (cooper, p) = Some q" by blast
    have "!!q q'. [|isqfree q; cooper q = Some q'|] ==> isqfree q'" using cooper_qfree by blast
    with q_def
    have "isqfree q" using qelim_qfree by blast
    then have "isqfree (psimpl q)" using psimpl_qfree
      by auto
    then show "isqfree p'"
      using prems
      by simp

    qed

    (* pa preserves semantics *)
    theorem pa_corr:
      "!! p'. pa p = Some p' ==> (qinterp ats p = qinterp ats p')"
    proof(simp only: pa_def)
      fix "p'"
      assume qep: "lift_un psimpl (qelim(cooper, p)) = Some p'"
     then have "∃ q. qelim (cooper, p) = Some q"
      by (cases "qelim(cooper, p)") auto
    then obtain "q" where q_def: "qelim (cooper, p) = Some q" by blast
      have cp1:"!!q q' ats.
        [|isqfree q; cooper q = Some q'|] ==> qinterp ats (QEx q) = qinterp ats q'"
        using cooper_corr by blast
      moreover have cp2: "!!q q'. [|isqfree q; cooper q = Some q'|] ==> isqfree q'"
        using cooper_qfree by blast
      ultimately have "qinterp ats p = qinterp ats q" using qelim_corr qep psimpl_corr q_def
        by blast
      then have "qinterp ats p = qinterp ats (psimpl q)" using psimpl_corr q_def
        by auto
      then show "qinterp ats p = qinterp ats p'" using prems
        by simp
    qed

    lemma [code]: "linearize (Mult i j) =
      (case linearize i of
      None => None
      | Some li => (case li of
         Cst b => (case linearize j of
          None => None
         | (Some lj) => Some (lin_mul(b,lj)))
      | _ => (case linearize j of
          None => None
        | (Some lj) => (case lj of
            Cst b => Some (lin_mul (b,li))
          | _ => None))))"
    by (simp add: measure_def inv_image_def)

    lemma [code]: "psimpl (And p q) =
      (let p'= psimpl p
      in (case p' of
           F => F
          |T => psimpl q
          | _ => let q' = psimpl q
                 in (case q' of
                         F => F
                       | T => p'
                       | _ => (And p' q'))))"

    by (simp add: measure_def inv_image_def)

    lemma [code]: "psimpl (Or p q) =
      (let p'= psimpl p
      in (case p' of
            T => T
          | F => psimpl q
          | _ => let q' = psimpl q
                 in (case q' of
                         T => T
                       | F => p'
                       | _ => (Or p' q'))))"

    by (simp add: measure_def inv_image_def)

    lemma [code]: "psimpl (Imp p q) =
      (let p'= psimpl p
      in (case p' of
           F => T
          |T => psimpl q
          | NOT p1 => let q' = psimpl q
                 in (case q' of
                         F => p1
                       | T => T
                       | _ => (Or p1 q'))
          | _ => let q' = psimpl q
                 in (case q' of
                         F => NOT p'
                       | T => T
                       | _ => (Imp p' q'))))"
    by (simp add: measure_def inv_image_def)

    declare zdvd_iff_zmod_eq_0 [code]

    (*
    generate_code ("presburger.ML") test = "pa"
    use "rcooper.ML"
    oracle rpresburger_oracle ("term") = RCooper.rpresburger_oracle
    use "rpresbtac.ML"
    setup RPresburger.setup
    *)

    end

lemma lift_bin_Some:

      lift_bin (c, x, y) = Some t ==> (∃a. x = Some a) ∧ (∃b. y = Some b)

lemma qff:

      [| !!q q'. [| isqfree q; qe q = Some q' |] ==> isqfree q';
         qelim (qe, p) = Some p' |]
      ==> isqfree p'

lemma qff:

      [| !!q q' ats.
            [| isqfree q; qe q = Some q' |] ==> qinterp ats (QEx q) = qinterp ats q';
         !!q q'. [| isqfree q; qe q = Some q' |] ==> isqfree q';
         qelim (qe, p) = Some p' |]
      ==> qinterp ats p = qinterp ats p'

lemma

      0 < lgth q

lemma nnf_corr:

      isqfree p ==> qinterp ats p = qinterp ats (nnf p)

lemma nnf_isnnf:

      isqfree p ==> isnnf (nnf p)

lemma nnf_isqfree:

      isnnf p ==> isqfree p

lemma nnf_qfree:

      isqfree p ==> isqfree (nnf p)

lemma islinintterm_subt:

      islinintterm (Add (Mult (Cst i) (Var n)) r) ==> islinintterm r

lemma islinintterm_cnz:

      islinintterm (Add (Mult (Cst i) (Var n)) r) ==> i ≠ 0

lemma islininttermc0r:

      islinintterm (Add (Mult (Cst c) (Var n)) r) ==> c ≠ 0 ∧ islinintterm r

lemma islinintterm_eq_islint:

      islinintterm t = islint t

lemma islintn_mon:

      [| islintn (n, t); m ≤ n |] ==> islintn (m, t)

lemma islintn_subt:

      islintn (n, Add (Mult (Cst i) (Var m)) r) ==> islintn (m + 1, r)

lemma nth_pos:

      0 < n --> (x # xs) ! n = (y # xs) ! n

lemma nth_pos2:

      0 < n ==> (x # xs) ! n = xs ! (n - 1)

lemma intterm_novar0:

      islinintterm (Add (Mult (Cst i) (Var n)) r)
      ==> I_intterm (x # ats) r = I_intterm (y # ats) r

lemma linterm_novar0:

      [| islintn (n, t); 0 < n |] ==> I_intterm (x # ats) t = I_intterm (y # ats) t

lemma dvd_period:

      a dvd d ==> (a dvd x + t) = (a dvd x + c * d + t)

lemma lin_add_cst_corr:

      islintn (n0.0, b)
      ==> I_intterm ats (lin_add (Cst a, b)) = I_intterm ats (Add (Cst a) b)

lemma lin_add_cst_corr2:

      islintn (n0.0, b)
      ==> I_intterm ats (lin_add (b, Cst a)) = I_intterm ats (Add b (Cst a))

lemma lin_add_corrh:

      [| islintn (n01.0, a); islintn (n02.0, b) |]
      ==> I_intterm ats (lin_add (a, b)) = I_intterm ats (Add a b)

lemma lin_add_corr:

      [| islinintterm a; islinintterm b |]
      ==> I_intterm ats (lin_add (a, b)) = I_intterm ats (Add a b)

lemma lin_add_cst_lint:

      islintn (n0.0, b) ==> islintn (n0.0, lin_add (Cst i, b))

lemma lin_add_cst_lint2:

      islintn (n0.0, b) ==> islintn (n0.0, lin_add (b, Cst i))

lemma lin_add_lint:

      [| islintn (n01.0, a); islintn (n02.0, b); n0.0 ≤ min n01.0 n02.0 |]
      ==> islintn (n0.0, lin_add (a, b))

lemma lin_add_lin:

      [| islinintterm a; islinintterm b |] ==> islinintterm (lin_add (a, b))

lemma zmult_zadd_distrib:

      a * (b + c) = a * b + a * c

lemma lin_mul_corr:

      islinintterm t
      ==> I_intterm ats (lin_mul (c, t)) = I_intterm ats (Mult (Cst c) t)

lemma lin_mul_lin:

      islinintterm t ==> islinintterm (lin_mul (c, t))

lemma lin_mul0:

      islinintterm t ==> lin_mul (0, t) = Cst 0

lemma lin_mul_lintn:

      islintn (m, t) ==> islintn (m, lin_mul (l, t))

lemma lin_neg_corr:

      islinintterm t ==> I_intterm ats (lin_neg t) = I_intterm ats (Neg t)

lemma lin_neg_lin:

      islinintterm t ==> islinintterm (lin_neg t)

lemma lin_neg_idemp:

      islinintterm i ==> lin_neg (lin_neg i) = i

lemma lin_neg_lin_add_distrib:

      [| islinintterm a; islinintterm b |]
      ==> lin_neg (lin_add (a, b)) = lin_add (lin_neg a, lin_neg b)

lemma linearize_linear1:

      linearize t ≠ None ==> islinintterm (the (linearize t))

lemma linearize_linear:

      linearize t = Some t' ==> islinintterm t'

lemma linearize_corr1:

      linearize t ≠ None ==> I_intterm ats t = I_intterm ats (the (linearize t))

lemma linearize_corr:

      linearize t = Some t' ==> I_intterm ats t = I_intterm ats t'

lemma linform_nnf:

      [| isnnf p; linform p = Some p' |] ==> isnnf p'

lemma linform_corr:

      [| isnnf p; linform p = Some lp |] ==> qinterp ats p = qinterp ats lp

lemma linform_lin:

      [| isnnf p; linform p = Some lp |] ==> islinform lp

lemma linform_isnnf:

      islinform p ==> isnnf p

lemma linform_isqfree:

      islinform p ==> isqfree p

lemma linform_qfree:

      [| isnnf p; linform p = Some p' |] ==> isqfree p'

lemma lcm_dvd1:

      [| 0 < m; 0 < n |] ==> m dvd lcm (m, n)

lemma lcm_dvd2:

      [| 0 < m; 0 < n |] ==> n dvd lcm (m, n)

lemma ilcm_dvd1:

      [| a ≠ 0; b ≠ 0 |] ==> a dvd ilcm a b

lemma ilcm_dvd2:

      [| a ≠ 0; b ≠ 0 |] ==> b dvd ilcm a b

lemma zdvd_self_abs1:

      d dvd ¦d¦

lemma zdvd_self_abs2:

      ¦d¦ dvd d

lemma lcm_pos:

      [| 0 < m; 0 < n |] ==> 0 < lcm (m, n)

lemma ilcm_pos:

      [| 0 < a; 0 < b |] ==> 0 < ilcm a b

lemma formlcm_pos:

      islinform p ==> 0 < formlcm p

lemma divideallc_mono:

      [| divideallc (c, p); c dvd d |] ==> divideallc (d, p)

lemma formlcm_divideallc:

      islinform p ==> divideallc (formlcm p, p)

lemma unified_islinform:

      isunified p ==> islinform p

lemma adjustcoeff_lenpos:

      0 < n
      ==> adjustcoeff (l, Le (Add (Mult (Cst i) (Var n)) r) (Cst c)) =
          Le (Add (Mult (Cst i) (Var n)) r) (Cst c)

lemma adjustcoeff_eqnpos:

      0 < n
      ==> adjustcoeff (l, Eq (Add (Mult (Cst i) (Var n)) r) (Cst c)) =
          Eq (Add (Mult (Cst i) (Var n)) r) (Cst c)

lemma zmult_zle_mono:

      [| i ≤ j; 0 ≤ k |] ==> k * i ≤ k * j

lemma zmult_zle_mono_eq:

      0 < k ==> (i ≤ j) = (k * i ≤ k * j)

lemma adjustcoeff_le_corr:

      [| 0 < l; 0 < i; i dvd l |] ==> (i * x + r ≤ 0) = (l * x + l div i * r ≤ 0)

lemma adjustcoeff_le_corr2:

      [| 0 < l; i < 0; i dvd l |]
      ==> (i * x + r ≤ 0) = (- l * x + - (l div i) * r ≤ 0)

lemma dvd_div_pos:

      [| 0 < b; a ≠ 0; a dvd b |] ==> b div a * a = b

lemma adjustcoeff_eq_corr:

      [| 0 < l; i ≠ 0; i dvd l |] ==> (i * x + r = 0) = (l * x + l div i * r = 0)

lemma adjustcoeff_corr:

      [| islinform p; divideallc (l, p); 0 < l |]
      ==> qinterp (a # ats) p = qinterp (a * l # ats) (adjustcoeff (l, p))

lemma unitycoeff_corr:

      islinform p ==> qinterp ats (QEx p) = qinterp ats (QEx (unitycoeff p))

lemma adjustcoeff_unified:

      [| islinform p; divideallc (l, p); 0 < l |] ==> isunified (adjustcoeff (l, p))

lemma adjustcoeff_lcm_unified:

      islinform p ==> isunified (adjustcoeff (formlcm p, p))

lemma unitycoeff_unified:

      islinform p ==> isunified (unitycoeff p)

lemma unified_isnnf:

      isunified p ==> isnnf p

lemma unified_isqfree:

      isunified p ==> isqfree p

lemma alldivide_mono:

      [| alldivide (d, p); d dvd d' |] ==> alldivide (d', p)

lemma zdvd_eq_zdvd_abs:

      (d dvd d') = (d dvd ¦d'¦)

lemma zdvd_refl_abs:

      d dvd ¦d¦

lemma divlcm_pos:

      islinform p ==> 0 < divlcm p

lemma nz_le:

      0 < x ==> x ≠ 0

lemma divlcm_corr:

      islinform p ==> alldivide (divlcm p, p)

lemma minusinf_eq:

      isunified p ==> ∃z. ∀x<z. qinterp (x # ats) p = qinterp (x # ats) (minusinf p)

lemma minusinf_repeats:

      [| alldivide (d, p); isunified p |]
      ==> qinterp (x # ats) (minusinf p) = qinterp ((x + c * d) # ats) (minusinf p)

lemma minusinf_repeats2:

      [| alldivide (d, p); isunified p |]
      ==> ∀x k. qinterp (x # ats) (minusinf p) =
                qinterp ((x - k * d) # ats) (minusinf p)

lemma minusinf_lemma:

      [| isunified p; ∃j∈{1..d}. qinterp (j # ats) (minusinf p) |]
      ==> ∃x. qinterp (x # ats) p

lemma minusinf_disj:

      isunified p
      ==> (∃x. qinterp (x # ats) (minusinf p)) =
          (∃j∈{1..divlcm p}. qinterp (j # ats) (minusinf p))

lemma minusinf_qfree:

      islinform p ==> isqfree (minusinf p)

lemma bset_lin:

      isunified p ==> ∀b∈set (bset p). islinintterm b

lemma bset_disj_repeat:

      [| isunified p; alldivide (d, p); 0 < d;
         qinterp (x # ats) q ∧
         ¬ (∃j∈{1..d}.
               ∃b∈set (bset p). qinterp ((I_intterm (a # ats) b + j) # ats) q) ∧
         qinterp (x # ats) p |]
      ==> qinterp ((x - d) # ats) p

lemma bset_disj_repeat2:

      isunified p
      ==> ∀x. ¬ (∃j∈{1..divlcm p}.
                    ∃b∈set (bset p).
                       qinterp ((I_intterm (a # ats) b + j) # ats) p) -->
              qinterp (x # ats) p --> qinterp ((x - divlcm p) # ats) p

lemma cooper_mi_eq:

      isunified p
      ==> (∃x. qinterp (x # ats) p) =
          ((∃j∈{1..divlcm p}. qinterp (j # ats) (minusinf p)) ∨
           (∃j∈{1..divlcm p}.
               ∃b∈set (bset p). qinterp ((I_intterm (a # ats) b + j) # ats) p))

lemma

      (¦i¦ = 1) = (i = 1 ∨ i = -1)

lemma mirror_unified:

      isunified p ==> isunified (mirror p)

lemma plusinf_eq_minusinf_mirror:

      isunified p
      ==> qinterp (x # ats) (plusinf p) = qinterp (- x # ats) (minusinf (mirror p))

lemma aset_eq_bset_mirror:

      isunified p ==> set (aset p) = set (map lin_neg (bset (mirror p)))

lemma aset_eq_bset_mirror2:

      isunified p ==> aset p = map lin_neg (bset (mirror p))

lemma divlcm_mirror_eq:

      isunified p ==> divlcm p = divlcm (mirror p)

lemma mirror_interp:

      isunified p ==> qinterp (x # ats) p = qinterp (- x # ats) (mirror p)

lemma mirror_interp2:

      islinform p ==> qinterp (x # ats) p = qinterp (- x # ats) (mirror p)

lemma mirror_ex:

      isunified p ==> (∃x. qinterp (x # ats) p) = (∃y. qinterp (y # ats) (mirror p))

lemma mirror_ex2:

      isunified p ==> qinterp ats (QEx p) = qinterp ats (QEx (mirror p))

lemma cooper_pi_eq:

      isunified p
      ==> (∃x. qinterp (x # ats) p) =
          ((∃j∈{1..divlcm p}. qinterp (- j # ats) (plusinf p)) ∨
           (∃j∈{1..divlcm p}.
               ∃b∈set (aset p). qinterp ((I_intterm (a # ats) b - j) # ats) p))

lemma subst_it_corr:

      I_intterm (a # ats) (subst_it i t) = I_intterm (I_intterm (a # ats) i # ats) t

lemma subst_p_corr:

      isqfree p
      ==> qinterp (a # ats) (subst_p i p) = qinterp (I_intterm (a # ats) i # ats) p

lemma I_intterm_novar0:

      novar0I x ==> I_intterm (a # ats) x = I_intterm (b # ats) x

lemma subst_p_novar0_corr:

      [| isqfree p; novar0I i |]
      ==> qinterp (a # ats) (subst_p i p) = qinterp (I_intterm (b # ats) i # ats) p

lemma lin_novar0:

      [| islinintterm x; novar0I x |] ==> ∃n>0. islintn (n, x)

lemma lintnpos_novar0:

      [| 0 < n; islintn (n, x) |] ==> novar0I x

lemma lin_add_novar0:

      [| novar0I a; novar0I b; islinintterm a; islinintterm b |]
      ==> novar0I (lin_add (a, b))

lemma lin_mul_novar0:

      [| islinintterm x; novar0I x |] ==> novar0I (lin_mul (i, x))

lemma lin_neg_novar0:

      [| islinintterm x; novar0I x |] ==> novar0I (lin_neg x)

lemma intterm_subt_novar0:

      islinintterm (Add (Mult (Cst c) (Var n)) r) ==> novar0I r

lemma intterm_decrvarsI:

      novar0I t ==> I_intterm (a # ats) t = I_intterm ats (decrvarsI t)

lemma decrvars_qfree:

      isqfree p ==> isqfree (decrvars p)

lemma novar0_qfree:

      novar0 p ==> isqfree p

lemma qinterp_novar0:

      novar0 p ==> qinterp (a # ats) p = qinterp ats (decrvars p)

lemma bset_novar0:

      isunified p ==> ∀b∈set (bset p). novar0I b

lemma subst_it_novar0:

      novar0I x ==> novar0I (subst_it x t)

lemma subst_p_novar0:

      [| novar0I x; isqfree p |] ==> novar0 (subst_p x p)

lemma linearize_novar0:

      [| novar0I t; linearize t = Some t' |] ==> novar0I t'

lemma psimpl_corr:

      qinterp ats p = qinterp ats (psimpl p)

lemma psimpl_novar0:

      novar0 p ==> novar0 (psimpl p)

lemma explode_disj_disj:

      isqfree p
      ==> qinterp (x # xs) (explode_disj (i # is, p)) =
          (qinterp (x # xs) (subst_p i p) ∨ qinterp (x # xs) (explode_disj (is, p)))

lemma explode_disj_corr:

      isqfree p
      ==> (∃x∈set xs. qinterp (a # ats) (subst_p x p)) =
          qinterp (a # ats) (explode_disj (xs, p))

lemma explode_disj_novar0:

      [| ∀x∈set xs. novar0I x; isqfree p |] ==> novar0 (explode_disj (xs, p))

lemma eval_Or_cases:

      qinterp (a # ats)
       (case f of T => T | F => g | _ => case g of T => T | F => f | _ => Or f g) =
      (qinterp (a # ats) f ∨ qinterp (a # ats) g)

lemma or_case_novar0:

      [| f ≠ T ∧ f ≠ F; g ≠ T ∧ g ≠ F; novar0 f; novar0 g |]
      ==> novar0
           (case f of T => T | F => g | _ => case g of T => T | F => f | _ => Or f g)

lemma list_insert_set:

      set (list_insert x xs) = set (x # xs)

lemma list_union_set:

      set (list_union (xs, ys)) = set (xs @ ys)

lemma list_set_set:

      set xs = set (list_set xs)

lemma iupto_set:

      set (iupto (i, j)) = {i..j}

lemma all_sums_novar0:

      [| ∀x∈set xs. novar0I x; ∀x∈set xs. islinintterm x |]
      ==> ∀x∈set (all_sums (d, xs)). novar0I x

lemma all_sums_ex:

      (∃j∈{1..d}. ∃b∈set xs. P (lin_add (b, Cst j))) =
      (∃x∈set (all_sums (d, xs)). P x)

lemma explode_minf_novar0:

      [| isunified p; set (bset p) = set B |] ==> novar0 (explode_minf (p, B))

lemma explode_minf_corr:

      [| isunified p; set (bset p) = set B |]
      ==> (∃x. qinterp (x # ats) p) = qinterp (a # ats) (explode_minf (p, B))

lemma explode_minf_corr2:

      [| isunified p; set (bset p) = set B |]
      ==> qinterp ats (QEx p) = qinterp ats (decrvars (explode_minf (p, B)))

lemma unify_ex:

      islinform p ==> qinterp ats (QEx p) = qinterp ats (QEx (fst (unify p)))

lemma unify_unified:

      islinform p ==> isunified (fst (unify p))

lemma unify_qfree:

      islinform p ==> isqfree (fst (unify p))

lemma unify_bst:

      [| islinform p; unify p = (q, B) |] ==> set B = set (bset q)

lemma explode_minf_unify_novar0:

      islinform p ==> novar0 (explode_minf (unify p))

lemma explode_minf_unify_corr2:

      islinform p
      ==> qinterp ats (QEx p) = qinterp ats (decrvars (explode_minf (unify p)))

lemma cooper_qfree:

      [| isqfree q; cooper q = Some q' |] ==> isqfree q'

lemma cooper_corr:

      [| isqfree q; cooper q = Some q' |] ==> qinterp ats (QEx q) = qinterp ats q'

lemma psimpl_qfree:

      isqfree p ==> isqfree (psimpl p)

theorem pa_qfree:

      pa p = Some p' ==> isqfree p'

theorem pa_corr:

      pa p = Some p' ==> qinterp ats p = qinterp ats p'

lemma

      linearize (Mult i j) =
      (case linearize i of None => None
       | Some li =>
           case li of
           Cst b =>
             case linearize j of None => None | Some lj => Some (lin_mul (b, lj))
           | _ => case linearize j of None => None
                  | Some lj => case lj of Cst b => Some (lin_mul (b, li)) | _ => None)

lemma

      psimpl (And p q) =
      (let p' = psimpl p
       in case p' of T => psimpl q | F => F
          | _ => let q' = psimpl q in case q' of T => p' | F => F | _ => And p' q')

lemma

      psimpl (Or p q) =
      (let p' = psimpl p
       in case p' of T => T | F => psimpl q
          | _ => let q' = psimpl q in case q' of T => T | F => p' | _ => Or p' q')

lemma

      psimpl (Imp p q) =
      (let p' = psimpl p
       in case p' of T => psimpl q | F => T
          | NOT p1 => let q' = psimpl q in case q' of T => T | F => p1 | _ => Or p1 q'
          | _ => let q' = psimpl q
                 in case q' of T => T | F => NOT p' | _ => Imp p' q')