Theory HS_VC_KAT_ndfun

(*  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 state transformers model to obtain verification and refinement components for 
hybrid programs. We retake the three methods for reasoning with evolution commands and their 
continuous dynamics: providing flows, solutions or invariants. ›

theory HS_VC_KAT_ndfun
  imports 
    "../HS_ODEs"
    "HS_VC_KAT"
    "../HS_VC_KA_ndfun"

begin

instantiation nd_fun :: (type) kat
begin

definition "n f = (λx. if ((f⇩_∙) x = {}) then {x} else {})⇧^∙"

lemma nd_fun_n_op_one[nd_fun_ka]: "n (n (1::'a nd_fun)) = 1"
  and nd_fun_n_op_mult[nd_fun_ka]: "n (n (n x ⋅ n y)) = n x ⋅ n y"
  and nd_fun_n_op_mult_comp[nd_fun_ka]: "n x ⋅ n (n x) = 0" 
  and nd_fun_n_op_de_morgan[nd_fun_ka]: "n (n (n x) ⋅ n (n y)) = n x + n y" for x::"'a nd_fun"
  unfolding n_op_nd_fun_def one_nd_fun_def times_nd_fun_def plus_nd_fun_def zero_nd_fun_def 
  by (auto simp: nd_fun_eq_iff kcomp_def)

instance
  by (intro_classes, auto simp: nd_fun_ka)

end

instantiation nd_fun :: (type) rkat
begin

definition "Ref_nd_fun P Q ≡ (λs. ⋃{(f⇩_∙) s|f. Hoare P f Q})⇧^∙"

instance
  apply(intro_classes)
  by (unfold Hoare_def n_op_nd_fun_def Ref_nd_fun_def times_nd_fun_def)
    (auto simp: kcomp_def le_fun_def less_eq_nd_fun_def)

end


subsubsection ‹ Regular programs›

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

type_synonym 'a pred = "'a ⇒ bool"

unbundle no floor_ceiling_syntax
no_notation tau (‹τ›)
        and Relation.relcomp (infixl ‹;› 75)
        and proto_near_quantale_class.bres (infixr ‹→› 60)

definition p2ndf :: "'a pred ⇒ 'a nd_fun" (‹(1⌈_⌉)›)
  where "⌈Q⌉ ≡ (λ x::'a. {s::'a. s = x ∧ Q s})⇧^∙"

lemma p2ndf_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⌉"
  "𝔱𝔱 ⌈P⌉ = ⌈P⌉"
  "n ⌈P⌉ = ⌈λs. ¬ P s⌉"
  unfolding p2ndf_def one_nd_fun_def less_eq_nd_fun_def times_nd_fun_def plus_nd_fun_def 
  by (auto simp: nd_fun_eq_iff kcomp_def le_fun_def n_op_nd_fun_def)

text ‹ Lemmas for verification condition generation ›

― ‹ Hoare Triples ›

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

lemma ndfun_kat_H: "❙{P❙} X ❙{Q❙} ⟷ (∀s s'. P s ⟶ s' ∈ (X⇩_∙) s ⟶ Q s')"
  unfolding Hoare_def p2ndf_def less_eq_nd_fun_def times_nd_fun_def kcomp_def 
  by (auto simp add: le_fun_def n_op_nd_fun_def)

― ‹ Skip ›

abbreviation "skip ≡ (1::'a nd_fun)"

lemma sH_skip[simp]: "❙{P❙} skip ❙{Q❙} ⟷ ⌈P⌉ ≤ ⌈Q⌉"
  unfolding ndfun_kat_H by (simp add: one_nd_fun_def)

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 ndfun_kat_H, simp add: p2ndf_def)

― ‹ Abort ›

abbreviation "abort ≡ (0::'a nd_fun)"

lemma sH_abort[simp]: "❙{P❙} abort ❙{Q❙} ⟷ True"
  unfolding ndfun_kat_H by (simp add: zero_nd_fun_def)

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

― ‹ Assignments ›

definition assign :: "'b ⇒ ('a^'b ⇒ 'a) ⇒ ('a^'b) nd_fun" (‹(2_ ::= _)› [70, 65] 61) 
  where "(x ::= e) = (λs. {vec_upd s x (e s)})⇧^∙"

lemma sH_assign[simp]: "❙{P❙} (x ::= e) ❙{Q❙} ⟷ (∀s. P s ⟶ Q (χ j. ((($) s)(x := (e s))) j))"
  unfolding ndfun_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) nd_fun" (‹(2_ ::= ? )› [70] 61)
    where "(x ::= ?) = (λs. {vec_upd s x k|k. True})⇧^∙"

lemma sH_nondet_assign[simp]: 
  "❙{P❙} (x ::= ?) ❙{Q❙} ⟷ (∀s. P s ⟶ (∀k. Q (χ j. ((($) s)(x := k)) j)))"
  unfolding ndfun_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 ›

abbreviation seq_seq :: "'a nd_fun ⇒ 'a nd_fun ⇒ 'a nd_fun" (infixl ‹;› 75)
  where "f ; g ≡ f ⋅ g"

lemma H_seq: "❙{P❙} X ❙{R❙} ⟹ ❙{R❙} Y ❙{Q❙} ⟹ ❙{P❙} X;Y ❙{Q❙}"
  by (auto intro: H_seq)

lemma sH_seq: "❙{P❙} X;Y ❙{Q❙} = ❙{P❙} X ❙{λs. ∀s'. s' ∈ (Y⇩_∙) s ⟶ Q s'❙}"
  unfolding ndfun_kat_H by (auto simp: times_nd_fun_def kcomp_def)

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 ndfun_kat_H by (auto simp: plus_nd_fun_def)

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

― ‹ Conditional Statement ›

abbreviation cond_sugar :: "'a pred ⇒ 'a nd_fun ⇒ 'a nd_fun ⇒ 'a nd_fun" (‹IF _ THEN _ ELSE _› [64,64] 63) 
  where "IF B THEN X ELSE Y ≡ 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: H_cond_iff ndfun_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 nd_fun ⇒ 'a nd_fun" (‹WHILE _ INV _ DO _› [64,64,64] 63) 
  where "WHILE B INV I DO X ≡ 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 H_while_inv, simp_all add: ndfun_kat_H)

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

― ‹ Finite Iteration ›

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

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

lemma H_loopI: "❙{I❙} X ❙{I❙} ⟹ ⌈P⌉ ≤ ⌈I⌉ ⟹ ⌈I⌉ ≤ ⌈Q⌉ ⟹ ❙{P❙} (LOOP X INV I) ❙{Q❙}"
  using 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 nd_fun" (‹EVOL›)
  where "EVOL φ G U = (λ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 ndfun_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 nd_fun" (‹(1x´= _ & _ on _ _ @ _)›) 
  where "(x´= f & G on U S @ t⇩₀) ≡ (λ s. g_orbital f G U S t⇩₀ s)⇧^∙"

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

lemma sH_g_orbital: "❙{P❙} (x´= f & G on U S @ t⇩₀) ❙{Q❙} = 
  (∀s. P s ⟶ (∀X∈ivp_sols f U S t⇩₀ s. ∀t∈U s. (∀τ∈down (U s) t. G (X τ)) ⟶ Q (X t)))"
  unfolding g_orbital_eq g_ode_def ndfun_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❙} γ⇧^φ⇧^∙ ❙{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 nd_fun" (‹(1x´=_ & _ on _ _ @ _ DINV _ )›) 
  where "(x´= f & G on U S @ t⇩₀ DINV I) = (x´= f & G on U S @ t⇩₀)"

lemma sH_g_orbital_guard: 
  assumes "R = (λs. G s ∧ Q s)"
  shows "❙{P❙} (x´= f & G on U S @ t⇩₀) ❙{Q❙} = ❙{P❙} (x´= f & G on U S @ t⇩₀) ❙{R❙}" 
  using assms unfolding g_orbital_eq ndfun_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⇩₀) ❙{I❙}" and "⌈I⌉ ≤ ⌈Q⌉"
  shows " ❙{P❙} (x´= f & G on U S @ t⇩₀) ❙{Q❙}"
  using assms(1) apply(rule_tac p'="⌈I⌉" in H_consl, simp)
  using assms(3) apply(rule_tac q'="⌈I⌉" in H_consr, simp)
  using assms(2) by simp

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

lemma H_g_ode_inv: "❙{I❙} (x´= f & G on U S @ t⇩₀) ❙{I❙} ⟹ ⌈P⌉ ≤ ⌈I⌉ ⟹ 
  ⌈λs. I s ∧ G s⌉ ≤ ⌈Q⌉ ⟹ ❙{P❙} (x´= f & G on U S @ t⇩₀ DINV I) ❙{Q❙}"
  unfolding g_ode_inv_def apply(rule_tac q'="⌈λs. I s ∧ G s⌉" in 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) ⟹ 1 ≤ Ref ⌈P⌉ ⌈Q⌉"
  by (auto simp: spec_def ndfun_kat_H one_nd_fun_def)

― ‹ Abort ›

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

― ‹ Sequential Composition ›

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

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

lemmas R_seq_mono = mult_isol_var

― ‹ Nondeterministic Choice ›

lemma R_choice: "(Ref ⌈P⌉ ⌈Q⌉) + (Ref ⌈P⌉ ⌈Q⌉) ≤ Ref ⌈P⌉ ⌈Q⌉"
  using R_choice[of "⌈P⌉" "⌈Q⌉"] .

lemma R_choice_law: "X ≤ Ref ⌈P⌉ ⌈Q⌉ ⟹ Y ≤ Ref ⌈P⌉ ⌈Q⌉ ⟹ X + Y ≤ Ref ⌈P⌉ ⌈Q⌉"
  using join.le_supI .

lemma R_choice_mono: "P' ≤ P ⟹ Q' ≤ Q ⟹ P' + Q' ⊆ P + Q"
  using set_plus_mono2 .

― ‹ Assignment ›

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

lemma R_assign_law: 
  "(∀s. P s ⟶ Q (χ j. ((($) s)(x := (e s))) j)) ⟹ (x ::= e) ≤ Ref ⌈P⌉ ⌈Q⌉"
  unfolding sH_assign[symmetric] spec_def .

lemma R_assignl: 
  "P = (λs. R (χ j. ((($) s)(x := e s)) j)) ⟹ (x ::= e) ; Ref ⌈R⌉ ⌈Q⌉ ≤ Ref ⌈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)) ⟹ Ref ⌈P⌉ ⌈R⌉; (x ::= e) ≤ Ref ⌈P⌉ ⌈Q⌉"
  apply(rule_tac R=R in R_seq_law, simp)
  by (rule_tac R_assign_law, simp)

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

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

― ‹ Nondeterministic Assignment ›

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

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

― ‹ Conditional Statement ›

lemma R_cond: 
  "(IF B THEN Ref ⌈λs. B s ∧ P s⌉ ⌈Q⌉ ELSE Ref ⌈λs. ¬ B s ∧ P s⌉ ⌈Q⌉) ≤ Ref ⌈P⌉ ⌈Q⌉"
  using 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'"
  unfolding kat_cond_def times_nd_fun_def plus_nd_fun_def n_op_nd_fun_def
  by (auto simp: kcomp_def less_eq_nd_fun_def p2ndf_def le_fun_def)

lemma R_cond_law: "X ≤ Ref ⌈λs. B s ∧ P s⌉ ⌈Q⌉ ⟹ Y ≤ Ref ⌈λs. ¬ B s ∧ P s⌉ ⌈Q⌉ ⟹ 
  (IF B THEN X ELSE Y) ≤ Ref ⌈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 (Ref ⌈λs. P s ∧ B s⌉ ⌈P⌉) ≤ Ref ⌈P⌉ ⌈K⌉"
  unfolding kat_while_inv_def using R_while[of "⌈B⌉" "⌈P⌉"] by simp

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

lemma R_while_mono: "X ≤ X' ⟹ (WHILE P INV I DO X) ≤ WHILE P INV I DO X'"
  by (simp add: kat_while_inv_def kat_while_def mult_isol mult_isor star_iso)

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

― ‹ Finite Iteration ›

lemma R_loop: "X ≤ Ref ⌈I⌉ ⌈I⌉ ⟹ ⌈P⌉ ≤ ⌈I⌉ ⟹ ⌈I⌉ ≤ ⌈Q⌉ ⟹ LOOP X INV I ≤ Ref ⌈P⌉ ⌈Q⌉"
  unfolding spec_def using H_loopI by blast

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

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

― ‹ Evolution command (flow) ›

lemma R_g_evol: 
  fixes φ :: "('a::preorder) ⇒ 'b ⇒ 'b"
  shows "(EVOL φ G U) ≤ Ref ⌈λs. ∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ P (φ t s)⌉ ⌈P⌉"
  unfolding 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) ≤ Ref ⌈P⌉ ⌈Q⌉"
  unfolding sH_g_evol[symmetric] 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) ; Ref ⌈R⌉ ⌈Q⌉ ≤ Ref ⌈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)) ⟹ 
  Ref ⌈P⌉ ⌈R⌉; (EVOL φ G U) ≤ Ref ⌈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 ; Ref ⌈Q⌉ ⌈Q⌉ ≤ 
  Ref ⌈λ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 "Ref ⌈Q⌉ ⌈λs. ∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ Q (φ t s)⌉; EVOL φ G U ≤ Ref ⌈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) ≤ 
  Ref ⌈λs. s∈S ⟶ (∀t∈U s. (∀τ∈down (U s) t. G (φ τ s)) ⟶ P (φ t s))⌉ ⌈P⌉"
  unfolding spec_def by (rule H_g_ode_subset[OF assms], auto)

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) ≤ Ref ⌈P⌉ ⌈Q⌉"
  unfolding spec_def by (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) ; Ref ⌈R⌉ ⌈Q⌉ ≤ Ref ⌈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 "Ref ⌈P⌉ ⌈R⌉; (x´= (λt. f) & G on U S @ 0) ≤ Ref ⌈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) ≤ 
  Ref ⌈λ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) ≤ Ref ⌈P⌉ ⌈Q⌉"
  unfolding sH_g_ode[symmetric] by (rule 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) ; Ref ⌈R⌉ ⌈Q⌉ ≤ Ref ⌈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)) ⟹ 
  Ref ⌈P⌉ ⌈R⌉; (x´= (λt. f) & G on (λs. T) S @ 0) ≤ Ref ⌈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) ≤ Ref ⌈P⌉ ⌈Q⌉"
  unfolding sH_g_ode_ivl[symmetric] by (rule R2)

end

― ‹ Evolution command (invariants) ›

lemma R_g_ode_inv: "diff_invariant I f T S t⇩₀ G ⟹ ⌈P⌉ ≤ ⌈I⌉ ⟹ ⌈λs. I s ∧ G s⌉ ≤ ⌈Q⌉ ⟹ 
  (x´=f & G on T S @ t⇩₀ DINV I) ≤ Ref ⌈P⌉ ⌈Q⌉"
  unfolding 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 nd_fun" (‹(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 nd_fun" (‹(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⇩₀) ❙{Q❙}"
  using assms unfolding g_orbital_eq ndfun_kat_H ivp_sols_def g_ode_def by auto

lemma diff_cut_rule:
  assumes wp_C:"Hoare ⌈P⌉ (x´= f & G on U S @ t⇩₀) ⌈C⌉"
    and wp_Q:"Hoare ⌈P⌉ (x´= f & (λ s. G s ∧ C s) on U S @ t⇩₀) ⌈Q⌉"
  shows "❙{P❙} (x´= f & G on U S @ t⇩₀) ❙{Q❙}"
proof(subst ndfun_kat_H, simp add: g_orbital_eq p2ndf_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⇩₀ 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⇩₀ 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) ndfun_kat_H, auto simp: g_ode_def)
  hence "X t ∈ g_orbital f (λs. G s ∧ C s) U S t⇩₀ 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) ndfun_kat_H) (auto simp: g_ode_def)
qed

lemma diff_inv_rule:
  assumes "⌈P⌉ ≤ ⌈I⌉" and "diff_invariant I f U S t⇩₀ G" and "⌈I⌉ ≤ ⌈Q⌉"
  shows "❙{P❙} (x´= f & G on U S @ t⇩₀) ❙{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