equivI has replaced equiv.intro
authorhaftmann
Mon Nov 29 13:44:54 2010 +0100 (2010-11-29)
changeset 408156e2d17cc0d1d
parent 40814 fa64f6278568
child 40816 19c492929756
equivI has replaced equiv.intro
NEWS
src/HOL/Algebra/Coset.thy
src/HOL/Equiv_Relations.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/NSA/StarDef.thy
src/HOL/Rat.thy
src/HOL/RealDef.thy
     1.1 --- a/NEWS	Mon Nov 29 12:15:14 2010 +0100
     1.2 +++ b/NEWS	Mon Nov 29 13:44:54 2010 +0100
     1.3 @@ -89,6 +89,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Abandoned locale equiv for equivalence relations.  INCOMPATIBILITY: use
     1.8 +equivI rather than equiv_intro.
     1.9 +
    1.10  * Code generator: globbing constant expressions "*" and "Theory.*" have been
    1.11  replaced by the more idiomatic "_" and "Theory._".  INCOMPATIBILITY.
    1.12  
     2.1 --- a/src/HOL/Algebra/Coset.thy	Mon Nov 29 12:15:14 2010 +0100
     2.2 +++ b/src/HOL/Algebra/Coset.thy	Mon Nov 29 13:44:54 2010 +0100
     2.3 @@ -606,7 +606,7 @@
     2.4  proof -
     2.5    interpret group G by fact
     2.6    show ?thesis
     2.7 -  proof (intro equiv.intro)
     2.8 +  proof (intro equivI)
     2.9      show "refl_on (carrier G) (rcong H)"
    2.10        by (auto simp add: r_congruent_def refl_on_def) 
    2.11    next
     3.1 --- a/src/HOL/Equiv_Relations.thy	Mon Nov 29 12:15:14 2010 +0100
     3.2 +++ b/src/HOL/Equiv_Relations.thy	Mon Nov 29 13:44:54 2010 +0100
     3.3 @@ -13,6 +13,15 @@
     3.4  definition equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where
     3.5    "equiv A r \<longleftrightarrow> refl_on A r \<and> sym r \<and> trans r"
     3.6  
     3.7 +lemma equivI:
     3.8 +  "refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> equiv A r"
     3.9 +  by (simp add: equiv_def)
    3.10 +
    3.11 +lemma equivE:
    3.12 +  assumes "equiv A r"
    3.13 +  obtains "refl_on A r" and "sym r" and "trans r"
    3.14 +  using assms by (simp add: equiv_def)
    3.15 +
    3.16  text {*
    3.17    Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O
    3.18    r = r"}.
     4.1 --- a/src/HOL/Library/Fraction_Field.thy	Mon Nov 29 12:15:14 2010 +0100
     4.2 +++ b/src/HOL/Library/Fraction_Field.thy	Mon Nov 29 13:44:54 2010 +0100
     4.3 @@ -43,7 +43,7 @@
     4.4  qed
     4.5    
     4.6  lemma equiv_fractrel: "equiv {x. snd x \<noteq> 0} fractrel"
     4.7 -  by (rule equiv.intro [OF refl_fractrel sym_fractrel trans_fractrel])
     4.8 +  by (rule equivI [OF refl_fractrel sym_fractrel trans_fractrel])
     4.9  
    4.10  lemmas UN_fractrel = UN_equiv_class [OF equiv_fractrel]
    4.11  lemmas UN_fractrel2 = UN_equiv_class2 [OF equiv_fractrel equiv_fractrel]
     5.1 --- a/src/HOL/NSA/StarDef.thy	Mon Nov 29 12:15:14 2010 +0100
     5.2 +++ b/src/HOL/NSA/StarDef.thy	Mon Nov 29 13:44:54 2010 +0100
     5.3 @@ -62,7 +62,7 @@
     5.4  by (simp add: starrel_def)
     5.5  
     5.6  lemma equiv_starrel: "equiv UNIV starrel"
     5.7 -proof (rule equiv.intro)
     5.8 +proof (rule equivI)
     5.9    show "refl starrel" by (simp add: refl_on_def)
    5.10    show "sym starrel" by (simp add: sym_def eq_commute)
    5.11    show "trans starrel" by (auto intro: transI elim!: ultra)
     6.1 --- a/src/HOL/Rat.thy	Mon Nov 29 12:15:14 2010 +0100
     6.2 +++ b/src/HOL/Rat.thy	Mon Nov 29 13:44:54 2010 +0100
     6.3 @@ -44,7 +44,7 @@
     6.4  qed
     6.5    
     6.6  lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel"
     6.7 -  by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel])
     6.8 +  by (rule equivI [OF refl_on_ratrel sym_ratrel trans_ratrel])
     6.9  
    6.10  lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel]
    6.11  lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel]
     7.1 --- a/src/HOL/RealDef.thy	Mon Nov 29 12:15:14 2010 +0100
     7.2 +++ b/src/HOL/RealDef.thy	Mon Nov 29 13:44:54 2010 +0100
     7.3 @@ -324,7 +324,7 @@
     7.4  
     7.5  lemma equiv_realrel: "equiv {X. cauchy X} realrel"
     7.6    using refl_realrel sym_realrel trans_realrel
     7.7 -  by (rule equiv.intro)
     7.8 +  by (rule equivI)
     7.9  
    7.10  subsection {* The field of real numbers *}
    7.11