author | wenzelm |
Tue, 06 Jul 1999 21:14:34 +0200 | |
changeset 6910 | 7c3503ae3d78 |
parent 6715 | 89891b0b596f |
child 7375 | 2cb340e66d15 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: Equiv.ML |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
2215 | 3 |
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 |
Copyright 1996 University of Cambridge |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
5 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
6 |
Equivalence relations in HOL Set Theory |
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 |
|
1978 | 9 |
val RSLIST = curry (op MRS); |
10 |
||
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
11 |
open Equiv; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
12 |
|
1894 | 13 |
Delrules [equalityI]; |
14 |
||
3439 | 15 |
(*** Suppes, Theorem 70: r is an equiv relation iff r^-1 O r = r ***) |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
16 |
|
3439 | 17 |
(** first half: equiv A r ==> r^-1 O r = r **) |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
18 |
|
5069 | 19 |
Goalw [trans_def,sym_def,converse_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
20 |
"[| sym(r); trans(r) |] ==> r^-1 O r <= r"; |
4746 | 21 |
by (Blast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
22 |
qed "sym_trans_comp_subset"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
23 |
|
5069 | 24 |
Goalw [refl_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
25 |
"refl A r ==> r <= r^-1 O r"; |
3718 | 26 |
by (Blast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
27 |
qed "refl_comp_subset"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
28 |
|
5069 | 29 |
Goalw [equiv_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
30 |
"equiv A r ==> r^-1 O r = r"; |
3718 | 31 |
by (Clarify_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
32 |
by (rtac equalityI 1); |
3718 | 33 |
by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1)); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
34 |
qed "equiv_comp_eq"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
35 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
36 |
(*second half*) |
5069 | 37 |
Goalw [equiv_def,refl_def,sym_def,trans_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
38 |
"[| r^-1 O r = r; Domain(r) = A |] ==> equiv A r"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
39 |
by (etac equalityE 1); |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
40 |
by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1); |
3718 | 41 |
by (ALLGOALS Fast_tac); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
42 |
qed "comp_equivI"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
43 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
44 |
(** Equivalence classes **) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
45 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
46 |
(*Lemma for the next result*) |
5069 | 47 |
Goalw [equiv_def,trans_def,sym_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
48 |
"[| equiv A r; (a,b): r |] ==> r^^{a} <= r^^{b}"; |
3718 | 49 |
by (Blast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
50 |
qed "equiv_class_subset"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
51 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
52 |
Goal "[| 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
|
53 |
by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
54 |
by (rewrite_goals_tac [equiv_def,sym_def]); |
3718 | 55 |
by (Blast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
56 |
qed "equiv_class_eq"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
57 |
|
5069 | 58 |
Goalw [equiv_def,refl_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
59 |
"[| equiv A r; a: A |] ==> a: r^^{a}"; |
3718 | 60 |
by (Blast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
61 |
qed "equiv_class_self"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
62 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
63 |
(*Lemma for the next result*) |
5069 | 64 |
Goalw [equiv_def,refl_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
65 |
"[| equiv A r; r^^{b} <= r^^{a}; b: A |] ==> (a,b): r"; |
3718 | 66 |
by (Blast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
67 |
qed "subset_equiv_class"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
68 |
|
5278 | 69 |
Goal "[| r^^{a} = r^^{b}; equiv A r; b: A |] ==> (a,b): r"; |
2215 | 70 |
by (REPEAT (ares_tac [equalityD2, subset_equiv_class] 1)); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
71 |
qed "eq_equiv_class"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
72 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
73 |
(*thus r^^{a} = r^^{b} as well*) |
5069 | 74 |
Goalw [equiv_def,trans_def,sym_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
75 |
"[| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> (a,b): r"; |
3718 | 76 |
by (Blast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
77 |
qed "equiv_class_nondisjoint"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
78 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
79 |
val [major] = goalw Equiv.thy [equiv_def,refl_def] |
1642 | 80 |
"equiv A r ==> r <= A Times A"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
81 |
by (rtac (major RS conjunct1 RS conjunct1) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
82 |
qed "equiv_type"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
83 |
|
5278 | 84 |
Goal "equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)"; |
4089 | 85 |
by (blast_tac (claset() addSIs [equiv_class_eq] |
3718 | 86 |
addDs [eq_equiv_class, equiv_type]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
87 |
qed "equiv_class_eq_iff"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
88 |
|
5278 | 89 |
Goal "[| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)"; |
4089 | 90 |
by (blast_tac (claset() addSIs [equiv_class_eq] |
3718 | 91 |
addDs [eq_equiv_class, equiv_type]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
92 |
qed "eq_equiv_class_iff"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
93 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
94 |
(*** Quotients ***) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
95 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
96 |
(** Introduction/elimination rules -- needed? **) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
97 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
98 |
Goalw [quotient_def] "x:A ==> r^^{x}: A/r"; |
3718 | 99 |
by (Blast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
100 |
qed "quotientI"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
101 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
102 |
val [major,minor] = goalw Equiv.thy [quotient_def] |
1465 | 103 |
"[| 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
|
104 |
\ ==> P"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
105 |
by (resolve_tac [major RS UN_E] 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
106 |
by (rtac minor 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
107 |
by (assume_tac 2); |
3718 | 108 |
by (Fast_tac 1); (*Blast_tac FAILS to prove it*) |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
109 |
qed "quotientE"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
110 |
|
5069 | 111 |
Goalw [equiv_def,refl_def,quotient_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
112 |
"equiv A r ==> Union(A/r) = A"; |
4089 | 113 |
by (blast_tac (claset() addSIs [equalityI]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
114 |
qed "Union_quotient"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
115 |
|
5069 | 116 |
Goalw [quotient_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
117 |
"[| equiv A r; X: A/r; Y: A/r |] ==> X=Y | (X Int Y = {})"; |
4089 | 118 |
by (safe_tac (claset() addSIs [equiv_class_eq])); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
119 |
by (assume_tac 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
120 |
by (rewrite_goals_tac [equiv_def,trans_def,sym_def]); |
4089 | 121 |
by (blast_tac (claset() addSIs [equalityI]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
122 |
qed "quotient_disj"; |
3358
13f1df323daf
Restoration of the two "bypassed" theorems Union_quotient and quotient_disj
paulson
parents:
2215
diff
changeset
|
123 |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
124 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
125 |
(**** Defining unary operations upon equivalence classes ****) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
126 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
127 |
(* theorem needed to prove UN_equiv_class *) |
6715
89891b0b596f
UN_singleton->UN_constant_eq removes clash with other UN_singleton
paulson
parents:
5278
diff
changeset
|
128 |
goal Set.thy "!!A. [| a:A; ! y:A. b(y)=c |] ==> (UN y:A. b(y))=c"; |
4089 | 129 |
by (fast_tac (claset() addSEs [equalityE] addSIs [equalityI]) 1); |
6715
89891b0b596f
UN_singleton->UN_constant_eq removes clash with other UN_singleton
paulson
parents:
5278
diff
changeset
|
130 |
qed "UN_constant_eq"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
131 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
132 |
|
6715
89891b0b596f
UN_singleton->UN_constant_eq removes clash with other UN_singleton
paulson
parents:
5278
diff
changeset
|
133 |
(** Could introduce a LOCALE with the assumptions |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
134 |
equiv A r; congruent r b |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
135 |
**) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
136 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
137 |
(*Conversion rule*) |
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
138 |
Goal "[| equiv A r; congruent r b; a: A |] \ |
6715
89891b0b596f
UN_singleton->UN_constant_eq removes clash with other UN_singleton
paulson
parents:
5278
diff
changeset
|
139 |
\ ==> (UN x:r^^{a}. b(x)) = b(a)"; |
89891b0b596f
UN_singleton->UN_constant_eq removes clash with other UN_singleton
paulson
parents:
5278
diff
changeset
|
140 |
by (rtac (equiv_class_self RS UN_constant_eq) 1 THEN REPEAT (assume_tac 1)); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
141 |
by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]); |
3718 | 142 |
by (Blast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
143 |
qed "UN_equiv_class"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
144 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
145 |
(*type checking of UN x:r``{a}. b(x) *) |
2215 | 146 |
val prems = goalw Equiv.thy [quotient_def] |
1465 | 147 |
"[| equiv A r; congruent r b; X: A/r; \ |
2215 | 148 |
\ !!x. x : A ==> b(x) : B |] \ |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
149 |
\ ==> (UN x:X. b(x)) : B"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
150 |
by (cut_facts_tac prems 1); |
3718 | 151 |
by (Clarify_tac 1); |
2215 | 152 |
by (stac UN_equiv_class 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
153 |
by (REPEAT (ares_tac prems 1)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
154 |
qed "UN_equiv_class_type"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
155 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
156 |
(*Sufficient conditions for injectiveness. Could weaken premises! |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
157 |
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
|
158 |
*) |
2215 | 159 |
val prems = goalw Equiv.thy [quotient_def] |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
160 |
"[| equiv A r; congruent r b; \ |
2215 | 161 |
\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \ |
1465 | 162 |
\ !!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
|
163 |
\ ==> X=Y"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
164 |
by (cut_facts_tac prems 1); |
3718 | 165 |
by (Clarify_tac 1); |
2215 | 166 |
by (rtac equiv_class_eq 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
167 |
by (REPEAT (ares_tac prems 1)); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
168 |
by (etac box_equals 1); |
2215 | 169 |
by (REPEAT (ares_tac [UN_equiv_class] 1)); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
170 |
qed "UN_equiv_class_inject"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
171 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
172 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
173 |
(**** Defining binary operations upon equivalence classes ****) |
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 |
|
5069 | 176 |
Goalw [congruent_def,congruent2_def,equiv_def,refl_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
177 |
"[| equiv A r; congruent2 r b; a: A |] ==> congruent r (b a)"; |
3718 | 178 |
by (Blast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
179 |
qed "congruent2_implies_congruent"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
180 |
|
5069 | 181 |
Goalw [congruent_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
182 |
"[| equiv A r; congruent2 r b; a: A |] ==> \ |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
183 |
\ congruent r (%x1. UN x2:r^^{a}. b x1 x2)"; |
3718 | 184 |
by (Clarify_tac 1); |
2215 | 185 |
by (rtac (equiv_type RS subsetD RS SigmaE2) 1 THEN REPEAT (assume_tac 1)); |
4089 | 186 |
by (asm_simp_tac (simpset() addsimps [UN_equiv_class, |
1465 | 187 |
congruent2_implies_congruent]) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
188 |
by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]); |
3718 | 189 |
by (Blast_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
190 |
qed "congruent2_implies_congruent_UN"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
191 |
|
5278 | 192 |
Goal "[| equiv A r; congruent2 r b; a1: A; a2: A |] \ |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
193 |
\ ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2"; |
4089 | 194 |
by (asm_simp_tac (simpset() addsimps [UN_equiv_class, |
1465 | 195 |
congruent2_implies_congruent, |
196 |
congruent2_implies_congruent_UN]) 1); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
197 |
qed "UN_equiv_class2"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
198 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
199 |
(*type checking*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
200 |
val prems = goalw Equiv.thy [quotient_def] |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
201 |
"[| equiv A r; congruent2 r b; \ |
1465 | 202 |
\ X1: A/r; X2: A/r; \ |
203 |
\ !!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
|
204 |
\ ==> (UN x1:X1. UN x2:X2. b x1 x2) : B"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
205 |
by (cut_facts_tac prems 1); |
3718 | 206 |
by (Clarify_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
207 |
by (REPEAT (ares_tac (prems@[UN_equiv_class_type, |
1465 | 208 |
congruent2_implies_congruent_UN, |
209 |
congruent2_implies_congruent, quotientI]) 1)); |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
210 |
qed "UN_equiv_class_type2"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
211 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
212 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
213 |
(*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
|
214 |
than the direct proof*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
215 |
val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def] |
1465 | 216 |
"[| equiv A r; \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
217 |
\ !! 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
|
218 |
\ !! 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
|
219 |
\ |] ==> congruent2 r b"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
220 |
by (cut_facts_tac prems 1); |
3718 | 221 |
by (Clarify_tac 1); |
4089 | 222 |
by (blast_tac (claset() addIs (trans::prems)) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
223 |
qed "congruent2I"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
224 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
225 |
val [equivA,commute,congt] = goal Equiv.thy |
1465 | 226 |
"[| equiv A r; \ |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
227 |
\ !! y z. [| y: A; z: A |] ==> b y z = b z y; \ |
1465 | 228 |
\ !! 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
|
229 |
\ |] ==> congruent2 r b"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
230 |
by (resolve_tac [equivA RS congruent2I] 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
231 |
by (rtac (commute RS trans) 1); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
232 |
by (rtac (commute RS trans RS sym) 3); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
233 |
by (rtac sym 5); |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
234 |
by (REPEAT (ares_tac [congt] 1 |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
235 |
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
|
236 |
qed "congruent2_commuteI"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
237 |
|
3374
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
238 |
|
4195 | 239 |
(*** Cardinality results suggested by Florian Kammueller ***) |
3374
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
240 |
|
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
241 |
(*Recall that equiv A r implies r <= A Times A (equiv_type) *) |
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
242 |
Goal "[| finite A; r <= A Times A |] ==> finite (A/r)"; |
3374
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
243 |
by (rtac finite_subset 1); |
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
244 |
by (etac (finite_Pow_iff RS iffD2) 2); |
3457 | 245 |
by (rewtac quotient_def); |
3374
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
246 |
by (Blast_tac 1); |
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
247 |
qed "finite_quotient"; |
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
248 |
|
5069 | 249 |
Goalw [quotient_def] |
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
250 |
"[| finite A; r <= A Times A; X : A/r |] ==> finite X"; |
3374
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
251 |
by (rtac finite_subset 1); |
3457 | 252 |
by (assume_tac 2); |
3374
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
253 |
by (Blast_tac 1); |
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
254 |
qed "finite_equiv_class"; |
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
255 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
256 |
Goal "[| finite A; equiv A r; ! X : A/r. k dvd card(X) |] \ |
3374
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
257 |
\ ==> k dvd card(A)"; |
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
258 |
by (rtac (Union_quotient RS subst) 1); |
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
259 |
by (assume_tac 1); |
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
260 |
by (rtac dvd_partition 1); |
4089 | 261 |
by (blast_tac (claset() delrules [equalityI] addEs [quotient_disj RS disjE]) 4); |
3374
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
262 |
by (ALLGOALS |
4089 | 263 |
(asm_simp_tac (simpset() addsimps [Union_quotient, equiv_type, |
3374
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
264 |
finite_quotient]))); |
182a2b76d19e
New proofs about cardinality. Suggested by Florian Kammueller
paulson
parents:
3358
diff
changeset
|
265 |
qed "equiv_imp_dvd_card"; |