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