# Theory Transfer_ODE

```theory Transfer_ODE
imports Transfer_Analysis
Ordinary_Differential_Equations.ODE_Analysis
"List-Index.List_Index"
begin

context includes lifting_syntax begin

lemma index_transfer[transfer_rule]:
"(list_all2 A ===> A ===> (=)) index index"
if [transfer_rule]: "bi_unique A"
unfolding index_def find_index_def
by transfer_prover

lemma interval_transfer[transfer_rule]: "(rel_set A ===> (=)) interval interval"
if [transfer_rule]: "bi_unique A" "bi_total A" "(A ===> A ===> (=)) inner inner" "(rel_set A) Basis Basis"
unfolding interval_def
by transfer_prover

lemma ll_on_open_transfer[transfer_rule]:
"(rel_set A ===> (A ===> B ===> C) ===> (rel_set B) ===> (=)) ll_on_open ll_on_open"
if [transfer_rule]:
"bi_unique A" "bi_total A" "(A ===> A ===> (=)) dist dist" "(A ===> A ===> (=)) inner inner" "(rel_set A) Basis Basis"
"bi_unique B" "bi_total B" "(B ===> B ===> (=)) dist dist"
"bi_unique C" "bi_total C" "(C ===> C ===> (=)) dist dist"
unfolding ll_on_open_def ll_on_open_axioms_def
by transfer_prover

lemma auto_ll_on_open_transfer[transfer_rule]:
"((A ===> A) ===> (rel_set A) ===> (=)) auto_ll_on_open auto_ll_on_open"
if [transfer_rule]: "bi_unique A" "bi_total A" "(A ===> A ===> (=)) dist dist"
unfolding auto_ll_on_open_def ll_on_open_axioms_def
by transfer_prover

lemma has_vderiv_on_transfer[transfer_rule]:
"(((=) ===> A) ===> ((=) ===> A) ===> rel_set (=) ===> (=)) (has_vderiv_on) (has_vderiv_on)"
if [transfer_rule]:
"A 0 0" "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
"((=) ===> A ===> A) (*⇩R) (*⇩R)"
"(A ===> A ===> A) (+) (+)"
"(A ===> A ===> A) (-) (-)"
"(A ===> (=)) norm norm"
unfolding has_vderiv_on_def has_vector_derivative_def has_derivative_within
by transfer_prover

lemma solves_ode_transfer[transfer_rule]:
"(((=) ===> A) ===> ((=) ===> A ===> A)  ===> rel_set (=) ===> rel_set A ===> (=)) (solves_ode) (solves_ode)"
if [transfer_rule]:
"A 0 0" "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
"((=) ===> A ===> A) (*⇩R) (*⇩R)"
"(A ===> A ===> A) (+) (+)"
"(A ===> A ===> A) (-) (-)"
"(A ===> (=)) norm norm"
unfolding solves_ode_def
by transfer_prover

lemma c1_on_open_transfer[transfer_rule]:
"((A ===> A) ===> (A ===> rel_blinfun A A) ===> rel_set A ===> (=)) c1_on_open c1_on_open"
if [transfer_rule]:
"bi_unique A" "bi_total A"
"(A ===> A ===> A) (+) (+)"
"(A ===> A ===> A) (-) (-)"
"((=) ===> A ===> A) (*⇩R) (*⇩R)"
"(A ===> (=)) norm norm"
"A 0 0"
unfolding c1_on_open_def has_derivative_at
by transfer_prover

end

end```