# 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) then show ?case by (metis add_0_right le_add1 length_0_conv length_zip min.idem upt_conv_Nil) 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)]" by (simp add: upt_rec) 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) by (metis add.commute shift_snth_ge sscan_const trans_le_add2) also have "f … = smap f (gtrace s v) !! (l + Suc i - length t)" by simp also have "smap f (gtrace s v) = sconst k" unfolding 12 by rule also have "sconst k !! (l + Suc i - length t) = k" by simp finally have 23: "even (f (gtarget (stake (Suc l + Suc i) (t @- s)) u))" using 13 by auto have "snd (gtarget (stake (Suc l + Suc i) (t @- s)) u) ∈ {p ∈ ⋃ (transition A (w !! (Suc l + i)) ` P (Suc l + i)). even (f (Suc (Suc l + i), p))}" using 21 22 23 by (metis (mono_tags) add_Suc_right mem_Collect_eq prod.collapse) also have "… = st_succ A (w !! (Suc l + i)) (fst (?m !! Suc (Suc l + i))) (P (Suc l + i))" unfolding st_succ_def f_def using 20 by simp also have "… = P (Suc (Suc l + i))" unfolding 100(2)[folded P_def] by rule also have "… = P (Suc l + Suc i)" by simp finally show ?case by this qed obtain l' where 16: "l' ≥ Suc l" "P l' = {}" using 4 by auto show "False" using 16 17 using nat_le_iff_add by auto qed qed qed subsection ‹Ranking Implies Word in Complement Language› definition reach where "reach A w i ≡ {target r p |r p. path A r p ∧ p ∈ initial A ∧ map fst r = stake i w}" lemma reach_0[simp]: "reach A w 0 = initial A" unfolding reach_def by auto lemma reach_Suc_empty: assumes "w !! n ∉ alphabet A" shows "reach A w (Suc n) = {}" proof safe fix q assume 1: "q ∈ reach A w (Suc n)" obtain r p where 2: "q = target r p" "path A r p" "p ∈ initial A" "map fst r = stake (Suc n) w" using 1 unfolding reach_def by blast have 3: "path A (take n r @ drop n r) p" using 2(2) by simp have 4: "map fst r = stake n w @ [w !! n]" using 2(4) stake_Suc by auto have 5: "map snd r = take n (map snd r) @ [q]" using 2(1, 4) 4 by (metis One_nat_def Suc_inject Suc_neq_Zero Suc_pred append.right_neutral append_eq_conv_conj drop_map id_take_nth_drop last_ConsR last_conv_nth length_0_conv length_map length_stake lessI nba.target_alt_def nba.states_alt_def zero_less_Suc) have 6: "drop n r = [(w !! n, q)]" using 4 5 by (metis append_eq_conv_conj append_is_Nil_conv append_take_drop_id drop_map length_greater_0_conv length_stake stake_cycle_le stake_invert_Nil take_map zip_Cons_Cons zip_map_fst_snd) show "q ∈ {}" using assms 3 unfolding 6 by auto qed lemma reach_Suc_succ: assumes "w !! n ∈ alphabet A" shows "reach A w (Suc n) = ⋃ (transition A (w !! n) ` reach A w n)" 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)" by (simp add: case_prod_beta') 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" unfolding refresh_5_def by (autoref_monadic (plain)) 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" unfolding expand_map_get_6_def by (autoref_monadic (plain)) 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" unfolding complement_succ_6_def by (autoref_monadic (plain)) 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