Theory UnwindingConditions

theory UnwindingConditions
imports "../Basics/BSPTaxonomy"
  "../../SystemSpecification/StateEventSystems"
begin

locale Unwinding =
fixes SES :: "('s, 'e) SES_rec"
and 𝒱 :: "'e V_rec"

assumes validSES: "SES_valid SES"
and validVU: "isViewOn 𝒱 Eβ‡˜SES⇙"

(* sublocale relations for Unwinding *)
sublocale Unwinding βŠ† BSPTaxonomyDifferentCorrections "induceES SES" "𝒱"
  by (unfold_locales, simp add: induceES_yields_ES validSES,
    simp add: induceES_def validVU)

(* body of Unwinding *)
context Unwinding
begin

(* output step consistency (osc) *)
definition osc :: "'s rel β‡’ bool"
where
"osc ur ≑ 
  βˆ€s1 ∈ Sβ‡˜SES⇙. βˆ€s1' ∈ Sβ‡˜SES⇙. βˆ€s2' ∈ Sβ‡˜SES⇙. βˆ€e ∈ (Eβ‡˜SES⇙ - Cβ‡˜π’±β‡™).
    (reachable SES s1 ∧ reachable SES s1' 
       ∧ s1' eβŸΆβ‡˜SES⇙ s2' ∧ (s1', s1) ∈ ur)
    ⟢ (βˆƒs2 ∈ Sβ‡˜SES⇙. βˆƒΞ΄. Ξ΄ β†Ώ Cβ‡˜π’±β‡™ = [] ∧ Ξ΄ β†Ώ Vβ‡˜π’±β‡™ = [e] β†Ώ Vβ‡˜π’±β‡™ 
          ∧ s1 Ξ΄βŸΉβ‡˜SES⇙ s2 ∧ (s2', s2) ∈ ur)"

(* locally-respects forwards (lrf) *)
definition lrf :: "'s rel β‡’ bool"
where
"lrf ur ≑ 
  βˆ€s ∈ Sβ‡˜SES⇙. βˆ€s' ∈ Sβ‡˜SES⇙. βˆ€c ∈ Cβ‡˜π’±β‡™. 
  ((reachable SES s ∧ s cβŸΆβ‡˜SES⇙ s') ⟢ (s', s) ∈ ur)"

(* locally-respects backwards (lrb) *)
definition lrb :: "'s rel β‡’ bool"
where
"lrb ur ≑ βˆ€s ∈ Sβ‡˜SES⇙. βˆ€c ∈ Cβ‡˜π’±β‡™. 
  (reachable SES s ⟢ (βˆƒs' ∈ Sβ‡˜SES⇙. (s cβŸΆβ‡˜SES⇙ s' ∧ ((s, s') ∈ ur))))"

(* forward-correctably respects forwards (fcrf) *)
definition fcrf :: "'e Gamma β‡’ 's rel β‡’ bool"
where
"fcrf Ξ“ ur ≑ 
  βˆ€c ∈ (Cβ‡˜π’±β‡™ ∩ Ξ₯β‡˜Ξ“β‡™). βˆ€v ∈ (Vβ‡˜π’±β‡™ ∩ βˆ‡β‡˜Ξ“β‡™). βˆ€s ∈ Sβ‡˜SES⇙. βˆ€s' ∈ Sβ‡˜SES⇙.
    ((reachable SES s ∧ s ([c] @ [v])βŸΉβ‡˜SES⇙ s')
      ⟢ (βˆƒs'' ∈ Sβ‡˜SES⇙. βˆƒΞ΄. (βˆ€d ∈ (set Ξ΄). d ∈ (Nβ‡˜π’±β‡™ ∩ Ξ”β‡˜Ξ“β‡™)) ∧
             s (Ξ΄ @ [v])βŸΉβ‡˜SES⇙ s'' ∧ (s', s'') ∈ ur))"

(* forward-correctably respects backwards (fcrb) *)
definition fcrb :: "'e Gamma β‡’ 's rel β‡’ bool"
where 
"fcrb Ξ“ ur ≑ 
  βˆ€c ∈ (Cβ‡˜π’±β‡™ ∩ Ξ₯β‡˜Ξ“β‡™). βˆ€v ∈ (Vβ‡˜π’±β‡™ ∩ βˆ‡β‡˜Ξ“β‡™). βˆ€s ∈ Sβ‡˜SES⇙. βˆ€s'' ∈ Sβ‡˜SES⇙.
  ((reachable SES s ∧ s vβŸΆβ‡˜SES⇙ s'')
    ⟢ (βˆƒs' ∈ Sβ‡˜SES⇙. βˆƒΞ΄. (βˆ€d ∈ (set Ξ΄). d ∈ (Nβ‡˜π’±β‡™ ∩ Ξ”β‡˜Ξ“β‡™)) ∧
          s ([c] @ Ξ΄ @ [v])βŸΉβ‡˜SES⇙ s' ∧ (s'', s') ∈ ur))"

(* ρ-enabledness *)
definition En :: "'e Rho β‡’ 's β‡’ 'e β‡’ bool"
where
"En ρ s e ≑ 
  βˆƒΞ² Ξ³. βˆƒs' ∈ Sβ‡˜SES⇙. βˆƒs'' ∈ Sβ‡˜SES⇙.
    s0β‡˜SES⇙ Ξ²βŸΉβ‡˜SES⇙ s ∧ (Ξ³ β†Ώ (ρ 𝒱) = Ξ² β†Ώ (ρ 𝒱)) 
     ∧ s0β‡˜SES⇙ Ξ³βŸΉβ‡˜SES⇙ s' ∧ s' eβŸΆβ‡˜SES⇙ s''"

(* locally-respects backwards for enabled events (lrbe) *)
definition lrbe :: "'e Rho β‡’ 's rel β‡’ bool"
where
"lrbe ρ ur ≑ 
  βˆ€s ∈ Sβ‡˜SES⇙. βˆ€c ∈ Cβ‡˜π’±β‡™ .  
  ((reachable SES s ∧ (En ρ s c)) 
    ⟢ (βˆƒs' ∈ Sβ‡˜SES⇙. (s cβŸΆβ‡˜SES⇙ s' ∧ (s, s') ∈ ur)))"

(* forward-correctable respects backwards for enabled events (fcrbe) *)
definition fcrbe :: "'e Gamma β‡’ 'e Rho β‡’ 's rel β‡’ bool"
where
"fcrbe Ξ“ ρ ur ≑ 
  βˆ€c ∈ (Cβ‡˜π’±β‡™ ∩ Ξ₯β‡˜Ξ“β‡™). βˆ€v ∈ (Vβ‡˜π’±β‡™ ∩ βˆ‡β‡˜Ξ“β‡™). βˆ€s ∈ Sβ‡˜SES⇙. βˆ€s'' ∈ Sβ‡˜SES⇙.
  ((reachable SES s ∧ s vβŸΆβ‡˜SES⇙ s'' ∧ (En ρ s c))
    ⟢ (βˆƒs' ∈ Sβ‡˜SES⇙. βˆƒΞ΄. (βˆ€d ∈ (set Ξ΄). d ∈ (Nβ‡˜π’±β‡™ ∩ Ξ”β‡˜Ξ“β‡™)) ∧
           s ([c] @ Ξ΄ @ [v])βŸΉβ‡˜SES⇙ s' ∧ (s'', s') ∈ ur))"

end

end