Theory GeneralVSProofs

theory GeneralVSProofs
  imports  DNFUni EqualityVS VSAlgos
begin


fun separateAtoms :: "atomUni list  (real * real * real) list * (real * real * real) list * (real * real * real) list * (real * real * real) list" where
  "separateAtoms [] = ([],[],[],[])"|
  "separateAtoms (EqUni p # L) = (let (a,b,c,d) = separateAtoms(L) in (p#a,b,c,d))"|
  "separateAtoms (LessUni p # L) = (let (a,b,c,d) = separateAtoms(L) in (a,p#b,c,d))"|
  "separateAtoms (LeqUni p # L) = (let (a,b,c,d) = separateAtoms(L) in (a,b,p#c,d))"|
  "separateAtoms (NeqUni p # L) = (let (a,b,c,d) = separateAtoms(L) in (a,b,c,p#d))"


lemma separate_aEval :
  assumes "separateAtoms L = (a,b,c,d)"
  shows "(lset L. aEvalUni l x) = 
      (((a,b,c)set a. a*x^2+b*x+c=0)  ((a,b,c)set b. a*x^2+b*x+c<0) 
      ((a,b,c)set c. a*x^2+b*x+c0)  ((a,b,c)set d. a*x^2+b*x+c0))"
  using assms proof(induction L arbitrary :a b c d)
  case Nil
  then show ?case by auto
next
  case (Cons At L)
  then have Cons1 : "a b c d. separateAtoms L = (a, b, c, d) 
    (lset L. aEvalUni l x) =
    ((aset a. case a of (a, ba, c)  a * x2 + ba * x + c = 0) 
     (aset b. case a of (a, ba, c)  a * x2 + ba * x + c < 0)
     (aset c. case a of (a, ba, c)  a * x2 + ba * x + c  0) 
     (aset d. case a of (a, ba, c)  a * x2 + ba * x + c  0))" "
    separateAtoms (At # L) = (a, b,c,d)" by auto
  then show ?case proof(cases At)
    case (LessUni p)
    show ?thesis proof(cases b)
      case Nil
      show ?thesis using Cons(2) unfolding LessUni separateAtoms.simps Nil
        apply(cases "separateAtoms L") by simp
    next
      case (Cons p' b')
      then have p_def : "p' = p" using Cons1(2) unfolding LessUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h1 :  "separateAtoms L = (a,b',c,d)" using Cons Cons1(2) unfolding LessUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h2 : "(aset (p # b'). case a of (a, ba, c)  a * x2 + ba * x + c < 0) = (
          (aset (b'). case a of (a, ba, c)  a * x2 + ba * x + c < 0) (case p of (a, ba, c)  a * x2 + ba * x + c < 0))"
        by auto
      have h3 : "(lset (LessUni p # L). aEvalUni l x) = ((lset (L). aEvalUni l x)(case p of (a, ba, c)  a * x2 + ba * x + c < 0))"
        by auto
      show ?thesis unfolding Cons LessUni p_def h2 h3 using Cons1(1)[OF h1]
        by auto
    qed
  next
    case (EqUni p)
    show ?thesis proof(cases a)
      case Nil
      show ?thesis using Cons(2) unfolding EqUni separateAtoms.simps Nil
        apply(cases "separateAtoms L") by simp
    next
      case (Cons p' a')
      then have p_def : "p' = p" using Cons1(2) unfolding EqUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h1 :  "separateAtoms L = (a',b,c,d)" using Cons Cons1(2) unfolding EqUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h2 : "(aset (p # a'). case a of (a, ba, c)  a * x2 + ba * x + c = 0) = (
          (aset (a'). case a of (a, ba, c)  a * x2 + ba * x + c = 0) (case p of (a, ba, c)  a * x2 + ba * x + c = 0))"
        by auto
      have h3 : "(lset (EqUni p # L). aEvalUni l x) = ((lset (L). aEvalUni l x)(case p of (a, ba, c)  a * x2 + ba * x + c = 0))"
        by auto
      show ?thesis unfolding Cons EqUni p_def h2 h3 using Cons1(1)[OF h1]
        by auto
    qed
  next
    case (LeqUni p)
    then show ?thesis proof(cases c)
      case Nil
      show ?thesis using Cons(2) unfolding LeqUni separateAtoms.simps Nil
        apply(cases "separateAtoms L") by simp
    next
      case (Cons p' a')
      then have p_def : "p' = p" using Cons1(2) unfolding LeqUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h1 :  "separateAtoms L = (a,b,a',d)" using Cons Cons1(2) unfolding LeqUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h2 : "(aset (p # a'). case a of (a, ba, c)  a * x2 + ba * x + c  0) = (
          (aset (a'). case a of (a, ba, c)  a * x2 + ba * x + c  0) (case p of (a, ba, c)  a * x2 + ba * x + c  0))"
        by auto
      have h3 : "(lset (LeqUni p # L). aEvalUni l x) = ((lset (L). aEvalUni l x)(case p of (a, ba, c)  a * x2 + ba * x + c  0))"
        by auto
      show ?thesis unfolding Cons LeqUni p_def h2 h3 using Cons1(1)[OF h1]
        by auto
    qed
  next
    case (NeqUni p)
    then show ?thesis proof(cases d)
      case Nil
      show ?thesis using Cons(2) unfolding NeqUni separateAtoms.simps Nil
        apply(cases "separateAtoms L") by simp
    next
      case (Cons p' a')
      then have p_def : "p' = p" using Cons1(2) unfolding NeqUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h1 :  "separateAtoms L = (a,b,c,a')" using Cons Cons1(2) unfolding NeqUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h2 : "(aset (p # a'). case a of (a, ba, c)  a * x2 + ba * x + c  0) = (
          (aset (a'). case a of (a, ba, c)  a * x2 + ba * x + c  0) (case p of (a, ba, c)  a * x2 + ba * x + c  0))"
        by auto
      have h3 : "(lset (NeqUni p # L). aEvalUni l x) = ((lset (L). aEvalUni l x)(case p of (a, ba, c)  a * x2 + ba * x + c  0))"
        by auto
      show ?thesis unfolding Cons NeqUni p_def h2 h3 using Cons1(1)[OF h1]
        by auto
    qed
  qed
qed

lemma splitAtoms_negInfinity :
  assumes "separateAtoms L = (a,b,c,d)"
  shows "(lset L. evalUni (substNegInfinityUni l) x) = (
  ((a,b,c)set a.(x. y<x. a*y^2+b*y+c=0))
  ((a,b,c)set b.(x. y<x. a*y^2+b*y+c<0))
  ((a,b,c)set c.(x. y<x. a*y^2+b*y+c0))
  ((a,b,c)set d.(x. y<x. a*y^2+b*y+c0)))"
  using assms proof(induction L arbitrary :a b c d)
  case Nil
  then show ?case by auto
next
  case (Cons At L)
  then have Cons1 : "a b c d. separateAtoms L = (a, b, c, d) 
    (lset L. evalUni (substNegInfinityUni l) x) =
    ((aset a. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c = 0) 
     (aset b. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0)
     (aset c. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0)
     (aset d. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0))" "separateAtoms (At # L) = (a, b, c, d)" by auto
  then show ?case proof(cases At)
    case (LessUni p)
    show ?thesis using LessUni Cons proof(induction b rule : list.induct)
      case Nil
      then have Nil : "b = []"
        using Cons.prems by auto
      show ?case using Cons(2) unfolding LessUni separateAtoms.simps Nil
        apply(cases "separateAtoms L") by simp
    next
      case (Cons p' b')
      then have p_def : "p' = p" using Cons1(2) unfolding LessUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h1 :  "separateAtoms L = (a,b',c,d)" using Cons Cons1(2) unfolding LessUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h2 : "(aset (p # b'). case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0) = (
          (aset ( b'). case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0) (case p of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0))"
        by auto
      have one: "(x. y<x. aEvalUni (LessUni p) y) = (case p of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0)"
        apply(cases p) by simp
      have "(lset (LessUni p # L). evalUni (substNegInfinityUni l) x) = ((evalUni (substNegInfinityUni (LessUni p)) x)(lset ( L). evalUni (substNegInfinityUni l) x))"
        by auto
      also have "... = (
      (case p of (a,ba,c)  x. y<x. a * y2 + ba * y + c < 0)
      (aset a. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c = 0) 
     (aset b'. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0)
     (aset c. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0)
     (aset d. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0))"
        unfolding infinity_evalUni[of "LessUni p" x, symmetric] Cons(3)[OF h1]  LessUni one by simp
      finally have h3 : "(lset (LessUni p # L). evalUni (substNegInfinityUni l) x) = (
      (case p of (a,ba,c)  x. y<x. a * y2 + ba * y + c < 0)
      (aset a. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c = 0) 
     (aset b'. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0)
     (aset c. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0)
     (aset d. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0) )"
        by auto
      show ?case unfolding Cons LessUni p_def h2 h3 using Cons1(1)[OF h1]
        by auto
    qed
  next
    case (EqUni p)
    show ?thesis using EqUni Cons proof(induction a rule : list.induct)
      case Nil
      then have Nil : "a = []"
        using Cons.prems by auto
      show ?case using Cons(2) unfolding EqUni separateAtoms.simps Nil
        apply(cases "separateAtoms L") by simp
    next
      case (Cons p' a')
      then have p_def : "p' = p" using Cons1(2) unfolding EqUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h1 :  "separateAtoms L = (a',b,c,d)" using Cons Cons1(2) unfolding EqUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h2 : "(aset (p # a'). case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c = 0) = (
          (aset ( a'). case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c = 0) (case p of (a, ba, c)  x. y<x. a * y2 + ba * y + c = 0))"
        by auto
      have one: "(x. y<x. aEvalUni (EqUni p) y) = (case p of (a, ba, c)  x. y<x. a * y2 + ba * y + c = 0)"
        apply(cases p) by simp
      have "(lset (EqUni p # L). evalUni (substNegInfinityUni l) x) = ((evalUni (substNegInfinityUni (EqUni p)) x)(lset ( L). evalUni (substNegInfinityUni l) x))"
        by auto
      also have "... = (
      (case p of (a,ba,c)  x. y<x. a * y2 + ba * y + c = 0)
      (aset a'. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c = 0) 
     (aset b. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0)
     (aset c. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0)
     (aset d. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0))"
        unfolding infinity_evalUni[of "EqUni p" x, symmetric] Cons(3)[OF h1] EqUni one by simp
      finally have h3 : "(lset (EqUni p # L). evalUni (substNegInfinityUni l) x) = (
      (case p of (a,ba,c)  x. y<x. a * y2 + ba * y + c = 0)
      (aset a'. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c = 0) 
     (aset b. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0)
     (aset c. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0)
     (aset d. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0))"
        by auto
      show ?case unfolding Cons EqUni p_def h2 h3 using Cons1(1)[OF h1]
        by auto
    qed
  next
    case (LeqUni p)
    show ?thesis using LeqUni Cons proof(induction c rule : list.induct)
      case Nil
      then have Nil : "c = []"
        using Cons.prems by auto
      show ?case using Cons(2) unfolding LeqUni separateAtoms.simps Nil
        apply(cases "separateAtoms L") by simp
    next
      case (Cons p' c')
      then have p_def : "p' = p" using Cons1(2) unfolding LeqUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h1 :  "separateAtoms L = (a,b,c',d)" using Cons Cons1(2) unfolding LeqUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h2 : "(aset (p # c'). case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0) = (
          (aset ( c'). case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0) (case p of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0))"
        by auto
      have one: "(x. y<x. aEvalUni (LeqUni p) y) = (case p of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0)"
        apply(cases p) by simp
      have "(lset (LeqUni p # L). evalUni (substNegInfinityUni l) x) = ((evalUni (substNegInfinityUni (LeqUni p)) x)(lset ( L). evalUni (substNegInfinityUni l) x))"
        by auto
      also have "... = (
      (case p of (a,ba,c)  x. y<x. a * y2 + ba * y + c  0)
      (aset a. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c = 0) 
     (aset b. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0)
     (aset c'. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0)
     (aset d. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0))"
        unfolding infinity_evalUni[of "LeqUni p" x, symmetric] Cons(3)[OF h1]  LeqUni one 
        by simp
      finally have h3 : "(lset (LeqUni p # L). evalUni (substNegInfinityUni l) x) = (
      (case p of (a,ba,c)  x. y<x. a * y2 + ba * y + c  0)
      (aset a. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c = 0) 
     (aset b. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0)
     (aset c'. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0)
     (aset d. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0) )"
        by auto
      show ?case unfolding Cons LeqUni p_def h2 h3 using Cons1(1)[OF h1]
        by auto
    qed
  next
    case (NeqUni p)
    show ?thesis using NeqUni Cons proof(induction d rule : list.induct)
      case Nil
      then have Nil : "d = []"
        using Cons.prems by auto
      show ?case using Cons(2) unfolding NeqUni separateAtoms.simps Nil
        apply(cases "separateAtoms L") by simp
    next
      case (Cons p' d')
      then have p_def : "p' = p" using Cons1(2) unfolding NeqUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h1 :  "separateAtoms L = (a,b,c,d')" using Cons Cons1(2) unfolding NeqUni separateAtoms.simps
        apply(cases "separateAtoms L") by simp
      have h2 : "(aset (p # d'). case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0) = (
          (aset ( d'). case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0) (case p of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0))"
        by auto
      have one: "(x. y<x. aEvalUni (NeqUni p) y) = (case p of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0)"
        apply(cases p) by simp
      have "(lset (NeqUni p # L). evalUni (substNegInfinityUni l) x) = ((evalUni (substNegInfinityUni (NeqUni p)) x)(lset ( L). evalUni (substNegInfinityUni l) x))"
        by auto
      also have "... = (
      (case p of (a,ba,c)  x. y<x. a * y2 + ba * y + c  0)
      (aset a. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c = 0) 
     (aset b. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0)
     (aset c. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0)
     (aset d'. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0))"
        unfolding infinity_evalUni[of "NeqUni p" x, symmetric] Cons(3)[OF h1]  NeqUni one 
        by simp
      finally have h3 : "(lset (NeqUni p # L). evalUni (substNegInfinityUni l) x) = (
      (case p of (a,ba,c)  x. y<x. a * y2 + ba * y + c  0)
      (aset a. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c = 0) 
     (aset b. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c < 0)
     (aset c. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0)
     (aset d'. case a of (a, ba, c)  x. y<x. a * y2 + ba * y + c  0) )"
        by auto
      show ?case unfolding Cons NeqUni p_def h2 h3 using Cons1(1)[OF h1]
        by auto
    qed
  qed
qed

lemma set_split : 
  assumes "separateAtoms L = (eq,les,leq,neq)"
  shows "set L = set (map EqUni eq @ map LessUni les @ map LeqUni leq @ map NeqUni neq)"
  using assms proof(induction L arbitrary :eq les leq neq)
  case Nil
  then show ?case by auto
next
  case (Cons At L)
  then show ?case proof(cases At)
    case (LessUni p)
    have "les'. p#les' = les  separateAtoms L = (eq, les', leq, neq)" using Cons(2) unfolding LessUni apply (cases "separateAtoms L") by auto
    then obtain les' where les' : "p#les' = les" "separateAtoms L = (eq, les', leq, neq)" by auto
    show ?thesis unfolding LessUni les'(1)[symmetric] using Cons(1)[OF les'(2)] by auto
  next
    case (EqUni p)
    have "eq'. p#eq' = eq  separateAtoms L = (eq', les, leq, neq)" using Cons(2) unfolding EqUni apply (cases "separateAtoms L") by auto
    then obtain eq' where eq' : "p#eq' = eq" "separateAtoms L = (eq', les, leq, neq)" by auto
    show ?thesis unfolding EqUni eq'(1)[symmetric] using Cons(1)[OF eq'(2)] by auto
  next
    case (LeqUni p)
    have "leq'. p#leq' = leq  separateAtoms L = (eq, les, leq', neq)" using Cons(2) unfolding LeqUni apply (cases "separateAtoms L")
      by auto
    then obtain leq' where leq' : "p#leq' = leq" "separateAtoms L = (eq, les, leq', neq)" by auto
    show ?thesis unfolding LeqUni leq'(1)[symmetric] using Cons(1)[OF leq'(2)] by auto
  next
    case (NeqUni p)
    have "neq'. p#neq' = neq  separateAtoms L = (eq, les, leq, neq')" using Cons(2) unfolding NeqUni apply (cases "separateAtoms L")
      by auto
    then obtain neq' where neq' : "p#neq' = neq" "separateAtoms L = (eq, les, leq, neq')" by auto
    show ?thesis unfolding NeqUni neq'(1)[symmetric] using Cons(1)[OF neq'(2)] by auto
  qed
qed

lemma set_split' : assumes "separateAtoms L = (eq,les,leq,neq)"
  shows "set (map P L) = set (map (P o EqUni) eq @ map (P o LessUni) les @ map (P o LeqUni) leq @ map (P o NeqUni) neq)"
  unfolding image_set[symmetric] set_split[OF assms]
  unfolding image_set map_append map_map by auto

lemma split_elimVar :
  assumes "separateAtoms L = (eq,les,leq,neq)"
  shows "(lset L. evalUni (elimVarUni_atom L' l) x) = 
  (((a',b',c')set eq. (evalUni (elimVarUni_atom L' (EqUni(a',b',c'))) x))
   ((a',b',c')set les. 
    (evalUni (elimVarUni_atom L' (LessUni(a',b',c'))) x))
 ((a',b',c')set leq. 
    (evalUni (elimVarUni_atom L' (LeqUni(a',b',c'))) x))
 ((a',b',c')set neq. 
    (evalUni (elimVarUni_atom L' (NeqUni(a',b',c'))) x)))"
proof-
  have c1: "(lset eq. evalUni (elimVarUni_atom L' (EqUni l)) x) = ((a', b', c')set eq. evalUni (elimVarUni_atom L' (EqUni (a', b', c'))) x)"
    by (metis (no_types, lifting) case_prodE case_prodI2)
  have c2: "(lset les. evalUni (elimVarUni_atom L' (LessUni l)) x) = ((a', b', c')set les. evalUni (elimVarUni_atom L' (LessUni (a', b', c'))) x)"
    by (metis (no_types, lifting) case_prodE case_prodI2)
  have c3: "(lset leq. evalUni (elimVarUni_atom L' (LeqUni l)) x) = ((a', b', c')set leq. evalUni (elimVarUni_atom L' (LeqUni (a', b', c'))) x)"
    by (metis (no_types, lifting) case_prodE case_prodI2)
  have c4: "(lset neq. evalUni (elimVarUni_atom L' (NeqUni l)) x) = ((a', b', c')set neq. evalUni (elimVarUni_atom L' (NeqUni (a', b', c'))) x)"
    by (metis (no_types, lifting) case_prodE case_prodI2)
  have h :  "((lEqUni ` set eq. evalUni (elimVarUni_atom L' l) x) 
         (lLessUni ` set les. evalUni (elimVarUni_atom L' l) x) 
    (lLeqUni ` set leq. evalUni (elimVarUni_atom L' l) x) 
    (lNeqUni ` set neq. evalUni (elimVarUni_atom L' l) x)
    ) = 
        ((lset eq. evalUni (elimVarUni_atom L' (EqUni l)) x) 
         (lset les. evalUni (elimVarUni_atom L' (LessUni l)) x) 
    (lset leq. evalUni (elimVarUni_atom L' (LeqUni l)) x) 
    (lset neq. evalUni (elimVarUni_atom L' (NeqUni l)) x)
    )"
    by auto
  then have "... = (((a', b', c')set eq. evalUni (elimVarUni_atom L' (EqUni (a', b', c'))) x) 
     ((a', b', c')set les. evalUni (elimVarUni_atom L' (LessUni (a', b', c'))) x) 
     ((a', b', c')set leq. evalUni (elimVarUni_atom L' (LeqUni (a', b', c'))) x) 
     ((a', b', c')set neq. evalUni (elimVarUni_atom L' (NeqUni (a', b', c'))) x))"
    using c1 c2 c3 c4 by auto
  then show ?thesis 
    unfolding set_split[OF assms] set_append bex_Un image_set[symmetric]
    using case_prodE case_prodI2  by auto
qed

lemma split_elimvar : 
  assumes "separateAtoms L = (eq,les,leq,neq)"
  shows "evalUni (elimVarUni_atom L At) x = evalUni (elimVarUni_atom ((map EqUni eq)@(map LessUni les) @ map LeqUni leq @ map NeqUni neq) At) x"
proof(cases At)
  case (LessUni p)
  then show ?thesis apply(cases p) apply simp unfolding eval_list_conj_Uni set_split'[OF assms] by simp
next
  case (EqUni p)
  then show ?thesis apply(cases p) apply simp unfolding eval_list_conj_Uni set_split'[OF assms] by simp
next
  case (LeqUni p)
  then show ?thesis apply(cases p) apply simp unfolding eval_list_conj_Uni set_split'[OF assms] by simp
next
  case (NeqUni p)
  then show ?thesis apply(cases p) apply simp unfolding eval_list_conj_Uni set_split'[OF assms] by simp
qed




lemma less : "
         ((a' = 0  b'  0) 
         ((d, e, f)set a. evalUni (substInfinitesimalLinearUni b' c' (EqUni (d, e, f))) x) 
         ((d, e, f)set b. evalUni (substInfinitesimalLinearUni b' c' (LessUni (d, e, f))) x) 
         ((d, e, f)set c. evalUni (substInfinitesimalLinearUni b' c' (LeqUni (d, e, f))) x) 
         ((d, e, f)set d. evalUni (substInfinitesimalLinearUni b' c' (NeqUni (d, e, f))) x) 
         a'  0 
         - b'2 + 4 * a' * c'  0 
         (((d, e, f)set a.
              evalUni
               (substInfinitesimalQuadraticUni (- b') 1 (b'2 - 4 * a' * c') (2 * a')
                 (EqUni (d, e, f)))
               x) 
          ((d, e, f)set b.
              evalUni
               (substInfinitesimalQuadraticUni (- b') 1 (b'2 - 4 * a' * c') (2 * a')
                 (LessUni (d, e, f)))
               x) 
          ((d, e, f)set c.
              evalUni
               (substInfinitesimalQuadraticUni (- b') 1 (b'2 - 4 * a' * c') (2 * a')
                 (LeqUni (d, e, f)))
               x) 
          ((d, e, f)set d.
              evalUni
               (substInfinitesimalQuadraticUni (- b') 1 (b'2 - 4 * a' * c') (2 * a')
                 (NeqUni (d, e, f)))
               x) 
          ((d, e, f)set a.
              evalUni
               (substInfinitesimalQuadraticUni (- b') (- 1) (b'2 - 4 * a' * c') (2 * a')
                 (EqUni (d, e, f)))
               x) 
          ((d, e, f)set b.
              evalUni
               (substInfinitesimalQuadraticUni (- b') (- 1) (b'2 - 4 * a' * c') (2 * a')
                 (LessUni (d, e, f)))
               x) 
          ((d, e, f)set c.
              evalUni
               (substInfinitesimalQuadraticUni (- b') (- 1) (b'2 - 4 * a' * c') (2 * a')
                 (LeqUni (d, e, f)))
               x) 
          ((d, e, f)set d.
              evalUni
               (substInfinitesimalQuadraticUni (- b') (- 1) (b'2 - 4 * a' * c') (2 * a')
                 (NeqUni (d, e, f)))
               x))) = 

          ((a' = 0  b'  0) 
         ((d, e, f)set a.
             (y'::real>-c'/b'. x::real {-c'/b'<..y'}. aEvalUni (EqUni (d, e, f)) x)) 
         ((d, e, f)set b.
            (y'::real>-c'/b'. x::real {-c'/b'<..y'}. aEvalUni (LessUni (d, e, f)) x))
         ((d, e, f)set c.
             (y'::real>-c'/b'. x::real {-c'/b'<..y'}. aEvalUni (LeqUni (d, e, f)) x)) 
         ((d, e, f)set d.
            (y'::real>-c'/b'. x::real {-c'/b'<..y'}. aEvalUni (NeqUni (d, e, f)) x)) 
         a'  0 
         - b'2 + 4 * a' * c'  0 
         (((d, e, f)set a.
              (y'>(- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a').
        x{(- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
           aEvalUni (EqUni (d,e,f)) x)) 
          ((d, e, f)set b.
              (y'>(- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a').
        x{(- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
           aEvalUni (LessUni (d,e,f)) x)) 
          ((d, e, f)set c.
              (y'>(- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a').
        x{(- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
           aEvalUni (LeqUni (d,e,f)) x)) 
          ((d, e, f)set d.
              (y'>(- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a').
        x{(- b' + 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
           aEvalUni (NeqUni (d,e,f)) x)) 
          ((d, e, f)set a.
              (y'>(- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a').
        x{(- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
           aEvalUni (EqUni (d,e,f)) x)) 
          ((d, e, f)set b.
              (y'>(- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a').
        x{(- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
           aEvalUni (LessUni (d,e,f)) x))  
          ((d, e, f)set c.
              (y'>(- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a').
        x{(- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
           aEvalUni (LeqUni (d,e,f)) x)) 
          ((d, e, f)set d.
              (y'>(- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a').
        x{(- b' + - 1 * sqrt (b'2 - 4 * a' * c')) / (2 * a')<..y'}.
           aEvalUni (NeqUni (d,e,f)) x))))"
proof(cases "a'=0")
  case True
  then have a' :  "a'=0" by auto
  then show ?thesis proof(cases "b'=0")
    case True
    then show ?thesis using a' by auto
  next
    case False
    then show ?thesis using True unfolding infinitesimal_linear'[of b' c' _ x, symmetric, OF False] by auto
  qed 
next
  case False
  then have a' : "a'  0" by auto
  then have d : "2 * a'  0" by auto
  show ?thesis proof(cases "0  b'2 - 4 * a' * c'")
    case True
    then show ?thesis using False
      unfolding infinitesimal_quad[OF d True, of "-b'", symmetric] by auto
  next
    case False
    then show ?thesis using a' by auto
  qed 
qed

lemma eq_inf : "((a, b, c)set (a::(real*real*real) list). x. y<x. a * y2 + b * y + c = 0) = ((a, b, c)set a. a=0b=0c=0)"
  using infinity_evalUni_EqUni[of _ x] by auto



text "This is the main quantifier elimination lemma, in the simplified framework. We are located directly underneath 
the most internal existential quantifier so F is completely free in quantifier and consists only of conjunction and disjunction.
The variable we are evaluating on, x, is removed in the generalVS\\_DNF converted formula as expanding out the evalUni function
determines that x doesn't play a role in the computation of it. It would be okay to replace the x in the second half with any variable,
but it is simplier this way

This conversion is defined as a \"veritcal\" translation as we remain within the univariate framework in both sides of the expression"

lemma eval_generalVS'' : "(x. evalUni (list_conj_Uni (map AtomUni L)) x) =
                               evalUni (generalVS_DNF L) x"
proof(cases "separateAtoms L")
  case (fields a b c d)
  have a : " P. (lset (map EqUni a)  (set (map LessUni b)  (set (map LeqUni c)  set (map NeqUni d))).P l) = 
            (((d,e,f)set a. P (EqUni (d,e,f)))  ((d,e,f)set b. P (LessUni (d,e,f)))  ((d,e,f)set c. P (LeqUni (d,e,f)))  ((d,e,f)set d. P (NeqUni (d,e,f))))"
    by auto
  show ?thesis apply(simp add: eval_list_conj_Uni separate_aEval[OF fields]
        splitAtoms_negInfinity[OF fields] eval_list_disj_Uni 
        del:elimVar.simps)

    unfolding eval_conj_atom generalVS_DNF.simps 
      split_elimVar[OF fields ] 

split_elimvar[OF fields]

    unfolding elimVarUni_atom.simps evalUni.simps aEvalUni.simps
      Rings.mult_zero_class.mult_zero_left Groups.add_0 eval_list_conj_Uni Groups.group_add_class.minus_zero 
      eval_map_all linearSubstitutionUni.simps quadraticSubUni.simps evalUni_if aEvalUni.simps
      set_append a less eq_inf
    using qe  by auto
qed


lemma forallx_substNegInf : "(¬evalUni (map_atomUni substNegInfinityUni F) x) = (x. ¬ evalUni (map_atomUni substNegInfinityUni F) x)"
proof(induction F)
  case TrueFUni
  then show ?case by simp
next
  case FalseFUni
  then show ?case  by simp
next
  case (AtomUni At)
  then show ?case apply(cases At) by auto  
next
  case (AndUni F1 F2)
  then show ?case  by auto
next
  case (OrUni F1 F2)
  then show ?case  by auto
qed

lemma linear_subst_map: "evalUni (map_atomUni (linearSubstitutionUni b c) F) x = evalUni F (-c/b)"
  apply(induction F)by auto

lemma quadratic_subst_map : "evalUni (map_atomUni (quadraticSubUni a b c d) F) x = evalUni F ((a+b*sqrt(c))/d)"
  apply(induction F)by auto




fun convert_atom_list :: "nat  atom list  real list  (atomUni list) option" where
  "convert_atom_list var [] xs = Some []"|
  "convert_atom_list var (a#as) xs = (
  case convert_atom var a xs of Some(a)  
  (case convert_atom_list var as xs of Some(as)  Some(a#as) | None  None)
   | None  None
)"





lemma convert_atom_list_change :
  assumes "length xs' = var"
  shows "convert_atom_list var L (xs' @ x # Γ) = convert_atom_list var L (xs' @ x' # Γ)"
  apply(induction L)using convert_atom_change[OF assms] apply simp_all
  by (metis)

lemma negInf_convert :
  assumes "convert_atom_list var L (xs' @ x # xs) = Some L'"
  assumes "length xs' = var"
  shows "(fset L. eval (substNegInfinity var f) (xs' @ x # xs))
         = (fset L'. evalUni (substNegInfinityUni f) x)"
  using assms
proof(induction L arbitrary : L')
  case Nil
  then show ?case by auto
next
  case (Cons a L)
  then show ?case proof(cases a)
    case (Less p)
    have h:  "MPoly_Type.degree p var < 3 
          eval (substNegInfinity var (Less p)) (xs' @ x # xs) = evalUni
           (substNegInfinityUni
             (LessUni
               (insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var 2),
                insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var (Suc 0)),
                insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var 0))))
           x"
      using convert_substNegInfinity[of var "Less p" xs' x xs, OF _ assms(2)] by simp
    show ?thesis using Cons(2)[symmetric] Cons(1) unfolding Less apply(cases " MPoly_Type.degree p var < 3")
      defer apply simp apply(cases "convert_atom_list var L (xs' @ x # xs)") apply (simp_all del: substNegInfinity.simps substNegInfinityUni.simps)
      unfolding h
      using assms(2) by presburger
  next
    case (Eq p)
    have h:  "MPoly_Type.degree p var < 3 
          eval (substNegInfinity var (Eq p)) (xs' @ x # xs) = evalUni
           (substNegInfinityUni
             (EqUni
               (insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var 2),
                insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var (Suc 0)),
                insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var 0))))
           x"
      using convert_substNegInfinity[of var "Eq p", OF _ assms(2)] by simp
    show ?thesis using Cons(2)[symmetric] Cons(1) unfolding Eq apply(cases " MPoly_Type.degree p var < 3")
      defer apply simp apply(cases "convert_atom_list var L (xs' @ x # xs)") apply (simp_all del: substNegInfinity.simps substNegInfinityUni.simps)
      unfolding h assms by auto
  next
    case (Leq p)
    have h:  "MPoly_Type.degree p var < 3 
          eval (substNegInfinity var (Leq p)) (xs' @ x # xs) = evalUni
           (substNegInfinityUni
             (LeqUni
               (insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var 2),
                insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var (Suc 0)),
                insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var 0))))
           x"
      using convert_substNegInfinity[of var "Leq p", OF _ assms(2)] by simp
    show ?thesis using Cons(2) unfolding Leq apply(cases " MPoly_Type.degree p var < 3") 
      defer apply simp 
      apply(cases "convert_atom_list var L (xs' @ x # xs)") 
      apply (simp_all del: substNegInfinity.simps substNegInfinityUni.simps)
      unfolding h using Cons.IH assms by auto 
  next
    case (Neq p)
    have h:  "MPoly_Type.degree p var < 3 
          eval (substNegInfinity var (Neq p)) (xs' @ x # xs) = evalUni
           (substNegInfinityUni
             (NeqUni
               (insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var 2),
                insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var (Suc 0)),
                insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var 0))))
           x"
      using convert_substNegInfinity[of var "Neq p", OF _ assms(2)] by simp
    show ?thesis using Cons(2) unfolding Neq apply(cases " MPoly_Type.degree p var < 3") defer apply simp 
      apply(cases "convert_atom_list var L (xs' @ x # xs)") 
      apply (simp_all del: substNegInfinity.simps substNegInfinityUni.simps)
      unfolding h using Cons.IH assms by auto
  qed
qed

lemma elimVar_atom_single :
  assumes "convert_atom var A (xs' @ x # xs) = Some A'"
  assumes "convert_atom_list var L2 (xs' @ x # xs) = Some L2'"
  assumes "length xs' = var"
  shows "eval (elimVar var L2 [] A) (xs' @ x # xs) = evalUni (elimVarUni_atom L2' A') x"
proof(cases A)
  case (Less p)
  define a where "a = insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var 2)"
  have a_def' : "a = insertion (nth_default 0 (xs' @ 0 # xs)) (isolate_variable_sparse p var 2)" unfolding a_def
    using insertion_isovarspars_free[of "(xs' @ x # xs)" var x p 2 0] assms by auto
  define b where "b = insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var (Suc 0))"
  have b_def' : "b = insertion (nth_default 0 (xs' @ 0 # xs)) (isolate_variable_sparse p var (Suc 0))" unfolding b_def
    using insertion_isovarspars_free[of "(xs' @ x # xs)" var x p "(Suc 0)" 0] assms by auto
  define c where "c = insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var 0)"
  have c_def' : "c = insertion (nth_default 0 (xs' @ 0 # xs)) (isolate_variable_sparse p var 0)" unfolding c_def
    using insertion_isovarspars_free[of "(xs' @ x # xs)" var x p 0 0] assms by auto
  have linear : "b0  (fset L2.
         eval
          (substInfinitesimalLinear var (-isolate_variable_sparse p var 0) (isolate_variable_sparse p var (Suc 0)) f)
          (xs' @ x # xs)) = (lset L2'. evalUni (substInfinitesimalLinearUni b c l) x)"
    using assms(2) proof(induction L2 arbitrary : L2')
    case Nil
    then show ?case by auto
  next
    case (Cons At L2)
    have "At'. convert_atom var At (xs' @ x # xs) = Some At'" proof(cases At)
      case (Less p)
      then show ?thesis using Cons(3) apply simp apply(cases "MPoly_Type.degree p var < 3") by simp_all
    next
      case (Eq p)
      then show ?thesis using Cons(3) apply simp apply(cases "MPoly_Type.degree p var < 3") by simp_all
    next
      case (Leq p)
      then show ?thesis using Cons(3) apply simp apply(cases "MPoly_Type.degree p var < 3") by auto
    next
      case (Neq p)
      then show ?thesis using Cons(3) apply simp apply(cases "MPoly_Type.degree p var < 3") by auto
    qed 
    then obtain At' where At' : "convert_atom var At (xs' @ x # xs) = Some At'" by auto
    have "L2's. convert_atom_list var L2 (xs' @ x # xs) = Some L2's"
      using Cons(3) At'
      apply(cases "convert_atom_list var L2 (xs' @ x # xs)") by auto
    then obtain L2's where L2's : "convert_atom_list var L2 (xs' @ x # xs) = Some L2's" by auto
    have L2' : "L2' = At' # L2's"
      using Cons(3) At'
      by (simp_all add: L2's)
    have h : "eval
         (substInfinitesimalLinear var (-isolate_variable_sparse p var 0) (isolate_variable_sparse p var (Suc 0))
            At)
         (xs' @ x # xs) = evalUni (substInfinitesimalLinearUni b c At') x"
    proof(cases "convert_atom var At (xs' @ x # xs)")
      case None
      then show ?thesis using At' apply(cases At)  by simp_all
    next
      case (Some a)
      have h1 : "var  vars (isolate_variable_sparse p var (Suc 0))"
        by (simp add: not_in_isovarspar) 
      have h2 : "var  vars (isolate_variable_sparse p var 0)"by (simp add: not_in_isovarspar) 
      have h :  "evalUni (substInfinitesimalLinearUni b c a) x =
    evalUni (substInfinitesimalLinearUni b c At') x"
      proof(cases At)
        case (Less p)
        then show ?thesis using At'[symmetric] Some[symmetric] apply(cases "MPoly_Type.degree p var < 3") by simp_all
      next
        case (Eq p)
        then show ?thesis using At'[symmetric] Some[symmetric] apply(cases "MPoly_Type.degree p var < 3") by simp_all
      next
        case (Leq x3)
        then show ?thesis using At' Some by auto 
      next
        case (Neq x4)
        then show ?thesis using At' Some by auto 
      qed
      show ?thesis unfolding convert_substInfinitesimalLinear[OF Some b_def[symmetric] c_def[symmetric] Cons(2) h1 h2 assms(3)]
        using h .
    qed
    show ?case unfolding L2' using h Cons(1)[OF Cons(2) L2's] by auto
  qed
  have quadratic_1 : "(a  0) 
     (4 * a * c  b2)  (fset L2.
          eval
           (substInfinitesimalQuadratic var
             (- isolate_variable_sparse p var (Suc 0)) 1
             ((isolate_variable_sparse p var (Suc 0))2 -
              4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0)
             (2 * isolate_variable_sparse p var 2) f)
           (xs' @ x # xs)) = (lset L2'.
          evalUni
           (substInfinitesimalQuadraticUni (- b) 1 (b2 - 4 * a * c) (2 * a) l)
           x)"
    using assms(2) proof(induction L2 arbitrary: L2')
    case Nil
    then show ?case by auto
  next
    case (Cons At L2)
    have "At'. convert_atom var At (xs' @ x # xs) = Some At'" proof(cases At)
      case (Less p)
      then show ?thesis using Cons(4) apply simp apply(cases "MPoly_Type.degree p var < 3") by simp_all
    next
      case (Eq p)
      then show ?thesis using Cons(4) apply simp apply(cases "MPoly_Type.degree p var < 3") by simp_all
    next
      case (Leq p)
      then show ?thesis using Cons(4) apply simp apply(cases "MPoly_Type.degree p var < 3") by auto
    next
      case (Neq p)
      then show ?thesis using Cons(4) apply simp apply(cases "MPoly_Type.degree p var < 3") by auto
    qed 
    then obtain At' where At' : "convert_atom var At (xs' @ x # xs) = Some At'" by auto
    have "L2's. convert_atom_list var L2 (xs' @ x # xs) = Some L2's"
      using Cons(4) At'
      apply(cases "convert_atom_list var L2 (xs' @ x # xs)") by auto
    then obtain L2's where L2's : "convert_atom_list var L2 (xs' @ x # xs) = Some L2's" by auto
    have L2' : "L2' = At' # L2's"
      using Cons(4) At' apply(cases At) apply auto
      by (simp_all add: L2's)
    have h1 :  "var < length (xs' @ x # xs)" using assms by auto
    have h2 : "2*a 0" using Cons by auto
    have h3 : "0b^2-4*a*c" using Cons(3) by auto
    have h4 : "varvars ((isolate_variable_sparse p var (Suc 0))2 -
            4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0)"
      by (metis add_uminus_conv_diff not_in_add not_in_isovarspar not_in_mult not_in_neg not_in_pow num_double numeral_times_numeral one_add_one power_0)
    have h5 : "xa. insertion (nth_default 0 ((xs' @ x # xs)[var := xa])) (- isolate_variable_sparse p var (Suc 0)) = -b"
      unfolding insertion_neg b_def
      by (metis insertion_isovarspars_free list_update_id) 
    have h6 : "xa. insertion (nth_default 0 ((xs' @ x # xs)[var := xa])) 1 = 1" by auto
    have h7 : "xa. insertion (nth_default 0 ((xs' @ x # xs)[var := xa]))
        ((isolate_variable_sparse p var (Suc 0))2 -
         4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0) =
       b2 - 4 * a * c" apply(simp add: insertion_four insertion_mult insertion_sub insertion_pow b_def a_def c_def)
      by (metis insertion_isovarspars_free list_update_id)
    have "xa. insertion (nth_default 0 (xs' @ xa # xs)) (2::real mpoly)  = (2::real)"
      by (metis MPoly_Type.insertion_one insertion_add one_add_one)  
    then have h8 : "xa. insertion (nth_default 0 ((xs' @ x # xs)[var := xa])) (2 * isolate_variable_sparse p var 2) = 2 * a"
      unfolding insertion_mult a_def apply auto
      by (metis assms(3) insertion_lowerPoly1 list_update_length not_in_isovarspar)
    have h9 : "varvars(- isolate_variable_sparse p var (Suc 0))"
      by (simp add: not_in_isovarspar not_in_neg)
    have h10 : "varvars(1::real mpoly)"
      by (metis h9 not_in_pow power.simps(1))
    have h11 : "varvars(2 * isolate_variable_sparse p var 2)"
      by (metis isovarspar_sum mult_2 not_in_isovarspar)
    have h :  "eval
      (substInfinitesimalQuadratic var (- isolate_variable_sparse p var (Suc 0)) 1
        ((isolate_variable_sparse p var (Suc 0))2 -
         4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0)
        (2 * isolate_variable_sparse p var 2) At)
      (xs' @ x # xs) =  evalUni
      (substInfinitesimalQuadraticUni (- b) 1 (b2 - 4 * a * c) (2 * a) At') x"
    proof (cases "convert_atom var At (xs' @ x # xs)")
      case None
      then show ?thesis using At' apply(cases At) by auto
    next
      case (Some aT)
      have h1 : "insertion (nth_default 0 (xs' @ x # xs)) (- isolate_variable_sparse p var (Suc 0)) = (-b)" unfolding b_def insertion_neg by auto
      have h2 : "insertion (nth_default 0 (xs' @ x # xs)) 1 = 1" by auto
      have h3 : "insertion (nth_default 0 (xs' @ x # xs)) (((isolate_variable_sparse p var (Suc 0))2 -
        4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0)) = (b2 - 4 * a * c)"
        unfolding insertion_mult insertion_pow insertion_four insertion_neg insertion_sub a_def b_def c_def
        by auto
      have h4 : "insertion (nth_default 0 (xs' @ x # xs)) (2 * isolate_variable_sparse p var 2) = 2 * a"
        unfolding insertion_mult a_def
        by (metis insertion_add insertion_mult mult_2)
      have h5 : "2 * a  0" using Cons by auto
      have h6 : "0  b2 - 4 * a * c" using Cons by auto
      have h7 : "varvars(- isolate_variable_sparse p var (Suc 0))"
        by (simp add: not_in_isovarspar not_in_neg)
      have h8 : "varvars(1::real mpoly)"
        by (metis h9 not_in_pow power.simps(1))
      have h9 : "var  vars ((isolate_variable_sparse p var (Suc 0))2 -
             4 * isolate_variable_sparse p var 2 *
             isolate_variable_sparse p var 0)"
        by (metis add_uminus_conv_diff not_in_add not_in_isovarspar not_in_mult not_in_neg not_in_pow num_double numeral_times_numeral one_add_one power_0)
      have h10 : "varvars(2 * isolate_variable_sparse p var 2)"
        by (metis isovarspar_sum mult_2 not_in_isovarspar)
      have h : "evalUni (substInfinitesimalQuadraticUni (- b) 1 (b2 - 4 * a * c) (2 * a) aT)
     x =
    evalUni (substInfinitesimalQuadraticUni (- b) 1 (b2 - 4 * a * c) (2 * a) At')
     x"proof(cases At)
        case (Less p)
        then show ?thesis using At'[symmetric] Some[symmetric] apply(cases "MPoly_Type.degree p var < 3") by auto
      next
        case (Eq p)
        then show ?thesis using At'[symmetric] Some[symmetric] apply(cases "MPoly_Type.degree p var < 3") by auto
      next
        case (Leq x3)
        then show ?thesis using At' using Some by auto
      next
        case (Neq x4)
        then show ?thesis using At' using Some by auto 
      qed
      show ?thesis unfolding convert_substInfinitesimalQuadratic[OF Some h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 assms(3)]
        using h .
    qed


    show ?case
      unfolding L2' apply(simp del : substInfinitesimalQuadratic.simps substInfinitesimalQuadraticUni.simps)
      unfolding 
        Cons(1)[OF Cons(2) Cons(3) L2's]
      unfolding h
      by auto
  qed
  have quadratic_2 : "(a  0) 
     (4 * a * c  b2)  (fset L2.
          eval
           (substInfinitesimalQuadratic var
             (- isolate_variable_sparse p var (Suc 0)) (- 1)
             ((isolate_variable_sparse p var (Suc 0))2 -
              4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0)
             (2 * isolate_variable_sparse p var 2) f)
           (xs' @ x # xs)) = (lset L2'.
          evalUni
           (substInfinitesimalQuadraticUni (- b) (- 1) (b2 - 4 * a * c) (2 * a)
             l)
           x)" 
    using assms(2) proof(induction L2 arbitrary: L2')
    case Nil
    then show ?case by auto
  next
    case (Cons At L2)
    have "At'. convert_atom var At (xs' @ x # xs) = Some At'" proof(cases At)
      case (Less p)
      then show ?thesis using Cons(4) apply simp apply(cases "MPoly_Type.degree p var < 3") by simp_all
    next
      case (Eq p)
      then show ?thesis using Cons(4) apply simp apply(cases "MPoly_Type.degree p var < 3") by simp_all
    next
      case (Leq p)
      then show ?thesis using Cons(4) apply simp apply(cases "MPoly_Type.degree p var < 3") by auto
    next
      case (Neq p)
      then show ?thesis using Cons(4) apply simp apply(cases "MPoly_Type.degree p var < 3") by auto
    qed 
    then obtain At' where At' : "convert_atom var At (xs' @ x # xs) = Some At'" by auto
    have "L2's. convert_atom_list var L2 (xs' @ x # xs) = Some L2's"
      using Cons(4) At'
      apply(cases "convert_atom_list var L2 (xs' @ x # xs)") by auto
    then obtain L2's where L2's : "convert_atom_list var L2 (xs' @ x # xs) = Some L2's" by auto
    have L2' : "L2' = At' # L2's"
      using Cons(4) At' apply(cases At) apply auto
      by (simp_all add: L2's)
    have h1 :  "var < length (xs' @ x # xs)" using assms by auto
    have h2 : "2*a 0" using Cons by auto
    have h3 : "0b^2-4*a*c" using Cons(3) by auto
    have h4 : "varvars ((isolate_variable_sparse p var (Suc 0))2 -
            4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0)"
      by (metis add_uminus_conv_diff not_in_add not_in_isovarspar not_in_mult not_in_neg not_in_pow num_double numeral_times_numeral one_add_one power_0)
    have h5 : "xa. insertion (nth_default 0 ((xs' @ x # xs)[var := xa])) (- isolate_variable_sparse p var (Suc 0)) = -b"
      unfolding insertion_neg b_def
      by (metis insertion_isovarspars_free list_update_id) 
    have h6 : "xa. insertion (nth_default 0 ((xs' @ x # xs)[var := xa])) (-1) = (-1)" unfolding insertion_neg by auto
    have h7 : "xa. insertion (nth_default 0 ((xs' @ x # xs)[var := xa]))
        ((isolate_variable_sparse p var (Suc 0))2 -
         4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0) =
       b2 - 4 * a * c" apply(simp add: insertion_four insertion_mult insertion_sub insertion_pow b_def a_def c_def) using assms
      by (metis insertion_isovarspars_free list_update_id)
    have "xa. insertion (nth_default 0 (xs' @ xa # xs)) (2::real mpoly)  = (2::real)"
      by (metis MPoly_Type.insertion_one insertion_add one_add_one)  
    then have h8 : "xa. insertion (nth_default 0 ((xs' @ x # xs)[var := xa])) (2 * isolate_variable_sparse p var 2) = 2 * a"
      unfolding insertion_mult a_def apply auto using assms
      by (metis (no_types, opaque_lifting) MPoly_Type.insertion_one add.inverse_inverse add_uminus_conv_diff arith_special(3) insertion_isovarspars_free insertion_neg insertion_sub list_update_id) 
    have h9 : "varvars(- isolate_variable_sparse p var (Suc 0))"
      by (simp add: not_in_isovarspar not_in_neg)
    have h10 : "varvars(- 1::real mpoly)"
      by (metis h9 not_in_neg not_in_pow power.simps(1))
    have h11 : "varvars(2 * isolate_variable_sparse p var 2)"
      by (metis isovarspar_sum mult_2 not_in_isovarspar)
    have h :  "eval
      (substInfinitesimalQuadratic var (- isolate_variable_sparse p var (Suc 0)) (-1)
        ((isolate_variable_sparse p var (Suc 0))2 -
         4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0)
        (2 * isolate_variable_sparse p var 2) At)
      (xs' @ x # xs) =  evalUni
      (substInfinitesimalQuadraticUni (- b) (-1) (b2 - 4 * a * c) (2 * a) At') x"
    proof (cases "convert_atom var At (xs' @ x # xs)")
      case None
      then show ?thesis using At' apply(cases At) by auto
    next
      case (Some aT)
      have h1 : "insertion (nth_default 0 (xs' @ x # xs)) (- isolate_variable_sparse p var (Suc 0)) = (-b)" unfolding b_def insertion_neg by auto
      have h2 : "insertion (nth_default 0 (xs' @ x # xs)) (-1) = -1" unfolding insertion_neg by auto
      have h3 : "insertion (nth_default 0 (xs' @ x # xs)) (((isolate_variable_sparse p var (Suc 0))2 -
        4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 0)) = (b2 - 4 * a * c)"
        unfolding insertion_mult insertion_pow insertion_four insertion_neg insertion_sub a_def b_def c_def using assms
        by auto
      have h4 : "insertion (nth_default 0 (xs' @ x # xs)) (2 * isolate_variable_sparse p var 2) = 2 * a"
        unfolding insertion_mult a_def
        by (metis insertion_add insertion_mult mult_2)
      have h5 : "2 * a  0" using Cons by auto
      have h6 : "0  b2 - 4 * a * c" using Cons by auto
      have h7 : "varvars(- isolate_variable_sparse p var (Suc 0))"
        by (simp add: not_in_isovarspar not_in_neg)
      have h8 : "varvars(- 1::real mpoly)"
        by (simp add: h10 not_in_neg)
      have