Theory CAVA_Automata.Digraph

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')*" using 1 by rule
    have 3: "u  reachable" "(u, v)  E*" 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: "xV  fi (f x) = x" and
    f_fi: "yf`V  f (fi y) = y" and
    fi_f_eq: "f x = y; xV  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: "vg_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 "uV"
    shows "v. v' = f v  vV  (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 "vV" "wV" using E_ss by auto
    from rtrancl_into_rtrancl obtain vv where "v' = f vv" "vvV" "(u,vv)E*"
      by blast
    from v' = f v vV v' = f vv vvV 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 wV 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')* `` g_V0 G')"
  proof -
    have "(g_E G')* `` g_V0 G'  f ` (E*``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