author haftmann Mon Nov 29 13:44:54 2010 +0100 (2010-11-29) changeset 40815 6e2d17cc0d1d parent 40814 fa64f6278568 child 40816 19c492929756
equivI has replaced equiv.intro
 NEWS file | annotate | diff | revisions src/HOL/Algebra/Coset.thy file | annotate | diff | revisions src/HOL/Equiv_Relations.thy file | annotate | diff | revisions src/HOL/Library/Fraction_Field.thy file | annotate | diff | revisions src/HOL/NSA/StarDef.thy file | annotate | diff | revisions src/HOL/Rat.thy file | annotate | diff | revisions src/HOL/RealDef.thy file | annotate | diff | revisions
```     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.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
```