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›
by (simp add: TESL_interp_homo_append inf_sup_aci(1))

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.
›
lemma TESL_sem_decreases_head:
  ‹⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L ⊇ ⟦⟦ φ # Φ ⟧⟧⇩T⇩E⇩S⇩L›
by simp

lemma TESL_sem_decreases_tail:
  ‹⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L ⊇ ⟦⟦ Φ @ [φ] ⟧⟧⇩T⇩E⇩S⇩L›
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 ‹⟦⟦ φ # Φ ⟧⟧⇩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 Φ')›
    by (simp add: assms)
  moreover have fxpntΦ: ‹⋂ ((λφ. ⟦ φ ⟧⇩T⇩E⇩S⇩L) ` set Φ) = ⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L›
    by (simp add: TESL_interpretation_image)
  moreover have fxpntΦ': ‹⋂ ((λφ. ⟦ φ ⟧⇩T⇩E⇩S⇩L) ` set Φ') = ⟦⟦ Φ' ⟧⟧⇩T⇩E⇩S⇩L›
    by (simp add: TESL_interpretation_image)
  moreover have ‹⋂ ((λφ. ⟦ φ ⟧⇩T⇩E⇩S⇩L) ` set Φ) = ⋂ ((λφ. ⟦ φ ⟧⇩T⇩E⇩S⇩L) ` 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 ‹⟦⟦ Φ ⟧⟧⇩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›
    by (simp add: TESL_interp_homo_append)
  moreover have ‹⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L ⊇ ⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L ∩ ⟦⟦ Φ⇩r ⟧⟧⇩T⇩E⇩S⇩L› by simp
  ultimately show ?thesis by simp
qed

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

lemma TESL_interp_decreases_add_tail:
  assumes ‹set Φ ⊆ set Φ'›
    shows ‹⟦⟦ Φ @ [φ] ⟧⟧⇩T⇩E⇩S⇩L ⊇ ⟦⟦ Φ' @ [φ] ⟧⟧⇩T⇩E⇩S⇩L›
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 ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ⇩2 ⟧⟧⇩T⇩E⇩S⇩L›
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 ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ⇩1 ⟧⟧⇩T⇩E⇩S⇩L›
using TESL_interp_absorb1 TESL_interp_commute assms by blast

section ‹Some special cases›

lemma NoSporadic_stable [simp]:
  ‹⟦⟦ Φ ⟧⟧⇩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

lemma NoSporadic_idem [simp]:
  ‹⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L ∩ ⟦⟦ NoSporadic Φ ⟧⟧⇩T⇩E⇩S⇩L = ⟦⟦ Φ ⟧⟧⇩T⇩E⇩S⇩L›
using NoSporadic_stable by blast

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

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

end