# Theory NegInfinity

```subsection "Negative Infinity"
theory NegInfinity
imports "HOL-Analysis.Poly_Roots" VSAlgos
begin

lemma freeIn_allzero : "freeIn var (allZero p var)"

lemma allzero_eval :
assumes lLength : "var < length L"
shows"(∃x. ∀y<x. aEval (Eq p) (list_update L var y) ) = (∀x. eval (allZero p var) (list_update L var x))"
proof-
define n where "n = MPoly_Type.degree p var"
define k where "k i x =((insertion (nth_default 0(list_update L var x)) (isolate_variable_sparse p var i)))" for i x
{fix x
have "(eval (allZero p var) (list_update L var x)) =
(∀i∈{0..<(MPoly_Type.degree p var)+1}. aEval (Eq(isolate_variable_sparse p var i)) (list_update L var x))"
also have "... = (∀i∈{0..<(MPoly_Type.degree p var)+1}. (insertion (nth_default 0(list_update L var x)) (isolate_variable_sparse p var i))=0)"
by simp
also have "... = (∀i≤(MPoly_Type.degree p var). (insertion (nth_default 0(list_update L var x)) (isolate_variable_sparse p var i))=0)"
by fastforce
also have "... = (∀y. (∑i≤(MPoly_Type.degree p var). ((insertion (nth_default 0(list_update L var x)) (isolate_variable_sparse p var i)) * y ^ i))=0)"
using polyfun_eq_const[where n="MPoly_Type.degree p var", where k="0", where c="λi. (insertion (nth_default 0(list_update L var x)) (isolate_variable_sparse p var i))"]
also have "... = (∀y. (∑i≤n. (k i x) * y ^ i)=0)"
using k_def n_def by simp
finally have  "(eval (allZero p var) (list_update L var x)) = (∀y. (∑i≤n. (k i x) * y ^ i)=0)"
by simp
}
then have h1 : "(∀x. (eval (allZero p var) (list_update L var x))) = (∀x.(∀y. (∑i≤n. (k i x) * y ^ i)=0))"
by simp

have "(∃y. ∀x<y. (∑i≤n. (k i x)* x^i)= 0) = (∃y. ∀x<y. (∑i≤(MPoly_Type.degree p var). (insertion (nth_default 0 (list_update L var x))(isolate_variable_sparse p var i))* x^i)= 0)"
using k_def n_def by simp
also have "... = (∃y. ∀x<y. insertion (nth_default 0 (list_update L var x)) (∑i≤(MPoly_Type.degree p var). (isolate_variable_sparse p var i)* Var var^i)= 0)"
by(simp add: insertion_sum' insertion_mult insertion_pow insertion_var lLength)
also have "... = (∃y. ∀x<y. insertion (nth_default 0 (list_update L var x)) p = 0)"
using sum_over_zero  by simp
also have "... = (∃y. ∀x<y. aEval (Eq p) (list_update L var x))"
by simp
finally have h2 : "(∃y. ∀x<y. aEval (Eq p) (list_update L var x)) = (∃y. ∀x<y. (∑i≤n. (k i x)* x^i)= 0)"
by simp

have k_all : "∀x y i. k i x = k i y"
unfolding k_def
have h3a : "(∃y. ∀x<y. (∑i≤n. (k i x)* x^i)= 0) ⟹ (∀x.(∀y. (∑i≤n. (k i x) * y ^ i)=0))"
proof-
assume h : "(∃y. ∀x<y. (∑i≤n. (k i x)* x^i)= 0)"
{fix z y
assume h : "(∀x<y. (∑i≤n. (k i x)* x^i)= 0)"
have "∀x<y.∀i≤n. k i x = k i z"
unfolding k_def
using insertion_isovarspars_free by blast
then have * : "∀x<y.∀i≤n. k i x * x ^ i = k i z * x^i"
by auto
then have "∀x<y. (∑i≤n. k i x * x ^ i) = (∑i≤n. k i z * x ^ i)"
by (metis (no_types, lifting) k_all sum.cong)
then have "∀x<y. (∑i≤n. (k i z)* x^i)= 0"
using h  by simp
then have "¬(finite {x. (∑i≤n. k i z * x ^ i) = 0})"
using infinite_Iio[where a="y"]  Inf_many_def[where P="λx. (∑i≤n. k i z * x ^ i) = 0"]
by (smt INFM_iff_infinite frequently_mono lessThan_def)
then have "∀i≤n. k i z = 0"
using  polyfun_rootbound[where n="n",  where c = "λi. k i z" ]
by blast
}
then have "∀x.∀i≤n. k i x = 0"
using h
by (meson gt_ex)
then show ?thesis by simp
qed
have h3b : "(∀x.(∀y. (∑i≤n. (k i x) * y ^ i)=0)) ⟹ (∃y. ∀x<y. (∑i≤n. (k i x)* x^i)= 0)"
proof-
assume h : "(∀x.(∀y. (∑i≤n. (k i x) * y ^ i)=0))"
{fix z y x
have "(∑i≤n. (k i z)* x^i)= 0"
using h k_all by blast
then have "∀i≤n. k i z = 0"
using polyfun_eq_const[where k="0", where c = "λi. k i z", where n="n"]
by (metis h)
}
then have "∀x.∀i≤n. k i x = 0"
by (meson gt_ex)
then show ?thesis by simp
qed
have h3 : "(∃y. ∀x<y. (∑i≤n. (k i x)* x^i)= 0) = (∀x.(∀y. (∑i≤n. (k i x) * y ^ i)=0))"
using h3a h3b by auto
show ?thesis using h1 h2 h3 by simp
qed

lemma freeIn_altNegInf : "freeIn var (alternateNegInfinity p var)"
proof-
have h1 : "∀i. var ∉ (vars (if (i::nat) mod 2 = 0 then (Const(1)::real mpoly) else (Const(-1)::real mpoly)))"
using var_not_in_Const[where var = "var", where x="1"] var_not_in_Const[where var = "var", where x="-1"]
by simp
define g where "g = (λF.λi.
let a_n = isolate_variable_sparse p var i in
let exp = (if i mod 2 = 0 then Const(1) else Const(-1)) in
or (Atom(Less (exp * a_n)))
(and (Atom (Eq a_n)) F)
)"
have h3 : "∀i. ∀F. (freeIn var F ⟶ freeIn var (g F i))"
using g_def h1
by (smt PolyAtoms.and_def not_in_isovarspar PolyAtoms.or_def freeIn.simps(1) freeIn.simps(2) freeIn.simps(7) freeIn.simps(8) not_in_mult)
define L where "L = ([0..<((MPoly_Type.degree p var)+1)])"
have "∀F. freeIn var F ⟶ freeIn var (foldl (g::atom fm ⇒ nat ⇒ atom fm) F (L::nat list))"
proof(induction L)
case Nil
then show ?case by simp
next
case (Cons a L)
then show ?case using h3 by simp
qed
then have "freeIn var (foldl g FalseF L)"
using freeIn.simps(6) by blast
then show ?thesis using g_def L_def by simp
qed

theorem freeIn_substNegInfinity : "freeIn var (substNegInfinity var A)"
apply(cases A) using freeIn_altNegInf freeIn_allzero by simp_all

end
```