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.
›
overloading morphism_TESL_atomic ≡ 
            ‹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.
›
overloading morphism_TESL_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.
›
overloading morphism_TESL_config ≡ 
            ‹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