Theory SymbolicPrimitive

chapter ‹Symbolic Primitives for Building Runs›

theory SymbolicPrimitive
  imports Run

begin

text‹
  We define here the primitive constraints on runs, towards which we translate
  TESL specifications in the operational semantics.
  These constraints refer to a specific symbolic run and can therefore access
  properties of the run at particular instants (for instance, the fact that a clock
  ticks at instant @{term ‹n›} of the run, or the time on a given clock at 
  that instant).

  In the previous chapters, we had no reference to particular instants of a run 
  because the TESL language should be invariant by stuttering in order to allow 
  the composition of specifications: adding an instant where no clock ticks to 
  a run that satisfies a formula should yield another run that satisfies the 
  same formula. However, when constructing runs that satisfy a formula, we
  need to be able to refer to the time or hamlet of a clock at a given instant.
›

text‹
  Counter expressions are used to get the number of ticks of a clock up to 
  (strictly or not) a given instant index.
›
datatype cnt_expr =
  TickCountLess ‹clock› ‹instant_index› (‹#<›)
| TickCountLeq ‹clock› ‹instant_index›  (‹#≤›)

subsection‹ Symbolic Primitives for Runs ›

text‹
  Tag values are used to refer to the time on a clock at a given instant index.
›
datatype tag_val =
  TSchematic ‹clock * instant_index› (‹τvar›)

datatype 'τ constr =
― ‹@{term ‹c ⇓ n @ τ›} constrains clock @{term ‹c›} to have time @{term ‹τ›}
    at instant @{term ‹n›} of the run.›
  Timestamp     ‹clock›   ‹instant_index› ‹'τ tag_const›         (‹_ ⇓ _ @ _›)
― ‹@{term ‹m @ n ⊕ δt ⇒ s›} constrains clock @{term ‹s›} to tick at the
    first instant at which the time on @{term ‹m›} has increased by @{term ‹δt›}
    from the value it had at instant @{term ‹n›} of the run.›
| TimeDelay     ‹clock›   ‹instant_index› ‹'τ tag_const› ‹clock› (‹_ @ _ ⊕ _ ⇒ _›)
― ‹@{term ‹c ⇑ n›} constrains clock @{term ‹c›} to tick
    at instant @{term ‹n›} of the run.›
| Ticks         ‹clock›   ‹instant_index›                        (‹_ ⇑ _›)
― ‹@{term ‹c ¬⇑ n›} constrains clock @{term ‹c›} not to tick
    at instant @{term ‹n›} of the run.›
| NotTicks      ‹clock›   ‹instant_index›                        (‹_ ¬⇑ _›)
― ‹@{term ‹c ¬⇑ < n›} constrains clock @{term ‹c›} not to tick
    before instant @{term ‹n›} of the run.›
| NotTicksUntil ‹clock›   ‹instant_index›                        (‹_ ¬⇑ < _›)
― ‹@{term ‹c ¬⇑ ≥ n›} constrains clock @{term ‹c›} not to tick
    at and after instant @{term ‹n›} of the run.›
| NotTicksFrom  ‹clock›   ‹instant_index›                        (‹_ ¬⇑ ≥ _›)
― ‹@{term ‹⌊τ1, τ2⌋ ∈ R›} constrains tag variables @{term ‹τ1›} and  @{term ‹τ2›} 
    to be in relation @{term ‹R›}.›
| TagArith      ‹tag_val› ‹tag_val› ‹('τ tag_const × 'τ tag_const) ⇒ bool› (‹⌊_, _⌋ ∈ _›)
― ‹@{term ‹⌈k1, k2⌉ ∈ R›} constrains counter expressions @{term ‹k1›} and  @{term ‹k2›} 
    to be in relation @{term ‹R›}.›
| TickCntArith  ‹cnt_expr› ‹cnt_expr› ‹(nat × nat) ⇒ bool›      (‹⌈_, _⌉ ∈ _›)
― ‹@{term ‹k1 ≼ k2›} constrains counter expression @{term ‹k1›} to be less or equal 
    to counter expression @{term ‹k2›}.›
| TickCntLeq    ‹cnt_expr› ‹cnt_expr›                            (‹_ ≼ _›)

type_synonym 'τ system = ‹'τ constr list›


text ‹
  The abstract machine has configurations composed of:
  ▪ the past @{term‹Γ›}, which captures choices that have already be made as a 
    list of symbolic primitive constraints on the run;
  ▪ the current index @{term ‹n›}, which is the index of the present instant;
  ▪ the present @{term‹Ψ›}, which captures the formulae that must be satisfied
    in the current instant;
  ▪ the future @{term‹Φ›}, which captures the constraints on the future of the run.
›
type_synonym 'τ config =
                ‹'τ system * instant_index * 'τ TESL_formula * 'τ TESL_formula›


section ‹Semantics of Primitive Constraints ›

text‹
  The semantics of the primitive constraints is defined in a way similar to
  the semantics of TESL formulae.
›
fun counter_expr_eval :: ‹('τ::linordered_field) run ⇒ cnt_expr ⇒ nat›
  (‹⟦ _ ⊢ _ ⟧cntexpr›)
where
  ‹⟦ ρ ⊢ #< clk indx ⟧cntexpr = run_tick_count_strictly ρ clk indx›
| ‹⟦ ρ ⊢ #≤ clk indx ⟧cntexpr = run_tick_count ρ clk indx›


fun symbolic_run_interpretation_primitive
  ::‹('τ::linordered_field) constr ⇒ 'τ run set› (‹⟦ _ ⟧prim›)
where
  ‹⟦ K ⇑ n  ⟧prim     = {ρ. hamlet ((Rep_run ρ) n K) }›
| ‹⟦ K @ n0 ⊕ δt ⇒ K' ⟧prim =
                  {ρ. ∀n ≥ n0. first_time ρ K n (time ((Rep_run ρ) n0 K) + δt)
                               ⟶ hamlet ((Rep_run ρ) n K')}›
| ‹⟦ K ¬⇑ n ⟧prim     = {ρ. ¬hamlet ((Rep_run ρ) n K) }›
| ‹⟦ K ¬⇑ < n ⟧prim   = {ρ. ∀i < n. ¬ hamlet ((Rep_run ρ) i K)}›
| ‹⟦ K ¬⇑ ≥ n ⟧prim   = {ρ. ∀i ≥ n. ¬ hamlet ((Rep_run ρ) i K) }›
| ‹⟦ K ⇓ n @ τ ⟧prim = {ρ. time ((Rep_run ρ) n K) = τ }›
| ‹⟦ ⌊τvar(K1, n1), τvar(K2, n2)⌋ ∈ R ⟧prim =
    { ρ. R (time ((Rep_run ρ) n1 K1), time ((Rep_run ρ) n2 K2)) }›
| ‹⟦ ⌈e1, e2⌉ ∈ R ⟧prim = { ρ. R (⟦ ρ ⊢ e1 ⟧cntexpr, ⟦ ρ ⊢ e2 ⟧cntexpr) }›
| ‹⟦ cnt_e1 ≼ cnt_e2 ⟧prim = { ρ. ⟦ ρ ⊢ cnt_e1 ⟧cntexpr ≤ ⟦ ρ ⊢ cnt_e2 ⟧cntexpr }›

text‹
  The composition of primitive constraints is their conjunction, and we get the
  set of satisfying runs by intersection.
›
fun symbolic_run_interpretation
  ::‹('τ::linordered_field) constr list ⇒ ('τ::linordered_field) run set›
  (‹⟦⟦ _ ⟧⟧prim›)
where
  ‹⟦⟦ [] ⟧⟧prim = {ρ. True }›
| ‹⟦⟦ γ # Γ ⟧⟧prim = ⟦ γ ⟧prim ∩ ⟦⟦ Γ ⟧⟧prim›

lemma symbolic_run_interp_cons_morph:
  ‹⟦ γ ⟧prim ∩ ⟦⟦ Γ ⟧⟧prim = ⟦⟦ γ # Γ ⟧⟧prim›
by auto

definition consistent_context :: ‹('τ::linordered_field) constr list ⇒ bool›
where 
  ‹consistent_context Γ ≡ ( ⟦⟦ Γ ⟧⟧prim ≠ {}) ›

subsection ‹Defining a method for witness construction›

text‹
  In order to build a run, we can start from an initial run in which no clock 
  ticks and the time is always 0 on any clock.
›
abbreviation initial_run :: ‹('τ::linordered_field) run› (‹ρ⊙›) where
  ‹ρ⊙ ≡ Abs_run ((λ_ _. (False, τcst 0)) ::nat ⇒ clock ⇒ (bool × 'τ tag_const))›

text‹
  To help avoiding that time flows backward, setting the time on a clock at a given 
  instant sets it for the future instants too.
›
fun time_update
  :: ‹nat ⇒ clock ⇒ ('τ::linordered_field) tag_const ⇒ (nat ⇒ 'τ instant)
      ⇒ (nat ⇒ 'τ instant)›
where
  ‹time_update n K τ ρ = (λn' K'. if K = K' ∧ n ≤ n'
                                  then (hamlet (ρ n K), τ)
                                  else ρ n' K')›


section ‹Rules and properties of consistence›

lemma context_consistency_preservationI:
  ‹consistent_context ((γ::('τ::linordered_field) constr)#Γ) ⟹ consistent_context Γ›
unfolding consistent_context_def by auto

― ‹This is very restrictive›
inductive context_independency
  ::‹('τ::linordered_field) constr ⇒ 'τ constr list ⇒ bool› (‹_ ⨝ _›)
where
  NotTicks_independency:
  ‹(K ⇑ n) ∉ set Γ ⟹ (K ¬⇑ n) ⨝ Γ›
| Ticks_independency:
  ‹(K ¬⇑ n) ∉ set Γ ⟹ (K ⇑ n) ⨝ Γ›
| Timestamp_independency:
  ‹(∄τ'. τ' = τ ∧ (K ⇓ n @ τ) ∈ set Γ) ⟹ (K ⇓ n @ τ) ⨝ Γ›


section‹Major Theorems›
subsection ‹Interpretation of a context›

text‹
  The interpretation of a context is the intersection of the interpretation 
  of its components.
›
theorem symrun_interp_fixpoint:
  ‹⋂ ((λγ. ⟦ γ ⟧prim) ` set Γ) = ⟦⟦ Γ ⟧⟧prim›
by (induction Γ, simp+)

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

theorem symrun_interp_expansion:
  ‹⟦⟦ Γ1 @ Γ2 ⟧⟧prim = ⟦⟦ Γ1 ⟧⟧prim ∩ ⟦⟦ Γ2 ⟧⟧prim›
by (induction Γ1, simp, auto)

section ‹Equations for the interpretation of symbolic primitives› 
subsection ‹General laws›

lemma symrun_interp_assoc:
  ‹⟦⟦ (Γ1 @ Γ2) @ Γ3 ⟧⟧prim = ⟦⟦ Γ1 @ (Γ2 @ Γ3) ⟧⟧prim›
by auto

lemma symrun_interp_commute:
  ‹⟦⟦ Γ1 @ Γ2 ⟧⟧prim = ⟦⟦ Γ2 @ Γ1 ⟧⟧prim›
by (simp add: symrun_interp_expansion inf_sup_aci(1))

lemma symrun_interp_left_commute:
  ‹⟦⟦ Γ1 @ (Γ2 @ Γ3) ⟧⟧prim = ⟦⟦ Γ2 @ (Γ1 @ Γ3) ⟧⟧prim›
unfolding symrun_interp_expansion by auto

lemma symrun_interp_idem:
  ‹⟦⟦ Γ @ Γ ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim›
using symrun_interp_expansion by auto

lemma symrun_interp_left_idem:
  ‹⟦⟦ Γ1 @ (Γ1 @ Γ2) ⟧⟧prim = ⟦⟦ Γ1 @ Γ2 ⟧⟧prim›
using symrun_interp_expansion by auto

lemma symrun_interp_right_idem:
  ‹⟦⟦ (Γ1 @ Γ2) @ Γ2 ⟧⟧prim = ⟦⟦ Γ1 @ Γ2 ⟧⟧prim›
unfolding symrun_interp_expansion by auto

lemmas symrun_interp_aci =  symrun_interp_commute
                            symrun_interp_assoc
                            symrun_interp_left_commute
                            symrun_interp_left_idem

― ‹Identity element›
lemma symrun_interp_neutral1:
  ‹⟦⟦ [] @ Γ ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim›
by simp

lemma symrun_interp_neutral2:
  ‹⟦⟦ Γ @ [] ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim›
by simp

subsection ‹Decreasing interpretation of symbolic primitives›

text‹
  Adding constraints to a context reduces the number of satisfying runs.
›
lemma TESL_sem_decreases_head:
  ‹⟦⟦ Γ ⟧⟧prim ⊇ ⟦⟦ γ # Γ ⟧⟧prim›
by simp

lemma TESL_sem_decreases_tail:
  ‹⟦⟦ Γ ⟧⟧prim ⊇ ⟦⟦ Γ @ [γ] ⟧⟧prim›
by (simp add: symrun_interp_expansion)

text‹
  Adding a constraint that is already in the context does not change the
  interpretation of the context.
›
lemma symrun_interp_formula_stuttering:
  assumes ‹γ ∈ set Γ›
    shows ‹⟦⟦ γ # Γ ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim›
proof -
  have ‹γ # Γ = [γ] @ Γ› by simp
  hence ‹⟦⟦ γ # Γ ⟧⟧prim = ⟦⟦ [γ] ⟧⟧prim ∩ ⟦⟦ Γ ⟧⟧prim›
    using symrun_interp_expansion by simp
  thus ?thesis using assms symrun_interp_fixpoint by fastforce
qed


text‹
  Removing duplicate constraints from a context does not change the
  interpretation of the context.
›
lemma symrun_interp_remdups_absorb:
  ‹⟦⟦ Γ ⟧⟧prim = ⟦⟦ remdups Γ ⟧⟧prim›
proof (induction Γ)
  case Cons
    thus ?case using symrun_interp_formula_stuttering by auto
qed simp

text‹
  Two identical sets of constraints have the same interpretation,
  the order in the context does not matter.
›
lemma symrun_interp_set_lifting:
  assumes ‹set Γ = set Γ'›
    shows ‹⟦⟦ Γ ⟧⟧prim = ⟦⟦ Γ' ⟧⟧prim›
proof -     
  have ‹set (remdups Γ) = set (remdups Γ')›
    by (simp add: assms)
  moreover have fxpntΓ: ‹⋂ ((λγ. ⟦ γ ⟧prim) ` set Γ) = ⟦⟦ Γ ⟧⟧prim›
    by (simp add: symrun_interp_fixpoint)
  moreover have fxpntΓ': ‹⋂ ((λγ. ⟦ γ ⟧prim) ` set Γ') = ⟦⟦ Γ' ⟧⟧prim›
    by (simp add: symrun_interp_fixpoint)
  moreover have ‹⋂ ((λγ. ⟦ γ ⟧prim) ` set Γ) = ⋂ ((λγ. ⟦ γ ⟧prim) ` set Γ')›
    by (simp add: assms)
  ultimately show ?thesis using symrun_interp_remdups_absorb by auto
qed

text‹
  The interpretation of contexts is contravariant with regard to set inclusion.
›
theorem symrun_interp_decreases_setinc:
  assumes ‹set Γ ⊆ set Γ'›
    shows ‹⟦⟦ Γ ⟧⟧prim ⊇ ⟦⟦ Γ' ⟧⟧prim›
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 ‹⟦⟦ Γ' ⟧⟧prim = ⟦⟦ Γ @ Γr ⟧⟧prim›
    using symrun_interp_set_lifting decompose by blast
  moreover have ‹⟦⟦ Γ @ Γr ⟧⟧prim = ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Γr ⟧⟧prim›
    by (simp add: symrun_interp_expansion)
  moreover have ‹⟦⟦ Γ ⟧⟧prim ⊇ ⟦⟦ Γ ⟧⟧prim ∩ ⟦⟦ Γr ⟧⟧prim› by simp
  ultimately show ?thesis by simp
qed

lemma symrun_interp_decreases_add_head:
  assumes ‹set Γ ⊆ set Γ'›
    shows ‹⟦⟦ γ # Γ ⟧⟧prim ⊇ ⟦⟦ γ # Γ' ⟧⟧prim›
using symrun_interp_decreases_setinc assms by auto

lemma symrun_interp_decreases_add_tail:
  assumes ‹set Γ ⊆ set Γ'›
    shows ‹⟦⟦ Γ @ [γ] ⟧⟧prim ⊇ ⟦⟦ Γ' @ [γ] ⟧⟧prim›
proof -
  from symrun_interp_decreases_setinc[OF assms] have ‹⟦⟦ Γ' ⟧⟧prim ⊆ ⟦⟦ Γ ⟧⟧prim› .
  thus ?thesis by (simp add: symrun_interp_expansion dual_order.trans)
qed

lemma symrun_interp_absorb1:
  assumes ‹set Γ1 ⊆ set Γ2›
    shows ‹⟦⟦ Γ1 @ Γ2 ⟧⟧prim = ⟦⟦ Γ2 ⟧⟧prim›
by (simp add: Int_absorb1 symrun_interp_decreases_setinc
                          symrun_interp_expansion assms)

lemma symrun_interp_absorb2:
  assumes ‹set Γ2 ⊆ set Γ1›
    shows ‹⟦⟦ Γ1 @ Γ2 ⟧⟧prim = ⟦⟦ Γ1 ⟧⟧prim›
using symrun_interp_absorb1 symrun_interp_commute assms by blast

end