equal
deleted
inserted
replaced
144 lemma R_O_Id [simp]: "R O Id = R" |
144 lemma R_O_Id [simp]: "R O Id = R" |
145 by fast |
145 by fast |
146 |
146 |
147 lemma Id_O_R [simp]: "Id O R = R" |
147 lemma Id_O_R [simp]: "Id O R = R" |
148 by fast |
148 by fast |
|
149 |
|
150 lemma rel_comp_empty1[simp]: "{} O R = {}" |
|
151 by blast |
|
152 |
|
153 lemma rel_comp_empty2[simp]: "R O {} = {}" |
|
154 by blast |
149 |
155 |
150 lemma O_assoc: "(R O S) O T = R O (S O T)" |
156 lemma O_assoc: "(R O S) O T = R O (S O T)" |
151 by blast |
157 by blast |
152 |
158 |
153 lemma trans_O_subset: "trans r ==> r O r \<subseteq> r" |
159 lemma trans_O_subset: "trans r ==> r O r \<subseteq> r" |