# Theory Denotational

```chapter ‹Denotational Semantics›

theory Denotational
imports
TESL
Run

begin
text‹
The denotational semantics maps TESL formulae to sets of satisfying runs.
Firstly, we define the semantics of atomic formulae (basic constructs of the
TESL language), then we define the semantics of compound formulae as the
intersection of the semantics of their components: a run must satisfy all
the individual formulae of a compound formula.
›
section ‹Denotational interpretation for atomic TESL formulae›
(*<*)
consts dummyT0 ::‹'τ tag_const›
consts dummyDeltaT ::‹'τ tag_const›

notation dummyT0     (‹t⇩0›)
notation dummyDeltaT (‹δt›)
(*>*)

fun TESL_interpretation_atomic
:: ‹('τ::linordered_field) TESL_atomic ⇒ 'τ run set› (‹⟦ _ ⟧⇩T⇩E⇩S⇩L›)
where
― ‹@{term ‹K⇩1 sporadic τ on K⇩2›} means that @{term ‹K⇩1›} should tick at an
instant where the time on @{term ‹K⇩2›} is @{term ‹τ›}.›
‹⟦ K⇩1 sporadic τ on K⇩2 ⟧⇩T⇩E⇩S⇩L =
{ρ. ∃n::nat. hamlet ((Rep_run ρ) n K⇩1) ∧ time ((Rep_run ρ) n K⇩2) = τ}›
― ‹@{term ‹time-relation ⌊K⇩1, K⇩2⌋ ∈ R›} means that at each instant, the time
on @{term ‹K⇩1›} and the time on @{term ‹K⇩2›} are in relation~@{term ‹R›}.›
| ‹⟦ time-relation ⌊K⇩1, K⇩2⌋ ∈ R ⟧⇩T⇩E⇩S⇩L =
{ρ. ∀n::nat. R (time ((Rep_run ρ) n K⇩1), time ((Rep_run ρ) n K⇩2))}›
― ‹@{term ‹master implies slave›} means that at each instant at which
@{term ‹master›} ticks, @{term ‹slave›} also ticks.›
| ‹⟦ master implies slave ⟧⇩T⇩E⇩S⇩L =
{ρ. ∀n::nat. hamlet ((Rep_run ρ) n master) ⟶ hamlet ((Rep_run ρ) n slave)}›
― ‹@{term ‹master implies not slave›} means that at each instant at which
@{term ‹master›} ticks, @{term ‹slave›} does not tick.›
| ‹⟦ master implies not slave ⟧⇩T⇩E⇩S⇩L =
{ρ. ∀n::nat. hamlet ((Rep_run ρ) n master) ⟶ ¬hamlet ((Rep_run ρ) n slave)}›
― ‹@{term ‹master time-delayed by δτ on measuring implies slave›} means that
at each instant at which  @{term ‹master›} ticks, @{term ‹slave›} will
tick after a delay @{term ‹δτ›} measured on the time scale
of @{term ‹measuring›}.›
| ‹⟦ master time-delayed by δτ on measuring implies slave ⟧⇩T⇩E⇩S⇩L =
― ‹
When master ticks, let's call @{term ‹t⇩0›} the current date on measuring. Then,
at the first instant when the date on measuring is @{term ‹t⇩0+δt›},
slave has to tick.
›
{ρ. ∀n. hamlet ((Rep_run ρ) n master) ⟶
(let measured_time = time ((Rep_run ρ) n measuring) in
∀m ≥ n.  first_time ρ measuring m (measured_time + δτ)
⟶ hamlet ((Rep_run ρ) m slave)
)
}›
― ‹@{term ‹K⇩1 weakly precedes K⇩2›} means that each tick on @{term ‹K⇩2›}
must be preceded by or coincide with at least one tick on @{term ‹K⇩1›}.
Therefore, at each instant @{term ‹n›}, the number of ticks on @{term ‹K⇩2›}
must be less or equal to the number of ticks on @{term ‹K⇩1›}.›
| ‹⟦ K⇩1 weakly precedes K⇩2 ⟧⇩T⇩E⇩S⇩L =
{ρ. ∀n::nat. (run_tick_count ρ K⇩2 n) ≤ (run_tick_count ρ K⇩1 n)}›
― ‹@{term ‹K⇩1 strictly precedes K⇩2›} means that each tick on @{term ‹K⇩2›}
must be preceded by at least one tick on @{term ‹K⇩1›} at a previous instant.
Therefore, at each instant n, the number of ticks on @{term ‹K⇩2›}
must be less or equal to the number of ticks on @{term ‹K⇩1›}
at instant n - 1.›
| ‹⟦ K⇩1 strictly precedes K⇩2 ⟧⇩T⇩E⇩S⇩L =
{ρ. ∀n::nat. (run_tick_count ρ K⇩2 n) ≤ (run_tick_count_strictly ρ K⇩1 n)}›
― ‹@{term ‹K⇩1 kills K⇩2›} means that when @{term ‹K⇩1›} ticks, @{term ‹K⇩2›}
cannot tick and is not allowed to tick at any further instant.›
| ‹⟦ K⇩1 kills K⇩2 ⟧⇩T⇩E⇩S⇩L =
{ρ. ∀n::nat. hamlet ((Rep_run ρ) n K⇩1)
⟶ (∀m≥n. ¬ hamlet ((Rep_run ρ) m K⇩2))}›

section ‹Denotational interpretation for TESL formulae›

text‹
To satisfy a formula, a run has to satisfy the conjunction of its atomic
formulae. Therefore, the interpretation of a formula is the intersection
of the interpretations of its components.
›
fun TESL_interpretation :: ‹('τ::linordered_field) TESL_formula ⇒ 'τ run set›
(‹⟦⟦ _ ⟧⟧⇩T⇩E⇩S⇩L›)
where
‹⟦⟦ [] ⟧⟧⇩T⇩E⇩S⇩L = {_. True}›
| ‹⟦⟦ φ # Φ ⟧⟧⇩T⇩E⇩S⇩L = ⟦ φ ⟧⇩T⇩E⇩S⇩L ∩ ⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L›

lemma TESL_interpretation_homo:
‹⟦ φ ⟧⇩T⇩E⇩S⇩L ∩ ⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ φ # Φ ⟧⟧⇩T⇩E⇩S⇩L›
by simp

subsection ‹Image interpretation lemma›

theorem TESL_interpretation_image:
‹⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L = ⋂ ((λφ. ⟦ φ ⟧⇩T⇩E⇩S⇩L) ` set Φ)›
by (induction Φ, simp+)

subsection ‹Expansion law›
text ‹Similar to the expansion laws of lattices.›

theorem TESL_interp_homo_append:
‹⟦⟦ Φ⇩1 @ Φ⇩2 ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ⇩1 ⟧⟧⇩T⇩E⇩S⇩L ∩ ⟦⟦ Φ⇩2 ⟧⟧⇩T⇩E⇩S⇩L›
by (induction Φ⇩1, simp, auto)

section ‹Equational laws for the denotation of TESL formulae›

lemma TESL_interp_assoc:
‹⟦⟦ (Φ⇩1 @ Φ⇩2) @ Φ⇩3 ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ⇩1 @ (Φ⇩2 @ Φ⇩3) ⟧⟧⇩T⇩E⇩S⇩L›
by auto

lemma TESL_interp_commute:
shows ‹⟦⟦ Φ⇩1 @ Φ⇩2 ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ⇩2 @ Φ⇩1 ⟧⟧⇩T⇩E⇩S⇩L›

lemma TESL_interp_left_commute:
‹⟦⟦ Φ⇩1 @ (Φ⇩2 @ Φ⇩3) ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ⇩2 @ (Φ⇩1 @ Φ⇩3) ⟧⟧⇩T⇩E⇩S⇩L›
unfolding TESL_interp_homo_append by auto

lemma TESL_interp_idem:
‹⟦⟦ Φ @ Φ ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L›
using TESL_interp_homo_append by auto

lemma TESL_interp_left_idem:
‹⟦⟦ Φ⇩1 @ (Φ⇩1 @ Φ⇩2) ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ⇩1 @ Φ⇩2 ⟧⟧⇩T⇩E⇩S⇩L›
using TESL_interp_homo_append by auto

lemma TESL_interp_right_idem:
‹⟦⟦ (Φ⇩1 @ Φ⇩2) @ Φ⇩2 ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ⇩1 @ Φ⇩2 ⟧⟧⇩T⇩E⇩S⇩L›
unfolding TESL_interp_homo_append by auto

lemmas TESL_interp_aci = TESL_interp_commute
TESL_interp_assoc
TESL_interp_left_commute
TESL_interp_left_idem

text ‹The empty formula is the identity element.›
lemma TESL_interp_neutral1:
‹⟦⟦ [] @ Φ ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L›
by simp

lemma TESL_interp_neutral2:
‹⟦⟦ Φ @ [] ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L›
by simp

section ‹Decreasing interpretation of TESL formulae›
text‹
Adding constraints to a TESL formula reduces the number of satisfying runs.
›
‹⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L ⊇ ⟦⟦ φ # Φ ⟧⟧⇩T⇩E⇩S⇩L›
by simp

lemma TESL_sem_decreases_tail:
‹⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L ⊇ ⟦⟦ Φ @ [φ] ⟧⟧⇩T⇩E⇩S⇩L›

text ‹
Repeating a formula in a specification does not change the specification.
›
lemma TESL_interp_formula_stuttering:
assumes ‹φ ∈ set Φ›
shows ‹⟦⟦ φ # Φ ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L›
proof -
have ‹φ # Φ = [φ] @ Φ› by simp
hence ‹⟦⟦ φ # Φ ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ [φ] ⟧⟧⇩T⇩E⇩S⇩L ∩ ⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L›
using TESL_interp_homo_append by simp
thus ?thesis using assms TESL_interpretation_image by fastforce
qed

text ‹
Removing duplicate formulae in a specification does not change the specification.
›
lemma TESL_interp_remdups_absorb:
‹⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ remdups Φ ⟧⟧⇩T⇩E⇩S⇩L›
proof (induction Φ)
case Cons
thus ?case using TESL_interp_formula_stuttering by auto
qed simp

text ‹
Specifications that contain the same formulae have the same semantics.
›
lemma TESL_interp_set_lifting:
assumes ‹set Φ = set Φ'›
shows ‹⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ' ⟧⟧⇩T⇩E⇩S⇩L›
proof -
have ‹set (remdups Φ) = set (remdups Φ')›
moreover have fxpntΦ: ‹⋂ ((λφ. ⟦ φ ⟧⇩T⇩E⇩S⇩L) ` set Φ) = ⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L›
moreover have fxpntΦ': ‹⋂ ((λφ. ⟦ φ ⟧⇩T⇩E⇩S⇩L) ` set Φ') = ⟦⟦ Φ' ⟧⟧⇩T⇩E⇩S⇩L›
moreover have ‹⋂ ((λφ. ⟦ φ ⟧⇩T⇩E⇩S⇩L) ` set Φ) = ⋂ ((λφ. ⟦ φ ⟧⇩T⇩E⇩S⇩L) ` set Φ')›
ultimately show ?thesis using TESL_interp_remdups_absorb by auto
qed

text ‹
The semantics of specifications is contravariant with respect to their inclusion.
›
theorem TESL_interp_decreases_setinc:
assumes ‹set Φ ⊆ set Φ'›
shows ‹⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L ⊇ ⟦⟦ Φ' ⟧⟧⇩T⇩E⇩S⇩L›
proof -
obtain Φ⇩r where decompose: ‹set (Φ @ Φ⇩r) = set Φ'› using assms by auto
hence ‹set (Φ @ Φ⇩r) = set Φ'› using assms by blast
moreover have ‹(set Φ) ∪ (set Φ⇩r) = set Φ'›
using assms decompose by auto
moreover have ‹⟦⟦ Φ' ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ @ Φ⇩r ⟧⟧⇩T⇩E⇩S⇩L›
using TESL_interp_set_lifting decompose by blast
moreover have ‹⟦⟦ Φ @ Φ⇩r ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L ∩ ⟦⟦ Φ⇩r ⟧⟧⇩T⇩E⇩S⇩L›
moreover have ‹⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L ⊇ ⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L ∩ ⟦⟦ Φ⇩r ⟧⟧⇩T⇩E⇩S⇩L› by simp
ultimately show ?thesis by simp
qed

assumes ‹set Φ ⊆ set Φ'›
shows ‹⟦⟦ φ # Φ ⟧⟧⇩T⇩E⇩S⇩L ⊇ ⟦⟦ φ # Φ' ⟧⟧⇩T⇩E⇩S⇩L›
using assms TESL_interp_decreases_setinc by auto

assumes ‹set Φ ⊆ set Φ'›
shows ‹⟦⟦ Φ @ [φ] ⟧⟧⇩T⇩E⇩S⇩L ⊇ ⟦⟦ Φ' @ [φ] ⟧⟧⇩T⇩E⇩S⇩L›
using TESL_interp_decreases_setinc[OF assms]

lemma TESL_interp_absorb1:
assumes ‹set Φ⇩1 ⊆ set Φ⇩2›
shows ‹⟦⟦ Φ⇩1 @ Φ⇩2 ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ⇩2 ⟧⟧⇩T⇩E⇩S⇩L›
TESL_interp_homo_append assms)

lemma TESL_interp_absorb2:
assumes ‹set Φ⇩2 ⊆ set Φ⇩1›
shows ‹⟦⟦ Φ⇩1 @ Φ⇩2 ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ⇩1 ⟧⟧⇩T⇩E⇩S⇩L›
using TESL_interp_absorb1 TESL_interp_commute assms by blast

section ‹Some special cases›

‹⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L ⊆ ⟦⟦ NoSporadic Φ ⟧⟧⇩T⇩E⇩S⇩L›
proof -
from filter_is_subset have ‹set (NoSporadic Φ) ⊆ set Φ› .
from TESL_interp_decreases_setinc[OF this] show ?thesis .
qed

‹⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L ∩ ⟦⟦ NoSporadic Φ ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L›