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