Theory Operational

theory Operational
imports SymbolicPrimitive
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 ⊨ ((C1 sporadic τ on C2) # Ψ) ▹ Φ)
     ↪e  (Γ, n ⊨ Ψ ▹ ((C1 sporadic τ on C2) # Φ))›
| 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 ⊨ ((C1 sporadic τ on C2) # Ψ) ▹ Φ)
     ↪e  (((C1 ⇑ n) # (C2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ)›
| sporadic_on_tvar_e1:
  ‹(Γ, n ⊨ ((C1 sporadic♯ τexpr on C2) # Ψ) ▹ Φ)
     ↪e  (Γ, n ⊨ Ψ ▹ ((C1 sporadic♯ τexpr on C2) # Φ))›
| sporadic_on_tvar_e2:
  ‹(Γ, n ⊨ ((C1 sporadic♯ τexpr on C2) # Ψ) ▹ Φ)
     ↪e  (((C1 ⇑ n) # (C2 ⇓ n @♯ τexpr) # Γ), n ⊨ Ψ ▹ Φ)›
| tagrel_e:
― ‹A relation between time scales has to be obeyed at every instant.›
  ‹(Γ, n ⊨ ((time-relation ⌊C1, C2⌋ ∈ R) # Ψ) ▹ Φ)
     ↪e  (((⌊τvar(C1, n), τvar(C2, n)⌋ ∈ R) # Γ), n
              ⊨ Ψ ▹ ((time-relation ⌊C1, C2⌋ ∈ 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 ⊨ ((C1 implies C2) # Ψ) ▹ Φ)
     ↪e  (((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ))›
| implies_e2:
― ‹It can also be handled in the present by making both the master and the slave
    clocks tick.›
  ‹(Γ, n ⊨ ((C1 implies C2) # Ψ) ▹ Φ)
     ↪e  (((C1 ⇑ n) # (C2 ⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies C2) # Φ))›
| 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 ⊨ ((C1 implies not C2) # Ψ) ▹ Φ)
     ↪e  (((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ))›
| 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 ⊨ ((C1 implies not C2) # Ψ) ▹ Φ)
     ↪e  (((C1 ⇑ n) # (C2 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ))›
| timedelayed_e1:
― ‹A timed delayed implication can be handled by forbidding a tick on 
    the master clock.›
  ‹(Γ, n ⊨ ((C1 time-delayed by δτ on C2 implies C3) # Ψ) ▹ Φ)
     ↪e  (((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ))›
| 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 ⊨ ((C1 time-delayed by δτ on C2 implies C3) # Ψ) ▹ Φ)
     ↪e  (((C1 ⇑ n) # (C2 @ n ⊕ δτ ⇒ C3) # Γ), n
            ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ))›
| timedelayed_tvar_e1:
  ‹(Γ, n ⊨ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ) ▹ Φ)
     ↪e  (((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))›
| timedelayed_tvar_e2:
  ‹(Γ, n ⊨ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ) ▹ Φ)
     ↪e  (((C1 ⇑ n) # Γ), n ⊨ ((C3 sporadic♯ ⦇τvar(C2, n) ⊕ δτ⦈ on C2) # Ψ)
                             ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ))›
| weakly_precedes_e:
― ‹A weak precedence relation has to hold at every instant.›
  ‹(Γ, n ⊨ ((C1 weakly precedes C2) # Ψ) ▹ Φ)
     ↪e  (((⌈# C2 n, # C1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
            ⊨ Ψ ▹ ((C1 weakly precedes C2) # Φ))›
| strictly_precedes_e:
― ‹A strict precedence relation has to hold at every instant.›
  ‹(Γ, n ⊨ ((C1 strictly precedes C2) # Ψ) ▹ Φ)
     ↪e  (((⌈# C2 n, #< C1 n⌉ ∈ (λ(x,y). x≤y)) # Γ), n
            ⊨ Ψ ▹ ((C1 strictly precedes C2) # Φ))›
| kills_e1:
― ‹A kill can be handled by forbidding a tick of the triggering clock.›
  ‹(Γ, n ⊨ ((C1 kills C2) # Ψ) ▹ Φ)
     ↪e  (((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ))›
| kills_e2:
― ‹It can also be handled by making the triggering clock tick and by forbidding 
    any further tick of the killed clock.›
  ‹(Γ, n ⊨ ((C1 kills C2) # Ψ) ▹ Φ)
     ↪e  (((C1 ⇑ n) # (C2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ))›

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)  ↪i2, n2 ⊨ Ψ2 ▹ Φ2)
    ⟹ (Γ1, n1 ⊨ Ψ1 ▹ Φ1)  ↪  (Γ2, n2 ⊨ Ψ2 ▹ Φ2)›
| elims_part:
  ‹(Γ1, n1 ⊨ Ψ1 ▹ Φ1)  ↪e2, 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
  ‹𝒞1n 𝒞2 ≡ (operational_semantics_step ^^ n) 𝒞1 𝒞2

definition operational_semantics_elim_inv
  ::‹('τ::linordered_field) config ⇒ 'τ config ⇒ bool›              (‹_ ↪e _› 70)
where
  ‹𝒞1e 𝒞2 ≡ 𝒞2e 𝒞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 ‹𝒞1n 𝒞2
  assumes ‹𝒞2m 𝒞3
    shows ‹𝒞1n + 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 ⊨ ((C1 sporadic τ on C2) # Ψ) ▹ Φ))
    ⊇ { Γ, n ⊨ Ψ ▹ ((C1 sporadic τ on C2) # Φ),
        ((C1 ⇑ n) # (C2 ⇓ n @ τ) # Γ), n ⊨ Ψ ▹ Φ }›
by (simp add: operational_semantics_step.simps
              operational_semantics_elim.sporadic_on_e1
              operational_semantics_elim.sporadic_on_e2)

lemma Cnext_solve_sporadicon_tvar:
  ‹(𝒞next (Γ, n ⊨ ((C1 sporadic♯ τexpr on C2) # Ψ) ▹ Φ))
    ⊇ { Γ, n ⊨ Ψ ▹ ((C1 sporadic♯ τexpr on C2) # Φ),
        ((C1 ⇑ n) # (C2 ⇓ n @♯ τexpr) # Γ), n ⊨ Ψ ▹ Φ }›
by (simp add: operational_semantics_step.simps
              operational_semantics_elim.sporadic_on_tvar_e1
              operational_semantics_elim.sporadic_on_tvar_e2)

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

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

lemma Cnext_solve_implies_not:
  ‹(𝒞next (Γ, n ⊨ ((C1 implies not C2) # Ψ) ▹ Φ))
    ⊇ { ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ),
        ((C1 ⇑ n) # (C2 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 implies not C2) # Φ) }›
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 ⊨ ((C1 time-delayed by δτ on C2 implies C3) # Ψ) ▹ Φ))
    ⊇ { ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ),
        ((C1 ⇑ n) # (C2 @ n ⊕ δτ ⇒ C3) # Γ), n
          ⊨ Ψ ▹ ((C1 time-delayed by δτ on C2 implies C3) # Φ) }›
by (simp add: operational_semantics_step.simps
              operational_semantics_elim.timedelayed_e1
              operational_semantics_elim.timedelayed_e2)

lemma Cnext_solve_timedelayed_tvar:
  ‹(𝒞next (Γ, n ⊨ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Ψ) ▹ Φ))
    ⊇ { ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ),
        ((C1 ⇑ n) # Γ), n
          ⊨ (C3 sporadic♯ ⦇τvar(C2, n) ⊕ δτ⦈ on C2) # Ψ
          ▹ ((C1 time-delayed⨝ by δτ on C2 implies C3) # Φ) }›
by (simp add: operational_semantics_step.simps
              operational_semantics_elim.timedelayed_tvar_e1
              operational_semantics_elim.timedelayed_tvar_e2)

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

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

lemma Cnext_solve_kills:
  ‹(𝒞next (Γ, n ⊨ ((C1 kills C2) # Ψ) ▹ Φ))
    ⊇ { ((C1 ¬⇑ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ),
        ((C1 ⇑ n) # (C2 ¬⇑ ≥ n) # Γ), n ⊨ Ψ ▹ ((C1 kills C2) # Φ) }›
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