# 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 "R⇩1 ⊆ R⇩2" "E⇩1 ⊆ E⇩2" "edge_preserving R⇩2 E⇩2 G"
shows "edge_preserving R⇩1 E⇩1 G"
using assms unfolding edge_preserving_def by blast

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

end

# 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 ≡ ∀ R∈Rs. 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 f⇩1 f⇩2 ≡ (∀ v ∈ vertices G. f⇩1  {v} = f⇩2  {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 f⇩1 f⇩2"
shows "agree_on G (f⇩1 O g) (f⇩2 O g)"
using assms unfolding agree_on_def by auto

lemma agree_on_then_eq:
assumes "agree_on G f⇩1 f⇩2" "Domain f⇩1 = vertices G" "Domain f⇩2 = vertices G"
shows "f⇩1 = f⇩2"
proof -
from assms have agr:"⋀ v. v∈Domain f⇩1 ⟹ f⇩1  {v} = f⇩2  {v}" unfolding agree_on_def by auto
have agr2:"⋀ v. v∉Domain f⇩1 ⟹ f⇩1  {v} = {}"
"⋀ v. v∉Domain f⇩2 ⟹ f⇩2  {v} = {}" by auto
with agr agr2 assms have "⋀ v. f⇩1  {v} = f⇩2  {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 e⇩1 v) G f"
shows "extensible (LG e⇩1 v, LG e⇩2 v) G f ⟷ graph_homomorphism (LG e⇩2 v) G f"
proof
assume "extensible (LG e⇩1 v, LG e⇩2 v) G f"
then obtain g where g: "graph_homomorphism (LG e⇩2 v) G g" "agree_on (LG e⇩1 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 e⇩2 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 ≡ ∀ R∈Rs. 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 G⇩1 G⇩2 f⇩1 f⇩2 ≡ (∀ h⇩1 h⇩2 G::('a, 'x) labeled_graph.
(graph_homomorphism (snd R) G h⇩1 ∧ graph_homomorphism G⇩1 G h⇩2 ∧ f⇩1 O h⇩2 ⊆ h⇩1)
⟶ (∃ h. graph_homomorphism G⇩2 G h ∧ h⇩2 ⊆ h))"

lemma weak_universalD[dest]:
assumes "weak_universal (t:: 'x itself) R (G⇩1::('a, 'b) labeled_graph) G⇩2 f⇩1 f⇩2"
shows "⋀  h⇩1 h⇩2 G::('a, 'x) labeled_graph.
graph_homomorphism (snd R) G h⇩1 ⟹ graph_homomorphism G⇩1 G h⇩2 ⟹ f⇩1 O h⇩2 ⊆ h⇩1
⟹ (∃ h. graph_homomorphism G⇩2 G h ∧ h⇩2 ⊆ h)"
using assms unfolding weak_universal_def by metis

lemma weak_universalI[intro]:
assumes "⋀ h⇩1 h⇩2 G::('a, 'x) labeled_graph.
graph_homomorphism (snd R) G h⇩1 ⟹ graph_homomorphism G⇩1 G h⇩2 ⟹ f⇩1 O h⇩2 ⊆ h⇩1
⟹ (∃ h. graph_homomorphism G⇩2 G h ∧ h⇩2 ⊆ h)"
shows "weak_universal (t:: 'x itself) R (G⇩1::('a, 'b) labeled_graph) G⇩2 f⇩1 f⇩2"
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 G⇩1 G⇩2 ≡ subgraph G⇩1 G⇩2 ∧
(∃ f⇩1 f⇩2. graph_homomorphism (fst R) G⇩1 f⇩1 ∧
graph_homomorphism (snd R) G⇩2 f⇩2 ∧
f⇩1 ⊆ f⇩2 ∧
weak_universal t R G⇩1 G⇩2 f⇩1 f⇩2
)"

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) ∨ (∃R∈Rs. 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 f⇩1 f⇩2 where
R:"(fst R,snd R) ∈ Rs" and f⇩1:"graph_homomorphism (fst R) (S i) f⇩1"
and wu:"weak_universal t R (S i) (S (i + 1)) f⇩1 f⇩2" by auto
from graph_homomorphism_composes[OF f⇩1 3(2)]
have ih_comp:"graph_homomorphism (fst R) C (f⇩1 O x)".
with maintainedD[OF consequence_graphD(1)[OF cgC R]]
have "extensible (fst R, snd R) C (f⇩1 O x)" by auto
from this[unfolded extensible_def prod.sel]
obtain g where g:"graph_homomorphism (snd R) C g" "f⇩1 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)) ∨
(∃R∈Rs. 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:"(⋃R∈Rs. {(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 ⊨ e⇩1 ⊑ e⇩2 = (:G:⟦e⇩1⟧ ⊆ :G:⟦e⇩2⟧)" and
eq_as_subsets:
"G ⊨ (e⇩1, e⇩2) = (G ⊨ e⇩1 ⊑ e⇩2 ∧ G ⊨ e⇩2 ⊑ e⇩1)"
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 "y∈vertices 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). x∈vertices G ∧ y∈vertices 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 e⇩1 e⇩2)
= (let G⇩1 = translation e⇩1 ; G⇩2 = translation e⇩2
in graph_union (map_graph_fn G⇩1 (λ x. if x=0 then 0 else x+card(vertices G⇩2)-1))
(map_graph_fn G⇩2 (λ x. if x=0 then card (vertices G⇩2) else x)))" |
"translation (A_Int e⇩1 e⇩2)
= (let G⇩1 = translation e⇩1 ; G⇩2 = translation e⇩2
in graph_union G⇩1 (map_graph_fn G⇩2 (λ x. if x<2 then x else x+card(vertices G⇩1)-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 r≥2" 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)"
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 "2≤card (vertices (translation X1))" "2≤card (vertices (translation X2))" by auto
hence "1 ≤card (vertices (translation X1))" "1≤card (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 e⇩1 e⇩2 f x y)
let ?f⇩1 = "id"
let ?f⇩2 = "(λ x. if x < 2 then x else x + card (vertices (translation e⇩1)) - 2)"
let ?G⇩1 = "translation e⇩1"
let ?G⇩2 = "translation e⇩2"
have f1:"(0, x) ∈ on_graph ?G⇩1 ?f⇩1 O f" "(1, y) ∈ on_graph ?G⇩1 ?f⇩1 O f"
and f2:"(0, x) ∈ on_graph ?G⇩2 ?f⇩2 O f" "(1, y) ∈ on_graph ?G⇩2 ?f⇩2 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 ?G⇩1 (map_graph_fn ?G⇩2 ?f⇩2)) G f"
by (auto simp:Let_def)
from graph_homo_union_id(1)[OF uni translation_graph]
have h1:"graph_homomorphism ?G⇩1 (translation (A_Int e⇩1 e⇩2)) (on_graph ?G⇩1 id)"
by (auto simp:Let_def graph_homomorphism_def)
have "graph (map_graph_fn ?G⇩2 ?f⇩2)" by auto
from graph_homo_union_id(2)[OF uni this]
have h2:"graph_homomorphism ?G⇩2 (translation (A_Int e⇩1 e⇩2)) (on_graph ?G⇩2 ?f⇩2)"
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 e⇩1 e⇩2 f x y)
let ?f⇩1 =  "(λ x. if x=0 then 0 else x+card(vertices (translation e⇩2))-1)"
let ?f⇩2 =  "(λ x. if x=0 then card (vertices (translation e⇩2)) else x)"
let ?G⇩1 = "translation e⇩1"
let ?G⇩2 = "translation e⇩2"
let ?v = "card (vertices (translation e⇩2))"
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 ?G⇩1 ?f⇩1 O f" "(1, v) ∈ on_graph ?G⇩1 ?f⇩1 O f"
and f2:"(0, v) ∈ on_graph ?G⇩2 ?f⇩2 O f" "(1, y) ∈ on_graph ?G⇩2 ?f⇩2 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 ?G⇩1 ?f⇩1) (map_graph_fn ?G⇩2 ?f⇩2)) G f"
by (auto simp:Let_def)
have "graph (map_graph_fn ?G⇩1 ?f⇩1)" by auto
from graph_homo_union_id(1)[OF uni this]
have h1:"graph_homomorphism ?G⇩1 (translation (A_Cmp e⇩1 e⇩2)) (on_graph ?G⇩1 ?f⇩1)"
by (auto simp:Let_def graph_homomorphism_def2)
have "graph (map_graph_fn ?G⇩2 ?f⇩2)" by auto
from graph_homo_union_id(2)[OF uni this]
have h2:"graph_homomorphism ?G⇩2 (translation (A_Cmp e⇩1 e⇩2)) (on_graph ?G⇩2 ?f⇩2)"
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 e⇩1 e⇩2)
from A_Int have assm:"(x, y) ∈ :G:⟦e⇩1⟧" "(x, y) ∈ :G:⟦e⇩2⟧" by auto
from A_Int(1)[OF assm(1)] obtain f⇩1 where
f⇩1:"graph_homomorphism (translation e⇩1) G f⇩1" "(0, x) ∈ f⇩1" "(1, y) ∈ f⇩1" by auto
from A_Int(2)[OF assm(2)] obtain f⇩2 where
f⇩2:"graph_homomorphism (translation e⇩2) G f⇩2" "(0, x) ∈ f⇩2" "(1, y) ∈ f⇩2" by auto
from f⇩1 f⇩2 have v:"Domain f⇩1 = vertices (translation e⇩1)" "Domain f⇩2 = vertices (translation e⇩2)"
unfolding graph_homomorphism_def by auto
let ?f⇩2 = "(λ x. if x < 2 then x else x + card (vertices (translation e⇩1)) - 2)"
let ?tr⇩2 = "on_graph (translation e⇩2) ?f⇩2"
have inj2:"inj_on ?f⇩2 (vertices (translation e⇩2))" unfolding inj_on_def by auto
have "(0,0) ∈ ?tr⇩2¯" "(1,1) ∈ ?tr⇩2¯" by auto
from this[THEN relcompI] f⇩2(2,3)
have zero_one:"(0,x) ∈ ?tr⇩2¯ O f⇩2"
"(1,y) ∈ ?tr⇩2¯ O f⇩2" by auto
{ fix yb zb
assume "(yb + card (vertices (translation e⇩1)) - 2, zb) ∈ f⇩1"
hence "yb + card (vertices (translation e⇩1)) - 2 ∈ vertices (translation e⇩1)" using v by auto
} note in_f[dest!] = this
have d_a:"Domain f⇩1 ∩  Domain (?tr⇩2¯ O f⇩2) = {0,1}"
using zero_one by (auto simp:v)
have d_b:"Domain (f⇩1 ∩ ?tr⇩2¯ O f⇩2) = {0,1}"
using zero_one f⇩1(2,3) by auto
note cmp2 = graph_homomorphism_composes[OF graph_homo_inv[OF translation_graph inj2] f⇩2(1)]
have "graph_homomorphism (translation (A_Int e⇩1 e⇩2)) G (f⇩1 ∪ ?tr⇩2¯ O f⇩2)"
using graph_homo_union[OF f⇩1(1) cmp2 d_a[folded d_b]]
by (auto simp:Let_def)
thus ?case using zero_one[THEN UnI2[of _ _ "f⇩1"]] by blast
next
case (A_Cmp e⇩1 e⇩2)
from A_Cmp obtain z where assm:"(x, z) ∈ :G:⟦e⇩1⟧" "(z, y) ∈ :G:⟦e⇩2⟧" by auto
from A_Cmp(1)[OF assm(1)] obtain f⇩1 where
f⇩1:"graph_homomorphism (translation e⇩1) G f⇩1" "(0, x) ∈ f⇩1" "(1, z) ∈ f⇩1" by auto
from A_Cmp(2)[OF assm(2)] obtain f⇩2 where
f⇩2:"graph_homomorphism (translation e⇩2) G f⇩2" "(0, z) ∈ f⇩2" "(1, y) ∈ f⇩2" by auto
from f⇩1 f⇩2 have v:"Domain f⇩1 = vertices (translation e⇩1)" "Domain f⇩2 = vertices (translation e⇩2)"
unfolding graph_homomorphism_def by auto
let ?f⇩1 = "(λ x. if x=0 then 0 else x+card(vertices (translation e⇩2))-1)"
let ?f⇩2 = "(λ x. if x=0 then card (vertices (translation e⇩2)) else x)"
let ?tr⇩1 = "on_graph (translation e⇩1) ?f⇩1"
let ?tr⇩2 = "on_graph (translation e⇩2) ?f⇩2"
have inj1:"inj_on ?f⇩1 (vertices (translation e⇩1))" unfolding inj_on_def by auto
have inj2:"inj_on ?f⇩2 (vertices (translation e⇩2))" unfolding inj_on_def by auto
have "(card (vertices (translation e⇩2)),0) ∈ ?tr⇩2¯" "(1,1) ∈ ?tr⇩2¯"
"(0,0) ∈ ?tr⇩1¯" "(card (vertices (translation e⇩2)),1) ∈ ?tr⇩1¯" by auto
from this[THEN relcompI] f⇩2(2,3) f⇩1(2,3)
have zero_one:"(card (vertices (translation e⇩2)),z) ∈ ?tr⇩1¯ O f⇩1"
"(0,x) ∈ ?tr⇩1¯ O f⇩1"
"(card (vertices (translation e⇩2)),z) ∈ ?tr⇩2¯ O f⇩2"
"(1,y) ∈ ?tr⇩2¯ O f⇩2" by auto
have [simp]:
"ye ∈ vertices (translation e⇩2) ⟹
(if ye = 0 then card (vertices (translation e⇩2)) else ye) =
(if yd = 0 then 0 else yd + card (vertices (translation e⇩2)) - 1) ⟷ ye = 0 ∧ yd = 1"
for ye yd using v inv_tr_card_min[OF verts_in_translation,of "e⇩2"]
by(cases "ye=0";cases "yd=0";auto)
have d_a:"Domain (?tr⇩1¯ O f⇩1) ∩  Domain (?tr⇩2¯ O f⇩2) = {card (vertices (translation e⇩2))}"
using zero_one using [[simproc del: defined_all]] by (auto simp: v)
have d_b:"Domain (?tr⇩1¯ O f⇩1 ∩ ?tr⇩2¯ O f⇩2) = {card (vertices (translation e⇩2))}"
using zero_one f⇩1(2,3) using [[simproc del: defined_all]] by auto
note cmp1 = graph_homomorphism_composes[OF graph_homo_inv[OF translation_graph inj1] f⇩1(1)]
note cmp2 = graph_homomorphism_composes[OF graph_homo_inv[OF translation_graph inj2] f⇩2(1)]
have "graph_homomorphism (translation (A_Cmp e⇩1 e⇩2)) G (?tr⇩1¯ O f⇩1 ∪ ?tr⇩2¯ O f⇩2)"
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 e⇩L,translation (A_Int e⇩L e⇩R)) G ⟷ G ⊨ e⇩L ⊑ e⇩R" (is "?rhs = ?lhs")
proof
assume lhs:?lhs
show ?rhs unfolding maintained_def proof(clarify) fix f
assume f:"graph_homomorphism (fst (translation e⇩L, translation (A_Int e⇩L e⇩R))) 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 (e⇩L ⊑ e⇩R)⟧" unfolding translation[OF assms] by auto
with lhs have "(x,y) ∈ :G:⟦snd (e⇩L ⊑ e⇩R)⟧" by auto
then obtain g where g: "graph_homomorphism (translation (A_Int e⇩L e⇩R)) G g"
and g2: "(0, x) ∈ g" "(1, y) ∈ g" unfolding translation[OF assms] by auto
have v:"vertices (translation (A_Int e⇩L e⇩R)) = Domain g"
"vertices (translation e⇩L) = Domain f" using f g
unfolding graph_homomorphism_def by auto
from subgraph_subset[of "translation e⇩L" "translation (A_Int e⇩L e⇩R)"]
graph_rule_translation[of e⇩L e⇩R]
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 e⇩L)) (edges G)"
and uni_f:"univalent f" by auto
let ?f = "(λx. if x < 2 then x else x + card (vertices (translation e⇩L)) - 2)"
define GR where "GR = map_graph_fn (translation e⇩R) ?f"
from g[unfolded graph_homomorphism_def]
have "edge_preserving g (edges (translation (A_Int e⇩L e⇩R))) (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 e⇩R)"
hence "?f a ∈ vertices (translation (A_Int e⇩L e⇩R))" by (auto simp:Let_def)
from this[unfolded v] verts_in_translation[of "A_Int e⇩L e⇩R",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 e⇩L]]
have df[dest]:"xa ∉ Domain f ⟹ (l,xa,xb) ∈ edges (translation e⇩L) ⟹ False"
"xa ∉ Domain f ⟹ (l,xb,xa) ∈ edges (translation e⇩L) ⟹ 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 e⇩L,unfolded inv_translation_def v]
have "xa < card(Domain f)" by auto
with minb verts_in_translation[of "A_Int e⇩L e⇩R",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 e⇩L) ⊆ vertices (translation (A_Int e⇩L e⇩R))"
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 e⇩L e⇩R)) G ?g"
proof(rule graph_homomorphismI)
show "?g  vertices (translation (A_Int e⇩L e⇩R)) ⊆ 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 e⇩L e⇩R))) (edges G)"
unfolding Let_def translation.simps graph_union_edges proof
show "edge_preserving ?g (edges (translation e⇩L)) (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 e⇩R) ?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 e⇩L) f ?g" unfolding agree_on_def by (auto simp:v)
from ie ih show "extensible (translation e⇩L, translation (A_Int e⇩L e⇩R)) G f"
unfolding extensible_def prod.sel by auto
qed next
assume rhs:?rhs
{ fix x y assume "(x,y) ∈ :G:⟦e⇩L⟧"
with translation[OF assms] obtain f
where f:"graph_homomorphism (fst (translation e⇩L, translation (A_Int e⇩L e⇩R))) 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 e⇩L e⇩R)) G g"
"agree_on (translation e⇩L) f g" by auto
hence "(x,y) ∈ :G:⟦A_Int e⇩L e⇩R⟧" 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

text ‹Lemma 6 is only used on rules of the form @{term "e⇩L ⊑ e⇩R"}.
The requirement of G being a graph can be dropped for one direction.›
lemma maintained_holds[intro]:
assumes ":G:⟦e⇩L⟧ ⊆ :G:⟦e⇩R⟧"
shows "maintained (transl_rule (e⇩L ⊑ e⇩R)) 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 (e⇩L ⊑ e⇩R)) G ⟷ (:G:⟦e⇩L⟧ ⊆ :G:⟦e⇩R⟧)"
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<