Theory Denotational

theory Denotational
imports Run
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     (‹t0)
notation dummyDeltaT (‹δt›)
(*>*)

fun TESL_interpretation_atomic
    :: ‹('τ::linordered_field) TESL_atomic ⇒ 'τ run set› (‹⟦ _ ⟧TESL)
where
  ― ‹@{term ‹C1 sporadic τ on C2›} means that @{term ‹C1›} should tick at an 
      instant where the time on @{term ‹C2›} is @{term ‹τ›}.›
    ‹⟦ C1 sporadic τ on C2TESL =
        {ρ. ∃n::nat. ticks ((Rep_run ρ) n C1) ∧ time ((Rep_run ρ) n C2) = τ}›
  ― ‹@{term ‹time-relation ⌊C1, C2⌋ ∈ R›} means that at each instant, the time 
      on @{term ‹C1›} and the time on @{term ‹C2›} are in relation~@{term ‹R›}.›
  | ‹⟦ time-relation ⌊C1, C2⌋ ∈ R ⟧TESL =
        {ρ. ∀n::nat. R (time ((Rep_run ρ) n C1), time ((Rep_run ρ) n C2))}›
  ― ‹@{term ‹master implies slave›} means that at each instant at which 
      @{term ‹master›} ticks, @{term ‹slave›} also ticks.›
  | ‹⟦ master implies slave ⟧TESL =
        {ρ. ∀n::nat. ticks ((Rep_run ρ) n master) ⟶ ticks ((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 ⟧TESL =
        {ρ. ∀n::nat. ticks ((Rep_run ρ) n master) ⟶ ¬ticks ((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 ⟧TESL =
    ― ‹
      When master ticks, let's call @{term ‹t0›} the current date on measuring. Then, 
      at the first instant when the date on measuring is @{term ‹t0+δt›}, 
      slave has to tick.
    ›
        {ρ. ∀n. ticks ((Rep_run ρ) n master) ⟶
                 (let measured_time = time ((Rep_run ρ) n measuring) in
                  ∀m ≥ n.  first_time ρ measuring m (measured_time + δτ)
                            ⟶ ticks ((Rep_run ρ) m slave)
                 )
        }›
  | ‹⟦ master time-delayed⨝ by δτ on measuring implies slave ⟧TESL =
    ― ‹
      When master ticks, let's call @{term ‹t0›} the current date on measuring. Then, 
      slave will be ticking at some instant(s) when the time on measuring is @{term ‹t0+δt›}.
    ›
        { ρ. ∀n. ticks ((Rep_run ρ) n master) ⟶
                 (let measured_time = time ((Rep_run ρ) n measuring) in
                  ∃m ≥ n. ticks ((Rep_run ρ) m slave)
                          ∧ time ((Rep_run ρ) m measuring) = measured_time + δτ
                 )
        }›
  ― ‹@{term ‹C1 weakly precedes C2›} means that each tick on @{term ‹C2›}
        must be preceded by or coincide with at least one tick on @{term ‹C1›}.
        Therefore, at each instant @{term ‹n›}, the number of ticks on @{term ‹C2›} 
        must be less or equal to the number of ticks on @{term ‹C1›}.›
  | ‹⟦ C1 weakly precedes C2TESL =
        {ρ. ∀n::nat. (run_tick_count ρ C2 n) ≤ (run_tick_count ρ C1 n)}›
  ― ‹@{term ‹C1 strictly precedes C2›} means that each tick on @{term ‹C2›}
        must be preceded by at least one tick on @{term ‹C1›} at a previous instant.
        Therefore, at each instant n, the number of ticks on @{term ‹C2›}
        must be less or equal to the number of ticks on @{term ‹C1›} 
        at instant n - 1.›
  | ‹⟦ C1 strictly precedes C2TESL =
        {ρ. ∀n::nat. (run_tick_count ρ C2 n) ≤ (run_tick_count_strictly ρ C1 n)}›
  ― ‹@{term ‹C1 kills C2›} means that when @{term ‹C1›} ticks, @{term ‹C2›}
        cannot tick and is not allowed to tick at any further instant.›
  | ‹⟦ C1 kills C2TESL =
        {ρ. ∀n::nat. ticks ((Rep_run ρ) n C1)
                        ⟶ (∀m≥n. ¬ ticks ((Rep_run ρ) m C2))}›
  ― ‹Additional constraints for the operational semantics›
  ― ‹@{term ‹C1 sporadic♯ ⦇τvar(Cpast, npast) ⊕ δτ⦈ on C2›} means that @{term ‹C1›} should tick at an 
      instant where the time on @{term ‹C2›} is @{term ‹⦇τvar(Cpast, npast) ⊕ δτ⦈›}.›
  | ‹⟦ C1 sporadic♯ ⦇τvar(Cpast, npast) ⊕ δτ⦈ on C2TESL =
        {ρ. ∃n::nat. ticks ((Rep_run ρ) n C1) ∧ time ((Rep_run ρ) n C2) = time ((Rep_run ρ) npast Cpast) + δτ }›

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›
  (‹⟦⟦ _ ⟧⟧TESL)
where
  ‹⟦⟦ [] ⟧⟧TESL = {_. True}›
| ‹⟦⟦ φ # Φ ⟧⟧TESL = ⟦ φ ⟧TESL ∩ ⟦⟦ Φ ⟧⟧TESL

lemma TESL_interpretation_homo:
  ‹⟦ φ ⟧TESL ∩ ⟦⟦ Φ ⟧⟧TESL = ⟦⟦ φ # Φ ⟧⟧TESL
by simp

subsection ‹Image interpretation lemma›

theorem TESL_interpretation_image:
  ‹⟦⟦ Φ ⟧⟧TESL = ⋂ ((λφ. ⟦ φ ⟧TESL) ` set Φ)›
by (induction Φ, simp+)

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

theorem TESL_interp_homo_append:
  ‹⟦⟦ Φ1 @ Φ2 ⟧⟧TESL = ⟦⟦ Φ1 ⟧⟧TESL ∩ ⟦⟦ Φ2 ⟧⟧TESL
by (induction Φ1, simp, auto)

section ‹Equational laws for the denotation of TESL formulae›

lemma TESL_interp_assoc:
  ‹⟦⟦ (Φ1 @ Φ2) @ Φ3 ⟧⟧TESL = ⟦⟦ Φ1 @ (Φ2 @ Φ3) ⟧⟧TESL
by auto

lemma TESL_interp_commute:
  shows ‹⟦⟦ Φ1 @ Φ2 ⟧⟧TESL = ⟦⟦ Φ2 @ Φ1 ⟧⟧TESL
by (simp add: TESL_interp_homo_append inf_sup_aci(1))

lemma TESL_interp_left_commute:
  ‹⟦⟦ Φ1 @ (Φ2 @ Φ3) ⟧⟧TESL = ⟦⟦ Φ2 @ (Φ1 @ Φ3) ⟧⟧TESL
unfolding TESL_interp_homo_append by auto

lemma TESL_interp_idem:
  ‹⟦⟦ Φ @ Φ ⟧⟧TESL = ⟦⟦ Φ ⟧⟧TESL
using TESL_interp_homo_append by auto

lemma TESL_interp_left_idem:
  ‹⟦⟦ Φ1 @ (Φ1 @ Φ2) ⟧⟧TESL = ⟦⟦ Φ1 @ Φ2 ⟧⟧TESL
using TESL_interp_homo_append by auto

lemma TESL_interp_right_idem:
  ‹⟦⟦ (Φ1 @ Φ2) @ Φ2 ⟧⟧TESL = ⟦⟦ Φ1 @ Φ2 ⟧⟧TESL
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:
  ‹⟦⟦ [] @ Φ ⟧⟧TESL = ⟦⟦ Φ ⟧⟧TESL
by simp

lemma TESL_interp_neutral2:
  ‹⟦⟦ Φ @ [] ⟧⟧TESL = ⟦⟦ Φ ⟧⟧TESL
by simp

section ‹Decreasing interpretation of TESL formulae›
text‹
  Adding constraints to a TESL formula reduces the number of satisfying runs.
›
lemma TESL_sem_decreases_head:
  ‹⟦⟦ Φ ⟧⟧TESL ⊇ ⟦⟦ φ # Φ ⟧⟧TESL
by simp

lemma TESL_sem_decreases_tail:
  ‹⟦⟦ Φ ⟧⟧TESL ⊇ ⟦⟦ Φ @ [φ] ⟧⟧TESL
by (simp add: TESL_interp_homo_append)

text ‹
  Repeating a formula in a specification does not change the specification.
›
lemma TESL_interp_formula_stuttering:
  assumes ‹φ ∈ set Φ›
    shows ‹⟦⟦ φ # Φ ⟧⟧TESL = ⟦⟦ Φ ⟧⟧TESL
proof -
  have ‹φ # Φ = [φ] @ Φ› by simp
  hence ‹⟦⟦ φ # Φ ⟧⟧TESL = ⟦⟦ [φ] ⟧⟧TESL ∩ ⟦⟦ Φ ⟧⟧TESL
    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:
  ‹⟦⟦ Φ ⟧⟧TESL = ⟦⟦ remdups Φ ⟧⟧TESL
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 ‹⟦⟦ Φ ⟧⟧TESL = ⟦⟦ Φ' ⟧⟧TESL
proof -     
  have ‹set (remdups Φ) = set (remdups Φ')›
    by (simp add: assms)
  moreover have fxpntΦ: ‹⋂ ((λφ. ⟦ φ ⟧TESL) ` set Φ) = ⟦⟦ Φ ⟧⟧TESL
    by (simp add: TESL_interpretation_image)
  moreover have fxpntΦ': ‹⋂ ((λφ. ⟦ φ ⟧TESL) ` set Φ') = ⟦⟦ Φ' ⟧⟧TESL
    by (simp add: TESL_interpretation_image)
  moreover have ‹⋂ ((λφ. ⟦ φ ⟧TESL) ` set Φ) = ⋂ ((λφ. ⟦ φ ⟧TESL) ` set Φ')›
    by (simp add: assms)
  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 ‹⟦⟦ Φ ⟧⟧TESL ⊇ ⟦⟦ Φ' ⟧⟧TESL
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 ‹⟦⟦ Φ' ⟧⟧TESL = ⟦⟦ Φ @ Φr ⟧⟧TESL
    using TESL_interp_set_lifting decompose by blast
  moreover have ‹⟦⟦ Φ @ Φr ⟧⟧TESL = ⟦⟦ Φ ⟧⟧TESL ∩ ⟦⟦ Φr ⟧⟧TESL
    by (simp add: TESL_interp_homo_append)
  moreover have ‹⟦⟦ Φ ⟧⟧TESL ⊇ ⟦⟦ Φ ⟧⟧TESL ∩ ⟦⟦ Φr ⟧⟧TESL by simp
  ultimately show ?thesis by simp
qed

lemma TESL_interp_decreases_add_head:
  assumes ‹set Φ ⊆ set Φ'›
    shows ‹⟦⟦ φ # Φ ⟧⟧TESL ⊇ ⟦⟦ φ # Φ' ⟧⟧TESL
using assms TESL_interp_decreases_setinc by auto

lemma TESL_interp_decreases_add_tail:
  assumes ‹set Φ ⊆ set Φ'›
    shows ‹⟦⟦ Φ @ [φ] ⟧⟧TESL ⊇ ⟦⟦ Φ' @ [φ] ⟧⟧TESL
using TESL_interp_decreases_setinc[OF assms] 
  by (simp add: TESL_interpretation_image dual_order.trans)

lemma TESL_interp_absorb1:
  assumes ‹set Φ1 ⊆ set Φ2
    shows ‹⟦⟦ Φ1 @ Φ2 ⟧⟧TESL = ⟦⟦ Φ2 ⟧⟧TESL
by (simp add: Int_absorb1 TESL_interp_decreases_setinc
                          TESL_interp_homo_append assms)

lemma TESL_interp_absorb2:
  assumes ‹set Φ2 ⊆ set Φ1
    shows ‹⟦⟦ Φ1 @ Φ2 ⟧⟧TESL = ⟦⟦ Φ1 ⟧⟧TESL
using TESL_interp_absorb1 TESL_interp_commute assms by blast

section ‹Some special cases›

lemma NoSporadic_stable [simp]:
  ‹⟦⟦ Φ ⟧⟧TESL ⊆ ⟦⟦ NoSporadic Φ ⟧⟧TESL
proof -
  from filter_is_subset have ‹set (NoSporadic Φ) ⊆ set Φ› .
  from TESL_interp_decreases_setinc[OF this] show ?thesis .
qed

lemma NoSporadic_idem [simp]:
  ‹⟦⟦ Φ ⟧⟧TESL ∩ ⟦⟦ NoSporadic Φ ⟧⟧TESL = ⟦⟦ Φ ⟧⟧TESL
using NoSporadic_stable by blast

lemma NoSporadic_setinc:
  ‹set (NoSporadic Φ) ⊆ set Φ›
by (rule filter_is_subset)

(*<*)
no_notation dummyT0    (‹t0)
no_notation dummyDeltaT (‹δt›)
(*>*)

end