(*  
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹(Generalized) Rabin Automata›

theory Rabin
  imports Main DTS
begin

type_synonym ('a, 'b) rabin_pair = "(('a, 'b) transition set × ('a, 'b) transition set)"
type_synonym ('a, 'b) generalized_rabin_pair = "(('a, 'b) transition set × ('a, 'b) transition set set)"

type_synonym ('a, 'b) rabin_condition = "('a, 'b) rabin_pair set"
type_synonym ('a, 'b) generalized_rabin_condition = "('a, 'b) generalized_rabin_pair set"

type_synonym ('a, 'b) rabin_automaton = "('a, 'b) DTS × 'a × ('a, 'b) rabin_condition"
type_synonym ('a, 'b) generalized_rabin_automaton = "('a, 'b) DTS × 'a × ('a, 'b) generalized_rabin_condition"

definition accepting_pair_R :: "('a, 'b) DTS → 'a → ('a, 'b) rabin_pair → 'b word → bool"
where
  "accepting_pair_R δ q₀ P w ≡ limit (run_t δ q₀ w) ∩ fst P = {} ∧ limit (run_t δ q₀ w) ∩ snd P ≠ {}"

definition accept_R :: "('a, 'b) rabin_automaton → 'b word → bool"
where 
  "accept_R R w ≡ (∃P ∈ (snd (snd R)). accepting_pair_R (fst R) (fst (snd R)) P w)"

definition accepting_pair_GR :: "('a, 'b) DTS → 'a → ('a, 'b) generalized_rabin_pair → 'b word → bool"
where
  "accepting_pair_GR δ q₀ P w ≡ limit (run_t δ q₀ w) ∩ fst P = {} ∧ (∀I ∈ snd P. limit (run_t δ q₀ w) ∩ I ≠ {})"

definition accept_GR :: "('a, 'b) generalized_rabin_automaton → 'b word → bool"
where 
  "accept_GR R w ≡ (∃(Fin, Inf) ∈ (snd (snd R)). accepting_pair_GR (fst R) (fst (snd R)) (Fin, Inf) w)"

declare accepting_pair_{R_def}[simp]
declare accepting_pair_{GR_def}[simp]

lemma accepting_pair_{R_simp}[simp]:
  "accepting_pair_R δ q₀ (F,I) w ≡ limit (run_t δ q₀ w) ∩ F = {} ∧ limit (run_t δ q₀ w) ∩ I ≠ {}"
  by simp

lemma accepting_pair_{GR_simp}[simp]:
  "accepting_pair_GR δ q₀ (F, I) w ≡ limit (run_t δ q₀ w) ∩ F = {} ∧ (∀I ∈ I. limit (run_t δ q₀ w) ∩ I ≠ {})"
  by simp

lemma accept_{R_simp}[simp]:
  "accept_R (δ, q₀, α) w = (∃(Fin, Inf) ∈ α. limit (run_t δ q₀ w) ∩ Fin = {} ∧ limit (run_t δ q₀ w) ∩ Inf ≠ {})"
  by (unfold accept_{R_def} accepting_pair_{R_def} case_prod_unfold fst_conv snd_conv; rule)

lemma accept_{GR_simp}[simp]: 
  "accept_GR (δ, q₀, α) w ⟷ (∃(Fin, Inf) ∈ α. limit (run_t δ q₀ w) ∩ Fin = {} ∧ (∀I ∈ Inf. limit (run_t δ q₀ w) ∩ I ≠ {}))"
  by (unfold accept_{GR_def} accepting_pair_{GR_def} case_prod_unfold fst_conv snd_conv; rule)

lemma accept_{GR_simp2}: 
  "accept_GR (δ, q₀, α) w ⟷ (∃P ∈ α. accepting_pair_GR δ q₀ P w)"
  by (unfold accept_{GR_def} accepting_pair_{GR_def} case_prod_unfold fst_conv snd_conv; rule)

type_synonym ('a, 'b) LTS = "('a, 'b) transition set"

definition LTS_is_inf_run :: "('q,'a) LTS → 'a word → 'q word → bool" where
  "LTS_is_inf_run Δ w r ⟷ (∀i. (r i, w i, r (Suc i)) ∈ Δ)"

fun accept_{R_LTS} :: "(('a, 'b) LTS × 'a × ('a, 'b) rabin_condition) → 'b word → bool"
where 
  "accept_{R_LTS} (δ, q₀, α) w ⟷ (∃(Fin, Inf) ∈ α. ∃r.
      LTS_is_inf_run δ w r ∧ r 0 = q₀
    ∧ limit (λi. (r i, w i, r (Suc i))) ∩ Fin = {}
    ∧ limit (λi. (r i, w i, r (Suc i))) ∩ Inf ≠ {})"

definition accepting_pair_{GR_LTS} :: "('a, 'b) LTS → 'a → ('a, 'b) generalized_rabin_pair → 'b word → bool"
where
  "accepting_pair_{GR_LTS} δ q₀ P w ≡ ∃r. LTS_is_inf_run δ w r ∧ r 0 = q₀
    ∧ limit (λi. (r i, w i, r (Suc i))) ∩ fst P = {}
    ∧ (∀I ∈ snd P. limit (λi. (r i, w i, r (Suc i))) ∩ I ≠ {})"

fun accept_{GR_LTS} :: "(('a, 'b) LTS × 'a × ('a, 'b) generalized_rabin_condition) → 'b word → bool"
where 
  "accept_{GR_LTS} (δ, q₀, α) w = (∃(Fin, Inf) ∈ α. accepting_pair_{GR_LTS} δ q₀ (Fin, Inf) w)"

lemma accept_{GR_LTS_E}:
  assumes "accept_{GR_LTS} R w"
  obtains F I where "(F, I) ∈ snd (snd R)"
   and "accepting_pair_{GR_LTS} (fst R) (fst (snd R)) (F, I) w"
proof -
  obtain δ q₀ α where "R = (δ, q₀, α)"
    using prod_cases3 by blast
  show "(∧F I. (F, I) ∈ snd (snd R) ==> accepting_pair_{GR_LTS} (fst R) (fst (snd R)) (F, I) w ==> thesis) ==> thesis"
    using assms unfolding ‹R = (δ, q₀, α)› by auto
qed

lemma accept_{GR_LTS_I}:
  "accepting_pair_{GR_LTS} δ q₀ (F, I) w ==> (F, I) ∈ α ==> accept_{GR_LTS} (δ, q₀, α) w"
  by auto

lemma accept_{GR_I}:
  "accepting_pair_GR δ q₀ (F, I) w ==> (F, I) ∈ α ==> accept_GR (δ, q₀, α) w"
  by auto

lemma transfer_accept:
  "accepting_pair_R δ q₀ (F, I) w ⟷ accepting_pair_GR δ q₀ (F, {I}) w"
  "accept_R (δ, q₀, α) w ⟷ accept_GR (δ, q₀, (λ(F, I). (F, {I})) ` α) w"
  by (simp add: case_prod_unfold)+

subsection ‹Restriction Lemmas›

lemma accepting_pair_{GR_restrict}:
  assumes "range w ⊆ Σ"
  shows "accepting_pair_GR δ q₀ (F, I) w = accepting_pair_GR δ q₀ (F ∩ reach_t Σ δ q₀, (λI. I ∩ reach_t Σ δ q₀) ` I) w"
proof -
  have "limit (run_t δ q₀ w) ∩ F = {} ⟷ limit (run_t δ q₀ w) ∩ (F ∩ reach_t Σ δ q₀) = {}"
    using assms[THEN limit_subseteq_reach(2), of δ q₀] by auto
  moreover
  have "(∀I∈I. limit (run_t δ q₀ w) ∩ I ≠ {}) = ((∀I∈{y. ∃x∈I. y = x ∩ reach_t Σ δ q₀}. limit (run_t δ q₀ w) ∩ I ≠ {}))"
     using assms[THEN limit_subseteq_reach(2), of δ q₀] by auto
  ultimately
  show ?thesis
    unfolding accepting_pair_{GR_simp} image_def by meson
qed

lemma accept_{GR_restrict}:
  assumes "range w ⊆ Σ"
  shows "accept_GR (δ, q₀, {(f x, g x) | x. P x}) w = accept_GR (δ, q₀, {(f x ∩ reach_t Σ δ q₀, (λI. I ∩ reach_t Σ δ q₀) ` g x) | x. P x}) w"
  apply (simp only: accept_{GR_simp})  
  apply (subst accepting_pair_{GR_restrict}[OF assms, simplified]) 
  apply simp
  apply standard
  apply (metis (no_types, lifting) imageE) 
  apply fastforce
  done

lemma accepting_pair_{R_restrict}:
  assumes "range w ⊆ Σ"
  shows "accepting_pair_R δ q₀ (F, I) w = accepting_pair_R δ q₀ (F ∩ reach_t Σ δ q₀, I ∩ reach_t Σ δ q₀) w"
  by (simp only: transfer_accept; subst accepting_pair_{GR_restrict}[OF assms]; simp)

lemma accept_{R_restrict}:
  assumes "range w ⊆ Σ"
  shows "accept_R (δ, q₀, {(f x, g x) | x. P x}) w = accept_R (δ, q₀, {(f x ∩ reach_t Σ δ q₀, g x ∩ reach_t Σ δ q₀) | x. P x}) w"
  by (simp only: accept_{R_simp}; subst accepting_pair_{R_restrict}[OF assms, simplified]; auto)

subsection ‹Abstraction Lemmas›

lemma accepting_pair_{GR_abstract}:
  assumes "finite (reach_t Σ δ q₀)" 
      and "finite (reach_t Σ δ' q₀')"
  assumes "range w ⊆ Σ"
  assumes "run_t δ q₀ w = f o (run_t δ' q₀' w)"
  assumes "∧t. t ∈ reach_t Σ δ' q₀' ==> f t ∈ F ⟷ t ∈ F'"
  assumes "∧t i. i ∈ I ==> t ∈ reach_t Σ δ' q₀' ==> f t ∈ I i ⟷ t ∈ I' i"
  shows "accepting_pair_GR δ q₀ (F, {I i | i. i ∈ I}) w ⟷ accepting_pair_GR δ' q₀' (F', {I' i | i. i ∈ I}) w"
proof -
  have "finite (range (run_t δ q₀ w))" (is "_ (range ?r)") 
    and "finite (range (run_t δ' q₀' w))" (is "_ (range ?r')")
    using assms(1,2,3) run_subseteq_reach(2) by (metis finite_subset)+
  then obtain k where 1: "limit ?r = range (suffix k ?r)"
    and 2: "limit ?r' = range (suffix k ?r')"
    using common_range_limit by blast
  have X: "limit (run_t δ q₀ w) = f ` limit (run_t δ' q₀' w)"
    unfolding 1 2 suffix_def by (auto simp add: assms(4))
  have 3: "(limit ?r ∩ F = {}) ⟷ (limit ?r' ∩ F' = {})"
    and 4: "(∀i ∈ I. limit ?r ∩ I i ≠ {}) ⟷ (∀i ∈ I. limit ?r' ∩ I' i ≠ {})"
    using assms(5,6) limit_subseteq_reach(2)[OF assms(3)] by (unfold X; fastforce)+
  thus ?thesis
    unfolding accepting_pair_{GR_simp} by blast
qed

lemma accepting_pair_{R_abstract}:
  assumes "finite (reach_t Σ δ q₀)" 
      and "finite (reach_t Σ δ' q₀')"
  assumes "range w ⊆ Σ"
  assumes "run_t δ q₀ w = f o (run_t δ' q₀' w)"
  assumes "∧t. t ∈ reach_t Σ δ' q₀' ==> f t ∈ F ⟷ t ∈ F'"
  assumes "∧t. t ∈ reach_t Σ δ' q₀' ==> f t ∈ I ⟷ t ∈ I'"
  shows "accepting_pair_R δ q₀ (F, I) w ⟷ accepting_pair_R δ' q₀' (F', I') w"
  using accepting_pair_{GR_abstract}[OF assms(1-5), of UNIV "λ_. I" "λ_. I'"] assms(6) by simp

subsection ‹LTS Lemmas›

lemma accepting_pair_{GR_LTS}:
  assumes "range w ⊆ Σ"
  shows "accepting_pair_GR δ q₀ (F, I) w ⟷ accepting_pair_{GR_LTS} (reach_t Σ δ q₀) q₀ (F, I) w" 
  (is "?lhs ⟷ ?rhs")
proof 
  {
    assume ?lhs
    moreover
    have "LTS_is_inf_run (reach_t Σ δ q₀) w (run δ q₀ w)"
      unfolding LTS_is_inf_run_def reach_{t_def} using assms(1) by auto
    moreover
    have "run δ q₀ w 0 = q₀"
      by simp
    ultimately
    show ?rhs
      unfolding accept_{GR_simp} accept_{GR_LTS}.simps accepting_pair_{GR_simp} run_t.simps limit_def accepting_pair_{GR_LTS_def} snd_conv fst_conv by blast
  }
  
  {
    assume ?rhs
    then obtain r where "LTS_is_inf_run (reach_t Σ δ q₀) w r"
      and "r 0 = q₀"
      and "limit (λi. (r i, w i, r (Suc i))) ∩ F = {}"
      and "∧I. I ∈ I ==> limit (λi. (r i, w i, r (Suc i))) ∩ I ≠ {}"
      unfolding accepting_pair_{GR_LTS_def} by auto
    moreover
    {
      fix i
      from ‹r 0 = q₀› ‹LTS_is_inf_run (reach_t Σ δ q₀) w r› have "r i = run δ q₀ w i"
        by (induction i; simp_all add: LTS_is_inf_run_def reach_{t_def}) metis
    }
    hence "r = run δ q₀ w"
      by blast
    hence "(λi. (r i, w i, r (Suc i))) = run_t δ q₀ w"
      by auto
    ultimately
    show ?lhs
      by auto
  }
qed

lemma accept_{GR_LTS}:
  assumes "range w ⊆ Σ"
  shows "accept_GR (δ, q₀, α) w ⟷ accept_{GR_LTS} (reach_t Σ δ q₀, q₀, α) w" 
  unfolding accept_{GR_def} fst_conv snd_conv accepting_pair_{GR_LTS}[OF assms] by simp

lemma accept_{R_LTS}:
  assumes "range w ⊆ Σ"
  shows "accept_R (δ, q₀, α) w ⟷ accept_{R_LTS} (reach_t Σ δ q₀, q₀, α) w"
  unfolding transfer_accept accept_{GR_LTS}.simps accept_{R_LTS}.simps accept_{GR_LTS}[OF assms] case_prod_unfold accepting_pair_{GR_LTS_def} by simp

subsection ‹Combination Lemmas›

lemma combine_rabin_pairs: 
  "(∧x. x ∈ I ==> accepting_pair_R δ q₀ (f x, g x) w) ==> accepting_pair_GR δ q₀ (∪{f x | x. x ∈ I}, {g x | x. x ∈ I}) w" 
  by auto

lemma combine_rabin_pairs_UNIV: 
  "accepting_pair_R δ q₀ (fin, UNIV) w ==> accepting_pair_GR δ q₀ (fin', inf') w ==> accepting_pair_GR δ q₀ (fin ∪ fin', inf') w"
  by auto

end