Theory utp_simple_time

section ‹ Simple UTP real-time theory ›

theory utp_simple_time imports "../utp" begin

text ‹ In this section we give a small example UTP theory, and show how Isabelle/UTP can be
  used to automate production of programming laws. ›

subsection ‹ Observation Space and Signature ›

text ‹ We first declare the observation space for our theory of timed relations. It consists
  of two variables, to denote time and the program state, respectively. ›

alphabet 's st_time = 
  clock :: nat  st :: 's

text ‹ A timed relation is a homogeneous relation over the declared observation space. ›

type_synonym 's time_rel = "'s st_time hrel"

text ‹ We introduce the following operator for adding an $n$-unit delay to a timed relation. ›

definition Wait :: "nat ⇒ 's time_rel" where
[upred_defs]: "Wait(n) = ($clock´ =⇩u $clock + «n» ∧ $st´ =⇩u $st)"

subsection ‹ UTP Theory ›

text ‹ We define a single healthiness condition which ensures that the clock monotonically
  advances, and so forbids reverse time travel. ›

definition HT :: "'s time_rel ⇒ 's time_rel" where
[upred_defs]: "HT(P) = (P ∧ $clock ≤⇩u $clock´)"

text ‹ This healthiness condition is idempotent, monotonic, and also continuous, meaning it
  distributes through arbitary non-empty infima. ›

theorem HT_idem: "HT(HT(P)) = HT(P)" by rel_auto

theorem HT_mono: "P ⊑ Q ⟹ HT(P) ⊑ HT(Q)" by rel_auto

theorem HT_continuous: "Continuous HT" by rel_auto

text ‹ We now create the UTP theory object for timed relations. This is done using a local 
  interpretation @{term "utp_theory_continuous HT"}. This raises the proof obligations
  that @{term HT} is both idempotent and continuous, which we have proved already. 
  The result of this command is a collection of theorems that can be derived from these 
  facts. Notably, we obtain a complete lattice of timed relations via the Knaster-Tarski theorem. 
  We also apply some locale rewrites so that the theorems that are exports have a more intuitive 
  form. ›

interpretation time_theory: utp_theory_continuous HT
  rewrites "P ∈ carrier time_theory.thy_order ⟷ P is HT"
  and "carrier time_theory.thy_order → carrier time_theory.thy_order ≡ ⟦HT⟧⇩H → ⟦HT⟧⇩H"
  and "le time_theory.thy_order = (⊑)"
  and "eq time_theory.thy_order = (=)"  
proof -
  show "utp_theory_continuous HT"
  proof
    show "⋀P. HT (HT P) = HT P"
      by (simp add: HT_idem)
    show "Continuous HT"
      by (simp add: HT_continuous)
  qed
qed (simp_all)

text ‹ The object \textit{time-theory} is a new namespace that contains both definitions and theorems.
  Since the theory forms a complete lattice, we obtain a top element, bottom element, and a
  least fixed-point constructor. We give all of these some intuitive syntax. ›

notation time_theory.utp_top ("⊤⇩t")
notation time_theory.utp_bottom ("⊥⇩t")
notation time_theory.utp_lfp ("μ⇩t")

text ‹ Below is a selection of theorems that have been exported by the locale interpretation. ›

thm time_theory.bottom_healthy
thm time_theory.top_higher
thm time_theory.meet_bottom
thm time_theory.LFP_unfold

subsection ‹ Closure Laws ›

text ‹ @{term HT} applied to @{term Wait} has no affect, since the latter always advances time. ›

lemma HT_Wait: "HT(Wait(n)) = Wait(n)" by (rel_auto)

lemma HT_Wait_closed [closure]: "Wait(n) is HT"
  by (simp add: HT_Wait Healthy_def)

text ‹ Relational identity, @{term II}, is likewise @{term HT}-healthy. ›

lemma HT_skip_closed [closure]: "II is HT"
  by (rel_auto)

text ‹ @{term HT} is closed under sequential composition, which can be shown 
  by transitivity of @{term "(≤)"}. ›

lemma HT_seqr_closed [closure]:
  "⟦ P is HT; Q is HT ⟧ ⟹ P ;; Q is HT"
  by (rel_auto, meson dual_order.trans) ― ‹ Sledgehammer required ›

text ‹ Assignment is also healthy, provided that the clock variable is not assigned. ›

lemma HT_assign_closed [closure]: "⟦ vwb_lens x; clock ⨝ x ⟧ ⟹ x := v is HT"
  by (rel_auto, metis (mono_tags, lifting) eq_iff lens.select_convs(1) lens_indep_get st_time.select_convs(1))

text ‹ An alternative characterisation of the above is that @{term x} is within the state space lens. ›

lemma HT_assign_closed' [closure]: "⟦ vwb_lens x; x ⊆⇩L st ⟧ ⟹ x := v is HT"
  by (rel_auto)

subsection ‹ Algebraic Laws ›

text ‹ Finally, we prove some useful algebraic laws. ›

theorem Wait_skip: "Wait(0) = II" by (rel_auto)
    
theorem Wait_Wait: "Wait(m) ;; Wait(n) = Wait (m + n)" by (rel_auto)

theorem Wait_cond: "Wait(m) ;; (P ◃ b ▹⇩r Q) = (Wait m ;; P) ◃ b⟦&clock+«m»/&clock⟧ ▹⇩r (Wait m ;; Q)"
  by (rel_auto)

end