src/HOL/Relation.thy
changeset 32235 8f9b8d14fc9f
parent 31011 506e57123cd1
child 32463 3a0a65ca2261
     1.1 --- a/src/HOL/Relation.thy	Mon Jul 27 17:36:30 2009 +0200
     1.2 +++ b/src/HOL/Relation.thy	Mon Jul 27 21:47:41 2009 +0200
     1.3 @@ -21,9 +21,9 @@
     1.4    converse  ("(_\<inverse>)" [1000] 999)
     1.5  
     1.6  definition
     1.7 -  rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"
     1.8 +  rel_comp  :: "[('a * 'b) set, ('b * 'c) set] => ('a * 'c) set"
     1.9      (infixr "O" 75) where
    1.10 -  "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
    1.11 +  "r O s == {(x,z). EX y. (x, y) : r & (y, z) : s}"
    1.12  
    1.13  definition
    1.14    Image :: "[('a * 'b) set, 'a set] => 'b set"
    1.15 @@ -140,15 +140,15 @@
    1.16  subsection {* Composition of two relations *}
    1.17  
    1.18  lemma rel_compI [intro]:
    1.19 -  "(a, b) : s ==> (b, c) : r ==> (a, c) : r O s"
    1.20 +  "(a, b) : r ==> (b, c) : s ==> (a, c) : r O s"
    1.21  by (unfold rel_comp_def) blast
    1.22  
    1.23  lemma rel_compE [elim!]: "xz : r O s ==>
    1.24 -  (!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r  ==> P) ==> P"
    1.25 +  (!!x y z. xz = (x, z) ==> (x, y) : r ==> (y, z) : s  ==> P) ==> P"
    1.26  by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE)
    1.27  
    1.28  lemma rel_compEpair:
    1.29 -  "(a, c) : r O s ==> (!!y. (a, y) : s ==> (y, c) : r ==> P) ==> P"
    1.30 +  "(a, c) : r O s ==> (!!y. (a, y) : r ==> (y, c) : s ==> P) ==> P"
    1.31  by (iprover elim: rel_compE Pair_inject ssubst)
    1.32  
    1.33  lemma R_O_Id [simp]: "R O Id = R"
    1.34 @@ -173,7 +173,7 @@
    1.35  by blast
    1.36  
    1.37  lemma rel_comp_subset_Sigma:
    1.38 -    "s \<subseteq> A \<times> B ==> r \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
    1.39 +    "r \<subseteq> A \<times> B ==> s \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
    1.40  by blast
    1.41  
    1.42  lemma rel_comp_distrib[simp]: "R O (S \<union> T) = (R O S) \<union> (R O T)"