src/HOL/Integ/Equiv.ML
 author berghofe Tue Jul 30 17:33:26 1996 +0200 (1996-07-30) changeset 1894 c2c8279d40f0 parent 1844 791e79473966 child 1978 e7df069acb74 permissions -rw-r--r--
Classical tactics now use default claset.
 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` 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); ``` berghofe@1894 ` 41` ```by (safe_tac (!claset)); ``` 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}"; ``` berghofe@1894 ` 51` ```by (safe_tac (!claset)); ``` 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` clasohm@925 ` 63` ```val prems = goalw Equiv.thy [equiv_def,refl_def] ``` clasohm@925 ` 64` ``` "[| equiv A r; a: A |] ==> a: r^^{a}"; ``` clasohm@925 ` 65` ```by (cut_facts_tac prems 1); ``` berghofe@1894 ` 66` ```by (Fast_tac 1); ``` clasohm@925 ` 67` ```qed "equiv_class_self"; ``` clasohm@925 ` 68` clasohm@925 ` 69` ```(*Lemma for the next result*) ``` clasohm@925 ` 70` ```goalw Equiv.thy [equiv_def,refl_def] ``` clasohm@972 ` 71` ``` "!!A r. [| equiv A r; r^^{b} <= r^^{a}; b: A |] ==> (a,b): r"; ``` berghofe@1894 ` 72` ```by (Fast_tac 1); ``` clasohm@925 ` 73` ```qed "subset_equiv_class"; ``` clasohm@925 ` 74` clasohm@925 ` 75` ```val prems = goal Equiv.thy ``` clasohm@972 ` 76` ``` "[| r^^{a} = r^^{b}; equiv A r; b: A |] ==> (a,b): r"; ``` clasohm@925 ` 77` ```by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1)); ``` clasohm@925 ` 78` ```qed "eq_equiv_class"; ``` clasohm@925 ` 79` clasohm@925 ` 80` ```(*thus r^^{a} = r^^{b} as well*) ``` clasohm@925 ` 81` ```goalw Equiv.thy [equiv_def,trans_def,sym_def] ``` clasohm@972 ` 82` ``` "!!A r. [| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> (a,b): r"; ``` berghofe@1894 ` 83` ```by (Fast_tac 1); ``` clasohm@925 ` 84` ```qed "equiv_class_nondisjoint"; ``` clasohm@925 ` 85` clasohm@925 ` 86` ```val [major] = goalw Equiv.thy [equiv_def,refl_def] ``` paulson@1642 ` 87` ``` "equiv A r ==> r <= A Times A"; ``` clasohm@925 ` 88` ```by (rtac (major RS conjunct1 RS conjunct1) 1); ``` clasohm@925 ` 89` ```qed "equiv_type"; ``` clasohm@925 ` 90` clasohm@925 ` 91` ```goal Equiv.thy ``` clasohm@972 ` 92` ``` "!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)"; ``` berghofe@1894 ` 93` ```by (safe_tac (!claset)); ``` clasohm@925 ` 94` ```by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1)); ``` clasohm@925 ` 95` ```by ((rtac eq_equiv_class 3) THEN ``` clasohm@925 ` 96` ``` (assume_tac 4) THEN (assume_tac 4) THEN (assume_tac 3)); ``` clasohm@925 ` 97` ```by ((dtac equiv_type 1) THEN (dtac rev_subsetD 1) THEN ``` clasohm@925 ` 98` ``` (assume_tac 1) THEN (dtac SigmaD1 1) THEN (assume_tac 1)); ``` clasohm@925 ` 99` ```by ((dtac equiv_type 1) THEN (dtac rev_subsetD 1) THEN ``` clasohm@925 ` 100` ``` (assume_tac 1) THEN (dtac SigmaD2 1) THEN (assume_tac 1)); ``` clasohm@925 ` 101` ```qed "equiv_class_eq_iff"; ``` clasohm@925 ` 102` clasohm@925 ` 103` ```goal Equiv.thy ``` clasohm@972 ` 104` ``` "!!A r. [| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)"; ``` berghofe@1894 ` 105` ```by (safe_tac (!claset)); ``` clasohm@925 ` 106` ```by ((rtac eq_equiv_class 1) THEN ``` clasohm@925 ` 107` ``` (assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1)); ``` clasohm@925 ` 108` ```by ((rtac equiv_class_eq 1) THEN ``` clasohm@925 ` 109` ``` (assume_tac 1) THEN (assume_tac 1)); ``` clasohm@925 ` 110` ```qed "eq_equiv_class_iff"; ``` clasohm@925 ` 111` clasohm@925 ` 112` ```(*** Quotients ***) ``` clasohm@925 ` 113` clasohm@925 ` 114` ```(** Introduction/elimination rules -- needed? **) ``` clasohm@925 ` 115` clasohm@925 ` 116` ```val prems = goalw Equiv.thy [quotient_def] "x:A ==> r^^{x}: A/r"; ``` clasohm@925 ` 117` ```by (rtac UN_I 1); ``` clasohm@925 ` 118` ```by (resolve_tac prems 1); ``` clasohm@925 ` 119` ```by (rtac singletonI 1); ``` clasohm@925 ` 120` ```qed "quotientI"; ``` clasohm@925 ` 121` clasohm@925 ` 122` ```val [major,minor] = goalw Equiv.thy [quotient_def] ``` clasohm@1465 ` 123` ``` "[| X:(A/r); !!x. [| X = r^^{x}; x:A |] ==> P |] \ ``` clasohm@925 ` 124` ```\ ==> P"; ``` clasohm@925 ` 125` ```by (resolve_tac [major RS UN_E] 1); ``` clasohm@925 ` 126` ```by (rtac minor 1); ``` clasohm@925 ` 127` ```by (assume_tac 2); ``` berghofe@1894 ` 128` ```by (Fast_tac 1); ``` clasohm@925 ` 129` ```qed "quotientE"; ``` clasohm@925 ` 130` clasohm@925 ` 131` ```(** Not needed by Theory Integ --> bypassed **) ``` clasohm@925 ` 132` ```(**goalw Equiv.thy [equiv_def,refl_def,quotient_def] ``` clasohm@925 ` 133` ``` "!!A r. equiv A r ==> Union(A/r) = A"; ``` paulson@1844 ` 134` ```by (Fast_tac 1); ``` clasohm@925 ` 135` ```qed "Union_quotient"; ``` clasohm@925 ` 136` ```**) ``` clasohm@925 ` 137` clasohm@925 ` 138` ```(** Not needed by Theory Integ --> bypassed **) ``` clasohm@925 ` 139` ```(*goalw Equiv.thy [quotient_def] ``` clasohm@925 ` 140` ``` "!!A r. [| equiv A r; X: A/r; Y: A/r |] ==> X=Y | (X Int Y <= 0)"; ``` berghofe@1894 ` 141` ```by (safe_tac (!claset addSIs [equiv_class_eq])); ``` clasohm@925 ` 142` ```by (assume_tac 1); ``` clasohm@925 ` 143` ```by (rewrite_goals_tac [equiv_def,trans_def,sym_def]); ``` berghofe@1894 ` 144` ```by (Fast_tac 1); ``` clasohm@925 ` 145` ```qed "quotient_disj"; ``` clasohm@925 ` 146` ```**) ``` clasohm@925 ` 147` clasohm@925 ` 148` ```(**** Defining unary operations upon equivalence classes ****) ``` clasohm@925 ` 149` clasohm@925 ` 150` ```(* theorem needed to prove UN_equiv_class *) ``` clasohm@925 ` 151` ```goal Set.thy "!!A. [| a:A; ! y:A. b(y)=b(a) |] ==> (UN y:A. b(y))=b(a)"; ``` berghofe@1894 ` 152` ```by (fast_tac (!claset addSEs [equalityE] addSIs [equalityI]) 1); ``` clasohm@925 ` 153` ```qed "UN_singleton_lemma"; ``` clasohm@925 ` 154` ```val UN_singleton = ballI RSN (2,UN_singleton_lemma); ``` clasohm@925 ` 155` clasohm@925 ` 156` clasohm@925 ` 157` ```(** These proofs really require as local premises ``` clasohm@925 ` 158` ``` equiv A r; congruent r b ``` clasohm@925 ` 159` ```**) ``` clasohm@925 ` 160` clasohm@925 ` 161` ```(*Conversion rule*) ``` clasohm@925 ` 162` ```val prems as [equivA,bcong,_] = goal Equiv.thy ``` clasohm@925 ` 163` ``` "[| equiv A r; congruent r b; a: A |] ==> (UN x:r^^{a}. b(x)) = b(a)"; ``` clasohm@925 ` 164` ```by (cut_facts_tac prems 1); ``` clasohm@925 ` 165` ```by (rtac UN_singleton 1); ``` clasohm@925 ` 166` ```by (rtac equiv_class_self 1); ``` clasohm@925 ` 167` ```by (assume_tac 1); ``` clasohm@925 ` 168` ```by (assume_tac 1); ``` clasohm@925 ` 169` ```by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]); ``` berghofe@1894 ` 170` ```by (Fast_tac 1); ``` clasohm@925 ` 171` ```qed "UN_equiv_class"; ``` clasohm@925 ` 172` clasohm@925 ` 173` ```(*Resolve th against the "local" premises*) ``` clasohm@925 ` 174` ```val localize = RSLIST [equivA,bcong]; ``` clasohm@925 ` 175` clasohm@925 ` 176` ```(*type checking of UN x:r``{a}. b(x) *) ``` clasohm@925 ` 177` ```val _::_::prems = goalw Equiv.thy [quotient_def] ``` clasohm@1465 ` 178` ``` "[| equiv A r; congruent r b; X: A/r; \ ``` clasohm@1465 ` 179` ```\ !!x. x : A ==> b(x) : B |] \ ``` clasohm@925 ` 180` ```\ ==> (UN x:X. b(x)) : B"; ``` clasohm@925 ` 181` ```by (cut_facts_tac prems 1); ``` berghofe@1894 ` 182` ```by (safe_tac (!claset)); ``` clasohm@925 ` 183` ```by (rtac (localize UN_equiv_class RS ssubst) 1); ``` clasohm@925 ` 184` ```by (REPEAT (ares_tac prems 1)); ``` clasohm@925 ` 185` ```qed "UN_equiv_class_type"; ``` clasohm@925 ` 186` clasohm@925 ` 187` ```(*Sufficient conditions for injectiveness. Could weaken premises! ``` clasohm@925 ` 188` ``` major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B ``` clasohm@925 ` 189` ```*) ``` clasohm@925 ` 190` ```val _::_::prems = goalw Equiv.thy [quotient_def] ``` clasohm@925 ` 191` ``` "[| equiv A r; congruent r b; \ ``` clasohm@925 ` 192` ```\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \ ``` clasohm@1465 ` 193` ```\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |] \ ``` clasohm@925 ` 194` ```\ ==> X=Y"; ``` clasohm@925 ` 195` ```by (cut_facts_tac prems 1); ``` berghofe@1894 ` 196` ```by (safe_tac ((!claset) delrules [equalityI])); ``` clasohm@925 ` 197` ```by (rtac (equivA RS equiv_class_eq) 1); ``` clasohm@925 ` 198` ```by (REPEAT (ares_tac prems 1)); ``` clasohm@925 ` 199` ```by (etac box_equals 1); ``` clasohm@925 ` 200` ```by (REPEAT (ares_tac [localize UN_equiv_class] 1)); ``` clasohm@925 ` 201` ```qed "UN_equiv_class_inject"; ``` clasohm@925 ` 202` clasohm@925 ` 203` clasohm@925 ` 204` ```(**** Defining binary operations upon equivalence classes ****) ``` clasohm@925 ` 205` clasohm@925 ` 206` clasohm@925 ` 207` ```goalw Equiv.thy [congruent_def,congruent2_def,equiv_def,refl_def] ``` clasohm@925 ` 208` ``` "!!A r. [| equiv A r; congruent2 r b; a: A |] ==> congruent r (b a)"; ``` berghofe@1894 ` 209` ```by (Fast_tac 1); ``` clasohm@925 ` 210` ```qed "congruent2_implies_congruent"; ``` clasohm@925 ` 211` clasohm@925 ` 212` ```val equivA::prems = goalw Equiv.thy [congruent_def] ``` clasohm@925 ` 213` ``` "[| equiv A r; congruent2 r b; a: A |] ==> \ ``` clasohm@925 ` 214` ```\ congruent r (%x1. UN x2:r^^{a}. b x1 x2)"; ``` clasohm@925 ` 215` ```by (cut_facts_tac (equivA::prems) 1); ``` berghofe@1894 ` 216` ```by (safe_tac (!claset)); ``` clasohm@925 ` 217` ```by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1); ``` clasohm@925 ` 218` ```by (assume_tac 1); ``` clasohm@1266 ` 219` ```by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class, ``` clasohm@1465 ` 220` ``` congruent2_implies_congruent]) 1); ``` clasohm@925 ` 221` ```by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]); ``` berghofe@1894 ` 222` ```by (Fast_tac 1); ``` clasohm@925 ` 223` ```qed "congruent2_implies_congruent_UN"; ``` clasohm@925 ` 224` clasohm@925 ` 225` ```val prems as equivA::_ = goal Equiv.thy ``` clasohm@925 ` 226` ``` "[| equiv A r; congruent2 r b; a1: A; a2: A |] \ ``` clasohm@925 ` 227` ```\ ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2"; ``` clasohm@925 ` 228` ```by (cut_facts_tac prems 1); ``` clasohm@1266 ` 229` ```by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class, ``` clasohm@1465 ` 230` ``` congruent2_implies_congruent, ``` clasohm@1465 ` 231` ``` congruent2_implies_congruent_UN]) 1); ``` clasohm@925 ` 232` ```qed "UN_equiv_class2"; ``` clasohm@925 ` 233` clasohm@925 ` 234` ```(*type checking*) ``` clasohm@925 ` 235` ```val prems = goalw Equiv.thy [quotient_def] ``` clasohm@925 ` 236` ``` "[| equiv A r; congruent2 r b; \ ``` clasohm@1465 ` 237` ```\ X1: A/r; X2: A/r; \ ``` clasohm@1465 ` 238` ```\ !!x1 x2. [| x1: A; x2: A |] ==> b x1 x2 : B |] \ ``` clasohm@925 ` 239` ```\ ==> (UN x1:X1. UN x2:X2. b x1 x2) : B"; ``` clasohm@925 ` 240` ```by (cut_facts_tac prems 1); ``` berghofe@1894 ` 241` ```by (safe_tac (!claset)); ``` clasohm@925 ` 242` ```by (REPEAT (ares_tac (prems@[UN_equiv_class_type, ``` clasohm@1465 ` 243` ``` congruent2_implies_congruent_UN, ``` clasohm@1465 ` 244` ``` congruent2_implies_congruent, quotientI]) 1)); ``` clasohm@925 ` 245` ```qed "UN_equiv_class_type2"; ``` clasohm@925 ` 246` clasohm@925 ` 247` clasohm@925 ` 248` ```(*Suggested by John Harrison -- the two subproofs may be MUCH simpler ``` clasohm@925 ` 249` ``` than the direct proof*) ``` clasohm@925 ` 250` ```val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def] ``` clasohm@1465 ` 251` ``` "[| equiv A r; \ ``` clasohm@972 ` 252` ```\ !! y z w. [| w: A; (y,z) : r |] ==> b y w = b z w; \ ``` clasohm@972 ` 253` ```\ !! y z w. [| w: A; (y,z) : r |] ==> b w y = b w z \ ``` clasohm@925 ` 254` ```\ |] ==> congruent2 r b"; ``` clasohm@925 ` 255` ```by (cut_facts_tac prems 1); ``` berghofe@1894 ` 256` ```by (safe_tac (!claset)); ``` clasohm@925 ` 257` ```by (rtac trans 1); ``` clasohm@925 ` 258` ```by (REPEAT (ares_tac prems 1 ``` clasohm@925 ` 259` ``` ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1)); ``` clasohm@925 ` 260` ```qed "congruent2I"; ``` clasohm@925 ` 261` clasohm@925 ` 262` ```val [equivA,commute,congt] = goal Equiv.thy ``` clasohm@1465 ` 263` ``` "[| equiv A r; \ ``` clasohm@925 ` 264` ```\ !! y z. [| y: A; z: A |] ==> b y z = b z y; \ ``` clasohm@1465 ` 265` ```\ !! y z w. [| w: A; (y,z): r |] ==> b w y = b w z \ ``` clasohm@925 ` 266` ```\ |] ==> congruent2 r b"; ``` clasohm@925 ` 267` ```by (resolve_tac [equivA RS congruent2I] 1); ``` clasohm@925 ` 268` ```by (rtac (commute RS trans) 1); ``` clasohm@925 ` 269` ```by (rtac (commute RS trans RS sym) 3); ``` clasohm@925 ` 270` ```by (rtac sym 5); ``` clasohm@925 ` 271` ```by (REPEAT (ares_tac [congt] 1 ``` clasohm@925 ` 272` ``` ORELSE etac (equivA RS equiv_type RS subsetD RS SigmaE2) 1)); ``` clasohm@925 ` 273` ```qed "congruent2_commuteI"; ``` clasohm@925 ` 274`