Theory NGBA_Graphs
section ‹Connecting Nondeterministic Generalized Büchi Automata to CAVA Automata Structures›
theory NGBA_Graphs
imports
NGBA
CAVA_Automata.Automata_Impl
begin
no_notation build (infixr "##" 65)
subsection ‹Regular Graphs›
definition ngba_g :: "('label, 'state) ngba ⇒ 'state graph_rec" where
"ngba_g A ≡ ⦇ g_V = UNIV, g_E = E_of_succ (successors A), g_V0 = initial A ⦈"
lemma ngba_g_graph[simp]: "graph (ngba_g A)" unfolding ngba_g_def graph_def by simp
lemma ngba_g_V0: "g_V0 (ngba_g A) = initial A" unfolding ngba_g_def by simp
lemma ngba_g_E_rtrancl: "(g_E (ngba_g A))⇧* = {(p, q). q ∈ reachable A p}"
unfolding ngba_g_def graph_rec.simps E_of_succ_def
proof safe
show "(p, q) ∈ {(p, q). q ∈ successors A p}⇧*" if "q ∈ reachable A p" for p q
using that by (induct) (auto intro: rtrancl_into_rtrancl)
show "q ∈ reachable A p" if "(p, q) ∈ {(p, q). q ∈ successors A p}⇧*" for p q
using that by induct auto
qed
lemma ngba_g_rtrancl_path: "(g_E (ngba_g A))⇧* = {(p, target r p) |r p. NGBA.path A r p}"
unfolding ngba_g_E_rtrancl by blast
lemma ngba_g_trancl_path: "(g_E (ngba_g A))⇧+ = {(p, target r p) |r p. NGBA.path A r p ∧ r ≠ []}"
unfolding ngba_g_def graph_rec.simps E_of_succ_def
proof safe
show "∃ r p. (x, y) = (p, target r p) ∧ NGBA.path A r p ∧ r ≠ []"
if "(x, y) ∈ {(p, q). q ∈ successors A p}⇧+" for x y
using that
proof induct
case (base y)
obtain a where 1: "a ∈ alphabet A" "y ∈ transition A a x" using base by auto
show ?case
proof (intro exI conjI)
show "(x, y) = (x, target [(a, y)] x)" by simp
show "NGBA.path A [(a, y)] x" using 1 by auto
show "[(a, y)] ≠ []" by simp
qed
next
case (step y z)
obtain r where 1: "y = target r x" "NGBA.path A r x" "r ≠ []" using step(3) by auto
obtain a where 2: "a ∈ alphabet A" "z ∈ transition A a y" using step(2) by auto
show ?case
proof (intro exI conjI)
show "(x, z) = (x, target (r @ [(a, z)]) x)" by simp
show "NGBA.path A (r @ [(a, z)]) x" using 1 2 by auto
show "r @ [(a, z)] ≠ []" by simp
qed
qed
show "(p, target r p) ∈ {(u, v). v ∈ successors A u}⇧+" if "NGBA.path A r p" "r ≠ []" for r p
using that by (induct) (fastforce intro: trancl_into_trancl2)+
qed
lemma ngba_g_ipath_run:
assumes "ipath (g_E (ngba_g A)) r"
obtains w
where "run A (w ||| smap (r ∘ Suc) nats) (r 0)"
proof -
have 1: "∃ a ∈ alphabet A. r (Suc i) ∈ transition A a (r i)" for i
using assms unfolding ipath_def ngba_g_def E_of_succ_def by auto
obtain wr where 2: "run A wr (r 0)" "⋀ i. target (stake i wr) (r 0) = r i"
proof (rule ngba.invariant_run_index)
show "∃ aq. (fst aq ∈ alphabet A ∧ snd aq ∈ transition A (fst aq) p) ∧ snd aq = r (Suc i) ∧ True"
if "p = r i" for i p using that 1 by auto
show "r 0 = r 0" by rule
qed auto
have 3: "smap (r ∘ Suc) nats = smap snd wr"
proof (rule eqI_snth)
fix i
have "smap (r ∘ Suc) nats !! i = r (Suc i)" by simp
also have "… = target (stake (Suc i) wr) (r 0)" unfolding 2(2) by rule
also have "… = (r 0 ## trace wr (r 0)) !! Suc i" by simp
also have "… = smap snd wr !! i" unfolding ngba.trace_alt_def by simp
finally show "smap (r ∘ Suc) nats !! i = smap snd wr !! i" by this
qed
show ?thesis
proof
show "run A (smap fst wr ||| smap (r ∘ Suc) nats) (r 0)" using 2(1) unfolding 3 by auto
qed
qed
lemma ngba_g_run_ipath:
assumes "run A (w ||| r) p"
shows "ipath (g_E (ngba_g A)) (snth (p ## r))"
proof
fix i
have 1: "w !! i ∈ alphabet A" "r !! i ∈ transition A (w !! i) (target (stake i (w ||| r)) p)"
using assms by (auto dest: ngba.run_snth)
have 2: "r !! i ∈ successors A ((p ## r) !! i)"
using 1 unfolding sscan_scons_snth[symmetric] ngba.trace_alt_def by auto
show "((p ## r) !! i, (p ## r) !! Suc i) ∈ g_E (ngba_g A)"
using 2 unfolding ngba_g_def graph_rec.simps E_of_succ_def by simp
qed
subsection ‹Indexed Generalized Büchi Graphs›
definition ngba_acc :: "'state pred gen ⇒ 'state ⇒ nat set" where
"ngba_acc cs p ≡ {k ∈ {0 ..< length cs}. (cs ! k) p}"
lemma ngba_acc_param[param]: "(ngba_acc, ngba_acc) ∈ ⟨S → bool_rel⟩ list_rel → S → ⟨nat_rel⟩ set_rel"
unfolding ngba_acc_def list_rel_def list_all2_conv_all_nth fun_rel_def by auto
definition ngba_igbg :: "('label, 'state) ngba ⇒ 'state igb_graph_rec" where
"ngba_igbg A ≡ graph_rec.extend (ngba_g A) ⦇ igbg_num_acc = length (accepting A), igbg_acc = ngba_acc (accepting A) ⦈"
lemma acc_run_language:
assumes "igb_graph (ngba_igbg A)"
shows "Ex (igb_graph.is_acc_run (ngba_igbg A)) ⟷ language A ≠ {}"
proof
interpret igb_graph "ngba_igbg A" using assms by this
have [simp]: "V0 = g_V0 (ngba_g A)" "E = g_E (ngba_g A)" "num_acc = length (accepting A)"
"k ∈ acc p ⟷ k < length (accepting A) ∧ (accepting A ! k) p" for p k
unfolding ngba_igbg_def ngba_acc_def graph_rec.defs by simp+
show "language A ≠ {}" if run: "Ex is_acc_run"
proof -
obtain r where 1: "is_acc_run r" using run by rule
have 2: "r 0 ∈ V0" "ipath E r" "is_acc r"
using 1 unfolding is_acc_run_def graph_defs.is_run_def by auto
obtain w where 3: "run A (w ||| smap (r ∘ Suc) nats) (r 0)" using ngba_g_ipath_run 2(2) by auto
have 4: "r 0 ## smap (r ∘ Suc) nats = smap r nats" by (simp) (metis stream.map_comp smap_siterate)
have 5: "infs (accepting A ! k) (r 0 ## smap (r ∘ Suc) nats)" if "k < length (accepting A)" for k
using 2(3) that unfolding infs_infm is_acc_def 4 by simp
have "w ∈ language A"
proof
show "r 0 ∈ initial A" using ngba_g_V0 2(1) by force
show "run A (w ||| smap (r ∘ Suc) nats) (r 0)" using 3 by this
show "gen infs (accepting A) (r 0 ## smap (r ∘ Suc) nats)"
unfolding gen_def all_set_conv_all_nth using 5 by simp
qed
then show ?thesis by auto
qed
show "Ex is_acc_run" if language: "language A ≠ {}"
proof -
obtain w where 1: "w ∈ language A" using language by auto
obtain r p where 2: "p ∈ initial A" "run A (w ||| r) p" "gen infs (accepting A) (p ## r)" using 1 by rule
have "is_acc_run (snth (p ## r))"
unfolding is_acc_run_def graph_defs.is_run_def
proof safe
show "(p ## r) !! 0 ∈ V0" using ngba_g_V0 2(1) by force
show "ipath E (snth (p ## r))" using ngba_g_run_ipath 2(2) by force
show "is_acc (snth (p ## r))" using 2(3) unfolding gen_def infs_infm is_acc_def by simp
qed
then show ?thesis by auto
qed
qed
end