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