Theory DFS_Invars_SCC

section ‹Invariants for SCCs›
theory DFS_Invars_SCC
imports 
  DFS_Invars_Basic
begin

definition scc_root' :: "('v × 'v) set ⇒ ('v,'es) state_scheme  ⇒ 'v ⇒ 'v set ⇒ bool"
    ― ‹@{term v} is a root of its scc 
        iff all the discovered parts of the scc can be reached by tree edges from @{term v}›
  where
  "scc_root' E s v scc ⟷ is_scc E scc 
                       ∧ v ∈ scc
                       ∧ v ∈ dom (discovered s) 
                       ∧ scc ∩ dom (discovered s) ⊆ (tree_edges s)⇧* `` {v}"

context param_DFS_defs begin
  abbreviation "scc_root ≡ scc_root' E"
  lemmas scc_root_def = scc_root'_def

  lemma scc_rootI:
    assumes "is_scc E scc"
    and "v ∈ dom (discovered s)"
    and "v ∈ scc"
    and "scc ∩ dom (discovered s) ⊆ (tree_edges s)⇧* `` {v}"
    shows "scc_root s v scc"
    using assms by (simp add: scc_root_def)

  definition "scc_roots s = {v. ∃scc. scc_root s v scc}"
end

context DFS_invar begin
  lemma scc_root_is_discovered:
    "scc_root s v scc ⟹ v ∈ dom (discovered s)"
    by (simp add: scc_root_def)

  lemma scc_root_scc_tree_rtrancl:
    assumes "scc_root s v scc"
    and "x ∈ scc" "x ∈ dom (discovered s)"
    shows "(v,x) ∈ (tree_edges s)⇧*"
    using assms
    by (auto simp add: scc_root_def)

  lemma scc_root_scc_reach:
    assumes "scc_root s r scc"
    and "v ∈ scc"
    shows "(r,v) ∈ E⇧*"
  proof -
    from assms have "is_scc E scc" "r ∈ scc" by (simp_all add: scc_root_def)
    with is_scc_connected assms show ?thesis by metis
  qed

  lemma scc_reach_scc_root:
    assumes "scc_root s r scc"
    and "v ∈ scc"
    shows "(v,r) ∈ E⇧*"
  proof -
    from assms have "is_scc E scc" "r ∈ scc" by (simp_all add: scc_root_def)
    with is_scc_connected assms show ?thesis by metis
  qed

  lemma scc_root_scc_tree_trancl:
    assumes "scc_root s v scc"
    and "x ∈ scc" "x ∈ dom (discovered s)" "x ≠ v"
    shows "(v,x) ∈ (tree_edges s)⇧+"
    using assms scc_root_scc_tree_rtrancl
    by (auto simp add: rtrancl_eq_or_trancl)

  lemma scc_root_unique_scc:
    "scc_root s v scc ⟹ scc_root s v scc' ⟹ scc = scc'"
    unfolding scc_root_def
    by (metis is_scc_unique)

  lemma scc_root_unique_root:
    assumes scc1: "scc_root s v scc"
    and scc2: "scc_root s v' scc"
    shows "v = v'"
  proof (rule ccontr)
    assume "v ≠ v'"
    from scc1 have "v ∈ scc" "v ∈ dom (discovered s)" 
      by (simp_all add: scc_root_def)
    with scc_root_scc_tree_trancl[OF scc2] ‹v ≠ v'› have "(v',v) ∈ (tree_edges s)⇧+" 
      by simp
    also from scc2 have "v' ∈ scc" "v' ∈ dom (discovered s)" 
      by (simp_all add: scc_root_def)
    with scc_root_scc_tree_trancl[OF scc1] ‹v≠v'› have "(v,v') ∈ (tree_edges s)⇧+" 
      by simp
    finally show False using no_loop_in_tree by contradiction
  qed

  lemma scc_root_unique_is_scc:
    assumes "scc_root s v scc"
    shows "scc_root s v (scc_of E v)"
  proof -
    from assms have "v ∈ scc" "is_scc E scc" by (simp_all add: scc_root_def)
    moreover have "v ∈ scc_of E v" "is_scc E (scc_of E v)" by simp_all
    ultimately have "scc = scc_of E v" using is_scc_unique by metis
    thus ?thesis using assms by simp
  qed

  lemma scc_root_finished_impl_scc_finished:
    assumes "v ∈ dom (finished s)"
    and "scc_root s v scc"
    shows "scc ⊆ dom (finished s)"
  proof
    fix x
    assume "x ∈ scc"

    let ?E = "Restr E scc"

    from assms have "is_scc E scc" "v ∈ scc" by (simp_all add: scc_root_def)
    hence "(v,x) ∈ (Restr E scc)⇧*" using ‹x ∈ scc›
      by (simp add: is_scc_connected')
    with rtrancl_is_path obtain p where "path ?E v p x" by metis
    thus "x ∈ dom (finished s)" 
    proof (induction p arbitrary: x rule: rev_induct)
      case Nil hence "v = x" by simp
      with assms show ?case by simp
    next
      case (snoc y ys) hence "path ?E v ys y" "(y,x) ∈ ?E" 
        by (simp_all add: path_append_conv)
      with snoc.IH have "y ∈ dom (finished s)" by simp
      moreover from ‹(y,x) ∈ ?E› have "(y,x) ∈ E" "x ∈ scc" by auto
      ultimately have "x ∈ dom (discovered s)"
        using finished_imp_succ_discovered
        by blast
      with ‹x ∈ scc› show ?case
        using assms scc_root_scc_tree_trancl tree_path_impl_parenthesis
        by blast
    qed
  qed

context begin interpretation timing_syntax .
  lemma scc_root_disc_le:
    assumes "scc_root s v scc"
    and "x ∈ scc" "x ∈ dom (discovered s)"
    shows "δ s v ≤ δ s x"
  proof (cases "x = v")
    case False with assms scc_root_scc_tree_trancl tree_path_disc have 
      "δ s v < δ s x" 
      by blast
    thus ?thesis by simp
  qed simp

  lemma scc_root_fin_ge:
    assumes "scc_root s v scc"
    and "v ∈ dom (finished s)"
    and "x ∈ scc"
    shows "φ s v ≥ φ s x"
  proof (cases "x = v")
    case False
    from assms scc_root_finished_impl_scc_finished have 
      "x ∈ dom (finished s)" by auto
    hence "x ∈ dom (discovered s)" using finished_discovered by auto
    with assms False have "(v,x) ∈ (tree_edges s)⇧+" 
      using scc_root_scc_tree_trancl by simp
    with tree_path_impl_parenthesis assms False show ?thesis by force
  qed simp

  lemma scc_root_is_Min_disc:
    assumes "scc_root s v scc"
    shows "Min (δ s ` (scc ∩ dom (discovered s))) = δ s v" (is "Min ?S = _")
  proof (rule Min_eqI)
    from discovered_finite show "finite ?S" by auto
    from scc_root_disc_le[OF assms] show "⋀y. y ∈ ?S ⟹ δ s v ≤ y" by force
    
    from assms have "v ∈ scc" "v ∈ dom (discovered s)"
      by (simp_all add: scc_root_def)
    thus "δ s v ∈ ?S" by auto
  qed

  lemma Min_disc_is_scc_root:
    assumes "v ∈ scc" "v ∈ dom (discovered s)"
    and "is_scc E scc"
    and min: "δ s v = Min (δ s ` (scc ∩ dom (discovered s)))"
    shows "scc_root s v scc"
  proof -
    {
      fix y
      assume A: "y ∈ scc" "y ∈ dom (discovered s)" "y ≠ v"
      with min have "δ s v ≤ δ s y" by auto
      with assms disc_unequal A have "δ s v < δ s y" by fastforce
    } note scc_disc = this

    {
      fix x
      assume A: "x ∈ scc ∩ dom (discovered s)"

      have "x ∈ (tree_edges s)⇧* `` {v}"
      proof (cases "v = x")
        case False with A scc_disc have δ: "δ s v < δ s x" by simp

        have "(v,x) ∈ (tree_edges s)⇧+"
        proof (cases "v ∈ dom (finished s)")
          case False with stack_set_def assms have 
            v_stack: "v ∈ set (stack s)" by auto
          show ?thesis
          proof (cases "x ∈ dom (finished s)")
            case True 
            with parenthesis_impl_tree_path_not_finished[of v x] assms δ False
            show ?thesis by auto
          next
            case False with A stack_set_def have "x ∈ set (stack s)" by auto
            with v_stack δ show ?thesis
              using on_stack_is_tree_path
              by simp
          qed
        next
          case True note v_fin = this

          let ?E = "Restr E scc"

          {
            fix y
            assume "(v, y) ∈ ?E" and "v ≠ y"
            hence *: "y ∈ succ v" "y ∈ scc" by auto
            with finished_imp_succ_discovered v_fin have 
              "y ∈ dom (discovered s)" by simp
            with scc_disc ‹v ≠ y› * have "δ s v < δ s y" by simp
            with * finished_succ_impl_path_in_tree v_fin have "(v,y) ∈ (tree_edges s)⇧+" by simp
          } note trancl_base = this

          from A have "x ∈ scc" by simp
          with assms have "(v,x) ∈ ?E⇧*"
            by (simp add: is_scc_connected')
          with ‹v≠x› have "(v,x) ∈ ?E⇧+" by (metis rtrancl_eq_or_trancl)
          thus ?thesis using ‹v≠x›
          proof (induction)
            case (base y) with trancl_base show ?case .
          next
            case (step y z)
            show ?case
            proof (cases "v = y")
              case True with step trancl_base show ?thesis by simp
            next
              case False with step have "(v,y) ∈ (tree_edges s)⇧+" by simp
              with tree_path_impl_parenthesis[OF _ v_fin] have 
                y_fin: "y ∈ dom (finished s)" 
                and y_t: "δ s v < δ s y" "φ s y < φ s v" 
                by auto
              with finished_discovered have y_disc: "y ∈ dom (discovered s)" 
                by auto

              from step have *: "z ∈ succ y" "z ∈ scc" by auto
              with finished_imp_succ_discovered y_fin have 
                z_disc: "z ∈ dom (discovered s)" by simp
              with * ‹v≠z› have δz: "δ s v < δ s z" by (simp add: scc_disc)
              

              from * edges_covered finished_no_pending[OF ‹y ∈ dom (finished s)›] 
                   y_disc have "(y,z) ∈ edges s" by auto
              thus ?thesis
              proof safe
                assume "(y,z) ∈ tree_edges s" with ‹(v,y) ∈ (tree_edges s)⇧+› show ?thesis ..
              next
                assume CE: "(y,z) ∈ cross_edges s" 
                with cross_edges_finished_decr y_fin y_t have "φ s z < φ s v" 
                  by force
                moreover note δz
                moreover from CE cross_edges_target_finished have 
                  "z ∈ dom (finished s)" by simp
                ultimately show ?thesis 
                  using parenthesis_impl_tree_path[OF v_fin] by metis
              next
                assume BE: "(y,z) ∈ back_edges s" 
                with back_edge_disc_lt_fin y_fin y_t have 
                  "δ s z < φ s v" by force
                moreover note δz
                moreover note z_disc
                ultimately have "z ∈ dom (finished s)" "φ s z < φ s v" 
                  using parenthesis_contained[OF v_fin] by simp_all
                with δz show ?thesis 
                  using parenthesis_impl_tree_path[OF v_fin] by metis
              qed
            qed
          qed
        qed
        thus ?thesis by auto
      qed simp
    }
    hence "scc ∩ dom (discovered s) ⊆ (tree_edges s)⇧* `` {v}" by blast

    with assms show ?thesis by (auto intro: scc_rootI)
  qed

  lemma scc_root_iff_Min_disc:
    assumes "is_scc E scc" "r ∈ scc" "r ∈ dom (discovered s)"
    shows "scc_root s r scc ⟷ Min (δ s ` (scc ∩ dom (discovered s))) = δ s r" (is "?L ⟷ ?R")
  proof
    assume "?L" with scc_root_is_Min_disc show "?R" .
  next
    assume "?R" with Min_disc_is_scc_root assms show "?L" by simp
  qed   

  lemma scc_root_exists:
    assumes "is_scc E scc"
    and scc: "scc ∩ dom (discovered s) ≠ {}"
    shows "∃r. scc_root s r scc"
  proof -
    let ?S = "scc ∩ dom (discovered s)"

    from discovered_finite have "finite (δ s`?S)" by auto
    moreover from scc have "δ s ` ?S ≠ {}" by auto
    moreover have "⋀(x::nat) f A. x ∉ f ` A ∨ (∃y. x = f y ∧ y ∈ A)" by blast 
      ― ‹autogenerated by sledgehammer›
    ultimately have "∃x ∈ ?S. δ s x = Min (δ s ` ?S)" by (metis Min_in)
    with Min_disc_is_scc_root ‹is_scc E scc› show ?thesis by auto
  qed

  lemma scc_root_of_node_exists:
    assumes "v ∈ dom (discovered s)"
    shows "∃r. scc_root s r (scc_of E v)"
  proof -
    have "is_scc E (scc_of E v)" by simp
    moreover have "v ∈ scc_of E v" by simp
    with assms have "scc_of E v ∩ dom (discovered s) ≠ {}" by blast
    ultimately show ?thesis using scc_root_exists by metis
  qed

  lemma scc_root_transfer':
    assumes "discovered s = discovered s'" "tree_edges s = tree_edges s'"
    shows "scc_root s r scc ⟷ scc_root s' r scc"
    unfolding scc_root_def
    by (simp add: assms)

  lemma scc_root_transfer:
    assumes inv: "DFS_invar G param s'"
    assumes r_d: "r ∈ dom (discovered s)"
    assumes d: "dom (discovered s) ⊆ dom (discovered s')"
               "∀x∈dom (discovered s). δ s x = δ s' x"
               "∀x∈dom (discovered s') - dom (discovered s). δ s' x ≥ counter s"
    and t: "tree_edges s ⊆ tree_edges s'"
    shows "scc_root s r scc ⟷ scc_root s' r scc"
  proof -
    interpret s': DFS_invar where s=s' by fact

    let ?sd = "scc ∩ dom (discovered s)"
    let ?sd' = "scc ∩ dom (discovered s')"
    let ?sdd = "scc ∩ (dom (discovered s') - dom (discovered s))"

    {
      assume r_s: "r ∈ scc" "is_scc E scc"
      with r_d have ne: "δ s'`?sd ≠ {}" by blast
      from discovered_finite have fin: "finite (δ s' ` ?sd)" by simp
    
      from timing_less_counter d have "⋀x. x∈δ s' ` ?sd ⟹ x < counter s" by auto
      hence Min: "Min (δ s' ` ?sd) < counter s"
        using Min_less_iff[OF fin] ne by blast

      from d have "Min (δ s ` ?sd) = Min (δ s' ` ?sd)" by (auto simp: image_def)
      also from d have "?sd' = ?sd ∪ ?sdd" by auto
      hence *: "δ s' ` ?sd' = δ s' ` ?sd ∪ δ s' ` ?sdd" by auto
      hence "Min (δ s' ` ?sd) = Min (δ s' ` ?sd')"
      proof (cases "?sdd = {}")
        case False
        from d have "⋀x. x ∈ δ s' ` ?sdd ⟹ x ≥ counter s" by auto
        moreover from False have ne': "δ s' ` ?sdd ≠ {}" by blast
        moreover from s'.discovered_finite have fin': "finite (δ s' ` ?sdd)" by blast
        ultimately have "Min (δ s' ` ?sdd) ≥ counter s"
          using Min_ge_iff by metis
        with Min Min_Un[OF fin ne fin' ne'] * show ?thesis by simp
      qed simp
      finally have "Min (δ s ` ?sd) = Min (δ s' ` ?sd')" .
    } note aux = this

    show ?thesis
    proof
      assume r: "scc_root s r scc"
      from r_d d have "δ s' r = δ s r" by simp
      also from r scc_root_is_Min_disc have "δ s r = Min (δ s ` ?sd)" by simp
      also from r aux have "Min (δ s ` ?sd) = Min (δ s' ` ?sd')" by (simp add: scc_root_def)
      finally show "scc_root s' r scc"
        using r_d d r[unfolded scc_root_def]
        by (blast intro!: s'.Min_disc_is_scc_root)
    next
      assume r': "scc_root s' r scc"
      from r_d d have "δ s r = δ s' r" by simp
      also from r' s'.scc_root_is_Min_disc have "δ s' r = Min (δ s' ` ?sd')" by simp
      also from r' aux have "Min (δ s' ` ?sd') = Min (δ s ` ?sd)" by (simp add: scc_root_def)
      finally show "scc_root s r scc"
        using r_d d r'[unfolded scc_root_def]
        by (blast intro!: Min_disc_is_scc_root)
    qed
  qed

end end

end