Session Graph_Saturation

Theory MissingRelation

theory MissingRelation
imports Main
begin

lemma range_dom[simp]:
  "f `` Domain f = Range f"
  "converse f `` Range f = Domain f" by auto

lemma Gr_Image_image[simp]:
  shows "BNF_Def.Gr A f `` B = f ` (A  B)"
  unfolding BNF_Def.Gr_def by auto

definition univalent where "univalent R = ( x y z. (x,y) R  (x,z) R  z = y)"

lemma univalent_right_unique[simp]:
  shows "right_unique (λ x y. (x,y)  R) = univalent R"
        "univalent {(x,y).r x y} = right_unique r"
  unfolding univalent_def right_unique_def by auto

declare univalent_right_unique(1)[pred_set_conv]

lemma univalent_inter[intro]:
  assumes "univalent f_a  univalent f_b"
  shows "univalent (f_a  f_b)"
  using assms unfolding univalent_def by auto

lemma univalent_union[intro]:
  assumes "univalent f_a" "univalent f_b" "Domain f_a  Domain f_b = Domain (f_a  f_b)"
  shows "univalent (f_a  f_b)"
  unfolding univalent_def
proof(clarify,rule ccontr)
  from assms have uni:"univalent (f_a  f_b)" by auto
  fix x y z
  assume a:"(x, y)  f_a  f_b" "(x, z)  f_a  f_b" "z  y"
  show False 
  proof(cases "(x,y)  f_a")
    case True
    hence fb:"(x,z)f_b" using a assms[unfolded univalent_def] by auto
    hence "x  (Domain f_a  Domain f_b)" using True by auto
    with assms uni fb True have "z = y" by (metis DomainE IntD1 IntD2 univalent_def)
    with a show False by auto
  next
    case False
    hence fb:"(x,z)f_a" "(x,y)  f_b" using a assms[unfolded univalent_def] by auto
    hence "x  (Domain f_a  Domain f_b)" by auto
    with assms uni fb have "z = y" by (metis DomainE IntD1 IntD2 univalent_def)
    with a show False by auto
  qed
qed

lemma Gr_domain[simp]:
  shows "Domain (BNF_Def.Gr A f) = A"
    and "Domain (BNF_Def.Gr A id O R) = A  Domain R" unfolding BNF_Def.Gr_def by auto

lemma in_Gr[simp]:
  shows "(x,y)  BNF_Def.Gr A f  x  A  f x = y"
  unfolding BNF_Def.Gr_def by auto

lemma Id_on_domain[simp]:
  "Domain (Id_on A O f) = A  Domain f" by auto

lemma Domain_id_on:
  shows "Domain (R O S) = Domain R  R¯ `` Domain S"
  by auto

lemma Id_on_int:
  "Id_on A O f = (A × UNIV)  f" by auto

lemma Domain_int_univ:
  "Domain (A × UNIV  f) = A  Domain f" by auto

lemma Domain_O:
  assumes "a  Domain x" "x `` a  Domain y"
  shows "a  Domain (x O y)"
  proof fix xa assume xa:"xa  a" hence "xa  Domain x" using assms by auto
    then obtain w where xaw:"(xa,w)  x" by auto
    with xa have "w  Domain y" using assms by auto
    then obtain v where "(w,v)  y" by auto
    with xaw have "(xa,v)  x O y" by auto
    thus "xa  Domain (x O y)" by auto qed

lemma fst_UNIV[intro]:
  "A  fst ` A × UNIV" by force

lemma Gr_range[simp]:
  shows "Range (BNF_Def.Gr A f) = f ` A" unfolding BNF_Def.Gr_def by auto

lemma tuple_disj[simp]:
  shows "{y. y = x  y = z} = {x,z}" by auto

lemma univalent_empty [intro]: "univalent {}" unfolding univalent_def by auto

lemma univalent_char : "univalent R  converse R O R  Id"
  unfolding univalent_def by auto

lemma univalentD [dest]: "univalent R  (x,y) R  (x,z) R  z = y"
  unfolding univalent_def by auto

lemma univalentI: "converse R O R  Id  univalent R"
  unfolding univalent_def by auto

lemma univalent_composes[intro]:assumes "univalent R" "univalent S"
 shows "univalent (R O S)" using assms unfolding univalent_char by auto

lemma id_univalent[intro]:"univalent (Id_on x)" unfolding univalent_char by auto

lemma univalent_insert:
  assumes " c. (a,c)  R"
  shows "univalent (insert (a,b) R)  univalent R"
  using assms unfolding univalent_def by auto

lemma univalent_set_distinctI[intro]: (* not an iff: duplicates of A and B might align *)
  assumes "distinct A"
  shows "univalent (set (zip A B))"
  using assms proof(induct A arbitrary:B)
  case (Cons a A)
  hence univ:"univalent (set (zip A (tl B)))" by auto
  from Cons(2) have "a  set (take x A)" for x using in_set_takeD by fastforce
  hence "a  Domain (set (zip A (tl B)))"
    unfolding Domain_fst set_map[symmetric] map_fst_zip_take by auto
  hence " c. (a,c)  set (zip A (tl B))" by auto
  from univ univalent_insert[OF this] show ?case by(cases B,auto)
qed auto

lemma set_zip_conv[simp]:
"(set (zip A B))¯ = set (zip B A)" unfolding set_zip by auto

lemma univalent_O_converse[simp]:
  assumes "univalent (converse R)"
  shows "R O converse R = Id_on (Domain R)"
  using assms[unfolded univalent_char] by auto

lemma Image_outside_Domain[simp]:
  assumes "Domain R  A = {}"
  shows "R `` A = {}"
  using assms by auto

lemma Image_Domain[simp]:
  assumes "Domain R = A"
  shows "R `` A = Range R"
  using assms by auto

lemma Domain_set_zip[simp]:
  assumes "length A = length B"
  shows "Domain (set (zip A B)) = set A"
  unfolding Domain_fst set_map[symmetric] map_fst_zip[OF assms]..

lemma Range_set_zip[simp]:
  assumes "length A = length B"
  shows "Range (set (zip A B)) = set B"
  unfolding Range_snd set_map[symmetric] map_snd_zip[OF assms]..

lemma Gr_univalent[intro]:
  shows "univalent (BNF_Def.Gr A f)"
  unfolding BNF_Def.Gr_def univalent_def by auto

lemma univalent_fn[simp]:
  assumes "univalent R"
  shows "BNF_Def.Gr (Domain R) (λ x. SOME y. (x,y)  R) = R" (is "?lhs = _")
  unfolding set_eq_iff
proof(clarify,standard)
  fix a b assume a:"(a, b)  R"
  hence "(a,SOME y. (a, y)  R)  R" using someI by metis
  with assms a have [simp]:"(SOME y. (a, y)  R) = b" by auto
  show "(a, b)  ?lhs" using a by auto
next
  fix a b assume a:"(a,b)  ?lhs"
  hence "a  Domain R" "(SOME y. (a, y)  R) = b" by auto
  thus "(a,b)  R" using someI by auto
qed

lemma Gr_not_in[intro]:
  shows "x  F  f x  y  (x,y)  BNF_Def.Gr F f" by auto

lemma Gr_insert[simp]:
  shows "BNF_Def.Gr (insert x F) f = insert (x,f x) (BNF_Def.Gr F f)"
  unfolding BNF_Def.Gr_def by auto

lemma Gr_empty[simp]:
  shows "BNF_Def.Gr {} f = {}" by auto

lemma Gr_card[simp]:
  shows "card (BNF_Def.Gr A f) = card A"
proof(cases "finite A")
  case True
  hence "finite (BNF_Def.Gr A f)" by (induct A,auto)
  with True show ?thesis by (induct A,auto)
next
  have [simp]: "infinite (Domain (A - {x})) = infinite (Domain (A::('a × 'b) set))"
    for A x
    using Diff_infinite_finite Domain_Diff_subset finite.emptyI
              finite.insertI finite_Domain finite_subset Diff_subset Domain_mono
    by metis
  have "infinite (Domain A)   a. a  fst ` A" for A::"('a × 'b) set"
    using finite.simps unfolding Domain_fst by fastforce
  hence [intro]:"infinite (Domain A)   a b. (a,b)  A" for A::"('a × 'b) set"
    by fast
  let ?Gr = "BNF_Def.Gr A f"
  case False
  hence "infinite ?Gr"
    by(intro infinite_coinduct[of "infinite o Domain"],auto)
  with False show ?thesis by (auto simp:BNF_Def.Gr_def)
qed

lemma univalent_finite[simp]:
  assumes "univalent R"
  shows "card (Domain R) = card R"
        "finite (Domain R)  finite R"
proof -
  let ?R = "BNF_Def.Gr (Domain R) (λ x. SOME y. (x,y)  R)"
  have "card (Domain ?R) = card ?R" by auto
  thus "card (Domain  R) = card  R"
    unfolding univalent_fn[OF assms].
  thus "finite (Domain R)  finite R"
    by (metis Domain_empty_iff card_0_eq card.infinite finite.emptyI)
qed

lemma trancl_power_least:
  "p  R+  (n. p  R ^^ Suc n  (p  R ^^ n  n = 0))"
proof
  assume "p  R+"
  from this[unfolded trancl_power] obtain n where p:"n>0" "p  R ^^ n" by auto
  define n' where "n' = n - 1"
  with p have "Suc n' = n" by auto
  with p have "p  R ^^ Suc n'" by auto
  thus "n. p  R ^^ Suc n  (p  R ^^ n  n = 0)" proof (induct n')
    case 0 hence "p  R ^^ 0 O R  (p  R ^^ 0  0 = 0)" by auto
    then show ?case by force
  next
    case (Suc n)
    show ?case proof(cases "p  R ^^ Suc n")
      case False with Suc show ?thesis by blast
    qed (rule Suc)
  qed next
  assume "n. p  R ^^ Suc n  (p  R ^^ n  n = 0)"
  with zero_less_Suc have "n>0. p  R ^^ n" by blast
  thus "p  R+" unfolding trancl_power.
qed

lemma refl_on_tranclI :
  assumes "refl_on A r"
  shows "refl_on A (trancl r)"
  proof
    show "r+  A × A"
      by( rule trancl_subset_Sigma
        , auto simp: assms[THEN refl_onD1] assms[THEN refl_onD2])
    show "x  A  (x, x)  r+" for x
      using assms[THEN refl_onD] by auto
  qed

definition idempotent where
  "idempotent r  r O r = r"

lemma trans_def: "trans r = ((Id  r) O r = r)" "trans r = (r O (Id  r) = r)"
  by(auto simp:trans_def)

lemma idempotent_impl_trans: "idempotent r  trans r"
  by(auto simp:trans_def idempotent_def)

lemma refl_trans_impl_idempotent[intro]: "refl_on A r  trans r  idempotent r"
  by(auto simp:refl_on_def trans_def idempotent_def)

lemma idempotent_subset:
  assumes "idempotent R" "S  R"
  shows "S O R  R" "R O S  R" "S O R O S  R"
  using assms by (auto simp:idempotent_def)

(* not really about relations, but I need it in GraphRewriting.thy.
   Renaming the entire file to 'preliminaries' just because this is here would be too much. *)
lemma list_sorted_max[simp]:
  shows "sorted list  list = (x#xs)  fold max xs x = (last list)"
proof (induct list arbitrary:x xs)
  case (Cons a list)
  hence "xs = y # ys  fold max ys y = last xs" "sorted (x # xs)" "sorted xs" for y ys 
    using Cons.prems(1,2) by auto
  hence "xs  []  fold max xs x = last xs"
    by (metis (full_types) fold_simps(2) max.orderE sorted.elims(2) sorted2)
  thus ?case unfolding Cons by auto
qed auto

end

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 "R1  R2" "E1  E2" "edge_preserving R2 E2 G"
  shows "edge_preserving R1 E1 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 G1 G2 f 
    = ( vertices G1 = Domain f
       graph G1  graph G2
       f `` vertices G1  vertices G2
       univalent f
       edge_preserving f (edges G1) (edges G2)
      )"

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 G1 G2 
   graph_homomorphism G1 G2 (Id_on (vertices G1))" 

lemma subgraph_trans:
  assumes "subgraph G1 G2" "subgraph G2 G3"
  shows "subgraph G1 G3"
proof-
  from assms[unfolded graph_homomorphism_def]
  have "Id_on (vertices G1) O Id_on (vertices G2) = Id_on (vertices G1)"
    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). v1vertices (map_graph f G)  v2vertices (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 "xedges G. (x, a, g ac, g ba)  on_triple (on_graph G f)"
          "xedges 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  xvertices 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 G1 G2"
  shows "vertices G1  vertices G2" "edges (restrict G1)  edges G2"
proof -
  have vrt:"Id_on (vertices G1) `` vertices G1  vertices G2"
    and ep:"edge_preserving (Id_on (vertices G1)) (edges G1) (edges G2)"
    using assms unfolding graph_homomorphism_def by auto
  hence "edges (restrict G1)  edges G2"
    using assms unfolding edge_preserving by auto
  thus "vertices G1  vertices G2" "edges (restrict G1)  edges G2"
    using vrt by auto
qed

text ‹Our definition of subgraph is equivalent to definition 7.›
lemma subgraph_def2:
  assumes "graph G1" "graph G2"
  shows "subgraph G1 G2  vertices G1  vertices G2  edges G1  edges G2"
proof
  assume "vertices G1  vertices G2  edges G1  edges G2"
  hence v:"vertices G1  vertices G2" and "edges G1  edges G2" by auto
  hence ep:"edge_preserving (Id_on (vertices G1)) (edges G1) (edges G2)"
    unfolding edge_preserving_def by auto
  show "subgraph G1 G2"
    using assms(2) v ep graph_homomorphism_Id[of "G1",folded assms]
    unfolding graph_homomorphism_def by auto
next
  assume sg:"subgraph G1 G2"
  hence vrt:"Id_on (vertices G1) `` vertices G1  vertices G2"
    and ep:"edge_preserving (Id_on (vertices G1)) (edges G1) (edges G2)"
    unfolding graph_homomorphism_def by auto
  hence "edges G1  edges G2"
    using assms unfolding edge_preserving by auto
  thus "vertices G1  vertices G2  edges G1  edges G2"
    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 G1 G2 = LG (edges G1  edges G2) (vertices G1  vertices G2)"

lemma graph_unionI[intro]:
  assumes "edges G1  edges G2"
          "vertices G1  vertices G2"
  shows "graph_union G1 G2 = G2"
  using assms unfolding graph_union_def by (cases "G2",auto)

lemma graph_union_iff:
  shows "graph_union G1 G2 = G2  (edges G1  edges G2  vertices G1  vertices G2)"
  unfolding graph_union_def by (cases "G2",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 G1 G2) = vertices G1  vertices G2"
  unfolding graph_union_def by auto
lemma graph_union_edges[simp]:
"edges (graph_union G1 G2) = edges G1  edges G2"
  unfolding graph_union_def by auto

lemma graph_union_preserves_restrict[intro]:
  assumes "G1 = restrict G1" "G2 = restrict G2"
  shows "graph_union G1 G2 = restrict (graph_union G1 G2)"
proof -
  let ?e = "edges G1  edges G2"
  let ?v = "vertices G1  vertices G2"
  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 G1)")
      case True
      hence "(l,v1,v2)  edges G1" "v1  vertices G1" "v2  vertices G1"
         by (auto simp:restrict_def)+
      thus ?thesis by auto
    next
      case False hence "(l,v1,v2)  edges (restrict G2)" using a assms by auto
      hence "(l,v1,v2)  edges G2" "v1  vertices G2" "v2  vertices G2"
         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 G1 G2 = (G1 = restrict G1  G2 = restrict G2  graph_union G1 G2 = G2)"
proof
  assume assms:"subgraph G1 G2"
  hence r:"G2 = restrict G2" "G1 = restrict G1"
    unfolding graph_homomorphism_def by auto
  from subgraph_subset[OF assms]
  have ss:"vertices (restrict G1)  vertices G2" "edges (restrict G1)  edges G2" by auto
  show "G1 = restrict G1  G2 = restrict G2  graph_union G1 G2 = G2"
  proof(cases G2)
    case (LG x1 x2) show ?thesis using ss r
    unfolding graph_union_def LG by auto
  qed next
  assume gu: "G1 = restrict G1  G2 = restrict G2  graph_union G1 G2 = G2"
  hence sub:"(edges G1  edges G2)  edges G2"
    "vertices G1  vertices G2"
    unfolding graph_union_def by (cases G2;auto)+
  have r:"G1 = restrict G1" "G2 = restrict G2" using gu by auto
  show "subgraph G1 G2" 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 G1 G2 f =
   (vertices G1 = Domain f  univalent f  G1 = restrict G1  G2 = restrict G2  graph_union (map_graph f G1) G2 = G2)"
   (is "?lhs = ?rhs")
proof 
  let ?m = "map_graph f G1"
  assume ?rhs
  hence assms : "vertices G1 = Domain f" "univalent f" "G1 = restrict G1"
    and sg: "subgraph ?m G2"
    and f_id:"f O Id_on (f `` vertices G1) = f" unfolding subgraph_def by auto
  hence "edge_preserving (Id_on (vertices ?m)) (edges ?m) (edges G2)"
    unfolding graph_homomorphism_def by auto
  hence "on_triple (f O Id_on (f `` vertices G1)) `` edges G1  edges G2"  (* rewriting peak *)
    unfolding relcomp_Image edge_preserving map_graph_selectors relcomp_on_triple.
  hence "edge_preserving f (edges G1) (edges G2)"
    unfolding edge_preserving f_id.
  thus ?lhs
    using sg assms unfolding graph_homomorphism_def
    by auto next
  assume ih:?lhs
  hence "vertices G1 = Domain f  univalent f  G1 = restrict G1  subgraph (map_graph f G1) G2"
    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

Theory RulesAndChains

section ‹Rules, and the chains we can make with them›
text ‹This describes graph rules, and the reasoning is fully on graphs here (no semantics).
      The formalisation builds up to Lemma 4 in the paper.›
theory RulesAndChains
imports LabeledGraphs
begin

type_synonym ('l,'v) graph_seq = "(nat  ('l, 'v) labeled_graph)"

text ‹Definition 8.›
definition chain :: "('l, 'v) graph_seq  bool" where
  "chain S   i. subgraph (S i) (S (i + 1))"

lemma chain_then_restrict:
  assumes "chain S" shows "S i = restrict (S i)"
  using assms[unfolded chain_def graph_homomorphism_def] by auto

lemma chain:
  assumes "chain S"
  shows "j  i  subgraph (S i) (S j)"
proof(induct "j-i" arbitrary:i j)
  case 0
  then show ?case using chain_then_restrict[OF assms] assms[unfolded chain_def] by auto
next
  case (Suc x)
  hence j:"i + x + 1 = j" by auto
  thus ?case
    using subgraph_trans[OF Suc(1) assms[unfolded chain_def,rule_format,of "i+x"],of i,unfolded j]
    using Suc by auto
qed

lemma chain_def2:
  "chain S = ( i j. j  i  subgraph (S i) (S j))"
proof
  show "chain S  i j. i  j  subgraph (S i) (S j)" using chain by auto
  show "i j. i  j  subgraph (S i) (S j)  chain S" unfolding chain_def by simp
qed

text ‹Second part of definition 8.›
definition chain_sup :: "('l, 'v) graph_seq  ('l, 'v) labeled_graph" where
  "chain_sup S  LG ( i. edges (S i)) ( i. vertices (S i))"

lemma chain_sup_const[simp]:
  "chain_sup (λ x. S) = S"
  unfolding chain_sup_def by auto

lemma chain_sup_subgraph[intro]:
  assumes "chain S"
  shows "subgraph (S j) (chain_sup S)"
proof -
  have c1: "S j = restrict (S j)" for j
    using assms[unfolded chain_def,rule_format,of j] graph_homomorphism_def by auto
  hence c2: "chain_sup S = restrict (chain_sup S)"
    unfolding chain_sup_def by fastforce
  have c3: "graph_union (S j) (chain_sup S) = chain_sup S"
    unfolding chain_sup_def graph_union_def by auto
  show ?thesis unfolding subgraph_def using c1 c2 c3 by auto
qed

lemma chain_sup_graph[intro]:
  assumes "chain S"
  shows "graph (chain_sup S)"
  using chain_sup_subgraph[OF assms]
  unfolding subgraph_def by auto

lemma map_graph_chain_sup:
"map_graph g (chain_sup S) = chain_sup (map_graph g o S)"
  unfolding map_graph_def chain_sup_def by auto

lemma graph_union_chain_sup[intro]:
  assumes " i. graph_union (S i) C = C"
  shows "graph_union (chain_sup S) C = C"
proof
  from assms have e:"edges (S i)  edges C" and v:"vertices (S i)  vertices C" for i
    by (auto simp:graph_union_iff)
  show "edges (chain_sup S)  edges C" using e unfolding chain_sup_def by auto
  show "vertices (chain_sup S)  vertices C" using v unfolding chain_sup_def by auto
qed


type_synonym ('l,'v) Graph_PreRule = "('l, 'v) labeled_graph × ('l, 'v) labeled_graph"
text ‹Definition 9.›
abbreviation graph_rule :: "('l,'v) Graph_PreRule  bool" where
"graph_rule R  subgraph (fst R) (snd R)  finite_graph (snd R)"

definition set_of_graph_rules :: "('l,'v) Graph_PreRule set  bool" where
"set_of_graph_rules Rs   RRs. graph_rule R"

lemma set_of_graph_rulesD[dest]:
  assumes "set_of_graph_rules Rs" "R  Rs"
  shows "finite_graph (fst R)" "finite_graph (snd R)" "subgraph (fst R) (snd R)"
  using assms(1)[unfolded set_of_graph_rules_def] assms(2)
        rev_finite_subset[of "vertices (snd R)"]
        rev_finite_subset[of "edges (snd R)"]
  unfolding subgraph_def graph_union_iff by auto

text ‹We define @{term agree_on} as an equivalence.›
definition agree_on where
"agree_on G f1 f2  ( v  vertices G. f1 `` {v} = f2 `` {v})"

lemma agree_on_empty[intro,simp]: "agree_on (LG {} {}) f g" unfolding agree_on_def by auto

lemma agree_on_comm[intro]: "agree_on X f g = agree_on X g f" unfolding agree_on_def by auto
lemma agree_on_refl[intro]:
  "agree_on R f f" unfolding agree_on_def by auto
lemma agree_on_trans:
  assumes "agree_on X f g" "agree_on X g h"
  shows "agree_on X f h" using assms unfolding agree_on_def by auto

lemma agree_on_equivp:
  shows "equivp (agree_on G)"
  by (auto intro:agree_on_trans intro!:equivpI simp:reflp_def symp_def transp_def agree_on_comm)

lemma agree_on_subset:
  assumes "f  g" "vertices G  Domain f" "univalent g"
  shows "agree_on G f g"
  using assms unfolding agree_on_def by auto

lemma agree_iff_subset[simp]:
  assumes "graph_homomorphism G X f" "univalent g"
  shows "agree_on G f g  f  g"
  using assms unfolding agree_on_def graph_homomorphism_def by auto

lemma agree_on_ext:
  assumes "agree_on G f1 f2"
  shows "agree_on G (f1 O g) (f2 O g)"
  using assms unfolding agree_on_def by auto

lemma agree_on_then_eq:
  assumes "agree_on G f1 f2" "Domain f1 = vertices G" "Domain f2 = vertices G"
  shows "f1 = f2"
proof -
  from assms have agr:" v. vDomain f1  f1 `` {v} = f2 `` {v}" unfolding agree_on_def by auto
  have agr2:" v. vDomain f1  f1 `` {v} = {}"
            " v. vDomain f2  f2 `` {v} = {}" by auto
  with agr agr2 assms have " v. f1 `` {v} = f2 `` {v}" by blast
  thus ?thesis by auto
qed

lemma agree_on_subg_compose:
  assumes "agree_on R g h" "agree_on F f g" "subgraph F R"
  shows "agree_on F f h"
  using assms unfolding agree_on_def subgraph_def graph_union_iff by auto

definition extensible :: "('l,'x) Graph_PreRule  ('l,'v) labeled_graph  ('x × 'v) set  bool"
  where
"extensible R G f  ( g. graph_homomorphism (snd R) G g  agree_on (fst R) f g)"

lemma extensibleI[intro]: (* not nice as a standard rule, since obtained variables cannot be used *)
  assumes "graph_homomorphism R2 G g" "agree_on R1 f g"
  shows "extensible (R1,R2) G f"
  using assms unfolding extensible_def by auto

lemma extensibleD[elim]:
  assumes "extensible R G f"
          " g. graph_homomorphism (snd R) G g  agree_on (fst R) f g  thesis"
  shows thesis using assms extensible_def by blast

lemma extensible_refl_concr[simp]:
  assumes "graph_homomorphism (LG e1 v) G f"
  shows "extensible (LG e1 v, LG e2 v) G f  graph_homomorphism (LG e2 v) G f"
proof
  assume "extensible (LG e1 v, LG e2 v) G f"
  then obtain g where g: "graph_homomorphism (LG e2 v) G g" "agree_on (LG e1 v) f g"
    unfolding extensible_def by auto
  hence d:"Domain f = Domain g" "univalent f" "univalent g" using assms
    unfolding graph_homomorphism_def by auto
  from g have subs:"f  g"
    by(subst agree_iff_subset[symmetric,OF assms],auto simp:graph_homomorphism_def)
  with d have "f = g" by auto
  thus "graph_homomorphism (LG e2 v) G f" using g by auto
qed (auto simp: assms extensible_def)

lemma   extensible_chain_sup[intro]:
assumes "chain S" "extensible R (S j) f"
shows "extensible R (chain_sup S) f"
proof -
  from assms obtain g where g:"graph_homomorphism (snd R) (S j) g  agree_on (fst R) f g"
    unfolding extensible_def by auto
  have [simp]:"g O Id_on (vertices (S j)) = g" using g[unfolded graph_homomorphism_def] by auto
  from g assms(1)
  have "graph_homomorphism (snd R) (S j) g" "subgraph (S j) (chain_sup S)" by auto
  from graph_homomorphism_composes[OF this]
  have "graph_homomorphism (snd R) (chain_sup S) g" by auto
  thus ?thesis using g unfolding extensible_def by blast
qed

text ‹Definition 11.›
definition maintained :: "('l,'x) Graph_PreRule  ('l,'v) labeled_graph  bool"
  where "maintained R G   f. graph_homomorphism (fst R) G f  extensible R G f"

abbreviation maintainedA
  :: "('l,'x) Graph_PreRule set  ('l, 'v) labeled_graph  bool"
  where "maintainedA Rs G   RRs. maintained R G"

lemma maintainedI[intro]:
  assumes " f. graph_homomorphism A G f  extensible (A,B) G f"
  shows "maintained (A,B) G"
  using assms unfolding maintained_def by auto
lemma maintainedD[dest]:
  assumes "maintained (A,B) G" "graph_homomorphism A G f"
  shows "extensible (A,B) G f"
  using assms unfolding maintained_def by auto

lemma maintainedD2[dest]:
  assumes "maintained (A,B) G" "graph_homomorphism A G f"
          " g. graph_homomorphism B G g  f  g  thesis"
        shows thesis
  using maintainedD[OF assms(1,2),unfolded extensible_def]
proof
  fix g
  assume "graph_homomorphism (snd (A, B)) G g  agree_on (fst (A, B)) f g"
  hence "graph_homomorphism B G g" "f  g"
    using assms(2) unfolding graph_homomorphism_def2 agree_on_def by auto
  from assms(3)[OF this] show thesis.
qed

lemma extensible_refl[intro]:
  "graph_homomorphism R G f  extensible (R,R) G f"
  unfolding extensible_def by auto

lemma maintained_refl[intro]:
  "maintained (R,R) G" by auto

text ‹Alternate version of definition 8.›
definition fin_maintained :: "('l,'x) Graph_PreRule  ('l,'v) labeled_graph  bool"
  where
"fin_maintained R G   F f. finite_graph F
                          subgraph F (fst R)
                          extensible (F,fst R) G f
                          graph_homomorphism F G f
                          extensible (F,snd R) G f"

lemma fin_maintainedI [intro]:
  assumes " F f. finite_graph F
            subgraph F (fst R)
            extensible (F,fst R) G f
            graph_homomorphism F G f
            extensible (F,snd R) G f"
  shows "fin_maintained R G" using assms unfolding fin_maintained_def by auto

lemma maintained_then_fin_maintained[simp]:
  assumes maintained:"maintained R G"
  shows "fin_maintained R G"
proof
  fix F f
  assume subg:"subgraph F (fst R)"
     and ext:"extensible (F, fst R) G f" and igh:"graph_homomorphism F G f"
  from ext[unfolded extensible_def prod.sel] obtain g where
     g:"graph_homomorphism (fst R) G g" "agree_on F f g" by blast
  from maintained[unfolded maintained_def,rule_format,OF g(1)] g(2) subg
       agree_on_subg_compose
  show "extensible (F, snd R) G f" unfolding extensible_def prod.sel by blast
qed

lemma fin_maintained_maintained:
  assumes "finite_graph (fst R)"
  shows "fin_maintained R G  maintained R G" (is "?lhs = ?rhs")
proof
  from assms rev_finite_subset
  have fin:"finite (vertices (fst R))"
           "finite (edges (fst R))"
           "subgraph (fst R) (fst R)"
    unfolding subgraph_def graph_union_iff by auto
  assume ?lhs
  with fin have "extensible (fst R, fst R) G f  graph_homomorphism (fst R) G f
          extensible R G f" for f unfolding fin_maintained_def by auto 
  thus ?rhs by (simp add: extensible_refl maintained_def)
qed simp

lemma extend_for_chain:
assumes "g 0 = f"
    and " i. graph_homomorphism (S i) C (g i)"
    and " i. agree_on (S i) (g i) (g (i + 1))"
    and "chain S"
  shows "extensible (S 0, chain_sup S) C f"
proof
  let ?g = "i. g i"
  from assms(4)[unfolded chain_def subgraph_def graph_union_iff]
  have v:"vertices (S i)  vertices (S (i + 1))"
    and e:"edges (S i)  edges (S (i + 1))" for i by auto
  { fix a b i
    assume a:"(a, b)  g i"
    hence "a  vertices (S i)" using assms(2)[of i]
      unfolding graph_homomorphism_def2 by auto
    from assms(3)[unfolded agree_on_def,rule_format,OF this] a
    have "(a, b)  g (Suc i)" by auto
  }
  hence gi:"g i  g (Suc i)" for i by auto
  have gij:"i  j  g i  g j" for i j proof(induct j)
    case (Suc j) with gi[of j] show ?case by (cases "i = Suc j",auto)
  qed auto
  from assms(1) have f_subset:"f  ?g" by auto
  from assms(2)[of 0,unfolded assms(1)] have domf:"Domain f = vertices (S 0)"
    and grC:"graph C" and v_dom:"vertices (S i) = Domain (g i)" for i using assms(2)
    unfolding graph_homomorphism_def by auto
  { fix x y z i j assume "(x, y)  g i" "(x, z)  g j"
    with gij[of i "max i j"] gij[of j "max i j"]
    have "(x,y)  g (max i j)" "(x,z)  g (max i j)" by auto
    with assms(2)[unfolded graph_homomorphism_def]
    have "y = z" by auto
  } note univ_strong = this
  hence univ:"univalent ?g" unfolding univalent_def by auto
  { fix xa x i
    assume "(xa, x)  g i"
    hence "x  vertices (map_graph (g i) (S i))"
      using assms(2) unfolding graph_homomorphism_def by auto
    hence "x  vertices C"
      using assms(2) unfolding graph_homomorphism_def2 graph_union_iff by blast
  } note eq_v = this
  { fix l x y x' y' j i
    assume "(l,x,y)  edges (S j)" "(x, x')  g i" "(y, y')  g i"
    with gij[of i "max i j"] gij[of j "max i j"]
         chain[OF assms(4),unfolded subgraph_def graph_union_iff, of i "max i j"]
         chain[OF assms(4),unfolded subgraph_def graph_union_iff, of j "max i j"]
    have "(x,x')  g (max i j)" "(y,y')  g (max i j)"
         "(l,x,y)  edges (S (max i j))" by auto
    hence "(l, x', y')  edges C"
      using assms(2)[unfolded graph_homomorphism_def2 graph_union_iff] by auto
  } note eq_e = this
  have "graph_union (map_graph (g i) (chain_sup S)) C = C" for i
    unfolding graph_union_iff using eq_e eq_v
    unfolding graph_homomorphism_def2 chain_sup_def by auto
  hence subg:"graph_union (map_graph ?g (chain_sup S)) C = C"
    apply (rule graph_map_union) using gij by auto
  have "(i. vertices (S i)) = (i. Domain (g i))" using v_dom by auto
  hence vd:"vertices (chain_sup S) = Domain ?g"
    unfolding chain_sup_def by auto
  show "graph_homomorphism (chain_sup S) C ?g"
    unfolding graph_homomorphism_def2
    using univ chain_sup_graph[OF assms(4)] grC vd subg by auto
  show "agree_on (S 0) f ?g" using agree_on_subset[OF f_subset _ univ] domf by auto
qed

text ‹Definition 8, second part.›
definition consequence_graph
  where "consequence_graph Rs G  graph G  ( R  Rs. subgraph (fst R) (snd R)  maintained R G)"

lemma consequence_graphI[intro]:
  assumes " R. R Rs  maintained R G"
          " R. R Rs  subgraph (fst R) (snd R)"
          "graph G"
  shows "consequence_graph Rs G"
  unfolding consequence_graph_def fin_maintained_def using assms by auto

lemma consequence_graphD[dest]:
  assumes "consequence_graph Rs G"
  shows " R. R Rs  maintained R G"
        " R. R Rs  subgraph (fst R) (snd R)"
        "graph G"
  using assms unfolding consequence_graph_def fin_maintained_def by auto

text ‹Definition 8 states: If furthermore S is a subgraph of G,
    and (S, G) is maintained in each consequence graph maintaining Rs,
    then G is a least consequence graph of S maintaining Rs.
    Note that the type of 'each consequence graph' isn't given here.
   Taken literally, this should mean 'for every possible type'.
   We avoid quantifying on types by making the type an argument.
   Consequently, when proving 'least', the first argument should be free.›
definition least
  :: "'x itself  (('l, 'v) Graph_PreRule) set  ('l, 'c) labeled_graph  ('l, 'c) labeled_graph  bool"
  where "least _ Rs S G  subgraph S G  
            ( C :: ('l, 'x) labeled_graph. consequence_graph Rs C  maintained (S,G) C)"

lemma leastI[intro]:
assumes "subgraph S (G:: ('l, 'c) labeled_graph)"
        " C :: ('l, 'x) labeled_graph. consequence_graph Rs C  maintained (S,G) C"
      shows "least (t:: 'x itself) Rs S G"
  using assms unfolding least_def by auto

definition least_consequence_graph
  :: "'x itself  (('l, 'v) Graph_PreRule) set
      ('l, 'c) labeled_graph  ('l, 'c) labeled_graph  bool"
  where "least_consequence_graph t Rs S G  consequence_graph Rs G  least t Rs S G"

lemma least_consequence_graphI[intro]:
assumes "consequence_graph Rs (G:: ('l, 'c) labeled_graph)"
        "subgraph S G"
        " C :: ('l, 'x) labeled_graph. consequence_graph Rs C  maintained (S,G) C"
      shows "least_consequence_graph (t:: 'x itself) Rs S G"
  using assms unfolding least_consequence_graph_def least_def by auto

text ‹Definition 12.›
definition fair_chain where
  "fair_chain Rs S  chain S  
    ( R f i. (R  Rs  graph_homomorphism (fst R) (S i) f)  ( j. extensible R (S j) f))"

lemma fair_chainI[intro]:
  assumes "chain S"
    " R f i. R  Rs  graph_homomorphism (fst R) (S i) f   j. extensible R (S j) f"
  shows "fair_chain Rs S"
  using assms unfolding fair_chain_def by blast

lemma fair_chainD:
  assumes "fair_chain Rs S"
  shows "chain S"
        "R  Rs  graph_homomorphism (fst R) (S i) f   j. extensible R (S j) f"
  using assms unfolding fair_chain_def by blast+

lemma find_graph_occurence_vertices:
  assumes "chain S" "finite V" "univalent f" "f `` V  vertices (chain_sup S)"
  shows " i. f `` V  vertices (S i)"
  using assms(2,4)
proof(induct V)
  case empty thus ?case by auto
next
  case (insert v V)
  from insert.prems have V:"f `` V  vertices (chain_sup S)"
    and v:"f `` {v}  vertices (chain_sup S)" by auto
  from insert.hyps(3)[OF V] obtain i where i:"f `` V  vertices (S i)" by auto
  have " j. f `` {v}  vertices (S j)"
  proof(cases "(f `` {v}) = {}")
    case False
    then obtain v' where f:"(v,v')  f" by auto
    hence "v'  vertices (chain_sup S)" using v by auto
    then show ?thesis using assms(3) f unfolding chain_sup_def by auto
  qed auto
  then obtain j where j:"f `` {v}  vertices (S j)" by blast
  have sg:"subgraph (S i) (S (max i j))" "subgraph (S j) (S (max i j))"
    by(rule chain[OF assms(1)],force)+
  have V:"(f  V × UNIV) `` V  vertices (S (max i j))"
    using i subgraph_subset[OF sg(1)] by auto
  have v:"f `` {v}  vertices (S (max i j))" using j subgraph_subset[OF sg(2)] by auto
  have "f `` insert v V  vertices (S (max i j))" using v V by auto
  thus ?case by blast
qed

lemma find_graph_occurence_edges:
  assumes "chain S" "finite E" "univalent f"
        "on_triple f `` E  edges (chain_sup S)"
      shows " i. on_triple f `` E  edges (S i)"
  using assms(2,4)
proof(induct E)
  case empty thus ?case unfolding graph_homomorphism_def by auto
next
  case (insert e E)
  have univ:"univalent (on_triple f)" using assms(3) by auto
  have [simp]:"restrict (S i) = S i" for i
    using chain[OF assms(1),unfolded subgraph_def,of i i] by auto
  from insert.prems have E:"on_triple f `` E  edges (chain_sup S)"
    and e:"on_triple f `` {e}  edges (chain_sup S)" by auto
  with insert.hyps obtain i where i:"on_triple f `` E  edges (S i)" by auto
  have " j. on_triple f `` {e}  edges (S j)"
  proof(cases "on_triple f `` {e} = {}")
    case False
    then obtain e' where f:"(e,e')  on_triple f" by auto
    hence "e'  edges (chain_sup S)" using e by auto
    then show ?thesis using univ f unfolding chain_sup_def by auto
  qed auto
  then obtain j where j:"on_triple f `` {e}  edges (S j)" by blast
  have sg:"subgraph (S i) (S (max i j))" "subgraph (S j) (S (max i j))"
    by(rule chain[OF assms(1)],force)+
  have E:"on_triple f `` E  edges (S (max i j))"
    using i subgraph_subset[OF sg(1)] by auto
  have e:"on_triple f `` {e}  edges (S (max i j))" using j subgraph_subset[OF sg(2)] by auto
  have "on_triple f `` insert e E  edges (S (max i j))" using e E by auto
  thus ?case by blast
qed

lemma find_graph_occurence:
  assumes "chain S" "finite E" "finite V" "graph_homomorphism (LG E V) (chain_sup S) f"
  shows " i. graph_homomorphism (LG E V) (S i) f"
proof -
  have [simp]:"restrict (S i) = S i" for i
    using chain[OF assms(1),unfolded subgraph_def,of i i] by auto
  from assms[unfolded graph_homomorphism_def edge_preserving labeled_graph.sel]
  have u:"univalent f" 
   and e:"on_triple f `` E  edges (chain_sup S)"
   and v:"f `` V  vertices (chain_sup S)"
    by blast+
  from find_graph_occurence_edges[OF assms(1,2) u e]
  obtain i where i:"on_triple f `` E  edges (S i)" by blast
  from find_graph_occurence_vertices[OF assms(1,3) u v]
  obtain j where j:"f `` V  vertices (S j)" by blast
  have sg:"subgraph (S i) (S (max i j))" "subgraph (S j) (S (max i j))"
    by(rule chain[OF assms(1)],force)+
  have e:"on_triple f `` E  edges (S (max i j))"
   and v:"f `` V  vertices (S (max i j))"
    using i j subgraph_subset(2)[OF sg(1)] subgraph_subset(1)[OF sg(2)] by auto
  have "graph_homomorphism (LG E V) (S (max i j)) f"
  proof(rule graph_homomorphismI)
    from assms[unfolded graph_homomorphism_def edge_preserving labeled_graph.sel] e v
    show "vertices (LG E V) = Domain f"
     and "univalent f"
     and "LG E V = restrict (LG E V)"
     and "f `` vertices (LG E V)  vertices (S (max i j))" 
     and "edge_preserving f (edges (LG E V)) (edges (S (max i j)))"
     and "S (max i j) = restrict (S (max i j))" by auto
  qed
  thus ?thesis by auto
qed


text ‹Lemma 3.
      Recall that in the paper, graph rules use finite graphs, i.e. both sides should be finite.
      We strengthen lemma 3 by requiring only the left hand side to be a finite graph.›
lemma fair_chain_impl_consequence_graph:
  assumes "fair_chain Rs S" " R. R  Rs  subgraph (fst R) (snd R)  finite_graph (fst R)"
  shows "consequence_graph Rs (chain_sup S)"
proof -
  { fix R assume a:"R  Rs"
    have fin_v:"finite (vertices (fst R))" and fin_e: "finite (edges (fst R))"
      using assms(2)[OF a] by auto
    { fix f assume "graph_homomorphism (LG (edges (fst R)) (vertices (fst R))) (chain_sup S) f"
      with find_graph_occurence[OF fair_chainD(1)[OF assms(1)] fin_e fin_v]  
      obtain i where "graph_homomorphism (fst R) (S i) f" by auto
      from fair_chainD(2)[OF assms(1) a this] obtain j
         where "extensible R (S j) f" by blast
      hence "extensible R (chain_sup S) f" using fair_chainD(1)[OF assms(1)] by auto
    }
    hence "maintained R (chain_sup S)" unfolding maintained_def by auto
  } note mnt = this
  from assms have "chain S" unfolding fair_chain_def by auto
  thus ?thesis unfolding consequence_graph_def using mnt assms(2) by blast
qed

text ‹We extract the weak universal property from the definition of weak pushout step.
      Again, the paper allows for arbitrary types in the quantifier,
          but we fix the type here in the definition that will be used in @{term pushout_step}.
          The type used here should suffice (and we cannot quantify over types anyways)›
definition weak_universal ::
    "'x itself  ('a, 'c) Graph_PreRule  ('a, 'b) labeled_graph  ('a, 'b) labeled_graph 
     ('c × 'b) set  ('c × 'b) set  bool" where
"weak_universal _ R G1 G2 f1 f2  ( h1 h2 G::('a, 'x) labeled_graph.
             (graph_homomorphism (snd R) G h1  graph_homomorphism G1 G h2  f1 O h2  h1)
          ( h. graph_homomorphism G2 G h  h2  h))"

lemma weak_universalD[dest]:
  assumes "weak_universal (t:: 'x itself) R (G1::('a, 'b) labeled_graph) G2 f1 f2"
  shows "  h1 h2 G::('a, 'x) labeled_graph.
         graph_homomorphism (snd R) G h1  graph_homomorphism G1 G h2  f1 O h2  h1
          ( h. graph_homomorphism G2 G h  h2  h)"
  using assms unfolding weak_universal_def by metis

lemma weak_universalI[intro]:
  assumes " h1 h2 G::('a, 'x) labeled_graph.
         graph_homomorphism (snd R) G h1  graph_homomorphism G1 G h2  f1 O h2  h1
          ( h. graph_homomorphism G2 G h  h2  h)"
  shows "weak_universal (t:: 'x itself) R (G1::('a, 'b) labeled_graph) G2 f1 f2"
  using assms unfolding weak_universal_def by force


text ‹Definition 13›
definition pushout_step ::
    "'x itself  ('a, 'c) Graph_PreRule  ('a, 'b) labeled_graph  ('a, 'b) labeled_graph  bool" where
"pushout_step t R G1 G2  subgraph G1 G2  
  ( f1 f2. graph_homomorphism (fst R) G1 f1 
           graph_homomorphism (snd R) G2 f2 
           f1  f2 
           weak_universal t R G1 G2 f1 f2
  )"

text ‹Definition 14›
definition Simple_WPC ::
    "'x itself  (('a, 'b) Graph_PreRule) set  (('a, 'd) graph_seq)  bool" where
"Simple_WPC t Rs S  set_of_graph_rules Rs
    ( i. (graph (S i)  S i = S (Suc i))  ( R  Rs. pushout_step t R (S i) (S (Suc i))))"

lemma Simple_WPCI [intro]:
  assumes "set_of_graph_rules Rs" "graph (S 0)"
          " i. (S i = S (Suc i))  ( R  Rs. pushout_step t R (S i) (S (Suc i)))"
        shows "Simple_WPC t Rs S"
proof -
  have "graph (S i)" for i proof(induct i)
    case (Suc i)
    then show ?case using assms(3) unfolding pushout_step_def subgraph_def by metis
  qed (fact assms)
  thus ?thesis using assms unfolding Simple_WPC_def by auto
qed

lemma Simple_WPC_Chain[simp]:
  assumes "Simple_WPC t Rs S"
  shows "chain S"
proof -
  have "subgraph (S i) (S (Suc i))" for i using assms
    unfolding Simple_WPC_def pushout_step_def by (cases "graph (S i)  S i = S (Suc i)",auto)
  thus ?thesis unfolding chain_def by auto
qed


text ‹Definition 14, second part. ›
inductive WPC ::
    "'x itself  (('a, 'b) Graph_PreRule) set  (('a, 'd) graph_seq)  bool"
  where
    wpc_simpl [simp, intro]: "Simple_WPC t Rs S  WPC t Rs S"
  | wpc_combo [simp, intro]: "chain S  ( i.  S'. S' 0 = S i  chain_sup S' = S (Suc i)  WPC t Rs S')  WPC t Rs S"

lemma extensible_from_chainI:
  assumes ch:"chain S"
  and igh:"graph_homomorphism (S 0) C f"
  and ind:" f i. graph_homomorphism (S i) C f 
                h. (graph_homomorphism (S (Suc i)) C h)  agree_on (S i) f h"
  shows "extensible (S 0,chain_sup S) C f"
proof -
  have ch:"chain S" using assms by auto
  hence r0:"x. graph_homomorphism (S 0) C x  (0 = 0  x = f)"
    using igh by auto
  { fix i x
    assume "graph_homomorphism (S i) C x  (i = 0  x = f)"
    hence "graph_homomorphism (S i) C x" by auto
    from ind[OF this]
    have "y. (graph_homomorphism (S (Suc i)) C y  (Suc i = 0  y = f))  agree_on (S i) x y"
      by auto
  }
  with r0
  have " g. ( i. (graph_homomorphism (S i) C (g i)  (i = 0  g i = f))
                 agree_on (S i) (g i) (g (Suc i)) )" by (rule dependent_nat_choice)
  then obtain g where
       mtn:"g 0 = f"
           "graph_homomorphism (S i) C (g i)"
           "agree_on (S i) (g i) (g (i + 1))" for i by auto
  from extend_for_chain[OF mtn ch] show ?thesis.
qed

text ‹Towards Lemma 4, this is the key inductive property.›
lemma wpc_least:
  assumes "WPC (t:: 'x itself) Rs S"
  shows "least t Rs (S 0) (chain_sup S)"
  using assms
proof(induction S)
  case (wpc_simpl t Rs S)
  hence gr:"set_of_graph_rules Rs"
    and ps:" i. S i = S (Suc i)  (RRs. pushout_step t R (S i) (S (i + 1)))"
    unfolding Simple_WPC_def by auto
  have ch[intro]:"chain S" using wpc_simpl by auto
  show ?case
  proof fix C::"('a,'x) labeled_graph"
    assume cgC:"consequence_graph Rs C"
    show "maintained (S 0, chain_sup S) C"
    proof(standard,rule extensible_from_chainI,goal_cases)
      case (3 f x i)
      show ?case proof(cases "S i = S (Suc i)")
        case True
        with 3 show ?thesis by auto
      next
        case False
        with ps[of i,unfolded pushout_step_def] obtain R f1 f2 where
        R:"(fst R,snd R)  Rs" and f1:"graph_homomorphism (fst R) (S i) f1"
        and wu:"weak_universal t R (S i) (S (i + 1)) f1 f2" by auto
        from graph_homomorphism_composes[OF f1 3(2)]
        have ih_comp:"graph_homomorphism (fst R) C (f1 O x)".
        with maintainedD[OF consequence_graphD(1)[OF cgC R]]
        have "extensible (fst R, snd R) C (f1 O x)" by auto
        from this[unfolded extensible_def prod.sel]
        obtain g where g:"graph_homomorphism (snd R) C g" "f1 O x  g"
          using agree_iff_subset[OF ih_comp] unfolding graph_homomorphism_def by auto
        from weak_universalD[OF wu g(1) 3(2) g(2)] obtain h where
          h:"graph_homomorphism (S (i + 1)) C h" "x  h" by auto
        hence "agree_on (S i) x h"
          by(subst agree_iff_subset[OF 3(2)], auto simp:graph_homomorphism_def)
        then show ?thesis using h(1) by auto
      qed
    qed auto
  qed auto
next
  case (wpc_combo S t Rs)
  hence ps:" i. S'. S' 0 = S i 
         chain_sup S' = S (Suc i) 
         WPC t Rs S' 
         least t Rs (S' 0) (chain_sup S')"
    and ch[intro]:"chain S" unfolding Simple_WPC_def by auto
  show ?case proof fix C :: "('a, 'x) labeled_graph"
    assume cgC:"consequence_graph Rs C"
    show "maintained (S 0, chain_sup S) C"
    proof(standard,rule extensible_from_chainI,goal_cases)
      case (3 f g i)
      from ps[of i] have "least t Rs (S i) (S (Suc i))" by auto
      with cgC have ss:"subgraph (S i) (S (Suc i))" "maintained (S i, S (Suc i)) C"
        unfolding least_def by auto
      from ss(2) 3(2) have "extensible (S i, S (Suc i)) C g" by auto
      thus ?case unfolding extensible_def prod.sel.
    qed auto
  qed auto
qed

text ‹Lemma 4.›
lemma wpc_least_consequence_graph:
  assumes "WPC t Rs S" "consequence_graph Rs (chain_sup S)"
  shows "least_consequence_graph t Rs (S 0) (chain_sup S)"
  using wpc_least assms unfolding least_consequence_graph_def by auto

end

Theory GraphRewriting

section ‹Graph rewriting and saturation›
text ‹Here we describe graph rewriting, again without connecting it to semantics.›
theory GraphRewriting
  imports RulesAndChains 
    "HOL-Library.Infinite_Set"
begin

(* Algorithm 1 on page 16 *)
text ‹To describe Algorithm 1, we give a single step instead of the recursive call.
This allows us to reason about its effect without dealing with non-termination.
We define a worklist, saying what work can be done.
A valid selection needs to be made in order to ensure fairness.
To do a step, we define the function extend, and use it in @{term make_step}.
A function that always makes a valid selection is used in this step. ›

abbreviation graph_of where
  "graph_of  λ X. LG (snd X) {0..<fst X}"

definition nextMax :: "nat set  nat"
  where
  "nextMax x  if x = {} then 0 else Suc (Max x)"

lemma nextMax_max[intro]:
  assumes "finite x" "v  x"
  shows "v < nextMax x" "v  nextMax x"
  using Max.coboundedI[OF assms] assms(2) unfolding nextMax_def by auto

definition worklist :: "nat × ('a × nat × nat) set
            (('a, 'b) labeled_graph × ('a, 'b) labeled_graph) set
               (nat × ('a, 'b) Graph_PreRule × ('b × nat) set) set" where
"worklist G Rs  let G = graph_of G
  in {(N,R,f). R Rs  graph_homomorphism (fst R) G f  N = nextMax (Range f)
                  ¬ extensible R G f }"

definition valid_selection where
"valid_selection Rs G R f 
  let wl = worklist G Rs in
    (nextMax (Range f), R,f)  wl 
    ( (N,_)  wl. N  nextMax (Range f)) 
    graph_rule R"

lemma valid_selection_exists:
  assumes "worklist G Rs  {}"
          "set_of_graph_rules Rs"
  shows "L R f. valid_selection Rs G R f"
proof -
  define wl where "wl = worklist G Rs" hence wl_ne:"wl  {}" using assms(1) by auto
  let ?N = "LEAST N. N  Domain wl"
  from wl_ne have " N. N  Domain wl" by auto
  with LeastI2 have "?N  Domain wl" by metis
  then obtain L R f where NLRf:"(?N,(L,R),f)wl" by auto
  hence N_def:"?N = nextMax (Range f)"
    and in_Rs: "(L,R)  Rs" unfolding wl_def worklist_def Let_def by auto
  from Least_le wl_ne Domain.intros case_prodI2 
  have min:"( (N',_)  wl. N'  ?N)" by (metis (no_types, lifting))
  from in_Rs have "finite_graph R" "subgraph L R"
    using assms(2)[unfolded set_of_graph_rules_def] by auto
  with min NLRf N_def show ?thesis unfolding wl_def[symmetric] valid_selection_def by auto
qed

definition valid_selector where
"valid_selector Rs selector   G.
   (worklist G Rs  {}  ( (R,f)UNIV. selector G = Some (R,f)
                                valid_selection Rs G R f)) 
   (worklist G Rs = {}  selector G = None)"

lemma valid_selectorD[dest]:
  assumes "valid_selector Rs selector"
  shows "worklist G Rs = {}  selector G = None"
        "selector G = Some (R,f)  valid_selection Rs G R f"
  using assms[unfolded valid_selector_def,rule_format,of G]
  by (cases "worklist G Rs = {}",auto)

text ‹The following gives a valid selector.
      This selector is not useful as concrete implementation, because it used the choice operation.›
definition non_constructive_selector where
"non_constructive_selector Rs G  let wl = worklist G Rs in
   if wl = {} then None else Some (SOME (R,f). valid_selection Rs G R f) "

lemma non_constructive_selector:
  assumes "set_of_graph_rules Rs"
  shows "valid_selector Rs (non_constructive_selector Rs)"
  unfolding valid_selector_def proof((clarify,standard;clarify),goal_cases)
  case (1 n E)
  let ?x = "(SOME (R, f). valid_selection Rs (n, E) R f)"
  from valid_selection_exists[OF 1 assms]
  have " R f. valid_selection Rs (n, E) R f" by auto
  hence " x. valid_selection Rs (n, E) (fst x) (snd x)"
    by auto
  from this prod.case_eq_if tfl_some
  have "¬ valid_selection Rs (n, E) (fst ?x) (snd ?x)  False"
    by (metis (mono_tags, lifting))
  thus ?case unfolding non_constructive_selector_def Let_def using 1 by (auto simp:prod_eq_iff)
qed (auto simp:non_constructive_selector_def)


text ‹The following is used to make a weak pushout step.
      In the paper, we aren't too specific on how this should be done. Here we are.
      We work on natural numbers in order to be able to pick fresh elements easily. ›
definition extend ::
    "nat  ('b, 'a::linorder) Graph_PreRule   ('a × nat) set  ('a × nat) set" where
"extend n R f  f  
   (let V_new = sorted_list_of_set (vertices (snd R) - vertices (fst R))
    in set (zip V_new [n..<(n+length V_new)]))"

lemma nextMax_set[simp]:
  assumes "sorted xs"
  shows "nextMax (set xs) = (if xs = Nil then 0 else Suc (last xs))"
  using assms
proof(induct xs)
  case Nil show ?case unfolding nextMax_def by auto
next
  case (Cons a list)
  hence "list  []  fold max list a = last list"
    using list_sorted_max by (metis last.simps)
  thus ?case unfolding nextMax_def Max.set_eq_fold by auto
qed

lemma nextMax_Un_eq[simp]:
"finite x  finite y  nextMax (x  y) = max (nextMax x) (nextMax y)"
  unfolding nextMax_def using Max_Un by auto

lemma extend: (* extensible into the new graph *)
  assumes "graph_homomorphism (fst R) (LG E {0..<n}) f" "graph_rule R"
  defines "g  extend n R f"
  defines "G'  LG ((on_triple g `` (edges (snd R)))  E) {0..<max n (nextMax (Range g))}"
  shows "graph_homomorphism (snd R) G' g" "agree_on (fst R) f g" "f  g"
        "subgraph (LG E {0..<n}) G'"
        "weak_universal (t:: 'x itself) R (LG E {0..<n}) G' f g"
proof -
  have ln:"length x = length [n..<n + length x]" for x::"'b list" by auto
  let ?R_L = "vertices (snd R) - vertices (fst R)"
  from assms
  have "graph_rule (fst R,snd R)" and fin_R:"finite (vertices (snd R))"
    and subsLR:"vertices (fst R)  vertices (snd R)" and gr_R:"graph (snd R)"
    unfolding subgraph_def graph_union_iff
    by auto
  hence fin_R_L[simp]:"finite ?R_L"
     and fin_L:"finite (vertices (fst R))"
     using finite_subset by auto
  from assms have f_dom:"Domain f = vertices (fst R)"
    and f_uni:"univalent f" unfolding graph_homomorphism_def by auto
  from assms[unfolded graph_homomorphism_def]
  have "f `` vertices (fst R)  vertices (LG E {0..<n})" by blast
  hence f_ran:"Range f  {0..<n}" using f_dom by auto
  let ?g = "(let V_new = sorted_list_of_set ?R_L
              in set (zip V_new [n..<n + length V_new]))" (* new part of g *)
  have fin_g':"finite ?g" "finite (Range ?g)" unfolding Let_def by auto
  have "finite (Domain f)" "univalent f" using assms(1) fin_L
    unfolding graph_homomorphism_def by auto
  hence fin_f:"finite (Range f)" unfolding Range_snd by auto
  hence fin_g:"finite (Range g)" unfolding extend_def g_def Let_def Range_Un_eq by auto
  have nextMax_f:"nextMax (Range f)  n"
    using f_ran Max_in[OF fin_f] by (simp add:nextMax_def Suc_leI subset_eq)
  
  have "x  Domain ?g  x  Domain f" for x unfolding f_dom Let_def by auto
  hence g_not_f:"(x,y)  ?g  (x,z)  f" for x y z by blast
  have uni_g':"univalent ?g" "univalent (converse ?g)" unfolding Let_def by auto
  with f_uni have uni_g:"univalent g" by (auto simp:g_def extend_def g_not_f)
  from fin_g have "(a,b)  g  b < Suc (Max (Range g))" for a b
    unfolding less_Suc_eq_le by (rule Max.coboundedI) force
  hence "(a,b)  g  b < nextMax (Range g)" for a b
    unfolding nextMax_def by (cases "Range g = {}",auto)
  hence in_g:"(a,b)  g  b < max n (nextMax (Range g))" for a b by fastforce
  let ?G = "LG E {0..<n}"
  have gr_G:"graph ?G" using assms(1) unfolding graph_homomorphism_def by blast
  hence "(a, aa, b)  E  b < max n c" "(a, aa, b)  E  aa < max n c"
    for a aa b c by fastforce+
  hence gr_G':"graph G'" unfolding G'_def restrict_def using in_g by auto
  show "subgraph (LG E {0..<n}) G'"
    unfolding subgraph_def2[OF gr_G gr_G'] unfolding G'_def by auto
  have g_dom:"vertices (snd R) = Domain g" using subsLR
    unfolding g_def extend_def Domain_Un_eq f_dom by (auto simp:Let_def)
  show "graph_homomorphism (snd R) G' g"
    by (intro graph_homomorphismI[OF g_dom _ uni_g _ gr_R gr_G'])
       (auto simp:G'_def intro:in_g)
  show "f  g" by (auto simp:g_def extend_def)
  thus "agree_on (fst R) f g" using f_dom uni_g agree_on_subset equalityE by metis
  show "weak_universal t R ?G G' f g" proof fix a:: "('b × 'x) set" fix b G
    assume a:"graph_homomorphism (snd R) G a"
             "graph_homomorphism ?G G b" "f O b  a"
    hence univ_b:"univalent b" and univ_a:"univalent a"
      and rng_b:"Range b  vertices G" and rng_a:"Range a  vertices G"
      and ep_b:"edge_preserving b (edges (LG E {0..<n})) (edges G)"
      and ep_a:"edge_preserving a (edges (snd R)) (edges G)"
      unfolding graph_homomorphism_def prod.sel labeled_graph.sel by blast+
    from a have dom_b:"Domain b = {0..<n}"
      and dom_a:"Domain a = vertices (snd R)" and v6: "graph G"
      unfolding graph_homomorphism_def prod.sel labeled_graph.sel by auto

    have help_dom_b:"(y, z)  b  n  y  False" for y z using dom_b
      by (metis Domain.DomainI atLeastLessThan_iff not_less)
    have disj_doms:"Domain b  Domain (?g¯ O a) = {}" using help_dom_b
      unfolding Let_def by (auto dest!:set_zip_leftD)

    have "max n (nextMax (Range ?g)) = n + length (sorted_list_of_set ?R_L)" (is "_ = ?len")
      unfolding Let_def Range_snd set_map[symmetric] map_snd_zip[OF ln] nextMax_set[OF sorted_upt]
      by (fastforce simp del: length_sorted_list_of_set)
    hence n_eq:"?len = max n (nextMax (Range g))"
      unfolding Range_snd[symmetric] g_def extend_def Range_Un_eq
                nextMax_Un_eq[OF fin_f fin_g'(2)] max.assoc[symmetric] max_absorb1[OF nextMax_f]
      by auto

    let ?h = "b  ?g¯ O a"

    have dg:"Domain (?g¯) = {n..<max n (nextMax (Range g))}"
      unfolding Let_def Domain_converse Range_set_zip[OF ln] atLeastLessThan_upt
      unfolding Range_snd n_eq ..
    have "?g `` Domain a = ?g `` (?R_L  vertices (fst R))"
      using dom_a subsLR by auto
    also have " = ?g `` ?R_L  ?g `` vertices (fst R)" by blast
    also have "?g `` vertices (fst R) = {}" apply(rule Image_outside_Domain)
      unfolding Let_def Domain_set_zip[OF ln] by auto
    also have "?g `` ?R_L = Range ?g" apply(rule Image_Domain)
      unfolding Let_def Domain_set_zip[OF ln] by auto
    finally have dg2:"?g `` Domain a = {n..<max n (nextMax (Range g))}"
      unfolding Let_def Range_set_zip[OF ln] set_sorted_list_of_set[OF fin_R_L] 
      unfolding n_eq set_upt by auto
    have "Domain (?g¯ O a) = {n..<max n (nextMax (Range g))}"
      unfolding Domain_id_on converse_converse dg dg2 by auto
    hence v1: "vertices G' = Domain ?h" unfolding G'_def Domain_Un_eq dom_b by auto
    have "b `` vertices G'  vertices G" "(?g¯ O a) `` vertices G'  vertices G"
      using rng_a rng_b by auto
    hence v2: "?h `` vertices G'  vertices G" by blast
    have v3: "univalent ?h"
      using disj_doms univalent_union[OF univ_b univalent_composes[OF uni_g'(2) univ_a]] by blast
    (* showing edge preservation *)
    { fix l x y x' y' assume a2:"(l,x,y)  edges G'" "(x,x')  ?h" "(y,y')  ?h"
      have "(l,x',y')  edges G" proof(cases "(l,x,y)  edges ?G")
        case True
        with gr_G[THEN restrictD]
        have "x  Domain b" "y  Domain b" unfolding dom_b by auto
        hence "x  Domain (converse ?g O a)" "y  Domain (converse ?g O a)"
          using disj_doms by blast+
        hence "(x,x')  b" "(y,y')  b" using a2 by auto
        with ep_b True show ?thesis unfolding edge_preserving by auto
      next
        have "g O ?h = f O b  ?g O b  ((f O ?g¯) O a  (?g O ?g¯) O a)"
          unfolding g_def extend_def by blast
        also have "(?g O ?g¯) = Id_on ?R_L"
          unfolding univalent_O_converse[OF uni_g'(2)] unfolding Let_def by auto
        also have "(f O ?g¯) = {}" using f_ran unfolding Let_def by (auto dest!:set_zip_leftD)
        also have "?g O b = {}" using help_dom_b unfolding Let_def by (auto dest!:set_zip_rightD)
        finally have gOh:"g O ?h  a" using a(3) by blast
        case False
        hence "(l,x,y)  on_triple g `` edges (snd R)" using a2(1) unfolding G'_def by auto
        then obtain r_x r_y
          where r:"(l,r_x,r_y)  edges (snd R)" "(r_x,x)  g" "(r_y,y)  g" by auto
        hence "(r_x,x')  a" "(r_y,y')  a" using gOh a2(2,3) by auto
        hence "(l,x',y')  on_triple a `` edges (snd R)" using r(1) unfolding on_triple_def by auto
        thus ?thesis using ep_a unfolding edge_preserving by auto
      qed
    }
    hence v4: "edge_preserving ?h (edges G') (edges G)" by auto
    have "graph_homomorphism G' G ?h" by(fact graph_homomorphismI[OF v1 v2 v3 v4 gr_G' v6])
    thus "h. graph_homomorphism G' G h  b  h" by auto
  qed
qed

text ‹Showing that the extend function indeed creates a valid pushout.›
lemma selector_pushout:
  assumes "valid_selector Rs selector" "selector G'' = Some (R,f)"
  defines "G  graph_of G''"
  assumes "graph G"
  defines "g  extend (fst G'') R f"
  defines "G'  LG (on_triple g `` edges (snd R)  (snd G'')) {0..<max (fst G'') (nextMax (Range g))}"
  shows "pushout_step (t:: 'x itself) R G G'"
proof -
  have "valid_selection Rs G'' R f" using assms by(cases "selector G''",auto)
  hence igh:"graph_homomorphism (fst R) G f" "graph_rule R"
    unfolding valid_selection_def worklist_def G_def Let_def by auto
  have "subgraph G G'"
       "graph_homomorphism (fst R) G f"
       "graph_homomorphism (snd R) G' g"
       "f  g"
       "weak_universal t R G G' f g"
    using extend[OF igh[unfolded G_def],folded g_def,folded G'_def,folded G_def] igh(1)
    by auto
  thus ?thesis unfolding pushout_step_def by auto
qed

text ‹Making a single step in Algorithm 1.
  A prerequisite is that its first argument is a @{term valid_selector}.›

definition make_step where
"make_step selector S 
   case selector S of
     None  S |
     Some (R,f)  (let g = extend (fst S) R f in
         (max (fst S) (nextMax (Range g)), (on_triple g `` (edges (snd R)))  (snd S)))"

lemma WPC_through_make_step:
  assumes "set_of_graph_rules Rs" "graph (graph_of (X 0))"
     and makestep: " i. X (Suc i) = make_step selector (X i)"
     and selector: "valid_selector Rs selector"
  shows "Simple_WPC t Rs (λ i. graph_of (X i))" "chain (λ i. graph_of (X i))"
proof
  note ms = makestep[unfolded make_step_def,rule_format]
  have gr:"graph (graph_of (X i))" for i proof(induct i)
    case (Suc i)
    then show ?case proof(cases "selector (X i)")
      case None
      then show ?thesis using ms Suc by auto
    next
      case (Some a)
      then obtain R f where Some:"selector (X i) = Some (R,f)" by fastforce
      then show ?thesis using ms[of i,unfolded Some Let_def]
        selector_pushout[OF selector Some Suc,of t
                        ,unfolded pushout_step_def subgraph_def]
        by auto
    qed
  qed (fact assms)
  show "chain (λ i. graph_of (X i))" unfolding chain_def
  proof(clarify) fix i
    show "subgraph (graph_of (X i)) (graph_of (X (i + 1)))"
    proof(cases "selector (X i)")
      case None
      then show ?thesis using ms gr by (auto intro!:graph_homomorphismI)
    next
      case Some
      then obtain R f where Some:"selector (X i) = Some (R,f)" by fastforce
      then show ?thesis using ms selector_pushout[OF selector Some gr,of t]
      unfolding pushout_step_def Let_def by simp
    qed
  qed
  show "graph_of (X i) = graph_of (X (Suc i)) 
         (RRs. pushout_step t R (graph_of (X i)) (graph_of (X (Suc i))))" for i
  proof(cases "selector (X i)")
    case None thus ?thesis using ms by auto
  next
    case Some
    then obtain R f where Some:"selector (X i) = Some (R,f)" by fastforce
    hence "R  Rs" 
      using valid_selectorD(2)[OF selector,unfolded valid_selection_def worklist_def Let_def]
      by(cases R,blast)
    then show ?thesis using ms[of i,unfolded Some Let_def] selector_pushout[OF selector Some gr]
      unfolding make_step_def by auto
  qed
qed (fact assms)+

lemma N_occurs_finitely_often:
  assumes "finite Rs" "set_of_graph_rules Rs" "graph (graph_of (X 0))"
      and makestep: " i. X (Suc i) = make_step selector (X i)"
      and selector: "valid_selector Rs selector"
    shows "finite {(R,f).  i. R Rs  graph_homomorphism (fst R) (graph_of (X i)) f
                         nextMax (Range f)  N}" (is "finite {(R,f).?P R f}")
proof -
  have prod_eq : "( x  {(x, y). A x y}. B x)  ( x. A (fst x) (snd x)  B x)"
     "(x  {(x, y). A x y})  (A (fst x) (snd x))"
    for A B x by auto
  let ?S = "{(R,f).?P R f}"
  let "?Q R f" = "Domain f = vertices (fst (R::('a, 'b) Graph_PreRule))  univalent f  nextMax (Range f)  N"
  have seteq:"(RRs. {(R', f). R' = R  ?Q R f}) = {(R,f). R  Rs  ?Q R f}" by auto
  have " R  Rs. finite {(R',f). R' = R  ?Q R f}"
  proof fix R assume "R  Rs"
    hence fin:"finite (vertices (fst R))" using assms by auto
    hence fin2:"finite (Pow (vertices (fst R) × {0..N}))" by auto
    have fin:"Domain x = vertices (fst R)  univalent x  finite (snd ` x)"
      for x:: "('b × nat) set" using fin univalent_finite[of x] by simp
    hence "Domain f = vertices (fst R) 
      univalent f  (a,b)  f  nextMax (Range f)  N  b  N" for f a b
      unfolding Range_snd using image_eqI nextMax_max(2) snd_conv order.trans by metis
    hence sub:"{f. ?Q R f}  Pow (vertices (fst R) × {0..N})"
      using nextMax_max[OF fin] by (auto simp:Range_snd image_def)
    from finite_subset[OF sub fin2] show "finite {(R',f). R' = R  ?Q R f}" by auto
  qed
  from this[folded finite_UN[OF assms(1)],unfolded seteq]
  have fin:"finite {(R,f). R  Rs  ?Q R f}".
  have "?P R f  R  Rs  ?Q R f" for R f
    unfolding graph_homomorphism_def by auto
  hence "?S  {(R,f). R  Rs  ?Q R f}" unfolding subset_eq prod_eq by blast
  from finite_subset[OF this fin] show ?thesis by auto
qed

lemma inj_on_infinite:
  assumes "infinite A" "inj_on f A" "range f  B"
  shows "infinite B"
proof -
  from assms[unfolded infinite_iff_countable_subset] obtain g::"nat  'a" where
    g:"inj g  range g  A" by blast
  hence i:"inj (f o g)" using assms(2) using comp_inj_on inj_on_subset by blast
  have "range (f o g)  B" using assms(3) by auto
  with i show ?thesis
    unfolding infinite_iff_countable_subset by blast
qed

lemma makestep_makes_selector_inj:
  assumes "selector (X y) = Some (R,f)"
          "selector (X x) = Some (R,f)"
          "valid_selector Rs selector"
    and step: " i. X (Suc i) = make_step selector (X i)"
    and chain:"chain (λ i. graph_of (X i))"
  shows "x = y"
proof(rule ccontr)
  assume a:"x  y"
  define x' y' where "x'  min x y" "y'  max x y"
  hence xy:"selector (X x') = Some (R, f)" "selector (X y') = Some (R, f)" "x' < y'"
    using assms(1,2) a unfolding min_def max_def by auto
  with valid_selectorD assms
  have "valid_selection Rs (X x') R f" "valid_selection Rs (X y') R f" by auto
  hence not_ex:"¬ extensible R (graph_of (X y')) f"
    and hom:"graph_homomorphism (fst R) (graph_of (X x')) f" "graph_rule R"
    unfolding valid_selection_def Let_def worklist_def by auto
  have X:"X (Suc x') = (max (fst (X x')) (nextMax (Range (extend (fst (X x')) R f))),
          on_triple (extend (fst (X x')) R f) `` edges (snd R)  snd (X x'))"
    unfolding step[unfolded make_step_def Let_def,rule_format] xy by auto
  let ?ex = "extend (fst (X x')) R f"
  have hom:"graph_homomorphism (snd R) (graph_of (X (Suc x'))) ?ex"
       and agr:"agree_on (fst R) f ?ex" using extend(1,2)[OF hom] unfolding X by auto
  from xy have "Suc x'  y'" by auto
  with chain[unfolded chain_def2] have "subgraph (graph_of (X (Suc x'))) (graph_of (X y'))" by auto
  from subgraph_preserves_hom[OF this hom]
  have hom:"graph_homomorphism (snd R) (graph_of (X y')) ?ex".
  with agr have "extensible R (graph_of (X y')) f" unfolding extensible_def by auto
  thus False using not_ex by auto
qed

lemma fair_through_make_step:
  assumes "finite Rs" "set_of_graph_rules Rs" "graph (graph_of (X 0))"
     (* It should suffice to take infinitely many make_steps, 
        rather than having every step be a make_step,
        but we focus on the algorithm as in the paper here *)
     and makestep: " i. X (Suc i) = make_step selector (X i)"
     and selector: "valid_selector Rs selector"
  shows "fair_chain Rs (λ i. graph_of (X i))"
proof
  show chn:"chain (λi. graph_of (X i))" using WPC_through_make_step assms by blast
  fix R f i
  assume Rs:"R  Rs" and h:"graph_homomorphism (fst R) (graph_of (X i)) f"
  hence R:"finite (vertices (snd R))" "subgraph (fst R) (snd R)"  "finite (vertices (fst R))"
    using assms by auto
  hence f:"finite f" "finite (Range f)" "finite (Domain f)" "univalent f" 
    using h unfolding graph_homomorphism_def Range_snd by auto
  define N where "N  nextMax (Range f)"
  fix S
  let "?Q X' j" = " fst X'  Rs
                   graph_homomorphism (fst (fst X')) (graph_of (X (j+i))) (snd X')
                   nextMax (Range (snd X'))  N"
  let ?S = "{(R,f). j. ?Q (R,f) j}"
  from assms(4) have "ia. X (Suc ia + i) = make_step selector (X (ia + i))" by auto
  note r = assms(1,2) chain_then_restrict[OF chn] this assms(5)
  from N_occurs_finitely_often[of Rs "λ j. X (j + i)",OF r]
  have fin_S:"finite ?S" by auto
  { assume a:"j. ¬ extensible R (graph_of (X j)) f"
    let "?P X' j" = "?Q X' j  Some X' = selector (X (j+i))"
    { fix j let ?j = "j+i" have "?j  i" by auto
      from subgraph_preserves_hom[OF chain[OF chn this] h]
      have h:"graph_homomorphism (fst R) (graph_of (X ?j)) f".
      have "¬ extensible R (graph_of (X ?j)) f" using a by blast 
      with h Rs have wl:"(nextMax (Range f),R,f)  worklist (X ?j) Rs" 
        unfolding worklist_def Let_def set_eq_iff by auto
      hence "worklist (X ?j) Rs  {}" by auto
      with valid_selectorD[OF selector]
      obtain R' f'
        where sel:"Some (R',f') = selector (X ?j)"
                  "valid_selection Rs (X ?j) R' f'" by auto
      hence max:"(nextMax (Range f'), R', f')  worklist (X ?j) Rs"
                "((N, _)worklist (X ?j) Rs. nextMax (Range f')  N)"
        unfolding valid_selection_def Let_def by auto
      with wl have "nextMax (Range f')  N" unfolding N_def by auto
      with max(1)[unfolded worklist_def Let_def mem_Collect_eq prod.case] sel(1)
      have " X'. ?P X' j" by (metis fst_conv snd_conv)
    }
    then obtain ch where ch:" j. ?P (ch j) j" by metis (* uses 'choice' internally *)
    have inj:"inj ch" proof fix x y assume "ch x = ch y"
      with ch[of x] ch[of y]
      have "selector (X (x + i)) = Some (ch x)" "selector (X (y + i)) = Some (ch x)" by auto
      with makestep_makes_selector_inj[OF _ _ selector makestep chn] have "x + i = y + i"
        by (cases "ch x",metis (full_types))
      thus "x = y" by auto
    qed
    have "ch x  ?S" for x using ch[of x] unfolding mem_Collect_eq by(intro case_prodI2) metis
    hence "range ch  ?S" unfolding UNIV_def by(rule image_Collect_subsetI)
    with infinite_iff_countable_subset inj have "infinite ?S" by blast
    with fin_S have "False" by auto
  }
  thus "j. extensible R (graph_of (X j)) f" by auto
qed

fun mk_chain where
  "mk_chain sel Rs init 0 = init" |
  "mk_chain sel Rs init (Suc n) = mk_chain sel Rs (make_step sel init) n"

lemma mk_chain:
  " i. mk_chain sel Rs init (Suc i) = make_step sel (mk_chain sel Rs init i)"
proof
  fix i
  show "mk_chain sel Rs init (Suc i) = make_step sel (mk_chain sel Rs init i)"
    by (induct i arbitrary:init,auto)
qed

text ‹Algorithm 1, abstractly.›
abbreviation the_lcg where
"the_lcg sel Rs init  chain_sup (λi. graph_of (mk_chain sel Rs init i))"

lemma mk_chain_edges:
  assumes "valid_selector Rules sel"
          " ((edges o snd) ` Rules)  L × UNIV"
          "edges (graph_of G)  L × UNIV"
  shows "edges (graph_of (mk_chain sel Rules G i))  L × UNIV"
using assms(3) proof(induct i arbitrary:G)
  case 0
  then show ?case using assms(2) by auto
next
  case (Suc i G)
  hence "edges (graph_of (make_step sel G))  L × UNIV"
  proof(cases "sel G")
    case None show ?thesis unfolding None make_step_def using Suc by auto
  next
    case (Some a)
    then obtain R f where Some:"sel G = Some (R, f)" by fastforce
    hence "(a, x, y)  edges (snd R)  a  L" for a x y
      using assms(2) valid_selectorD(2)[OF assms(1) Some]
      unfolding valid_selection_def Let_def worklist_def by auto
    then show ?thesis unfolding Some make_step_def Let_def using Suc by auto
  qed
  thus ?case unfolding mk_chain.simps by(rule Suc)
qed

lemma the_lcg_edges:
  assumes "valid_selector Rules sel"
          "fst ` ( ((edges o snd) ` Rules))  L" (is "fst `?fR  _")
          "fst ` snd G  L"
  shows "fst ` edges (the_lcg sel Rules G)  L"
proof -
  from assms have "fst `?fR × UNIV  L × UNIV" "fst `(edges (graph_of G)) × UNIV  L × UNIV"
    by auto
  hence "( ((edges o snd) ` Rules))  L × UNIV" "edges (graph_of G)  L × UNIV"
    using fst_UNIV[of ?fR] fst_UNIV[of "(edges (graph_of G))"] by blast+
  note assms = assms(1) this
  have "edges (graph_of (mk_chain sel Rules G i))  L × UNIV" for i
    using mk_chain_edges[OF assms,unfolded Times_subset_cancel2[OF UNIV_I]].
  hence "edges (the_lcg sel Rules G)  L × UNIV" unfolding chain_sup_def by auto
  thus ?thesis by auto
qed

text ‹Lemma 9.›
lemma lcg_through_make_step:
assumes "finite Rs" "set_of_graph_rules Rs" "graph (graph_of init)"
        "valid_selector Rs sel"
  shows "least_consequence_graph t Rs (graph_of init) (the_lcg sel Rs init)"
proof -
  from assms have gr:"graph (graph_of (mk_chain sel Rs init 0))" by auto
  note assms = assms(1,2) this mk_chain assms(4)
  from set_of_graph_rulesD[OF assms(2)]
  have "(R. R  Rs  subgraph (fst R) (snd R)  finite_graph (fst R))" by auto
  from fair_chain_impl_consequence_graph[OF fair_through_make_step[OF assms] this]
       wpc_simpl[OF WPC_through_make_step(1)[OF assms(2-)],THEN wpc_least] 
  show ?thesis unfolding least_consequence_graph_def by auto
qed

end

Theory LabeledGraphSemantics

section ‹Semantics in labeled graphs›

theory LabeledGraphSemantics
imports LabeledGraphs
begin


text ‹GetRel describes the main way we interpret graphs: as describing a set of binary relations.›

definition getRel where
"getRel l G = {(x,y). (l,x,y)  edges G}"

lemma getRel_dom:
  assumes "graph G"
  shows "(a,b)  getRel l G  a  vertices G"
        "(a,b)  getRel l G  b  vertices G"
  using assms unfolding getRel_def by auto

lemma getRel_subgraph[simp]:
  assumes "(y, z)  getRel l G" "subgraph G G'"
  shows "(y,z)  getRel l G'" using assms by (auto simp:getRel_def subgraph_def graph_union_iff)

lemma getRel_homR: (* slows down proofs in the common case *)
  assumes "(y, z)  getRel l G" "(y,u)  f" "(z,v)  f"
  shows "(u, v)  getRel l (map_graph f G)"
  using assms by (auto simp:getRel_def on_triple_def)

lemma getRel_hom[intro]: (* faster proofs in the common case *)
  assumes "(y, z)  getRel l G" "y  vertices G" "z  vertices G"
  shows "(f y, f z)  getRel l (map_graph_fn G f)"
  using assms by (auto intro!:getRel_homR)

lemma getRel_hom_map[simp]:
  assumes "graph G"
  shows "getRel l (map_graph_fn G f) = map_prod f f ` (getRel l G)"
proof
  { fix x y
    assume a:"(x, y)  getRel l G"
    hence "x  vertices G" "y vertices G" using assms unfolding getRel_def by auto
    hence "(f x, f y)  getRel l (map_graph_fn G f)" using a by auto
  }
  then show "map_prod f f ` getRel l G  getRel l (map_graph_fn G f)" by auto
qed (cases G,auto simp:getRel_def)


text ‹The thing called term in the paper is called @{term alligorical_term} here.
      This naming is chosen because an allegory has precisely these operations, plus identity. ›
(* Deviating from the paper in having a constant constructor.
   We'll use that constructor for top, bottom, etc.. *)
datatype 'v allegorical_term
 = A_Int "'v allegorical_term" "'v allegorical_term"
 | A_Cmp "'v allegorical_term" "'v allegorical_term"
 | A_Cnv "'v allegorical_term"
 | A_Lbl (a_lbl : 'v)


text ‹The interpretation of terms, Definition 2.›
fun semantics where
"semantics G (A_Int a b) = semantics G a  semantics G b" |
"semantics G (A_Cmp a b) = semantics G a O semantics G b" |
"semantics G (A_Cnv a) = converse (semantics G a)" |
"semantics G (A_Lbl l) = getRel l G"

notation semantics (":_:⟦_" 55)

type_synonym 'v sentence = "'v allegorical_term × 'v allegorical_term"

datatype 'v Standard_Constant = S_Top | S_Bot | S_Idt | S_Const 'v

text ‹Definition 3. We don't define sentences but instead simply work with pairs of terms.›
abbreviation holds where
"holds G S  :G:⟦fst S = :G:⟦snd S"
notation holds (infix "" 55)

abbreviation subset_sentence where
"subset_sentence A B  (A,A_Int A B)"

notation subset_sentence (infix "" 60)

text ‹Lemma 1.›
lemma sentence_iff[simp]:
  "G  e1  e2 = (:G:⟦e1  :G:⟦e2)" and
  eq_as_subsets:
  "G  (e1, e2) = (G  e1  e2  G  e2  e1)"
  by auto

lemma map_graph_in[intro]:
  assumes "graph G" "(a,b)  :G:⟦e"
  shows "(f a,f b)  :map_graph_fn G f:⟦e"
  using assms by(induct e arbitrary: a b,auto intro!:relcompI)

lemma semantics_subset_vertices:
  assumes "graph A" shows ":A:⟦e  vertices A × vertices A"
  using assms by(induct e,auto simp:getRel_def)
lemma semantics_in_vertices:
  assumes "graph A" "(a,b)  :A:⟦e"
  shows "a  vertices A" "b  vertices A"
  using assms by(induct e arbitrary:a b,auto simp:getRel_def)

lemma map_graph_semantics[simp]:
  assumes "graph A" and i:"inj_on f (vertices A)"
  shows ":map_graph_fn A f:⟦e = map_prod f f ` (:A:⟦e)"
proof(induct e)
  have io:"inj_on (map_prod f f) (vertices A × vertices A)"
    using i unfolding inj_on_def by simp
  note s = semantics_subset_vertices[OF assms(1)]
  case (A_Int e1 e2) thus ?case by (auto simp:inj_on_image_Int[OF io s s]) next
  case (A_Cmp e1 e2)
  {  fix xa ya xb yb assume "(xa, ya)  :A:⟦e1" "(xb, yb)  :A:⟦e2" "f ya = f xb"
    moreover hence "ya = xb"
      using i[unfolded inj_on_def] semantics_in_vertices[OF assms(1)] by auto
    ultimately have "(f xa, f yb)  map_prod f f ` ((:A:⟦e1) O (:A:⟦e2))" by auto
  }
  with A_Cmp show ?case by auto
qed (insert assms,auto)

lemma graph_union_semantics:
  shows "(:A:⟦e)  (:B:⟦e)  :graph_union A B:⟦e"
  by(induct e,auto simp:getRel_def)

lemma subgraph_semantics:
  assumes "subgraph A B" "(a,b)  :A:⟦e"
  shows "(a,b)  :B:⟦e"
  using assms by(induct e arbitrary: a b,auto intro!:relcompI)

lemma graph_homomorphism_semantics:
  assumes "graph_homomorphism A B f" "(a,b)  :A:⟦e" "(a,a')  f" "(b,b')  f"
  shows "(a',b')  :B:⟦e"
  using assms proof(induct e arbitrary: a b a' b')
  have g:"graph A" using assms unfolding graph_homomorphism_def2 by auto
  case (A_Cmp e1 e2)
  then obtain y where y:"(a, y)  :A:⟦e1" "(y, b)  :A:⟦e2" by auto
  hence "yvertices A" using semantics_in_vertices[OF g] by auto
  with A_Cmp obtain y' where "(y,y')  f" unfolding graph_homomorphism_def by auto
  from A_Cmp(1)[OF assms(1) y(1) A_Cmp(5) this] A_Cmp(2)[OF assms(1) y(2) this A_Cmp(6)]
  show ?case by auto
next
  case (A_Lbl x) thus ?case by (auto simp:getRel_def graph_homomorphism_def2 graph_union_iff)
qed auto

lemma graph_homomorphism_nonempty:
  assumes "graph_homomorphism A B f" ":A:⟦e  {}"
  shows ":B:⟦e  {}"
proof-
  from assms have g:"graph A" unfolding graph_homomorphism_def by auto
  from assms obtain a b where ab:"(a,b)  :A:⟦e" by auto
  from semantics_in_vertices[OF g ab] obtain a' b' where
    "(a,a')  f" "(b,b')  f" using assms(1) unfolding graph_homomorphism_def by auto
  from graph_homomorphism_semantics[OF assms(1) ab this] show ?thesis by auto
qed

lemma getRel_map_fn[intro]:
  assumes "a2  vertices G" "b2  vertices G" "(a2,b2)  getRel l G"
          "f a2 = a" "f b2 = b"
        shows "(a,b)  getRel l (map_graph_fn G f)"
proof -
  from assms(1,2)
  have "((l, a2, b2), (l, f a2, f b2))  on_triple {(a, f a) |a. a  vertices G}" by auto
  thus ?thesis using assms(3-) by (simp add:getRel_def BNF_Def.Gr_def Image_def,blast)
qed
  

end

Theory StandardModels

section ‹Standard Models›
text ‹We define the kind of models we are interested in here.
      In particular, we care about standard graphs.
      To allow some reuse, we distinguish a generic version called @{term standard},
      from an instantiated abbreviation @{term standard'}.
      There is little we can prove about these definition here, except for Lemma 2.›
theory StandardModels
imports LabeledGraphSemantics Main
begin

abbreviation "a_bot  A_Lbl S_Bot"
abbreviation "a_top  A_Lbl S_Top"
abbreviation "a_idt  A_Lbl S_Idt"
notation a_bot ("")
notation a_top ("")
notation a_idt ("𝟭")
                                       
type_synonym 'v std_term = "'v Standard_Constant allegorical_term"
type_synonym 'v std_sentence = "'v std_term × 'v std_term"
type_synonym ('v,'a) std_graph = "('v Standard_Constant, ('v+'a)) labeled_graph"

abbreviation ident_rel where
"ident_rel idt G  getRel idt G = (λ x.(x,x)) ` vertices G"

lemma ident_relI[intro]:
  assumes min:" x. x  vertices G  (x,x)  getRel idt G"
  and max1:" x y. (x,y)  getRel idt G  x = y"
  and max2:" x y. (x,y)  getRel idt G  x  vertices G"
shows "ident_rel idt G"
proof
  from max1 max2 have " x y. (x,y)  getRel idt G  (x = y  x  vertices G)" by simp
  thus "getRel idt G  (λx. (x, x)) ` vertices G" by auto
  show "(λx. (x, x)) ` vertices G  getRel idt G" using min by auto
qed


text ‹Definition 4, generically.›
definition standard :: "('l × 'v) set  'l  'l  'l  ('l, 'v) labeled_graph  bool" where
"standard C b t idt G
    G = restrict G
    vertices G  {}
    ident_rel idt G
    getRel b G = {}
    getRel t G = {(x,y). xvertices G  yvertices G}
    ( (l,v)  C. getRel l G = {(v,v)})"

text ‹Definition 4.›
abbreviation standard' :: "'v set  ('v,'a) std_graph  bool" where
"standard' C  standard ((λ c. (S_Const c,Inl c)) ` C) S_Bot S_Top S_Idt"

text ‹Definition 5.›
definition model :: "'v set  ('v,'a) std_graph  ('v std_sentence) set  bool" where
"model C G T  standard' C G  ( S  T. G  S)"

text ‹Definition 5.›
abbreviation consistent :: "'b itself  'v set  ('v std_sentence) set  bool" where
"consistent _ C T   (G::('v,'b) std_graph). model C G T"

text ‹Definition 6.›
definition entails :: "'b itself  'v set  ('v std_sentence) set  'v std_sentence  bool"  where
"entails _ C T S   (G::('v,'b) std_graph). model C G T  G  S"

lemma standard_top_not_bot[intro]:
"standard' C G  :G:⟦  :G:⟦"
  unfolding standard_def by auto

text ‹Lemma 2.›
lemma consistent_iff_entails_nonsense:
"consistent t C T = (¬ entails t C T (,))"
proof
  show "consistent t C T  ¬ entails t C T (, )"
    using standard_top_not_bot unfolding entails_def model_def
    by fastforce
qed (auto simp:entails_def model_def)

end

Theory RuleSemanticsConnection

section ‹Translating terms into Graphs›
text ‹We define the translation function and its properties.›

theory RuleSemanticsConnection
imports LabeledGraphSemantics RulesAndChains
begin

text ‹Definition 15.›
fun translation :: "'c allegorical_term  ('c, nat) labeled_graph" where
"translation (A_Lbl l) = LG {(l,0,1)} {0,1}" |
"translation (A_Cnv e) = map_graph_fn (translation e) (λ x. if x<2 then (1-x) else x)" |
"translation (A_Cmp e1 e2)
  = (let G1 = translation e1 ; G2 = translation e2
     in graph_union (map_graph_fn G1 (λ x. if x=0 then 0 else x+card(vertices G2)-1))
                    (map_graph_fn G2 (λ x. if x=0 then card (vertices G2) else x)))" |
"translation (A_Int e1 e2)
  = (let G1 = translation e1 ; G2 = translation e2
     in graph_union G1 (map_graph_fn G2 (λ x. if x<2 then x else x+card(vertices G1)-2)))"

definition inv_translation where
"inv_translation r  {0..<card r} = r  {0,1}r"

lemma inv_translationI4[intro]:
  assumes "finite r" " x. x < card r  x  r"
  shows "r={0..<card r}"
proof(insert assms,induct "card r" arbitrary:r)
  case (Suc x r)
  let ?r = "r - {x}"
  from Suc have p:"x = card ?r" "finite ?r" by auto
  have p2:"xa < card ?r  xa  ?r" for xa
    using Suc.prems(2)[of xa] Suc.hyps(2) unfolding p(1)[symmetric] by auto
  from Suc.hyps(1)[OF p p2] have "?r={0..<card ?r}".
  with Suc.hyps(2) Suc.prems(1) show ?case
    by (metis atLeast0_lessThan_Suc card_Diff_singleton_if insert_Diff n_not_Suc_n p(1))
qed auto

lemma inv_translationI[intro!]:
assumes "finite r" " x. x < card r  x  r" "0  r" "Suc 0  r"
shows "inv_translation r"
proof -
  from inv_translationI4[OF assms(1,2),symmetric]
  have c:" {0..<card r} = r " by auto
  from assms(3,4) have "{0,1}  r" by auto
  with c inv_translation_def show ?thesis by auto
qed

lemma verts_in_translation_finite[intro]:
"finite (vertices (translation X))"
"finite (edges (translation X))"
"0  vertices (translation X)"
"Suc 0  vertices (translation X)"
proof(atomize(full),induction X)
  case (A_Int X1 X2)
  then show ?case by (auto simp:Let_def)
next
  case (A_Cmp X1 X2)
  then show ?case by (auto simp:Let_def)
next
  have [simp]:"{x::nat. x < 2} = {0,1}" by auto
  case (A_Cnv X)
  then show ?case by auto
qed auto

lemma inv_tr_card_min:
  assumes "inv_translation r"
  shows "card r  2" 
proof -
  note [simp] = inv_translation_def
  have "{0..<x} = r  2  x  0  r  1  r" for x by auto
  thus ge2:"card r2" using assms by auto
qed

lemma verts_in_translation[intro]:
"inv_translation (vertices (translation X))"
proof(induct X)
  { fix r
    assume assms:"inv_translation r"
    note [simp] = inv_translation_def
    from assms have a1:"finite r"
      by (intro card_ge_0_finite) auto
    have [simp]:"{0..<Suc x} = {0..<x}  {x}" for x by auto
    note ge2 = inv_tr_card_min[OF assms]
    from ge2 assms have r0:"r  {0} = {0}" "r  {x. x < 2} = {0,1}" by auto
    have [intro!]:"x. x  r  x < card r"
     and g6:"x. x < card r  x  r"
      using assms[unfolded inv_translation_def] atLeastLessThan_iff by blast+
    have g4:"r  {x. ¬ x < 2} = {2..<card r}"
            "r  (Collect ((<) 0)) = {1..<card r}" using assms by fastforce+
    have ins:"1  r" "0  r" using assms by auto
    have d:"Suc (Suc (card r - 2)) = card r"
      using ge2 One_nat_def Suc_diff_Suc Suc_pred 
            numeral_2_eq_2 by presburger
    note ge2 ins g4 g6 r0 d
  } note inv_translationD[simp] = this
  {
    fix a b c
    assume assm:"b  (a::nat)"
    have "(λx. x + a - b) ` {b..<c} = {a..<c+a-b}" (is "?lhs = ?rhs")
    proof -
      from assm have "?lhs = (λx. x + (a - b)) ` {b..<c}" by auto
      also have " = ?rhs" 
        unfolding linordered_semidom_class.image_add_atLeastLessThan' using assm by auto
      finally show ?thesis by auto
    qed
  } note e[simp] = this
  { fix r z
    assume a1: "inv_translation z" and a2: "inv_translation r"
    let ?z2 = "card z + card r - 2"
    let ?z1 = "card z + card r - Suc 0"
    from a1 a2
    have le1:"Suc 0  card r"
      by (metis Suc_leD inv_translationD(1) numerals(2))
    hence le2: "card r  ?z1"
      by (metis Suc_leD a1 inv_translationD(1) numerals(2) ordered_cancel_comm_monoid_diff_class.le_add_diff)
    with le1 have b:"{card r ..< ?z1}  {Suc 0 ..< card r} = {Suc 0 ..< ?z1}"
      by auto
    have a:"(insert (card r) {0..<card z + card r - Suc 0}) = {0..<card z + card r - Suc 0}"
      using le1 le2 a1 a2
      by (metis Suc_leD add_Suc_right atLeastLessThan_iff diff_Suc_Suc insert_absorb inv_translationD(1) linorder_not_less not_less_eq_eq numerals(2) ordered_cancel_comm_monoid_diff_class.le_add_diff)
    from a1 a2
    have "card z + card r - 2  card (r::nat set)"
      by (simp add: ordered_cancel_comm_monoid_diff_class.le_add_diff)
    with a2
    have c:"card (r  {card r..<?z2}) = ?z2"
      by (metis atLeast0LessThan card_atLeastLessThan diff_zero inv_translation_def ivl_disj_un_one(2))+
    note a b c
  } note [simp] = this
  have [simp]:"a < x  insert a {Suc a..<x} = {a..<x}" for a x by auto
  { case (A_Int X1 X2)
    let ?v1 = "vertices (translation X1)"
    from A_Int have [simp]:"(insert 0 (insert (Suc 0) (?v1  x))) = ?v1  x"
      for x unfolding inv_translation_def by auto
    from A_Int show ?case by (auto simp:Let_def linorder_not_le)
  next
    case (A_Cmp X1 X2)
    hence "2card (vertices (translation X1))" "2card (vertices (translation X2))" by auto
    hence "1 card (vertices (translation X1))" "1card (vertices (translation X2))"
          "1 < card (vertices (translation X1)) + card (vertices (translation X2)) - 1"
      by auto
    from this A_Cmp
    show ?case by (auto simp:Let_def)
  next
    case (A_Cnv X)
    thus ?case by (auto simp:Let_def)
  }
qed auto

lemma translation_graph[intro]:
"graph (translation X)"
  by (induct X, auto simp:Let_def)

lemma graph_rule_translation[intro]: (* remark at the end of Def 15 *)
"graph_rule (translation X, translation (A_Int X Y))"
  using verts_in_translation_finite[of X] verts_in_translation_finite[of "A_Int X Y"]
        translation_graph[of X] translation_graph[of "A_Int X Y"]
  by (auto simp:Let_def subgraph_def2)

lemma graph_hom_translation[intro]:
  "graph_homomorphism (LG {} {0,1}) (translation X) (Id_on {0,1})"
  using verts_in_translation[of X]
  unfolding inv_translation_def graph_homomorphism_def2 by auto

lemma translation_right_to_left:
  assumes f:"graph_homomorphism (translation e) G f" "(0, x)  f" "(1, y)  f"
  shows "(x, y)  :G:⟦e"
  using f
proof(induct e arbitrary:f x y)
case (A_Int e1 e2 f x y)
  let ?f1 = "id"
  let ?f2 = "(λ x. if x < 2 then x else x + card (vertices (translation e1)) - 2)"
  let ?G1 = "translation e1"
  let ?G2 = "translation e2"
  have f1:"(0, x)  on_graph ?G1 ?f1 O f" "(1, y)  on_graph ?G1 ?f1 O f"
   and f2:"(0, x)  on_graph ?G2 ?f2 O f" "(1, y)  on_graph ?G2 ?f2 O f"
    using A_Int.prems(2,3) by (auto simp:BNF_Def.Gr_def relcomp_def)
  from A_Int.prems(1)
  have uni:"graph_homomorphism (graph_union ?G1 (map_graph_fn ?G2 ?f2)) G f"
    by (auto simp:Let_def)
  from graph_homo_union_id(1)[OF uni translation_graph]
  have h1:"graph_homomorphism ?G1 (translation (A_Int e1 e2)) (on_graph ?G1 id)"
    by (auto simp:Let_def graph_homomorphism_def)
  have "graph (map_graph_fn ?G2 ?f2)" by auto
  from graph_homo_union_id(2)[OF uni this]
  have h2:"graph_homomorphism ?G2 (translation (A_Int e1 e2)) (on_graph ?G2 ?f2)"
    by (auto simp:Let_def graph_homomorphism_def)
  from A_Int.hyps(1)[OF graph_homomorphism_composes[OF h1 A_Int.prems(1)] f1]
       A_Int.hyps(2)[OF graph_homomorphism_composes[OF h2 A_Int.prems(1)] f2]
  show ?case by auto
next
  case (A_Cmp e1 e2 f x y)
  let ?f1 =  "(λ x. if x=0 then 0 else x+card(vertices (translation e2))-1)"
  let ?f2 =  "(λ x. if x=0 then card (vertices (translation e2)) else x)" 
  let ?G1 = "translation e1"
  let ?G2 = "translation e2"
  let ?v = "card (vertices (translation e2))"
  from A_Cmp.prems(1) have "?v  Domain f" by (auto simp:Let_def graph_homomorphism_def)
  then obtain v where v:"(?v,v)  f" by auto
  have f1:"(0, x)  on_graph ?G1 ?f1 O f" "(1, v)  on_graph ?G1 ?f1 O f"
   and f2:"(0, v)  on_graph ?G2 ?f2 O f" "(1, y)  on_graph ?G2 ?f2 O f"
    using A_Cmp.prems(2,3) v by auto
  from A_Cmp.prems(1)
  have uni:"graph_homomorphism (graph_union (map_graph_fn ?G1 ?f1) (map_graph_fn ?G2 ?f2)) G f"
    by (auto simp:Let_def)
  have "graph (map_graph_fn ?G1 ?f1)" by auto
  from graph_homo_union_id(1)[OF uni this]
  have h1:"graph_homomorphism ?G1 (translation (A_Cmp e1 e2)) (on_graph ?G1 ?f1)"
    by (auto simp:Let_def graph_homomorphism_def2)
  have "graph (map_graph_fn ?G2 ?f2)" by auto
  from graph_homo_union_id(2)[OF uni this]
  have h2:"graph_homomorphism ?G2 (translation (A_Cmp e1 e2)) (on_graph ?G2 ?f2)"
    by (auto simp:Let_def graph_homomorphism_def2)
  from A_Cmp.hyps(1)[OF graph_homomorphism_composes[OF h1 A_Cmp.prems(1)] f1]
       A_Cmp.hyps(2)[OF graph_homomorphism_composes[OF h2 A_Cmp.prems(1)] f2]
  show ?case by auto
next
  case (A_Cnv e f x y)
  let ?f = "(λ x. if x < 2 then 1 - x else x)"
  let ?G = "translation e"
  have i:"graph_homomorphism ?G (map_graph_fn ?G ?f) (on_graph ?G ?f)" using A_Cnv by auto
  have "(0, y)  on_graph ?G ?f O f" "(1, x)  on_graph ?G ?f O f"
    using A_Cnv.prems(3,2) by (auto simp:BNF_Def.Gr_def relcomp_def)
  from A_Cnv.hyps(1)[OF graph_homomorphism_composes[OF i] this] A_Cnv.prems(1)
  show ?case by auto
next
case (A_Lbl l f x y)
  hence "edge_preserving f {(l,0,1)} (edges G)" unfolding graph_homomorphism_def by auto
  with A_Lbl(2,3) show ?case by (auto simp:getRel_def edge_preserving_def)
qed

lemma translation_homomorphism:
  assumes "graph_homomorphism (translation e) G f"
  shows "f `` {0} × f `` {1}  :G:⟦e" ":G:⟦e  {}"
  using translation_right_to_left[OF assms] assms[unfolded graph_homomorphism_def2]
        verts_in_translation_finite[of e] by auto

text ‹Lemma 5.›
lemma translation:
  assumes "graph G"
  shows "(x, y)  :G:⟦e  ( f. graph_homomorphism (translation e) G f  (0,x)  f  (1,y)  f)"
(is "?lhs = ?rhs")
proof
  have [dest]:"y + card (vertices (translation (e::'a allegorical_term))) - 2 < 2  (y::nat) < 2"
    for y e using inv_tr_card_min[OF verts_in_translation,of e] by linarith
  {  fix y fix e::"'a allegorical_term"
     assume "y + card (vertices (translation e)) - 2  vertices (translation e)"
     hence "y + card (vertices (translation e)) - 2 < card (vertices (translation e))"
       using verts_in_translation[of e,unfolded inv_translation_def] by auto
     hence "y < 2" using inv_tr_card_min[OF verts_in_translation,of e] by auto
  } note [dest!] = this
  {  fix y fix e::"'a allegorical_term"
     assume "y + card (vertices (translation e)) - Suc 0  vertices (translation e)"
     hence "y + card (vertices (translation e)) - Suc 0  {0..<card (vertices (translation e))}"
       using verts_in_translation[of e,unfolded inv_translation_def] by simp
     hence "y = 0" using inv_tr_card_min[OF verts_in_translation,of e] by auto
   } note [dest!] = this
   {  fix y fix e::"'a allegorical_term"
     assume "card (vertices (translation e))  vertices (translation e)"
     hence "card (vertices (translation e))  {0..<card (vertices (translation e))}"
       using verts_in_translation[of e,unfolded inv_translation_def] by auto
     hence "False" by auto
   } note [dest!] = this
  {  fix y fix e::"'a allegorical_term"
     assume "y + card (vertices (translation e))  Suc 0"
     hence " card (vertices (translation e))  Suc 0" by auto
     hence "False" using inv_tr_card_min[OF verts_in_translation[of e]] by auto
   } note [dest!] = this
  assume ?lhs
  then show ?rhs
  proof(induct e arbitrary:x y)
    case (A_Int e1 e2)
    from A_Int have assm:"(x, y)  :G:⟦e1" "(x, y)  :G:⟦e2" by auto
    from A_Int(1)[OF assm(1)] obtain f1 where
      f1:"graph_homomorphism (translation e1) G f1" "(0, x)  f1" "(1, y)  f1" by auto
    from A_Int(2)[OF assm(2)] obtain f2 where
      f2:"graph_homomorphism (translation e2) G f2" "(0, x)  f2" "(1, y)  f2" by auto
    from f1 f2 have v:"Domain f1 = vertices (translation e1)" "Domain f2 = vertices (translation e2)"
      unfolding graph_homomorphism_def by auto
    let ?f2 = "(λ x. if x < 2 then x else x + card (vertices (translation e1)) - 2)"
    let ?tr2 = "on_graph (translation e2) ?f2"
    have inj2:"inj_on ?f2 (vertices (translation e2))" unfolding inj_on_def by auto
    have "(0,0)  ?tr2¯" "(1,1)  ?tr2¯" by auto
    from this[THEN relcompI] f2(2,3) 
    have zero_one:"(0,x)  ?tr2¯ O f2"
                  "(1,y)  ?tr2¯ O f2" by auto
    { fix yb zb
      assume "(yb + card (vertices (translation e1)) - 2, zb)  f1"
      hence "yb + card (vertices (translation e1)) - 2  vertices (translation e1)" using v by auto
    } note in_f[dest!] = this
    have d_a:"Domain f1   Domain (?tr2¯ O f2) = {0,1}"
      using zero_one by (auto simp:v)
    have d_b:"Domain (f1  ?tr2¯ O f2) = {0,1}"
      using zero_one f1(2,3) by auto
    note cmp2 = graph_homomorphism_composes[OF graph_homo_inv[OF translation_graph inj2] f2(1)]
    have "graph_homomorphism (translation (A_Int e1 e2)) G (f1  ?tr2¯ O f2)"
      using graph_homo_union[OF f1(1) cmp2 d_a[folded d_b]]
      by (auto simp:Let_def)
    thus ?case using zero_one[THEN UnI2[of _ _ "f1"]] by blast
  next
    case (A_Cmp e1 e2)
    from A_Cmp obtain z where assm:"(x, z)  :G:⟦e1" "(z, y)  :G:⟦e2" by auto
    from A_Cmp(1)[OF assm(1)] obtain f1 where
      f1:"graph_homomorphism (translation e1) G f1" "(0, x)  f1" "(1, z)  f1" by auto
    from A_Cmp(2)[OF assm(2)] obtain f2 where
      f2:"graph_homomorphism (translation e2) G f2" "(0, z)  f2" "(1, y)  f2" by auto
    from f1 f2 have v:"Domain f1 = vertices (translation e1)" "Domain f2 = vertices (translation e2)"
      unfolding graph_homomorphism_def by auto
    let ?f1 = "(λ x. if x=0 then 0 else x+card(vertices (translation e2))-1)"
    let ?f2 = "(λ x. if x=0 then card (vertices (translation e2)) else x)"
    let ?tr1 = "on_graph (translation e1) ?f1"
    let ?tr2 = "on_graph (translation e2) ?f2"
    have inj1:"inj_on ?f1 (vertices (translation e1))" unfolding inj_on_def by auto
    have inj2:"inj_on ?f2 (vertices (translation e2))" unfolding inj_on_def by auto
    have "(card (vertices (translation e2)),0)  ?tr2¯" "(1,1)  ?tr2¯"
         "(0,0)  ?tr1¯" "(card (vertices (translation e2)),1)  ?tr1¯" by auto
    from this[THEN relcompI] f2(2,3) f1(2,3) 
    have zero_one:"(card (vertices (translation e2)),z)  ?tr1¯ O f1"
                  "(0,x)  ?tr1¯ O f1"
                  "(card (vertices (translation e2)),z)  ?tr2¯ O f2"
                  "(1,y)  ?tr2¯ O f2" by auto
    have [simp]:
        "ye  vertices (translation e2) 
       (if ye = 0 then card (vertices (translation e2)) else ye) =
       (if yd = 0 then 0 else yd + card (vertices (translation e2)) - 1)  ye = 0  yd = 1"
        for ye yd using v inv_tr_card_min[OF verts_in_translation,of "e2"]
        by(cases "ye=0";cases "yd=0";auto)
    have d_a:"Domain (?tr1¯ O f1)   Domain (?tr2¯ O f2) = {card (vertices (translation e2))}"
      using zero_one using [[simproc del: defined_all]] by (auto simp: v)
    have d_b:"Domain (?tr1¯ O f1  ?tr2¯ O f2) = {card (vertices (translation e2))}"
      using zero_one f1(2,3) using [[simproc del: defined_all]] by auto
    note cmp1 = graph_homomorphism_composes[OF graph_homo_inv[OF translation_graph inj1] f1(1)]
    note cmp2 = graph_homomorphism_composes[OF graph_homo_inv[OF translation_graph inj2] f2(1)]
    have "graph_homomorphism (translation (A_Cmp e1 e2)) G (?tr1¯ O f1  ?tr2¯ O f2)"
      unfolding Let_def translation.simps
      by (rule graph_homo_union[OF cmp1 cmp2 d_a[folded d_b]])
    thus ?case using zero_one by blast
  next
    case (A_Cnv e)
    let ?G = "translation (A_Cnv e)"
    from A_Cnv obtain f where
      f:"graph_homomorphism (translation e) G f" "(0, y)  f" "(1, x)  f" by auto
    hence v:"Domain f = vertices (translation e)"
      unfolding graph_homomorphism_def by auto
    define n where "n  card (vertices (translation e))"
    from verts_in_translation f inv_tr_card_min[OF verts_in_translation] v(1)
    have n:"vertices (translation e) = {0..<n}" "{0..<n}  {x. x < 2} = {1,0}"
      "Domain f = {0..<n}" "{0..<n}  {x. ¬ x < 2} = {2..<n}"
      and n2: "n  2"
      by (auto simp:n_def inv_translation_def)
    then have [simp]:"insert (Suc 0) {2..<n} = {1..<n}"
      "insert 0 {Suc 0..<n} = {0..<n}" using [[simproc del: defined_all]] by auto
    let ?f = "on_graph ?G (λ x. if x < 2 then 1 - x else x)"
    have h:"graph_homomorphism ?G G (?f O f)"
    proof(rule graph_homomorphism_composes[OF _ f(1)],rule graph_homomorphismI)
      show "vertices ?G = Domain ?f"
        by (auto simp:Domain_int_univ)
      show "?f `` vertices ?G  vertices (translation e)" using n2 by auto
      show "univalent ?f" by auto
      show "edge_preserving ?f (edges (translation (A_Cnv e))) (edges (translation e))"
        by (rule edge_preserving_on_graphI,auto simp: BNF_Def.Gr_def)
    qed (auto intro:assms)
    have xy:"(0, x)  ?f O f" "(1, y)  ?f O f" using n2 f(2,3) n(1,2) by auto
    with h show ?case by auto
  next
    case (A_Lbl l)
    let ?f = "{(0,x),(1,y)}"
    have xy:"x  vertices G" "y  vertices G" using assms A_Lbl by (auto simp:getRel_def)
    have "graph_homomorphism (translation (A_Lbl l)) G ?f  (0, x)  ?f  (1, y)  ?f"
      using assms A_Lbl xy unfolding graph_homomorphism_def2
      by (auto simp:univalent_def getRel_def on_triple_def Image_def graph_union_def insert_absorb)
    then show ?case by auto
  qed
qed (insert translation_right_to_left,auto)

abbreviation transl_rule ::
    "'a sentence  ('a, nat) labeled_graph × ('a, nat) labeled_graph" where
"transl_rule R  (translation (fst R),translation (snd R))"

text ‹Lemma 6.›
lemma maintained_holds_iff:
  assumes "graph G"
  shows "maintained (translation eL,translation (A_Int eL eR)) G  G  eL  eR" (is "?rhs = ?lhs")
proof
  assume lhs:?lhs
  show ?rhs unfolding maintained_def proof(clarify) fix f
    assume f:"graph_homomorphism (fst (translation eL, translation (A_Int eL eR))) G f"
    then obtain x y where f2:"(0,x)  f" "(1,y)  f" unfolding graph_homomorphism_def
      by (metis DomainE One_nat_def prod.sel(1) verts_in_translation_finite(3,4))
    with f have "(x,y)  :G:⟦fst (eL  eR)" unfolding translation[OF assms] by auto
    with lhs have "(x,y)  :G:⟦snd (eL  eR)" by auto
    then obtain g where g: "graph_homomorphism (translation (A_Int eL eR)) G g"
                   and g2: "(0, x)  g" "(1, y)  g" unfolding translation[OF assms] by auto
    have v:"vertices (translation (A_Int eL eR)) = Domain g"
           "vertices (translation eL) = Domain f" using f g
      unfolding graph_homomorphism_def by auto
    from subgraph_subset[of "translation eL" "translation (A_Int eL eR)"]
         graph_rule_translation[of eL eR]
    have dom_sub: "Domain f  Domain g"
      using v unfolding prod.sel by argo
    hence dom_le:"card (Domain f)  card (Domain g)"
      by (metis card.infinite card_mono inv_tr_card_min not_less rel_simps(51) v(1) verts_in_translation)
    have c_f:"card (Domain f)  2" using inv_tr_card_min[OF verts_in_translation] v by metis
    from f[unfolded graph_homomorphism_def]
    have ep_f:"edge_preserving f (edges (translation eL)) (edges G)"
     and uni_f:"univalent f" by auto
    let ?f = "(λx. if x < 2 then x else x + card (vertices (translation eL)) - 2)"
    define GR where "GR = map_graph_fn (translation eR) ?f"
    from g[unfolded graph_homomorphism_def]
    have "edge_preserving g (edges (translation (A_Int eL eR))) (edges G)"
     and uni_g:"univalent g" by auto
    from edge_preserving_subset[OF subset_refl _ this(1)]
    have ep_g:"edge_preserving g (edges GR) (edges G)" by (auto simp:Let_def GR_def)
    { fix a assume a:"a  vertices (translation eR)"
      hence "?f a  vertices (translation (A_Int eL eR))" by (auto simp:Let_def)
      from this[unfolded v] verts_in_translation[of "A_Int eL eR",unfolded inv_translation_def v] 
      have "¬ a < 2  a + card (Domain f) - 2 < card (Domain g)" by auto
    } note[intro!] = this
    have [intro!]: " ¬ aa < 2  card (Domain f)  aa + card (Domain f) - 2" for aa by simp
    from v(2) restrictD[OF translation_graph[of eL]]
    have df[dest]:"xa  Domain f  (l,xa,xb)  edges (translation eL)  False"
                  "xa  Domain f  (l,xb,xa)  edges (translation eL)  False"
                  for xa l xb unfolding edge_preserving by auto
    { fix l xa xb ya
      assume assm: "(l,xa,xb)  edges GR"
      with c_f dom_le
      have "xa  {0,1}  {card (Domain f)..<card (Domain g)}"
           "xb  {0,1}  {card (Domain f)..<card (Domain g)}"
        unfolding GR_def v by auto
      hence minb:"xa  {0,1}  xa  card (Domain f)" "xb  {0,1}  xb  card (Domain f)"
        by auto
      { fix z xa assume minb:"xa  {0,1}  xa  card (Domain f)" and z:"(xa,z)  f" 
        from z verts_in_translation[of eL,unfolded inv_translation_def v] 
        have "xa < card(Domain f)" by auto
        with minb verts_in_translation[of "A_Int eL eR",unfolded inv_translation_def v]
        have x:"xa  {0,1}  xa  Domain g" by auto
        then obtain v where g:"(xa,v)  g" by auto
        consider "xa = 0  z = x" | "xa = 1  z = y"
          using x f2[THEN univalentD[OF uni_f]] z by auto
        hence "v = z" using g g2[THEN univalentD[OF uni_g]] by metis
        hence "(xa,z)  g" using g by auto
      }
      note minb[THEN this]
    }
    with f2 g2[THEN univalentD[OF uni_g]]
    have dg:"(l,xa,xb)  edges GR  (xa,ya)  f  (xa,ya)  g"
            "(l,xb,xa)  edges GR  (xa,ya)  f  (xa,ya)  g"
            for xa l xb ya
      unfolding edge_preserving by (auto)
    have "vertices (translation eL)  vertices (translation (A_Int eL eR))"
      by(rule subgraph_subset,insert graph_rule_translation,auto)
    hence subdom:"Domain f  Domain g" unfolding v.
    let ?g = "f  (Id_on (UNIV - Domain f) O g)"
    have [simp]:"Domain ?g = Domain g" using subdom unfolding Domain_Un_eq by auto
    have ih:"graph_homomorphism (translation (A_Int eL eR)) G ?g"
    proof(rule graph_homomorphismI)
      show "?g `` vertices (translation (A_Int eL eR))  vertices G"
        using g[unfolded graph_homomorphism_def] f[unfolded graph_homomorphism_def]
        by (auto simp: v simp del:translation.simps)
      show "edge_preserving ?g (edges (translation (A_Int eL eR))) (edges G)"
        unfolding Let_def translation.simps graph_union_edges proof
        show "edge_preserving ?g (edges (translation eL)) (edges G)"
          using edge_preserving_atomic[OF ep_f] unfolding edge_preserving by auto
        have "edge_preserving ?g (edges GR) (edges G)"
          using edge_preserving_atomic[OF ep_g] dg unfolding edge_preserving by (auto;blast)
        thus "edge_preserving ?g (edges (map_graph_fn (translation eR) ?f)) (edges G)"
          by (auto simp:GR_def)
        qed
    qed (insert f[unfolded graph_homomorphism_def] g[unfolded graph_homomorphism_def],auto simp:Let_def)
    have ie:"agree_on (translation eL) f ?g" unfolding agree_on_def by (auto simp:v)
    from ie ih show "extensible (translation eL, translation (A_Int eL eR)) G f"
      unfolding extensible_def prod.sel by auto
  qed next
  assume rhs:?rhs
  { fix x y assume "(x,y)  :G:⟦eL"
    with translation[OF assms] obtain f
      where f:"graph_homomorphism (fst (translation eL, translation (A_Int eL eR))) G f"
              "(0, x)  f" "(1, y)  f" by auto
    with rhs[unfolded maintained_def,rule_format,OF f(1),unfolded extensible_def]
    obtain g where g:"graph_homomorphism (translation (A_Int eL eR)) G g"
                     "agree_on (translation eL) f g" by auto
    hence "(x,y)  :G:⟦A_Int eL eR" using f unfolding agree_on_def translation[OF assms] by auto
  }
  thus ?lhs by auto
qed

lemma translation_self[intro]:
"(0, 1)  :translation e:⟦e"
proof(induct e)
  case (A_Int e1 e2)
  let ?f = "(λx. if x < 2 then x else x + card (vertices (translation e1)) - 2)"
  have f: "(?f 0,?f 1) :map_graph_fn (translation e2) ?f:⟦e2"
    using map_graph_in[OF translation_graph A_Int(2),of ?f] by auto
  let ?G = "graph_union (translation e1) (map_graph_fn (translation e2) ?f)"
  have "{(0,1)}  :(translation e1):⟦e1" using A_Int by auto
  moreover have "{(0,1)}  :map_graph_fn (translation e2) ?f:⟦e2" using f by auto
  moreover have ":map_graph_fn (translation e2) ?f:⟦e2  :?G:⟦e2" ":translation e1:⟦e1  :?G:⟦e1"
    using graph_union_semantics by blast+
  ultimately show ?case by (auto simp:Let_def)
next
  case (A_Cmp e1 e2)
  let ?f1 = "λx. if x = 0 then 0 else x + card (vertices (translation e2)) - 1"
  have f1: "(?f1 0,?f1 1) :map_graph_fn (translation e1) ?f1:⟦e1"
    using map_graph_in[OF translation_graph A_Cmp(1),of ?f1] by auto
  let ?f2 = "λx. if x = 0 then card (vertices (translation e2)) else x"
  have f2: "(?f2 0,?f2 1) :map_graph_fn (translation e2) ?f2:⟦e2"
    using map_graph_in[OF translation_graph A_Cmp(2),of ?f2] by auto
  let ?G = "graph_union (map_graph_fn (translation e1) ?f1) (map_graph_fn (translation e2) ?f2)"
  have "{(0,1)} = {(0,card (vertices (translation e2)))} O {(card (vertices (translation e2)),1)}"
    by auto
  also have "{(0,card (vertices (translation e2)))}  :map_graph_fn (translation e1) ?f1:⟦e1"
    using f1 by auto
  also have ":map_graph_fn (translation e1) ?f1:⟦e1  :?G:⟦e1"
    using graph_union_semantics by auto
  also have "{(card (vertices (translation e2)),1)}  :map_graph_fn (translation e2) ?f2:⟦e2"
    using f2 by auto
  also have ":map_graph_fn (translation e2) ?f2:⟦e2  :?G:⟦e2"
    using graph_union_semantics by blast
  also have "(:?G:⟦e1) O (:?G:⟦e2) = :translation (A_Cmp e1 e2):⟦A_Cmp e1 e2"
    by (auto simp:Let_def)
  finally show ?case by auto
next
  case (A_Cnv e)
  from map_graph_in[OF translation_graph this,of "(λx. if x < (2::nat) then 1 - x else x)"]
  show ?case using map_graph_in[OF translation_graph] by auto
qed (simp add:getRel_def)

text ‹Lemma 6 is only used on rules of the form @{term "eL  eR"}.
      The requirement of G being a graph can be dropped for one direction.›
lemma maintained_holds[intro]:
  assumes ":G:⟦eL  :G:⟦eR" 
  shows "maintained (transl_rule (eL  eR)) G"
proof (cases "graph G")
  case True
  thus ?thesis using assms sentence_iff maintained_holds_iff prod.sel by metis
next
  case False
  thus ?thesis by (auto simp:maintained_def graph_homomorphism_def)
qed

lemma maintained_holds_subset_iff[simp]:
  assumes "graph G"
  shows "maintained (transl_rule (eL  eR)) G  (:G:⟦eL  :G:⟦eR)"
  using assms maintained_holds_iff sentence_iff prod.sel by metis

end

Theory StandardRules

section ‹Standard Rules›
text ‹We define the standard rules here, and prove the relation to standard rules.
      This means proving that the graph rules do what they say they do.›
theory StandardRules
imports StandardModels RuleSemanticsConnection
begin


text ‹Definition 16 makes this remark. We don't have a specific version of Definition 16.›
lemma conflict_free:
":G:⟦A_Lbl l = {}  ( (l',x,y)edges G. l'  l)"
  by (auto simp:getRel_def)


text ‹Definition 17, abstractly.
      It's unlikely that we wish to use the top rule for any symbol except top,
      but stating it abstractly makes it consistent with the other rules.›
(* Definition 17 *)
definition top_rule :: "'l  ('l,nat) Graph_PreRule" where	
"top_rule t = (LG {} {0,1},LG {(t,0,1)} {0,1})"	

text ‹Proof that definition 17 does what it says it does.›
lemma top_rule[simp]:
  assumes "graph G"
  shows "maintained (top_rule r) G  vertices G × vertices G = getRel r G"
proof
  assume a:"maintained (top_rule r) G"
  { fix a b assume "a  vertices G" "b  vertices G"
    hence "graph_homomorphism (LG {} {0, 1}) G {(0::nat,a),(1,b)}"
      using assms unfolding graph_homomorphism_def univalent_def by auto
    with a[unfolded maintained_def top_rule_def] extensible_refl_concr
    have "graph_homomorphism (LG {(r, 0, 1)} {0::nat, 1}) G {(0::nat, a), (1, b)}" by simp
    hence "(a, b)  getRel r G"
      unfolding graph_homomorphism_def2 graph_union_iff getRel_def by auto
  }
  thus "vertices G × vertices G = getRel r G" using getRel_dom[OF assms] by auto next
  assume a:"vertices G × vertices G = getRel r G"
  { fix f assume a2:"graph_homomorphism (fst (top_rule r)) G f"
    hence f:"f `` {0, 1}  vertices G" "on_triple f `` {}  edges G"
          "univalent f" "Domain f = {0, 1}"
      unfolding top_rule_def prod.sel graph_homomorphism_concr_graph[OF assms graph_empty_e]
      by argo+
    from a2 have ih:"graph_homomorphism (LG {} {0, 1}) G f" unfolding top_rule_def by auto
    have "extensible (top_rule r) G f" unfolding top_rule_def extensible_refl_concr[OF ih]
      graph_homomorphism_concr_graph[OF assms graph_single]
      using f a[unfolded getRel_def] by fastforce
  }
  thus "maintained (top_rule r) G" unfolding maintained_def by auto
qed

text ‹Definition 18.›
(* Definition 18 *)
definition nonempty_rule :: "('l,nat) Graph_PreRule" where
"nonempty_rule = (LG {} {},LG {} {0})"	

text ‹Proof that definition 18 does what it says it does.›
lemma nonempty_rule[simp]:
  assumes "graph G"
  shows "maintained nonempty_rule G  vertices G  {}"
proof -
  have "vertices G = {}  graph_homomorphism (LG {} {0}) G x  False"
       "v  vertices G  graph_homomorphism (LG {} {0}) G {(0,v)}"
       for v::"'b" and x::"(nat × 'b) set"
    unfolding graph_homomorphism_concr_graph[OF assms graph_empty_e] univalent_def by blast+
  thus ?thesis unfolding nonempty_rule_def maintained_def extensible_def by (auto intro:assms)
qed


text ‹Definition 19.›
definition reflexivity_rule :: "'l  ('l,nat) Graph_PreRule" where
  "reflexivity_rule t = (LG {} {0},LG {(t,0,0)} {0})"	
definition symmetry_rule :: "'l  ('l,nat) Graph_PreRule" where
"symmetry_rule t = (transl_rule (A_Cnv (A_Lbl t)  A_Lbl t))"
definition transitive_rule :: "'l  ('l,nat) Graph_PreRule" where
"transitive_rule t = (transl_rule (A_Cmp (A_Lbl t) (A_Lbl t)  A_Lbl t))"
definition congruence_rule :: "'l  'l  ('l,nat) Graph_PreRule" where
"congruence_rule t l = (transl_rule (A_Cmp (A_Cmp (A_Lbl t) (A_Lbl l)) (A_Lbl t)  A_Lbl l))"
abbreviation congruence_rules :: "'l  'l set  ('l,nat) Graph_PreRule set"
    where
"congruence_rules t L  congruence_rule t ` L"

lemma are_rules[intro]:
"graph_rule nonempty_rule"	
"graph_rule (top_rule t)"	
"graph_rule (reflexivity_rule i)"	
  unfolding reflexivity_rule_def top_rule_def nonempty_rule_def graph_homomorphism_def	
  by auto


text ‹Just before Lemma 7, we remark that if I is an identity, it maintains the identity rules.›

lemma ident_rel_refl:
  assumes "graph G" "ident_rel idt G"
  shows "maintained (reflexivity_rule idt) G"
  unfolding reflexivity_rule_def
proof(rule maintainedI) fix f
  assume "graph_homomorphism (LG {} {0::nat}) G f"
  hence f:"Domain f = {0}" "graph G" "f `` {0}  vertices G" "univalent f"
    unfolding graph_homomorphism_def by force+
  from assms(2) univalentD[OF f(4)] f(3)
  have "edge_preserving f {(idt, 0, 0)} (edges G)" unfolding edge_preserving
    by (auto simp:getRel_def set_eq_iff image_def)
  with f have "graph_homomorphism (LG {(idt, 0, 0)} {0}) G f"
              "agree_on (LG {} {0}) f f" using assms
    unfolding graph_homomorphism_def labeled_graph.sel agree_on_def univalent_def
    by auto
  then show "extensible (LG {} {0}, LG {(idt, 0, 0)} {0}) G f"
    unfolding extensible_def prod.sel by auto
qed

lemma
  assumes "ident_rel idt G"
  shows ident_rel_trans:"maintained (transitive_rule idt) G"
    and ident_rel_symm :"maintained (symmetry_rule idt) G"
    and ident_rel_cong :"maintained (congruence_rule idt l) G"
  unfolding transitive_rule_def symmetry_rule_def congruence_rule_def
  by(intro maintained_holds,insert assms,force)+

text ‹Definition 19.›
definition identity_rules ::
  "'a Standard_Constant set  (('a Standard_Constant, nat) Graph_PreRule) set" where
  "identity_rules L  {reflexivity_rule S_Idt,transitive_rule S_Idt,symmetry_rule S_Idt}
                        congruence_rules S_Idt L"

lemma identity_rules_graph_rule:
  assumes "x  identity_rules L"
  shows "graph_rule x"
proof -
  from graph_rule_translation
  have gr:" u v . graph_rule (transl_rule (u  v))" by auto
  consider "x = reflexivity_rule S_Idt" | "x = transitive_rule S_Idt" | "x = symmetry_rule S_Idt"
    |  " v w. x = congruence_rule v w" using assms unfolding identity_rules_def Un_iff by blast
  thus ?thesis using gr are_rules(3)
    unfolding congruence_rule_def transitive_rule_def symmetry_rule_def
    by cases fast+
qed

text ‹Definition 19, showing that the properties indeed do what they claim to do.›
lemma
  assumes g[intro]:"graph (G :: ('a, 'b) labeled_graph)"
  shows reflexivity_rule: "maintained (reflexivity_rule l) G  refl_on (vertices G) (getRel l G)"
    and transitive_rule: "maintained (transitive_rule l) G  trans (getRel l G)"
    and symmetry_rule: "maintained (symmetry_rule l) G  sym (getRel l G)"
proof -
  { from assms have gr:"getRel l G  vertices G × vertices G" by (auto simp:getRel_def)
    assume m:"maintained (reflexivity_rule l) G" (is "maintained ?r G")
    note [simp] = reflexivity_rule_def
    show r:"refl_on (vertices G) (getRel l G)"
    proof(rule refl_onI[OF gr]) fix x
      assume assm:"x  vertices G"  define f where "f = {(0::nat,x)}"
      have "graph_homomorphism (fst ?r) G f" using assm
        by (auto simp:graph_homomorphism_def univalent_def f_def)
      from m[unfolded maintained_def] this 
      obtain g::"(nat×'b) set"
        where g:"graph_homomorphism (snd ?r) G g"
                "agree_on (fst ?r) f g"
        unfolding extensible_def by blast
      have " n v. (n,v)  g  (n = 0)  (v = x)" using g unfolding
        agree_on_def graph_homomorphism_def f_def by auto
      with g(2) have "g = {(0,x)}" unfolding agree_on_def f_def by auto
      with g(1) show "(x,x) getRel l G"
        unfolding graph_homomorphism_def edge_preserving getRel_def by auto
    qed
  }
  { assume m:"maintained (transitive_rule l) G"
    from m[unfolded maintained_holds_subset_iff[OF g] transitive_rule_def]
    show "trans (getRel l G)" unfolding trans_def by auto
  }
  { assume m:"maintained (symmetry_rule l) G"
    from m[unfolded maintained_holds_subset_iff[OF g] symmetry_rule_def]
    show "sym (getRel l G)" unfolding sym_def by auto
  }
qed

lemma finite_identity_rules[intro]:
  assumes "finite L"
  shows "finite (identity_rules L)"
  using assms unfolding identity_rules_def by auto

lemma equivalence:
  assumes gr:"graph G" and m:"maintainedA {reflexivity_rule I,transitive_rule I,symmetry_rule I} G"
  shows "equiv (vertices G) (getRel I G)"
proof(rule equivI)
  show "refl_on (vertices G) (getRel I G)" using m by(intro reflexivity_rule[OF gr],auto)
  show "sym (getRel I G)" using m by(intro symmetry_rule[OF gr],auto)
  show "trans (getRel I G)" using m by(intro transitive_rule[OF gr],auto)
qed

lemma congruence_rule:
 (* Transitivity is not needed for this proof, but it's more convenient to reuse in this form *)
  assumes g:"graph G"
      and mA:"maintainedA {reflexivity_rule I,transitive_rule I,symmetry_rule I} G"
      and m:"maintained (congruence_rule I l) G"
    shows "(λ v. getRel l G `` {v}) respects (getRel I G)" (is "?g1")
      and "(λ v. (getRel l G)¯ `` {v}) respects (getRel I G)" (is "?g2")
proof -
  (* Both parts of this lemma are proved using roughly the same proof. *)
  note eq = equivalence[OF g mA]
  { fix y z
    assume aI:"(y, z)getRel I G"
    hence a2:"(z, y)getRel I G" using eq[unfolded equiv_def sym_def] by auto
    hence a3:"(z, z)getRel I G" "(y, y)getRel I G"
      using eq[unfolded equiv_def refl_on_def] by auto
    { fix x
      { assume al:"(y,x)  getRel l G"
        hence "x  vertices G" using g unfolding getRel_def by auto
        hence r:"(x,x)  getRel I G" using eq[unfolded equiv_def refl_on_def] by auto
        note relcompI[OF relcompI[OF a2 al] r]
      } note yx = this
      { assume al:"(z,x)  getRel l G"
        hence "x  vertices G" using g unfolding getRel_def by auto
        hence r:"(x,x)  getRel I G" using eq[unfolded equiv_def refl_on_def] by auto
        note relcompI[OF relcompI[OF aI al] r]
      } note zx = this
      from zx yx m[unfolded maintained_holds_subset_iff[OF g] congruence_rule_def]
      have "(y,x)  getRel l G  (z,x)  getRel l G" by auto
    } note v1 = this
    { fix x
      { assume al:"(x,y)  getRel l G"
        hence "x  vertices G" using g unfolding getRel_def by auto
        hence r:"(x,x)  getRel I G" using eq[unfolded equiv_def refl_on_def] by auto
        note relcompI[OF relcompI[OF r al] aI]
      } note yx = this
      { assume al:"(x,z)  getRel l G"
        hence "x  vertices G" using g unfolding getRel_def by auto
        hence r:"(x,x)  getRel I G" using eq[unfolded equiv_def refl_on_def] by auto
        note relcompI[OF relcompI[OF r al] a2]
      } note zx = this
      from zx yx m[unfolded maintained_holds_subset_iff[OF g] congruence_rule_def]
      have "(x,y)  getRel l G  (x,z)  getRel l G" by auto
    } note v2 = this
    from v1 v2
    have "getRel l G `` {y} = getRel l G `` {z}"
         "(getRel l G)¯ `` {y} = (getRel l G)¯ `` {z}" by auto
  }
  thus ?g1 ?g2 unfolding congruent_def by force+
qed


text ‹Lemma 7, strengthened with an extra property to make subsequent proofs easier to carry out.›
lemma identity_rules:
  assumes "graph G"
          "maintainedA (identity_rules L) G"
          "fst ` edges G  L"
  shows " f. f o f = f
          ident_rel S_Idt (map_graph_fn G f)
          subgraph (map_graph_fn G f) G
          ( l x y. (l,x,y)  edges G  (l,f x,f y)  edges G)"
proof -
  (* While this proof defines a concrete f, we only expose it using an existential quantifier.
     The reason is that the f of our choice is non-constructive,
     and its definition relies on the axiom of choice.
     In fact, this theorem applies to the infinite case too,
     which means that it's probably equivalent to the axiom of choice.
     We therefore have no hopes of giving an executable concrete f here.
     In the implementation, we will be able to use finiteness of G (which is not required here),
     and therefore we can construct an f with these properties again.
     Unfortunately, this does mean doing roughly the same proof twice. *)
  have ma:"maintainedA {reflexivity_rule S_Idt, transitive_rule S_Idt, symmetry_rule S_Idt} G"
    using assms(2) by (auto simp:identity_rules_def)
  note equiv = equivalence[OF assms(1) this]
  { fix l x y
    assume "(x, y)  getRel l G" hence l:"l  L" using assms(3) unfolding getRel_def by auto
    have r1:"(λv. getRel l G `` {v}) respects getRel S_Idt G"
      apply(intro congruence_rule[OF assms(1) ma])
      using assms(2) l unfolding identity_rules_def by auto
    have r2:"(λv. (getRel l G)¯ `` {v}) respects getRel S_Idt G"
      apply(intro congruence_rule[OF assms(1) ma])
      using assms(2) l unfolding identity_rules_def by auto
    note congr = r1 r2
  } note congr = this
  define P where P:"P = (λ x y. y  getRel S_Idt G `` {x})"
  { fix x
    assume a:"getRel S_Idt G `` {x}  {}"
    hence " y. P x y" unfolding P by auto
    hence p:"P x (Eps (P x))" unfolding some_eq_ex by auto
    { fix y
      assume b:"P x y"
      hence "(x,y)  getRel S_Idt G" unfolding P by auto
      from equiv_class_eq[OF equiv this]
      have "getRel S_Idt G `` {x} = getRel S_Idt G `` {y}".
    } note u = this[OF p]
    have "getRel S_Idt G `` {Eps (P x)} = getRel S_Idt G `` {x}"
      unfolding u by (fact refl)
    hence "Eps (P (Eps (P x))) = Eps (P x)" unfolding P by auto
  } note P_eq = this
  define f where f:"f = (λ x. (if getRel S_Idt G `` {x} = {} then x else (SOME y. P x y<