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