# HG changeset patch
# User paulson
# Date 1169655050 -3600
# Node ID e7d6cb237b5eb0d3410fc204f68db71e42ed1645
# Parent  58f554f51f0d163284af0defdc279e23e601f470
some new lemmas

diff -r 58f554f51f0d -r e7d6cb237b5e src/HOL/Relation.thy
--- 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 *}
 
diff -r 58f554f51f0d -r e7d6cb237b5e src/HOL/Set.thy
--- 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 *}
 
diff -r 58f554f51f0d -r e7d6cb237b5e src/HOL/Transitive_Closure.thy
--- 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"