src/HOL/Relation.thy
 changeset 21404 eb85850d3eb7 parent 21210 c17fd2df4e9e child 22172 e7d6cb237b5e
```     1.1 --- a/src/HOL/Relation.thy	Fri Nov 17 02:19:55 2006 +0100
1.2 +++ b/src/HOL/Relation.thy	Fri Nov 17 02:20:03 2006 +0100
1.3 @@ -13,54 +13,69 @@
1.4  subsection {* Definitions *}
1.5
1.6  definition
1.7 -  converse :: "('a * 'b) set => ('b * 'a) set"    ("(_^-1)" [1000] 999)
1.8 +  converse :: "('a * 'b) set => ('b * 'a) set"
1.9 +    ("(_^-1)" [1000] 999) where
1.10    "r^-1 == {(y, x). (x, y) : r}"
1.11
1.12  notation (xsymbols)
1.13    converse  ("(_\<inverse>)" [1000] 999)
1.14
1.15  definition
1.16 -  rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 75)
1.17 +  rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"
1.18 +    (infixr "O" 75) where
1.19    "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
1.20
1.21 -  Image :: "[('a * 'b) set, 'a set] => 'b set"                (infixl "``" 90)
1.22 +definition
1.23 +  Image :: "[('a * 'b) set, 'a set] => 'b set"
1.24 +    (infixl "``" 90) where
1.25    "r `` s == {y. EX x:s. (x,y):r}"
1.26
1.27 -  Id    :: "('a * 'a) set"  -- {* the identity relation *}
1.28 +definition
1.29 +  Id :: "('a * 'a) set" where -- {* the identity relation *}
1.30    "Id == {p. EX x. p = (x,x)}"
1.31
1.32 -  diag  :: "'a set => ('a * 'a) set"  -- {* diagonal: identity over a set *}
1.33 +definition
1.34 +  diag  :: "'a set => ('a * 'a) set" where -- {* diagonal: identity over a set *}
1.35    "diag A == \<Union>x\<in>A. {(x,x)}"
1.36
1.37 -  Domain :: "('a * 'b) set => 'a set"
1.38 +definition
1.39 +  Domain :: "('a * 'b) set => 'a set" where
1.40    "Domain r == {x. EX y. (x,y):r}"
1.41
1.42 -  Range  :: "('a * 'b) set => 'b set"
1.43 +definition
1.44 +  Range  :: "('a * 'b) set => 'b set" where
1.45    "Range r == Domain(r^-1)"
1.46
1.47 -  Field :: "('a * 'a) set => 'a set"
1.48 +definition
1.49 +  Field :: "('a * 'a) set => 'a set" where
1.50    "Field r == Domain r \<union> Range r"
1.51
1.52 -  refl   :: "['a set, ('a * 'a) set] => bool"  -- {* reflexivity over a set *}
1.53 +definition
1.54 +  refl :: "['a set, ('a * 'a) set] => bool" where -- {* reflexivity over a set *}
1.55    "refl A r == r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
1.56
1.57 -  sym    :: "('a * 'a) set => bool"  -- {* symmetry predicate *}
1.58 +definition
1.59 +  sym :: "('a * 'a) set => bool" where -- {* symmetry predicate *}
1.60    "sym r == ALL x y. (x,y): r --> (y,x): r"
1.61
1.62 -  antisym:: "('a * 'a) set => bool"  -- {* antisymmetry predicate *}
1.63 +definition
1.64 +  antisym :: "('a * 'a) set => bool" where -- {* antisymmetry predicate *}
1.65    "antisym r == ALL x y. (x,y):r --> (y,x):r --> x=y"
1.66
1.67 -  trans  :: "('a * 'a) set => bool"  -- {* transitivity predicate *}
1.68 +definition
1.69 +  trans :: "('a * 'a) set => bool" where -- {* transitivity predicate *}
1.70    "trans r == (ALL x y z. (x,y):r --> (y,z):r --> (x,z):r)"
1.71
1.72 -  single_valued :: "('a * 'b) set => bool"
1.73 +definition
1.74 +  single_valued :: "('a * 'b) set => bool" where
1.75    "single_valued r == ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z)"
1.76
1.77 -  inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set"
1.78 +definition
1.79 +  inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" where
1.80    "inv_image r f == {(x, y). (f x, f y) : r}"
1.81
1.82  abbreviation
1.83 -  reflexive :: "('a * 'a) set => bool"  -- {* reflexivity over a type *}
1.84 +  reflexive :: "('a * 'a) set => bool" where -- {* reflexivity over a type *}
1.85    "reflexive == refl UNIV"
1.86
1.87
```