--- a/NEWS Mon Nov 29 12:15:14 2010 +0100
+++ b/NEWS Mon Nov 29 13:44:54 2010 +0100
@@ -89,6 +89,9 @@
*** HOL ***
+* Abandoned locale equiv for equivalence relations. INCOMPATIBILITY: use
+equivI rather than equiv_intro.
+
* Code generator: globbing constant expressions "*" and "Theory.*" have been
replaced by the more idiomatic "_" and "Theory._". INCOMPATIBILITY.
--- a/src/HOL/Algebra/Coset.thy Mon Nov 29 12:15:14 2010 +0100
+++ b/src/HOL/Algebra/Coset.thy Mon Nov 29 13:44:54 2010 +0100
@@ -606,7 +606,7 @@
proof -
interpret group G by fact
show ?thesis
- proof (intro equiv.intro)
+ proof (intro equivI)
show "refl_on (carrier G) (rcong H)"
by (auto simp add: r_congruent_def refl_on_def)
next
--- a/src/HOL/Equiv_Relations.thy Mon Nov 29 12:15:14 2010 +0100
+++ b/src/HOL/Equiv_Relations.thy Mon Nov 29 13:44:54 2010 +0100
@@ -13,6 +13,15 @@
definition equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where
"equiv A r \<longleftrightarrow> refl_on A r \<and> sym r \<and> trans r"
+lemma equivI:
+ "refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> equiv A r"
+ by (simp add: equiv_def)
+
+lemma equivE:
+ assumes "equiv A r"
+ obtains "refl_on A r" and "sym r" and "trans r"
+ using assms by (simp add: equiv_def)
+
text {*
Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O
r = r"}.
--- a/src/HOL/Library/Fraction_Field.thy Mon Nov 29 12:15:14 2010 +0100
+++ b/src/HOL/Library/Fraction_Field.thy Mon Nov 29 13:44:54 2010 +0100
@@ -43,7 +43,7 @@
qed
lemma equiv_fractrel: "equiv {x. snd x \<noteq> 0} fractrel"
- by (rule equiv.intro [OF refl_fractrel sym_fractrel trans_fractrel])
+ by (rule equivI [OF refl_fractrel sym_fractrel trans_fractrel])
lemmas UN_fractrel = UN_equiv_class [OF equiv_fractrel]
lemmas UN_fractrel2 = UN_equiv_class2 [OF equiv_fractrel equiv_fractrel]
--- a/src/HOL/NSA/StarDef.thy Mon Nov 29 12:15:14 2010 +0100
+++ b/src/HOL/NSA/StarDef.thy Mon Nov 29 13:44:54 2010 +0100
@@ -62,7 +62,7 @@
by (simp add: starrel_def)
lemma equiv_starrel: "equiv UNIV starrel"
-proof (rule equiv.intro)
+proof (rule equivI)
show "refl starrel" by (simp add: refl_on_def)
show "sym starrel" by (simp add: sym_def eq_commute)
show "trans starrel" by (auto intro: transI elim!: ultra)
--- a/src/HOL/Rat.thy Mon Nov 29 12:15:14 2010 +0100
+++ b/src/HOL/Rat.thy Mon Nov 29 13:44:54 2010 +0100
@@ -44,7 +44,7 @@
qed
lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel"
- by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel])
+ by (rule equivI [OF refl_on_ratrel sym_ratrel trans_ratrel])
lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel]
lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel]
--- a/src/HOL/RealDef.thy Mon Nov 29 12:15:14 2010 +0100
+++ b/src/HOL/RealDef.thy Mon Nov 29 13:44:54 2010 +0100
@@ -324,7 +324,7 @@
lemma equiv_realrel: "equiv {X. cauchy X} realrel"
using refl_realrel sym_realrel trans_realrel
- by (rule equiv.intro)
+ by (rule equivI)
subsection {* The field of real numbers *}