Session Buchi_Complementation

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