Theory LabeledGraphs

section ‹Labeled Graphs›
text ‹We define graphs as in the paper. Graph homomorphisms and subgraphs are defined slightly
      differently.
      Their correspondence to the definitions in the paper is given by separate lemmas.
      After defining graphs, we only talk about the semantics until after defining homomorphisms.
      The reason is that graph rewriting can be done without knowing about semantics.›

theory LabeledGraphs
imports MissingRelation
begin

datatype ('l,'v) labeled_graph
  = LG (edges:"('l × 'v × 'v) set") (vertices:"'v set")

definition restrict where
  "restrict G = LG {(l,v1,v2) ∈ edges G. v1 ∈ vertices G ∧ v2 ∈ vertices G } (vertices G)"

text ‹Definition 1. We define graphs and show that any graph with no edges (in particular
       the empty graph) is indeed a graph.›
abbreviation graph where
  "graph X ≡ X = restrict X"

lemma graph_empty_e[intro]: "graph (LG {} v)" unfolding restrict_def by auto

lemma graph_single[intro]: "graph (LG {(a,b,c)} {b,c})" unfolding restrict_def by auto

abbreviation finite_graph where
  "finite_graph X ≡ graph X ∧ finite (vertices X) ∧ finite (edges X)"

lemma restrict_idemp[simp]:
  "restrict (restrict x) = restrict x"
by(cases x,auto simp:restrict_def)

lemma vertices_restrict[simp]:
  "vertices (restrict G) = vertices G"
  by(cases G,auto simp:restrict_def)

lemma restrictI[intro]:
  assumes "edges G ⊆ {(l,v1,v2). v1 ∈ vertices G ∧ v2 ∈ vertices G }"
  shows "G = restrict G"
  using assms by(cases G,auto simp:restrict_def)

lemma restrict_subsD[dest]:
  assumes "edges G ⊆ edges (restrict G)"
  shows "G = restrict G"
  using assms by(cases G,auto simp:restrict_def)

lemma restrictD[dest]:
  assumes "G = restrict G"
  shows "edges G ⊆ {(l,v1,v2). v1 ∈ vertices G ∧ v2 ∈ vertices G }"
proof -
  have "edges (restrict G) ⊆ {(l,v1,v2). v1 ∈ vertices G ∧ v2 ∈ vertices G }"
    by (cases G,auto simp:restrict_def)
  thus ?thesis using assms by auto
qed

(* Given a relation on vertices, make one on edges *)
definition on_triple where "on_triple R ≡ {((l,s,t),(l',s',t')) . l=l' ∧ (s,s') ∈ R ∧ (t,t') ∈ R}"

lemma on_triple[simp]:
  "((l1,v1,v2),(l2,v3,v4)) ∈ on_triple R ⟷ (v1,v3)∈ R ∧ (v2,v4) ∈ R ∧ l1 = l2"
unfolding on_triple_def by auto

lemma on_triple_univ[intro!]:
  "univalent f ⟹ univalent (on_triple f)"
  unfolding on_triple_def univalent_def by auto

lemma on_tripleD[dest]:
  assumes "((l1,v1,v2),(l2,v3,v4)) ∈ on_triple R"
  shows "l2 = l1" "(v1,v3)∈ R" "(v2,v4) ∈ R"
 using assms unfolding on_triple_def by auto

lemma on_triple_ID_restrict[simp]:
  shows "on_triple (Id_on (vertices G)) `` edges G = edges (restrict G)"
  unfolding on_triple_def by(cases G,auto simp:restrict_def)

lemma relcomp_on_triple[simp]:
  shows "on_triple (R O S) = on_triple R O on_triple S"
  unfolding on_triple_def by fast

lemma on_triple_preserves_finite[intro]:
"finite E  ⟹ finite (on_triple (BNF_Def.Gr A f) `` E)"
  by (auto simp:on_triple_def BNF_Def.Gr_def)

lemma on_triple_fst[simp]:
  assumes "vertices G = Domain g" "graph G"
  shows "x ∈ fst ` on_triple g `` (edges G) ⟷ x ∈ fst ` edges G"
proof
  assume "x ∈ fst ` on_triple g `` edges G"
  then obtain a b where "(x,a,b) ∈ on_triple g `` edges G" by force
  then obtain c d where "(x,c,d) ∈ edges G" unfolding on_triple_def by auto
  thus "x ∈ fst ` edges G" by force next
  assume "x ∈ fst ` edges G"
  then obtain a b where ab:"(x,a,b) ∈ edges G" by force
  then obtain c d where "(a,c) ∈ g" "(b,d) ∈ g" using assms by force
  hence "(x,c,d) ∈ on_triple g `` edges G" using ab unfolding on_triple_def by auto
  thus "x ∈ fst ` on_triple g `` edges G" by (metis fst_conv image_iff)
qed

definition edge_preserving where
  "edge_preserving h e1 e2 ≡ 
     (∀ (k,v1,v2) ∈ e1. ∀ v1' v2'. ((v1, v1') ∈ h ∧ (v2,v2') ∈ h)
                                    ⟶ (k,v1',v2') ∈ e2)"

lemma edge_preserving_atomic:
  assumes "edge_preserving h1 e1 e2" "(v1, v1') ∈ h1" "(v2, v2') ∈ h1" "(k, v1, v2) ∈ e1"
  shows "(k, v1', v2') ∈ e2"
using assms unfolding edge_preserving_def by auto

lemma edge_preservingI[intro]:
  assumes "on_triple R `` E ⊆ G"
  shows "edge_preserving R E G"
  unfolding edge_preserving_def proof(clarify,goal_cases)
  case (1 a s t v1' v2')
  thus ?case by (intro assms[THEN subsetD]) (auto simp:on_triple_def)
  qed

lemma on_triple_dest[dest]:
  assumes "on_triple R `` E ⊆ G"
          "(l,x,y) ∈ E" "(x,xx) ∈ R" "(y,yy) ∈ R"
        shows "(l,xx,yy) ∈ G"
  using assms unfolding Image_def on_triple_def by blast

lemma edge_preserving:
  shows "edge_preserving R E G ⟷ on_triple R `` E ⊆ G"
proof
  assume "edge_preserving R E G"
  hence "⋀ k v1 v2 v1' v2'. (k, v1, v2)∈E ⟹
            (v1, v1') ∈ R ⟹ (v2, v2') ∈ R ⟹ (k, v1', v2') ∈ G"
    unfolding edge_preserving_def by auto
  then show "on_triple R `` E ⊆ G" unfolding Image_def by auto
qed auto

lemma edge_preserving_subset:
  assumes "R⇩1 ⊆ R⇩2" "E⇩1 ⊆ E⇩2" "edge_preserving R⇩2 E⇩2 G"
  shows "edge_preserving R⇩1 E⇩1 G"
  using assms unfolding edge_preserving_def by blast

lemma edge_preserving_unionI[intro]:
  assumes "edge_preserving f A G" "edge_preserving f B G"
  shows "edge_preserving f (A ∪ B) G"
  using assms unfolding edge_preserving_def by blast

lemma compose_preserves_edge_preserving:
  assumes "edge_preserving h1 e1 e2" "edge_preserving h2 e2 e3"
  shows "edge_preserving (h1 O h2) e1 e3" unfolding edge_preserving_def
proof(standard,standard,standard,standard,standard,standard,goal_cases)
  case (1 _ k _ v1 v2 v1'' v2'')
  hence 1:"(k, v1, v2) ∈ e1" "(v1, v1'') ∈ h1 O h2" "(v2, v2'') ∈ h1 O h2" by auto
  then obtain v1' v2' where
    v:"(v1,v1') ∈ h1" "(v1',v1'') ∈ h2" "(v2,v2') ∈ h1" "(v2',v2'') ∈ h2" by auto
  from edge_preserving_atomic[OF assms(1) v(1,3) 1(1)]
       edge_preserving_atomic[OF assms(2) v(2,4)]
  show ?case by metis
qed

lemma edge_preserving_Id[intro]: "edge_preserving (Id_on y) x x"
unfolding edge_preserving_def by auto

text ‹This is an alternate version of definition 10. We require @term{vertices s = Domain h}
   to ensure that graph homomorphisms are sufficiently unique:
   The partiality follows the definition in the paper, per the remark before Def. 7.
   but it means that we cannot use Isabelle's total functions for the homomorphisms.
   We show that graph homomorphisms and embeddings coincide in a separate lemma.›

definition graph_homomorphism where
  "graph_homomorphism G⇩1 G⇩2 f 
    = ( vertices G⇩1 = Domain f
      ∧ graph G⇩1 ∧ graph G⇩2
      ∧ f `` vertices G⇩1 ⊆ vertices G⇩2
      ∧ univalent f
      ∧ edge_preserving f (edges G⇩1) (edges G⇩2)
      )"

lemma graph_homomorphismI:
  assumes "vertices s = Domain h"
          "h `` vertices s ⊆ vertices t"
          "univalent h"
          "edge_preserving h (edges s) (edges t)"
          "s = restrict s" "t = restrict t"
  shows "graph_homomorphism s t h" using assms unfolding graph_homomorphism_def by auto

lemma graph_homomorphism_composes[intro]:
  assumes "graph_homomorphism a b x"
          "graph_homomorphism b c y"
  shows "graph_homomorphism a c (x O y)" proof(rule graph_homomorphismI,goal_cases)
  case 1
    have "vertices a ⊆ Domain x" "x `` vertices a ⊆ Domain y"
      using assms(1,2)[unfolded graph_homomorphism_def] by blast+
    from this Domain_O[OF this]
    show ?case using assms[unfolded graph_homomorphism_def] by auto
  next
  case 2 from assms show ?case unfolding graph_homomorphism_def by blast 
  qed (insert assms,auto simp:graph_homomorphism_def intro:compose_preserves_edge_preserving)

lemma graph_homomorphism_empty[simp]:
  "graph_homomorphism (LG {} {}) G f ⟷ f = {} ∧ graph G"
unfolding graph_homomorphism_def by auto

lemma graph_homomorphism_Id[intro]:
  shows "graph_homomorphism (restrict a) (restrict a) (Id_on (vertices a))"
  by (rule graph_homomorphismI;auto simp:edge_preserving_def)

lemma Id_on_vertices_identity:
  assumes "graph_homomorphism a b f"
          "(aa, ba) ∈ f"
  shows "(aa, ba) ∈ Id_on (vertices a) O f"
        "(aa, ba) ∈ f O Id_on (vertices b)"
  using assms unfolding graph_homomorphism_def by auto

text ‹Alternate version of definition 7.›
abbreviation subgraph
  where "subgraph G⇩1 G⇩2 
  ≡ graph_homomorphism G⇩1 G⇩2 (Id_on (vertices G⇩1))" 

lemma subgraph_trans:
  assumes "subgraph G⇩1 G⇩2" "subgraph G⇩2 G⇩3"
  shows "subgraph G⇩1 G⇩3"
proof-
  from assms[unfolded graph_homomorphism_def]
  have "Id_on (vertices G⇩1) O Id_on (vertices G⇩2) = Id_on (vertices G⇩1)"
    by auto
  with graph_homomorphism_composes[OF assms] show ?thesis by auto
qed

text ‹ Just before Definition 7 in the paper, a notation is introduced for applying a function to
       a graph. We use @{term map_graph} for this, and the version @{term map_graph_fn} in
       case that its first argument is a total function rather than a partial one. ›
(* Introducing the map notation just above Def 7 in the paper *)
definition map_graph :: "('c × 'b) set ⇒ ('a, 'c) labeled_graph ⇒ ('a, 'b) labeled_graph" where
  "map_graph f G = LG (on_triple f `` (edges G)) (f `` (vertices G))"

lemma map_graph_selectors[simp]:
  "vertices (map_graph f G) = f `` (vertices G)"
  "edges (map_graph f G) = on_triple f `` (edges G)"
  unfolding map_graph_def by auto

lemma map_graph_comp[simp]:
  assumes "Range g ⊆ Domain f"
  shows "map_graph (g O f) = map_graph f o map_graph g"
proof(standard,goal_cases) (* need goal_cases to get the type of x right *)
  case (1 x)
  from assms have "map_graph (g O f) x = (map_graph f o map_graph g) x"
    unfolding map_graph_def by auto
  thus ?case by auto
qed

lemma map_graph_returns_restricted:
  assumes "vertices G = Domain f"
  shows "map_graph f G = restrict (map_graph f G)"
  using assms by(cases G,auto simp:map_graph_def restrict_def)

lemma map_graph_preserves_restricted[intro]:
  assumes "graph G"
  shows "graph (map_graph f G)"
proof(rule restrictI,standard) fix x
  assume "x ∈ edges (map_graph f G)"
  with assms show "x ∈ {(l, v1, v2). v1∈vertices (map_graph f G) ∧ v2∈vertices (map_graph f G)}"
    by(cases x,auto simp:map_graph_def)
qed

lemma map_graph_edge_preserving[intro]:
  shows "edge_preserving f (edges G) (edges (map_graph f G))"
  unfolding map_graph_def by auto

lemma map_graph_homo[intro]:
  assumes "univalent f" "vertices G = Domain f" "G = restrict G"
  shows "graph_homomorphism G (map_graph f G) f"
proof(rule graph_homomorphismI)
  show "f `` vertices G ⊆ vertices (map_graph f G)"
    unfolding map_graph_def by auto
  show "edge_preserving f (edges G) (edges (map_graph f G))" by auto
  show "map_graph f G = restrict (map_graph f G)" using assms by auto
qed fact+

lemma map_graph_homo_simp:
  "graph_homomorphism G (map_graph f G) f
   ⟷ univalent f ∧ vertices G = Domain f ∧ graph G"
proof
  show "graph_homomorphism G (map_graph f G) f ⟹
    univalent f ∧ vertices G = Domain f ∧ G = restrict G"
    unfolding graph_homomorphism_def by blast
qed auto

abbreviation on_graph where
"on_graph G f ≡ BNF_Def.Gr (vertices G) f"

abbreviation map_graph_fn where
"map_graph_fn G f ≡ map_graph (on_graph G f) G"

lemma map_graph_fn_graphI[intro]:
"graph (map_graph_fn G f)" unfolding map_graph_def restrict_def by auto

lemma on_graph_id[simp]:
  shows "on_graph B id = Id_on (vertices B)"
  unfolding BNF_Def.Gr_def by auto

lemma in_on_graph[intro]:
  assumes "x ∈ vertices G" "(a x,y) ∈ b"
  shows "(x, y) ∈ on_graph G a O b"
  using assms unfolding BNF_Def.Gr_def by auto

lemma on_graph_comp:
  "on_graph G (f o g) = on_graph G g O on_graph (map_graph_fn G g) f"
  unfolding BNF_Def.Gr_def by auto

lemma map_graph_fn_eqI:
  assumes "⋀ x. x ∈ vertices G ⟹ f x = g x"
  shows "map_graph_fn G f = map_graph_fn G g" (is "?l = ?r")
proof -
  {  fix a ac ba
    assume "(a, ac, ba) ∈ edges G" "ac ∈ vertices G" "ba ∈ vertices G"
    hence "∃x∈edges G. (x, a, g ac, g ba) ∈ on_triple (on_graph G f)"
          "∃x∈edges G. (x, a, g ac, g ba) ∈ on_triple (on_graph G g)"
      using assms by (metis in_Gr on_triple)+
  }
  hence e:"edges ?l = edges ?r" using assms by (auto simp:Image_def) 
  have v:"vertices ?l = vertices ?r" using assms by (auto simp:image_def)
  from e v show ?thesis by(cases ?l,cases ?r,auto)
qed

lemma map_graph_fn_comp[simp]:
"map_graph_fn G (f o g) = map_graph_fn (map_graph_fn G g) f"
  unfolding on_graph_comp by auto

lemma map_graph_fn_id[simp]:
"map_graph_fn X id = restrict X"
"map_graph (Id_on (vertices X)) X = restrict X"
  unfolding BNF_Def.Gr_def map_graph_def on_triple_def restrict_def by (cases X,force)+

lemma graph_homo[intro!]:
  assumes "graph G"
  shows "graph_homomorphism G (map_graph_fn G f) (on_graph G f)"
  using assms unfolding map_graph_homo_simp BNF_Def.Gr_def univalent_def by auto

lemma graph_homo_inv[intro!]:
  assumes "graph G" "inj_on f (vertices G)"
  shows "graph_homomorphism (map_graph_fn G f) G (converse (on_graph G f))"
proof(rule graph_homomorphismI)
  show "univalent ((on_graph G f)¯)" using assms(2)
    unfolding univalent_def BNF_Def.Gr_def inj_on_def by auto
  show "edge_preserving ((on_graph G f)¯) (edges (map_graph_fn G f)) (edges G)"
    using assms unfolding edge_preserving inj_on_def by auto auto
qed (insert assms(1),auto)

lemma edge_preserving_on_graphI[intro]:
  assumes "⋀ l x y. (l,x,y)∈edges X ⟹ x∈vertices X ⟹ y ∈ vertices X ⟹ (l,f x,f y) ∈ Y"
  shows "edge_preserving (on_graph X f) (edges X) Y"
  using assms unfolding edge_preserving_def BNF_Def.Gr_def by auto

lemma subgraph_subset:
  assumes "subgraph G⇩1 G⇩2"
  shows "vertices G⇩1 ⊆ vertices G⇩2" "edges (restrict G⇩1) ⊆ edges G⇩2"
proof -
  have vrt:"Id_on (vertices G⇩1) `` vertices G⇩1 ⊆ vertices G⇩2"
    and ep:"edge_preserving (Id_on (vertices G⇩1)) (edges G⇩1) (edges G⇩2)"
    using assms unfolding graph_homomorphism_def by auto
  hence "edges (restrict G⇩1) ⊆ edges G⇩2"
    using assms unfolding edge_preserving by auto
  thus "vertices G⇩1 ⊆ vertices G⇩2" "edges (restrict G⇩1) ⊆ edges G⇩2"
    using vrt by auto
qed

text ‹Our definition of subgraph is equivalent to definition 7.›
lemma subgraph_def2:
  assumes "graph G⇩1" "graph G⇩2"
  shows "subgraph G⇩1 G⇩2 ⟷ vertices G⇩1 ⊆ vertices G⇩2 ∧ edges G⇩1 ⊆ edges G⇩2"
proof
  assume "vertices G⇩1 ⊆ vertices G⇩2 ∧ edges G⇩1 ⊆ edges G⇩2"
  hence v:"vertices G⇩1 ⊆ vertices G⇩2" and "edges G⇩1 ⊆ edges G⇩2" by auto
  hence ep:"edge_preserving (Id_on (vertices G⇩1)) (edges G⇩1) (edges G⇩2)"
    unfolding edge_preserving_def by auto
  show "subgraph G⇩1 G⇩2"
    using assms(2) v ep graph_homomorphism_Id[of "G⇩1",folded assms]
    unfolding graph_homomorphism_def by auto
next
  assume sg:"subgraph G⇩1 G⇩2"
  hence vrt:"Id_on (vertices G⇩1) `` vertices G⇩1 ⊆ vertices G⇩2"
    and ep:"edge_preserving (Id_on (vertices G⇩1)) (edges G⇩1) (edges G⇩2)"
    unfolding graph_homomorphism_def by auto
  hence "edges G⇩1 ⊆ edges G⇩2"
    using assms unfolding edge_preserving by auto
  thus "vertices G⇩1 ⊆ vertices G⇩2 ∧ edges G⇩1 ⊆ edges G⇩2"
    using vrt by auto
qed

text ‹We also define @{term graph_union}. In contrast to the paper, our definition ignores the labels.
      The corresponding definition in the paper is written just above Definition 7.
      Adding labels to graphs would require a lot of unnecessary additional bookkeeping.
      Nowhere in the paper is the union actually used on different sets of labels,
      in which case these definitions coincide.›

(* Since the set of labels is an implicit type, the notion of graph_union does not completely correspond to the one in the paper *)
definition graph_union where
"graph_union G⇩1 G⇩2 = LG (edges G⇩1 ∪ edges G⇩2) (vertices G⇩1 ∪ vertices G⇩2)"

lemma graph_unionI[intro]:
  assumes "edges G⇩1 ⊆ edges G⇩2"
          "vertices G⇩1 ⊆ vertices G⇩2"
  shows "graph_union G⇩1 G⇩2 = G⇩2"
  using assms unfolding graph_union_def by (cases "G⇩2",auto)

lemma graph_union_iff:
  shows "graph_union G⇩1 G⇩2 = G⇩2 ⟷ (edges G⇩1 ⊆ edges G⇩2 ∧ vertices G⇩1 ⊆ vertices G⇩2)"
  unfolding graph_union_def by (cases "G⇩2",auto)

lemma graph_union_idemp[simp]:
"graph_union A A = A"
"graph_union A (graph_union A B) = (graph_union A B)"
"graph_union A (graph_union B A) = (graph_union B A)"
unfolding graph_union_def by auto

lemma graph_union_vertices[simp]:
"vertices (graph_union G⇩1 G⇩2) = vertices G⇩1 ∪ vertices G⇩2"
  unfolding graph_union_def by auto
lemma graph_union_edges[simp]:
"edges (graph_union G⇩1 G⇩2) = edges G⇩1 ∪ edges G⇩2"
  unfolding graph_union_def by auto

lemma graph_union_preserves_restrict[intro]:
  assumes "G⇩1 = restrict G⇩1" "G⇩2 = restrict G⇩2"
  shows "graph_union G⇩1 G⇩2 = restrict (graph_union G⇩1 G⇩2)"
proof -
  let ?e = "edges G⇩1 ∪ edges G⇩2"
  let ?v = "vertices G⇩1 ∪ vertices G⇩2"
  let ?r = "{(l, v1, v2). (l, v1, v2) ∈ ?e ∧ v1 ∈ ?v ∧ v2 ∈ ?v}" (* restricted edges *)
  { fix l v1 v2
    assume a:"(l,v1,v2) ∈ ?e"
    have "(l,v1,v2) ∈ ?r" proof(cases "(l,v1,v2) ∈ edges (restrict G⇩1)")
      case True
      hence "(l,v1,v2) ∈ edges G⇩1" "v1 ∈ vertices G⇩1" "v2 ∈ vertices G⇩1"
         by (auto simp:restrict_def)+
      thus ?thesis by auto
    next
      case False hence "(l,v1,v2) ∈ edges (restrict G⇩2)" using a assms by auto
      hence "(l,v1,v2) ∈ edges G⇩2" "v1 ∈ vertices G⇩2" "v2 ∈ vertices G⇩2"
         by (auto simp:restrict_def)+
      then show ?thesis by auto
    qed
  }
  hence "?e = ?r" by auto
  thus ?thesis unfolding graph_union_def by auto
qed

lemma graph_map_union[intro]:
  assumes "⋀ i::nat. graph_union (map_graph (g i) X) Y = Y" "⋀ i j. i ≤ j ⟹ g i ⊆ g j"
  shows "graph_union (map_graph (⋃i. g i) X) Y = Y"
proof
  from assms have e:"edges (map_graph (g i) X) ⊆ edges Y"
              and v:"vertices (map_graph (g i) X) ⊆ vertices Y" for i by (auto simp:graph_union_iff)
  { fix a ac ba aa b x xa
    assume a:"(a, ac, ba) ∈ edges X" "(ac, aa) ∈ g x" "(ba, b) ∈ g xa"
    have "(a, aa, b) ∈ edges Y"
    proof(cases "x < xa")
      case True
      hence "(a, ac, ba) ∈ edges X" "(ac, aa) ∈ g xa" "(ba, b) ∈ g xa"
        using a assms(2)[of x xa] by auto
      then show ?thesis using e[of xa] by auto
    next
      case False
      hence "(a, ac, ba) ∈ edges X" "(ac, aa) ∈ g x" "(ba, b) ∈ g x"
        using a assms(2)[of xa x] by auto
      then show ?thesis using e[of x] by auto
    qed
  }
  thus "edges (map_graph (⋃i. g i) X) ⊆ edges Y" by auto
  show "vertices (map_graph (⋃i. g i) X) ⊆ vertices Y" using v by auto
qed

text ‹We show that @{term subgraph} indeed matches the definition in the paper (Definition 7).›

lemma subgraph_def:
"subgraph G⇩1 G⇩2 = (G⇩1 = restrict G⇩1 ∧ G⇩2 = restrict G⇩2 ∧ graph_union G⇩1 G⇩2 = G⇩2)"
proof
  assume assms:"subgraph G⇩1 G⇩2"
  hence r:"G⇩2 = restrict G⇩2" "G⇩1 = restrict G⇩1"
    unfolding graph_homomorphism_def by auto
  from subgraph_subset[OF assms]
  have ss:"vertices (restrict G⇩1) ⊆ vertices G⇩2" "edges (restrict G⇩1) ⊆ edges G⇩2" by auto
  show "G⇩1 = restrict G⇩1 ∧ G⇩2 = restrict G⇩2 ∧ graph_union G⇩1 G⇩2 = G⇩2"
  proof(cases G⇩2)
    case (LG x1 x2) show ?thesis using ss r
    unfolding graph_union_def LG by auto
  qed next
  assume gu: "G⇩1 = restrict G⇩1 ∧ G⇩2 = restrict G⇩2 ∧ graph_union G⇩1 G⇩2 = G⇩2"
  hence sub:"(edges G⇩1 ∪ edges G⇩2) ⊆ edges G⇩2"
    "vertices G⇩1 ⊆ vertices G⇩2"
    unfolding graph_union_def by (cases G⇩2;auto)+
  have r:"G⇩1 = restrict G⇩1" "G⇩2 = restrict G⇩2" using gu by auto
  show "subgraph G⇩1 G⇩2" unfolding subgraph_def2[OF r] using sub by auto
qed

lemma subgraph_refl[simp]: 
"subgraph G G = (G = restrict G)"
  unfolding subgraph_def graph_union_def by(cases G,auto)

lemma subgraph_restrict[simp]:
  "subgraph G (restrict G) = graph G"
  using subgraph_refl subgraph_def by auto

text ‹Definition 10. We write @{term graph_homomorphism} instead of embedding.›
lemma graph_homomorphism_def2: (* Shows a graph homomorphism is an embedding as in the paper *)
  shows "graph_homomorphism G⇩1 G⇩2 f =
   (vertices G⇩1 = Domain f ∧ univalent f ∧ G⇩1 = restrict G⇩1 ∧ G⇩2 = restrict G⇩2 ∧ graph_union (map_graph f G⇩1) G⇩2 = G⇩2)"
   (is "?lhs = ?rhs")
proof 
  let ?m = "map_graph f G⇩1"
  assume ?rhs
  hence assms : "vertices G⇩1 = Domain f" "univalent f" "G⇩1 = restrict G⇩1"
    and sg: "subgraph ?m G⇩2"
    and f_id:"f O Id_on (f `` vertices G⇩1) = f" unfolding subgraph_def by auto
  hence "edge_preserving (Id_on (vertices ?m)) (edges ?m) (edges G⇩2)"
    unfolding graph_homomorphism_def by auto
  hence "on_triple (f O Id_on (f `` vertices G⇩1)) `` edges G⇩1 ⊆ edges G⇩2"  (* rewriting peak *)
    unfolding relcomp_Image edge_preserving map_graph_selectors relcomp_on_triple.
  hence "edge_preserving f (edges G⇩1) (edges G⇩2)"
    unfolding edge_preserving f_id.
  thus ?lhs
    using sg assms unfolding graph_homomorphism_def
    by auto next
  assume ih:?lhs
  hence "vertices G⇩1 = Domain f ∧ univalent f ∧ G⇩1 = restrict G⇩1 ∧ subgraph (map_graph f G⇩1) G⇩2"
    unfolding graph_homomorphism_def edge_preserving
    by auto
  thus ?rhs unfolding subgraph_def by auto
qed


lemma map_graph_preserves_subgraph[intro]:
  assumes "subgraph A B"
  shows "subgraph (map_graph f A) (map_graph f B)"
  using assms unfolding subgraph_def by (auto simp:graph_union_iff)

lemma graph_homomorphism_concr_graph:
  assumes "graph G" "graph (LG e v)"
  shows "graph_homomorphism (LG e v) G x ⟷
         x `` v ⊆ vertices G ∧ on_triple x `` e ⊆ edges G ∧ univalent x ∧ Domain x = v"
  using assms unfolding graph_homomorphism_def2 graph_union_iff by auto

lemma subgraph_preserves_hom:
  assumes "subgraph A B"
          "graph_homomorphism X A h"
  shows "graph_homomorphism X B h"
  using assms by (meson graph_homomorphism_def2 map_graph_preserves_restricted subgraph_def subgraph_trans)

lemma graph_homo_union_id:
assumes "graph_homomorphism (graph_union A B) G f"
shows "graph A ⟹ graph_homomorphism A G (Id_on (vertices A) O f)"
      "graph B ⟹ graph_homomorphism B G (Id_on (vertices B) O f)"
  using assms unfolding graph_homomorphism_def edge_preserving
  by (auto dest:edge_preserving_atomic)

lemma graph_homo_union[intro]:
  assumes
   "graph_homomorphism A G f_a"
   "graph_homomorphism B G f_b"
   "Domain f_a ∩ Domain f_b = Domain (f_a ∩ f_b)"
  shows "graph_homomorphism (graph_union A B) G (f_a ∪ f_b)"
proof(rule graph_homomorphismI)
  have v0:"f_a `` vertices A ⊆ vertices G" "f_b `` vertices B ⊆ vertices G"
          "vertices A = Domain f_a" "vertices B = Domain f_b"
          "graph A" "graph B"
          "univalent f_a" "univalent f_b"
          "edge_preserving f_a (edges A) (edges G)"
          "edge_preserving f_b (edges B) (edges G)"
    using assms(1,2) unfolding graph_homomorphism_def by blast+
  hence v: "f_a `` vertices (graph_union A B) ⊆ vertices G"
           "f_b `` vertices (graph_union A B) ⊆ vertices G" by auto
  show uni:"univalent (f_a ∪ f_b)" using assms(3) v0 by auto
  show "(f_a ∪ f_b) `` vertices (graph_union A B) ⊆ vertices G" using v by auto
  have f_a:"Id_on (vertices A) O (f_a ∪ f_b) = f_a"
        using uni v0(3)
        by (cases A,auto simp:univalent_def on_triple_def Image_def)
  have onA:"on_triple (f_a ∪ f_b) `` edges A = on_triple (Id_on (vertices A) O (f_a ∪ f_b)) `` edges A"
    unfolding relcomp_on_triple relcomp_Image on_triple_ID_restrict v0(5)[symmetric] ..
  have f_b:"Id_on (vertices B) O (f_a ∪ f_b) = f_b"
        using uni v0(4) unfolding Un_commute[of f_a _]
        by (cases B,auto simp:univalent_def on_triple_def Image_def)
  have onB:"on_triple (f_a ∪ f_b) `` edges B = on_triple (Id_on (vertices B) O (f_a ∪ f_b)) `` edges B"
    unfolding relcomp_on_triple relcomp_Image on_triple_ID_restrict v0(6)[symmetric] ..
  have "edge_preserving (f_a ∪ f_b) (edges A) (edges G)"
       "edge_preserving (f_a ∪ f_b) (edges B) (edges G)"
    using v0(9,10) unfolding edge_preserving onA[unfolded f_a] onB[unfolded f_b] by auto
  thus "edge_preserving (f_a ∪ f_b) (edges (graph_union A B)) (edges G)"
    by auto
qed (insert assms[unfolded graph_homomorphism_def],auto)

lemma graph_homomorphism_on_graph:
  assumes "graph_homomorphism A B R"
  shows "graph_homomorphism A (map_graph_fn B f) (R O on_graph B f)"
proof -
  from assms have "Range R ⊆ vertices B"
    and ep: "edge_preserving R (edges A) (edges B)" unfolding graph_homomorphism_def by auto
  hence d:"Domain R ⊆ Domain (R O on_graph B f)" unfolding Domain_id_on by auto
  have v:"vertices (map_graph (R O on_graph B f) A) ⊆ vertices (map_graph_fn B f)"
    unfolding BNF_Def.Gr_def map_graph_selectors by auto
  have e:"edges (map_graph (R O on_graph B f) A) ⊆ edges (map_graph_fn B f)" using ep
    unfolding BNF_Def.Gr_def map_graph_selectors edge_preserving by auto
  have u:"graph_union (map_graph (R O on_graph B f) A) (map_graph_fn B f) = map_graph_fn B f"
    using e v graph_unionI by metis
  from d assms u show "graph_homomorphism A (map_graph_fn B f) (R O on_graph B f)"
    unfolding graph_homomorphism_def2 by auto
qed

end