# Theory Digraph_Isomorphism

```theory Digraph_Isomorphism imports
Arc_Walk
Digraph
Digraph_Component
begin

section ‹Isomorphisms of Digraphs›

record ('a,'b,'aa,'bb) digraph_isomorphism =
iso_verts :: "'a ⇒ 'aa"
iso_arcs :: "'b ⇒ 'bb"
iso_head :: "'bb ⇒ 'aa"
iso_tail :: "'bb ⇒ 'aa"

definition (in pre_digraph) digraph_isomorphism :: "('a,'b,'aa,'bb) digraph_isomorphism ⇒ bool" where
"digraph_isomorphism hom ≡
wf_digraph G ∧
inj_on (iso_verts hom) (verts G) ∧
inj_on (iso_arcs hom) (arcs G) ∧
(∀a ∈ arcs G.
iso_verts hom (tail G a) = iso_tail hom (iso_arcs hom a) ∧
iso_verts hom (head G a) = iso_head hom (iso_arcs hom a))"

definition (in pre_digraph) inv_iso :: "('a,'b,'aa,'bb) digraph_isomorphism ⇒ ('aa,'bb,'a,'b) digraph_isomorphism" where
"inv_iso hom ≡ ⦇
iso_verts = the_inv_into (verts G) (iso_verts hom),
iso_arcs = the_inv_into (arcs G) (iso_arcs hom),
iso_head = head G,
iso_tail = tail G
⦈"

definition app_iso
:: "('a,'b,'aa,'bb) digraph_isomorphism ⇒ ('a,'b) pre_digraph ⇒ ('aa,'bb) pre_digraph" where
"app_iso hom G ≡ ⦇ verts = iso_verts hom ` verts G, arcs = iso_arcs hom ` arcs G,
tail = iso_tail hom, head = iso_head hom ⦈"

definition digraph_iso :: "('a,'b) pre_digraph ⇒ ('c,'d) pre_digraph ⇒ bool"  where
"digraph_iso G H ≡ ∃f. pre_digraph.digraph_isomorphism G f ∧ H = app_iso f G"

lemma verts_app_iso: "verts (app_iso hom G) = iso_verts hom ` verts G"
and arcs_app_iso: "arcs (app_iso hom G) = iso_arcs hom `arcs G"
and tail_app_iso: "tail (app_iso hom G) = iso_tail hom"
and head_app_iso: "head (app_iso hom G) = iso_head hom"
by (auto simp: app_iso_def)

lemmas app_iso_simps[simp] = verts_app_iso arcs_app_iso tail_app_iso head_app_iso

context pre_digraph begin

lemma
assumes "digraph_isomorphism hom"
shows iso_verts_inv_iso: "⋀u. u ∈ verts G ⟹ iso_verts (inv_iso hom) (iso_verts hom u) = u"
and iso_arcs_inv_iso: "⋀a. a ∈ arcs G ⟹ iso_arcs (inv_iso hom) (iso_arcs hom a) = a"
and iso_verts_iso_inv: "⋀u. u ∈ verts (app_iso hom G) ⟹ iso_verts hom (iso_verts (inv_iso hom) u) = u"
and iso_arcs_iso_inv: "⋀a. a ∈ arcs (app_iso hom G) ⟹ iso_arcs hom (iso_arcs (inv_iso hom) a) = a"
and iso_tail_inv_iso: "iso_tail (inv_iso hom) = tail G"
and iso_head_inv_iso: "iso_head (inv_iso hom) = head G"
and verts_app_inv_iso:"iso_verts (inv_iso hom) ` iso_verts hom ` verts G = verts G"
and arcs_app_inv_iso:"iso_arcs (inv_iso hom) ` iso_arcs hom ` arcs G = arcs G"
using assms by (auto simp: inv_iso_def digraph_isomorphism_def the_inv_into_f_f)

lemmas iso_inv_simps[simp] =
iso_verts_inv_iso iso_verts_iso_inv
iso_arcs_inv_iso iso_arcs_iso_inv
verts_app_inv_iso arcs_app_inv_iso
iso_tail_inv_iso iso_head_inv_iso

lemma app_iso_inv[simp]:
assumes "digraph_isomorphism hom"
shows "app_iso (inv_iso hom) (app_iso hom G) = G"
using assms by (intro pre_digraph.equality) (auto intro: rev_image_eqI)

lemma iso_verts_eq_iff[simp]:
assumes "digraph_isomorphism hom" "u ∈ verts G" "v ∈ verts G"
shows "iso_verts hom u = iso_verts hom v ⟷ u = v"
using assms by (auto simp: digraph_isomorphism_def dest: inj_onD)

lemma iso_arcs_eq_iff[simp]:
assumes "digraph_isomorphism hom" "e1 ∈ arcs G" "e2 ∈ arcs G"
shows "iso_arcs hom e1 = iso_arcs hom e2 ⟷ e1 = e2"
using assms by (auto simp: digraph_isomorphism_def dest: inj_onD)

lemma
assumes "digraph_isomorphism hom" "e ∈ arcs G"
shows iso_verts_tail: "iso_tail hom (iso_arcs hom e) = iso_verts hom (tail G e)"
and iso_verts_head: "iso_head hom (iso_arcs hom e) = iso_verts hom (head G e)"
using assms unfolding digraph_isomorphism_def by auto

lemma digraph_isomorphism_inj_on_arcs:
"digraph_isomorphism hom ⟹ inj_on (iso_arcs hom) (arcs G)"
by (auto simp: digraph_isomorphism_def)

lemma digraph_isomorphism_inj_on_verts:
"digraph_isomorphism hom ⟹ inj_on (iso_verts hom) (verts G)"
by (auto simp: digraph_isomorphism_def)

end

lemma (in wf_digraph) wf_digraphI_app_iso[intro?]:
assumes "digraph_isomorphism hom"
shows "wf_digraph (app_iso hom G)"
proof unfold_locales
fix e assume "e ∈ arcs (app_iso hom G)"
then obtain e' where e': "e' ∈ arcs G" "iso_arcs hom e' = e"
by auto
then have "iso_verts hom (head G e') ∈ verts (app_iso hom G)"
"iso_verts hom (tail G e') ∈ verts (app_iso hom G)"
by auto
then show "tail (app_iso hom G) e ∈ verts (app_iso hom G)"
"head (app_iso hom G) e ∈ verts (app_iso hom G)"
using e' assms by (auto simp: iso_verts_tail iso_verts_head)
qed

lemma (in fin_digraph) fin_digraphI_app_iso[intro?]:
assumes "digraph_isomorphism hom"
shows "fin_digraph (app_iso hom G)"
proof -
interpret H: wf_digraph "app_iso hom G" using assms ..
show ?thesis by unfold_locales auto
qed

context wf_digraph begin

lemma digraph_isomorphism_invI:
assumes "digraph_isomorphism hom" shows "pre_digraph.digraph_isomorphism (app_iso hom G) (inv_iso hom)"
proof (unfold pre_digraph.digraph_isomorphism_def, safe)
show "inj_on (iso_verts (inv_iso hom)) (verts (app_iso hom G))"
"inj_on (iso_arcs (inv_iso hom)) (arcs (app_iso hom G))"
using assms unfolding pre_digraph.digraph_isomorphism_def inv_iso_def
by (auto intro: inj_on_the_inv_into)
next
show "wf_digraph (app_iso hom G)" using assms ..
next
fix a assume "a ∈ arcs (app_iso hom G)"
then obtain b where B: "a = iso_arcs hom b" "b ∈ arcs G"
by auto

with assms have [simp]:
"iso_tail hom (iso_arcs hom b) = iso_verts hom (tail G b)"
"iso_head hom (iso_arcs hom b) = iso_verts hom (head G b)"
"inj_on (iso_arcs hom) (arcs G)"
"inj_on (iso_verts hom) (verts G)"
by (auto simp: digraph_isomorphism_def)

from B show "iso_verts (inv_iso hom) (tail (app_iso hom G) a)
= iso_tail (inv_iso hom) (iso_arcs (inv_iso hom) a)"
by (auto simp: inv_iso_def the_inv_into_f_f)
from B show "iso_verts (inv_iso hom) (head (app_iso hom G) a)
= iso_head (inv_iso hom) (iso_arcs (inv_iso hom) a)"
by (auto simp: inv_iso_def the_inv_into_f_f)
qed

lemma awalk_app_isoI:
assumes "awalk u p v" and hom: "digraph_isomorphism hom"
shows "pre_digraph.awalk (app_iso hom G) (iso_verts hom u) (map (iso_arcs hom) p) (iso_verts hom v)"
proof -
interpret H: wf_digraph "app_iso hom G" using hom ..
from assms show ?thesis
by (induct p arbitrary: u)
(auto simp: awalk_simps H.awalk_simps iso_verts_head iso_verts_tail)
qed

lemma awalk_app_isoD:
assumes w: "pre_digraph.awalk (app_iso hom G) u p v" and hom: "digraph_isomorphism hom"
shows "awalk (iso_verts (inv_iso hom) u) (map (iso_arcs (inv_iso hom)) p) (iso_verts (inv_iso hom) v)"
proof -
interpret H: wf_digraph "app_iso hom G" using hom ..
from assms show ?thesis
by (induct p arbitrary: u)
(force simp: awalk_simps H.awalk_simps iso_verts_head iso_verts_tail)+
qed

lemma awalk_verts_app_iso_eq:
assumes "digraph_isomorphism hom" and "awalk u p v"
shows "pre_digraph.awalk_verts (app_iso hom G) (iso_verts hom u) (map (iso_arcs hom) p)
= map (iso_verts hom) (awalk_verts u p)"
using assms
by (induct p arbitrary: u)
(auto simp: pre_digraph.awalk_verts.simps iso_verts_head iso_verts_tail awalk_Cons_iff)

(*
lemma awalk_verts_app_iso_eq':
assumes hom: "digraph_isomorphism hom" and w: "pre_digraph.awalk (app_iso hom G) u p v"
shows "pre_digraph.awalk_verts (app_iso hom G) u p
= map (iso_verts hom) (awalk_verts (iso_verts (inv_iso hom) u) (map (iso_arcs (inv_iso hom)) p))"
proof -
interpret H: wf_digraph "app_iso hom G" using hom ..
have w': "awalk (iso_verts (inv_iso hom) u) (map (iso_arcs (inv_iso hom)) p) (iso_verts (inv_iso hom) v)"
using w hom by (rule awalk_app_isoD)
have "pre_digraph.awalk_verts (app_iso hom G) u p =
pre_digraph.awalk_verts (app_iso hom G) (iso_verts hom (iso_verts (inv_iso hom) u)) (map (iso_arcs hom) (map (iso_arcs (inv_iso hom)) p))"
using hom w by (auto simp add: o_def subsetD cong: map_cong)
also have "… = map (iso_verts hom) (awalk_verts (iso_verts (inv_iso hom) u) (map (iso_arcs (inv_iso hom)) p))"
using hom w' by (rule awalk_verts_app_iso_eq)
finally show ?thesis .
qed
*)

lemma arcs_ends_app_iso_eq:
assumes "digraph_isomorphism hom"
shows "arcs_ends (app_iso hom G) = (λ(u,v). (iso_verts hom u, iso_verts hom v)) ` arcs_ends G"
using assms by (auto simp: arcs_ends_conv image_image iso_verts_head iso_verts_tail
intro!: rev_image_eqI)

lemma in_arcs_app_iso_eq:
assumes "digraph_isomorphism hom" and "u ∈ verts G"
shows "in_arcs (app_iso hom G) (iso_verts hom u) = iso_arcs hom ` in_arcs G u"
using assms unfolding in_arcs_def by (auto simp: iso_verts_head)

lemma out_arcs_app_iso_eq:
assumes "digraph_isomorphism hom" and "u ∈ verts G"
shows "out_arcs (app_iso hom G) (iso_verts hom u) = iso_arcs hom ` out_arcs G u"
using assms unfolding out_arcs_def by (auto simp: iso_verts_tail)

lemma in_degree_app_iso_eq:
assumes "digraph_isomorphism hom" and "u ∈ verts G"
shows "in_degree (app_iso hom G) (iso_verts hom u) = in_degree G u"
unfolding in_degree_def in_arcs_app_iso_eq[OF assms]
proof (rule card_image)
from assms show "inj_on (iso_arcs hom) (in_arcs G u)"
unfolding digraph_isomorphism_def by - (rule subset_inj_on, auto)
qed

lemma out_degree_app_iso_eq:
assumes "digraph_isomorphism hom" and "u ∈ verts G"
shows "out_degree (app_iso hom G) (iso_verts hom u) = out_degree G u"
unfolding out_degree_def out_arcs_app_iso_eq[OF assms]
proof (rule card_image)
from assms show "inj_on (iso_arcs hom) (out_arcs G u)"
unfolding digraph_isomorphism_def by - (rule subset_inj_on, auto)
qed

lemma in_arcs_app_iso_eq':
assumes "digraph_isomorphism hom" and "u ∈ verts (app_iso hom G)"
shows "in_arcs (app_iso hom G) u = iso_arcs hom ` in_arcs G (iso_verts (inv_iso hom) u)"
using assms in_arcs_app_iso_eq[of hom "iso_verts (inv_iso hom) u"] by auto

lemma out_arcs_app_iso_eq':
assumes "digraph_isomorphism hom" and "u ∈ verts (app_iso hom G)"
shows "out_arcs (app_iso hom G) u = iso_arcs hom ` out_arcs G (iso_verts (inv_iso hom) u)"
using assms out_arcs_app_iso_eq[of hom "iso_verts (inv_iso hom) u"] by auto

lemma in_degree_app_iso_eq':
assumes "digraph_isomorphism hom" and "u ∈ verts (app_iso hom G)"
shows "in_degree (app_iso hom G) u = in_degree G (iso_verts (inv_iso hom) u)"
using assms in_degree_app_iso_eq[of hom "iso_verts (inv_iso hom) u"] by auto

lemma out_degree_app_iso_eq':
assumes "digraph_isomorphism hom" and "u ∈ verts (app_iso hom G)"
shows "out_degree (app_iso hom G) u = out_degree G (iso_verts (inv_iso hom) u)"
using assms out_degree_app_iso_eq[of hom "iso_verts (inv_iso hom) u"] by auto

lemmas app_iso_eq =
awalk_verts_app_iso_eq
arcs_ends_app_iso_eq
in_arcs_app_iso_eq'
out_arcs_app_iso_eq'
in_degree_app_iso_eq'
out_degree_app_iso_eq'

lemma reachableI_app_iso:
assumes r: "u →⇧* v" and hom: "digraph_isomorphism hom"
shows "(iso_verts hom u) →⇧*⇘app_iso hom G⇙ (iso_verts hom v)"
proof -
interpret H: wf_digraph "app_iso hom G" using hom ..
from r obtain p where "awalk u p v" by (auto simp: reachable_awalk)
then have "H.awalk (iso_verts hom u) (map (iso_arcs hom) p) (iso_verts hom v)"
using hom by (rule awalk_app_isoI)
then show ?thesis by (auto simp: H.reachable_awalk)
qed

lemma awalk_app_iso_eq:
assumes hom: "digraph_isomorphism hom"
assumes "u ∈ iso_verts hom ` verts G" "v ∈ iso_verts hom ` verts G" "set p ⊆ iso_arcs hom ` arcs G"
shows "pre_digraph.awalk (app_iso hom G) u p v
⟷ awalk (iso_verts (inv_iso hom) u) (map (iso_arcs (inv_iso hom)) p) (iso_verts (inv_iso hom) v)"
proof -
interpret H: wf_digraph "app_iso hom G" using hom ..
from assms show ?thesis
by (induct p arbitrary: u)
(auto simp: awalk_simps H.awalk_simps iso_verts_head iso_verts_tail)
qed

lemma reachable_app_iso_eq:
assumes hom: "digraph_isomorphism hom"
assumes "u ∈ iso_verts hom ` verts G" "v ∈ iso_verts hom ` verts G"
shows "u →⇧*⇘app_iso hom G⇙ v ⟷ iso_verts (inv_iso hom) u →⇧* iso_verts (inv_iso hom) v" (is "?L ⟷ ?R")
proof -
interpret H: wf_digraph "app_iso hom G" using hom ..

show ?thesis
proof
assume ?L
then obtain p where "H.awalk u p v" by (auto simp: H.reachable_awalk)
moreover
then have "set p ⊆ iso_arcs hom ` arcs G" by (simp add: H.awalk_def)
ultimately
show ?R using assms by (auto simp: awalk_app_iso_eq reachable_awalk)
next
assume ?R
then obtain p0 where "awalk (iso_verts (inv_iso hom) u) p0 (iso_verts (inv_iso hom) v)"
by (auto simp: reachable_awalk)
moreover
then have "set p0 ⊆ arcs G" by (simp add: awalk_def)
define p where "p = map (iso_arcs hom) p0"
have "set p ⊆ iso_arcs hom ` arcs G" "p0 = map (iso_arcs (inv_iso hom)) p"
using ‹set p0 ⊆ _› hom by (auto simp: p_def map_idI subsetD)
ultimately
show ?L using assms by (auto simp: awalk_app_iso_eq[symmetric] H.reachable_awalk)
qed
qed

lemma connectedI_app_iso:
assumes c: "connected G" and hom: "digraph_isomorphism hom"
shows "connected (app_iso hom G)"
proof -
have *: "symcl (arcs_ends (app_iso hom G)) = (λ(u,v). (iso_verts hom u, iso_verts hom v)) ` symcl (arcs_ends G)"
using hom by (auto simp add: app_iso_eq symcl_def)
{ fix u v assume "(u,v) ∈ rtrancl_on (verts G) (symcl (arcs_ends G))"
then have "(iso_verts hom u, iso_verts hom v) ∈ rtrancl_on (verts (app_iso hom G)) (symcl (arcs_ends (app_iso hom G)))"
proof induct
case (step x y)
have "(iso_verts hom x, iso_verts hom y)
∈ rtrancl_on (verts (app_iso hom G)) (symcl (arcs_ends (app_iso hom G)))"
using step by (rule_tac rtrancl_on_into_rtrancl_on[where b="iso_verts hom x"]) (auto simp: *)
then show ?case
by (rule rtrancl_on_trans) (rule step)
qed auto }
with c show ?thesis unfolding connected_conv by auto
qed

end

lemma digraph_iso_swap:
assumes "wf_digraph G" "digraph_iso G H" shows "digraph_iso H G"
proof -
from assms obtain f where "pre_digraph.digraph_isomorphism G f" "H = app_iso f G"
unfolding digraph_iso_def by auto
then have "pre_digraph.digraph_isomorphism H (pre_digraph.inv_iso G f)" "app_iso (pre_digraph.inv_iso G f) H = G"
using assms by (simp_all add: wf_digraph.digraph_isomorphism_invI pre_digraph.app_iso_inv)
then show ?thesis unfolding digraph_iso_def by auto
qed

definition
o_iso :: "('c,'d,'e,'f) digraph_isomorphism ⇒ ('a,'b,'c,'d) digraph_isomorphism ⇒ ('a,'b,'e,'f) digraph_isomorphism"
where
"o_iso hom2 hom1 = ⦇
iso_verts = iso_verts hom2 o iso_verts hom1,
iso_arcs = iso_arcs hom2 o iso_arcs hom1,
iso_head = iso_head hom2,
iso_tail = iso_tail hom2
⦈"

lemma digraph_iso_trans[trans]:
assumes "digraph_iso G H" "digraph_iso H I" shows "digraph_iso G I"
proof -
from assms obtain hom1 where "pre_digraph.digraph_isomorphism G hom1" "H = app_iso hom1 G"
by (auto simp: digraph_iso_def)
moreover
from assms obtain hom2 where "pre_digraph.digraph_isomorphism H hom2" "I = app_iso hom2 H"
by (auto simp: digraph_iso_def)
ultimately
have "pre_digraph.digraph_isomorphism G (o_iso hom2 hom1)" "I = app_iso (o_iso hom2 hom1) G"
apply (auto simp: o_iso_def app_iso_def pre_digraph.digraph_isomorphism_def)
apply (rule comp_inj_on)
apply auto
apply (rule comp_inj_on)
apply auto
done
then show ?thesis by (auto simp: digraph_iso_def)
qed

lemma (in pre_digraph) digraph_isomorphism_subgraphI:
assumes "digraph_isomorphism hom"
assumes "subgraph H G"
shows "pre_digraph.digraph_isomorphism H hom"
using assms by (auto simp: pre_digraph.digraph_isomorphism_def subgraph_def compatible_def intro: subset_inj_on)

(* XXX move *)
lemma (in wf_digraph) verts_app_inv_iso_subgraph:
assumes hom: "digraph_isomorphism hom" and "V ⊆ verts G"
shows "iso_verts (inv_iso hom) ` iso_verts hom ` V = V"
proof -
have "⋀x. x ∈ V ⟹ iso_verts (inv_iso hom) (iso_verts hom x) = x"
using assms by auto
then show ?thesis by (auto simp: image_image cong: image_cong)
qed

(* XXX move *)
lemma (in wf_digraph) arcs_app_inv_iso_subgraph:
assumes hom: "digraph_isomorphism hom" and "A ⊆ arcs G"
shows "iso_arcs (inv_iso hom) ` iso_arcs hom ` A = A"
proof -
have "⋀x. x ∈ A ⟹ iso_arcs (inv_iso hom) (iso_arcs hom x) = x"
using assms by auto
then show ?thesis by (auto simp: image_image cong: image_cong)
qed

(* XXX move *)
lemma (in pre_digraph) app_iso_inv_subgraph[simp]:
assumes "digraph_isomorphism hom" "subgraph H G"
shows "app_iso (inv_iso hom) (app_iso hom H) = H"
proof -
from assms interpret wf_digraph G by auto
have "⋀u. u ∈ verts H ⟹ u ∈ verts G" "⋀a. a ∈ arcs H ⟹ a ∈ arcs G"
using assms by auto
with assms show ?thesis
by (intro pre_digraph.equality) (auto simp: verts_app_inv_iso_subgraph
arcs_app_inv_iso_subgraph compatible_def)
qed

lemma (in wf_digraph) app_iso_iso_inv_subgraph[simp]:
assumes "digraph_isomorphism hom"
assumes subg: "subgraph H (app_iso hom G)"
shows "app_iso hom (app_iso (inv_iso hom) H) = H"
proof -
have "⋀u. u ∈ verts H ⟹ u ∈ iso_verts hom ` verts G" "⋀a. a ∈ arcs H ⟹ a ∈ iso_arcs hom ` arcs G"
using assms by (auto simp: subgraph_def)
with assms show ?thesis
by (intro pre_digraph.equality) (auto simp: compatible_def image_image cong: image_cong)
qed

lemma (in pre_digraph) subgraph_app_isoI':
assumes hom: "digraph_isomorphism hom"
assumes subg: "subgraph H H'" "subgraph H' G"
shows "subgraph (app_iso hom H) (app_iso hom H')"
proof -
have "subgraph H G" using subg by (rule subgraph_trans)
then have "pre_digraph.digraph_isomorphism H hom" "pre_digraph.digraph_isomorphism H' hom"
using assms by (auto intro: digraph_isomorphism_subgraphI)
then show ?thesis
using assms by (auto simp: subgraph_def wf_digraph.wf_digraphI_app_iso compatible_def
intro: digraph_isomorphism_subgraphI)
qed

lemma (in pre_digraph) subgraph_app_isoI:
assumes "digraph_isomorphism hom"
assumes "subgraph H G"
shows "subgraph (app_iso hom H) (app_iso hom G)"
using assms by (auto intro: subgraph_app_isoI' wf_digraph.subgraph_refl)

lemma (in pre_digraph) app_iso_eq_conv:
assumes "digraph_isomorphism hom"
assumes "subgraph H1 G" "subgraph H2 G"
shows "app_iso hom H1 = app_iso hom H2 ⟷ H1 = H2" (is "?L ⟷ ?R")
proof
assume ?L
then have "app_iso (inv_iso hom) (app_iso hom H1) = app_iso (inv_iso hom) (app_iso hom H2)"
by simp
with assms show ?R by auto
qed simp

lemma in_arcs_app_iso_cases:
assumes "a ∈ arcs (app_iso hom G)"
obtains a0 where "a = iso_arcs hom a0" "a0 ∈ arcs G"
using assms by auto

lemma in_verts_app_iso_cases:
assumes "v ∈ verts (app_iso hom G)"
obtains v0 where "v = iso_verts hom v0" "v0 ∈ verts G"
using assms by auto

lemma (in wf_digraph) max_subgraph_iso:
assumes hom: "digraph_isomorphism hom"
assumes subg: "subgraph H (app_iso hom G)"
shows "pre_digraph.max_subgraph (app_iso hom G) P H
⟷ max_subgraph (P o app_iso hom) (app_iso (inv_iso hom) H)"
proof -
have hom_inv: "pre_digraph.digraph_isomorphism (app_iso hom G) (inv_iso hom)"
using hom by (rule digraph_isomorphism_invI)
interpret aG: wf_digraph "app_iso hom G" using hom ..

have *: "subgraph (app_iso (inv_iso hom) H) G"
using hom pre_digraph.subgraph_app_isoI'[OF hom_inv subg aG.subgraph_refl] by simp
define H0 where "H0 = app_iso (inv_iso hom) H"
then have H0: "H = app_iso hom H0" "subgraph H0 G"
using hom subg ‹subgraph _ G› by auto

show ?thesis (is "?L ⟷ ?R")
proof
assume ?L then show ?R using assms H0
by (auto simp: max_subgraph_def aG.max_subgraph_def pre_digraph.subgraph_app_isoI'
subgraph_refl pre_digraph.app_iso_eq_conv)
next
assume ?R
then show ?L
using assms hom_inv pre_digraph.subgraph_app_isoI[OF hom_inv]
apply (auto simp: max_subgraph_def aG.max_subgraph_def)
apply (erule allE[of _ "app_iso (inv_iso hom) H'" for H'])
apply (auto simp: pre_digraph.subgraph_app_isoI' pre_digraph.app_iso_eq_conv)
done
qed
qed

lemma (in pre_digraph) max_subgraph_cong:
assumes "H = H'" "⋀H''. subgraph H' H'' ⟹ subgraph H'' G ⟹ P H'' = P' H''"
shows "max_subgraph P H = max_subgraph P' H'"
using assms by (auto simp: max_subgraph_def intro: wf_digraph.subgraph_refl)

lemma (in pre_digraph) inj_on_app_iso:
assumes hom: "digraph_isomorphism hom"
assumes "S ⊆ {H. subgraph H G}"
shows "inj_on (app_iso hom) S"
using assms by (intro inj_onI) (subst (asm) app_iso_eq_conv, auto)

subsection ‹Graph Invariants›

context
fixes G hom assumes hom: "pre_digraph.digraph_isomorphism G hom"
begin

interpretation wf_digraph G using hom by (auto simp: pre_digraph.digraph_isomorphism_def)

lemma card_verts_iso[simp]: "card (iso_verts hom ` verts G) = card (verts G)"
using hom by (intro card_image digraph_isomorphism_inj_on_verts)

lemma card_arcs_iso[simp]: "card (iso_arcs hom ` arcs G) = card (arcs G)"
using hom by (intro card_image digraph_isomorphism_inj_on_arcs)

lemma strongly_connected_iso[simp]: "strongly_connected (app_iso hom G) ⟷ strongly_connected G"
using hom by (auto simp: strongly_connected_def reachable_app_iso_eq)

lemma subgraph_strongly_connected_iso:
assumes "subgraph H G"
shows "strongly_connected (app_iso hom H) ⟷ strongly_connected H"
proof -
interpret H: wf_digraph H using ‹subgraph H G› ..
have "H.digraph_isomorphism hom" using hom assms by (rule digraph_isomorphism_subgraphI)
then show ?thesis
using assms by (auto simp: strongly_connected_def H.reachable_app_iso_eq)
qed

lemma sccs_iso[simp]: "pre_digraph.sccs (app_iso hom G) = app_iso hom ` sccs" (is "?L = ?R")
proof (intro set_eqI iffI)
fix x assume "x ∈ ?L"
then have "subgraph x (app_iso hom G)"
by (auto simp: pre_digraph.sccs_def)
then show "x ∈ ?R"
using ‹x ∈ ?L› hom by (auto simp: pre_digraph.sccs_altdef2 max_subgraph_iso
subgraph_strongly_connected_iso cong: max_subgraph_cong  intro: rev_image_eqI)
next
fix x assume "x ∈ ?R"
then obtain x0 where "x0 ∈ sccs" "x = app_iso hom x0" by auto
then show "x ∈ ?L"
using hom by (auto simp: pre_digraph.sccs_altdef2 max_subgraph_iso subgraph_app_isoI
subgraphI_max_subgraph subgraph_strongly_connected_iso cong: max_subgraph_cong)
qed

lemma card_sccs_iso[simp]: "card (app_iso hom ` sccs) = card sccs"
apply (rule card_image)
using hom
apply (rule inj_on_app_iso)
apply auto
done

end

end
```