Theory TESL

theory TESL
imports Main
(*chapter‹The Core of the TESL Language: Syntax and Basics›*)
text‹\chapter[Core TESL: Syntax and Basics]{The Core of the TESL Language: Syntax and Basics}›

theory TESL
imports Main

begin

section‹Syntactic Representation›
text‹
  We define here the syntax of TESL specifications.
›

subsection‹Basic elements of a specification›
text‹
  The following items appear in specifications:
  ▪ Clocks, which are identified by a name.
  ▪ An instant on a clock is identified by its index, starting from 0
  ▪ Tag constants are just constants of a type which denotes the metric time space.
›

datatype     clock         = Clk ‹string›
type_synonym instant_index = ‹nat›

datatype      tag_const =  TConst   (the_tag_const : )         (‹τcst)

text‹
  Tag variables are used to refer to the time on a clock at a given instant index.
  Tag expressions are used to build a new tag by adding a constant delay to a tag variable.
›
datatype tag_var =
  TSchematic ‹clock * instant_index› (‹τvar)
datatype  tag_expr      =  (* Const    ‹'τ tag_const›          (‹⦇ _ ⦈›) *)
                              AddDelay ‹tag_var› ‹'τ tag_const› (‹⦇ _ ⊕ _ ⦈›)

subsection‹Operators for the TESL language›
text‹
  The type of atomic TESL constraints, which can be combined to form specifications.
›
datatype  TESL_atomic =
    SporadicOn         ‹clock› ‹'τ tag_const›  ‹clock›  (‹_ sporadic _ on _› 55)
  | TagRelation        ‹clock› ‹clock› ‹('τ tag_const × 'τ tag_const) ⇒ bool› 
                                                      (‹time-relation ⌊_, _⌋ ∈ _› 55)
  | Implies            ‹clock› ‹clock›                  (infixr ‹implies› 55)
  | ImpliesNot         ‹clock› ‹clock›                  (infixr ‹implies not› 55)
  | TimeDelayedBy      ‹clock› ‹'τ tag_const› ‹clock› ‹clock›
                                                      (‹_ time-delayed by _ on _ implies _› 55)
  | RelaxedTimeDelayed ‹clock› ‹'τ tag_const› ‹clock› ‹clock›
                                                      (‹_ time-delayed⨝ by _ on _ implies _› 55)
  | WeaklyPrecedes     ‹clock› ‹clock›                  (infixr ‹weakly precedes› 55)
  | StrictlyPrecedes   ‹clock› ‹clock›                  (infixr ‹strictly precedes› 55)
  | Kills              ‹clock› ‹clock›                  (infixr ‹kills› 55)
― ‹The following constraints are not part of the TESL language,
    they are added only for implementing the operational semantics›
  | SporadicOnTvar     ‹clock› ‹'τ tag_expr›  ‹clock›   (‹_ sporadic♯ _ on _› 55)

text ‹
  Some constraints were introduced for the implementation of the operational semantics.
  They are not allowed in user-level TESL specification and are not public.
›
fun is_public_atom :: ‹'τ TESL_atomic ⇒ bool› where
    ‹is_public_atom (_ sporadic♯ _ on _)                  = False›
  | ‹is_public_atom _                                     = True›

text‹
  A TESL formula is just a list of atomic constraints, with implicit conjunction
  for the semantics.
›
type_synonym  TESL_formula = ‹'τ TESL_atomic list›

fun is_public_spec :: ‹'τ TESL_atomic list ⇒ bool› where
    ‹is_public_spec [] = True›
  | ‹is_public_spec (φ#S) = ((is_public_atom φ) ∧ (is_public_spec S))›

text‹
  We call ∗‹positive atoms› the atomic constraints that create ticks from nothing.
  Only sporadic constraints are positive in the current version of TESL.
›
fun positive_atom :: ‹'τ TESL_atomic ⇒ bool› where
    ‹positive_atom (_ sporadic _ on _) = True›
  | ‹positive_atom (_ sporadic♯ _ on _) = True›
  | ‹positive_atom _                   = False›

text‹
  The @{term ‹NoSporadic›} function removes sporadic constraints from a TESL formula.
›
abbreviation NoSporadic :: ‹'τ TESL_formula ⇒ 'τ TESL_formula›
where 
  ‹NoSporadic f ≡ (List.filter (λfatom. case fatom of
      _ sporadic _ on _ ⇒ False
    | _ ⇒ True) f)›

subsection‹Field Structure of the Metric Time Space›
text‹
  In order to handle tag relations and delays, tags must belong to a field.
  We show here that this is the case when the type parameter of @{typ ‹'τ tag_const›} 
  is itself a field.
›
instantiation tag_const ::(field)field
begin
  fun inverse_tag_const
  where ‹inverse (τcst t) = τcst (inverse t)›

  fun divide_tag_const 
    where ‹divide (τcst t1) (τcst t2) = τcst (divide t1 t2)›

  fun uminus_tag_const
    where ‹uminus (τcst t) = τcst (uminus t)›

fun minus_tag_const
  where ‹minus (τcst t1) (τcst t2) = τcst (minus t1 t2)›

definition ‹one_tag_const ≡ τcst 1›

fun times_tag_const
  where ‹times (τcst t1) (τcst t2) = τcst (times t1 t2)›

definition ‹zero_tag_const ≡ τcst 0›

fun plus_tag_const
  where ‹plus (τcst t1) (τcst t2) = τcst (plus t1 t2)›

instance proof
  text‹Multiplication is associative.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
                               and c::‹'τ::field tag_const›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  moreover obtain v where ‹b = τcst v› using tag_const.exhaust by blast
  moreover obtain w where ‹c = τcst w› using tag_const.exhaust by blast
  ultimately show ‹a * b * c = a * (b * c)›
    by (simp add: TESL.times_tag_const.simps)
next
  text‹Multiplication is commutative.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  moreover obtain v where ‹b = τcst v› using tag_const.exhaust by blast
  ultimately show ‹ a * b = b * a›
    by (simp add: TESL.times_tag_const.simps)
next
  text‹One is neutral for multiplication.›
  fix a::‹'τ::field tag_const›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  thus ‹1 * a = a›
    by (simp add: TESL.times_tag_const.simps one_tag_const_def)
next
  text‹Addition is associative.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
                               and c::‹'τ::field tag_const›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  moreover obtain v where ‹b = τcst v› using tag_const.exhaust by blast
  moreover obtain w where ‹c = τcst w› using tag_const.exhaust by blast
  ultimately show ‹a + b + c = a + (b + c)›
    by (simp add: TESL.plus_tag_const.simps)
next
  text‹Addition is commutative.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  moreover obtain v where ‹b = τcst v› using tag_const.exhaust by blast
  ultimately show ‹a + b = b + a›
    by (simp add: TESL.plus_tag_const.simps)
next
  text‹Zero is neutral for addition.›
  fix a::‹'τ::field tag_const›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  thus ‹0 + a = a›
    by (simp add: TESL.plus_tag_const.simps zero_tag_const_def)
next
  text‹The sum of an element and its opposite is zero.›
  fix a::‹'τ::field tag_const›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  thus ‹-a + a = 0›
    by (simp add: TESL.plus_tag_const.simps
                  TESL.uminus_tag_const.simps
                  zero_tag_const_def)
next
  text‹Subtraction is adding the opposite.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  moreover obtain v where ‹b = τcst v› using tag_const.exhaust by blast
  ultimately show ‹a - b = a + -b›
    by (simp add: TESL.minus_tag_const.simps
                  TESL.plus_tag_const.simps
                  TESL.uminus_tag_const.simps)
next
  text‹Distributive property of multiplication over addition.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
                               and c::‹'τ::field tag_const›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  moreover obtain v where ‹b = τcst v› using tag_const.exhaust by blast
  moreover obtain w where ‹c = τcst w› using tag_const.exhaust by blast
  ultimately show ‹(a + b) * c = a * c + b * c›
    by (simp add: TESL.plus_tag_const.simps
                  TESL.times_tag_const.simps
                  ring_class.ring_distribs(2))
next
  text‹The neutral elements are distinct.›
  show ‹(0::('τ::field tag_const)) ≠ 1›
    by (simp add: one_tag_const_def zero_tag_const_def)
next
  text‹The product of an element and its inverse is 1.›
  fix a::‹'τ::field tag_const› assume h:‹a ≠ 0›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  moreover with h have ‹u ≠ 0› by (simp add: zero_tag_const_def)
  ultimately show ‹inverse a * a = 1›
    by (simp add: TESL.inverse_tag_const.simps
                  TESL.times_tag_const.simps
                  one_tag_const_def)
next
  text‹Dividing is multiplying by the inverse.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
  obtain u where ‹a = τcst u› using tag_const.exhaust by blast
  moreover obtain v where ‹b = τcst v› using tag_const.exhaust by blast
  ultimately show ‹a div b = a * inverse b›
    by (simp add: TESL.divide_tag_const.simps
                  TESL.inverse_tag_const.simps
                  TESL.times_tag_const.simps
                  divide_inverse)
next
  text‹Zero is its own inverse.›
  show ‹inverse (0::('τ::field tag_const)) = 0›
    by (simp add: TESL.inverse_tag_const.simps zero_tag_const_def)
qed

end

text‹
  For comparing dates (which are represented by tags) on clocks, we need an order on tags.
›

instantiation tag_const :: (order)order
begin
  inductive less_eq_tag_const :: ‹'a tag_const ⇒ 'a tag_const ⇒ bool›
  where
    Int_less_eq[simp]:      ‹n ≤ m ⟹ (TConst n) ≤ (TConst m)›

  definition less_tag: ‹(x::'a tag_const) < y ⟷ (x ≤ y) ∧ (x ≠ y)›

  instance proof
    show ‹⋀x y :: 'a tag_const. (x < y) = (x ≤ y ∧ ¬ y ≤ x)›
      using less_eq_tag_const.simps less_tag by auto
  next
    fix x::‹'a tag_const›
    from tag_const.exhaust obtain x0::'a where ‹x = TConst x0 by blast
    with Int_less_eq show ‹x ≤ x› by simp
  next
    show ‹⋀x y z  :: 'a tag_const. x ≤ y ⟹ y ≤ z ⟹ x ≤ z›
      using less_eq_tag_const.simps by auto
  next
    show ‹⋀x y  :: 'a tag_const. x ≤ y ⟹ y ≤ x ⟹ x = y›
      using less_eq_tag_const.simps by auto
  qed

end

text‹
  For ensuring that time does never flow backwards, we need a total order on tags.
›
instantiation tag_const :: (linorder)linorder
begin
  instance proof
    fix x::‹'a tag_const› and y::‹'a tag_const›
    from tag_const.exhaust obtain x0::'a where ‹x = TConst x0 by blast
    moreover from tag_const.exhaust obtain y0::'a where ‹y = TConst y0 by blast
    ultimately show ‹x ≤ y ∨ y ≤ x› using less_eq_tag_const.simps by fastforce
  qed

end

end