202
J. Kolˇ c´ ak et al.
Using the syntactic Lie derivative (Definition 12), we state a sound inference
rule that does not need K to be represented explicitly. We note that there is
strong support for Lie derivatives in the tool KeYmaera X, as a key syntactic
operation behind the differential invariant (DI) rule (Definition 13).
Definition 22. Let δ :=
˙
x = e & Q
and δ :=
˙
x = e & Q
be two dynamics
and let (g, g) ∈ T ( V ) × T ( V ) (which is supposed to be a synchronizer). We
define the synchronized dynamics of (δ, δ) with respect to (g, g) as follows:
δ ⊗ (g,g) δ :=
˙
x = e, ˙
x =
L δ g
L δ g
· e
&
Q ∧ Q ∧ L δ g > 0 ∧ L δ g > 0
Lemma 23. Let (g, g) be a synchronizer of (δ, δ) from (ω 0 , ω 0 ). The following
are equivalent, where the semantical transition relations are from Definition 5.
1. (ω 0 , ω 0 ) −
δ; δ
→ (ω, ω) and (ω, ω) ∈
g = g
2. (ω 0 , ω 0 ) −
δ ⊗ (g,g) δ
→ (ω, ω)
Proof. We first prove (1 ⇒ 2). In the proof of Lemma 20, we can observe that
˙
g ψ (s) =
L δ g
ψ(s) , and analogously, ˙
g ψ (s) =
L δ g
ψ(s) . Hence we obtain
˙
K(s) =
L δ g
ψ(s)
L δ g
ψ(K(s))
=
L δ g
L δ g
ρ(s)
(6)
where ρ : [0, t) → R
VVV is defined by ρ(s) :=
ψ(s), ψ(K(s))
.
We note that K : [0, t] → [0, K(t)] is a time-stretch function, and that ψ
is a solution of ˙
x = e, that is, ˙
ψ(u) =
e
ψ(u) whenever 0 ≤ u < t = K(t).
Combined with Lemma 17, we obtain
˙
ψ ◦ K
(s) = ˙
K(s) ·
e
ψ(K(s)) = ˙
K(s) ·
e
ρ(s)
whenever 0 ≤ s < t.
Hence, with the fact that ψ is a solution of ˙
x = e, we obtain
˙
ρ(s) =
˙
ψ(s),
˙
ψ ◦ K
(s)
=
e
ρ(s) , ˙
K(s) ·
e
ρ(s)
=
e,
L δ g
L δ g
· e
ρ(s)
whenever 0 ≤ s < t. Here the last equality is from (6). This concludes that ρ is
a solution of the dynamics δ ⊗ (g,g) δ. It remains to prove that for all τ ∈ [0, t],
Q ∧ Q ∧ L δ g > 0 ∧ L δ g > 0
ρ(τ ) is true. This is an easy consequence of item 1,
and the fact that (g, g) is a synchronizer of (δ, δ) from (ω 0 , ω 0 ).
For the direction (2 ⇒ 1), let (ξ, ξ) : [0, T ) → R
V
× R
V be the unique solution
of δ ⊗ (g,g) δ from (ω 0 , ω 0 ). Then there is t ∈ [0, T ) such that (ξ(t), ξ(t)) = (ω, ω).
Let us prove that (ω, ω) ∈
g = g
. The function h : s ∈ [0, T ) →
g
ξ(s) −
g
ξ(s) is equal to 0 at s = 0 and its derivative is given by:
˙
h(s) =
L δ g
ξ(s) −
L δ g
ξ(s) .
L δ g
ξ(s)
L δ g
ξ(s)
= 0
J. Kolˇ c´ ak et al.
Using the syntactic Lie derivative (Definition 12), we state a sound inference
rule that does not need K to be represented explicitly. We note that there is
strong support for Lie derivatives in the tool KeYmaera X, as a key syntactic
operation behind the differential invariant (DI) rule (Definition 13).
Definition 22. Let δ :=
˙
x = e & Q
and δ :=
˙
x = e & Q
be two dynamics
and let (g, g) ∈ T ( V ) × T ( V ) (which is supposed to be a synchronizer). We
define the synchronized dynamics of (δ, δ) with respect to (g, g) as follows:
δ ⊗ (g,g) δ :=
˙
x = e, ˙
x =
L δ g
L δ g
· e
&
Q ∧ Q ∧ L δ g > 0 ∧ L δ g > 0
Lemma 23. Let (g, g) be a synchronizer of (δ, δ) from (ω 0 , ω 0 ). The following
are equivalent, where the semantical transition relations are from Definition 5.
1. (ω 0 , ω 0 ) −
δ; δ
→ (ω, ω) and (ω, ω) ∈
g = g
2. (ω 0 , ω 0 ) −
δ ⊗ (g,g) δ
→ (ω, ω)
Proof. We first prove (1 ⇒ 2). In the proof of Lemma 20, we can observe that
˙
g ψ (s) =
L δ g
ψ(s) , and analogously, ˙
g ψ (s) =
L δ g
ψ(s) . Hence we obtain
˙
K(s) =
L δ g
ψ(s)
L δ g
ψ(K(s))
=
L δ g
L δ g
ρ(s)
(6)
where ρ : [0, t) → R
VVV is defined by ρ(s) :=
ψ(s), ψ(K(s))
.
We note that K : [0, t] → [0, K(t)] is a time-stretch function, and that ψ
is a solution of ˙
x = e, that is, ˙
ψ(u) =
e
ψ(u) whenever 0 ≤ u < t = K(t).
Combined with Lemma 17, we obtain
˙
ψ ◦ K
(s) = ˙
K(s) ·
e
ψ(K(s)) = ˙
K(s) ·
e
ρ(s)
whenever 0 ≤ s < t.
Hence, with the fact that ψ is a solution of ˙
x = e, we obtain
˙
ρ(s) =
˙
ψ(s),
˙
ψ ◦ K
(s)
=
e
ρ(s) , ˙
K(s) ·
e
ρ(s)
=
e,
L δ g
L δ g
· e
ρ(s)
whenever 0 ≤ s < t. Here the last equality is from (6). This concludes that ρ is
a solution of the dynamics δ ⊗ (g,g) δ. It remains to prove that for all τ ∈ [0, t],
Q ∧ Q ∧ L δ g > 0 ∧ L δ g > 0
ρ(τ ) is true. This is an easy consequence of item 1,
and the fact that (g, g) is a synchronizer of (δ, δ) from (ω 0 , ω 0 ).
For the direction (2 ⇒ 1), let (ξ, ξ) : [0, T ) → R
V
× R
V be the unique solution
of δ ⊗ (g,g) δ from (ω 0 , ω 0 ). Then there is t ∈ [0, T ) such that (ξ(t), ξ(t)) = (ω, ω).
Let us prove that (ω, ω) ∈
g = g
. The function h : s ∈ [0, T ) →
g
ξ(s) −
g
ξ(s) is equal to 0 at s = 0 and its derivative is given by:
˙
h(s) =
L δ g
ξ(s) −
L δ g
ξ(s) .
L δ g
ξ(s)
L δ g
ξ(s)
= 0