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 : 'τ) (‹τ⇩c⇩s⇩t›)
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› (‹τ⇩v⇩a⇩r›)
datatype 'τ tag_expr =
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)
| 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 (λ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⇩1) (τ⇩c⇩s⇩t t⇩2) = τ⇩c⇩s⇩t (divide t⇩1 t⇩2)›
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⇩1) (τ⇩c⇩s⇩t t⇩2) = τ⇩c⇩s⇩t (minus t⇩1 t⇩2)›
definition ‹one_tag_const ≡ τ⇩c⇩s⇩t 1›
fun times_tag_const
where ‹times (τ⇩c⇩s⇩t t⇩1) (τ⇩c⇩s⇩t t⇩2) = τ⇩c⇩s⇩t (times t⇩1 t⇩2)›
definition ‹zero_tag_const ≡ τ⇩c⇩s⇩t 0›
fun plus_tag_const
where ‹plus (τ⇩c⇩s⇩t t⇩1) (τ⇩c⇩s⇩t t⇩2) = τ⇩c⇩s⇩t (plus t⇩1 t⇩2)›
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 = τ⇩c⇩s⇩t u› using tag_const.exhaust by blast
moreover obtain v where ‹b = τ⇩c⇩s⇩t v› using tag_const.exhaust by blast
moreover obtain w where ‹c = τ⇩c⇩s⇩t 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 = τ⇩c⇩s⇩t u› using tag_const.exhaust by blast
moreover obtain v where ‹b = τ⇩c⇩s⇩t 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 = τ⇩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 where ‹a = τ⇩c⇩s⇩t u› using tag_const.exhaust by blast
moreover obtain v where ‹b = τ⇩c⇩s⇩t v› using tag_const.exhaust by blast
moreover obtain w where ‹c = τ⇩c⇩s⇩t 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 = τ⇩c⇩s⇩t u› using tag_const.exhaust by blast
moreover obtain v where ‹b = τ⇩c⇩s⇩t 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 = τ⇩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 where ‹a = τ⇩c⇩s⇩t u› using tag_const.exhaust by blast
moreover obtain v where ‹b = τ⇩c⇩s⇩t 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 = τ⇩c⇩s⇩t u› using tag_const.exhaust by blast
moreover obtain v where ‹b = τ⇩c⇩s⇩t v› using tag_const.exhaust by blast
moreover obtain w where ‹c = τ⇩c⇩s⇩t 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 = τ⇩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 where ‹a = τ⇩c⇩s⇩t u› using tag_const.exhaust by blast
moreover obtain v where ‹b = τ⇩c⇩s⇩t 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 x⇩0::'a where ‹x = TConst x⇩0› 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⇩0::'a where ‹x = TConst x⇩0› by blast
moreover from tag_const.exhaust obtain y⇩0::'a where ‹y = TConst y⇩0› by blast
ultimately show ‹x ≤ y ∨ y ≤ x› using less_eq_tag_const.simps by fastforce
qed
end
end