Theory Timed_Automata.Graphs

(* Author: Simon Wimmer *)
chapter ‹Graphs›

theory Graphs
  imports
    More_List Stream_More
    "HOL-Library.Rewrite"
begin

section ‹Basic Definitions and Theorems›

locale Graph_Defs =
  fixes E :: "'a  'a  bool"
begin

inductive steps where
  Single: "steps [x]" |
  Cons: "steps (x # y # xs)" if "E x y" "steps (y # xs)"

lemmas [intro] = steps.intros

lemma steps_append:
  "steps (xs @ tl ys)" if "steps xs" "steps ys" "last xs = hd ys"
  using that by induction (auto 4 4 elim: steps.cases)

lemma steps_append':
  "steps xs" if "steps as" "steps bs" "last as = hd bs" "as @ tl bs = xs"
  using steps_append that by blast

coinductive run where
  "run (x ## y ## xs)" if "E x y" "run (y ## xs)"

lemmas [intro] = run.intros

lemma steps_appendD1:
  "steps xs" if "steps (xs @ ys)" "xs  []"
  using that proof (induction xs)
  case Nil
  then show ?case by auto
next
  case (Cons a xs)
  then show ?case
    by - (cases xs; auto elim: steps.cases)
qed

lemma steps_appendD2:
  "steps ys" if "steps (xs @ ys)" "ys  []"
  using that by (induction xs) (auto elim: steps.cases)

lemma steps_appendD3:
  "steps (xs @ [x])  E x y" if "steps (xs @ [x, y])"
  using that proof (induction xs)
  case Nil
  then show ?case by (auto elim!: steps.cases)
next
  case prems: (Cons a xs)
  then show ?case by (cases xs) (auto elim: steps.cases)
qed

lemma steps_ConsD:
  "steps xs" if "steps (x # xs)" "xs  []"
  using that by (auto elim: steps.cases)

lemmas stepsD = steps_ConsD steps_appendD1 steps_appendD2

lemma steps_alt_induct[consumes 1, case_names Single Snoc]:
  assumes
    "steps x" "(x. P [x])"
    "y x xs. E y x  steps (xs @ [y])  P (xs @ [y])  P (xs @ [y,x])"
  shows "P x"
  using assms(1)
  proof (induction rule: rev_induct)
    case Nil
    then show ?case by (auto elim: steps.cases)
  next
    case prems: (snoc x xs)
    then show ?case by (cases xs rule: rev_cases) (auto intro: assms(2,3) dest!: steps_appendD3)
  qed

lemma steps_appendI:
  "steps (xs @ [x, y])" if "steps (xs @ [x])" "E x y"
  using that
proof (induction xs)
  case Nil
  then show ?case by auto
next
  case (Cons a xs)
  then show ?case by (cases xs; auto elim: steps.cases)
qed

lemma steps_append_single:
  assumes
    "steps xs" "E (last xs) x" "xs  []"
  shows "steps (xs @ [x])"
  using assms(3,1,2) by (induction xs rule: list_nonempty_induct) (auto 4 4 elim: steps.cases)

lemma extend_run:
  assumes
    "steps xs" "E (last xs) x" "run (x ## ys)" "xs  []"
  shows "run (xs @- x ## ys)"
  using assms(4,1-3) by (induction xs rule: list_nonempty_induct) (auto 4 3 elim: steps.cases)

lemma run_cycle:
  assumes "steps xs" "E (last xs) (hd xs)" "xs  []"
  shows "run (cycle xs)"
  using assms proof (coinduction arbitrary: xs)
  case run
  then show ?case
    apply (rewrite at cycle xs stream.collapse[symmetric])
    apply (rewrite at stl (cycle xs) stream.collapse[symmetric])
    apply clarsimp
    apply (erule steps.cases)
    subgoal for x
      apply (rule conjI)
       apply (simp; fail)
      apply (rule disjI1)
      apply (inst_existentials xs)
         apply (simp, metis cycle_Cons[of x "[]", simplified])
      by auto
    subgoal for x y xs'
      apply (rule conjI)
       apply (simp; fail)
      apply (rule disjI1)
      apply (inst_existentials "y # xs' @ [x]")
      using steps_append_single[of "y # xs'" x]
         apply (auto elim: steps.cases split: if_split_asm simp: cycle_Cons)
      done
    done
qed

lemma run_stl:
  "run (stl xs)" if "run xs"
  using that by (auto elim: run.cases)

lemma run_sdrop:
  "run (sdrop n xs)" if "run xs"
  using that by (induction n arbitrary: xs) (auto intro: run_stl)

lemma run_reachable':
  assumes "run (x ## xs)" "E** x0 x"
  shows "pred_stream (λ x. E** x0 x) xs"
  using assms by (coinduction arbitrary: x xs) (auto 4 3 elim: run.cases)

lemma run_reachable:
  assumes "run (x0 ## xs)"
  shows "pred_stream (λ x. E** x0 x) xs"
  by (rule run_reachable'[OF assms]) blast

lemma run_decomp:
  assumes "run (xs @- ys)" "xs  []"
  shows "steps xs  run ys  E (last xs) (shd ys)"
using assms(2,1) proof (induction xs rule: list_nonempty_induct)
  case (single x)
  then show ?case by (auto elim: run.cases)
next
  case (cons x xs)
  then show ?case by (cases xs; auto 4 4 elim: run.cases)
qed

lemma steps_decomp:
  assumes "steps (xs @ ys)" "xs  []" "ys  []"
  shows "steps xs  steps ys  E (last xs) (hd ys)"
using assms(2,1,3) proof (induction xs rule: list_nonempty_induct)
  case (single x)
  then show ?case by (auto elim: steps.cases)
next
  case (cons x xs)
  then show ?case by (cases xs; auto 4 4 elim: steps.cases)
qed

lemma steps_rotate:
  assumes "steps (x # xs @ y # ys @ [x])"
  shows "steps (y # ys @ x # xs @ [y])"
proof -
  from steps_decomp[of "x # xs" "y # ys @ [x]"] assms have
    "steps (x # xs)" "steps (y # ys @ [x])" "E (last (x # xs)) y"
    by auto
  then have "steps ((x # xs) @ [y])" by (blast intro: steps_append_single)
  from steps_append[OF steps (y # ys @ [x]) this] show ?thesis by auto
qed

lemma run_shift_coinduct[case_names run_shift, consumes 1]:
  assumes "R w"
      and " w. R w   u v x y. w = u @- x ## y ## v  steps (u @ [x])  E x y  R (y ## v)"
  shows "run w"
  using assms(2)[OF R w] proof (coinduction arbitrary: w)
  case (run w)
  then obtain u v x y where "w = u @- x ## y ## v" "steps (u @ [x])" "E x y" "R (y ## v)"
    by auto
  then show ?case
    apply -
    apply (drule assms(2))
    apply (cases u)
     apply force
    subgoal for z zs
      apply (cases zs)
      subgoal
        apply simp
        apply safe
         apply (force elim: steps.cases)
        subgoal for u' v' x' y'
          by (inst_existentials "x # u'") (cases u'; auto)
        done
      subgoal for a as
        apply simp
        apply safe
         apply (force elim: steps.cases)
        subgoal for u' v' x' y'
          apply (inst_existentials "a # as @ x # u'")
          using steps_append[of "a # as @ [x, y]" "u' @ [x']"]
          apply simp
          apply (drule steps_appendI[of "a # as" x, rotated])
          by (cases u'; force elim: steps.cases)+
        done
      done
    done
qed

lemma run_flat_coinduct[case_names run_shift, consumes 1]:
  assumes "R xss"
    and
    " xs ys xss.
    R (xs ## ys ## xss)  xs  []  steps xs  E (last xs) (hd ys)  R (ys ## xss)"
  shows "run (flat xss)"
proof -
  obtain xs ys xss' where "xss = xs ## ys ## xss'" by (metis stream.collapse)
  with assms(2)[OF assms(1)[unfolded this]] show ?thesis
  proof (coinduction arbitrary: xs ys xss' xss rule: run_shift_coinduct)
    case (run_shift xs ys xss' xss)
    from run_shift show ?case
      apply (cases xss')
      apply clarify
      apply (drule assms(2))
      apply (inst_existentials "butlast xs" "tl ys @- flat xss'" "last xs" "hd ys")
         apply (cases ys)
          apply (simp; fail)
      subgoal premises prems for x1 x2 z zs
      proof (cases "xs = []")
        case True
        with prems show ?thesis
          by auto
      next
        case False
        then have "xs = butlast xs @ [last xs]" by auto
        then have "butlast xs @- last xs ## tail = xs @- tail" for tail
          by (metis shift.simps(1,2) shift_append)
        with prems show ?thesis by simp
      qed
        apply (simp; fail)
       apply assumption
      subgoal for ws wss
        by (inst_existentials ys ws wss) (cases ys, auto)
      done
  qed
qed

lemma steps_non_empty[simp]:
  "¬ steps []"
  by (auto elim: steps.cases)

lemma steps_non_empty'[simp]:
  "xs  []" if "steps xs"
  using that by auto

(* XXX Generalize *)
lemma steps_replicate:
  "steps (hd xs # concat (replicate n (tl xs)))" if "last xs = hd xs" "steps xs" "n > 0"
  using that
proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  show ?case
  proof (cases n)
    case 0
    with Suc.prems show ?thesis by (cases xs; auto)
  next
    case prems: (Suc nat)
    from Suc.prems have [simp]: "hd xs # tl xs @ ys = xs @ ys" for ys
      by (cases xs; auto)
    from Suc.prems have **: "tl xs @ ys = tl (xs @ ys)" for ys
      by (cases xs; auto)
    from prems Suc show ?thesis
      by (fastforce intro: steps_append')
  qed
qed

notation E (‹_  _› [100, 100] 40)

abbreviation reaches (‹_ →* _› [100, 100] 40) where "reaches x y  E** x y"

abbreviation reaches1 (‹_ + _› [100, 100] 40) where "reaches1 x y  E++ x y"

lemma steps_reaches:
  "hd xs →* last xs" if "steps xs"
  using that by (induction xs) auto

lemma steps_reaches':
  "x →* y" if "steps xs" "hd xs = x" "last xs = y"
  using that steps_reaches by auto

lemma reaches_steps:
  " xs. hd xs = x  last xs = y  steps xs" if "x →* y"
  using that
  apply (induction)
   apply force
  apply clarsimp
  subgoal for z xs
    by (inst_existentials "xs @ [z]", (cases xs; simp), auto intro: steps_append_single)
  done

lemma reaches_steps_iff:
  "x →* y  ( xs. hd xs = x  last xs = y  steps xs)"
  using steps_reaches reaches_steps by fast

lemma steps_reaches1:
  "x + y" if "steps (x # xs @ [y])"
  by (metis list.sel(1,3) rtranclp_into_tranclp2 snoc_eq_iff_butlast steps.cases steps_reaches that)

lemma stepsI:
  "steps (x # xs)" if "x  hd xs" "steps xs"
  using that by (cases xs) auto

lemma reaches1_steps:
  " xs. steps (x # xs @ [y])" if "x + y"
proof -
  from that obtain z where "x  z" "z →* y"
    by atomize_elim (simp add: tranclpD)
  from reaches_steps[OF this(2)] obtain xs where *: "hd xs = z" "last xs = y" "steps xs"
    by auto
  then obtain xs' where [simp]: "xs = xs' @ [y]"
    by atomize_elim (auto 4 3 intro: append_butlast_last_id[symmetric])
  with x  z * show ?thesis
    by (auto intro: stepsI)
qed

lemma reaches1_steps_iff:
  "x + y  ( xs. steps (x # xs @ [y]))"
  using steps_reaches1 reaches1_steps by fast

lemma reaches_steps_iff2:
  "x →* y  (x = y  (vs. steps (x # vs @ [y])))"
  by (simp add: Nitpick.rtranclp_unfold reaches1_steps_iff)

lemma reaches1_reaches_iff1:
  "x + y  ( z. x  z  z →* y)"
  by (auto dest: tranclpD)

lemma reaches1_reaches_iff2:
  "x + y  ( z. x →* z  z  y)"
  apply safe
   apply (metis Nitpick.rtranclp_unfold tranclp.cases)
  by auto

lemma
  "x + z" if "x →* y" "y + z"
  using that by auto

lemma
  "x + z" if "x + y" "y →* z"
  using that by auto

lemma steps_append2:
  "steps (xs @ x # ys)" if "steps (xs @ [x])" "steps (x # ys)"
  using that by (auto dest: steps_append)

lemma reaches1_steps_append:
  assumes "a + b" "steps xs" "hd xs = b"
  shows " ys. steps (a # ys @ xs)"
  using assms by (fastforce intro: steps_append' dest: reaches1_steps)

lemma steps_last_step:
  " a. a  last xs" if "steps xs" "length xs > 1"
  using that by induction auto

lemma steps_remove_cycleE:
  assumes "steps (a # xs @ [b])"
  obtains ys where "steps (a # ys @ [b])" "distinct ys" "a  set ys" "b  set ys" "set ys  set xs"
  using assms
proof (induction "length xs" arbitrary: xs rule: less_induct)
  case less
  note prems = less.prems(2) and intro = less.prems(1) and IH = less.hyps
  consider
    "distinct xs" "a  set xs" "b  set xs" | "a  set xs" | "b  set xs" | "¬ distinct xs"
    by auto
  then consider (goal) ?case
    | (a) as bs where "xs = as @ a # bs" | (b) as bs where "xs = as @ b # bs"
    | (between) x as bs cs where "xs = as @ x # bs @ x # cs"
    using prems by (cases; fastforce dest: not_distinct_decomp simp: split_list intro: intro)
  then show ?case
  proof cases
    case a
    with prems show ?thesis
      by - (rule IH[where xs = bs], auto 4 3 intro: intro dest: stepsD)
  next
    case b
    with prems have "steps (a # as @ b # [] @ (bs @ [b]))"
      by simp
    then have "steps (a # as @ [b])"
      by (metis Cons_eq_appendI Graph_Defs.steps_appendD1 append_eq_appendI neq_Nil_conv)
    with b show ?thesis
      by - (rule IH[where xs = as], auto 4 3 dest: stepsD intro: intro)
  next
    case between
    with prems have "steps (a # as @ x # cs @ [b])"
      by simp (metis
          stepsI append_Cons list.distinct(1) list.sel(1) list.sel(3) steps_append steps_decomp)
    with between show ?thesis
      by - (rule IH[where xs = "as @ x # cs"], auto 4 3 intro: intro dest: stepsD)
  qed
qed

lemma reaches1_stepsE:
  assumes "a + b"
  obtains xs where "steps (a # xs @ [b])" "distinct xs" "a  set xs" "b  set xs"
proof -
  from assms obtain xs where "steps (a # xs @ [b])"
    by (auto dest: reaches1_steps)
  then show ?thesis
    by - (erule steps_remove_cycleE, rule that)
qed

lemma reaches_stepsE:
  assumes "a →* b"
  obtains "a = b" | xs where "steps (a # xs @ [b])" "distinct xs" "a  set xs" "b  set xs"
proof -
  from assms consider "a = b" | xs where "a + b"
    by (meson rtranclpD)
  then show ?thesis
    by cases ((erule reaches1_stepsE)?; rule that; assumption)+
qed

definition sink where
  "sink a  b. a  b"

lemma sink_or_cycle:
  assumes "finite {b. reaches a b}"
  obtains b where "reaches a b" "sink b" | b where "reaches a b" "reaches1 b b"
proof -
  let ?S = "{b. reaches1 a b}"
  have "?S  {b. reaches a b}"
    by auto
  then have "finite ?S"
    using assms by (rule finite_subset)
  then show ?thesis
    using that
  proof (induction ?S arbitrary: a rule: finite_psubset_induct)
    case psubset
    consider (empty) "Collect (reaches1 a) = {}" | b where "reaches1 a b"
      by auto
    then show ?case
    proof cases
      case empty
      then have "sink a"
        unfolding sink_def by auto
      with psubset.prems show ?thesis
        by auto
    next
      case 2
      show ?thesis
      proof (cases "reaches b a")
        case True
        with reaches1 a b have "reaches1 a a"
          by auto
        with psubset.prems show ?thesis
          by auto
      next
        case False
        show ?thesis
        proof (cases "reaches1 b b")
          case True
          with reaches1 a b psubset.prems show ?thesis
            by (auto intro: tranclp_into_rtranclp)
        next
          case False
          with ¬ reaches b a reaches1 a b have "Collect (reaches1 b)  Collect (reaches1 a)"
            by (intro psubsetI) auto
          then show ?thesis
            using reaches1 a b psubset.prems
            by - (erule psubset.hyps; meson tranclp_into_rtranclp tranclp_rtranclp_tranclp)
        qed
      qed
    qed
  qed
qed

text ‹
  A directed graph where every node has at least one ingoing edge, contains a directed cycle.
›
lemma directed_graph_indegree_ge_1_cycle':
  assumes "finite S" "S  {}" " y  S.  x  S. E x y"
  shows " x  S.  y. E x y  E** y x"
  using assms
proof (induction arbitrary: E rule: finite_ne_induct)
  case (singleton x)
  then show ?case by auto
next
  case (insert x S E)
  from insert.prems obtain y where "y  insert x S" "E y x"
    by auto
  show ?case
  proof (cases "y = x")
    case True
    with E y x show ?thesis by auto
  next
    case False
    with y  _ have "y  S" by auto
    define E' where "E' a b  E a b  (a = y  E x b)" for a b
    have E'_E: " c. E a c  E** c b" if "E' a b" for a b
      using that E y x unfolding E'_def by auto
    have [intro]: "E** a b" if "E' a b" for a b
      using that E y x unfolding E'_def by auto
    have [intro]: "E** a b" if "E'** a b" for a b
      using that by (induction; blast intro: rtranclp_trans)
    have "yS. xS. E' x y"
    proof (rule ballI)
      fix b assume "b  S"
      with insert.prems obtain a where "a  insert x S" "E a b"
        by auto
      show "aS. E' a b"
      proof (cases "a = x")
        case True
        with E a b have "E' y b" unfolding E'_def by simp
        with y  S show ?thesis ..
      next
        case False
        with a  _ E a b show ?thesis unfolding E'_def by auto
      qed
    qed
    from insert.IH[OF this] obtain x y where "x  S" "E' x y" "E'** y x" by safe
    then show ?thesis by (blast intro: rtranclp_trans dest: E'_E)
    qed
  qed

lemma directed_graph_indegree_ge_1_cycle:
  assumes "finite S" "S  {}" " y  S.  x  S. E x y"
  shows " x  S.  y. x + x"
  using directed_graph_indegree_ge_1_cycle'[OF assms] reaches1_reaches_iff1 by blast


text ‹Vertices of a graph›

definition "vertices = {x. y. E x y  E y x}"

lemma reaches1_verts:
  assumes "x + y"
  shows "x  vertices" and "y  vertices"
  using assms reaches1_reaches_iff2 reaches1_reaches_iff1 vertices_def by blast+


lemmas graphI =
  steps.intros
  steps_append_single
  steps_reaches'
  stepsI

end (* Graph Defs *)


section ‹Graphs with a Start Node›

locale Graph_Start_Defs = Graph_Defs +
  fixes s0 :: 'a
begin

definition reachable where
  "reachable = E** s0"

lemma start_reachable[intro!, simp]:
  "reachable s0"
  unfolding reachable_def by auto

lemma reachable_step:
  "reachable b" if "reachable a" "E a b"
  using that unfolding reachable_def by auto

lemma reachable_reaches:
  "reachable b" if "reachable a" "a →* b"
  using that(2,1) by induction (auto intro: reachable_step)

lemma reachable_steps_append:
  assumes "reachable a" "steps xs" "hd xs = a" "last xs = b"
  shows "reachable b"
  using assms by (auto intro: graphI reachable_reaches)

lemmas steps_reachable = reachable_steps_append[of s0, simplified]

lemma reachable_steps_elem:
  "reachable y" if "reachable x" "steps xs" "y  set xs" "hd xs = x"
proof -
  from y  set xs obtain as bs where [simp]: "xs = as @ y # bs"
    by (auto simp: in_set_conv_decomp)
  show ?thesis
  proof (cases "as = []")
    case True
    with that show ?thesis
      by simp
  next
    case False
    (* XXX *)
    from steps xs have "steps (as @ [y])"
      by (auto intro: stepsD)
    with as  [] hd xs = x reachable x show ?thesis
      by (auto 4 3 intro: reachable_reaches graphI)
  qed
qed

lemma reachable_steps:
  " xs. steps xs  hd xs = s0  last xs = x" if "reachable x"
  using that unfolding reachable_def
proof induction
  case base
  then show ?case by (inst_existentials "[s0]"; force)
next
  case (step y z)
  from step.IH obtain xs where "steps xs" "s0 = hd xs" "y = last xs" by clarsimp
  with step.hyps show ?case
    apply (inst_existentials "xs @ [z]")
    apply (force intro: graphI)
    by (cases xs; auto)+
qed

lemma reachable_cycle_iff:
  "reachable x  x + x  ( ws xs. steps (s0 # ws @ [x] @ xs @ [x]))"
proof (safe, goal_cases)
  case (2 ws)
  then show ?case
    by (auto intro: steps_reachable stepsD)
next
  case (3 ws xs)
  then show ?case
    by (auto intro: stepsD steps_reaches1)
next
  case prems: 1
  from reachable x prems(2) have "s0 + x"
    unfolding reachable_def by auto
  with x + x show ?case
    by (fastforce intro: steps_append' dest: reaches1_steps)
qed

lemma reachable_induct[consumes 1, case_names start step, induct pred: reachable]:
  assumes "reachable x"
    and "P s0"
    and " a b. reachable a  P a  a  b  P b"
  shows "P x"
  using assms(1) unfolding reachable_def
  by induction (auto intro: assms(2-)[unfolded reachable_def])

lemmas graphI_aggressive =
  tranclp_into_rtranclp
  rtranclp.rtrancl_into_rtrancl
  tranclp.trancl_into_trancl
  rtranclp_into_tranclp2

lemmas graphI_aggressive1 =
  graphI_aggressive
  steps_append'

lemmas graphI_aggressive2 =
  graphI_aggressive
  stepsD
  steps_reaches1
  steps_reachable

lemmas graphD =
  reaches1_steps

lemmas graphD_aggressive =
  tranclpD

lemmas graph_startI =
  reachable_reaches
  start_reachable

end (* Graph Start Defs *)


section ‹Subgraphs›

subsection ‹Edge-induced Subgraphs›

locale Subgraph_Defs = G: Graph_Defs +
  fixes E' :: "'a  'a  bool"
begin

sublocale G': Graph_Defs E' .

end (* Subgraph Defs *)

locale Subgraph_Start_Defs = G: Graph_Start_Defs +
  fixes E' :: "'a  'a  bool"
begin

sublocale G': Graph_Start_Defs E' s0 .

end (* Subgraph Start Defs *)

locale Subgraph = Subgraph_Defs +
  assumes subgraph[intro]: "E' a b  E a b"
begin

lemma non_subgraph_cycle_decomp:
  " c d. G.reaches a c  E c d  ¬ E' c d  G.reaches d b" if
  "G.reaches1 a b" "¬ G'.reaches1 a b" for a b
    using that
  proof induction
    case (base y)
    then show ?case
      by auto
  next
    case (step y z)
    show ?case
    proof (cases "E' y z")
      case True
      with step have "¬ G'.reaches1 a y"
        by (auto intro: tranclp.trancl_into_trancl) (* XXX *)
      with step obtain c d where
        "G.reaches a c" "E c d" "¬ E' c d" "G.reaches d y"
        by auto
      with E' y z show ?thesis
        by (blast intro: rtranclp.rtrancl_into_rtrancl) (* XXX *)
    next
      case False
      with step show ?thesis
        by (intro exI conjI) auto
    qed
  qed

lemma reaches:
  "G.reaches a b" if "G'.reaches a b"
  using that by induction (auto intro: rtranclp.intros(2))

lemma reaches1:
  "G.reaches1 a b" if "G'.reaches1 a b"
  using that by induction (auto intro: tranclp.intros(2))

end (* Subgraph *)

locale Subgraph_Start = Subgraph_Start_Defs + Subgraph
begin

lemma reachable_subgraph[intro]: "G.reachable b" if G.reachable a G'.reaches a b for a b
  using that by (auto intro: G.graph_startI mono_rtranclp[rule_format, of E'])

lemma reachable:
  "G.reachable x" if "G'.reachable x"
  using that by (fastforce simp: G.reachable_def G'.reachable_def)

end (* Subgraph Start *)

subsection ‹Node-induced Subgraphs›

locale Subgraph_Node_Defs = Graph_Defs +
  fixes V :: "'a  bool"
begin

definition E' where "E' x y  E x y  V x  V y"

sublocale Subgraph E E' by standard (auto simp: E'_def)

lemma subgraph':
  "E' x y" if "E x y" "V x" "V y"
  using that unfolding E'_def by auto

lemma E'_V1:
  "V x" if "E' x y"
  using that unfolding E'_def by auto

lemma E'_V2:
  "V y" if "E' x y"
  using that unfolding E'_def by auto

lemma G'_reaches_V:
  "V y" if "G'.reaches x y" "V x"
  using that by (cases) (auto intro: E'_V2)

lemma G'_steps_V_all:
  "list_all V xs" if "G'.steps xs" "V (hd xs)"
  using that by induction (auto intro: E'_V2)

lemma G'_steps_V_last:
  "V (last xs)" if "G'.steps xs" "V (hd xs)"
  using that by induction (auto dest: E'_V2)

lemmas subgraphI = E'_V1 E'_V2 G'_reaches_V

lemmas subgraphD = E'_V1 E'_V2 G'_reaches_V

end (* Subgraph Node *)


locale Subgraph_Node_Defs_Notation = Subgraph_Node_Defs
begin

no_notation E (‹_  _› [100, 100] 40)
notation E' (‹_  _› [100, 100] 40)
no_notation reaches (‹_ →* _› [100, 100] 40)
notation G'.reaches (‹_ →* _› [100, 100] 40)
no_notation reaches1 (‹_ + _› [100, 100] 40)
notation G'.reaches1 (‹_ + _› [100, 100] 40)

end (* Subgraph_Node_Defs_Notation *)


subsection ‹The Reachable Subgraph›

context Graph_Start_Defs
begin

interpretation Subgraph_Node_Defs_Notation E reachable .

sublocale reachable_subgraph: Subgraph_Node_Defs E reachable .

lemma reachable_supgraph:
  "x  y" if "E x y" "reachable x"
  using that unfolding E'_def by (auto intro: graph_startI)

lemma reachable_reaches_equiv: "reaches x y  x →* y" if "reachable x" for x y
  apply standard
  subgoal premises prems
    using prems reachable x
    by induction (auto dest: reachable_supgraph intro: graph_startI graphI_aggressive)
  subgoal premises prems
    using prems reachable x
    by induction (auto dest: subgraph)
  done

lemma reachable_reaches1_equiv: "reaches1 x y  x + y" if "reachable x" for x y
  apply standard
  subgoal premises prems
    using prems reachable x
    by induction (auto dest: reachable_supgraph intro: graph_startI graphI_aggressive)
  subgoal premises prems
    using prems reachable x
    by induction (auto dest: subgraph)
  done

lemma reachable_steps_equiv:
  "steps (x # xs)  G'.steps (x # xs)" if "reachable x"
  apply standard
  subgoal premises prems
    using prems reachable x
    by (induction "x # xs" arbitrary: x xs) (auto dest: reachable_supgraph intro: graph_startI)
  subgoal premises prems
    using prems by induction auto
  done

end (* Graph Start Defs *)


section ‹Bundles›

bundle graph_automation
begin

lemmas [intro] = Graph_Defs.graphI Graph_Start_Defs.graph_startI
lemmas [dest]  = Graph_Start_Defs.graphD

end (* Bundle *)

bundle reaches_steps_iff =
  Graph_Defs.reaches1_steps_iff [iff]
  Graph_Defs.reaches_steps_iff  [iff]

bundle graph_automation_aggressive
begin

unbundle graph_automation

lemmas [intro] = Graph_Start_Defs.graphI_aggressive
lemmas [dest]  = Graph_Start_Defs.graphD_aggressive

end (* Bundle *)

bundle subgraph_automation
begin

unbundle graph_automation

lemmas [intro] = Subgraph_Node_Defs.subgraphI
lemmas [dest]  = Subgraph_Node_Defs.subgraphD

end (* Bundle *)


section ‹Directed Acyclic Graphs›
locale DAG = Graph_Defs +
  assumes acyclic: "¬ E++ x x"
begin

lemma topological_numbering:
  fixes S assumes "finite S"
  shows "f :: _  nat. inj_on f S  (x  S. y  S. E x y  f x < f y)"
  using assms
proof (induction rule: finite_psubset_induct)
  case (psubset A)
  show ?case
  proof (cases "A = {}")
    case True
    then show ?thesis
      by simp
  next
    case False
    then obtain x where x: "x  A" "y  A. ¬E y x"
      using directed_graph_indegree_ge_1_cycle[OF finite A] acyclic by auto
    let ?A = "A - {x}"
    from x  A have "?A  A"
      by auto
    from psubset.IH(1)[OF this] obtain f :: "_  nat" where f:
      "inj_on f ?A" "x?A. y?A. x  y  f x < f y"
      by blast
    let ?f = "λy. if x  y then f y + 1 else 0"
    from x  A have "A = insert x ?A"
      by auto
    from inj_on f ?A have "inj_on ?f A"
      by (auto simp: inj_on_def)
    moreover from f(2) x(2) have "xA. yA. x  y  ?f x < ?f y"
      by auto
    ultimately show ?thesis
      by blast
  qed
qed

end


section ‹Finite Graphs›

locale Finite_Graph = Graph_Defs +
  assumes finite_graph: "finite vertices"

locale Finite_DAG = Finite_Graph + DAG
begin

lemma finite_reachable:
  "finite {y. x →* y}" (is "finite ?S")
proof -
  have "?S  insert x vertices"
    by (metis insertCI mem_Collect_eq reaches1_verts(2) rtranclpD subsetI)
  also from finite_graph have "finite " ..
  finally show ?thesis .
qed

end


section ‹Graph Invariants›

locale Graph_Invariant = Graph_Defs +
  fixes P :: "'a  bool"
  assumes invariant: "P a  a  b  P b"
begin

lemma invariant_steps:
  "list_all P as" if "steps (a # as)" "P a"
  using that by (induction "a # as" arbitrary: as a) (auto intro: invariant)

lemma invariant_reaches:
  "P b" if "a →* b" "P a"
  using that by (induction; blast intro: invariant)

lemma invariant_run:
  assumes run: "run (x ## xs)" and P: "P x"
  shows "pred_stream P (x ## xs)"
  using run P by (coinduction arbitrary: x xs) (auto 4 3 elim: invariant run.cases)

text ‹Every graph invariant induces a subgraph.›
sublocale Subgraph_Node_Defs where E = E and V = P .

lemma subgraph':
  assumes "x  y" "P x"
  shows "E' x y"
  using assms by (intro subgraph') (auto intro: invariant)

lemma invariant_steps_iff:
  "G'.steps (v # vs)  steps (v # vs)" if "P v"
  apply (rule iffI)
  subgoal
    using G'.steps_alt_induct steps_appendI by blast
  subgoal premises prems
    using prems P v by (induction "v # vs" arbitrary: v vs) (auto intro: subgraph' invariant)
  done

lemma invariant_reaches_iff:
  "G'.reaches u v  reaches u v" if "P u"
  using that by (simp add: reaches_steps_iff2 G'.reaches_steps_iff2 invariant_steps_iff)

lemma invariant_reaches1_iff:
  "G'.reaches1 u v  reaches1 u v" if "P u"
  using that by (simp add: reaches1_steps_iff G'.reaches1_steps_iff invariant_steps_iff)

end (* Graph Invariant *)

locale Graph_Invariants = Graph_Defs +
  fixes P Q :: "'a  bool"
  assumes invariant: "P a  a  b  Q b" and Q_P: "Q a  P a"
begin

sublocale Pre: Graph_Invariant E P
  by standard (blast intro: invariant Q_P)

sublocale Post: Graph_Invariant E Q
  by standard (blast intro: invariant Q_P)

lemma invariant_steps:
  "list_all Q as" if "steps (a # as)" "P a"
  using that by (induction "a # as" arbitrary: as a) (auto intro: invariant Q_P)

lemma invariant_run:
  assumes run: "run (x ## xs)" and P: "P x"
  shows "pred_stream Q xs"
  using run P by (coinduction arbitrary: x xs) (auto 4 4 elim: invariant run.cases intro: Q_P)

lemma invariant_reaches1:
  "Q b" if "a + b" "P a"
  using that by (induction; blast intro: invariant Q_P)

end (* Graph Invariants *)

locale Graph_Invariant_Start = Graph_Start_Defs + Graph_Invariant +
  assumes P_s0: "P s0"
begin

lemma invariant_steps:
  "list_all P as" if "steps (s0 # as)"
  using that P_s0 by (rule invariant_steps)

lemma invariant_reaches:
  "P b" if "s0 →* b"
  using invariant_reaches[OF that P_s0] .

lemmas invariant_run = invariant_run[OF _ P_s0]

end (* Graph Invariant Start *)

locale Graph_Invariant_Strong = Graph_Defs +
  fixes P :: "'a  bool"
  assumes invariant: "a  b  P b"
begin

sublocale inv: Graph_Invariant by standard (rule invariant)

lemma P_invariant_steps:
  "list_all P as" if "steps (a # as)"
  using that by (induction "a # as" arbitrary: as a) (auto intro: invariant)

lemma steps_last_invariant:
  "P (last xs)" if "steps (x # xs)" "xs  []"
  using steps_last_step[of "x # xs"] that by (auto intro: invariant)

lemmas invariant_reaches = inv.invariant_reaches

lemma invariant_reaches1:
  "P b" if "a + b"
  using that by (induction; blast intro: invariant)

end (* Graph Invariant *)


section ‹Simulations and Bisimulations›
locale Simulation_Defs =
  fixes A :: "'a  'a  bool" and B :: "'b  'b  bool"
    and sim :: "'a  'b  bool" (infixr  60)
begin

sublocale A: Graph_Defs A .

sublocale B: Graph_Defs B .

end (* Simulation Defs *)

locale Simulation = Simulation_Defs +
  assumes A_B_step: " a b a'. A a b  a  a'  ( b'. B a' b'  b  b')"
begin

lemma simulation_reaches:
  " b'. B** b b'  a'  b'" if "A** a a'" "a  b"
  using that by (induction rule: rtranclp_induct) (auto intro: rtranclp.intros(2) dest: A_B_step)

lemma simulation_reaches1:
  " b'. B++ b b'  a'  b'" if "A++ a a'" "a  b"
  using that by (induction rule: tranclp_induct) (auto 4 3 intro: tranclp.intros(2) dest: A_B_step)

lemma simulation_steps:
  " bs. B.steps (b # bs)  list_all2 (λ a b. a  b) as bs" if "A.steps (a # as)" "a  b"
  using that
  apply (induction "a # as" arbitrary: a b as)
   apply force
  apply (frule A_B_step, auto)
  done

lemma simulation_run:
  " ys. B.run (y ## ys)  stream_all2 (∼) xs ys" if "A.run (x ## xs)" "x  y"
proof -
  let ?ys = "sscan (λ a' b. SOME b'. B b b'  a'  b') xs y"
  have "B.run (y ## ?ys)"
    using that by (coinduction arbitrary: x y xs) (force dest!: someI_ex A_B_step elim: A.run.cases)
  moreover have "stream_all2 (∼) xs ?ys"
    using that by (coinduction arbitrary: x y xs) (force dest!: someI_ex A_B_step elim: A.run.cases)
  ultimately show ?thesis by blast
qed

end (* Simulation *)

lemma (in Subgraph) Subgraph_Simulation:
  "Simulation E' E (=)"
  by standard auto

locale Simulation_Invariant = Simulation_Defs +
  fixes PA :: "'a  bool" and PB :: "'b  bool"
  assumes A_B_step: " a b a'. A a b  PA a  PB a'  a  a'  ( b'. B a' b'  b  b')"
  assumes A_invariant[intro]: " a b. PA a  A a b  PA b"
  assumes B_invariant[intro]: " a b. PB a  B a b  PB b"
begin

definition "equiv'  λ a b. a  b  PA a  PB b"

sublocale Simulation A B equiv' by standard (auto dest: A_B_step simp: equiv'_def)

sublocale PA_invariant: Graph_Invariant A PA by standard blast

sublocale PB_invariant: Graph_Invariant B PB by standard blast

lemma simulation_reaches:
  " b'. B** b b'  a'  b'  PA a'  PB b'" if "A** a a'" "a  b" "PA a" "PB b"
  using simulation_reaches[of a a' b] that unfolding equiv'_def by simp

lemma simulation_steps:
  " bs. B.steps (b # bs)  list_all2 (λ a b. a  b  PA a  PB b) as bs"
  if "A.steps (a # as)" "a  b" "PA a" "PB b"
  using simulation_steps[of a as b] that unfolding equiv'_def by simp

lemma simulation_steps':
  " bs. B.steps (b # bs)  list_all2 (λ a b. a  b) as bs  list_all PA as  list_all PB bs"
  if "A.steps (a # as)" "a  b" "PA a" "PB b"
  using simulation_steps[OF that]
  by (force dest: list_all2_set1 list_all2_set2 simp: list_all_iff elim: list_all2_mono)

context
  fixes f
  assumes eq: "a  b  b = f a"
begin

lemma simulation_steps'_map:
  " bs.
    B.steps (b # bs)  bs = map f as
     list_all2 (λ a b. a  b) as bs
     list_all PA as  list_all PB bs"
  if "A.steps (a # as)" "a  b" "PA a" "PB b"
proof -
  from simulation_steps'[OF that] obtain bs where guessed:
    "B.steps (b # bs)"
    "list_all2 (∼) as bs"
    "list_all PA as"
    "list_all PB bs"
    by safe
  from this(2) have "bs = map f as"
    by (induction; simp add: eq)
  with guessed show ?thesis
    by auto
qed

end (* Context for Equality Relation *)

end (* Simulation Invariant *)

locale Simulation_Invariants = Simulation_Defs +
  fixes PA QA :: "'a  bool" and PB QB :: "'b  bool"
  assumes A_B_step: " a b a'. A a b  PA a  PB a'  a  a'  ( b'. B a' b'  b  b')"
  assumes A_invariant[intro]: " a b. PA a  A a b  QA b"
  assumes B_invariant[intro]: " a b. PB a  B a b  QB b"
  assumes PA_QA[intro]: " a. QA a  PA a" and PB_QB[intro]: " a. QB a  PB a"
begin

sublocale Pre: Simulation_Invariant A B "(∼)" PA PB
  by standard (auto intro: A_B_step)

sublocale Post: Simulation_Invariant A B "(∼)" QA QB
  by standard (auto intro: A_B_step)

sublocale A_invs: Graph_Invariants A PA QA
  by standard auto

sublocale B_invs: Graph_Invariants B PB QB
  by standard auto

lemma simulation_reaches1:
  " b2. B.reaches1 b1 b2  a2  b2  QB b2" if "A.reaches1 a1 a2" "a1  b1" "PA a1" "PB b1"
  using that
  by - (drule Pre.simulation_reaches1, auto intro: B_invs.invariant_reaches1 simp: Pre.equiv'_def)

lemma reaches1_unique:
  assumes unique: " b2. a  b2  QB b2  b2 = b"
    and that: "A.reaches1 a a" "a  b" "PA a" "PB b"
  shows "B.reaches1 b b"
  using that by (auto dest: unique simulation_reaches1)

end (* Simualation Invariants *)

locale Bisimulation = Simulation_Defs +
  assumes A_B_step: " a b a'. A a b  a  a'  ( b'. B a' b'  b  b')"
  assumes B_A_step: " a a' b'. B a' b'  a  a'  ( b. A a b  b  b')"
begin

sublocale A_B: Simulation A B "(∼)" by standard (rule A_B_step)

sublocale B_A: Simulation B A "λ x y. y  x" by standard (rule B_A_step)

lemma A_B_reaches:
  " b'. B** b b'  a'  b'" if "A** a a'" "a  b"
  using A_B.simulation_reaches[OF that] .

lemma B_A_reaches:
  " b'. A** b b'  b'  a'" if "B** a a'" "b  a"
  using B_A.simulation_reaches[OF that] .

end (* Bisim *)

locale Bisimulation_Invariant = Simulation_Defs +
  fixes PA :: "'a  bool" and PB :: "'b  bool"
  assumes A_B_step: " a b a'. A a b  a  a'  PA a  PB a'  ( b'. B a' b'  b  b')"
  assumes B_A_step: " a a' b'. B a' b'  a  a'  PA a  PB a'  ( b. A a b  b  b')"
  assumes A_invariant[intro]: " a b. PA a  A a b  PA b"
  assumes B_invariant[intro]: " a b. PB a  B a b  PB b"
begin

sublocale PA_invariant: Graph_Invariant A PA by standard blast

sublocale PB_invariant: Graph_Invariant B PB by standard blast

lemmas B_steps_invariant[intro] = PB_invariant.invariant_reaches

definition "equiv'  λ a b. a  b  PA a  PB b"

sublocale bisim: Bisimulation A B equiv'
  by standard (clarsimp simp add: equiv'_def, frule A_B_step B_A_step, assumption; auto)+

sublocale A_B: Simulation_Invariant A B "(∼)" PA PB
  by (standard; blast intro: A_B_step B_A_step)

sublocale B_A: Simulation_Invariant B A "λ x y. y  x" PB PA
  by (standard; blast intro: A_B_step B_A_step)

context
  fixes f
  assumes eq: "a  b  b = f a"
    and inj: " a b. PB (f a)  PA b  f a = f b  a = b"
begin

lemma list_all2_inj_map_eq:
  "as = bs" if "list_all2 (λa b. a = f b) (map f as) bs" "list_all PB (map f as)" "list_all PA bs"
  using that inj
  by (induction "map f as" bs arbitrary: as rule: list_all2_induct) (auto simp: inj_on_def)

lemma steps_map_equiv:
  "A.steps (a # as)  B.steps (b # map f as)" if "a  b" "PA a" "PB b"
  using A_B.simulation_steps'_map[of f a as b] B_A.simulation_steps'[of b "map f as" a] that eq
  by (auto dest: list_all2_inj_map_eq)

lemma steps_map:
  " as. bs = map f as" if "B.steps (f a # bs)" "PA a" "PB (f a)"
proof -
  have "a  f a" unfolding eq ..
  from B_A.simulation_steps'[OF that(1) this PB _ PA _] obtain as where
    "A.steps (a # as)"
    "list_all2 (λa b. b  a) bs as"
    "list_all PB bs"
    "list_all PA as"
    by safe
  from this(2) show ?thesis
    unfolding eq by (inst_existentials as, induction rule: list_all2_induct, auto)
qed

lemma reaches_equiv:
  "A.reaches a a'  B.reaches (f a) (f a')" if "PA a" "PB (f a)"
  apply safe
   apply (drule A_B.simulation_reaches[of a a' "f a"]; simp add: eq that)
  apply (drule B_A.simulation_reaches)
     defer
     apply (rule that | clarsimp simp: eq | metis inj)+
  done

end (* Context for Equality Relation *)

lemma equiv'_D:
  "a  b" if "A_B.equiv' a b"
  using that unfolding A_B.equiv'_def by auto

lemma equiv'_rotate_1:
  "B_A.equiv' b a" if "A_B.equiv' a b"
  using that by (auto simp: B_A.equiv'_def A_B.equiv'_def)

lemma equiv'_rotate_2:
  "A_B.equiv' a b" if "B_A.equiv' b a"
  using that by (auto simp: B_A.equiv'_def A_B.equiv'_def)

lemma stream_all2_equiv'_D:
  "stream_all2 (∼) xs ys" if "stream_all2 A_B.equiv' xs ys"
  using stream_all2_weaken[OF that equiv'_D] by fast

lemma stream_all2_equiv'_D2:
  "stream_all2 B_A.equiv' ys xs  stream_all2 ((∼)¯¯) ys xs"
  by (coinduction arbitrary: xs ys) (auto simp: B_A.equiv'_def)

lemma stream_all2_rotate_1:
  "stream_all2 B_A.equiv' ys xs  stream_all2 A_B.equiv' xs ys"
  by (coinduction arbitrary: xs ys) (auto simp: B_A.equiv'_def A_B.equiv'_def)

lemma stream_all2_rotate_2:
  "stream_all2 A_B.equiv' xs ys  stream_all2 B_A.equiv' ys xs"
  by (coinduction arbitrary: xs ys) (auto simp: B_A.equiv'_def A_B.equiv'_def)

end (* Bisim Invariant *)

locale Bisimulation_Invariants = Simulation_Defs +
  fixes PA QA :: "'a  bool" and PB QB :: "'b  bool"
  assumes A_B_step: " a b a'. A a b  a  a'  PA a  PB a'  ( b'. B a' b'  b  b')"
  assumes B_A_step: " a a' b'. B a' b'  a  a'  PA a  PB a'  ( b. A a b  b  b')"
  assumes A_invariant[intro]: " a b. PA a  A a b  QA b"
  assumes B_invariant[intro]: " a b. PB a  B a b  QB b"
  assumes PA_QA[intro]: " a. QA a  PA a" and PB_QB[intro]: " a. QB a  PB a"
begin

sublocale PA_invariant: Graph_Invariant A PA by standard blast

sublocale PB_invariant: Graph_Invariant B PB by standard blast

sublocale QA_invariant: Graph_Invariant A QA by standard blast

sublocale QB_invariant: Graph_Invariant B QB by standard blast

sublocale Pre_Bisim: Bisimulation_Invariant A B "(∼)" PA PB
  by standard (auto intro: A_B_step B_A_step)

sublocale Post_Bisim: Bisimulation_Invariant A B "(∼)" QA QB
  by standard (auto intro: A_B_step B_A_step)

sublocale A_B: Simulation_Invariants A B "(∼)" PA QA PB QB
  by standard (blast intro: A_B_step)+

sublocale B_A: Simulation_Invariants B A "λ x y. y  x" PB QB PA QA
  by standard (blast intro: B_A_step)+

context
  fixes f
  assumes eq[simp]: "a  b  b = f a"
    and inj: " a b. QB (f a)  QA b  f a = f b  a = b"
begin

lemmas list_all2_inj_map_eq = Post_Bisim.list_all2_inj_map_eq[OF eq inj]
lemmas steps_map_equiv' = Post_Bisim.steps_map_equiv[OF eq inj]

lemma list_all2_inj_map_eq':
  "as = bs" if "list_all2 (λa b. a = f b) (map f as) bs" "list_all QB (map f as)" "list_all QA bs"
  using that by (rule list_all2_inj_map_eq)

lemma steps_map_equiv:
  "A.steps (a # as)  B.steps (b # map f as)" if "a  b" "PA a" "PB b"
proof
  assume "A.steps (a # as)"
  then show "B.steps (b # map f as)"
  proof cases
    case Single
    then show ?thesis by auto
  next
    case prems: (Cons a' xs)
    from A_B_step[OF A a a' a  b PA a PB b] obtain b' where "B b b'" "a'  b'"
      by auto
    with steps_map_equiv'[OF a'  b', of xs] prems that show ?thesis
      by auto
  qed
next
  assume "B.steps (b # map f as)"
  then show "A.steps (a # as)"
  proof cases
    case Single
    then show ?thesis by auto
  next
    case prems: (Cons b' xs)
    from B_A_step[OF B b b' a  b PA a PB b] obtain a' where "A a a'" "a'  b'"
      by auto
    with that prems have "QA a'" "QB b'"
      by auto
    with A a a' a'  b' steps_map_equiv'[OF a'  b', of "tl as"] prems that show ?thesis
      apply clarsimp
      subgoal for z zs
        using inj[rule_format, of z a'] by auto
      done
  qed
qed

lemma steps_map:
  " as. bs = map f as" if "B.steps (f a # bs)" "PA a" "PB (f a)"
  using that proof cases
  case Single
  then show ?thesis by simp
next
  case prems: (Cons b' xs)
  from B_A_step[OF B _ b' _ PA a PB (f a)] obtain a' where "A a a'" "a'  b'"
    by auto
  with that prems have "QA a'" "QB b'"
    by auto
  with Post_Bisim.steps_map[OF eq inj, of a' xs] prems a'  b' obtain ys where "xs = map f ys"
    by auto
  with bs = _ a'  b' show ?thesis
    by (inst_existentials "a' # ys") auto
qed

text @{thm Post_Bisim.reaches_equiv} cannot be lifted directly:
  injectivity cannot be applied for the reflexive case.
›
lemma reaches1_equiv:
  "A.reaches1 a a'  B.reaches1 (f a) (f a')" if "PA a" "PB (f a)"
proof safe
  assume "A.reaches1 a a'"
  then obtain a'' where prems: "A a a''" "A.reaches a'' a'"
    including graph_automation_aggressive by blast
  from A_B_step[OF A a _ _ that] obtain b where "B (f a) b" "a''  b"
    by auto
  with that prems have "QA a''" "QB b"
    by auto
  with Post_Bisim.reaches_equiv[OF eq inj, of a'' a'] prems B (f a) b a''  b
  show "B.reaches1 (f a) (f a')"
    by auto
next
  assume "B.reaches1 (f a) (f a')"
  then obtain b where prems: "B (f a) b" "B.reaches b (f a')"
    including graph_automation_aggressive by blast
  from B_A_step[OF B _ b _ PA a PB (f a)] obtain a'' where "A a a''" "a''  b"
    by auto
  with that prems have "QA a''" "QB b"
    by auto
  with Post_Bisim.reaches_equiv[OF eq inj, of a'' a'] prems A a a'' a''  b
  show "A.reaches1 a a'"
    by auto
qed

end (* Context for Equality Relation *)

end (* Bisim Invariant *)

lemma Bisimulation_Invariant_composition:
  assumes
    "Bisimulation_Invariant A B sim1 PA PB"
    "Bisimulation_Invariant B C sim2 PB PC"
  shows
    "Bisimulation_Invariant A C (λ a c.  b. PB b  sim1 a b  sim2 b c) PA PC"
proof -
  interpret A: Bisimulation_Invariant A B sim1 PA PB
    by (rule assms(1))
  interpret B: Bisimulation_Invariant B C sim2 PB PC
    by (rule assms(2))
  show ?thesis
    by (standard; (blast dest: A.A_B_step B.A_B_step | blast dest: A.B_A_step B.B_A_step))
qed

lemma Bisimulation_Invariant_filter:
  assumes
    "Bisimulation_Invariant A B sim PA PB"
    " a b. sim a b  PA a  PB b  FA a  FB b"
    " a b. A a b  FA b  A' a b"
    " a b. B a b  FB b  B' a b"
  shows
    "Bisimulation_Invariant A' B' sim PA PB"
proof -
  interpret Bisimulation_Invariant A B sim PA PB
    by (rule assms(1))
  have unfold:
    "A' = (λ a b. A a b  FA b)" "B' = (λ a b. B a b  FB b)"
    using assms(3,4) by auto
  show ?thesis
    unfolding unfold
    apply standard
    using assms(2) apply (blast dest: A_B_step)
    using assms(2) apply (blast dest: B_A_step)
    by blast+
qed

lemma Bisimulation_Invariants_filter:
  assumes
    "Bisimulation_Invariants A B sim PA QA PB QB"
    " a b. QA a  QB b  FA a  FB b"
    " a b. A a b  FA b  A' a b"
    " a b. B a b  FB b  B' a b"
  shows
    "Bisimulation_Invariants A' B' sim PA QA PB QB"
proof -
  interpret Bisimulation_Invariants A B sim PA QA PB QB
    by (rule assms(1))
  have unfold:
    "A' = (λ a b. A a b  FA b)" "B' = (λ a b. B a b  FB b)"
    using assms(3,4) by auto
  show ?thesis
    unfolding unfold
    apply standard
    using assms(2) apply (blast dest: A_B_step)
    using assms(2) apply (blast dest: B_A_step)
    by blast+
qed

lemma Bisimulation_Invariants_composition:
  assumes
    "Bisimulation_Invariants A B sim1 PA QA PB QB"
    "Bisimulation_Invariants B C sim2 PB QB PC QC"
  shows
    "Bisimulation_Invariants A C (λ a c.  b. PB b  sim1 a b  sim2 b c) PA QA PC QC"
proof -
  interpret A: Bisimulation_Invariants A B sim1 PA QA PB QB
    by (rule assms(1))
  interpret B: Bisimulation_Invariants B C sim2 PB QB PC QC
    by (rule assms(2))
  show ?thesis
    by (standard, blast dest: A.A_B_step B.A_B_step) (blast dest: A.B_A_step B.B_A_step)+
qed

lemma Bisimulation_Invariant_Invariants_composition:
  assumes
    "Bisimulation_Invariant A B sim1 PA PB"
    "Bisimulation_Invariants B C sim2 PB QB PC QC"
  shows
    "Bisimulation_Invariants A C (λ a c.  b. PB b  sim1 a b  sim2 b c) PA PA PC QC"
proof -
  interpret Bisimulation_Invariant A B sim1 PA PB
    by (rule assms(1))
  interpret B: Bisimulation_Invariants B C sim2 PB QB PC QC
    by (rule assms(2))
  interpret A: Bisimulation_Invariants A B sim1 PA PA PB QB
    by (standard; blast intro: A_B_step B_A_step)+
  show ?thesis
    by (standard; (blast dest: A.A_B_step B.A_B_step | blast dest: A.B_A_step B.B_A_step))
qed

lemma Bisimulation_Invariant_Bisimulation_Invariants:
  assumes "Bisimulation_Invariant A B sim PA PB"
  shows "Bisimulation_Invariants A B sim PA PA PB PB"
proof -
  interpret Bisimulation_Invariant A B sim PA PB
    by (rule assms)
  show ?thesis
    by (standard; blast intro: A_B_step B_A_step)
qed

lemma Bisimulation_Invariant_strengthen_post:
  assumes
    "Bisimulation_Invariant A B sim PA PB"
    " a b. PA' a  PA b  A a b  PA' b"
    " a. PA' a  PA a"
  shows "Bisimulation_Invariant A B sim PA' PB"
proof -
  interpret Bisimulation_Invariant A B sim PA PB
    by (rule assms)
  show ?thesis
    by (standard; blast intro: A_B_step B_A_step assms)
qed

lemma Bisimulation_Invariant_strengthen_post':
  assumes
    "Bisimulation_Invariant A B sim PA PB"
    " a b. PB' a  PB b  B a b  PB' b"
    " a. PB' a  PB a"
  shows "Bisimulation_Invariant A B sim PA PB'"
proof -
  interpret Bisimulation_Invariant A B sim PA PB
    by (rule assms)
  show ?thesis
    by (standard; blast intro: A_B_step B_A_step assms)
qed

lemma Simulation_Invariant_strengthen_post:
  assumes
    "Simulation_Invariant A B sim PA PB"
    " a b. PA a  PA b  A a b  PA' b"
    " a. PA' a  PA a"
  shows "Simulation_Invariant A B sim PA' PB"
proof -
  interpret Simulation_Invariant A B sim PA PB
    by (rule assms)
  show ?thesis
    by (standard; blast intro: A_B_step assms)
qed

lemma Simulation_Invariant_strengthen_post':
  assumes
    "Simulation_Invariant A B sim PA PB"
    " a b. PB a  PB b  B a b  PB' b"
    " a. PB' a  PB a"
  shows "Simulation_Invariant A B sim PA PB'"
proof -
  interpret Simulation_Invariant A B sim PA PB
    by (rule assms)
  show ?thesis
    by (standard; blast intro: A_B_step assms)
qed

lemma Simulation_Invariants_strengthen_post:
  assumes
    "Simulation_Invariants A B sim PA QA PB QB"
    " a b. PA a  QA b  A a b  QA' b"
    " a. QA' a  QA a"
  shows "Simulation_Invariants A B sim PA QA' PB QB"
proof -
  interpret Simulation_Invariants A B sim PA QA PB QB
    by (rule assms)
  show ?thesis
    by (standard; blast intro: A_B_step assms)
qed

lemma Simulation_Invariants_strengthen_post':
  assumes
    "Simulation_Invariants A B sim PA QA PB QB"
    " a b. PB a  QB b  B a b  QB' b"
    " a. QB' a  QB a"
  shows "Simulation_Invariants A B sim PA QA PB QB'"
proof -
  interpret Simulation_Invariants A B sim PA QA PB QB
    by (rule assms)
  show ?thesis
    by (standard; blast intro: A_B_step assms)
qed

lemma Bisimulation_Invariant_sim_replace:
  assumes "Bisimulation_Invariant A B sim PA PB"
      and " a b. PA a  PB b  sim a b  sim' a b"
    shows "Bisimulation_Invariant A B sim' PA PB"
proof -
  interpret Bisimulation_Invariant A B sim PA PB
    by (rule assms(1))
  show ?thesis
    apply standard
    using assms(2) apply (blast dest: A_B_step)
    using assms(2) apply (blast dest: B_A_step)
    by blast+
qed

end (* Theory *)