Theory TA_Equivalences

theory TA_Equivalences
  imports
    Timed_Automata.Timed_Automata
    Munta_Base.Normalized_Zone_Semantics_Impl_Refine
begin

locale TA_Equiv =
  fixes A B :: "('a, 'c, 't :: time, 's) ta"
  fixes S :: "'s set"
  assumes state_set_trans_of: "state_set (trans_of A) ⊆ S"
  assumes invs: "∀ l ∈ S. inv_of A l = inv_of B l"
  assumes trans_eq: "trans_of A = trans_of B"
begin

lemma delay1:
  "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩" if "l ∈ S" "B ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩"
  using that invs by (auto elim!: step_t.cases)

lemma action1:
  "A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l',u'⟩" if "B ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l',u'⟩"
proof -
  from that have "l ∈ S" "l' ∈ S"
    using state_set_trans_of by (auto elim!: step_a.cases simp: trans_eq state_set_def)
  with that invs show ?thesis
    by (auto elim!: step_a.cases simp: trans_eq intro: step_a.intros)
qed

lemma delay2:
  "B ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩" if "l ∈ S" "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩"
  using that invs by (auto elim!: step_t.cases)

lemma action2:
  "B ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l',u'⟩" if "A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l',u'⟩"
proof -
  from that have "l ∈ S" "l' ∈ S"
    using state_set_trans_of by (auto elim!: step_a.cases simp: trans_eq[symmetric] state_set_def)
  with that invs show ?thesis
    by (auto elim!: step_a.cases simp: trans_eq [symmetric] intro: step_a.intros)
qed

lemma step1:
  "A ⊢ ⟨l, u⟩ → ⟨l',u'⟩" if "l ∈ S" "B ⊢ ⟨l, u⟩ → ⟨l',u'⟩"
  using that(2,1) by cases (auto dest: action1 delay1)

lemma step2:
  "B ⊢ ⟨l, u⟩ → ⟨l',u'⟩" if "l ∈ S" "A ⊢ ⟨l, u⟩ → ⟨l',u'⟩"
  using that(2,1) by cases (auto dest: action2 delay2)

lemma S_inv:
  "l' ∈ S" if "A ⊢ ⟨l, u⟩ → ⟨l',u'⟩" "l ∈ S"
  using that state_set_trans_of
  by (auto elim!: step.cases step_a.cases step_t.cases simp: state_set_def)

interpretation interp: Bisimulation_Invariant
  "λ (l, u) (l', u'). A ⊢ ⟨l, u⟩ → ⟨l',u'⟩"
  "λ (l, u) (l', u'). B ⊢ ⟨l, u⟩ → ⟨l',u'⟩"
  "λ lu lu'. lu' = lu" "λ (l, u). l ∈ S" "λ (l, u). l ∈ S"
  by standard (auto dest: step1 step2 intro: S_inv)



end (* TA Equiv *)

end (* Theory *)