[STATEMENT]
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 "(\<lambda> v. getRel l G `` {v}) respects (getRel I G)" (is "?g1")
      and "(\<lambda> v. (getRel l G)\<inverse> `` {v}) respects (getRel I G)" (is "?g2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G &&& (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
(* Both parts of this lemma are proved using roughly the same proof. *)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
note eq = equivalence[OF g mA]
[PROOF STATE]
proof (state)
this:
equiv (vertices G) (getRel I G)

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
equiv (vertices G) (getRel I G)

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
fix y z
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
assume aI:"(y, z)\<in>getRel I G"
[PROOF STATE]
proof (state)
this:
(y, z) \<in> getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
hence a2:"(z, y)\<in>getRel I G"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> getRel I G

goal (1 subgoal):
 1. (z, y) \<in> getRel I G
[PROOF STEP]
using eq[unfolded equiv_def sym_def]
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> getRel I G
refl_on (vertices G) (getRel I G) \<and> (\<forall>x y. (x, y) \<in> getRel I G \<longrightarrow> (y, x) \<in> getRel I G) \<and> trans (getRel I G)

goal (1 subgoal):
 1. (z, y) \<in> getRel I G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(z, y) \<in> getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
hence a3:"(z, z)\<in>getRel I G" "(y, y)\<in>getRel I G"
[PROOF STATE]
proof (prove)
using this:
(z, y) \<in> getRel I G

goal (1 subgoal):
 1. (z, z) \<in> getRel I G &&& (y, y) \<in> getRel I G
[PROOF STEP]
using eq[unfolded equiv_def refl_on_def]
[PROOF STATE]
proof (prove)
using this:
(z, y) \<in> getRel I G
(getRel I G \<subseteq> vertices G \<times> vertices G \<and> (\<forall>x\<in>vertices G. (x, x) \<in> getRel I G)) \<and> sym (getRel I G) \<and> trans (getRel I G)

goal (1 subgoal):
 1. (z, z) \<in> getRel I G &&& (y, y) \<in> getRel I G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(z, z) \<in> getRel I G
(y, y) \<in> getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(z, z) \<in> getRel I G
(y, y) \<in> getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
assume al:"(y,x) \<in> getRel l G"
[PROOF STATE]
proof (state)
this:
(y, x) \<in> getRel l G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
hence "x \<in> vertices G"
[PROOF STATE]
proof (prove)
using this:
(y, x) \<in> getRel l G

goal (1 subgoal):
 1. x \<in> vertices G
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
(y, x) \<in> getRel l G
graph G

goal (1 subgoal):
 1. x \<in> vertices G
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(y, x) \<in> {(x, y). (l, x, y) \<in> edges G}
graph G

goal (1 subgoal):
 1. x \<in> vertices G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vertices G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
hence r:"(x,x) \<in> getRel I G"
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices G

goal (1 subgoal):
 1. (x, x) \<in> getRel I G
[PROOF STEP]
using eq[unfolded equiv_def refl_on_def]
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices G
(getRel I G \<subseteq> vertices G \<times> vertices G \<and> (\<forall>x\<in>vertices G. (x, x) \<in> getRel I G)) \<and> sym (getRel I G) \<and> trans (getRel I G)

goal (1 subgoal):
 1. (x, x) \<in> getRel I G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, x) \<in> getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
note relcompI[OF relcompI[OF a2 al] r]
[PROOF STATE]
proof (state)
this:
(z, x) \<in> (getRel I G O getRel l G) O getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(y, x) \<in> getRel l G \<Longrightarrow> (z, x) \<in> (getRel I G O getRel l G) O getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
note yx = this
[PROOF STATE]
proof (state)
this:
(y, x) \<in> getRel l G \<Longrightarrow> (z, x) \<in> (getRel I G O getRel l G) O getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(y, x) \<in> getRel l G \<Longrightarrow> (z, x) \<in> (getRel I G O getRel l G) O getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
assume al:"(z,x) \<in> getRel l G"
[PROOF STATE]
proof (state)
this:
(z, x) \<in> getRel l G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
hence "x \<in> vertices G"
[PROOF STATE]
proof (prove)
using this:
(z, x) \<in> getRel l G

goal (1 subgoal):
 1. x \<in> vertices G
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
(z, x) \<in> getRel l G
graph G

goal (1 subgoal):
 1. x \<in> vertices G
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(z, x) \<in> {(x, y). (l, x, y) \<in> edges G}
graph G

goal (1 subgoal):
 1. x \<in> vertices G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vertices G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
hence r:"(x,x) \<in> getRel I G"
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices G

goal (1 subgoal):
 1. (x, x) \<in> getRel I G
[PROOF STEP]
using eq[unfolded equiv_def refl_on_def]
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices G
(getRel I G \<subseteq> vertices G \<times> vertices G \<and> (\<forall>x\<in>vertices G. (x, x) \<in> getRel I G)) \<and> sym (getRel I G) \<and> trans (getRel I G)

goal (1 subgoal):
 1. (x, x) \<in> getRel I G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, x) \<in> getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
note relcompI[OF relcompI[OF aI al] r]
[PROOF STATE]
proof (state)
this:
(y, x) \<in> (getRel I G O getRel l G) O getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(z, x) \<in> getRel l G \<Longrightarrow> (y, x) \<in> (getRel I G O getRel l G) O getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
note zx = this
[PROOF STATE]
proof (state)
this:
(z, x) \<in> getRel l G \<Longrightarrow> (y, x) \<in> (getRel I G O getRel l G) O getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
from zx yx m[unfolded maintained_holds_subset_iff[OF g] congruence_rule_def]
[PROOF STATE]
proof (chain)
picking this:
(z, x) \<in> getRel l G \<Longrightarrow> (y, x) \<in> (getRel I G O getRel l G) O getRel I G
(y, x) \<in> getRel l G \<Longrightarrow> (z, x) \<in> (getRel I G O getRel l G) O getRel I G
:G:\<lbrakk>A_Cmp (A_Cmp (A_Lbl I) (A_Lbl l)) (A_Lbl I)\<rbrakk> \<subseteq> :G:\<lbrakk>A_Lbl l\<rbrakk>
[PROOF STEP]
have "(y,x) \<in> getRel l G \<longleftrightarrow> (z,x) \<in> getRel l G"
[PROOF STATE]
proof (prove)
using this:
(z, x) \<in> getRel l G \<Longrightarrow> (y, x) \<in> (getRel I G O getRel l G) O getRel I G
(y, x) \<in> getRel l G \<Longrightarrow> (z, x) \<in> (getRel I G O getRel l G) O getRel I G
:G:\<lbrakk>A_Cmp (A_Cmp (A_Lbl I) (A_Lbl l)) (A_Lbl I)\<rbrakk> \<subseteq> :G:\<lbrakk>A_Lbl l\<rbrakk>

goal (1 subgoal):
 1. ((y, x) \<in> getRel l G) = ((z, x) \<in> getRel l G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((y, x) \<in> getRel l G) = ((z, x) \<in> getRel l G)

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
((y, ?x2) \<in> getRel l G) = ((z, ?x2) \<in> getRel l G)

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
note v1 = this
[PROOF STATE]
proof (state)
this:
((y, ?x2) \<in> getRel l G) = ((z, ?x2) \<in> getRel l G)

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
((y, ?x2) \<in> getRel l G) = ((z, ?x2) \<in> getRel l G)

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
assume al:"(x,y) \<in> getRel l G"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> getRel l G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
hence "x \<in> vertices G"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> getRel l G

goal (1 subgoal):
 1. x \<in> vertices G
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> getRel l G
graph G

goal (1 subgoal):
 1. x \<in> vertices G
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(x, y). (l, x, y) \<in> edges G}
graph G

goal (1 subgoal):
 1. x \<in> vertices G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vertices G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
hence r:"(x,x) \<in> getRel I G"
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices G

goal (1 subgoal):
 1. (x, x) \<in> getRel I G
[PROOF STEP]
using eq[unfolded equiv_def refl_on_def]
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices G
(getRel I G \<subseteq> vertices G \<times> vertices G \<and> (\<forall>x\<in>vertices G. (x, x) \<in> getRel I G)) \<and> sym (getRel I G) \<and> trans (getRel I G)

goal (1 subgoal):
 1. (x, x) \<in> getRel I G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, x) \<in> getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
note relcompI[OF relcompI[OF r al] aI]
[PROOF STATE]
proof (state)
this:
(x, z) \<in> (getRel I G O getRel l G) O getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(x, y) \<in> getRel l G \<Longrightarrow> (x, z) \<in> (getRel I G O getRel l G) O getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
note yx = this
[PROOF STATE]
proof (state)
this:
(x, y) \<in> getRel l G \<Longrightarrow> (x, z) \<in> (getRel I G O getRel l G) O getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(x, y) \<in> getRel l G \<Longrightarrow> (x, z) \<in> (getRel I G O getRel l G) O getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
assume al:"(x,z) \<in> getRel l G"
[PROOF STATE]
proof (state)
this:
(x, z) \<in> getRel l G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
hence "x \<in> vertices G"
[PROOF STATE]
proof (prove)
using this:
(x, z) \<in> getRel l G

goal (1 subgoal):
 1. x \<in> vertices G
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
(x, z) \<in> getRel l G
graph G

goal (1 subgoal):
 1. x \<in> vertices G
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(x, z) \<in> {(x, y). (l, x, y) \<in> edges G}
graph G

goal (1 subgoal):
 1. x \<in> vertices G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vertices G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
hence r:"(x,x) \<in> getRel I G"
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices G

goal (1 subgoal):
 1. (x, x) \<in> getRel I G
[PROOF STEP]
using eq[unfolded equiv_def refl_on_def]
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices G
(getRel I G \<subseteq> vertices G \<times> vertices G \<and> (\<forall>x\<in>vertices G. (x, x) \<in> getRel I G)) \<and> sym (getRel I G) \<and> trans (getRel I G)

goal (1 subgoal):
 1. (x, x) \<in> getRel I G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, x) \<in> getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
note relcompI[OF relcompI[OF r al] a2]
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (getRel I G O getRel l G) O getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(x, z) \<in> getRel l G \<Longrightarrow> (x, y) \<in> (getRel I G O getRel l G) O getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
note zx = this
[PROOF STATE]
proof (state)
this:
(x, z) \<in> getRel l G \<Longrightarrow> (x, y) \<in> (getRel I G O getRel l G) O getRel I G

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
from zx yx m[unfolded maintained_holds_subset_iff[OF g] congruence_rule_def]
[PROOF STATE]
proof (chain)
picking this:
(x, z) \<in> getRel l G \<Longrightarrow> (x, y) \<in> (getRel I G O getRel l G) O getRel I G
(x, y) \<in> getRel l G \<Longrightarrow> (x, z) \<in> (getRel I G O getRel l G) O getRel I G
:G:\<lbrakk>A_Cmp (A_Cmp (A_Lbl I) (A_Lbl l)) (A_Lbl I)\<rbrakk> \<subseteq> :G:\<lbrakk>A_Lbl l\<rbrakk>
[PROOF STEP]
have "(x,y) \<in> getRel l G \<longleftrightarrow> (x,z) \<in> getRel l G"
[PROOF STATE]
proof (prove)
using this:
(x, z) \<in> getRel l G \<Longrightarrow> (x, y) \<in> (getRel I G O getRel l G) O getRel I G
(x, y) \<in> getRel l G \<Longrightarrow> (x, z) \<in> (getRel I G O getRel l G) O getRel I G
:G:\<lbrakk>A_Cmp (A_Cmp (A_Lbl I) (A_Lbl l)) (A_Lbl I)\<rbrakk> \<subseteq> :G:\<lbrakk>A_Lbl l\<rbrakk>

goal (1 subgoal):
 1. ((x, y) \<in> getRel l G) = ((x, z) \<in> getRel l G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((x, y) \<in> getRel l G) = ((x, z) \<in> getRel l G)

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
((?x2, y) \<in> getRel l G) = ((?x2, z) \<in> getRel l G)

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
note v2 = this
[PROOF STATE]
proof (state)
this:
((?x2, y) \<in> getRel l G) = ((?x2, z) \<in> getRel l G)

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
from v1 v2
[PROOF STATE]
proof (chain)
picking this:
((y, ?x2) \<in> getRel l G) = ((z, ?x2) \<in> getRel l G)
((?x2, y) \<in> getRel l G) = ((?x2, z) \<in> getRel l G)
[PROOF STEP]
have "getRel l G `` {y} = getRel l G `` {z}"
         "(getRel l G)\<inverse> `` {y} = (getRel l G)\<inverse> `` {z}"
[PROOF STATE]
proof (prove)
using this:
((y, ?x2) \<in> getRel l G) = ((z, ?x2) \<in> getRel l G)
((?x2, y) \<in> getRel l G) = ((?x2, z) \<in> getRel l G)

goal (1 subgoal):
 1. getRel l G `` {y} = getRel l G `` {z} &&& (getRel l G)\<inverse> `` {y} = (getRel l G)\<inverse> `` {z}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getRel l G `` {y} = getRel l G `` {z}
(getRel l G)\<inverse> `` {y} = (getRel l G)\<inverse> `` {z}

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?y2, ?z2) \<in> getRel I G \<Longrightarrow> getRel l G `` {?y2} = getRel l G `` {?z2}
(?y2, ?z2) \<in> getRel I G \<Longrightarrow> (getRel l G)\<inverse> `` {?y2} = (getRel l G)\<inverse> `` {?z2}

goal (2 subgoals):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G
 2. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
thus ?g1 ?g2
[PROOF STATE]
proof (prove)
using this:
(?y2, ?z2) \<in> getRel I G \<Longrightarrow> getRel l G `` {?y2} = getRel l G `` {?z2}
(?y2, ?z2) \<in> getRel I G \<Longrightarrow> (getRel l G)\<inverse> `` {?y2} = (getRel l G)\<inverse> `` {?z2}

goal (1 subgoal):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel I G &&& (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G
[PROOF STEP]
unfolding congruent_def
[PROOF STATE]
proof (prove)
using this:
(?y2, ?z2) \<in> getRel I G \<Longrightarrow> getRel l G `` {?y2} = getRel l G `` {?z2}
(?y2, ?z2) \<in> getRel I G \<Longrightarrow> (getRel l G)\<inverse> `` {?y2} = (getRel l G)\<inverse> `` {?z2}

goal (1 subgoal):
 1. \<forall>(y, z)\<in>getRel I G. getRel l G `` {y} = getRel l G `` {z} &&& \<forall>(y, z)\<in>getRel I G. (getRel l G)\<inverse> `` {y} = (getRel l G)\<inverse> `` {z}
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
(\<lambda>v. getRel l G `` {v}) respects getRel I G
(\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel I G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma identity_rules:
  assumes "graph G"
          "maintainedA (identity_rules L) G"
          "fst ` edges G \<subseteq> L"
  shows "\<exists> f. f o f = f
         \<and> ident_rel S_Idt (map_graph_fn G f)
         \<and> subgraph (map_graph_fn G f) G
         \<and> (\<forall> l x y. (l,x,y) \<in> edges G \<longleftrightarrow> (l,f x,f y) \<in> edges G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
(* 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. *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
have ma:"maintainedA {reflexivity_rule S_Idt, transitive_rule S_Idt, symmetry_rule S_Idt} G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintainedA {reflexivity_rule S_Idt, transitive_rule S_Idt, symmetry_rule S_Idt} G
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
maintainedA (identity_rules L) G

goal (1 subgoal):
 1. maintainedA {reflexivity_rule S_Idt, transitive_rule S_Idt, symmetry_rule S_Idt} G
[PROOF STEP]
by (auto simp:identity_rules_def)
[PROOF STATE]
proof (state)
this:
maintainedA {reflexivity_rule S_Idt, transitive_rule S_Idt, symmetry_rule S_Idt} G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
note equiv = equivalence[OF assms(1) this]
[PROOF STATE]
proof (state)
this:
equiv (vertices G) (getRel S_Idt G)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
equiv (vertices G) (getRel S_Idt G)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
fix l x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
assume "(x, y) \<in> getRel l G"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> getRel l G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence l:"l \<in> L"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> getRel l G

goal (1 subgoal):
 1. l \<in> L
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> getRel l G
fst ` edges G \<subseteq> L

goal (1 subgoal):
 1. l \<in> L
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(x, y). (l, x, y) \<in> edges G}
fst ` edges G \<subseteq> L

goal (1 subgoal):
 1. l \<in> L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<in> L

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
have r1:"(\<lambda>v. getRel l G `` {v}) respects getRel S_Idt G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v. getRel l G `` {v}) respects getRel S_Idt G
[PROOF STEP]
apply(intro congruence_rule[OF assms(1) ma])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained (congruence_rule S_Idt l) G
[PROOF STEP]
using assms(2) l
[PROOF STATE]
proof (prove)
using this:
maintainedA (identity_rules L) G
l \<in> L

goal (1 subgoal):
 1. maintained (congruence_rule S_Idt l) G
[PROOF STEP]
unfolding identity_rules_def
[PROOF STATE]
proof (prove)
using this:
maintainedA ({reflexivity_rule S_Idt, transitive_rule S_Idt, symmetry_rule S_Idt} \<union> congruence_rules S_Idt L) G
l \<in> L

goal (1 subgoal):
 1. maintained (congruence_rule S_Idt l) G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>v. getRel l G `` {v}) respects getRel S_Idt G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
have r2:"(\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel S_Idt G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel S_Idt G
[PROOF STEP]
apply(intro congruence_rule[OF assms(1) ma])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained (congruence_rule S_Idt l) G
[PROOF STEP]
using assms(2) l
[PROOF STATE]
proof (prove)
using this:
maintainedA (identity_rules L) G
l \<in> L

goal (1 subgoal):
 1. maintained (congruence_rule S_Idt l) G
[PROOF STEP]
unfolding identity_rules_def
[PROOF STATE]
proof (prove)
using this:
maintainedA ({reflexivity_rule S_Idt, transitive_rule S_Idt, symmetry_rule S_Idt} \<union> congruence_rules S_Idt L) G
l \<in> L

goal (1 subgoal):
 1. maintained (congruence_rule S_Idt l) G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel S_Idt G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
note congr = r1 r2
[PROOF STATE]
proof (state)
this:
(\<lambda>v. getRel l G `` {v}) respects getRel S_Idt G
(\<lambda>v. (getRel l G)\<inverse> `` {v}) respects getRel S_Idt G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?x2, ?y2) \<in> getRel ?l2 G \<Longrightarrow> (\<lambda>v. getRel ?l2 G `` {v}) respects getRel S_Idt G
(?x2, ?y2) \<in> getRel ?l2 G \<Longrightarrow> (\<lambda>v. (getRel ?l2 G)\<inverse> `` {v}) respects getRel S_Idt G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
note congr = this
[PROOF STATE]
proof (state)
this:
(?x2, ?y2) \<in> getRel ?l2 G \<Longrightarrow> (\<lambda>v. getRel ?l2 G `` {v}) respects getRel S_Idt G
(?x2, ?y2) \<in> getRel ?l2 G \<Longrightarrow> (\<lambda>v. (getRel ?l2 G)\<inverse> `` {v}) respects getRel S_Idt G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
define P where P:"P = (\<lambda> x y. y \<in> getRel S_Idt G `` {x})"
[PROOF STATE]
proof (state)
this:
P = (\<lambda>x y. y \<in> getRel S_Idt G `` {x})

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
P = (\<lambda>x y. y \<in> getRel S_Idt G `` {x})

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
assume a:"getRel S_Idt G `` {x} \<noteq> {}"
[PROOF STATE]
proof (state)
this:
getRel S_Idt G `` {x} \<noteq> {}

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence "\<exists> y. P x y"
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt G `` {x} \<noteq> {}

goal (1 subgoal):
 1. \<exists>y. P x y
[PROOF STEP]
unfolding P
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt G `` {x} \<noteq> {}

goal (1 subgoal):
 1. \<exists>y. y \<in> getRel S_Idt G `` {x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y. P x y

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence p:"P x (Eps (P x))"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. P x y

goal (1 subgoal):
 1. P x (Eps (P x))
[PROOF STEP]
unfolding some_eq_ex
[PROOF STATE]
proof (prove)
using this:
\<exists>y. P x y

goal (1 subgoal):
 1. Ex (P x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P x (Eps (P x))

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
P x (Eps (P x))

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
assume b:"P x y"
[PROOF STATE]
proof (state)
this:
P x y

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence "(x,y) \<in> getRel S_Idt G"
[PROOF STATE]
proof (prove)
using this:
P x y

goal (1 subgoal):
 1. (x, y) \<in> getRel S_Idt G
[PROOF STEP]
unfolding P
[PROOF STATE]
proof (prove)
using this:
y \<in> getRel S_Idt G `` {x}

goal (1 subgoal):
 1. (x, y) \<in> getRel S_Idt G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> getRel S_Idt G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
from equiv_class_eq[OF equiv this]
[PROOF STATE]
proof (chain)
picking this:
getRel S_Idt G `` {x} = getRel S_Idt G `` {y}
[PROOF STEP]
have "getRel S_Idt G `` {x} = getRel S_Idt G `` {y}"
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt G `` {x} = getRel S_Idt G `` {y}

goal (1 subgoal):
 1. getRel S_Idt G `` {x} = getRel S_Idt G `` {y}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
getRel S_Idt G `` {x} = getRel S_Idt G `` {y}

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
P x ?y2 \<Longrightarrow> getRel S_Idt G `` {x} = getRel S_Idt G `` {?y2}

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
note u = this[OF p]
[PROOF STATE]
proof (state)
this:
getRel S_Idt G `` {x} = getRel S_Idt G `` {Eps (P x)}

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
have "getRel S_Idt G `` {Eps (P x)} = getRel S_Idt G `` {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getRel S_Idt G `` {Eps (P x)} = getRel S_Idt G `` {x}
[PROOF STEP]
unfolding u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getRel S_Idt G `` {Eps (P x)} = getRel S_Idt G `` {Eps (P x)}
[PROOF STEP]
by (fact refl)
[PROOF STATE]
proof (state)
this:
getRel S_Idt G `` {Eps (P x)} = getRel S_Idt G `` {x}

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence "Eps (P (Eps (P x))) = Eps (P x)"
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt G `` {Eps (P x)} = getRel S_Idt G `` {x}

goal (1 subgoal):
 1. Eps (P (Eps (P x))) = Eps (P x)
[PROOF STEP]
unfolding P
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt G `` {SOME y. y \<in> getRel S_Idt G `` {x}} = getRel S_Idt G `` {x}

goal (1 subgoal):
 1. (SOME y. y \<in> getRel S_Idt G `` {SOME y. y \<in> getRel S_Idt G `` {x}}) = (SOME y. y \<in> getRel S_Idt G `` {x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Eps (P (Eps (P x))) = Eps (P x)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
getRel S_Idt G `` {?x2} \<noteq> {} \<Longrightarrow> Eps (P (Eps (P ?x2))) = Eps (P ?x2)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
note P_eq = this
[PROOF STATE]
proof (state)
this:
getRel S_Idt G `` {?x2} \<noteq> {} \<Longrightarrow> Eps (P (Eps (P ?x2))) = Eps (P ?x2)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
define f where f:"f = (\<lambda> x. (if getRel S_Idt G `` {x} = {} then x else (SOME y. P x y)))"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>x. if getRel S_Idt G `` {x} = {} then x else SOME y. P x y)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
have "(f \<circ> f) x = f x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<circ> f) x = f x
[PROOF STEP]
proof(cases "getRel S_Idt G `` {x} = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. getRel S_Idt G `` {x} = {} \<Longrightarrow> (f \<circ> f) x = f x
 2. getRel S_Idt G `` {x} \<noteq> {} \<Longrightarrow> (f \<circ> f) x = f x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
getRel S_Idt G `` {x} \<noteq> {}

goal (2 subgoals):
 1. getRel S_Idt G `` {x} = {} \<Longrightarrow> (f \<circ> f) x = f x
 2. getRel S_Idt G `` {x} \<noteq> {} \<Longrightarrow> (f \<circ> f) x = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
getRel S_Idt G `` {x} \<noteq> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt G `` {x} \<noteq> {}

goal (1 subgoal):
 1. (f \<circ> f) x = f x
[PROOF STEP]
using P_eq
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt G `` {x} \<noteq> {}
getRel S_Idt G `` {?x2} \<noteq> {} \<Longrightarrow> Eps (P (Eps (P ?x2))) = Eps (P ?x2)

goal (1 subgoal):
 1. (f \<circ> f) x = f x
[PROOF STEP]
by (simp add:o_def f)
[PROOF STATE]
proof (state)
this:
(f \<circ> f) x = f x

goal (1 subgoal):
 1. getRel S_Idt G `` {x} = {} \<Longrightarrow> (f \<circ> f) x = f x
[PROOF STEP]
qed (auto simp:o_def f)
[PROOF STATE]
proof (state)
this:
(f \<circ> f) ?x = f ?x

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence idemp: "f o f = f"
[PROOF STATE]
proof (prove)
using this:
(f \<circ> f) ?x = f ?x

goal (1 subgoal):
 1. f \<circ> f = f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<circ> f = f

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
from equivE equiv
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>equiv ?A ?r; \<lbrakk>refl_on ?A ?r; sym ?r; trans ?r\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
equiv (vertices G) (getRel S_Idt G)
[PROOF STEP]
have refl:"refl_on (vertices G) (getRel S_Idt G)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>equiv ?A ?r; \<lbrakk>refl_on ?A ?r; sym ?r; trans ?r\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
equiv (vertices G) (getRel S_Idt G)

goal (1 subgoal):
 1. refl_on (vertices G) (getRel S_Idt G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
refl_on (vertices G) (getRel S_Idt G)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence [intro]:"x \<in> vertices G \<Longrightarrow> (x, x) \<in> getRel S_Idt G" for x
[PROOF STATE]
proof (prove)
using this:
refl_on (vertices G) (getRel S_Idt G)

goal (1 subgoal):
 1. x \<in> vertices G \<Longrightarrow> (x, x) \<in> getRel S_Idt G
[PROOF STEP]
unfolding refl_on_def
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt G \<subseteq> vertices G \<times> vertices G \<and> (\<forall>x\<in>vertices G. (x, x) \<in> getRel S_Idt G)

goal (1 subgoal):
 1. x \<in> vertices G \<Longrightarrow> (x, x) \<in> getRel S_Idt G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> vertices G \<Longrightarrow> (?x, ?x) \<in> getRel S_Idt G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence vert_P:"x \<in> vertices G \<Longrightarrow> (x, Eps (P x)) \<in> getRel S_Idt G" for x
[PROOF STATE]
proof (prove)
using this:
?x \<in> vertices G \<Longrightarrow> (?x, ?x) \<in> getRel S_Idt G

goal (1 subgoal):
 1. x \<in> vertices G \<Longrightarrow> (x, Eps (P x)) \<in> getRel S_Idt G
[PROOF STEP]
unfolding P getRel_def
[PROOF STATE]
proof (prove)
using this:
?x \<in> vertices G \<Longrightarrow> (?x, ?x) \<in> {(x, y). (S_Idt, x, y) \<in> edges G}

goal (1 subgoal):
 1. x \<in> vertices G \<Longrightarrow> (x, SOME y. y \<in> {(x, y). (S_Idt, x, y) \<in> edges G} `` {x}) \<in> {(x, y). (S_Idt, x, y) \<in> edges G}
[PROOF STEP]
by (metis tfl_some Image_singleton_iff getRel_def)
[PROOF STATE]
proof (state)
this:
?x \<in> vertices G \<Longrightarrow> (?x, Eps (P ?x)) \<in> getRel S_Idt G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
have r1:"x \<in> vertices G \<longleftrightarrow> P x x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> vertices G) = P x x
[PROOF STEP]
using refl
[PROOF STATE]
proof (prove)
using this:
refl_on (vertices G) (getRel S_Idt G)

goal (1 subgoal):
 1. (x \<in> vertices G) = P x x
[PROOF STEP]
unfolding refl_on_def P
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt G \<subseteq> vertices G \<times> vertices G \<and> (\<forall>x\<in>vertices G. (x, x) \<in> getRel S_Idt G)

goal (1 subgoal):
 1. (x \<in> vertices G) = (x \<in> getRel S_Idt G `` {x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(?x \<in> vertices G) = P ?x ?x

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
have r2[simp]:"getRel S_Idt G `` {x} = {} \<longleftrightarrow> x \<notin> vertices G" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (getRel S_Idt G `` {x} = {}) = (x \<notin> vertices G)
[PROOF STEP]
using refl assms(1)
[PROOF STATE]
proof (prove)
using this:
refl_on (vertices G) (getRel S_Idt G)
graph G

goal (1 subgoal):
 1. (getRel S_Idt G `` {x} = {}) = (x \<notin> vertices G)
[PROOF STEP]
unfolding refl_on_def
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt G \<subseteq> vertices G \<times> vertices G \<and> (\<forall>x\<in>vertices G. (x, x) \<in> getRel S_Idt G)
graph G

goal (1 subgoal):
 1. (getRel S_Idt G `` {x} = {}) = (x \<notin> vertices G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(getRel S_Idt G `` {?x} = {}) = (?x \<notin> vertices G)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(getRel S_Idt G `` {?x} = {}) = (?x \<notin> vertices G)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
assume "(S_Idt,x,y)\<in> edges G"
[PROOF STATE]
proof (state)
this:
(S_Idt, x, y) \<in> edges G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence "(x,y) \<in> getRel S_Idt G"
[PROOF STATE]
proof (prove)
using this:
(S_Idt, x, y) \<in> edges G

goal (1 subgoal):
 1. (x, y) \<in> getRel S_Idt G
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(S_Idt, x, y) \<in> edges G

goal (1 subgoal):
 1. (x, y) \<in> {(x, y). (S_Idt, x, y) \<in> edges G}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> getRel S_Idt G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence "getRel S_Idt G `` {x} = getRel S_Idt G `` {y}"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> getRel S_Idt G

goal (1 subgoal):
 1. getRel S_Idt G `` {x} = getRel S_Idt G `` {y}
[PROOF STEP]
using equiv_class_eq[OF equiv]
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> getRel S_Idt G
(?a, ?b) \<in> getRel S_Idt G \<Longrightarrow> getRel S_Idt G `` {?a} = getRel S_Idt G `` {?b}

goal (1 subgoal):
 1. getRel S_Idt G `` {x} = getRel S_Idt G `` {y}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
getRel S_Idt G `` {x} = getRel S_Idt G `` {y}

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence "Eps (P x) = Eps (P y)"
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt G `` {x} = getRel S_Idt G `` {y}

goal (1 subgoal):
 1. Eps (P x) = Eps (P y)
[PROOF STEP]
unfolding P
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt G `` {x} = getRel S_Idt G `` {y}

goal (1 subgoal):
 1. (SOME y. y \<in> getRel S_Idt G `` {x}) = (SOME ya. ya \<in> getRel S_Idt G `` {y})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Eps (P x) = Eps (P y)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(S_Idt, ?x2, ?y2) \<in> edges G \<Longrightarrow> Eps (P ?x2) = Eps (P ?y2)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
note idt_eq = this
[PROOF STATE]
proof (state)
this:
(S_Idt, ?x2, ?y2) \<in> edges G \<Longrightarrow> Eps (P ?x2) = Eps (P ?y2)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
have ident:"ident_rel S_Idt (map_graph_fn G f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ident_rel S_Idt (map_graph_fn G f)
[PROOF STEP]
proof(rule ident_relI,goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> vertices (map_graph_fn G f) \<Longrightarrow> (x, x) \<in> getRel S_Idt (map_graph_fn G f)
 2. \<And>x y. (x, y) \<in> getRel S_Idt (map_graph_fn G f) \<Longrightarrow> x = y
 3. \<And>x y. (x, y) \<in> getRel S_Idt (map_graph_fn G f) \<Longrightarrow> x \<in> vertices (map_graph_fn G f)
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:
x \<in> vertices (map_graph_fn G f)

goal (3 subgoals):
 1. \<And>x. x \<in> vertices (map_graph_fn G f) \<Longrightarrow> (x, x) \<in> getRel S_Idt (map_graph_fn G f)
 2. \<And>x y. (x, y) \<in> getRel S_Idt (map_graph_fn G f) \<Longrightarrow> x = y
 3. \<And>x y. (x, y) \<in> getRel S_Idt (map_graph_fn G f) \<Longrightarrow> x \<in> vertices (map_graph_fn G f)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices (map_graph_fn G f)

goal (1 subgoal):
 1. (x, x) \<in> getRel S_Idt (map_graph_fn G f)
[PROOF STEP]
unfolding f
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices (map_graph_fn G (\<lambda>x. if getRel S_Idt G `` {x} = {} then x else Eps (P x)))

goal (1 subgoal):
 1. (x, x) \<in> getRel S_Idt (map_graph_fn G (\<lambda>x. if getRel S_Idt G `` {x} = {} then x else Eps (P x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, x) \<in> getRel S_Idt (map_graph_fn G f)

goal (2 subgoals):
 1. \<And>x y. (x, y) \<in> getRel S_Idt (map_graph_fn G f) \<Longrightarrow> x = y
 2. \<And>x y. (x, y) \<in> getRel S_Idt (map_graph_fn G f) \<Longrightarrow> x \<in> vertices (map_graph_fn G f)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. (x, y) \<in> getRel S_Idt (map_graph_fn G f) \<Longrightarrow> x = y
 2. \<And>x y. (x, y) \<in> getRel S_Idt (map_graph_fn G f) \<Longrightarrow> x \<in> vertices (map_graph_fn G f)
[PROOF STEP]
case (2 x y)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> getRel S_Idt (map_graph_fn G f)

goal (2 subgoals):
 1. \<And>x y. (x, y) \<in> getRel S_Idt (map_graph_fn G f) \<Longrightarrow> x = y
 2. \<And>x y. (x, y) \<in> getRel S_Idt (map_graph_fn G f) \<Longrightarrow> x \<in> vertices (map_graph_fn G f)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> getRel S_Idt (map_graph_fn G f)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(x, y). (S_Idt, x, y) \<in> edges (map_graph_fn G f)}

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (auto simp:f intro!:idt_eq)
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> getRel S_Idt (map_graph_fn G f) \<Longrightarrow> x \<in> vertices (map_graph_fn G f)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> getRel S_Idt (map_graph_fn G f) \<Longrightarrow> x \<in> vertices (map_graph_fn G f)
[PROOF STEP]
case (3 x y)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> getRel S_Idt (map_graph_fn G f)

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> getRel S_Idt (map_graph_fn G f) \<Longrightarrow> x \<in> vertices (map_graph_fn G f)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> getRel S_Idt (map_graph_fn G f)

goal (1 subgoal):
 1. x \<in> vertices (map_graph_fn G f)
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(x, y). (S_Idt, x, y) \<in> edges (map_graph_fn G f)}

goal (1 subgoal):
 1. x \<in> vertices (map_graph_fn G f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vertices (map_graph_fn G f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ident_rel S_Idt (map_graph_fn G f)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ident_rel S_Idt (map_graph_fn G f)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
fix l x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
assume a:"(l,x,y) \<in> edges G" "x \<in> vertices G" "y \<in> vertices G"
[PROOF STATE]
proof (state)
this:
(l, x, y) \<in> edges G
x \<in> vertices G
y \<in> vertices G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence f:"(f x, x) \<in> getRel S_Idt G" "(f y, y) \<in> getRel S_Idt G"
[PROOF STATE]
proof (prove)
using this:
(l, x, y) \<in> edges G
x \<in> vertices G
y \<in> vertices G

goal (1 subgoal):
 1. (f x, x) \<in> getRel S_Idt G &&& (f y, y) \<in> getRel S_Idt G
[PROOF STEP]
using vert_P equivE[OF equiv] sym_def
[PROOF STATE]
proof (prove)
using this:
(l, x, y) \<in> edges G
x \<in> vertices G
y \<in> vertices G
?x \<in> vertices G \<Longrightarrow> (?x, Eps (P ?x)) \<in> getRel S_Idt G
(\<lbrakk>refl_on (vertices G) (getRel S_Idt G); sym (getRel S_Idt G); trans (getRel S_Idt G)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
sym ?r = (\<forall>x y. (x, y) \<in> ?r \<longrightarrow> (y, x) \<in> ?r)

goal (1 subgoal):
 1. (f x, x) \<in> getRel S_Idt G &&& (f y, y) \<in> getRel S_Idt G
[PROOF STEP]
unfolding f
[PROOF STATE]
proof (prove)
using this:
(l, x, y) \<in> edges G
x \<in> vertices G
y \<in> vertices G
?x \<in> vertices G \<Longrightarrow> (?x, Eps (P ?x)) \<in> getRel S_Idt G
(\<lbrakk>refl_on (vertices G) (getRel S_Idt G); sym (getRel S_Idt G); trans (getRel S_Idt G)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
sym ?r = (\<forall>x y. (x, y) \<in> ?r \<longrightarrow> (y, x) \<in> ?r)

goal (1 subgoal):
 1. (if getRel S_Idt G `` {x} = {} then x else Eps (P x), x) \<in> getRel S_Idt G &&& (if getRel S_Idt G `` {y} = {} then y else Eps (P y), y) \<in> getRel S_Idt G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f x, x) \<in> getRel S_Idt G
(f y, y) \<in> getRel S_Idt G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
(l, x, y) \<in> edges G
x \<in> vertices G
y \<in> vertices G
[PROOF STEP]
have gr:"(x, y) \<in> getRel l G"
[PROOF STATE]
proof (prove)
using this:
(l, x, y) \<in> edges G
x \<in> vertices G
y \<in> vertices G

goal (1 subgoal):
 1. (x, y) \<in> getRel l G
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(l, x, y) \<in> edges G
x \<in> vertices G
y \<in> vertices G

goal (1 subgoal):
 1. (x, y) \<in> {(x, y). (l, x, y) \<in> edges G}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> getRel l G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
from congruentD[OF congr(1)[OF gr] f(1)] congruentD[OF congr(2)[OF gr] f(2)] a(1)
[PROOF STATE]
proof (chain)
picking this:
getRel l G `` {f x} = getRel l G `` {x}
(getRel l G)\<inverse> `` {f y} = (getRel l G)\<inverse> `` {y}
(l, x, y) \<in> edges G
[PROOF STEP]
have "(l,f x, f y) \<in> edges G"
[PROOF STATE]
proof (prove)
using this:
getRel l G `` {f x} = getRel l G `` {x}
(getRel l G)\<inverse> `` {f y} = (getRel l G)\<inverse> `` {y}
(l, x, y) \<in> edges G

goal (1 subgoal):
 1. (l, f x, f y) \<in> edges G
[PROOF STEP]
unfolding set_eq_iff getRel_def
[PROOF STATE]
proof (prove)
using this:
\<forall>xa. (xa \<in> {(x, y). (l, x, y) \<in> edges G} `` {f x}) = (xa \<in> {(x, y). (l, x, y) \<in> edges G} `` {x})
\<forall>x. (x \<in> {(x, y). (l, x, y) \<in> edges G}\<inverse> `` {f y}) = (x \<in> {(x, y). (l, x, y) \<in> edges G}\<inverse> `` {y})
(l, x, y) \<in> edges G

goal (1 subgoal):
 1. (l, f x, f y) \<in> edges G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(l, f x, f y) \<in> edges G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?l2, ?x2, ?y2) \<in> edges G; ?x2 \<in> vertices G; ?y2 \<in> vertices G\<rbrakk> \<Longrightarrow> (?l2, f ?x2, f ?y2) \<in> edges G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
note gu1 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?l2, ?x2, ?y2) \<in> edges G; ?x2 \<in> vertices G; ?y2 \<in> vertices G\<rbrakk> \<Longrightarrow> (?l2, f ?x2, f ?y2) \<in> edges G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?l2, ?x2, ?y2) \<in> edges G; ?x2 \<in> vertices G; ?y2 \<in> vertices G\<rbrakk> \<Longrightarrow> (?l2, f ?x2, f ?y2) \<in> edges G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
assume a: "x \<in> vertices G"
[PROOF STATE]
proof (state)
this:
x \<in> vertices G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
with vert_P
[PROOF STATE]
proof (chain)
picking this:
?x \<in> vertices G \<Longrightarrow> (?x, Eps (P ?x)) \<in> getRel S_Idt G
x \<in> vertices G
[PROOF STEP]
have "(x,Eps (P x)) \<in> getRel S_Idt G"
[PROOF STATE]
proof (prove)
using this:
?x \<in> vertices G \<Longrightarrow> (?x, Eps (P ?x)) \<in> getRel S_Idt G
x \<in> vertices G

goal (1 subgoal):
 1. (x, Eps (P x)) \<in> getRel S_Idt G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, Eps (P x)) \<in> getRel S_Idt G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence "Eps (P x) \<in> vertices G"
[PROOF STATE]
proof (prove)
using this:
(x, Eps (P x)) \<in> getRel S_Idt G

goal (1 subgoal):
 1. Eps (P x) \<in> vertices G
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
(x, Eps (P x)) \<in> getRel S_Idt G
graph G

goal (1 subgoal):
 1. Eps (P x) \<in> vertices G
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(x, Eps (P x)) \<in> {(x, y). (S_Idt, x, y) \<in> edges G}
graph G

goal (1 subgoal):
 1. Eps (P x) \<in> vertices G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Eps (P x) \<in> vertices G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence "f x \<in> vertices G"
[PROOF STATE]
proof (prove)
using this:
Eps (P x) \<in> vertices G

goal (1 subgoal):
 1. f x \<in> vertices G
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
Eps (P x) \<in> vertices G
x \<in> vertices G

goal (1 subgoal):
 1. f x \<in> vertices G
[PROOF STEP]
unfolding f
[PROOF STATE]
proof (prove)
using this:
Eps (P x) \<in> vertices G
x \<in> vertices G

goal (1 subgoal):
 1. (if getRel S_Idt G `` {x} = {} then x else Eps (P x)) \<in> vertices G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f x \<in> vertices G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> vertices G \<Longrightarrow> f ?x2 \<in> vertices G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
note gu2 = this
[PROOF STATE]
proof (state)
this:
?x2 \<in> vertices G \<Longrightarrow> f ?x2 \<in> vertices G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
have "graph_union (map_graph_fn G f) G = G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_union (map_graph_fn G f) G = G
[PROOF STEP]
using gu1 gu2 assms(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?l2, ?x2, ?y2) \<in> edges G; ?x2 \<in> vertices G; ?y2 \<in> vertices G\<rbrakk> \<Longrightarrow> (?l2, f ?x2, f ?y2) \<in> edges G
?x2 \<in> vertices G \<Longrightarrow> f ?x2 \<in> vertices G
graph G

goal (1 subgoal):
 1. graph_union (map_graph_fn G f) G = G
[PROOF STEP]
unfolding graph_union_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?l2, ?x2, ?y2) \<in> edges G; ?x2 \<in> vertices G; ?y2 \<in> vertices G\<rbrakk> \<Longrightarrow> (?l2, f ?x2, f ?y2) \<in> edges G
?x2 \<in> vertices G \<Longrightarrow> f ?x2 \<in> vertices G
graph G

goal (1 subgoal):
 1. LG (edges (map_graph_fn G f) \<union> edges G) (vertices (map_graph_fn G f) \<union> vertices G) = G
[PROOF STEP]
by(cases G,auto)
[PROOF STATE]
proof (state)
this:
graph_union (map_graph_fn G f) G = G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
hence subg: "subgraph (map_graph_fn G f) G"
[PROOF STATE]
proof (prove)
using this:
graph_union (map_graph_fn G f) G = G

goal (1 subgoal):
 1. subgraph (map_graph_fn G f) G
[PROOF STEP]
unfolding subgraph_def
[PROOF STATE]
proof (prove)
using this:
graph_union (map_graph_fn G f) G = G

goal (1 subgoal):
 1. graph (map_graph_fn G f) \<and> graph G \<and> graph_union (map_graph_fn G f) G = G
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
graph_union (map_graph_fn G f) G = G
graph G

goal (1 subgoal):
 1. graph (map_graph_fn G f) \<and> graph G \<and> graph_union (map_graph_fn G f) G = G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subgraph (map_graph_fn G f) G

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
have congr:"((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G)" for l x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (l, x, y) \<in> edges G \<Longrightarrow> (l, f x, f y) \<in> edges G
 2. (l, f x, f y) \<in> edges G \<Longrightarrow> (l, x, y) \<in> edges G
[PROOF STEP]
assume a:"((l, f x, f y) \<in> edges G)"
[PROOF STATE]
proof (state)
this:
(l, f x, f y) \<in> edges G

goal (2 subgoals):
 1. (l, x, y) \<in> edges G \<Longrightarrow> (l, f x, f y) \<in> edges G
 2. (l, f x, f y) \<in> edges G \<Longrightarrow> (l, x, y) \<in> edges G
[PROOF STEP]
hence gr:"(f x, f y) \<in> getRel l G"
[PROOF STATE]
proof (prove)
using this:
(l, f x, f y) \<in> edges G

goal (1 subgoal):
 1. (f x, f y) \<in> getRel l G
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(l, f x, f y) \<in> edges G

goal (1 subgoal):
 1. (f x, f y) \<in> {(x, y). (l, x, y) \<in> edges G}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f x, f y) \<in> getRel l G

goal (2 subgoals):
 1. (l, x, y) \<in> edges G \<Longrightarrow> (l, f x, f y) \<in> edges G
 2. (l, f x, f y) \<in> edges G \<Longrightarrow> (l, x, y) \<in> edges G
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
(l, f x, f y) \<in> edges G
[PROOF STEP]
have fv:"f x \<in> vertices G" "f y \<in> vertices G"
[PROOF STATE]
proof (prove)
using this:
(l, f x, f y) \<in> edges G

goal (1 subgoal):
 1. f x \<in> vertices G &&& f y \<in> vertices G
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
(l, f x, f y) \<in> edges G
graph G

goal (1 subgoal):
 1. f x \<in> vertices G &&& f y \<in> vertices G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f x \<in> vertices G
f y \<in> vertices G

goal (2 subgoals):
 1. (l, x, y) \<in> edges G \<Longrightarrow> (l, f x, f y) \<in> edges G
 2. (l, f x, f y) \<in> edges G \<Longrightarrow> (l, x, y) \<in> edges G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
f x \<in> vertices G
f y \<in> vertices G

goal (2 subgoals):
 1. (l, x, y) \<in> edges G \<Longrightarrow> (l, f x, f y) \<in> edges G
 2. (l, f x, f y) \<in> edges G \<Longrightarrow> (l, x, y) \<in> edges G
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (l, x__, y) \<in> edges G \<Longrightarrow> (l, f x__, f y) \<in> edges G
 2. (l, f x__, f y) \<in> edges G \<Longrightarrow> (l, x__, y) \<in> edges G
[PROOF STEP]
assume a:"f x \<in> vertices G" "x \<notin> vertices G"
[PROOF STATE]
proof (state)
this:
f x \<in> vertices G
x \<notin> vertices G

goal (2 subgoals):
 1. (l, x__, y) \<in> edges G \<Longrightarrow> (l, f x__, f y) \<in> edges G
 2. (l, f x__, f y) \<in> edges G \<Longrightarrow> (l, x__, y) \<in> edges G
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
graph G
f x \<in> vertices G
x \<notin> vertices G
[PROOF STEP]
have "getRel S_Idt G `` {x} = {}"
[PROOF STATE]
proof (prove)
using this:
graph G
f x \<in> vertices G
x \<notin> vertices G

goal (1 subgoal):
 1. getRel S_Idt G `` {x} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getRel S_Idt G `` {x} = {}

goal (2 subgoals):
 1. (l, x__, y) \<in> edges G \<Longrightarrow> (l, f x__, f y) \<in> edges G
 2. (l, f x__, f y) \<in> edges G \<Longrightarrow> (l, x__, y) \<in> edges G
[PROOF STEP]
with a f
[PROOF STATE]
proof (chain)
picking this:
f x \<in> vertices G
x \<notin> vertices G
f = (\<lambda>x. if getRel S_Idt G `` {x} = {} then x else SOME y. P x y)
getRel S_Idt G `` {x} = {}
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
f x \<in> vertices G
x \<notin> vertices G
f = (\<lambda>x. if getRel S_Idt G `` {x} = {} then x else SOME y. P x y)
getRel S_Idt G `` {x} = {}

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. (l, x__, y) \<in> edges G \<Longrightarrow> (l, f x__, f y) \<in> edges G
 2. (l, f x__, f y) \<in> edges G \<Longrightarrow> (l, x__, y) \<in> edges G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>f ?xa2 \<in> vertices G; ?xa2 \<notin> vertices G\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. (l, x, y) \<in> edges G \<Longrightarrow> (l, f x, f y) \<in> edges G
 2. (l, f x, f y) \<in> edges G \<Longrightarrow> (l, x, y) \<in> edges G
[PROOF STEP]
with fv
[PROOF STATE]
proof (chain)
picking this:
f x \<in> vertices G
f y \<in> vertices G
\<lbrakk>f ?xa2 \<in> vertices G; ?xa2 \<notin> vertices G\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have v:"x \<in> vertices G" "y \<in> vertices G"
[PROOF STATE]
proof (prove)
using this:
f x \<in> vertices G
f y \<in> vertices G
\<lbrakk>f ?xa2 \<in> vertices G; ?xa2 \<notin> vertices G\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. x \<in> vertices G &&& y \<in> vertices G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vertices G
y \<in> vertices G

goal (2 subgoals):
 1. (l, x, y) \<in> edges G \<Longrightarrow> (l, f x, f y) \<in> edges G
 2. (l, f x, f y) \<in> edges G \<Longrightarrow> (l, x, y) \<in> edges G
[PROOF STEP]
have gx:"(x, f x) \<in> getRel S_Idt G" and gy:"(y, f y) \<in> getRel S_Idt G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, f x) \<in> getRel S_Idt G &&& (y, f y) \<in> getRel S_Idt G
[PROOF STEP]
by (auto simp: f v vert_P)
[PROOF STATE]
proof (state)
this:
(x, f x) \<in> getRel S_Idt G
(y, f y) \<in> getRel S_Idt G

goal (2 subgoals):
 1. (l, x, y) \<in> edges G \<Longrightarrow> (l, f x, f y) \<in> edges G
 2. (l, f x, f y) \<in> edges G \<Longrightarrow> (l, x, y) \<in> edges G
[PROOF STEP]
from congruentD[OF congr(1)[OF gr] gx] gr
[PROOF STATE]
proof (chain)
picking this:
getRel l G `` {x} = getRel l G `` {f x}
(f x, f y) \<in> getRel l G
[PROOF STEP]
have "(x, f y) \<in> getRel l G"
[PROOF STATE]
proof (prove)
using this:
getRel l G `` {x} = getRel l G `` {f x}
(f x, f y) \<in> getRel l G

goal (1 subgoal):
 1. (x, f y) \<in> getRel l G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, f y) \<in> getRel l G

goal (2 subgoals):
 1. (l, x, y) \<in> edges G \<Longrightarrow> (l, f x, f y) \<in> edges G
 2. (l, f x, f y) \<in> edges G \<Longrightarrow> (l, x, y) \<in> edges G
[PROOF STEP]
with congruentD[OF congr(2)[OF gr] gy]
[PROOF STATE]
proof (chain)
picking this:
(getRel l G)\<inverse> `` {y} = (getRel l G)\<inverse> `` {f y}
(x, f y) \<in> getRel l G
[PROOF STEP]
have "(x, y) \<in> getRel l G"
[PROOF STATE]
proof (prove)
using this:
(getRel l G)\<inverse> `` {y} = (getRel l G)\<inverse> `` {f y}
(x, f y) \<in> getRel l G

goal (1 subgoal):
 1. (x, y) \<in> getRel l G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> getRel l G

goal (2 subgoals):
 1. (l, x, y) \<in> edges G \<Longrightarrow> (l, f x, f y) \<in> edges G
 2. (l, f x, f y) \<in> edges G \<Longrightarrow> (l, x, y) \<in> edges G
[PROOF STEP]
thus "((l, x, y) \<in> edges G)"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> getRel l G

goal (1 subgoal):
 1. (l, x, y) \<in> edges G
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(x, y). (l, x, y) \<in> edges G}

goal (1 subgoal):
 1. (l, x, y) \<in> edges G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(l, x, y) \<in> edges G

goal (1 subgoal):
 1. (l, x, y) \<in> edges G \<Longrightarrow> (l, f x, f y) \<in> edges G
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (l, x, y) \<in> edges G \<Longrightarrow> (l, f x, f y) \<in> edges G
[PROOF STEP]
assume e:"((l, x, y) \<in> edges G)"
[PROOF STATE]
proof (state)
this:
(l, x, y) \<in> edges G

goal (1 subgoal):
 1. (l, x, y) \<in> edges G \<Longrightarrow> (l, f x, f y) \<in> edges G
[PROOF STEP]
hence "x \<in> vertices G" "y \<in> vertices G"
[PROOF STATE]
proof (prove)
using this:
(l, x, y) \<in> edges G

goal (1 subgoal):
 1. x \<in> vertices G &&& y \<in> vertices G
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
(l, x, y) \<in> edges G
graph G

goal (1 subgoal):
 1. x \<in> vertices G &&& y \<in> vertices G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vertices G
y \<in> vertices G

goal (1 subgoal):
 1. (l, x, y) \<in> edges G \<Longrightarrow> (l, f x, f y) \<in> edges G
[PROOF STEP]
from gu1[OF e this]
[PROOF STATE]
proof (chain)
picking this:
(l, f x, f y) \<in> edges G
[PROOF STEP]
show "((l, f x, f y) \<in> edges G)"
[PROOF STATE]
proof (prove)
using this:
(l, f x, f y) \<in> edges G

goal (1 subgoal):
 1. (l, f x, f y) \<in> edges G
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(l, f x, f y) \<in> edges G

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((?l, ?x, ?y) \<in> edges G) = ((?l, f ?x, f ?y) \<in> edges G)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
from idemp ident subg congr
[PROOF STATE]
proof (chain)
picking this:
f \<circ> f = f
ident_rel S_Idt (map_graph_fn G f)
subgraph (map_graph_fn G f) G
((?l, ?x, ?y) \<in> edges G) = ((?l, f ?x, f ?y) \<in> edges G)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<circ> f = f
ident_rel S_Idt (map_graph_fn G f)
subgraph (map_graph_fn G f) G
((?l, ?x, ?y) \<in> edges G) = ((?l, f ?x, f ?y) \<in> edges G)

goal (1 subgoal):
 1. \<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>f. f \<circ> f = f \<and> ident_rel S_Idt (map_graph_fn G f) \<and> subgraph (map_graph_fn G f) G \<and> (\<forall>l x y. ((l, x, y) \<in> edges G) = ((l, f x, f y) \<in> edges G))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma idemp_embedding_maintained_preserved:
  assumes subg:"subgraph (map_graph_fn G f) G" and f:"\<And> x. x\<in>vertices G \<Longrightarrow> (f o f) x = f x"
      and maint:"maintained r G"
    shows "maintained r (map_graph_fn G f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
fix h
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
assume hom_h:"graph_homomorphism (fst r) (map_graph_fn G f) h"
[PROOF STATE]
proof (state)
this:
graph_homomorphism (fst r) (map_graph_fn G f) h

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
from subgraph_preserves_hom[OF subg this] maint[unfolded maintained_def extensible_def]
[PROOF STATE]
proof (chain)
picking this:
graph_homomorphism (fst r) G h
\<forall>f. graph_homomorphism (fst r) G f \<longrightarrow> (\<exists>g. graph_homomorphism (snd r) G g \<and> agree_on (fst r) f g)
[PROOF STEP]
obtain g where g:"graph_homomorphism (snd r) G g"
                     "agree_on (fst r) h g"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (fst r) G h
\<forall>f. graph_homomorphism (fst r) G f \<longrightarrow> (\<exists>g. graph_homomorphism (snd r) G g \<and> agree_on (fst r) f g)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>graph_homomorphism (snd r) G g; agree_on (fst r) h g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
graph_homomorphism (snd r) G g
agree_on (fst r) h g

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
graph_homomorphism (snd r) G g
agree_on (fst r) h g

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
fix v x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
have subs:"h `` {v} \<subseteq> vertices (map_graph_fn G f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h `` {v} \<subseteq> vertices (map_graph_fn G f)
[PROOF STEP]
using hom_h[unfolded graph_homomorphism_def]
[PROOF STATE]
proof (prove)
using this:
vertices (fst r) = Domain h \<and> graph (fst r) \<and> graph (map_graph_fn G f) \<and> h `` vertices (fst r) \<subseteq> vertices (map_graph_fn G f) \<and> univalent h \<and> edge_preserving h (edges (fst r)) (edges (map_graph_fn G f))

goal (1 subgoal):
 1. h `` {v} \<subseteq> vertices (map_graph_fn G f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h `` {v} \<subseteq> vertices (map_graph_fn G f)

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
assume "v\<in>vertices (fst r)" and x:"(v, x) \<in> g"
[PROOF STATE]
proof (state)
this:
v \<in> vertices (fst r)
(v, x) \<in> g

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
hence "g `` {v} = h `` {v}"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices (fst r)
(v, x) \<in> g

goal (1 subgoal):
 1. g `` {v} = h `` {v}
[PROOF STEP]
using g(2)[unfolded agree_on_def,rule_format,of v]
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices (fst r)
(v, x) \<in> g
v \<in> vertices (fst r) \<Longrightarrow> h `` {v} = g `` {v}

goal (1 subgoal):
 1. g `` {v} = h `` {v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g `` {v} = h `` {v}

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
hence "g `` {v} \<subseteq> vertices (map_graph_fn G f)"
[PROOF STATE]
proof (prove)
using this:
g `` {v} = h `` {v}

goal (1 subgoal):
 1. g `` {v} \<subseteq> vertices (map_graph_fn G f)
[PROOF STEP]
using subs
[PROOF STATE]
proof (prove)
using this:
g `` {v} = h `` {v}
h `` {v} \<subseteq> vertices (map_graph_fn G f)

goal (1 subgoal):
 1. g `` {v} \<subseteq> vertices (map_graph_fn G f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g `` {v} \<subseteq> vertices (map_graph_fn G f)

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
hence x2:"x \<in> vertices (map_graph_fn G f)"
[PROOF STATE]
proof (prove)
using this:
g `` {v} \<subseteq> vertices (map_graph_fn G f)

goal (1 subgoal):
 1. x \<in> vertices (map_graph_fn G f)
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
g `` {v} \<subseteq> vertices (map_graph_fn G f)
(v, x) \<in> g

goal (1 subgoal):
 1. x \<in> vertices (map_graph_fn G f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vertices (map_graph_fn G f)

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> vertices (map_graph_fn G f)
[PROOF STEP]
obtain y where "x = f y" "y \<in> vertices G"
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices (map_graph_fn G f)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>x = f y; y \<in> vertices G\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = f y
y \<in> vertices G

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
hence f:"f x = x"
[PROOF STATE]
proof (prove)
using this:
x = f y
y \<in> vertices G

goal (1 subgoal):
 1. f x = x
[PROOF STEP]
using f x2
[PROOF STATE]
proof (prove)
using this:
x = f y
y \<in> vertices G
?x \<in> vertices G \<Longrightarrow> (f \<circ> f) ?x = f ?x
x \<in> vertices (map_graph_fn G f)

goal (1 subgoal):
 1. f x = x
[PROOF STEP]
unfolding o_def
[PROOF STATE]
proof (prove)
using this:
x = f y
y \<in> vertices G
?x \<in> vertices G \<Longrightarrow> f (f ?x) = f ?x
x \<in> vertices (map_graph_fn G f)

goal (1 subgoal):
 1. f x = x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
f x = x

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
from x2 subgraph_subset[OF subg]
[PROOF STATE]
proof (chain)
picking this:
x \<in> vertices (map_graph_fn G f)
vertices (map_graph_fn G f) \<subseteq> vertices G
edges (restrict (map_graph_fn G f)) \<subseteq> edges G
[PROOF STEP]
have "(x, f x) \<in> on_graph G f"
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices (map_graph_fn G f)
vertices (map_graph_fn G f) \<subseteq> vertices G
edges (restrict (map_graph_fn G f)) \<subseteq> edges G

goal (1 subgoal):
 1. (x, f x) \<in> on_graph G f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, f x) \<in> on_graph G f

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
(v, x) \<in> g
(x, f x) \<in> on_graph G f
[PROOF STEP]
have "(v, x) \<in> g O on_graph G f" "f x = x"
[PROOF STATE]
proof (prove)
using this:
(v, x) \<in> g
(x, f x) \<in> on_graph G f

goal (1 subgoal):
 1. (v, x) \<in> g O on_graph G f &&& f x = x
[PROOF STEP]
unfolding f
[PROOF STATE]
proof (prove)
using this:
(v, x) \<in> g
(x, x) \<in> on_graph G f

goal (1 subgoal):
 1. (v, x) \<in> g O on_graph G f &&& x = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v, x) \<in> g O on_graph G f
f x = x

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v2 \<in> vertices (fst r); (?v2, ?x2) \<in> g\<rbrakk> \<Longrightarrow> (?v2, ?x2) \<in> g O on_graph G f
\<lbrakk>?v2 \<in> vertices (fst r); (?v2, ?x2) \<in> g\<rbrakk> \<Longrightarrow> f ?x2 = ?x2

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
hence agr:"agree_on (fst r) h (g O on_graph G f)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v2 \<in> vertices (fst r); (?v2, ?x2) \<in> g\<rbrakk> \<Longrightarrow> (?v2, ?x2) \<in> g O on_graph G f
\<lbrakk>?v2 \<in> vertices (fst r); (?v2, ?x2) \<in> g\<rbrakk> \<Longrightarrow> f ?x2 = ?x2

goal (1 subgoal):
 1. agree_on (fst r) h (g O on_graph G f)
[PROOF STEP]
using g(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v2 \<in> vertices (fst r); (?v2, ?x2) \<in> g\<rbrakk> \<Longrightarrow> (?v2, ?x2) \<in> g O on_graph G f
\<lbrakk>?v2 \<in> vertices (fst r); (?v2, ?x2) \<in> g\<rbrakk> \<Longrightarrow> f ?x2 = ?x2
agree_on (fst r) h g

goal (1 subgoal):
 1. agree_on (fst r) h (g O on_graph G f)
[PROOF STEP]
unfolding agree_on_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v2 \<in> vertices (fst r); (?v2, ?x2) \<in> g\<rbrakk> \<Longrightarrow> (?v2, ?x2) \<in> g O on_graph G f
\<lbrakk>?v2 \<in> vertices (fst r); (?v2, ?x2) \<in> g\<rbrakk> \<Longrightarrow> f ?x2 = ?x2
\<forall>v\<in>vertices (fst r). h `` {v} = g `` {v}

goal (1 subgoal):
 1. \<forall>v\<in>vertices (fst r). h `` {v} = (g O on_graph G f) `` {v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
agree_on (fst r) h (g O on_graph G f)

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
have "extensible r (map_graph_fn G f) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extensible r (map_graph_fn G f) h
[PROOF STEP]
unfolding extensible_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. graph_homomorphism (snd r) (map_graph_fn G f) g \<and> agree_on (fst r) h g
[PROOF STEP]
using graph_homomorphism_on_graph[OF g(1)] agr
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (snd r) (map_graph_fn G ?f) (g O on_graph G ?f)
agree_on (fst r) h (g O on_graph G f)

goal (1 subgoal):
 1. \<exists>g. graph_homomorphism (snd r) (map_graph_fn G f) g \<and> agree_on (fst r) h g
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
extensible r (map_graph_fn G f) h

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
graph_homomorphism (fst r) (map_graph_fn G f) ?h2 \<Longrightarrow> extensible r (map_graph_fn G f) ?h2

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (fst r) (map_graph_fn G f) ?h2 \<Longrightarrow> extensible r (map_graph_fn G f) ?h2

goal (1 subgoal):
 1. maintained r (map_graph_fn G f)
[PROOF STEP]
unfolding maintained_def
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (fst r) (map_graph_fn G f) ?h2 \<Longrightarrow> extensible r (map_graph_fn G f) ?h2

goal (1 subgoal):
 1. \<forall>fa. graph_homomorphism (fst r) (map_graph_fn G f) fa \<longrightarrow> extensible r (map_graph_fn G f) fa
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
maintained r (map_graph_fn G f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma constant_rules:
  assumes "standard' C G" "c \<in> C"
  shows "maintained (const_exists c) G"
        "maintained (const_exists_rev c) G"
        "maintained (const_prop c) G"
        "c' \<in> C \<Longrightarrow> c \<noteq> c' \<Longrightarrow> maintained (const_disj c c') G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (maintained (const_exists c) G &&& maintained (const_exists_rev c) G) &&& maintained (const_prop c) G &&& (\<lbrakk>c' \<in> C; c \<noteq> c'\<rbrakk> \<Longrightarrow> maintained (const_disj c c') G)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. maintained (const_exists c) G
 2. maintained (const_exists_rev c) G
 3. maintained (const_prop c) G
 4. \<lbrakk>c' \<in> C; c \<noteq> c'\<rbrakk> \<Longrightarrow> maintained (const_disj c c') G
[PROOF STEP]
note a = assms[unfolded standard_def]
[PROOF STATE]
proof (state)
this:
graph G \<and> vertices G \<noteq> {} \<and> ident_rel S_Idt G \<and> getRel S_Bot G = {} \<and> getRel S_Top G = {(x, y). x \<in> vertices G \<and> y \<in> vertices G} \<and> (\<forall>(l, v)\<in>(\<lambda>c. (S_Const c, Inl c)) ` C. getRel l G = {(v, v)})
c \<in> C

goal (4 subgoals):
 1. maintained (const_exists c) G
 2. maintained (const_exists_rev c) G
 3. maintained (const_prop c) G
 4. \<lbrakk>c' \<in> C; c \<noteq> c'\<rbrakk> \<Longrightarrow> maintained (const_disj c c') G
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
graph G \<and> vertices G \<noteq> {} \<and> ident_rel S_Idt G \<and> getRel S_Bot G = {} \<and> getRel S_Top G = {(x, y). x \<in> vertices G \<and> y \<in> vertices G} \<and> (\<forall>(l, v)\<in>(\<lambda>c. (S_Const c, Inl c)) ` C. getRel l G = {(v, v)})
c \<in> C
[PROOF STEP]
have g:"graph G"
[PROOF STATE]
proof (prove)
using this:
graph G \<and> vertices G \<noteq> {} \<and> ident_rel S_Idt G \<and> getRel S_Bot G = {} \<and> getRel S_Top G = {(x, y). x \<in> vertices G \<and> y \<in> vertices G} \<and> (\<forall>(l, v)\<in>(\<lambda>c. (S_Const c, Inl c)) ` C. getRel l G = {(v, v)})
c \<in> C

goal (1 subgoal):
 1. graph G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph G

goal (4 subgoals):
 1. maintained (const_exists c) G
 2. maintained (const_exists_rev c) G
 3. maintained (const_prop c) G
 4. \<lbrakk>c' \<in> C; c \<noteq> c'\<rbrakk> \<Longrightarrow> maintained (const_disj c c') G
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
graph G \<and> vertices G \<noteq> {} \<and> ident_rel S_Idt G \<and> getRel S_Bot G = {} \<and> getRel S_Top G = {(x, y). x \<in> vertices G \<and> y \<in> vertices G} \<and> (\<forall>(l, v)\<in>(\<lambda>c. (S_Const c, Inl c)) ` C. getRel l G = {(v, v)})
c \<in> C
[PROOF STEP]
have gr_c:"getRel (S_Const c) G = {(Inl c, Inl c)}"
       "getRel S_Idt G = Id_on (vertices G)" "getRel S_Bot G = {}"
       "getRel S_Top G = vertices G \<times> vertices G"
[PROOF STATE]
proof (prove)
using this:
graph G \<and> vertices G \<noteq> {} \<and> ident_rel S_Idt G \<and> getRel S_Bot G = {} \<and> getRel S_Top G = {(x, y). x \<in> vertices G \<and> y \<in> vertices G} \<and> (\<forall>(l, v)\<in>(\<lambda>c. (S_Const c, Inl c)) ` C. getRel l G = {(v, v)})
c \<in> C

goal (1 subgoal):
 1. (getRel (S_Const c) G = {(Inl c, Inl c)} &&& getRel S_Idt G = Id_on (vertices G)) &&& getRel S_Bot G = {} &&& getRel S_Top G = vertices G \<times> vertices G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getRel (S_Const c) G = {(Inl c, Inl c)}
getRel S_Idt G = Id_on (vertices G)
getRel S_Bot G = {}
getRel S_Top G = vertices G \<times> vertices G

goal (4 subgoals):
 1. maintained (const_exists c) G
 2. maintained (const_exists_rev c) G
 3. maintained (const_prop c) G
 4. \<lbrakk>c' \<in> C; c \<noteq> c'\<rbrakk> \<Longrightarrow> maintained (const_disj c c') G
[PROOF STEP]
with g
[PROOF STATE]
proof (chain)
picking this:
graph G
getRel (S_Const c) G = {(Inl c, Inl c)}
getRel S_Idt G = Id_on (vertices G)
getRel S_Bot G = {}
getRel S_Top G = vertices G \<times> vertices G
[PROOF STEP]
have inlc:"Inl c \<in> vertices G"
[PROOF STATE]
proof (prove)
using this:
graph G
getRel (S_Const c) G = {(Inl c, Inl c)}
getRel S_Idt G = Id_on (vertices G)
getRel S_Bot G = {}
getRel S_Top G = vertices G \<times> vertices G

goal (1 subgoal):
 1. Inl c \<in> vertices G
[PROOF STEP]
by (metis getRel_dom(1) singletonI)
[PROOF STATE]
proof (state)
this:
Inl c \<in> vertices G

goal (4 subgoals):
 1. maintained (const_exists c) G
 2. maintained (const_exists_rev c) G
 3. maintained (const_prop c) G
 4. \<lbrakk>c' \<in> C; c \<noteq> c'\<rbrakk> \<Longrightarrow> maintained (const_disj c c') G
[PROOF STEP]
thus "maintained (const_exists c) G" "maintained (const_exists_rev c) G"
       "maintained (const_prop c) G"
[PROOF STATE]
proof (prove)
using this:
Inl c \<in> vertices G

goal (1 subgoal):
 1. maintained (const_exists c) G &&& maintained (const_exists_rev c) G &&& maintained (const_prop c) G
[PROOF STEP]
unfolding const_prop_def const_exists_rev_def const_exists_def maintained_holds_subset_iff[OF g]
[PROOF STATE]
proof (prove)
using this:
Inl c \<in> vertices G

goal (1 subgoal):
 1. :G:\<lbrakk>\<top>\<rbrakk> \<subseteq> :G:\<lbrakk>A_Cmp (A_Cmp \<top> (A_Lbl (S_Const c))) \<top>\<rbrakk> &&& :G:\<lbrakk>A_Cmp (A_Cmp (A_Lbl (S_Const c)) \<top>) (A_Lbl (S_Const c))\<rbrakk> \<subseteq> :G:\<lbrakk>A_Lbl (S_Const c)\<rbrakk> &&& :G:\<lbrakk>A_Lbl (S_Const c)\<rbrakk> \<subseteq> :G:\<lbrakk>\<one>\<rbrakk>
[PROOF STEP]
by (auto simp:gr_c relcomp_unfold)
[PROOF STATE]
proof (state)
this:
maintained (const_exists c) G
maintained (const_exists_rev c) G
maintained (const_prop c) G

goal (1 subgoal):
 1. \<lbrakk>c' \<in> C; c \<noteq> c'\<rbrakk> \<Longrightarrow> maintained (const_disj c c') G
[PROOF STEP]
assume "c' \<in> C"
[PROOF STATE]
proof (state)
this:
c' \<in> C

goal (1 subgoal):
 1. \<lbrakk>c' \<in> C; c \<noteq> c'\<rbrakk> \<Longrightarrow> maintained (const_disj c c') G
[PROOF STEP]
with a
[PROOF STATE]
proof (chain)
picking this:
graph G \<and> vertices G \<noteq> {} \<and> ident_rel S_Idt G \<and> getRel S_Bot G = {} \<and> getRel S_Top G = {(x, y). x \<in> vertices G \<and> y \<in> vertices G} \<and> (\<forall>(l, v)\<in>(\<lambda>c. (S_Const c, Inl c)) ` C. getRel l G = {(v, v)})
c \<in> C
c' \<in> C
[PROOF STEP]
have gr_c':"getRel (S_Const c') G = {(Inl c', Inl c')}"
[PROOF STATE]
proof (prove)
using this:
graph G \<and> vertices G \<noteq> {} \<and> ident_rel S_Idt G \<and> getRel S_Bot G = {} \<and> getRel S_Top G = {(x, y). x \<in> vertices G \<and> y \<in> vertices G} \<and> (\<forall>(l, v)\<in>(\<lambda>c. (S_Const c, Inl c)) ` C. getRel l G = {(v, v)})
c \<in> C
c' \<in> C

goal (1 subgoal):
 1. getRel (S_Const c') G = {(Inl c', Inl c')}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getRel (S_Const c') G = {(Inl c', Inl c')}

goal (1 subgoal):
 1. \<lbrakk>c' \<in> C; c \<noteq> c'\<rbrakk> \<Longrightarrow> maintained (const_disj c c') G
[PROOF STEP]
thus "c \<noteq> c' \<Longrightarrow>  maintained (const_disj c c') G"
[PROOF STATE]
proof (prove)
using this:
getRel (S_Const c') G = {(Inl c', Inl c')}

goal (1 subgoal):
 1. c \<noteq> c' \<Longrightarrow> maintained (const_disj c c') G
[PROOF STEP]
unfolding const_disj_def maintained_holds_subset_iff[OF g]
[PROOF STATE]
proof (prove)
using this:
getRel (S_Const c') G = {(Inl c', Inl c')}

goal (1 subgoal):
 1. c \<noteq> c' \<Longrightarrow> :G:\<lbrakk>A_Cmp (A_Lbl (S_Const c)) (A_Lbl (S_Const c'))\<rbrakk> \<subseteq> :G:\<lbrakk>\<bottom>\<rbrakk>
[PROOF STEP]
using gr_c
[PROOF STATE]
proof (prove)
using this:
getRel (S_Const c') G = {(Inl c', Inl c')}
getRel (S_Const c) G = {(Inl c, Inl c)}
getRel S_Idt G = Id_on (vertices G)
getRel S_Bot G = {}
getRel S_Top G = vertices G \<times> vertices G

goal (1 subgoal):
 1. c \<noteq> c' \<Longrightarrow> :G:\<lbrakk>A_Cmp (A_Lbl (S_Const c)) (A_Lbl (S_Const c'))\<rbrakk> \<subseteq> :G:\<lbrakk>\<bottom>\<rbrakk>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<noteq> c' \<Longrightarrow> maintained (const_disj c c') G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma constant_rules_graph_rule:
  assumes "x \<in> constant_rules C"
  shows "graph_rule x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_rule x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. graph_rule x
[PROOF STEP]
from graph_rule_translation
[PROOF STATE]
proof (chain)
picking this:
graph_rule (translation ?X, translation (A_Int ?X ?Y))
[PROOF STEP]
have gr:"\<And> u v . graph_rule (transl_rule (u \<sqsubseteq> v))"
[PROOF STATE]
proof (prove)
using this:
graph_rule (translation ?X, translation (A_Int ?X ?Y))

goal (1 subgoal):
 1. \<And>u v. graph_rule (transl_rule (u \<sqsubseteq> v))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_rule (transl_rule (?u \<sqsubseteq> ?v))

goal (1 subgoal):
 1. graph_rule x
[PROOF STEP]
consider "\<exists> v. x = const_exists v" | "\<exists> v. x = const_exists_rev v" |  "\<exists> v. x = const_prop v"
    |  "\<exists> v w. x = const_disj v w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>v. x = const_exists v \<Longrightarrow> thesis; \<exists>v. x = const_exists_rev v \<Longrightarrow> thesis; \<exists>v. x = const_prop v \<Longrightarrow> thesis; \<exists>v w. x = const_disj v w \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> constant_rules C

goal (1 subgoal):
 1. \<lbrakk>\<exists>v. x = const_exists v \<Longrightarrow> thesis; \<exists>v. x = const_exists_rev v \<Longrightarrow> thesis; \<exists>v. x = const_prop v \<Longrightarrow> thesis; \<exists>v w. x = const_disj v w \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding constant_rules_def Un_iff
[PROOF STATE]
proof (prove)
using this:
((x \<in> const_exists ` C \<or> x \<in> const_exists_rev ` C) \<or> x \<in> const_prop ` C) \<or> x \<in> {const_disj c\<^sub>1 c\<^sub>2 |c\<^sub>1 c\<^sub>2. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<and> c\<^sub>1 \<noteq> c\<^sub>2}

goal (1 subgoal):
 1. \<lbrakk>\<exists>v. x = const_exists v \<Longrightarrow> thesis; \<exists>v. x = const_exists_rev v \<Longrightarrow> thesis; \<exists>v. x = const_prop v \<Longrightarrow> thesis; \<exists>v w. x = const_disj v w \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<exists>v. x = const_exists v \<Longrightarrow> ?thesis1; \<exists>v. x = const_exists_rev v \<Longrightarrow> ?thesis1; \<exists>v. x = const_prop v \<Longrightarrow> ?thesis1; \<exists>v w. x = const_disj v w \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1

goal (1 subgoal):
 1. graph_rule x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>v. x = const_exists v \<Longrightarrow> ?thesis1; \<exists>v. x = const_exists_rev v \<Longrightarrow> ?thesis1; \<exists>v. x = const_prop v \<Longrightarrow> ?thesis1; \<exists>v w. x = const_disj v w \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1

goal (1 subgoal):
 1. graph_rule x
[PROOF STEP]
using gr
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>v. x = const_exists v \<Longrightarrow> ?thesis1; \<exists>v. x = const_exists_rev v \<Longrightarrow> ?thesis1; \<exists>v. x = const_prop v \<Longrightarrow> ?thesis1; \<exists>v w. x = const_disj v w \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1
graph_rule (transl_rule (?u \<sqsubseteq> ?v))

goal (1 subgoal):
 1. graph_rule x
[PROOF STEP]
unfolding const_exists_def const_exists_rev_def const_prop_def const_disj_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>v. x = transl_rule (\<top> \<sqsubseteq> A_Cmp (A_Cmp \<top> (A_Lbl (S_Const v))) \<top>) \<Longrightarrow> ?thesis1; \<exists>v. x = transl_rule (A_Cmp (A_Cmp (A_Lbl (S_Const v)) \<top>) (A_Lbl (S_Const v)) \<sqsubseteq> A_Lbl (S_Const v)) \<Longrightarrow> ?thesis1; \<exists>v. x = transl_rule (A_Lbl (S_Const v) \<sqsubseteq> \<one>) \<Longrightarrow> ?thesis1; \<exists>v w. x = transl_rule (A_Cmp (A_Lbl (S_Const v)) (A_Lbl (S_Const w)) \<sqsubseteq> \<bottom>) \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1
graph_rule (transl_rule (?u \<sqsubseteq> ?v))

goal (1 subgoal):
 1. graph_rule x
[PROOF STEP]
by cases fast+
[PROOF STATE]
proof (state)
this:
graph_rule x

goal:
No subgoals!
[PROOF STEP]
qed