src/HOL/Relation.thy
changeset 60057 86fa63ce8156
parent 59518 28cfc60dea7a
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Relation.thy	Mon Apr 13 13:03:41 2015 +0200
     1.2 +++ b/src/HOL/Relation.thy	Tue Apr 14 11:32:01 2015 +0200
     1.3 @@ -216,6 +216,8 @@
     1.4    "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)"
     1.5    by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
     1.6  
     1.7 +lemma reflp_equality [simp]: "reflp op ="
     1.8 +by(simp add: reflp_def)
     1.9  
    1.10  subsubsection {* Irreflexivity *}
    1.11  
    1.12 @@ -357,6 +359,8 @@
    1.13  lemma antisym_empty [simp]: "antisym {}"
    1.14    by (unfold antisym_def) blast
    1.15  
    1.16 +lemma antisymP_equality [simp]: "antisymP op ="
    1.17 +by(auto intro: antisymI)
    1.18  
    1.19  subsubsection {* Transitivity *}
    1.20