Theory HS_VC_MKA_rel

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

subsection ‹Verification of hybrid programs›

text ‹ We show that relations form an antidomain Kleene algebra. This allows us to inherit 
the rules of the wlp calculus for regular programs. Finally, we derive three methods for 
verifying correctness specifications for the continuous dynamics of hybrid systems in this 
setting. ›

theory HS_VC_MKA_rel
  imports 
    "../HS_ODEs" 
    "HS_VC_MKA"
    "../HS_VC_KA_rel"

begin

definition rel_ad :: "'a rel ⇒ 'a rel" where
  "rel_ad R = {(x,x) | x. ¬ (∃y. (x,y) ∈ R)}"

interpretation rel_aka: antidomain_kleene_algebra rel_ad "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)" rtrancl
  by  unfold_locales (auto simp: rel_ad_def)


subsubsection ‹ Regular programs›

text ‹ Lemmas for manipulation of predicates in the relational model ›

type_synonym 'a pred = "'a ⇒ bool"

no_notation Archimedean_Field.ceiling ("⌈_⌉")
        and antidomain_semiringl.ads_d ("d")

notation Id ("skip")
     and relcomp (infixl ";" 70)
     and zero_class.zero ("0")
     and rel_aka.fbox ("wp")

definition p2r :: "'a pred ⇒ 'a rel" ("(1⌈_⌉)") where
  "⌈P⌉ = {(s,s) |s. P s}"

lemma p2r_simps[simp]: 
  "⌈P⌉ ≤ ⌈Q⌉ = (∀s. P s ⟶ Q s)"
  "(⌈P⌉ = ⌈Q⌉) = (∀s. P s = Q s)"
  "(⌈P⌉ ; ⌈Q⌉) = ⌈λ s. P s ∧ Q s⌉"
  "(⌈P⌉ ∪ ⌈Q⌉) = ⌈λ s. P s ∨ Q s⌉"
  "rel_ad ⌈P⌉ = ⌈λs. ¬ P s⌉"
  "rel_aka.ads_d ⌈P⌉ = ⌈P⌉"
  unfolding p2r_def rel_ad_def rel_aka.ads_d_def by auto

lemma in_p2r [simp]: "(a,b) ∈ ⌈P⌉ = (P a ∧ a = b)"
  by (auto simp: p2r_def)

text ‹ Lemmas for verification condition generation ›

lemma wp_rel: "wp R ⌈P⌉ = ⌈λ x. ∀ y. (x,y) ∈ R ⟶ P y⌉"
  unfolding rel_aka.fbox_def p2r_def rel_ad_def by auto

― ‹ Tests ›

lemma wp_test[simp]: "wp ⌈P⌉ ⌈Q⌉ = ⌈λs. P s ⟶ Q s⌉"
  by (subst wp_rel, simp add: p2r_def)

― ‹ Assignments ›

definition assign :: "'b ⇒ ('a^'b ⇒ 'a) ⇒ ('a^'b) rel" ("(2_ ::= _)" [70, 65] 61) 
  where "(x ::= e) = {(s, vec_upd s x (e s))| s. True}" 

lemma wp_assign [simp]: "wp (x ::= e) ⌈Q⌉ = ⌈λs. Q (χ j. ((($) s)(x := (e s))) j)⌉"
  unfolding wp_rel vec_upd_def assign_def by (auto simp: fun_upd_def)

― ‹ Nondeterministic assignments ›

definition nondet_assign :: "'b ⇒ ('a^'b) rel" ("(2_ ::= ? )" [70] 61)
  where "(x ::= ?) = {(s,vec_upd s x k)|s k. True}"

lemma wp_nondet_assign[simp]: "wp (x ::= ?) ⌈P⌉ = ⌈λs. ∀k. P (χ j. ((($) s)(x := k)) j)⌉"
  unfolding wp_rel nondet_assign_def vec_upd_eq apply(clarsimp, safe)
  by (erule_tac x="(χ j. if j = x then k else s $ j)" in allE, auto)

― ‹ Nondeterministic choice ›

lemma le_wp_choice_iff: "⌈P⌉ ≤ wp (X ∪ Y) ⌈Q⌉ ⟷ ⌈P⌉ ≤ wp X ⌈Q⌉ ∧ ⌈P⌉ ≤ wp Y ⌈Q⌉"
  using rel_aka.le_fbox_choice_iff[of "⌈P⌉"] by simp

― ‹ Conditional statement ›

abbreviation cond_sugar :: "'a pred ⇒ 'a rel ⇒ 'a rel ⇒ 'a rel" ("IF _ THEN _ ELSE _" [64,64] 63) 
  where "IF P THEN X ELSE Y ≡ rel_aka.aka_cond ⌈P⌉ X Y"

― ‹ Finite iteration ›

abbreviation loopi_sugar :: "'a rel ⇒ 'a pred ⇒ 'a rel" ("LOOP _ INV _ " [64,64] 63)
  where "LOOP R INV I ≡ rel_aka.aka_loopi R ⌈I⌉"

lemma change_loopI: "LOOP X INV G = LOOP X INV I"
  by (unfold rel_aka.aka_loopi_def, simp)

lemma wp_loopI: 
  "⌈P⌉ ≤ ⌈I⌉ ⟹ ⌈I⌉ ≤ ⌈Q⌉ ⟹ ⌈I⌉ ≤ wp R ⌈I⌉ ⟹ ⌈P⌉ ≤ wp (LOOP R INV I) ⌈Q⌉"
  using rel_aka.fbox_loopi[of "⌈P⌉"] by auto

lemma wp_loopI_break: 
  "⌈P⌉ ≤ wp Y ⌈I⌉ ⟹ ⌈I⌉ ≤ wp X ⌈I⌉ ⟹ ⌈I⌉ ≤ ⌈Q⌉  ⟹ ⌈P⌉ ≤ wp (Y ; (LOOP X INV I)) ⌈Q⌉"
  using rel_aka.fbox_loopi_break[of "⌈P⌉"] by auto


subsubsection ‹ Evolution commands ›

text ‹Verification by providing evolution›

definition g_evol :: "(('a::ord) ⇒ 'b ⇒ 'b) ⇒ 'b pred ⇒ ('b ⇒ 'a set) ⇒ 'b rel" ("EVOL")
  where "EVOL φ G U = {(s,s') |s s'. s' ∈ g_orbit (λt. φ t s) G (U s)}"

lemma wp_g_dyn[simp]:  
  fixes φ :: "('a::preorder) ⇒ 'b ⇒ 'b"
  shows "wp (EVOL φ G U) ⌈Q⌉ = ⌈λs. ∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s)⌉"
  unfolding wp_rel g_evol_def g_orbit_eq by auto

text ‹Verification by providing solutions›

definition g_ode :: "(real ⇒ ('a::banach)⇒'a) ⇒ 'a pred ⇒ ('a ⇒ real set) ⇒ 'a set ⇒ real ⇒ 
  'a rel" ("(1x´=_ & _ on _ _ @ _)") 
  where "(x´= f & G on U S @ t0) = {(s,s') |s s'. s' ∈ g_orbital f G U S t0 s}"

lemma wp_g_orbital: "wp (x´= f & G on U S @ t0) ⌈Q⌉ = 
  ⌈λs. ∀X∈Sols f U S t0 s. ∀t∈U s. (∀τ∈down (U s) t. G (X τ)) ⟶ Q (X t)⌉"
  unfolding g_orbital_eq wp_rel ivp_sols_def g_ode_def by auto

context local_flow
begin

lemma wp_g_ode_subset:
  assumes "⋀s. s ∈ S ⟹ 0 ∈ U s ∧ is_interval (U s) ∧ U s ⊆ T"
  shows "wp (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 wp_g_orbital, clarsimp, 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 s) t. X τ = φ τ s")
   apply(clarsimp, fastforce, rule ballI)
  apply(rule ivp_unique_solution[OF _ _ _ _ _ in_ivp_sols])
  using assms by auto

lemma wp_g_ode: "wp (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 wp_g_ode_subset, simp_all add: init_time interval_time)

lemma wp_g_ode_ivl: "t ≥ 0 ⟹ t ∈ T ⟹ wp (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 wp_g_ode_subset, simp_all add: subintervalI init_time real_Icc_closed_segment)
  by (auto simp: closed_segment_eq_real_ivl)

lemma wp_orbit: "wp ({(s,s') | s s'. s' ∈ γφ s}) ⌈Q⌉ = ⌈λs. s ∈ S ⟶ (∀t∈T. Q (φ t s))⌉"
  unfolding orbit_def wp_g_ode g_ode_def[symmetric] by auto

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 rel" ("(1x´=_ & _ on _ _ @ _ DINV _ )") 
  where "(x´= f & G on U S @ t0 DINV I) = (x´= f & G on U S @ t0)"

lemma wp_g_orbital_guard: 
  assumes "H = (λs. G s ∧ Q s)"
  shows "wp (x´= f & G on U S @ t0) ⌈Q⌉ = wp (x´= f & G on U S @ t0) ⌈H⌉"
  unfolding wp_g_orbital using assms by auto

lemma wp_g_orbital_inv:
  assumes "⌈P⌉ ≤ ⌈I⌉" and "⌈I⌉ ≤ wp (x´= f & G on U S @ t0) ⌈I⌉" and "⌈I⌉ ≤ ⌈Q⌉"
  shows "⌈P⌉ ≤ wp (x´= f & G on U S @ t0) ⌈Q⌉"
  using assms(1) 
  apply(rule order.trans)
  using assms(2) 
  apply(rule order.trans)
  apply(rule rel_aka.fbox_iso)
  using assms(3) by auto

lemma wp_diff_inv[simp]: "(⌈I⌉ ≤ wp (x´= f & G on U S @ t0) ⌈I⌉) = diff_invariant I f U S t0 G"
  unfolding diff_invariant_eq wp_g_orbital by(auto simp: p2r_def)

lemma diff_inv_guard_ignore:
  assumes "⌈I⌉ ≤ wp (x´= f & (λs. True) on U S @ t0) ⌈I⌉"
  shows "⌈I⌉ ≤ wp (x´= f & G on U S @ t0) ⌈I⌉"
  using assms unfolding wp_diff_inv diff_invariant_eq by auto

context local_flow
begin

lemma wp_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⌉ = wp (x´= (λt. f) & (λs. True) on U S @ 0) ⌈λs. s ∈ S ⟶ I s⌉)"
  unfolding wp_diff_inv[symmetric] 
  apply(subst wp_g_ode_subset[OF assms], simp)+
  apply(clarsimp, safe, force)
   apply(erule_tac x=0 in ballE)
  using init_time in_domain ivp(2) assms apply(force, force)
  apply(erule_tac x=s 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 (auto simp: p2r_def)

end

lemma wp_g_odei: "⌈P⌉ ≤ ⌈I⌉ ⟹ ⌈I⌉ ≤ wp (x´= f & G on U S @ t0) ⌈I⌉ ⟹ ⌈λs. I s ∧ G s⌉ ≤ ⌈Q⌉ ⟹ 
  ⌈P⌉ ≤ wp (x´= f & G on U S @ t0 DINV I) ⌈Q⌉"
  unfolding g_ode_inv_def 
  apply(rule_tac b="wp (x´= f & G on U S @ t0) ⌈I⌉" in order.trans)
   apply(rule_tac I="I" in wp_g_orbital_inv, simp_all)
  apply(subst wp_g_orbital_guard, simp)
  by (rule rel_aka.fbox_iso, simp)


subsubsection ‹ 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 rel" ("(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 rel" ("(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 "wp (x´= f & G) ⌈Q⌉ = 
  ⌈λs. ∀t≥0. (∀τ∈{0..t}. G (φ τ s)) ⟶ Q (φ t s)⌉"
  by (subst local_flow.wp_g_ode_subset[OF assms], auto)

lemma diff_solve_axiom2: 
  fixes c::"'a::{heine_borel, banach}"
  shows "wp (x´=(λs. c) & G) ⌈Q⌉ = 
  ⌈λs. ∀t≥0. (∀τ∈{0..t}. G (s + τ *R c)) ⟶ Q (s + t *R c)⌉"
  apply(subst local_flow.wp_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. P s ⟶ (∀t≥0. (∀τ∈{0..t}. G (φ τ s)) ⟶ Q (φ t s))"
  shows "⌈P⌉ ≤ wp (x´= f & G) ⌈Q⌉"
  using assms by (subst local_flow.wp_g_ode_subset[OF assms(1)], auto)

lemma diff_weak_axiom1: "Id ⊆ wp (x´= f & G on U S @ t0) ⌈G⌉"
  unfolding wp_rel g_ode_def g_orbital_eq by auto

lemma diff_weak_axiom2: 
  "wp (x´= f & G on T S @ t0) ⌈Q⌉ = wp (x´= f & G on T S @ t0) ⌈λ s. G s ⟶ Q s⌉"
  unfolding wp_g_orbital image_def by force

lemma diff_weak_rule: 
  assumes "⌈G⌉ ≤ ⌈Q⌉"
  shows "⌈P⌉ ≤ wp (x´= f & G on U S @ t0) ⌈Q⌉"
  using assms by (auto simp: wp_g_orbital)

lemma wp_g_evol_IdD:
  assumes "wp (x´= f & G on U S @ t0) ⌈C⌉ = Id"
    and "∀τ∈(down (U s) t). (s, x τ) ∈ (x´= f & G on U S @ t0)"
  shows "∀τ∈(down (U s) t). C (x τ)"
proof
  fix τ assume "τ ∈ (down (U s) t)"
  hence "x τ ∈ g_orbital f G U S t0 s" 
    using assms(2) unfolding g_ode_def by blast
  also have "∀y. y ∈ (g_orbital f G U S t0 s) ⟶ C y" 
    using assms(1) unfolding wp_rel g_ode_def by(auto simp: p2r_def)
  ultimately show "C (x τ)" 
    by blast
qed

lemma diff_cut_axiom:
  assumes "wp (x´= f & G on U S @ t0) ⌈C⌉ = Id"
  shows "wp (x´= f & G on U S @ t0) ⌈Q⌉ = wp (x´= f & (λs. G s ∧ C s) on U S @ t0) ⌈Q⌉"
proof(rule_tac f="λ x. wp x ⌈Q⌉" in HOL.arg_cong, rule subset_antisym)
  show "(x´=f & G on U S @ t0) ⊆ (x´=f & λs. G s ∧ C s on U S @ t0)"
  proof(clarsimp simp: g_ode_def)
    fix s and s' assume "s' ∈ g_orbital f G U S t0 s"
    then obtain τ::real and X where x_ivp: "X ∈ Sols f U S t0 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 t0 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› by auto
    ultimately have "∀t∈(down (U s) τ). X t ∈ g_orbital f G U S t0 s"
      using g_orbitalI[OF x_ivp] by (metis (mono_tags, lifting))
    hence "∀t∈(down (U s) τ). C (X t)" 
      using wp_g_evol_IdD[OF assms(1)] unfolding g_ode_def by blast
    thus "s' ∈ g_orbital f (λs. G s ∧ C s) U S t0 s"
      using g_orbitalI[OF x_ivp ‹τ ∈ U s›] guard_x ‹X τ = s'› by fastforce
  qed
next show "(x´=f & λs. G s ∧ C s on U S @ t0) ⊆ (x´=f & G on U S @ t0)"  
    by (auto simp: g_orbital_eq g_ode_def)
qed

lemma diff_cut_rule:
  assumes wp_C: "⌈P⌉ ≤ wp (x´= f & G on U S @ t0) ⌈C⌉"
    and wp_Q: "⌈P⌉ ≤ wp (x´= f & (λs. G s ∧ C s) on U S @ t0) ⌈Q⌉"
  shows "⌈P⌉ ≤ wp (x´= f & G on U S @ t0) ⌈Q⌉"
proof(subst wp_rel, simp add: g_orbital_eq p2r_def g_ode_def, 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 t0 s" 
    and guard_x:"∀x. x ∈ U s ∧ x ≤ t ⟶ G (X x)"
  have "∀t∈(down (U s) t). X t ∈ g_orbital f G U S t0 s"
    using g_orbitalI[OF x_ivp] guard_x by auto
  hence "∀t∈(down (U s) t). C (X t)" 
    using wp_C ‹P s› by (subst (asm) wp_rel, auto simp: g_ode_def)
  hence "X t ∈ g_orbital f (λs. G s ∧ C s) U S t0 s"
    using guard_x ‹t ∈ U s› by (auto intro!: g_orbitalI x_ivp)
  thus "Q (X t)"
    using ‹P s› wp_Q by (subst (asm) wp_rel) (auto simp: g_ode_def)
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,s) ∈ wp (x´= f & G) ⌈I⌉"
  using assms unfolding wp_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 "wp (x´= f & G) ⌈I⌉ = wp ⌈G⌉ ⌈I⌉"
proof(unfold wp_g_orbital, subst wp_rel, 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 t0 G" and "⌈I⌉ ≤ ⌈Q⌉"
  shows "⌈P⌉ ≤ wp (x´= f & G on U S @ t0) ⌈Q⌉"
  apply(rule wp_g_orbital_inv[OF assms(1) _ assms(3)])
  unfolding wp_diff_inv using assms(2) .

end