src/HOL/Relation.thy
changeset 13639 8ee6ea6627e1
parent 13550 5a176b8dda84
child 13812 91713a1915ee
     1.1 --- a/src/HOL/Relation.thy	Thu Oct 10 14:21:49 2002 +0200
     1.2 +++ b/src/HOL/Relation.thy	Thu Oct 10 14:23:19 2002 +0200
     1.3 @@ -20,9 +20,6 @@
     1.4    rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
     1.5    "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
     1.6  
     1.7 -  fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
     1.8 -  "fun_rel_comp f R == {g. ALL x. (f x, g x) : R}"
     1.9 -
    1.10    Image :: "[('a * 'b) set, 'a set] => 'b set"                (infixl "``" 90)
    1.11    "r `` s == {y. EX x:s. (x,y):r}"
    1.12  
    1.13 @@ -141,20 +138,6 @@
    1.14    by blast
    1.15  
    1.16  
    1.17 -subsection {* Composition of function and relation *}
    1.18 -
    1.19 -lemma fun_rel_comp_mono: "A \<subseteq> B ==> fun_rel_comp f A \<subseteq> fun_rel_comp f B"
    1.20 -  by (unfold fun_rel_comp_def) fast
    1.21 -
    1.22 -lemma fun_rel_comp_unique:
    1.23 -  "ALL x. EX! y. (f x, y) : R ==> EX! g. g : fun_rel_comp f R"
    1.24 -  apply (unfold fun_rel_comp_def)
    1.25 -  apply (rule_tac a = "%x. THE y. (f x, y) : R" in ex1I)
    1.26 -  apply (fast dest!: theI')
    1.27 -  apply (fast intro: ext the1_equality [symmetric])
    1.28 -  done
    1.29 -
    1.30 -
    1.31  subsection {* Reflexivity *}
    1.32  
    1.33  lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"