--- a/src/HOL/Relation.thy Thu Oct 10 14:21:49 2002 +0200
+++ b/src/HOL/Relation.thy Thu Oct 10 14:23:19 2002 +0200
@@ -20,9 +20,6 @@
rel_comp :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set" (infixr "O" 60)
"r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
- fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
- "fun_rel_comp f R == {g. ALL x. (f x, g x) : R}"
-
Image :: "[('a * 'b) set, 'a set] => 'b set" (infixl "``" 90)
"r `` s == {y. EX x:s. (x,y):r}"
@@ -141,20 +138,6 @@
by blast
-subsection {* Composition of function and relation *}
-
-lemma fun_rel_comp_mono: "A \<subseteq> B ==> fun_rel_comp f A \<subseteq> fun_rel_comp f B"
- by (unfold fun_rel_comp_def) fast
-
-lemma fun_rel_comp_unique:
- "ALL x. EX! y. (f x, y) : R ==> EX! g. g : fun_rel_comp f R"
- apply (unfold fun_rel_comp_def)
- apply (rule_tac a = "%x. THE y. (f x, y) : R" in ex1I)
- apply (fast dest!: theI')
- apply (fast intro: ext the1_equality [symmetric])
- done
-
-
subsection {* Reflexivity *}
lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"