# Theory InfinitesimalsUni

```theory InfinitesimalsUni
imports Infinitesimals UniAtoms NegInfinityUni QE

begin

fun convertDerivativeUni ::  "real * real * real ⇒ atomUni fmUni" where
"convertDerivativeUni (a,b,c) =
OrUni(AtomUni(LessUni(a,b,c)))(AndUni(AtomUni(EqUni(a,b,c)))(
OrUni(AtomUni(LessUni(0,2*a,b)))(AndUni(AtomUni(EqUni(0,2*a,b)))(
(AtomUni(LessUni(0,0,2*a)))
))
))
"

lemma convert_convertDerivative :
assumes "convert_poly var p (xs'@x#xs) = Some(a,b,c)"
assumes "length xs' = var"
shows "eval (convertDerivative var p) (xs'@x#xs) = evalUni (convertDerivativeUni (a,b,c)) x"
proof(cases "MPoly_Type.degree p var = 0")
case True
then show ?thesis using assms apply (simp add: isovar_greater_degree eval_or eval_and insertion_mult insertion_const)
using sum_over_zero[of p var] by auto
next
case False
then have nonzero: "MPoly_Type.degree p var ≠ 0" by auto
then show ?thesis proof(cases "MPoly_Type.degree p var = 1")
case True
have h1 : "MPoly_Type.degree p var < 3" using True by auto
have h2 : "get_coeffs var p = (isolate_variable_sparse p var 2, isolate_variable_sparse p var 1, isolate_variable_sparse p var 0)" by auto
have h : "insertion (nth_default 0 (xs' @ x # xs)) p = b * x + c"
using poly_to_univar[OF h1 h2 _ _ _ assms(2), of  a x xs b c x] using assms(1) apply(cases "MPoly_Type.degree p var < 3") apply simp_all
using isovar_greater_degree[of p var] unfolding True by simp
have h3: "MPoly_Type.degree (isolate_variable_sparse p var (Suc 0) * Const 1) var = 0"
using degree_mult[of "isolate_variable_sparse p var (Suc 0)" "Const 1" var]
using degree_isovarspar mult_one_right by presburger
show ?thesis
using assms True
unfolding convertDerivative.simps[of _ p] convertDerivative.simps[of _ "(derivative var p)"]
apply (simp add: derivative_def isovar_greater_degree eval_or eval_and insertion_add insertion_mult insertion_const HOL.arg_cong[OF sum_over_zero[of p var], of "insertion (nth_default var (xs'@x#xs))"] insertion_var_zero del:convertDerivative.simps)
unfolding h     h3 by(simp del:convertDerivative.simps)
next
case False
then have deg2 :  "MPoly_Type.degree p var = 2"
by (metis One_nat_def assms(1) convert_poly.simps le_SucE less_Suc0 less_Suc_eq_le nonzero numeral_2_eq_2 numeral_3_eq_3 option.distinct(1))
then have first : "isolate_variable_sparse p var (Suc (Suc 0)) ≠ 0"
by (metis MPoly_Type.degree_zero isolate_variable_sparse_degree_eq_zero_iff nat.distinct(1) numeral_2_eq_2)
have second : "(isolate_variable_sparse p var (Suc (Suc 0)) * Var var)≠0"
by (metis MPoly_Type.degree_zero One_nat_def ExecutiblePolyProps.degree_one Zero_not_Suc first mult_eq_0_iff)
have other : "Const (2::real)≠0"
have thing: "(Var var::real mpoly) ≠ 0"
using second by auto
have degree: "MPoly_Type.degree
(isolate_variable_sparse p var (Suc 0) * Const 1 +
isolate_variable_sparse p var (Suc (Suc 0)) * Var var * Const 2)
var -
Suc 0 = 0"
apply simp apply(rule Nat.eq_imp_le) apply(rule degree_less_sum'[of _ _ 0])
apply (simp add: degree_isovarspar mult_one_right)  apply auto
unfolding degree_mult[OF second other, of var] degree_const apply simp
unfolding degree_mult[OF first thing] degree_one
using degree_isovarspar by force
have insertion: "insertion (nth_default 0 (xs'@x#xs)) (∑(i::nat)≤2. isolate_variable_sparse p var i * Var var ^ i) = a * x^2 + b * x + c"
proof(cases "MPoly_Type.degree p var = 1")
case True
then show ?thesis
using False by blast
next
case False
then have deg2 :  "MPoly_Type.degree p var = 2"
by (metis One_nat_def assms(1) convert_poly.simps le_SucE less_Suc0 less_Suc_eq_le nonzero numeral_2_eq_2 numeral_3_eq_3 option.distinct(1))
then have degless3 : "MPoly_Type.degree p var < 3" by auto
have thing : "var<length(xs'@x # xs)" using assms by auto
have h : "(∑i≤2. isolate_variable_sparse p var i * Var var ^ i) = p"
using deg2
by (metis sum_over_zero)
have three: "(3::nat) = Suc(Suc(Suc(0)))" by auto
have "(∑i = 0..<3. insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var i) * x ^ i) =
(insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 0) * x ^ 0) +
(insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var (1::nat)) * x ^ (1::nat)) +
(insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var (2::nat)) * x ^ (2::nat))"
proof -
have "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var (MPoly_Type.degree p var)) * x ^ MPoly_Type.degree p var + (x * insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 1) + (insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 0) + (∑n = 0..<0. insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var n) * x ^ n))) = insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 0) + x * insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 1) + insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var (MPoly_Type.degree p var)) * x ^ MPoly_Type.degree p var"
by auto
then show "(∑n = 0..<0. insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var n) * x ^ n) + insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 0) * x ^ 0 + insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var (Suc 0)) * x ^ Suc 0 + insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var (Suc (Suc 0))) * x ^ Suc (Suc 0) = insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 0) * x ^ 0 + insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 1) * x ^ 1 + insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 2) * x⇧2"
by (metis (no_types) One_nat_def Suc_1 add.commute deg2 mult.commute mult.left_neutral power_0 power_one_right)
qed
also have "... =  a * x⇧2 + b * x + c"
unfolding Power.power_class.power.power_0 Power.monoid_mult_class.power_one_right Groups.monoid_mult_class.mult_1_right
using assms unfolding convert_poly.simps using degless3 by simp
finally have h2  :"(∑i = 0..<3. insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var i) * x ^ i) =  a * x⇧2 + b * x + c "
.
show ?thesis using sum_over_degree_insertion[OF thing deg2, of x] apply auto  using h h2 using assms(2) by auto
qed
have insertionb: "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var (Suc 0)) = b"
using assms apply(cases "MPoly_Type.degree p var < 3") by simp_all
have insertiona : "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var (Suc (Suc 0))) = a"
using assms apply(cases "MPoly_Type.degree p var < 3")  apply simp_all
have x :  "insertion (nth_default 0 (xs' @ x # xs)) (Var var) = x" using insertion_var[of var "(xs' @ x # xs)" x] using assms(2) by auto
have zero1 : "insertion (nth_default 0 (xs' @ x # xs))
(isolate_variable_sparse (isolate_variable_sparse p var (Suc 0)) var (Suc 0)) = 0"
have zero2 : "insertion (nth_default 0 (xs' @ x # xs))
(isolate_variable_sparse (isolate_variable_sparse p var (Suc (Suc 0))) var 0) = a"
using degree0isovarspar degree_isovarspar insertiona by presburger
have zero3 : "insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse (Var var) var (Suc 0)) = 1" using isolate_var_one
using MPoly_Type.insertion_one by fastforce
have zero4 : "insertion (nth_default 0 (xs' @ x # xs))
(isolate_variable_sparse (isolate_variable_sparse p var (Suc (Suc 0))) var (Suc 0)) = 0"
have insertion_deriv : "insertion (nth_default 0 (xs'@x#xs))
(isolate_variable_sparse
(isolate_variable_sparse p var (Suc 0) * Const 1 +
isolate_variable_sparse p var (Suc (Suc 0)) * Var var * Const 2)
var (Suc 0)) = 2*a"
unfolding isovarspar_sum isolate_variable_sparse_mult apply auto
unfolding const_lookup_suc const_lookup_zero Rings.mult_zero_class.mult_zero_right
unfolding insertion_add insertion_mult insertion_const apply auto
unfolding zero1 zero2 zero3 zero4 by simp
have deg2 : "MPoly_Type.degree p var = 2" using degree_convert_eq[OF assms(1)] False nonzero by auto
then show ?thesis
using assms
unfolding convertDerivative.simps[of _ p] convertDerivative.simps[of _ "(derivative var p)"] convertDerivative.simps[of _ "(derivative var (derivative var p))"]
apply (simp add: x insertionb insertiona insertion_deriv insertion degree derivative_def isovar_greater_degree eval_or eval_and insertion_add insertion_mult insertion_const HOL.arg_cong[OF sum_over_zero[of p var], of "insertion (nth_default 0 (xs'@x#xs))"] insertion_var_zero del:convertDerivative.simps)
by (smt (z3) One_nat_def degree_isovarspar distrib_right insertion_deriv isolate_variable_sparse_ne_zeroD mult_one_right neq0_conv not_one_le_zero zero1)
qed
qed

fun linearSubstitutionUni :: "real ⇒ real ⇒ atomUni ⇒ atomUni fmUni" where
"linearSubstitutionUni b c a = (if aEvalUni a (-c/b) then TrueFUni else FalseFUni)"

lemma convert_linearSubstitutionUni:
assumes "convert_atom var a (xs'@x#xs) = Some(a')"
assumes "insertion (nth_default 0 (xs'@x#xs)) b = B"
assumes "insertion (nth_default 0 (xs'@x#xs)) c = C"
assumes "B ≠ 0"
assumes "var∉(vars b)"
assumes "var∉(vars c)"
assumes "length xs' = var"
shows "aEval (linear_substitution var (-c) b a) (xs'@x#xs) = evalUni (linearSubstitutionUni B C a') x"
using assms
proof -
have "aEval a (xs'@(-C/B)#xs) = evalUni (linearSubstitutionUni B C a') x"
using assms(1) proof(cases "a")
case (Less p)
then have "MPoly_Type.degree p var < 3" using assms(1)apply(cases "MPoly_Type.degree p var < 3") by auto
then show ?thesis
using Less assms apply simp
using poly_to_univar by force
next
case (Eq p)
then have "MPoly_Type.degree p var < 3" using assms(1)apply(cases "MPoly_Type.degree p var < 3") by auto
then show ?thesis
using Eq assms apply simp
using poly_to_univar by force
next
case (Leq p)
then have "MPoly_Type.degree p var < 3" using assms(1)apply(cases "MPoly_Type.degree p var < 3") by auto
then show ?thesis
using Leq assms apply simp
using poly_to_univar by force
next
case (Neq p)
then have "MPoly_Type.degree p var < 3" using assms(1)apply(cases "MPoly_Type.degree p var < 3") by auto
then show ?thesis
using Neq assms apply simp
using poly_to_univar by force
qed
then have subst : "aEval a ((xs'@x#xs)[var := - C / B]) = evalUni (linearSubstitutionUni B C a') x" using assms by auto
have hlength : "var< length (xs'@x#xs)" using assms by auto
have inB : "insertion (nth_default 0 ((xs'@x#xs)[var := - C / B])) b = B" using assms apply auto apply(cases a) apply auto
have inC : "insertion (nth_default 0 ((xs'@x#xs)[var := - C / B])) (-c) = -C" using assms apply auto apply(cases a) apply auto
have freenegc : "var∉vars(-c)" using assms not_in_neg by auto
show ?thesis using linear[OF hlength assms(4)  freenegc assms(5) inC inB, of a ] subst
using  var_not_in_eval3[OF var_not_in_linear[OF freenegc assms(5)] assms(7)]
by (metis assms(7) list_update_length)
qed
(*
substInfinitesimalLinear var b c A
substitutes -c/b+epsilon for variable var in atom A
assumes b is nonzero
defined in page 615
*)
fun substInfinitesimalLinearUni :: "real ⇒ real ⇒ atomUni ⇒ atomUni fmUni" where
"substInfinitesimalLinearUni b c (EqUni p) = allZero' p"|
"substInfinitesimalLinearUni b c (LessUni p) =
map_atomUni (linearSubstitutionUni b c) (convertDerivativeUni p)"|
"substInfinitesimalLinearUni b c (LeqUni p) =
OrUni
(allZero' p)
(map_atomUni (linearSubstitutionUni b c) (convertDerivativeUni p))"|
"substInfinitesimalLinearUni b c (NeqUni p) = negUni (allZero' p)"

lemma convert_linear_subst_fm :
assumes "convert_atom var a (xs'@x#xs) = Some a'"
assumes "insertion (nth_default 0 (xs'@x#xs)) b = B"
assumes "insertion (nth_default 0 (xs'@x#xs)) c = C"
assumes "B ≠ 0"
assumes "var∉(vars b)"
assumes "var∉(vars c)"
assumes "length xs' = var"
shows "aEval (linear_substitution (var + 0) (liftPoly 0 0 (-c)) (liftPoly 0 0 b) a) (xs'@x#xs) =
evalUni (linearSubstitutionUni B C a') x"
proof-
have lb : "insertion (nth_default 0 (xs'@x#xs)) (liftPoly 0 0 b) = B" unfolding lift00 using assms(2) by auto
have lc : "insertion (nth_default 0 (xs'@x#xs)) (liftPoly 0 0 c) = C" unfolding lift00 using assms(3) insertion_neg by auto
have nb : "var ∉ vars (liftPoly 0 0 b)" using not_in_lift[OF assms(5), of 0] by auto
have nc : "var ∉ vars (liftPoly 0 0 c)" using not_in_lift[OF assms(6)] not_in_neg
using assms(6) lift00 by auto
then show ?thesis using assms using lb lc convert_linearSubstitutionUni[OF assms(1)  lb lc assms(4) nb nc]
qed

lemma evalUni_if : "evalUni (if cond then TrueFUni else FalseFUni) x = cond"
by(cases cond)(auto)

lemma degree_less_sum' : "MPoly_Type.degree (p::real mpoly) var = n ⟹ MPoly_Type.degree (q::real mpoly) var = m ⟹ n < m ⟹ MPoly_Type.degree (p + q) var = m"
using degree_less_sum[of q var m p n]

lemma convert_substInfinitesimalLinear_less :
assumes "convert_poly var p (xs'@x#xs) = Some(p')"
assumes "insertion (nth_default 0 (xs'@x#xs)) b = B"
assumes "insertion (nth_default 0 (xs'@x#xs)) c = C"
assumes "B ≠ 0"
assumes "var∉(vars b)"
assumes "var∉(vars c)"
assumes "length xs' = var"
shows "
eval (liftmap
(λx. λA. Atom(linear_substitution (var+x) (liftPoly 0 x (-c)) (liftPoly 0 x b) A))
(convertDerivative var p)
0) (xs'@x#xs) =
evalUni (map_atomUni (linearSubstitutionUni B C) (convertDerivativeUni p')) x"
proof(cases p')
case (fields a' b' c')
have h : "convert_poly var p (xs'@x#xs) = Some (a', b', c')"
using assms fields by auto
have h2 : "∃F'. convert_fm var (convertDerivative var p) xs = Some F'"
unfolding convertDerivative.simps[of _ p] convertDerivative.simps[of _ "derivative var p"] convertDerivative.simps[of _ "derivative var (derivative var p)"]
apply( auto simp del: convertDerivative.simps)
using degree_convert_eq h apply blast
using assms(1) degree_convert_eq apply blast
apply (metis Suc_eq_plus1 degree_derivative gr_implies_not0 less_trans_Suc nat_neq_iff)
using assms(1) degree_convert_eq apply blast
apply (meson assms(1) degree_convert_eq)
apply (metis One_nat_def Suc_eq_plus1 degree_derivative less_2_cases less_Suc_eq nat_neq_iff numeral_3_eq_3 one_add_one)
using assms(1) degree_convert_eq apply blast
using degree_derivative apply force
using assms(1) degree_convert_eq apply blast
apply (meson assms(1) degree_convert_eq)
apply (metis degree_derivative eq_numeral_Suc less_add_one less_trans_Suc not_less_eq numeral_2_eq_2 pred_numeral_simps(3))
apply (meson assms(1) degree_convert_eq)
using degree_derivative apply fastforce
by (meson assms(1) degree_convert_eq)
have c'_insertion : "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 0) = c'"
using assms fields unfolding convert_poly.simps apply(cases "MPoly_Type.degree p var < 3") by auto
have b'_insertion : "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var (Suc 0)) = b'"
using assms fields unfolding convert_poly.simps apply(cases "MPoly_Type.degree p var < 3") by auto
then have b'_insertion2 : "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 1) = b'"
by auto
have a'_insertion : "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 2) = a'"
using assms fields unfolding convert_poly.simps apply(cases "MPoly_Type.degree p var < 3") by auto
have liftb : "liftPoly 0 0 b = b" using lift00 by auto
have liftc : "liftPoly 0 0 c = c" using lift00 by auto
have b'_insertion' : "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse (isolate_variable_sparse p var (Suc 0)) var 0) = b'"
using assms fields unfolding convert_poly.simps apply(cases "MPoly_Type.degree p var < 3") apply auto
have insertion_into_1 : "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse (Const 1) var 0) = 1"
have twominusone : "((2-1)::nat) = 1" by auto
show ?thesis
proof(cases "MPoly_Type.degree p var = 0")
case True
have simp: "(convertDerivative var p)=Atom(Less p)"
using True
by auto
have azero : "a'=0"
by (metis MPoly_Type.insertion_zero True a'_insertion isolate_variable_sparse_ne_zeroD nat.simps(3) not_less numeral_2_eq_2 zero_less_iff_neq_zero)
have bzero : "b'=0"
using True b'_insertion isovar_greater_degree by fastforce
show ?thesis unfolding fields substInfinitesimalLinearUni.simps
convertDerivativeUni.simps linearSubstitutionUni.simps map_atomUni.simps evalUni.simps evalUni_if aEvalUni.simps
substInfinitesimalLinear.simps convertDerivative.simps[of _ p] True simp liftmap.simps
linear_substitution.simps
unfolding c'_insertion by auto
next
case False
then have degnot0 : "MPoly_Type.degree p var ≠ 0" by auto
then show ?thesis
proof(cases "MPoly_Type.degree p var = 1")
case True
then have simp : "convertDerivative var p = Or (fm.Atom (Less p)) (And (fm.Atom (Eq p)) (fm.Atom (Less (derivative var p))))"
by (metis One_nat_def Suc_eq_plus1 add_right_imp_eq convertDerivative.simps degnot0 degree_derivative zero_less_one)
have azero : "a'=0"
by (metis MPoly_Type.insertion_zero One_nat_def True a'_insertion isovar_greater_degree lessI numeral_2_eq_2)
have degderiv : "MPoly_Type.degree (isolate_variable_sparse p var (Suc 0) * Const 1) var = 0"
using degree_mult
show ?thesis
unfolding fields substInfinitesimalLinearUni.simps
convertDerivativeUni.simps linearSubstitutionUni.simps map_atomUni.simps evalUni.simps evalUni_if aEvalUni.simps
substInfinitesimalLinear.simps True simp liftmap.simps
linear_substitution.simps eval_Or eval_And liftb liftc
apply auto
unfolding derivative_def True insertion_sub insertion_mult c'_insertion b'_insertion assms lift00 apply auto
unfolding insertion_sub insertion_mult c'_insertion b'_insertion assms lift00
apply (smt diff_divide_eq_iff divide_less_0_iff mult_less_0_iff)
apply (smt mult_imp_less_div_pos neg_less_divide_eq zero_le_mult_iff)
using assms(4) mult.commute nonzero_mult_div_cancel_left
apply smt
unfolding degderiv apply auto
unfolding isolate_variable_sparse_mult apply auto
unfolding insertion_mult defer
apply (smt assms(4) diff_divide_eq_iff divide_less_0_iff mult_less_0_iff)
defer
using assms(4) apply blast
unfolding b'_insertion' insertion_into_1 apply auto
by (smt assms(4) less_divide_eq mult_pos_neg2 no_zero_divisors zero_less_mult_pos)
next
case False
then have degreetwo : "MPoly_Type.degree p var = 2" using degnot0
by (metis One_nat_def degree_convert_eq h less_2_cases less_Suc_eq numeral_2_eq_2 numeral_3_eq_3)
have two : "(2::nat) = Suc(Suc 0)" by auto
have sum : "(∑i = 0..<2. isolate_variable_sparse p var i * (- c) ^ i * b ^ (2 - i)) =
isolate_variable_sparse p var 0 * (- c) ^ 0 * b ^ (2 - 0) + isolate_variable_sparse p var 1 * (- c) ^ 1 * b ^ (2 - 1) "
have a : "isolate_variable_sparse p var (Suc (Suc 0)) ≠ 0"
by (metis degnot0 degree_isovarspar degreetwo isolate_variable_sparse_degree_eq_zero_iff numeral_2_eq_2)
have b : "((Var var * Const 2) :: real mpoly) ≠ (0::real mpoly)"
by (metis MPoly_Type.degree_zero ExecutiblePolyProps.degree_one mult_eq_0_iff nonzero_const_is_nonzero zero_neq_numeral zero_neq_one)
have degreedeg1 : "MPoly_Type.degree
(isolate_variable_sparse p var (Suc 0) * Const 1 +
isolate_variable_sparse p var (Suc (Suc 0)) * Var var * Const 2)
var  = 1"
apply(rule degree_less_sum'[where n ="0"])
apply (simp add: degree_isovarspar mult_one_right) defer
apply simp
using degree_mult[OF a b, of var]
by (metis (no_types, opaque_lifting) ExecutiblePolyProps.degree_one add.left_neutral b degree_const degree_isovarspar degree_mult mult.commute mult_zero_class.mult_zero_right)
have simp : "(convertDerivative var p) = Or (fm.Atom (Less p))
(And (fm.Atom (Eq p))
(Or (fm.Atom (Less (derivative var p)))
(And (fm.Atom (Eq (derivative var p))) (fm.Atom (Less (derivative var (derivative var p)))))))"
using degreetwo
by (metis One_nat_def Suc_1 Suc_eq_plus1 add_diff_cancel_right' convertDerivative.simps degree_derivative neq0_conv zero_less_Suc)
have a : "insertion (nth_default 0 (xs'@x#xs))
(isolate_variable_sparse
(isolate_variable_sparse p var (Suc 0) * Const 1 +
isolate_variable_sparse p var (Suc (Suc 0)) * Var var * Const 2)
var 0) = b'" unfolding isovarspar_sum isolate_variable_sparse_mult apply auto
unfolding const_lookup_suc const_lookup_zero Rings.mult_zero_class.mult_zero_right
by (simp add: b'_insertion' isolate_var_0 mult_one_right)
have b : "insertion (nth_default 0 (xs'@x#xs))
(isolate_variable_sparse
(isolate_variable_sparse p var (Suc 0) * Const 1 +
isolate_variable_sparse p var (Suc (Suc 0)) * Var var * Const 2)
var (Suc 0)) = 2 * a'"
unfolding isovarspar_sum isolate_variable_sparse_mult apply auto
unfolding const_lookup_suc const_lookup_zero Rings.mult_zero_class.mult_zero_right
by (metis MPoly_Type.insertion_one MPoly_Type.insertion_zero One_nat_def a'_insertion add.commute add.right_neutral degree0isovarspar degree_isovarspar isolate_var_one isovar_greater_degree mult.commute mult.right_neutral mult_zero_class.mult_zero_right numeral_2_eq_2 zero_less_one)
have simp_insertion_blob : "insertion (nth_default 0 (xs'@x#xs))
(isolate_variable_sparse
(isolate_variable_sparse p var (Suc 0) * Const 1 +
isolate_variable_sparse p var (Suc (Suc 0)) * Var var * Const 2)
var 0 *
b -
isolate_variable_sparse
(isolate_variable_sparse p var (Suc 0) * Const 1 +
isolate_variable_sparse p var (Suc (Suc 0)) * Var var * Const 2)
var (Suc 0) *
c) = b' * B - 2 * a' * C"
unfolding insertion_sub insertion_mult assms a b by auto
have a : "isolate_variable_sparse
(isolate_variable_sparse p var (Suc 0) * Const 1 +
isolate_variable_sparse p var (Suc (Suc 0)) * Var var * Const 2)
var (Suc 0) ≠ 0"
by (metis MPoly_Type.degree_zero One_nat_def degreedeg1 isolate_variable_sparse_degree_eq_zero_iff zero_neq_one)
have b' : "(Const 1::real mpoly) ≠ 0"
have degreeblob : "MPoly_Type.degree
(isolate_variable_sparse
(isolate_variable_sparse p var (Suc 0) * Const 1 +
isolate_variable_sparse p var (Suc (Suc 0)) * Var var * Const 2)
var (Suc 0) *
Const 1)
var = 0"
unfolding degree_mult[OF a b', of var]
by (simp add: degree_isovarspar degree_eq_iff monomials_Const)
have otherblob : "insertion (nth_default 0 (xs'@x#xs))
(isolate_variable_sparse
(isolate_variable_sparse
(isolate_variable_sparse p var (Suc 0) * Const 1 +
isolate_variable_sparse p var (Suc (Suc 0)) * Var var * Const 2)
var (Suc 0) *
Const 1)
var 0) = 2 * a'" using b
by (simp add: degree0isovarspar degree_isovarspar mult_one_right)

have "(c' * B⇧2 - b' * C * B + a' * C⇧2 < 0) = ((c' * B⇧2 - b' * C * B + a' * C⇧2)/(B⇧2) < 0)"
also have "... = (((c' * B⇧2)/(B⇧2) - (b' * C * B)/(B⇧2) + (a' * C⇧2)/(B⇧2)) < 0)"
by (metis (no_types, lifting) add_divide_distrib diff_divide_distrib )
also have "... = (a' * (C / B)⇧2 - b' * C / B + c' < 0)"
proof -
{ assume "c' + a' * (C / B)⇧2 - b' * (C / B) < 0"
then have ?thesis
by (simp add: assms(4) power2_eq_square) }
moreover
{ assume "¬ c' + a' * (C / B)⇧2 - b' * (C / B) < 0"
then have ?thesis
ultimately show ?thesis
by fastforce
qed
finally have h1: "(c' * B⇧2 - b' * C * B + a' * C⇧2 < 0) = (a' * (C / B)⇧2 - b' * C / B + c' < 0)"
.
have "(c' * B⇧2 - b' * C * B + a' * C⇧2 = 0) = ((c' * B⇧2 - b' * C * B + a' * C⇧2)/(B⇧2) = 0)"
also have "... = (((c' * B⇧2)/(B⇧2) - (b' * C * B)/(B⇧2) + (a' * C⇧2)/(B⇧2)) = 0)"
by (metis (no_types, lifting) add_divide_distrib diff_divide_distrib )
also have "... = (a' * (C / B)⇧2 - b' * C / B + c' = 0)"
proof -
{ assume "c' + a' * (C * (C / (B * B))) - b' * (C / B) ≠ 0"
then have ?thesis
by (simp add: assms(4) power2_eq_square) }
moreover
{ assume "c' + a' * (C * (C / (B * B))) - b' * (C / B) = 0"
then have ?thesis
ultimately show ?thesis
by fastforce
qed
finally have h2 : "(c' * B⇧2 - b' * C * B + a' * C⇧2 = 0) = (a' * (C / B)⇧2 - b' * C / B + c' = 0)"
.
have h3 : "((b' * B - 2 * a' * C) * B < 0) = (b' < 2 * a' * C / B)"
by (smt assms(4) less_divide_eq zero_le_mult_iff)
have h4 : "(b' * B = 2 * a' * C) = (b' = 2 * a' * C / B)"
show ?thesis unfolding fields substInfinitesimalLinearUni.simps
convertDerivativeUni.simps linearSubstitutionUni.simps map_atomUni.simps evalUni.simps evalUni_if aEvalUni.simps
substInfinitesimalLinear.simps degreetwo simp liftmap.simps
linear_substitution.simps eval_Or eval_And liftb liftc
apply simp
unfolding derivative_def degreetwo insertion_sub insertion_mult c'_insertion b'_insertion assms  apply simp
unfolding sum insertion_add insertion_mult insertion_pow insertion_neg assms
unfolding b'_insertion2 c'_insertion a'_insertion
unfolding Power.power_class.power.power_0  Groups.monoid_mult_class.mult_1_right
twominusone degreedeg1 apply simp
unfolding insertion_mult assms simp_insertion_blob degreeblob
unfolding insertion_mult insertion_sub assms otherblob apply simp
unfolding otherblob h1 h2 h3 h4 unfolding lift00 insertion_neg assms insertion_isovarspars_free insertion_sum insertion_mult insertion_sub degree0isovarspar degree_isovarspar mult_one_right insertion_sum_var insertion_pow insertion_neg sum
unfolding assms b'_insertion c'_insertion a'_insertion insertion_neg insertion_mult insertion_add insertion_pow apply simp
by (smt assms(2) assms(3) b'_insertion h1 h2 h3 h4 insertion_mult insertion_sub mult_one_right simp_insertion_blob)
qed
qed
qed
lemma convert_substInfinitesimalLinear:
assumes "convert_atom var a (xs'@x#xs) = Some(a')"
assumes "insertion (nth_default 0 (xs'@x#xs)) b = B"
assumes "insertion (nth_default 0 (xs'@x#xs)) c = C"
assumes "B ≠ 0"
assumes "var∉(vars b)"
assumes "var∉(vars c)"
assumes "length xs' = var"
shows "eval (substInfinitesimalLinear var (-c) b a) (xs'@x#xs) = evalUni (substInfinitesimalLinearUni B C a') x"
using assms
proof(cases a)
case (Less p)
have "∃p'. convert_poly var p (xs'@x#xs) = Some p'"
using Less assms(1) apply(cases "MPoly_Type.degree p var < 3") by auto
then obtain p' where p'_def : "convert_poly var p (xs'@x#xs) = Some p'" by auto
have A'_simp :  "a' = LessUni p'"
using assms Less
using p'_def by auto
have h1 : "eval (convertDerivative var p) (xs'@x#xs) = evalUni (convertDerivativeUni p') x" using convert_convertDerivative
apply ( cases p')
using A'_simp Less assms by auto
show ?thesis unfolding A'_simp using convert_substInfinitesimalLinear_less[OF p'_def assms(2-7)] unfolding Less by auto
next
case (Eq p)
define p' where "p' = (case convert_poly var p (xs'@x#xs) of Some p' ⇒ p')"
have A'_simp :  "a' = EqUni p'"
using assms Eq
using p'_def by auto
show ?thesis
unfolding Eq A'_simp substInfinitesimalLinear.simps substInfinitesimalLinearUni.simps
using convert_allZero A'_simp Eq assms by auto
next
case (Leq p)
have "∃p'. convert_poly var p (xs' @ x # xs) = Some p'"
using assms(1) unfolding Leq apply auto apply(cases "MPoly_Type.degree p var < 3") by auto
then obtain p' where p'_def : "convert_poly var p (xs' @ x # xs) = Some p'" by metis
have A'_simp :  "a' = LeqUni p'"
using assms Leq
using p'_def by auto
have h1 : "eval (convertDerivative var p) (xs'@x#xs) = evalUni (convertDerivativeUni p') x" using convert_convertDerivative
apply(cases p')
using A'_simp Leq assms by auto
show ?thesis unfolding A'_simp Leq substInfinitesimalLinear.simps eval_Or substInfinitesimalLinearUni.simps evalUni.simps
using convert_substInfinitesimalLinear_less[OF p'_def assms(2-7)]
convert_allZero[OF p'_def assms(7)] by simp
next
case (Neq p)
have "∃p'. convert_poly var p (xs' @ x # xs) = Some p'"
using assms(1) unfolding Neq apply auto apply(cases "MPoly_Type.degree p var < 3") by auto
then obtain p' where p'_def : "convert_poly var p (xs' @ x # xs) = Some p'" by metis
have A'_simp :  "a' = NeqUni p'"
using assms Neq
using p'_def by auto
show ?thesis
unfolding Neq A'_simp substInfinitesimalLinear.simps substInfinitesimalLinearUni.simps
using convert_allZero[OF p'_def assms(7)]
by (metis A'_simp Neq assms(1) assms(7) convert_substNegInfinity eval.simps(6) eval_neg substNegInfinityUni.simps(4) substNegInfinity.simps(4))
qed

lemma either_or:
fixes r :: "real"
assumes a: "(∃y'>r. ∀x∈{r<..y'}.  (aEvalUni (EqUni (a, b, c)) x) ∨ (aEvalUni (LessUni (a, b, c)) x))"
shows "(∃y'>r. ∀x∈{r<..y'}.  (aEvalUni (EqUni (a, b, c)) x)) ∨
(∃y'>r. ∀x∈{r<..y'}.  (aEvalUni (LessUni (a, b, c)) x))"
proof  (cases "a = 0 ∧ b = 0 ∧ c= 0")
case True
then have "(∃y'>r. ∀x∈{r<..y'}.  (aEvalUni (EqUni (a, b, c)) x))"
using assms by auto
then show ?thesis
by blast
next
case False
then have noz: "a≠0 ∨ b≠0 ∨ c≠0" by auto
obtain y1' where y1prop: "y1' > r ∧ (∀x∈{r<..y1'}. (aEvalUni (EqUni (a, b, c)) x) ∨ (aEvalUni (LessUni (a, b, c)) x))"
using a by auto
obtain y2' where y2prop: "y2' > r ∧ (∀x∈{r<..y2'}. a * x⇧2 + b * x + c ≠ 0)"
using noz nonzcoeffs[of a b c] by auto
let ?y = "min y1' y2'"
have ygt: "?y > r" using y1prop y2prop by auto
have "∀x∈{r<..?y}. (aEvalUni (LessUni (a, b, c)) x)"
using y1prop y2prop greaterThanAtMost_iff
by force
then show ?thesis using ygt
by blast
qed

lemma infinitesimal_linear'_helper :
assumes at_is: "At = LessUni p ∨ At = EqUni p"
assumes "B ≠ 0"
shows "((∃y'::real>-C/B. ∀x::real ∈{-C/B<..y'}. aEvalUni At x)
= evalUni (substInfinitesimalLinearUni B C At) x)"
proof (cases "At = LessUni p")
case True
then have LessUni: "At = LessUni p" by auto
then show ?thesis proof(cases p)
case (fields a b c)
then show ?thesis
unfolding LessUni fields
using one_root_a_lt0[where r="C/B", where a= "a", where b="b",where c= "c"] apply(auto)
using continuity_lem_lt0_expanded[where a= "a", where b = "2 * a * C / B ", where c = "c"]  apply (auto)
using continuity_lem_gt0_expanded[where a = "a", where b = "2 * a * C / B",where c = "c", where r = "- (C / B)"] apply (auto)
apply (meson less_eq_real_def linorder_not_less)
using one_root_a_gt0[where r = "C/B", where a = "a", where b="b", where c="c"] apply (auto)
using continuity_lem_lt0_expanded[where a= "a", where b = "2 * a * C / B", where c= "c"]
apply (auto)
using continuity_lem_gt0_expanded[where a = "a", where b = "2 * a * C / B",where c = "c", where r = "- (C / B)"]
apply (auto) apply (meson less_eq_real_def linorder_not_less)
using case_d1 apply (auto)
using continuity_lem_lt0_expanded[where a= "a", where b = "b", where c= "c"]
apply (auto)
using continuity_lem_gt0_expanded[where a = "a", where b = "b",where c = "c", where r = "- (C / B)"]
apply (auto) apply (meson less_eq_real_def linorder_not_less)
using case_d4 apply (auto)
using continuity_lem_lt0_expanded[where a= "a", where b = "b", where c= "c"]
apply (auto)
using continuity_lem_gt0_expanded[where a = "a", where b = "b",where c = "c", where r = "- (C / B)"]
apply (auto)
by (meson less_eq_real_def linorder_not_le)
qed
next
case False
then have EqUni: "At = EqUni p" using at_is by auto
then show ?thesis proof(cases p)
case (fields a b c)
show ?thesis
using continuity_lem_eq0[where r= "-(C/B)"] apply blast
using continuity_lem_eq0[where r= "-(C/B)"] apply blast
using continuity_lem_eq0[where r= "-(C/B)"] apply blast
using linordered_field_no_ub by blast
qed
qed

(* I assume substInfinitesimalLinearUni' was supposed to be substInfinitesimalLinearUni?*)
lemma infinitesimal_linear' :
assumes "B ≠ 0"
shows "(∃y'::real>-C/B. ∀x::real ∈{-C/B<..y'}. aEvalUni At x)
= evalUni (substInfinitesimalLinearUni B C At) x"
proof(cases At)
case (LessUni p)
then show ?thesis using infinitesimal_linear'_helper[of At p B C] assms by auto
next
case (EqUni p)
then show ?thesis  using infinitesimal_linear'_helper[of At p B C] assms by (auto)
next
case (LeqUni p)
then show ?thesis proof(cases p)
case (fields a b c)
have same: "∀x. aEvalUni (LeqUni p) x = (aEvalUni (EqUni p) x) ∨ (aEvalUni (LessUni p) x)"
by force
have "⋀a b c.
At = LeqUni p ⟹
p = (a, b, c) ⟹
(∃y'>- C / B. ∀x∈{- C / B<..y'}. aEvalUni At x) =
evalUni (substInfinitesimalLinearUni B C At) x "
proof -
fix a b c
assume atis: "At = LeqUni p"
assume p_is: " p = (a, b, c)"
have s1: "(∃y'>- C / B. ∀x∈{- C / B<..y'}. aEvalUni At x) = (∃y'>- C / B. ∀x∈{- C / B<..y'}.  (aEvalUni (EqUni p) x) ∨ (aEvalUni (LessUni p) x))"
using atis same aEvalUni.simps(2) aEvalUni.simps(3) fields less_eq_real_def
by blast
have s2: "... = (∃y'>- C / B. ∀x∈{- C / B<..y'}.  (aEvalUni (EqUni p) x)) ∨ (∃y'>- C / B. ∀x∈{- C / B<..y'}. (aEvalUni (LessUni p) x))"
using either_or[where r = "-C/B"] p_is
by blast
have eq1: "(∃y'>- C / B. ∀x∈{- C / B<..y'}.  (aEvalUni (EqUni p) x)) =  (evalUni (substInfinitesimalLinearUni B C (EqUni p)) x)"
using infinitesimal_linear'_helper[where At = "EqUni p", where p = "p", where B = "B", where C= "C"]
assms by auto
have eq2: "(∃y'>- C / B. ∀x∈{- C / B<..y'}. (aEvalUni (LessUni p) x)) = (evalUni (substInfinitesimalLinearUni B C (LessUni p)) x)"
using infinitesimal_linear'_helper[where At = "LessUni p", where p = "p", where B = "B", where C= "C"]
assms by auto
have z1: "(∃y'>- C / B. ∀x∈{- C / B<..y'}. aEvalUni At x) = ((evalUni (substInfinitesimalLinearUni B C (EqUni p)) x) ∨ (evalUni (substInfinitesimalLinearUni B C (LessUni p)) x))"
using s1 s2 eq1 eq2  by auto
have z2: "(evalUni (substInfinitesimalLinearUni B C (EqUni p)) x) ∨ (evalUni (substInfinitesimalLinearUni B C (LessUni p)) x) = evalUni (substInfinitesimalLinearUni B C (LeqUni p)) x"
by auto
have z3: "(evalUni (substInfinitesimalLinearUni B C At) x) = evalUni (substInfinitesimalLinearUni B C (LeqUni p)) x"
using LeqUni by auto
then have z4: "(evalUni (substInfinitesimalLinearUni B C (EqUni p)) x) ∨ (evalUni (substInfinitesimalLinearUni B C (LessUni p)) x) = (evalUni (substInfinitesimalLinearUni B C At) x) "
using z2 z3 by auto
let ?a = "(evalUni (substInfinitesimalLinearUni B C (EqUni p)) x) ∨ (evalUni (substInfinitesimalLinearUni B C (LessUni p)) x)"
let ?b = "(∃y'>- C / B. ∀x∈{- C / B<..y'}. aEvalUni At x)"
let ?c = "(evalUni (substInfinitesimalLinearUni B C At) x)"
have t1: "?b = ?a" using z1 by auto
have t2: "?a = ?c" using z4
then have "?b = ?c" using t1 t2 by auto
then show "(∃y'>- C / B. ∀x∈{- C / B<..y'}. aEvalUni At x) = evalUni (substInfinitesimalLinearUni B C At) x"
by auto
qed
then show ?thesis
using LeqUni fields by blast
qed
next
case (NeqUni p)
then show ?thesis proof(cases p)
case (fields a b c)
then show ?thesis unfolding NeqUni fields using nonzcoeffs  by (auto)
qed
qed

fun quadraticSubUni :: "real ⇒ real ⇒ real ⇒ real ⇒ atomUni ⇒ atomUni fmUni" where
"quadraticSubUni a b c d A = (if aEvalUni A ((a+b*sqrt(c))/d) then TrueFUni else FalseFUni)"

fun substInfinitesimalQuadraticUni :: "real ⇒ real ⇒ real ⇒ real ⇒ atomUni ⇒ atomUni fmUni" where
"substInfinitesimalQuadraticUni a b c d (EqUni p) = allZero' p"|
"substInfinitesimalQuadraticUni a b c d (LessUni p) = map_atomUni (quadraticSubUni a b c d) (convertDerivativeUni p)"|
"substInfinitesimalQuadraticUni a b c d (LeqUni p) = OrUni(map_atomUni (quadraticSubUni a b c d) (convertDerivativeUni p)) (allZero' p)"|
"substInfinitesimalQuadraticUni a b c d (NeqUni p) = negUni (allZero' p)"

lemma weird :
fixes D::"real"
assumes dneq: "D ≠ (0::real)"
shows
"((a'::real) * (((A::real) + (B::real) * sqrt (C::real)) / (D::real))⇧2 + (b'::real) * (A + B * sqrt C) / D + c' < 0 ∨
a' * ((A + B * sqrt C) / D)⇧2 + b' * (A + B * sqrt C) / D + (c'::real) = 0 ∧
(b' + a' * (A + B * sqrt C) * 2 / D < 0 ∨
b' + a' * (A + B * sqrt C) * 2 / D = 0 ∧ 2 * a' < 0)) =
(a' * ((A + B * sqrt C) / D)⇧2 + b' * (A + B * sqrt C) / D + c' < 0 ∨
a' * ((A + B * sqrt C) / D)⇧2 + b' * (A + B * sqrt C) / D + c' = 0 ∧
(2 * a' * (A + B * sqrt C) / D + b' < 0 ∨
2 * a' * (A + B * sqrt C) / D + b' = 0 ∧ a' < 0))"
proof (cases "(a' * ((A + B * sqrt C) / D)⇧2 + b' * (A + B * sqrt C) / D + c' < 0)")
case True
then show ?thesis
by auto
next
case False
have "a' * (A + B * sqrt C) * 2 = 2 * a' * (A + B * sqrt C)" by auto
then have "a' * (A + B * sqrt C) * 2 / D =2 * a' * (A + B * sqrt C) / D "
using dneq by simp
then have "b' + a' * (A + B * sqrt C) * 2 / D = 2 * a' * (A + B * sqrt C) / D + b'"
then have "(b' + a' * (A + B * sqrt C) * 2 / D < 0 ∨ b' + a' * (A + B * sqrt C) * 2 / D = 0 ∧ a' < 0)
= (2 * a' * (A + B * sqrt C) / D + b' < 0 ∨ 2 * a' * (A + B * sqrt C) / D + b' = 0 ∧ a' < 0)"
by (simp add: ‹b' + a' * (A + B * sqrt C) * 2 / D = 2 * a' * (A + B * sqrt C) / D + b'›)
then have "(a' * ((A + B * sqrt C) / D)⇧2 + b' * (A + B * sqrt C) / D + c' = 0 ∧
(b' + a' * (A + B * sqrt C) * 2 / D < 0 ∨ b' + a' * (A + B * sqrt C) * 2 / D = 0 ∧ a' < 0)) =
(a' * ((A + B * sqrt C) / D)⇧2 + b' * (A + B * sqrt C) / D + c' = 0 ∧
(2 * a' * (A + B * sqrt C) / D + b' < 0 ∨ 2 * a' * (A + B * sqrt C) / D + b' = 0 ∧ a' < 0))"
by blast
then show ?thesis using False by simp
qed

assumes "convert_poly var p (xs'@x#xs) = Some p'"
assumes "insertion (nth_default 0 (xs'@x#xs)) a = A"
assumes "insertion (nth_default 0 (xs'@x#xs)) b = B"
assumes "insertion (nth_default 0 (xs'@x#xs)) c = C"
assumes "insertion (nth_default 0 (xs'@x#xs)) d = D"
assumes "D ≠ 0"
assumes "0 ≤ C"
assumes "var∉(vars a)"
assumes "var∉(vars b)"
assumes "var∉(vars c)"
assumes "var∉(vars d)"
assumes "length xs' = var"
shows "eval (quadratic_sub_fm var a b c d (convertDerivative var p)) (xs'@x#xs) = evalUni (map_atomUni (quadraticSubUni A B C D) (convertDerivativeUni p')) x"
proof(cases p')
case (fields a' b' c')
have h : "convert_poly var p (xs'@x#xs) = Some (a', b', c')"
using assms fields by auto
have h2 : "∃F'. convert_fm var (convertDerivative var p) (xs'@x#xs) = Some F'"
unfolding convertDerivative.simps[of _ p] convertDerivative.simps[of _ "derivative var p"] convertDerivative.simps[of _ "derivative var (derivative var p)"]
apply (auto simp del: convertDerivative.simps)
using degree_convert_eq h apply blast
using assms(1) degree_convert_eq apply blast
using degree_derivative apply fastforce
apply (metis degree_convert_eq h   numeral_3_eq_3 )
apply (metis (no_types, lifting) One_nat_def add.right_neutral add_Suc_right degree_derivative less_Suc_eq_0_disj less_Suc_eq_le neq0_conv numeral_3_eq_3)
apply (metis One_nat_def Suc_eq_plus1 degree_derivative less_2_cases less_Suc_eq nat_neq_iff numeral_3_eq_3 one_add_one)
apply (meson assms(1) degree_convert_eq)
using degree_derivative apply fastforce
using assms(1) degree_convert_eq apply blast
apply (meson assms(1) degree_convert_eq)
apply (metis degree_derivative less_Suc_eq less_add_one not_less_eq numeral_3_eq_3)
apply (meson assms(1) degree_convert_eq)
apply (metis (no_types, opaque_lifting) Suc_1 Suc_eq_plus1 degree_derivative less_2_cases less_Suc_eq numeral_3_eq_3)
using assms(1) degree_convert_eq by blast
have c'_insertion : "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 0) = c'"
using assms fields unfolding convert_poly.simps apply(cases "MPoly_Type.degree p var < 3") by auto
then have c'_insertion'' : "⋀x. insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var 0) = c'"
using assms(12) not_in_isovarspar[of p var 0 "isolate_variable_sparse p var 0", OF HOL.refl]
by (metis list_update_length not_contains_insertion)
have b'_insertion : "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var (Suc 0)) = b'"
using assms fields unfolding convert_poly.simps apply(cases "MPoly_Type.degree p var < 3") by auto
then have b'_insertion'' : "⋀x. insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var (Suc 0)) = b'"
using assms(12) not_in_isovarspar[of p var "Suc 0" "isolate_variable_sparse p var (Suc 0)", OF HOL.refl]
by (metis list_update_length not_contains_insertion)
then have b'_insertion2 : "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 1) = b'"
by auto
have a'_insertion : "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse p var 2) = a'"
using assms fields unfolding convert_poly.simps apply(cases "MPoly_Type.degree p var < 3") by auto
then have a'_insertion'' : "⋀x. insertion (nth_default 0 (xs' @ x # xs)) (isolate_variable_sparse p var 2) = a'"
using assms(12) not_in_isovarspar[of p var 2 "isolate_variable_sparse p var 2", OF HOL.refl]
by (metis list_update_length not_contains_insertion)
have liftb : "liftPoly 0 0 b = b" using lift00 by auto
have liftc : "liftPoly 0 0 c = c" using lift00 by auto
have b'_insertion' : "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse (isolate_variable_sparse p var (Suc 0)) var 0) = b'"
using assms fields unfolding convert_poly.simps apply(cases "MPoly_Type.degree p var < 3") apply auto
using degree0isovarspar degree_isovarspar by auto
have insertion_into_1 : "insertion (nth_default 0 (xs'@x#xs)) (isolate_variable_sparse (Const 1) var 0) = 1"
have twominusone : "((2-1)::nat) = 1" by auto
have length0 : "var < length (xs'@x#xs)" using assms by auto
have altinserta : "∀xa. insertion (nth_default 0 ((xs'@x#xs)[var := xa])) a = A"
using assms by (metis list_update_length not_contains_insertion)
have altinserta' : "⋀xa. insertion (nth_default 0 ((xs'@x#xs)[var := xa])) a = A"
using assms by (metis list_update_length not_contains_insertion)
have altinsertb : "∀xa. insertion (nth_default 0 ((xs'@x#xs)[var := xa])) b = B"
using assms by (metis list_update_length not_contains_insertion)
have altinsertb' : "⋀xa. insertion (nth_default 0 ((xs'@x#xs)[var := xa])) b = B"
using assms by (metis list_update_length not_contains_insertion)
have altinsertc : "∀xa. insertion (nth_default 0 ((xs'@x#xs)[var := xa])) c = C"
using assms by (metis list_update_length not_contains_insertion)
have altinsertc' : "⋀xa. insertion (nth_default 0 ((xs'@x#xs)[var := xa])) c = C"
using assms by (metis list_update_length not_contains_insertion)
have altinsertd : "∀xa. insertion (nth_default 0 ((xs'@x#xs)[var := xa])) d = D"
using assms by (metis list_update_length not_contains_insertion)
have altinsertd' : "⋀xa. insertion (nth_default 0 ((xs'@x#xs)[var := xa])) d = D"
using assms by (metis list_update_length not_contains_insertion)
have freeInQuadraticSub : "∀At. eval (quadratic_sub var a b c d At) ((xs'@x#xs)[var := sqrt C]) = eval (quadratic_sub var a b c d At) ((xs'@x#xs))"
by (metis assms(10) assms(11) assms(8) assms(9) free_in_quad list_update_id var_not_in_eval)
have quad : "⋀At. (eval (quadratic_sub var a b c d At) (xs'@x#xs) =
aEval At ((xs'@x#xs)[var := (A + B * sqrt C) / D]))"
using quadratic_sub[OF length0 assms(6-7) assms(10) altinserta altinsertb altinsertc altinsertd, symmetric]
show ?thesis
proof(cases "MPoly_Type.degree p var = 0")
case True
then have simp: "(convertDerivative var p)=Atom(Less p)"
by auto
have azero : "a'=0"
by (metis MPoly_Type.insertion_zero True a'_insertion isolate_variable_sparse_ne_zeroD nat.simps(3) not_less numeral_2_eq_2 zero_less_iff_neq_zero)
have bzero : "b'=0"
using True b'_insertion isovar_greater_degree by fastforce
define p1 where "p1 = isolate_variable_sparse p var 0"
have degree_p1: "MPoly_Type.degree p1 var = 0" unfolding p1_def
define p2 where "p2 = isolate_variable_sparse p1 var 0 * Const 0 * Var var + isolate_variable_sparse p1 var 0 * Const 1"
define A where "A = isolate_variable_sparse p2 var 0"
define B where "B = isolate_variable_sparse p2 var (Suc 0)"
show ?thesis
fields
convertDerivativeUni.simps map_atomUni.simps quadraticSubUni.simps aEvalUni.simps evalUni.simps evalUni_if
True simp azero bzero
apply (simp add:True c'_insertion p1_def[symmetric] degree_p1 p2_def[symmetric] A_def[symmetric] B_def[symmetric])
unfolding A_def B_def p2_def p1_def  degree0isovarspar[OF True] isovarspar_sum mult_one_right mult_zero_right mult_zero_left const_lookup_zero const_lookup_suc
apply simp
unfolding insertion_add insertion_sub insertion_mult insertion_pow insertion_const c'_insertion apply simp
using ‹isolate_variable_sparse p var 0 = p› b'_insertion2 bzero c'_insertion by force
next
case False
then have degreenonzero : "MPoly_Type.degree p var ≠0" by auto
show ?thesis
proof(cases "MPoly_Type.degree p var = 1")
case True
then have simp : "convertDerivative var p = Or (fm.Atom (Less p)) (And (fm.Atom (Eq p)) (fm.Atom (Less (derivative var p))))"
by (metis One_nat_def Suc_eq_plus1 add_right_imp_eq convertDerivative.simps degree_derivative degreenonzero less_numeral_extra(1))
have azero : "a'=0"
by (metis MPoly_Type.insertion_zero One_nat_def True a'_insertion isovar_greater_degree lessI numeral_2_eq_2)
have degderiv : "MPoly_Type.degree (isolate_variable_sparse p var (Suc 0) * Const 1) var = 0"
using degree_mult
have thing : "var<length (xs'@((A + B * sqrt C) / D # xs))" using assms by auto
have insertp : "insertion (nth_default 0 (xs'@((A + B * sqrt C) / D # xs))) p = b' * (A + B * sqrt C) / D + c'"
using sum_over_degree_insertion[OF thing True, of "(A + B * sqrt C) / D", symmetric] unfolding list_update_length  assms(12)[symmetric] apply simp
unfolding assms(12) unfolding c'_insertion'' b'_insertion''  by auto
have insertb : "insertion (nth_default 0 (xs'@(A + B * sqrt C) / D # xs))
(isolate_variable_sparse p var (Suc 0) * Const 1) = b'"
unfolding insertion_mult insertion_const b'_insertion'' by simp
show ?thesis
fields
convertDerivativeUni.simps map_atomUni.simps quadraticSubUni.simps aEvalUni.simps evalUni.simps evalUni_if
True simp azero
apply simp
unfolding insertp insertb insertion_mult insertion_const
using assms(12) b'_insertion'' insertp by force
next
case False
then have degree2 : "MPoly_Type.degree p var = 2" using degreenonzero
using h less_Suc_eq by fastforce
have simp : "(convertDerivative var p) = Or (fm.Atom (Less p))
(And (fm.Atom (Eq p))
(Or (fm.Atom (Less (derivative var p)))
(And (fm.Atom (Eq (derivative var p))) (fm.Atom (Less (derivative var (derivative var p)))))))"
have insertionp : "var < length (xs'@(A + B * sqrt C) / D # xs)" using assms by auto
have three : "3 = Suc(Suc(Suc(0)))" by auto
have two : "2 = Suc(Suc(0))" by auto
have insertionp : "insertion (nth_default 0 ((xs'@x # xs)[var := (A + B * sqrt C) / D])) p = a' * ((A + B * sqrt C) / D)⇧2 + b' * (A + B * sqrt C) / D + c'"
using sum_over_degree_insertion[OF insertionp degree2, of "(A + B * sqrt C) / D", symmetric] unfolding
a'_insertion[symmetric] b'_insertion[symmetric] c'_insertion[symmetric]
insertion_isovarspars_free[of _ _ "(A + B * sqrt C) / D" _ _ x]
unfolding two apply simp
using assms(12) by force
have insertion_simp : "insertion (nth_default 0 ((xs' @ x # xs)[var := (A + B * sqrt C) / D])) = insertion (nth_default 0 ((xs' @ ((A + B * sqrt C) / D) # xs)))"
using assms
by (metis list_update_length)
have degreeone : "MPoly_Type.degree
(isolate_variable_sparse p var (Suc 0) * Const 1 +
isolate_variable_sparse p var (Suc (Suc 0)) * Var var * Const 2)
var = 1"
apply(rule degree_less_sum'[where n=0])
apply (smt One_nat_def ExecutiblePolyProps.degree_one degree2 degree_const degree_isovarspar degree_mult degreenonzero isolate_variable_sparse_degree_eq_zero_iff mult.commute nonzero_const_is_nonzero numeral_2_eq_2 plus_1_eq_Suc)
by simp
have zero1 : " insertion (nth_default 0 (xs' @ (A + B * sqrt C) / D # xs))
(isolate_variable_sparse (isolate_variable_sparse p var (Suc 0)) var (Suc 0)) = 0"
have zero2 : "insertion (nth_default 0 (xs' @ (A + B * sqrt C) / D # xs))
(isolate_variable_sparse (isolate_variable_sparse p var (Suc (Suc 0))) var 0) = a'"
using a'_insertion'' degree0isovarspar degree_isovarspar numeral_2_eq_2 by force
have zero3 : "insertion (nth_default 0 (xs' @ (A + B * sqrt C) / D # xs)) (isolate_variable_sparse (Var var) var (Suc 0)) = 1"
using isolate_var_one by fastforce
have zero4 : "insertion (nth_default 0 (xs' @ (A + B * sqrt C) / D # xs))
(isolate_variable_sparse (isolate_variable_sparse p var (Suc (Suc 0))) var (Suc 0)) = 0"
have insertiona' : " insertion (nth_default 0 (xs' @ (A + B * sqrt C) / D # xs))
(isolate_variable_sparse
(isolate_variable_sparse p var (Suc 0) * Const 1 +
isolate_variable_sparse p var (Suc (Suc 0)) * Var var * Const 2)
var (Suc 0) *
Const 1) = 2 * a'"
unfolding isovarspar_sum isolate_variable_sparse_mult apply auto
unfolding const_lookup_suc const_lookup_zero Rings.mult_zero_class.mult_zero_right
unfolding insertion_add insertion_mult insertion_const b'_insertion' apply auto
unfolding zero1 zero2 zero3 zero4 by auto
have a' :  "insertion (nth_default 0 (xs' @ (A + B * sqrt C) / D # xs)) (isolate_variable_sparse p var (Suc (Suc 0))) = a'"
unfolding two[symmetric] unfolding a'_insertion'' by auto
have var: "insertion (nth_default 0 (xs' @ (A + B * sqrt C) / D # xs)) (Var var) = (A + B * sqrt C) / D" using assms
by (metis insertion_simp insertion_var length0)
show ?thesis
fields
convertDerivativeUni.simps map_atomUni.simps quadraticSubUni.simps aEvalUni.simps evalUni.simps evalUni_if
degree2 simp
unfolding insertionp
unfolding insertion_simp
unfolding b'_insertion'' a'_insertion''
unfolding
degreeone apply simp
unfolding a' var
unfolding insertiona'
using weird[OF assms(6)] by auto
qed
qed
qed

assumes "convert_atom var At (xs'@ x#xs) = Some(At')"
assumes "insertion (nth_default 0 (xs'@ x#xs)) a = A"
assumes "insertion (nth_default 0 (xs'@ x#xs)) b = B"
assumes "insertion (nth_default 0 (xs'@ x#xs)) c = C"
assumes "insertion (nth_default 0 (xs'@ x#xs)) d = D"
assumes "D ≠ 0"
assumes "0 ≤ C"
assumes "var∉(vars a)"
assumes "var∉(vars b)"
assumes "var∉(vars c)"
assumes "var∉(vars d)"
assumes "length xs' = var"
shows "eval (substInfinitesimalQuadratic var a b c d At) (xs'@ x#xs) = evalUni (substInfinitesimalQuadraticUni A B C D At') x"
using assms
proof(cases At)
case (Less p)
define p' where "p' = (case convert_poly var p (xs'@ x#xs) of Some p' ⇒ p')"
have At'_simp :  "At' = LessUni p'"
using assms Less
using p'_def by auto
show ?thesis
by (metis At'_simp Less None_eq_map_option_iff assms(1) convert_atom.simps(1) option.distinct(1) option.exhaust_sel option.the_def p'_def substInfinitesimalQuadraticUni.simps(2) substInfinitesimalQuadratic.simps(2))
next
case (Eq p)
define p' where "p' = (case convert_poly var p (xs'@ x#xs) of Some p' ⇒ p')"
have At'_simp :  "At' = EqUni p'"
using assms Eq
using p'_def by auto
show ?thesis