Quelle  TESL.thy

(*chapter\<open>The Core of the TESL Language: Syntax and Basics\<close>*)
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 : 'τ)         (‹τ_cst›)


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_atom. case f_atom 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 t₁) (τ_cst t₂) = τ_cst (divide t₁ t₂)›

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

fun minus_tag_const
  where ‹minus (τ_cst t₁) (τ_cst t₂) = τ_cst (minus t₁ t₂)›

definition ‹one_tag_const ≡ τ_cst 1›

fun times_tag_const
  where ‹times (τ_cst t₁) (τ_cst t₂) = τ_cst (times t₁ t₂)›

definition ‹zero_tag_const ≡ τ_cst 0›

fun plus_tag_const
  where ‹plus (τ_cst t₁) (τ_cst t₂) = τ_cst (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 = τ_cst u› and ‹b = τ_cst v› and ‹c = τ_cst 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 = τ_cst u› and ‹b = τ_cst 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 = τ_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 v w where ‹a = τ_cst u› and ‹b = τ_cst v› and ‹c = τ_cst 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 = τ_cst u› and ‹b = τ_cst 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 = τ_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 v where ‹a = τ_cst u› and ‹b = τ_cst 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 = τ_cst u› and ‹b = τ_cst v› and ‹c = τ_cst 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 = τ_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 v where ‹a = τ_cst u› and ‹b = τ_cst 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