author nipkow Mon, 17 Mar 2008 16:47:24 +0100 changeset 26297 74012d599204 parent 26296 988a103afbab child 26298 53e382ccf71f
 src/HOL/Relation.thy file | annotate | diff | comparison | revisions
```--- 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 {} {}"