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