--- a/src/HOL/Library/Graphs.thy Tue Jun 19 00:02:16 2007 +0200
+++ b/src/HOL/Library/Graphs.thy Tue Jun 19 18:00:49 2007 +0200
@@ -3,7 +3,7 @@
Author: Alexander Krauss, TU Muenchen
*)
-header "" (* FIXME proper header *)
+header {* General Graphs as Sets *}
theory Graphs
imports Main SCT_Misc Kleene_Algebras ExecutableSet
@@ -215,7 +215,6 @@
unfolding graph_pow_def by simp_all
qed
-
lemma graph_leqI:
assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'"
shows "G \<le> H"
@@ -223,7 +222,6 @@
unfolding graph_leq_def has_edge_def
by auto
-
lemma in_graph_plusE:
assumes "has_edge (G + H) n e n'"
assumes "has_edge G n e n' \<Longrightarrow> P"
@@ -232,6 +230,13 @@
using assms
by (auto simp: in_grplus)
+lemma in_graph_compE:
+ assumes GH: "has_edge (G * H) n e n'"
+ obtains e1 k e2
+ where "has_edge G n e1 k" "has_edge H k e2 n'" "e = e1 * e2"
+ using GH
+ by (auto simp: in_grcomp)
+
lemma
assumes "x \<in> S k"
shows "x \<in> (\<Union>k. S k)"