src/HOL/Relation.thy
changeset 11136 e34e7f6d9b57
parent 10832 e33b47e4246d
child 12487 bbd564190c9b
     1.1 --- a/src/HOL/Relation.thy	Thu Feb 15 16:00:38 2001 +0100
     1.2 +++ b/src/HOL/Relation.thy	Thu Feb 15 16:00:40 2001 +0100
     1.3 @@ -13,47 +13,50 @@
     1.4    converse :: "('a * 'b) set => ('b * 'a) set"    ("(_\\<inverse>)" [1000] 999)
     1.5  
     1.6  constdefs
     1.7 -  comp  :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set"  (infixr "O" 60)
     1.8 +  comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
     1.9      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
    1.10  
    1.11 -  Image :: "[('a*'b) set,'a set] => 'b set"                (infixl "``" 90)
    1.12 +  Image :: "[('a * 'b) set, 'a set] => 'b set"                (infixl "``" 90)
    1.13      "r `` s == {y. ? x:s. (x,y):r}"
    1.14  
    1.15 -  Id    :: "('a * 'a)set"                            (*the identity relation*)
    1.16 +  Id    :: "('a * 'a) set"                            (*the identity relation*)
    1.17      "Id == {p. ? x. p = (x,x)}"
    1.18  
    1.19 -  diag  :: "'a set => ('a * 'a)set"          (*diagonal: identity over a set*)
    1.20 +  diag  :: "'a set => ('a * 'a) set"          (*diagonal: identity over a set*)
    1.21      "diag(A) == UN x:A. {(x,x)}"
    1.22    
    1.23 -  Domain :: "('a*'b) set => 'a set"
    1.24 +  Domain :: "('a * 'b) set => 'a set"
    1.25      "Domain(r) == {x. ? y. (x,y):r}"
    1.26  
    1.27 -  Range  :: "('a*'b) set => 'b set"
    1.28 +  Range  :: "('a * 'b) set => 'b set"
    1.29      "Range(r) == Domain(r^-1)"
    1.30  
    1.31 -  Field :: "('a*'a)set=>'a set"
    1.32 +  Field :: "('a * 'a) set => 'a set"
    1.33      "Field r == Domain r Un Range r"
    1.34  
    1.35 -  refl   :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*)
    1.36 +  refl   :: "['a set, ('a * 'a) set] => bool" (*reflexivity over a set*)
    1.37      "refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)"
    1.38  
    1.39 -  sym    :: "('a*'a) set=>bool"             (*symmetry predicate*)
    1.40 +  sym    :: "('a * 'a) set => bool"             (*symmetry predicate*)
    1.41      "sym(r) == ALL x y. (x,y): r --> (y,x): r"
    1.42  
    1.43 -  antisym:: "('a * 'a)set => bool"          (*antisymmetry predicate*)
    1.44 +  antisym:: "('a * 'a) set => bool"          (*antisymmetry predicate*)
    1.45      "antisym(r) == ALL x y. (x,y):r --> (y,x):r --> x=y"
    1.46  
    1.47 -  trans  :: "('a * 'a)set => bool"          (*transitivity predicate*)
    1.48 +  trans  :: "('a * 'a) set => bool"          (*transitivity predicate*)
    1.49      "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
    1.50  
    1.51 -  single_valued :: "('a * 'b)set => bool"
    1.52 +  single_valued :: "('a * 'b) set => bool"
    1.53      "single_valued r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
    1.54  
    1.55    fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
    1.56      "fun_rel_comp f R == {g. !x. (f x, g x) : R}"
    1.57  
    1.58 +  inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set"
    1.59 +    "inv_image r f == {(x,y). (f(x), f(y)) : r}"
    1.60 +
    1.61  syntax
    1.62 -  reflexive :: "('a * 'a)set => bool"       (*reflexivity over a type*)
    1.63 +  reflexive :: "('a * 'a) set => bool"       (*reflexivity over a type*)
    1.64  translations
    1.65    "reflexive" == "refl UNIV"
    1.66