# HG changeset patch
# User nipkow
# Date 1205768844 -3600
# Node ID 74012d599204b0a4943d9cb3e45eb70e5f832921
# Parent  988a103afbab8f6ec8077b4021a63bfd9d644fd2
added lemmas

diff -r 988a103afbab -r 74012d599204 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Mar 17 16:13:05 2008 +0100
+++ b/src/HOL/Relation.thy	Mon Mar 17 16:47:24 2008 +0100
@@ -54,6 +54,10 @@
   refl :: "['a set, ('a * 'a) set] => bool" where -- {* reflexivity over a set *}
   "refl A r == r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
 
+abbreviation
+  reflexive :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
+  "reflexive == refl UNIV"
+
 definition
   sym :: "('a * 'a) set => bool" where -- {* symmetry predicate *}
   "sym r == ALL x y. (x,y): r --> (y,x): r"
@@ -74,10 +78,6 @@
   inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" where
   "inv_image r f == {(x, y). (f x, f y) : r}"
 
-abbreviation
-  reflexive :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
-  "reflexive == refl UNIV"
-
 
 subsection {* The identity relation *}
 
@@ -195,6 +195,9 @@
   "ALL x:S. refl (A x) (r x) \<Longrightarrow> refl (UNION S A) (UNION S r)"
 by (unfold refl_def) blast
 
+lemma refl_empty[simp]: "refl {} {}"
+by(simp add:refl_def)
+
 lemma refl_diag: "refl A (diag A)"
 by (rule reflI [OF diag_subset_Times diagI])