# 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_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
```