author  paulson 
Wed, 11 Sep 1996 18:46:07 +0200  
changeset 1978  e7df069acb74 
parent 1894  c2c8279d40f0 
child 2036  62ff902eeffc 
permissions  rwrr 
1465  1 
(* Title: Equiv.ML 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

2 
ID: $Id$ 
1465  3 
Authors: Riccardo Mattolini, Dip. Sistemi e Informatica 
4 
Lawrence C Paulson, Cambridge University Computer Laboratory 

925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

5 
Copyright 1994 Universita' di Firenze 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

6 
Copyright 1993 University of Cambridge 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

7 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

8 
Equivalence relations in HOL Set Theory 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

9 
*) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

10 

1978  11 
val RSLIST = curry (op MRS); 
12 

925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

13 
open Equiv; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

14 

1894  15 
Delrules [equalityI]; 
16 

925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

17 
(*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

18 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

19 
(** first half: equiv A r ==> converse(r) O r = r **) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

20 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

21 
goalw Equiv.thy [trans_def,sym_def,converse_def] 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

22 
"!!r. [ sym(r); trans(r) ] ==> converse(r) O r <= r"; 
1894  23 
by (fast_tac (!claset addSEs [converseD]) 1); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

24 
qed "sym_trans_comp_subset"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

25 

1045  26 
goalw Equiv.thy [refl_def] 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

27 
"!!A r. refl A r ==> r <= converse(r) O r"; 
1894  28 
by (fast_tac (!claset addIs [compI]) 1); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

29 
qed "refl_comp_subset"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

30 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

31 
goalw Equiv.thy [equiv_def] 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

32 
"!!A r. equiv A r ==> converse(r) O r = r"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

33 
by (rtac equalityI 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

34 
by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

35 
ORELSE etac conjE 1)); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

36 
qed "equiv_comp_eq"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

37 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

38 
(*second half*) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

39 
goalw Equiv.thy [equiv_def,refl_def,sym_def,trans_def] 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

40 
"!!A r. [ converse(r) O r = r; Domain(r) = A ] ==> equiv A r"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

41 
by (etac equalityE 1); 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset

42 
by (subgoal_tac "ALL x y. (x,y) : r > (y,x) : r" 1); 
1894  43 
by (safe_tac (!claset)); 
44 
by (fast_tac (!claset addSIs [converseI] addIs [compI]) 3); 

45 
by (ALLGOALS (fast_tac (!claset addIs [compI] addSEs [compE]))); 

925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

46 
qed "comp_equivI"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

47 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

48 
(** Equivalence classes **) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

49 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

50 
(*Lemma for the next result*) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

51 
goalw Equiv.thy [equiv_def,trans_def,sym_def] 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset

52 
"!!A r. [ equiv A r; (a,b): r ] ==> r^^{a} <= r^^{b}"; 
1894  53 
by (safe_tac (!claset)); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

54 
by (rtac ImageI 1); 
1894  55 
by (Fast_tac 2); 
56 
by (Fast_tac 1); 

925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

57 
qed "equiv_class_subset"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

58 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset

59 
goal Equiv.thy "!!A r. [ equiv A r; (a,b): r ] ==> r^^{a} = r^^{b}"; 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

60 
by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1)); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

61 
by (rewrite_goals_tac [equiv_def,sym_def]); 
1894  62 
by (Fast_tac 1); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

63 
qed "equiv_class_eq"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

64 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

65 
val prems = goalw Equiv.thy [equiv_def,refl_def] 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

66 
"[ equiv A r; a: A ] ==> a: r^^{a}"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

67 
by (cut_facts_tac prems 1); 
1894  68 
by (Fast_tac 1); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

69 
qed "equiv_class_self"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

70 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

71 
(*Lemma for the next result*) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

72 
goalw Equiv.thy [equiv_def,refl_def] 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset

73 
"!!A r. [ equiv A r; r^^{b} <= r^^{a}; b: A ] ==> (a,b): r"; 
1894  74 
by (Fast_tac 1); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

75 
qed "subset_equiv_class"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

76 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

77 
val prems = goal Equiv.thy 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset

78 
"[ r^^{a} = r^^{b}; equiv A r; b: A ] ==> (a,b): r"; 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

79 
by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1)); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

80 
qed "eq_equiv_class"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

81 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

82 
(*thus r^^{a} = r^^{b} as well*) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

83 
goalw Equiv.thy [equiv_def,trans_def,sym_def] 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset

84 
"!!A r. [ equiv A r; x: (r^^{a} Int r^^{b}) ] ==> (a,b): r"; 
1894  85 
by (Fast_tac 1); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

86 
qed "equiv_class_nondisjoint"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

87 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

88 
val [major] = goalw Equiv.thy [equiv_def,refl_def] 
1642  89 
"equiv A r ==> r <= A Times A"; 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

90 
by (rtac (major RS conjunct1 RS conjunct1) 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

91 
qed "equiv_type"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

92 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

93 
goal Equiv.thy 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset

94 
"!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)"; 
1894  95 
by (safe_tac (!claset)); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

96 
by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1)); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

97 
by ((rtac eq_equiv_class 3) THEN 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

98 
(assume_tac 4) THEN (assume_tac 4) THEN (assume_tac 3)); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

99 
by ((dtac equiv_type 1) THEN (dtac rev_subsetD 1) THEN 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

100 
(assume_tac 1) THEN (dtac SigmaD1 1) THEN (assume_tac 1)); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

101 
by ((dtac equiv_type 1) THEN (dtac rev_subsetD 1) THEN 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

102 
(assume_tac 1) THEN (dtac SigmaD2 1) THEN (assume_tac 1)); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

103 
qed "equiv_class_eq_iff"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

104 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

105 
goal Equiv.thy 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset

106 
"!!A r. [ equiv A r; x: A; y: A ] ==> (r^^{x} = r^^{y}) = ((x,y): r)"; 
1894  107 
by (safe_tac (!claset)); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

108 
by ((rtac eq_equiv_class 1) THEN 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

109 
(assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1)); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

110 
by ((rtac equiv_class_eq 1) THEN 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

111 
(assume_tac 1) THEN (assume_tac 1)); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

112 
qed "eq_equiv_class_iff"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

113 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

114 
(*** Quotients ***) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

115 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

116 
(** Introduction/elimination rules  needed? **) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

117 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

118 
val prems = goalw Equiv.thy [quotient_def] "x:A ==> r^^{x}: A/r"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

119 
by (rtac UN_I 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

120 
by (resolve_tac prems 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

121 
by (rtac singletonI 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

122 
qed "quotientI"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

123 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

124 
val [major,minor] = goalw Equiv.thy [quotient_def] 
1465  125 
"[ X:(A/r); !!x. [ X = r^^{x}; x:A ] ==> P ] \ 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

126 
\ ==> P"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

127 
by (resolve_tac [major RS UN_E] 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

128 
by (rtac minor 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

129 
by (assume_tac 2); 
1894  130 
by (Fast_tac 1); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

131 
qed "quotientE"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

132 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

133 
(** Not needed by Theory Integ > bypassed **) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

134 
(**goalw Equiv.thy [equiv_def,refl_def,quotient_def] 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

135 
"!!A r. equiv A r ==> Union(A/r) = A"; 
1844  136 
by (Fast_tac 1); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

137 
qed "Union_quotient"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

138 
**) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

139 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

140 
(** Not needed by Theory Integ > bypassed **) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

141 
(*goalw Equiv.thy [quotient_def] 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

142 
"!!A r. [ equiv A r; X: A/r; Y: A/r ] ==> X=Y  (X Int Y <= 0)"; 
1894  143 
by (safe_tac (!claset addSIs [equiv_class_eq])); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

144 
by (assume_tac 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

145 
by (rewrite_goals_tac [equiv_def,trans_def,sym_def]); 
1894  146 
by (Fast_tac 1); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

147 
qed "quotient_disj"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

148 
**) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

149 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

150 
(**** Defining unary operations upon equivalence classes ****) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

151 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

152 
(* theorem needed to prove UN_equiv_class *) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

153 
goal Set.thy "!!A. [ a:A; ! y:A. b(y)=b(a) ] ==> (UN y:A. b(y))=b(a)"; 
1894  154 
by (fast_tac (!claset addSEs [equalityE] addSIs [equalityI]) 1); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

155 
qed "UN_singleton_lemma"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

156 
val UN_singleton = ballI RSN (2,UN_singleton_lemma); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

157 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

158 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

159 
(** These proofs really require as local premises 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

160 
equiv A r; congruent r b 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

161 
**) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

162 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

163 
(*Conversion rule*) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

164 
val prems as [equivA,bcong,_] = goal Equiv.thy 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

165 
"[ equiv A r; congruent r b; a: A ] ==> (UN x:r^^{a}. b(x)) = b(a)"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

166 
by (cut_facts_tac prems 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

167 
by (rtac UN_singleton 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

168 
by (rtac equiv_class_self 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

169 
by (assume_tac 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

170 
by (assume_tac 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

171 
by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]); 
1894  172 
by (Fast_tac 1); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

173 
qed "UN_equiv_class"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

174 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

175 
(*Resolve th against the "local" premises*) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

176 
val localize = RSLIST [equivA,bcong]; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

177 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

178 
(*type checking of UN x:r``{a}. b(x) *) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

179 
val _::_::prems = goalw Equiv.thy [quotient_def] 
1465  180 
"[ equiv A r; congruent r b; X: A/r; \ 
181 
\ !!x. x : A ==> b(x) : B ] \ 

925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

182 
\ ==> (UN x:X. b(x)) : B"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

183 
by (cut_facts_tac prems 1); 
1894  184 
by (safe_tac (!claset)); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

185 
by (rtac (localize UN_equiv_class RS ssubst) 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

186 
by (REPEAT (ares_tac prems 1)); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

187 
qed "UN_equiv_class_type"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

188 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

189 
(*Sufficient conditions for injectiveness. Could weaken premises! 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

190 
major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

191 
*) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

192 
val _::_::prems = goalw Equiv.thy [quotient_def] 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

193 
"[ equiv A r; congruent r b; \ 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

194 
\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \ 
1465  195 
\ !!x y. [ x:A; y:A; b(x)=b(y) ] ==> (x,y):r ] \ 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

196 
\ ==> X=Y"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

197 
by (cut_facts_tac prems 1); 
1894  198 
by (safe_tac ((!claset) delrules [equalityI])); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

199 
by (rtac (equivA RS equiv_class_eq) 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

200 
by (REPEAT (ares_tac prems 1)); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

201 
by (etac box_equals 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

202 
by (REPEAT (ares_tac [localize UN_equiv_class] 1)); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

203 
qed "UN_equiv_class_inject"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

204 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

205 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

206 
(**** Defining binary operations upon equivalence classes ****) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

207 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

208 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

209 
goalw Equiv.thy [congruent_def,congruent2_def,equiv_def,refl_def] 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

210 
"!!A r. [ equiv A r; congruent2 r b; a: A ] ==> congruent r (b a)"; 
1894  211 
by (Fast_tac 1); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

212 
qed "congruent2_implies_congruent"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

213 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

214 
val equivA::prems = goalw Equiv.thy [congruent_def] 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

215 
"[ equiv A r; congruent2 r b; a: A ] ==> \ 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

216 
\ congruent r (%x1. UN x2:r^^{a}. b x1 x2)"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

217 
by (cut_facts_tac (equivA::prems) 1); 
1894  218 
by (safe_tac (!claset)); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

219 
by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

220 
by (assume_tac 1); 
1266  221 
by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class, 
1465  222 
congruent2_implies_congruent]) 1); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

223 
by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]); 
1894  224 
by (Fast_tac 1); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

225 
qed "congruent2_implies_congruent_UN"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

226 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

227 
val prems as equivA::_ = goal Equiv.thy 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

228 
"[ equiv A r; congruent2 r b; a1: A; a2: A ] \ 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

229 
\ ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

230 
by (cut_facts_tac prems 1); 
1266  231 
by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class, 
1465  232 
congruent2_implies_congruent, 
233 
congruent2_implies_congruent_UN]) 1); 

925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

234 
qed "UN_equiv_class2"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

235 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

236 
(*type checking*) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

237 
val prems = goalw Equiv.thy [quotient_def] 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

238 
"[ equiv A r; congruent2 r b; \ 
1465  239 
\ X1: A/r; X2: A/r; \ 
240 
\ !!x1 x2. [ x1: A; x2: A ] ==> b x1 x2 : B ] \ 

925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

241 
\ ==> (UN x1:X1. UN x2:X2. b x1 x2) : B"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

242 
by (cut_facts_tac prems 1); 
1894  243 
by (safe_tac (!claset)); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

244 
by (REPEAT (ares_tac (prems@[UN_equiv_class_type, 
1465  245 
congruent2_implies_congruent_UN, 
246 
congruent2_implies_congruent, quotientI]) 1)); 

925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

247 
qed "UN_equiv_class_type2"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

248 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

249 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

250 
(*Suggested by John Harrison  the two subproofs may be MUCH simpler 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

251 
than the direct proof*) 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

252 
val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def] 
1465  253 
"[ equiv A r; \ 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset

254 
\ !! y z w. [ w: A; (y,z) : r ] ==> b y w = b z w; \ 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset

255 
\ !! y z w. [ w: A; (y,z) : r ] ==> b w y = b w z \ 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

256 
\ ] ==> congruent2 r b"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

257 
by (cut_facts_tac prems 1); 
1894  258 
by (safe_tac (!claset)); 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

259 
by (rtac trans 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

260 
by (REPEAT (ares_tac prems 1 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

261 
ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1)); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

262 
qed "congruent2I"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

263 

15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

264 
val [equivA,commute,congt] = goal Equiv.thy 
1465  265 
"[ equiv A r; \ 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

266 
\ !! y z. [ y: A; z: A ] ==> b y z = b z y; \ 
1465  267 
\ !! y z w. [ w: A; (y,z): r ] ==> b w y = b w z \ 
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

268 
\ ] ==> congruent2 r b"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

269 
by (resolve_tac [equivA RS congruent2I] 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

270 
by (rtac (commute RS trans) 1); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

271 
by (rtac (commute RS trans RS sym) 3); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

272 
by (rtac sym 5); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

273 
by (REPEAT (ares_tac [congt] 1 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

274 
ORELSE etac (equivA RS equiv_type RS subsetD RS SigmaE2) 1)); 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

275 
qed "congruent2_commuteI"; 
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset

276 