src/ZF/ex/equiv.ML
 author clasohm Thu Sep 16 12:20:38 1993 +0200 (1993-09-16) changeset 0 a5a9c433f639 child 7 268f93ab3bc4 permissions -rw-r--r--
Initial revision
 clasohm@0 ` 1` ```(* Title: ZF/ex/equiv.ML ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@0 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 4` ``` Copyright 1993 University of Cambridge ``` clasohm@0 ` 5` clasohm@0 ` 6` ```For equiv.thy. Equivalence relations in Zermelo-Fraenkel Set Theory ``` clasohm@0 ` 7` ```*) ``` clasohm@0 ` 8` clasohm@0 ` 9` ```val RSLIST = curry (op MRS); ``` clasohm@0 ` 10` clasohm@0 ` 11` ```open Equiv; ``` clasohm@0 ` 12` clasohm@0 ` 13` ```(*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***) ``` clasohm@0 ` 14` clasohm@0 ` 15` ```(** first half: equiv(A,r) ==> converse(r) O r = r **) ``` clasohm@0 ` 16` clasohm@0 ` 17` ```goalw Equiv.thy [trans_def,sym_def] ``` clasohm@0 ` 18` ``` "!!r. [| sym(r); trans(r) |] ==> converse(r) O r <= r"; ``` clasohm@0 ` 19` ```by (fast_tac (ZF_cs addSEs [converseD,compE]) 1); ``` clasohm@0 ` 20` ```val sym_trans_comp_subset = result(); ``` clasohm@0 ` 21` clasohm@0 ` 22` ```goalw Equiv.thy [refl_def] ``` clasohm@0 ` 23` ``` "!!A r. refl(A,r) ==> r <= converse(r) O r"; ``` clasohm@0 ` 24` ```by (fast_tac (ZF_cs addSIs [converseI] addIs [compI]) 1); ``` clasohm@0 ` 25` ```val refl_comp_subset = result(); ``` clasohm@0 ` 26` clasohm@0 ` 27` ```goalw Equiv.thy [equiv_def] ``` clasohm@0 ` 28` ``` "!!A r. equiv(A,r) ==> converse(r) O r = r"; ``` clasohm@0 ` 29` ```by (rtac equalityI 1); ``` clasohm@0 ` 30` ```by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1 ``` clasohm@0 ` 31` ``` ORELSE etac conjE 1)); ``` clasohm@0 ` 32` ```val equiv_comp_eq = result(); ``` clasohm@0 ` 33` clasohm@0 ` 34` ```(*second half*) ``` clasohm@0 ` 35` ```goalw Equiv.thy [equiv_def,refl_def,sym_def,trans_def] ``` clasohm@0 ` 36` ``` "!!A r. [| converse(r) O r = r; domain(r) = A |] ==> equiv(A,r)"; ``` clasohm@0 ` 37` ```by (etac equalityE 1); ``` clasohm@0 ` 38` ```by (subgoal_tac "ALL x y. : r --> : r" 1); ``` clasohm@0 ` 39` ```by (safe_tac ZF_cs); ``` clasohm@0 ` 40` ```by (fast_tac (ZF_cs addSIs [converseI] addIs [compI]) 3); ``` clasohm@0 ` 41` ```by (ALLGOALS (fast_tac ``` clasohm@0 ` 42` ``` (ZF_cs addSIs [converseI] addIs [compI] addSEs [compE]))); ``` clasohm@0 ` 43` ```by flexflex_tac; ``` clasohm@0 ` 44` ```val comp_equivI = result(); ``` clasohm@0 ` 45` clasohm@0 ` 46` ```(** Equivalence classes **) ``` clasohm@0 ` 47` clasohm@0 ` 48` ```(*Lemma for the next result*) ``` clasohm@0 ` 49` ```goalw Equiv.thy [equiv_def,trans_def,sym_def] ``` clasohm@0 ` 50` ``` "!!A r. [| equiv(A,r); : r |] ==> r``{a} <= r``{b}"; ``` clasohm@0 ` 51` ```by (fast_tac ZF_cs 1); ``` clasohm@0 ` 52` ```val equiv_class_subset = result(); ``` clasohm@0 ` 53` clasohm@0 ` 54` ```goal Equiv.thy "!!A r. [| equiv(A,r); : r |] ==> r``{a} = r``{b}"; ``` clasohm@0 ` 55` ```by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1)); ``` clasohm@0 ` 56` ```by (rewrite_goals_tac [equiv_def,sym_def]); ``` clasohm@0 ` 57` ```by (fast_tac ZF_cs 1); ``` clasohm@0 ` 58` ```val equiv_class_eq = result(); ``` clasohm@0 ` 59` clasohm@0 ` 60` ```val prems = goalw Equiv.thy [equiv_def,refl_def] ``` clasohm@0 ` 61` ``` "[| equiv(A,r); a: A |] ==> a: r``{a}"; ``` clasohm@0 ` 62` ```by (cut_facts_tac prems 1); ``` clasohm@0 ` 63` ```by (fast_tac ZF_cs 1); ``` clasohm@0 ` 64` ```val equiv_class_self = result(); ``` clasohm@0 ` 65` clasohm@0 ` 66` ```(*Lemma for the next result*) ``` clasohm@0 ` 67` ```goalw Equiv.thy [equiv_def,refl_def] ``` clasohm@0 ` 68` ``` "!!A r. [| equiv(A,r); r``{b} <= r``{a}; b: A |] ==> : r"; ``` clasohm@0 ` 69` ```by (fast_tac ZF_cs 1); ``` clasohm@0 ` 70` ```val subset_equiv_class = result(); ``` clasohm@0 ` 71` clasohm@0 ` 72` ```val prems = goal Equiv.thy ``` clasohm@0 ` 73` ``` "[| r``{a} = r``{b}; equiv(A,r); b: A |] ==> : r"; ``` clasohm@0 ` 74` ```by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1)); ``` clasohm@0 ` 75` ```val eq_equiv_class = result(); ``` clasohm@0 ` 76` clasohm@0 ` 77` ```(*thus r``{a} = r``{b} as well*) ``` clasohm@0 ` 78` ```goalw Equiv.thy [equiv_def,trans_def,sym_def] ``` clasohm@0 ` 79` ``` "!!A r. [| equiv(A,r); x: (r``{a} Int r``{b}) |] ==> : r"; ``` clasohm@0 ` 80` ```by (fast_tac ZF_cs 1); ``` clasohm@0 ` 81` ```val equiv_class_nondisjoint = result(); ``` clasohm@0 ` 82` clasohm@0 ` 83` ```val [major] = goalw Equiv.thy [equiv_def,refl_def] ``` clasohm@0 ` 84` ``` "equiv(A,r) ==> r <= A*A"; ``` clasohm@0 ` 85` ```by (rtac (major RS conjunct1 RS conjunct1) 1); ``` clasohm@0 ` 86` ```val equiv_type = result(); ``` clasohm@0 ` 87` clasohm@0 ` 88` ```goal Equiv.thy ``` clasohm@0 ` 89` ``` "!!A r. equiv(A,r) ==> : r <-> r``{x} = r``{y} & x:A & y:A"; ``` clasohm@0 ` 90` ```by (fast_tac (ZF_cs addIs [eq_equiv_class, equiv_class_eq] ``` clasohm@0 ` 91` ``` addDs [equiv_type]) 1); ``` clasohm@0 ` 92` ```val equiv_class_eq_iff = result(); ``` clasohm@0 ` 93` clasohm@0 ` 94` ```goal Equiv.thy ``` clasohm@0 ` 95` ``` "!!A r. [| equiv(A,r); x: A; y: A |] ==> r``{x} = r``{y} <-> : r"; ``` clasohm@0 ` 96` ```by (fast_tac (ZF_cs addIs [eq_equiv_class, equiv_class_eq] ``` clasohm@0 ` 97` ``` addDs [equiv_type]) 1); ``` clasohm@0 ` 98` ```val eq_equiv_class_iff = result(); ``` clasohm@0 ` 99` clasohm@0 ` 100` ```(*** Quotients ***) ``` clasohm@0 ` 101` clasohm@0 ` 102` ```(** Introduction/elimination rules -- needed? **) ``` clasohm@0 ` 103` clasohm@0 ` 104` ```val prems = goalw Equiv.thy [quotient_def] "x:A ==> r``{x}: A/r"; ``` clasohm@0 ` 105` ```by (rtac RepFunI 1); ``` clasohm@0 ` 106` ```by (resolve_tac prems 1); ``` clasohm@0 ` 107` ```val quotientI = result(); ``` clasohm@0 ` 108` clasohm@0 ` 109` ```val major::prems = goalw Equiv.thy [quotient_def] ``` clasohm@0 ` 110` ``` "[| X: A/r; !!x. [| X = r``{x}; x:A |] ==> P |] \ ``` clasohm@0 ` 111` ```\ ==> P"; ``` clasohm@0 ` 112` ```by (rtac (major RS RepFunE) 1); ``` clasohm@0 ` 113` ```by (eresolve_tac prems 1); ``` clasohm@0 ` 114` ```by (assume_tac 1); ``` clasohm@0 ` 115` ```val quotientE = result(); ``` clasohm@0 ` 116` clasohm@0 ` 117` ```goalw Equiv.thy [equiv_def,refl_def,quotient_def] ``` clasohm@0 ` 118` ``` "!!A r. equiv(A,r) ==> Union(A/r) = A"; ``` clasohm@0 ` 119` ```by (fast_tac eq_cs 1); ``` clasohm@0 ` 120` ```val Union_quotient = result(); ``` clasohm@0 ` 121` clasohm@0 ` 122` ```goalw Equiv.thy [quotient_def] ``` clasohm@0 ` 123` ``` "!!A r. [| equiv(A,r); X: A/r; Y: A/r |] ==> X=Y | (X Int Y <= 0)"; ``` clasohm@0 ` 124` ```by (safe_tac (ZF_cs addSIs [equiv_class_eq])); ``` clasohm@0 ` 125` ```by (assume_tac 1); ``` clasohm@0 ` 126` ```by (rewrite_goals_tac [equiv_def,trans_def,sym_def]); ``` clasohm@0 ` 127` ```by (fast_tac ZF_cs 1); ``` clasohm@0 ` 128` ```val quotient_disj = result(); ``` clasohm@0 ` 129` clasohm@0 ` 130` ```(**** Defining unary operations upon equivalence classes ****) ``` clasohm@0 ` 131` clasohm@0 ` 132` ```(** These proofs really require as local premises ``` clasohm@0 ` 133` ``` equiv(A,r); congruent(r,b) ``` clasohm@0 ` 134` ```**) ``` clasohm@0 ` 135` clasohm@0 ` 136` ```(*Conversion rule*) ``` clasohm@0 ` 137` ```val prems as [equivA,bcong,_] = goal Equiv.thy ``` clasohm@0 ` 138` ``` "[| equiv(A,r); congruent(r,b); a: A |] ==> (UN x:r``{a}. b(x)) = b(a)"; ``` clasohm@0 ` 139` ```by (cut_facts_tac prems 1); ``` clasohm@0 ` 140` ```by (rtac UN_singleton 1); ``` clasohm@0 ` 141` ```by (etac equiv_class_self 1); ``` clasohm@0 ` 142` ```by (assume_tac 1); ``` clasohm@0 ` 143` ```by (rewrite_goals_tac [equiv_def,sym_def,congruent_def]); ``` clasohm@0 ` 144` ```by (fast_tac ZF_cs 1); ``` clasohm@0 ` 145` ```val UN_equiv_class = result(); ``` clasohm@0 ` 146` clasohm@0 ` 147` ```(*Resolve th against the "local" premises*) ``` clasohm@0 ` 148` ```val localize = RSLIST [equivA,bcong]; ``` clasohm@0 ` 149` clasohm@0 ` 150` ```(*type checking of UN x:r``{a}. b(x) *) ``` clasohm@0 ` 151` ```val _::_::prems = goalw Equiv.thy [quotient_def] ``` clasohm@0 ` 152` ``` "[| equiv(A,r); congruent(r,b); X: A/r; \ ``` clasohm@0 ` 153` ```\ !!x. x : A ==> b(x) : B |] \ ``` clasohm@0 ` 154` ```\ ==> (UN x:X. b(x)) : B"; ``` clasohm@0 ` 155` ```by (cut_facts_tac prems 1); ``` clasohm@0 ` 156` ```by (safe_tac ZF_cs); ``` clasohm@0 ` 157` ```by (rtac (localize UN_equiv_class RS ssubst) 1); ``` clasohm@0 ` 158` ```by (REPEAT (ares_tac prems 1)); ``` clasohm@0 ` 159` ```val UN_equiv_class_type = result(); ``` clasohm@0 ` 160` clasohm@0 ` 161` ```(*Sufficient conditions for injectiveness. Could weaken premises! ``` clasohm@0 ` 162` ``` major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B ``` clasohm@0 ` 163` ```*) ``` clasohm@0 ` 164` ```val _::_::prems = goalw Equiv.thy [quotient_def] ``` clasohm@0 ` 165` ``` "[| equiv(A,r); congruent(r,b); \ ``` clasohm@0 ` 166` ```\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \ ``` clasohm@0 ` 167` ```\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> :r |] \ ``` clasohm@0 ` 168` ```\ ==> X=Y"; ``` clasohm@0 ` 169` ```by (cut_facts_tac prems 1); ``` clasohm@0 ` 170` ```by (safe_tac ZF_cs); ``` clasohm@0 ` 171` ```by (rtac (equivA RS equiv_class_eq) 1); ``` clasohm@0 ` 172` ```by (REPEAT (ares_tac prems 1)); ``` clasohm@0 ` 173` ```by (etac box_equals 1); ``` clasohm@0 ` 174` ```by (REPEAT (ares_tac [localize UN_equiv_class] 1)); ``` clasohm@0 ` 175` ```val UN_equiv_class_inject = result(); ``` clasohm@0 ` 176` clasohm@0 ` 177` clasohm@0 ` 178` ```(**** Defining binary operations upon equivalence classes ****) ``` clasohm@0 ` 179` clasohm@0 ` 180` clasohm@0 ` 181` ```goalw Equiv.thy [congruent_def,congruent2_def,equiv_def,refl_def] ``` clasohm@0 ` 182` ``` "!!A r. [| equiv(A,r); congruent2(r,b); a: A |] ==> congruent(r,b(a))"; ``` clasohm@0 ` 183` ```by (fast_tac ZF_cs 1); ``` clasohm@0 ` 184` ```val congruent2_implies_congruent = result(); ``` clasohm@0 ` 185` clasohm@0 ` 186` ```val equivA::prems = goalw Equiv.thy [congruent_def] ``` clasohm@0 ` 187` ``` "[| equiv(A,r); congruent2(r,b); a: A |] ==> \ ``` clasohm@0 ` 188` ```\ congruent(r, %x1. UN x2:r``{a}. b(x1,x2))"; ``` clasohm@0 ` 189` ```by (cut_facts_tac (equivA::prems) 1); ``` clasohm@0 ` 190` ```by (safe_tac ZF_cs); ``` clasohm@0 ` 191` ```by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1); ``` clasohm@0 ` 192` ```by (assume_tac 1); ``` clasohm@0 ` 193` ```by (ASM_SIMP_TAC (ZF_ss addrews [equivA RS UN_equiv_class, ``` clasohm@0 ` 194` ``` congruent2_implies_congruent]) 1); ``` clasohm@0 ` 195` ```by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]); ``` clasohm@0 ` 196` ```by (fast_tac ZF_cs 1); ``` clasohm@0 ` 197` ```val congruent2_implies_congruent_UN = result(); ``` clasohm@0 ` 198` clasohm@0 ` 199` ```val prems as equivA::_ = goal Equiv.thy ``` clasohm@0 ` 200` ``` "[| equiv(A,r); congruent2(r,b); a1: A; a2: A |] \ ``` clasohm@0 ` 201` ```\ ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)"; ``` clasohm@0 ` 202` ```by (cut_facts_tac prems 1); ``` clasohm@0 ` 203` ```by (ASM_SIMP_TAC (ZF_ss addrews [equivA RS UN_equiv_class, ``` clasohm@0 ` 204` ``` congruent2_implies_congruent, ``` clasohm@0 ` 205` ``` congruent2_implies_congruent_UN]) 1); ``` clasohm@0 ` 206` ```val UN_equiv_class2 = result(); ``` clasohm@0 ` 207` clasohm@0 ` 208` ```(*type checking*) ``` clasohm@0 ` 209` ```val prems = goalw Equiv.thy [quotient_def] ``` clasohm@0 ` 210` ``` "[| equiv(A,r); congruent2(r,b); \ ``` clasohm@0 ` 211` ```\ X1: A/r; X2: A/r; \ ``` clasohm@0 ` 212` ```\ !!x1 x2. [| x1: A; x2: A |] ==> b(x1,x2) : B |] \ ``` clasohm@0 ` 213` ```\ ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B"; ``` clasohm@0 ` 214` ```by (cut_facts_tac prems 1); ``` clasohm@0 ` 215` ```by (safe_tac ZF_cs); ``` clasohm@0 ` 216` ```by (REPEAT (ares_tac (prems@[UN_equiv_class_type, ``` clasohm@0 ` 217` ``` congruent2_implies_congruent_UN, ``` clasohm@0 ` 218` ``` congruent2_implies_congruent, quotientI]) 1)); ``` clasohm@0 ` 219` ```val UN_equiv_class_type2 = result(); ``` clasohm@0 ` 220` clasohm@0 ` 221` clasohm@0 ` 222` ```(*Suggested by John Harrison -- the two subproofs may be MUCH simpler ``` clasohm@0 ` 223` ``` than the direct proof*) ``` clasohm@0 ` 224` ```val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def] ``` clasohm@0 ` 225` ``` "[| equiv(A,r); \ ``` clasohm@0 ` 226` ```\ !! y z w. [| w: A; : r |] ==> b(y,w) = b(z,w); \ ``` clasohm@0 ` 227` ```\ !! y z w. [| w: A; : r |] ==> b(w,y) = b(w,z) \ ``` clasohm@0 ` 228` ```\ |] ==> congruent2(r,b)"; ``` clasohm@0 ` 229` ```by (cut_facts_tac prems 1); ``` clasohm@0 ` 230` ```by (safe_tac ZF_cs); ``` clasohm@0 ` 231` ```by (rtac trans 1); ``` clasohm@0 ` 232` ```by (REPEAT (ares_tac prems 1 ``` clasohm@0 ` 233` ``` ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1)); ``` clasohm@0 ` 234` ```val congruent2I = result(); ``` clasohm@0 ` 235` clasohm@0 ` 236` ```val [equivA,commute,congt] = goal Equiv.thy ``` clasohm@0 ` 237` ``` "[| equiv(A,r); \ ``` clasohm@0 ` 238` ```\ !! y z w. [| y: A; z: A |] ==> b(y,z) = b(z,y); \ ``` clasohm@0 ` 239` ```\ !! y z w. [| w: A; : r |] ==> b(w,y) = b(w,z) \ ``` clasohm@0 ` 240` ```\ |] ==> congruent2(r,b)"; ``` clasohm@0 ` 241` ```by (resolve_tac [equivA RS congruent2I] 1); ``` clasohm@0 ` 242` ```by (rtac (commute RS trans) 1); ``` clasohm@0 ` 243` ```by (rtac (commute RS trans RS sym) 3); ``` clasohm@0 ` 244` ```by (rtac sym 5); ``` clasohm@0 ` 245` ```by (REPEAT (ares_tac [congt] 1 ``` clasohm@0 ` 246` ``` ORELSE etac (equivA RS equiv_type RS subsetD RS SigmaE2) 1)); ``` clasohm@0 ` 247` ```val congruent2_commuteI = result(); ``` clasohm@0 ` 248` clasohm@0 ` 249` ```(***OBSOLETE VERSION ``` clasohm@0 ` 250` ```(*Rules congruentI and congruentD would simplify use of rewriting below*) ``` clasohm@0 ` 251` ```val [equivA,ZinA,congt,commute] = goalw Equiv.thy [quotient_def] ``` clasohm@0 ` 252` ``` "[| equiv(A,r); Z: A/r; \ ``` clasohm@0 ` 253` ```\ !!w. [| w: A |] ==> congruent(r, %z.b(w,z)); \ ``` clasohm@0 ` 254` ```\ !!x y. [| x: A; y: A |] ==> b(y,x) = b(x,y) \ ``` clasohm@0 ` 255` ```\ |] ==> congruent(r, %w. UN z: Z. b(w,z))"; ``` clasohm@0 ` 256` ```val congt' = rewrite_rule [congruent_def] congt; ``` clasohm@0 ` 257` ```by (cut_facts_tac [ZinA,congt] 1); ``` clasohm@0 ` 258` ```by (rewtac congruent_def); ``` clasohm@0 ` 259` ```by (safe_tac ZF_cs); ``` clasohm@0 ` 260` ```by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1); ``` clasohm@0 ` 261` ```by (assume_tac 1); ``` clasohm@0 ` 262` ```by (ASM_SIMP_TAC (ZF_ss addrews [congt RS (equivA RS UN_equiv_class)]) 1); ``` clasohm@0 ` 263` ```by (rtac (commute RS trans) 1); ``` clasohm@0 ` 264` ```by (rtac (commute RS trans RS sym) 3); ``` clasohm@0 ` 265` ```by (rtac sym 5); ``` clasohm@0 ` 266` ```by (REPEAT (ares_tac [congt' RS spec RS spec RS mp] 1)); ``` clasohm@0 ` 267` ```val congruent_commuteI = result(); ``` clasohm@0 ` 268` ```***) ```