src/HOL/Relation.thy
changeset 41056 dcec9bc71ee9
parent 40923 be80c93ac0a2
child 41792 ff3cb0c418b7
equal deleted inserted replaced
41055:d6f45159ae84 41056:dcec9bc71ee9
   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"