adding a definition for refl_on which is friendly for quickcheck and nitpick
authorbulwahn
Tue Dec 07 13:33:28 2010 +0100 (2010-12-07)
changeset 41056dcec9bc71ee9
parent 41055 d6f45159ae84
child 41065 13424972ade4
adding a definition for refl_on which is friendly for quickcheck and nitpick
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Tue Dec 07 12:10:13 2010 +0100
     1.2 +++ b/src/HOL/Relation.thy	Tue Dec 07 13:33:28 2010 +0100
     1.3 @@ -227,6 +227,9 @@
     1.4  lemma refl_on_Id_on: "refl_on A (Id_on A)"
     1.5  by (rule refl_onI [OF Id_on_subset_Times Id_onI])
     1.6  
     1.7 +lemma refl_on_def'[nitpick_def, code]:
     1.8 +  "refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))"
     1.9 +by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
    1.10  
    1.11  subsection {* Antisymmetry *}
    1.12