Theory Mojmir_Rabin

theory Mojmir_Rabin
imports Mojmir Rabin List2
(*  
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹Translation to Deterministic Transition-Based Rabin Automata›

theory Mojmir_Rabin
  imports Main Mojmir Rabin "Auxiliary/List2"
begin

locale mojmir_to_rabin_def = mojmir_def 
begin
  
definition failR :: "('b ⇒ nat option, 'a) transition set"
where
  "failR = {(r, ν, s) | r ν s q q'. r q ≠ None ∧ q' = δ q ν ∧ q' ∉ F ∧ sink q'}"

definition succeedR :: "nat ⇒ ('b ⇒ nat option, 'a) transition set"
where
  "succeedR i = {(r, ν, s) | r ν s q. r q = Some i ∧ q ∉ F - {q0} ∧ (δ q ν) ∈ F}"

definition mergeR :: "nat ⇒ ('b ⇒ nat option, 'a) transition set"
where
  "mergeR i = {(r, ν, s) | r ν s q q' j. r q = Some j ∧ j < i ∧ q' = δ q ν ∧
        ((∃q''. q' = δ q'' ν ∧ r q'' ≠ None ∧ q'' ≠ q) ∨ q' = q0) ∧ q' ∉ F}"

abbreviation QR
where
  "QR ≡ reach Σ step initial"

abbreviation q
where
  "q ≡ initial"

abbreviation δ
where
   ≡ step"

abbreviation Acc
where
  "Acc j ≡ (failR ∪ mergeR j, succeedR j)"

abbreviation 
where
  "ℛ ≡ (δ, q, {Acc j | j. j < max_rank})"

end



subsection ‹Well-formedness›

lemma function_set_finite:
  assumes "finite R"
  assumes "finite A"
  shows "finite {f. (∀x. x ∉ R ⟶ f x = c) ∧ (∀x. x ∈ R ⟶ f x ∈ A)}" (is "finite ?F")
  using assms(1)
proof (induction R rule: finite_induct)
  case empty
    have "{f. (∀x. x ∈ {} ⟶ f x ∈ A) ∧ (∀x. x ∉ {} ⟶ f x = c)} ⊆ {λx. c}"
      by auto
    thus ?case
      using finite_subset by auto
next
  case (insert r R)
    let ?F = "{f. (∀x. x ∉ R ∪ {r} ⟶ f x = c) ∧ (∀x. x ∈ R ∪ {r} ⟶ f x ∈ A)}"
    let ?F' = "{f. (∀x. x ∉ R ⟶ f x = c) ∧ (∀x. x ∈ R ⟶ f x ∈ A)}"
 
    have "?F ⊆ {f(r := a) | f a. f ∈ ?F' ∧ a ∈ A}" (is "_ ⊆ ?X")
    proof 
      fix f
      assume "f ∈ ?F"
      hence "f(r := c) ∈ ?F'" and "f r ∈ A"
        using insert(2) by (simp, blast)
      hence "f(r := c, r := (f r)) ∈ ?X"
        by blast
      thus "f ∈ ?X"
        by simp
    qed
    moreover
    have "finite (?F' × A)"
      using assms(2) insert(3) by simp  
    have "(λ(f,a). f(r:=a)) ` (?F' × A) = ?X"
      by auto
    hence "finite ?X"
      using finite_imageI[OF ‹finite (?F' × A)›, of "(λ(f,a). f(r:=a))"] by presburger
    ultimately
    have "finite ?F"
      by (blast intro: finite_subset)
    thus ?case
      unfolding insert_def by simp
qed

lemma (in semi_mojmir) wellformed_ℛ:
  shows "finite (reach Σ step initial)"
proof (rule finite_subset)
  let ?R = "{f. (∀x. x ∉ reach Σ δ q0 ⟶ f x = None) ∧ 
    (∀x. x ∈ reach Σ δ q0 ⟶ f x ∈ {None} ∪ Some ` {0..<max_rank})}"

  show "reach Σ step initial ⊆ ?R"
  proof
    fix x 
    assume "x ∈ reach Σ step initial"
    then obtain w where x_def: "x = foldl step initial w" and "set w ⊆ Σ"
      unfolding reach_foldl_def[OF nonempty_Σ] by blast
    obtain a where "a ∈ Σ"
      using nonempty_Σ by blast
    have "range (w ⌢ (λi. a)) ⊆ Σ"
      using ‹set w ⊆ Σ› ‹a ∈ Σ› unfolding conc_def by auto
    then interpret : semi_mojmir Σ δ q0 "(w ⌢ (λi. a))"
      using finite_reach finite_Σ by (unfold_locales; simp_all)
    have "x = (λq. ℌ.state_rank q (length w))" 
      unfolding ℌ.state_rank_step_foldl x_def using prefix_conc_length subsequence_def by metis
    thus "x ∈ ?R"
      using ℌ.state_rank_in_function_set by meson
  qed

  have "finite ({None} ∪ Some ` {0..<max_rank})"
    by blast
  thus "finite ?R"
    using finite_reach by (blast intro: function_set_finite)
qed

locale mojmir_to_rabin = mojmir + mojmir_to_rabin_def begin

subsection ‹Correctness›

lemma imp_and_not_imp_eq:
  assumes "P ⟹ Q"
  assumes "¬P ⟹ ¬Q"
  shows "P = Q"
  using assms by blast  

lemma finite_limit_intersection:
  assumes "finite (range f)"
  assumes "⋀x::nat. x ∈ A ⟷ (f x) ∈ B"
  shows "finite A ⟷ limit f ∩ B = {}"
proof (rule imp_and_not_imp_eq)
  assume "finite A"
  {
    fix x
    assume "x > Max (A ∪ {0})"
    moreover
    have "finite (A ∪ {0})"
      using ‹finite A› by simp
    ultimately
    have "x ∉ A"
      using Max.coboundedI 
      by (metis insert_iff insert_is_Un not_le sup.commute)
    hence "f x ∉ B"
      using assms(2) by simp
  }
  hence "f ` {Suc (Max (A ∪ {0}))..} ∩ B = {}"
    by auto
  thus "limit f ∩ B = {}"
    using limit_subset[of f] by blast
next
  assume "infinite A"
  have "f ` A ⊆ B"
    unfolding image_def using assms by auto 
  moreover
  have "finite (range f)"
    using assms(1) unfolding limit_def Inf_many_def by simp  
  hence "finite (f ` A)"
    by (metis infinite_iff_countable_subset subset_UNIV subset_image_iff)
  then obtain y where "y ∈ f ` A" and "∃n. f n = y"
    unfolding Inf_many_def using pigeonhole_infinite[OF ‹infinite A›] by fast
  ultimately
  show "limit f ∩ B ≠ {}"
    using limit_iff_frequent by fast
qed

lemma finite_range_run:
  defines "r ≡ runt δ q w"
  shows "finite (range r)"
proof -
  {
    fix n
    have "⋀n. w n ∈ Σ" and "set (map w [0..<n]) ⊆ Σ" and "set ( map w [0..<Suc n]) ⊆ Σ"
      using bounded_w by auto 
    hence "r n ∈ QR × Σ × QR"
      unfolding runt.simps run_foldl reach_foldl_def[OF nonempty_Σ] r_def 
      unfolding fst_conv comp_def snd_conv by blast
  }
  hence "range r ⊆ QR × Σ × QR"
    by blast
  thus "finite (range r)"
    using finite_Σ wellformed_ℛ 
    by (blast dest: finite_subset)
qed

theorem mojmir_accept_iff_rabin_accept_rank:
  shows "(finite (fail) ∧ finite (merge i) ∧ infinite (succeed  i))
    ⟷ accepting_pairR δ q (Acc i) w"
  (is "?lhs = ?rhs")
proof
  define r where "r = runt δ q w" 
  have r_alt_def: "⋀i. r i = (λq. state_rank q i, w i, λq. state_rank q (Suc i))"
    using r_def state_rank_step_foldl run_foldl by fastforce

  have F: "⋀x. x ∈ fail_t ⟷ (r x) ∈ failR"
    unfolding fail_t_def failR_def r_alt_def by blast
  have B: "⋀x i. x ∈ merge_t i ⟷ (r x) ∈ mergeR i"
    unfolding merge_t_def mergeR_def r_alt_def by blast
  have S: "⋀x i. x ∈ succeed_t i ⟷ (r x) ∈ succeedR i"
    unfolding succeed_t_def succeedR_def r_alt_def by blast

  have "finite (range r)"
    using finite_range_run r_def by simp
  note finite_limit_rule = finite_limit_intersection[OF ‹finite (range r)›]
 
  {
    assume "?lhs"
    hence "finite fail_t" and "finite (merge_t i)" and "infinite (succeed_t i)"
      unfolding finite_fail_t finite_merge_t finite_succeed_t by blast+

    have "limit r ∩ failR = {}"
      by (metis finite_limit_rule F ‹finite (fail_t)›)
    moreover
    have "limit r ∩ mergeR i = {}"
      by (metis finite_limit_rule B ‹finite (merge_t i)›)
    ultimately
    have "limit r ∩ fst (Acc i) = {}"
      by auto
    moreover
    have "limit r ∩ succeedR i ≠ {}"
      by (metis finite_limit_rule S ‹infinite (succeed_t i)›)
    hence "limit r ∩ snd (Acc i) ≠ {}"
      by auto
    ultimately
    show ?rhs
      unfolding r_def by simp
  }

  {
    assume ?rhs
    hence "limit r ∩ failR = {}" and "limit r ∩ mergeR i = {}" and "limit r ∩ (succeedR i) ≠ {}"
      unfolding r_def by auto 

    have "finite fail_t"
      by (metis finite_limit_rule F ‹limit r ∩ failR = {}›)
    moreover
    have "finite (merge_t i)"
      by (metis finite_limit_rule B ‹limit r ∩ mergeR i = {}›)
    moreover
    have "infinite (succeed_t i)"
      by (metis finite_limit_rule S ‹limit r ∩ (succeedR i) ≠ {}›)
    ultimately
    show ?lhs
      unfolding finite_fail_t finite_merge_t finite_succeed_t by blast
  }
qed

theorem mojmir_accept_iff_rabin_accept:
  "accept ⟷ acceptR ℛ w"
  unfolding mojmir_accept_iff_token_set_accept mojmir_accept_iff_rabin_accept_rank by auto

definition smallest_accepting_rank :: "nat option"
where 
  "smallest_accepting_rank ≡ (if acceptR ℛ w then 
    Some (LEAST i. accepting_pairR δ q (Acc i) w) else None)"

theorem Mojmir_rabin_smallest_accepting_rank:
  "smallest_accepting_rank = smallest_accepting_rank"
  by (simp only: smallest_accepting_rank_def smallest_accepting_rank_def 
    mojmir_accept_iff_rabin_accept mojmir_accept_iff_rabin_accept_rank)

lemma smallest_accepting_rank_properties:
  "smallest_accepting_rank = Some i ⟹ accepting_pairR δ q (Acc i) w"
  by (unfold Mojmir_rabin_smallest_accepting_rank[symmetric] mojmir_accept_iff_rabin_accept_rank[symmetric];
      blast dest: smallest_accepting_rank_properties)

end

end