Theory Hybrid_Systems_VCs.HS_VC_Spartan

(*  Title:       Verification components for hybrid systems 
    Author:      Jonathan Julián Huerta y Munive, 2020
    Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
*)

section ‹ Verification components for hybrid systems ›

text ‹ A light-weight version of the verification components. We define the forward box 
operator to compute weakest liberal preconditions (wlps) of hybrid programs. Then we 
introduce three methods for verifying correctness specifications of the continuous 
dynamics of a HS. ›

theory HS_VC_Spartan
  imports HS_ODEs
                        
begin

type_synonym 'a pred = "'a ⇒ bool"

no_notation Transitive_Closure.rtrancl ("(_⇧*)" [1000] 999)

notation Union ("μ")
     and g_orbital ("(1x´=_ & _ on _ _ @ _)")


subsection ‹Verification of regular programs›

text ‹ Lemmas for verification condition generation ›

definition fbox :: "('a ⇒ 'b set) ⇒ 'b pred ⇒ 'a pred" ("|_] _" [61,81] 82)
  where "|F] P = (λs. (∀s'. s' ∈ F s ⟶ P s'))"

lemma fbox_iso: "P ≤ Q ⟹ |F] P ≤ |F] Q"
  unfolding fbox_def by auto

lemma fbox_anti: "∀s. F⇩1 s ⊆ F⇩2 s ⟹ |F⇩2] P ≤ |F⇩1] P"
  unfolding fbox_def by auto

lemma fbox_invariants: 
  assumes "I ≤ |F] I" and "J ≤ |F] J"
  shows "(λs. I s ∧ J s) ≤ |F] (λs. I s ∧ J s)"
    and "(λs. I s ∨ J s) ≤ |F] (λs. I s ∨ J s)"
  using assms unfolding fbox_def by auto

― ‹ Skip ›

abbreviation "skip ≡ (λs. {s})"

lemma fbox_eta[simp]: "fbox skip P = P"
  unfolding fbox_def by simp

― ‹ Tests ›

definition test :: "'a pred ⇒ 'a ⇒ 'a set" ("(1¿_?)")
  where "¿P? = (λs. {x. x = s ∧ P x})"

lemma fbox_test[simp]: "(λs. ( |¿P?] Q) s) = (λs. P s ⟶ Q s)"
  unfolding fbox_def test_def by simp

― ‹ Assignments ›

definition vec_upd :: "'a^'n ⇒ 'n ⇒ 'a ⇒ 'a^'n"
  where "vec_upd s i a = (χ j. ((($) s)(i := a)) j)"

lemma vec_upd_eq: "vec_upd s i a = (χ j. if j = i then a else s$j)"
  by (simp add: vec_upd_def)

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 fbox_assign[simp]: "|x ::= e] Q = (λs. Q (χ j. ((($) s)(x := (e s))) j))"
  unfolding vec_upd_def assign_def by (subst fbox_def) simp

― ‹ Nondeterministic assignments ›

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]: "|x ::= ?] P = (λs. ∀k. P (χ j. if j = x then k else s$j))"
  unfolding fbox_def 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)

― ‹ Nondeterministic choice ›

lemma fbox_choice: "|(λs. F s ∪ G s)] P = (λs. ( |F] P) s ∧ ( |G] P) s)"
  unfolding fbox_def by auto

lemma le_fbox_choice_iff: "P ≤ |(λs. F s ∪ G s)] Q ⟷ P ≤ |F] Q ∧ P ≤ |G] Q"
  unfolding fbox_def by auto

― ‹ Sequential composition ›

definition kcomp :: "('a ⇒ 'b set) ⇒ ('b ⇒ 'c set) ⇒ ('a  ⇒ 'c set)" (infixl ";" 75) where
  "F ; G = μ ∘ 𝒫 G ∘ F"

lemma kcomp_eq: "(f ; g) x = ⋃ {g y |y. y ∈ f x}"
  unfolding kcomp_def image_def by auto

lemma fbox_kcomp[simp]: "|G ; F] P = |G] |F] P"
  unfolding fbox_def kcomp_def by auto

lemma hoare_kcomp:
  assumes "P ≤ |G] R" "R ≤ |F] Q"
  shows "P ≤ |G ; F] Q"
  apply(subst fbox_kcomp) 
  by (rule order.trans[OF assms(1)]) (rule fbox_iso[OF assms(2)])

― ‹ Conditional statement ›

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 ≡ (λs. if P s then X s else Y s)"

lemma fbox_if_then_else[simp]:
  "|IF T THEN X ELSE Y] Q = (λs. (T s ⟶ ( |X] Q) s) ∧ (¬ T s ⟶ ( |Y] Q) s))"
  unfolding fbox_def ifthenelse_def by auto

lemma hoare_if_then_else:
  assumes "(λs. P s ∧ T s) ≤ |X] Q"
    and "(λs. P s ∧ ¬ T s) ≤ |Y] Q"
  shows "P ≤ |IF T THEN X ELSE Y] Q"
  using assms unfolding fbox_def ifthenelse_def by auto

― ‹ Finite iteration ›

definition kpower :: "('a ⇒ 'a set) ⇒ nat ⇒ ('a ⇒ 'a set)" 
  where "kpower f n = (λs. ((;) f ^^ n) skip s)"

lemma kpower_base:
  shows "kpower f 0 s = {s}" and "kpower f (Suc 0) s = f s"
  unfolding kpower_def by(auto simp: kcomp_eq)

lemma kpower_simp: "kpower f (Suc n) s = (f ; kpower f n) s"
  unfolding kcomp_eq 
  apply(induct n)
  unfolding kpower_base 
   apply(force simp: subset_antisym)
  unfolding kpower_def kcomp_eq by simp

definition kleene_star :: "('a ⇒ 'a set) ⇒ ('a ⇒ 'a set)" ("(_⇧*)" [1000] 999)
  where "(f⇧*) s = ⋃ {kpower f n s |n. n ∈ UNIV}"

lemma kpower_inv: 
  fixes F :: "'a ⇒ 'a set"
  assumes "∀s. I s ⟶ (∀s'. s' ∈ F s ⟶ I s')" 
  shows "∀s. I s ⟶ (∀s'. s' ∈ (kpower F n s) ⟶ I s')"
  apply(clarsimp, induct n)
  unfolding kpower_base kpower_simp 
   apply(simp_all add: kcomp_eq, clarsimp) 
  apply(subgoal_tac "I y", simp)
  using assms by blast

lemma kstar_inv: "I ≤ |F] I ⟹ I ≤ |F⇧*] I"
  unfolding kleene_star_def fbox_def 
  apply clarsimp
  apply(unfold le_fun_def, subgoal_tac "∀x. I x ⟶ (∀s'. s' ∈ F x ⟶ I s')")
  using kpower_inv[of I F] by blast simp

lemma fbox_kstarI:
  assumes "P ≤ I" and "I ≤ Q" and "I ≤ |F] I" 
  shows "P ≤ |F⇧*] Q"
proof-
  have "I ≤ |F⇧*] I"
    using assms(3) kstar_inv by blast
  hence "P ≤ |F⇧*] I"
    using assms(1) by auto
  also have "|F⇧*] I ≤ |F⇧*] Q"
    by (rule fbox_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 ≡ (F⇧*)"

lemma change_loopI: "LOOP X INV G = LOOP X INV I"
  unfolding loopi_def by simp

lemma fbox_loopI: "P ≤ I ⟹ I ≤ Q ⟹ I ≤ |F] I ⟹ P ≤ |LOOP F INV I] Q"
  unfolding loopi_def using fbox_kstarI[of "P"] by simp

lemma wp_loopI_break: 
  "P ≤ |Y] I ⟹ I ≤ |X] I ⟹ I ≤ Q ⟹ P ≤ |Y ; (LOOP X INV I)] Q"
  by (rule hoare_kcomp, force) (rule fbox_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 "|EVOL φ G U] Q = (λs. (∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s)))"
  unfolding g_evol_def g_orbit_eq fbox_def by auto

text ‹ Verification by providing solutions ›

lemma fbox_g_orbital: "|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 τ)) ⟶ Q (X t))"
  unfolding fbox_def g_orbital_eq by (auto simp: fun_eq_iff)

context local_flow
begin

lemma fbox_g_ode_subset:
  assumes "⋀s. s ∈ S ⟹ 0 ∈ U s ∧ is_interval (U s) ∧ U s ⊆ T"
  shows "|x´= (λt. f) & G on U S @ 0] Q = 
  (λ s. s ∈ S ⟶ (∀t∈(U s). (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s)))"
  apply(unfold fbox_g_orbital fun_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 fbox_g_ode: "|x´=(λt. f) & G on (λs. T) S @ 0] Q = 
  (λs. s ∈ S ⟶ (∀t∈T. (∀τ∈down T t. G (φ τ s)) ⟶ Q (φ t s)))"
  by (subst fbox_g_ode_subset, simp_all add: init_time interval_time)

lemma fbox_g_ode_ivl: "t ≥ 0 ⟹ t ∈ T ⟹ |x´=(λt. f) & G on (λs. {0..t}) S @ 0] Q = 
  (λs. s ∈ S ⟶ (∀t∈{0..t}. (∀τ∈{0..t}. G (φ τ s)) ⟶ Q (φ t s)))"
  apply(subst fbox_g_ode_subset, simp_all add: subintervalI init_time real_Icc_closed_segment)
  by (auto simp: closed_segment_eq_real_ivl)

lemma fbox_orbit: "|γ⇧φ] Q = (λs. s ∈ S ⟶ (∀ t ∈ T. Q (φ t s)))"
  unfolding orbit_def fbox_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 fbox_g_orbital_guard: 
  assumes "H = (λs. G s ∧ Q s)"
  shows "|x´=f & G on U S @ t⇩0] Q = |x´=f & G on U S @ t⇩0] H "
  unfolding fbox_g_orbital using assms by auto

lemma fbox_g_orbital_inv:
  assumes "P ≤ I" and "I ≤ |x´=f & G on U S @ t⇩0] I" and "I ≤ Q"
  shows "P ≤ |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 fbox_iso[OF assms(3)])

lemma fbox_diff_inv[simp]: 
  "(I ≤ |x´=f & G on U S @ t⇩0] I) = diff_invariant I f U S t⇩0 G"
  by (auto simp: diff_invariant_def ivp_sols_def fbox_def g_orbital_eq)

lemma diff_inv_guard_ignore:
  assumes "I ≤ |x´= f & (λs. True) on U S @ t⇩0] I"
  shows "I ≤ |x´= f & G on U S @ t⇩0] I"
  using assms unfolding fbox_diff_inv diff_invariant_eq image_le_pred by auto

context local_flow
begin

lemma fbox_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) = |x´= (λt. f) & (λs. True) on U S @ 0] (λs. s ∈ S ⟶ I s))"
  unfolding fbox_diff_inv[symmetric] 
  apply(subst fbox_g_ode_subset[OF assms], simp)+
  apply(clarsimp simp: le_fun_def fun_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 fbox_g_odei: "P ≤ I ⟹ I ≤ |x´= f & G on U S @ t⇩0] I ⟹ (λs. I s ∧ G s) ≤ Q ⟹ 
  P ≤ |x´= f & G on U S @ t⇩0 DINV I] Q"
  unfolding g_ode_inv_def 
  apply(rule_tac b="|x´= f & G on U S @ t⇩0] I" in order.trans)
   apply(rule_tac I="I" in fbox_g_orbital_inv, simp_all)
  apply(subst fbox_g_orbital_guard, simp)
  by (rule fbox_iso, force)


subsection ‹ Derivation of the rules of dL ›

text ‹ We derive rules of differential dynamic logic (dL). This allows the components to reason 
in the style of that logic. ›

abbreviation g_dl_ode ::"(('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 "|x´= f & G] Q = 
  (λs. ∀t≥0. (∀τ∈{0..t}. G (φ τ s)) ⟶ Q (φ t s))"
  by (subst local_flow.fbox_g_ode_subset[OF assms], auto)

lemma diff_solve_axiom2: 
  fixes c::"'a::{heine_borel, banach}"
  shows "|x´=(λs. c) & G] Q = 
  (λs. ∀t≥0. (∀τ∈{0..t}. G (s + τ *⇩R c)) ⟶ Q (s + t *⇩R c))"
  by (subst local_flow.fbox_g_ode_subset[OF line_is_local_flow, of UNIV], auto)

lemma diff_solve_rule:
  assumes "local_flow f UNIV UNIV φ"
    and "∀s. P s ⟶ (∀t≥0. (∀τ∈{0..t}. G (φ τ s)) ⟶ Q (φ t s))"
  shows "P ≤ |x´= f & G] Q"
  using assms by(subst local_flow.fbox_g_ode_subset[OF assms(1)]) auto

lemma diff_weak_axiom1: "( |x´= f & G on U S @ t⇩0] G) s"
  unfolding fbox_def g_orbital_eq by auto

lemma diff_weak_axiom2: "|x´= f & G on T S @ t⇩0] Q = |x´= f & G on T S @ t⇩0] (λs. G s ⟶ Q s)"
  unfolding fbox_g_orbital image_def by force
  
lemma diff_weak_rule: "G ≤ Q ⟹ P ≤ |x´= f & G on T S @ t⇩0] Q"
  by(auto intro: g_orbitalD simp: le_fun_def g_orbital_eq fbox_def)

lemma fbox_g_orbital_eq_univD:
  assumes "|x´= f & G on U S @ t⇩0] C = (λs. True)" 
    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 "∀s'. s' ∈ (x´= f & G on U S @ t⇩0) s ⟶ C s'"
    using assms(1) unfolding fbox_def by meson 
  ultimately show "C (x τ)" 
    by blast
qed

lemma diff_cut_axiom:
  assumes "|x´= f & G on U S @ t⇩0] C = (λs. True)"
  shows "|x´= f & G on U S @ t⇩0] Q = |x´= f & (λs. G s ∧ C s) on U S @ t⇩0] Q"
proof(rule_tac f="λ x. |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 U 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 fbox_def by meson
    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'› 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 fbox_C: "P ≤ |x´= f & G on U S @ t⇩0] C"
    and fbox_Q: "P ≤ |x´= f & (λs. G s ∧ C s) on U S @ t⇩0] Q"
  shows "P ≤ |x´= f & G on U S @ t⇩0] Q"
proof(subst fbox_def, subst g_orbital_eq, clarsimp)
  fix t::real and X::"real ⇒ 'a" and s assume "P s" 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 fbox_C ‹P s› by (subst (asm) fbox_def, 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 "Q (X t)"
    using ‹P s› fbox_Q by (subst (asm) fbox_def) 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 "( |x´= f & G] I) s"
  using assms unfolding fbox_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 "|x´= f & G] I = |(λs. {x. s = x ∧ G s})] I"
proof(unfold fbox_g_orbital, subst fbox_def, clarsimp simp: fun_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 ≤ I" and "diff_invariant I f U S t⇩0 G" and "I ≤ Q"
  shows "P ≤ |x´= f & G on U S @ t⇩0] Q"
  apply(rule fbox_g_orbital_inv[OF assms(1) _ assms(3)])
  unfolding fbox_diff_inv using assms(2) .

end