# 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 "(∀l∈set 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+c≤0) ∧ (∀(a,b,c)∈set d. a*x^2+b*x+c≠0))"
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) ⟹
(∀l∈set L. aEvalUni l x) =
((∀a∈set a. case a of (a, ba, c) ⇒ a * x⇧2 + ba * x + c = 0) ∧
(∀a∈set b. case a of (a, ba, c) ⇒ a * x⇧2 + ba * x + c < 0)∧
(∀a∈set c. case a of (a, ba, c) ⇒ a * x⇧2 + ba * x + c ≤ 0) ∧
(∀a∈set d. case a of (a, ba, c) ⇒ a * x⇧2 + 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 : "(∀a∈set (p # b'). case a of (a, ba, c) ⇒ a * x⇧2 + ba * x + c < 0) = (
(∀a∈set (b'). case a of (a, ba, c) ⇒ a * x⇧2 + ba * x + c < 0)∧ (case p of (a, ba, c) ⇒ a * x⇧2 + ba * x + c < 0))"
by auto
have h3 : "(∀l∈set (LessUni p # L). aEvalUni l x) = ((∀l∈set (L). aEvalUni l x)∧(case p of (a, ba, c) ⇒ a * x⇧2 + 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 : "(∀a∈set (p # a'). case a of (a, ba, c) ⇒ a * x⇧2 + ba * x + c = 0) = (
(∀a∈set (a'). case a of (a, ba, c) ⇒ a * x⇧2 + ba * x + c = 0)∧ (case p of (a, ba, c) ⇒ a * x⇧2 + ba * x + c = 0))"
by auto
have h3 : "(∀l∈set (EqUni p # L). aEvalUni l x) = ((∀l∈set (L). aEvalUni l x)∧(case p of (a, ba, c) ⇒ a * x⇧2 + 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 : "(∀a∈set (p # a'). case a of (a, ba, c) ⇒ a * x⇧2 + ba * x + c ≤ 0) = (
(∀a∈set (a'). case a of (a, ba, c) ⇒ a * x⇧2 + ba * x + c ≤ 0)∧ (case p of (a, ba, c) ⇒ a * x⇧2 + ba * x + c ≤ 0))"
by auto
have h3 : "(∀l∈set (LeqUni p # L). aEvalUni l x) = ((∀l∈set (L). aEvalUni l x)∧(case p of (a, ba, c) ⇒ a * x⇧2 + 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 : "(∀a∈set (p # a'). case a of (a, ba, c) ⇒ a * x⇧2 + ba * x + c ≠ 0) = (
(∀a∈set (a'). case a of (a, ba, c) ⇒ a * x⇧2 + ba * x + c ≠ 0)∧ (case p of (a, ba, c) ⇒ a * x⇧2 + ba * x + c ≠ 0))"
by auto
have h3 : "(∀l∈set (NeqUni p # L). aEvalUni l x) = ((∀l∈set (L). aEvalUni l x)∧(case p of (a, ba, c) ⇒ a * x⇧2 + 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 "(∀l∈set 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+c≤0))∧
(∀(a,b,c)∈set d.(∃x. ∀y<x. a*y^2+b*y+c≠0)))"
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) ⟹
(∀l∈set L. evalUni (substNegInfinityUni l) x) =
((∀a∈set a. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c = 0) ∧
(∀a∈set b. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c < 0)∧
(∀a∈set c. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≤ 0)∧
(∀a∈set d. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + 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 : "(∀a∈set (p # b'). case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c < 0) = (
(∀a∈set ( b'). case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c < 0)∧ (case p of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + 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 * y⇧2 + ba * y + c < 0)"
apply(cases p) by simp
have "(∀l∈set (LessUni p # L). evalUni (substNegInfinityUni l) x) = ((evalUni (substNegInfinityUni (LessUni p)) x)∧(∀l∈set ( L). evalUni (substNegInfinityUni l) x))"
by auto
also have "... = (
(case p of (a,ba,c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c < 0)∧
(∀a∈set a. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c = 0) ∧
(∀a∈set b'. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c < 0)∧
(∀a∈set c. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≤ 0)∧
(∀a∈set d. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≠ 0))"
unfolding infinity_evalUni[of "LessUni p" x, symmetric] Cons(3)[OF h1]  LessUni one by simp
finally have h3 : "(∀l∈set (LessUni p # L). evalUni (substNegInfinityUni l) x) = (
(case p of (a,ba,c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c < 0)∧
(∀a∈set a. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c = 0) ∧
(∀a∈set b'. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c < 0)∧
(∀a∈set c. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≤ 0)∧
(∀a∈set d. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + 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 : "(∀a∈set (p # a'). case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c = 0) = (
(∀a∈set ( a'). case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c = 0)∧ (case p of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + 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 * y⇧2 + ba * y + c = 0)"
apply(cases p) by simp
have "(∀l∈set (EqUni p # L). evalUni (substNegInfinityUni l) x) = ((evalUni (substNegInfinityUni (EqUni p)) x)∧(∀l∈set ( L). evalUni (substNegInfinityUni l) x))"
by auto
also have "... = (
(case p of (a,ba,c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c = 0)∧
(∀a∈set a'. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c = 0) ∧
(∀a∈set b. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c < 0)∧
(∀a∈set c. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≤ 0)∧
(∀a∈set d. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≠ 0))"
unfolding infinity_evalUni[of "EqUni p" x, symmetric] Cons(3)[OF h1] EqUni one by simp
finally have h3 : "(∀l∈set (EqUni p # L). evalUni (substNegInfinityUni l) x) = (
(case p of (a,ba,c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c = 0)∧
(∀a∈set a'. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c = 0) ∧
(∀a∈set b. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c < 0)∧
(∀a∈set c. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≤ 0)∧
(∀a∈set d. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + 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 : "(∀a∈set (p # c'). case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≤ 0) = (
(∀a∈set ( c'). case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≤ 0)∧ (case p of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + 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 * y⇧2 + ba * y + c ≤ 0)"
apply(cases p) by simp
have "(∀l∈set (LeqUni p # L). evalUni (substNegInfinityUni l) x) = ((evalUni (substNegInfinityUni (LeqUni p)) x)∧(∀l∈set ( L). evalUni (substNegInfinityUni l) x))"
by auto
also have "... = (
(case p of (a,ba,c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≤ 0)∧
(∀a∈set a. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c = 0) ∧
(∀a∈set b. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c < 0)∧
(∀a∈set c'. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≤ 0)∧
(∀a∈set d. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≠ 0))"
unfolding infinity_evalUni[of "LeqUni p" x, symmetric] Cons(3)[OF h1]  LeqUni one
by simp
finally have h3 : "(∀l∈set (LeqUni p # L). evalUni (substNegInfinityUni l) x) = (
(case p of (a,ba,c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≤ 0)∧
(∀a∈set a. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c = 0) ∧
(∀a∈set b. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c < 0)∧
(∀a∈set c'. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≤ 0)∧
(∀a∈set d. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + 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 : "(∀a∈set (p # d'). case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≠ 0) = (
(∀a∈set ( d'). case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≠ 0)∧ (case p of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + 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 * y⇧2 + ba * y + c ≠ 0)"
apply(cases p) by simp
have "(∀l∈set (NeqUni p # L). evalUni (substNegInfinityUni l) x) = ((evalUni (substNegInfinityUni (NeqUni p)) x)∧(∀l∈set ( L). evalUni (substNegInfinityUni l) x))"
by auto
also have "... = (
(case p of (a,ba,c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≠ 0)∧
(∀a∈set a. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c = 0) ∧
(∀a∈set b. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c < 0)∧
(∀a∈set c. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≤ 0)∧
(∀a∈set d'. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≠ 0))"
unfolding infinity_evalUni[of "NeqUni p" x, symmetric] Cons(3)[OF h1]  NeqUni one
by simp
finally have h3 : "(∀l∈set (NeqUni p # L). evalUni (substNegInfinityUni l) x) = (
(case p of (a,ba,c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≠ 0)∧
(∀a∈set a. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c = 0) ∧
(∀a∈set b. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c < 0)∧
(∀a∈set c. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + ba * y + c ≤ 0)∧
(∀a∈set d'. case a of (a, ba, c) ⇒ ∃x. ∀y<x. a * y⇧2 + 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 "(∃l∈set 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: "(∃l∈set 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: "(∃l∈set 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: "(∃l∈set 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: "(∃l∈set 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 :  "((∃l∈EqUni ` set eq. evalUni (elimVarUni_atom L' l) x) ∨
(∃l∈LessUni ` set les. evalUni (elimVarUni_atom L' l) x) ∨
(∃l∈LeqUni ` set leq. evalUni (elimVarUni_atom L' l) x) ∨
(∃l∈NeqUni ` set neq. evalUni (elimVarUni_atom L' l) x)
) =
((∃l∈set eq. evalUni (elimVarUni_atom L' (EqUni l)) x) ∨
(∃l∈set les. evalUni (elimVarUni_atom L' (LessUni l)) x) ∨
(∃l∈set leq. evalUni (elimVarUni_atom L' (LeqUni l)) x) ∨
(∃l∈set 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 * y⇧2 + b * y + c = 0) = (∀(a, b, c)∈set a. a=0∧b=0∧c=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. (∀l∈set (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
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 "(∀f∈set L. eval (substNegInfinity var f) (xs' @ x # xs))
= (∀f∈set 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 : "b≠0 ⟹ (∀f∈set L2.
eval
(substInfinitesimalLinear var (-isolate_variable_sparse p var 0) (isolate_variable_sparse p var (Suc 0)) f)
(xs' @ x # xs)) = (∀l∈set 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'
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))"
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 ≤ b⇧2) ⟹ (∀f∈set L2.
eval
(- 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)) = (∀l∈set L2'.
evalUni
(substInfinitesimalQuadraticUni (- b) 1 (b⇧2 - 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
have h1 :  "var < length (xs' @ x # xs)" using assms by auto
have h2 : "2*a ≠0" using Cons by auto
have h3 : "0≤b^2-4*a*c" using Cons(3) by auto
have h4 : "var∉vars ((isolate_variable_sparse p var (Suc 0))⇧2 -
4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 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) =
b⇧2 - 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)"
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 : "var∉vars(- isolate_variable_sparse p var (Suc 0))"
have h10 : "var∉vars(1::real mpoly)"
by (metis h9 not_in_pow power.simps(1))
have h11 : "var∉vars(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 (b⇧2 - 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)) = (b⇧2 - 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
have h5 : "2 * a ≠ 0" using Cons by auto
have h6 : "0 ≤ b⇧2 - 4 * a * c" using Cons by auto
have h7 : "var∉vars(- isolate_variable_sparse p var (Suc 0))"
have h8 : "var∉vars(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)"
have h10 : "var∉vars(2 * isolate_variable_sparse p var 2)"
by (metis isovarspar_sum mult_2 not_in_isovarspar)
have h : "evalUni (substInfinitesimalQuadraticUni (- b) 1 (b⇧2 - 4 * a * c) (2 * a) aT)
x =
evalUni (substInfinitesimalQuadraticUni (- b) 1 (b⇧2 - 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
Cons(1)[OF Cons(2) Cons(3) L2's]
unfolding h
by auto
qed
have quadratic_2 : "(a ≠ 0) ⟹
(4 * a * c ≤ b⇧2) ⟹ (∀f∈set L2.
eval
(- 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)) = (∀l∈set L2'.
evalUni
(substInfinitesimalQuadraticUni (- b) (- 1) (b⇧2 - 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
have h1 :  "var < length (xs' @ x # xs)" using assms by auto
have h2 : "2*a ≠0" using Cons by auto
have h3 : "0≤b^2-4*a*c" using Cons(3) by auto
have h4 : "var∉vars ((isolate_variable_sparse p var (Suc 0))⇧2 -
4 * isolate_variable_sparse p var 2 * isolate_variable_sparse p var 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) =
b⇧2 - 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)"
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 : "var∉vars(- isolate_variable_sparse p var (Suc 0))"
have h10 : "var∉vars(- 1::real mpoly)"
by (metis h9 not_in_neg not_in_pow power.simps(1))
have h11 : "var∉vars(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) (b⇧2 - 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)) = (b⇧2 - 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