[STATEMENT]
lemma finite_constant[intro]:
  assumes "finite C"
  shows "finite (constant_rules C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (constant_rules C)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (constant_rules C)
[PROOF STEP]
have "{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} \<subseteq> case_prod const_disj ` (C \<times> C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {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} \<subseteq> (\<lambda>(x, y). const_disj x y) ` (C \<times> C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{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} \<subseteq> (\<lambda>(x, y). const_disj x y) ` (C \<times> C)

goal (1 subgoal):
 1. finite (constant_rules C)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{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} \<subseteq> (\<lambda>(x, y). const_disj x y) ` (C \<times> C)

goal (1 subgoal):
 1. finite (constant_rules C)
[PROOF STEP]
have "finite \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ((\<lambda>(x, y). const_disj x y) ` (C \<times> C))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite C

goal (1 subgoal):
 1. finite ((\<lambda>(x, y). const_disj x y) ` (C \<times> C))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite ((\<lambda>(x, y). const_disj x y) ` (C \<times> C))

goal (1 subgoal):
 1. finite (constant_rules C)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{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} \<subseteq> (\<lambda>(x, y). const_disj x y) ` (C \<times> C)
finite ((\<lambda>(x, y). const_disj x y) ` (C \<times> C))
[PROOF STEP]
have "finite {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}"
[PROOF STATE]
proof (prove)
using this:
{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} \<subseteq> (\<lambda>(x, y). const_disj x y) ` (C \<times> C)
finite ((\<lambda>(x, y). const_disj x y) ` (C \<times> C))

goal (1 subgoal):
 1. finite {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}
[PROOF STEP]
by(rule finite_subset)
[PROOF STATE]
proof (state)
this:
finite {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. finite (constant_rules C)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {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. finite (constant_rules C)
[PROOF STEP]
unfolding constant_rules_def
[PROOF STATE]
proof (prove)
using this:
finite {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. finite (const_exists ` C \<union> const_exists_rev ` C \<union> const_prop ` C \<union> {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})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite {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}
finite C

goal (1 subgoal):
 1. finite (const_exists ` C \<union> const_exists_rev ` C \<union> const_prop ` C \<union> {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})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (constant_rules C)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma standard_maintains_constant_rules:
  assumes "standard' C G" "R\<in>constant_rules C"
  shows "maintained R G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained R G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. maintained R G
[PROOF STEP]
from assms(2)[unfolded constant_rules_def]
[PROOF STATE]
proof (chain)
picking this:
R \<in> const_exists ` C \<union> const_exists_rev ` C \<union> const_prop ` C \<union> {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}
[PROOF STEP]
consider "\<exists> c \<in> C. R = const_exists c"
         | "\<exists> c \<in> C. R = const_exists_rev c"
         | "\<exists> c \<in> C. R = const_prop c"
         | "\<exists> 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 \<and> R = const_disj c\<^sub>1 c\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
R \<in> const_exists ` C \<union> const_exists_rev ` C \<union> const_prop ` C \<union> {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>c\<in>C. R = const_exists c \<Longrightarrow> thesis; \<exists>c\<in>C. R = const_exists_rev c \<Longrightarrow> thesis; \<exists>c\<in>C. R = const_prop c \<Longrightarrow> thesis; \<exists>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 \<and> R = const_disj c\<^sub>1 c\<^sub>2 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<exists>c\<in>C. R = const_exists c \<Longrightarrow> ?thesis; \<exists>c\<in>C. R = const_exists_rev c \<Longrightarrow> ?thesis; \<exists>c\<in>C. R = const_prop c \<Longrightarrow> ?thesis; \<exists>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 \<and> R = const_disj c\<^sub>1 c\<^sub>2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. maintained R G
[PROOF STEP]
from this assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<exists>c\<in>C. R = const_exists c \<Longrightarrow> ?thesis; \<exists>c\<in>C. R = const_exists_rev c \<Longrightarrow> ?thesis; \<exists>c\<in>C. R = const_prop c \<Longrightarrow> ?thesis; \<exists>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 \<and> R = const_disj c\<^sub>1 c\<^sub>2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
standard' C G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>c\<in>C. R = const_exists c \<Longrightarrow> ?thesis; \<exists>c\<in>C. R = const_exists_rev c \<Longrightarrow> ?thesis; \<exists>c\<in>C. R = const_prop c \<Longrightarrow> ?thesis; \<exists>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 \<and> R = const_disj c\<^sub>1 c\<^sub>2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
standard' C G

goal (1 subgoal):
 1. maintained R G
[PROOF STEP]
by(cases,auto simp:constant_rules)
[PROOF STATE]
proof (state)
this:
maintained R G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma constant_rules_empty[simp]:
  "constant_rules {} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. constant_rules {} = {}
[PROOF STEP]
by (auto simp:constant_rules_def)


[STATEMENT]
lemma constant_rules_mono:
  assumes "C\<^sub>1 \<subseteq> C\<^sub>2"
  shows "constant_rules C\<^sub>1 \<subseteq> constant_rules C\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. constant_rules C\<^sub>1 \<subseteq> constant_rules C\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<subseteq> C\<^sub>2

goal (1 subgoal):
 1. constant_rules C\<^sub>1 \<subseteq> constant_rules C\<^sub>2
[PROOF STEP]
unfolding constant_rules_def
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<subseteq> C\<^sub>2

goal (1 subgoal):
 1. const_exists ` C\<^sub>1 \<union> const_exists_rev ` C\<^sub>1 \<union> const_prop ` C\<^sub>1 \<union> {const_disj c\<^sub>1 c\<^sub>2 |c\<^sub>1 c\<^sub>2. c\<^sub>1 \<in> C\<^sub>1 \<and> c\<^sub>2 \<in> C\<^sub>1 \<and> c\<^sub>1 \<noteq> c\<^sub>2} \<subseteq> const_exists ` C\<^sub>2 \<union> const_exists_rev ` C\<^sub>2 \<union> const_prop ` C\<^sub>2 \<union> {const_disj c\<^sub>1 c\<^sub>2 |c\<^sub>1 c\<^sub>2. c\<^sub>1 \<in> C\<^sub>2 \<and> c\<^sub>2 \<in> C\<^sub>2 \<and> c\<^sub>1 \<noteq> c\<^sub>2}
[PROOF STEP]
by(intro Un_mono,auto)


[STATEMENT]
lemma identity_rules_mono:
  assumes "C\<^sub>1 \<subseteq> C\<^sub>2"
  shows "identity_rules C\<^sub>1 \<subseteq> identity_rules C\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. identity_rules C\<^sub>1 \<subseteq> identity_rules C\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<subseteq> C\<^sub>2

goal (1 subgoal):
 1. identity_rules C\<^sub>1 \<subseteq> identity_rules C\<^sub>2
[PROOF STEP]
unfolding identity_rules_def
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<subseteq> C\<^sub>2

goal (1 subgoal):
 1. {reflexivity_rule S_Idt, transitive_rule S_Idt, symmetry_rule S_Idt} \<union> congruence_rules S_Idt C\<^sub>1 \<subseteq> {reflexivity_rule S_Idt, transitive_rule S_Idt, symmetry_rule S_Idt} \<union> congruence_rules S_Idt C\<^sub>2
[PROOF STEP]
by auto


[STATEMENT]
lemma maintainedA_invmono:
  assumes "C\<^sub>1 \<subseteq> C\<^sub>2" "L\<^sub>1 \<subseteq> L\<^sub>2"
  shows "maintainedA (standard_rules C\<^sub>2 L\<^sub>2) G \<Longrightarrow> maintainedA (standard_rules C\<^sub>1 L\<^sub>1) G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintainedA (standard_rules C\<^sub>2 L\<^sub>2) G \<Longrightarrow> maintainedA (standard_rules C\<^sub>1 L\<^sub>1) G
[PROOF STEP]
using standard_rules_mono[OF assms]
[PROOF STATE]
proof (prove)
using this:
standard_rules C\<^sub>1 L\<^sub>1 \<subseteq> standard_rules C\<^sub>2 L\<^sub>2

goal (1 subgoal):
 1. maintainedA (standard_rules C\<^sub>2 L\<^sub>2) G \<Longrightarrow> maintainedA (standard_rules C\<^sub>1 L\<^sub>1) G
[PROOF STEP]
by auto


[STATEMENT]
lemma maintained_preserved_by_isomorphism:
  assumes "\<And> x. x \<in> vertices G \<Longrightarrow> (f \<circ> g) x = x" "graph G"
      and "maintained r (map_graph_fn G g)"
  shows "maintained r G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained r G
[PROOF STEP]
proof(cases r)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. r = (a, b) \<Longrightarrow> maintained r G
[PROOF STEP]
case (Pair L R)
[PROOF STATE]
proof (state)
this:
r = (L, R)

goal (1 subgoal):
 1. \<And>a b. r = (a, b) \<Longrightarrow> maintained r G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained r G
[PROOF STEP]
unfolding Pair
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained (L, R) G
[PROOF STEP]
proof(standard,goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. graph_homomorphism L G f \<Longrightarrow> extensible (L, R) G f
[PROOF STEP]
case (1 h)
[PROOF STATE]
proof (state)
this:
graph_homomorphism L G h

goal (1 subgoal):
 1. \<And>f. graph_homomorphism L G f \<Longrightarrow> extensible (L, R) G f
[PROOF STEP]
from assms(3)[unfolded maintained_def Pair] graph_homomorphism_on_graph[OF this, of g]
[PROOF STATE]
proof (chain)
picking this:
\<forall>f. graph_homomorphism (fst (L, R)) (map_graph_fn G g) f \<longrightarrow> extensible (L, R) (map_graph_fn G g) f
graph_homomorphism L (map_graph_fn G g) (h O on_graph G g)
[PROOF STEP]
have "extensible (L, R) (map_graph_fn G g) (h O on_graph G g)"
[PROOF STATE]
proof (prove)
using this:
\<forall>f. graph_homomorphism (fst (L, R)) (map_graph_fn G g) f \<longrightarrow> extensible (L, R) (map_graph_fn G g) f
graph_homomorphism L (map_graph_fn G g) (h O on_graph G g)

goal (1 subgoal):
 1. extensible (L, R) (map_graph_fn G g) (h O on_graph G g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extensible (L, R) (map_graph_fn G g) (h O on_graph G g)

goal (1 subgoal):
 1. \<And>f. graph_homomorphism L G f \<Longrightarrow> extensible (L, R) G f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extensible (L, R) (map_graph_fn G g) (h O on_graph G g)
[PROOF STEP]
obtain h2
      where h2:"graph_homomorphism R (map_graph_fn G g) h2" "agree_on L (h O on_graph G g) h2"
[PROOF STATE]
proof (prove)
using this:
extensible (L, R) (map_graph_fn G g) (h O on_graph G g)

goal (1 subgoal):
 1. (\<And>h2. \<lbrakk>graph_homomorphism R (map_graph_fn G g) h2; agree_on L (h O on_graph G g) h2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding extensible_def
[PROOF STATE]
proof (prove)
using this:
\<exists>ga. graph_homomorphism (snd (L, R)) (map_graph_fn G g) ga \<and> agree_on (fst (L, R)) (h O on_graph G g) ga

goal (1 subgoal):
 1. (\<And>h2. \<lbrakk>graph_homomorphism R (map_graph_fn G g) h2; agree_on L (h O on_graph G g) h2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism R (map_graph_fn G g) h2
agree_on L (h O on_graph G g) h2

goal (1 subgoal):
 1. \<And>f. graph_homomorphism L G f \<Longrightarrow> extensible (L, R) G f
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
graph_homomorphism L G h
[PROOF STEP]
have h_id:"h O Id_on (vertices G) = h"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism L G h

goal (1 subgoal):
 1. h O Id_on (vertices G) = h
[PROOF STEP]
unfolding graph_homomorphism_def
[PROOF STATE]
proof (prove)
using this:
vertices L = Domain h \<and> graph L \<and> graph G \<and> h `` vertices L \<subseteq> vertices G \<and> univalent h \<and> edge_preserving h (edges L) (edges G)

goal (1 subgoal):
 1. h O Id_on (vertices G) = h
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h O Id_on (vertices G) = h

goal (1 subgoal):
 1. \<And>f. graph_homomorphism L G f \<Longrightarrow> extensible (L, R) G f
[PROOF STEP]
let ?h = "h2 O on_graph (map_graph_fn G g) f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. graph_homomorphism L G f \<Longrightarrow> extensible (L, R) G f
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
?x \<in> vertices G \<Longrightarrow> (f \<circ> g) ?x = ?x
[PROOF STEP]
have "on_graph G (f \<circ> g) = Id_on (vertices G)"
[PROOF STATE]
proof (prove)
using this:
?x \<in> vertices G \<Longrightarrow> (f \<circ> g) ?x = ?x

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

goal (1 subgoal):
 1. \<And>f. graph_homomorphism L G f \<Longrightarrow> extensible (L, R) G f
[PROOF STEP]
hence "map_graph_fn G (f \<circ> g) = G"
[PROOF STATE]
proof (prove)
using this:
on_graph G (f \<circ> g) = Id_on (vertices G)

goal (1 subgoal):
 1. map_graph_fn G (f \<circ> g) = G
[PROOF STEP]
using assms(2) map_graph_fn_id
[PROOF STATE]
proof (prove)
using this:
on_graph G (f \<circ> g) = Id_on (vertices G)
graph G
map_graph_fn ?X id = restrict ?X
map_graph (Id_on (vertices ?X)) ?X = restrict ?X

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

goal (1 subgoal):
 1. \<And>f. graph_homomorphism L G f \<Longrightarrow> extensible (L, R) G f
[PROOF STEP]
with graph_homomorphism_on_graph[OF h2(1),of f]
[PROOF STATE]
proof (chain)
picking this:
graph_homomorphism R (map_graph_fn (map_graph_fn G g) f) (h2 O on_graph (map_graph_fn G g) f)
map_graph_fn G (f \<circ> g) = G
[PROOF STEP]
have igh:"graph_homomorphism R G ?h"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism R (map_graph_fn (map_graph_fn G g) f) (h2 O on_graph (map_graph_fn G g) f)
map_graph_fn G (f \<circ> g) = G

goal (1 subgoal):
 1. graph_homomorphism R G (h2 O on_graph (map_graph_fn G g) f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism R G (h2 O on_graph (map_graph_fn G g) f)

goal (1 subgoal):
 1. \<And>f. graph_homomorphism L G f \<Longrightarrow> extensible (L, R) G f
[PROOF STEP]
have "g x = g xa \<Longrightarrow> x \<in> (vertices G) \<Longrightarrow> xa \<in> (vertices G) \<Longrightarrow> x = xa"
      for x xa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g x = g xa; x \<in> vertices G; xa \<in> vertices G\<rbrakk> \<Longrightarrow> x = xa
[PROOF STEP]
using assms(1) o_def
[PROOF STATE]
proof (prove)
using this:
?x \<in> vertices G \<Longrightarrow> (f \<circ> g) ?x = ?x
?f \<circ> ?g = (\<lambda>x. ?f (?g x))

goal (1 subgoal):
 1. \<lbrakk>g x = g xa; x \<in> vertices G; xa \<in> vertices G\<rbrakk> \<Longrightarrow> x = xa
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<lbrakk>g ?x = g ?xa; ?x \<in> vertices G; ?xa \<in> vertices G\<rbrakk> \<Longrightarrow> ?x = ?xa

goal (1 subgoal):
 1. \<And>f. graph_homomorphism L G f \<Longrightarrow> extensible (L, R) G f
[PROOF STEP]
hence "g x = g xa \<Longrightarrow> x \<in> (vertices G) \<Longrightarrow> xa \<in> (vertices G) \<Longrightarrow> (x, xa) \<in> Id_on (vertices G)"
      for x xa
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>g ?x = g ?xa; ?x \<in> vertices G; ?xa \<in> vertices G\<rbrakk> \<Longrightarrow> ?x = ?xa

goal (1 subgoal):
 1. \<lbrakk>g x = g xa; x \<in> vertices G; xa \<in> vertices G\<rbrakk> \<Longrightarrow> (x, xa) \<in> Id_on (vertices G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>g ?x = g ?xa; ?x \<in> vertices G; ?xa \<in> vertices G\<rbrakk> \<Longrightarrow> (?x, ?xa) \<in> Id_on (vertices G)

goal (1 subgoal):
 1. \<And>f. graph_homomorphism L G f \<Longrightarrow> extensible (L, R) G f
[PROOF STEP]
hence id:"(on_graph G g) O on_graph (map_graph_fn G g) f = Id_on (vertices G)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>g ?x = g ?xa; ?x \<in> vertices G; ?xa \<in> vertices G\<rbrakk> \<Longrightarrow> (?x, ?xa) \<in> Id_on (vertices G)

goal (1 subgoal):
 1. on_graph G g O on_graph (map_graph_fn G g) f = Id_on (vertices G)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>g ?x = g ?xa; ?x \<in> vertices G; ?xa \<in> vertices G\<rbrakk> \<Longrightarrow> (?x, ?xa) \<in> Id_on (vertices G)
?x \<in> vertices G \<Longrightarrow> (f \<circ> g) ?x = ?x

goal (1 subgoal):
 1. on_graph G g O on_graph (map_graph_fn G g) f = Id_on (vertices G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
on_graph G g O on_graph (map_graph_fn G g) f = Id_on (vertices G)

goal (1 subgoal):
 1. \<And>f. graph_homomorphism L G f \<Longrightarrow> extensible (L, R) G f
[PROOF STEP]
from agree_on_ext[OF h2(2),of "on_graph (map_graph_fn G g) f",unfolded O_assoc]
[PROOF STATE]
proof (chain)
picking this:
agree_on L (h O on_graph G g O on_graph (map_graph_fn G g) f) (h2 O on_graph (map_graph_fn G g) f)
[PROOF STEP]
have agh:"agree_on L h ?h"
[PROOF STATE]
proof (prove)
using this:
agree_on L (h O on_graph G g O on_graph (map_graph_fn G g) f) (h2 O on_graph (map_graph_fn G g) f)

goal (1 subgoal):
 1. agree_on L h (h2 O on_graph (map_graph_fn G g) f)
[PROOF STEP]
unfolding agree_on_def id h_id
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vertices L. h `` {v} = (h2 O on_graph (map_graph_fn G g) f) `` {v}

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

goal (1 subgoal):
 1. \<And>f. graph_homomorphism L G f \<Longrightarrow> extensible (L, R) G f
[PROOF STEP]
from igh agh
[PROOF STATE]
proof (chain)
picking this:
graph_homomorphism R G (h2 O on_graph (map_graph_fn G g) f)
agree_on L h (h2 O on_graph (map_graph_fn G g) f)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism R G (h2 O on_graph (map_graph_fn G g) f)
agree_on L h (h2 O on_graph (map_graph_fn G g) f)

goal (1 subgoal):
 1. extensible (L, R) G h
[PROOF STEP]
unfolding extensible_def
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism R G (h2 O on_graph (map_graph_fn G g) f)
agree_on L h (h2 O on_graph (map_graph_fn G g) f)

goal (1 subgoal):
 1. \<exists>g. graph_homomorphism (snd (L, R)) G g \<and> agree_on (fst (L, R)) h g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extensible (L, R) G h

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
maintained r G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma standard_identity_rules:
  assumes "standard' C G"
  shows "maintained (reflexivity_rule S_Idt) G"
        "maintained (transitive_rule S_Idt) G"
        "maintained (symmetry_rule S_Idt) G"
        "maintained (congruence_rule S_Idt l) G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (maintained (reflexivity_rule S_Idt) G &&& maintained (transitive_rule S_Idt) G) &&& maintained (symmetry_rule S_Idt) G &&& maintained (congruence_rule S_Idt l) G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. maintained (reflexivity_rule S_Idt) G
 2. maintained (transitive_rule S_Idt) G
 3. maintained (symmetry_rule S_Idt) G
 4. maintained (congruence_rule S_Idt l) 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)})

goal (4 subgoals):
 1. maintained (reflexivity_rule S_Idt) G
 2. maintained (transitive_rule S_Idt) G
 3. maintained (symmetry_rule S_Idt) G
 4. maintained (congruence_rule S_Idt l) 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)})
[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)})

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

goal (4 subgoals):
 1. maintained (reflexivity_rule S_Idt) G
 2. maintained (transitive_rule S_Idt) G
 3. maintained (symmetry_rule S_Idt) G
 4. maintained (congruence_rule S_Idt l) 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)})
[PROOF STEP]
have gr:"getRel S_Idt G = Id_on (vertices G)" "getRel S_Bot G = {}"
       "getRel S_Top G = vertices G \<times> vertices G"
    and v_gr:"\<forall>a b. ((S_Idt, a, b) \<in> edges G) = (a \<in> vertices G \<and> b = a)"
[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)})

goal (1 subgoal):
 1. (getRel S_Idt G = Id_on (vertices G) &&& getRel S_Bot G = {} &&& getRel S_Top G = vertices G \<times> vertices G) &&& \<forall>a b. ((S_Idt, a, b) \<in> edges G) = (a \<in> vertices G \<and> b = a)
[PROOF STEP]
unfolding getRel_def
[PROOF STATE]
proof (prove)
using this:
graph G \<and> vertices G \<noteq> {} \<and> {(x, y). (S_Idt, x, y) \<in> edges G} = (\<lambda>x. (x, x)) ` vertices G \<and> {(x, y). (S_Bot, x, y) \<in> edges G} = {} \<and> {(x, y). (S_Top, x, y) \<in> edges 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. {(x, y). (l, x, y) \<in> edges G} = {(v, v)})

goal (1 subgoal):
 1. ({(x, y). (S_Idt, x, y) \<in> edges G} = Id_on (vertices G) &&& {(x, y). (S_Bot, x, y) \<in> edges G} = {} &&& {(x, y). (S_Top, x, y) \<in> edges G} = vertices G \<times> vertices G) &&& \<forall>a b. ((S_Idt, a, b) \<in> edges G) = (a \<in> vertices G \<and> b = a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getRel S_Idt G = Id_on (vertices G)
getRel S_Bot G = {}
getRel S_Top G = vertices G \<times> vertices G
\<forall>a b. ((S_Idt, a, b) \<in> edges G) = (a \<in> vertices G \<and> b = a)

goal (4 subgoals):
 1. maintained (reflexivity_rule S_Idt) G
 2. maintained (transitive_rule S_Idt) G
 3. maintained (symmetry_rule S_Idt) G
 4. maintained (congruence_rule S_Idt l) G
[PROOF STEP]
thus "maintained (transitive_rule S_Idt) G" "maintained (symmetry_rule S_Idt) G"
       "maintained (congruence_rule S_Idt l) G"
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt G = Id_on (vertices G)
getRel S_Bot G = {}
getRel S_Top G = vertices G \<times> vertices G
\<forall>a b. ((S_Idt, a, b) \<in> edges G) = (a \<in> vertices G \<and> b = a)

goal (1 subgoal):
 1. maintained (transitive_rule S_Idt) G &&& maintained (symmetry_rule S_Idt) G &&& maintained (congruence_rule S_Idt l) G
[PROOF STEP]
unfolding transitive_rule_def symmetry_rule_def congruence_rule_def
              maintained_holds_subset_iff[OF g]
[PROOF STATE]
proof (prove)
using this:
getRel S_Idt G = Id_on (vertices G)
getRel S_Bot G = {}
getRel S_Top G = vertices G \<times> vertices G
\<forall>a b. ((S_Idt, a, b) \<in> edges G) = (a \<in> vertices G \<and> b = a)

goal (1 subgoal):
 1. :G:\<lbrakk>A_Cmp \<one> \<one>\<rbrakk> \<subseteq> :G:\<lbrakk>\<one>\<rbrakk> &&& :G:\<lbrakk>A_Cnv \<one>\<rbrakk> \<subseteq> :G:\<lbrakk>\<one>\<rbrakk> &&& :G:\<lbrakk>A_Cmp (A_Cmp \<one> (A_Lbl l)) \<one>\<rbrakk> \<subseteq> :G:\<lbrakk>A_Lbl l\<rbrakk>
[PROOF STEP]
by (auto simp:gr relcomp_unfold)
[PROOF STATE]
proof (state)
this:
maintained (transitive_rule S_Idt) G
maintained (symmetry_rule S_Idt) G
maintained (congruence_rule S_Idt l) G

goal (1 subgoal):
 1. maintained (reflexivity_rule S_Idt) G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
maintained (transitive_rule S_Idt) G
maintained (symmetry_rule S_Idt) G
maintained (congruence_rule S_Idt l) G

goal (1 subgoal):
 1. maintained (reflexivity_rule S_Idt) G
[PROOF STEP]
fix f :: "(nat \<times> ('a + 'b)) set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. maintained (reflexivity_rule S_Idt) G
[PROOF STEP]
assume "graph_homomorphism (LG {} {0}) G f"
[PROOF STATE]
proof (state)
this:
graph_homomorphism (LG {} {0}) G f

goal (1 subgoal):
 1. maintained (reflexivity_rule S_Idt) G
[PROOF STEP]
hence u:"univalent f" and d:"Domain f = {0}"
       and r:"f `` {0} \<subseteq> vertices G"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (LG {} {0}) G f

goal (1 subgoal):
 1. univalent f &&& Domain f = {0} &&& f `` {0} \<subseteq> vertices G
[PROOF STEP]
unfolding graph_homomorphism_def
[PROOF STATE]
proof (prove)
using this:
vertices (LG {} {0}) = Domain f \<and> graph (LG {} {0}) \<and> graph G \<and> f `` vertices (LG {} {0}) \<subseteq> vertices G \<and> univalent f \<and> edge_preserving f (edges (LG {} {0})) (edges G)

goal (1 subgoal):
 1. univalent f &&& Domain f = {0} &&& f `` {0} \<subseteq> vertices G
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
univalent f
Domain f = {0}
f `` {0} \<subseteq> vertices G

goal (1 subgoal):
 1. maintained (reflexivity_rule S_Idt) G
[PROOF STEP]
from d
[PROOF STATE]
proof (chain)
picking this:
Domain f = {0}
[PROOF STEP]
obtain v where v:"(0,v) \<in> f"
[PROOF STATE]
proof (prove)
using this:
Domain f = {0}

goal (1 subgoal):
 1. (\<And>v. (0, v) \<in> f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0, v) \<in> f

goal (1 subgoal):
 1. maintained (reflexivity_rule S_Idt) G
[PROOF STEP]
hence f:"f = {(0,v)}"
[PROOF STATE]
proof (prove)
using this:
(0, v) \<in> f

goal (1 subgoal):
 1. f = {(0, v)}
[PROOF STEP]
using d insert_iff mk_disjoint_insert all_not_in_conv old.prod.exhaust
            u[unfolded univalent_def] Domain.intros[of _ _ f,unfolded d,THEN singletonD]
[PROOF STATE]
proof (prove)
using this:
(0, v) \<in> f
Domain f = {0}
(?a \<in> insert ?b ?A) = (?a = ?b \<or> ?a \<in> ?A)
?a \<in> ?A \<Longrightarrow> \<exists>B. ?A = insert ?a B \<and> ?a \<notin> B
(\<forall>x. x \<notin> ?A) = (?A = {})
(\<And>a b. ?y = (a, b) \<Longrightarrow> ?P) \<Longrightarrow> ?P
\<forall>x y z. (x, y) \<in> f \<and> (x, z) \<in> f \<longrightarrow> z = y
(?b, ?b1) \<in> f \<Longrightarrow> ?b = 0

goal (1 subgoal):
 1. f = {(0, v)}
[PROOF STEP]
by (metis (no_types))
[PROOF STATE]
proof (state)
this:
f = {(0, v)}

goal (1 subgoal):
 1. maintained (reflexivity_rule S_Idt) G
[PROOF STEP]
from v r
[PROOF STATE]
proof (chain)
picking this:
(0, v) \<in> f
f `` {0} \<subseteq> vertices G
[PROOF STEP]
have v:"v \<in> vertices G"
[PROOF STATE]
proof (prove)
using this:
(0, v) \<in> f
f `` {0} \<subseteq> vertices G

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

goal (1 subgoal):
 1. maintained (reflexivity_rule S_Idt) G
[PROOF STEP]
with v_gr
[PROOF STATE]
proof (chain)
picking this:
\<forall>a b. ((S_Idt, a, b) \<in> edges G) = (a \<in> vertices G \<and> b = a)
v \<in> vertices G
[PROOF STEP]
have "(S_Idt, v, v) \<in> edges G"
[PROOF STATE]
proof (prove)
using this:
\<forall>a b. ((S_Idt, a, b) \<in> edges G) = (a \<in> vertices G \<and> b = a)
v \<in> vertices G

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

goal (1 subgoal):
 1. maintained (reflexivity_rule S_Idt) G
[PROOF STEP]
hence "edge_preserving {(0, v)} {(S_Idt, 0, 0)} (edges G)"
[PROOF STATE]
proof (prove)
using this:
(S_Idt, v, v) \<in> edges G

goal (1 subgoal):
 1. edge_preserving {(0::'c, v)} {(S_Idt, 0::'c, 0::'c)} (edges G)
[PROOF STEP]
unfolding edge_preserving
[PROOF STATE]
proof (prove)
using this:
(S_Idt, v, v) \<in> edges G

goal (1 subgoal):
 1. on_triple {(0::'c, v)} `` {(S_Idt, 0::'c, 0::'c)} \<subseteq> edges G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
edge_preserving {(0::?'c1, v)} {(S_Idt, 0::?'c1, 0::?'c1)} (edges G)

goal (1 subgoal):
 1. maintained (reflexivity_rule S_Idt) G
[PROOF STEP]
hence "graph_homomorphism (LG {(S_Idt, 0, 0)} {0}) G f"
[PROOF STATE]
proof (prove)
using this:
edge_preserving {(0::?'c1, v)} {(S_Idt, 0::?'c1, 0::?'c1)} (edges G)

goal (1 subgoal):
 1. graph_homomorphism (LG {(S_Idt, 0, 0)} {0}) G f
[PROOF STEP]
unfolding f
      graph_homomorphism_def
[PROOF STATE]
proof (prove)
using this:
edge_preserving {(0::?'c1, v)} {(S_Idt, 0::?'c1, 0::?'c1)} (edges G)

goal (1 subgoal):
 1. vertices (LG {(S_Idt, 0, 0)} {0}) = Domain {(0, v)} \<and> graph (LG {(S_Idt, 0, 0)} {0}) \<and> graph G \<and> {(0, v)} `` vertices (LG {(S_Idt, 0, 0)} {0}) \<subseteq> vertices G \<and> univalent {(0, v)} \<and> edge_preserving {(0, v)} (edges (LG {(S_Idt, 0, 0)} {0})) (edges G)
[PROOF STEP]
using g v
[PROOF STATE]
proof (prove)
using this:
edge_preserving {(0::?'c1, v)} {(S_Idt, 0::?'c1, 0::?'c1)} (edges G)
graph G
v \<in> vertices G

goal (1 subgoal):
 1. vertices (LG {(S_Idt, 0, 0)} {0}) = Domain {(0, v)} \<and> graph (LG {(S_Idt, 0, 0)} {0}) \<and> graph G \<and> {(0, v)} `` vertices (LG {(S_Idt, 0, 0)} {0}) \<subseteq> vertices G \<and> univalent {(0, v)} \<and> edge_preserving {(0, v)} (edges (LG {(S_Idt, 0, 0)} {0})) (edges G)
[PROOF STEP]
by (auto simp:univalent_def)
[PROOF STATE]
proof (state)
this:
graph_homomorphism (LG {(S_Idt, 0, 0)} {0}) G f

goal (1 subgoal):
 1. maintained (reflexivity_rule S_Idt) G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
graph_homomorphism (LG {} {0}) G ?f2 \<Longrightarrow> graph_homomorphism (LG {(S_Idt, 0, 0)} {0}) G ?f2

goal (1 subgoal):
 1. maintained (reflexivity_rule S_Idt) G
[PROOF STEP]
thus "maintained (reflexivity_rule S_Idt) G"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (LG {} {0}) G ?f2 \<Longrightarrow> graph_homomorphism (LG {(S_Idt, 0, 0)} {0}) G ?f2

goal (1 subgoal):
 1. maintained (reflexivity_rule S_Idt) G
[PROOF STEP]
unfolding reflexivity_rule_def maintained_def
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (LG {} {0}) G ?f2 \<Longrightarrow> graph_homomorphism (LG {(S_Idt, 0, 0)} {0}) G ?f2

goal (1 subgoal):
 1. \<forall>f. graph_homomorphism (fst (LG {} {0}, LG {(S_Idt, 0, 0)} {0})) G f \<longrightarrow> extensible (LG {} {0}, LG {(S_Idt, 0, 0)} {0}) G f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
maintained (reflexivity_rule S_Idt) G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma standard_maintains_identity_rules:
  assumes "standard' C G" "x\<in>identity_rules L"
  shows "maintained x G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained x G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. maintained x G
[PROOF STEP]
consider "x = reflexivity_rule S_Idt" | "x = transitive_rule S_Idt" | "x = symmetry_rule S_Idt"
    |  "\<exists> l. x = congruence_rule S_Idt l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = reflexivity_rule S_Idt \<Longrightarrow> thesis; x = transitive_rule S_Idt \<Longrightarrow> thesis; x = symmetry_rule S_Idt \<Longrightarrow> thesis; \<exists>l. x = congruence_rule S_Idt l \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
standard' C G
x \<in> identity_rules L

goal (1 subgoal):
 1. \<lbrakk>x = reflexivity_rule S_Idt \<Longrightarrow> thesis; x = transitive_rule S_Idt \<Longrightarrow> thesis; x = symmetry_rule S_Idt \<Longrightarrow> thesis; \<exists>l. x = congruence_rule S_Idt l \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding identity_rules_def Un_iff
[PROOF STATE]
proof (prove)
using this:
standard' C G
x \<in> {reflexivity_rule S_Idt, transitive_rule S_Idt, symmetry_rule S_Idt} \<or> x \<in> congruence_rules S_Idt L

goal (1 subgoal):
 1. \<lbrakk>x = reflexivity_rule S_Idt \<Longrightarrow> thesis; x = transitive_rule S_Idt \<Longrightarrow> thesis; x = symmetry_rule S_Idt \<Longrightarrow> thesis; \<exists>l. x = congruence_rule S_Idt l \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = reflexivity_rule S_Idt \<Longrightarrow> ?thesis; x = transitive_rule S_Idt \<Longrightarrow> ?thesis; x = symmetry_rule S_Idt \<Longrightarrow> ?thesis; \<exists>l. x = congruence_rule S_Idt l \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. maintained x G
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = reflexivity_rule S_Idt \<Longrightarrow> ?thesis; x = transitive_rule S_Idt \<Longrightarrow> ?thesis; x = symmetry_rule S_Idt \<Longrightarrow> ?thesis; \<exists>l. x = congruence_rule S_Idt l \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. maintained x G
[PROOF STEP]
using standard_identity_rules[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = reflexivity_rule S_Idt \<Longrightarrow> ?thesis; x = transitive_rule S_Idt \<Longrightarrow> ?thesis; x = symmetry_rule S_Idt \<Longrightarrow> ?thesis; \<exists>l. x = congruence_rule S_Idt l \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
maintained (reflexivity_rule S_Idt) G
maintained (transitive_rule S_Idt) G
maintained (symmetry_rule S_Idt) G
maintained (congruence_rule S_Idt ?l) G

goal (1 subgoal):
 1. maintained x G
[PROOF STEP]
by(cases,auto)
[PROOF STATE]
proof (state)
this:
maintained x G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma standard_maintains_rules:
  assumes "standard' C G"
  shows "maintainedA (standard_rules C L) G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintainedA (standard_rules C L) G
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R. R \<in> standard_rules C L \<Longrightarrow> maintained R G
[PROOF STEP]
fix R
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R. R \<in> standard_rules C L \<Longrightarrow> maintained R G
[PROOF STEP]
assume "R \<in> standard_rules C L"
[PROOF STATE]
proof (state)
this:
R \<in> standard_rules C L

goal (1 subgoal):
 1. \<And>R. R \<in> standard_rules C L \<Longrightarrow> maintained R G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
R \<in> standard_rules C L
[PROOF STEP]
consider "R \<in> constant_rules C" | "R \<in> identity_rules L"
    | "R = top_rule S_Top" | "R = nonempty_rule"
[PROOF STATE]
proof (prove)
using this:
R \<in> standard_rules C L

goal (1 subgoal):
 1. \<lbrakk>R \<in> constant_rules C \<Longrightarrow> thesis; R \<in> identity_rules L \<Longrightarrow> thesis; R = top_rule S_Top \<Longrightarrow> thesis; R = nonempty_rule \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp:standard_rules_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>R \<in> constant_rules C \<Longrightarrow> ?thesis; R \<in> identity_rules L \<Longrightarrow> ?thesis; R = top_rule S_Top \<Longrightarrow> ?thesis; R = nonempty_rule \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>R. R \<in> standard_rules C L \<Longrightarrow> maintained R G
[PROOF STEP]
thus "maintained R G"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>R \<in> constant_rules C \<Longrightarrow> ?thesis; R \<in> identity_rules L \<Longrightarrow> ?thesis; R = top_rule S_Top \<Longrightarrow> ?thesis; R = nonempty_rule \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. maintained R G
[PROOF STEP]
using assms standard_maintains_constant_rules[OF assms]
          standard_maintains_identity_rules[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>R \<in> constant_rules C \<Longrightarrow> ?thesis; R \<in> identity_rules L \<Longrightarrow> ?thesis; R = top_rule S_Top \<Longrightarrow> ?thesis; R = nonempty_rule \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
standard' C G
?R \<in> constant_rules C \<Longrightarrow> maintained ?R G
?x \<in> identity_rules ?L \<Longrightarrow> maintained ?x G

goal (1 subgoal):
 1. maintained R G
[PROOF STEP]
by (cases,auto simp:standard_def)
[PROOF STATE]
proof (state)
this:
maintained R G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma standard_rules_edges:
  assumes "(lhs, rhs) \<in> standard_rules C L" "(l, x, y) \<in> edges rhs"
  shows "(l = S_Bot \<Longrightarrow> thesis) \<Longrightarrow>
         (l = S_Top \<Longrightarrow> thesis) \<Longrightarrow>
         (l = S_Idt \<Longrightarrow> thesis) \<Longrightarrow>
         (l \<in> S_Const ` C \<Longrightarrow> thesis) \<Longrightarrow>
         (l \<in> L \<Longrightarrow> thesis) \<Longrightarrow> thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l = S_Bot \<Longrightarrow> thesis; l = S_Top \<Longrightarrow> thesis; l = S_Idt \<Longrightarrow> thesis; l \<in> S_Const ` C \<Longrightarrow> thesis; l \<in> L \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms [[simproc del: defined_all]]
[PROOF STATE]
proof (prove)
using this:
(lhs, rhs) \<in> standard_rules C L
(l, x, y) \<in> edges rhs

goal (1 subgoal):
 1. \<lbrakk>l = S_Bot \<Longrightarrow> thesis; l = S_Top \<Longrightarrow> thesis; l = S_Idt \<Longrightarrow> thesis; l \<in> S_Const ` C \<Longrightarrow> thesis; l \<in> L \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: Let_def standard_rules_def constant_rules_def identity_rules_def
   const_exists_def const_exists_rev_def const_prop_def const_disj_def
   reflexivity_rule_def transitive_rule_def symmetry_rule_def congruence_rule_def
   top_rule_def nonempty_rule_def)