Theory Rabin

(*  
    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⇩0 P w ≡ limit (run⇩t δ q⇩0 w) ∩ fst P = {} ∧ limit (run⇩t δ q⇩0 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⇩G⇩R :: "('a, 'b) DTS ⇒ 'a ⇒ ('a, 'b) generalized_rabin_pair ⇒ 'b word ⇒ bool"
where
  "accepting_pair⇩G⇩R δ q⇩0 P w ≡ limit (run⇩t δ q⇩0 w) ∩ fst P = {} ∧ (∀I ∈ snd P. limit (run⇩t δ q⇩0 w) ∩ I ≠ {})"

definition accept⇩G⇩R :: "('a, 'b) generalized_rabin_automaton ⇒ 'b word ⇒ bool"
where 
  "accept⇩G⇩R R w ≡ (∃(Fin, Inf) ∈ (snd (snd R)). accepting_pair⇩G⇩R (fst R) (fst (snd R)) (Fin, Inf) w)"

declare accepting_pair⇩R_def[simp]
declare accepting_pair⇩G⇩R_def[simp]

lemma accepting_pair⇩R_simp[simp]:
  "accepting_pair⇩R δ q⇩0 (F,I) w ≡ limit (run⇩t δ q⇩0 w) ∩ F = {} ∧ limit (run⇩t δ q⇩0 w) ∩ I ≠ {}"
  by simp

lemma accepting_pair⇩G⇩R_simp[simp]:
  "accepting_pair⇩G⇩R δ q⇩0 (F, ℐ) w ≡ limit (run⇩t δ q⇩0 w) ∩ F = {} ∧ (∀I ∈ ℐ. limit (run⇩t δ q⇩0 w) ∩ I ≠ {})"
  by simp

lemma accept⇩R_simp[simp]:
  "accept⇩R (δ, q⇩0, α) w = (∃(Fin, Inf) ∈ α. limit (run⇩t δ q⇩0 w) ∩ Fin = {} ∧ limit (run⇩t δ q⇩0 w) ∩ Inf ≠ {})"
  by (unfold accept⇩R_def accepting_pair⇩R_def case_prod_unfold fst_conv snd_conv; rule)

lemma accept⇩G⇩R_simp[simp]: 
  "accept⇩G⇩R (δ, q⇩0, α) w ⟷ (∃(Fin, Inf) ∈ α. limit (run⇩t δ q⇩0 w) ∩ Fin = {} ∧ (∀I ∈ Inf. limit (run⇩t δ q⇩0 w) ∩ I ≠ {}))"
  by (unfold accept⇩G⇩R_def accepting_pair⇩G⇩R_def case_prod_unfold fst_conv snd_conv; rule)

lemma accept⇩G⇩R_simp2: 
  "accept⇩G⇩R (δ, q⇩0, α) w ⟷ (∃P ∈ α. accepting_pair⇩G⇩R δ q⇩0 P w)"
  by (unfold accept⇩G⇩R_def accepting_pair⇩G⇩R_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⇩0, α) w ⟷ (∃(Fin, Inf) ∈ α. ∃r. 
      LTS_is_inf_run δ w r ∧ r 0 = q⇩0 
    ∧ limit (λi. (r i, w i, r (Suc i))) ∩ Fin = {} 
    ∧ limit (λi. (r i, w i, r (Suc i))) ∩ Inf ≠ {})"

definition accepting_pair⇩G⇩R_LTS :: "('a, 'b) LTS ⇒ 'a ⇒ ('a, 'b) generalized_rabin_pair ⇒ 'b word ⇒ bool"
where
  "accepting_pair⇩G⇩R_LTS δ q⇩0 P w ≡ ∃r. LTS_is_inf_run δ w r ∧ r 0 = q⇩0 
    ∧ 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⇩G⇩R_LTS :: "(('a, 'b) LTS × 'a × ('a, 'b) generalized_rabin_condition) ⇒ 'b word ⇒ bool"
where 
  "accept⇩G⇩R_LTS (δ, q⇩0, α) w = (∃(Fin, Inf) ∈ α. accepting_pair⇩G⇩R_LTS δ q⇩0 (Fin, Inf) w)"

lemma accept⇩G⇩R_LTS_E:
  assumes "accept⇩G⇩R_LTS R w"
  obtains F I where "(F, I) ∈ snd (snd R)"
   and "accepting_pair⇩G⇩R_LTS (fst R) (fst (snd R)) (F, I) w"
proof -
  obtain δ q⇩0 α where "R = (δ, q⇩0, α)"
    using prod_cases3 by blast
  show "(⋀F I. (F, I) ∈ snd (snd R) ⟹ accepting_pair⇩G⇩R_LTS (fst R) (fst (snd R)) (F, I) w ⟹ thesis) ⟹ thesis"
    using assms unfolding ‹R = (δ, q⇩0, α)› by auto
qed

lemma accept⇩G⇩R_LTS_I:
  "accepting_pair⇩G⇩R_LTS δ q⇩0 (F, ℐ) w ⟹ (F, ℐ) ∈ α ⟹ accept⇩G⇩R_LTS (δ, q⇩0, α) w"
  by auto

lemma accept⇩G⇩R_I:
  "accepting_pair⇩G⇩R δ q⇩0 (F, ℐ) w ⟹ (F, ℐ) ∈ α ⟹ accept⇩G⇩R (δ, q⇩0, α) w"
  by auto

lemma transfer_accept:
  "accepting_pair⇩R δ q⇩0 (F, I) w ⟷ accepting_pair⇩G⇩R δ q⇩0 (F, {I}) w"
  "accept⇩R (δ, q⇩0, α) w ⟷ accept⇩G⇩R (δ, q⇩0, (λ(F, I). (F, {I})) ` α) w"
  by (simp add: case_prod_unfold)+

subsection ‹Restriction Lemmas›

lemma accepting_pair⇩G⇩R_restrict:
  assumes "range w ⊆ Σ"
  shows "accepting_pair⇩G⇩R δ q⇩0 (F, ℐ) w = accepting_pair⇩G⇩R δ q⇩0 (F ∩ reach⇩t Σ δ q⇩0, (λI. I ∩ reach⇩t Σ δ q⇩0) ` ℐ) w"
proof -
  have "limit (run⇩t δ q⇩0 w) ∩ F = {} ⟷ limit (run⇩t δ q⇩0 w) ∩ (F ∩ reach⇩t Σ δ q⇩0) = {}"
    using assms[THEN limit_subseteq_reach(2), of δ q⇩0] by auto
  moreover
  have "(∀I∈ℐ. limit (run⇩t δ q⇩0 w) ∩ I ≠ {}) = ((∀I∈{y. ∃x∈ℐ. y = x ∩ reach⇩t Σ δ q⇩0}. limit (run⇩t δ q⇩0 w) ∩ I ≠ {}))"
     using assms[THEN limit_subseteq_reach(2), of δ q⇩0] by auto
  ultimately
  show ?thesis
    unfolding accepting_pair⇩G⇩R_simp image_def by meson
qed

lemma accept⇩G⇩R_restrict:
  assumes "range w ⊆ Σ"
  shows "accept⇩G⇩R (δ, q⇩0, {(f x, g x) | x. P x}) w = accept⇩G⇩R (δ, q⇩0, {(f x ∩ reach⇩t Σ δ q⇩0, (λI. I ∩ reach⇩t Σ δ q⇩0) ` g x) | x. P x}) w"
  apply (simp only: accept⇩G⇩R_simp)  
  apply (subst accepting_pair⇩G⇩R_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⇩0 (F, I) w = accepting_pair⇩R δ q⇩0 (F ∩ reach⇩t Σ δ q⇩0, I ∩ reach⇩t Σ δ q⇩0) w"
  by (simp only: transfer_accept; subst accepting_pair⇩G⇩R_restrict[OF assms]; simp)

lemma accept⇩R_restrict:
  assumes "range w ⊆ Σ"
  shows "accept⇩R (δ, q⇩0, {(f x, g x) | x. P x}) w = accept⇩R (δ, q⇩0, {(f x ∩ reach⇩t Σ δ q⇩0, g x ∩ reach⇩t Σ δ q⇩0) | 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⇩G⇩R_abstract:
  assumes "finite (reach⇩t Σ δ q⇩0)" 
      and "finite (reach⇩t Σ δ' q⇩0')"
  assumes "range w ⊆ Σ"
  assumes "run⇩t δ q⇩0 w = f o (run⇩t δ' q⇩0' w)"
  assumes "⋀t. t ∈ reach⇩t Σ δ' q⇩0' ⟹ f t ∈ F ⟷ t ∈ F'"
  assumes "⋀t i. i ∈ ℐ ⟹ t ∈ reach⇩t Σ δ' q⇩0' ⟹ f t ∈ I i ⟷ t ∈ I' i"
  shows "accepting_pair⇩G⇩R δ q⇩0 (F, {I i | i. i ∈ ℐ}) w ⟷ accepting_pair⇩G⇩R δ' q⇩0' (F', {I' i | i. i ∈ ℐ}) w"
proof -
  have "finite (range (run⇩t δ q⇩0 w))" (is "_ (range ?r)") 
    and "finite (range (run⇩t δ' q⇩0' 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⇩0 w) = f ` limit (run⇩t δ' q⇩0' w)"
    unfolding 1 2 suffix_def by (auto simp add: assms(4))
  have 3: "(limit ?r ∩ F = {}) ⟷ (limit ?r' ∩ F' = {})"
    and 4: "(∀i ∈ ℐ. limit ?r ∩ 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⇩G⇩R_simp by blast
qed

lemma accepting_pair⇩R_abstract:
  assumes "finite (reach⇩t Σ δ q⇩0)" 
      and "finite (reach⇩t Σ δ' q⇩0')"
  assumes "range w ⊆ Σ"
  assumes "run⇩t δ q⇩0 w  = f o (run⇩t δ' q⇩0' w)"
  assumes "⋀t. t ∈ reach⇩t Σ δ' q⇩0' ⟹ f t ∈ F ⟷ t ∈ F'"
  assumes "⋀t. t ∈ reach⇩t Σ δ' q⇩0' ⟹ f t ∈ I ⟷ t ∈ I'"
  shows "accepting_pair⇩R δ q⇩0 (F, I) w ⟷ accepting_pair⇩R δ' q⇩0' (F', I') w"
  using accepting_pair⇩G⇩R_abstract[OF assms(1-5), of UNIV "λ_. I" "λ_. I'"] assms(6) by simp

subsection ‹LTS Lemmas›

lemma accepting_pair⇩G⇩R_LTS:
  assumes "range w ⊆ Σ"
  shows "accepting_pair⇩G⇩R δ q⇩0 (F, ℐ) w ⟷ accepting_pair⇩G⇩R_LTS (reach⇩t Σ δ q⇩0) q⇩0 (F, ℐ) w" 
  (is "?lhs ⟷ ?rhs")
proof 
  {
    assume ?lhs
    moreover
    have "LTS_is_inf_run (reach⇩t Σ δ q⇩0) w (run δ q⇩0 w)"
      unfolding LTS_is_inf_run_def reach⇩t_def using assms(1) by auto
    moreover
    have "run δ q⇩0 w 0 = q⇩0"
      by simp
    ultimately
    show ?rhs
      unfolding accept⇩G⇩R_simp accept⇩G⇩R_LTS.simps accepting_pair⇩G⇩R_simp run⇩t.simps limit_def accepting_pair⇩G⇩R_LTS_def snd_conv fst_conv by blast
  }
  
  {
    assume ?rhs
    then obtain r where "LTS_is_inf_run (reach⇩t Σ δ q⇩0) w r"
      and "r 0 = q⇩0"
      and "limit (λi. (r i, w i, r (Suc i))) ∩ F = {}"
      and "⋀I. I ∈ ℐ ⟹ limit (λi. (r i, w i, r (Suc i))) ∩ I ≠ {}"
      unfolding accepting_pair⇩G⇩R_LTS_def by auto
    moreover
    {
      fix i
      from ‹r 0 = q⇩0› ‹LTS_is_inf_run (reach⇩t Σ δ q⇩0) w r› have "r i = run δ q⇩0 w i"
        by (induction i; simp_all add: LTS_is_inf_run_def reach⇩t_def) metis
    }
    hence "r = run δ q⇩0 w"
      by blast
    hence "(λi. (r i, w i, r (Suc i))) = run⇩t δ q⇩0 w"
      by auto
    ultimately
    show ?lhs
      by auto
  }
qed

lemma accept⇩G⇩R_LTS:
  assumes "range w ⊆ Σ"
  shows "accept⇩G⇩R (δ, q⇩0, α) w ⟷ accept⇩G⇩R_LTS (reach⇩t Σ δ q⇩0, q⇩0, α) w" 
  unfolding accept⇩G⇩R_def fst_conv snd_conv accepting_pair⇩G⇩R_LTS[OF assms] by simp

lemma accept⇩R_LTS:
  assumes "range w ⊆ Σ"
  shows "accept⇩R (δ, q⇩0, α) w ⟷ accept⇩R_LTS (reach⇩t Σ δ q⇩0, q⇩0, α) w"
  unfolding transfer_accept accept⇩G⇩R_LTS.simps accept⇩R_LTS.simps accept⇩G⇩R_LTS[OF assms] case_prod_unfold accepting_pair⇩G⇩R_LTS_def by simp

subsection ‹Combination Lemmas›

lemma combine_rabin_pairs: 
  "(⋀x. x ∈ I ⟹ accepting_pair⇩R δ q⇩0 (f x, g x) w) ⟹ accepting_pair⇩G⇩R δ q⇩0 (⋃{f x | x. x ∈ I}, {g x | x. x ∈ I}) w" 
  by auto

lemma combine_rabin_pairs_UNIV: 
  "accepting_pair⇩R δ q⇩0 (fin, UNIV) w ⟹ accepting_pair⇩G⇩R δ q⇩0 (fin', inf') w ⟹ accepting_pair⇩G⇩R δ q⇩0 (fin ∪ fin', inf') w"
  by auto

end