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"
```