equal
deleted
inserted
replaced
225 by(simp add:refl_on_def) |
225 by(simp add:refl_on_def) |
226 |
226 |
227 lemma refl_on_Id_on: "refl_on A (Id_on A)" |
227 lemma refl_on_Id_on: "refl_on A (Id_on A)" |
228 by (rule refl_onI [OF Id_on_subset_Times Id_onI]) |
228 by (rule refl_onI [OF Id_on_subset_Times Id_onI]) |
229 |
229 |
|
230 lemma refl_on_def'[nitpick_def, code]: |
|
231 "refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))" |
|
232 by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2) |
230 |
233 |
231 subsection {* Antisymmetry *} |
234 subsection {* Antisymmetry *} |
232 |
235 |
233 lemma antisymI: |
236 lemma antisymI: |
234 "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r" |
237 "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r" |