# Theory Alternate

section ‹Alternating Function Iteration›

theory Alternate
imports Main
begin

primrec alternate :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ nat ⇒ ('a ⇒ 'a)" where
"alternate f g 0 = id" | "alternate f g (Suc k) = alternate g f k ∘ f"

lemma alternate_Suc[simp]: "alternate f g (Suc k) = (if even k then f else g) ∘ alternate f g k"
proof (induct k arbitrary: f g)
case (0)
show ?case by simp
next
case (Suc k)
have "alternate f g (Suc (Suc k)) = alternate g f (Suc k) ∘ f" by auto
also have "… = (if even k then g else f) ∘ (alternate g f k ∘ f)" unfolding Suc by auto
also have "… = (if even (Suc k) then f else g) ∘ alternate f g (Suc k)" by auto
finally show ?case by this
qed

declare alternate.simps(2)[simp del]

lemma alternate_antimono:
assumes "⋀ x. f x ≤ x" "⋀ x. g x ≤ x"
shows "antimono (alternate f g)"
proof
fix k l :: nat
assume 1: "k ≤ l"
obtain n where 2: "l = k + n" using le_Suc_ex 1 by auto
have 3: "alternate f g (k + n) ≤ alternate f g k"
proof (induct n)
case (0)
show ?case by simp
next
case (Suc n)
have "alternate f g (k + Suc n) ≤ alternate f g (k + n)" using assms by (auto intro: le_funI)
also have "… ≤ alternate f g k" using Suc by this
finally show ?case by this
qed
show "alternate f g l ≤ alternate f g k" using 3 unfolding 2 by this
qed

end


# Theory Graph

section ‹Run Graphs›

theory Graph
imports "Transition_Systems_and_Automata.NBA"
begin

type_synonym 'state node = "nat × 'state"

abbreviation "ginitial A ≡ {0} × initial A"
abbreviation "gaccepting A ≡ accepting A ∘ snd"

global_interpretation graph: transition_system_initial
"const"
"λ u (k, p). w !! k ∈ alphabet A ∧ u ∈ {Suc k} × transition A (w !! k) p ∩ V"
"λ v. v ∈ ginitial A ∩ V"
for A w V
defines
gpath = graph.path and grun = graph.run and
greachable = graph.reachable and gnodes = graph.nodes
by this

text ‹We disable rules that are degenerate due to @{term "execute = const"}.›
declare graph.reachable.execute[rule del]
declare graph.nodes.execute[rule del]

abbreviation "gtarget ≡ graph.target"
abbreviation "gstates ≡ graph.states"
abbreviation "gtrace ≡ graph.trace"

abbreviation gsuccessors :: "('label, 'state) nba ⇒ 'label stream ⇒
'state node set ⇒ 'state node ⇒ 'state node set" where
"gsuccessors A w V ≡ graph.successors TYPE('label) w A V"

abbreviation "gusuccessors A w ≡ gsuccessors A w UNIV"
abbreviation "gupath A w ≡ gpath A w UNIV"
abbreviation "gurun A w ≡ grun A w UNIV"
abbreviation "gureachable A w ≡ greachable A w UNIV"
abbreviation "gunodes A w ≡ gnodes A w UNIV"

lemma gtarget_alt_def: "gtarget r v = last (v # r)" using fold_const by this
lemma gstates_alt_def: "gstates r v = r" by simp
lemma gtrace_alt_def: "gtrace r v = r" by simp

lemma gpath_elim[elim?]:
assumes "gpath A w V s v"
obtains r k p
where "s = [Suc k ..< Suc k + length r] || r" "v = (k, p)"
proof -
obtain t r where 1: "s = t || r" "length t = length r"
using zip_map_fst_snd[of s] by (metis length_map)
obtain k p where 2: "v = (k, p)" by force
have 3: "t = [Suc k ..< Suc k + length r]"
using assms 1 2
proof (induct arbitrary: t r k p)
case (nil v)
next
case (cons u v s)
have 1: "t || r = (hd t, hd r) # (tl t || tl r)"
by (metis cons.prems(1) hd_Cons_tl neq_Nil_conv zip.simps(1) zip_Cons_Cons zip_Nil)
have 2: "s = tl t || tl r" using cons 1 by simp
have "t = hd t # tl t" using cons(4) by (metis hd_Cons_tl list.simps(3) zip_Nil)
also have "hd t = Suc k" using "1" cons.hyps(1) cons.prems(1) cons.prems(3) by auto
also have "tl t = [Suc (Suc k) ..< Suc (Suc k) + length (tl r)]"
using cons(3)[OF 2] using "1" ‹hd t = Suc k› cons.prems(1) cons.prems(2) by auto
finally show ?case using cons.prems(2) upt_rec by auto
qed
show ?thesis using that 1 2 3 by simp
qed

lemma gpath_path[symmetric]: "path A (stake (length r) (sdrop k w) || r) p ⟷
gpath A w UNIV ([Suc k ..< Suc k + length r] || r) (k, p)"
proof (induct r arbitrary: k p)
case (Nil)
show ?case by auto
next
case (Cons q r)
have 1: "path A (stake (length r) (sdrop (Suc k) w) || r) q ⟷
gpath A w UNIV ([Suc (Suc k) ..< Suc k + length (q # r)] || r) (Suc k, q)"
using Cons[of "Suc k" "q"] by simp
have "stake (length (q # r)) (sdrop k w) || q # r =
(w !! k, q) # (stake (length r) (sdrop (Suc k) w) || r)" by simp
also have "path A … p ⟷
gpath A w UNIV ((Suc k, q) # ([Suc (Suc k) ..< Suc k + length (q # r)] || r)) (k, p)"
using 1 by auto
also have "(Suc k, q) # ([Suc (Suc k) ..< Suc k + length (q # r)] || r) =
Suc k # [Suc (Suc k) ..< Suc k + length (q # r)] || q # r" unfolding zip_Cons_Cons by rule
also have "Suc k # [Suc (Suc k) ..< Suc k + length (q # r)] = [Suc k ..< Suc k + length (q # r)]"
finally show ?case by this
qed

lemma grun_elim[elim?]:
assumes "grun A w V s v"
obtains r k p
where "s = fromN (Suc k) ||| r" "v = (k, p)"
proof -
obtain t r where 1: "s = t ||| r" using szip_smap by metis
obtain k p where 2: "v = (k, p)" by force
have 3: "t = fromN (Suc k)"
using assms unfolding 1 2
by (coinduction arbitrary: t r k p) (force iff: eq_scons elim: graph.run.cases)
show ?thesis using that 1 2 3 by simp
qed

lemma run_grun:
assumes "run A (sdrop k w ||| r) p"
shows "gurun A w (fromN (Suc k) ||| r) (k, p)"
using assms by (coinduction arbitrary: k p r) (auto elim: nba.run.cases)

lemma grun_run:
assumes "grun A w V (fromN (Suc k) ||| r) (k, p)"
shows "run A (sdrop k w ||| r) p"
proof -
have 2: "∃ ka wa. sdrop k (stl w :: 'a stream) = sdrop ka wa ∧ P ka wa" if "P (Suc k) w" for P k w
using that by (metis sdrop.simps(2))
show ?thesis using assms by (coinduction arbitrary: k p w r) (auto intro!: 2 elim: graph.run.cases)
qed

lemma greachable_reachable:
fixes l q k p
defines "u ≡ (l, q)"
defines "v ≡ (k, p)"
assumes "u ∈ greachable A w V v"
shows "q ∈ reachable A p"
using assms(3, 1, 2)
proof (induct arbitrary: l q k p)
case reflexive
then show ?case by auto
next
case (execute u)
have 1: "q ∈ successors A (snd u)" using execute by auto
have "snd u ∈ reachable A p" using execute by auto
also have "q ∈ reachable A (snd u)" using 1 by blast
finally show ?case by this
qed

lemma gnodes_nodes: "gnodes A w V ⊆ UNIV × nodes A"
proof
fix v
assume "v ∈ gnodes A w V"
then show "v ∈ UNIV × nodes A" by induct auto
qed

lemma gpath_subset:
assumes "gpath A w V r v"
assumes "set (gstates r v) ⊆ U"
shows "gpath A w U r v"
using assms by induct auto
lemma grun_subset:
assumes "grun A w V r v"
assumes "sset (gtrace r v) ⊆ U"
shows "grun A w U r v"
using assms
proof (coinduction arbitrary: r v)
case (run a s r v)
have 1: "grun A w V s a" using run(1, 2) by fastforce
have 2: "a ∈ gusuccessors A w v" using run(1, 2) by fastforce
show ?case using 1 2 run(1, 3) by force
qed

lemma greachable_subset: "greachable A w V v ⊆ insert v V"
proof
fix u
assume "u ∈ greachable A w V v"
then show "u ∈ insert v V" by induct auto
qed

lemma gtrace_infinite:
assumes "grun A w V r v"
shows "infinite (sset (gtrace r v))"
using assms by (metis grun_elim gtrace_alt_def infinite_Ici sset_fromN sset_szip_finite)

lemma infinite_greachable_gtrace:
assumes "grun A w V r v"
assumes "u ∈ sset (gtrace r v)"
shows "infinite (greachable A w V u)"
proof -
obtain i where 1: "u = gtrace r v !! i" using sset_range imageE assms(2) by metis
have 2: "gtarget (stake (Suc i) r) v = u" unfolding 1 sscan_snth by rule
have "infinite (sset (sdrop (Suc i) (gtrace r v)))"
using gtrace_infinite[OF assms(1)]
by (metis List.finite_set finite_Un sset_shift stake_sdrop)
also have "sdrop (Suc i) (gtrace r v) = gtrace (sdrop (Suc i) r) (gtarget (stake (Suc i) r) v)"
by simp
also have "sset … ⊆ greachable A w V u"
using assms(1) 2 by (metis graph.reachable.reflexive graph.reachable_trace graph.run_sdrop)
finally show ?thesis by this
qed

lemma finite_nodes_gsuccessors:
assumes "finite (nodes A)"
assumes "v ∈ gunodes A w"
shows "finite (gusuccessors A w v)"
proof -
have "gusuccessors A w v ⊆ gureachable A w v" by rule
also have "… ⊆ gunodes A w" using assms(2) by blast
also have "… ⊆ UNIV × nodes A" using gnodes_nodes by this
finally have 3: "gusuccessors A w v ⊆ UNIV × nodes A" by this
have "gusuccessors A w v ⊆ {Suc (fst v)} × nodes A" using 3 by auto
also have "finite …" using assms(1) by simp
finally show ?thesis by this
qed

end


# Theory Ranking

section ‹Rankings›

theory Ranking
imports
"Alternate"
"Graph"
begin

subsection ‹Rankings›

type_synonym 'state ranking = "'state node ⇒ nat"

definition ranking :: "('label, 'state) nba ⇒ 'label stream ⇒ 'state ranking ⇒ bool" where
"ranking A w f ≡
(∀ v ∈ gunodes A w. f v ≤ 2 * card (nodes A)) ∧
(∀ v ∈ gunodes A w. ∀ u ∈ gusuccessors A w v. f u ≤ f v) ∧
(∀ v ∈ gunodes A w. gaccepting A v ⟶ even (f v)) ∧
(∀ v ∈ gunodes A w. ∀ r k. gurun A w r v ⟶ smap f (gtrace r v) = sconst k ⟶ odd k)"

subsection ‹Ranking Implies Word not in Language›

lemma ranking_stuck:
assumes "ranking A w f"
assumes "v ∈ gunodes A w" "gurun A w r v"
obtains n k
where "smap f (gtrace (sdrop n r) (gtarget (stake n r) v)) = sconst k"
proof -
have 0: "f u ≤ f v" if "v ∈ gunodes A w" "u ∈ gusuccessors A w v" for v u
using assms(1) that unfolding ranking_def by auto
have 1: "shd (v ## gtrace r v) ∈ gunodes A w" using assms(2) by auto
have 2: "sdescending (smap f (v ## gtrace r v))"
using 1 assms(3)
proof (coinduction arbitrary: r v rule: sdescending.coinduct)
case sdescending
obtain u s where 1: "r = u ## s" using stream.exhaust by blast
have 2: "v ∈ gunodes A w" using sdescending(1) by simp
have 3: "gurun A w (u ## s) v" using sdescending(2) 1 by auto
have 4: "u ∈ gusuccessors A w v" using 3 by auto
have 5: "u ∈ gureachable A w v" using graph.reachable_successors 4 by blast
show ?case
unfolding 1
proof (intro exI conjI disjI1)
show "f u ≤ f v" using 0 2 4 by this
show "shd (u ## gtrace s u) ∈ gunodes A w" using 2 5 by auto
show "gurun A w s u" using 3 by auto
qed auto
qed
obtain s k where 3: "smap f (v ## gtrace r v) = s @- sconst k"
using sdescending_stuck[OF 2] by metis
have "gtrace (sdrop (Suc (length s)) r) (gtarget (stake (Suc (length s)) r) v) = sdrop (Suc (length s)) (gtrace r v)"
using sscan_sdrop by rule
also have "smap f … = sdrop (length s) (smap f (v ## gtrace r v))"
by (metis "3" id_apply sdrop_simps(2) sdrop_smap sdrop_stl shift_eq siterate.simps(2) stream.sel(2))
also have "… = sconst k" unfolding 3 using shift_eq by metis
finally show ?thesis using that by blast
qed

lemma ranking_stuck_odd:
assumes "ranking A w f"
assumes "v ∈ gunodes A w" "gurun A w r v"
obtains n
where "Ball (sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v)))) odd"
proof -
obtain n k where 1: "smap f (gtrace (sdrop n r) (gtarget (stake n r) v)) = sconst k"
using ranking_stuck assms by this
have 2: "gtarget (stake n r) v ∈ gunodes A w"
using assms(2, 3) by (simp add: graph.nodes_target graph.run_stake)
have 3: "gurun A w (sdrop n r) (gtarget (stake n r) v)"
using assms(2, 3) by (simp add: graph.run_sdrop)
have 4: "odd k" using 1 2 3 assms(1) unfolding ranking_def by meson
have 5: "Ball (sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v)))) odd"
unfolding 1 using 4 by simp
show ?thesis using that 5 by this
qed

lemma ranking_language:
assumes "ranking A w f"
shows "w ∉ language A"
proof
assume 1: "w ∈ language A"
obtain r p where 2: "run A (w ||| r) p" "p ∈ initial A" "infs (accepting A) (p ## r)" using 1 by rule
let ?r = "fromN 1 ||| r"
let ?v = "(0, p)"
have 3: "?v ∈ gunodes A w" "gurun A w ?r ?v" using 2(1, 2) by (auto intro: run_grun)

obtain n where 4: "Ball (sset (smap f (gtrace (sdrop n ?r) (gtarget (stake n ?r) ?v)))) odd"
using ranking_stuck_odd assms 3 by this
let ?s = "stake n ?r"
let ?t = "sdrop n ?r"
let ?u = "gtarget ?s ?v"

have "sset (gtrace ?t ?u) ⊆ gureachable A w ?v"
proof (intro graph.reachable_trace graph.reachable_target graph.reachable.reflexive)
show "gupath A w ?s ?v" using graph.run_stake 3(2) by this
show "gurun A w ?t ?u" using graph.run_sdrop 3(2) by this
qed
also have "… ⊆ gunodes A w" using 3(1) by blast
finally have 7: "sset (gtrace ?t ?u) ⊆ gunodes A w" by this
have 8: "⋀ p. p ∈ gunodes A w ⟹ gaccepting A p ⟹ even (f p)"
using assms unfolding ranking_def by auto
have 9: "⋀ p. p ∈ sset (gtrace ?t ?u) ⟹ gaccepting A p ⟹ even (f p)" using 7 8 by auto

have 19: "infs (accepting A) (smap snd ?r)" using 2(3) by simp
have 18: "infs (gaccepting A) ?r" using 19 by simp
have 17: "infs (gaccepting A) (gtrace ?r ?v)" using 18 unfolding gtrace_alt_def by this
have 16: "infs (gaccepting A) (gtrace (?s @- ?t) ?v)" using 17 unfolding stake_sdrop by this
have 15: "infs (gaccepting A) (gtrace ?t ?u)" using 16 by simp
have 13: "infs (even ∘ f) (gtrace ?t ?u)" using infs_mono[OF _ 15] 9 by simp
have 12: "infs even (smap f (gtrace ?t ?u))" using 13 by (simp add: comp_def)
have 11: "Bex (sset (smap f (gtrace ?t ?u))) even" using 12 infs_any by metis

show False using 4 11 by auto
qed

subsection ‹Word not in Language Implies Ranking›

subsubsection ‹Removal of Endangered Nodes›

definition clean :: "('label, 'state) nba ⇒ 'label stream ⇒ 'state node set ⇒ 'state node set" where
"clean A w V ≡ {v ∈ V. infinite (greachable A w V v)}"

lemma clean_decreasing: "clean A w V ⊆ V" unfolding clean_def by auto
lemma clean_successors:
assumes "v ∈ V" "u ∈ gusuccessors A w v"
shows "u ∈ clean A w V ⟹ v ∈ clean A w V"
proof -
assume 1: "u ∈ clean A w V"
have 2: "u ∈ V" "infinite (greachable A w V u)" using 1 unfolding clean_def by auto
have 3: "u ∈ greachable A w V v" using graph.reachable.execute assms(2) 2(1) by blast
have 4: "greachable A w V u ⊆ greachable A w V v" using 3 by blast
have 5: "infinite (greachable A w V v)" using 2(2) 4 by (simp add: infinite_super)
show "v ∈ clean A w V" unfolding clean_def using assms(1) 5 by simp
qed

subsubsection ‹Removal of Safe Nodes›

definition prune :: "('label, 'state) nba ⇒ 'label stream ⇒ 'state node set ⇒ 'state node set" where
"prune A w V ≡ {v ∈ V. ∃ u ∈ greachable A w V v. gaccepting A u}"

lemma prune_decreasing: "prune A w V ⊆ V" unfolding prune_def by auto
lemma prune_successors:
assumes "v ∈ V" "u ∈ gusuccessors A w v"
shows "u ∈ prune A w V ⟹ v ∈ prune A w V"
proof -
assume 1: "u ∈ prune A w V"
have 2: "u ∈ V" "∃ x ∈ greachable A w V u. gaccepting A x" using 1 unfolding prune_def by auto
have 3: "u ∈ greachable A w V v" using graph.reachable.execute assms(2) 2(1) by blast
have 4: "greachable A w V u ⊆ greachable A w V v" using 3 by blast
show "v ∈ prune A w V" unfolding prune_def using assms(1) 2(2) 4 by auto
qed

subsubsection ‹Run Graph Interation›

definition graph :: "('label, 'state) nba ⇒ 'label stream ⇒ nat ⇒ 'state node set" where
"graph A w k ≡ alternate (clean A w) (prune A w) k (gunodes A w)"

abbreviation "level A w k l ≡ {v ∈ graph A w k. fst v = l}"

lemma graph_0[simp]: "graph A w 0 = gunodes A w" unfolding graph_def by simp
lemma graph_Suc[simp]: "graph A w (Suc k) = (if even k then clean A w else prune A w) (graph A w k)"
unfolding graph_def by simp

lemma graph_antimono: "antimono (graph A w)"
using alternate_antimono clean_decreasing prune_decreasing
unfolding antimono_def le_fun_def graph_def
by metis
lemma graph_nodes: "graph A w k ⊆ gunodes A w" using graph_0 graph_antimono le0 antimonoD by metis
lemma graph_successors:
assumes "v ∈ gunodes A w" "u ∈ gusuccessors A w v"
shows "u ∈ graph A w k ⟹ v ∈ graph A w k"
using assms
proof (induct k arbitrary: u v)
case 0
show ?case using 0(2) by simp
next
case (Suc k)
have 1: "v ∈ graph A w k" using Suc using antimono_iff_le_Suc graph_antimono rev_subsetD by blast
show ?case using Suc(2) clean_successors[OF 1 Suc(4)] prune_successors[OF 1 Suc(4)] by auto
qed

lemma graph_level_finite:
assumes "finite (nodes A)"
shows "finite (level A w k l)"
proof -
have "level A w k l ⊆ {v ∈ gunodes A w. fst v = l}" by (simp add: graph_nodes subset_CollectI)
also have "{v ∈ gunodes A w. fst v = l} ⊆ {l} × nodes A" using gnodes_nodes by force
also have "finite ({l} × nodes A)" using assms(1) by simp
finally show ?thesis by this
qed

lemma find_safe:
assumes "w ∉ language A"
assumes "V ≠ {}" "V ⊆ gunodes A w"
assumes "⋀ v. v ∈ V ⟹ gsuccessors A w V v ≠ {}"
obtains v
where "v ∈ V" "∀ u ∈ greachable A w V v. ¬ gaccepting A u"
proof (rule ccontr)
assume 1: "¬ thesis"
have 2: "⋀ v. v ∈ V ⟹ ∃ u ∈ greachable A w V v. gaccepting A u" using that 1 by auto
have 3: "⋀ r v. v ∈ initial A ⟹ run A (w ||| r) v ⟹ fins (accepting A) r" using assms(1) by auto
obtain v where 4: "v ∈ V" using assms(2) by force
obtain x where 5: "x ∈ greachable A w V v" "gaccepting A x" using 2 4 by blast
obtain y where 50: "gpath A w V y v" "x = gtarget y v" using 5(1) by rule
obtain r where 6: "grun A w V r x" "infs (λ x. x ∈ V ∧ gaccepting A x) r"
proof (rule graph.recurring_condition)
show "x ∈ V ∧ gaccepting A x" using greachable_subset 4 5 by blast
next
fix v
assume 1: "v ∈ V ∧ gaccepting A v"
obtain v' where 20: "v' ∈ gsuccessors A w V v" using assms(4) 1 by (meson IntE equals0I)
have 21: "v' ∈ V" using 20 by auto
have 22: "∃ u ∈ greachable A w V v'. u ∈ V ∧ gaccepting A u"
using greachable_subset 2 21 by blast
obtain r where 30: "gpath A w V r v'" "gtarget r v' ∈ V ∧ gaccepting A (gtarget r v')"
using 22 by blast
show "∃ r. r ≠ [] ∧ gpath A w V r v ∧ gtarget r v ∈ V ∧ gaccepting A (gtarget r v)"
proof (intro exI conjI)
show "v' # r ≠ []" by simp
show "gpath A w V (v' # r) v" using 20 30 by auto
show "gtarget (v' # r) v ∈ V" using 30 by simp
show "gaccepting A (gtarget (v' # r) v)" using 30 by simp
qed
qed auto
obtain u where 100: "u ∈ ginitial A" "v ∈ gureachable A w u" using 4 assms(3) by blast
have 101: "gupath A w y v" using gpath_subset 50(1) subset_UNIV by this
have 102: "gurun A w r x" using grun_subset 6(1) subset_UNIV by this
obtain t where 103: "gupath A w t u" "v = gtarget t u" using 100(2) by rule
have 104: "gurun A w (t @- y @- r) u" using 101 102 103 50(2) by auto
obtain s q where 7: "t @- y @- r = fromN (Suc 0) ||| s" "u = (0, q)"
using grun_elim[OF 104] 100(1) by blast
have 8: "run A (w ||| s) q" using grun_run[OF 104[unfolded 7]] by simp
have 9: "q ∈ initial A" using 100(1) 7(2) by auto
have 91: "sset (trace (w ||| s) q) ⊆ reachable A q"
using nba.reachable_trace nba.reachable.reflexive 8 by this
have 10: "fins (accepting A) s" using 3 9 8 by this
have 12: "infs (gaccepting A) r" using infs_mono[OF _ 6(2)] by simp
have "s = smap snd (t @- y @- r)" unfolding 7(1) by simp
also have "infs (accepting A) …" using 12 by (simp add: comp_def)
finally have 13: "infs (accepting A) s" by this
show False using 10 13 by simp
qed

lemma remove_run:
assumes "finite (nodes A)" "w ∉ language A"
assumes "V ⊆ gunodes A w" "clean A w V ≠ {}"
obtains v r
where
"grun A w V r v"
"sset (gtrace r v) ⊆ clean A w V"
"sset (gtrace r v) ⊆ - prune A w (clean A w V)"
proof -
obtain u where 1: "u ∈ clean A w V" "∀ x ∈ greachable A w (clean A w V) u. ¬ gaccepting A x"
proof (rule find_safe)
show "w ∉ language A" using assms(2) by this
show "clean A w V ≠ {}" using assms(4) by this
show "clean A w V ⊆ gunodes A w" using assms(3) by (meson clean_decreasing subset_iff)
next
fix v
assume 1: "v ∈ clean A w V"
have 2: "v ∈ V" using 1 clean_decreasing by blast
have 3: "infinite (greachable A w V v)" using 1 clean_def by auto
have "gsuccessors A w V v ⊆ gusuccessors A w v" by auto
also have "finite …" using 2 assms(1, 3) finite_nodes_gsuccessors by blast
finally have 4: "finite (gsuccessors A w V v)" by this
have 5: "infinite (insert v (⋃((greachable A w V)  (gsuccessors A w V v))))"
using graph.reachable_step 3 by metis
obtain u where 6: "u ∈ gsuccessors A w V v" "infinite (greachable A w V u)" using 4 5 by auto
have 7: "u ∈ clean A w V" using 6 unfolding clean_def by auto
show "gsuccessors A w (clean A w V) v ≠ {}" using 6(1) 7 by auto
qed auto
have 2: "u ∈ V" using 1(1) unfolding clean_def by auto
have 3: "infinite (greachable A w V u)" using 1(1) unfolding clean_def by simp
have 4: "finite (gsuccessors A w V v)" if "v ∈ greachable A w V u" for v
proof -
have 1: "v ∈ V" using that greachable_subset 2 by blast
have "gsuccessors A w V v ⊆ gusuccessors A w v" by auto
also have "finite …" using 1 assms(1, 3) finite_nodes_gsuccessors by blast
finally show ?thesis by this
qed
obtain r where 5: "grun A w V r u" using graph.koenig[OF 3 4] by this
have 6: "greachable A w V u ⊆ V" using 2 greachable_subset by blast
have 7: "sset (gtrace r u) ⊆ V"
using graph.reachable_trace[OF graph.reachable.reflexive 5(1)] 6 by blast
have 8: "sset (gtrace r u) ⊆ clean A w V"
unfolding clean_def using 7 infinite_greachable_gtrace[OF 5(1)] by auto
have 9: "sset (gtrace r u) ⊆ greachable A w (clean A w V) u"
using 5 8 by (metis graph.reachable.reflexive graph.reachable_trace grun_subset)
show ?thesis
proof
show "grun A w V r u" using 5(1) by this
show "sset (gtrace r u) ⊆ clean A w V" using 8 by this
show "sset (gtrace r u) ⊆ - prune A w (clean A w V)"
proof (intro subsetI ComplI)
fix p
assume 10: "p ∈ sset (gtrace r u)" "p ∈ prune A w (clean A w V)"
have 20: "∃ x ∈ greachable A w (clean A w V) p. gaccepting A x"
using 10(2) unfolding prune_def by auto
have 30: "greachable A w (clean A w V) p ⊆ greachable A w (clean A w V) u"
using 10(1) 9 by blast
show "False" using 1(2) 20 30 by force
qed
qed
qed

lemma level_bounded:
assumes "finite (nodes A)" "w ∉ language A"
obtains n
where "⋀ l. l ≥ n ⟹ card (level A w (2 * k) l) ≤ card (nodes A) - k"
proof (induct k arbitrary: thesis)
case (0)
show ?case
proof (rule 0)
fix l :: nat
have "finite ({l} × nodes A)" using assms(1) by simp
also have "level A w 0 l ⊆ {l} × nodes A" using gnodes_nodes by force
also (card_mono) have "card … = card (nodes A)" using assms(1) by simp
finally show "card (level A w (2 * 0) l) ≤ card (nodes A) - 0" by simp
qed
next
case (Suc k)
show ?case
proof (cases "graph A w (Suc (2 * k)) = {}")
case True
have 3: "graph A w (2 * Suc k) = {}" using True prune_decreasing by simp blast
show ?thesis using Suc(2) 3 by simp
next
case False
obtain v r where 1:
"grun A w (graph A w (2 * k)) r v"
"sset (gtrace r v) ⊆ graph A w (Suc (2 * k))"
"sset (gtrace r v) ⊆ - graph A w (Suc (Suc (2 * k)))"
proof (rule remove_run)
show "finite (nodes A)" "w ∉ language A" using assms by this
show "clean A w (graph A w (2 * k)) ≠ {}" using False by simp
show "graph A w (2 * k) ⊆ gunodes A w" using graph_nodes by this
qed auto
obtain l q where 2: "v = (l, q)" by force
obtain n where 90: "⋀ l. n ≤ l ⟹ card (level A w (2 * k) l) ≤ card (nodes A) - k"
using Suc(1) by blast
show ?thesis
proof (rule Suc(2))
fix j
assume 100: "n + Suc l ≤ j"
have 6: "graph A w (Suc (Suc (2 * k))) ⊆ graph A w (Suc (2 * k))"
using graph_antimono antimono_iff_le_Suc by blast
have 101: "gtrace r v !! (j - Suc l) ∈ graph A w (Suc (2 * k))" using 1(2) snth_sset by auto
have 102: "gtrace r v !! (j - Suc l) ∉ graph A w (Suc (Suc (2 * k)))" using 1(3) snth_sset by blast
have 103: "gtrace r v !! (j - Suc l) ∈ level A w (Suc (2 * k)) j"
using 1(1) 100 101 2 by (auto elim: grun_elim)
have 104: "gtrace r v !! (j - Suc l) ∉ level A w (Suc (Suc (2 * k))) j" using 100 102 by simp
have "level A w (2 * Suc k) j = level A w (Suc (Suc (2 * k))) j" by simp
also have "… ⊂ level A w (Suc (2 * k)) j" using 103 104 6 by blast
also have "… ⊆ level A w (2 * k) j" by (simp add: Collect_mono clean_def)
finally have 105: "level A w (2 * Suc k) j ⊂ level A w (2 * k) j" by this
have "card (level A w (2 * Suc k) j) < card (level A w (2 * k) j)"
using assms(1) 105 by (simp add: graph_level_finite psubset_card_mono)
also have "… ≤ card (nodes A) - k" using 90 100 by simp
finally show "card (level A w (2 * Suc k) j) ≤ card (nodes A) - Suc k" by simp
qed
qed
qed
lemma graph_empty:
assumes "finite (nodes A)" "w ∉ language A"
shows "graph A w (Suc (2 * card (nodes A))) = {}"
proof -
obtain n where 1: "⋀ l. l ≥ n ⟹ card (level A w (2 * card (nodes A)) l) = 0"
using level_bounded[OF assms(1, 2), of "card (nodes A)"] by auto
have "graph A w (2 * card (nodes A)) =
(⋃ l ∈ {..< n}. level A w (2 * card (nodes A)) l) ∪
(⋃ l ∈ {n ..}. level A w (2 * card (nodes A)) l)"
by auto
also have "(⋃ l ∈ {n ..}. level A w (2 * card (nodes A)) l) = {}"
using graph_level_finite assms(1) 1 by fastforce
also have "finite ((⋃ l ∈ {..< n}. level A w (2 * card (nodes A)) l) ∪ {})"
using graph_level_finite assms(1) by auto
finally have 100: "finite (graph A w (2 * card (nodes A)))" by this
have 101: "finite (greachable A w (graph A w (2 * card (nodes A))) v)" for v
using 100 greachable_subset[of A w "graph A w (2 * card (nodes A))" v]
using finite_insert infinite_super by auto
show ?thesis using 101 by (simp add: clean_def)
qed
lemma graph_le:
assumes "finite (nodes A)" "w ∉ language A"
assumes "v ∈ graph A w k"
shows "k ≤ 2 * card (nodes A)"
using graph_empty graph_antimono assms
by (metis (no_types, lifting) Suc_leI antimono_def basic_trans_rules(30) empty_iff not_le_imp_less)

subsection ‹Node Ranks›

definition rank :: "('label, 'state) nba ⇒ 'label stream ⇒ 'state node ⇒ nat" where
"rank A w v ≡ GREATEST k. v ∈ graph A w k"

lemma rank_member:
assumes "finite (nodes A)" "w ∉ language A" "v ∈ gunodes A w"
shows "v ∈ graph A w (rank A w v)"
unfolding rank_def
proof (rule GreatestI_nat)
show "v ∈ graph A w 0" using assms(3) by simp
show "k ≤ 2 * card (nodes A)" if "v ∈ graph A w k" for k
using graph_le assms(1, 2) that by blast
qed
lemma rank_removed:
assumes "finite (nodes A)" "w ∉ language A"
shows "v ∉ graph A w (Suc (rank A w v))"
proof
assume "v ∈ graph A w (Suc (rank A w v))"
then have 2: "Suc (rank A w v) ≤ rank A w v"
unfolding rank_def using Greatest_le_nat graph_le assms by metis
then show "False" by auto
qed
lemma rank_le:
assumes "finite (nodes A)" "w ∉ language A"
assumes "v ∈ gunodes A w" "u ∈ gusuccessors A w v"
shows "rank A w u ≤ rank A w v"
unfolding rank_def
proof (rule Greatest_le_nat)
have 1: "u ∈ gureachable A w v" using graph.reachable_successors assms(4) by blast
have 2: "u ∈ gunodes A w" using assms(3) 1 by auto
show "v ∈ graph A w (GREATEST k. u ∈ graph A w k)"
unfolding rank_def[symmetric]
proof (rule graph_successors)
show "v ∈ gunodes A w" using assms(3) by this
show "u ∈ gusuccessors A w v" using assms(4) by this
show "u ∈ graph A w (rank A w u)" using rank_member assms(1, 2) 2 by this
qed
show "k ≤ 2 * card (nodes A)" if "v ∈ graph A w k" for k
using graph_le assms(1, 2) that by blast
qed

lemma language_ranking:
assumes "finite (nodes A)" "w ∉ language A"
shows "ranking A w (rank A w)"
unfolding ranking_def
proof (intro conjI ballI allI impI)
fix v
assume 1: "v ∈ gunodes A w"
have 2: "v ∈ graph A w (rank A w v)" using rank_member assms 1 by this
show "rank A w v ≤ 2 * card (nodes A)" using graph_le assms 2 by this
next
fix v u
assume 1: "v ∈ gunodes A w" "u ∈ gusuccessors A w v"
show "rank A w u ≤ rank A w v" using rank_le assms 1 by this
next
fix v
assume 1: "v ∈ gunodes A w" "gaccepting A v"
have 2: "v ∈ graph A w (rank A w v)" using rank_member assms 1(1) by this
have 3: "v ∉ graph A w (Suc (rank A w v))" using rank_removed assms by this
have 4: "v ∈ prune A w (graph A w (rank A w v))" using 2 1(2) unfolding prune_def by auto
have 5: "graph A w (Suc (rank A w v)) ≠ prune A w (graph A w (rank A w v))" using 3 4 by blast
show "even (rank A w v)" using 5 by auto
next
fix v r k
assume 1: "v ∈ gunodes A w" "gurun A w r v" "smap (rank A w) (gtrace r v) = sconst k"
have "sset (gtrace r v) ⊆ gureachable A w v"
using 1(2) by (metis graph.reachable.reflexive graph.reachable_trace)
then have 6: "sset (gtrace r v) ⊆ gunodes A w" using 1(1) by blast
have 60: "rank A w  sset (gtrace r v) ⊆ {k}"
using 1(3) by (metis equalityD1 sset_sconst stream.set_map)
have 50: "sset (gtrace r v) ⊆ graph A w k"
using rank_member[OF assms] subsetD[OF 6] 60 unfolding image_subset_iff by auto
have 70: "grun A w (graph A w k) r v" using grun_subset 1(2) 50 by this
have 7: "sset (gtrace r v) ⊆ clean A w (graph A w k)"
unfolding clean_def using 50 infinite_greachable_gtrace[OF 70] by auto
have 8: "sset (gtrace r v) ∩ graph A w (Suc k) = {}" using rank_removed[OF assms] 60 by blast
have 9: "sset (gtrace r v) ≠ {}" using stream.set_sel(1) by auto
have 10: "graph A w (Suc k) ≠ clean A w (graph A w k)" using 7 8 9 by blast
show "odd k" using 10 unfolding graph_Suc by auto
qed

subsection ‹Correctness Theorem›

theorem language_ranking_iff:
assumes "finite (nodes A)"
shows "w ∉ language A ⟷ (∃ f. ranking A w f)"
using ranking_language language_ranking assms by blast

end


# Theory Complementation

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)))"
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
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 "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
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)
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)"
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 {})"
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 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) ∘ m n" for i n unfolding R_Suc by (induct i) (auto)
have R_reach: "R i n S ⊆ reach A w (n + i)" if "S ⊆ reach A w n" for i n S
using snth_in assms(2) that m_def by (induct i) (auto)
have P_R: "P (k + i) = R i k (P k)" for i
using 22 by (induct i) (auto simp add: case_prod_beta' m_def st_succ_def)

have 50: "R i n S = (⋃ p ∈ S. R i n {p})" for i n S
by (induct i) (auto simp add: m_def prod.case_eq_if)
have 51: "R (i + j) n S = {}" if "R i n S = {}" for i j n S
using that by (induct j) (auto simp add: m_def prod.case_eq_if)
have 52: "R j n S = {}" if "i ≤ j" "R i n S = {}" for i j n S
using 51 by (metis le_add_diff_inverse that(1) that(2))

have 1: "∃ p ∈ S. ∀ i. R i n {p} ≠ {}"
if assms: "finite S" "⋀ i. R i n S ≠ {}" for n S
proof (rule ccontr)
assume 1: "¬ (∃ p ∈ S. ∀ i. R i n {p} ≠ {})"
obtain f where 3: "⋀ p. p ∈ S ⟹ R (f p) n {p} = {}" using 1 by metis
have 4: "R (Sup (f  S)) n {p} = {}" if "p ∈ S" for p
proof (rule 52)
show "f p ≤ Sup (f  S)" using assms(1) that by (auto intro: le_cSup_finite)
show "R (f p) n {p} = {}" using 3 that by this
qed
have "R (Sup (f  S)) n S = (⋃ p ∈ S. R (Sup (f  S)) n {p})" using 50 by this
also have "… = {}" using 4 by simp
finally have 5: "R (Sup (f  S)) n S = {}" by this
show "False" using that(2) 5 by auto
qed
have 2: "⋀ i. R i (k + 0) (P k) ≠ {}" using 22 P_R by simp
obtain p where 3: "p ∈ P k" "⋀ i. R i k {p} ≠ {}" using 1[OF P_finite 2] by auto

define Q where "Q n p ≡ (∀ i. R i (k + n) {p} ≠ {}) ∧ p ∈ P (k + n)" for n p
have 5: "∃ q ∈ transition A (w !! (k + n)) p. Q (Suc n) q" if "Q n p" for n p
proof -
have 11: "p ∈ P (k + n)" "⋀ i. R i (k + n) {p} ≠ {}" using that unfolding Q_def by auto
have 12: "R (Suc i) (k + n) {p} ≠ {}" for i using 11(2) by this
have 13: "R i (k + Suc n) (m (k + n) {p}) ≠ {}" for i using 12 unfolding R_Suc' by simp
have "{p} ⊆ P (k + n)" using 11(1) by auto
also have "… ⊆ reach A w (k + n)" using P_reach by this
finally have "R 1 (k + n) {p} ⊆ reach A w (k + n + 1)" using R_reach by blast
also have "… ⊆ nodes A" using reach_nodes by this
also have "finite (nodes A)" using assms(1) by this
finally have 14: "finite (m (k + n) {p})" by simp
obtain q where 14: "q ∈ m (k + n) {p}" "⋀ i. R i (k + Suc n) {q} ≠ {}"
using 1[OF 14 13] by auto
show ?thesis
unfolding Q_def prod.case
proof (intro bexI conjI allI)
show "⋀ i. R i (k + Suc n) {q} ≠ {}" using 14(2) by this
show "q ∈ P (k + Suc n)"
using 14(1) 11(1) 22 unfolding m_def by (auto simp add: st_succ_def)
show "q ∈ transition A (w !! (k + n)) p" using 14(1) unfolding m_def by simp
qed
qed
obtain r where 23:
"run A r p" "⋀ i. Q i ((p ## trace r p) !! i)" "⋀ i. fst (r !! i) = w !! (k + i)"
proof (rule nba.invariant_run_index[of Q 0 p A "λ n p a. fst a = w !! (k + n)"])
show "Q 0 p" unfolding Q_def using 3 by auto
show "∃ a. (fst a ∈ alphabet A ∧ snd a ∈ transition A (fst a) p) ∧
Q (Suc n) (snd a) ∧ fst a = w !! (k + n)" if "Q n p" for n p
using snth_in assms(2) 5 that by fastforce
qed auto
have 20: "smap fst r = sdrop k w" using 23(3) by (intro eqI_snth) (simp add: case_prod_beta)
have 21: "(p ## smap snd r) !! i ∈ P (k + i)" for i
using 23(2) unfolding Q_def unfolding nba.trace_alt_def by simp
obtain r where 23: "run A (sdrop k w ||| stl r) (shd r)" "⋀ i. r !! i ∈ P (k + i)"
using 20 21 23(1) by (metis stream.sel(1) stream.sel(2) szip_smap)
let ?v = "(k, shd r)"
let ?r = "fromN (Suc k) ||| stl r"
have "shd r = r !! 0" by simp
also have "… ∈ P k" using 23(2)[of 0] by simp
also have "… ⊆ reach A w k" using P_reach by this
finally have 24: "?v ∈ gunodes A w" using reach_gunodes by blast
have 25: "gurun A w ?r ?v" using run_grun 23(1) by this
obtain l where 26: "Ball (sset (smap f' (gtrace (sdrop l ?r) (gtarget (stake l ?r) ?v)))) odd"
using ranking_stuck_odd 0 24 25 by this
have 27: "f' (Suc (k + l), r !! Suc l) =
shd (smap f' (gtrace (sdrop l ?r) (gtarget (stake l ?r) ?v)))" by (simp add: algebra_simps)
also have "… ∈ sset (smap f' (gtrace (sdrop l ?r) (gtarget (stake l ?r) ?v)))"
using shd_sset by this
finally have 28: "odd (f' (Suc (k + l), r !! Suc l))" using 26 by auto
have "r !! Suc l ∈ P (Suc (k + l))" using 23(2) by (metis add_Suc_right)
also have "… = {p ∈ ⋃ (transition A (w !! (k + l))  P (k + l)).
even (the (g (Suc (k + l)) p))}" using 23(2) by (auto simp: st_succ_def)
also have "… ⊆ {p. even (the (g (Suc (k + l)) p))}" by auto
finally have 29: "even (the (g (Suc (k + l)) (r !! Suc l)))" by auto
have 30: "r !! Suc l ∈ reach A w (Suc (k + l))"
using 23(2) P_reach by (metis add_Suc_right subsetCE)
have 31: "even (f' (Suc (k + l), r !! Suc l))" using 29 30 unfolding g_def by simp
show "False" using 28 31 by simp
qed
have 11: "infs (λ k. P k = {}) nats" using 10 unfolding infs_snth by simp
have "infs (λ S. S = {}) (smap snd (smap g nats ||| smap P nats))"
using 11 by (simp add: comp_def)
then have "infs (λ x. snd x = {}) (smap g nats ||| smap P nats)"
by (simp add: comp_def del: szip_smap_snd)
then have "infs (λ (f, P). P = {}) (smap g nats ||| smap P nats)"
then have "infs (λ (f, P). P = {}) (stl (smap g nats ||| smap P nats))" by blast
then have "infs (λ (f, P). P = {}) (smap snd (w ||| stl (smap g nats ||| smap P nats)))" by simp
then have "infs (λ (f, P). P = {}) (stl s)" unfolding s_def by simp
then show ?thesis unfolding complement_def by auto
qed
qed
qed

subsection ‹Correctness Theorem›

theorem complement_language:
assumes "finite (nodes A)"
shows "language (complement A) = streams (alphabet A) - language A"
proof (safe del: notI)
have 1: "alphabet (complement A) = alphabet A" unfolding complement_def nba.sel by rule
show "w ∈ streams (alphabet A)" if "w ∈ language (complement A)" for w
using nba.language_alphabet that 1 by force
show "w ∉ language A" if "w ∈ language (complement A)" for w
using complement_ranking ranking_language that by metis
show "w ∈ language (complement A)" if "w ∈ streams (alphabet A)" "w ∉ language A" for w
using language_ranking ranking_complement assms that by blast
qed

end


# Theory Complementation_Implement

section ‹Complementation Implementation›

theory Complementation_Implement
imports
"HOL-Library.Lattice_Syntax"
"Transition_Systems_and_Automata.NBA_Implement"
"Complementation"
begin

type_synonym item = "nat × bool"
type_synonym 'state items = "'state ⇀ item"

type_synonym state = "(nat × item) list"
abbreviation "item_rel ≡ nat_rel ×⇩r bool_rel"
abbreviation "state_rel ≡ ⟨nat_rel, item_rel⟩ list_map_rel"

abbreviation "pred A a q ≡ {p. q ∈ transition A a p}"

subsection ‹Phase 1›

definition cs_lr :: "'state items ⇒ 'state lr" where
"cs_lr f ≡ map_option fst ∘ f"
definition cs_st :: "'state items ⇒ 'state st" where
"cs_st f ≡ f - Some  snd - {True}"
abbreviation cs_abs :: "'state items ⇒ 'state cs" where
"cs_abs f ≡ (cs_lr f, cs_st f)"
definition cs_rep :: "'state cs ⇒ 'state items" where
"cs_rep ≡ λ (g, P) p. map_option (λ k. (k, p ∈ P)) (g p)"

lemma cs_abs_rep[simp]: "cs_rep (cs_abs f) = f"
proof
show "cs_rep (cs_abs f) x = f x" for x
unfolding cs_lr_def cs_st_def cs_rep_def by (cases "f x") (force+)
qed
lemma cs_rep_lr[simp]: "cs_lr (cs_rep (g, P)) = g"
proof
show "cs_lr (cs_rep (g, P)) x = g x" for x
unfolding cs_rep_def cs_lr_def by (cases "g x") (auto)
qed
lemma cs_rep_st[simp]: "cs_st (cs_rep (g, P)) = P ∩ dom g"
unfolding cs_rep_def cs_st_def by force

lemma cs_lr_dom[simp]: "dom (cs_lr f) = dom f" unfolding cs_lr_def by simp
lemma cs_lr_apply[simp]:
assumes "p ∈ dom f"
shows "the (cs_lr f p) = fst (the (f p))"
using assms unfolding cs_lr_def by auto

lemma cs_rep_dom[simp]: "dom (cs_rep (g, P)) = dom g" unfolding cs_rep_def by auto
lemma cs_rep_apply[simp]:
assumes "p ∈ dom f"
shows "fst (the (cs_rep (f, P) p)) = the (f p)"
using assms unfolding cs_rep_def by auto

abbreviation cs_rel :: "('state items × 'state cs) set" where
"cs_rel ≡ br cs_abs top"

lemma cs_rel_inv_single_valued: "single_valued (cs_rel¯)"
by (auto intro!: inj_onI) (metis cs_abs_rep)

definition refresh_1 :: "'state items ⇒ 'state items" where
"refresh_1 f ≡ if True ∈ snd  ran f then f else map_option (apsnd top) ∘ f"
definition ranks_1 ::
"('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set" where
"ranks_1 A a f ≡ {g.
dom g = ⋃((transition A a)  (dom f)) ∧
(∀ p ∈ dom f. ∀ q ∈ transition A a p. fst (the (g q)) ≤ fst (the (f p))) ∧
(∀ q ∈ dom g. accepting A q ⟶ even (fst (the (g q)))) ∧
cs_st g = {q ∈ ⋃((transition A a)  (cs_st f)). even (fst (the (g q)))}}"
definition complement_succ_1 ::
"('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set" where
"complement_succ_1 A a = ranks_1 A a ∘ refresh_1"
definition complement_1 :: "('label, 'state) nba ⇒ ('label, 'state items) nba" where
"complement_1 A ≡ nba
(alphabet A)
({const (Some (2 * card (nodes A), False)) | initial A})
(complement_succ_1 A)
(λ f. cs_st f = {})"

lemma refresh_1_dom[simp]: "dom (refresh_1 f) = dom f" unfolding refresh_1_def by simp
lemma refresh_1_apply[simp]: "fst (the (refresh_1 f p)) = fst (the (f p))"
unfolding refresh_1_def by (cases "f p") (auto)
lemma refresh_1_cs_st[simp]: "cs_st (refresh_1 f) = (if cs_st f = {} then dom f else cs_st f)"
unfolding refresh_1_def cs_st_def ran_def image_def vimage_def by auto

lemma complement_succ_1_abs:
assumes "g ∈ complement_succ_1 A a f"
shows "cs_abs g ∈ complement_succ A a (cs_abs f)"
unfolding complement_succ_def
proof (simp, rule)
have 1:
"dom g = ⋃((transition A a)  (dom f))"
"∀ p ∈ dom f. ∀ q ∈ transition A a p. fst (the (g q)) ≤ fst (the (f p))"
"∀ p ∈ dom g. accepting A p ⟶ even (fst (the (g p)))"
using assms unfolding complement_succ_1_def ranks_1_def by simp_all
show "cs_lr g ∈ lr_succ A a (cs_lr f)"
unfolding lr_succ_def
proof (intro CollectI conjI ballI impI)
show "dom (cs_lr g) = ⋃ (transition A a  dom (cs_lr f))" using 1 by simp
next
fix p q
assume 2: "p ∈ dom (cs_lr f)" "q ∈ transition A a p"
have 3: "q ∈ dom (cs_lr g)" using 1 2 by auto
show "the (cs_lr g q) ≤ the (cs_lr f p)" using 1 2 3 by simp
next
fix p
assume 2: "p ∈ dom (cs_lr g)" "accepting A p"
show "even (the (cs_lr g p))" using 1 2 by auto
qed
have 2: "cs_st g = {q ∈ ⋃ (transition A a  cs_st (refresh_1 f)). even (fst (the (g q)))}"
using assms unfolding complement_succ_1_def ranks_1_def by simp
show "cs_st g = st_succ A a (cs_lr g) (cs_st f)"
proof (cases "cs_st f = {}")
case True
have 3: "the (cs_lr g q) = fst (the (g q))" if "q ∈ ⋃((transition A a)  (dom f))" for q
using that 1(1) by simp
show ?thesis using 2 3 unfolding st_succ_def refresh_1_cs_st True cs_lr_dom 1(1) by force
next
case False
have 3: "the (cs_lr g q) = fst (the (g q))" if "q ∈ ⋃((transition A a)  (cs_st f))" for q
using that 1(1) by
(auto intro!: cs_lr_apply)
(metis IntE UN_iff cs_abs_rep cs_lr_dom cs_rep_st domD prod.collapse)
have "cs_st g = {q ∈ ⋃ (transition A a  cs_st (refresh_1 f)). even (fst (the (g q)))}"
using 2 by this
also have "cs_st (refresh_1 f) = cs_st f" using False by simp
also have "{q ∈ ⋃((transition A a)  (cs_st f)). even (fst (the (g q)))} =
{q ∈ ⋃((transition A a)  (cs_st f)). even (the (cs_lr g q))}" using 3 by metis
also have "… = st_succ A a (cs_lr g) (cs_st f)" unfolding st_succ_def using False by simp
finally show ?thesis by this
qed
qed
lemma complement_succ_1_rep:
assumes "P ⊆ dom f" "(g, Q) ∈ complement_succ A a (f, P)"
shows "cs_rep (g, Q) ∈ complement_succ_1 A a (cs_rep (f, P))"
unfolding complement_succ_1_def ranks_1_def comp_apply
proof (intro CollectI conjI ballI impI)
have 1:
"dom g = ⋃((transition A a)  (dom f))"
"∀ p ∈ dom f. ∀ q ∈ transition A a p. the (g q) ≤ the (f p)"
"∀ p ∈ dom g. accepting A p ⟶ even (the (g p))"
using assms(2) unfolding complement_succ_def lr_succ_def by simp_all
have 2: "Q = {q ∈ if P = {} then dom g else ⋃((transition A a)  P). even (the (g q))}"
using assms(2) unfolding complement_succ_def st_succ_def by simp
have 3: "Q ⊆ dom g" unfolding 2 1(1) using assms(1) by auto
show "dom (cs_rep (g, Q)) = ⋃ (transition A a  dom (refresh_1 (cs_rep (f, P))))" using 1 by simp
show "⋀ p q. p ∈ dom (refresh_1 (cs_rep (f, P))) ⟹ q ∈ transition A a p ⟹
fst (the (cs_rep (g, Q) q)) ≤ fst (the (refresh_1 (cs_rep (f, P)) p))"
using 1(1, 2) by (auto) (metis UN_I cs_rep_apply domI option.sel)
show "⋀ p. p ∈ dom (cs_rep (g, Q)) ⟹ accepting A p ⟹ even (fst (the (cs_rep (g, Q) p)))"
using 1(1, 3) by auto
show "cs_st (cs_rep (g, Q)) = {q ∈ ⋃ (transition A a  cs_st (refresh_1 (cs_rep (f, P)))).
even (fst (the (cs_rep (g, Q) q)))}"
proof (cases "P = {}")
case True
have "cs_st (cs_rep (g, Q)) = Q" using 3 by auto
also have "… = {q ∈ dom g. even (the (g q))}" unfolding 2 using True by auto
also have "… = {q ∈ dom g. even (fst (the (cs_rep (g, Q) q)))}" using cs_rep_apply by metis
also have "dom g = ⋃((transition A a)  (dom f))" using 1(1) by this
also have "dom f = cs_st (refresh_1 (cs_rep (f, P)))" using True by simp
finally show ?thesis by this
next
case False
have 4: "fst (the (cs_rep (g, Q) q)) = the (g q)" if "q ∈ ⋃((transition A a)  P)" for q
using 1(1) that assms(1) by (fast intro: cs_rep_apply)
have "cs_st (cs_rep (g, Q)) = Q" using 3 by auto
also have "… = {q ∈ ⋃((transition A a)  P). even (the (g q))}" unfolding 2 using False by auto
also have "… = {q ∈ ⋃((transition A a)  P). even (fst (the (cs_rep (g, Q) q)))}" using 4 by force
also have "P = (cs_st (refresh_1 (cs_rep (f, P))))" using assms(1) False by auto
finally show ?thesis by simp
qed
qed

lemma complement_succ_1_refine: "(complement_succ_1, complement_succ) ∈
Id → Id → cs_rel → ⟨cs_rel⟩ set_rel"
proof (clarsimp simp: br_set_rel_alt in_br_conv)
fix A :: "('a, 'b) nba"
fix a f
show "complement_succ A a (cs_abs f) = cs_abs  complement_succ_1 A a f"
proof safe
fix g Q
assume 1: "(g, Q) ∈ complement_succ A a (cs_abs f)"
have 2: "Q ⊆ dom g"
using 1 unfolding complement_succ_def lr_succ_def st_succ_def
by (auto) (metis IntE cs_abs_rep cs_lr_dom cs_rep_st)
have 3: "cs_st f ⊆ dom (cs_lr f)" unfolding cs_st_def by auto
show "(g, Q) ∈ cs_abs  complement_succ_1 A a f"
proof
show "(g, Q) = cs_abs (cs_rep (g, Q))" using 2 by auto
have "cs_rep (g, Q) ∈ complement_succ_1 A a (cs_rep (cs_abs f))"
using complement_succ_1_rep 3 1 by this
also have "cs_rep (cs_abs f) = f" by simp
finally show "cs_rep (g, Q) ∈ complement_succ_1 A a f" by this
qed
next
fix g
assume 1: "g ∈ complement_succ_1 A a f"
show "cs_abs g ∈ complement_succ A a (cs_abs f)" using complement_succ_1_abs 1 by this
qed
qed
lemma complement_1_refine: "(complement_1, complement) ∈ ⟨Id, Id⟩ nba_rel → ⟨Id, cs_rel⟩ nba_rel"
unfolding complement_1_def complement_def
proof parametricity
fix A B :: "('a, 'b) nba"
assume 1: "(A, B) ∈ ⟨Id, Id⟩ nba_rel"
have 2: "(const (Some (2 * card (nodes B), False)) | initial B,
const (Some (2 * card (nodes B))) | initial B, {}) ∈ cs_rel"
unfolding cs_lr_def cs_st_def in_br_conv by (force simp: restrict_map_def)
show "(complement_succ_1 A, complement_succ B) ∈ Id → cs_rel → ⟨cs_rel⟩ set_rel"
using complement_succ_1_refine 1 by parametricity auto
show "({const (Some (2 * card (nodes A), False)) | initial A},
{const (Some (2 * card (nodes B))) | initial B} × {{}}) ∈ ⟨cs_rel⟩ set_rel"
using 1 2 by simp parametricity
show "(λ f. cs_st f = {}, λ (f, P). P = {}) ∈ cs_rel → bool_rel" by (auto simp: in_br_conv)
qed

subsection ‹Phase 2›

definition ranks_2 :: "('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set" where
"ranks_2 A a f ≡ {g.
dom g = ⋃((transition A a)  (dom f)) ∧
(∀ q l d. g q = Some (l, d) ⟶
l ≤ ⨅ (fst  Some - f  pred A a q) ∧
(d ⟷ ⨆ (snd  Some - f  pred A a q) ∧ even l) ∧
(accepting A q ⟶ even l))}"
definition complement_succ_2 ::
"('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set" where
"complement_succ_2 A a ≡ ranks_2 A a ∘ refresh_1"
definition complement_2 :: "('label, 'state) nba ⇒ ('label, 'state items) nba" where
"complement_2 A ≡ nba
(alphabet A)
({const (Some (2 * card (nodes A), False)) | initial A})
(complement_succ_2 A)
(λ f. True ∉ snd  ran f)"

lemma ranks_2_refine: "ranks_2 = ranks_1"
proof (intro ext)
fix A :: "('a, 'b) nba" and a f
show "ranks_2 A a f = ranks_1 A a f"
proof safe
fix g
assume 1: "g ∈ ranks_2 A a f"
have 2: "dom g = ⋃((transition A a)  (dom f))" using 1 unfolding ranks_2_def by auto
have 3: "g q = Some (l, d) ⟹ l ≤ ⨅ (fst  Some - f  pred A a q)" for q l d
using 1 unfolding ranks_2_def by auto
have 4: "g q = Some (l, d) ⟹ d ⟷ ⨆ (snd  Some - f  pred A a q) ∧ even l" for q l d
using 1 unfolding ranks_2_def by auto
have 5: "g q = Some (l, d) ⟹ accepting A q ⟹ even l" for q l d
using 1 unfolding ranks_2_def by auto
show "g ∈ ranks_1 A a f"
unfolding ranks_1_def
proof (intro CollectI conjI ballI impI)
show "dom g = ⋃((transition A a)  (dom f))" using 2 by this
next
fix p q
assume 10: "p ∈ dom f" "q ∈ transition A a p"
obtain k c where 11: "f p = Some (k, c)" using 10(1) by auto
have 12: "q ∈ dom g" using 10 2 by auto
obtain l d where 13: "g q = Some (l, d)" using 12 by auto
have "fst (the (g q)) = l" unfolding 13 by simp
also have "… ≤ ⨅ (fst  Some - f  pred A a q)" using 3 13 by this
also have "… ≤ k"
proof (rule cInf_lower)
show "k ∈ fst  Some - f  pred A a q" using 11 10(2) by force
show "bdd_below (fst  Some - f  pred A a q)" by simp
qed
also have "… = fst (the (f p))" unfolding 11 by simp
finally show "fst (the (g q)) ≤ fst (the (f p))" by this
next
fix q
assume 10: "q ∈ dom g" "accepting A q"
show "even (fst (the (g q)))" using 10 5 by auto
next
show "cs_st g = {q ∈ ⋃((transition A a)  (cs_st f)). even (fst (the (g q)))}"
proof
show "cs_st g ⊆ {q ∈ ⋃((transition A a)  (cs_st f)). even (fst (the (g q)))}"
using 4 unfolding cs_st_def image_def vimage_def by auto metis+
show "{q ∈ ⋃((transition A a)  (cs_st f)). even (fst (the (g q)))} ⊆ cs_st g"
proof safe
fix p q
assume 10: "even (fst (the (g q)))" "p ∈ cs_st f" "q ∈ transition A a p"
have 12: "q ∈ dom g" using 10 2 unfolding cs_st_def by auto
show "q ∈ cs_st g" using 10 4 12 unfolding cs_st_def image_def by force
qed
qed
qed
next
fix g
assume 1: "g ∈ ranks_1 A a f"
have 2: "dom g = ⋃((transition A a)  (dom f))" using 1 unfolding ranks_1_def by auto
have 3: "⋀ p q. p ∈ dom f ⟹ q ∈ transition A a p ⟹ fst (the (g q)) ≤ fst (the (f p))"
using 1 unfolding ranks_1_def by auto
have 4: "⋀ q. q ∈ dom g ⟹ accepting A q ⟹ even (fst (the (g q)))"
using 1 unfolding ranks_1_def by auto
have 5: "cs_st g = {q ∈ ⋃((transition A a)  (cs_st f)). even (fst (the (g q)))}"
using 1 unfolding ranks_1_def by auto
show "g ∈ ranks_2 A a f"
unfolding ranks_2_def
proof (intro CollectI conjI allI impI)
show "dom g = ⋃((transition A a)  (dom f))" using 2 by this
next
fix q l d
assume 10: "g q = Some (l, d)"
have 11: "q ∈ dom g" using 10 by auto
show "l ≤ ⨅ (fst  Some - f  pred A a q)"
proof (rule cInf_greatest)
show "fst  Some - f  pred A a q ≠ {}" using 11 unfolding 2 image_def vimage_def by force
show "⋀ x. x ∈ fst  Some - f  pred A a q ⟹ l ≤ x"
using 3 10 by (auto) (metis domI fst_conv option.sel)
qed
have "d ⟷ q ∈ cs_st g" unfolding cs_st_def by (force simp: 10)
also have "cs_st g = {q ∈ ⋃((transition A a)  (cs_st f)). even (fst (the (g q)))}" using 5 by this
also have "q ∈ … ⟷ (∃ x ∈ cs_st f. q ∈ transition A a x) ∧ even l"
unfolding mem_Collect_eq 10 by simp
also have "… ⟷ ⨆ (snd  Some - f  pred A a q) ∧ even l"
unfolding cs_st_def image_def vimage_def by auto metis+
finally show "d ⟷ ⨆ (snd  Some - f  pred A a q) ∧ even l" by this
show "accepting A q ⟹ even l" using 4 10 11 by force
qed
qed
qed

lemma complement_2_refine: "(complement_2, complement_1) ∈ ⟨Id, Id⟩ nba_rel → ⟨Id, Id⟩ nba_rel"
unfolding complement_2_def complement_1_def complement_succ_2_def complement_succ_1_def
unfolding ranks_2_refine cs_st_def image_def vimage_def ran_def by auto

subsection ‹Phase 3›

definition bounds_3 :: "('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items" where
"bounds_3 A a f ≡ λ q. let S = Some - f  pred A a q in
if S = {} then None else Some (⨅(fst  S), ⨆(snd  S))"
definition items_3 :: "('label, 'state) nba ⇒ 'state ⇒ item ⇒ item set" where
"items_3 A p ≡ λ (k, c). {(l, c ∧ even l) |l. l ≤ k ∧ (accepting A p ⟶ even l)}"
definition get_3 :: "('label, 'state) nba ⇒ 'state items ⇒ ('state ⇀ item set)" where
"get_3 A f ≡ λ p. map_option (items_3 A p) (f p)"
definition complement_succ_3 ::
"('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set" where
"complement_succ_3 A a ≡ expand_map ∘ get_3 A ∘ bounds_3 A a ∘ refresh_1"
definition complement_3 :: "('label, 'state) nba ⇒ ('label, 'state items) nba" where
"complement_3 A ≡ nba
(alphabet A)
({(Some ∘ (const (2 * card (nodes A), False))) | initial A})
(complement_succ_3 A)
(λ f. ∀ (p, k, c) ∈ map_to_set f. ¬ c)"

lemma bounds_3_dom[simp]: "dom (bounds_3 A a f) = ⋃((transition A a)  (dom f))"
unfolding bounds_3_def Let_def dom_def by (force split: if_splits)

lemma items_3_nonempty[intro!, simp]: "items_3 A p s ≠ {}" unfolding items_3_def by auto
lemma items_3_finite[intro!, simp]: "finite (items_3 A p s)"
unfolding items_3_def by (auto split: prod.splits)

lemma get_3_dom[simp]: "dom (get_3 A f) = dom f" unfolding get_3_def by (auto split: bind_splits)
lemma get_3_finite[intro, simp]: "S ∈ ran (get_3 A f) ⟹ finite S"
unfolding get_3_def ran_def by auto
lemma get_3_update[simp]: "get_3 A (f (p ↦ s)) = (get_3 A f) (p ↦ items_3 A p s)"
unfolding get_3_def by auto

lemma expand_map_get_bounds_3: "expand_map ∘ get_3 A ∘ bounds_3 A a = ranks_2 A a"
proof (intro ext set_eqI, unfold comp_apply)
fix f g
have 1: "(∀ x S y. get_3 A (bounds_3 A a f) x = Some S ⟶ g x = Some y ⟶ y ∈ S) ⟷
(∀ q S l d. get_3 A (bounds_3 A a f) q = Some S ⟶ g q = Some (l, d) ⟶ (l, d) ∈ S)"
by auto
have 2: "(∀ S. get_3 A (bounds_3 A a f) q = Some S ⟶ g q = Some (l, d) ⟶ (l, d) ∈ S) ⟷
(g q = Some (l, d) ⟶ l ≤ ⨅(fst  (Some - f  pred A a q)) ∧
(d ⟷ ⨆(snd  (Some - f  pred A a q)) ∧ even l) ∧ (accepting A q ⟶ even l))"
if 3: "dom g = ⋃((transition A a)  (dom f))" for q l d
proof -
have 4: "q ∉ dom g" if "Some - f  pred A a q = {}" unfolding 3 using that by force
show ?thesis unfolding get_3_def items_3_def bounds_3_def Let_def using 4 by auto
qed
show "g ∈ expand_map (get_3 A (bounds_3 A a f)) ⟷ g ∈ ranks_2 A a f"
unfolding expand_map_alt_def ranks_2_def mem_Collect_eq
unfolding get_3_dom bounds_3_dom 1 using 2 by blast
qed

lemma complement_succ_3_refine: "complement_succ_3 = complement_succ_2"
unfolding complement_succ_3_def complement_succ_2_def expand_map_get_bounds_3 by rule
lemma complement_initial_3_refine: "{const (Some (2 * card (nodes A), False)) | initial A} =
{(Some ∘ (const (2 * card (nodes A), False))) | initial A}"
unfolding comp_apply by rule
lemma complement_accepting_3_refine: "True ∉ snd  ran f ⟷ (∀ (p, k, c) ∈ map_to_set f. ¬ c)"
unfolding map_to_set_def ran_def by auto

lemma complement_3_refine: "(complement_3, complement_2) ∈ ⟨Id, Id⟩ nba_rel → ⟨Id, Id⟩ nba_rel"
unfolding complement_3_def complement_2_def
unfolding complement_succ_3_refine complement_initial_3_refine complement_accepting_3_refine
by auto

subsection ‹Phase 4›

definition items_4 :: "('label, 'state) nba ⇒ 'state ⇒ item ⇒ item set" where
"items_4 A p ≡ λ (k, c). {(l, c ∧ even l) |l. k ≤ Suc l ∧ l ≤ k ∧ (accepting A p ⟶ even l)}"
definition get_4 :: "('label, 'state) nba ⇒ 'state items ⇒ ('state ⇀ item set)" where
"get_4 A f ≡ λ p. map_option (items_4 A p) (f p)"
definition complement_succ_4 ::
"('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set" where
"complement_succ_4 A a ≡ expand_map ∘ get_4 A ∘ bounds_3 A a ∘ refresh_1"
definition complement_4 :: "('label, 'state) nba ⇒ ('label, 'state items) nba" where
"complement_4 A ≡ nba
(alphabet A)
({(Some ∘ (const (2 * card (nodes A), False))) | initial A})
(complement_succ_4 A)
(λ f. ∀ (p, k, c) ∈ map_to_set f. ¬ c)"

lemma get_4_dom[simp]: "dom (get_4 A f) = dom f" unfolding get_4_def by (auto split: bind_splits)

definition R :: "'state items rel" where
"R ≡ {(f, g).
dom f = dom g ∧
(∀ p ∈ dom f. fst (the (f p)) ≤ fst (the (g p))) ∧
(∀ p ∈ dom f. snd (the (f p)) ⟷ snd (the (g p)))}"

lemma bounds_R:
assumes "(f, g) ∈ R"
assumes "bounds_3 A a (refresh_1 f) p = Some (n, e)"
assumes "bounds_3 A a (refresh_1 g) p = Some (k, c)"
shows "n ≤ k" "e ⟷ c"
proof -
have 1:
"dom f = dom g"
"∀ p ∈ dom f. fst (the (f p)) ≤ fst (the (g p))"
"∀ p ∈ dom f. snd (the (f p)) ⟷ snd (the (g p))"
using assms(1) unfolding R_def by auto
have "n = ⨅(fst  (Some - refresh_1 f  pred A a p))"
using assms(2) unfolding bounds_3_def by (auto simp: Let_def split: if_splits)
also have "fst  Some - refresh_1 f  pred A a p = fst  Some - f  pred A a p"
proof
show " fst  Some - refresh_1 f  pred A a p ⊆ fst  Some - f  pred A a p"
unfolding refresh_1_def image_def
by (auto simp: map_option_case split: option.split) (force)
show "fst  Some - f  pred A a p ⊆ fst  Some - refresh_1 f  pred A a p"
unfolding refresh_1_def image_def
by (auto simp: map_option_case split: option.split) (metis fst_conv option.sel)
qed
also have "… = fst  Some - f  (pred A a p ∩ dom f)"
unfolding dom_def image_def Int_def by auto metis
also have "… = fst  the  f  (pred A a p ∩ dom f)"
unfolding dom_def by force
also have "… = (fst ∘ the ∘ f)  (pred A a p ∩ dom f)" by force
also have "⨅((fst ∘ the ∘ f)  (pred A a p ∩ dom f)) ≤
⨅((fst ∘ the ∘ g)  (pred A a p ∩ dom g))"
proof (rule cINF_mono)
show "pred A a p ∩ dom g ≠ {}"
using assms(2) 1(1) unfolding bounds_3_def refresh_1_def
by (auto simp: Let_def split: if_splits) (force+)
show "bdd_below ((fst ∘ the ∘ f)  (pred A a p ∩ dom f))" by rule
show "∃ n ∈ pred A a p ∩ dom f. (fst ∘ the ∘ f) n ≤ (fst ∘ the ∘ g) m"
if "m ∈ pred A a p ∩ dom g" for m using 1 that by auto
qed
also have "(fst ∘ the ∘ g)  (pred A a p ∩ dom g) = fst  the  g  (pred A a p ∩ dom g)" by force
also have "… = fst  Some - g  (pred A a p ∩ dom g)"
unfolding dom_def by force
also have "… = fst  Some - g  pred A a p"
unfolding dom_def image_def Int_def by auto metis
also have "… = fst  Some - refresh_1 g  pred A a p"
proof
show "fst  Some - g  pred A a p ⊆ fst  Some - refresh_1 g  pred A a p"
unfolding refresh_1_def image_def
by (auto simp: map_option_case split: option.split) (metis fst_conv option.sel)
show "fst  Some - refresh_1 g  pred A a p ⊆ fst  Some - g  pred A a p"
unfolding refresh_1_def image_def
by (auto simp: map_option_case split: option.split) (force)
qed
also have "⨅(fst  (Some - refresh_1 g  pred A a p)) = k"
using assms(3) unfolding bounds_3_def by (auto simp: Let_def split: if_splits)
finally show "n ≤ k" by this
have "e ⟷ ⨆(snd  (Some - refresh_1 f  pred A a p))"
using assms(2) unfolding bounds_3_def by (auto simp: Let_def split: if_splits)
also have "snd  Some - refresh_1 f  pred A a p = snd  Some - refresh_1 f  (pred A a p ∩ dom (refresh_1 f))"
unfolding dom_def image_def Int_def by auto metis
also have "… = snd  the  refresh_1 f  (pred A a p ∩ dom (refresh_1 f))"
unfolding dom_def by force
also have "… = (snd ∘ the ∘ refresh_1 f)  (pred A a p ∩ dom (refresh_1 f))" by force
also have "… = (snd ∘ the ∘ refresh_1 g)  (pred A a p ∩ dom (refresh_1 g))"
proof (rule image_cong)
show "pred A a p ∩ dom (refresh_1 f) = pred A a p ∩ dom (refresh_1 g)"
unfolding refresh_1_dom 1(1) by rule
show "(snd ∘ the ∘ refresh_1 f) q ⟷ (snd ∘ the ∘ refresh_1 g) q"
if 2: "q ∈ pred A a p ∩ dom (refresh_1 g)" for q
proof
have 3: "∀ x ∈ ran f. ¬ snd x ⟹ (n, True) ∈ ran g ⟹ g q = Some (k, c) ⟹ c" for n k c
using 1(1, 3) unfolding dom_def ran_def
by (auto dest!: Collect_inj) (metis option.sel snd_conv)
have 4: "g q = Some (n, True) ⟹ f q = Some (k, c) ⟹ c" for n k c
using 1(3) unfolding dom_def by force
have 5: "∀ x ∈ ran g. ¬ snd x ⟹ (k, True) ∈ ran f ⟹ False" for k
using 1(1, 3) unfolding dom_def ran_def
by (auto dest!: Collect_inj) (metis option.sel snd_conv)
show "(snd ∘ the ∘ refresh_1 f) q ⟹ (snd ∘ the ∘ refresh_1 g) q"
using 1(1, 3) 2 3 unfolding refresh_1_def by (force split: if_splits)
show "(snd ∘ the ∘ refresh_1 g) q ⟹ (snd ∘ the ∘ refresh_1 f) q"
using 1(1, 3) 2 4 5 unfolding refresh_1_def
by (auto simp: map_option_case split: option.splits if_splits) (force+)
qed
qed
also have "… = snd  the  refresh_1 g  (pred A a p ∩ dom (refresh_1 g))" by force
also have "… = snd  Some - refresh_1 g  (pred A a p ∩ dom (refresh_1 g))"
unfolding dom_def by force
also have "… = snd  Some - refresh_1 g  pred A a p"
unfolding dom_def image_def Int_def by auto metis
also have "⨆(snd  (Some - refresh_1 g  pred A a p)) ⟷ c"
using assms(3) unfolding bounds_3_def by (auto simp: Let_def split: if_splits)
finally show "e ⟷ c" by this
qed

lemma complement_4_language_1: "language (complement_3 A) ⊆ language (complement_4 A)"
proof (rule simulation_language)
show "alphabet (complement_3 A) ⊆ alphabet (complement_4 A)"
unfolding complement_3_def complement_4_def by simp
show "∃ q ∈ initial (complement_4 A). (p, q) ∈ R" if "p ∈ initial (complement_3 A)" for p
using that unfolding complement_3_def complement_4_def R_def by simp
show "∃ g' ∈ transition (complement_4 A) a g. (f', g') ∈ R"
if "f' ∈ transition (complement_3 A) a f" "(f, g) ∈ R"
for a f f' g
proof -
have 1: "f' ∈ expand_map (get_3 A (bounds_3 A a (refresh_1 f)))"
using that(1) unfolding complement_3_def complement_succ_3_def by auto
have 2:
"dom f = dom g"
"∀ p ∈ dom f. fst (the (f p)) ≤ fst (the (g p))"
"∀ p ∈ dom f. snd (the (f p)) ⟷ snd (the (g p))"
using that(2) unfolding R_def by auto
have "dom f' = dom (get_3 A (bounds_3 A a (refresh_1 f)))" using expand_map_dom 1 by this
also have "… = dom (bounds_3 A a (refresh_1 f))" by simp
finally have 3: "dom f' = dom (bounds_3 A a (refresh_1 f))" by this
define g' where "g' p ≡ do
{
(k, c) ← bounds_3 A a (refresh_1 g) p;
(l, d) ← f' p;
Some (if even k = even l then k else k - 1, d)
}" for p
have 4: "g' p = do
{
kc ← bounds_3 A a (refresh_1 g) p;
ld ← f' p;
Some (if even (fst kc) = even (fst ld) then fst kc else fst kc - 1, snd ld)
}" for p unfolding g'_def case_prod_beta by rule
have "dom g' = dom (bounds_3 A a (refresh_1 g)) ∩ dom f'" using 4 bind_eq_Some_conv by fastforce
also have "… = dom f'" using 2 3 by simp
finally have 5: "dom g' = dom f'" by this
have 6: "(l, d) ∈ items_3 A p (k, c)"
if "bounds_3 A a (refresh_1 f) p = Some (k, c)" "f' p = Some (l, d)" for p k c l d
using 1 that unfolding expand_map_alt_def get_3_def by blast
show ?thesis
unfolding complement_4_def nba.sel complement_succ_4_def comp_apply
proof
show "(f', g') ∈ R"
unfolding R_def mem_Collect_eq prod.case
proof (intro conjI ballI)
show "dom f' = dom g'" using 5 by rule
next
fix p
assume 10: "p ∈ dom f'"
have 11: "p ∈ dom (bounds_3 A a (refresh_1 g))" using 2(1) 3 10 by simp
obtain k c where 12: "bounds_3 A a (refresh_1 g) p = Some (k, c)" using 11 by fast
obtain l d where 13: "f' p = Some (l, d)" using 10 by auto
obtain n e where 14: "bounds_3 A a (refresh_1 f) p = Some (n, e)" using 10 3 by fast
have 15: "(l, d) ∈ items_3 A p (n, e)" using 6 14 13 by this
have 16: "n ≤ k" using bounds_R(1) that(2) 14 12 by this
have 17: "l ≤ k" using 15 16 unfolding items_3_def by simp
have 18: "even k ⟷ odd l ⟹ l ≤ k ⟹ l ≤ k - 1" by presburger
have 19: "e ⟷ c" using bounds_R(2) that(2) 14 12 by this
show "fst (the (f' p)) ≤ fst (the (g' p))" using 17 18 unfolding 4 12 13 by simp
show "snd (the (f' p)) ⟷ snd (the (g' p))" using 19 unfolding 4 12 13 by simp
qed
show "g' ∈ expand_map (get_4 A (bounds_3 A a (refresh_1 g)))"
unfolding expand_map_alt_def mem_Collect_eq
proof (intro conjI allI impI)
show "dom g' = dom (get_4 A (bounds_3 A a (refresh_1 g)))" using 2(1) 3 5 by simp
fix p S xy
assume 10: "get_4 A (bounds_3 A a (refresh_1 g)) p = Some S"
assume 11: "g' p = Some xy"
obtain k c where 12: "bounds_3 A a (refresh_1 g) p = Some (k, c)" "S = items_4 A p (k, c)"
using 10 unfolding get_4_def by auto
obtain l d where 13: "f' p = Some (l, d)" "xy = (if even k ⟷ even l then k else k - 1, d)"
using 11 12 unfolding g'_def by (auto split: bind_splits)
obtain n e where 14: "bounds_3 A a (refresh_1 f) p = Some (n, e)" using 13(1) 3 by fast
have 15: "(l, d) ∈ items_3 A p (n, e)" using 6 14 13(1) by this
have 16: "n ≤ k" using bounds_R(1) that(2) 14 12(1) by this
have 17: "e ⟷ c" using bounds_R(2) that(2) 14 12(1) by this
show "xy ∈ S" using 15 16 17 unfolding 12(2) 13(2) items_3_def items_4_def by auto
qed
qed
qed
show "⋀ p q. (p, q) ∈ R ⟹ accepting (complement_3 A) p ⟹ accepting (complement_4 A) q"
unfolding complement_3_def complement_4_def R_def map_to_set_def
by (auto) (metis domIff eq_snd_iff option.exhaust_sel option.sel)
qed
lemma complement_4_less: "complement_4 A ≤ complement_3 A"
unfolding less_eq_nba_def
unfolding complement_4_def complement_3_def nba.sel
unfolding complement_succ_4_def complement_succ_3_def
proof (safe intro!: le_funI, unfold comp_apply)
fix a f g
assume "g ∈ expand_map (get_4 A (bounds_3 A a (refresh_1 f)))"
then show "g ∈ expand_map (get_3 A (bounds_3 A a (refresh_1 f)))"
unfolding get_4_def get_3_def items_4_def items_3_def expand_map_alt_def by blast
qed
lemma complement_4_language_2: "language (complement_4 A) ⊆ language (complement_3 A)"
using language_mono complement_4_less by (auto dest: monoD)
lemma complement_4_language: "language (complement_3 A) = language (complement_4 A)"
using complement_4_language_1 complement_4_language_2 by blast

lemma complement_4_finite[simp]:
assumes "finite (nodes A)"
shows "finite (nodes (complement_4 A))"
proof -
have "(nodes (complement_3 A), nodes (complement_2 A)) ∈ ⟨Id⟩ set_rel"
using complement_3_refine by parametricity auto
also have "(nodes (complement_2 A), nodes (complement_1 A)) ∈ ⟨Id⟩ set_rel"
using complement_2_refine by parametricity auto
also have "(nodes (complement_1 A), nodes (complement A)) ∈ ⟨cs_rel⟩ set_rel"
using complement_1_refine by parametricity auto
finally have 1: "(nodes (complement_3 A), nodes (complement A)) ∈ ⟨cs_rel⟩ set_rel" by simp
have 2: "finite (nodes (complement A))" using complement_finite assms(1) by this
have 3: "finite (nodes (complement_3 A))"
using finite_set_rel_transfer_back 1 cs_rel_inv_single_valued 2 by this
have 4: "nodes (complement_4 A) ⊆ nodes (complement_3 A)"
using nodes_mono complement_4_less by (auto dest: monoD)
show "finite (nodes (complement_4 A))" using finite_subset 4 3 by this
qed
lemma complement_4_correct:
assumes "finite (nodes A)"
shows "language (complement_4 A) = streams (alphabet A) - language A"
proof -
have "language (complement_4 A) = language (complement_3 A)"
using complement_4_language by rule
also have "(language (complement_3 A), language (complement_2 A)) ∈ ⟨⟨Id⟩ stream_rel⟩ set_rel"
using complement_3_refine by parametricity auto
also have "(language (complement_2 A), language (complement_1 A)) ∈ ⟨⟨Id⟩ stream_rel⟩ set_rel"
using complement_2_refine by parametricity auto
also have "(language (complement_1 A), language (complement A)) ∈ ⟨⟨Id⟩ stream_rel⟩ set_rel"
using complement_1_refine by parametricity auto
also have "language (complement A) = streams (alphabet A) - language A"
using complement_language assms(1) by this
finally show "language (complement_4 A) = streams (alphabet A) - language A" by simp
qed

subsection ‹Phase 5›

definition refresh_5 :: "'state items ⇒ 'state items nres" where
"refresh_5 f ≡ if ∃ (p, k, c) ∈ map_to_set f. c
then RETURN f
else do
{
ASSUME (finite (dom f));
FOREACH (map_to_set f) (λ (p, k, c) m. do
{
ASSERT (p ∉ dom m);
RETURN (m (p ↦ (k, True)))
}
) Map.empty
}"
definition merge_5 :: "item ⇒ item option ⇒ item" where
"merge_5 ≡ λ (k, c). λ None ⇒ (k, c) | Some (l, d) ⇒ (k ⊓ l, c ⊔ d)"
definition bounds_5 :: "('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items nres" where
"bounds_5 A a f ≡ do
{
ASSUME (finite (dom f));
ASSUME (∀ p. finite (transition A a p));
FOREACH (map_to_set f) (λ (p, s) m.
FOREACH (transition A a p) (λ q f.
RETURN (f (q ↦ merge_5 s (f q))))
m)
Map.empty
}"
definition items_5 :: "('label, 'state) nba ⇒ 'state ⇒ item ⇒ item set" where
"items_5 A p ≡ λ (k, c). do
{
let values = if accepting A p then Set.filter even {k - 1 .. k} else {k - 1 .. k};
let item = λ l. (l, c ∧ even l);
item  values
}"
definition get_5 :: "('label, 'state) nba ⇒ 'state items ⇒ ('state ⇀ item set)" where
"get_5 A f ≡ λ p. map_option (items_5 A p) (f p)"
definition expand_5 :: "('a ⇀ 'b set) ⇒ ('a ⇀ 'b) set nres" where
"expand_5 f ≡ FOREACH (map_to_set f) (λ (x, S) X. do {
ASSERT (∀ g ∈ X. x ∉ dom g);
ASSERT (∀ a ∈ S. ∀ b ∈ S. a ≠ b ⟶ (λ y. (λ g. g (x ↦ y))  X) a ∩ (λ y. (λ g. g (x ↦ y))  X) b = {});
RETURN (⋃ y ∈ S. (λ g. g (x ↦ y))  X)
}) {Map.empty}"
definition complement_succ_5 ::
"('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set nres" where
"complement_succ_5 A a f ≡ do
{
f ← refresh_5 f;
f ← bounds_5 A a f;
ASSUME (finite (dom f));
expand_5 (get_5 A f)
}"

lemma bounds_3_empty: "bounds_3 A a Map.empty = Map.empty"
unfolding bounds_3_def Let_def by auto
lemma bounds_3_update: "bounds_3 A a (f (p ↦ s)) =
override_on (bounds_3 A a f) (Some ∘ merge_5 s ∘ bounds_3 A a (f (p := None))) (transition A a p)"
proof
note fun_upd_image[simp]
fix q
show "bounds_3 A a (f (p ↦ s)) q =
override_on (bounds_3 A a f) (Some ∘ merge_5 s ∘ bounds_3 A a (f (p := None))) (transition A a p) q"
proof (cases "q ∈ transition A a p")
case True
define S where "S ≡ Some - f  (pred A a q - {p})"
have 1: "Some - f (p := Some s)  pred A a q = insert s S" using True unfolding S_def by auto
have 2: "Some - f (p := None)  pred A a q = S" unfolding S_def by auto
have "bounds_3 A a (f (p ↦ s)) q = Some (⨅(fst  (insert s S)), ⨆(snd  (insert s S)))"
unfolding bounds_3_def 1 by simp
also have "… = Some (merge_5 s (bounds_3 A a (f (p := None)) q))"
unfolding 2 bounds_3_def merge_5_def by (cases s) (simp_all add: cInf_insert)
also have "… = override_on (bounds_3 A a f) (Some ∘ merge_5 s ∘ bounds_3 A a (f (p := None)))
(transition A a p) q" using True by simp
finally show ?thesis by this
next
case False
then have "pred A a q ∩ {x. x ≠ p} = pred A a q"
by auto
with False show ?thesis by (simp add: bounds_3_def)
qed
qed

lemma refresh_5_refine: "(refresh_5, λ f. RETURN (refresh_1 f)) ∈ Id → ⟨Id⟩ nres_rel"
proof safe
fix f :: "'a ⇒ item option"
have 1: "(∃ (p, k, c) ∈ map_to_set f. c) ⟷ True ∈ snd  ran f"
unfolding image_def map_to_set_def ran_def by force
show "(refresh_5 f, RETURN (refresh_1 f)) ∈ ⟨Id⟩ nres_rel"
unfolding refresh_5_def refresh_1_def 1
by (refine_vcg FOREACH_rule_map_eq[where X = "λ m. map_option (apsnd ⊤) ∘ m"]) (auto)
qed
lemma bounds_5_refine: "(bounds_5 A a, λ f. RETURN (bounds_3 A a f)) ∈ Id → ⟨Id⟩ nres_rel"
unfolding bounds_5_def by
(refine_vcg FOREACH_rule_map_eq[where X = "bounds_3 A a"] FOREACH_rule_insert_eq)
(auto simp: override_on_insert bounds_3_empty bounds_3_update)
lemma items_5_refine: "items_5 = items_4"
unfolding items_5_def items_4_def by (intro ext) (auto split: if_splits)
lemma get_5_refine: "get_5 = get_4"
unfolding get_5_def get_4_def items_5_refine by rule
lemma expand_5_refine: "(expand_5 f, ASSERT (finite (dom f)) ⪢ RETURN (expand_map f)) ∈ ⟨Id⟩ nres_rel"
unfolding expand_5_def
by (refine_vcg FOREACH_rule_map_eq[where X = expand_map]) (auto dest!: expand_map_dom map_upd_eqD1)

lemma complement_succ_5_refine: "(complement_succ_5, RETURN ∘∘∘ complement_succ_4) ∈
Id → Id → Id → ⟨Id⟩ nres_rel"
unfolding complement_succ_5_def complement_succ_4_def get_5_refine comp_apply
by (refine_vcg vcg1[OF refresh_5_refine] vcg1[OF bounds_5_refine] vcg0[OF expand_5_refine]) (auto)

subsection ‹Phase 6›

definition expand_map_get_6 :: "('label, 'state) nba ⇒ 'state items ⇒ 'state items set nres" where
"expand_map_get_6 A f ≡ FOREACH (map_to_set f) (λ (k, v) X. do {
ASSERT (∀ g ∈ X. k ∉ dom g);
ASSERT (∀ a ∈ (items_5 A k v). ∀ b ∈ (items_5 A k v). a ≠ b ⟶ (λ y. (λ g. g (k ↦ y))  X) a ∩ (λ y. (λ g. g (k ↦ y))  X) b = {});
RETURN (⋃ y ∈ items_5 A k v. (λ g. g (k ↦ y))  X)
}) {Map.empty}"

lemma expand_map_get_6_refine: "(expand_map_get_6, expand_5 ∘∘ get_5) ∈ Id → Id → ⟨Id⟩ nres_rel"
unfolding expand_map_get_6_def expand_5_def get_5_def by (auto intro: FOREACH_rule_map_map[param_fo])

definition complement_succ_6 ::
"('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set nres" where
"complement_succ_6 A a f ≡ do
{
f ← refresh_5 f;
f ← bounds_5 A a f;
ASSUME (finite (dom f));
expand_map_get_6 A f
}"

lemma complement_succ_6_refine:
"(complement_succ_6, complement_succ_5) ∈ Id → Id → Id → ⟨Id⟩ nres_rel"
unfolding complement_succ_6_def complement_succ_5_def
by (refine_vcg vcg2[OF expand_map_get_6_refine]) (auto intro: refine_IdI)

subsection ‹Phase 7›

interpretation autoref_syn by this

context
fixes fi f
assumes fi[autoref_rules]: "(fi, f) ∈ state_rel"
begin

private lemma [simp]: "finite (dom f)"
using list_map_rel_finite fi unfolding finite_map_rel_def by force

schematic_goal refresh_7: "(?f :: ?'a, refresh_5 f) ∈ ?R"

end

concrete_definition refresh_7 uses refresh_7

lemma refresh_7_refine: "(λ f. RETURN (refresh_7 f), refresh_5) ∈ state_rel → ⟨state_rel⟩ nres_rel"
using refresh_7.refine by fast

context
fixes A :: "('label, nat) nba"
fixes succi a fi f
assumes succi[autoref_rules]: "(succi, transition A a) ∈ nat_rel → ⟨nat_rel⟩ list_set_rel"
assumes fi[autoref_rules]: "(fi, f) ∈ state_rel"
begin

private lemma [simp]: "finite (transition A a p)"
using list_set_rel_finite succi[param_fo] unfolding finite_set_rel_def by blast
private lemma [simp]: "finite (dom f)" using fi by force

private lemma [autoref_op_pat]: "transition A a ≡ OP (transition A a)" by simp

private lemma [autoref_rules]: "(min, min) ∈ nat_rel → nat_rel → nat_rel" by simp

schematic_goal bounds_7:
notes ty_REL[where R = "⟨nat_rel, item_rel⟩ dflt_ahm_rel", autoref_tyrel]
shows "(?f :: ?'a, bounds_5 A a f) ∈ ?R"
unfolding bounds_5_def merge_5_def sup_bool_def inf_nat_def by (autoref_monadic (plain))

end

concrete_definition bounds_7 uses bounds_7

lemma bounds_7_refine: "(si, transition A a) ∈ nat_rel → ⟨nat_rel⟩ list_set_rel ⟹
(λ p. RETURN (bounds_7 si p), bounds_5 A a) ∈
state_rel → ⟨⟨nat_rel, item_rel⟩ dflt_ahm_rel⟩ nres_rel"
using bounds_7.refine by auto

context
fixes A :: "('label, nat) nba"
fixes acci
assumes [autoref_rules]: "(acci, accepting A) ∈ nat_rel → bool_rel"
begin

private lemma [autoref_op_pat]: "accepting A ≡ OP (accepting A)" by simp

private lemma [autoref_rules]: "((dvd), (dvd)) ∈ nat_rel → nat_rel → bool_rel" by simp
private lemma [autoref_rules]: "(λ k l. upt k (Suc l), atLeastAtMost) ∈
nat_rel → nat_rel → ⟨nat_rel⟩ list_set_rel"
by (auto simp: list_set_rel_def in_br_conv)

schematic_goal items_7: "(?f :: ?'a, items_5 A) ∈ ?R"
unfolding items_5_def Let_def Set.filter_def by autoref

end

concrete_definition items_7 uses items_7

(* TODO: use generic expand_map implementation *)
context
fixes A :: "('label, nat) nba"
fixes ai
fixes fi f
assumes ai: "(ai, accepting A) ∈ nat_rel → bool_rel"
assumes fi[autoref_rules]: "(fi, f) ∈ ⟨nat_rel, item_rel⟩ dflt_ahm_rel"
begin

private lemma [simp]: "finite (dom f)"
using dflt_ahm_rel_finite_nat fi unfolding finite_map_rel_def by force
private lemma [simp]:
assumes "⋀ m. m ∈ S ⟹ x ∉ dom m"
shows "inj_on (λ m. m (x ↦ y)) S"
using assms unfolding dom_def inj_on_def by (auto) (metis fun_upd_triv fun_upd_upd)
private lemmas [simp] = op_map_update_def[abs_def]

private lemma [autoref_op_pat]: "items_5 A ≡ OP (items_5 A)" by simp

private lemmas [autoref_rules] = items_7.refine[OF ai]

schematic_goal expand_map_get_7: "(?f, expand_map_get_6 A f) ∈
⟨⟨state_rel⟩ list_set_rel⟩ nres_rel"

end

concrete_definition expand_map_get_7 uses expand_map_get_7

lemma expand_map_get_7_refine:
assumes "(ai, accepting A) ∈ nat_rel → bool_rel"
shows "(λ fi. RETURN (expand_map_get_7 ai fi),
λ f. ASSUME (finite (dom f)) ⪢ expand_map_get_6 A f) ∈
⟨nat_rel, item_rel⟩ dflt_ahm_rel → ⟨⟨state_rel⟩ list_set_rel⟩ nres_rel"
using expand_map_get_7.refine[OF assms] by auto

context
fixes A :: "('label, nat) nba"
fixes a :: "'label"
fixes p :: "nat items"
fixes Ai
fixes ai
fixes pi
assumes Ai: "(Ai, A) ∈ ⟨Id, Id⟩ nbai_nba_rel"
assumes ai: "(ai, a) ∈ Id"
assumes pi[autoref_rules]: "(pi, p) ∈ state_rel"
begin

private lemmas succi = nbai_nba_param(4)[THEN fun_relD, OF Ai, THEN fun_relD, OF ai]
private lemmas acceptingi = nbai_nba_param(5)[THEN fun_relD, OF Ai]

private lemma [autoref_op_pat]: "(λ g. ASSUME (finite (dom g)) ⪢ expand_map_get_6 A g) ≡
OP (λ g. ASSUME (finite (dom g)) ⪢ expand_map_get_6 A g)" by simp
private lemma [autoref_op_pat]: "bounds_5 A a ≡ OP (bounds_5 A a)" by simp

private lemmas [autoref_rules] =
refresh_7_refine
bounds_7_refine[OF succi]
expand_map_get_7_refine[OF acceptingi]

schematic_goal complement_succ_7: "(?f :: ?'a, complement_succ_6 A a p) ∈ ?R"

end

concrete_definition complement_succ_7 uses complement_succ_7

lemma complement_succ_7_refine:
"(RETURN ∘∘∘ complement_succ_7, complement_succ_6) ∈
⟨Id, Id⟩ nbai_nba_rel → Id → state_rel →
⟨⟨state_rel⟩ list_set_rel⟩ nres_rel"
using complement_succ_7.refine unfolding comp_apply by parametricity

context
fixes A :: "('label, nat) nba"
fixes Ai
fixes n ni :: nat
assumes Ai: "(Ai, A) ∈ ⟨Id, Id⟩ nbai_nba_rel"
assumes ni[autoref_rules]: "(ni, n) ∈ Id"
begin

private lemma [autoref_op_pat]: "initial A ≡ OP (initial A)" by simp

private lemmas [autoref_rules] = nbai_nba_param(3)[THEN fun_relD, OF Ai]

schematic_goal complement_initial_7:
"(?f, {(Some ∘ (const (2 * n, False))) | initial A}) ∈ ⟨state_rel⟩ list_set_rel"
by autoref

end

concrete_definition complement_initial_7 uses complement_initial_7

schematic_goal complement_accepting_7: "(?f, λ f. ∀ (p, k, c) ∈ map_to_set f. ¬ c) ∈
state_rel → bool_rel"
by autoref

concrete_definition complement_accepting_7 uses complement_accepting_7

definition complement_7 :: "('label, nat) nbai ⇒ nat ⇒ ('label, state) nbai" where
"complement_7 Ai ni ≡ nbai
(alphabeti Ai)
(complement_initial_7 Ai ni)
(complement_succ_7 Ai)
(complement_accepting_7)"

lemma complement_7_refine[autoref_rules]:
assumes "(Ai, A) ∈ ⟨Id, Id⟩ nbai_nba_rel"
assumes "(ni,
(OP card ::: ⟨Id⟩ ahs_rel bhc → nat_rel) $((OP nodes ::: ⟨Id, Id⟩ nbai_nba_rel → ⟨Id⟩ ahs_rel bhc)$ A)) ∈ nat_rel"
shows "(complement_7 Ai ni, (OP complement_4 :::
⟨Id, Id⟩ nbai_nba_rel → ⟨Id, state_rel⟩ nbai_nba_rel) $A) ∈ ⟨Id, state_rel⟩ nbai_nba_rel" proof - note complement_succ_7_refine also note complement_succ_6_refine also note complement_succ_5_refine finally have 1: "(complement_succ_7, complement_succ_4) ∈ ⟨Id, Id⟩ nbai_nba_rel → Id → state_rel → ⟨state_rel⟩ list_set_rel" unfolding nres_rel_comp unfolding nres_rel_def unfolding fun_rel_def by auto show ?thesis unfolding complement_7_def complement_4_def using 1 complement_initial_7.refine complement_accepting_7.refine assms unfolding autoref_tag_defs by parametricity qed end # Theory Formula section ‹Boolean Formulae› theory Formula imports Main begin datatype 'a formula = False | True | Variable 'a | Negation "'a formula" | Conjunction "'a formula" "'a formula" | Disjunction "'a formula" "'a formula" primrec satisfies :: "'a set ⇒ 'a formula ⇒ bool" where "satisfies A False ⟷ HOL.False" | "satisfies A True ⟷ HOL.True" | "satisfies A (Variable a) ⟷ a ∈ A" | "satisfies A (Negation x) ⟷ ¬ satisfies A x" | "satisfies A (Conjunction x y) ⟷ satisfies A x ∧ satisfies A y" | "satisfies A (Disjunction x y) ⟷ satisfies A x ∨ satisfies A y" end # Theory Complementation_Final section ‹Final Instantiation of Algorithms Related to Complementation› theory Complementation_Final imports "Complementation_Implement" "Formula" "Transition_Systems_and_Automata.NBA_Translate" "Transition_Systems_and_Automata.NGBA_Algorithms" "HOL-Library.Multiset" begin subsection ‹Syntax› (* TODO: this syntax has unnecessarily high inner binding strength, requiring extra parentheses the regular let syntax correctly uses inner binding strength 0: ("(2_ =/ _)" 10) *) no_syntax "_do_let" :: "[pttrn, 'a] ⇒ do_bind" ("(2let _ =/ _)" [1000, 13] 13) syntax "_do_let" :: "[pttrn, 'a] ⇒ do_bind" ("(2let _ =/ _)" 13) subsection ‹Hashcodes on Complement States› definition "hci k ≡ uint32_of_nat k * 1103515245 + 12345" definition "hc ≡ λ (p, q, b). hci p + hci q * 31 + (if b then 1 else 0)" definition "list_hash xs ≡ fold ((XOR) ∘ hc) xs 0" lemma list_hash_eq: assumes "distinct xs" "distinct ys" "set xs = set ys" shows "list_hash xs = list_hash ys" proof - have "mset (remdups xs) = mset (remdups ys)" using assms(3) using set_eq_iff_mset_remdups_eq by blast then have "mset xs = mset ys" using assms(1, 2) by (simp add: distinct_remdups_id) have "fold ((XOR) ∘ hc) xs = fold ((XOR) ∘ hc) ys" apply (rule fold_multiset_equiv) apply (simp_all add: fun_eq_iff ac_simps) using ‹mset xs = mset ys› . then show ?thesis unfolding list_hash_def by simp qed definition state_hash :: "nat ⇒ Complementation_Implement.state ⇒ nat" where "state_hash n p ≡ nat_of_hashcode (list_hash p) mod n" lemma state_hash_bounded_hashcode[autoref_ga_rules]: "is_bounded_hashcode state_rel (gen_equals (Gen_Map.gen_ball (foldli ∘ list_map_to_list)) (list_map_lookup (=)) (prod_eq (=) (⟷))) state_hash" proof show [param]: "(gen_equals (Gen_Map.gen_ball (foldli ∘ list_map_to_list)) (list_map_lookup (=)) (prod_eq (=) (⟷)), (=)) ∈ state_rel → state_rel → bool_rel" by autoref show "state_hash n xs = state_hash n ys" if "xs ∈ Domain state_rel" "ys ∈ Domain state_rel" "gen_equals (Gen_Map.gen_ball (foldli ∘ list_map_to_list)) (list_map_lookup (=)) (prod_eq (=) (=)) xs ys" for xs ys n proof - have 1: "distinct (map fst xs)" "distinct (map fst ys)" using that(1, 2) unfolding list_map_rel_def list_map_invar_def by (auto simp: in_br_conv) have 2: "distinct xs" "distinct ys" using 1 by (auto intro: distinct_mapI) have 3: "(xs, map_of xs) ∈ state_rel" "(ys, map_of ys) ∈ state_rel" using 1 unfolding list_map_rel_def list_map_invar_def by (auto simp: in_br_conv) have 4: "(gen_equals (Gen_Map.gen_ball (foldli ∘ list_map_to_list)) (list_map_lookup (=)) (prod_eq (=) (⟷)) xs ys, map_of xs = map_of ys) ∈ bool_rel" using 3 by parametricity have 5: "map_to_set (map_of xs) = map_to_set (map_of ys)" using that(3) 4 by simp have 6: "set xs = set ys" using map_to_set_map_of 1 5 by blast show "state_hash n xs = state_hash n ys" unfolding state_hash_def using list_hash_eq 2 6 by metis qed show "state_hash n x < n" if "1 < n" for n x using that unfolding state_hash_def by simp qed subsection ‹Complementation› schematic_goal complement_impl: assumes [simp]: "finite (NBA.nodes A)" assumes [autoref_rules]: "(Ai, A) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel" shows "(?f :: ?'c, op_translate (complement_4 A)) ∈ ?R" by (autoref_monadic (plain)) concrete_definition complement_impl uses complement_impl theorem complement_impl_correct: assumes "finite (NBA.nodes A)" assumes "(Ai, A) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel" shows "NBA.language (nbae_nba (nbaei_nbae (complement_impl Ai))) = streams (nba.alphabet A) - NBA.language A" using op_translate_language[OF complement_impl.refine[OF assms]] using complement_4_correct[OF assms(1)] by simp subsection ‹Language Subset› definition [simp]: "op_language_subset A B ≡ NBA.language A ⊆ NBA.language B" lemmas [autoref_op_pat] = op_language_subset_def[symmetric] schematic_goal language_subset_impl: assumes [simp]: "finite (NBA.nodes B)" assumes [autoref_rules]: "(Ai, A) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel" assumes [autoref_rules]: "(Bi, B) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel" shows "(?f :: ?'c, do { let AB' = intersect' A (complement_4 B); ASSERT (finite (NGBA.nodes AB')); RETURN (NGBA.language AB' = {}) }) ∈ ?R" by (autoref_monadic (plain)) concrete_definition language_subset_impl uses language_subset_impl lemma language_subset_impl_refine[autoref_rules]: assumes "SIDE_PRECOND (finite (NBA.nodes A))" assumes "SIDE_PRECOND (finite (NBA.nodes B))" assumes "SIDE_PRECOND (nba.alphabet A ⊆ nba.alphabet B)" assumes "(Ai, A) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel" assumes "(Bi, B) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel" shows "(language_subset_impl Ai Bi, (OP op_language_subset ::: ⟨Id, nat_rel⟩ nbai_nba_rel → ⟨Id, nat_rel⟩ nbai_nba_rel → bool_rel)$ A $B) ∈ bool_rel" proof - have "(RETURN (language_subset_impl Ai Bi), do { let AB' = intersect' A (complement_4 B); ASSERT (finite (NGBA.nodes AB')); RETURN (NGBA.language AB' = {}) }) ∈ ⟨bool_rel⟩ nres_rel" using language_subset_impl.refine assms(2, 4, 5) unfolding autoref_tag_defs by this also have "(do { let AB' = intersect' A (complement_4 B); ASSERT (finite (NGBA.nodes AB')); RETURN (NGBA.language AB' = {}) }, RETURN (NBA.language A ⊆ NBA.language B)) ∈ ⟨bool_rel⟩ nres_rel" proof refine_vcg show "finite (NGBA.nodes (intersect' A (complement_4 B)))" using assms(1, 2) by auto have 1: "NBA.language A ⊆ streams (nba.alphabet B)" using nba.language_alphabet streams_mono2 assms(3) unfolding autoref_tag_defs by blast have 2: "NBA.language (complement_4 B) = streams (nba.alphabet B) - NBA.language B" using complement_4_correct assms(2) by auto show "(NGBA.language (intersect' A (complement_4 B)) = {}, NBA.language A ⊆ NBA.language B) ∈ bool_rel" using 1 2 by auto qed finally show ?thesis using RETURN_nres_relD unfolding nres_rel_comp by force qed subsection ‹Language Equality› definition [simp]: "op_language_equal A B ≡ NBA.language A = NBA.language B" lemmas [autoref_op_pat] = op_language_equal_def[symmetric] schematic_goal language_equal_impl: assumes [simp]: "finite (NBA.nodes A)" assumes [simp]: "finite (NBA.nodes B)" assumes [simp]: "nba.alphabet A = nba.alphabet B" assumes [autoref_rules]: "(Ai, A) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel" assumes [autoref_rules]: "(Bi, B) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel" shows "(?f :: ?'c, NBA.language A ⊆ NBA.language B ∧ NBA.language B ⊆ NBA.language A) ∈ ?R" by autoref concrete_definition language_equal_impl uses language_equal_impl lemma language_equal_impl_refine[autoref_rules]: assumes "SIDE_PRECOND (finite (NBA.nodes A))" assumes "SIDE_PRECOND (finite (NBA.nodes B))" assumes "SIDE_PRECOND (nba.alphabet A = nba.alphabet B)" assumes "(Ai, A) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel" assumes "(Bi, B) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel" shows "(language_equal_impl Ai Bi, (OP op_language_equal ::: ⟨Id, nat_rel⟩ nbai_nba_rel → ⟨Id, nat_rel⟩ nbai_nba_rel → bool_rel)$ A $B) ∈ bool_rel" using language_equal_impl.refine[OF assms[unfolded autoref_tag_defs]] by auto schematic_goal product_impl: assumes [simp]: "finite (NBA.nodes B)" assumes [autoref_rules]: "(Ai, A) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel" assumes [autoref_rules]: "(Bi, B) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel" shows "(?f :: ?'c, do { let AB' = intersect A (complement_4 B); ASSERT (finite (NBA.nodes AB')); op_translate AB' }) ∈ ?R" by (autoref_monadic (plain)) concrete_definition product_impl uses product_impl (* TODO: possible optimizations: - introduce op_map_map operation for maps instead of manually iterating via FOREACH - consolidate various binds and maps in expand_map_get_7 *) export_code Set.empty Set.insert Set.member "Inf :: 'a set set ⇒ 'a set" "Sup :: 'a set set ⇒ 'a set" image Pow set nat_of_integer integer_of_nat Variable Negation Conjunction Disjunction satisfies map_formula nbaei alphabetei initialei transitionei acceptingei nbae_nba_impl complement_impl language_equal_impl product_impl in SML module_name Complementation file_prefix Complementation end # Theory Complementation_Build section ‹Build and test exported program with MLton› theory Complementation_Build imports Complementation_Final begin external_file ‹code/Autool.mlb› external_file ‹code/Prelude.sml› external_file ‹code/Autool.sml› compile_generated_files ✐‹contributor Makarius› ‹code/Complementation.ML› (in Complementation_Final) external_files ‹code/Autool.mlb› ‹code/Prelude.sml› ‹code/Autool.sml› export_files ‹code/Complementation.sml› and ‹code/Autool› (exe) where ‹fn dir => let val exec = Generated_Files.execute (dir + Path.basic "code"); val _ = exec ‹Prepare› "mv Complementation.ML Complementation.sml"; val _ = exec ‹Compilation› (File.bash_path \<^path>‹$ISABELLE_MLTON› ^
" -profile time -default-type intinf Autool.mlb");
val _ = exec ‹Test› "./Autool help";
in () end›

end

# File ‹code/Autool.mlb›

\$(SML_LIB)/basis/basis.mlb
Prelude.sml
ann
"nonexhaustiveBind ignore"
"nonexhaustiveMatch ignore"
"redundantBind ignore"
"redundantMatch ignore"
in
Complementation.sml
end
Autool.sml


# File ‹code/Prelude.sml›

structure Unsynchronized =
struct

datatype ref = datatype ref;

end;

fun tracing msg = TextIO.output (TextIO.stdErr, msg ^ "\n");


# File ‹code/Autool.sml›

open Complementation
open String
open List

fun eq x y = (x = y)

fun println w = print (w ^ "\n")

fun return x = [x]
fun bind xs f = concat (map f xs)
fun foldl' y f [] = y
| foldl' y f (x :: xs) = foldl f x xs
fun takeWhile P [] = []
| takeWhile P (x :: xs) = if P x then x :: takeWhile P xs else []
fun lookup x [] = NONE |
lookup x ((k, v) :: xs) = if x = k then SOME v else lookup x xs
fun upto k = if k = 0 then [] else (k - 1) :: upto (k - 1)

fun splitFirst u w =
if w = ""
then if u = "" then SOME ("", "") else NONE
else
if isPrefix u w
then SOME ("", extract (w, size u, NONE))
else case splitFirst u (extract (w, 1, NONE)) of
NONE => NONE |
SOME (v, w') => SOME (str (sub (w, 0)) ^ v, w')
fun split u w = case splitFirst u w of NONE => [w] | SOME (v, w') => v :: split u w'

fun showInt k = Int.toString k
fun parseInt w = case Int.fromString w of SOME n => n

fun showNat k = showInt (integer_of_nat k)
fun parseNat w = nat_of_integer (parseInt w)

fun showString w = "\"" ^ w ^ "\""
fun parseString w = substring (w, 1, size w - 2)

fun showTuple f g (x, y) = "(" ^ f x ^ ", " ^ g y ^ ")"
fun showSequence f xs = concatWith ", " (map f xs)
fun showList f xs = "[" ^ showSequence f xs ^ "]"
fun showSet f (Set xs) = "{" ^ showSequence f xs ^ "}"
| showSet f (Coset xs) = "- {" ^ showSequence f xs ^ "}"

fun showFormula f False = "f"
| showFormula f True = "t"
| showFormula f (Variable v) = f v
| showFormula f (Negation x) = "!" ^ showFormula f x
| showFormula f (Conjunction (x, y)) = "(" ^ showFormula f x ^ " & " ^ showFormula f y ^ ")"
| showFormula f (Disjunction (x, y)) = "(" ^ showFormula f x ^ " | " ^ showFormula f y ^ ")"
fun parseFormula parseVariable input = let
fun parseConstant w cs = if isPrefix w (implode cs) then [(w, drop (cs, size w))] else []
fun parseAtom input1 =
bind (parseConstant "f" input1) (fn (_, input2) =>
return (False, input2))
@
bind (parseConstant "t" input1) (fn (_, input2) =>
return (True, input2))
@
bind (parseVariable input1) (fn (variable, input2) =>
return (Variable variable, input2))
@
bind (parseConstant "(" input1) (fn (_, input2) =>
bind (parseDisjunction input2) (fn (disjunction, input3) =>
bind (parseConstant ")" input3) (fn (_, input4) =>
return (disjunction, input4))))
and parseLiteral input1 =
bind (parseAtom input1) (fn (atom, input2) =>
return (atom, input2))
@
bind (parseConstant "!" input1) (fn (_, input2) =>
bind (parseAtom input2) (fn (atom, input3) =>
return (Negation atom, input3)))
and parseConjunction input1 =
bind (parseLiteral input1) (fn (literal, input2) =>
return (literal, input2))
@
bind (parseLiteral input1) (fn (literal, input2) =>
bind (parseConstant "&" input2) (fn (_, input3) =>
bind (parseConjunction input3) (fn (conjunction, input4) =>
return (Conjunction (literal, conjunction), input4))))
and parseDisjunction input1 =
bind (parseConjunction input1) (fn (conjunction, input2) =>
return (conjunction, input2))
@
bind (parseConjunction input1) (fn (conjunction, input2) =>
bind (parseConstant "|" input2) (fn (_, input3) =>
bind (parseDisjunction input3) (fn (disjunction, input4) =>
return (Disjunction (conjunction, disjunction), input4))))
val input' = filter (not o Char.isSpace) (explode input)
val result = map (fn (exp, _) => exp) (filter (fn (exp, rest) => null rest) (parseDisjunction input'))
in hd result end

datatype hoaProperty =
HoaVersion of string |
HoaName of string |
HoaProperties of string list |
HoaAtomicPropositions of nat * string list |
HoaAcceptanceConditionName of string |
HoaAcceptanceCondition of string |
HoaStartState of nat |
HoaStateCount of nat |
HoaProperty of string * string
datatype hoaTransition = HoaTransition of nat formula * nat
datatype hoaState = HoaState of nat * nat list * hoaTransition list
datatype hoaAutomaton = HoaAutomaton of hoaProperty list * hoaState list

fun showHoaAutomaton (HoaAutomaton (ps, ss)) = let
fun showProperty (HoaVersion w) = "HOA: " ^ w ^ "\n"
| showProperty (HoaName w) = "name: " ^ showString w ^ "\n"
| showProperty (HoaProperties ws) = "properties: " ^ concatWith " " ws ^ "\n"
| showProperty (HoaAtomicPropositions (n, ps)) = "AP: " ^ showNat n ^ " " ^ concatWith " " (map showString ps) ^ "\n"
| showProperty (HoaAcceptanceConditionName w) = "acc-name: " ^ w ^ "\n"
| showProperty (HoaAcceptanceCondition w) = "Acceptance: " ^ w ^ "\n"
| showProperty (HoaStartState p) = "Start: " ^ showNat p ^ "\n"
| showProperty (HoaStateCount n) = "States: " ^ showNat n ^ "\n"
| showProperty (HoaProperty (name, value)) = name ^ ": " ^ value ^ "\n"
fun showTransition (HoaTransition (a, q)) = "[" ^ showFormula showNat a ^ "]" ^ " " ^ showNat q ^ "\n"
fun showState (HoaState (p, cs, ts)) = "State: " ^ showNat p ^ " " ^ showSet showNat (Set cs) ^ "\n" ^ String.concat (map showTransition ts)
in String.concat (map showProperty ps) ^ "--BODY--" ^ "\n" ^ String.concat (map showState ss) ^ "--END--" ^ "\n" end
fun parseHoaAutomaton path = let
fun parseVariable cs = case takeWhile Char.isDigit cs of
[] => [] | xs => [(parseNat (implode xs), drop (cs, length xs))]
fun inputLine input = case TextIO.inputLine input of SOME w => substring (w, 0, size w - 1)
fun parseProperty w = case split ": " w of
["HOA", u] => HoaVersion u |
["name", u] => HoaName (substring (u, 1, size u - 2)) |
["properties", u] => HoaProperties (split " " u) |
["AP", u] => (case split " " u of v :: vs => HoaAtomicPropositions (parseNat v, map parseString vs)) |
["acc-name", u] => HoaAcceptanceConditionName u |
["Acceptance", u] => HoaAcceptanceCondition u |
["Start", u] => HoaStartState (parseNat u) |
["States", u] => HoaStateCount (parseNat u) |
[name, value] => HoaProperty (name, value)
fun parseProperties input = case inputLine input of w =>
if w = "--BODY--" then []
else parseProperty w :: parseProperties input
fun parseTransition w = case split "] " (substring (w, 1, size w - 1)) of
[u, v] => HoaTransition (parseFormula parseVariable u, parseNat v)
fun parseTransitions input = case inputLine input of w =>
if isPrefix "State" w orelse w = "--END--" then ([], w)
else case parseTransitions input of (ts, w') => (parseTransition w :: ts, w')
fun parseStateHeader w = case split " {" w of
[u] => (parseNat u, []) |
[u, "}"] => (parseNat u, []) |
[u, v] => (parseNat u, map parseNat (split ", " (substring (v, 0, size v - 1))))
fun parseState input w =
case split ": " w of ["State", u] =>
case parseStateHeader u of (p, cs) =>
case parseTransitions input of (ts, w') =>
(HoaState (p, cs, ts), w')
fun parseStates input w =
if w = "--END--" then []
else case parseState input w of (p, w') => p :: parseStates input w'
val input = TextIO.openIn path
val properties = parseProperties input
val states = parseStates input (inputLine input)
in HoaAutomaton (properties, states) before TextIO.closeIn input end

fun toNbaei (HoaAutomaton (properties, states)) = let
fun atomicPropositions (HoaAtomicPropositions (_, ps) :: properties) = ps
| atomicPropositions (_ :: properties) = atomicPropositions properties
val aps = atomicPropositions properties
val alphabet = case pow {equal = eq} (Set aps) of Set pps => pps
fun startStates [] = []
| startStates (HoaStartState p :: properties) = p :: startStates properties
| startStates (property :: properties) = startStates properties
val initial = startStates properties
fun mapFormula f = map_formula (fn k => nth (aps, integer_of_nat k)) f
fun expandTransition p f q = map (fn P => (p, (P, q))) (filter (fn x => satisfies {equal = eq} x f) alphabet)
fun stateTransitions (HoaState (p, cs, ts)) = concat (map (fn HoaTransition (f, q) => expandTransition p (mapFormula f) q) ts)
val transitions = concat (map stateTransitions states)
val accepting = map (fn HoaState (p, cs, ts) => p) (filter (fn HoaState (p, cs, ts) => not (null cs)) states)
in (aps, Nbaei (alphabet, initial, transitions, accepting)) end
fun toHoaAutomaton aps (Nbaei (a, i, t, c)) = let
val Set nodes = sup_seta {equal = eq}
(image (fn (p, (_, q)) => insert {equal = eq} p (insert {equal = eq} q bot_set)) (Set t));
val properties =
[HoaVersion "v1"] @
[HoaProperties ["trans-labels", "explicit-labels", "state-acc"]] @
[HoaAtomicPropositions (nat_of_integer (length aps), aps)] @
[HoaAcceptanceConditionName "Buchi"] @
[HoaAcceptanceCondition "1 Inf(0)"] @
map HoaStartState i @
[HoaStateCount (nat_of_integer (length nodes))]
fun literal ps k = if member {equal = eq} (nth (aps, k)) ps
then Variable (nat_of_integer k) else Negation (Variable (nat_of_integer k))
fun formula ps = foldl' True Conjunction (map (literal ps) (upto (length aps)))
fun transitions p = map (fn (p, (a, q)) => HoaTransition (formula a, q)) (filter (fn (p', (a, q)) => p' = p) t)
fun state p = HoaState (p, if member {equal = eq} p (Set c) then [nat_of_integer 0] else [], transitions p)
val states = map state nodes
in HoaAutomaton (properties, states) end

fun showNbaei f g (Nbaei (a, i, t, c)) =
showList f a ^ "\n" ^
showList g i ^ "\n" ^
showList (showTuple g (showTuple f g)) t ^ "\n" ^
showList g c ^ "\n"
fun write_automaton f path automaton = let
fun t (p, (a, q)) = Int.toString (integer_of_nat p) ^ " " ^ f a ^ " " ^ Int.toString (integer_of_nat q) ^ "\n"
val output = TextIO.openOut path
fun write [] = () | write (x :: xs) = (TextIO.output (output, t x); write xs)
val _ = write (transitionei automaton)
val _ = TextIO.closeOut output
in () end

val parameters = CommandLine.arguments ()
val _ = case hd parameters of
"help" => println "Available Commands: help | complement <automaton> | equivalence <automaton1> <automaton2>" |
"complement" => let
val (aps, nbaei) = toNbaei (parseHoaAutomaton (nth (parameters, 1)))
val nbai = nbae_nba_impl eq eq nbaei
val complement = toHoaAutomaton aps (complement_impl nbai)
in print (showHoaAutomaton complement) end |
"complement_quick" => let
val (aps, nbaei) = toNbaei (parseHoaAutomaton (nth (parameters, 1)))
val nbai = nbae_nba_impl eq eq nbaei
val complement = complement_impl nbai
in write_automaton (showSet showString) (nth (parameters, 2)) complement end |
"equivalence" => let
val (aps1, nbaei1) = toNbaei (parseHoaAutomaton (nth (parameters, 1)))
val (aps2, nbaei2) = toNbaei (parseHoaAutomaton (nth (parameters, 2)))
val nbai1 = nbae_nba_impl eq eq nbaei1
val nbai2 = nbae_nba_impl eq eq nbaei2
in println (Bool.toString (language_equal_impl {equal = eq} nbai1 nbai2)) end |
"product" => let
val (aps1, nbaei1) = toNbaei (parseHoaAutomaton (nth (parameters, 1)))
val (aps2, nbaei2) = toNbaei (parseHoaAutomaton (nth (parameters, 2)))
val nbai1 = nbae_nba_impl eq eq nbaei1
val nbai2 = nbae_nba_impl eq eq nbaei2
val product = product_impl {equal = eq} nbai1 nbai2
in write_automaton (showSet showString) (nth (parameters, 3)) product end |
"parse" => let
val ha = parseHoaAutomaton (nth (parameters, 1))
val (aps, nbaei) = toNbaei ha
val _ = println (showNbaei (showSet showString) showNat nbaei)
in print (showHoaAutomaton (toHoaAutomaton aps nbaei)) end