Theory Simulation_Graphs

theory Simulation_Graphs
  imports
    "library/CTL"
    "library/More_List"
begin

lemmas [simp] = holds.simps

chapter ‹Simulation Graphs›

section ‹Simulation Graphs›

locale Simulation_Graph_Defs = Graph_Defs C for C :: "'a ⇒ 'a ⇒ bool" +
  fixes A :: "'a set ⇒ 'a set ⇒ bool"
begin

sublocale Steps: Graph_Defs A .

abbreviation "Steps ≡ Steps.steps"
abbreviation "Run ≡ Steps.run"

lemmas Steps_appendD1 = Steps.steps_appendD1

lemmas Steps_appendD2 = Steps.steps_appendD2

lemmas steps_alt_induct = Steps.steps_alt_induct

lemmas Steps_appendI = Steps.steps_appendI

lemmas Steps_cases = Steps.steps.cases

end (* Simulation Graph *)

locale Simulation_Graph_Poststable = Simulation_Graph_Defs +
  assumes poststable: "A S T ⟹ ∀ s' ∈ T. ∃ s ∈ S. C s s'"

locale Simulation_Graph_Prestable = Simulation_Graph_Defs +
  assumes prestable: "A S T ⟹ ∀ s ∈ S. ∃ s' ∈ T. C s s'"

locale Double_Simulation_Defs =
  fixes C :: "'a ⇒ 'a ⇒ bool" ― ‹Concrete step relation›
    and A1 :: "'a set ⇒ 'a set ⇒ bool" ― ‹Step relation for the first abstraction layer›
    and P1 :: "'a set ⇒ bool" ― ‹Valid states of the first abstraction layer›
    and A2 :: "'a set ⇒ 'a set ⇒ bool" ― ‹Step relation for the second abstraction layer›
    and P2 :: "'a set ⇒ bool" ― ‹Valid states of the second abstraction layer›
begin

sublocale Simulation_Graph_Defs C A2 .

sublocale pre_defs: Simulation_Graph_Defs C A1 .

definition "closure a = {x. P1 x ∧ a ∩ x ≠ {}}"

definition "A2' a b ≡ ∃ x y. a = closure x ∧ b = closure y ∧ A2 x y"

sublocale post_defs: Simulation_Graph_Defs A1 A2' .

lemma closure_mono:
  "closure a ⊆ closure b" if "a ⊆ b"
  using that unfolding closure_def by auto

lemma closure_intD:
  "x ∈ closure a ∧ x ∈ closure b" if "x ∈ closure (a ∩ b)"
  using that closure_mono by blast

end (* Double Simulation Graph Defs *)

locale Double_Simulation = Double_Simulation_Defs +
  assumes prestable: "A1 S T ⟹ ∀ s ∈ S. ∃ s' ∈ T. C s s'"
      and closure_poststable: "s' ∈ closure y ⟹ A2 x y ⟹ ∃s∈closure x. A1 s s'"
      and P1_distinct: "P1 x ⟹ P1 y ⟹ x ≠ y ⟹ x ∩ y = {}"
      and P1_finite: "finite {x. P1 x}"
      and P2_cover: "P2 a ⟹ ∃ x. P1 x ∧ x ∩ a ≠ {}"
begin

sublocale post: Simulation_Graph_Poststable A1 A2'
  unfolding A2'_def by standard (auto dest: closure_poststable)

sublocale pre: Simulation_Graph_Prestable C A1
  by standard (rule prestable)

end (* Double Simulation *)

locale Finite_Graph = Graph_Defs +
  fixes x⇩0
  assumes finite_reachable: "finite {x. E⇧*⇧* x⇩0 x}"

locale Simulation_Graph_Complete_Defs =
  Simulation_Graph_Defs C A for C :: "'a ⇒ 'a ⇒ bool" and A :: "'a set ⇒ 'a set ⇒ bool" +
  fixes P :: "'a set ⇒ bool" ― ‹well-formed abstractions›

locale Simulation_Graph_Complete = Simulation_Graph_Complete_Defs +
  simulation: Simulation_Invariant C A "(∈)" "λ _. True" P
begin

lemmas complete = simulation.A_B_step
lemmas P_invariant = simulation.B_invariant

end

locale Simulation_Graph_Finite_Complete = Simulation_Graph_Complete +
  fixes a⇩0
  assumes finite_abstract_reachable: "finite {a. A⇧*⇧* a⇩0 a}"
begin

sublocale Steps_finite: Finite_Graph A a⇩0
  by standard (rule finite_abstract_reachable)

end (* Simulation Graph Finite Complete *)

locale Double_Simulation_Complete = Double_Simulation +
  fixes a⇩0
  assumes complete: "C x y ⟹ x ∈ S ⟹ P2 S ⟹ ∃ T. A2 S T ∧ y ∈ T"
  assumes P2_invariant: "P2 a ⟹ A2 a a' ⟹ P2 a'"
      and P2_a⇩0: "P2 a⇩0"
begin

sublocale Simulation_Graph_Complete C A2 P2
  by standard (blast intro: complete P2_invariant)+

sublocale P2_invariant: Graph_Invariant_Start A2 a⇩0 P2
  by (standard; blast intro: P2_invariant P2_a⇩0)

end (* Double Simulation Finite Complete *)

locale Double_Simulation_Finite_Complete = Double_Simulation_Complete +
  assumes finite_abstract_reachable: "finite {a. A2⇧*⇧* a⇩0 a}"
begin

sublocale Simulation_Graph_Finite_Complete C A2 P2 a⇩0
  by standard (blast intro: complete finite_abstract_reachable P2_invariant)+

end (* Double Simulation Finite Complete *)

locale Simulation_Graph_Complete_Prestable = Simulation_Graph_Complete + Simulation_Graph_Prestable
begin

sublocale Graph_Invariant A P by standard (rule P_invariant)

end (* Simulation Graph Complete Prestable *)

locale Double_Simulation_Complete_Bisim = Double_Simulation_Complete +
assumes A1_complete: "C x y ⟹ P1 S ⟹ x ∈ S ⟹ ∃ T. A1 S T ∧ y ∈ T"
      and P1_invariant: "P1 S ⟹ A1 S T ⟹ P1 T"
begin

sublocale bisim: Simulation_Graph_Complete_Prestable C A1 P1
  by standard (blast intro: A1_complete P1_invariant)+

end (* Double Simulation Finite Complete Bisim *)

locale Double_Simulation_Finite_Complete_Bisim =
  Double_Simulation_Finite_Complete + Double_Simulation_Complete_Bisim

locale Double_Simulation_Complete_Bisim_Cover = Double_Simulation_Complete_Bisim +
  assumes P2_P1_cover: "P2 a ⟹ x ∈ a ⟹ ∃ a'. a ∩ a' ≠ {} ∧ P1 a' ∧ x ∈ a'"

locale Double_Simulation_Finite_Complete_Bisim_Cover =
  Double_Simulation_Finite_Complete_Bisim + Double_Simulation_Complete_Bisim_Cover

locale Double_Simulation_Complete_Abstraction_Prop =
  Double_Simulation_Complete +
  fixes φ :: "'a ⇒ bool" ― ‹The property we want to check›
  assumes φ_A1_compatible: "A1 a b ⟹ b ⊆ {x. φ x} ∨ b ∩ {x. φ x} = {}"
      and φ_P2_compatible: "P2 a ⟹ a ∩ {x. φ x} ≠ {} ⟹ P2 (a ∩ {x. φ x})"
      and φ_A2_compatible: "A2⇧*⇧* a⇩0 a ⟹ a ∩ {x. φ x} ≠ {} ⟹ A2⇧*⇧* a⇩0 (a ∩ {x. φ x})"
      and P2_non_empty: "P2 a ⟹ a ≠ {}"

locale Double_Simulation_Complete_Abstraction_Prop_Bisim =
  Double_Simulation_Complete_Abstraction_Prop + Double_Simulation_Complete_Bisim

locale Double_Simulation_Finite_Complete_Abstraction_Prop =
  Double_Simulation_Complete_Abstraction_Prop + Double_Simulation_Finite_Complete

locale Double_Simulation_Finite_Complete_Abstraction_Prop_Bisim =
  Double_Simulation_Finite_Complete_Abstraction_Prop + Double_Simulation_Finite_Complete_Bisim

section ‹Poststability›

context Simulation_Graph_Poststable
begin

lemma Steps_poststable:
  "∃ xs. steps xs ∧ list_all2 (∈) xs as ∧ last xs = x" if "Steps as" "x ∈ last as"
  using that
proof induction
  case (Single a)
  then show ?case by auto
next
  case (Cons a b as)
  then obtain xs where "A a b" "steps xs" "list_all2 (∈) xs (b # as)" "x = last xs"
    by clarsimp
  then have "hd xs ∈ b" by (cases xs) auto
  with poststable[OF ‹A a b›] obtain y where "y ∈ a" "C y (hd xs)" by auto
  with ‹list_all2 _ _ _› ‹steps _› ‹x = _› show ?case by (cases xs) auto
qed

lemma reaches_poststable:
  "∃ x ∈ a. reaches x y" if "Steps.reaches a b" "y ∈ b"
  using that unfolding reaches_steps_iff Steps.reaches_steps_iff
  apply clarify
  apply (drule Steps_poststable, assumption)
  apply clarify
  subgoal for as xs
    apply (cases "xs = []")
     apply force
    apply (rule bexI[where x = "hd xs"])
    using list.rel_sel by (auto dest: Graph_Defs.steps_non_empty')
  done    

lemma Steps_steps_cycle:
  "∃ x xs. steps (x # xs @ [x]) ∧ (∀ x ∈ set xs. ∃ a ∈ set as ∪ {a}. x ∈ a) ∧ x ∈ a"
  if assms: "Steps (a # as @ [a])" "finite a" "a ≠ {}"
proof -
  define E where
    "E x y = (∃ xs. steps (x # xs @ [y]) ∧ (∀ x ∈ set xs ∪ {x, y}. ∃ a ∈ set as ∪ {a}. x ∈ a))"
    for x y
  from assms(2-) have "∃ x. E x y ∧ x ∈ a" if "y ∈ a" for y
    using that unfolding E_def
    apply simp
    apply (drule Steps_poststable[OF assms(1), simplified])
    apply clarify
    subgoal for xs
      apply (inst_existentials "hd xs" "tl (butlast xs)")
      subgoal by (cases xs) auto
      subgoal by (auto elim: steps.cases dest!: list_all2_set1)
      subgoal by (drule list_all2_set1) (cases xs, auto dest: in_set_butlastD)
      by (cases xs) auto
    done
  with ‹finite a› ‹a ≠ {}› obtain x y where cycle: "E x y" "E⇧*⇧* y x" "x ∈ a"
    by (force dest!: Graph_Defs.directed_graph_indegree_ge_1_cycle')
  have trans[intro]: "E x z" if "E x y" "E y z" for x y z
    using that unfolding E_def
    apply safe
    subgoal for xs ys
      apply (inst_existentials "xs @ y # ys")
       apply (drule steps_append, assumption; simp; fail)
      by (cases ys, auto dest: list.set_sel(2)[rotated] elim: steps.cases)
    done
  have "E x z" if "E⇧*⇧* y z" "E x y" "x ∈ a" for x y z
  using that proof induction
    case base
    then show ?case unfolding E_def by force
  next
    case (step y z)
    then show ?case by auto
  qed
  with cycle have "E x x" by blast
  with ‹x ∈ a› show ?thesis unfolding E_def by auto
qed

end (* Simulation Graph Poststable *)

section ‹Prestability›

context Simulation_Graph_Prestable
begin

lemma Steps_prestable:
  "∃ xs. steps (x # xs) ∧ list_all2 (∈) (x # xs) as" if "Steps as" "x ∈ hd as"
  using that
proof (induction arbitrary: x)
  case (Single a)
  then show ?case by auto
next
  case (Cons a b as)
  from prestable[OF ‹A a b›] ‹x ∈ _› obtain y where "y ∈ b" "C x y" by auto
  with Cons.IH[of y] obtain xs where "y ∈ b" "C x y" "steps (y # xs)" "list_all2 (∈) xs as"
    by clarsimp
  with ‹x ∈ _› show ?case by auto
qed

lemma reaches_prestable:
  "∃ y. reaches x y ∧ y ∈ b" if "Steps.reaches a b" "x ∈ a"
  using that unfolding reaches_steps_iff Steps.reaches_steps_iff
  by (force simp: hd_map last_map dest: list_all2_last dest!: Steps_prestable)

text ‹Abstract cycles lead to concrete infinite runs.›
lemma Steps_run_cycle_buechi:
  "∃ xs. run (x ## xs) ∧ stream_all2 (∈) xs (cycle (as @ [a]))"
  if assms: "Steps (a # as @ [a])" "x ∈ a"
proof -
  note C = Steps_prestable[OF assms(1), simplified]
  define P where "P ≡ λ x xs. steps (last x # xs) ∧ list_all2 (∈) xs (as @ [a])"
  define f where "f ≡ λ x. SOME xs. P x xs"
  from Steps_prestable[OF assms(1)] ‹x ∈ a› obtain ys where ys:
    "steps (x # ys)" "list_all2 (∈) (x # ys) (a # as @ [a])"
    by auto
  define xs where "xs = flat (siterate f ys)"
  from ys have "P [x] ys" unfolding P_def by auto
  from ‹P _ _› have *: "∃ xs. P xs ys" by blast
  have P_1[intro]:"ys ≠ []" if "P xs ys" for xs ys using that unfolding P_def by (cases ys) auto
  have P_2[intro]: "last ys ∈ a" if "P xs ys" for xs ys
    using that P_1[OF that] unfolding P_def by (auto dest:  list_all2_last)
  from * have "stream_all2 (∈) xs (cycle (as @ [a]))"
    unfolding xs_def proof (coinduction arbitrary: ys rule: stream_rel_coinduct_shift)
    case prems: stream_rel
    then have "ys ≠ []" "last ys ∈ a" by (blast dest: P_1 P_2)+
    from ‹ys ≠ []› C[OF ‹last ys ∈ a›] have "∃ xs. P ys xs" unfolding P_def by auto
    from someI_ex[OF this] have "P ys (f ys)" unfolding f_def .
    with ‹ys ≠ []› prems show ?case
      apply (inst_existentials ys "flat (siterate f (f ys))" "as @ [a]" "cycle (as @ [a])")
           apply (subst siterate.ctr; simp; fail)
          apply (subst cycle_decomp; simp; fail)
       by (auto simp: P_def)
  qed
  from * have "run xs"
    unfolding xs_def proof (coinduction arbitrary: ys rule: run_flat_coinduct)
    case prems: (run_shift xs ws xss ys)
    then have "ys ≠ []" "last ys ∈ a" by (blast dest: P_1 P_2)+
    from ‹ys ≠ []› C[OF ‹last ys ∈ a›] have "∃ xs. P ys xs" unfolding P_def by auto
    from someI_ex[OF this] have "P ys (f ys)" unfolding f_def .
    with ‹ys ≠ []› prems show ?case by (auto elim: steps.cases simp: P_def)
  qed
  with P_1[OF ‹P _ _›] ‹steps (x # ys)› have "run (x ## xs)"
    unfolding xs_def
    by (subst siterate.ctr, subst (asm) siterate.ctr) (cases ys; auto elim: steps.cases)
  with ‹stream_all2 _ _ _› show ?thesis by blast
qed

lemma Steps_run_cycle_buechi'':
  "∃ xs. run (x ## xs) ∧ (∀ x ∈ sset xs. ∃ a ∈ set as ∪ {a}. x ∈ a) ∧ infs (λx. x ∈ b) (x ## xs)"
  if assms: "Steps (a # as @ [a])" "x ∈ a" "b ∈ set (a # as @ [a])"
  using Steps_run_cycle_buechi[OF that(1,2)] that(2,3)
  apply safe
  apply (rule exI conjI)+
   apply assumption
  apply (subst alw_ev_stl[symmetric])
  by (force dest: alw_ev_HLD_cycle[of _ _ b] stream_all2_sset1)

lemma Steps_run_cycle_buechi':
  "∃ xs. run (x ## xs) ∧ (∀ x ∈ sset xs. ∃ a ∈ set as ∪ {a}. x ∈ a) ∧ infs (λx. x ∈ a) (x ## xs)"
  if assms: "Steps (a # as @ [a])" "x ∈ a"
  using Steps_run_cycle_buechi''[OF that] ‹x ∈ a› by auto

lemma Steps_run_cycle':
  "∃ xs. run (x ## xs) ∧ (∀ x ∈ sset xs. ∃ a ∈ set as ∪ {a}. x ∈ a)"
  if assms: "Steps (a # as @ [a])" "x ∈ a"
  using Steps_run_cycle_buechi'[OF assms] by auto

lemma Steps_run_cycle:
  "∃ xs. run xs ∧ (∀ x ∈ sset xs. ∃ a ∈ set as ∪ {a}. x ∈ a) ∧ shd xs ∈ a"
  if assms: "Steps (a # as @ [a])" "a ≠ {}"
  using Steps_run_cycle'[OF assms(1)] assms(2) by force

paragraph ‹Unused›

lemma Steps_cycle_every_prestable':
  "∃ b y. C x y ∧ y ∈ b ∧ b ∈ set as ∪ {a}"
  if assms: "Steps (as @ [a])" "x ∈ b" "b ∈ set as"
  using assms
proof (induction "as @ [a]" arbitrary: as)
  case Single
  then show ?case by simp
next
  case (Cons a c xs)
  show ?case
  proof (cases "a = b")
    case True
    with prestable[OF ‹A a c›] ‹x ∈ b› obtain y where "y ∈ c" "C x y"
      by auto
    with ‹a # c # _ = _› show ?thesis
      apply (inst_existentials c y)
    proof (assumption+, cases as, goal_cases)
      case (2 a list)
      then show ?case by (cases list) auto
    qed simp
  next
    case False
    with Cons.hyps(3)[of "tl as"] Cons.prems Cons.hyps(1,2,4-) show ?thesis by (cases as) auto
  qed
qed

lemma Steps_cycle_first_prestable:
  "∃ b y. C x y ∧ x ∈ b ∧ b ∈ set as ∪ {a}" if assms: "Steps (a # as @ [a])" "x ∈ a"
proof (cases as)
  case Nil
  with assms show ?thesis by (auto elim!: Steps_cases dest: prestable)
next
  case (Cons b as)
  with assms show ?thesis by (auto 4 4 elim: Steps_cases dest: prestable)
qed

lemma Steps_cycle_every_prestable:
  "∃ b y. C x y ∧ y ∈ b ∧ b ∈ set as ∪ {a}"
  if assms: "Steps (a # as @ [a])" "x ∈ b" "b ∈ set as ∪ {a}"
  using assms Steps_cycle_every_prestable'[of "a # as" a] Steps_cycle_first_prestable by auto

end (* Simulation Graph Prestable *)


section ‹Double Simulation›

context Double_Simulation
begin

lemma closure_involutive:
  "closure (⋃ (closure x)) = closure x"
  unfolding closure_def by (auto dest: P1_distinct)

lemma closure_finite:
  "finite (closure x)"
  using P1_finite unfolding closure_def by auto

lemma closure_non_empty:
  "closure x ≠ {}" if "P2 x"
  using that unfolding closure_def by (auto dest!: P2_cover)

lemma P1_closure_id:
  "closure R = {R}" if "P1 R" "R ≠ {}"
  unfolding closure_def using that P1_distinct by blast

lemma A2'_A2_closure:
  "A2' (closure x) (closure y)" if "A2 x y"
  using that unfolding A2'_def by auto

lemma Steps_Union:
  "post_defs.Steps (map closure xs)" if "Steps xs"
using that proof (induction xs rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc y xs)
  show ?case
  proof (cases xs rule: rev_cases)
    case Nil
    then show ?thesis by auto
  next
    case (snoc ys z)
    with Steps_appendD1[OF ‹Steps (xs @ [y])›] have "Steps xs" by simp
    then have *: "post_defs.Steps (map closure xs)" by (rule snoc.IH)
    with ‹xs = _› snoc.prems have "A2 z y"
      by (metis Steps.steps_appendD3 append_Cons append_assoc append_self_conv2)
    with ‹A2 z y› have "A2' (closure z) (closure y)" by (auto dest!: A2'_A2_closure)
    with * post_defs.Steps_appendI show ?thesis
      by (simp add: ‹xs = _›)
  qed
qed

lemma closure_reaches:
  "post_defs.Steps.reaches (closure x) (closure y)" if "Steps.reaches x y"
  using that
  unfolding Steps.reaches_steps_iff post_defs.Steps.reaches_steps_iff
  apply clarify
  apply (drule Steps_Union)
  subgoal for xs
    by (cases "xs = []"; force simp: hd_map last_map)
  done

lemma post_Steps_non_empty:
  "x ≠ {}" if "post_defs.Steps (a # as)" "x ∈ b" "b ∈ set as"
  using that
proof (induction "a # as" arbitrary: a as)
  case Single
  then show ?case by auto
next
  case (Cons a c as)
  then show ?case by (auto simp: A2'_def closure_def)
qed

lemma Steps_run_cycle':
  "∃ xs. run xs ∧ (∀ x ∈ sset xs. ∃ a ∈ set as ∪ {a}. x ∈ ⋃ a) ∧ shd xs ∈ ⋃ a"
  if assms: "post_defs.Steps (a # as @ [a])" "finite a" "a ≠ {}"
proof -
  from post.Steps_steps_cycle[OF assms] obtain a1 as1 where guessed:
    "pre_defs.Steps (a1 # as1 @ [a1])"
    "∀x∈set as1. ∃a∈set as ∪ {a}. x ∈ a"
    "a1 ∈ a"
    by atomize_elim
  from assms(1) ‹a1 ∈ a› have "a1 ≠ {}" by (auto dest!: post_Steps_non_empty)
  with guessed pre.Steps_run_cycle[of a1 as1] obtain xs where
    "run xs" "∀x∈sset xs. ∃a∈set as1 ∪ {a1}. x ∈ a" "shd xs ∈ a1"
    by atomize_elim auto
  with guessed(2,3) show ?thesis
    by (inst_existentials xs) (metis Un_iff UnionI empty_iff insert_iff)+
qed

lemma Steps_run_cycle:
  "∃ xs. run xs ∧ (∀ x ∈ sset xs. ∃ a ∈ set as ∪ {a}. x ∈ ⋃ (closure a)) ∧ shd xs ∈ ⋃ (closure a)"
  if assms: "Steps (a # as @ [a])" "P2 a"
proof -
  from Steps_Union[OF assms(1)] have "post_defs.Steps (closure a # map closure as @ [closure a])"
    by simp
  from Steps_run_cycle'[OF this closure_finite closure_non_empty[OF ‹P2 a›]]
    show ?thesis by (force dest: list_all2_set2)
qed

lemma Steps_run_cycle2:
  "∃ x xs. run (x ## xs) ∧ x ∈ ⋃ (closure a⇩0)
  ∧ (∀ x ∈ sset xs. ∃ a ∈ set as ∪ {a} ∪ set bs. x ∈ ⋃ a)
  ∧ infs (λx. x ∈ ⋃ a) (x ## xs)"
  if assms: "post_defs.Steps (closure a⇩0 # as @ a # bs @ [a])" "a ≠ {}"
proof -
  note as1 = assms
  from
    post_defs.Steps.steps_decomp[of "closure a⇩0 # as" "a # bs @ [a]"]
    as1(1)[unfolded this]
  have *:
    "post_defs.Steps (closure a⇩0 # as)"
    "post_defs.Steps (a # bs @ [a])"
    "A2' (last (closure a⇩0 # as)) (a)"
    by (simp split: if_split_asm add: last_map)+
  then have "finite a"
    unfolding A2'_def by (metis closure_finite)
  from post.Steps_steps_cycle[OF *(2) ‹finite a› ‹a ≠ {}›] obtain a1 as1 where as1:
    "pre_defs.Steps (a1 # as1 @ [a1])"
    "∀x∈set as1. ∃a∈set bs ∪ {a}. x ∈ a"
    "a1 ∈ a"
    by atomize_elim
  with post.poststable[OF *(3)] obtain a2 where "a2 ∈ last (closure a⇩0 # as)" "A1 a2 a1"
    by auto
  with post.Steps_poststable[OF *(1), of a2] obtain as2 where as2:
    "pre_defs.Steps as2" "list_all2 (∈) as2 (closure a⇩0 # as)" "last as2 = a2"
    by (auto split: if_split_asm simp: last_map)
  from as2(2) have "hd as2 ∈ closure a⇩0" by (cases as2) auto
  then have "hd as2 ≠ {}" unfolding closure_def by auto
  then obtain x⇩0 where "x⇩0 ∈ hd as2" by auto
  from pre.Steps_prestable[OF as2(1) ‹x⇩0 ∈ _›] obtain xs where xs:
    "steps (x⇩0 # xs)" "list_all2 (∈) (x⇩0 # xs) as2"
    by auto
  with ‹last as2 = a2› have "last (x⇩0 # xs) ∈ a2"
    unfolding list_all2_Cons1 by (auto intro: list_all2_last)
  with pre.prestable[OF ‹A1 a2 a1›] obtain y where "C (last (x⇩0 # xs)) y" "y ∈ a1" by auto
  from pre.Steps_run_cycle_buechi'[OF as1(1) ‹y ∈ a1›] obtain ys where ys:
    "run (y ## ys)" "∀x∈sset ys. ∃a∈set as1 ∪ {a1}. x ∈ a" "infs (λx. x ∈ a1) (y ## ys)"
    by auto
  from ys(3) ‹a1 ∈ a› have "infs (λx. x ∈ ⋃ a) (y ## ys)"
    by (auto simp: HLD_iff elim!: alw_ev_mono)
  from extend_run[OF xs(1) ‹C _ _› ‹run (y ## ys)›] have "run ((x⇩0 # xs) @- y ## ys)" by simp
  then show ?thesis
    apply (inst_existentials x⇩0 "xs @- y ## ys")
      apply (simp; fail)
    using ‹x⇩0 ∈ _› ‹hd as2 ∈ _› apply (auto; fail)
    using xs(2) as2(2) *(2) ‹y ∈ a1› ‹a1 ∈ _› ys(2) as1(2)
    unfolding list_all2_op_map_iff list_all2_Cons1 list_all2_Cons2
      apply auto
       apply (fastforce dest!: list_all2_set1)
     apply blast
    using ‹infs (λx. x ∈ ⋃ a) (y ## ys)›
    by (simp add: sdrop_shift)
qed

lemma Steps_run_cycle'':
  "∃ x xs. run (x ## xs) ∧ x ∈ ⋃ (closure a⇩0)
  ∧ (∀ x ∈ sset xs. ∃ a ∈ set as ∪ {a} ∪ set bs. x ∈ ⋃ (closure a))
  ∧ infs (λx. x ∈ ⋃ (closure a)) (x ## xs)"
  if assms: "Steps (a⇩0 # as @ a # bs @ [a])" "P2 a"
proof -
  from Steps_Union[OF assms(1)] have "post_defs.Steps (map closure (a⇩0 # as @ a # bs @ [a]))"
    by simp
  from Steps_run_cycle2[OF this[simplified] closure_non_empty[OF ‹P2 a›]] show ?thesis
    by clarify (auto simp: image_def intro!: exI conjI)
qed

paragraph ‹Unused›

lemma post_Steps_P1:
  "P1 x" if "post_defs.Steps (a # as)" "x ∈ b" "b ∈ set as"
  using that
proof (induction "a # as" arbitrary: a as)
  case Single
  then show ?case by auto
next
  case (Cons a c as)
  then show ?case by (auto simp: A2'_def closure_def)
qed

lemma strong_compatibility_impl_weak:
  fixes φ :: "'a ⇒ bool" ― ‹The property we want to check›
  assumes φ_closure_compatible: "⋀ x a. x ∈ a ⟹ φ x ⟷ (∀ x ∈ ⋃ (closure a). φ x)"
  shows "φ x ⟹ x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ φ y"
  by (auto simp: closure_def dest: φ_closure_compatible)

end (* Double Simulation Graph *)


section ‹Finite Graphs›

context Finite_Graph
begin

subsection ‹Infinite Büchi Runs Correspond to Finite Cycles›

lemma run_finite_state_set:
  assumes "run (x⇩0 ## xs)"
  shows "finite (sset (x⇩0 ## xs))"
proof -
  let ?S = "{x. E⇧*⇧* x⇩0 x}"
  from run_reachable[OF assms] have "sset xs ⊆ ?S" unfolding stream.pred_set by auto
  moreover have "finite ?S" using finite_reachable by auto
  ultimately show ?thesis by (auto intro: finite_subset)
qed

lemma run_finite_state_set_cycle:
  assumes "run (x⇩0 ## xs)"
  shows
    "∃ ys zs. run (x⇩0 ## ys @- cycle zs) ∧ set ys ∪ set zs ⊆ {x⇩0} ∪ sset xs ∧ zs ≠ []"
proof -
  from run_finite_state_set[OF assms] have "finite (sset (x⇩0 ## xs))" .
  with sdistinct_infinite_sset[of "x⇩0 ## xs"] not_sdistinct_decomp[of "x⇩0 ## xs"] obtain x ws ys zs
    where "x⇩0 ## xs = ws @- x ## ys @- x ## zs"
    by force
  then have decomp: "x⇩0 ## xs = (ws @ [x]) @- ys @- x ## zs" by simp
  from run_decomp[OF assms[unfolded decomp]] have decomp_first:
    "steps (ws @ [x])"
    "run (ys @- x ## zs)"
    "x → (if ys = [] then shd (x ## zs) else hd ys)"
    by auto
  from run_sdrop[OF assms, of "length (ws @ [x])"] have "run (sdrop (length ws) xs)"
    by simp
  moreover from decomp have "sdrop (length ws) xs = ys @- x ## zs"
    by (cases ws; simp add: sdrop_shift)
  ultimately have "run ((ys @ [x]) @- zs)" by simp
  from run_decomp[OF this] have "steps (ys @ [x])" "run zs" "x → shd zs"
    by auto
  from run_cycle[OF this(1)] decomp_first have
    "run (cycle (ys @ [x]))"
    by (force split: if_split_asm)
  with
    extend_run[of "(ws @ [x])" "if ys = [] then shd (x ## zs) else hd ys" "stl (cycle (ys @ [x]))"]
    decomp_first
  have
    "run ((ws @ [x]) @- cycle (ys @ [x]))"
    apply (simp split: if_split_asm)
    subgoal
      using cycle_Cons[of x "[]", simplified] by auto
    apply (cases ys)
     apply (simp; fail)
    by (simp add: cycle_Cons)
  with decomp show ?thesis
    apply (inst_existentials "tl (ws @ [x])" "(ys @ [x])")
    by (cases ws; force)+
qed

(* XXX Duplication *)
lemma buechi_run_finite_state_set_cycle:
  assumes "run (x⇩0 ## xs)" "alw (ev (holds φ)) (x⇩0 ## xs)"
  shows
  "∃ ys zs.
    run (x⇩0 ## ys @- cycle zs) ∧ set ys ∪ set zs ⊆ {x⇩0} ∪ sset xs
    ∧ zs ≠ [] ∧ (∃ x ∈ set zs. φ x)"
proof -
  from run_finite_state_set[OF assms(1)] have "finite (sset (x⇩0 ## xs))" .
  with sset_sfilter[OF ‹alw (ev _) _›] have "finite (sset (sfilter φ (x⇩0 ## xs)))"
    by (rule finite_subset)
  from finite_sset_sfilter_decomp[OF this assms(2)] obtain x ws ys zs where
    decomp: "x⇩0 ## xs = (ws @ [x]) @- ys @- x ## zs" and "φ x"
    by simp metis
  from run_decomp[OF assms(1)[unfolded decomp]] have decomp_first:
    "steps (ws @ [x])"
    "run (ys @- x ## zs)"
    "x → (if ys = [] then shd (x ## zs) else hd ys)"
    by auto
  from run_sdrop[OF assms(1), of "length (ws @ [x])"] have "run (sdrop (length ws) xs)"
    by simp
  moreover from decomp have "sdrop (length ws) xs = ys @- x ## zs"
    by (cases ws; simp add: sdrop_shift)
  ultimately have "run ((ys @ [x]) @- zs)" by simp
  from run_decomp[OF this] have "steps (ys @ [x])" "run zs" "x → shd zs"
    by auto
  from run_cycle[OF this(1)] decomp_first have
    "run (cycle (ys @ [x]))"
    by (force split: if_split_asm)
  with
    extend_run[of "(ws @ [x])" "if ys = [] then shd (x ## zs) else hd ys" "stl (cycle (ys @ [x]))"]
    decomp_first
  have
    "run ((ws @ [x]) @- cycle (ys @ [x]))"
    apply (simp split: if_split_asm)
    subgoal
      using cycle_Cons[of x "[]", simplified] by auto
    apply (cases ys)
     apply (simp; fail)
    by (simp add: cycle_Cons)
  with decomp ‹φ x› show ?thesis
    apply (inst_existentials "tl (ws @ [x])" "(ys @ [x])")
    by (cases ws; force)+
qed

lemma run_finite_state_set_cycle_steps:
  assumes "run (x⇩0 ## xs)"
  shows "∃ x ys zs. steps (x⇩0 # ys @ x # zs @ [x]) ∧ {x} ∪ set ys ∪ set zs ⊆ {x⇩0} ∪ sset xs"
proof -
  from run_finite_state_set_cycle[OF assms] obtain ys zs where guessed:
    "run (x⇩0 ## ys @- cycle zs)"
    "set ys ∪ set zs ⊆ {x⇩0} ∪ sset xs"
    "zs ≠ []"
    by auto
  from ‹zs ≠ []› have "cycle zs = (hd zs # tl zs @ [hd zs]) @- cycle (tl zs @ [hd zs])"
    apply (cases zs)
     apply (simp; fail)
    apply simp
    apply (subst cycle_Cons[symmetric])
    apply (subst cycle_decomp)
    by simp+
  from guessed(1)[unfolded this] have
    "run ((x⇩0 # ys @ hd zs # tl zs @ [hd zs]) @- cycle (tl zs @ [hd zs]))"
    by simp
  from run_decomp[OF this] guessed(2,3) show ?thesis
    by (inst_existentials "hd zs" ys "tl zs") (auto dest: list.set_sel)
qed

(* XXX Duplication *)
lemma buechi_run_finite_state_set_cycle_steps:
  assumes "run (x⇩0 ## xs)" "alw (ev (holds φ)) (x⇩0 ## xs)"
  shows
  "∃ x ys zs.
    steps (x⇩0 # ys @ x # zs @ [x]) ∧ {x} ∪ set ys ∪ set zs ⊆ {x⇩0} ∪ sset xs
    ∧ (∃ y ∈ set (x # zs). φ y)"
proof -
  from buechi_run_finite_state_set_cycle[OF assms] obtain ys zs x where guessed:
    "run (x⇩0 ## ys @- cycle zs)"
    "set ys ∪ set zs ⊆ {x⇩0} ∪ sset xs"
    "zs ≠ []"
    "x ∈ set zs"
    "φ x"
    by safe
  from ‹zs ≠ []› have "cycle zs = (hd zs # tl zs @ [hd zs]) @- cycle (tl zs @ [hd zs])"
    apply (cases zs)
     apply (simp; fail)
    apply simp
    apply (subst cycle_Cons[symmetric])
    apply (subst cycle_decomp)
    by simp+
  from guessed(1)[unfolded this] have
    "run ((x⇩0 # ys @ hd zs # tl zs @ [hd zs]) @- cycle (tl zs @ [hd zs]))"
    by simp
  from run_decomp[OF this] guessed(2,3,4,5) show ?thesis
    by (inst_existentials "hd zs" ys "tl zs") (auto 4 4 dest: list.set_sel)
qed

lemma cycle_steps_run:
  assumes "steps (x⇩0 # ys @ x # zs @ [x])"
  shows "∃ xs. run (x⇩0 ## xs) ∧ sset xs = {x} ∪ set ys ∪ set zs"
proof -
  from assms have "steps (x⇩0 # ys @ [x])" "steps (x # zs @ [x])"
    (* apply (smt Graph_Defs.stepsI append_eq_append_conv2 append_is_Nil_conv hd_append2 list.inject list.sel(1) list.simps(3) steps.cases steps_append_single steps_decomp) *)
     apply (metis Graph_Defs.steps_appendD1 append.assoc append_Cons append_Nil snoc_eq_iff_butlast)
    by (metis Graph_Defs.steps_appendD2 append_Cons assms snoc_eq_iff_butlast)
    
  (*
  proof -
    have f1: "∀as asa asb p. ((asb::'a list) @ asa = [] ∨ Graph_Defs.steps p (asb @ asa)) ∨ ¬ Graph_Defs.steps p (asb @ asa @ as)"
      by (metis (no_types) Graph_Defs.steps_appendD1 append.assoc)
    have f2: "∀as a. [a::'a] @ as = a # as"
      by simp
    have f3: "steps ((x⇩0 # ys) @ (x # zs) @ [x])"
      using assms by fastforce
    have "(x⇩0 # ys) @ x # zs ≠ []"
      by force
    then have "steps ((x⇩0 # ys) @ [x])"
      using f3 f2 f1 by (metis snoc_eq_iff_butlast)
    then show "steps (x⇩0 # ys @ [x])"
      by auto
  *)
  from this(2) have "x → hd (zs @ [x])" "steps (zs @ [x])"
     apply (metis Graph_Defs.steps_decomp last_snoc list.sel(1) list.sel(3) snoc_eq_iff_butlast steps_ConsD steps_append')
    by (meson steps_ConsD ‹steps (x # zs @ [x])› snoc_eq_iff_butlast)
  from run_cycle[OF this(2)] this(1) have "run (cycle (zs @ [x]))" by auto
  with extend_run[OF ‹steps (x⇩0 # ys @ [x])›, of "hd (zs @ [x])" "stl (cycle (zs @ [x]))"] ‹x → _›
  have "run (x⇩0 ## ys @- x ## cycle (zs @ [x]))"
    by simp (metis cycle.ctr)
  then show ?thesis
    by auto
qed

lemma buechi_run_lasso:
  assumes "run (x⇩0 ## xs)" "alw (ev (holds φ)) (x⇩0 ## xs)"
  obtains x where "reaches x⇩0 x" "reaches1 x x" "φ x"
proof -
  from buechi_run_finite_state_set_cycle_steps[OF assms] obtain x ys zs y where
    "steps (x⇩0 # ys @ x # zs @ [x])" "y ∈ set (x # zs)" "φ y"
    by safe
  from ‹y ∈ _› consider "y = x" | as bs where "zs = as @ y # bs"
    by (meson set_ConsD split_list)
  then have "∃ as bs. steps (x⇩0 # as @ [y]) ∧ steps (y # bs @ [y])"
  proof cases
    case 1
    (* XXX Decision procedure *)
    with ‹steps _› show ?thesis
      by simp (metis Graph_Defs.steps_appendD2 append.assoc append_Cons list.distinct(1))
next
  case 2
  with ‹steps _› show ?thesis
    by simp (metis (no_types)
        reaches1_steps steps_reaches append_Cons last_appendR list.distinct(1) list.sel(1)
        reaches1_reaches_iff2 reaches1_steps_append steps_decomp)
qed
  with ‹φ y› show ?thesis
    including graph_automation by (intro that[of y]) (auto intro: steps_reaches1)
qed

end (* Finite Graph *)


section ‹Complete Simulation Graphs›

context Simulation_Graph_Defs
begin

definition "abstract_run x xs = x ## sscan (λ y a. SOME b. A a b ∧ y ∈ b) xs x"

lemma abstract_run_ctr:
  "abstract_run x xs = x ## abstract_run (SOME b. A x b ∧ shd xs ∈ b) (stl xs)"
  unfolding abstract_run_def by (subst sscan.ctr) (rule HOL.refl)

end

context Simulation_Graph_Complete
begin

lemma steps_complete:
  "∃ as. Steps (a # as) ∧ list_all2 (∈) xs as" if "steps (x # xs)" "x ∈ a" "P a"
  using that by (induction xs arbitrary: x a) (erule steps.cases; fastforce dest!: complete)+

lemma abstract_run_Run:
  "Run (abstract_run a xs)" if "run (x ## xs)" "x ∈ a" "P a"
  using that
proof (coinduction arbitrary: a x xs)
  case (run a x xs)
  obtain y ys where "xs = y ## ys" by (metis stream.collapse)
  with run have "C x y" "run (y ## ys)" by (auto elim: run.cases)
  from complete[OF ‹C x y› _ ‹P a› ‹x ∈ a›] obtain b where "A a b ∧ y ∈ b" by auto
  then have "A a (SOME b. A a b ∧ y ∈ b) ∧ y ∈ (SOME b. A a b ∧ y ∈ b)" by (rule someI)
  moreover with ‹P a› have "P (SOME b. A a b ∧ y ∈ b)" by (blast intro: P_invariant)
  ultimately show ?case using ‹run (y ## ys)› unfolding ‹xs = _›
    apply (subst abstract_run_ctr, simp)
    apply (subst abstract_run_ctr, simp)
    by (auto simp: abstract_run_ctr[symmetric])
qed

lemma abstract_run_abstract:
  "stream_all2 (∈) (x ## xs) (abstract_run a xs)" if "run (x ## xs)" "x ∈ a" "P a"
using that proof (coinduction arbitrary: a x xs)
  case run: (stream_rel x' u b' v a x xs)
  obtain y ys where "xs = y ## ys" by (metis stream.collapse)
  with run have "C x y" "run (y ## ys)" by (auto elim: run.cases)
  from complete[OF ‹C x y› _ ‹P a› ‹x ∈ a›] obtain b where "A a b ∧ y ∈ b" by auto
  then have "A a (SOME b. A a b ∧ y ∈ b) ∧ y ∈ (SOME b. A a b ∧ y ∈ b)" by (rule someI)
  with ‹run (y ## ys)› ‹x ∈ a› ‹P a› run(1,2) ‹xs = _› show ?case
    by (subst (asm) abstract_run_ctr) (auto intro: P_invariant)
qed

lemma run_complete:
  "∃ as. Run (a ## as) ∧ stream_all2 (∈) xs as" if "run (x ## xs)" "x ∈ a" "P a"
  using abstract_run_Run[OF that] abstract_run_abstract[OF that]
  apply (subst (asm) abstract_run_ctr)
  apply (subst (asm) (2) abstract_run_ctr)
  by auto

end (* Simulation Graph Complete Abstraction *)


subsection ‹Runs in Finite Complete Graphs›

context Simulation_Graph_Finite_Complete
begin

lemma run_finite_state_set_cycle_steps:
  assumes "run (x⇩0 ## xs)" "x⇩0 ∈ a⇩0" "P a⇩0"
  shows "∃ x ys zs.
    Steps (a⇩0 # ys @ x # zs @ [x]) ∧ (∀ a ∈ {x} ∪ set ys ∪ set zs. ∃ x ∈ {x⇩0} ∪ sset xs. x ∈ a)"
  using run_complete[OF assms]
  apply safe
  apply (drule Steps_finite.run_finite_state_set_cycle_steps)
  apply safe
  subgoal for as x ys zs
    apply (inst_existentials x ys zs)
    using assms(2) by (auto dest: stream_all2_sset2)
  done

lemma buechi_run_finite_state_set_cycle_steps:
  assumes "run (x⇩0 ## xs)" "x⇩0 ∈ a⇩0" "P a⇩0" "alw (ev (holds φ)) (x⇩0 ## xs)"
  shows "∃ x ys zs.
    Steps (a⇩0 # ys @ x # zs @ [x])
    ∧ (∀ a ∈ {x} ∪ set ys ∪ set zs. ∃ x ∈ {x⇩0} ∪ sset xs. x ∈ a)
    ∧ (∃ y ∈ set (x # zs). ∃ a ∈ y. φ a)"
  using run_complete[OF assms(1-3)]
  apply safe
  apply (drule Steps_finite.buechi_run_finite_state_set_cycle_steps[where φ = "λ S. ∃ x ∈ S. φ x"])
  subgoal for as
    using assms(4)
    apply (subst alw_ev_stl[symmetric], simp)
    apply (erule alw_stream_all2_mono[where Q = "ev (holds φ)"], fastforce)
    by (metis (mono_tags, lifting) ev_holds_sset stream_all2_sset1)
  apply safe
  subgoal for as x ys zs y a
    apply (inst_existentials x ys zs)
    using assms(2) by (auto dest: stream_all2_sset2)
  done

lemma buechi_run_finite_state_set_cycle_lasso:
  assumes "run (x⇩0 ## xs)" "x⇩0 ∈ a⇩0" "P a⇩0" "alw (ev (holds φ)) (x⇩0 ## xs)"
  shows "∃a. Steps.reaches a⇩0 a ∧ Steps.reaches1 a a ∧ (∃y ∈ a. φ y)"
proof -
  from buechi_run_finite_state_set_cycle_steps[OF assms] obtain b as bs a y where lasso:
    "Steps (a⇩0 # as @ b # bs @ [b])" "a ∈ set (b # bs)" "y ∈ a" "φ y"
    by safe
  from ‹a ∈ set _› consider "b = a" | bs1 bs2 where "bs = bs1 @ a # bs2"
    using split_list by fastforce
  then have "Steps.reaches a⇩0 a ∧ Steps.reaches1 a a"
    using ‹Steps _›
    apply cases
     apply safe
    subgoal
      by (simp add: Steps.steps_reaches')
    subgoal
      by (blast dest: Steps.stepsD intro: Steps.steps_reaches1)
    subgoal for bs1 bs2
      by (subgoal_tac "Steps ((a⇩0 # as @ b # bs1 @ [a]) @ (bs2 @ [b]))")
        (drule Steps.stepsD, auto elim: Steps.steps_reaches')
    subgoal
      by (metis (no_types)
          Steps.steps_reaches1 Steps.steps_rotate Steps_appendD2 append_Cons append_eq_append_conv2
          list.distinct(1))
    done
  with lasso show ?thesis
    by auto
qed

end (* Simulation Graph Finite Complete Abstraction *)

section ‹Finite Complete Double Simulations›

context Double_Simulation
begin

lemma Run_closure:
  "post_defs.Run (smap closure xs)" if "Run xs"
using that proof (coinduction arbitrary: xs)
  case prems: run
  then obtain x y ys where "xs = x ## y ## ys" "A2 x y" "Run (y ## ys)"
    by (auto elim: Steps.run.cases)
  with A2'_A2_closure[OF ‹A2 x y›] show ?case
    by force
qed

lemma closure_set_finite:
  "finite (closure ` UNIV)" (is "finite ?S")
proof -
  have "?S ⊆ {x. x ⊆ {x. P1 x}}"
    unfolding closure_def by auto
  also have "finite …"
    using P1_finite by auto
  finally show ?thesis .
qed

lemma A2'_empty_step:
  "b = {}" if "A2' a b" "a = {}"
  using that closure_poststable unfolding A2'_def by auto

lemma A2'_empty_invariant:
  "Graph_Invariant A2' (λ x. x = {})"
  by standard (rule A2'_empty_step)

end (* Double Simulation *)

context Double_Simulation_Complete
begin

lemmas P2_invariant_Steps = P2_invariant.invariant_steps

interpretation Steps_finite: Finite_Graph A2' "closure a⇩0"
proof
  have "{x. post_defs.Steps.reaches (closure a⇩0) x} ⊆ closure ` UNIV"
    by (auto 4 3 simp: A2'_def elim: rtranclp.cases)
  also have "finite …"
    by (fact closure_set_finite)
  finally show "finite {x. post_defs.Steps.reaches (closure a⇩0) x}" .
qed

theorem infinite_run_cycle_iff':
  assumes "⋀ x xs. run (x ## xs) ⟹ x ∈ ⋃(closure a⇩0) ⟹ ∃ y ys. y ∈ a⇩0 ∧ run (y ## ys)"
  shows
    "(∃ x⇩0 xs. x⇩0 ∈ ⋃ (closure a⇩0) ∧ run (x⇩0 ## xs)) ⟷
     (∃ as a bs. post_defs.Steps (closure a⇩0 # as @ a # bs @ [a]) ∧ a ≠ {})"
proof (safe, goal_cases)
  case prems: (1 x⇩0 X xs)
  from assms[OF prems(1)] prems(2,3) obtain y ys where "y ∈ a⇩0" "run (y ## ys)"
    by auto
  from run_complete[OF this(2,1) P2_a⇩0] obtain as where "Run (a⇩0 ## as)" "stream_all2 (∈) ys as"
    by auto
  from P2_invariant.invariant_run[OF ‹Run _›] have *: "∀ a ∈ sset (a⇩0 ## as). P2 a"
    unfolding stream.pred_set by auto
  from Steps_finite.run_finite_state_set_cycle_steps[OF Run_closure[OF ‹Run _›, simplified]] show ?case
    using ‹stream_all2 _ _ _› ‹y ∈ _›  * closure_non_empty by force+
next
  case prems: (2 as a bs x)
  with post_defs.Steps.steps_decomp[of "closure a⇩0 # as @ [a]" "bs @ [a]"] have
    "post_defs.Steps (closure a⇩0 # as @ [a])" "post_defs.Steps (bs @ [a])" "A2' a (hd (bs @ [a]))"
    by auto
  from prems(2,3) Steps_run_cycle2[OF prems(1)] show ?case
    by auto
qed

corollary infinite_run_cycle_iff:
  "(∃ x⇩0 xs. x⇩0 ∈ a⇩0 ∧ run (x⇩0 ## xs)) ⟷
   (∃ as a bs. post_defs.Steps (closure a⇩0 # as @ a # bs @ [a]) ∧ a ≠ {})"
  if "⋃(closure a⇩0) = a⇩0" "P2 a⇩0"
  by (subst ‹_ = a⇩0›[symmetric]) (rule infinite_run_cycle_iff', auto simp: that)

context
  fixes φ :: "'a ⇒ bool" ― ‹The property we want to check›
  assumes φ_closure_compatible: "P2 a ⟹ x ∈ ⋃ (closure a) ⟹ φ x ⟷ (∀ x ∈ ⋃ (closure a). φ x)"
begin

text ‹
  We need the condition ‹a ≠ {}› in the following theorem because we cannot prove a lemma like this:
›

lemma
  "∃ bs. Steps bs ∧ closure a # as = map closure bs" if "post_defs.Steps (closure a # as)"
  using that
  oops

text ‹One possible fix would be to add the stronger assumption ‹A2 a b ⟹ P2 b›.›

theorem infinite_buechi_run_cycle_iff_closure:
  assumes
    "⋀ x xs. run (x ## xs) ⟹ x ∈ ⋃(closure a⇩0) ⟹ alw (ev (holds φ)) xs
      ⟹ ∃ y ys. y ∈ a⇩0 ∧ run (y ## ys) ∧ alw (ev (holds φ)) ys"
      and "⋀ a. P2 a ⟹ a ⊆ ⋃ (closure a)"
  shows
  "(∃ x⇩0 xs. x⇩0 ∈ ⋃ (closure a⇩0) ∧ run (x⇩0 ## xs) ∧ alw (ev (holds φ)) (x⇩0 ## xs))
  ⟷ (∃ as a bs. a ≠ {} ∧ post_defs.Steps (closure a⇩0 # as @ a # bs @ [a]) ∧ (∀ x ∈ ⋃ a. φ x))"
proof (safe, goal_cases)
  case prems: (1 x⇩0 xs)
  from assms(1)[OF prems(3)] prems(1,2,4) obtain y ys where
    "y ∈ a⇩0" "run (y ## ys)" "alw (ev (holds φ)) ys"
    by auto
  from run_complete[OF this(2,1) P2_a⇩0] obtain as where "Run (a⇩0 ## as)" "stream_all2 (∈) ys as"
    by auto
  from P2_invariant.invariant_run[OF ‹Run _›] have "pred_stream P2 (a⇩0 ## as)"
    by auto
  from Run_closure[OF ‹Run _›] have "post_defs.Run (closure a⇩0 ## smap closure as)"
    by simp
  from ‹alw (ev (holds φ)) ys› ‹stream_all2 _ _ _› have "alw (ev (holds (λ a. ∃ x ∈ a. φ x))) as"
    by (rule alw_ev_lockstep) auto
  then have "alw (ev (holds (λ a. ∃ x ∈ ⋃ a. φ x))) (closure a⇩0 ## smap closure as)"
    apply -
    apply rule
    apply (rule alw_ev_lockstep[where Q = "λ a b. b = closure a ∧ P2 a"], assumption)
    subgoal
      using ‹Run (a⇩0 ## as)›
      by - (rule stream_all2_combine[where P = "eq_onp P2" and Q = "λ a b. b = closure a"],
            subst stream.pred_rel[symmetric],
            auto dest: P2_invariant.invariant_run simp: stream.rel_refl eq_onp_def
           )
    subgoal for a x
      by (auto dest!: assms(2))
    done
  from Steps_finite.buechi_run_finite_state_set_cycle_steps[OF ‹post_defs.Run (_ ## _)› this]
  obtain a ys zs where guessed:
    "post_defs.Steps (closure a⇩0 # ys @ a # zs @ [a])"
    "a = closure a⇩0 ∨ a ∈ closure ` sset as"
    "set ys ⊆ insert (closure a⇩0) (closure ` sset as)"
    "set zs ⊆ insert (closure a⇩0) (closure ` sset as)"
    "(∃y∈a. ∃x∈y. φ x) ∨ (∃y∈set zs. ∃y'∈y. ∃x∈y'. φ x)"
    by clarsimp
  from guessed(5) show ?case
  proof (standard, goal_cases)
    case prems: 1
    from guessed(1) have "post_defs.Steps (closure a⇩0 # ys @ [a])"
      by (metis
          Graph_Defs.graphI(3) Graph_Defs.steps_decomp append.simps(2) list.sel(1) list.simps(3)
         )
    from ‹pred_stream _ _› guessed(2) obtain a' where "a = closure a'" "P2 a'"
      by (auto simp: stream.pred_set)
    from prems obtain x R where "x ∈ R" "R ∈ a" "φ x" by auto
    with ‹P2 a'› have "∀ x ∈ ⋃ a. φ x"
      unfolding ‹a = _› by (subst φ_closure_compatible[symmetric]) auto
    with guessed(1,2) show ?case
      using ‹R ∈ a› by blast
  next
    case prems: 2
    then obtain R b x where *: "x ∈ R" "R ∈ b" "b ∈ set zs" "φ x"
      by auto
    from ‹b ∈ set zs› obtain zs1 zs2 where "zs = zs1 @ b # zs2" by (force simp: split_list)
    with guessed(1) have "post_defs.Steps ((closure a⇩0 # ys @ a # zs1 @ [b]) @ zs2 @ [a])"
      by simp
    with guessed(1) have "post_defs.Steps (closure a⇩0 # ys @ a # zs1 @ [b])"
      by - (drule Graph_Defs.steps_decomp, auto)
    from ‹pred_stream _ _› guessed(4) ‹zs = _› obtain b' where "b = closure b'" "P2 b'"
      by (auto simp: stream.pred_set)
    with * have *: "∀ x ∈ ⋃ b. φ x"
      unfolding ‹b = _› by (subst φ_closure_compatible[symmetric]) auto
    from ‹zs = _› guessed(1) have "post_defs.Steps ((closure a⇩0 # ys) @ (a # zs1 @ [b]) @ zs2 @ [a])"
      by simp
    then have "post_defs.Steps (a # zs1 @ [b])" by (blast dest!: post_defs.Steps.steps_decomp)
    with ‹zs = _› guessed * show ?case
      using
        ‹R ∈ b›
        post_defs.Steps.steps_append[of "closure a⇩0 # ys @ a # zs1 @ b # zs2 @ [a]" "a # zs1 @ [b]"]
      by (inst_existentials "ys @ a # zs1" b "zs2 @ a # zs1") auto
  qed
next
  case prems: (2 as a bs x)
  then have "a ≠ {}"
    by auto
  from prems post_defs.Steps.steps_decomp[of "closure a⇩0 # as @ [a]" "bs @ [a]"] have
    "post_defs.Steps (closure a⇩0 # as @ [a])"
    by auto
  with Steps_run_cycle2[OF prems(1) ‹a ≠ {}›] prems show ?case
    unfolding HLD_iff by clarify (drule alw_ev_mono[where ψ = "holds φ"], auto)
qed

end (* Context for Fixed Formula *)

end (* Double Simulation Finite Complete Abstraction *)

context Double_Simulation_Finite_Complete
begin

lemmas P2_invariant_Steps = P2_invariant.invariant_steps

theorem infinite_run_cycle_iff':
  assumes "P2 a⇩0" "⋀ x xs. run (x ## xs) ⟹ x ∈ ⋃(closure a⇩0) ⟹ ∃ y ys. y ∈ a⇩0 ∧ run (y ## ys)"
  shows "(∃ x⇩0 xs. x⇩0 ∈ a⇩0 ∧ run (x⇩0 ## xs)) ⟷ (∃ as a bs. Steps (a⇩0 # as @ a # bs @ [a]))"
proof (safe, goal_cases)
  case (1 x⇩0 xs)
  from run_finite_state_set_cycle_steps[OF this(2,1)] ‹P2 a⇩0› show ?case by auto
next
  case prems: (2 as a bs)
  with Steps.steps_decomp[of "a⇩0 # as @ [a]" "bs @ [a]"] have "Steps (a⇩0 # as @ [a])" by auto
  from P2_invariant_Steps[OF this] have "P2 a" by auto
  from Steps_run_cycle''[OF prems this] assms(2) show ?case by auto
qed

corollary infinite_run_cycle_iff:
  "(∃ x⇩0 xs. x⇩0 ∈ a⇩0 ∧ run (x⇩0 ## xs)) ⟷ (∃ as a bs. Steps (a⇩0 # as @ a # bs @ [a]))"
  if "⋃(closure a⇩0) = a⇩0" "P2 a⇩0"
  by (rule infinite_run_cycle_iff', auto simp: that)

context
  fixes φ :: "'a ⇒ bool" ― ‹The property we want to check›
  assumes φ_closure_compatible: "x ∈ a ⟹ φ x ⟷ (∀ x ∈ ⋃(closure a). φ x)"
begin

theorem infinite_buechi_run_cycle_iff:
  "(∃ x⇩0 xs. x⇩0 ∈ a⇩0 ∧ run (x⇩0 ## xs) ∧ alw (ev (holds φ)) (x⇩0 ## xs))
  ⟷ (∃ as a bs. Steps (a⇩0 # as @ a # bs @ [a]) ∧ (∀ x ∈ ⋃(closure a). φ x))"
  if "⋃(closure a⇩0) = a⇩0"
proof (safe, goal_cases)
  case (1 x⇩0 xs)
  from buechi_run_finite_state_set_cycle_steps[OF this(2,1) P2_a⇩0, of φ] this(3) obtain a ys zs
    where
    "infs φ xs"
    "Steps (a⇩0 # ys @ a # zs @ [a])"
    "x⇩0 ∈ a ∨ (∃x∈sset xs. x ∈ a)"
    "∀a∈set ys ∪ set zs. x⇩0 ∈ a ∨ (∃x∈sset xs. x ∈ a)"
    "(∃x∈a. φ x) ∨ (∃y∈set zs. ∃x∈y. φ x)"
    by clarsimp
  note guessed = this(2-)
  from guessed(4) show ?case
  proof (standard, goal_cases)
    case 1
    then obtain x where "x ∈ a" "φ x" by auto
    with φ_closure_compatible have "∀ x ∈ ⋃(closure a). φ x" by blast
    with guessed(1,2) show ?case by auto
  next
    case 2
    then obtain b x where "x ∈ b" "b ∈ set zs" "φ x" by auto
    with φ_closure_compatible have *: "∀ x ∈ ⋃(closure b). φ x" by blast
    from ‹b ∈ set zs› obtain zs1 zs2 where "zs = zs1 @ b # zs2" by (force simp: split_list)
    with guessed(1) have "Steps ((a⇩0 # ys) @ (a # zs1 @ [b]) @ zs2 @ [a])" by simp
    then have "Steps (a # zs1 @ [b])" by (blast dest!: Steps.steps_decomp)
    with ‹zs = _› guessed * show ?case
      apply (inst_existentials "ys @ a # zs1" b "zs2 @ a # zs1")
      using Steps.steps_append[of "a⇩0 # ys @ a # zs1 @ b # zs2 @ [a]" "a # zs1 @ [b]"]
      by auto
  qed
next
  case prems: (2 as a bs)
  with Steps.steps_decomp[of "a⇩0 # as @ [a]" "bs @ [a]"] have "Steps (a⇩0 # as @ [a])" by auto
  from P2_invariant_Steps[OF this] have "P2 a" by auto
  from Steps_run_cycle''[OF prems(1) this] prems this that show ?case
    apply safe
    subgoal for x xs b
      by (inst_existentials x xs) (auto elim!: alw_ev_mono)
    done
qed

end (* Context for Fixed Formula *)

end (* Double Simulation Finite Complete Abstraction *)


section ‹Encoding of Properties in Runs›

text ‹
  This approach only works if we assume strong compatibility of the property.
  For weak compatibility, encoding in the automaton is likely the right way.
›

context Double_Simulation_Complete_Abstraction_Prop
begin

definition "C_φ x y ≡ C x y ∧ φ y"
definition "A1_φ a b ≡ A1 a b ∧ b ⊆ {x. φ x}"
definition "A2_φ S S' ≡ ∃ S''. A2 S S'' ∧ S'' ∩ {x. φ x} = S' ∧ S' ≠ {}"

lemma A2_φ_P2_invariant:
  "P2 a" if "A2_φ⇧*⇧* a⇩0 a"
proof -
  interpret invariant: Graph_Invariant_Start A2_φ a⇩0 P2
    by standard (auto intro: φ_P2_compatible P2_invariant P2_a⇩0 simp: A2_φ_def)
  from invariant.invariant_reaches[OF that] show ?thesis .
qed

sublocale phi: Double_Simulation_Complete C_φ A1_φ P1 A2_φ P2 a⇩0
proof (standard, goal_cases)
  case (1 S T)
  then show ?case unfolding A1_φ_def C_φ_def by (auto 4 4 dest: φ_A1_compatible prestable)
next
  case (2 y b a)
  then obtain c where "A2 a c" "c ∩ {x. φ x} = b" unfolding A2_φ_def by auto
  with ‹y ∈ _› have "y ∈ closure c" by (auto dest: closure_intD)
  moreover have "y ⊆ {x. φ x}"
    by (smt "2"(1) φ_A1_compatible ‹A2 a c› ‹c ∩ {x. φ x} = b› ‹y ∈ closure c› closure_def
        closure_poststable inf_assoc inf_bot_right inf_commute mem_Collect_eq)
  ultimately show ?case using ‹A2 a c› unfolding A1_φ_def A2_φ_def
    by (auto dest: closure_poststable)
next
  case (3 x y)
  then show ?case by (rule P1_distinct)
next
  case 4
  then show ?case by (rule P1_finite)
next
  case (5 a)
  then show ?case by (rule P2_cover)
next
  case (6 x y S)
  then show ?case unfolding C_φ_def A2_φ_def by (auto dest!: complete)
next
  case (7 a a')
  then show ?case unfolding A2_φ_def by (auto intro: P2_invariant φ_P2_compatible)
next
  case 8
  then show ?case by (rule P2_a⇩0)
qed

lemma phi_run_iff:
  "phi.run (x ## xs) ∧ φ x ⟷ run (x ## xs) ∧ pred_stream φ (x ## xs)"
proof -
  have "phi.run xs" if "run xs" "pred_stream φ xs" for xs
    using that by (coinduction arbitrary: xs) (auto elim: run.cases simp: C_φ_def)
  moreover have "run xs" if "phi.run xs" for xs
    using that by (coinduction arbitrary: xs) (auto elim: phi.run.cases simp: C_φ_def)
  moreover have "pred_stream φ xs" if "phi.run (x ## xs)" "φ x"
    using that by (coinduction arbitrary: xs x) (auto 4 3 elim: phi.run.cases simp: C_φ_def)
  ultimately show ?thesis by auto
qed

end (* Double Simulation Complete Abstraction Prop *)

context Double_Simulation_Finite_Complete_Abstraction_Prop
begin

sublocale phi: Double_Simulation_Finite_Complete C_φ A1_φ P1 A2_φ P2 a⇩0
proof (standard, goal_cases)
  case 1
  have "{a. A2_φ⇧*⇧* a⇩0 a} ⊆ {a. Steps.reaches a⇩0 a}"
    apply safe
    subgoal premises prems for x
        using prems
        proof (induction x1 ≡ a⇩0 x rule: rtranclp.induct)
          case rtrancl_refl
          then show ?case by blast
        next
          case prems: (rtrancl_into_rtrancl b c)
          then have "c ≠ {}"
            by - (rule P2_non_empty, auto intro: A2_φ_P2_invariant)
          from ‹A2_φ b c› obtain S'' x where
            "A2 b S''" "c = S'' ∩ {x. φ x}" "x ∈ S''" "φ x"
            unfolding A2_φ_def by auto
          with prems ‹c ≠ {}› φ_A2_compatible[of S''] show ?case
            including graph_automation_aggressive by auto
        qed
    done
  then show ?case (is "finite ?S") using finite_abstract_reachable by (rule finite_subset)
qed

corollary infinite_run_cycle_iff:
  "(∃ x⇩0 xs. x⇩0 ∈ a⇩0 ∧ run (x⇩0 ## xs) ∧ pred_stream φ (x⇩0 ## xs)) ⟷
   (∃ as a bs. phi.Steps (a⇩0 # as @ a # bs @ [a]))"
  if "⋃(closure a⇩0) = a⇩0" "a⇩0 ⊆ {x. φ x}"
  unfolding phi.infinite_run_cycle_iff[OF that(1) P2_a⇩0, symmetric] phi_run_iff[symmetric]
  using that(2) by auto

theorem Alw_ev_mc:
  "(∀ x⇩0 ∈ a⇩0. Alw_ev (Not o φ) x⇩0) ⟷ ¬ (∃ as a bs. phi.Steps (a⇩0 # as @ a # bs @ [a]))"
  if "⋃(closure a⇩0) = a⇩0" "a⇩0 ⊆ {x. φ x}"
  unfolding Alw_ev alw_holds_pred_stream_iff infinite_run_cycle_iff[OF that, symmetric]
  by (auto simp: comp_def)

end (* Double Simulation Finite Complete Abstraction Prop *)

context Simulation_Graph_Defs
begin

definition "represent_run x as = x ## sscan (λ b x. SOME y. C x y ∧ y ∈ b) as x"

lemma represent_run_ctr:
  "represent_run x as = x ## represent_run (SOME y. C x y ∧ y ∈ shd as) (stl as)"
  unfolding represent_run_def by (subst sscan.ctr) (rule HOL.refl)

end (* Simulation Graph Defs *)

context Simulation_Graph_Prestable
begin

lemma represent_run_Run:
  "run (represent_run x as)" if "Run (a ## as)" "x ∈ a"
using that
proof (coinduction arbitrary: a x as)
  case (run a x as)
  obtain b bs where "as = b ## bs" by (metis stream.collapse)
  with run have "A a b" "Run (b ## bs)" by (auto elim: Steps.run.cases)
  from prestable[OF ‹A a b›] ‹x ∈ a› obtain y where "C x y ∧ y ∈ b" by auto
  then have "C x (SOME y. C x y ∧ y ∈ b) ∧ (SOME y. C x y ∧ y ∈ b) ∈ b" by (rule someI)
  then show ?case using ‹Run (b ## bs)› unfolding ‹as = _›
    apply (subst represent_run_ctr, simp)
    apply (subst represent_run_ctr, simp)
    by (auto simp: represent_run_ctr[symmetric])
qed

lemma represent_run_represent:
  "stream_all2 (∈) (represent_run x as) (a ## as)" if "Run (a ## as)" "x ∈ a"
using that
proof (coinduction arbitrary: a x as)
  case (stream_rel x' xs a' as' a x as)
  obtain b bs where "as = b ## bs" by (metis stream.collapse)
  with stream_rel have "A a b" "Run (b ## bs)" by (auto elim: Steps.run.cases)
  from prestable[OF ‹A a b›] ‹x ∈ a› obtain y where "C x y ∧ y ∈ b" by auto
  then have "C x (SOME y. C x y ∧ y ∈ b) ∧ (SOME y. C x y ∧ y ∈ b) ∈ b" by (rule someI)
  with ‹x' ## xs = _› ‹a' ## as' = _› ‹x ∈ a› ‹Run (b ## bs)› show ?case unfolding ‹as = _›
    by (subst (asm) represent_run_ctr) auto
qed

end (* Simulation Graph Prestable *)

context Simulation_Graph_Complete_Prestable
begin

lemma step_bisim:
  "∃y'. C x' y' ∧ (∃a. P a ∧ y ∈ a ∧ y' ∈ a)" if "C x y" "x ∈ a" "x' ∈ a" "P a"
proof -
  from complete[OF ‹C x y› _ ‹P a› ‹x ∈ a›] obtain b' where "A a b'" "y ∈ b'"
    by auto
  from prestable[OF ‹A a b'›] ‹x' ∈ a› obtain y' where "y' ∈ b'" "C x' y'"
    by auto
  with ‹P a› ‹A a b'› ‹y ∈ b'› show ?thesis
    by auto
qed

sublocale steps_bisim:
  Bisimulation_Invariant C C "λ x y. ∃ a. P a ∧ x ∈ a ∧ y ∈ a" "λ _. True" "λ _. True"
  by (standard; meson step_bisim)

lemma runs_bisim:
  "∃ ys. run (y ## ys) ∧ stream_all2 (λ x y. ∃ a. x ∈ a ∧ y ∈ a ∧ P a) xs ys"
  if "run (x ## xs)" "x ∈ a" "y ∈ a" "P a"
  using that
  by - (drule steps_bisim.bisim.A_B.simulation_run[of _ _ y],
        auto elim!: stream_all2_weaken simp: steps_bisim.equiv'_def
       )

lemma runs_bisim':
  "∃ ys. run (y ## ys)" if "run (x ## xs)" "x ∈ a" "y ∈ a" "P a"
  using runs_bisim[OF that] by blast

context
  fixes Q :: "'a ⇒ bool"
  assumes compatible: "Q x ⟹ x ∈ a ⟹ y ∈ a ⟹ P a ⟹ Q y"
begin

lemma Alw_ev_compatible':
  assumes "∀xs. run (x ## xs) ⟶ ev (holds Q) (x ## xs)" "run (y ## xs)" "x ∈ a" "y ∈ a" "P a"
  shows "ev (holds Q) (y ## xs)"
proof -
  from assms obtain ys where "run (x ## ys)" "stream_all2 steps_bisim.equiv' xs ys"
    by (auto 4 3 simp: steps_bisim.equiv'_def dest: steps_bisim.bisim.A_B.simulation_run)
  with assms(1) have "ev (holds Q) (x ## ys)"
    by auto
  from ‹stream_all2 _ _ _› assms have "stream_all2 steps_bisim.B_A.equiv' (x ## ys) (y ## xs)"
    by (fastforce
          simp: steps_bisim.equiv'_def steps_bisim.A_B.equiv'_def
          intro: steps_bisim.stream_all2_rotate_2
       )
  then show ?thesis
    by - (rule steps_bisim.ev_ψ_φ[OF _ _ ‹ev _ _›],
          auto dest: compatible simp: steps_bisim.A_B.equiv'_def
         )
qed

lemma Alw_ev_compatible:
  "Alw_ev Q x ⟷ Alw_ev Q y" if "x ∈ a" "y ∈ a" "P a"
  unfolding Alw_ev_def using that by (auto intro: Alw_ev_compatible')

end (* Context for Compatibility *)

lemma steps_bisim:
  "∃ ys. steps (y # ys) ∧ list_all2 (λ x y. ∃ a. x ∈ a ∧ y ∈ a ∧ P a) xs ys"
  if "steps (x # xs)" "x ∈ a" "y ∈ a" "P a"
  using that
  by (auto 4 4
      dest: steps_bisim.bisim.A_B.simulation_steps
      intro: list_all2_mono simp: steps_bisim.equiv'_def
     )

end (* Simulation Graph Complete Prestable *)

context Subgraph_Node_Defs
begin

lemma subgraph_runD:
  "run xs" if "G'.run xs"
  by (metis G'.run.cases run.coinduct subgraph that)

lemma subgraph_V_all:
  "pred_stream V xs" if "G'.run xs"
  by (metis (no_types, lifting) G'.run.simps Subgraph_Node_Defs.E'_V1 stream.inject stream_pred_coinduct that)

lemma subgraph_runI:
  "G'.run xs" if "pred_stream V xs" "run xs"
  using that 
  by (coinduction arbitrary: xs) (metis Subgraph_Node_Defs.E'_def run.cases stream.pred_inject)

lemma subgraph_run_iff:
  "G'.run xs ⟷ pred_stream V xs ∧ run xs"
  using subgraph_V_all subgraph_runD subgraph_runI by blast

end

context Double_Simulation_Finite_Complete_Abstraction_Prop_Bisim
begin

sublocale sim_complete: Simulation_Graph_Complete_Prestable C_φ A1_φ P1
  by (standard; force dest: P1_invariant φ_A1_compatible A1_complete simp: C_φ_def A1_φ_def)

lemma runs_closure_bisim:
  "∃y ys. y ∈ a⇩0 ∧ phi.run (y ## ys)" if "phi.run (x ## xs)" "x ∈ ⋃(phi.closure a⇩0)"
  using that(2) sim_complete.runs_bisim'[OF that(1)] unfolding phi.closure_def by auto

lemma infinite_run_cycle_iff':
  "(∃x⇩0 xs. x⇩0 ∈ a⇩0 ∧ phi.run (x⇩0 ## xs)) = (∃as a bs. phi.Steps (a⇩0 # as @ a # bs @ [a]))"
  by (intro phi.infinite_run_cycle_iff' P2_a⇩0 runs_closure_bisim)

corollary infinite_run_cycle_iff:
  "(∃ x⇩0 xs. x⇩0 ∈ a⇩0 ∧ run (x⇩0 ## xs) ∧ pred_stream φ (x⇩0 ## xs)) ⟷
   (∃ as a bs. phi.Steps (a⇩0 # as @ a # bs @ [a]))"
  if "a⇩0 ⊆ {x. φ x}"
  unfolding infinite_run_cycle_iff'[symmetric] phi_run_iff[symmetric] using that by auto

theorem Alw_ev_mc:
  "(∀ x⇩0 ∈ a⇩0. Alw_ev (Not o φ) x⇩0) ⟷ ¬ (∃ as a bs. phi.Steps (a⇩0 # as @ a # bs @ [a]))"
  if "a⇩0 ⊆ {x. φ x}"
  unfolding Alw_ev alw_holds_pred_stream_iff infinite_run_cycle_iff[OF that, symmetric]
  by (auto simp: comp_def)

(* XXX Move? *)
lemma phi_Steps_Alw_ev:
  "¬ (∃ as a bs. phi.Steps (a⇩0 # as @ a # bs @ [a])) ⟷ phi.Steps.Alw_ev (λ _. False) a⇩0"
  unfolding phi.Steps.Alw_ev
  by (auto 4 3 dest:
      sdrop_wait phi.Steps_finite.run_finite_state_set_cycle_steps phi.Steps_finite.cycle_steps_run
      simp: not_alw_iff comp_def
     )

theorem Alw_ev_mc':
  "(∀ x⇩0 ∈ a⇩0. Alw_ev (Not o φ) x⇩0) ⟷ phi.Steps.Alw_ev (λ _. False) a⇩0"
  if "a⇩0 ⊆ {x. φ x}"
  unfolding Alw_ev_mc[OF that] phi_Steps_Alw_ev[symmetric] ..

end (* Double Simulation Finite Complete Abstraction Prop *)

context Graph_Start_Defs
begin

interpretation Bisimulation_Invariant E E "(=)" reachable reachable
  including graph_automation by standard auto

lemma Alw_alw_iff_default:
  "Alw_alw φ x ⟷ Alw_alw ψ x" if "⋀ x. reachable x ⟹ φ x ⟷ ψ x" "reachable x"
  by (rule Alw_alw_iff_strong) (auto simp: that A_B.equiv'_def)

lemma Alw_ev_iff_default:
  "Alw_ev φ x ⟷ Alw_ev ψ x" if "⋀ x. reachable x ⟹ φ x ⟷ ψ x" "reachable x"
  by (rule Alw_ev_iff) (auto simp: that A_B.equiv'_def)

end (* Graph Start Defs *)

context Double_Simulation_Complete_Bisim_Cover
begin

lemma P2_closure_subs:
  "a ⊆ ⋃(closure a)" if "P2 a"
  using P2_P1_cover[OF that] unfolding closure_def by fastforce

lemma (in Double_Simulation_Complete) P2_Steps_last:
  "P2 (last as)" if "Steps as" "a⇩0 = hd as"
  using that by - (cases as, auto dest!: P2_invariant_Steps simp: list_all_iff P2_a⇩0)

lemma (in Double_Simulation) compatible_closure:
  assumes compatible: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y"
      and "∀ x ∈ a. P x"
    shows "∀ x ∈ ⋃(closure a). P x"
  unfolding closure_def using assms(2) by (auto dest: compatible)

lemma compatible_closure_all_iff:
  assumes compatible: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y" and "P2 a"
  shows "(∀ x ∈ a. P x) ⟷ (∀ x ∈ ⋃(closure a). P x)"
  using ‹P2 a› by (auto dest!: P2_closure_subs dest: compatible simp: closure_def)

lemma compatible_closure_ex_iff:
  assumes compatible: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y" and "P2 a"
  shows "(∃ x ∈ a. P x) ⟷ (∃ x ∈ ⋃(closure a). P x)"
  using ‹P2 a› by (auto 4 3 dest!: P2_closure_subs dest: compatible P2_cover simp: closure_def)

lemma (in Double_Simulation_Complete_Bisim) no_deadlock_closureI:
  "∀ x⇩0 ∈ ⋃(closure a⇩0). ¬ deadlock x⇩0" if "∀ x⇩0 ∈ a⇩0. ¬ deadlock x⇩0"
  using that by - (rule compatible_closure, simp, rule bisim.steps_bisim.deadlock_iff, auto)

context
  fixes P
  assumes P1_P: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y"
begin

lemma reaches_all_1:
  fixes b :: "'a set" and y :: "'a" and as :: "'a set list"
  assumes A: "∀y. (∃x⇩0∈⋃(closure (hd as)). ∃xs. hd xs = x⇩0 ∧ last xs = y ∧ steps xs) ⟶ P y"
     and "y ∈ last as" and "a⇩0 = hd as" and "Steps as"
  shows "P y"
proof -
  from assms obtain bs where [simp]: "as = a⇩0 # bs" by (cases as) auto
  from Steps_Union[OF ‹Steps _›] have "post_defs.Steps (map closure as)" .
  from ‹Steps as› ‹a⇩0 = _› have "P2 (last as)"
    by (rule P2_Steps_last)
  obtain b2 where b2: "y ∈ b2" "b2 ∈ last (closure a⇩0 # map closure bs)"
    apply atomize_elim
    apply simp
    apply safe
    using ‹y ∈ _› P2_closure_subs[OF ‹P2 (last as)›]
    by (auto simp: last_map)
  with post.Steps_poststable[OF ‹post_defs.Steps _›, of b2] obtain as' where as':
    "pre_defs.Steps as'" "list_all2 (∈) as' (closure a⇩0 # map closure bs)" "last as' = b2"
    by auto
  then obtain x⇩0 where "x⇩0 ∈ hd as'"
    by (cases as') (auto split: if_split_asm simp: closure_def)
  from pre.Steps_prestable[OF ‹pre_defs.Steps _› ‹x⇩0 ∈ _›] obtain xs where
    "steps (x⇩0 # xs)" "list_all2 (∈) (x⇩0 # xs) as'"
    by auto
  from ‹x⇩0 ∈ _› ‹list_all2 (∈) as' _› have "x⇩0 ∈ ⋃(closure a⇩0)"
    by (cases as') auto
  with A ‹steps _› have "P (last (x⇩0 # xs))"
    by fastforce
  from as' have "P1 b2"
    using b2 by (auto simp: closure_def last_map split: if_split_asm)
  from ‹list_all2 (∈) as' _› ‹list_all2 (∈) _ as'› ‹_ = b2› have "last (x⇩0 # xs) ∈ b2"
     by (fastforce dest!: list_all2_last)
  from P1_P[OF this ‹y ∈ b2› ‹P1 b2›] ‹P _› show "P y" ..
qed

lemma reaches_all_2:
  fixes x⇩0 a xs
  assumes A: "∀b y. (∃xs. hd xs = a⇩0 ∧ last xs = b ∧ Steps xs) ∧ y ∈ b ⟶ P y"
    and "hd xs ∈ a" and "a ∈ closure a⇩0" and "steps xs"
  shows "P (last xs)"
proof -
  {
    fix y x⇩0 xs
    assume "hd xs ∈ a⇩0" and "steps xs"
    then obtain x ys where [simp]: "xs = x # ys" "x ∈ a⇩0" by (cases xs) auto
    from steps_complete[of x ys a⇩0] ‹steps xs› P2_a⇩0 obtain as where
      "Steps (a⇩0 # as)" "list_all2 (∈) ys as"
      by auto
    then have "last xs ∈ last (a⇩0 # as)"
      by (fastforce dest: list_all2_last)
    with A ‹Steps _› ‹x ∈ _› have "P (last xs)"
      by (force split: if_split_asm)
  } note * = this
  from ‹a ∈ closure a⇩0› obtain x where x: "x ∈ a" "x ∈ a⇩0" "P1 a"
    by (auto simp: closure_def)
  with ‹hd xs ∈ a› ‹steps xs› bisim.steps_bisim[of "hd xs" "tl xs" a x] obtain xs' where
    "hd xs' = x" "steps xs'" "list_all2 (λ x y. ∃ a. x ∈ a ∧ y ∈ a ∧ P1 a) xs xs'"
    apply atomize_elim
    apply clarsimp
    subgoal for ys
      by (inst_existentials "x # ys"; force simp: list_all2_Cons2)
    done
  with *[of xs'] x have "P (last xs')"
    by auto
  from ‹steps xs› ‹list_all2 _ xs xs'› obtain b where "last xs ∈ b" "last xs' ∈ b" "P1 b"
    by atomize_elim (fastforce dest!: list_all2_last)
  from P1_P[OF this] ‹P (last xs')› show "P (last xs)" ..
qed

lemma reaches_all:
  "(∀ y. (∃ x⇩0∈⋃(closure a⇩0). reaches x⇩0 y) ⟶ P y) ⟷ (∀ b y. Steps.reaches a⇩0 b ∧ y ∈ b ⟶ P y)"
  unfolding reaches_steps_iff Steps.reaches_steps_iff using reaches_all_1 reaches_all_2 by auto

lemma reaches_all':
  "(∀x⇩0∈⋃(closure a⇩0). ∀y. reaches x⇩0 y ⟶ P y) = (∀y. Steps.reaches a⇩0 y ⟶ (∀x∈y. P x))"
  using reaches_all by auto

lemma reaches_all'':
  "(∀ y. ∀ x⇩0∈a⇩0. reaches x⇩0 y ⟶ P y) ⟷ (∀ b y. Steps.reaches a⇩0 b ∧ y ∈ b ⟶ P y)"
proof -
  have "(∀x⇩0∈a⇩0. ∀y. reaches x⇩0 y ⟶ P y) ⟷ (∀x⇩0∈⋃(closure a⇩0). ∀y. reaches x⇩0 y ⟶ P y)"
    apply (rule compatible_closure_all_iff[OF _ P2_a⇩0])
    apply safe
    subgoal for a x y y'
      by (blast dest: P1_P bisim.steps_bisim.A_B.simulation_reaches[of _ _ x])
    subgoal for a x y y'
      by (blast dest: P1_P bisim.steps_bisim.A_B.simulation_reaches[of _ _ y])
    done
  from this[unfolded reaches_all'] show ?thesis
    by auto
qed

lemma reaches_ex:
  "(∃y. ∃x⇩0∈⋃(closure a⇩0). reaches x⇩0 y ∧ P y) = (∃b y. Steps.reaches a⇩0 b ∧ y ∈ b ∧ P y)"
proof (safe, goal_cases)
  case (1 y x⇩0 X)
  then obtain x where "x ∈ X" "x ∈ a⇩0" "P1 X"
    unfolding closure_def by auto
  with ‹x⇩0 ∈ _› ‹reaches _ _› obtain y' Y where "reaches x y'" "P1 Y" "y' ∈ Y" "y ∈ Y"
    by (auto dest: bisim.steps_bisim.A_B.simulation_reaches[of _ _ x])
  with simulation.simulation_reaches[OF ‹reaches x y'› ‹x ∈ a⇩0› _ P2_a⇩0] ‹P _› show ?case
    by (auto dest: P1_P)
next
  case (2 b y)
  with ‹y ∈ b› obtain Y where "y ∈ Y" "Y ∈ closure b" "P1 Y"
    unfolding closure_def
    by (metis (mono_tags, lifting) P2_P1_cover P2_invariant.invariant_reaches mem_Collect_eq)
  from closure_reaches[OF ‹Steps.reaches _ _›] have
    "post_defs.Steps.reaches (closure a⇩0) (closure b)"
    by auto
  from post.reaches_poststable[OF this ‹Y ∈ _›] obtain X where
    "X ∈ closure a⇩0 " "pre_defs.Steps.reaches X Y"
    by auto
  then obtain x where "x ∈ X" "x ∈ a⇩0"
    unfolding closure_def by auto
  from pre.reaches_prestable[OF ‹pre_defs.Steps.reaches X Y› ‹x ∈ X›] obtain y' where
    "reaches x y'" "y' ∈ Y"
    by auto
  with ‹x ∈ X› ‹X ∈ _› ‹P y› ‹P1 Y› ‹y ∈ Y› show ?case
    by (auto dest: P1_P)
qed

lemma reaches_ex':
  "(∃ y. ∃ x⇩0∈a⇩0. reaches x⇩0 y ∧ P y) ⟷ (∃ b y. Steps.reaches a⇩0 b ∧ y ∈ b ∧ P y)"
proof -
  (* XXX Move this one and others *)
  have "(∃x⇩0∈a⇩0. ∃y. reaches x⇩0 y ∧ P y) ⟷ (∃x⇩0∈⋃(closure a⇩0). ∃y. reaches x⇩0 y ∧ P y)"
    apply (rule compatible_closure_ex_iff[OF _ P2_a⇩0])
    apply safe
    subgoal for a x y y'
      by (blast dest: P1_P bisim.steps_bisim.A_B.simulation_reaches[of _ _ y])
    subgoal for a x y y'
      by (blast dest: P1_P bisim.steps_bisim.A_B.simulation_reaches[of _ _ x])
    done
  from this reaches_ex show ?thesis
    by auto
qed

end (* Context for Compatibility *)

lemma (in Double_Simulation_Complete_Bisim) P1_deadlocked_compatible:
  "deadlocked x = deadlocked y" if "x ∈ a" "y ∈ a" "P1 a" for x y a
  unfolding deadlocked_def using that apply auto
  subgoal
    using A1_complete prestable by blast
  subgoal using A1_complete prestable by blast
  done

lemma steps_Steps_no_deadlock:
  "¬ Steps.deadlock a⇩0"
  if no_deadlock: "∀ x⇩0 ∈ ⋃(closure a⇩0). ¬ deadlock x⇩0"
proof -
  from P1_deadlocked_compatible have
    "(∀y. (∃x⇩0∈⋃(closure a⇩0). reaches x⇩0 y) ⟶ (Not ∘ deadlocked) y) =
     (∀b y. Steps.reaches a⇩0 b ∧ y ∈ b ⟶ (Not ∘ deadlocked) y)"
    using reaches_all[of "Not o deadlocked"] unfolding comp_def by blast
  then show "¬ Steps.deadlock a⇩0"
    using no_deadlock
    unfolding Steps.deadlock_def deadlock_def
    apply safe
    subgoal
      by (simp add: Graph_Defs.deadlocked_def)
         (metis  P2_cover P2_invariant.invariant_reaches disjoint_iff_not_equal simulation.A_B_step)
    subgoal 
      by auto
    done
qed

lemma steps_Steps_no_deadlock1:
  "¬ Steps.deadlock a⇩0"
  if no_deadlock: "∀ x⇩0 ∈ a⇩0. ¬ deadlock x⇩0" and closure_simp: "⋃(closure a⇩0) = a⇩0"
  using steps_Steps_no_deadlock[unfolded closure_simp, OF no_deadlock] .

lemma Alw_alw_iff:
  "(∀ x⇩0 ∈ ⋃(closure a⇩0). Alw_alw P x⇩0) ⟷ Steps.Alw_alw (λ a. ∀ c ∈ a. P c) a⇩0"
  if P1_P: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y"
  and no_deadlock: "∀ x⇩0 ∈ ⋃(closure a⇩0). ¬ deadlock x⇩0"
proof -
  from steps_Steps_no_deadlock[OF no_deadlock] show ?thesis
  by (simp add: Alw_alw_iff Steps.Alw_alw_iff no_deadlock  Steps.Ex_ev Ex_ev)
     (rule reaches_all'[simplified]; erule P1_P; assumption)
qed

lemma Alw_alw_iff1:
  "(∀ x⇩0 ∈ a⇩0. Alw_alw P x⇩0) ⟷ Steps.Alw_alw (λ a. ∀ c ∈ a. P c) a⇩0"
  if P1_P: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y"
  and no_deadlock: "∀ x⇩0 ∈ a⇩0. ¬ deadlock x⇩0" and closure_simp: "⋃(closure a⇩0) = a⇩0"
  using Alw_alw_iff[OF P1_P] no_deadlock unfolding closure_simp by auto

lemma Alw_alw_iff2:
  "(∀ x⇩0 ∈ a⇩0. Alw_alw P x⇩0) ⟷ Steps.Alw_alw (λ a. ∀ c ∈ a. P c) a⇩0"
  if P1_P: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y"
  and no_deadlock: "∀ x⇩0 ∈ a⇩0. ¬ deadlock x⇩0"
proof -
  have "(∀ x⇩0 ∈ a⇩0. Alw_alw P x⇩0) ⟷ (∀ x⇩0 ∈ ⋃(closure a⇩0). Alw_alw P x⇩0)"
    apply -
    apply (rule compatible_closure_all_iff, rule bisim.steps_bisim.Alw_alw_iff_strong)
    unfolding bisim.steps_bisim.A_B.equiv'_def
    by (blast intro: P2_a⇩0 dest: P1_P)+
  also have "… ⟷ Steps.Alw_alw (λ a. ∀ c ∈ a. P c) a⇩0"
    by (rule Alw_alw_iff[OF P1_P no_deadlock_closureI[OF no_deadlock]])
  finally show ?thesis .
qed

lemma Steps_all_Alw_ev:
  "∀ x⇩0 ∈ a⇩0. Alw_ev P x⇩0" if "Steps.Alw_ev (λ a. ∀ c ∈ a. P c) a⇩0"
  using that unfolding Alw_ev_def Steps.Alw_ev_def
  apply safe
  apply (drule run_complete[OF _ _ P2_a⇩0], assumption)
  apply safe
  apply (elim allE impE, assumption)
  subgoal premises prems for x xs as
    using prems(4,3,1)
    by (induction "a⇩0 ## as" arbitrary: a⇩0 as x xs rule: ev.induct)
       (auto 4 3 elim: stream.rel_cases intro: ev_Stream)
  done

lemma closure_compatible_Steps_all_ex_iff:
  "Steps.Alw_ev (λ a. ∀ c ∈ a. P c) a⇩0 ⟷ Steps.Alw_ev (λ a. ∃ c ∈ a. P c) a⇩0"
  if closure_P: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P2 a ⟹ P x ⟷ P y"
proof -
  interpret Bisimulation_Invariant A2 A2 "(=)" P2 P2
    by standard auto
  show ?thesis
    using P2_a⇩0
    by - (rule Alw_ev_iff, unfold A_B.equiv'_def; meson P2_cover closure_P disjoint_iff_not_equal)
qed

lemma (in -) compatible_imp:
  assumes "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y"
      and "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ Q x ⟷ Q y"
    shows "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ (Q x ⟶ P x) ⟷ (Q y ⟶ P y)"
  using assms by metis

lemma Leadsto_iff:
  "(∀ x⇩0 ∈ ⋃(closure a⇩0). leadsto P Q x⇩0) ⟷ Steps.Alw_alw (λa. ∀c∈a. P c ⟶ Alw_ev Q c) a⇩0"
  if  P1_P: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y"
  and P1_Q: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ Q x ⟷ Q y"
  and no_deadlock: "∀ x⇩0 ∈ ⋃(closure a⇩0). ¬ deadlock x⇩0"
  unfolding leadsto_def
  by (subst Alw_alw_iff[OF _ no_deadlock],
      intro compatible_imp bisim.Alw_ev_compatible,
      (subst (asm) P1_Q; force), (assumption | intro HOL.refl P1_P)+
     )

lemma Leadsto_iff1:
  "(∀ x⇩0 ∈ a⇩0. leadsto P Q x⇩0) ⟷ Steps.Alw_alw (λa. ∀c∈a. P c ⟶ Alw_ev Q c) a⇩0"
  if  P1_P: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y"
  and P1_Q: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ Q x ⟷ Q y"
  and no_deadlock: "∀ x⇩0 ∈ a⇩0. ¬ deadlock x⇩0" and closure_simp: "⋃(closure a⇩0) = a⇩0"
  by (subst closure_simp[symmetric], rule Leadsto_iff)
     (auto simp: closure_simp no_deadlock dest: P1_Q P1_P)

lemma Leadsto_iff2:
  "(∀ x⇩0 ∈ a⇩0. leadsto P Q x⇩0) ⟷ Steps.Alw_alw (λa. ∀c∈a. P c ⟶ Alw_ev Q c) a⇩0"
  if  P1_P: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y"
  and P1_Q: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ Q x ⟷ Q y"
  and no_deadlock: "∀ x⇩0 ∈ a⇩0. ¬ deadlock x⇩0"
proof -
  have "(∀ x⇩0 ∈ a⇩0. leadsto P Q x⇩0) ⟷ (∀ x⇩0 ∈ ⋃(closure a⇩0). leadsto P Q x⇩0)"
    apply -
    apply (rule compatible_closure_all_iff, rule bisim.steps_bisim.Leadsto_iff)
    unfolding bisim.steps_bisim.A_B.equiv'_def by (blast intro: P2_a⇩0 dest: P1_P P1_Q)+
  also have "… ⟷ Steps.Alw_alw (λa. ∀c∈a. P c ⟶ Alw_ev Q c) a⇩0"
    by (rule Leadsto_iff[OF _ _ no_deadlock_closureI[OF no_deadlock]]; rule P1_P P1_Q)
  finally show ?thesis .
qed

lemma (in -) compatible_convert1:
  assumes "⋀ x y a. P x ⟹ x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P y"
  shows "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y"
    by (auto intro: assms)

lemma (in -) compatible_convert2:
  assumes "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y"
  shows "⋀ x y a. P x ⟹ x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P y"
  using assms by meson

lemma (in Double_Simulation_Defs)
  assumes compatible: "⋀ x y a. P x ⟹ x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P y"
    and that: "∀ x ∈ a. P x"
  shows "∀ x ∈ ⋃(closure a). P x"
  using that unfolding closure_def by (auto dest: compatible)

end (* Double Simulation Finite Complete Bisim *)

context Double_Simulation_Finite_Complete_Bisim_Cover
begin

lemma Alw_ev_Steps_ex:
  "(∀ x⇩0 ∈ ⋃(closure a⇩0). Alw_ev P x⇩0) ⟶ Steps.Alw_ev (λ a. ∃ c ∈ a. P c) a⇩0"
  if closure_P: "⋀ a x y. x ∈ ⋃(closure a) ⟹ y ∈ ⋃(closure a) ⟹ P2 a ⟹ P x ⟷ P y"
  unfolding Alw_ev Steps.Alw_ev
  apply safe
  apply (frule Steps_finite.run_finite_state_set_cycle_steps)
  apply clarify
  apply (frule Steps_run_cycle'')
   apply (auto dest!: P2_invariant.invariant_run simp: stream.pred_set; fail)
  unfolding that
   apply clarify
  subgoal premises prems for xs x ys zs x' xs' R
  proof -
    from ‹x' ∈ R› ‹R ∈ _› that have ‹x' ∈ ⋃(closure a⇩0)›
      by auto
    with prems(5,9) have
      "∀ c ∈ {x'} ∪ sset xs'. ∃ y ∈ {a⇩0} ∪ sset xs. c ∈ ⋃(closure y)"
      by fast
    with prems(3) have *:
      "∀ c ∈ {x'} ∪ sset xs'. ∃ y ∈ {a⇩0} ∪ sset xs. c ∈ ⋃(closure y) ∧ (∀ c ∈ y. ¬ P c)"
      unfolding alw_holds_sset by simp
    from ‹Run _› have **: "P2 y" if "y ∈ {a⇩0} ∪ sset xs" for y
      using that by (auto dest!: P2_invariant.invariant_run simp: stream.pred_set)
    have ***: "¬ P c" if "c ∈ ⋃(closure y)" "∀ d ∈ y. ¬ P d" "P2 y" for c y
    proof -
      from that P2_cover[OF ‹P2 y›] obtain d where "d ∈ y" "d ∈ ⋃(closure y)"
        by (fastforce dest!: P2_closure_subs)
      with that closure_P show ?thesis
        by blast
    qed
    from * have "∀ c ∈ {x'} ∪ sset xs'. ¬ P c"
      by (fastforce intro: ** dest!: ***[rotated])
    with prems(1) ‹run _› ‹x' ∈ ⋃(closure _)› show ?thesis
      unfolding alw_holds_sset by auto
  qed
  done

lemma Alw_ev_Steps_ex2:
  "(∀ x⇩0 ∈ a⇩0. Alw_ev P x⇩0) ⟶ Steps.Alw_ev (λ a. ∃ c ∈ a. P c) a⇩0"
  if  closure_P: "⋀ a x y. x ∈ ⋃(closure a) ⟹ y ∈ ⋃(closure a) ⟹ P2 a ⟹ P x ⟷ P y"
  and P1_P: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y"
proof -
  have "(∀ x⇩0 ∈ a⇩0. Alw_ev P x⇩0) ⟷ (∀ x⇩0 ∈ ⋃(closure a⇩0). Alw_ev P x⇩0)"
    by (intro compatible_closure_all_iff bisim.Alw_ev_compatible; auto dest: P1_P simp: P2_a⇩0)
  also have "… ⟶ Steps.Alw_ev (λ a. ∃ c ∈ a. P c) a⇩0"
    by (intro Alw_ev_Steps_ex that)
  finally show ?thesis .
qed

lemma Alw_ev_Steps_ex1:
  "(∀ x⇩0 ∈ a⇩0. Alw_ev P x⇩0) ⟶ Steps.Alw_ev (λ a. ∃ c ∈ a. P c) a⇩0" if "⋃(closure a⇩0) = a⇩0"
  and closure_P: "⋀ a x y. x ∈ ⋃(closure a) ⟹ y ∈ ⋃(closure a) ⟹ P2 a ⟹ P x ⟷ P y"
  by (subst that(1)[symmetric]) (intro Alw_ev_Steps_ex closure_P; assumption)

lemma closure_compatible_Alw_ev_Steps_iff:
  "(∀ x⇩0 ∈ a⇩0. Alw_ev P x⇩0) ⟷ Steps.Alw_ev (λ a. ∀ c ∈ a. P c) a⇩0"
  if closure_P: "⋀ a x y. x ∈ ⋃(closure a) ⟹ y ∈ ⋃(closure a) ⟹ P2 a ⟹ P x ⟷ P y"
    and P1_P: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y"
  apply standard
  subgoal
    apply (subst closure_compatible_Steps_all_ex_iff[OF closure_P])
       prefer 4
       apply (rule Alw_ev_Steps_ex2[OF that, rule_format])
    by (auto dest!: P2_closure_subs)
  by (rule Steps_all_Alw_ev) (auto dest: P2_closure_subs)

lemma Leadsto_iff':
  "(∀ x⇩0 ∈ a⇩0. leadsto P Q x⇩0)
   ⟷ Steps.Alw_alw (λ a. (∀ c ∈ a. P c) ⟶ Steps.Alw_ev (λ a. ∀ c ∈ a. Q c) a) a⇩0"
  if  P1_P: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P x ⟷ P y"
    and P1_Q: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ Q x ⟷ Q y"
    and closure_Q: "⋀ a x y. x ∈ ⋃(closure a) ⟹ y ∈ ⋃(closure a) ⟹ P2 a ⟹ Q x ⟷ Q y"
    and closure_P: "⋀ a x y. x ∈ a ⟹ y ∈ a ⟹ P2 a ⟹ P x ⟷ P y"
    and no_deadlock: "∀ x⇩0 ∈ a⇩0. ¬ deadlock x⇩0" and closure_simp: "⋃(closure a⇩0) = a⇩0"
  apply (subst Leadsto_iff1, (rule that; assumption)+)
  subgoal
    apply (rule P2_invariant.Alw_alw_iff_default)
    subgoal premises prems for a
    proof -
      have "P2 a"
        by (rule P2_invariant.invariant_reaches[OF prems[unfolded Graph_Start_Defs.reachable_def]])
      interpret a: Double_Simulation_Finite_Complete_Bisim_Cover C A1 P1 A2 P2 a
        apply standard
              apply (rule complete; assumption; fail)
             apply (rule P2_invariant; assumption)
        subgoal
          by (fact ‹P2 a›)
        subgoal
        proof -
          have "{b. Steps.reaches a b} ⊆ {b. Steps.reaches a⇩0 b}"
            by (blast intro: rtranclp_trans prems[unfolded Graph_Start_Defs.reachable_def])
          with finite_abstract_reachable show ?thesis
            by - (rule finite_subset)
        qed

          apply (rule A1_complete; assumption)
         apply (rule P1_invariant; assumption)
        apply (rule P2_P1_cover; assumption)
        done
      from ‹P2 a› show ?thesis
        by - (subst a.closure_compatible_Alw_ev_Steps_iff[symmetric], (rule that; assumption)+,
            auto dest: closure_P intro: that
            )
    qed
    ..
  done

context
  fixes P :: "'a ⇒ bool" ― ‹The property we want to check›
  assumes closure_P: "⋀ a x y. x ∈ ⋃(closure a) ⟹ y ∈ ⋃(closure a) ⟹ P2 a ⟹ P x ⟷ P y"
  and P1_P: "⋀ a x y. P x ⟹ x ∈ a ⟹ y ∈ a ⟹ P1 a ⟹ P y"
begin

lemma run_alw_ev_bisim:
  "run (x ## xs) ⟹ x ∈ ⋃(closure a⇩0) ⟹ alw (ev (holds P)) xs
      ⟹ ∃ y ys. y ∈ a⇩0 ∧ run (y ## ys) ∧ alw (ev (holds P)) ys"
  unfolding closure_def
  apply safe
  apply (rotate_tac 3)
  apply (drule bisim.runs_bisim, assumption+)
  apply (auto elim: P1_P dest: alw_ev_lockstep[of P _ _ _ P])
  done

lemma φ_closure_compatible:
  "P2 a ⟹ x ∈ ⋃(closure a) ⟹ P x ⟷ (∀ x ∈ ⋃(closure a). P x)"
  using closure_P by blast

theorem infinite_buechi_run_cycle_iff:
  "(∃ x⇩0 xs. x⇩0 ∈ ⋃(closure a⇩0) ∧ run (x⇩0 ## xs) ∧ alw (ev (holds P)) (x⇩0 ## xs))
  ⟷ (∃ as a bs. a ≠ {} ∧ post_defs.Steps (closure a⇩0 # as @ a # bs @ [a]) ∧ (∀ x ∈ ⋃ a. P x))"
  by (rule
      infinite_buechi_run_cycle_iff_closure[OF
        φ_closure_compatible run_alw_ev_bisim P2_closure_subs
        ]
      )
end (* Property *)

end (* Double Simulation Finite Complete Bisim Cover *)

text ‹Possible Solution›
context Graph_Invariant
begin

definition "E_inv x y ≡ E x y ∧ P x ∧ P y"

lemma bisim_E_inv:
  "Bisimulation_Invariant E E_inv (=) P P"
  by standard (auto intro: invariant simp: E_inv_def)

interpretation G_inv: Graph_Defs E_inv .

lemma steps_G_inv_steps:
  "steps (x # xs) ⟷ G_inv.steps (x # xs)" if "P x"
proof -
  interpret Bisimulation_Invariant E E_inv "(=)" P P
    by (rule bisim_E_inv)
  from ‹P x› show ?thesis
    by (auto 4 3 simp: equiv'_def list.rel_eq
        dest: bisim.A_B.simulation_steps bisim.B_A.simulation_steps
          list_all2_mono[of _ _ _ "(=)"]
       )
qed

end (* Graph Invariant *)

paragraph ‹‹R_of›/‹from_R››

definition "R_of lR = snd ` lR"

definition "from_R l R = {(l, u) | u. u ∈ R}"

lemma from_R_fst:
  "∀x∈from_R l R. fst x = l"
  unfolding from_R_def by auto

lemma R_of_from_R [simp]:
  "R_of (from_R l R) = R"
  unfolding R_of_def from_R_def image_def by auto

lemma from_R_loc:
  "l' = l" if "(l', u) ∈ from_R l Z"
  using that unfolding from_R_def by auto

lemma from_R_val:
  "u ∈ Z" if "(l', u) ∈ from_R l Z"
  using that unfolding from_R_def by auto

lemma from_R_R_of:
  "from_R l (R_of S) = S" if "∀ x ∈ S. fst x = l"
  using that unfolding from_R_def R_of_def by force

lemma R_ofI[intro]:
  "Z ∈ R_of S" if "(l, Z) ∈ S"
  using that unfolding R_of_def by force

lemma from_R_I[intro]:
  "(l', u') ∈ from_R l' Z'" if "u' ∈ Z'"
  using that unfolding from_R_def by auto

lemma R_of_non_emptyD:
  "a ≠ {}" if "R_of a ≠ {}"
  using that unfolding R_of_def by simp

lemma R_of_empty[simp]:
  "R_of {} = {}"
  using R_of_non_emptyD by metis

lemma fst_simp:
  "x = l" if "∀x∈a. fst x = l" "(x, y) ∈ a"
  using that by auto

lemma from_R_D:
  "u ∈ Z" if "(l', u) ∈ from_R l Z"
  using that unfolding from_R_def by auto

locale Double_Simulation_paired_Defs =
  fixes C :: "('a × 'b) ⇒ ('a × 'b) ⇒ bool" ― ‹Concrete step relation›
    and A1 :: "('a × 'b set) ⇒ ('a × 'b set) ⇒ bool"
    ― ‹Step relation for the first abstraction layer›
    and P1 :: "('a × 'b set) ⇒ bool" ― ‹Valid states of the first abstraction layer›
    and A2 :: "('a × 'b set) ⇒ ('a × 'b set) ⇒ bool"
    ― ‹Step relation for the second abstraction layer›
    and P2 :: "('a × 'b set) ⇒ bool" ― ‹Valid states of the second abstraction layer›
begin

definition
  "A1' = (λ lR lR'. ∃ l l'. (∀ x ∈ lR. fst x = l) ∧ (∀ x ∈ lR'. fst x = l')
    ∧ P1 (l, R_of lR) ∧ A1 (l, R_of lR) (l', R_of lR')
    )"

definition
  "A2' = (λ lR lR'. ∃ l l'. (∀ x ∈ lR. fst x = l) ∧ (∀ x ∈ lR'. fst x = l')
    ∧ P2 (l, R_of lR) ∧ A2 (l, R_of lR) (l', R_of lR')
    )"

definition
  "P1' = (λ lR. ∃ l. (∀ x ∈ lR. fst x = l) ∧ P1 (l, R_of lR))"

definition
  "P2' = (λ lR. ∃ l. (∀ x ∈ lR. fst x = l) ∧ P2 (l, R_of lR))"

definition "closure' l a = {x. P1 (l, x) ∧ a ∩ x ≠ {}}"

sublocale sim: Double_Simulation_Defs C A1' P1' A2' P2' .

end

locale Double_Simulation_paired = Double_Simulation_paired_Defs +
  assumes prestable: "P1 (l, S) ⟹ A1 (l, S) (l', T) ⟹ ∀ s ∈ S. ∃ s' ∈ T. C (l, s) (l', s')"
      and closure_poststable:
        "s' ∈ closure' l' y ⟹ P2 (l, x) ⟹ A2 (l, x) (l', y)
        ⟹ ∃s∈closure' l x. A1 (l, s) (l', s')"
      and P1_distinct: "P1 (l, x) ⟹ P1 (l, y) ⟹ x ≠ y ⟹ x ∩ y = {}"
      and P1_finite: "finite {(l, x). P1 (l, x)}"
      and P2_cover: "P2 (l, a) ⟹ ∃ x. P1 (l, x) ∧ x ∩ a ≠ {}"
begin

sublocale sim: Double_Simulation C A1' P1' A2' P2'
proof (standard, goal_cases)
  case (1 S T)
  then show ?case
    unfolding A1'_def by (metis from_R_I from_R_R_of from_R_val prestable prod.collapse)
next
  case (2 s' y x)
  then show ?case
    unfolding A2'_def A1'_def sim.closure_def
    unfolding P1'_def
    apply clarify
    subgoal premises prems for l l1 l2
    proof -
      from prems have "l2 = l1"
        by force
      from prems have "R_of s' ∈ closure' l1 (R_of y)"
        unfolding closure'_def by auto
      with ‹A2 _ _› ‹P2 _› closure_poststable[of "R_of s'" l1 "R_of y" l "R_of x"] obtain s where
        "s ∈ closure' l (R_of x)" "A1 (l, s) (l1, R_of s')"
        by auto
      with prems from_R_fst R_of_from_R show ?thesis
        apply -
        unfolding ‹l2 = l1›
        apply (rule bexI[where x = "from_R l s"])
         apply (inst_existentials l l1)
            apply (simp add: from_R_fst; fail)+
        subgoal
          unfolding closure'_def by auto
         apply (simp; fail)
        unfolding closure'_def
        apply (intro CollectI conjI exI)
          apply fastforce
         apply fastforce
        apply (fastforce simp: R_of_def from_R_def)
        done
    qed
    done
next
  case (3 x y)
  then show ?case
    unfolding P1'_def using P1_distinct
    by (smt disjoint_iff_not_equal eq_fst_iff from_R_R_of from_R_val)
next
  case 4
  have "{x. ∃l. (∀x∈x. fst x = l) ∧ P1 (l, R_of x)} ⊆ (λ (l, x). from_R l x) ` {(l, x). P1 (l, x)}"
    using from_R_R_of image_iff by fastforce
  with P1_finite show ?case
    unfolding P1'_def by (auto elim: finite_subset)
next
  case (5 a)
  then show ?case
    unfolding P1'_def P2'_def
    apply clarify
    apply (frule P2_cover)
    apply clarify
    subgoal for l x
      apply (inst_existentials "from_R l x" l, (simp add: from_R_fst)+)
      using R_of_def by (fastforce simp: from_R_fst)
    done
qed

context
  assumes P2_invariant: "P2 a ⟹ A2 a a' ⟹ P2 a'"
begin

(* This lemma could be more general by adding non-emptiness as an invariant
  (see use of double_sim.P2_cover below )
*)
lemma A2_A2'_bisim: "Bisimulation_Invariant A2 A2' (λ (l, Z) b. b = from_R l Z) P2 P2'"
  apply standard
  subgoal A2_A2' for a b a'
    unfolding P2'_def
    apply clarify
    apply (inst_existentials "from_R (fst b) (snd b)")
    subgoal for x y l
      unfolding A2'_def
      apply simp
      apply (inst_existentials l)
      by (auto dest!: P2_cover simp: from_R_def)
    by clarsimp
  subgoal A2'_A2 for a a' b'
    using from_R_fst by (fastforce dest: sim.P2_cover simp: from_R_R_of A2'_def)
  subgoal P2_invariant for a b
    by (fact P2_invariant)
  subgoal P2'_invariant for a b
    unfolding P2'_def A2'_def using P2_invariant by blast
  done

end (* Context for invariance of P2 *)

end (* Double Simulation paired *)

locale Double_Simulation_Complete_paired = Double_Simulation_paired +
  fixes l⇩0 a⇩0
  assumes complete: "C (l, x) (l', y) ⟹ x ∈ S ⟹ P2 (l, S) ⟹ ∃ T. A2 (l, S) (l', T) ∧ y ∈ T"
  assumes P2_invariant: "P2 a ⟹ A2 a a' ⟹ P2 a'"
      and P2_a⇩0': "P2 (l⇩0, a⇩0)"
begin

interpretation Bisimulation_Invariant A2 A2' "λ (l, Z) b. b = from_R l Z" P2 P2'
  by (rule A2_A2'_bisim[OF P2_invariant])

sublocale Double_Simulation_Complete C A1' P1' A2' P2' "from_R l⇩0 a⇩0"
proof (standard, goal_cases)
  case prems: (1 x y S) ― ‹complete›
  then show ?case
    unfolding A2'_def P2'_def using from_R_fst
    by (clarify; cases x; cases y; simp; fastforce dest!: complete[of _ _ _ _ "R_of S"])
next
  case prems: (2 a a') ― ‹P2 invariant›
  then show ?case
    by (meson A2'_def P2'_def P2_invariant)
next
  case prems: 3 ― ‹P2 start›
  then show ?case
    using P2'_def P2_a⇩0' from_R_fst by fastforce
qed

sublocale P2_invariant': Graph_Invariant_Start A2 "(l⇩0, a⇩0)" P2
  by (standard; rule P2_a⇩0')

end (* Double Simulation Complete paired *)

locale Double_Simulation_Finite_Complete_paired = Double_Simulation_Complete_paired +
  assumes finite_abstract_reachable: "finite {(l, a). A2⇧*⇧* (l⇩0, a⇩0) (l, a) ∧ P2 (l, a)}"
begin

interpretation Bisimulation_Invariant A2 A2' "λ (l, Z) b. b = from_R l Z" P2 P2'
  by (rule A2_A2'_bisim[OF P2_invariant])

sublocale Double_Simulation_Finite_Complete C A1' P1' A2' P2' "from_R l⇩0 a⇩0"
proof (standard, goal_cases)
  case prems: 1 ― ‹The set of abstract reachable states is finite.›
  have *: "∃ l. x = from_R l (R_of x) ∧ A2⇧*⇧* (l⇩0, a⇩0) (l, R_of x)"
    if "sim.Steps.reaches (from_R l⇩0 a⇩0) x" for x
    using bisim.B_A_reaches[OF that, of "(l⇩0, a⇩0)"] P2_a⇩0' P2'_def equiv'_def from_R_fst by fastforce 
  have "{a. sim.Steps.reaches (from_R l⇩0 a⇩0) a}
    ⊆ (λ (l, R). from_R l R) ` {(l, a). A2⇧*⇧* (l⇩0, a⇩0) (l, a) ∧ P2 (l, a)}"
    using P2_a⇩0' by (fastforce dest: * intro: P2_invariant'.invariant_reaches)
  then show ?case
    using finite_abstract_reachable by (auto elim!: finite_subset)
qed

end (* Double Simulation Finite Complete paired *)

locale Double_Simulation_Complete_Bisim_paired = Double_Simulation_Complete_paired +
  assumes A1_complete: "C (l, x) (l', y) ⟹ P1 (l,S) ⟹ x ∈ S ⟹ ∃ T. A1 (l, S) (l', T) ∧ y ∈ T"
      and P1_invariant: "P1 (l, S) ⟹ A1 (l, S) (l', T) ⟹ P1 (l', T)"
begin

sublocale Double_Simulation_Complete_Bisim C A1' P1' A2' P2' "from_R l⇩0 a⇩0"
proof (standard, goal_cases)
case (1 x y S)
  then show ?case
    unfolding A1'_def P1'_def
    apply (cases x; cases y; simp)
    apply (drule A1_complete[where S = "R_of S"])
      apply fastforce
     apply fastforce
    apply clarify
    subgoal for a b l' ba l T
      by (inst_existentials "from_R l' T" l l') (auto simp: from_R_fst)
    done
next
  case (2 S T)
  then show ?case
    unfolding A1'_def P1'_def by (auto intro: P1_invariant)
qed

end (* Double Simulation Complete Bisim paired *)

locale Double_Simulation_Finite_Complete_Bisim_paired = Double_Simulation_Finite_Complete_paired +
  Double_Simulation_Complete_Bisim_paired
begin

sublocale Double_Simulation_Finite_Complete_Bisim C A1' P1' A2' P2' "from_R l⇩0 a⇩0" ..

end (* Double Simulation Finite Complete Bisim paired *)

locale Double_Simulation_Complete_Bisim_Cover_paired =
  Double_Simulation_Complete_Bisim_paired +
  assumes P2_P1_cover: "P2 (l, a) ⟹ x ∈ a ⟹ ∃ a'. a ∩ a' ≠ {} ∧ P1 (l, a') ∧ x ∈ a'"
begin

sublocale Double_Simulation_Complete_Bisim_Cover C A1' P1' A2' P2' "from_R l⇩0 a⇩0"
  apply standard
  unfolding P2'_def P1'_def
  apply clarify
  apply (drule P2_P1_cover, force)
  apply clarify
  subgoal for a aa b l a'
    by (inst_existentials "from_R l a'") (fastforce simp: from_R_fst)+
  done

end (* Double Simulation Complete Bisim Cover paired *)

locale Double_Simulation_Finite_Complete_Bisim_Cover_paired =
  Double_Simulation_Complete_Bisim_Cover_paired +
  Double_Simulation_Finite_Complete_Bisim_paired
begin

sublocale Double_Simulation_Finite_Complete_Bisim_Cover C A1' P1' A2' P2' "from_R l⇩0 a⇩0" ..

end (* Double Simulation Finite Complete Bisim Cover paired *)

locale Double_Simulation_Complete_Abstraction_Prop_paired =
  Double_Simulation_Complete_paired +
  fixes P :: "'a ⇒ bool" ― ‹The property we want to check›
  assumes P2_non_empty: "P2 (l, a) ⟹ a ≠ {}"
begin

definition "φ = P o fst"

lemma P2_φ:
  "a ∩ Collect φ = a" if "P2' a" "a ∩ Collect φ ≠ {}"
  using that unfolding φ_def P2'_def by (auto simp del: fst_conv)

sublocale Double_Simulation_Complete_Abstraction_Prop C A1' P1' A2' P2' "from_R l⇩0 a⇩0" φ
proof (standard, goal_cases)
  case (1 a b)
  then obtain l where "∀x∈b. fst x = l"
    unfolding A1'_def by fast
  then show ?case
    unfolding φ_def by (auto simp del: fst_conv)
next
  case (2 a)
  then show ?case
    by - (frule P2_φ, auto)
next
  case prems: (3 a)
  then have "P2' a"
    by (simp add: P2_invariant.invariant_reaches)
  from P2_φ[OF this] prems show ?case
    by simp
next
  case (4 a)
  then show ?case
    unfolding P2'_def by (auto dest!: P2_non_empty)
qed

end (* Double Simulation Complete Abstraction Prop paired *)

locale Double_Simulation_Finite_Complete_Abstraction_Prop_paired =
  Double_Simulation_Complete_Abstraction_Prop_paired +
  Double_Simulation_Finite_Complete_paired
begin

sublocale Double_Simulation_Finite_Complete_Abstraction_Prop C A1' P1' A2' P2' "from_R l⇩0 a⇩0" φ ..

end (* Double Simulation Finite Complete Abstraction Prop paired *)

locale Double_Simulation_Complete_Abstraction_Prop_Bisim_paired =
  Double_Simulation_Complete_Abstraction_Prop_paired +
  Double_Simulation_Complete_Bisim_paired
begin

interpretation bisim: Bisimulation_Invariant A2 A2' "λ (l, Z) b. b = from_R l Z" P2 P2'
  by (rule A2_A2'_bisim[OF P2_invariant])

sublocale Double_Simulation_Complete_Abstraction_Prop_Bisim
  C A1' P1' A2' P2' "from_R l⇩0 a⇩0" φ ..

lemma P2'_non_empty:
  "P2' a ⟹ a ≠ {}"
  using P2_non_empty unfolding P2'_def by force

lemma from_R_int_φ[simp]:
  "from_R l R ∩ Collect φ = from_R l R" if "P l"
  using from_R_fst that unfolding φ_def by fastforce

interpretation G⇩φ: Graph_Start_Defs
  "λ (l, Z) (l', Z'). A2 (l, Z) (l', Z') ∧ P l'" "(l⇩0, a⇩0)" .

interpretation Bisimulation_Invariant "λ (l, Z) (l', Z'). A2 (l, Z) (l', Z') ∧ P l'"
  A2_φ "λ (l, Z) b. b = from_R l Z" P2 P2'
  apply standard
  unfolding A2_φ_def
     apply clarify
  subgoal for l a l' a'
    apply (drule bisim.A_B_step)
    prefer 3
       apply assumption
      apply safe
    apply (frule P_invariant, assumption+)
    using from_R_fst by (fastforce simp: φ_def P2'_def dest!: P2'_non_empty)+
  subgoal for a a' b'
    apply clarify
    apply (drule bisim.B_A_step)
       prefer 2
       apply assumption
      apply safe
    apply (frule P2_invariant, assumption+)
    apply (subst (asm) (3) φ_def)
    apply simp
    apply (elim allE impE, assumption)
    using from_R_fst apply force
    apply (subst (asm) (2) from_R_int_φ)
    using from_R_fst by fastforce+
  subgoal
    by blast
  subgoal
    using φ_P2_compatible by blast
  done

lemma from_R_subs_φ:
  "from_R l a ⊆ Collect φ" if "P l"
  using that unfolding φ_def from_R_def by auto

lemma P2'_from_R:
  "∃ l' Z'. x = from_R l' Z'" if "P2' x"
  using that unfolding P2'_def by (fastforce dest: from_R_R_of)

lemma P2_from_R_list':
  "∃ as'. map (λ(x, y). from_R x y) as' = as" if "list_all P2' as"
  by (rule list_all_map[OF _ that]) (auto dest!: P2'_from_R)

end (* Double Simulation Complete Abstraction Prop Bisim paired *)

locale Double_Simulation_Finite_Complete_Abstraction_Prop_Bisim_paired =
  Double_Simulation_Complete_Abstraction_Prop_Bisim_paired +
  Double_Simulation_Finite_Complete_Bisim_paired
begin

interpretation bisim: Bisimulation_Invariant A2 A2' "λ (l, Z) b. b = from_R l Z" P2 P2'
  by (rule A2_A2'_bisim[OF P2_invariant])

sublocale Double_Simulation_Finite_Complete_Abstraction_Prop_Bisim
  C A1' P1' A2' P2' "from_R l⇩0 a⇩0" φ ..

interpretation G⇩φ: Graph_Start_Defs
  "λ (l, Z) (l', Z'). A2 (l, Z) (l', Z') ∧ P l'" "(l⇩0, a⇩0)" .

interpretation Bisimulation_Invariant "λ (l, Z) (l', Z'). A2 (l, Z) (l', Z') ∧ P l'"
  A2_φ "λ (l, Z) b. b = from_R l Z" P2 P2'
  apply standard
  unfolding A2_φ_def
     apply clarify
  subgoal for l a l' a'
    apply (drule bisim.A_B_step)
    prefer 3
       apply assumption
      apply safe
    apply (frule P_invariant, assumption+)
    using from_R_fst by (fastforce simp: φ_def P2'_def dest!: P2'_non_empty)+
  subgoal for a a' b'
    apply clarify
    apply (drule bisim.B_A_step)
       prefer 2
       apply assumption
      apply safe
    apply (frule P2_invariant, assumption+)
    apply (subst (asm) (3) φ_def)
    apply simp
    apply (elim allE impE, assumption)
    using from_R_fst apply force
    apply (subst (asm) (2) from_R_int_φ)
    using from_R_fst by fastforce+
  subgoal
    by blast
  subgoal
    using φ_P2_compatible by blast
  done

theorem Alw_ev_mc:
  "(∀x⇩0∈a⇩0. sim.Alw_ev (Not ∘ φ) (l⇩0, x⇩0)) ⟷
    ¬ P l⇩0 ∨ (∄as a bs. G⇩φ.steps ((l⇩0, a⇩0) # as @ a # bs @ [a]))"
  apply (subst steps_map_equiv[of "λ (l, Z). from_R l Z" _ "from_R l⇩0 a⇩0"])
       apply force
      apply (clarsimp simp: from_R_def)
  subgoal
    by (fastforce dest!: P2'_non_empty)
     apply (simp; fail)
    apply (rule P2_a⇩0'; fail)
   apply (rule phi.P2_a⇩0; fail)
proof (cases "P l⇩0", goal_cases)
  case 1
  have *: "(∀x⇩0∈a⇩0. sim.Alw_ev (Not ∘ φ) (l⇩0, x⇩0)) ⟷ (∀x⇩0∈from_R l⇩0 a⇩0. sim.Alw_ev (Not ∘ φ) x⇩0)"
    unfolding from_R_def by auto
  from ‹P _› show ?case
    unfolding *
    apply (subst Alw_ev_mc[OF from_R_subs_φ], assumption)
    apply (auto simp del: map_map)
    apply (frule phi.P2_invariant.invariant_steps)
    apply (auto dest!: P2'_from_R P2_from_R_list')
    done
next
  case 2
  then have "∀x⇩0∈a⇩0. sim.Alw_ev (Not ∘ φ) (l⇩0, x⇩0)"
    unfolding sim.Alw_ev_def by (force simp: φ_def)
  with ‹¬ P l⇩0› show ?case
    by auto
qed

theorem Alw_ev_mc1:
  "(∀x⇩0∈a⇩0. sim.Alw_ev (Not ∘ φ) (l⇩0, x⇩0)) ⟷ ¬ (P l⇩0 ∧ (∃a. G⇩φ.reachable a ∧ G⇩φ.reaches1 a a))"
  unfolding Alw_ev_mc using G⇩φ.reachable_cycle_iff by auto

end (* Double Simulation Finite Complete Abstraction Prop Bisim paired *)

context Double_Simulation_Complete_Bisim_Cover_paired
begin

interpretation bisim: Bisimulation_Invariant A2 A2' "λ (l, Z) b. b = from_R l Z" P2 P2'
  by (rule A2_A2'_bisim[OF P2_invariant])

interpretation Start: Double_Simulation_Complete_Abstraction_Prop_Bisim_paired
  C A1 P1 A2 P2 l⇩0 a⇩0 "λ _. True"
  using P2_cover by - (standard, blast)

lemma sim_reaches_equiv:
  "P2_invariant'.reaches (l, Z) (l', Z') ⟷ sim.Steps.reaches (from_R l Z) (from_R l' Z')"
  if "P2 (l, Z)"
  apply (subst bisim.reaches_equiv[of "λ (l, Z). from_R l Z"])
      apply force
     apply clarsimp
  subgoal
    by (metis Int_emptyI R_of_from_R from_R_fst sim.P2_cover)
    apply (rule that)
  subgoal
    apply clarsimp
    using P2'_def from_R_fst that by force
  by auto

lemma reaches_all:
  assumes
    "⋀ u u' R l. u ∈ R ⟹ u' ∈ R ⟹ P1 (l, R) ⟹ P l u ⟷ P l u'"
  shows
    "(∀ u. (∃ x⇩0∈⋃(sim.closure (from_R l⇩0 a⇩0)). sim.reaches x⇩0 (l, u)) ⟶ P l u) ⟷
     (∀ Z u. P2_invariant'.reaches (l⇩0, a⇩0) (l, Z) ∧ u ∈ Z ⟶ P l u)"
proof -
  let ?P = "λ (l, u). P l u"
  have *: "⋀a x y. x ∈ a ⟹ y ∈ a ⟹ P1' a ⟹ ?P x = ?P y"
    unfolding P1'_def by clarsimp (subst assms[rotated 2], force+, metis fst_conv)+
  let ?P = "λ (l', u). l' = l ⟶ P l u"
  have *: "x ∈ a ⟹ y ∈ a ⟹ P1' a ⟹ ?P x = ?P y" for a x y
    by (frule *[of x a y], assumption+; auto simp: P1'_def; metis fst_conv)
  have
    "(∀b. (∃y∈sim.closure (from_R l⇩0 a⇩0). ∃x⇩0∈y. sim.reaches x⇩0 (l, b)) ⟶ P l b) ⟷
     (∀b ba. sim.Steps.reaches (from_R l⇩0 a⇩0) b ∧ (l, ba) ∈ b ⟶ P l ba)"
    unfolding sim.reaches_steps_iff sim.Steps.reaches_steps_iff
    apply safe
    subgoal for b b' xs
      apply (rule reaches_all_1[of ?P xs "(l, b')", simplified])
          apply (erule *; assumption; fail)
         apply (simp; fail)+
      done

    subgoal premises prems for b y a b' xs
      apply (rule
          reaches_all_2[of ?P xs y, unfolded ‹last xs = (l, b)›, simplified]
          )
          apply (erule *; assumption; fail)
      using prems by auto
    done
  then show ?thesis
    unfolding sim_reaches_equiv[OF P2_a⇩0']
    apply simp
    subgoal premises prems
      apply safe
      subgoal for Z u
        unfolding from_R_def by auto
      subgoal for a u
        apply (frule P2_invariant.invariant_reaches)
        apply (auto dest!: Start.P2'_from_R simp: from_R_def)
        done
      done
    done
qed

context
  fixes P Q :: "'a ⇒ bool" ― ‹The state properties we want to check›
begin

definition "φ' = P o fst"

definition "ψ = Q o fst"

lemma ψ_closure_compatible:
  "ψ (l, x) ⟹ x ∈ a ⟹ y ∈ a ⟹ P1 (l, a) ⟹ ψ (l, y)"
  unfolding φ'_def ψ_def by auto

lemma ψ_closure_compatible':
  "(Not o ψ) (l, x) ⟹ x ∈ a ⟹ y ∈ a ⟹ P1 (l, a) ⟹ (Not o ψ) (l, y)"
  by (auto dest: ψ_closure_compatible)

lemma P1_P1':
  "R ≠ {} ⟹ P1 (l, R) ⟹ P1' (from_R l R)"
  using P1'_def from_R_fst by fastforce

lemma ψ_Alw_ev_compatible:
  assumes "u ∈ R" "u' ∈ R" "P1 (l, R)"
  shows "sim.Alw_ev (Not ∘ ψ) (l, u) = sim.Alw_ev (Not ∘ ψ) (l, u')"
  apply (rule bisim.Alw_ev_compatible[of _ _ "from_R l R"])
  subgoal for x a y
    using ψ_closure_compatible unfolding P1'_def by (metis ψ_def comp_def)
  using assms by (auto intro: P1_P1')

interpretation Graph_Start_Defs A2 "(l⇩0, a⇩0)" .

interpretation G⇩ψ: Graph_Start_Defs
  "λ (l, Z) (l', Z'). A2 (l, Z) (l', Z') ∧ Q l'" "(l⇩0, a⇩0)" .

end (* State *)

end (* Double Simulation Complete Bisim Cover paired *)

context Double_Simulation_Finite_Complete_Bisim_Cover_paired
begin

interpretation bisim: Bisimulation_Invariant A2 A2' "λ (l, Z) b. b = from_R l Z" P2 P2'
  by (rule A2_A2'_bisim[OF P2_invariant])

context
  fixes P Q :: "'a ⇒ bool" ― ‹The state properties we want to check›
begin

interpretation Graph_Start_Defs A2 "(l⇩0, a⇩0)" .

interpretation G⇩ψ: Graph_Start_Defs
  "λ (l, Z) (l', Z'). A2 (l, Z) (l', Z') ∧ Q l'" "(l⇩0, a⇩0)" .

lemma Alw_ev_mc1:
  "(∀x⇩0∈from_R l Z. sim.Alw_ev (Not ∘ ψ Q) x⇩0) ⟷
      ¬ (Q l ∧ (∃a. G⇩ψ.reaches (l, Z) a ∧ G⇩ψ.reaches1 a a))"
  if "P2_invariant'.reachable (l, Z)" for l Z
proof -
  from that have "P2 (l, Z)"
    using P2_invariant'.invariant_reaches unfolding P2_invariant'.reachable_def by auto
  interpret Start': Double_Simulation_Finite_Complete_Abstraction_Prop_Bisim_paired
    C A1 P1 A2 P2 l Z Q
    apply standard
    subgoal
      by (fact complete)
    subgoal
      by (fact P2_invariant)
    subgoal
      by (fact ‹P2 (l, Z)›)
    subgoal
      using P2_cover by blast
    subgoal
      by (fact A1_complete)
    subgoal
      by (fact P1_invariant)
    subgoal
    proof -
      have "{(l', a). A2⇧*⇧* (l,Z) (l',a) ∧ P2 (l',a)} ⊆ {(l, a). A2⇧*⇧* (l⇩0,a⇩0) (l,a) ∧ P2 (l,a)}"
        using that unfolding P2_invariant'.reachable_def by auto
      with finite_abstract_reachable show ?thesis
        by - (erule finite_subset)
    qed
    done
  show ?thesis
    using Start'.Alw_ev_mc1[unfolded Start'.φ_def]
    unfolding ψ_def Graph_Start_Defs.reachable_def from_R_def by auto
qed

theorem leadsto_mc1:
  "(∀x⇩0∈a⇩0. sim.leadsto (φ' P) (Not ∘ ψ Q) (l⇩0, x⇩0)) ⟷
   (∄x. P2_invariant'.reaches (l⇩0, a⇩0) x ∧ P (fst x) ∧ Q (fst x)
      ∧ (∃a. G⇩ψ.reaches x a ∧ G⇩ψ.reaches1 a a)
   )"
  if  no_deadlock: "∀x⇩0∈a⇩0. ¬ sim.deadlock (l⇩0, x⇩0)"
proof -
  from steps_Steps_no_deadlock[OF no_deadlock_closureI] no_deadlock have
    "¬ sim.Steps.deadlock (from_R l⇩0 a⇩0)"
    unfolding from_R_def by auto
  then have no_deadlock': "¬ P2_invariant'.deadlock (l⇩0, a⇩0)"
    by (subst bisim.deadlock_iff) (auto simp: P2_a⇩0' from_R_fst P2'_def)
  have "(∀x⇩0∈a⇩0. sim.leadsto (φ' P) (Not ∘ ψ Q) (l⇩0, x⇩0)) ⟷
    (∀x⇩0∈from_R l⇩0 a⇩0. sim.leadsto (φ' P) (Not ∘ ψ Q) x⇩0)
    "
    unfolding from_R_def by auto
  also have "… ⟷ sim.Steps.Alw_alw (λa. ∀c∈a. φ' P c ⟶ sim.Alw_ev (Not ∘ ψ Q) c) (from_R l⇩0 a⇩0)"
    apply (rule Leadsto_iff2[OF _ _ _])
    subgoal for a x y
      unfolding P1'_def φ'_def by (auto dest: fst_simp)
    subgoal for a x y
      unfolding P1'_def ψ_def by (auto dest: fst_simp)
    subgoal
      using no_deadlock unfolding from_R_def by auto
    done
  also have
    "…⟷ P2_invariant'.Alw_alw (λ(l,Z).∀c∈from_R l Z. φ' P c ⟶ sim.Alw_ev (Not ∘ ψ Q) c) (l⇩0,a⇩0)"
    by (auto simp: bisim.A_B.equiv'_def P2_a⇩0 P2_a⇩0' intro!: bisim.Alw_alw_iff_strong[symmetric])
  also have
    "… ⟷ P2_invariant'.Alw_alw
      (λ(l, Z). P l ⟶ ¬ (Q l ∧ (∃a. G⇩ψ.reaches (l, Z) a ∧ G⇩ψ.reaches1 a a))) (l⇩0, a⇩0)"
    by (rule P2_invariant'.Alw_alw_iff_default)
       (auto simp: φ'_def from_R_def dest: Alw_ev_mc1[symmetric])
  also have
    "… ⟷ (∄x. P2_invariant'.reaches (l⇩0,a⇩0) x ∧ P (fst x) ∧ Q (fst x)
      ∧ (∃a. G⇩ψ.reaches x a ∧ G⇩ψ.reaches1 a a))"
    unfolding P2_invariant'.Alw_alw_iff by (auto simp: P2_invariant'.Ex_ev no_deadlock')
  finally show ?thesis .
qed

end (* State *)

end (* Double Simulation Finite Complete Bisim Cover paired *)

paragraph ‹The second bisimulation property in prestable and complete simulation graphs.›

context Simulation_Graph_Complete_Prestable
begin

lemma C_A_bisim:
  "Bisimulation_Invariant C A (λ x a. x ∈ a) (λ_. True) P"
  by (standard; blast intro: complete dest: prestable)

interpretation Bisimulation_Invariant C A "λ x a. x ∈ a" "λ _. True" P
  by (rule C_A_bisim)

lemma C_A_Leadsto_iff:
  fixes φ ψ :: "'a ⇒ bool"
  assumes φ_compatible: "⋀ x y a. φ x ⟹ x ∈ a ⟹ y ∈ a ⟹ P a ⟹ φ y"
      and ψ_compatible: "⋀ x y a. ψ x ⟹ x ∈ a ⟹ y ∈ a ⟹ P a ⟹ ψ y"
      and "x ∈ a" "P a"
    shows "leadsto φ ψ x = Steps.leadsto (λ a. ∀ x ∈ a. φ x) (λ a. ∀ x ∈ a. ψ x) a"
  by (rule Leadsto_iff)
     (auto intro: φ_compatible ψ_compatible simp: ‹x ∈ a› ‹P a› simulation.equiv'_def)

end (* Simulation Graph Complete Prestable *)

paragraph ‹Comments›

text ‹
▪ Pre-stability can easily be extended to infinite runs (see construction with @{term sscan} above)
▪ Post-stability can not
▪ Pre-stability + Completeness means that for every two concrete states in the same abstract class,
  there are equivalent runs
▪ For Büchi properties, the predicate has to be compatible with whole closures instead of single
  ‹P1›-states. This is because for a finite graph where every node has at least indegree one,
  we cannot necessarily conclude that there is a cycle through ∗‹every› node.
›


locale Graph_Abstraction =
  Graph_Defs A for A :: "'a set ⇒ 'a set ⇒ bool" +
fixes α :: "'a set ⇒ 'a set"
assumes idempotent: "α(α(x)) = α(x)"
assumes enlarging: "x ⊆ α(x)"
assumes α_mono: "x ⊆ y ⟹ α(x) ⊆ α(y)"
assumes mono: "a ⊆ a' ⟹ A a b ⟹ ∃b'. b ⊆ b' ∧ A a' b'"
assumes finite_abstraction: "finite (α ` UNIV)"
begin

definition E where "E a b ≡ ∃b'. A a b' ∧ b = α(b')"

interpretation sim1: Simulation_Invariant A E "λa b. α(a) ⊆ b" "λ_. True" "λ_. True"
  apply standard
  unfolding E_def
    apply auto
  apply (frule mono[rotated])
   apply (erule order.trans[rotated], rule enlarging)
  apply (auto intro!: α_mono)
  done

interpretation sim2: Simulation_Invariant A E "λa b. a ⊆ b" "λ_. True" "λx. α(x) = x"
  apply standard
  subgoal
    unfolding E_def
    apply auto
    apply (drule (1) mono)
    apply safe
    apply (intro conjI exI)
      apply assumption
     apply (rule HOL.refl)
    apply (erule order.trans, rule enlarging)
    done
   apply assumption
  unfolding E_def
  apply (elim exE conjE)
  apply (simp add: idempotent)
  done

text ‹This variant needs the least assumptions.›
interpretation sim3: Simulation_Invariant A E "λa b. a ⊆ b" "λ_. True" "λ_. True"
  apply standard
  unfolding E_def
    apply auto
  apply (drule (1) mono)
  apply safe
  apply (intro conjI exI)
    apply assumption
   apply (rule HOL.refl)
  apply (erule order.trans, rule enlarging)
  done

interpretation sim4: Simulation_Invariant A E "λa b. a ⊆ b" "λ_. True" "λa. ∃a'. α a' = a"
  apply standard
  unfolding E_def
    apply auto
  apply (drule (1) mono)
  apply safe
  apply (intro conjI exI)
    apply assumption
   apply (rule HOL.refl)
  apply (erule order.trans, rule enlarging)
  done

end (* Abstraction Operators *)

lemmas [simp del] = holds.simps

end (* Theory *)