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