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
  sporadic_on_e1:
― ‹A sporadic constraint can be ignored in the present and rejected into the future.›
  ‹(Γ, n ⊢ ((K1 sporadic τ on K2) # Ψ) ▹ Φ)
     ↪e  (Γ, n ⊢ Ψ ▹ ((K1 sporadic τ on K2) # Φ))›
| sporadic_on_e2:
― ‹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 ⊢ ((K1 sporadic τ on K2) # Ψ) ▹ Φ)
     ↪e  (((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ)›
| tagrel_e:
― ‹A relation between time scales has to be obeyed at every instant.›
  ‹(Γ, n ⊢ ((time-relation ⌊K1, K2⌋ ∈ R) # Ψ) ▹ Φ)
     ↪e  (((⌊τvar(K1, n), τvar(K2, n)⌋ ∈ R) # Γ), n
              ⊢ Ψ ▹ ((time-relation ⌊K1, K2⌋ ∈ 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 ⊢ ((K1 implies K2) # Ψ) ▹ Φ)
     ↪e  (((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ))›
| implies_e2:
― ‹It can also be handled in the present by making both the master and the slave
    clocks tick.›
  ‹(Γ, n ⊢ ((K1 implies K2) # Ψ) ▹ Φ)
     ↪e  (((K1 ⇑ n) # (K2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ))›
| 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 ⊢ ((K1 implies not K2) # Ψ) ▹ Φ)
     ↪e  (((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ))›
| 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 ⊢ ((K1 implies not K2) # Ψ) ▹ Φ)
     ↪e  (((K1 ⇑ n) # (K2 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ))›
| timedelayed_e1:
― ‹A timed delayed implication can be handled by forbidding a tick on 
    the master clock.›
  ‹(Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ)
     ↪e  (((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ))›
| 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 ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ)
     ↪e  (((K1 ⇑ n) # (K2 @ n ⊕ δτ ⇒ K3) # Γ), n
            ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ))›
| weakly_precedes_e:
― ‹A weak precedence relation has to hold at every instant.›
  ‹(Γ, n ⊢ ((K1 weakly precedes K2) # Ψ) ▹ Φ)
     ↪e  (((⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
            ⊢ Ψ ▹ ((K1 weakly precedes K2) # Φ))›
| strictly_precedes_e:
― ‹A strict precedence relation has to hold at every instant.›
  ‹(Γ, n ⊢ ((K1 strictly precedes K2) # Ψ) ▹ Φ)
     ↪e  (((⌈#≤ K2 n, #< K1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
            ⊢ Ψ ▹ ((K1 strictly precedes K2) # Φ))›
| kills_e1:
― ‹A kill can be handled by forbidding a tick of the triggering clock.›
  ‹(Γ, n ⊢ ((K1 kills K2) # Ψ) ▹ Φ)
     ↪e  (((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 kills K2) # Φ))›
| kills_e2:
― ‹It can also be handled by making the triggering clock tick and by forbidding 
    any further tick of the killed clock.›
  ‹(Γ, n ⊢ ((K1 kills K2) # Ψ) ▹ Φ)
     ↪e  (((K1 ⇑ n) # (K2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K1 kills K2) # Φ))›

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, n1 ⊢ Ψ1 ▹ Φ1)  ↪i  (Γ2, n2 ⊢ Ψ2 ▹ Φ2)
    ⟹ (Γ1, n1 ⊢ Ψ1 ▹ Φ1)  ↪  (Γ2, n2 ⊢ Ψ2 ▹ Φ2)›
| elims_part:
  ‹(Γ1, n1 ⊢ Ψ1 ▹ Φ1)  ↪e  (Γ2, n2 ⊢ Ψ2 ▹ Φ2)
    ⟹ (Γ1, n1 ⊢ Ψ1 ▹ Φ1)  ↪  (Γ2, n2 ⊢ Ψ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]
by (simp add: relpowp_add) 

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› (‹𝒞next _›)
where
  ‹𝒞next 𝒮 ≡ { 𝒮'. 𝒮 ↪ 𝒮' }›

text ‹
  Advancing to the next instant is possible when there are no more constraints 
  on the current instant.
›
lemma Cnext_solve_instant:
  ‹(𝒞next (Γ, n ⊢ [] ▹ Φ)) ⊇ { Γ, Suc n ⊢ Φ ▹ [] }›
by (simp add: operational_semantics_step.simps operational_semantics_intro.instant_i)

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.
›
lemma Cnext_solve_sporadicon:
  ‹(𝒞next (Γ, n ⊢ ((K1 sporadic τ on K2) # Ψ) ▹ Φ))
    ⊇ { Γ, n ⊢ Ψ ▹ ((K1 sporadic τ on K2) # Φ),
        ((K1 ⇑ n) # (K2 ⇓ n @ τ) # Γ), n ⊢ Ψ ▹ Φ }›
by (simp add: operational_semantics_step.simps
              operational_semantics_elim.sporadic_on_e1
              operational_semantics_elim.sporadic_on_e2)

lemma Cnext_solve_tagrel:
  ‹(𝒞next (Γ, n ⊢ ((time-relation ⌊K1, K2⌋ ∈ R) # Ψ) ▹ Φ))
    ⊇ { ((⌊τvar(K1, n), τvar(K2, n)⌋ ∈ R) # Γ),n
          ⊢ Ψ ▹ ((time-relation ⌊K1, K2⌋ ∈ R) # Φ) }›
by (simp add: operational_semantics_step.simps operational_semantics_elim.tagrel_e)

lemma Cnext_solve_implies:
  ‹(𝒞next (Γ, n ⊢ ((K1 implies K2) # Ψ) ▹ Φ))
    ⊇ { ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ),
         ((K1 ⇑ n) # (K2 ⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies K2) # Φ) }›
by (simp add: operational_semantics_step.simps operational_semantics_elim.implies_e1
              operational_semantics_elim.implies_e2)

lemma Cnext_solve_implies_not:
  ‹(𝒞next (Γ, n ⊢ ((K1 implies not K2) # Ψ) ▹ Φ))
    ⊇ { ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ),
        ((K1 ⇑ n) # (K2 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 implies not K2) # Φ) }›
by (simp add: operational_semantics_step.simps
              operational_semantics_elim.implies_not_e1
              operational_semantics_elim.implies_not_e2)

lemma Cnext_solve_timedelayed:
  ‹(𝒞next (Γ, n ⊢ ((K1 time-delayed by δτ on K2 implies K3) # Ψ) ▹ Φ))
    ⊇ { ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ),
        ((K1 ⇑ n) # (K2 @ n ⊕ δτ ⇒ K3) # Γ), n
          ⊢ Ψ ▹ ((K1 time-delayed by δτ on K2 implies K3) # Φ) }›
by (simp add: operational_semantics_step.simps
              operational_semantics_elim.timedelayed_e1
              operational_semantics_elim.timedelayed_e2)

lemma Cnext_solve_weakly_precedes:
  ‹(𝒞next (Γ, n ⊢ ((K1 weakly precedes K2) # Ψ) ▹ Φ))
    ⊇ { ((⌈#≤ K2 n, #≤ K1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
          ⊢ Ψ ▹ ((K1 weakly precedes K2) # Φ) }›
by (simp add: operational_semantics_step.simps
              operational_semantics_elim.weakly_precedes_e)

lemma Cnext_solve_strictly_precedes:
  ‹(𝒞next (Γ, n ⊢ ((K1 strictly precedes K2) # Ψ) ▹ Φ))
    ⊇ { ((⌈#≤ K2 n, #< K1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
          ⊢ Ψ ▹ ((K1 strictly precedes K2) # Φ) }›
by (simp add: operational_semantics_step.simps
              operational_semantics_elim.strictly_precedes_e)

lemma Cnext_solve_kills:
  ‹(𝒞next (Γ, n ⊢ ((K1 kills K2) # Ψ) ▹ Φ))
    ⊇ { ((K1 ¬⇑ n) # Γ), n ⊢ Ψ ▹ ((K1 kills K2) # Φ),
        ((K1 ⇑ n) # (K2 ¬⇑ ≥ n) # Γ), n ⊢ Ψ ▹ ((K1 kills K2) # Φ) }›
by (simp add: operational_semantics_step.simps operational_semantics_elim.kills_e1
              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