--- a/src/HOL/Relation.thy Wed Jan 24 13:15:16 2007 +0100
+++ b/src/HOL/Relation.thy Wed Jan 24 17:10:50 2007 +0100
@@ -356,6 +356,11 @@
lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s"
by blast
+lemma fst_eq_Domain: "fst ` R = Domain R";
+ apply auto
+ apply (rule image_eqI, auto)
+ done
+
subsection {* Range *}
@@ -392,6 +397,11 @@
lemma Range_Union: "Range (Union S) = (\<Union>A\<in>S. Range A)"
by blast
+lemma snd_eq_Range: "snd ` R = Range R";
+ apply auto
+ apply (rule image_eqI, auto)
+ done
+
subsection {* Image of a set under a relation *}
--- a/src/HOL/Set.thy Wed Jan 24 13:15:16 2007 +0100
+++ b/src/HOL/Set.thy Wed Jan 24 17:10:50 2007 +0100
@@ -1422,6 +1422,9 @@
lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
by blast
+lemma Diff_Int2: "A \<inter> C - B \<inter> C = A \<inter> C - B"
+ by blast
+
text {* \medskip Set complement *}
--- a/src/HOL/Transitive_Closure.thy Wed Jan 24 13:15:16 2007 +0100
+++ b/src/HOL/Transitive_Closure.thy Wed Jan 24 17:10:50 2007 +0100
@@ -259,6 +259,10 @@
thus ?thesis by iprover
qed
+lemmas trancl_induct2 =
+ trancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
+ consumes 1, case_names base step]
+
lemma trancl_trans_induct:
assumes major: "(x,y) : r^+"
and cases: "!!x y. (x,y) : r ==> P x y"