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