Removed obsolete function "fun_rel_comp".
authorberghofe
Thu Oct 10 14:23:19 2002 +0200 (2002-10-10)
changeset 136398ee6ea6627e1
parent 13638 2b234b079245
child 13640 993576f4de30
Removed obsolete function "fun_rel_comp".
src/HOL/Relation.ML
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.ML	Thu Oct 10 14:21:49 2002 +0200
     1.2 +++ b/src/HOL/Relation.ML	Thu Oct 10 14:23:19 2002 +0200
     1.3 @@ -73,9 +73,6 @@
     1.4  val diag_eqI = thm "diag_eqI";
     1.5  val diag_iff = thm "diag_iff";
     1.6  val diag_subset_Times = thm "diag_subset_Times";
     1.7 -val fun_rel_comp_def = thm "fun_rel_comp_def";
     1.8 -val fun_rel_comp_mono = thm "fun_rel_comp_mono";
     1.9 -val fun_rel_comp_unique = thm "fun_rel_comp_unique";
    1.10  val inv_image_def = thm "inv_image_def";
    1.11  val pair_in_Id_conv = thm "pair_in_Id_conv";
    1.12  val reflD = thm "reflD";
     2.1 --- a/src/HOL/Relation.thy	Thu Oct 10 14:21:49 2002 +0200
     2.2 +++ b/src/HOL/Relation.thy	Thu Oct 10 14:23:19 2002 +0200
     2.3 @@ -20,9 +20,6 @@
     2.4    rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
     2.5    "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
     2.6  
     2.7 -  fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
     2.8 -  "fun_rel_comp f R == {g. ALL x. (f x, g x) : R}"
     2.9 -
    2.10    Image :: "[('a * 'b) set, 'a set] => 'b set"                (infixl "``" 90)
    2.11    "r `` s == {y. EX x:s. (x,y):r}"
    2.12  
    2.13 @@ -141,20 +138,6 @@
    2.14    by blast
    2.15  
    2.16  
    2.17 -subsection {* Composition of function and relation *}
    2.18 -
    2.19 -lemma fun_rel_comp_mono: "A \<subseteq> B ==> fun_rel_comp f A \<subseteq> fun_rel_comp f B"
    2.20 -  by (unfold fun_rel_comp_def) fast
    2.21 -
    2.22 -lemma fun_rel_comp_unique:
    2.23 -  "ALL x. EX! y. (f x, y) : R ==> EX! g. g : fun_rel_comp f R"
    2.24 -  apply (unfold fun_rel_comp_def)
    2.25 -  apply (rule_tac a = "%x. THE y. (f x, y) : R" in ex1I)
    2.26 -  apply (fast dest!: theI')
    2.27 -  apply (fast intro: ext the1_equality [symmetric])
    2.28 -  done
    2.29 -
    2.30 -
    2.31  subsection {* Reflexivity *}
    2.32  
    2.33  lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"