SSL Language.thy

section ‹The Static Representation of a Language›

theory Language
  imports Semantics
begin

locale language =
  semantics step final
  for
    step :: "'state ==> 'state ==> bool" and
    final :: "'state ==> bool" +
  fixes
    load :: "'prog ==> 'state ==> bool"

context language begin

text ‹
  language locale represents the concrete program representation (type variable @{typ 'prog}), which can be transformed into a program state (type variable @{typ 'state}) by the @{term load } function.
  set of initial states of the transition system is implicitly defined by the codomain of @{term load}.
 ›


subsection ‹Program behaviour›

definition prog_behaves :: "'prog ==> 'state behaviour ==> bool" (infix ‹⇓› 50) where
  "prog_behaves = load OO state_behaves"

text ‹If both the @{term load} and @{term step} relations are deterministic, then so is the behaviour of a program.›

lemma right_unique_prog_behaves:
  assumes
    right_unique_load: "right_unique load" and
    right_unique_step: "right_unique step"
  shows "right_unique prog_behaves"
  unfolding prog_behaves_def
  using right_unique_state_behaves[OF right_unique_step] right_unique_load
  by (auto intro: right_unique_OO)

end

end