author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 2469  b50b8c0eec01 
permissions  rwrr 
1461  1 
(* Title: ZF/EquivClass.ML 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

4 
Copyright 1994 University of Cambridge 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

5 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

6 
For EquivClass.thy. Equivalence relations in ZermeloFraenkel Set Theory 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

7 
*) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

8 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

9 
val RSLIST = curry (op MRS); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

10 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

11 
open EquivClass; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

12 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

13 
(*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

14 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

15 
(** first half: equiv(A,r) ==> converse(r) O r = r **) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

16 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

17 
goalw EquivClass.thy [trans_def,sym_def] 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

18 
"!!r. [ sym(r); trans(r) ] ==> converse(r) O r <= r"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

19 
by (fast_tac (ZF_cs addSEs [converseD,compE]) 1); 
760  20 
qed "sym_trans_comp_subset"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

21 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

22 
goalw EquivClass.thy [refl_def] 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

23 
"!!A r. [ refl(A,r); r <= A*A ] ==> r <= converse(r) O r"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

24 
by (fast_tac (ZF_cs addSIs [converseI] addIs [compI]) 1); 
760  25 
qed "refl_comp_subset"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

26 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

27 
goalw EquivClass.thy [equiv_def] 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

28 
"!!A r. equiv(A,r) ==> converse(r) O r = r"; 
749  29 
by (fast_tac (subset_cs addSIs [equalityI, sym_trans_comp_subset, 
1461  30 
refl_comp_subset]) 1); 
760  31 
qed "equiv_comp_eq"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

32 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

33 
(*second half*) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

34 
goalw EquivClass.thy [equiv_def,refl_def,sym_def,trans_def] 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

35 
"!!A r. [ converse(r) O r = r; domain(r) = A ] ==> equiv(A,r)"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

36 
by (etac equalityE 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

37 
by (subgoal_tac "ALL x y. <x,y> : r > <y,x> : r" 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

38 
by (safe_tac ZF_cs); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

39 
by (fast_tac (ZF_cs addSIs [converseI] addIs [compI]) 3); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

40 
by (ALLGOALS (fast_tac 
1461  41 
(ZF_cs addSIs [converseI] addIs [compI] addSEs [compE]))); 
760  42 
qed "comp_equivI"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

43 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

44 
(** Equivalence classes **) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

45 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

46 
(*Lemma for the next result*) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

47 
goalw EquivClass.thy [trans_def,sym_def] 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

48 
"!!A r. [ sym(r); trans(r); <a,b>: r ] ==> r``{a} <= r``{b}"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

49 
by (fast_tac ZF_cs 1); 
760  50 
qed "equiv_class_subset"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

51 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

52 
goalw EquivClass.thy [equiv_def] 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

53 
"!!A r. [ equiv(A,r); <a,b>: r ] ==> r``{a} = r``{b}"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

54 
by (safe_tac (subset_cs addSIs [equalityI, equiv_class_subset])); 
1461  55 
by (rewtac sym_def); 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

56 
by (fast_tac ZF_cs 1); 
760  57 
qed "equiv_class_eq"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

58 

749  59 
goalw EquivClass.thy [equiv_def,refl_def] 
60 
"!!A r. [ equiv(A,r); a: A ] ==> a: r``{a}"; 

535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

61 
by (fast_tac ZF_cs 1); 
760  62 
qed "equiv_class_self"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

63 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

64 
(*Lemma for the next result*) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

65 
goalw EquivClass.thy [equiv_def,refl_def] 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

66 
"!!A r. [ equiv(A,r); r``{b} <= r``{a}; b: A ] ==> <a,b>: r"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

67 
by (fast_tac ZF_cs 1); 
760  68 
qed "subset_equiv_class"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

69 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

70 
val prems = goal EquivClass.thy 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

71 
"[ r``{a} = r``{b}; equiv(A,r); b: A ] ==> <a,b>: r"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

72 
by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1)); 
760  73 
qed "eq_equiv_class"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

74 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

75 
(*thus r``{a} = r``{b} as well*) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

76 
goalw EquivClass.thy [equiv_def,trans_def,sym_def] 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

77 
"!!A r. [ equiv(A,r); x: (r``{a} Int r``{b}) ] ==> <a,b>: r"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

78 
by (fast_tac ZF_cs 1); 
760  79 
qed "equiv_class_nondisjoint"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

80 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

81 
goalw EquivClass.thy [equiv_def] "!!A r. equiv(A,r) ==> r <= A*A"; 
1076
68f088887f48
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
1013
diff
changeset

82 
by (safe_tac subset_cs); 
760  83 
qed "equiv_type"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

84 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

85 
goal EquivClass.thy 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

86 
"!!A r. equiv(A,r) ==> <x,y>: r <> r``{x} = r``{y} & x:A & y:A"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

87 
by (fast_tac (ZF_cs addIs [eq_equiv_class, equiv_class_eq] 
1461  88 
addDs [equiv_type]) 1); 
760  89 
qed "equiv_class_eq_iff"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

90 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

91 
goal EquivClass.thy 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

92 
"!!A r. [ equiv(A,r); x: A; y: A ] ==> r``{x} = r``{y} <> <x,y>: r"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

93 
by (fast_tac (ZF_cs addIs [eq_equiv_class, equiv_class_eq] 
1461  94 
addDs [equiv_type]) 1); 
760  95 
qed "eq_equiv_class_iff"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

96 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

97 
(*** Quotients ***) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

98 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

99 
(** Introduction/elimination rules  needed? **) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

100 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

101 
val prems = goalw EquivClass.thy [quotient_def] "x:A ==> r``{x}: A/r"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

102 
by (rtac RepFunI 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

103 
by (resolve_tac prems 1); 
760  104 
qed "quotientI"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

105 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

106 
val major::prems = goalw EquivClass.thy [quotient_def] 
1461  107 
"[ X: A/r; !!x. [ X = r``{x}; x:A ] ==> P ] \ 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

108 
\ ==> P"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

109 
by (rtac (major RS RepFunE) 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

110 
by (eresolve_tac prems 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

111 
by (assume_tac 1); 
760  112 
qed "quotientE"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

113 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

114 
goalw EquivClass.thy [equiv_def,refl_def,quotient_def] 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

115 
"!!A r. equiv(A,r) ==> Union(A/r) = A"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

116 
by (fast_tac eq_cs 1); 
760  117 
qed "Union_quotient"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

118 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

119 
goalw EquivClass.thy [quotient_def] 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

120 
"!!A r. [ equiv(A,r); X: A/r; Y: A/r ] ==> X=Y  (X Int Y <= 0)"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

121 
by (safe_tac (ZF_cs addSIs [equiv_class_eq])); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

122 
by (assume_tac 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

123 
by (rewrite_goals_tac [equiv_def,trans_def,sym_def]); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

124 
by (fast_tac ZF_cs 1); 
760  125 
qed "quotient_disj"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

126 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

127 
(**** Defining unary operations upon equivalence classes ****) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

128 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

129 
(** These proofs really require as local premises 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

130 
equiv(A,r); congruent(r,b) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

131 
**) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

132 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

133 
(*Conversion rule*) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

134 
val prems as [equivA,bcong,_] = goal EquivClass.thy 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

135 
"[ equiv(A,r); congruent(r,b); a: A ] ==> (UN x:r``{a}. b(x)) = b(a)"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

136 
by (cut_facts_tac prems 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

137 
by (rtac ([refl RS UN_cong, UN_constant] MRS trans) 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

138 
by (etac equiv_class_self 2); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

139 
by (assume_tac 2); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

140 
by (rewrite_goals_tac [equiv_def,sym_def,congruent_def]); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

141 
by (fast_tac ZF_cs 1); 
760  142 
qed "UN_equiv_class"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

143 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

144 
(*type checking of UN x:r``{a}. b(x) *) 
946  145 
val prems = goalw EquivClass.thy [quotient_def] 
1461  146 
"[ equiv(A,r); congruent(r,b); X: A/r; \ 
147 
\ !!x. x : A ==> b(x) : B ] \ 

535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

148 
\ ==> (UN x:X. b(x)) : B"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

149 
by (cut_facts_tac prems 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

150 
by (safe_tac ZF_cs); 
946  151 
by (asm_simp_tac (ZF_ss addsimps (UN_equiv_class::prems)) 1); 
760  152 
qed "UN_equiv_class_type"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

153 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

154 
(*Sufficient conditions for injectiveness. Could weaken premises! 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

155 
major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

156 
*) 
946  157 
val prems = goalw EquivClass.thy [quotient_def] 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

158 
"[ equiv(A,r); congruent(r,b); \ 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

159 
\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \ 
1461  160 
\ !!x y. [ x:A; y:A; b(x)=b(y) ] ==> <x,y>:r ] \ 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

161 
\ ==> X=Y"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

162 
by (cut_facts_tac prems 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

163 
by (safe_tac ZF_cs); 
946  164 
by (rtac equiv_class_eq 1); 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

165 
by (REPEAT (ares_tac prems 1)); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

166 
by (etac box_equals 1); 
946  167 
by (REPEAT (ares_tac [UN_equiv_class] 1)); 
760  168 
qed "UN_equiv_class_inject"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

169 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

170 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

171 
(**** Defining binary operations upon equivalence classes ****) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

172 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

173 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

174 
goalw EquivClass.thy [congruent_def,congruent2_def,equiv_def,refl_def] 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

175 
"!!A r. [ equiv(A,r); congruent2(r,b); a: A ] ==> congruent(r,b(a))"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

176 
by (fast_tac ZF_cs 1); 
760  177 
qed "congruent2_implies_congruent"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

178 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

179 
val equivA::prems = goalw EquivClass.thy [congruent_def] 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

180 
"[ equiv(A,r); congruent2(r,b); a: A ] ==> \ 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

181 
\ congruent(r, %x1. UN x2:r``{a}. b(x1,x2))"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

182 
by (cut_facts_tac (equivA::prems) 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

183 
by (safe_tac ZF_cs); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

184 
by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

185 
by (assume_tac 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

186 
by (asm_simp_tac (ZF_ss addsimps [equivA RS UN_equiv_class, 
1461  187 
congruent2_implies_congruent]) 1); 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

188 
by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

189 
by (fast_tac ZF_cs 1); 
760  190 
qed "congruent2_implies_congruent_UN"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

191 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

192 
val prems as equivA::_ = goal EquivClass.thy 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

193 
"[ equiv(A,r); congruent2(r,b); a1: A; a2: A ] \ 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

194 
\ ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

195 
by (cut_facts_tac prems 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

196 
by (asm_simp_tac (ZF_ss addsimps [equivA RS UN_equiv_class, 
1461  197 
congruent2_implies_congruent, 
198 
congruent2_implies_congruent_UN]) 1); 

760  199 
qed "UN_equiv_class2"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

200 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

201 
(*type checking*) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

202 
val prems = goalw EquivClass.thy [quotient_def] 
1461  203 
"[ equiv(A,r); congruent2(r,b); \ 
204 
\ X1: A/r; X2: A/r; \ 

205 
\ !!x1 x2. [ x1: A; x2: A ] ==> b(x1,x2) : B \ 

749  206 
\ ] ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

207 
by (cut_facts_tac prems 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

208 
by (safe_tac ZF_cs); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

209 
by (REPEAT (ares_tac (prems@[UN_equiv_class_type, 
1461  210 
congruent2_implies_congruent_UN, 
211 
congruent2_implies_congruent, quotientI]) 1)); 

760  212 
qed "UN_equiv_class_type2"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

213 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

214 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

215 
(*Suggested by John Harrison  the two subproofs may be MUCH simpler 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

216 
than the direct proof*) 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

217 
val prems = goalw EquivClass.thy [congruent2_def,equiv_def,refl_def] 
1461  218 
"[ equiv(A,r); \ 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

219 
\ !! y z w. [ w: A; <y,z> : r ] ==> b(y,w) = b(z,w); \ 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

220 
\ !! y z w. [ w: A; <y,z> : r ] ==> b(w,y) = b(w,z) \ 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

221 
\ ] ==> congruent2(r,b)"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

222 
by (cut_facts_tac prems 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

223 
by (safe_tac ZF_cs); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

224 
by (rtac trans 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

225 
by (REPEAT (ares_tac prems 1 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

226 
ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1)); 
760  227 
qed "congruent2I"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

228 

9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

229 
val [equivA,commute,congt] = goal EquivClass.thy 
1461  230 
"[ equiv(A,r); \ 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

231 
\ !! y z. [ y: A; z: A ] ==> b(y,z) = b(z,y); \ 
1461  232 
\ !! y z w. [ w: A; <y,z>: r ] ==> b(w,y) = b(w,z) \ 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

233 
\ ] ==> congruent2(r,b)"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

234 
by (resolve_tac [equivA RS congruent2I] 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

235 
by (rtac (commute RS trans) 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

236 
by (rtac (commute RS trans RS sym) 3); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

237 
by (rtac sym 5); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

238 
by (REPEAT (ares_tac [congt] 1 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

239 
ORELSE etac (equivA RS equiv_type RS subsetD RS SigmaE2) 1)); 
760  240 
qed "congruent2_commuteI"; 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

241 

723
82caba9e130f
ZF/EquivClass/congruent_commuteI: uncommented and simplified proof
lcp
parents:
535
diff
changeset

242 
(*Obsolete?*) 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

243 
val [equivA,ZinA,congt,commute] = goalw EquivClass.thy [quotient_def] 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

244 
"[ equiv(A,r); Z: A/r; \ 
1461  245 
\ !!w. [ w: A ] ==> congruent(r, %z.b(w,z)); \ 
246 
\ !!x y. [ x: A; y: A ] ==> b(y,x) = b(x,y) \ 

535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

247 
\ ] ==> congruent(r, %w. UN z: Z. b(w,z))"; 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

248 
val congt' = rewrite_rule [congruent_def] congt; 
723
82caba9e130f
ZF/EquivClass/congruent_commuteI: uncommented and simplified proof
lcp
parents:
535
diff
changeset

249 
by (cut_facts_tac [ZinA] 1); 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

250 
by (rewtac congruent_def); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

251 
by (safe_tac ZF_cs); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

252 
by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1); 
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

253 
by (assume_tac 1); 
723
82caba9e130f
ZF/EquivClass/congruent_commuteI: uncommented and simplified proof
lcp
parents:
535
diff
changeset

254 
by (asm_simp_tac (ZF_ss addsimps [commute, 
1461  255 
[equivA, congt] MRS UN_equiv_class]) 1); 
535
9d62c7e08699
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp
parents:
diff
changeset

256 
by (REPEAT (ares_tac [congt' RS spec RS spec RS mp] 1)); 
760  257 
qed "congruent_commuteI"; 