Theory Mojmir_Rabin
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 fail⇩R :: "('b ⇒ nat option, 'a) transition set"
where
"fail⇩R = {(r, ν, s) | r ν s q q'. r q ≠ None ∧ q' = δ q ν ∧ q' ∉ F ∧ sink q'}"
definition succeed⇩R :: "nat ⇒ ('b ⇒ nat option, 'a) transition set"
where
"succeed⇩R i = {(r, ν, s) | r ν s q. r q = Some i ∧ q ∉ F - {q⇩0} ∧ (δ q ν) ∈ F}"
definition merge⇩R :: "nat ⇒ ('b ⇒ nat option, 'a) transition set"
where
"merge⇩R 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' = q⇩0) ∧ q' ∉ F}"
abbreviation Q⇩R
where
"Q⇩R ≡ reach Σ step initial"
abbreviation q⇩ℛ
where
"q⇩ℛ ≡ initial"
abbreviation δ⇩ℛ
where
"δ⇩ℛ ≡ step"
abbreviation Acc⇩ℛ
where
"Acc⇩ℛ j ≡ (fail⇩R ∪ merge⇩R j, succeed⇩R 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 Σ δ q⇩0 ⟶ f x = None) ∧
(∀x. x ∈ reach Σ δ q⇩0 ⟶ 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 Σ δ q⇩0 "(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 ≡ run⇩t δ⇩ℛ 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 ∈ Q⇩R × Σ × Q⇩R"
unfolding run⇩t.simps run_foldl reach_foldl_def[OF nonempty_Σ] r_def
unfolding fst_conv comp_def snd_conv by blast
}
hence "range r ⊆ Q⇩R × Σ × Q⇩R"
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_pair⇩R δ⇩ℛ q⇩ℛ (Acc⇩ℛ i) w"
(is "?lhs = ?rhs")
proof
define r where "r = run⇩t δ⇩ℛ 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) ∈ fail⇩R"
unfolding fail_t_def fail⇩R_def r_alt_def by blast
have B: "⋀x i. x ∈ merge_t i ⟷ (r x) ∈ merge⇩R i"
unfolding merge_t_def merge⇩R_def r_alt_def by blast
have S: "⋀x i. x ∈ succeed_t i ⟷ (r x) ∈ succeed⇩R i"
unfolding succeed_t_def succeed⇩R_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 ∩ fail⇩R = {}"
by (metis finite_limit_rule F ‹finite (fail_t)›)
moreover
have "limit r ∩ merge⇩R i = {}"
by (metis finite_limit_rule B ‹finite (merge_t i)›)
ultimately
have "limit r ∩ fst (Acc⇩ℛ i) = {}"
by auto
moreover
have "limit r ∩ succeed⇩R 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 ∩ fail⇩R = {}" and "limit r ∩ merge⇩R i = {}" and "limit r ∩ (succeed⇩R i) ≠ {}"
unfolding r_def by auto
have "finite fail_t"
by (metis finite_limit_rule F ‹limit r ∩ fail⇩R = {}›)
moreover
have "finite (merge_t i)"
by (metis finite_limit_rule B ‹limit r ∩ merge⇩R i = {}›)
moreover
have "infinite (succeed_t i)"
by (metis finite_limit_rule S ‹limit r ∩ (succeed⇩R i) ≠ {}›)
ultimately
show ?lhs
unfolding finite_fail_t finite_merge_t finite_succeed_t by blast
}
qed
theorem mojmir_accept_iff_rabin_accept:
"accept ⟷ accept⇩R ℛ 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 accept⇩R ℛ w then
Some (LEAST i. accepting_pair⇩R δ⇩ℛ 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_pair⇩R δ⇩ℛ 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