equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Graphs.thy |
1 (* Title: HOL/Library/Graphs.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Alexander Krauss, TU Muenchen |
3 Author: Alexander Krauss, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header "" (* FIXME proper header *) |
6 header {* General Graphs as Sets *} |
7 |
7 |
8 theory Graphs |
8 theory Graphs |
9 imports Main SCT_Misc Kleene_Algebras ExecutableSet |
9 imports Main SCT_Misc Kleene_Algebras ExecutableSet |
10 begin |
10 begin |
11 |
11 |
213 |
213 |
214 show "a ^ 0 = 1" "\<And>n. a ^ (Suc n) = a * a ^ n" |
214 show "a ^ 0 = 1" "\<And>n. a ^ (Suc n) = a * a ^ n" |
215 unfolding graph_pow_def by simp_all |
215 unfolding graph_pow_def by simp_all |
216 qed |
216 qed |
217 |
217 |
218 |
|
219 lemma graph_leqI: |
218 lemma graph_leqI: |
220 assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'" |
219 assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'" |
221 shows "G \<le> H" |
220 shows "G \<le> H" |
222 using assms |
221 using assms |
223 unfolding graph_leq_def has_edge_def |
222 unfolding graph_leq_def has_edge_def |
224 by auto |
223 by auto |
225 |
|
226 |
224 |
227 lemma in_graph_plusE: |
225 lemma in_graph_plusE: |
228 assumes "has_edge (G + H) n e n'" |
226 assumes "has_edge (G + H) n e n'" |
229 assumes "has_edge G n e n' \<Longrightarrow> P" |
227 assumes "has_edge G n e n' \<Longrightarrow> P" |
230 assumes "has_edge H n e n' \<Longrightarrow> P" |
228 assumes "has_edge H n e n' \<Longrightarrow> P" |
231 shows P |
229 shows P |
232 using assms |
230 using assms |
233 by (auto simp: in_grplus) |
231 by (auto simp: in_grplus) |
|
232 |
|
233 lemma in_graph_compE: |
|
234 assumes GH: "has_edge (G * H) n e n'" |
|
235 obtains e1 k e2 |
|
236 where "has_edge G n e1 k" "has_edge H k e2 n'" "e = e1 * e2" |
|
237 using GH |
|
238 by (auto simp: in_grcomp) |
234 |
239 |
235 lemma |
240 lemma |
236 assumes "x \<in> S k" |
241 assumes "x \<in> S k" |
237 shows "x \<in> (\<Union>k. S k)" |
242 shows "x \<in> (\<Union>k. S k)" |
238 using assms by blast |
243 using assms by blast |