--- a/src/HOL/Equiv_Relations.thy Sat Jul 18 21:44:18 2015 +0200
+++ b/src/HOL/Equiv_Relations.thy Sat Jul 18 22:58:50 2015 +0200
@@ -2,13 +2,13 @@
Copyright 1996 University of Cambridge
*)
-section {* Equivalence Relations in Higher-Order Set Theory *}
+section \<open>Equivalence Relations in Higher-Order Set Theory\<close>
theory Equiv_Relations
imports Groups_Big Relation
begin
-subsection {* Equivalence relations -- set version *}
+subsection \<open>Equivalence relations -- set version\<close>
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"
@@ -22,12 +22,12 @@
obtains "refl_on A r" and "sym r" and "trans r"
using assms by (simp add: equiv_def)
-text {*
+text \<open>
Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O
r = r"}.
First half: @{text "equiv A r ==> r\<inverse> O r = r"}.
-*}
+\<close>
lemma sym_trans_comp_subset:
"sym r ==> trans r ==> r\<inverse> O r \<subseteq> r"
@@ -43,7 +43,7 @@
apply (iprover intro: sym_trans_comp_subset refl_on_comp_subset)+
done
-text {* Second half. *}
+text \<open>Second half.\<close>
lemma comp_equivI:
"r\<inverse> O r = r ==> Domain r = A ==> equiv A r"
@@ -55,11 +55,11 @@
done
-subsection {* Equivalence classes *}
+subsection \<open>Equivalence classes\<close>
lemma equiv_class_subset:
"equiv A r ==> (a, b) \<in> r ==> r``{a} \<subseteq> r``{b}"
- -- {* lemma for the next result *}
+ -- \<open>lemma for the next result\<close>
by (unfold equiv_def trans_def sym_def) blast
theorem equiv_class_eq: "equiv A r ==> (a, b) \<in> r ==> r``{a} = r``{b}"
@@ -73,7 +73,7 @@
lemma subset_equiv_class:
"equiv A r ==> r``{b} \<subseteq> r``{a} ==> b \<in> A ==> (a,b) \<in> r"
- -- {* lemma for the next result *}
+ -- \<open>lemma for the next result\<close>
by (unfold equiv_def refl_on_def) blast
lemma eq_equiv_class:
@@ -96,10 +96,10 @@
by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
-subsection {* Quotients *}
+subsection \<open>Quotients\<close>
definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set" (infixl "'/'/" 90) where
- "A//r = (\<Union>x \<in> A. {r``{x}})" -- {* set of equiv classes *}
+ "A//r = (\<Union>x \<in> A. {r``{x}})" -- \<open>set of equiv classes\<close>
lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
by (unfold quotient_def) blast
@@ -160,7 +160,7 @@
apply blast
done
-subsection {* Refinement of one equivalence relation WRT another *}
+subsection \<open>Refinement of one equivalence relation WRT another\<close>
lemma refines_equiv_class_eq:
"\<lbrakk>R \<subseteq> S; equiv A R; equiv A S\<rbrakk> \<Longrightarrow> R``(S``{a}) = S``{a}"
@@ -187,9 +187,9 @@
done
-subsection {* Defining unary operations upon equivalence classes *}
+subsection \<open>Defining unary operations upon equivalence classes\<close>
-text{*A congruence-preserving function*}
+text\<open>A congruence-preserving function\<close>
definition congruent :: "('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
"congruent r f \<longleftrightarrow> (\<forall>(y, z) \<in> r. f y = f z)"
@@ -209,13 +209,13 @@
lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
- -- {* lemma required to prove @{text UN_equiv_class} *}
+ -- \<open>lemma required to prove @{text UN_equiv_class}\<close>
by auto
lemma UN_equiv_class:
"equiv A r ==> f respects r ==> a \<in> A
==> (\<Union>x \<in> r``{a}. f x) = f a"
- -- {* Conversion rule *}
+ -- \<open>Conversion rule\<close>
apply (rule equiv_class_self [THEN UN_constant_eq], assumption+)
apply (unfold equiv_def congruent_def sym_def)
apply (blast del: equalityI)
@@ -230,11 +230,11 @@
apply auto
done
-text {*
+text \<open>
Sufficient conditions for injectiveness. Could weaken premises!
major premise could be an inclusion; bcong could be @{text "!!y. y \<in>
A ==> f y \<in> B"}.
-*}
+\<close>
lemma UN_equiv_class_inject:
"equiv A r ==> f respects r ==>
@@ -252,9 +252,9 @@
done
-subsection {* Defining binary operations upon equivalence classes *}
+subsection \<open>Defining binary operations upon equivalence classes\<close>
-text{*A congruence-preserving function of two arguments*}
+text\<open>A congruence-preserving function of two arguments\<close>
definition congruent2 :: "('a \<times> 'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
"congruent2 r1 r2 f \<longleftrightarrow> (\<forall>(y1, z1) \<in> r1. \<forall>(y2, z2) \<in> r2. f y1 y2 = f z1 z2)"
@@ -268,7 +268,7 @@
"congruent2 r1 r2 f \<Longrightarrow> (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
using assms by (auto simp add: congruent2_def)
-text{*Abbreviation for the common case where the relations are identical*}
+text\<open>Abbreviation for the common case where the relations are identical\<close>
abbreviation
RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool"
(infixr "respects2" 80) where
@@ -310,8 +310,8 @@
lemma UN_UN_split_split_eq:
"(\<Union>(x1, x2) \<in> X. \<Union>(y1, y2) \<in> Y. A x1 x2 y1 y2) =
(\<Union>x \<in> X. \<Union>y \<in> Y. (\<lambda>(x1, x2). (\<lambda>(y1, y2). A x1 x2 y1 y2) y) x)"
- -- {* Allows a natural expression of binary operators, *}
- -- {* without explicit calls to @{text split} *}
+ -- \<open>Allows a natural expression of binary operators,\<close>
+ -- \<open>without explicit calls to @{text split}\<close>
by auto
lemma congruent2I:
@@ -319,8 +319,8 @@
==> (!!y z w. w \<in> A2 ==> (y,z) \<in> r1 ==> f y w = f z w)
==> (!!y z w. w \<in> A1 ==> (y,z) \<in> r2 ==> f w y = f w z)
==> congruent2 r1 r2 f"
- -- {* Suggested by John Harrison -- the two subproofs may be *}
- -- {* \emph{much} simpler than the direct proof. *}
+ -- \<open>Suggested by John Harrison -- the two subproofs may be\<close>
+ -- \<open>\emph{much} simpler than the direct proof.\<close>
apply (unfold congruent2_def equiv_def refl_on_def)
apply clarify
apply (blast intro: trans)
@@ -340,12 +340,12 @@
done
-subsection {* Quotients and finiteness *}
+subsection \<open>Quotients and finiteness\<close>
-text {*Suggested by Florian Kammüller*}
+text \<open>Suggested by Florian Kammüller\<close>
lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
- -- {* recall @{thm equiv_type} *}
+ -- \<open>recall @{thm equiv_type}\<close>
apply (rule finite_subset)
apply (erule_tac [2] finite_Pow_iff [THEN iffD2])
apply (unfold quotient_def)
@@ -381,7 +381,7 @@
done
-subsection {* Projection *}
+subsection \<open>Projection\<close>
definition proj where "proj r x = r `` {x}"
@@ -429,13 +429,13 @@
using assms in_quotient_imp_in_rel equiv_type by fastforce
-subsection {* Equivalence relations -- predicate version *}
+subsection \<open>Equivalence relations -- predicate version\<close>
-text {* Partial equivalences *}
+text \<open>Partial equivalences\<close>
definition part_equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
"part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> (\<forall>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y)"
- -- {* John-Harrison-style characterization *}
+ -- \<open>John-Harrison-style characterization\<close>
lemma part_equivpI:
"(\<exists>x. R x x) \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> part_equivp R"
@@ -481,10 +481,10 @@
by (auto elim: part_equivpE)
-text {* Total equivalences *}
+text \<open>Total equivalences\<close>
definition equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
- "equivp R \<longleftrightarrow> (\<forall>x y. R x y = (R x = R y))" -- {* John-Harrison-style characterization *}
+ "equivp R \<longleftrightarrow> (\<forall>x y. R x y = (R x = R y))" -- \<open>John-Harrison-style characterization\<close>
lemma equivpI:
"reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R"