Theory HS_VC_PT
section ‹ Verification components with Predicate Transformers ›
text ‹ We use the categorical forward box operator @{text fb⇩ℱ} to compute weakest liberal
preconditions (wlps) of hybrid programs. Then we repeat the three methods for verifying
correctness specifications of the continuous dynamics of a HS. ›
theory HS_VC_PT
imports
"Transformer_Semantics.Kleisli_Quantaloid"
"../HS_ODEs"
begin
no_notation bres (infixr "→" 60)
and dagger ("_⇧†" [101] 100)
and "Relation.relcomp" (infixl ";" 75)
and eta ("η")
and kcomp (infixl "∘⇩K" 75)
type_synonym 'a pred = "'a ⇒ bool"
notation eta ("skip")
and kcomp (infixl ";" 75)
and g_orbital ("(1x´=_ & _ on _ _ @ _)")
subsection ‹Verification of regular programs›
text ‹Properties of the forward box operator. ›
lemma "fb⇩ℱ F S = (⋂ ∘ 𝒫 (- op⇩K F)) (- S)"
unfolding ffb_def map_dual_def dual_set_def klift_def by simp
lemma "fb⇩ℱ F S = {s. F s ⊆ S}"
by (auto simp: ffb_def kop_def klift_def map_dual_def dual_set_def f2r_def r2f_def)
lemma ffb_eq: "fb⇩ℱ F S = {s. ∀s'. s' ∈ F s ⟶ s' ∈ S}"
by (auto simp: ffb_def kop_def klift_def map_dual_def dual_set_def f2r_def r2f_def)
lemma ffb_iso: "P ≤ Q ⟹ fb⇩ℱ F P ≤ fb⇩ℱ F Q"
unfolding ffb_eq by auto
lemma ffb_invariants:
assumes "{s. I s} ≤ fb⇩ℱ F {s. I s}" and "{s. J s} ≤ fb⇩ℱ F {s. J s}"
shows "{s. I s ∧ J s} ≤ fb⇩ℱ F {s. I s ∧ J s}"
and "{s. I s ∨ J s} ≤ fb⇩ℱ F {s. I s ∨ J s}"
using assms unfolding ffb_eq by auto
lemma ffb_skip[simp]: "fb⇩ℱ skip S = S"
unfolding ffb_def by(simp add: kop_def klift_def map_dual_def)
definition test :: "'a pred ⇒ 'a ⇒ 'a set" ("(1¿_?)")
where "¿P? = (λs. {x. x = s ∧ P x})"
lemma ffb_test[simp]: "fb⇩ℱ ¿P? Q = {s. P s ⟶ s ∈ Q}"
unfolding ffb_eq test_def by simp
definition assign :: "'n ⇒ ('a^'n ⇒ 'a) ⇒ ('a^'n) ⇒ ('a^'n) set" ("(2_ ::= _)" [70, 65] 61)
where "(x ::= e) = (λs. {vec_upd s x (e s)})"
lemma ffb_assign[simp]: "fb⇩ℱ (x ::= e) Q = {s. (χ j. ((($) s)(x := (e s))) j) ∈ Q}"
unfolding vec_upd_def assign_def by (subst ffb_eq) simp
definition nondet_assign :: "'n ⇒ 'a^'n ⇒ ('a^'n) set" ("(2_ ::= ? )" [70] 61)
where "(x ::= ?) = (λs. {(vec_upd s x k)|k. True})"
lemma fbox_nondet_assign[simp]: "fb⇩ℱ (x ::= ?) P = {s. ∀k. (χ j. if j = x then k else s$j) ∈ P}"
unfolding ffb_eq nondet_assign_def vec_upd_eq apply(simp add: fun_eq_iff, safe)
by (erule_tac x="(χ j. if j = x then k else _ $ j)" in allE, auto)
lemma ffb_choice: "fb⇩ℱ (λs. F s ∪ G s) P = fb⇩ℱ F P ∩ fb⇩ℱ G P"
unfolding ffb_eq by auto
lemma le_ffb_choice_iff: "P ⊆ fb⇩ℱ (λs. F s ∪ G s) Q ⟷ P ⊆ fb⇩ℱ F Q ∧ P ⊆ fb⇩ℱ G Q"
unfolding ffb_eq by auto
lemma ffb_kcomp[simp]: "fb⇩ℱ (G ; F) P = fb⇩ℱ G (fb⇩ℱ F P)"
unfolding ffb_eq by (auto simp: kcomp_def)
lemma hoare_kcomp:
assumes "P ≤ fb⇩ℱ F R" "R ≤ fb⇩ℱ G Q"
shows "P ≤ fb⇩ℱ (F ; G) Q"
apply(subst ffb_kcomp)
by (rule order.trans[OF assms(1)]) (rule ffb_iso[OF assms(2)])
definition ifthenelse :: "'a pred ⇒ ('a ⇒ 'b set) ⇒ ('a ⇒ 'b set) ⇒ ('a ⇒ 'b set)"
("IF _ THEN _ ELSE _" [64,64,64] 63) where
"IF P THEN X ELSE Y = (λ x. if P x then X x else Y x)"
lemma ffb_if_then_else[simp]:
"fb⇩ℱ (IF T THEN X ELSE Y) Q = {s. T s ⟶ s ∈ fb⇩ℱ X Q} ∩ {s. ¬ T s ⟶ s ∈ fb⇩ℱ Y Q}"
unfolding ffb_eq ifthenelse_def by auto
lemma hoare_if_then_else:
assumes "P ∩ {s. T s} ≤ fb⇩ℱ X Q"
and "P ∩ {s. ¬ T s} ≤ fb⇩ℱ Y Q"
shows "P ≤ fb⇩ℱ (IF T THEN X ELSE Y) Q"
using assms
apply(subst ffb_eq)
apply(subst (asm) ffb_eq)+
unfolding ifthenelse_def by auto
lemma kpower_inv: "I ≤ {s. ∀y. y ∈ F s ⟶ y ∈ I} ⟹ I ≤ {s. ∀y. y ∈ (kpower F n s) ⟶ y ∈ I}"
apply(induct n, simp)
apply simp
by(auto simp: kcomp_prop)
lemma kstar_inv: "I ≤ fb⇩ℱ F I ⟹ I ⊆ fb⇩ℱ (kstar F) I"
unfolding kstar_def ffb_eq apply clarsimp
using kpower_inv by blast
lemma ffb_kstarI:
assumes "P ≤ I" and "I ≤ Q" and "I ≤ fb⇩ℱ F I"
shows "P ≤ fb⇩ℱ (kstar F) Q"
proof-
have "I ⊆ fb⇩ℱ (kstar F) I"
using assms(3) kstar_inv by blast
hence "P ≤ fb⇩ℱ (kstar F) I"
using assms(1) by auto
also have "fb⇩ℱ (kstar F) I ≤ fb⇩ℱ (kstar F) Q"
by (rule ffb_iso[OF assms(2)])
finally show ?thesis .
qed
definition loopi :: "('a ⇒ 'a set) ⇒ 'a pred ⇒ ('a ⇒ 'a set)" ("LOOP _ INV _ " [64,64] 63)
where "LOOP F INV I ≡ (kstar F)"
lemma change_loopI: "LOOP X INV G = LOOP X INV I"
unfolding loopi_def by simp
lemma ffb_loopI: "P ≤ {s. I s} ⟹ {s. I s} ≤ Q ⟹ {s. I s} ≤ fb⇩ℱ F {s. I s} ⟹ P ≤ fb⇩ℱ (LOOP F INV I) Q"
unfolding loopi_def using ffb_kstarI[of "P"] by simp
lemma ffb_loopI_break:
"P ≤ fb⇩ℱ Y {s. I s} ⟹ {s. I s} ≤ fb⇩ℱ X {s. I s} ⟹ {s. I s} ≤ Q ⟹ P ≤ fb⇩ℱ (Y ; (LOOP X INV I)) Q"
by (rule hoare_kcomp, force) (rule ffb_loopI, auto)
subsection ‹Verification of hybrid programs›
text ‹Verification by providing evolution›
definition g_evol :: "(('a::ord) ⇒ 'b ⇒ 'b) ⇒ 'b pred ⇒ ('b ⇒ 'a set) ⇒ ('b ⇒ 'b set)" ("EVOL")
where "EVOL φ G U = (λs. g_orbit (λt. φ t s) G (U s))"
lemma fbox_g_evol[simp]:
fixes φ :: "('a::preorder) ⇒ 'b ⇒ 'b"
shows "fb⇩ℱ (EVOL φ G U) Q = {s. (∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ (φ t s) ∈ Q)}"
unfolding g_evol_def g_orbit_eq ffb_eq by auto
text ‹Verification by providing solutions›
lemma ffb_g_orbital: "fb⇩ℱ (x´= f & G on U S @ t⇩0) Q =
{s. ∀X∈Sols f U S t⇩0 s. ∀t∈U s. (∀τ∈down (U s) t. G (X τ)) ⟶ (X t) ∈ Q}"
unfolding ffb_eq g_orbital_eq by (auto simp: fun_eq_iff)
context local_flow
begin
lemma ffb_g_ode_subset:
assumes "⋀s. s ∈ S ⟹ 0 ∈ U s ∧ is_interval (U s) ∧ U s ⊆ T"
shows "fb⇩ℱ (x´= (λt. f) & G on U S @ 0) Q =
{s. s ∈ S ⟶ (∀t∈(U s). (∀τ∈down (U s) t. G (φ τ s)) ⟶ (φ t s) ∈ Q)}"
apply(unfold ffb_g_orbital set_eq_iff)
apply(clarify, rule iffI; clarify)
apply(force simp: in_ivp_sols assms)
apply(frule ivp_solsD(2), frule ivp_solsD(3), frule ivp_solsD(4))
apply(subgoal_tac "∀τ∈down (U x) t. X τ = φ τ x")
apply(clarsimp, fastforce, rule ballI)
apply(rule ivp_unique_solution[OF _ _ _ _ _ in_ivp_sols])
using assms by auto
lemma ffb_g_ode: "fb⇩ℱ (x´= (λt. f) & G on (λs. T) S @ 0) Q =
{s. s ∈ S ⟶ (∀t∈T. (∀τ∈down T t. G (φ τ s)) ⟶ (φ t s) ∈ Q)}" (is "_ = ?wlp")
by (subst ffb_g_ode_subset, simp_all add: init_time interval_time)
lemma ffb_g_ode_ivl: "t ≥ 0 ⟹ t ∈ T ⟹ fb⇩ℱ (x´=(λt. f) & G on (λs. {0..t}) S @ 0) Q =
{s. s ∈ S ⟶ (∀t∈{0..t}. (∀τ∈{0..t}. G (φ τ s)) ⟶ (φ t s) ∈ Q)}"
apply(subst ffb_g_ode_subset, simp_all add: subintervalI init_time real_Icc_closed_segment)
by (auto simp: closed_segment_eq_real_ivl)
lemma ffb_orbit: "fb⇩ℱ γ⇧φ Q = {s. s ∈ S ⟶ (∀ t ∈ T. φ t s ∈ Q)}"
unfolding orbit_def ffb_g_ode by simp
end
text ‹ Verification with differential invariants ›
definition g_ode_inv :: "(real ⇒ ('a::banach)⇒'a) ⇒ 'a pred ⇒ ('a ⇒ real set) ⇒ 'a set ⇒
real ⇒ 'a pred ⇒ ('a ⇒ 'a set)" ("(1x´=_ & _ on _ _ @ _ DINV _ )")
where "(x´= f & G on U S @ t⇩0 DINV I) = (x´= f & G on U S @ t⇩0)"
lemma ffb_g_orbital_guard:
assumes "H = (λs. G s ∧ Q s)"
shows "fb⇩ℱ (x´= f & G on U S @ t⇩0) {s. Q s} = fb⇩ℱ (x´= f & G on U S @ t⇩0) {s. H s}"
unfolding ffb_g_orbital using assms by auto
lemma ffb_g_orbital_inv:
assumes "P ≤ I" and "I ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0) I" and "I ≤ Q"
shows "P ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0) Q"
using assms(1)
apply(rule order.trans)
using assms(2)
apply(rule order.trans)
by (rule ffb_iso[OF assms(3)])
lemma ffb_diff_inv[simp]:
"({s. I s} ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0) {s. I s}) = diff_invariant I f U S t⇩0 G"
by (auto simp: diff_invariant_def ivp_sols_def ffb_eq g_orbital_eq)
lemma bdf_diff_inv:
"diff_invariant I f U S t⇩0 G = (bd⇩ℱ (x´= f & G on U S @ t⇩0) {s. I s} ≤ {s. I s})"
unfolding ffb_fbd_galois_var by (auto simp: diff_invariant_def ivp_sols_def ffb_eq g_orbital_eq)
lemma diff_inv_guard_ignore:
assumes "{s. I s} ≤ fb⇩ℱ (x´= f & (λs. True) on U S @ t⇩0) {s. I s}"
shows "{s. I s} ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0) {s. I s}"
using assms unfolding ffb_diff_inv diff_invariant_eq image_le_pred by auto
context local_flow
begin
lemma ffb_diff_inv_eq:
assumes "⋀s. s ∈ S ⟹ 0 ∈ U s ∧ is_interval (U s) ∧ U s ⊆ T"
shows "diff_invariant I (λt. f) U S 0 (λs. True) =
({s. s ∈ S ⟶ I s} = fb⇩ℱ (x´= (λt. f) & (λs. True) on U S @ 0) {s. s ∈ S ⟶ I s})"
unfolding ffb_diff_inv[symmetric]
apply(subst ffb_g_ode_subset[OF assms], simp)+
apply(clarsimp simp: set_eq_iff, safe, force)
apply(erule_tac x=0 in ballE)
using init_time in_domain ivp(2) assms apply(force, force)
apply(erule_tac x=x in allE, clarsimp, erule_tac x=t in ballE)
using in_domain ivp(2) assms by force+
lemma diff_inv_eq_inv_set:
"diff_invariant I (λt. f) (λs. T) S 0 (λs. True) = (∀s. I s ⟶ γ⇧φ s ⊆ {s. I s})"
unfolding diff_inv_eq_inv_set orbit_def by simp
end
lemma ffb_g_odei: "P ≤ {s. I s} ⟹ {s. I s} ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0) {s. I s} ⟹
{s. I s ∧ G s} ≤ Q ⟹ P ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0 DINV I) Q"
unfolding g_ode_inv_def
apply(rule_tac b="fb⇩ℱ (x´= f & G on U S @ t⇩0) {s. I s}" in order.trans)
apply(rule_tac I="{s. I s}" in ffb_g_orbital_inv, simp_all)
apply(subst ffb_g_orbital_guard, simp)
by (rule ffb_iso, force)
subsection ‹ Derivation of the rules of dL ›
text‹ We derive domain specific rules of differential dynamic logic (dL). First we present a
generalised version, then we show the rules as instances of the general ones.›
abbreviation g_dl_orbit ::"(('a::banach)⇒'a) ⇒ 'a pred ⇒ 'a ⇒ 'a set" ("(1x´=_ & _)")
where "(x´=f & G) ≡ (x´=(λt. f) & G on (λs. {t. t ≥ 0}) UNIV @ 0)"
abbreviation g_dl_ode_inv ::"(('a::banach)⇒'a) ⇒ 'a pred ⇒ 'a pred ⇒ 'a ⇒ 'a set" ("(1x´=_ & _ DINV _)")
where "(x´=f & G DINV I) ≡ (x´=(λt. f) & G on (λs. {t. t ≥ 0}) UNIV @ 0 DINV I)"
lemma diff_solve_axiom1:
assumes "local_flow f UNIV UNIV φ"
shows "fb⇩ℱ (x´= f & G) Q =
{s. ∀t≥0. (∀τ∈{0..t}. G (φ τ s)) ⟶ (φ t s) ∈ Q}"
by (subst local_flow.ffb_g_ode_subset[OF assms], auto)
lemma diff_solve_axiom2:
fixes c::"'a::{heine_borel, banach}"
shows "fb⇩ℱ (x´=(λs. c) & G) Q =
{s. ∀t≥0. (∀τ∈{0..t}. G (s + τ *⇩R c)) ⟶ (s + t *⇩R c) ∈ Q}"
apply(subst local_flow.ffb_g_ode_subset[where φ="(λt s. s + t *⇩R c)" and T=UNIV])
by (rule line_is_local_flow, auto)
lemma diff_solve_rule:
assumes "local_flow f UNIV UNIV φ"
and "∀s. s ∈ P ⟶ (∀t≥0. (∀τ∈{0..t}. G (φ τ s)) ⟶ (φ t s) ∈ Q)"
shows "P ≤ fb⇩ℱ (x´= f & G) Q"
using assms by(subst local_flow.ffb_g_ode_subset[OF assms(1)]) auto
lemma diff_weak_axiom1: "s ∈ (fb⇩ℱ (x´= f & G on U S @ t⇩0) {s. G s})"
unfolding ffb_eq g_orbital_eq by auto
lemma diff_weak_axiom2: "fb⇩ℱ (x´= f & G on T S @ t⇩0) Q = fb⇩ℱ (x´= f & G on T S @ t⇩0) {s. G s ⟶ s ∈ Q}"
unfolding ffb_g_orbital image_def by force
lemma diff_weak_rule: "{s. G s} ≤ Q ⟹ P ≤ fb⇩ℱ (x´= f & G on T S @ t⇩0) Q"
by(auto intro: g_orbitalD simp: le_fun_def g_orbital_eq ffb_eq)
lemma ffb_g_orbital_eq_univD:
assumes "fb⇩ℱ (x´= f & G on U S @ t⇩0) {s. C s} = UNIV"
and "∀τ∈(down (U s) t). x τ ∈ (x´= f & G on U S @ t⇩0) s"
shows "∀τ∈(down (U s) t). C (x τ)"
proof
fix τ assume "τ ∈ (down (U s) t)"
hence "x τ ∈ (x´= f & G on U S @ t⇩0) s"
using assms(2) by blast
also have "∀y. y ∈ (x´= f & G on U S @ t⇩0) s ⟶ C y"
using assms(1) unfolding ffb_eq by fastforce
ultimately show "C (x τ)" by blast
qed
lemma diff_cut_axiom:
assumes "fb⇩ℱ (x´= f & G on U S @ t⇩0) {s. C s} = UNIV"
shows "fb⇩ℱ (x´= f & G on U S @ t⇩0) Q = fb⇩ℱ (x´= f & (λs. G s ∧ C s) on U S @ t⇩0) Q"
proof(rule_tac f="λ x. fb⇩ℱ x Q" in HOL.arg_cong, rule ext, rule subset_antisym)
fix s
{fix s' assume "s' ∈ (x´= f & G on U S @ t⇩0) s"
then obtain τ::real and X where x_ivp: "X ∈ Sols f U S t⇩0 s"
and "X τ = s'" and "τ ∈ (U s)" and guard_x:"𝒫 X (down (U s) τ) ⊆ {s. G s}"
using g_orbitalD[of s' "f" G _ S t⇩0 s] by blast
have "∀t∈(down (U s) τ). 𝒫 X (down (U s) t) ⊆ {s. G s}"
using guard_x by (force simp: image_def)
also have "∀t∈(down (U s) τ). t ∈ (U s)"
using ‹τ ∈ (U s)› closed_segment_subset_interval by auto
ultimately have "∀t∈(down (U s) τ). X t ∈ (x´= f & G on U S @ t⇩0) s"
using g_orbitalI[OF x_ivp] by (metis (mono_tags, lifting))
hence "∀t∈(down (U s) τ). C (X t)"
using assms unfolding ffb_eq by fastforce
hence "s' ∈ (x´= f & (λs. G s ∧ C s) on U S @ t⇩0) s"
using g_orbitalI[OF x_ivp ‹τ ∈ (U s)›] guard_x ‹X τ = s'›
unfolding image_le_pred by fastforce}
thus "(x´= f & G on U S @ t⇩0) s ⊆ (x´= f & (λs. G s ∧ C s) on U S @ t⇩0) s"
by blast
next show "⋀s. (x´= f & (λs. G s ∧ C s) on U S @ t⇩0) s ⊆ (x´= f & G on U S @ t⇩0) s"
by (auto simp: g_orbital_eq)
qed
lemma diff_cut_rule:
assumes ffb_C: "P ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0) {s. C s}"
and ffb_Q: "P ≤ fb⇩ℱ (x´= f & (λs. G s ∧ C s) on U S @ t⇩0) Q"
shows "P ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0) Q"
proof(subst ffb_eq, subst g_orbital_eq, clarsimp)
fix t::real and X::"real ⇒ 'a" and s assume "s ∈ P" and "t ∈ (U s)"
and x_ivp:"X ∈ Sols f U S t⇩0 s"
and guard_x:"∀τ. τ ∈ (U s) ∧ τ ≤ t ⟶ G (X τ)"
have "∀τ∈(down (U s) t). X τ ∈ (x´= f & G on U S @ t⇩0) s"
using g_orbitalI[OF x_ivp] guard_x unfolding image_le_pred by auto
hence "∀τ∈(down (U s) t). C (X τ)"
using ffb_C ‹s ∈ P› by (subst (asm) ffb_eq, auto)
hence "X t ∈ (x´= f & (λs. G s ∧ C s) on U S @ t⇩0) s"
using guard_x ‹t ∈ (U s)› by (auto intro!: g_orbitalI x_ivp)
thus "(X t) ∈ Q"
using ‹s ∈ P› ffb_Q by (subst (asm) ffb_eq) auto
qed
lemma diff_inv_axiom1:
assumes "G s ⟶ I s" and "diff_invariant I (λt. f) (λs. {t. t ≥ 0}) UNIV 0 G"
shows "s ∈ (fb⇩ℱ (x´= f & G) {s. I s})"
using assms unfolding ffb_g_orbital diff_invariant_eq apply clarsimp
by (erule_tac x=s in allE, frule ivp_solsD(2), clarsimp)
lemma diff_inv_axiom2:
assumes "picard_lindeloef (λt. f) UNIV UNIV 0"
and "⋀s. {t::real. t ≥ 0} ⊆ picard_lindeloef.ex_ivl (λt. f) UNIV UNIV 0 s"
and "diff_invariant I (λt. f) (λs. {t::real. t ≥ 0}) UNIV 0 G"
shows "fb⇩ℱ (x´= f & G) {s. I s} = fb⇩ℱ (λs. {x. s = x ∧ G s}) {s. I s}"
proof(unfold ffb_g_orbital, subst ffb_eq, clarsimp simp: set_eq_iff)
fix s
let "?ex_ivl s" = "picard_lindeloef.ex_ivl (λt. f) UNIV UNIV 0 s"
let "?lhs s" =
"∀X∈Sols (λt. f) (λs. {t. t ≥ 0}) UNIV 0 s. ∀t≥0. (∀τ. 0 ≤ τ ∧ τ ≤ t ⟶ G (X τ)) ⟶ I (X t)"
obtain X where xivp1: "X ∈ Sols (λt. f) (λs. ?ex_ivl s) UNIV 0 s"
using picard_lindeloef.flow_in_ivp_sols_ex_ivl[OF assms(1)] by auto
have xivp2: "X ∈ Sols (λt. f) (λs. Collect ((≤) 0)) UNIV 0 s"
by (rule in_ivp_sols_subset[OF _ _ xivp1], simp_all add: assms(2))
hence shyp: "X 0 = s"
using ivp_solsD by auto
have dinv: "∀s. I s ⟶ ?lhs s"
using assms(3) unfolding diff_invariant_eq by auto
{assume "?lhs s" and "G s"
hence "I s"
by (erule_tac x=X in ballE, erule_tac x=0 in allE, auto simp: shyp xivp2)}
hence "?lhs s ⟶ (G s ⟶ I s)"
by blast
moreover
{assume "G s ⟶ I s"
hence "?lhs s"
apply(clarify, subgoal_tac "∀τ. 0 ≤ τ ∧ τ ≤ t ⟶ G (X τ)")
apply(erule_tac x=0 in allE, frule ivp_solsD(2), simp)
using dinv by blast+}
ultimately show "?lhs s = (G s ⟶ I s)"
by blast
qed
lemma diff_inv_rule:
assumes "P ≤ {s. I s}" and "diff_invariant I f U S t⇩0 G" and "{s. I s} ≤ Q"
shows "P ≤ fb⇩ℱ (x´= f & G on U S @ t⇩0) Q"
apply(rule ffb_g_orbital_inv[OF assms(1) _ assms(3)])
unfolding ffb_diff_inv using assms(2) .
end