# Theory Operational

chapter ‹Operational Semantics›
text‹\label{chap:operational_semantics}›

theory Operational
imports
SymbolicPrimitive

begin

text‹
The operational semantics defines rules to build symbolic runs from a TESL
specification (a set of TESL formulae).
Symbolic runs are described using the symbolic primitives presented in the
previous chapter.
Therefore, the operational semantics compiles a set of constraints on runs,
as defined by the denotational semantics, into a set of symbolic constraints
on the instants of the runs. Concrete runs can then be obtained by solving the
constraints at each instant.
›

section‹Operational steps›

text ‹
We introduce a notation to describe configurations:
▪ @{term ‹Γ›} is the context, the set of symbolic constraints on past instants of the run;
▪ @{term ‹n›} is the index of the current instant, the present;
▪ @{term ‹Ψ›} is the TESL formula that must be satisfied at the current instant (present);
▪ @{term ‹Φ›} is the TESL formula that must be satisfied for the following instants (the future).
›
abbreviation uncurry_conf
::‹('τ::linordered_field) system ⇒ instant_index ⇒ 'τ TESL_formula ⇒ 'τ TESL_formula
⇒ 'τ config›                                                  (‹_, _ ⊢ _ ▹ _› 80)
where
‹Γ, n ⊢ Ψ ▹ Φ ≡ (Γ, n, Ψ, Φ)›

text ‹
The only introduction rule allows us to progress to the next instant
when there are no more constraints to satisfy for the present instant.
›
inductive operational_semantics_intro
::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪⇩i _› 70)
where
instant_i:
‹(Γ, n ⊢ [] ▹ Φ) ↪⇩i  (Γ, Suc n ⊢ Φ ▹ [])›

text ‹
The elimination rules describe how TESL formulae for the present are transformed
into constraints on the past and on the future.
›
inductive operational_semantics_elim
::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪⇩e _› 70)
where
― ‹A sporadic constraint can be ignored in the present and rejected into the future.›
‹(Γ, n ⊢ ((K⇩1 sporadic τ on K⇩2) # Ψ) ▹ Φ)
↪⇩e  (Γ, n ⊢ Ψ ▹ ((K⇩1 sporadic τ on K⇩2) # Φ))›
― ‹It can also be handled in the present by making the clock tick and have
the expected time. Once it has been handled, it is no longer a constraint
to satisfy, so it disappears from the future.›
‹(Γ, n ⊢ ((K⇩1 sporadic τ on K⇩2) # Ψ) ▹ Φ)
↪⇩e  (((K⇩1 ⇑ n) # (K⇩2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ)›
| tagrel_e:
― ‹A relation between time scales has to be obeyed at every instant.›
‹(Γ, n ⊢ ((time-relation ⌊K⇩1, K⇩2⌋ ∈ R) # Ψ) ▹ Φ)
↪⇩e  (((⌊τ⇩v⇩a⇩r(K⇩1, n), τ⇩v⇩a⇩r(K⇩2, n)⌋ ∈ R) # Γ), n
⊢ Ψ ▹ ((time-relation ⌊K⇩1, K⇩2⌋ ∈ R) # Φ))›
| implies_e1:
― ‹An implication can be handled in the present by forbidding a tick of the master
clock. The implication is copied back into the future because it holds for
the whole run.›
‹(Γ, n ⊢ ((K⇩1 implies K⇩2) # Ψ) ▹ Φ)
↪⇩e  (((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ))›
| implies_e2:
― ‹It can also be handled in the present by making both the master and the slave
clocks tick.›
‹(Γ, n ⊢ ((K⇩1 implies K⇩2) # Ψ) ▹ Φ)
↪⇩e  (((K⇩1 ⇑ n) # (K⇩2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ))›
| implies_not_e1:
― ‹A negative implication can be handled in the present by forbidding a tick of
the master clock. The implication is copied back into the future because
it holds for the whole run.›
‹(Γ, n ⊢ ((K⇩1 implies not K⇩2) # Ψ) ▹ Φ)
↪⇩e  (((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ))›
| implies_not_e2:
― ‹It can also be handled in the present by making the master clock ticks and
forbidding a tick on the slave clock.›
‹(Γ, n ⊢ ((K⇩1 implies not K⇩2) # Ψ) ▹ Φ)
↪⇩e  (((K⇩1 ⇑ n) # (K⇩2 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ))›
| timedelayed_e1:
― ‹A timed delayed implication can be handled by forbidding a tick on
the master clock.›
‹(Γ, n ⊢ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Ψ) ▹ Φ)
↪⇩e  (((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ))›
| timedelayed_e2:
― ‹It can also be handled by making the master clock tick and adding a constraint
that makes the slave clock tick when the delay has elapsed on the measuring clock.›
‹(Γ, n ⊢ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Ψ) ▹ Φ)
↪⇩e  (((K⇩1 ⇑ n) # (K⇩2 @ n ⊕ δτ ⇒ K⇩3) # Γ), n
⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ))›
| weakly_precedes_e:
― ‹A weak precedence relation has to hold at every instant.›
‹(Γ, n ⊢ ((K⇩1 weakly precedes K⇩2) # Ψ) ▹ Φ)
↪⇩e  (((⌈#⇧≤ K⇩2 n, #⇧≤ K⇩1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
⊢ Ψ ▹ ((K⇩1 weakly precedes K⇩2) # Φ))›
| strictly_precedes_e:
― ‹A strict precedence relation has to hold at every instant.›
‹(Γ, n ⊢ ((K⇩1 strictly precedes K⇩2) # Ψ) ▹ Φ)
↪⇩e  (((⌈#⇧≤ K⇩2 n, #⇧< K⇩1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
⊢ Ψ ▹ ((K⇩1 strictly precedes K⇩2) # Φ))›
| kills_e1:
― ‹A kill can be handled by forbidding a tick of the triggering clock.›
‹(Γ, n ⊢ ((K⇩1 kills K⇩2) # Ψ) ▹ Φ)
↪⇩e  (((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ))›
| kills_e2:
― ‹It can also be handled by making the triggering clock tick and by forbidding
any further tick of the killed clock.›
‹(Γ, n ⊢ ((K⇩1 kills K⇩2) # Ψ) ▹ Φ)
↪⇩e  (((K⇩1 ⇑ n) # (K⇩2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ))›

text ‹
A step of the operational semantics is either the application of the introduction
rule or the application of an elimination rule.
›
inductive operational_semantics_step
::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪ _› 70)
where
intro_part:
‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1)  ↪⇩i  (Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2)
⟹ (Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1)  ↪  (Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2)›
| elims_part:
‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1)  ↪⇩e  (Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2)
⟹ (Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1)  ↪  (Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2)›

text ‹
We introduce notations for the reflexive transitive closure of the operational
semantic step, its transitive closure and its reflexive closure.
›
abbreviation operational_semantics_step_rtranclp
::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪⇧*⇧* _› 70)
where
‹𝒞⇩1 ↪⇧*⇧* 𝒞⇩2 ≡ operational_semantics_step⇧*⇧* 𝒞⇩1 𝒞⇩2›

abbreviation operational_semantics_step_tranclp
::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪⇧+⇧+ _› 70)
where
‹𝒞⇩1 ↪⇧+⇧+ 𝒞⇩2 ≡ operational_semantics_step⇧+⇧+ 𝒞⇩1 𝒞⇩2›

abbreviation operational_semantics_step_reflclp
::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪⇧=⇧= _› 70)
where
‹𝒞⇩1 ↪⇧=⇧= 𝒞⇩2 ≡ operational_semantics_step⇧=⇧= 𝒞⇩1 𝒞⇩2›

abbreviation operational_semantics_step_relpowp
::‹('τ::linordered_field) config ⇒ nat ⇒ 'τ config ⇒ bool›       (‹_ ↪⇗_⇖ _› 70)
where
‹𝒞⇩1 ↪⇗n⇖ 𝒞⇩2 ≡ (operational_semantics_step ^^ n) 𝒞⇩1 𝒞⇩2›

definition operational_semantics_elim_inv
::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪⇩e⇧← _› 70)
where
‹𝒞⇩1 ↪⇩e⇧← 𝒞⇩2 ≡ 𝒞⇩2 ↪⇩e 𝒞⇩1›

section‹Basic Lemmas›

text ‹
If a configuration can be reached in @{term ‹m›} steps from a configuration that
can be reached in @{term ‹n›} steps from an original configuration, then it can be
reached in @{term ‹n+m›} steps from the original configuration.
›
lemma operational_semantics_trans_generalized:
assumes ‹𝒞⇩1 ↪⇗n⇖ 𝒞⇩2›
assumes ‹𝒞⇩2 ↪⇗m⇖ 𝒞⇩3›
shows ‹𝒞⇩1 ↪⇗n + m⇖ 𝒞⇩3›
using relcompp.relcompI[of  ‹operational_semantics_step ^^ n› _ _
‹operational_semantics_step ^^ m›, OF assms]

text ‹
We consider the set of configurations that can be reached in one operational
step from a given configuration.
›
abbreviation Cnext_solve
::‹('τ::linordered_field) config ⇒ 'τ config set› (‹𝒞⇩n⇩e⇩x⇩t _›)
where
‹𝒞⇩n⇩e⇩x⇩t 𝒮 ≡ { 𝒮'. 𝒮 ↪ 𝒮' }›

text ‹
Advancing to the next instant is possible when there are no more constraints
on the current instant.
›
lemma Cnext_solve_instant:
‹(𝒞⇩n⇩e⇩x⇩t (Γ, n ⊢ [] ▹ Φ)) ⊇ { Γ, Suc n ⊢ Φ ▹ [] }›

text ‹
The following lemmas state that the configurations produced by the elimination
rules of the operational semantics belong to the configurations that can be
reached in one step.
›
‹(𝒞⇩n⇩e⇩x⇩t (Γ, n ⊢ ((K⇩1 sporadic τ on K⇩2) # Ψ) ▹ Φ))
⊇ { Γ, n ⊢ Ψ ▹ ((K⇩1 sporadic τ on K⇩2) # Φ),
((K⇩1 ⇑ n) # (K⇩2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ }›

lemma Cnext_solve_tagrel:
‹(𝒞⇩n⇩e⇩x⇩t (Γ, n ⊢ ((time-relation ⌊K⇩1, K⇩2⌋ ∈ R) # Ψ) ▹ Φ))
⊇ { ((⌊τ⇩v⇩a⇩r(K⇩1, n), τ⇩v⇩a⇩r(K⇩2, n)⌋ ∈ R) # Γ),n
⊢ Ψ ▹ ((time-relation ⌊K⇩1, K⇩2⌋ ∈ R) # Φ) }›

lemma Cnext_solve_implies:
‹(𝒞⇩n⇩e⇩x⇩t (Γ, n ⊢ ((K⇩1 implies K⇩2) # Ψ) ▹ Φ))
⊇ { ((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ),
((K⇩1 ⇑ n) # (K⇩2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies K⇩2) # Φ) }›
operational_semantics_elim.implies_e2)

lemma Cnext_solve_implies_not:
‹(𝒞⇩n⇩e⇩x⇩t (Γ, n ⊢ ((K⇩1 implies not K⇩2) # Ψ) ▹ Φ))
⊇ { ((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ),
((K⇩1 ⇑ n) # (K⇩2 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 implies not K⇩2) # Φ) }›
operational_semantics_elim.implies_not_e1
operational_semantics_elim.implies_not_e2)

lemma Cnext_solve_timedelayed:
‹(𝒞⇩n⇩e⇩x⇩t (Γ, n ⊢ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Ψ) ▹ Φ))
⊇ { ((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ),
((K⇩1 ⇑ n) # (K⇩2 @ n ⊕ δτ ⇒ K⇩3) # Γ), n
⊢ Ψ ▹ ((K⇩1 time-delayed by δτ on K⇩2 implies K⇩3) # Φ) }›
operational_semantics_elim.timedelayed_e1
operational_semantics_elim.timedelayed_e2)

lemma Cnext_solve_weakly_precedes:
‹(𝒞⇩n⇩e⇩x⇩t (Γ, n ⊢ ((K⇩1 weakly precedes K⇩2) # Ψ) ▹ Φ))
⊇ { ((⌈#⇧≤ K⇩2 n, #⇧≤ K⇩1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
⊢ Ψ ▹ ((K⇩1 weakly precedes K⇩2) # Φ) }›
operational_semantics_elim.weakly_precedes_e)

lemma Cnext_solve_strictly_precedes:
‹(𝒞⇩n⇩e⇩x⇩t (Γ, n ⊢ ((K⇩1 strictly precedes K⇩2) # Ψ) ▹ Φ))
⊇ { ((⌈#⇧≤ K⇩2 n, #⇧< K⇩1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
⊢ Ψ ▹ ((K⇩1 strictly precedes K⇩2) # Φ) }›
operational_semantics_elim.strictly_precedes_e)

lemma Cnext_solve_kills:
‹(𝒞⇩n⇩e⇩x⇩t (Γ, n ⊢ ((K⇩1 kills K⇩2) # Ψ) ▹ Φ))
⊇ { ((K⇩1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ),
((K⇩1 ⇑ n) # (K⇩2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K⇩1 kills K⇩2) # Φ) }›
operational_semantics_elim.kills_e2)

text ‹
An empty specification can be reduced to an empty specification for
an arbitrary number of steps.
›
lemma empty_spec_reductions:
‹([], 0 ⊢ [] ▹ []) ↪⇗k⇖ ([], k ⊢ [] ▹ [])›
proof (induct k)
case 0 thus ?case by simp
next
case Suc thus ?case
using instant_i operational_semantics_step.simps by fastforce
qed

end