src/HOL/Equiv_Relations.thy
changeset 60517 f16e4fb20652
parent 59528 4862f3dc9540
child 60688 01488b559910
     1.1 --- a/src/HOL/Equiv_Relations.thy	Fri Jun 19 07:53:33 2015 +0200
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Fri Jun 19 07:53:35 2015 +0200
     1.3 @@ -523,6 +523,20 @@
     1.4    "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
     1.5    by (erule equivpE, erule transpE)
     1.6  
     1.7 +
     1.8 +subsection \<open>Prominent examples\<close>
     1.9 +
    1.10 +lemma equivp_associated:
    1.11 +  "equivp associated"
    1.12 +proof (rule equivpI)
    1.13 +  show "reflp associated"
    1.14 +    by (rule reflpI) simp
    1.15 +  show "symp associated"
    1.16 +    by (rule sympI) (simp add: associated_sym)
    1.17 +  show "transp associated"
    1.18 +    by (rule transpI) (fact associated_trans)
    1.19 +qed
    1.20 +
    1.21  hide_const (open) proj
    1.22  
    1.23  end