Theory TESL

(*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.
  ▪ 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 : 'τ)         (‹τ⇩_c⇩_s⇩_t›)


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)
  | WeaklyPrecedes   ‹clock› ‹clock›                  (infixr ‹weakly precedes› 55)
  | StrictlyPrecedes ‹clock› ‹clock›                  (infixr ‹strictly precedes› 55)
  | Kills            ‹clock› ‹clock›                  (infixr ‹kills› 55)

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

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 _                   = False›

text‹
  The @{term ‹NoSporadic›} function removes sporadic constraints from a TESL formula.
›
abbreviation NoSporadic :: ‹'τ TESL_formula ⇒ 'τ TESL_formula›
where 
  ‹NoSporadic f ≡ (List.filter (λf⇩_a⇩_t⇩_o⇩_m. case f⇩_a⇩_t⇩_o⇩_m 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 (τ⇩_c⇩_s⇩_t t) = τ⇩_c⇩_s⇩_t (inverse t)›

  fun divide_tag_const 
    where ‹divide (τ⇩_c⇩_s⇩_t t⇩₁) (τ⇩_c⇩_s⇩_t t⇩₂) = τ⇩_c⇩_s⇩_t (divide t⇩₁ t⇩₂)›

  fun uminus_tag_const
    where ‹uminus (τ⇩_c⇩_s⇩_t t) = τ⇩_c⇩_s⇩_t (uminus t)›

fun minus_tag_const
  where ‹minus (τ⇩_c⇩_s⇩_t t⇩₁) (τ⇩_c⇩_s⇩_t t⇩₂) = τ⇩_c⇩_s⇩_t (minus t⇩₁ t⇩₂)›

definition ‹one_tag_const ≡ τ⇩_c⇩_s⇩_t 1›

fun times_tag_const
  where ‹times (τ⇩_c⇩_s⇩_t t⇩₁) (τ⇩_c⇩_s⇩_t t⇩₂) = τ⇩_c⇩_s⇩_t (times t⇩₁ t⇩₂)›

definition ‹zero_tag_const ≡ τ⇩_c⇩_s⇩_t 0›

fun plus_tag_const
  where ‹plus (τ⇩_c⇩_s⇩_t t⇩₁) (τ⇩_c⇩_s⇩_t t⇩₂) = τ⇩_c⇩_s⇩_t (plus t⇩₁ t⇩₂)›

instance proof
  text‹Multiplication is associative.›
  fix a::‹'τ::field tag_const› and b::‹'τ::field tag_const›
                               and c::‹'τ::field tag_const›
  obtain u v w where ‹a = τ⇩_c⇩_s⇩_t u› and ‹b = τ⇩_c⇩_s⇩_t v› and ‹c = τ⇩_c⇩_s⇩_t w›
    using tag_const.exhaust by metis
  thus ‹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 v where ‹a = τ⇩_c⇩_s⇩_t u› and ‹b = τ⇩_c⇩_s⇩_t v› using tag_const.exhaust by metis
  thus ‹ 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 = τ⇩_c⇩_s⇩_t 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 v w where ‹a = τ⇩_c⇩_s⇩_t u› and ‹b = τ⇩_c⇩_s⇩_t v› and ‹c = τ⇩_c⇩_s⇩_t w›
    using tag_const.exhaust by metis
  thus ‹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 v where ‹a = τ⇩_c⇩_s⇩_t u› and ‹b = τ⇩_c⇩_s⇩_t v› using tag_const.exhaust by metis
  thus ‹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 = τ⇩_c⇩_s⇩_t 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 = τ⇩_c⇩_s⇩_t 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 v where ‹a = τ⇩_c⇩_s⇩_t u› and ‹b = τ⇩_c⇩_s⇩_t v› using tag_const.exhaust by metis
  thus ‹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 v w where ‹a = τ⇩_c⇩_s⇩_t u› and ‹b = τ⇩_c⇩_s⇩_t v› and ‹c = τ⇩_c⇩_s⇩_t w›
    using tag_const.exhaust by metis
  thus ‹(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 = τ⇩_c⇩_s⇩_t 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 v where ‹a = τ⇩_c⇩_s⇩_t u› and ‹b = τ⇩_c⇩_s⇩_t v› using tag_const.exhaust by metis
  thus ‹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 x⇩₀::'a where ‹x = TConst x⇩₀› 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 x⇩₀::'a where ‹x = TConst x⇩₀› by blast
    moreover from tag_const.exhaust obtain y⇩₀::'a where ‹y = TConst y⇩₀› by blast
    ultimately show ‹x ≤ y ∨ y ≤ x› using less_eq_tag_const.simps by fastforce
  qed

end

end