# Theory Config_Morphisms

```theory Config_Morphisms
imports Hygge_Theory
begin

text ‹
TESL morphisms change the time on clocks, preserving the ticks.
›
consts morphism :: ‹'a ⇒ ('τ::linorder ⇒ 'τ::linorder) ⇒ 'a› (infixl ‹⨂› 100)

text ‹
Applying a TESL morphism to a tag simply changes its value.
›
overloading morphism_tagconst ≡ ‹morphism :: 'τ tag_const ⇒ ('τ::linorder ⇒ 'τ) ⇒ 'τ tag_const›
begin
definition morphism_tagconst :
‹(x::'τ tag_const) ⨂ (f::('τ::linorder ⇒ 'τ)) = (τ⇩c⇩s⇩t o f)(the_tag_const x) ›
end

text ‹
Applying a TESL morphism to an atomic formula only changes the dates.
›
‹morphism :: 'τ TESL_atomic ⇒ ('τ::linorder ⇒ 'τ) ⇒ 'τ TESL_atomic›
begin
definition morphism_TESL_atomic :
‹(Ψ::'τ TESL_atomic) ⨂ (f::('τ::linorder ⇒ 'τ)) =
(case Ψ of
(C sporadic t on C')     ⇒ (C sporadic (t⨂f) on C')
| (time-relation ⌊C, C'⌋∈R)⇒ (time-relation ⌊C, C'⌋ ∈ (λ(t, t'). R(t⨂f,t'⨂f)))
| (C implies C')           ⇒ (C implies C')
| (C implies not C')       ⇒ (C implies not C')
| (C time-delayed by t on C' implies C'')
⇒ (C time-delayed by t⨂f on C' implies C'')
| (C weakly precedes C')   ⇒ (C weakly precedes C')
| (C strictly precedes C') ⇒ (C strictly precedes C')
| (C kills C')             ⇒ (C kills C'))›
end

text ‹
Applying a TESL morphism to a formula amounts to apply it to each atomic formula.
›
‹morphism :: 'τ TESL_formula ⇒ ('τ::linorder ⇒ 'τ) ⇒ 'τ TESL_formula›
begin
definition  morphism_TESL_formula :
‹(Ψ::'τ TESL_formula) ⨂ (f::('τ::linorder ⇒ 'τ)) = map (λx. x ⨂ f) Ψ›
end

text ‹
Applying a TESL morphism to a configuration amounts to apply it to the
present and future formulae. The past (in the context @{term ‹Γ›}) is not changed.
›
‹morphism :: ('τ::linordered_field) config ⇒ ('τ ⇒ 'τ) ⇒ 'τ config›
begin
fun  morphism_TESL_config
where  ‹((Γ, n ⊢ Ψ ▹ Φ)::('τ::linordered_field) config) ⨂ (f::('τ ⇒ 'τ)) =
(Γ, n ⊢ (Ψ⨂f) ▹ (Φ⨂f))›
end

text ‹
A TESL formula is called consistent if it possesses Kripke-models
in its denotational interpretation.
›

definition consistent :: ‹('τ::linordered_field) TESL_formula ⇒ bool›
where   ‹consistent Ψ ≡ ⟦⟦ Ψ ⟧⟧⇩T⇩E⇩S⇩L ≠ {}›

text ‹
If we can derive a consistent finite context from a TESL formula, the formula is consistent.
›
theorem consistency_finite :
assumes start             : ‹([], 0 ⊢ Ψ ▹ [])  ↪⇧*⇧* (Γ⇩1, n⇩1 ⊢ [] ▹ [])›
and init_invariant    : ‹consistent_context Γ⇩1›
shows ‹consistent Ψ›
proof -
have * : ‹∃ n. (([], 0 ⊢ Ψ ▹ []) ↪⇗n⇖ (Γ⇩1, n⇩1 ⊢ [] ▹ []))›
by (simp add: rtranclp_imp_relpowp start)
show ?thesis
unfolding consistent_context_def consistent_def
using * consistent_context_def init_invariant soundness by fastforce
qed

subsubsection ‹Snippets on runs›

text ‹
A run with no ticks and constant time for all clocks.
›
definition const_nontick_run :: ‹(clock ⇒ 'τ tag_const) ⇒ ('τ::linordered_field) run › (‹□_› 80)
where ‹□f ≡  Abs_run(λn c. (False, f c))›

text ‹
Ensure a clock ticks in a run at a given instant.
›
definition set_tick :: ‹('τ::linordered_field) run ⇒ nat ⇒ clock ⇒ ('τ) run›
where   ‹set_tick r k c = Abs_run(λn c.  if k = n
then (True , time(Rep_run r k c))
else Rep_run r k c) ›

text ‹
Ensure a clock does not tick in a run at a given instant.
›
definition unset_tick :: ‹('τ::linordered_field) run ⇒ nat ⇒ clock ⇒ ('τ) run›
where   ‹unset_tick r k c = Abs_run(λn c.  if k = n
then (False , time(Rep_run r k c))
else Rep_run r k c) ›

text ‹
Replace all instants after k in a run with the instants from another run.
Warning: the result may not be a proper run since time may not be monotonous
from instant k to instant k+1.
›
definition patch :: ‹('τ::linordered_field) run ⇒ nat ⇒ 'τ run ⇒ 'τ run› (‹_ ≫⇗_⇖ _› 80)
where   ‹r ≫⇗k⇖r' ≡ Abs_run(λn c. if n ≤ k then Rep_run (r) n c else  Rep_run (r') n c)›

text ‹
For some infinite cases, the idea for a proof scheme looks as follows: if we can derive
from the initial configuration @{term ‹([], 0 ⊢ Ψ ▹ [])›} a start-point of a lasso
@{term ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1)›}, and if we can traverse the lasso one time
@{term ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) ↪⇧+⇧+ (Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2)›} to isomorphic one,
we can always always make a derivation along the lasso. If the entry point of the lasso had traces
with prefixes consistent to @{term ‹Γ⇩1›}, then there exist traces consisting of this prefix and
repetitions of the delta-prefix of the lasso which are consistent with @{term ‹Ψ›} which implies
the logical consistency of  @{term ‹Ψ›}.

So far the idea. Remains to prove it. Why does one symbolic run along a lasso generalises to
arbitrary runs ?
›

theorem consistency_coinduct :
assumes start             : ‹([], 0 ⊢ Ψ ▹ [])   ↪⇧*⇧* (Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1)›
and loop              : ‹(Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) ↪⇧+⇧+ (Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2)›
and init_invariant    : ‹consistent_context Γ⇩1›
and post_invariant    : ‹consistent_context Γ⇩2›
and retract_condition : ‹(Γ⇩2, n⇩2 ⊢ Ψ⇩2 ▹ Φ⇩2) ⨂ (f::'τ ⇒ 'τ) = (Γ⇩1, n⇩1 ⊢ Ψ⇩1 ▹ Φ⇩1) ›
shows ‹consistent (Ψ :: ('τ :: linordered_field)TESL_formula)›
oops

end
```