# Theory Infinitesimals

```subsection "Infinitesimals"
theory Infinitesimals
imports ExecutiblePolyProps LinearCase QuadraticCase NegInfinity Debruijn
begin

assumes "var ∉ vars a"
"var ∉ vars b"
"var ∉ vars c"
"var ∉ vars d"
shows "freeIn var (substInfinitesimalQuadratic var a b c d At)"
proof(cases At)
case (Less p)
apply(rule free_in_quad_fm[of var a b c d "(convertDerivative var p)"])
using assms by auto
next
case (Eq p)
then show ?thesis apply simp
apply(rule freeIn_list_conj)
apply auto
using not_in_isovarspar by simp_all
next
case (Leq p)
then show ?thesis unfolding substInfinitesimalQuadratic.simps Leq freeIn.simps
using free_in_quad_fm[of var a b c d "(convertDerivative var p)", OF assms] apply simp
apply(rule freeIn_list_conj)
using not_in_isovarspar by simp_all
next
case (Neq p)
then show ?thesis apply (auto simp add:neg_def)
apply(rule freeIn_list_conj)
apply auto
using not_in_isovarspar by simp_all
qed

lemma freeIn_substInfinitesimalQuadratic_fm : assumes "var ∉ vars a"
"var ∉ vars b"
"var ∉ vars c"
"var ∉ vars d"
shows"freeIn var (substInfinitesimalQuadratic_fm var a b c d F)"
proof-
{fix z
have "freeIn (var+z)
(liftmap
(λx. substInfinitesimalQuadratic (var + x) (liftPoly 0 x a) (liftPoly 0 x b)
(liftPoly 0 x c) (liftPoly 0 x d))
F z)"
apply(induction F arbitrary:z) apply auto
}then show ?thesis
qed

lemma freeIn_substInfinitesimalLinear:
assumes "var ∉ vars a" "var ∉ vars b"
shows "freeIn var (substInfinitesimalLinear var a b At)"
proof(cases At)
case (Less p)
show ?thesis unfolding Less substInfinitesimalLinear.simps
using var_not_in_linear_fm[of var a b "(convertDerivative var p)", OF assms]
unfolding linear_substitution_fm.simps linear_substitution_fm_helper.simps .
next
case (Eq p)
then show ?thesis apply simp apply(rule freeIn_list_conj)
apply auto
using not_in_isovarspar by simp_all
next
case (Leq p)
show ?thesis unfolding Leq substInfinitesimalLinear.simps freeIn.simps
using var_not_in_linear_fm[of var a b "(convertDerivative var p)", OF assms]
unfolding linear_substitution_fm.simps linear_substitution_fm_helper.simps apply simp apply(rule freeIn_list_conj)
apply auto
using not_in_isovarspar by simp_all
next
case (Neq p)
then show ?thesis apply (auto simp add:neg_def) apply(rule freeIn_list_conj)
apply auto
using not_in_isovarspar by simp_all
qed

lemma freeIn_substInfinitesimalLinear_fm:
assumes "var ∉ vars a" "var ∉ vars b"
shows "freeIn var (substInfinitesimalLinear_fm var a b F)"
proof-
{fix z
have "freeIn (var+z)
(liftmap (λx. substInfinitesimalLinear (var + x) (liftPoly 0 x a) (liftPoly 0 x b)) F z)"
apply(induction F arbitrary:z) apply auto
apply(rule freeIn_substInfinitesimalLinear)