converted to Isar script
authorpaulson
Sat Sep 21 21:10:34 2002 +0200 (2002-09-21)
changeset 13574f9796358e66f
parent 13573 37b22343c35a
child 13575 ecb6ecd9af13
converted to Isar script
src/ZF/Integ/EquivClass.ML
src/ZF/Integ/EquivClass.thy
src/ZF/IsaMakefile
     1.1 --- a/src/ZF/Integ/EquivClass.ML	Fri Sep 20 11:49:38 2002 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,246 +0,0 @@
     1.4 -(*  Title:      ZF/EquivClass.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1994  University of Cambridge
     1.8 -
     1.9 -Equivalence relations in Zermelo-Fraenkel Set Theory 
    1.10 -*)
    1.11 -
    1.12 -(*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***)
    1.13 -
    1.14 -(** first half: equiv(A,r) ==> converse(r) O r = r **)
    1.15 -
    1.16 -Goalw [trans_def,sym_def]
    1.17 -    "[| sym(r); trans(r) |] ==> converse(r) O r <= r";
    1.18 -by (Blast_tac 1);
    1.19 -qed "sym_trans_comp_subset";
    1.20 -
    1.21 -Goalw [refl_def]
    1.22 -    "[| refl(A,r); r <= A*A |] ==> r <= converse(r) O r";
    1.23 -by (Blast_tac 1);
    1.24 -qed "refl_comp_subset";
    1.25 -
    1.26 -Goalw [equiv_def]
    1.27 -    "equiv(A,r) ==> converse(r) O r = r";
    1.28 -by (blast_tac (subset_cs addSIs [sym_trans_comp_subset, refl_comp_subset]) 1);
    1.29 -qed "equiv_comp_eq";
    1.30 -
    1.31 -(*second half*)
    1.32 -Goalw [equiv_def,refl_def,sym_def,trans_def]
    1.33 -    "[| converse(r) O r = r;  domain(r) = A |] ==> equiv(A,r)";
    1.34 -by (etac equalityE 1);
    1.35 -by (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r" 1);
    1.36 -by (ALLGOALS Fast_tac);
    1.37 -qed "comp_equivI";
    1.38 -
    1.39 -(** Equivalence classes **)
    1.40 -
    1.41 -(*Lemma for the next result*)
    1.42 -Goalw [trans_def,sym_def]
    1.43 -    "[| sym(r);  trans(r);  <a,b>: r |] ==> r``{a} <= r``{b}";
    1.44 -by (Blast_tac 1);
    1.45 -qed "equiv_class_subset";
    1.46 -
    1.47 -Goalw [equiv_def]
    1.48 -    "[| equiv(A,r);  <a,b>: r |] ==> r``{a} = r``{b}";
    1.49 -by (safe_tac (subset_cs addSIs [equalityI, equiv_class_subset]));
    1.50 -by (rewtac sym_def);
    1.51 -by (Blast_tac 1);
    1.52 -qed "equiv_class_eq";
    1.53 -
    1.54 -Goalw [equiv_def,refl_def]
    1.55 -    "[| equiv(A,r);  a: A |] ==> a: r``{a}";
    1.56 -by (Blast_tac 1);
    1.57 -qed "equiv_class_self";
    1.58 -
    1.59 -(*Lemma for the next result*)
    1.60 -Goalw [equiv_def,refl_def]
    1.61 -    "[| equiv(A,r);  r``{b} <= r``{a};  b: A |] ==> <a,b>: r";
    1.62 -by (Blast_tac 1);
    1.63 -qed "subset_equiv_class";
    1.64 -
    1.65 -Goal "[| r``{a} = r``{b};  equiv(A,r);  b: A |] ==> <a,b>: r";
    1.66 -by (REPEAT (ares_tac[equalityD2, subset_equiv_class] 1));
    1.67 -qed "eq_equiv_class";
    1.68 -
    1.69 -(*thus r``{a} = r``{b} as well*)
    1.70 -Goalw [equiv_def,trans_def,sym_def]
    1.71 -    "[| equiv(A,r);  x: (r``{a} Int r``{b}) |] ==> <a,b>: r";
    1.72 -by (Blast_tac 1);
    1.73 -qed "equiv_class_nondisjoint";
    1.74 -
    1.75 -Goalw [equiv_def] "equiv(A,r) ==> r <= A*A";
    1.76 -by (safe_tac subset_cs);
    1.77 -qed "equiv_type";
    1.78 -
    1.79 -Goal "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A";
    1.80 -by (blast_tac (claset() addIs [eq_equiv_class, equiv_class_eq]
    1.81 -                      addDs [equiv_type]) 1);
    1.82 -qed "equiv_class_eq_iff";
    1.83 -
    1.84 -Goal "[| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} <-> <x,y>: r";
    1.85 -by (blast_tac (claset() addIs [eq_equiv_class, equiv_class_eq]
    1.86 -                      addDs [equiv_type]) 1);
    1.87 -qed "eq_equiv_class_iff";
    1.88 -
    1.89 -(*** Quotients ***)
    1.90 -
    1.91 -(** Introduction/elimination rules -- needed? **)
    1.92 -
    1.93 -Goalw [quotient_def] "x:A ==> r``{x}: A//r";
    1.94 -by (etac RepFunI 1);
    1.95 -qed "quotientI";
    1.96 -AddTCs [quotientI];
    1.97 -
    1.98 -val major::prems = Goalw [quotient_def]
    1.99 -    "[| X: A//r;  !!x. [| X = r``{x};  x:A |] ==> P |]   \
   1.100 -\    ==> P";
   1.101 -by (rtac (major RS RepFunE) 1);
   1.102 -by (eresolve_tac prems 1);
   1.103 -by (assume_tac 1);
   1.104 -qed "quotientE";
   1.105 -
   1.106 -Goalw [equiv_def,refl_def,quotient_def]
   1.107 -    "equiv(A,r) ==> Union(A//r) = A";
   1.108 -by (Blast_tac 1);
   1.109 -qed "Union_quotient";
   1.110 -
   1.111 -Goalw [quotient_def]
   1.112 -    "[| equiv(A,r);  X: A//r;  Y: A//r |] ==> X=Y | (X Int Y <= 0)";
   1.113 -by (safe_tac (claset() addSIs [equiv_class_eq]));
   1.114 -by (assume_tac 1);
   1.115 -by (rewrite_goals_tac [equiv_def,trans_def,sym_def]);
   1.116 -by (Blast_tac 1);
   1.117 -qed "quotient_disj";
   1.118 -
   1.119 -(**** Defining unary operations upon equivalence classes ****)
   1.120 -
   1.121 -(** These proofs really require as local premises
   1.122 -     equiv(A,r);  congruent(r,b)
   1.123 -**)
   1.124 -
   1.125 -(*Conversion rule*)
   1.126 -val prems as [equivA,bcong,_] = goal (the_context ())
   1.127 -    "[| equiv(A,r);  congruent(r,b);  a: A |] ==> (UN x:r``{a}. b(x)) = b(a)";
   1.128 -by (cut_facts_tac prems 1);
   1.129 -by (rtac ([refl RS UN_cong, UN_constant] MRS trans) 1);
   1.130 -by (etac equiv_class_self 2);
   1.131 -by (assume_tac 2);
   1.132 -by (rewrite_goals_tac [equiv_def,sym_def,congruent_def]);
   1.133 -by (Blast_tac 1);
   1.134 -qed "UN_equiv_class";
   1.135 -
   1.136 -(*type checking of  UN x:r``{a}. b(x) *)
   1.137 -val prems = Goalw [quotient_def]
   1.138 -    "[| equiv(A,r);  congruent(r,b);  X: A//r;   \
   1.139 -\       !!x.  x : A ==> b(x) : B |]     \
   1.140 -\    ==> (UN x:X. b(x)) : B";
   1.141 -by (cut_facts_tac prems 1);
   1.142 -by Safe_tac;
   1.143 -by (asm_simp_tac (simpset() addsimps UN_equiv_class::prems) 1);
   1.144 -qed "UN_equiv_class_type";
   1.145 -
   1.146 -(*Sufficient conditions for injectiveness.  Could weaken premises!
   1.147 -  major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
   1.148 -*)
   1.149 -val prems = Goalw [quotient_def]
   1.150 -    "[| equiv(A,r);   congruent(r,b);  \
   1.151 -\       (UN x:X. b(x))=(UN y:Y. b(y));  X: A//r;  Y: A//r;  \
   1.152 -\       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |]         \
   1.153 -\    ==> X=Y";
   1.154 -by (cut_facts_tac prems 1);
   1.155 -by Safe_tac;
   1.156 -by (rtac equiv_class_eq 1);
   1.157 -by (REPEAT (ares_tac prems 1));
   1.158 -by (etac box_equals 1);
   1.159 -by (REPEAT (ares_tac [UN_equiv_class] 1));
   1.160 -qed "UN_equiv_class_inject";
   1.161 -
   1.162 -
   1.163 -(**** Defining binary operations upon equivalence classes ****)
   1.164 -
   1.165 -
   1.166 -Goalw [congruent_def,congruent2_def,equiv_def,refl_def]
   1.167 -    "[| equiv(A,r);  congruent2(r,b);  a: A |] ==> congruent(r,b(a))";
   1.168 -by (Blast_tac 1);
   1.169 -qed "congruent2_implies_congruent";
   1.170 -
   1.171 -val equivA::prems = goalw (the_context ()) [congruent_def]
   1.172 -    "[| equiv(A,r);  congruent2(r,b);  a: A |] ==> \
   1.173 -\    congruent(r, %x1. UN x2:r``{a}. b(x1,x2))";
   1.174 -by (cut_facts_tac (equivA::prems) 1);
   1.175 -by Safe_tac;
   1.176 -by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
   1.177 -by (assume_tac 1);
   1.178 -by (asm_simp_tac (simpset() addsimps [equivA RS UN_equiv_class,
   1.179 -                                     congruent2_implies_congruent]) 1);
   1.180 -by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
   1.181 -by (Blast_tac 1);
   1.182 -qed "congruent2_implies_congruent_UN";
   1.183 -
   1.184 -val prems as equivA::_ = goal (the_context ())
   1.185 -    "[| equiv(A,r);  congruent2(r,b);  a1: A;  a2: A |]  \
   1.186 -\    ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)";
   1.187 -by (cut_facts_tac prems 1);
   1.188 -by (asm_simp_tac (simpset() addsimps [equivA RS UN_equiv_class,
   1.189 -                                     congruent2_implies_congruent,
   1.190 -                                     congruent2_implies_congruent_UN]) 1);
   1.191 -qed "UN_equiv_class2";
   1.192 -
   1.193 -(*type checking*)
   1.194 -val prems = Goalw [quotient_def]
   1.195 -    "[| equiv(A,r);  congruent2(r,b);                   \
   1.196 -\       X1: A//r;  X2: A//r;                            \
   1.197 -\       !!x1 x2.  [| x1: A; x2: A |] ==> b(x1,x2) : B   \
   1.198 -\    |] ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B";
   1.199 -by (cut_facts_tac prems 1);
   1.200 -by Safe_tac;
   1.201 -by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
   1.202 -                             congruent2_implies_congruent_UN,
   1.203 -                             congruent2_implies_congruent, quotientI]) 1));
   1.204 -qed "UN_equiv_class_type2";
   1.205 -
   1.206 -
   1.207 -(*Suggested by John Harrison -- the two subproofs may be MUCH simpler
   1.208 -  than the direct proof*)
   1.209 -val prems = Goalw [congruent2_def,equiv_def,refl_def]
   1.210 -    "[| equiv(A,r);     \
   1.211 -\       !! y z w. [| w: A;  <y,z> : r |] ==> b(y,w) = b(z,w);      \
   1.212 -\       !! y z w. [| w: A;  <y,z> : r |] ==> b(w,y) = b(w,z)       \
   1.213 -\    |] ==> congruent2(r,b)";
   1.214 -by (cut_facts_tac prems 1);
   1.215 -by Safe_tac;
   1.216 -by (rtac trans 1);
   1.217 -by (REPEAT (ares_tac prems 1
   1.218 -     ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
   1.219 -qed "congruent2I";
   1.220 -
   1.221 -val [equivA,commute,congt] = Goal
   1.222 -    "[| equiv(A,r);     \
   1.223 -\       !! y z. [| y: A;  z: A |] ==> b(y,z) = b(z,y);        \
   1.224 -\       !! y z w. [| w: A;  <y,z>: r |] ==> b(w,y) = b(w,z)     \
   1.225 -\    |] ==> congruent2(r,b)";
   1.226 -by (resolve_tac [equivA RS congruent2I] 1);
   1.227 -by (rtac (commute RS trans) 1);
   1.228 -by (rtac (commute RS trans RS sym) 3);
   1.229 -by (rtac sym 5);
   1.230 -by (REPEAT (ares_tac [congt] 1
   1.231 -     ORELSE etac (equivA RS equiv_type RS subsetD RS SigmaE2) 1));
   1.232 -qed "congruent2_commuteI";
   1.233 -
   1.234 -(*Obsolete?*)
   1.235 -val [equivA,ZinA,congt,commute] = Goalw [quotient_def]
   1.236 -    "[| equiv(A,r);  Z: A//r;  \
   1.237 -\       !!w. [| w: A |] ==> congruent(r, %z. b(w,z));    \
   1.238 -\       !!x y. [| x: A;  y: A |] ==> b(y,x) = b(x,y)    \
   1.239 -\    |] ==> congruent(r, %w. UN z: Z. b(w,z))";
   1.240 -val congt' = rewrite_rule [congruent_def] congt;
   1.241 -by (cut_facts_tac [ZinA] 1);
   1.242 -by (rewtac congruent_def);
   1.243 -by Safe_tac;
   1.244 -by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
   1.245 -by (assume_tac 1);
   1.246 -by (asm_simp_tac (simpset() addsimps [commute,
   1.247 -                                     [equivA, congt] MRS UN_equiv_class]) 1);
   1.248 -by (REPEAT (ares_tac [congt' RS spec RS spec RS mp] 1));
   1.249 -qed "congruent_commuteI";
     2.1 --- a/src/ZF/Integ/EquivClass.thy	Fri Sep 20 11:49:38 2002 +0200
     2.2 +++ b/src/ZF/Integ/EquivClass.thy	Sat Sep 21 21:10:34 2002 +0200
     2.3 @@ -3,21 +3,260 @@
     2.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.5      Copyright   1994  University of Cambridge
     2.6  
     2.7 -Equivalence relations in Zermelo-Fraenkel Set Theory 
     2.8  *)
     2.9  
    2.10 -EquivClass = Trancl + Perm + 
    2.11 +header{*Equivalence Relations*}
    2.12 +
    2.13 +theory EquivClass = Trancl + Perm:
    2.14  
    2.15  constdefs
    2.16  
    2.17 -  quotient    :: [i,i]=>i    (infixl "'/'/" 90)  (*set of equiv classes*)
    2.18 +  quotient   :: "[i,i]=>i"    (infixl "'/'/" 90)  (*set of equiv classes*)
    2.19        "A//r == {r``{x} . x:A}"
    2.20  
    2.21 -  congruent   :: [i,i=>i]=>o
    2.22 +  congruent  :: "[i,i=>i]=>o"
    2.23        "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
    2.24  
    2.25 -  congruent2  :: [i,[i,i]=>i]=>o
    2.26 -      "congruent2(r,b) == ALL y1 z1 y2 z2. 
    2.27 +  congruent2 :: "[i,[i,i]=>i]=>o"
    2.28 +      "congruent2(r,b) == ALL y1 z1 y2 z2.
    2.29             <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
    2.30  
    2.31 +subsection{*Suppes, Theorem 70:
    2.32 +    @{term r} is an equiv relation iff @{term "converse(r) O r = r"}*}
    2.33 +
    2.34 +(** first half: equiv(A,r) ==> converse(r) O r = r **)
    2.35 +
    2.36 +lemma sym_trans_comp_subset:
    2.37 +    "[| sym(r); trans(r) |] ==> converse(r) O r <= r"
    2.38 +apply (unfold trans_def sym_def, blast)
    2.39 +done
    2.40 +
    2.41 +lemma refl_comp_subset:
    2.42 +    "[| refl(A,r); r <= A*A |] ==> r <= converse(r) O r"
    2.43 +apply (unfold refl_def, blast)
    2.44 +done
    2.45 +
    2.46 +lemma equiv_comp_eq:
    2.47 +    "equiv(A,r) ==> converse(r) O r = r"
    2.48 +apply (unfold equiv_def)
    2.49 +apply (blast del: subsetI
    2.50 +             intro!: sym_trans_comp_subset refl_comp_subset)
    2.51 +done
    2.52 +
    2.53 +(*second half*)
    2.54 +lemma comp_equivI:
    2.55 +    "[| converse(r) O r = r;  domain(r) = A |] ==> equiv(A,r)"
    2.56 +apply (unfold equiv_def refl_def sym_def trans_def)
    2.57 +apply (erule equalityE)
    2.58 +apply (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r", blast+)
    2.59 +done
    2.60 +
    2.61 +(** Equivalence classes **)
    2.62 +
    2.63 +(*Lemma for the next result*)
    2.64 +lemma equiv_class_subset:
    2.65 +    "[| sym(r);  trans(r);  <a,b>: r |] ==> r``{a} <= r``{b}"
    2.66 +by (unfold trans_def sym_def, blast)
    2.67 +
    2.68 +lemma equiv_class_eq:
    2.69 +    "[| equiv(A,r);  <a,b>: r |] ==> r``{a} = r``{b}"
    2.70 +apply (unfold equiv_def)
    2.71 +apply (safe del: subsetI intro!: equalityI equiv_class_subset)
    2.72 +apply (unfold sym_def, blast)
    2.73 +done
    2.74 +
    2.75 +lemma equiv_class_self:
    2.76 +    "[| equiv(A,r);  a: A |] ==> a: r``{a}"
    2.77 +by (unfold equiv_def refl_def, blast)
    2.78 +
    2.79 +(*Lemma for the next result*)
    2.80 +lemma subset_equiv_class:
    2.81 +    "[| equiv(A,r);  r``{b} <= r``{a};  b: A |] ==> <a,b>: r"
    2.82 +by (unfold equiv_def refl_def, blast)
    2.83 +
    2.84 +lemma eq_equiv_class: "[| r``{a} = r``{b};  equiv(A,r);  b: A |] ==> <a,b>: r"
    2.85 +by (assumption | rule equalityD2 subset_equiv_class)+
    2.86 +
    2.87 +(*thus r``{a} = r``{b} as well*)
    2.88 +lemma equiv_class_nondisjoint:
    2.89 +    "[| equiv(A,r);  x: (r``{a} Int r``{b}) |] ==> <a,b>: r"
    2.90 +by (unfold equiv_def trans_def sym_def, blast)
    2.91 +
    2.92 +lemma equiv_type: "equiv(A,r) ==> r <= A*A"
    2.93 +by (unfold equiv_def, blast)
    2.94 +
    2.95 +lemma equiv_class_eq_iff:
    2.96 +     "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A"
    2.97 +by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
    2.98 +
    2.99 +lemma eq_equiv_class_iff:
   2.100 +     "[| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} <-> <x,y>: r"
   2.101 +by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
   2.102 +
   2.103 +(*** Quotients ***)
   2.104 +
   2.105 +(** Introduction/elimination rules -- needed? **)
   2.106 +
   2.107 +lemma quotientI [TC]: "x:A ==> r``{x}: A//r"
   2.108 +apply (unfold quotient_def)
   2.109 +apply (erule RepFunI)
   2.110 +done
   2.111 +
   2.112 +lemma quotientE:
   2.113 +    "[| X: A//r;  !!x. [| X = r``{x};  x:A |] ==> P |] ==> P"
   2.114 +by (unfold quotient_def, blast)
   2.115 +
   2.116 +lemma Union_quotient:
   2.117 +    "equiv(A,r) ==> Union(A//r) = A"
   2.118 +by (unfold equiv_def refl_def quotient_def, blast)
   2.119 +
   2.120 +lemma quotient_disj:
   2.121 +    "[| equiv(A,r);  X: A//r;  Y: A//r |] ==> X=Y | (X Int Y <= 0)"
   2.122 +apply (unfold quotient_def)
   2.123 +apply (safe intro!: equiv_class_eq, assumption)
   2.124 +apply (unfold equiv_def trans_def sym_def, blast)
   2.125 +done
   2.126 +
   2.127 +subsection{*Defining Unary Operations upon Equivalence Classes*}
   2.128 +
   2.129 +(** Could have a locale with the premises equiv(A,r)  and  congruent(r,b)
   2.130 +**)
   2.131 +
   2.132 +(*Conversion rule*)
   2.133 +lemma UN_equiv_class:
   2.134 +    "[| equiv(A,r);  congruent(r,b);  a: A |] ==> (UN x:r``{a}. b(x)) = b(a)"
   2.135 +apply (rule trans [OF refl [THEN UN_cong] UN_constant])
   2.136 +apply (erule_tac [2] equiv_class_self)
   2.137 +prefer 2 apply assumption
   2.138 +apply (unfold equiv_def sym_def congruent_def, blast)
   2.139 +done
   2.140 +
   2.141 +(*type checking of  UN x:r``{a}. b(x) *)
   2.142 +lemma UN_equiv_class_type:
   2.143 +    "[| equiv(A,r);  congruent(r,b);  X: A//r;  !!x.  x : A ==> b(x) : B |]
   2.144 +     ==> (UN x:X. b(x)) : B"
   2.145 +apply (unfold quotient_def, safe)
   2.146 +apply (simp (no_asm_simp) add: UN_equiv_class)
   2.147 +done
   2.148 +
   2.149 +(*Sufficient conditions for injectiveness.  Could weaken premises!
   2.150 +  major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
   2.151 +*)
   2.152 +lemma UN_equiv_class_inject:
   2.153 +    "[| equiv(A,r);   congruent(r,b);
   2.154 +        (UN x:X. b(x))=(UN y:Y. b(y));  X: A//r;  Y: A//r;
   2.155 +        !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |]
   2.156 +     ==> X=Y"
   2.157 +apply (unfold quotient_def, safe)
   2.158 +apply (rule equiv_class_eq, assumption)
   2.159 +apply (rotate_tac -2) 
   2.160 +apply (simp add: UN_equiv_class [of A r b])  
   2.161 +done
   2.162 +
   2.163 +
   2.164 +subsection{*Defining Binary Operations upon Equivalence Classes*}
   2.165 +
   2.166 +
   2.167 +lemma congruent2_implies_congruent:
   2.168 +    "[| equiv(A,r);  congruent2(r,b);  a: A |] ==> congruent(r,b(a))"
   2.169 +apply (unfold congruent_def congruent2_def equiv_def refl_def, blast)
   2.170 +done
   2.171 +
   2.172 +lemma congruent2_implies_congruent_UN:
   2.173 +    "[| equiv(A,r);  congruent2(r,b);  a: A |] ==>
   2.174 +     congruent(r, %x1. UN x2:r``{a}. b(x1,x2))"
   2.175 +apply (unfold congruent_def, safe)
   2.176 +apply (frule equiv_type [THEN subsetD], assumption)
   2.177 +apply clarify 
   2.178 +apply (simp add: UN_equiv_class [of A r] congruent2_implies_congruent)
   2.179 +apply (unfold congruent2_def equiv_def refl_def, blast)
   2.180 +done
   2.181 +
   2.182 +lemma UN_equiv_class2:
   2.183 +    "[| equiv(A,r);  congruent2(r,b);  a1: A;  a2: A |]
   2.184 +     ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)"
   2.185 +by (simp add: UN_equiv_class [of A r] congruent2_implies_congruent
   2.186 +              congruent2_implies_congruent_UN)
   2.187 +
   2.188 +(*type checking*)
   2.189 +lemma UN_equiv_class_type2:
   2.190 +    "[| equiv(A,r);  congruent2(r,b);
   2.191 +        X1: A//r;  X2: A//r;
   2.192 +        !!x1 x2.  [| x1: A; x2: A |] ==> b(x1,x2) : B
   2.193 +     |] ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B"
   2.194 +apply (unfold quotient_def, safe)
   2.195 +apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN 
   2.196 +                    congruent2_implies_congruent quotientI)
   2.197 +done
   2.198 +
   2.199 +
   2.200 +(*Suggested by John Harrison -- the two subproofs may be MUCH simpler
   2.201 +  than the direct proof*)
   2.202 +lemma congruent2I:
   2.203 +    "[| equiv(A,r);
   2.204 +        !! y z w. [| w: A;  <y,z> : r |] ==> b(y,w) = b(z,w);
   2.205 +        !! y z w. [| w: A;  <y,z> : r |] ==> b(w,y) = b(w,z)
   2.206 +     |] ==> congruent2(r,b)"
   2.207 +apply (unfold congruent2_def equiv_def refl_def, safe)
   2.208 +apply (blast intro: trans) 
   2.209 +done
   2.210 +
   2.211 +lemma congruent2_commuteI:
   2.212 + assumes equivA: "equiv(A,r)"
   2.213 +     and commute: "!! y z. [| y: A;  z: A |] ==> b(y,z) = b(z,y)"
   2.214 +     and congt:   "!! y z w. [| w: A;  <y,z>: r |] ==> b(w,y) = b(w,z)"
   2.215 + shows "congruent2(r,b)"
   2.216 +apply (insert equivA [THEN equiv_type, THEN subsetD]) 
   2.217 +apply (rule congruent2I [OF equivA])
   2.218 +apply (rule commute [THEN trans])
   2.219 +apply (rule_tac [3] commute [THEN trans, symmetric])
   2.220 +apply (rule_tac [5] sym) 
   2.221 +apply (blast intro: congt)+
   2.222 +done
   2.223 +
   2.224 +(*Obsolete?*)
   2.225 +lemma congruent_commuteI:
   2.226 +    "[| equiv(A,r);  Z: A//r;
   2.227 +        !!w. [| w: A |] ==> congruent(r, %z. b(w,z));
   2.228 +        !!x y. [| x: A;  y: A |] ==> b(y,x) = b(x,y)
   2.229 +     |] ==> congruent(r, %w. UN z: Z. b(w,z))"
   2.230 +apply (simp (no_asm) add: congruent_def)
   2.231 +apply (safe elim!: quotientE)
   2.232 +apply (frule equiv_type [THEN subsetD], assumption)
   2.233 +apply (simp add: UN_equiv_class [of A r]) 
   2.234 +apply (simp add: congruent_def) 
   2.235 +done
   2.236 +
   2.237 +ML
   2.238 +{*
   2.239 +val sym_trans_comp_subset = thm "sym_trans_comp_subset";
   2.240 +val refl_comp_subset = thm "refl_comp_subset";
   2.241 +val equiv_comp_eq = thm "equiv_comp_eq";
   2.242 +val comp_equivI = thm "comp_equivI";
   2.243 +val equiv_class_subset = thm "equiv_class_subset";
   2.244 +val equiv_class_eq = thm "equiv_class_eq";
   2.245 +val equiv_class_self = thm "equiv_class_self";
   2.246 +val subset_equiv_class = thm "subset_equiv_class";
   2.247 +val eq_equiv_class = thm "eq_equiv_class";
   2.248 +val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";
   2.249 +val equiv_type = thm "equiv_type";
   2.250 +val equiv_class_eq_iff = thm "equiv_class_eq_iff";
   2.251 +val eq_equiv_class_iff = thm "eq_equiv_class_iff";
   2.252 +val quotientI = thm "quotientI";
   2.253 +val quotientE = thm "quotientE";
   2.254 +val Union_quotient = thm "Union_quotient";
   2.255 +val quotient_disj = thm "quotient_disj";
   2.256 +val UN_equiv_class = thm "UN_equiv_class";
   2.257 +val UN_equiv_class_type = thm "UN_equiv_class_type";
   2.258 +val UN_equiv_class_inject = thm "UN_equiv_class_inject";
   2.259 +val congruent2_implies_congruent = thm "congruent2_implies_congruent";
   2.260 +val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN";
   2.261 +val congruent_commuteI = thm "congruent_commuteI";
   2.262 +val UN_equiv_class2 = thm "UN_equiv_class2";
   2.263 +val UN_equiv_class_type2 = thm "UN_equiv_class_type2";
   2.264 +val congruent2I = thm "congruent2I";
   2.265 +val congruent2_commuteI = thm "congruent2_commuteI";
   2.266 +val congruent_commuteI = thm "congruent_commuteI";
   2.267 +*}
   2.268 +
   2.269  end
     3.1 --- a/src/ZF/IsaMakefile	Fri Sep 20 11:49:38 2002 +0200
     3.2 +++ b/src/ZF/IsaMakefile	Sat Sep 21 21:10:34 2002 +0200
     3.3 @@ -33,7 +33,7 @@
     3.4    CardinalArith.thy Cardinal_AC.thy \
     3.5    Datatype.ML Datatype.thy Epsilon.thy Finite.thy	\
     3.6    Fixedpt.thy Inductive.ML Inductive.thy 	\
     3.7 -  InfDatatype.thy Integ/Bin.thy Integ/EquivClass.ML	\
     3.8 +  InfDatatype.thy Integ/Bin.thy \
     3.9    Integ/EquivClass.thy Integ/Int.thy Integ/IntArith.thy	\
    3.10    Integ/IntDiv.thy Integ/int_arith.ML			\
    3.11    Let.ML Let.thy List.thy Main.ML Main.thy	\