# 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› (‹τ⇩v⇩a⇩r›)

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 ‹⌈k⇩1, k⇩2⌉ ∈ R›} constrains counter expressions @{term ‹k⇩1›} and  @{term ‹k⇩2›}
to be in relation @{term ‹R›}.›
| TickCntArith  ‹cnt_expr› ‹cnt_expr› ‹(nat × nat) ⇒ bool›      (‹⌈_, _⌉ ∈ _›)
― ‹@{term ‹k⇩1 ≼ k⇩2›} constrains counter expression @{term ‹k⇩1›} to be less or equal
to counter expression @{term ‹k⇩2›}.›
| 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›
(‹⟦ _ ⊢ _ ⟧⇩c⇩n⇩t⇩e⇩x⇩p⇩r›)
where
‹⟦ ρ ⊢ #⇧< clk indx ⟧⇩c⇩n⇩t⇩e⇩x⇩p⇩r = run_tick_count_strictly ρ clk indx›
| ‹⟦ ρ ⊢ #⇧≤ clk indx ⟧⇩c⇩n⇩t⇩e⇩x⇩p⇩r = run_tick_count ρ clk indx›

fun symbolic_run_interpretation_primitive
::‹('τ::linordered_field) constr ⇒ 'τ run set› (‹⟦ _ ⟧⇩p⇩r⇩i⇩m›)
where
‹⟦ K ⇑ n  ⟧⇩p⇩r⇩i⇩m     = {ρ. hamlet ((Rep_run ρ) n K) }›
| ‹⟦ K @ n⇩0 ⊕ δt ⇒ K' ⟧⇩p⇩r⇩i⇩m =
{ρ. ∀n ≥ n⇩0. first_time ρ K n (time ((Rep_run ρ) n⇩0 K) + δt)
⟶ hamlet ((Rep_run ρ) n K')}›
| ‹⟦ K ¬⇑ n ⟧⇩p⇩r⇩i⇩m     = {ρ. ¬hamlet ((Rep_run ρ) n K) }›
| ‹⟦ K ¬⇑ < n ⟧⇩p⇩r⇩i⇩m   = {ρ. ∀i < n. ¬ hamlet ((Rep_run ρ) i K)}›
| ‹⟦ K ¬⇑ ≥ n ⟧⇩p⇩r⇩i⇩m   = {ρ. ∀i ≥ n. ¬ hamlet ((Rep_run ρ) i K) }›
| ‹⟦ K ⇓ n @ τ ⟧⇩p⇩r⇩i⇩m = {ρ. time ((Rep_run ρ) n K) = τ }›
| ‹⟦ ⌊τ⇩v⇩a⇩r(K⇩1, n⇩1), τ⇩v⇩a⇩r(K⇩2, n⇩2)⌋ ∈ R ⟧⇩p⇩r⇩i⇩m =
{ ρ. R (time ((Rep_run ρ) n⇩1 K⇩1), time ((Rep_run ρ) n⇩2 K⇩2)) }›
| ‹⟦ ⌈e⇩1, e⇩2⌉ ∈ R ⟧⇩p⇩r⇩i⇩m = { ρ. R (⟦ ρ ⊢ e⇩1 ⟧⇩c⇩n⇩t⇩e⇩x⇩p⇩r, ⟦ ρ ⊢ e⇩2 ⟧⇩c⇩n⇩t⇩e⇩x⇩p⇩r) }›
| ‹⟦ cnt_e⇩1 ≼ cnt_e⇩2 ⟧⇩p⇩r⇩i⇩m = { ρ. ⟦ ρ ⊢ cnt_e⇩1 ⟧⇩c⇩n⇩t⇩e⇩x⇩p⇩r ≤ ⟦ ρ ⊢ cnt_e⇩2 ⟧⇩c⇩n⇩t⇩e⇩x⇩p⇩r }›

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›
(‹⟦⟦ _ ⟧⟧⇩p⇩r⇩i⇩m›)
where
‹⟦⟦ [] ⟧⟧⇩p⇩r⇩i⇩m = {ρ. True }›
| ‹⟦⟦ γ # Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦ γ ⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›

lemma symbolic_run_interp_cons_morph:
‹⟦ γ ⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ γ # Γ ⟧⟧⇩p⇩r⇩i⇩m›
by auto

definition consistent_context :: ‹('τ::linordered_field) constr list ⇒ bool›
where
‹consistent_context Γ ≡ ( ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m ≠ {}) ›

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, τ⇩c⇩s⇩t 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:
‹⋂ ((λγ. ⟦ γ ⟧⇩p⇩r⇩i⇩m) ` set Γ) = ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
by (induction Γ, simp+)

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

theorem symrun_interp_expansion:
‹⟦⟦ Γ⇩1 @ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩1 ⟧⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m›
by (induction Γ⇩1, simp, auto)

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

lemma symrun_interp_assoc:
‹⟦⟦ (Γ⇩1 @ Γ⇩2) @ Γ⇩3 ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩1 @ (Γ⇩2 @ Γ⇩3) ⟧⟧⇩p⇩r⇩i⇩m›
by auto

lemma symrun_interp_commute:
‹⟦⟦ Γ⇩1 @ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩2 @ Γ⇩1 ⟧⟧⇩p⇩r⇩i⇩m›

lemma symrun_interp_left_commute:
‹⟦⟦ Γ⇩1 @ (Γ⇩2 @ Γ⇩3) ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩2 @ (Γ⇩1 @ Γ⇩3) ⟧⟧⇩p⇩r⇩i⇩m›
unfolding symrun_interp_expansion by auto

lemma symrun_interp_idem:
‹⟦⟦ Γ @ Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
using symrun_interp_expansion by auto

lemma symrun_interp_left_idem:
‹⟦⟦ Γ⇩1 @ (Γ⇩1 @ Γ⇩2) ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩1 @ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m›
using symrun_interp_expansion by auto

lemma symrun_interp_right_idem:
‹⟦⟦ (Γ⇩1 @ Γ⇩2) @ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩1 @ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m›
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:
‹⟦⟦ [] @ Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
by simp

lemma symrun_interp_neutral2:
‹⟦⟦ Γ @ [] ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
by simp

subsection ‹Decreasing interpretation of symbolic primitives›

text‹
Adding constraints to a context reduces the number of satisfying runs.
›
‹⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m ⊇ ⟦⟦ γ # Γ ⟧⟧⇩p⇩r⇩i⇩m›
by simp

lemma TESL_sem_decreases_tail:
‹⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m ⊇ ⟦⟦ Γ @ [γ] ⟧⟧⇩p⇩r⇩i⇩m›

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 ‹⟦⟦ γ # Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
proof -
have ‹γ # Γ = [γ] @ Γ› by simp
hence ‹⟦⟦ γ # Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ [γ] ⟧⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
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:
‹⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ remdups Γ ⟧⟧⇩p⇩r⇩i⇩m›
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 ‹⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ' ⟧⟧⇩p⇩r⇩i⇩m›
proof -
have ‹set (remdups Γ) = set (remdups Γ')›
moreover have fxpntΓ: ‹⋂ ((λγ. ⟦ γ ⟧⇩p⇩r⇩i⇩m) ` set Γ) = ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m›
moreover have fxpntΓ': ‹⋂ ((λγ. ⟦ γ ⟧⇩p⇩r⇩i⇩m) ` set Γ') = ⟦⟦ Γ' ⟧⟧⇩p⇩r⇩i⇩m›
moreover have ‹⋂ ((λγ. ⟦ γ ⟧⇩p⇩r⇩i⇩m) ` set Γ) = ⋂ ((λγ. ⟦ γ ⟧⇩p⇩r⇩i⇩m) ` set Γ')›
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 ‹⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m ⊇ ⟦⟦ Γ' ⟧⟧⇩p⇩r⇩i⇩m›
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 ‹⟦⟦ Γ' ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ @ Γ⇩r ⟧⟧⇩p⇩r⇩i⇩m›
using symrun_interp_set_lifting decompose by blast
moreover have ‹⟦⟦ Γ @ Γ⇩r ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Γ⇩r ⟧⟧⇩p⇩r⇩i⇩m›
moreover have ‹⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m ⊇ ⟦⟦ Γ ⟧⟧⇩p⇩r⇩i⇩m ∩ ⟦⟦ Γ⇩r ⟧⟧⇩p⇩r⇩i⇩m› by simp
ultimately show ?thesis by simp
qed

assumes ‹set Γ ⊆ set Γ'›
shows ‹⟦⟦ γ # Γ ⟧⟧⇩p⇩r⇩i⇩m ⊇ ⟦⟦ γ # Γ' ⟧⟧⇩p⇩r⇩i⇩m›
using symrun_interp_decreases_setinc assms by auto

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

lemma symrun_interp_absorb1:
assumes ‹set Γ⇩1 ⊆ set Γ⇩2›
shows ‹⟦⟦ Γ⇩1 @ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m = ⟦⟦ Γ⇩2 ⟧⟧⇩p⇩r⇩i⇩m›