src/HOL/Equiv_Relations.thy
changeset 40815 6e2d17cc0d1d
parent 40812 ff16e22e8776
child 40816 19c492929756
     1.1 --- a/src/HOL/Equiv_Relations.thy	Mon Nov 29 12:15:14 2010 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Mon Nov 29 13:44:54 2010 +0100
     1.3 @@ -13,6 +13,15 @@
     1.4  definition equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where
     1.5    "equiv A r \<longleftrightarrow> refl_on A r \<and> sym r \<and> trans r"
     1.6  
     1.7 +lemma equivI:
     1.8 +  "refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> equiv A r"
     1.9 +  by (simp add: equiv_def)
    1.10 +
    1.11 +lemma equivE:
    1.12 +  assumes "equiv A r"
    1.13 +  obtains "refl_on A r" and "sym r" and "trans r"
    1.14 +  using assms by (simp add: equiv_def)
    1.15 +
    1.16  text {*
    1.17    Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O
    1.18    r = r"}.