diff --git a/thys/Buchi_Complementation/Complementation.thy b/thys/Buchi_Complementation/Complementation.thy
--- a/thys/Buchi_Complementation/Complementation.thy
+++ b/thys/Buchi_Complementation/Complementation.thy
@@ -1,606 +1,605 @@
section \Complementation\
theory Complementation
imports
"Transition_Systems_and_Automata.Maps"
"Ranking"
begin
subsection \Level Rankings and Complementation States\
type_synonym 'state lr = "'state \ nat"
definition lr_succ :: "('label, 'state) nba \ 'label \ 'state lr \ 'state lr set" where
"lr_succ A a f \ {g.
dom g = \ (transition A a ` dom f) \
(\ p \ dom f. \ q \ transition A a p. the (g q) \ the (f p)) \
(\ q \ dom g. accepting A q \ even (the (g q)))}"
type_synonym 'state st = "'state set"
definition st_succ :: "('label, 'state) nba \ 'label \ 'state lr \ 'state st \ 'state st" where
"st_succ A a g P \ {q \ if P = {} then dom g else \ (transition A a ` P). even (the (g q))}"
type_synonym 'state cs = "'state lr \ 'state st"
definition complement_succ :: "('label, 'state) nba \ 'label \ 'state cs \ 'state cs set" where
"complement_succ A a \ \ (f, P). {(g, st_succ A a g P) |g. g \ lr_succ A a f}"
definition complement :: "('label, 'state) nba \ ('label, 'state cs) nba" where
"complement A \ nba
(alphabet A)
({const (Some (2 * card (nodes A))) |` initial A} \ {{}})
(complement_succ A)
(\ (f, P). P = {})"
lemma dom_nodes:
assumes "fP \ nodes (complement A)"
shows "dom (fst fP) \ nodes A"
using assms unfolding complement_def complement_succ_def lr_succ_def by (induct) (auto, blast)
lemma ran_nodes:
assumes "fP \ nodes (complement A)"
shows "ran (fst fP) \ {0 .. 2 * card (nodes A)}"
using assms
proof induct
case (initial fP)
show ?case
using initial unfolding complement_def by (auto) (metis eq_refl option.inject ran_restrictD)
next
case (execute fP agQ)
obtain f P where 1: "fP = (f, P)" by force
have 2: "ran f \ {0 .. 2 * card (nodes A)}" using execute(2) unfolding 1 by auto
obtain a g Q where 3: "agQ = (a, (g, Q))" using prod_cases3 by this
have 4: "p \ dom f \ q \ transition A a p \ the (g q) \ the (f p)" for p q
using execute(3)
unfolding 1 3 complement_def nba.simps complement_succ_def lr_succ_def
by simp
have 8: "dom g = \((transition A a) ` (dom f))"
using execute(3)
unfolding 1 3 complement_def nba.simps complement_succ_def lr_succ_def
by simp
show ?case
unfolding 1 3 ran_def
proof safe
fix q k
assume 5: "fst (snd (a, (g, Q))) q = Some k"
have 6: "q \ dom g" using 5 by auto
obtain p where 7: "p \ dom f" "q \ transition A a p" using 6 unfolding 8 by auto
have "k = the (g q)" using 5 by auto
also have "\ \ the (f p)" using 4 7 by this
also have "\ \ 2 * card (nodes A)" using 2 7(1) by (simp add: domD ranI subset_eq)
finally show "k \ {0 .. 2 * card (nodes A)}" by auto
qed
qed
lemma states_nodes:
assumes "fP \ nodes (complement A)"
shows "snd fP \ nodes A"
using assms
proof induct
case (initial fP)
show ?case using initial unfolding complement_def by auto
next
case (execute fP agQ)
obtain f P where 1: "fP = (f, P)" by force
have 2: "P \ nodes A" using execute(2) unfolding 1 by auto
obtain a g Q where 3: "agQ = (a, (g, Q))" using prod_cases3 by this
have 11: "a \ alphabet A" using execute(3) unfolding 3 complement_def by auto
have 10: "(g, Q) \ nodes (complement A)" using execute(1, 3) unfolding 1 3 by auto
have 4: "dom g \ nodes A" using dom_nodes[OF 10] by simp
have 5: "\ (transition A a ` P) \ nodes A" using 2 11 by auto
have 6: "Q \ nodes A"
using execute(3)
unfolding 1 3 complement_def nba.simps complement_succ_def st_succ_def
using 4 5
by (auto split: if_splits)
show ?case using 6 unfolding 3 by auto
qed
theorem complement_finite:
assumes "finite (nodes A)"
shows "finite (nodes (complement A))"
proof -
let ?lrs = "{f. dom f \ nodes A \ ran f \ {0 .. 2 * card (nodes A)}}"
have 1: "finite ?lrs" using finite_set_of_finite_maps' assms by auto
let ?states = "Pow (nodes A)"
have 2: "finite ?states" using assms by simp
have "nodes (complement A) \ ?lrs \ ?states" by (force dest: dom_nodes ran_nodes states_nodes)
also have "finite \" using 1 2 by simp
finally show ?thesis by this
qed
lemma complement_trace_snth:
assumes "run (complement A) (w ||| r) p"
defines "m \ p ## trace (w ||| r) p"
obtains
"fst (m !! Suc k) \ lr_succ A (w !! k) (fst (m !! k))"
"snd (m !! Suc k) = st_succ A (w !! k) (fst (m !! Suc k)) (snd (m !! k))"
proof
have 1: "r !! k \ transition (complement A) (w !! k) (m !! k)" using nba.run_snth assms by force
show "fst (m !! Suc k) \ lr_succ A (w !! k) (fst (m !! k))"
using assms(2) 1 unfolding complement_def complement_succ_def nba.trace_alt_def by auto
show "snd (m !! Suc k) = st_succ A (w !! k) (fst (m !! Suc k)) (snd (m !! k))"
using assms(2) 1 unfolding complement_def complement_succ_def nba.trace_alt_def by auto
qed
subsection \Word in Complement Language Implies Ranking\
lemma complement_ranking:
assumes "w \ language (complement A)"
obtains f
where "ranking A w f"
proof -
obtain r p where 1:
"run (complement A) (w ||| r) p"
"p \ initial (complement A)"
"infs (accepting (complement A)) (p ## r)"
using assms by rule
let ?m = "p ## r"
obtain 100:
"fst (?m !! Suc k) \ lr_succ A (w !! k) (fst (?m !! k))"
"snd (?m !! Suc k) = st_succ A (w !! k) (fst (?m !! Suc k)) (snd (?m !! k))"
for k using complement_trace_snth 1(1) unfolding nba.trace_alt_def szip_smap_snd by metis
define f where "f \ \ (k, q). the (fst (?m !! k) q)"
define P where "P k \ snd (?m !! k)" for k
have 2: "snd v \ dom (fst (?m !! fst v))" if "v \ gunodes A w" for v
using that
proof induct
case (initial v)
then show ?case using 1(2) unfolding complement_def by auto
next
case (execute v u)
- have "snd u \ \ ((transition A (w !! fst v)) ` (dom (fst (?m !! fst v))))"
+ have "snd u \ \ (transition A (w !! fst v) ` dom (fst (?m !! fst v)))"
using execute(2, 3) by auto
also have "\ = dom (fst (?m !! Suc (fst v)))"
using 100 unfolding lr_succ_def by simp
also have "Suc (fst v) = fst u" using execute(3) by auto
finally show ?case by this
qed
have 3: "f u \ f v" if 10: "v \ gunodes A w" and 11: "u \ gusuccessors A w v" for u v
proof -
have 15: "snd u \ transition A (w !! fst v) (snd v)" using 11 by auto
have 16: "snd v \ dom (fst (?m !! fst v))" using 2 10 by this
have "f u = the (fst (?m !! fst u) (snd u))" unfolding f_def by (simp add: case_prod_beta)
also have "fst u = Suc (fst v)" using 11 by auto
also have "the (fst (?m !! \) (snd u)) \ the (fst (?m !! fst v) (snd v))"
using 100 15 16 unfolding lr_succ_def by auto
also have "\ = f v" unfolding f_def by (simp add: case_prod_beta)
finally show "f u \ f v" by this
qed
have 4: "\ l \ k. P l = {}" for k
proof -
have 15: "infs (\ (k, P). P = {}) ?m" using 1(3) unfolding complement_def by auto
obtain l where 17: "l \ k" "snd (?m !! l) = {}" using 15 unfolding infs_snth by force
have 19: "P l = {}" unfolding P_def using 17 by auto
show ?thesis using 19 17(1) by auto
qed
show ?thesis
proof (rule that, unfold ranking_def, intro conjI ballI impI allI)
fix v
assume "v \ gunodes A w"
then show "f v \ 2 * card (nodes A)"
proof induct
case (initial v)
then show ?case using 1(2) unfolding complement_def f_def by auto
next
case (execute v u)
have "f u \ f v" using 3[OF execute(1)] execute(3) by simp
also have "\ \ 2 * card (nodes A)" using execute(2) by this
finally show ?case by this
qed
next
fix v u
assume 10: "v \ gunodes A w"
assume 11: "u \ gusuccessors A w v"
show "f u \ f v" using 3 10 11 by this
next
fix v
assume 10: "v \ gunodes A w"
assume 11: "gaccepting A v"
show "even (f v)"
using 10
proof cases
case (initial)
then show ?thesis using 1(2) unfolding complement_def f_def by auto
next
case (execute u)
have 12: "snd v \ dom (fst (?m !! fst v))" using execute graph.nodes.execute 2 by blast
have 12: "snd v \ dom (fst (?m !! Suc (fst u)))" using 12 execute(2) by auto
have 13: "accepting A (snd v)" using 11 by auto
have "f v = the (fst (?m !! fst v) (snd v))" unfolding f_def by (simp add: case_prod_beta)
also have "fst v = Suc (fst u)" using execute(2) by auto
also have "even (the (fst (?m !! Suc (fst u)) (snd v)))"
using 100 12 13 unfolding lr_succ_def by simp
finally show ?thesis by this
qed
next
fix v s k
assume 10: "v \ gunodes A w"
assume 11: "gurun A w s v"
assume 12: "smap f (gtrace s v) = sconst k"
show "odd k"
proof
assume 13: "even k"
obtain t u where 14: "u \ ginitial A" "gupath A w t u" "v = gtarget t u" using 10 by auto
obtain l where 15: "l \ length t" "P l = {}" using 4 by auto
- obtain l' where 16: "l' \ Suc l" "P l' = {}" using 4 by auto
have 30: "gurun A w (t @- s) u" using 11 14 by auto
have 21: "fst (gtarget (stake (Suc l) (t @- s)) u) = Suc l" for l
unfolding sscan_snth[symmetric] using 30 14(1) by (auto elim!: grun_elim)
have 17: "snd (gtarget (stake (Suc l + i) (t @- s)) u) \ P (Suc l + i)" for i
proof (induct i)
case (0)
have 20: "gtarget (stake (Suc l) (t @- s)) u \ gunodes A w"
using 14 11 by (force simp add: 15(1) le_SucI graph.run_stake stake_shift)
have "snd (gtarget (stake (Suc l) (t @- s)) u) \
dom (fst (?m !! fst (gtarget (stake (Suc l) (t @- s)) u)))"
using 2[OF 20] by this
also have "fst (gtarget (stake (Suc l) (t @- s)) u) = Suc l" using 21 by this
finally have 22: "snd (gtarget (stake (Suc l) (t @- s)) u) \ dom (fst (?m !! Suc l))" by this
have "gtarget (stake (Suc l) (t @- s)) u = gtrace (t @- s) u !! l" unfolding sscan_snth by rule
also have "\ = gtrace s v !! (l - length t)" using 15(1) by simp
also have "f \ = smap f (gtrace s v) !! (l - length t)" by simp
also have "smap f (gtrace s v) = sconst k" unfolding 12 by rule
also have "sconst k !! (l - length t) = k" by simp
finally have 23: "even (f (gtarget (stake (Suc l) (t @- s)) u))" using 13 by simp
- have 24: "snd (gtarget (stake (Suc l) (t @- s)) u) \
+ have "snd (gtarget (stake (Suc l) (t @- s)) u) \
{p \ dom (fst (?m !! Suc l)). even (f (Suc l, p))}"
using 21 22 23 by (metis (mono_tags, lifting) mem_Collect_eq prod.collapse)
also have "\ = st_succ A (w !! l) (fst (?m !! Suc l)) (P l)"
unfolding 15(2) st_succ_def f_def by simp
also have "\ = P (Suc l)" using 100(2) unfolding P_def by rule
- also have "P (Suc l) = P (l + Suc 0)" by simp
finally show ?case by auto
next
case (Suc i)
have 20: "P (Suc l + i) \ {}" using Suc by auto
have 21: "fst (gtarget (stake (Suc l + Suc i) (t @- s)) u) = Suc l + Suc i"
using 21 by (simp add: stake_shift)
have "gtarget (stake (Suc l + Suc i) (t @- s)) u = gtrace (t @- s) u !! (l + Suc i)"
unfolding sscan_snth by simp
also have "\ \ gusuccessors A w (gtarget (stake (Suc (l + i)) (t @- s)) u)"
using graph.run_snth[OF 30, of "l + Suc i"] by simp
finally have 220: "snd (gtarget (stake (Suc (Suc l + i)) (t @- s)) u) \
transition A (w !! (Suc l + i)) (snd (gtarget (stake (Suc (l + i)) (t @- s)) u))"
using 21 by auto
have 22: "snd (gtarget (stake (Suc l + Suc i) (t @- s)) u) \
\ (transition A (w !! (Suc l + i)) ` P (Suc l + i))" using 220 Suc by auto
have "gtarget (stake (Suc l + Suc i) (t @- s)) u = gtrace (t @- s) u !! (l + Suc i)"
unfolding sscan_snth by simp
also have "\ = gtrace s v !! (l + Suc i - length t)" using 15(1)
by (metis add.commute shift_snth_ge sscan_const trans_le_add2)
also have "f \ = smap f (gtrace s v) !! (l + Suc i - length t)" by simp
also have "smap f (gtrace s v) = sconst k" unfolding 12 by rule
also have "sconst k !! (l + Suc i - length t) = k" by simp
finally have 23: "even (f (gtarget (stake (Suc l + Suc i) (t @- s)) u))" using 13 by auto
have "snd (gtarget (stake (Suc l + Suc i) (t @- s)) u) \
{p \ \ (transition A (w !! (Suc l + i)) ` P (Suc l + i)). even (f (Suc (Suc l + i), p))}"
using 21 22 23 by (metis (mono_tags) add_Suc_right mem_Collect_eq prod.collapse)
also have "\ = st_succ A (w !! (Suc l + i)) (fst (?m !! Suc (Suc l + i))) (P (Suc l + i))"
unfolding st_succ_def f_def using 20 by simp
also have "\ = P (Suc (Suc l + i))" unfolding 100(2)[folded P_def] by rule
also have "\ = P (Suc l + Suc i)" by simp
finally show ?case by this
qed
+ obtain l' where 16: "l' \ Suc l" "P l' = {}" using 4 by auto
show "False" using 16 17 using nat_le_iff_add by auto
qed
qed
qed
subsection \Ranking Implies Word in Complement Language\
definition reach where
"reach A w i \ {target r p |r p. path A r p \ p \ initial A \ map fst r = stake i w}"
lemma reach_0[simp]: "reach A w 0 = initial A" unfolding reach_def by auto
lemma reach_Suc_empty:
assumes "w !! n \ alphabet A"
shows "reach A w (Suc n) = {}"
proof safe
fix q
assume 1: "q \ reach A w (Suc n)"
obtain r p where 2: "q = target r p" "path A r p" "p \ initial A" "map fst r = stake (Suc n) w"
using 1 unfolding reach_def by blast
have 3: "path A (take n r @ drop n r) p" using 2(2) by simp
have 4: "map fst r = stake n w @ [w !! n]" using 2(4) stake_Suc by auto
have 5: "map snd r = take n (map snd r) @ [q]" using 2(1, 4) 4
by (metis One_nat_def Suc_inject Suc_neq_Zero Suc_pred append.right_neutral
append_eq_conv_conj drop_map id_take_nth_drop last_ConsR last_conv_nth length_0_conv
length_map length_stake lessI nba.target_alt_def nba.states_alt_def zero_less_Suc)
have 6: "drop n r = [(w !! n, q)]" using 4 5
by (metis append_eq_conv_conj append_is_Nil_conv append_take_drop_id drop_map
length_greater_0_conv length_stake stake_cycle_le stake_invert_Nil
take_map zip_Cons_Cons zip_map_fst_snd)
show "q \ {}" using assms 3 unfolding 6 by auto
qed
lemma reach_Suc_succ:
assumes "w !! n \ alphabet A"
- shows "reach A w (Suc n) = \((transition A (w !! n) ` (reach A w n)))"
+ shows "reach A w (Suc n) = \ (transition A (w !! n) ` reach A w n)"
proof safe
fix q
assume 1: "q \ reach A w (Suc n)"
obtain r p where 2: "q = target r p" "path A r p" "p \ initial A" "map fst r = stake (Suc n) w"
using 1 unfolding reach_def by blast
have 3: "path A (take n r @ drop n r) p" using 2(2) by simp
have 4: "map fst r = stake n w @ [w !! n]" using 2(4) stake_Suc by auto
have 5: "map snd r = take n (map snd r) @ [q]" using 2(1, 4) 4
by (metis One_nat_def Suc_inject Suc_neq_Zero Suc_pred append.right_neutral
append_eq_conv_conj drop_map id_take_nth_drop last_ConsR last_conv_nth length_0_conv
length_map length_stake lessI nba.target_alt_def nba.states_alt_def zero_less_Suc)
have 6: "drop n r = [(w !! n, q)]" using 4 5
by (metis append_eq_conv_conj append_is_Nil_conv append_take_drop_id drop_map
length_greater_0_conv length_stake stake_cycle_le stake_invert_Nil
take_map zip_Cons_Cons zip_map_fst_snd)
show "q \ \((transition A (w !! n) ` (reach A w n)))"
unfolding reach_def
proof (intro UN_I CollectI exI conjI)
show "target (take n r) p = target (take n r) p" by rule
show "path A (take n r) p" using 3 by blast
show "p \ initial A" using 2(3) by this
show "map fst (take n r) = stake n w" using 2 by (metis length_stake lessI nat.distinct(1)
stake_cycle_le stake_invert_Nil take_map take_stake)
show "q \ transition A (w !! n) (target (take n r) p)" using 3 unfolding 6 by auto
qed
next
fix p q
assume 1: "p \ reach A w n" "q \ transition A (w !! n) p"
obtain r x where 2: "p = target r x" "path A r x" "x \ initial A" "map fst r = stake n w"
using 1(1) unfolding reach_def by blast
show "q \ reach A w (Suc n)"
unfolding reach_def
proof (intro CollectI exI conjI)
show "q = target (r @ [(w !! n, q)]) x" using 1 2 by auto
show "path A (r @ [(w !! n, q)]) x" using assms 1(2) 2(1, 2) by auto
show "x \ initial A" using 2(3) by this
show "map fst (r @ [(w !! n, q)]) = stake (Suc n) w" using 1 2
by (metis eq_fst_iff list.simps(8) list.simps(9) map_append stake_Suc)
qed
qed
lemma reach_Suc[simp]: "reach A w (Suc n) = (if w !! n \ alphabet A
- then \((transition A (w !! n) ` (reach A w n))) else {})"
+ then \ (transition A (w !! n) ` reach A w n) else {})"
using reach_Suc_empty reach_Suc_succ by metis
lemma reach_nodes: "reach A w i \ nodes A" by (induct i) (auto)
lemma reach_gunodes: "{i} \ reach A w i \ gunodes A w"
by (induct i) (auto intro: graph.nodes.execute)
lemma ranking_complement:
assumes "finite (nodes A)" "w \ streams (alphabet A)" "ranking A w f"
shows "w \ language (complement A)"
proof -
define f' where "f' \ \ (k, p). if k = 0 then 2 * card (nodes A) else f (k, p)"
have 0: "ranking A w f'"
unfolding ranking_def
proof (intro conjI ballI impI allI)
show "\ v. v \ gunodes A w \ f' v \ 2 * card (nodes A)"
using assms(3) unfolding ranking_def f'_def by auto
show "\ v u. v \ gunodes A w \ u \ gusuccessors A w v \ f' u \ f' v"
using assms(3) unfolding ranking_def f'_def by fastforce
show "\ v. v \ gunodes A w \ gaccepting A v \ even (f' v)"
using assms(3) unfolding ranking_def f'_def by auto
next
have 1: "v \ gunodes A w \ gurun A w r v \ smap f (gtrace r v) = sconst k \ odd k"
for v r k using assms(3) unfolding ranking_def by meson
fix v r k
assume 2: "v \ gunodes A w" "gurun A w r v" "smap f' (gtrace r v) = sconst k"
have 20: "shd r \ gureachable A w v" using 2
by (auto) (metis graph.reachable.reflexive graph.reachable_trace gtrace_alt_def subsetD shd_sset)
obtain 3:
"shd r \ gunodes A w"
"gurun A w (stl r) (shd r)"
"smap f' (gtrace (stl r) (shd r)) = sconst k"
using 2 20 by (metis (no_types, lifting) eq_id_iff graph.nodes_trans graph.run_scons_elim
siterate.simps(2) sscan.simps(2) stream.collapse stream.map_sel(2))
have 4: "k \ 0" if "(k, p) \ sset r" for k p
proof -
obtain ra ka pa where 1: "r = fromN (Suc ka) ||| ra" "v = (ka, pa)"
using grun_elim[OF 2(2)] by this
have 2: "k \ sset (fromN (Suc ka))" using 1(1) that
by (metis image_eqI prod.sel(1) szip_smap_fst stream.set_map)
show ?thesis using 2 by simp
qed
have 5: "smap f' (gtrace (stl r) (shd r)) = smap f (gtrace (stl r) (shd r))"
proof (rule stream.map_cong)
show "gtrace (stl r) (shd r) = gtrace (stl r) (shd r)" by rule
next
fix z
assume 1: "z \ sset (gtrace (stl r) (shd r))"
have 2: "fst z \ 0" using 4 1 by (metis gtrace_alt_def prod.collapse stl_sset)
show "f' z = f z" using 2 unfolding f'_def by (auto simp: case_prod_beta)
qed
show "odd k" using 1 3 5 by simp
qed
define g where "g i p \ if p \ reach A w i then Some (f' (i, p)) else None" for i p
have g_dom[simp]: "dom (g i) = reach A w i" for i
unfolding g_def by (auto) (metis option.simps(3))
have g_0[simp]: "g 0 = const (Some (2 * card (nodes A))) |` initial A"
unfolding g_def f'_def by auto
have g_Suc[simp]: "g (Suc n) \ lr_succ A (w !! n) (g n)" for n
unfolding lr_succ_def
proof (intro CollectI conjI ballI impI)
show "dom (g (Suc n)) = \ (transition A (w !! n) ` dom (g n))" using snth_in assms(2) by auto
next
fix p q
assume 100: "p \ dom (g n)" "q \ transition A (w !! n) p"
have 101: "q \ reach A w (Suc n)" using snth_in assms(2) 100 by auto
have 102: "(n, p) \ gunodes A w" using 100(1) reach_gunodes g_dom by blast
have 103: "(Suc n, q) \ gusuccessors A w (n, p)" using snth_in assms(2) 102 100(2) by auto
have 104: "p \ reach A w n" using 100(1) by simp
have "g (Suc n) q = Some (f' (Suc n, q))" using 101 unfolding g_def by simp
also have "the \ = f' (Suc n, q)" by simp
also have "\ \ f' (n, p)" using 0 unfolding ranking_def using 102 103 by simp
also have "\ = the (Some (f' (n, p)))" by simp
also have "Some (f' (n, p)) = g n p" using 104 unfolding g_def by simp
finally show "the (g (Suc n) q) \ the (g n p)" by this
next
fix p
assume 100: "p \ dom (g (Suc n))" "accepting A p"
have 101: "p \ reach A w (Suc n)" using 100(1) by simp
have 102: "(Suc n, p) \ gunodes A w" using 101 reach_gunodes by blast
have 103: "gaccepting A (Suc n, p)" using 100(2) by simp
have "the (g (Suc n) p) = f' (Suc n, p)" using 101 unfolding g_def by simp
also have "even \" using 0 unfolding ranking_def using 102 103 by auto
finally show "even (the (g (Suc n) p))" by this
qed
define P where "P \ rec_nat {} (\ n. st_succ A (w !! n) (g (Suc n)))"
have P_0[simp]: "P 0 = {}" unfolding P_def by simp
have P_Suc[simp]: "P (Suc n) = st_succ A (w !! n) (g (Suc n)) (P n)" for n
unfolding P_def by simp
have P_reach: "P n \ reach A w n" for n
using snth_in assms(2) by (induct n) (auto simp add: st_succ_def)
have "P n \ reach A w n" for n using P_reach by auto
also have "\ n \ nodes A" for n using reach_nodes by this
also have "finite (nodes A)" using assms(1) by this
finally have P_finite: "finite (P n)" for n by this
define s where "s \ smap g nats ||| smap P nats"
show ?thesis
proof
show "run (complement A) (w ||| stl s) (shd s)"
proof (intro nba.snth_run conjI, simp_all del: stake.simps stake_szip)
fix k
show "w !! k \ alphabet (complement A)" using snth_in assms(2) unfolding complement_def by auto
have "stl s !! k = s !! Suc k" by simp
also have "\ \ complement_succ A (w !! k) (s !! k)"
unfolding complement_succ_def s_def using P_Suc by simp
also have "\ = complement_succ A (w !! k) (target (stake k (w ||| stl s)) (shd s))"
unfolding sscan_scons_snth[symmetric] nba.trace_alt_def by simp
also have "\ = transition (complement A) (w !! k) (target (stake k (w ||| stl s)) (shd s))"
unfolding complement_def nba.sel by rule
finally show "stl s !! k \
transition (complement A) (w !! k) (target (stake k (w ||| stl s)) (shd s))" by this
qed
show "shd s \ initial (complement A)" unfolding complement_def s_def using P_0 by simp
show "infs (accepting (complement A)) (shd s ## stl s)"
proof -
have 10: "\ n. \ k \ n. P k = {}"
proof (rule ccontr)
assume 20: "\ (\ n. \ k \ n. P k = {})"
obtain k where 22: "P (k + n) \ {}" for n using 20 using le_add1 by blast
- define m where "m n S \ {p \ \((transition A (w !! n) ` S)). even (the (g (Suc n) p))}" for n S
+ define m where "m n S \ {p \ \ (transition A (w !! n) ` S). even (the (g (Suc n) p))}" for n S
define R where "R i n S \ rec_nat S (\ i. m (n + i)) i" for i n S
have R_0[simp]: "R 0 n = id" for n unfolding R_def by auto
have R_Suc[simp]: "R (Suc i) n = m (n + i) \ R i n" for i n unfolding R_def by auto
have R_Suc': "R (Suc i) n = R i (Suc n) \