[STATEMENT]
lemma chain_sup_subgraph[intro]:
  assumes "chain S"
  shows "subgraph (S j) (chain_sup S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph (S j) (chain_sup S)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subgraph (S j) (chain_sup S)
[PROOF STEP]
have c1: "S j = restrict (S j)" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph (S j)
[PROOF STEP]
using assms[unfolded chain_def,rule_format,of j] graph_homomorphism_def
[PROOF STATE]
proof (prove)
using this:
subgraph (S j) (S (j + 1))
graph_homomorphism ?G\<^sub>1 ?G\<^sub>2 ?f = (vertices ?G\<^sub>1 = Domain ?f \<and> graph ?G\<^sub>1 \<and> graph ?G\<^sub>2 \<and> ?f `` vertices ?G\<^sub>1 \<subseteq> vertices ?G\<^sub>2 \<and> univalent ?f \<and> edge_preserving ?f (edges ?G\<^sub>1) (edges ?G\<^sub>2))

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

goal (1 subgoal):
 1. subgraph (S j) (chain_sup S)
[PROOF STEP]
hence c2: "chain_sup S = restrict (chain_sup S)"
[PROOF STATE]
proof (prove)
using this:
graph (S ?j)

goal (1 subgoal):
 1. graph (chain_sup S)
[PROOF STEP]
unfolding chain_sup_def
[PROOF STATE]
proof (prove)
using this:
graph (S ?j)

goal (1 subgoal):
 1. graph (LG (\<Union>i. edges (S i)) (\<Union>i. vertices (S i)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
graph (chain_sup S)

goal (1 subgoal):
 1. subgraph (S j) (chain_sup S)
[PROOF STEP]
have c3: "graph_union (S j) (chain_sup S) = chain_sup S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_union (S j) (chain_sup S) = chain_sup S
[PROOF STEP]
unfolding chain_sup_def graph_union_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LG (edges (S j) \<union> edges (LG (\<Union>i. edges (S i)) (\<Union>i. vertices (S i)))) (vertices (S j) \<union> vertices (LG (\<Union>i. edges (S i)) (\<Union>i. vertices (S i)))) = LG (\<Union>i. edges (S i)) (\<Union>i. vertices (S i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_union (S j) (chain_sup S) = chain_sup S

goal (1 subgoal):
 1. subgraph (S j) (chain_sup S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph (S j) (chain_sup S)
[PROOF STEP]
unfolding subgraph_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph (S j) \<and> graph (chain_sup S) \<and> graph_union (S j) (chain_sup S) = chain_sup S
[PROOF STEP]
using c1 c2 c3
[PROOF STATE]
proof (prove)
using this:
graph (S ?j)
graph (chain_sup S)
graph_union (S j) (chain_sup S) = chain_sup S

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chain_sup_graph[intro]:
  assumes "chain S"
  shows "graph (chain_sup S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph (chain_sup S)
[PROOF STEP]
using chain_sup_subgraph[OF assms]
[PROOF STATE]
proof (prove)
using this:
subgraph (S ?j) (chain_sup S)

goal (1 subgoal):
 1. graph (chain_sup S)
[PROOF STEP]
unfolding subgraph_def
[PROOF STATE]
proof (prove)
using this:
graph (S ?j) \<and> graph (chain_sup S) \<and> graph_union (S ?j) (chain_sup S) = chain_sup S

goal (1 subgoal):
 1. graph (chain_sup S)
[PROOF STEP]
by auto


[STATEMENT]
lemma map_graph_chain_sup:
"map_graph g (chain_sup S) = chain_sup (map_graph g o S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_graph g (chain_sup S) = chain_sup (map_graph g \<circ> S)
[PROOF STEP]
unfolding map_graph_def chain_sup_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LG (on_triple g `` edges (LG (\<Union>i. edges (S i)) (\<Union>i. vertices (S i)))) (g `` vertices (LG (\<Union>i. edges (S i)) (\<Union>i. vertices (S i)))) = LG (\<Union>i. edges (((\<lambda>G. LG (on_triple g `` edges G) (g `` vertices G)) \<circ> S) i)) (\<Union>i. vertices (((\<lambda>G. LG (on_triple g `` edges G) (g `` vertices G)) \<circ> S) i))
[PROOF STEP]
by auto


[STATEMENT]
lemma graph_union_chain_sup[intro]:
  assumes "\<And> i. graph_union (S i) C = C"
  shows "graph_union (chain_sup S) C = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_union (chain_sup S) C = C
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. edges (chain_sup S) \<subseteq> edges C
 2. vertices (chain_sup S) \<subseteq> vertices C
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
graph_union (S ?i) C = C
[PROOF STEP]
have e:"edges (S i) \<subseteq> edges C" and v:"vertices (S i) \<subseteq> vertices C" for i
[PROOF STATE]
proof (prove)
using this:
graph_union (S ?i) C = C

goal (1 subgoal):
 1. edges (S i) \<subseteq> edges C &&& vertices (S i) \<subseteq> vertices C
[PROOF STEP]
by (auto simp:graph_union_iff)
[PROOF STATE]
proof (state)
this:
edges (S ?i) \<subseteq> edges C
vertices (S ?i) \<subseteq> vertices C

goal (2 subgoals):
 1. edges (chain_sup S) \<subseteq> edges C
 2. vertices (chain_sup S) \<subseteq> vertices C
[PROOF STEP]
show "edges (chain_sup S) \<subseteq> edges C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges (chain_sup S) \<subseteq> edges C
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
edges (S ?i) \<subseteq> edges C

goal (1 subgoal):
 1. edges (chain_sup S) \<subseteq> edges C
[PROOF STEP]
unfolding chain_sup_def
[PROOF STATE]
proof (prove)
using this:
edges (S ?i) \<subseteq> edges C

goal (1 subgoal):
 1. edges (LG (\<Union>i. edges (S i)) (\<Union>i. vertices (S i))) \<subseteq> edges C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
edges (chain_sup S) \<subseteq> edges C

goal (1 subgoal):
 1. vertices (chain_sup S) \<subseteq> vertices C
[PROOF STEP]
show "vertices (chain_sup S) \<subseteq> vertices C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertices (chain_sup S) \<subseteq> vertices C
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
vertices (S ?i) \<subseteq> vertices C

goal (1 subgoal):
 1. vertices (chain_sup S) \<subseteq> vertices C
[PROOF STEP]
unfolding chain_sup_def
[PROOF STATE]
proof (prove)
using this:
vertices (S ?i) \<subseteq> vertices C

goal (1 subgoal):
 1. vertices (LG (\<Union>i. edges (S i)) (\<Union>i. vertices (S i))) \<subseteq> vertices C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vertices (chain_sup S) \<subseteq> vertices C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_of_graph_rulesD[dest]:
  assumes "set_of_graph_rules Rs" "R \<in> Rs"
  shows "finite_graph (fst R)" "finite_graph (snd R)" "subgraph (fst R) (snd R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_graph (fst R) &&& finite_graph (snd R) &&& subgraph (fst R) (snd R)
[PROOF STEP]
using assms(1)[unfolded set_of_graph_rules_def] assms(2)
        rev_finite_subset[of "vertices (snd R)"]
        rev_finite_subset[of "edges (snd R)"]
[PROOF STATE]
proof (prove)
using this:
\<forall>R\<in>Rs. graph_rule R
R \<in> Rs
\<lbrakk>finite (vertices (snd R)); ?A \<subseteq> vertices (snd R)\<rbrakk> \<Longrightarrow> finite ?A
\<lbrakk>finite (edges (snd R)); ?A \<subseteq> edges (snd R)\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite_graph (fst R) &&& finite_graph (snd R) &&& subgraph (fst R) (snd R)
[PROOF STEP]
unfolding subgraph_def graph_union_iff
[PROOF STATE]
proof (prove)
using this:
\<forall>R\<in>Rs. (graph (fst R) \<and> graph (snd R) \<and> edges (fst R) \<subseteq> edges (snd R) \<and> vertices (fst R) \<subseteq> vertices (snd R)) \<and> finite_graph (snd R)
R \<in> Rs
\<lbrakk>finite (vertices (snd R)); ?A \<subseteq> vertices (snd R)\<rbrakk> \<Longrightarrow> finite ?A
\<lbrakk>finite (edges (snd R)); ?A \<subseteq> edges (snd R)\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite_graph (fst R) &&& finite_graph (snd R) &&& graph (fst R) \<and> graph (snd R) \<and> edges (fst R) \<subseteq> edges (snd R) \<and> vertices (fst R) \<subseteq> vertices (snd R)
[PROOF STEP]
by auto


[STATEMENT]
lemma agree_on_comm[intro]: "agree_on X f g = agree_on X g f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. agree_on X f g = agree_on X g f
[PROOF STEP]
unfolding agree_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>v\<in>vertices X. f `` {v} = g `` {v}) = (\<forall>v\<in>vertices X. g `` {v} = f `` {v})
[PROOF STEP]
by auto


[STATEMENT]
lemma agree_on_refl[intro]:
  "agree_on R f f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. agree_on R f f
[PROOF STEP]
unfolding agree_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v\<in>vertices R. f `` {v} = f `` {v}
[PROOF STEP]
by auto


[STATEMENT]
lemma agree_on_trans:
  assumes "agree_on X f g" "agree_on X g h"
  shows "agree_on X f h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. agree_on X f h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
agree_on X f g
agree_on X g h

goal (1 subgoal):
 1. agree_on X f h
[PROOF STEP]
unfolding agree_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vertices X. f `` {v} = g `` {v}
\<forall>v\<in>vertices X. g `` {v} = h `` {v}

goal (1 subgoal):
 1. \<forall>v\<in>vertices X. f `` {v} = h `` {v}
[PROOF STEP]
by auto


[STATEMENT]
lemma agree_on_equivp:
  shows "equivp (agree_on G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivp (agree_on G)
[PROOF STEP]
by (auto intro:agree_on_trans intro!:equivpI simp:reflp_def symp_def transp_def agree_on_comm)


[STATEMENT]
lemma agree_on_subset:
  assumes "f \<subseteq> g" "vertices G \<subseteq> Domain f" "univalent g"
  shows "agree_on G f g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. agree_on G f g
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<subseteq> g
vertices G \<subseteq> Domain f
univalent g

goal (1 subgoal):
 1. agree_on G f g
[PROOF STEP]
unfolding agree_on_def
[PROOF STATE]
proof (prove)
using this:
f \<subseteq> g
vertices G \<subseteq> Domain f
univalent g

goal (1 subgoal):
 1. \<forall>v\<in>vertices G. f `` {v} = g `` {v}
[PROOF STEP]
by auto


[STATEMENT]
lemma agree_iff_subset[simp]:
  assumes "graph_homomorphism G X f" "univalent g"
  shows "agree_on G f g \<longleftrightarrow> f \<subseteq> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. agree_on G f g = (f \<subseteq> g)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism G X f
univalent g

goal (1 subgoal):
 1. agree_on G f g = (f \<subseteq> g)
[PROOF STEP]
unfolding agree_on_def graph_homomorphism_def
[PROOF STATE]
proof (prove)
using this:
vertices G = Domain f \<and> graph G \<and> graph X \<and> f `` vertices G \<subseteq> vertices X \<and> univalent f \<and> edge_preserving f (edges G) (edges X)
univalent g

goal (1 subgoal):
 1. (\<forall>v\<in>vertices G. f `` {v} = g `` {v}) = (f \<subseteq> g)
[PROOF STEP]
by auto


[STATEMENT]
lemma agree_on_ext:
  assumes "agree_on G f\<^sub>1 f\<^sub>2"
  shows "agree_on G (f\<^sub>1 O g) (f\<^sub>2 O g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. agree_on G (f\<^sub>1 O g) (f\<^sub>2 O g)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
agree_on G f\<^sub>1 f\<^sub>2

goal (1 subgoal):
 1. agree_on G (f\<^sub>1 O g) (f\<^sub>2 O g)
[PROOF STEP]
unfolding agree_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vertices G. f\<^sub>1 `` {v} = f\<^sub>2 `` {v}

goal (1 subgoal):
 1. \<forall>v\<in>vertices G. (f\<^sub>1 O g) `` {v} = (f\<^sub>2 O g) `` {v}
[PROOF STEP]
by auto


[STATEMENT]
lemma agree_on_then_eq:
  assumes "agree_on G f\<^sub>1 f\<^sub>2" "Domain f\<^sub>1 = vertices G" "Domain f\<^sub>2 = vertices G"
  shows "f\<^sub>1 = f\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<^sub>1 = f\<^sub>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f\<^sub>1 = f\<^sub>2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
agree_on G f\<^sub>1 f\<^sub>2
Domain f\<^sub>1 = vertices G
Domain f\<^sub>2 = vertices G
[PROOF STEP]
have agr:"\<And> v. v\<in>Domain f\<^sub>1 \<Longrightarrow> f\<^sub>1 `` {v} = f\<^sub>2 `` {v}"
[PROOF STATE]
proof (prove)
using this:
agree_on G f\<^sub>1 f\<^sub>2
Domain f\<^sub>1 = vertices G
Domain f\<^sub>2 = vertices G

goal (1 subgoal):
 1. \<And>v. v \<in> Domain f\<^sub>1 \<Longrightarrow> f\<^sub>1 `` {v} = f\<^sub>2 `` {v}
[PROOF STEP]
unfolding agree_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vertices G. f\<^sub>1 `` {v} = f\<^sub>2 `` {v}
Domain f\<^sub>1 = vertices G
Domain f\<^sub>2 = vertices G

goal (1 subgoal):
 1. \<And>v. v \<in> Domain f\<^sub>1 \<Longrightarrow> f\<^sub>1 `` {v} = f\<^sub>2 `` {v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?v \<in> Domain f\<^sub>1 \<Longrightarrow> f\<^sub>1 `` {?v} = f\<^sub>2 `` {?v}

goal (1 subgoal):
 1. f\<^sub>1 = f\<^sub>2
[PROOF STEP]
have agr2:"\<And> v. v\<notin>Domain f\<^sub>1 \<Longrightarrow> f\<^sub>1 `` {v} = {}"
            "\<And> v. v\<notin>Domain f\<^sub>2 \<Longrightarrow> f\<^sub>2 `` {v} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v. v \<notin> Domain f\<^sub>1 \<Longrightarrow> f\<^sub>1 `` {v} = {}) &&& (\<And>v. v \<notin> Domain f\<^sub>2 \<Longrightarrow> f\<^sub>2 `` {v} = {})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?v \<notin> Domain f\<^sub>1 \<Longrightarrow> f\<^sub>1 `` {?v} = {}
?v \<notin> Domain f\<^sub>2 \<Longrightarrow> f\<^sub>2 `` {?v} = {}

goal (1 subgoal):
 1. f\<^sub>1 = f\<^sub>2
[PROOF STEP]
with agr agr2 assms
[PROOF STATE]
proof (chain)
picking this:
?v \<in> Domain f\<^sub>1 \<Longrightarrow> f\<^sub>1 `` {?v} = f\<^sub>2 `` {?v}
?v \<notin> Domain f\<^sub>1 \<Longrightarrow> f\<^sub>1 `` {?v} = {}
?v \<notin> Domain f\<^sub>2 \<Longrightarrow> f\<^sub>2 `` {?v} = {}
agree_on G f\<^sub>1 f\<^sub>2
Domain f\<^sub>1 = vertices G
Domain f\<^sub>2 = vertices G
?v \<notin> Domain f\<^sub>1 \<Longrightarrow> f\<^sub>1 `` {?v} = {}
?v \<notin> Domain f\<^sub>2 \<Longrightarrow> f\<^sub>2 `` {?v} = {}
[PROOF STEP]
have "\<And> v. f\<^sub>1 `` {v} = f\<^sub>2 `` {v}"
[PROOF STATE]
proof (prove)
using this:
?v \<in> Domain f\<^sub>1 \<Longrightarrow> f\<^sub>1 `` {?v} = f\<^sub>2 `` {?v}
?v \<notin> Domain f\<^sub>1 \<Longrightarrow> f\<^sub>1 `` {?v} = {}
?v \<notin> Domain f\<^sub>2 \<Longrightarrow> f\<^sub>2 `` {?v} = {}
agree_on G f\<^sub>1 f\<^sub>2
Domain f\<^sub>1 = vertices G
Domain f\<^sub>2 = vertices G
?v \<notin> Domain f\<^sub>1 \<Longrightarrow> f\<^sub>1 `` {?v} = {}
?v \<notin> Domain f\<^sub>2 \<Longrightarrow> f\<^sub>2 `` {?v} = {}

goal (1 subgoal):
 1. \<And>v. f\<^sub>1 `` {v} = f\<^sub>2 `` {v}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f\<^sub>1 `` {?v} = f\<^sub>2 `` {?v}

goal (1 subgoal):
 1. f\<^sub>1 = f\<^sub>2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f\<^sub>1 `` {?v} = f\<^sub>2 `` {?v}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma agree_on_subg_compose:
  assumes "agree_on R g h" "agree_on F f g" "subgraph F R"
  shows "agree_on F f h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. agree_on F f h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
agree_on R g h
agree_on F f g
subgraph F R

goal (1 subgoal):
 1. agree_on F f h
[PROOF STEP]
unfolding agree_on_def subgraph_def graph_union_iff
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>vertices R. g `` {v} = h `` {v}
\<forall>v\<in>vertices F. f `` {v} = g `` {v}
graph F \<and> graph R \<and> edges F \<subseteq> edges R \<and> vertices F \<subseteq> vertices R

goal (1 subgoal):
 1. \<forall>v\<in>vertices F. f `` {v} = h `` {v}
[PROOF STEP]
by auto


[STATEMENT]
lemma extensibleI[intro]: (* not nice as a standard rule, since obtained variables cannot be used *)
  assumes "graph_homomorphism R2 G g" "agree_on R1 f g"
  shows "extensible (R1,R2) G f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extensible (R1, R2) G f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism R2 G g
agree_on R1 f g

goal (1 subgoal):
 1. extensible (R1, R2) G f
[PROOF STEP]
unfolding extensible_def
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism R2 G g
agree_on R1 f g

goal (1 subgoal):
 1. \<exists>g. graph_homomorphism (snd (R1, R2)) G g \<and> agree_on (fst (R1, R2)) f g
[PROOF STEP]
by auto


[STATEMENT]
lemma extensibleD[elim]:
  assumes "extensible R G f"
          "\<And> g. graph_homomorphism (snd R) G g \<Longrightarrow> agree_on (fst R) f g \<Longrightarrow> thesis"
  shows thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using assms extensible_def
[PROOF STATE]
proof (prove)
using this:
extensible R G f
\<lbrakk>graph_homomorphism (snd R) G ?g; agree_on (fst R) f ?g\<rbrakk> \<Longrightarrow> thesis
extensible ?R ?G ?f \<equiv> \<exists>g. graph_homomorphism (snd ?R) ?G g \<and> agree_on (fst ?R) ?f g

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma extensible_refl_concr[simp]:
  assumes "graph_homomorphism (LG e\<^sub>1 v) G f"
  shows "extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f \<longleftrightarrow> graph_homomorphism (LG e\<^sub>2 v) G f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f = graph_homomorphism (LG e\<^sub>2 v) G f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f \<Longrightarrow> graph_homomorphism (LG e\<^sub>2 v) G f
 2. graph_homomorphism (LG e\<^sub>2 v) G f \<Longrightarrow> extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f
[PROOF STEP]
assume "extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f"
[PROOF STATE]
proof (state)
this:
extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f

goal (2 subgoals):
 1. extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f \<Longrightarrow> graph_homomorphism (LG e\<^sub>2 v) G f
 2. graph_homomorphism (LG e\<^sub>2 v) G f \<Longrightarrow> extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f
[PROOF STEP]
obtain g where g: "graph_homomorphism (LG e\<^sub>2 v) G g" "agree_on (LG e\<^sub>1 v) f g"
[PROOF STATE]
proof (prove)
using this:
extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>graph_homomorphism (LG e\<^sub>2 v) G g; agree_on (LG e\<^sub>1 v) f g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding extensible_def
[PROOF STATE]
proof (prove)
using this:
\<exists>g. graph_homomorphism (snd (LG e\<^sub>1 v, LG e\<^sub>2 v)) G g \<and> agree_on (fst (LG e\<^sub>1 v, LG e\<^sub>2 v)) f g

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>graph_homomorphism (LG e\<^sub>2 v) G g; agree_on (LG e\<^sub>1 v) f g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism (LG e\<^sub>2 v) G g
agree_on (LG e\<^sub>1 v) f g

goal (2 subgoals):
 1. extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f \<Longrightarrow> graph_homomorphism (LG e\<^sub>2 v) G f
 2. graph_homomorphism (LG e\<^sub>2 v) G f \<Longrightarrow> extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f
[PROOF STEP]
hence d:"Domain f = Domain g" "univalent f" "univalent g"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (LG e\<^sub>2 v) G g
agree_on (LG e\<^sub>1 v) f g

goal (1 subgoal):
 1. Domain f = Domain g &&& univalent f &&& univalent g
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (LG e\<^sub>2 v) G g
agree_on (LG e\<^sub>1 v) f g
graph_homomorphism (LG e\<^sub>1 v) G f

goal (1 subgoal):
 1. Domain f = Domain g &&& univalent f &&& univalent g
[PROOF STEP]
unfolding graph_homomorphism_def
[PROOF STATE]
proof (prove)
using this:
vertices (LG e\<^sub>2 v) = Domain g \<and> graph (LG e\<^sub>2 v) \<and> graph G \<and> g `` vertices (LG e\<^sub>2 v) \<subseteq> vertices G \<and> univalent g \<and> edge_preserving g (edges (LG e\<^sub>2 v)) (edges G)
agree_on (LG e\<^sub>1 v) f g
vertices (LG e\<^sub>1 v) = Domain f \<and> graph (LG e\<^sub>1 v) \<and> graph G \<and> f `` vertices (LG e\<^sub>1 v) \<subseteq> vertices G \<and> univalent f \<and> edge_preserving f (edges (LG e\<^sub>1 v)) (edges G)

goal (1 subgoal):
 1. Domain f = Domain g &&& univalent f &&& univalent g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Domain f = Domain g
univalent f
univalent g

goal (2 subgoals):
 1. extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f \<Longrightarrow> graph_homomorphism (LG e\<^sub>2 v) G f
 2. graph_homomorphism (LG e\<^sub>2 v) G f \<Longrightarrow> extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f
[PROOF STEP]
from g
[PROOF STATE]
proof (chain)
picking this:
graph_homomorphism (LG e\<^sub>2 v) G g
agree_on (LG e\<^sub>1 v) f g
[PROOF STEP]
have subs:"f \<subseteq> g"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (LG e\<^sub>2 v) G g
agree_on (LG e\<^sub>1 v) f g

goal (1 subgoal):
 1. f \<subseteq> g
[PROOF STEP]
by(subst agree_iff_subset[symmetric,OF assms],auto simp:graph_homomorphism_def)
[PROOF STATE]
proof (state)
this:
f \<subseteq> g

goal (2 subgoals):
 1. extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f \<Longrightarrow> graph_homomorphism (LG e\<^sub>2 v) G f
 2. graph_homomorphism (LG e\<^sub>2 v) G f \<Longrightarrow> extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f
[PROOF STEP]
with d
[PROOF STATE]
proof (chain)
picking this:
Domain f = Domain g
univalent f
univalent g
f \<subseteq> g
[PROOF STEP]
have "f = g"
[PROOF STATE]
proof (prove)
using this:
Domain f = Domain g
univalent f
univalent g
f \<subseteq> g

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

goal (2 subgoals):
 1. extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f \<Longrightarrow> graph_homomorphism (LG e\<^sub>2 v) G f
 2. graph_homomorphism (LG e\<^sub>2 v) G f \<Longrightarrow> extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f
[PROOF STEP]
thus "graph_homomorphism (LG e\<^sub>2 v) G f"
[PROOF STATE]
proof (prove)
using this:
f = g

goal (1 subgoal):
 1. graph_homomorphism (LG e\<^sub>2 v) G f
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
f = g
graph_homomorphism (LG e\<^sub>2 v) G g
agree_on (LG e\<^sub>1 v) f g

goal (1 subgoal):
 1. graph_homomorphism (LG e\<^sub>2 v) G f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism (LG e\<^sub>2 v) G f

goal (1 subgoal):
 1. graph_homomorphism (LG e\<^sub>2 v) G f \<Longrightarrow> extensible (LG e\<^sub>1 v, LG e\<^sub>2 v) G f
[PROOF STEP]
qed (auto simp: assms extensible_def)


[STATEMENT]
lemma   extensible_chain_sup[intro]:
assumes "chain S" "extensible R (S j) f"
shows "extensible R (chain_sup S) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extensible R (chain_sup S) f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. extensible R (chain_sup S) f
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
chain S
extensible R (S j) f
[PROOF STEP]
obtain g where g:"graph_homomorphism (snd R) (S j) g \<and> agree_on (fst R) f g"
[PROOF STATE]
proof (prove)
using this:
chain S
extensible R (S j) f

goal (1 subgoal):
 1. (\<And>g. graph_homomorphism (snd R) (S j) g \<and> agree_on (fst R) f g \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding extensible_def
[PROOF STATE]
proof (prove)
using this:
chain S
\<exists>g. graph_homomorphism (snd R) (S j) g \<and> agree_on (fst R) f g

goal (1 subgoal):
 1. (\<And>g. graph_homomorphism (snd R) (S j) g \<and> agree_on (fst R) f g \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism (snd R) (S j) g \<and> agree_on (fst R) f g

goal (1 subgoal):
 1. extensible R (chain_sup S) f
[PROOF STEP]
have [simp]:"g O Id_on (vertices (S j)) = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g O Id_on (vertices (S j)) = g
[PROOF STEP]
using g[unfolded graph_homomorphism_def]
[PROOF STATE]
proof (prove)
using this:
(vertices (snd R) = Domain g \<and> graph (snd R) \<and> graph (S j) \<and> g `` vertices (snd R) \<subseteq> vertices (S j) \<and> univalent g \<and> edge_preserving g (edges (snd R)) (edges (S j))) \<and> agree_on (fst R) f g

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

goal (1 subgoal):
 1. extensible R (chain_sup S) f
[PROOF STEP]
from g assms(1)
[PROOF STATE]
proof (chain)
picking this:
graph_homomorphism (snd R) (S j) g \<and> agree_on (fst R) f g
chain S
[PROOF STEP]
have "graph_homomorphism (snd R) (S j) g" "subgraph (S j) (chain_sup S)"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (snd R) (S j) g \<and> agree_on (fst R) f g
chain S

goal (1 subgoal):
 1. graph_homomorphism (snd R) (S j) g &&& subgraph (S j) (chain_sup S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism (snd R) (S j) g
subgraph (S j) (chain_sup S)

goal (1 subgoal):
 1. extensible R (chain_sup S) f
[PROOF STEP]
from graph_homomorphism_composes[OF this]
[PROOF STATE]
proof (chain)
picking this:
graph_homomorphism (snd R) (chain_sup S) (g O Id_on (vertices (S j)))
[PROOF STEP]
have "graph_homomorphism (snd R) (chain_sup S) g"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (snd R) (chain_sup S) (g O Id_on (vertices (S j)))

goal (1 subgoal):
 1. graph_homomorphism (snd R) (chain_sup S) g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism (snd R) (chain_sup S) g

goal (1 subgoal):
 1. extensible R (chain_sup S) f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (snd R) (chain_sup S) g

goal (1 subgoal):
 1. extensible R (chain_sup S) f
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (snd R) (chain_sup S) g
graph_homomorphism (snd R) (S j) g \<and> agree_on (fst R) f g

goal (1 subgoal):
 1. extensible R (chain_sup S) f
[PROOF STEP]
unfolding extensible_def
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (snd R) (chain_sup S) g
graph_homomorphism (snd R) (S j) g \<and> agree_on (fst R) f g

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma maintainedI[intro]:
  assumes "\<And> f. graph_homomorphism A G f \<Longrightarrow> extensible (A,B) G f"
  shows "maintained (A,B) G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained (A, B) G
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism A G ?f \<Longrightarrow> extensible (A, B) G ?f

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

goal (1 subgoal):
 1. \<forall>f. graph_homomorphism (fst (A, B)) G f \<longrightarrow> extensible (A, B) G f
[PROOF STEP]
by auto


[STATEMENT]
lemma maintainedD[dest]:
  assumes "maintained (A,B) G" "graph_homomorphism A G f"
  shows "extensible (A,B) G f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extensible (A, B) G f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
maintained (A, B) G
graph_homomorphism A G f

goal (1 subgoal):
 1. extensible (A, B) G f
[PROOF STEP]
unfolding maintained_def
[PROOF STATE]
proof (prove)
using this:
\<forall>f. graph_homomorphism (fst (A, B)) G f \<longrightarrow> extensible (A, B) G f
graph_homomorphism A G f

goal (1 subgoal):
 1. extensible (A, B) G f
[PROOF STEP]
by auto


[STATEMENT]
lemma maintainedD2[dest]:
  assumes "maintained (A,B) G" "graph_homomorphism A G f"
          "\<And> g. graph_homomorphism B G g \<Longrightarrow> f \<subseteq> g \<Longrightarrow> thesis"
        shows thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using maintainedD[OF assms(1,2),unfolded extensible_def]
[PROOF STATE]
proof (prove)
using this:
\<exists>g. graph_homomorphism (snd (A, B)) G g \<and> agree_on (fst (A, B)) f g

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. graph_homomorphism (snd (A, B)) G x \<and> agree_on (fst (A, B)) f x \<Longrightarrow> thesis
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. graph_homomorphism (snd (A, B)) G x \<and> agree_on (fst (A, B)) f x \<Longrightarrow> thesis
[PROOF STEP]
assume "graph_homomorphism (snd (A, B)) G g \<and> agree_on (fst (A, B)) f g"
[PROOF STATE]
proof (state)
this:
graph_homomorphism (snd (A, B)) G g \<and> agree_on (fst (A, B)) f g

goal (1 subgoal):
 1. \<And>x. graph_homomorphism (snd (A, B)) G x \<and> agree_on (fst (A, B)) f x \<Longrightarrow> thesis
[PROOF STEP]
hence "graph_homomorphism B G g" "f \<subseteq> g"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (snd (A, B)) G g \<and> agree_on (fst (A, B)) f g

goal (1 subgoal):
 1. graph_homomorphism B G g &&& f \<subseteq> g
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (snd (A, B)) G g \<and> agree_on (fst (A, B)) f g
graph_homomorphism A G f

goal (1 subgoal):
 1. graph_homomorphism B G g &&& f \<subseteq> g
[PROOF STEP]
unfolding graph_homomorphism_def2 agree_on_def
[PROOF STATE]
proof (prove)
using this:
(vertices (snd (A, B)) = Domain g \<and> univalent g \<and> graph (snd (A, B)) \<and> graph G \<and> graph_union (map_graph g (snd (A, B))) G = G) \<and> (\<forall>v\<in>vertices (fst (A, B)). f `` {v} = g `` {v})
vertices A = Domain f \<and> univalent f \<and> graph A \<and> graph G \<and> graph_union (map_graph f A) G = G

goal (1 subgoal):
 1. vertices B = Domain g \<and> univalent g \<and> graph B \<and> graph G \<and> graph_union (map_graph g B) G = G &&& f \<subseteq> g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism B G g
f \<subseteq> g

goal (1 subgoal):
 1. \<And>x. graph_homomorphism (snd (A, B)) G x \<and> agree_on (fst (A, B)) f x \<Longrightarrow> thesis
[PROOF STEP]
from assms(3)[OF this]
[PROOF STATE]
proof (chain)
picking this:
thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extensible_refl[intro]:
  "graph_homomorphism R G f \<Longrightarrow> extensible (R,R) G f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_homomorphism R G f \<Longrightarrow> extensible (R, R) G f
[PROOF STEP]
unfolding extensible_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_homomorphism R G f \<Longrightarrow> \<exists>g. graph_homomorphism (snd (R, R)) G g \<and> agree_on (fst (R, R)) f g
[PROOF STEP]
by auto


[STATEMENT]
lemma maintained_refl[intro]:
  "maintained (R,R) G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained (R, R) G
[PROOF STEP]
by auto


[STATEMENT]
lemma fin_maintainedI [intro]:
  assumes "\<And> F f. finite_graph F
           \<Longrightarrow> subgraph F (fst R)
           \<Longrightarrow> extensible (F,fst R) G f
           \<Longrightarrow> graph_homomorphism F G f
           \<Longrightarrow> extensible (F,snd R) G f"
  shows "fin_maintained R G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fin_maintained R G
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite_graph ?F; subgraph ?F (fst R); extensible (?F, fst R) G ?f; graph_homomorphism ?F G ?f\<rbrakk> \<Longrightarrow> extensible (?F, snd R) G ?f

goal (1 subgoal):
 1. fin_maintained R G
[PROOF STEP]
unfolding fin_maintained_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite_graph ?F; subgraph ?F (fst R); extensible (?F, fst R) G ?f; graph_homomorphism ?F G ?f\<rbrakk> \<Longrightarrow> extensible (?F, snd R) G ?f

goal (1 subgoal):
 1. \<forall>F f. finite_graph F \<longrightarrow> subgraph F (fst R) \<longrightarrow> extensible (F, fst R) G f \<longrightarrow> graph_homomorphism F G f \<longrightarrow> extensible (F, snd R) G f
[PROOF STEP]
by auto


[STATEMENT]
lemma maintained_then_fin_maintained[simp]:
  assumes maintained:"maintained R G"
  shows "fin_maintained R G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fin_maintained R G
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F f. \<lbrakk>finite_graph F; subgraph F (fst R); extensible (F, fst R) G f; graph_homomorphism F G f\<rbrakk> \<Longrightarrow> extensible (F, snd R) G f
[PROOF STEP]
fix F f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F f. \<lbrakk>finite_graph F; subgraph F (fst R); extensible (F, fst R) G f; graph_homomorphism F G f\<rbrakk> \<Longrightarrow> extensible (F, snd R) G f
[PROOF STEP]
assume subg:"subgraph F (fst R)"
     and ext:"extensible (F, fst R) G f" and igh:"graph_homomorphism F G f"
[PROOF STATE]
proof (state)
this:
subgraph F (fst R)
extensible (F, fst R) G f
graph_homomorphism F G f

goal (1 subgoal):
 1. \<And>F f. \<lbrakk>finite_graph F; subgraph F (fst R); extensible (F, fst R) G f; graph_homomorphism F G f\<rbrakk> \<Longrightarrow> extensible (F, snd R) G f
[PROOF STEP]
from ext[unfolded extensible_def prod.sel]
[PROOF STATE]
proof (chain)
picking this:
\<exists>g. graph_homomorphism (fst R) G g \<and> agree_on F f g
[PROOF STEP]
obtain g where
     g:"graph_homomorphism (fst R) G g" "agree_on F f g"
[PROOF STATE]
proof (prove)
using this:
\<exists>g. graph_homomorphism (fst R) G g \<and> agree_on F f g

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

goal (1 subgoal):
 1. \<And>F f. \<lbrakk>finite_graph F; subgraph F (fst R); extensible (F, fst R) G f; graph_homomorphism F G f\<rbrakk> \<Longrightarrow> extensible (F, snd R) G f
[PROOF STEP]
from maintained[unfolded maintained_def,rule_format,OF g(1)] g(2) subg
       agree_on_subg_compose
[PROOF STATE]
proof (chain)
picking this:
extensible R G g
agree_on F f g
subgraph F (fst R)
\<lbrakk>agree_on ?R ?g ?h; agree_on ?F ?f ?g; subgraph ?F ?R\<rbrakk> \<Longrightarrow> agree_on ?F ?f ?h
[PROOF STEP]
show "extensible (F, snd R) G f"
[PROOF STATE]
proof (prove)
using this:
extensible R G g
agree_on F f g
subgraph F (fst R)
\<lbrakk>agree_on ?R ?g ?h; agree_on ?F ?f ?g; subgraph ?F ?R\<rbrakk> \<Longrightarrow> agree_on ?F ?f ?h

goal (1 subgoal):
 1. extensible (F, snd R) G f
[PROOF STEP]
unfolding extensible_def prod.sel
[PROOF STATE]
proof (prove)
using this:
\<exists>ga. graph_homomorphism (snd R) G ga \<and> agree_on (fst R) g ga
agree_on F f g
subgraph F (fst R)
\<lbrakk>agree_on ?R ?g ?h; agree_on ?F ?f ?g; subgraph ?F ?R\<rbrakk> \<Longrightarrow> agree_on ?F ?f ?h

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fin_maintained_maintained:
  assumes "finite_graph (fst R)"
  shows "fin_maintained R G \<longleftrightarrow> maintained R G" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fin_maintained R G = maintained R G
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fin_maintained R G \<Longrightarrow> maintained R G
 2. maintained R G \<Longrightarrow> fin_maintained R G
[PROOF STEP]
from assms rev_finite_subset
[PROOF STATE]
proof (chain)
picking this:
finite_graph (fst R)
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> finite ?A
[PROOF STEP]
have fin:"finite (vertices (fst R))"
           "finite (edges (fst R))"
           "subgraph (fst R) (fst R)"
[PROOF STATE]
proof (prove)
using this:
finite_graph (fst R)
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (vertices (fst R)) &&& finite (edges (fst R)) &&& subgraph (fst R) (fst R)
[PROOF STEP]
unfolding subgraph_def graph_union_iff
[PROOF STATE]
proof (prove)
using this:
finite_graph (fst R)
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (vertices (fst R)) &&& finite (edges (fst R)) &&& graph (fst R) \<and> graph (fst R) \<and> edges (fst R) \<subseteq> edges (fst R) \<and> vertices (fst R) \<subseteq> vertices (fst R)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (vertices (fst R))
finite (edges (fst R))
subgraph (fst R) (fst R)

goal (2 subgoals):
 1. fin_maintained R G \<Longrightarrow> maintained R G
 2. maintained R G \<Longrightarrow> fin_maintained R G
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
fin_maintained R G

goal (2 subgoals):
 1. fin_maintained R G \<Longrightarrow> maintained R G
 2. maintained R G \<Longrightarrow> fin_maintained R G
[PROOF STEP]
with fin
[PROOF STATE]
proof (chain)
picking this:
finite (vertices (fst R))
finite (edges (fst R))
subgraph (fst R) (fst R)
fin_maintained R G
[PROOF STEP]
have "extensible (fst R, fst R) G f \<Longrightarrow> graph_homomorphism (fst R) G f
         \<Longrightarrow> extensible R G f" for f
[PROOF STATE]
proof (prove)
using this:
finite (vertices (fst R))
finite (edges (fst R))
subgraph (fst R) (fst R)
fin_maintained R G

goal (1 subgoal):
 1. \<lbrakk>extensible (fst R, fst R) G f; graph_homomorphism (fst R) G f\<rbrakk> \<Longrightarrow> extensible R G f
[PROOF STEP]
unfolding fin_maintained_def
[PROOF STATE]
proof (prove)
using this:
finite (vertices (fst R))
finite (edges (fst R))
subgraph (fst R) (fst R)
\<forall>F f. finite_graph F \<longrightarrow> subgraph F (fst R) \<longrightarrow> extensible (F, fst R) G f \<longrightarrow> graph_homomorphism F G f \<longrightarrow> extensible (F, snd R) G f

goal (1 subgoal):
 1. \<lbrakk>extensible (fst R, fst R) G f; graph_homomorphism (fst R) G f\<rbrakk> \<Longrightarrow> extensible R G f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>extensible (fst R, fst R) G ?f; graph_homomorphism (fst R) G ?f\<rbrakk> \<Longrightarrow> extensible R G ?f

goal (2 subgoals):
 1. fin_maintained R G \<Longrightarrow> maintained R G
 2. maintained R G \<Longrightarrow> fin_maintained R G
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>extensible (fst R, fst R) G ?f; graph_homomorphism (fst R) G ?f\<rbrakk> \<Longrightarrow> extensible R G ?f

goal (1 subgoal):
 1. maintained R G
[PROOF STEP]
by (simp add: extensible_refl maintained_def)
[PROOF STATE]
proof (state)
this:
maintained R G

goal (1 subgoal):
 1. maintained R G \<Longrightarrow> fin_maintained R G
[PROOF STEP]
qed simp


[STATEMENT]
lemma extend_for_chain:
assumes "g 0 = f"
    and "\<And> i. graph_homomorphism (S i) C (g i)"
    and "\<And> i. agree_on (S i) (g i) (g (i + 1))"
    and "chain S"
  shows "extensible (S 0, chain_sup S) C f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extensible (S 0, chain_sup S) C f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
let ?g = "\<Union>i. g i"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
from assms(4)[unfolded chain_def subgraph_def graph_union_iff]
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. graph (S i) \<and> graph (S (i + 1)) \<and> edges (S i) \<subseteq> edges (S (i + 1)) \<and> vertices (S i) \<subseteq> vertices (S (i + 1))
[PROOF STEP]
have v:"vertices (S i) \<subseteq> vertices (S (i + 1))"
    and e:"edges (S i) \<subseteq> edges (S (i + 1))" for i
[PROOF STATE]
proof (prove)
using this:
\<forall>i. graph (S i) \<and> graph (S (i + 1)) \<and> edges (S i) \<subseteq> edges (S (i + 1)) \<and> vertices (S i) \<subseteq> vertices (S (i + 1))

goal (1 subgoal):
 1. vertices (S i) \<subseteq> vertices (S (i + 1)) &&& edges (S i) \<subseteq> edges (S (i + 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vertices (S ?i) \<subseteq> vertices (S (?i + 1))
edges (S ?i) \<subseteq> edges (S (?i + 1))

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
vertices (S ?i) \<subseteq> vertices (S (?i + 1))
edges (S ?i) \<subseteq> edges (S (?i + 1))

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
fix a b i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
assume a:"(a, b) \<in> g i"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> g i

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
hence "a \<in> vertices (S i)"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> g i

goal (1 subgoal):
 1. a \<in> vertices (S i)
[PROOF STEP]
using assms(2)[of i]
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> g i
graph_homomorphism (S i) C (g i)

goal (1 subgoal):
 1. a \<in> vertices (S i)
[PROOF STEP]
unfolding graph_homomorphism_def2
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> g i
vertices (S i) = Domain (g i) \<and> univalent (g i) \<and> graph (S i) \<and> graph C \<and> graph_union (map_graph (g i) (S i)) C = C

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

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
from assms(3)[unfolded agree_on_def,rule_format,OF this] a
[PROOF STATE]
proof (chain)
picking this:
g i `` {a} = g (i + 1) `` {a}
(a, b) \<in> g i
[PROOF STEP]
have "(a, b) \<in> g (Suc i)"
[PROOF STATE]
proof (prove)
using this:
g i `` {a} = g (i + 1) `` {a}
(a, b) \<in> g i

goal (1 subgoal):
 1. (a, b) \<in> g (Suc i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a, b) \<in> g (Suc i)

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?a2, ?b2) \<in> g ?i2 \<Longrightarrow> (?a2, ?b2) \<in> g (Suc ?i2)

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
hence gi:"g i \<subseteq> g (Suc i)" for i
[PROOF STATE]
proof (prove)
using this:
(?a2, ?b2) \<in> g ?i2 \<Longrightarrow> (?a2, ?b2) \<in> g (Suc ?i2)

goal (1 subgoal):
 1. g i \<subseteq> g (Suc i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g ?i \<subseteq> g (Suc ?i)

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
have gij:"i \<le> j \<Longrightarrow> g i \<subseteq> g j" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> j \<Longrightarrow> g i \<subseteq> g j
[PROOF STEP]
proof(induct j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<le> 0 \<Longrightarrow> g i \<subseteq> g 0
 2. \<And>j. \<lbrakk>i \<le> j \<Longrightarrow> g i \<subseteq> g j; i \<le> Suc j\<rbrakk> \<Longrightarrow> g i \<subseteq> g (Suc j)
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
i \<le> j \<Longrightarrow> g i \<subseteq> g j
i \<le> Suc j

goal (2 subgoals):
 1. i \<le> 0 \<Longrightarrow> g i \<subseteq> g 0
 2. \<And>j. \<lbrakk>i \<le> j \<Longrightarrow> g i \<subseteq> g j; i \<le> Suc j\<rbrakk> \<Longrightarrow> g i \<subseteq> g (Suc j)
[PROOF STEP]
with gi[of j]
[PROOF STATE]
proof (chain)
picking this:
g j \<subseteq> g (Suc j)
i \<le> j \<Longrightarrow> g i \<subseteq> g j
i \<le> Suc j
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
g j \<subseteq> g (Suc j)
i \<le> j \<Longrightarrow> g i \<subseteq> g j
i \<le> Suc j

goal (1 subgoal):
 1. g i \<subseteq> g (Suc j)
[PROOF STEP]
by (cases "i = Suc j",auto)
[PROOF STATE]
proof (state)
this:
g i \<subseteq> g (Suc j)

goal (1 subgoal):
 1. i \<le> 0 \<Longrightarrow> g i \<subseteq> g 0
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
?i \<le> ?j \<Longrightarrow> g ?i \<subseteq> g ?j

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
g 0 = f
[PROOF STEP]
have f_subset:"f \<subseteq> ?g"
[PROOF STATE]
proof (prove)
using this:
g 0 = f

goal (1 subgoal):
 1. f \<subseteq> \<Union> (range g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<subseteq> \<Union> (range g)

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
from assms(2)[of 0,unfolded assms(1)]
[PROOF STATE]
proof (chain)
picking this:
graph_homomorphism (S 0) C f
[PROOF STEP]
have domf:"Domain f = vertices (S 0)"
    and grC:"graph C" and v_dom:"vertices (S i) = Domain (g i)" for i
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (S 0) C f

goal (1 subgoal):
 1. Domain f = vertices (S 0) &&& graph C &&& vertices (S i) = Domain (g i)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (S 0) C f
graph_homomorphism (S ?i) C (g ?i)

goal (1 subgoal):
 1. Domain f = vertices (S 0) &&& graph C &&& vertices (S i) = Domain (g i)
[PROOF STEP]
unfolding graph_homomorphism_def
[PROOF STATE]
proof (prove)
using this:
vertices (S 0) = Domain f \<and> graph (S 0) \<and> graph C \<and> f `` vertices (S 0) \<subseteq> vertices C \<and> univalent f \<and> edge_preserving f (edges (S 0)) (edges C)
vertices (S ?i) = Domain (g ?i) \<and> graph (S ?i) \<and> graph C \<and> g ?i `` vertices (S ?i) \<subseteq> vertices C \<and> univalent (g ?i) \<and> edge_preserving (g ?i) (edges (S ?i)) (edges C)

goal (1 subgoal):
 1. Domain f = vertices (S 0) &&& graph C &&& vertices (S i) = Domain (g i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Domain f = vertices (S 0)
graph C
vertices (S ?i) = Domain (g ?i)

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Domain f = vertices (S 0)
graph C
vertices (S ?i) = Domain (g ?i)

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
fix x y z i j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
assume "(x, y) \<in> g i" "(x, z) \<in> g j"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> g i
(x, z) \<in> g j

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
with gij[of i "max i j"] gij[of j "max i j"]
[PROOF STATE]
proof (chain)
picking this:
i \<le> max i j \<Longrightarrow> g i \<subseteq> g (max i j)
j \<le> max i j \<Longrightarrow> g j \<subseteq> g (max i j)
(x, y) \<in> g i
(x, z) \<in> g j
[PROOF STEP]
have "(x,y) \<in> g (max i j)" "(x,z) \<in> g (max i j)"
[PROOF STATE]
proof (prove)
using this:
i \<le> max i j \<Longrightarrow> g i \<subseteq> g (max i j)
j \<le> max i j \<Longrightarrow> g j \<subseteq> g (max i j)
(x, y) \<in> g i
(x, z) \<in> g j

goal (1 subgoal):
 1. (x, y) \<in> g (max i j) &&& (x, z) \<in> g (max i j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> g (max i j)
(x, z) \<in> g (max i j)

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
with assms(2)[unfolded graph_homomorphism_def]
[PROOF STATE]
proof (chain)
picking this:
vertices (S ?i) = Domain (g ?i) \<and> graph (S ?i) \<and> graph C \<and> g ?i `` vertices (S ?i) \<subseteq> vertices C \<and> univalent (g ?i) \<and> edge_preserving (g ?i) (edges (S ?i)) (edges C)
(x, y) \<in> g (max i j)
(x, z) \<in> g (max i j)
[PROOF STEP]
have "y = z"
[PROOF STATE]
proof (prove)
using this:
vertices (S ?i) = Domain (g ?i) \<and> graph (S ?i) \<and> graph C \<and> g ?i `` vertices (S ?i) \<subseteq> vertices C \<and> univalent (g ?i) \<and> edge_preserving (g ?i) (edges (S ?i)) (edges C)
(x, y) \<in> g (max i j)
(x, z) \<in> g (max i j)

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

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?x2, ?y2) \<in> g ?i2; (?x2, ?z2) \<in> g ?j2\<rbrakk> \<Longrightarrow> ?y2 = ?z2

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
note univ_strong = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?x2, ?y2) \<in> g ?i2; (?x2, ?z2) \<in> g ?j2\<rbrakk> \<Longrightarrow> ?y2 = ?z2

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
hence univ:"univalent ?g"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x2, ?y2) \<in> g ?i2; (?x2, ?z2) \<in> g ?j2\<rbrakk> \<Longrightarrow> ?y2 = ?z2

goal (1 subgoal):
 1. univalent (\<Union> (range g))
[PROOF STEP]
unfolding univalent_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x2, ?y2) \<in> g ?i2; (?x2, ?z2) \<in> g ?j2\<rbrakk> \<Longrightarrow> ?y2 = ?z2

goal (1 subgoal):
 1. \<forall>x y z. (x, y) \<in> \<Union> (range g) \<and> (x, z) \<in> \<Union> (range g) \<longrightarrow> z = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
univalent (\<Union> (range g))

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
univalent (\<Union> (range g))

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
fix xa x i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
assume "(xa, x) \<in> g i"
[PROOF STATE]
proof (state)
this:
(xa, x) \<in> g i

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
hence "x \<in> vertices (map_graph (g i) (S i))"
[PROOF STATE]
proof (prove)
using this:
(xa, x) \<in> g i

goal (1 subgoal):
 1. x \<in> vertices (map_graph (g i) (S i))
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(xa, x) \<in> g i
graph_homomorphism (S ?i) C (g ?i)

goal (1 subgoal):
 1. x \<in> vertices (map_graph (g i) (S i))
[PROOF STEP]
unfolding graph_homomorphism_def
[PROOF STATE]
proof (prove)
using this:
(xa, x) \<in> g i
vertices (S ?i) = Domain (g ?i) \<and> graph (S ?i) \<and> graph C \<and> g ?i `` vertices (S ?i) \<subseteq> vertices C \<and> univalent (g ?i) \<and> edge_preserving (g ?i) (edges (S ?i)) (edges C)

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

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
hence "x \<in> vertices C"
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices (map_graph (g i) (S i))

goal (1 subgoal):
 1. x \<in> vertices C
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices (map_graph (g i) (S i))
graph_homomorphism (S ?i) C (g ?i)

goal (1 subgoal):
 1. x \<in> vertices C
[PROOF STEP]
unfolding graph_homomorphism_def2 graph_union_iff
[PROOF STATE]
proof (prove)
using this:
x \<in> vertices (map_graph (g i) (S i))
vertices (S ?i) = Domain (g ?i) \<and> univalent (g ?i) \<and> graph (S ?i) \<and> graph C \<and> edges (map_graph (g ?i) (S ?i)) \<subseteq> edges C \<and> vertices (map_graph (g ?i) (S ?i)) \<subseteq> vertices C

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

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?xa2, ?x2) \<in> g ?i2 \<Longrightarrow> ?x2 \<in> vertices C

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
note eq_v = this
[PROOF STATE]
proof (state)
this:
(?xa2, ?x2) \<in> g ?i2 \<Longrightarrow> ?x2 \<in> vertices C

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(?xa2, ?x2) \<in> g ?i2 \<Longrightarrow> ?x2 \<in> vertices C

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
fix l x y x' y' j i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
assume "(l,x,y) \<in> edges (S j)" "(x, x') \<in> g i" "(y, y') \<in> g i"
[PROOF STATE]
proof (state)
this:
(l, x, y) \<in> edges (S j)
(x, x') \<in> g i
(y, y') \<in> g i

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
with gij[of i "max i j"] gij[of j "max i j"]
         chain[OF assms(4),unfolded subgraph_def graph_union_iff, of i "max i j"]
         chain[OF assms(4),unfolded subgraph_def graph_union_iff, of j "max i j"]
[PROOF STATE]
proof (chain)
picking this:
i \<le> max i j \<Longrightarrow> g i \<subseteq> g (max i j)
j \<le> max i j \<Longrightarrow> g j \<subseteq> g (max i j)
i \<le> max i j \<Longrightarrow> graph (S i) \<and> graph (S (max i j)) \<and> edges (S i) \<subseteq> edges (S (max i j)) \<and> vertices (S i) \<subseteq> vertices (S (max i j))
j \<le> max i j \<Longrightarrow> graph (S j) \<and> graph (S (max i j)) \<and> edges (S j) \<subseteq> edges (S (max i j)) \<and> vertices (S j) \<subseteq> vertices (S (max i j))
(l, x, y) \<in> edges (S j)
(x, x') \<in> g i
(y, y') \<in> g i
[PROOF STEP]
have "(x,x') \<in> g (max i j)" "(y,y') \<in> g (max i j)"
         "(l,x,y) \<in> edges (S (max i j))"
[PROOF STATE]
proof (prove)
using this:
i \<le> max i j \<Longrightarrow> g i \<subseteq> g (max i j)
j \<le> max i j \<Longrightarrow> g j \<subseteq> g (max i j)
i \<le> max i j \<Longrightarrow> graph (S i) \<and> graph (S (max i j)) \<and> edges (S i) \<subseteq> edges (S (max i j)) \<and> vertices (S i) \<subseteq> vertices (S (max i j))
j \<le> max i j \<Longrightarrow> graph (S j) \<and> graph (S (max i j)) \<and> edges (S j) \<subseteq> edges (S (max i j)) \<and> vertices (S j) \<subseteq> vertices (S (max i j))
(l, x, y) \<in> edges (S j)
(x, x') \<in> g i
(y, y') \<in> g i

goal (1 subgoal):
 1. (x, x') \<in> g (max i j) &&& (y, y') \<in> g (max i j) &&& (l, x, y) \<in> edges (S (max i j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, x') \<in> g (max i j)
(y, y') \<in> g (max i j)
(l, x, y) \<in> edges (S (max i j))

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
hence "(l, x', y') \<in> edges C"
[PROOF STATE]
proof (prove)
using this:
(x, x') \<in> g (max i j)
(y, y') \<in> g (max i j)
(l, x, y) \<in> edges (S (max i j))

goal (1 subgoal):
 1. (l, x', y') \<in> edges C
[PROOF STEP]
using assms(2)[unfolded graph_homomorphism_def2 graph_union_iff]
[PROOF STATE]
proof (prove)
using this:
(x, x') \<in> g (max i j)
(y, y') \<in> g (max i j)
(l, x, y) \<in> edges (S (max i j))
vertices (S ?i) = Domain (g ?i) \<and> univalent (g ?i) \<and> graph (S ?i) \<and> graph C \<and> edges (map_graph (g ?i) (S ?i)) \<subseteq> edges C \<and> vertices (map_graph (g ?i) (S ?i)) \<subseteq> vertices C

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

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?l2, ?x2, ?y2) \<in> edges (S ?j2); (?x2, ?x'2) \<in> g ?i2; (?y2, ?y'2) \<in> g ?i2\<rbrakk> \<Longrightarrow> (?l2, ?x'2, ?y'2) \<in> edges C

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
note eq_e = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?l2, ?x2, ?y2) \<in> edges (S ?j2); (?x2, ?x'2) \<in> g ?i2; (?y2, ?y'2) \<in> g ?i2\<rbrakk> \<Longrightarrow> (?l2, ?x'2, ?y'2) \<in> edges C

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
have "graph_union (map_graph (g i) (chain_sup S)) C = C" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_union (map_graph (g i) (chain_sup S)) C = C
[PROOF STEP]
unfolding graph_union_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges (map_graph (g i) (chain_sup S)) \<subseteq> edges C \<and> vertices (map_graph (g i) (chain_sup S)) \<subseteq> vertices C
[PROOF STEP]
using eq_e eq_v
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?l2, ?x2, ?y2) \<in> edges (S ?j2); (?x2, ?x'2) \<in> g ?i2; (?y2, ?y'2) \<in> g ?i2\<rbrakk> \<Longrightarrow> (?l2, ?x'2, ?y'2) \<in> edges C
(?xa2, ?x2) \<in> g ?i2 \<Longrightarrow> ?x2 \<in> vertices C

goal (1 subgoal):
 1. edges (map_graph (g i) (chain_sup S)) \<subseteq> edges C \<and> vertices (map_graph (g i) (chain_sup S)) \<subseteq> vertices C
[PROOF STEP]
unfolding graph_homomorphism_def2 chain_sup_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?l2, ?x2, ?y2) \<in> edges (S ?j2); (?x2, ?x'2) \<in> g ?i2; (?y2, ?y'2) \<in> g ?i2\<rbrakk> \<Longrightarrow> (?l2, ?x'2, ?y'2) \<in> edges C
(?xa2, ?x2) \<in> g ?i2 \<Longrightarrow> ?x2 \<in> vertices C

goal (1 subgoal):
 1. edges (map_graph (g i) (LG (\<Union>i. edges (S i)) (\<Union>i. vertices (S i)))) \<subseteq> edges C \<and> vertices (map_graph (g i) (LG (\<Union>i. edges (S i)) (\<Union>i. vertices (S i)))) \<subseteq> vertices C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_union (map_graph (g ?i) (chain_sup S)) C = C

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
hence subg:"graph_union (map_graph ?g (chain_sup S)) C = C"
[PROOF STATE]
proof (prove)
using this:
graph_union (map_graph (g ?i) (chain_sup S)) C = C

goal (1 subgoal):
 1. graph_union (map_graph (\<Union> (range g)) (chain_sup S)) C = C
[PROOF STEP]
apply (rule graph_map_union)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. i \<le> j \<Longrightarrow> g i \<subseteq> g j
[PROOF STEP]
using gij
[PROOF STATE]
proof (prove)
using this:
?i \<le> ?j \<Longrightarrow> g ?i \<subseteq> g ?j

goal (1 subgoal):
 1. \<And>i j. i \<le> j \<Longrightarrow> g i \<subseteq> g j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_union (map_graph (\<Union> (range g)) (chain_sup S)) C = C

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
have "(\<Union>i. vertices (S i)) = (\<Union>i. Domain (g i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i. vertices (S i)) = (\<Union>i. Domain (g i))
[PROOF STEP]
using v_dom
[PROOF STATE]
proof (prove)
using this:
vertices (S ?i) = Domain (g ?i)

goal (1 subgoal):
 1. (\<Union>i. vertices (S i)) = (\<Union>i. Domain (g i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>i. vertices (S i)) = (\<Union>i. Domain (g i))

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
hence vd:"vertices (chain_sup S) = Domain ?g"
[PROOF STATE]
proof (prove)
using this:
(\<Union>i. vertices (S i)) = (\<Union>i. Domain (g i))

goal (1 subgoal):
 1. vertices (chain_sup S) = Domain (\<Union> (range g))
[PROOF STEP]
unfolding chain_sup_def
[PROOF STATE]
proof (prove)
using this:
(\<Union>i. vertices (S i)) = (\<Union>i. Domain (g i))

goal (1 subgoal):
 1. vertices (LG (\<Union>i. edges (S i)) (\<Union>i. vertices (S i))) = Domain (\<Union> (range g))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vertices (chain_sup S) = Domain (\<Union> (range g))

goal (2 subgoals):
 1. graph_homomorphism (chain_sup S) C ?g
 2. agree_on (S 0) f ?g
[PROOF STEP]
show "graph_homomorphism (chain_sup S) C ?g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_homomorphism (chain_sup S) C (\<Union> (range g))
[PROOF STEP]
unfolding graph_homomorphism_def2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertices (chain_sup S) = Domain (\<Union> (range g)) \<and> univalent (\<Union> (range g)) \<and> graph (chain_sup S) \<and> graph C \<and> graph_union (map_graph (\<Union> (range g)) (chain_sup S)) C = C
[PROOF STEP]
using univ chain_sup_graph[OF assms(4)] grC vd subg
[PROOF STATE]
proof (prove)
using this:
univalent (\<Union> (range g))
graph (chain_sup S)
graph C
vertices (chain_sup S) = Domain (\<Union> (range g))
graph_union (map_graph (\<Union> (range g)) (chain_sup S)) C = C

goal (1 subgoal):
 1. vertices (chain_sup S) = Domain (\<Union> (range g)) \<and> univalent (\<Union> (range g)) \<and> graph (chain_sup S) \<and> graph C \<and> graph_union (map_graph (\<Union> (range g)) (chain_sup S)) C = C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism (chain_sup S) C (\<Union> (range g))

goal (1 subgoal):
 1. agree_on (S 0) f (\<Union> (range g))
[PROOF STEP]
show "agree_on (S 0) f ?g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. agree_on (S 0) f (\<Union> (range g))
[PROOF STEP]
using agree_on_subset[OF f_subset _ univ] domf
[PROOF STATE]
proof (prove)
using this:
vertices ?G \<subseteq> Domain f \<Longrightarrow> agree_on ?G f (\<Union> (range g))
Domain f = vertices (S 0)

goal (1 subgoal):
 1. agree_on (S 0) f (\<Union> (range g))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
agree_on (S 0) f (\<Union> (range g))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma consequence_graphI[intro]:
  assumes "\<And> R. R\<in> Rs \<Longrightarrow> maintained R G"
          "\<And> R. R\<in> Rs \<Longrightarrow> subgraph (fst R) (snd R)"
          "graph G"
  shows "consequence_graph Rs G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consequence_graph Rs G
[PROOF STEP]
unfolding consequence_graph_def fin_maintained_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph G \<and> (\<forall>R\<in>Rs. subgraph (fst R) (snd R) \<and> maintained R G)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?R \<in> Rs \<Longrightarrow> maintained ?R G
?R \<in> Rs \<Longrightarrow> subgraph (fst ?R) (snd ?R)
graph G

goal (1 subgoal):
 1. graph G \<and> (\<forall>R\<in>Rs. subgraph (fst R) (snd R) \<and> maintained R G)
[PROOF STEP]
by auto


[STATEMENT]
lemma consequence_graphD[dest]:
  assumes "consequence_graph Rs G"
  shows "\<And> R. R\<in> Rs \<Longrightarrow> maintained R G"
        "\<And> R. R\<in> Rs \<Longrightarrow> subgraph (fst R) (snd R)"
        "graph G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>R. R \<in> Rs \<Longrightarrow> maintained R G) &&& (\<And>R. R \<in> Rs \<Longrightarrow> subgraph (fst R) (snd R)) &&& graph G
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
consequence_graph Rs G

goal (1 subgoal):
 1. (\<And>R. R \<in> Rs \<Longrightarrow> maintained R G) &&& (\<And>R. R \<in> Rs \<Longrightarrow> subgraph (fst R) (snd R)) &&& graph G
[PROOF STEP]
unfolding consequence_graph_def fin_maintained_def
[PROOF STATE]
proof (prove)
using this:
graph G \<and> (\<forall>R\<in>Rs. subgraph (fst R) (snd R) \<and> maintained R G)

goal (1 subgoal):
 1. (\<And>R. R \<in> Rs \<Longrightarrow> maintained R G) &&& (\<And>R. R \<in> Rs \<Longrightarrow> subgraph (fst R) (snd R)) &&& graph G
[PROOF STEP]
by auto


[STATEMENT]
lemma leastI[intro]:
assumes "subgraph S (G:: ('l, 'c) labeled_graph)"
        "\<And> C :: ('l, 'x) labeled_graph. consequence_graph Rs C \<Longrightarrow> maintained (S,G) C"
      shows "least (t:: 'x itself) Rs S G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least t Rs S G
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subgraph S G
consequence_graph Rs ?C \<Longrightarrow> maintained (S, G) ?C

goal (1 subgoal):
 1. least t Rs S G
[PROOF STEP]
unfolding least_def
[PROOF STATE]
proof (prove)
using this:
subgraph S G
consequence_graph Rs ?C \<Longrightarrow> maintained (S, G) ?C

goal (1 subgoal):
 1. subgraph S G \<and> (\<forall>C. consequence_graph Rs C \<longrightarrow> maintained (S, G) C)
[PROOF STEP]
by auto


[STATEMENT]
lemma least_consequence_graphI[intro]:
assumes "consequence_graph Rs (G:: ('l, 'c) labeled_graph)"
        "subgraph S G"
        "\<And> C :: ('l, 'x) labeled_graph. consequence_graph Rs C \<Longrightarrow> maintained (S,G) C"
      shows "least_consequence_graph (t:: 'x itself) Rs S G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_consequence_graph t Rs S G
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
consequence_graph Rs G
subgraph S G
consequence_graph Rs ?C \<Longrightarrow> maintained (S, G) ?C

goal (1 subgoal):
 1. least_consequence_graph t Rs S G
[PROOF STEP]
unfolding least_consequence_graph_def least_def
[PROOF STATE]
proof (prove)
using this:
consequence_graph Rs G
subgraph S G
consequence_graph Rs ?C \<Longrightarrow> maintained (S, G) ?C

goal (1 subgoal):
 1. consequence_graph Rs G \<and> subgraph S G \<and> (\<forall>C. consequence_graph Rs C \<longrightarrow> maintained (S, G) C)
[PROOF STEP]
by auto


[STATEMENT]
lemma fair_chainI[intro]:
  assumes "chain S"
    "\<And> R f i. R \<in> Rs \<Longrightarrow> graph_homomorphism (fst R) (S i) f \<Longrightarrow> \<exists> j. extensible R (S j) f"
  shows "fair_chain Rs S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fair_chain Rs S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
chain S
\<lbrakk>?R \<in> Rs; graph_homomorphism (fst ?R) (S ?i) ?f\<rbrakk> \<Longrightarrow> \<exists>j. extensible ?R (S j) ?f

goal (1 subgoal):
 1. fair_chain Rs S
[PROOF STEP]
unfolding fair_chain_def
[PROOF STATE]
proof (prove)
using this:
chain S
\<lbrakk>?R \<in> Rs; graph_homomorphism (fst ?R) (S ?i) ?f\<rbrakk> \<Longrightarrow> \<exists>j. extensible ?R (S j) ?f

goal (1 subgoal):
 1. chain S \<and> (\<forall>R f i. R \<in> Rs \<and> graph_homomorphism (fst R) (S i) f \<longrightarrow> (\<exists>j. extensible R (S j) f))
[PROOF STEP]
by blast


[STATEMENT]
lemma fair_chainD:
  assumes "fair_chain Rs S"
  shows "chain S"
        "R \<in> Rs \<Longrightarrow> graph_homomorphism (fst R) (S i) f \<Longrightarrow> \<exists> j. extensible R (S j) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain S &&& (\<lbrakk>R \<in> Rs; graph_homomorphism (fst R) (S i) f\<rbrakk> \<Longrightarrow> \<exists>j. extensible R (S j) f)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
fair_chain Rs S

goal (1 subgoal):
 1. chain S &&& (\<lbrakk>R \<in> Rs; graph_homomorphism (fst R) (S i) f\<rbrakk> \<Longrightarrow> \<exists>j. extensible R (S j) f)
[PROOF STEP]
unfolding fair_chain_def
[PROOF STATE]
proof (prove)
using this:
chain S \<and> (\<forall>R f i. R \<in> Rs \<and> graph_homomorphism (fst R) (S i) f \<longrightarrow> (\<exists>j. extensible R (S j) f))

goal (1 subgoal):
 1. chain S &&& (\<lbrakk>R \<in> Rs; graph_homomorphism (fst R) (S i) f\<rbrakk> \<Longrightarrow> \<exists>j. extensible R (S j) f)
[PROOF STEP]
by blast+


[STATEMENT]
lemma find_graph_occurence_vertices:
  assumes "chain S" "finite V" "univalent f" "f `` V \<subseteq> vertices (chain_sup S)"
  shows "\<exists> i. f `` V \<subseteq> vertices (S i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. f `` V \<subseteq> vertices (S i)
[PROOF STEP]
using assms(2,4)
[PROOF STATE]
proof (prove)
using this:
finite V
f `` V \<subseteq> vertices (chain_sup S)

goal (1 subgoal):
 1. \<exists>i. f `` V \<subseteq> vertices (S i)
[PROOF STEP]
proof(induct V)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f `` {} \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` {} \<subseteq> vertices (S i)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; f `` F \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` F \<subseteq> vertices (S i); f `` insert x F \<subseteq> vertices (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. f `` insert x F \<subseteq> vertices (S i)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
f `` {} \<subseteq> vertices (chain_sup S)

goal (2 subgoals):
 1. f `` {} \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` {} \<subseteq> vertices (S i)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; f `` F \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` F \<subseteq> vertices (S i); f `` insert x F \<subseteq> vertices (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. f `` insert x F \<subseteq> vertices (S i)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
f `` {} \<subseteq> vertices (chain_sup S)

goal (1 subgoal):
 1. \<exists>i. f `` {} \<subseteq> vertices (S i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i. f `` {} \<subseteq> vertices (S i)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; f `` F \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` F \<subseteq> vertices (S i); f `` insert x F \<subseteq> vertices (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. f `` insert x F \<subseteq> vertices (S i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; f `` F \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` F \<subseteq> vertices (S i); f `` insert x F \<subseteq> vertices (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. f `` insert x F \<subseteq> vertices (S i)
[PROOF STEP]
case (insert v V)
[PROOF STATE]
proof (state)
this:
finite V
v \<notin> V
f `` V \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` V \<subseteq> vertices (S i)
f `` insert v V \<subseteq> vertices (chain_sup S)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; f `` F \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` F \<subseteq> vertices (S i); f `` insert x F \<subseteq> vertices (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. f `` insert x F \<subseteq> vertices (S i)
[PROOF STEP]
from insert.prems
[PROOF STATE]
proof (chain)
picking this:
f `` insert v V \<subseteq> vertices (chain_sup S)
[PROOF STEP]
have V:"f `` V \<subseteq> vertices (chain_sup S)"
    and v:"f `` {v} \<subseteq> vertices (chain_sup S)"
[PROOF STATE]
proof (prove)
using this:
f `` insert v V \<subseteq> vertices (chain_sup S)

goal (1 subgoal):
 1. f `` V \<subseteq> vertices (chain_sup S) &&& f `` {v} \<subseteq> vertices (chain_sup S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f `` V \<subseteq> vertices (chain_sup S)
f `` {v} \<subseteq> vertices (chain_sup S)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; f `` F \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` F \<subseteq> vertices (S i); f `` insert x F \<subseteq> vertices (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. f `` insert x F \<subseteq> vertices (S i)
[PROOF STEP]
from insert.hyps(3)[OF V]
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. f `` V \<subseteq> vertices (S i)
[PROOF STEP]
obtain i where i:"f `` V \<subseteq> vertices (S i)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. f `` V \<subseteq> vertices (S i)

goal (1 subgoal):
 1. (\<And>i. f `` V \<subseteq> vertices (S i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f `` V \<subseteq> vertices (S i)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; f `` F \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` F \<subseteq> vertices (S i); f `` insert x F \<subseteq> vertices (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. f `` insert x F \<subseteq> vertices (S i)
[PROOF STEP]
have "\<exists> j. f `` {v} \<subseteq> vertices (S j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. f `` {v} \<subseteq> vertices (S j)
[PROOF STEP]
proof(cases "(f `` {v}) = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f `` {v} = {} \<Longrightarrow> \<exists>j. f `` {v} \<subseteq> vertices (S j)
 2. f `` {v} \<noteq> {} \<Longrightarrow> \<exists>j. f `` {v} \<subseteq> vertices (S j)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
f `` {v} \<noteq> {}

goal (2 subgoals):
 1. f `` {v} = {} \<Longrightarrow> \<exists>j. f `` {v} \<subseteq> vertices (S j)
 2. f `` {v} \<noteq> {} \<Longrightarrow> \<exists>j. f `` {v} \<subseteq> vertices (S j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f `` {v} \<noteq> {}
[PROOF STEP]
obtain v' where f:"(v,v') \<in> f"
[PROOF STATE]
proof (prove)
using this:
f `` {v} \<noteq> {}

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

goal (2 subgoals):
 1. f `` {v} = {} \<Longrightarrow> \<exists>j. f `` {v} \<subseteq> vertices (S j)
 2. f `` {v} \<noteq> {} \<Longrightarrow> \<exists>j. f `` {v} \<subseteq> vertices (S j)
[PROOF STEP]
hence "v' \<in> vertices (chain_sup S)"
[PROOF STATE]
proof (prove)
using this:
(v, v') \<in> f

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

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

goal (2 subgoals):
 1. f `` {v} = {} \<Longrightarrow> \<exists>j. f `` {v} \<subseteq> vertices (S j)
 2. f `` {v} \<noteq> {} \<Longrightarrow> \<exists>j. f `` {v} \<subseteq> vertices (S j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v' \<in> vertices (chain_sup S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v' \<in> vertices (chain_sup S)

goal (1 subgoal):
 1. \<exists>j. f `` {v} \<subseteq> vertices (S j)
[PROOF STEP]
using assms(3) f
[PROOF STATE]
proof (prove)
using this:
v' \<in> vertices (chain_sup S)
univalent f
(v, v') \<in> f

goal (1 subgoal):
 1. \<exists>j. f `` {v} \<subseteq> vertices (S j)
[PROOF STEP]
unfolding chain_sup_def
[PROOF STATE]
proof (prove)
using this:
v' \<in> vertices (LG (\<Union>i. edges (S i)) (\<Union>i. vertices (S i)))
univalent f
(v, v') \<in> f

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

goal (1 subgoal):
 1. f `` {v} = {} \<Longrightarrow> \<exists>j. f `` {v} \<subseteq> vertices (S j)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<exists>j. f `` {v} \<subseteq> vertices (S j)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; f `` F \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` F \<subseteq> vertices (S i); f `` insert x F \<subseteq> vertices (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. f `` insert x F \<subseteq> vertices (S i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. f `` {v} \<subseteq> vertices (S j)
[PROOF STEP]
obtain j where j:"f `` {v} \<subseteq> vertices (S j)"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. f `` {v} \<subseteq> vertices (S j)

goal (1 subgoal):
 1. (\<And>j. f `` {v} \<subseteq> vertices (S j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f `` {v} \<subseteq> vertices (S j)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; f `` F \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` F \<subseteq> vertices (S i); f `` insert x F \<subseteq> vertices (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. f `` insert x F \<subseteq> vertices (S i)
[PROOF STEP]
have sg:"subgraph (S i) (S (max i j))" "subgraph (S j) (S (max i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph (S i) (S (max i j)) &&& subgraph (S j) (S (max i j))
[PROOF STEP]
by(rule chain[OF assms(1)],force)+
[PROOF STATE]
proof (state)
this:
subgraph (S i) (S (max i j))
subgraph (S j) (S (max i j))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; f `` F \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` F \<subseteq> vertices (S i); f `` insert x F \<subseteq> vertices (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. f `` insert x F \<subseteq> vertices (S i)
[PROOF STEP]
have V:"(f \<inter> V \<times> UNIV) `` V \<subseteq> vertices (S (max i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<inter> V \<times> UNIV) `` V \<subseteq> vertices (S (max i j))
[PROOF STEP]
using i subgraph_subset[OF sg(1)]
[PROOF STATE]
proof (prove)
using this:
f `` V \<subseteq> vertices (S i)
vertices (S i) \<subseteq> vertices (S (max i j))
edges (restrict (S i)) \<subseteq> edges (S (max i j))

goal (1 subgoal):
 1. (f \<inter> V \<times> UNIV) `` V \<subseteq> vertices (S (max i j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f \<inter> V \<times> UNIV) `` V \<subseteq> vertices (S (max i j))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; f `` F \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` F \<subseteq> vertices (S i); f `` insert x F \<subseteq> vertices (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. f `` insert x F \<subseteq> vertices (S i)
[PROOF STEP]
have v:"f `` {v} \<subseteq> vertices (S (max i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f `` {v} \<subseteq> vertices (S (max i j))
[PROOF STEP]
using j subgraph_subset[OF sg(2)]
[PROOF STATE]
proof (prove)
using this:
f `` {v} \<subseteq> vertices (S j)
vertices (S j) \<subseteq> vertices (S (max i j))
edges (restrict (S j)) \<subseteq> edges (S (max i j))

goal (1 subgoal):
 1. f `` {v} \<subseteq> vertices (S (max i j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f `` {v} \<subseteq> vertices (S (max i j))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; f `` F \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` F \<subseteq> vertices (S i); f `` insert x F \<subseteq> vertices (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. f `` insert x F \<subseteq> vertices (S i)
[PROOF STEP]
have "f `` insert v V \<subseteq> vertices (S (max i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f `` insert v V \<subseteq> vertices (S (max i j))
[PROOF STEP]
using v V
[PROOF STATE]
proof (prove)
using this:
f `` {v} \<subseteq> vertices (S (max i j))
(f \<inter> V \<times> UNIV) `` V \<subseteq> vertices (S (max i j))

goal (1 subgoal):
 1. f `` insert v V \<subseteq> vertices (S (max i j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f `` insert v V \<subseteq> vertices (S (max i j))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; f `` F \<subseteq> vertices (chain_sup S) \<Longrightarrow> \<exists>i. f `` F \<subseteq> vertices (S i); f `` insert x F \<subseteq> vertices (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. f `` insert x F \<subseteq> vertices (S i)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
f `` insert v V \<subseteq> vertices (S (max i j))

goal (1 subgoal):
 1. \<exists>i. f `` insert v V \<subseteq> vertices (S i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i. f `` insert v V \<subseteq> vertices (S i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_graph_occurence_edges:
  assumes "chain S" "finite E" "univalent f"
        "on_triple f `` E \<subseteq> edges (chain_sup S)"
      shows "\<exists> i. on_triple f `` E \<subseteq> edges (S i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. on_triple f `` E \<subseteq> edges (S i)
[PROOF STEP]
using assms(2,4)
[PROOF STATE]
proof (prove)
using this:
finite E
on_triple f `` E \<subseteq> edges (chain_sup S)

goal (1 subgoal):
 1. \<exists>i. on_triple f `` E \<subseteq> edges (S i)
[PROOF STEP]
proof(induct E)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. on_triple f `` {} \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` {} \<subseteq> edges (S i)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
on_triple f `` {} \<subseteq> edges (chain_sup S)

goal (2 subgoals):
 1. on_triple f `` {} \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` {} \<subseteq> edges (S i)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
on_triple f `` {} \<subseteq> edges (chain_sup S)

goal (1 subgoal):
 1. \<exists>i. on_triple f `` {} \<subseteq> edges (S i)
[PROOF STEP]
unfolding graph_homomorphism_def
[PROOF STATE]
proof (prove)
using this:
on_triple f `` {} \<subseteq> edges (chain_sup S)

goal (1 subgoal):
 1. \<exists>i. on_triple f `` {} \<subseteq> edges (S i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i. on_triple f `` {} \<subseteq> edges (S i)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
case (insert e E)
[PROOF STATE]
proof (state)
this:
finite E
e \<notin> E
on_triple f `` E \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` E \<subseteq> edges (S i)
on_triple f `` insert e E \<subseteq> edges (chain_sup S)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
have univ:"univalent (on_triple f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. univalent (on_triple f)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
univalent f

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

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
have [simp]:"restrict (S i) = S i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict (S i) = S i
[PROOF STEP]
using chain[OF assms(1),unfolded subgraph_def,of i i]
[PROOF STATE]
proof (prove)
using this:
i \<le> i \<Longrightarrow> graph (S i) \<and> graph (S i) \<and> graph_union (S i) (S i) = S i

goal (1 subgoal):
 1. restrict (S i) = S i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
restrict (S ?i1) = S ?i1

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
from insert.prems
[PROOF STATE]
proof (chain)
picking this:
on_triple f `` insert e E \<subseteq> edges (chain_sup S)
[PROOF STEP]
have E:"on_triple f `` E \<subseteq> edges (chain_sup S)"
    and e:"on_triple f `` {e} \<subseteq> edges (chain_sup S)"
[PROOF STATE]
proof (prove)
using this:
on_triple f `` insert e E \<subseteq> edges (chain_sup S)

goal (1 subgoal):
 1. on_triple f `` E \<subseteq> edges (chain_sup S) &&& on_triple f `` {e} \<subseteq> edges (chain_sup S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
on_triple f `` E \<subseteq> edges (chain_sup S)
on_triple f `` {e} \<subseteq> edges (chain_sup S)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
with insert.hyps
[PROOF STATE]
proof (chain)
picking this:
finite E
e \<notin> E
on_triple f `` E \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` E \<subseteq> edges (S i)
on_triple f `` E \<subseteq> edges (chain_sup S)
on_triple f `` {e} \<subseteq> edges (chain_sup S)
[PROOF STEP]
obtain i where i:"on_triple f `` E \<subseteq> edges (S i)"
[PROOF STATE]
proof (prove)
using this:
finite E
e \<notin> E
on_triple f `` E \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` E \<subseteq> edges (S i)
on_triple f `` E \<subseteq> edges (chain_sup S)
on_triple f `` {e} \<subseteq> edges (chain_sup S)

goal (1 subgoal):
 1. (\<And>i. on_triple f `` E \<subseteq> edges (S i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
on_triple f `` E \<subseteq> edges (S i)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
have "\<exists> j. on_triple f `` {e} \<subseteq> edges (S j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. on_triple f `` {e} \<subseteq> edges (S j)
[PROOF STEP]
proof(cases "on_triple f `` {e} = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. on_triple f `` {e} = {} \<Longrightarrow> \<exists>j. on_triple f `` {e} \<subseteq> edges (S j)
 2. on_triple f `` {e} \<noteq> {} \<Longrightarrow> \<exists>j. on_triple f `` {e} \<subseteq> edges (S j)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
on_triple f `` {e} \<noteq> {}

goal (2 subgoals):
 1. on_triple f `` {e} = {} \<Longrightarrow> \<exists>j. on_triple f `` {e} \<subseteq> edges (S j)
 2. on_triple f `` {e} \<noteq> {} \<Longrightarrow> \<exists>j. on_triple f `` {e} \<subseteq> edges (S j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
on_triple f `` {e} \<noteq> {}
[PROOF STEP]
obtain e' where f:"(e,e') \<in> on_triple f"
[PROOF STATE]
proof (prove)
using this:
on_triple f `` {e} \<noteq> {}

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

goal (2 subgoals):
 1. on_triple f `` {e} = {} \<Longrightarrow> \<exists>j. on_triple f `` {e} \<subseteq> edges (S j)
 2. on_triple f `` {e} \<noteq> {} \<Longrightarrow> \<exists>j. on_triple f `` {e} \<subseteq> edges (S j)
[PROOF STEP]
hence "e' \<in> edges (chain_sup S)"
[PROOF STATE]
proof (prove)
using this:
(e, e') \<in> on_triple f

goal (1 subgoal):
 1. e' \<in> edges (chain_sup S)
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
(e, e') \<in> on_triple f
on_triple f `` {e} \<subseteq> edges (chain_sup S)

goal (1 subgoal):
 1. e' \<in> edges (chain_sup S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e' \<in> edges (chain_sup S)

goal (2 subgoals):
 1. on_triple f `` {e} = {} \<Longrightarrow> \<exists>j. on_triple f `` {e} \<subseteq> edges (S j)
 2. on_triple f `` {e} \<noteq> {} \<Longrightarrow> \<exists>j. on_triple f `` {e} \<subseteq> edges (S j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e' \<in> edges (chain_sup S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e' \<in> edges (chain_sup S)

goal (1 subgoal):
 1. \<exists>j. on_triple f `` {e} \<subseteq> edges (S j)
[PROOF STEP]
using univ f
[PROOF STATE]
proof (prove)
using this:
e' \<in> edges (chain_sup S)
univalent (on_triple f)
(e, e') \<in> on_triple f

goal (1 subgoal):
 1. \<exists>j. on_triple f `` {e} \<subseteq> edges (S j)
[PROOF STEP]
unfolding chain_sup_def
[PROOF STATE]
proof (prove)
using this:
e' \<in> edges (LG (\<Union>i. edges (S i)) (\<Union>i. vertices (S i)))
univalent (on_triple f)
(e, e') \<in> on_triple f

goal (1 subgoal):
 1. \<exists>j. on_triple f `` {e} \<subseteq> edges (S j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j. on_triple f `` {e} \<subseteq> edges (S j)

goal (1 subgoal):
 1. on_triple f `` {e} = {} \<Longrightarrow> \<exists>j. on_triple f `` {e} \<subseteq> edges (S j)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<exists>j. on_triple f `` {e} \<subseteq> edges (S j)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. on_triple f `` {e} \<subseteq> edges (S j)
[PROOF STEP]
obtain j where j:"on_triple f `` {e} \<subseteq> edges (S j)"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. on_triple f `` {e} \<subseteq> edges (S j)

goal (1 subgoal):
 1. (\<And>j. on_triple f `` {e} \<subseteq> edges (S j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
on_triple f `` {e} \<subseteq> edges (S j)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
have sg:"subgraph (S i) (S (max i j))" "subgraph (S j) (S (max i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph (S i) (S (max i j)) &&& subgraph (S j) (S (max i j))
[PROOF STEP]
by(rule chain[OF assms(1)],force)+
[PROOF STATE]
proof (state)
this:
subgraph (S i) (S (max i j))
subgraph (S j) (S (max i j))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
have E:"on_triple f `` E \<subseteq> edges (S (max i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. on_triple f `` E \<subseteq> edges (S (max i j))
[PROOF STEP]
using i subgraph_subset[OF sg(1)]
[PROOF STATE]
proof (prove)
using this:
on_triple f `` E \<subseteq> edges (S i)
vertices (S i) \<subseteq> vertices (S (max i j))
edges (restrict (S i)) \<subseteq> edges (S (max i j))

goal (1 subgoal):
 1. on_triple f `` E \<subseteq> edges (S (max i j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
on_triple f `` E \<subseteq> edges (S (max i j))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
have e:"on_triple f `` {e} \<subseteq> edges (S (max i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. on_triple f `` {e} \<subseteq> edges (S (max i j))
[PROOF STEP]
using j subgraph_subset[OF sg(2)]
[PROOF STATE]
proof (prove)
using this:
on_triple f `` {e} \<subseteq> edges (S j)
vertices (S j) \<subseteq> vertices (S (max i j))
edges (restrict (S j)) \<subseteq> edges (S (max i j))

goal (1 subgoal):
 1. on_triple f `` {e} \<subseteq> edges (S (max i j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
on_triple f `` {e} \<subseteq> edges (S (max i j))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
have "on_triple f `` insert e E \<subseteq> edges (S (max i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. on_triple f `` insert e E \<subseteq> edges (S (max i j))
[PROOF STEP]
using e E
[PROOF STATE]
proof (prove)
using this:
on_triple f `` {e} \<subseteq> edges (S (max i j))
on_triple f `` E \<subseteq> edges (S (max i j))

goal (1 subgoal):
 1. on_triple f `` insert e E \<subseteq> edges (S (max i j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
on_triple f `` insert e E \<subseteq> edges (S (max i j))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; on_triple f `` F \<subseteq> edges (chain_sup S) \<Longrightarrow> \<exists>i. on_triple f `` F \<subseteq> edges (S i); on_triple f `` insert x F \<subseteq> edges (chain_sup S)\<rbrakk> \<Longrightarrow> \<exists>i. on_triple f `` insert x F \<subseteq> edges (S i)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
on_triple f `` insert e E \<subseteq> edges (S (max i j))

goal (1 subgoal):
 1. \<exists>i. on_triple f `` insert e E \<subseteq> edges (S i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i. on_triple f `` insert e E \<subseteq> edges (S i)

goal:
No subgoals!
[PROOF STEP]
qed