Quelle  Digraph.thy

section ‹Directed Graphs›
(* Author: Peter Lammich *)
theory Digraph
  imports 
  CAVA_Base.CAVA_Base
  Digraph_Basic
begin

subsection "Directed Graphs with Explicit Node Set and Set of Initial Nodes"

record 'v graph_rec = 
  g_V :: "'v set"
  g_E :: "'v digraph"  
  g_V0 :: "'v set"

definition graph_restrict :: "('v, 'more) graph_rec_scheme ==> 'v set ==> ('v, 'more) graph_rec_scheme"
  where "graph_restrict G R ≡
  (
    g_V = g_V G,
    g_E = rel_restrict (g_E G) R,
    g_V0 = g_V0 G - R,
    … = graph_rec.more G
  )"

lemma graph_restrict_simps[simp]:
  "g_V (graph_restrict G R) = g_V G"
  "g_E (graph_restrict G R) = rel_restrict (g_E G) R"
  "g_V0 (graph_restrict G R) = g_V0 G - R"
  "graph_rec.more (graph_restrict G R) = graph_rec.more G"
  unfolding graph_restrict_def by auto

lemma graph_restrict_trivial[simp]: "graph_restrict G {} = G" by simp

locale graph_defs =
  fixes G :: "('v, 'more) graph_rec_scheme"
begin

  abbreviation "V ≡ g_V G"
  abbreviation "E ≡ g_E G"
  abbreviation "V0 ≡ g_V0 G"

  abbreviation "reachable ≡ E^* `` V0"
  abbreviation "succ v ≡ E `` {v}"

  lemma finite_V0: "finite reachable ==> finite V0" by (auto intro: finite_subset)

  definition is_run
    ― ‹Infinite run, i.e., a rooted infinite path›
    where "is_run r ≡ r 0 ∈ V0 ∧ ipath E r"

  lemma run_ipath: "is_run r ==> ipath E r" unfolding is_run_def by auto
  lemma run_V0: "is_run r ==> r 0 ∈ V0" unfolding is_run_def by auto

  lemma run_reachable: "is_run r ==> range r ⊆ reachable"
    unfolding is_run_def using ipath_to_rtrancl by blast

end

locale graph =
  graph_defs G
  for G :: "('v, 'more) graph_rec_scheme"
  +
  assumes V0_ss: "V0 ⊆ V"
  assumes E_ss: "E ⊆ V × V"
begin

  lemma reachable_V: "reachable ⊆ V" using V0_ss E_ss by (auto elim: rtrancl_induct)

  lemma finite_E: "finite V ==> finite E" using finite_subset E_ss by auto

end

(* TODO: finite reachability is handled using loose assumptions, while finitely branching
  graphs are captured using a locale. it may be advantageous to unify this. *)
locale fb_graph =
  graph G
  for G :: "('v, 'more) graph_rec_scheme"
  +
  assumes finite_V0[simp, intro!]: "finite V0"
  assumes finitely_branching[simp, intro]: "v ∈ reachable ==> finite (succ v)"
begin

  lemma fb_graph_subset:
    assumes "g_V G' = V"
    assumes "g_E G' ⊆ E"
    assumes "finite (g_V0 G')"
    assumes "g_V0 G' ⊆ reachable"
    shows "fb_graph G'"
  proof
    show "g_V0 G' ⊆ g_V G'" using reachable_V assms(1, 4) by simp
    show "g_E G' ⊆ g_V G' × g_V G'" using E_ss assms(1, 2) by simp
    show "finite (g_V0 G')" using assms(3) by this
  next
    fix v
    assume 1: "v ∈ (g_E G')^* `` g_V0 G'"
    obtain u where 2: "u ∈ g_V0 G'" "(u, v) ∈ (g_E G')<sup>*</sup>" using 1 by rule
    have 3: "u ∈ reachable" "(u, v) ∈ E<sup>*</sup>" using rtrancl_mono assms(2, 4) 2 by auto
    have 4: "v ∈ reachable" using rtrancl_image_advance_rtrancl 3 by metis
    have 5: "finite (E `` {v})" using 4 by rule
    have 6: "g_E G' `` {v} ⊆ E `` {v}" using assms(2) by auto
    show "finite (g_E G' `` {v})" using finite_subset 5 6 by auto
  qed

  lemma fb_graph_restrict: "fb_graph (graph_restrict G R)"
    by (rule fb_graph_subset, auto simp: rel_restrict_sub)

end

lemma (in graph) fb_graphI_fr:
  assumes "finite reachable"
  shows "fb_graph G"
proof
  from assms show "finite V0" by (rule finite_subset[rotated]) auto
  fix v
  assume "v ∈ reachable"
  hence "succ v ⊆ reachable" by (metis Image_singleton_iff rtrancl_image_advance subsetI)
  thus "finite (succ v)" using assms by (rule finite_subset)
qed

abbreviation "rename_E f E ≡ (λ(u,v). (f u, f v))`E"

definition "fr_rename_ext ecnv f G ≡ (
    g_V = f`(g_V G),
    g_E = rename_E f (g_E G),
    g_V0 = (f`g_V0 G),
    … = ecnv G
  )"

locale g_rename_precond =
  graph G
  for G :: "('u,'more) graph_rec_scheme"
  +
  fixes f :: "'u ==> 'v"
  fixes ecnv :: "('u, 'more) graph_rec_scheme ==> 'more'"
  assumes INJ: "inj_on f V"
begin

  abbreviation "G' ≡ fr_rename_ext ecnv f G"

  lemma G'_fields:
    "g_V G' = f`V"
    "g_V0 G' = f`V0"
    "g_E G' = rename_E f E"
    unfolding fr_rename_ext_def by simp_all

  definition "fi ≡ the_inv_into V f"

  lemma 
    fi_f: "x∈V ==> fi (f x) = x" and
    f_fi: "y∈f`V ==> f (fi y) = y" and
    fi_f_eq: "[f x = y; x∈V] ==> fi y = x"
    unfolding fi_def
    by (auto 
      simp: the_inv_into_f_f f_the_inv_into_f the_inv_into_f_eq INJ)

  lemma E'_to_E: "(u,v) ∈ g_E G' ==> (fi u, fi v)∈E"
    using E_ss
    by (auto simp: fi_f G'_fields)

  lemma V0'_to_V0: "v∈g_V0 G' ==> fi v ∈ V0"
    using V0_ss
    by (auto simp: fi_f G'_fields)


  lemma rtrancl_E'_sim:
    assumes "(f u,v')∈(g_E G')^*"
    assumes "u∈V"
    shows "∃v. v' = f v ∧ v∈V ∧ (u,v)∈E^*"
    using assms
  proof (induction "f u" v' arbitrary: u)
    case (rtrancl_into_rtrancl v' w' u)
    then obtain v w where "v' = f v" "w' = f w" "(v,w)∈E"
      by (auto simp: G'_fields)
    hence "v∈V" "w∈V" using E_ss by auto
    from rtrancl_into_rtrancl obtain vv where "v' = f vv" "vv∈V" "(u,vv)∈E^*"
      by blast
    from ‹v' = f v› ‹v∈V› ‹v' = f vv› ‹vv∈V› have [simp]: "vv = v"
      using INJ by (metis inj_on_contraD)

    note ‹(u,vv)∈E^*›[simplified]
    also note ‹(v,w)∈E›
    finally show ?case using ‹w' = f w› ‹w∈V› by blast
  qed auto
    
  lemma rtrancl_E'_to_E: assumes "(u,v)∈(g_E G')^*" shows "(fi u, fi v)∈E^*"
    using assms apply induction
    by (fastforce intro: E'_to_E rtrancl_into_rtrancl)+

  lemma G'_invar: "graph G'"
    apply unfold_locales
  proof -
    show "g_V0 G' ⊆ g_V G'"
      using V0_ss by (auto simp: G'_fields) []

    show "g_E G' ⊆ g_V G' × g_V G'"
      using E_ss by (auto simp: G'_fields) []
  qed

  sublocale G': graph G' using G'_invar .

  lemma G'_finite_reachable:
    assumes "finite ((g_E G)^* `` g_V0 G)"
    shows "finite ((g_E G')<sup>*</sup> `` g_V0 G')"
  proof -
    have "(g_E G')^* `` g_V0 G' ⊆ f ` (E<sup>*</sup>``V0)"
      apply (clarsimp_all simp: G'_fields(2))
      apply (drule rtrancl_E'_sim)
      using V0_ss apply auto []
      apply auto
      done
    thus ?thesis using finite_subset assms by blast
  qed

  lemma V'_to_V: "v ∈ G'.V ==> fi v ∈ V"
    by (auto simp: fi_f G'_fields)

  lemma ipath_sim1: "ipath E r ==> ipath G'.E (f o r)"
    unfolding ipath_def by (auto simp: G'_fields)

  lemma ipath_sim2: "ipath G'.E r ==> ipath E (fi o r)"
    unfolding ipath_def 
    apply (clarsimp simp: G'_fields)
    apply (drule_tac x=i in spec)
    using E_ss
    by (auto simp: fi_f)

  lemma run_sim1: "is_run r ==> G'.is_run (f o r)"
    unfolding is_run_def G'.is_run_def
    apply (intro conjI)
    apply (auto simp: G'_fields) []
    apply (auto simp: ipath_sim1)
    done

  lemma run_sim2: "G'.is_run r ==> is_run (fi o r)"
    unfolding is_run_def G'.is_run_def
    by (auto simp: ipath_sim2 V0'_to_V0)

end


end