Theory Rabin

theory Rabin
imports DTS
(*  
    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_pairR :: "('a, 'b) DTS ⇒ 'a ⇒ ('a, 'b) rabin_pair ⇒ 'b word ⇒ bool"
where
  "accepting_pairR δ q0 P w ≡ limit (runt δ q0 w) ∩ fst P = {} ∧ limit (runt δ q0 w) ∩ snd P ≠ {}"

definition acceptR :: "('a, 'b) rabin_automaton ⇒ 'b word ⇒ bool"
where 
  "acceptR R w ≡ (∃P ∈ (snd (snd R)). accepting_pairR (fst R) (fst (snd R)) P w)"

definition accepting_pairGR :: "('a, 'b) DTS ⇒ 'a ⇒ ('a, 'b) generalized_rabin_pair ⇒ 'b word ⇒ bool"
where
  "accepting_pairGR δ q0 P w ≡ limit (runt δ q0 w) ∩ fst P = {} ∧ (∀I ∈ snd P. limit (runt δ q0 w) ∩ I ≠ {})"

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

declare accepting_pairR_def[simp]
declare accepting_pairGR_def[simp]

lemma accepting_pairR_simp[simp]:
  "accepting_pairR δ q0 (F,I) w ≡ limit (runt δ q0 w) ∩ F = {} ∧ limit (runt δ q0 w) ∩ I ≠ {}"
  by simp

lemma accepting_pairGR_simp[simp]:
  "accepting_pairGR δ q0 (F, ℐ) w ≡ limit (runt δ q0 w) ∩ F = {} ∧ (∀I ∈ ℐ. limit (runt δ q0 w) ∩ I ≠ {})"
  by simp

lemma acceptR_simp[simp]:
  "acceptR (δ, q0, α) w = (∃(Fin, Inf) ∈ α. limit (runt δ q0 w) ∩ Fin = {} ∧ limit (runt δ q0 w) ∩ Inf ≠ {})"
  by (unfold acceptR_def accepting_pairR_def case_prod_unfold fst_conv snd_conv; rule)

lemma acceptGR_simp[simp]: 
  "acceptGR (δ, q0, α) w ⟷ (∃(Fin, Inf) ∈ α. limit (runt δ q0 w) ∩ Fin = {} ∧ (∀I ∈ Inf. limit (runt δ q0 w) ∩ I ≠ {}))"
  by (unfold acceptGR_def accepting_pairGR_def case_prod_unfold fst_conv snd_conv; rule)

lemma acceptGR_simp2: 
  "acceptGR (δ, q0, α) w ⟷ (∃P ∈ α. accepting_pairGR δ q0 P w)"
  by (unfold acceptGR_def accepting_pairGR_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 acceptR_LTS :: "(('a, 'b) LTS × 'a × ('a, 'b) rabin_condition) ⇒ 'b word ⇒ bool"
where 
  "acceptR_LTS (δ, q0, α) w ⟷ (∃(Fin, Inf) ∈ α. ∃r. 
      LTS_is_inf_run δ w r ∧ r 0 = q0 
    ∧ limit (λi. (r i, w i, r (Suc i))) ∩ Fin = {} 
    ∧ limit (λi. (r i, w i, r (Suc i))) ∩ Inf ≠ {})"

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

lemma acceptGR_LTS_E:
  assumes "acceptGR_LTS R w"
  obtains F I where "(F, I) ∈ snd (snd R)"
   and "accepting_pairGR_LTS (fst R) (fst (snd R)) (F, I) w"
proof -
  obtain δ q0 α where "R = (δ, q0, α)"
    using prod_cases3 by blast
  show "(⋀F I. (F, I) ∈ snd (snd R) ⟹ accepting_pairGR_LTS (fst R) (fst (snd R)) (F, I) w ⟹ thesis) ⟹ thesis"
    using assms unfolding ‹R = (δ, q0, α)› by auto
qed

lemma acceptGR_LTS_I:
  "accepting_pairGR_LTS δ q0 (F, ℐ) w ⟹ (F, ℐ) ∈ α ⟹ acceptGR_LTS (δ, q0, α) w"
  by auto

lemma acceptGR_I:
  "accepting_pairGR δ q0 (F, ℐ) w ⟹ (F, ℐ) ∈ α ⟹ acceptGR (δ, q0, α) w"
  by auto

lemma transfer_accept:
  "accepting_pairR δ q0 (F, I) w ⟷ accepting_pairGR δ q0 (F, {I}) w"
  "acceptR (δ, q0, α) w ⟷ acceptGR (δ, q0, (λ(F, I). (F, {I})) ` α) w"
  by (simp add: case_prod_unfold)+

subsection ‹Restriction Lemmas›

lemma accepting_pairGR_restrict:
  assumes "range w ⊆ Σ"
  shows "accepting_pairGR δ q0 (F, ℐ) w = accepting_pairGR δ q0 (F ∩ reacht Σ δ q0, (λI. I ∩ reacht Σ δ q0) ` ℐ) w"
proof -
  have "limit (runt δ q0 w) ∩ F = {} ⟷ limit (runt δ q0 w) ∩ (F ∩ reacht Σ δ q0) = {}"
    using assms[THEN limit_subseteq_reach(2), of δ q0] by auto
  moreover
  have "(∀I∈ℐ. limit (runt δ q0 w) ∩ I ≠ {}) = ((∀I∈{y. ∃x∈ℐ. y = x ∩ reacht Σ δ q0}. limit (runt δ q0 w) ∩ I ≠ {}))"
     using assms[THEN limit_subseteq_reach(2), of δ q0] by auto
  ultimately
  show ?thesis
    unfolding accepting_pairGR_simp image_def by meson
qed

lemma acceptGR_restrict:
  assumes "range w ⊆ Σ"
  shows "acceptGR (δ, q0, {(f x, g x) | x. P x}) w = acceptGR (δ, q0, {(f x ∩ reacht Σ δ q0, (λI. I ∩ reacht Σ δ q0) ` g x) | x. P x}) w"
  apply (simp only: acceptGR_simp)  
  apply (subst accepting_pairGR_restrict[OF assms, simplified]) 
  apply simp
  apply standard
  apply (metis (no_types, lifting) imageE) 
  apply fastforce
  done

lemma accepting_pairR_restrict:
  assumes "range w ⊆ Σ"
  shows "accepting_pairR δ q0 (F, I) w = accepting_pairR δ q0 (F ∩ reacht Σ δ q0, I ∩ reacht Σ δ q0) w"
  by (simp only: transfer_accept; subst accepting_pairGR_restrict[OF assms]; simp)

lemma acceptR_restrict:
  assumes "range w ⊆ Σ"
  shows "acceptR (δ, q0, {(f x, g x) | x. P x}) w = acceptR (δ, q0, {(f x ∩ reacht Σ δ q0, g x ∩ reacht Σ δ q0) | x. P x}) w"
  by (simp only: acceptR_simp; subst accepting_pairR_restrict[OF assms, simplified]; auto)

subsection ‹Abstraction Lemmas›

lemma accepting_pairGR_abstract:
  assumes "finite (reacht Σ δ q0)" 
      and "finite (reacht Σ δ' q0')"
  assumes "range w ⊆ Σ"
  assumes "runt δ q0 w = f o (runt δ' q0' w)"
  assumes "⋀t. t ∈ reacht Σ δ' q0' ⟹ f t ∈ F ⟷ t ∈ F'"
  assumes "⋀t i. i ∈ ℐ ⟹ t ∈ reacht Σ δ' q0' ⟹ f t ∈ I i ⟷ t ∈ I' i"
  shows "accepting_pairGR δ q0 (F, {I i | i. i ∈ ℐ}) w ⟷ accepting_pairGR δ' q0' (F', {I' i | i. i ∈ ℐ}) w"
proof -
  have "finite (range (runt δ q0 w))" (is "_ (range ?r)") 
    and "finite (range (runt δ' q0' 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 (runt δ q0 w) = f ` limit (runt δ' q0' 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_pairGR_simp by blast
qed

lemma accepting_pairR_abstract:
  assumes "finite (reacht Σ δ q0)" 
      and "finite (reacht Σ δ' q0')"
  assumes "range w ⊆ Σ"
  assumes "runt δ q0 w  = f o (runt δ' q0' w)"
  assumes "⋀t. t ∈ reacht Σ δ' q0' ⟹ f t ∈ F ⟷ t ∈ F'"
  assumes "⋀t. t ∈ reacht Σ δ' q0' ⟹ f t ∈ I ⟷ t ∈ I'"
  shows "accepting_pairR δ q0 (F, I) w ⟷ accepting_pairR δ' q0' (F', I') w"
  using accepting_pairGR_abstract[OF assms(1-5), of UNIV "λ_. I" "λ_. I'"] assms(6) by simp

subsection ‹LTS Lemmas›

lemma accepting_pairGR_LTS:
  assumes "range w ⊆ Σ"
  shows "accepting_pairGR δ q0 (F, ℐ) w ⟷ accepting_pairGR_LTS (reacht Σ δ q0) q0 (F, ℐ) w" 
  (is "?lhs ⟷ ?rhs")
proof 
  {
    assume ?lhs
    moreover
    have "LTS_is_inf_run (reacht Σ δ q0) w (run δ q0 w)"
      unfolding LTS_is_inf_run_def reacht_def using assms(1) by auto
    moreover
    have "run δ q0 w 0 = q0"
      by simp
    ultimately
    show ?rhs
      unfolding acceptGR_simp acceptGR_LTS.simps accepting_pairGR_simp runt.simps limit_def accepting_pairGR_LTS_def snd_conv fst_conv by blast
  }
  
  {
    assume ?rhs
    then obtain r where "LTS_is_inf_run (reacht Σ δ q0) w r"
      and "r 0 = q0"
      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_pairGR_LTS_def by auto
    moreover
    {
      fix i
      from ‹r 0 = q0 ‹LTS_is_inf_run (reacht Σ δ q0) w r› have "r i = run δ q0 w i"
        by (induction i; simp_all add: LTS_is_inf_run_def reacht_def) metis
    }
    hence "r = run δ q0 w"
      by blast
    hence "(λi. (r i, w i, r (Suc i))) = runt δ q0 w"
      by auto
    ultimately
    show ?lhs
      by auto
  }
qed

lemma acceptGR_LTS:
  assumes "range w ⊆ Σ"
  shows "acceptGR (δ, q0, α) w ⟷ acceptGR_LTS (reacht Σ δ q0, q0, α) w" 
  unfolding acceptGR_def fst_conv snd_conv accepting_pairGR_LTS[OF assms] by simp

lemma acceptR_LTS:
  assumes "range w ⊆ Σ"
  shows "acceptR (δ, q0, α) w ⟷ acceptR_LTS (reacht Σ δ q0, q0, α) w"
  unfolding transfer_accept acceptGR_LTS.simps acceptR_LTS.simps acceptGR_LTS[OF assms] case_prod_unfold accepting_pairGR_LTS_def by simp

subsection ‹Combination Lemmas›

lemma combine_rabin_pairs: 
  "(⋀x. x ∈ I ⟹ accepting_pairR δ q0 (f x, g x) w) ⟹ accepting_pairGR δ q0 (⋃{f x | x. x ∈ I}, {g x | x. x ∈ I}) w" 
  by auto

lemma combine_rabin_pairs_UNIV: 
  "accepting_pairR δ q0 (fin, UNIV) w ⟹ accepting_pairGR δ q0 (fin', inf') w ⟹ accepting_pairGR δ q0 (fin ∪ fin', inf') w"
  by auto

end