author paulson Fri, 02 Apr 2004 17:06:15 +0200 changeset 14512 e516d7cfa249 parent 14511 73493236e97f child 14513 81d32b739a2b
variable renamings and other cosmetic changes
 src/HOL/Integ/Equiv.thy file | annotate | diff | comparison | revisions
--- a/src/HOL/Integ/Equiv.thy	Fri Apr 02 16:21:57 2004 +0200
+++ b/src/HOL/Integ/Equiv.thy	Fri Apr 02 17:06:15 2004 +0200
@@ -87,7 +87,7 @@
"equiv A r ==> ((x, y) \<in> r) = (r{x} = r{y} & x \<in> A & y \<in> A)"
by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)

-corollary eq_equiv_class_iff:
+theorem eq_equiv_class_iff:
"equiv A r ==> x \<in> A ==> y \<in> A ==> (r{x} = r{y}) = ((x, y) \<in> r)"
by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)

@@ -137,16 +137,16 @@
subsection {* Defining unary operations upon equivalence classes *}

locale congruent =
-  fixes r and b
-  assumes congruent: "(y, z) \<in> r ==> b y = b z"
+  fixes r and f
+  assumes congruent: "(y, z) \<in> r ==> f y = f z"

-lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. b y = c ==> (\<Union>y \<in> A. b(y))=c"
+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} *}
by auto

lemma UN_equiv_class:
-  "equiv A r ==> congruent r b ==> a \<in> A
-    ==> (\<Union>x \<in> r{a}. b x) = b a"
+  "equiv A r ==> congruent r f ==> a \<in> A
+    ==> (\<Union>x \<in> r{a}. f x) = f a"
-- {* Conversion rule *}
apply (rule equiv_class_self [THEN UN_constant_eq], assumption+)
apply (unfold equiv_def congruent_def sym_def)
@@ -154,8 +154,8 @@
done

lemma UN_equiv_class_type:
-  "equiv A r ==> congruent r b ==> X \<in> A//r ==>
-    (!!x. x \<in> A ==> b x : B) ==> (\<Union>x \<in> X. b x) : B"
+  "equiv A r ==> congruent r f ==> X \<in> A//r ==>
+    (!!x. x \<in> A ==> f x \<in> B) ==> (\<Union>x \<in> X. f x) \<in> B"
apply (unfold quotient_def)
apply clarify
apply (subst UN_equiv_class)
@@ -165,19 +165,19 @@
text {*
Sufficient conditions for injectiveness.  Could weaken premises!
major premise could be an inclusion; bcong could be @{text "!!y. y \<in>
-  A ==> b y \<in> B"}.
+  A ==> f y \<in> B"}.
*}

lemma UN_equiv_class_inject:
-  "equiv A r ==> congruent r b ==>
-    (\<Union>x \<in> X. b x) = (\<Union>y \<in> Y. b y) ==> X \<in> A//r ==> Y \<in> A//r
-    ==> (!!x y. x \<in> A ==> y \<in> A ==> b x = b y ==> (x, y) \<in> r)
+  "equiv A r ==> congruent r f ==>
+    (\<Union>x \<in> X. f x) = (\<Union>y \<in> Y. f y) ==> X \<in> A//r ==> Y \<in> A//r
+    ==> (!!x y. x \<in> A ==> y \<in> A ==> f x = f y ==> (x, y) \<in> r)
==> X = Y"
apply (unfold quotient_def)
apply clarify
apply (rule equiv_class_eq)
apply assumption
-  apply (subgoal_tac "b x = b xa")
+  apply (subgoal_tac "f x = f xa")
apply blast
apply (erule box_equals)
apply (assumption | rule UN_equiv_class)+
@@ -187,17 +187,17 @@
subsection {* Defining binary operations upon equivalence classes *}

locale congruent2 =
-  fixes r and b
+  fixes r and f
assumes congruent2:
-    "(y1, z1) \<in> r ==> (y2, z2) \<in> r ==> b y1 y2 = b z1 z2"
+    "(y1, z1) \<in> r ==> (y2, z2) \<in> r ==> f y1 y2 = f z1 z2"

lemma congruent2_implies_congruent:
-    "equiv A r ==> congruent2 r b ==> a \<in> A ==> congruent r (b a)"
+    "equiv A r ==> congruent2 r f ==> a \<in> A ==> congruent r (f a)"
by (unfold congruent_def congruent2_def equiv_def refl_def) blast

lemma congruent2_implies_congruent_UN:
-  "equiv A r ==> congruent2 r b ==> a \<in> A ==>
-    congruent r (\<lambda>x1. \<Union>x2 \<in> r{a}. b x1 x2)"
+  "equiv A r ==> congruent2 r f ==> a \<in> A ==>
+    congruent r (\<lambda>x1. \<Union>x2 \<in> r{a}. f x1 x2)"
apply (unfold congruent_def)
apply clarify
apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+)
@@ -207,15 +207,15 @@
done

lemma UN_equiv_class2:
-  "equiv A r ==> congruent2 r b ==> a1 \<in> A ==> a2 \<in> A
-    ==> (\<Union>x1 \<in> r{a1}. \<Union>x2 \<in> r{a2}. b x1 x2) = b a1 a2"
+  "equiv A r ==> congruent2 r f ==> a1 \<in> A ==> a2 \<in> A
+    ==> (\<Union>x1 \<in> r{a1}. \<Union>x2 \<in> r{a2}. f x1 x2) = f a1 a2"
congruent2_implies_congruent_UN)

lemma UN_equiv_class_type2:
-  "equiv A r ==> congruent2 r b ==> X1 \<in> A//r ==> X2 \<in> A//r
-    ==> (!!x1 x2. x1 \<in> A ==> x2 \<in> A ==> b x1 x2 \<in> B)
-    ==> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. b x1 x2) \<in> B"
+  "equiv A r ==> congruent2 r f ==> X1 \<in> A//r ==> X2 \<in> A//r
+    ==> (!!x1 x2. x1 \<in> A ==> x2 \<in> A ==> f x1 x2 \<in> B)
+    ==> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. f x1 x2) \<in> B"
apply (unfold quotient_def)
apply clarify
apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN
@@ -231,9 +231,9 @@

lemma congruent2I:
"equiv A r
-    ==> (!!y z w. w \<in> A ==> (y, z) \<in> r ==> b y w = b z w)
-    ==> (!!y z w. w \<in> A ==> (y, z) \<in> r ==> b w y = b w z)
-    ==> congruent2 r b"
+    ==> (!!y z w. w \<in> A ==> (y, z) \<in> r ==> f y w = f z w)
+    ==> (!!y z w. w \<in> A ==> (y, z) \<in> r ==> f w y = f w z)
+    ==> congruent2 r f"
-- {* Suggested by John Harrison -- the two subproofs may be *}
-- {* \emph{much} simpler than the direct proof. *}
apply (unfold congruent2_def equiv_def refl_def)
@@ -243,9 +243,9 @@

lemma congruent2_commuteI:
assumes equivA: "equiv A r"
-    and commute: "!!y z. y \<in> A ==> z \<in> A ==> b y z = b z y"
-    and congt: "!!y z w. w \<in> A ==> (y, z) \<in> r ==> b w y = b w z"
-  shows "congruent2 r b"
+    and commute: "!!y z. y \<in> A ==> z \<in> A ==> f y z = f z y"
+    and congt: "!!y z w. w \<in> A ==> (y, z) \<in> r ==> f w y = f w z"
+  shows "congruent2 r f"
apply (rule equivA [THEN congruent2I])
apply (rule commute [THEN trans])
apply (rule_tac [3] commute [THEN trans, symmetric])
@@ -287,9 +287,6 @@

ML
{*
-
-(* legacy ML bindings *)
-
val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
val UN_constant_eq = thm "UN_constant_eq";
val UN_equiv_class = thm "UN_equiv_class";