Theory HS_VC_KAT_rel

(*  Title:       Verification and refinement of hybrid systems in the relational KAT
    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 use our relational model to obtain verification and refinement components for hybrid 
programs. We devise three methods for reasoning with evolution commands and their continuous 
dynamics: providing flows, solutions or invariants. ›

theory HS_VC_KAT_rel
  imports 
    "../HS_ODEs"
    "HS_VC_KAT"
    "../HS_VC_KA_rel"

begin

interpretation rel_tests: test_semiring "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)" "λx. Id ∩ ( - x)"
  by (standard, auto)

interpretation rel_kat: kat "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)" rtrancl "λx. Id ∩ ( - x)"
  by (unfold_locales)

definition rel_R :: "'a rel ⇒ 'a rel ⇒ 'a rel" where 
  "rel_R P Q = ⋃{X. rel_kat.Hoare P X Q}"

interpretation rel_rkat: rkat "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)" rtrancl "(λX. Id ∩ - X)" rel_R
  by (standard, auto simp: rel_R_def rel_kat.Hoare_def)


subsubsection ‹ Regular programs›

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

type_synonym 'a pred = "'a ⇒ bool"

notation Id (‹skip›)
     and empty (‹abort›)
     and relcomp (infixr ‹;› 75)

unbundle no floor_ceiling_syntax
no_notation tau (‹τ›)
        and n_op (‹n _› [90] 91)

definition p2r :: "'a pred ⇒ 'a rel" (‹⌈_⌉›) 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_tests.t ⌈P⌉ = ⌈P⌉"
  "(- Id) ∪ ⌈P⌉ = - ⌈λs. ¬ P s⌉"
  "Id ∩ (- ⌈P⌉) = ⌈λs. ¬ P s⌉"
  unfolding p2r_def by auto

text ‹ Lemmas for verification condition generation ›

lemma RdL_is_rRKAT: "(∀x. {(x,x)}; R1 ⊆ {(x,x)}; R2) = (R1 ⊆ R2)"
  by auto (* Refinement in dL is that of rKAT *)

― ‹ Hoare Triples ›

abbreviation relHoare (‹❙{_❙}_❙{_❙}›) 
  where "❙{P❙}X❙{Q❙} ≡ rel_kat.Hoare ⌈P⌉ X ⌈Q⌉"

lemma rel_kat_H: "❙{P❙} X ❙{Q❙} ⟷ (∀s s'. P s ⟶ (s,s') ∈ X ⟶ Q s')"
  by (simp add: rel_kat.Hoare_def, auto simp add: p2r_def)

― ‹ Skip ›

lemma sH_skip[simp]: "❙{P❙} skip ❙{Q❙} ⟷ ⌈P⌉ ≤ ⌈Q⌉"
  unfolding rel_kat_H by simp

lemma H_skip: "❙{P❙} skip ❙{P❙}"
  by simp

― ‹ Tests ›

lemma sH_test[simp]: "❙{P❙} ⌈R⌉ ❙{Q❙} = (∀s. P s ⟶ R s ⟶ Q s)"
  by (subst rel_kat_H, simp add: p2r_def)

― ‹ Abort ›

lemma sH_abort[simp]: "❙{P❙} abort ❙{Q❙} ⟷ True"
  unfolding rel_kat_H by simp

lemma H_abort: "❙{P❙} abort ❙{Q❙}"
  by simp

― ‹ 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 sH_assign[simp]: "❙{P❙} (x ::= e) ❙{Q❙} ⟷ (∀s. P s ⟶ Q (χ j. ((($) s)(x := (e s))) j))"
  unfolding rel_kat_H vec_upd_def assign_def by (auto simp: fun_upd_def)

lemma H_assign: "P = (λs. Q (χ j. ((($) s)(x := (e s))) j)) ⟹ ❙{P❙} (x ::= e) ❙{Q❙}"
  by simp

― ‹ Nondeterministic assignments ›

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

lemma sH_nondet_assign[simp]: 
  "❙{P❙} (x ::= ?) ❙{Q❙} ⟷ (∀s. P s ⟶ (∀k. Q (χ j. ((($) s)(x := k)) j)))"
  unfolding rel_kat_H vec_upd_def nondet_assign_def by (auto simp: fun_upd_def)

lemma H_nondet_assign: "❙{λs. ∀k. P (χ j. ((($) s)(x := k)) j)❙} (x ::= ?) ❙{P❙}"
  by simp

― ‹ Sequential Composition ›

lemma H_seq: "❙{P❙} X ❙{R❙} ⟹ ❙{R❙} Y ❙{Q❙} ⟹ ❙{P❙} X;Y ❙{Q❙}"
  using rel_kat.H_seq .

lemma sH_seq: "❙{P❙} X;Y ❙{Q❙} = ❙{P❙} X ❙{λs. ∀s'. (s, s') ∈ Y ⟶ Q s'❙}"
  unfolding rel_kat_H by auto

lemma H_assignl: 
  assumes "❙{K❙} X ❙{Q❙}" 
    and "∀s. P s ⟶ K (vec_lambda ((($) s)(x := e s)))"
  shows "❙{P❙} (x ::= e);X ❙{Q❙}"
  apply(rule H_seq, subst sH_assign)
  using assms by auto

― ‹ Nondeterministic Choice ›

lemma sH_choice: "❙{P❙} X ∪ Y ❙{Q❙} ⟷ (❙{P❙} X ❙{Q❙} ∧ ❙{P❙} Y ❙{Q❙})"
  unfolding rel_kat_H by auto

lemma H_choice: "❙{P❙} X ❙{Q❙} ⟹ ❙{P❙} Y ❙{Q❙} ⟹ ❙{P❙} X ∪ Y ❙{Q❙}"
  using rel_kat.H_choice .

― ‹ Conditional Statement ›

abbreviation cond_sugar :: "'a pred ⇒ 'a rel ⇒ 'a rel ⇒ 'a rel" 
  (‹IF _ THEN _ ELSE _› [64,64] 63) 
  where "IF B THEN X ELSE Y ≡ rel_kat.kat_cond ⌈B⌉ X Y"

lemma sH_cond[simp]: 
  "❙{P❙} (IF B THEN X ELSE Y) ❙{Q❙} ⟷ (❙{λs. P s ∧ B s❙} X ❙{Q❙} ∧ ❙{λs. P s ∧ ¬ B s❙} Y ❙{Q❙})"
  by (auto simp: rel_kat.H_cond_iff rel_kat_H)

lemma H_cond: 
  "❙{λs. P s ∧ B s❙} X ❙{Q❙} ⟹ ❙{λs. P s ∧ ¬ B s❙} Y ❙{Q❙} ⟹ ❙{P❙} (IF B THEN X ELSE Y) ❙{Q❙}"
  by simp

― ‹ While Loop ›

abbreviation while_inv_sugar :: "'a pred ⇒ 'a pred ⇒ 'a rel ⇒ 'a rel" 
  (‹WHILE _ INV _ DO _› [64,64,64] 63) 
  where "WHILE B INV I DO X ≡ rel_kat.kat_while_inv ⌈B⌉ ⌈I⌉ X"

lemma sH_whileI: "∀s. P s ⟶ I s ⟹ ∀s. I s ∧ ¬ B s ⟶ Q s ⟹ ❙{λs. I s ∧ B s❙} X ❙{I❙} 
  ⟹ ❙{P❙} (WHILE B INV I DO X) ❙{Q❙}"
  by (rule rel_kat.H_while_inv, auto simp: p2r_def rel_kat.Hoare_def, fastforce)

lemma "❙{λs. P s ∧ B s❙} X ❙{λs. P s❙} ⟹ ❙{P❙} (WHILE B INV I DO X) ❙{λs. P s ∧ ¬ B s❙}"
  using rel_kat.H_while[of "⌈P⌉" "⌈B⌉" X]
  unfolding rel_kat.kat_while_inv_def by auto

― ‹ Finite Iteration ›

abbreviation loopi_sugar :: "'a rel ⇒ 'a pred ⇒ 'a rel" (‹LOOP _ INV _ › [64,64] 63)
  where "LOOP X INV I ≡ rel_kat.kat_loop_inv X ⌈I⌉"

lemma H_loop: "❙{P❙} X ❙{P❙} ⟹ ❙{P❙} (LOOP X INV I) ❙{P❙}"
  by (auto intro: rel_kat.H_loop)

lemma H_loopI: "❙{I❙} X ❙{I❙} ⟹ ⌈P⌉ ⊆ ⌈I⌉ ⟹ ⌈I⌉ ⊆ ⌈Q⌉ ⟹ ❙{P❙} (LOOP X INV I) ❙{Q❙}"
  using rel_kat.H_loop_inv[of "⌈P⌉" "⌈I⌉" X "⌈Q⌉"] by auto


subsubsection ‹ Evolution commands ›

― ‹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 sH_g_evol[simp]:  
  fixes φ :: "('a::preorder) ⇒ 'b ⇒ 'b"
  shows "❙{P❙} (EVOL φ G U) ❙{Q❙} = (∀s. P s ⟶ (∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s)))"
  unfolding rel_kat_H g_evol_def g_orbit_eq by auto

lemma H_g_evol: 
  fixes φ :: "('a::preorder) ⇒ 'b ⇒ 'b"
  assumes "P = (λs. (∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s)))"
  shows "❙{P❙} (EVOL φ G U) ❙{Q❙}"
  by (simp add: assms)

― ‹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 T S @ t⇩0) = {(s,s') |s s'. s' ∈ g_orbital f G T S t⇩0 s}"

lemma H_g_orbital: 
  "P = (λs. (∀X∈ivp_sols f U S t⇩0 s. ∀t∈U s. (∀τ∈down (U s) t. G (X τ)) ⟶ Q (X t))) ⟹ 
  ❙{P❙} (x´= f & G on U S @ t⇩0) ❙{Q❙}"
  unfolding rel_kat_H g_ode_def g_orbital_eq by clarsimp

lemma sH_g_orbital: "❙{P❙} (x´= f & G on U S @ t⇩0) ❙{Q❙} = 
  (∀s. P s ⟶ (∀X∈ivp_sols f U S t⇩0 s. ∀t∈U s. (∀τ∈down (U s) t. G (X τ)) ⟶ Q (X t)))"
  unfolding g_orbital_eq g_ode_def rel_kat_H by auto

context local_flow
begin

lemma sH_g_ode_subset: 
  assumes "⋀s. s ∈ S ⟹ 0 ∈ U s ∧ is_interval (U s) ∧ U s ⊆ T"
  shows "❙{P❙} (x´= (λt. f) & G on U S @ 0) ❙{Q❙} = 
  (∀s∈S. P s ⟶ (∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s)))"
proof(unfold sH_g_orbital, clarsimp, safe)
  fix s t
  assume hyps: "s ∈ S" "P s" "t ∈ U s" "∀τ. τ ∈ U s ∧ τ ≤ t ⟶ G (φ τ s)"
    and main: "∀s. P s ⟶ (∀X∈Sols (λt. f) U S 0 s. ∀t∈U s. (∀τ. τ ∈ U s ∧ τ ≤ t ⟶ G (X τ)) ⟶ Q (X t))"
  hence "(λt. φ t s) ∈ Sols (λt. f) U S 0 s"
    using in_ivp_sols assms by blast
  thus "Q (φ t s)"
    using main hyps by fastforce
next
  fix s X t
  assume hyps: "P s" "X ∈ Sols (λt. f) U S 0 s" "t ∈ U s"  "∀τ. τ ∈ U s ∧ τ ≤ t ⟶ G (X τ)"
    and main: "∀s∈S. P s ⟶ (∀t∈U s. (∀τ. τ ∈ U s ∧ τ ≤ t ⟶ G (φ τ s)) ⟶ Q (φ t s))"
  hence obs: "s ∈ S"
    using ivp_sols_def[of "λt. f"] init_time by auto
  hence "∀τ∈down (U s) t. X τ = φ τ s"
    using eq_solution hyps assms by blast
  thus "Q (X t)"
    using hyps main obs by auto
qed

lemma H_g_ode_subset:
  assumes "⋀s. s ∈ S ⟹ 0 ∈ U s ∧ is_interval (U s) ∧ U s ⊆ T"
    and "P = (λs. s ∈ S ⟶ (∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s)))" 
  shows "❙{P❙} (x´= (λt. f) & G on U S @ 0) ❙{Q❙}"
  using assms apply(subst sH_g_ode_subset[OF assms(1)])
  unfolding assms by auto

lemma sH_g_ode: "❙{P❙} (x´= (λt. f) & G on (λs. T) S @ 0) ❙{Q❙} = 
  (∀s∈S. P s ⟶ (∀t∈T. (∀τ∈down T t. G (φ τ s)) ⟶ Q (φ t s)))"
  by (subst sH_g_ode_subset, auto simp: init_time interval_time)

lemma sH_g_ode_ivl: "t ≥ 0 ⟹ t ∈ T ⟹ ❙{P❙} (x´= (λt. f) & G on (λs. {0..t}) S @ 0) ❙{Q❙} = 
  (∀s∈S. P s ⟶ (∀t∈{0..t}. (∀τ∈{0..t}. G (φ τ s)) ⟶ Q (φ t s)))"
  apply(subst sH_g_ode_subset; clarsimp, (force)?)
  using init_time interval_time mem_is_interval_1_I by blast

lemma sH_orbit: "❙{P❙} ({(s,s') | s s'. s' ∈ γ⇧φ s}) ❙{Q❙} = (∀s ∈ S. P s ⟶ (∀ t ∈ T. Q (φ t s)))"
  using sH_g_ode unfolding orbit_def g_ode_def by auto

end

― ‹ 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 @ t⇩0 DINV I) = (x´= f & G on U S @ t⇩0)"

lemma sH_g_orbital_guard: 
  assumes "R = (λs. G s ∧ Q s)"
  shows "❙{P❙} (x´= f & G on U S @ t⇩0) ❙{Q❙} = ❙{P❙} (x´= f & G on U S @ t⇩0) ❙{R❙}" 
  using assms unfolding g_orbital_eq rel_kat_H ivp_sols_def g_ode_def by auto

lemma sH_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_tac p'="⌈I⌉" in rel_kat.H_consl, simp)
  using assms(3) apply(rule_tac q'="⌈I⌉" in rel_kat.H_consr, simp)
  using assms(2) by simp

lemma sH_diff_inv[simp]: "❙{I❙} (x´= f & G on U S @ t⇩0) ❙{I❙} = diff_invariant I f U S t⇩0 G"
  unfolding diff_invariant_eq rel_kat_H g_orbital_eq g_ode_def by auto

lemma H_g_ode_inv: "❙{I❙} (x´= f & G on U S @ t⇩0) ❙{I❙} ⟹ ⌈P⌉ ≤ ⌈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 q'="⌈λs. I s ∧ G s⌉" in rel_kat.H_consr, simp)
  apply(subst sH_g_orbital_guard[symmetric], force)
  by (rule_tac I="I" in sH_g_orbital_inv, simp_all)


subsection ‹ Refinement Components ›

― ‹ Skip ›

lemma R_skip: "(∀s. P s ⟶ Q s) ⟹ skip ≤ rel_R ⌈P⌉ ⌈Q⌉"
  by (rule rel_rkat.R2, simp)

― ‹ Abort ›

lemma R_abort: "abort ≤ rel_R ⌈P⌉ ⌈Q⌉"
  by (rule rel_rkat.R2, simp)

― ‹ Sequential Composition ›

lemma R_seq: "(rel_R ⌈P⌉ ⌈R⌉) ; (rel_R ⌈R⌉ ⌈Q⌉) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  using rel_rkat.R_seq by blast

lemma R_seq_law: "X ≤ rel_R ⌈P⌉ ⌈R⌉ ⟹ Y ≤ rel_R ⌈R⌉ ⌈Q⌉ ⟹ X; Y ≤ rel_R ⌈P⌉ ⌈Q⌉"
  unfolding rel_rkat.spec_def by (rule H_seq)

lemmas R_seq_mono = relcomp_mono

― ‹ Nondeterministic Choice ›

lemma R_choice: "(rel_R ⌈P⌉ ⌈Q⌉) ∪ (rel_R ⌈P⌉ ⌈Q⌉) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  using rel_rkat.R_choice[of "⌈P⌉" "⌈Q⌉"] .

lemma R_choice_law: "X ≤ rel_R ⌈P⌉ ⌈Q⌉ ⟹ Y ≤ rel_R ⌈P⌉ ⌈Q⌉ ⟹ X ∪ Y ≤ rel_R ⌈P⌉ ⌈Q⌉"
  using le_supI .

lemma R_choice_mono: "P' ⊆ P ⟹ Q' ⊆ Q ⟹ P' ∪ Q' ⊆ P ∪ Q"
  using Un_mono .

― ‹ Assignment ›

lemma R_assign: "(x ::= e) ≤ rel_R ⌈λs. P (χ j. ((($) s)(x := e s)) j)⌉ ⌈P⌉"
  unfolding rel_rkat.spec_def by (rule H_assign, clarsimp simp: fun_upd_def)

lemma R_assign_law: 
  "(∀s. P s ⟶ Q (χ j. ((($) s)(x := (e s))) j)) ⟹ (x ::= e) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  unfolding sH_assign[symmetric] by (rule rel_rkat.R2)

lemma R_assignl: "P = (λs. R (χ j. ((($) s)(x := e s)) j)) ⟹ 
  (x ::= e) ; rel_R ⌈R⌉ ⌈Q⌉ ≤ rel_R ⌈P⌉ ⌈Q⌉"
  apply(rule_tac R=R in R_seq_law)
  by (rule_tac R_assign_law, simp_all)

lemma R_assignr: "R = (λs. Q (χ j. ((($) s)(x := e s)) j)) ⟹ 
  rel_R ⌈P⌉ ⌈R⌉; (x ::= e) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  apply(rule_tac R=R in R_seq_law, simp)
  by (rule_tac R_assign_law, simp)

lemma "(x ::= e) ; rel_R ⌈Q⌉ ⌈Q⌉ ≤ rel_R ⌈(λs. Q (χ j. ((($) s)(x := e s)) j))⌉ ⌈Q⌉"
  by (rule R_assignl) simp

lemma "rel_R ⌈Q⌉ ⌈(λs. Q (χ j. ((($) s)(x := e s)) j))⌉; (x ::= e) ≤ rel_R ⌈Q⌉ ⌈Q⌉"
  by (rule R_assignr) simp

― ‹ Nondeterministic Assignment ›

lemma R_nondet_assign: "(x ::= ?) ≤ rel_R ⌈λs. ∀k. P (χ j. ((($) s)(x := k)) j)⌉ ⌈P⌉"
  unfolding rel_rkat.spec_def by (rule H_nondet_assign)

lemma R_nondet_assign_law: 
  "(∀s. P s ⟶ (∀k. Q (χ j. ((($) s)(x := k)) j))) ⟹ (x ::= ?) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  unfolding sH_nondet_assign[symmetric] by (rule rel_rkat.R2)

― ‹ Conditional Statement ›

lemma R_cond: 
  "(IF B THEN rel_R ⌈λs. B s ∧ P s⌉ ⌈Q⌉ ELSE rel_R ⌈λs. ¬ B s ∧ P s⌉ ⌈Q⌉) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  using rel_rkat.R_cond[of "⌈B⌉" "⌈P⌉" "⌈Q⌉"] by simp

lemma R_cond_mono: "X ≤ X' ⟹ Y ≤ Y' ⟹ (IF P THEN X ELSE Y) ≤ IF P THEN X' ELSE Y'"
  by (auto simp: rel_kat.kat_cond_def)

lemma R_cond_law: "X ≤ rel_R ⌈λs. B s ∧ P s⌉ ⌈Q⌉ ⟹ Y ≤ rel_R ⌈λs. ¬ B s ∧ P s⌉ ⌈Q⌉ ⟹ 
  (IF B THEN X ELSE Y) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  by (rule order_trans; (rule R_cond_mono)?, (rule R_cond)?) auto

― ‹ While Loop ›

lemma R_while: "K = (λs. P s ∧ ¬ B s) ⟹ 
  WHILE B INV I DO (rel_R ⌈λs. P s ∧ B s⌉ ⌈P⌉) ≤ rel_R ⌈P⌉ ⌈K⌉"
  unfolding rel_kat.kat_while_inv_def using rel_rkat.R_while[of "⌈B⌉" "⌈P⌉"] by simp

lemma R_whileI:
  "X ≤ rel_R ⌈I⌉ ⌈I⌉ ⟹ ⌈P⌉ ≤ ⌈λs. I s ∧ B s⌉ ⟹ ⌈λs. I s ∧ ¬ B s⌉ ≤ ⌈Q⌉ ⟹ 
  WHILE B INV I DO X ≤ rel_R ⌈P⌉ ⌈Q⌉"
  by (rule rel_rkat.R2, rule rel_kat.H_while_inv, auto simp: rel_kat_H rel_rkat.spec_def)

lemma R_while_mono: "X ≤ X' ⟹ (WHILE P INV I DO X) ⊆ WHILE P INV I DO X'"
  by (simp add: rel_dioid.mult_isol rel_dioid.mult_isor rel_ka.conway.dagger_iso 
      rel_kat.kat_while_def rel_kat.kat_while_inv_def)

lemma R_while_law: "X ≤ rel_R ⌈λs. P s ∧ B s⌉ ⌈P⌉ ⟹ Q = (λs. P s ∧ ¬ B s) ⟹ 
  (WHILE B INV I DO X) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  by (rule order_trans; (rule R_while_mono)?, (rule R_while)?)

― ‹ Finite Iteration ›

lemma R_loop:"LOOP rel_R ⌈P⌉ ⌈P⌉ INV I ≤ rel_R ⌈P⌉ ⌈P⌉"
  using rel_rkat.R_loop .

lemma R_loopI: 
  "X ≤ rel_R ⌈I⌉ ⌈I⌉ ⟹ ⌈P⌉ ≤ ⌈I⌉ ⟹ ⌈I⌉ ≤ ⌈Q⌉ ⟹ LOOP X INV I ≤ rel_R ⌈P⌉ ⌈Q⌉"
  unfolding rel_rkat.spec_def using H_loopI by blast

lemma R_loop_mono: "X ≤ X' ⟹ LOOP X INV I ⊆ LOOP X' INV I"
  unfolding rel_kat.kat_loop_inv_def by (simp add: rel_ka.star_iso)

― ‹ Evolution command (flow) ›

lemma R_g_evol: 
  fixes φ :: "('a::preorder) ⇒ 'b ⇒ 'b"
  shows "(EVOL φ G U) ≤ rel_R ⌈λs. ∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ P (φ t s)⌉ ⌈P⌉"
  unfolding rel_rkat.spec_def by (rule H_g_evol, simp)

lemma R_g_evol_law: 
  fixes φ :: "('a::preorder) ⇒ 'b ⇒ 'b"
  shows "(∀s. P s ⟶ (∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s))) ⟹ (EVOL φ G U) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  unfolding sH_g_evol[symmetric] rel_rkat.spec_def .

lemma R_g_evoll: 
  fixes φ :: "('a::preorder) ⇒ 'b ⇒ 'b"
  shows "P = (λs. ∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ R (φ t s)) ⟹ 
  (EVOL φ G U) ; rel_R ⌈R⌉ ⌈Q⌉ ≤ rel_R ⌈P⌉ ⌈Q⌉"
  apply(rule_tac R=R in R_seq_law)
  by (rule_tac R_g_evol_law, simp_all)

lemma R_g_evolr: 
  fixes φ :: "('a::preorder) ⇒ 'b ⇒ 'b"
  shows "R = (λs. ∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s)) ⟹ 
  rel_R ⌈P⌉ ⌈R⌉; (EVOL φ G U) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  apply(rule_tac R=R in R_seq_law, simp)
  by (rule_tac R_g_evol_law, simp)

lemma 
  fixes φ :: "('a::preorder) ⇒ 'b ⇒ 'b"
  shows "EVOL φ G U ; rel_R ⌈Q⌉ ⌈Q⌉ ≤ rel_R ⌈λs. ∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s)⌉ ⌈Q⌉"
  by (rule R_g_evoll) simp

lemma 
  fixes φ :: "('a::preorder) ⇒ 'b ⇒ 'b"
  shows "rel_R ⌈Q⌉ ⌈λs. ∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s)⌉; EVOL φ G U ≤ rel_R ⌈Q⌉ ⌈Q⌉"
  by (rule R_g_evolr) simp

― ‹ Evolution command (ode) ›

context local_flow
begin

lemma R_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) ≤ 
  rel_R ⌈λs. s∈S ⟶ (∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ P (φ t s))⌉ ⌈P⌉"
  unfolding rel_rkat.spec_def by (rule H_g_ode_subset[OF assms], simp_all)

lemma R_g_ode_rule_subset: 
  assumes "⋀s. s ∈ S ⟹ 0 ∈ U s ∧ is_interval (U s) ∧ U s ⊆ T"
  shows "(∀s∈S. P s ⟶ (∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s))) ⟹ 
  (x´= (λt. f) & G on U S @ 0) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  by (rule rel_rkat.R2, subst sH_g_ode_subset[OF assms], auto)

lemma R_g_odel_subset: 
  assumes "⋀s. s ∈ S ⟹ 0 ∈ U s ∧ is_interval (U s) ∧ U s ⊆ T"
    and "P = (λs. ∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ R (φ t s))"
  shows "(x´= (λt. f) & G on U S @ 0) ; rel_R ⌈R⌉ ⌈Q⌉ ≤ rel_R ⌈P⌉ ⌈Q⌉"
  apply (rule_tac R=R in R_seq_law, rule_tac R_g_ode_rule_subset)
  by (simp_all add: assms)

lemma R_g_oder_subset: 
  assumes "⋀s. s ∈ S ⟹ 0 ∈ U s ∧ is_interval (U s) ∧ U s ⊆ T"
    and "R = (λs. ∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s))"
  shows "rel_R ⌈P⌉ ⌈R⌉; (x´= (λt. f) & G on U S @ 0) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  apply (rule_tac R=R in R_seq_law, simp)
  by (rule_tac R_g_ode_rule_subset, simp_all add: assms)

lemma R_g_ode: "(x´= (λt. f) & G on (λs. T) S @ 0) ≤ 
  rel_R ⌈λs. s∈S ⟶ (∀t∈T. (∀τ∈down T t. G (φ τ s)) ⟶ P (φ t s))⌉ ⌈P⌉"
  by (rule R_g_ode_subset, auto simp: init_time interval_time)

lemma R_g_ode_law: "(∀s∈S. P s ⟶ (∀t∈T. (∀τ∈down T t. G (φ τ s)) ⟶ Q (φ t s))) ⟹ 
  (x´= (λt. f) & G on (λs. T) S @ 0) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  unfolding sH_g_ode[symmetric] by (rule rel_rkat.R2)

lemma R_g_odel: "P = (λs. ∀t∈T. (∀τ∈down T t. G (φ τ s)) ⟶ R (φ t s)) ⟹ 
  (x´= (λt. f) & G on (λs. T) S @ 0) ; rel_R ⌈R⌉ ⌈Q⌉ ≤ rel_R ⌈P⌉ ⌈Q⌉"
  by (rule R_g_odel_subset, auto simp: init_time interval_time)

lemma R_g_oder: "R = (λs. ∀t∈T. (∀τ∈down T t. G (φ τ s)) ⟶ Q (φ t s)) ⟹ 
  rel_R ⌈P⌉ ⌈R⌉; (x´= (λt. f) & G on (λs. T) S @ 0) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  by (rule R_g_oder_subset, auto simp: init_time interval_time)

lemma R_g_ode_ivl: 
  "t ≥ 0 ⟹ t ∈ T ⟹ (∀s∈S. P s ⟶ (∀t∈{0..t}. (∀τ∈{0..t}. G (φ τ s)) ⟶ Q (φ t s))) ⟹ 
  (x´= (λt. f) & G on (λs. {0..t}) S @ 0) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  unfolding sH_g_ode_ivl[symmetric] by (rule rel_rkat.R2)

end

― ‹ Evolution command (invariants) ›

lemma R_g_ode_inv: "diff_invariant I f T S t⇩0 G ⟹ ⌈P⌉ ≤ ⌈I⌉ ⟹ ⌈λs. I s ∧ G s⌉ ≤ ⌈Q⌉ ⟹ 
  (x´=f & G on T S @ t⇩0 DINV I) ≤ rel_R ⌈P⌉ ⌈Q⌉"
  unfolding rel_rkat.spec_def by (auto simp: H_g_ode_inv)


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 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_rule1:
  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.sH_g_ode_subset, auto)

lemma diff_solve_rule2: 
  fixes c::"'a::{heine_borel, banach}"
  assumes "∀s. P s ⟶ (∀t≥0. (∀τ∈{0..t}. G (s + τ *⇩R c)) ⟶ Q (s + t *⇩R c))"
  shows "❙{P❙} (x´=(λs. c) & G) ❙{Q❙}"
  apply(subst local_flow.sH_g_ode_subset[where T=UNIV and φ="(λ t x. x + t *⇩R c)"])
  using line_is_local_flow assms by auto

lemma diff_weak_rule: 
  assumes "⌈G⌉ ≤ ⌈Q⌉"
  shows "❙{P❙} (x´= f & G on U S @ t⇩0) ❙{Q❙}"
  using assms unfolding g_orbital_eq rel_kat_H ivp_sols_def g_ode_def by auto

lemma diff_cut_rule:
  assumes wp_C:"rel_kat.Hoare ⌈P⌉ (x´= f & G on U S @ t⇩0) ⌈C⌉"
    and wp_Q:"rel_kat.Hoare ⌈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 rel_kat_H, 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 ∈ ivp_sols f U S t⇩0 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 t⇩0 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) rel_kat_H, auto simp: g_ode_def)
  hence "X t ∈ g_orbital f (λs. G s ∧ C s) 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› wp_Q by (subst (asm) rel_kat_H) (auto simp: g_ode_def)
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(subst g_ode_inv_def[symmetric, where I=I], rule H_g_ode_inv)
  unfolding sH_diff_inv using assms by auto

end