src/HOL/Integ/Equiv.ML
 author paulson Thu Aug 06 15:48:13 1998 +0200 (1998-08-06) changeset 5278 a903b66822e2 parent 5148 74919e8f221c child 6715 89891b0b596f permissions -rw-r--r--
even more tidying of Goal commands
 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` nipkow@3439 ` 15` ```(*** Suppes, Theorem 70: r is an equiv relation iff r^-1 O r = r ***) ``` clasohm@925 ` 16` nipkow@3439 ` 17` ```(** first half: equiv A r ==> r^-1 O r = r **) ``` clasohm@925 ` 18` wenzelm@5069 ` 19` ```Goalw [trans_def,sym_def,converse_def] ``` paulson@5148 ` 20` ``` "[| sym(r); trans(r) |] ==> r^-1 O r <= r"; ``` paulson@4746 ` 21` ```by (Blast_tac 1); ``` clasohm@925 ` 22` ```qed "sym_trans_comp_subset"; ``` clasohm@925 ` 23` wenzelm@5069 ` 24` ```Goalw [refl_def] ``` paulson@5148 ` 25` ``` "refl A r ==> r <= r^-1 O r"; ``` paulson@3718 ` 26` ```by (Blast_tac 1); ``` clasohm@925 ` 27` ```qed "refl_comp_subset"; ``` clasohm@925 ` 28` wenzelm@5069 ` 29` ```Goalw [equiv_def] ``` paulson@5148 ` 30` ``` "equiv A r ==> r^-1 O r = r"; ``` paulson@3718 ` 31` ```by (Clarify_tac 1); ``` clasohm@925 ` 32` ```by (rtac equalityI 1); ``` paulson@3718 ` 33` ```by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1)); ``` clasohm@925 ` 34` ```qed "equiv_comp_eq"; ``` clasohm@925 ` 35` clasohm@925 ` 36` ```(*second half*) ``` wenzelm@5069 ` 37` ```Goalw [equiv_def,refl_def,sym_def,trans_def] ``` paulson@5148 ` 38` ``` "[| r^-1 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@3718 ` 41` ```by (ALLGOALS Fast_tac); ``` 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*) ``` wenzelm@5069 ` 47` ```Goalw [equiv_def,trans_def,sym_def] ``` paulson@5148 ` 48` ``` "[| equiv A r; (a,b): r |] ==> r^^{a} <= r^^{b}"; ``` paulson@3718 ` 49` ```by (Blast_tac 1); ``` clasohm@925 ` 50` ```qed "equiv_class_subset"; ``` clasohm@925 ` 51` paulson@5143 ` 52` ```Goal "[| equiv A r; (a,b): r |] ==> r^^{a} = r^^{b}"; ``` clasohm@925 ` 53` ```by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1)); ``` clasohm@925 ` 54` ```by (rewrite_goals_tac [equiv_def,sym_def]); ``` paulson@3718 ` 55` ```by (Blast_tac 1); ``` clasohm@925 ` 56` ```qed "equiv_class_eq"; ``` clasohm@925 ` 57` wenzelm@5069 ` 58` ```Goalw [equiv_def,refl_def] ``` paulson@5148 ` 59` ``` "[| equiv A r; a: A |] ==> a: r^^{a}"; ``` paulson@3718 ` 60` ```by (Blast_tac 1); ``` clasohm@925 ` 61` ```qed "equiv_class_self"; ``` clasohm@925 ` 62` clasohm@925 ` 63` ```(*Lemma for the next result*) ``` wenzelm@5069 ` 64` ```Goalw [equiv_def,refl_def] ``` paulson@5148 ` 65` ``` "[| equiv A r; r^^{b} <= r^^{a}; b: A |] ==> (a,b): r"; ``` paulson@3718 ` 66` ```by (Blast_tac 1); ``` clasohm@925 ` 67` ```qed "subset_equiv_class"; ``` clasohm@925 ` 68` paulson@5278 ` 69` ```Goal "[| r^^{a} = r^^{b}; equiv A r; b: A |] ==> (a,b): r"; ``` paulson@2215 ` 70` ```by (REPEAT (ares_tac [equalityD2, subset_equiv_class] 1)); ``` clasohm@925 ` 71` ```qed "eq_equiv_class"; ``` clasohm@925 ` 72` clasohm@925 ` 73` ```(*thus r^^{a} = r^^{b} as well*) ``` wenzelm@5069 ` 74` ```Goalw [equiv_def,trans_def,sym_def] ``` paulson@5148 ` 75` ``` "[| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> (a,b): r"; ``` paulson@3718 ` 76` ```by (Blast_tac 1); ``` clasohm@925 ` 77` ```qed "equiv_class_nondisjoint"; ``` clasohm@925 ` 78` clasohm@925 ` 79` ```val [major] = goalw Equiv.thy [equiv_def,refl_def] ``` paulson@1642 ` 80` ``` "equiv A r ==> r <= A Times A"; ``` clasohm@925 ` 81` ```by (rtac (major RS conjunct1 RS conjunct1) 1); ``` clasohm@925 ` 82` ```qed "equiv_type"; ``` clasohm@925 ` 83` paulson@5278 ` 84` ```Goal "equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)"; ``` wenzelm@4089 ` 85` ```by (blast_tac (claset() addSIs [equiv_class_eq] ``` paulson@3718 ` 86` ``` addDs [eq_equiv_class, equiv_type]) 1); ``` clasohm@925 ` 87` ```qed "equiv_class_eq_iff"; ``` clasohm@925 ` 88` paulson@5278 ` 89` ```Goal "[| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)"; ``` wenzelm@4089 ` 90` ```by (blast_tac (claset() addSIs [equiv_class_eq] ``` paulson@3718 ` 91` ``` addDs [eq_equiv_class, equiv_type]) 1); ``` clasohm@925 ` 92` ```qed "eq_equiv_class_iff"; ``` clasohm@925 ` 93` clasohm@925 ` 94` ```(*** Quotients ***) ``` clasohm@925 ` 95` clasohm@925 ` 96` ```(** Introduction/elimination rules -- needed? **) ``` clasohm@925 ` 97` paulson@5143 ` 98` ```Goalw [quotient_def] "x:A ==> r^^{x}: A/r"; ``` paulson@3718 ` 99` ```by (Blast_tac 1); ``` clasohm@925 ` 100` ```qed "quotientI"; ``` clasohm@925 ` 101` clasohm@925 ` 102` ```val [major,minor] = goalw Equiv.thy [quotient_def] ``` clasohm@1465 ` 103` ``` "[| X:(A/r); !!x. [| X = r^^{x}; x:A |] ==> P |] \ ``` clasohm@925 ` 104` ```\ ==> P"; ``` clasohm@925 ` 105` ```by (resolve_tac [major RS UN_E] 1); ``` clasohm@925 ` 106` ```by (rtac minor 1); ``` clasohm@925 ` 107` ```by (assume_tac 2); ``` paulson@3718 ` 108` ```by (Fast_tac 1); (*Blast_tac FAILS to prove it*) ``` clasohm@925 ` 109` ```qed "quotientE"; ``` clasohm@925 ` 110` wenzelm@5069 ` 111` ```Goalw [equiv_def,refl_def,quotient_def] ``` paulson@5148 ` 112` ``` "equiv A r ==> Union(A/r) = A"; ``` wenzelm@4089 ` 113` ```by (blast_tac (claset() addSIs [equalityI]) 1); ``` clasohm@925 ` 114` ```qed "Union_quotient"; ``` clasohm@925 ` 115` wenzelm@5069 ` 116` ```Goalw [quotient_def] ``` paulson@5148 ` 117` ``` "[| equiv A r; X: A/r; Y: A/r |] ==> X=Y | (X Int Y = {})"; ``` wenzelm@4089 ` 118` ```by (safe_tac (claset() addSIs [equiv_class_eq])); ``` clasohm@925 ` 119` ```by (assume_tac 1); ``` clasohm@925 ` 120` ```by (rewrite_goals_tac [equiv_def,trans_def,sym_def]); ``` wenzelm@4089 ` 121` ```by (blast_tac (claset() addSIs [equalityI]) 1); ``` clasohm@925 ` 122` ```qed "quotient_disj"; ``` paulson@3358 ` 123` clasohm@925 ` 124` clasohm@925 ` 125` ```(**** Defining unary operations upon equivalence classes ****) ``` clasohm@925 ` 126` clasohm@925 ` 127` ```(* theorem needed to prove UN_equiv_class *) ``` clasohm@925 ` 128` ```goal Set.thy "!!A. [| a:A; ! y:A. b(y)=b(a) |] ==> (UN y:A. b(y))=b(a)"; ``` wenzelm@4089 ` 129` ```by (fast_tac (claset() addSEs [equalityE] addSIs [equalityI]) 1); ``` clasohm@925 ` 130` ```qed "UN_singleton_lemma"; ``` clasohm@925 ` 131` ```val UN_singleton = ballI RSN (2,UN_singleton_lemma); ``` clasohm@925 ` 132` clasohm@925 ` 133` paulson@2215 ` 134` ```(** These proofs really require the local premises ``` clasohm@925 ` 135` ``` equiv A r; congruent r b ``` clasohm@925 ` 136` ```**) ``` clasohm@925 ` 137` clasohm@925 ` 138` ```(*Conversion rule*) ``` paulson@5143 ` 139` ```Goal "[| equiv A r; congruent r b; a: A |] \ ``` paulson@2215 ` 140` ```\ ==> (UN x:r^^{a}. b(x)) = b(a)"; ``` paulson@2215 ` 141` ```by (rtac (equiv_class_self RS UN_singleton) 1 THEN REPEAT (assume_tac 1)); ``` clasohm@925 ` 142` ```by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]); ``` paulson@3718 ` 143` ```by (Blast_tac 1); ``` clasohm@925 ` 144` ```qed "UN_equiv_class"; ``` clasohm@925 ` 145` clasohm@925 ` 146` ```(*type checking of UN x:r``{a}. b(x) *) ``` paulson@2215 ` 147` ```val prems = goalw Equiv.thy [quotient_def] ``` clasohm@1465 ` 148` ``` "[| equiv A r; congruent r b; X: A/r; \ ``` paulson@2215 ` 149` ```\ !!x. x : A ==> b(x) : B |] \ ``` clasohm@925 ` 150` ```\ ==> (UN x:X. b(x)) : B"; ``` clasohm@925 ` 151` ```by (cut_facts_tac prems 1); ``` paulson@3718 ` 152` ```by (Clarify_tac 1); ``` paulson@2215 ` 153` ```by (stac UN_equiv_class 1); ``` clasohm@925 ` 154` ```by (REPEAT (ares_tac prems 1)); ``` clasohm@925 ` 155` ```qed "UN_equiv_class_type"; ``` clasohm@925 ` 156` clasohm@925 ` 157` ```(*Sufficient conditions for injectiveness. Could weaken premises! ``` clasohm@925 ` 158` ``` major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B ``` clasohm@925 ` 159` ```*) ``` paulson@2215 ` 160` ```val prems = goalw Equiv.thy [quotient_def] ``` clasohm@925 ` 161` ``` "[| equiv A r; congruent r b; \ ``` paulson@2215 ` 162` ```\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \ ``` clasohm@1465 ` 163` ```\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |] \ ``` clasohm@925 ` 164` ```\ ==> X=Y"; ``` clasohm@925 ` 165` ```by (cut_facts_tac prems 1); ``` paulson@3718 ` 166` ```by (Clarify_tac 1); ``` paulson@2215 ` 167` ```by (rtac equiv_class_eq 1); ``` clasohm@925 ` 168` ```by (REPEAT (ares_tac prems 1)); ``` clasohm@925 ` 169` ```by (etac box_equals 1); ``` paulson@2215 ` 170` ```by (REPEAT (ares_tac [UN_equiv_class] 1)); ``` clasohm@925 ` 171` ```qed "UN_equiv_class_inject"; ``` clasohm@925 ` 172` clasohm@925 ` 173` clasohm@925 ` 174` ```(**** Defining binary operations upon equivalence classes ****) ``` clasohm@925 ` 175` clasohm@925 ` 176` wenzelm@5069 ` 177` ```Goalw [congruent_def,congruent2_def,equiv_def,refl_def] ``` paulson@5148 ` 178` ``` "[| equiv A r; congruent2 r b; a: A |] ==> congruent r (b a)"; ``` paulson@3718 ` 179` ```by (Blast_tac 1); ``` clasohm@925 ` 180` ```qed "congruent2_implies_congruent"; ``` clasohm@925 ` 181` wenzelm@5069 ` 182` ```Goalw [congruent_def] ``` paulson@5148 ` 183` ``` "[| equiv A r; congruent2 r b; a: A |] ==> \ ``` clasohm@925 ` 184` ```\ congruent r (%x1. UN x2:r^^{a}. b x1 x2)"; ``` paulson@3718 ` 185` ```by (Clarify_tac 1); ``` paulson@2215 ` 186` ```by (rtac (equiv_type RS subsetD RS SigmaE2) 1 THEN REPEAT (assume_tac 1)); ``` wenzelm@4089 ` 187` ```by (asm_simp_tac (simpset() addsimps [UN_equiv_class, ``` clasohm@1465 ` 188` ``` congruent2_implies_congruent]) 1); ``` clasohm@925 ` 189` ```by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]); ``` paulson@3718 ` 190` ```by (Blast_tac 1); ``` clasohm@925 ` 191` ```qed "congruent2_implies_congruent_UN"; ``` clasohm@925 ` 192` paulson@5278 ` 193` ```Goal "[| equiv A r; congruent2 r b; a1: A; a2: A |] \ ``` clasohm@925 ` 194` ```\ ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2"; ``` wenzelm@4089 ` 195` ```by (asm_simp_tac (simpset() addsimps [UN_equiv_class, ``` clasohm@1465 ` 196` ``` congruent2_implies_congruent, ``` clasohm@1465 ` 197` ``` congruent2_implies_congruent_UN]) 1); ``` clasohm@925 ` 198` ```qed "UN_equiv_class2"; ``` clasohm@925 ` 199` clasohm@925 ` 200` ```(*type checking*) ``` clasohm@925 ` 201` ```val prems = goalw Equiv.thy [quotient_def] ``` clasohm@925 ` 202` ``` "[| equiv A r; congruent2 r b; \ ``` clasohm@1465 ` 203` ```\ X1: A/r; X2: A/r; \ ``` clasohm@1465 ` 204` ```\ !!x1 x2. [| x1: A; x2: A |] ==> b x1 x2 : B |] \ ``` clasohm@925 ` 205` ```\ ==> (UN x1:X1. UN x2:X2. b x1 x2) : B"; ``` clasohm@925 ` 206` ```by (cut_facts_tac prems 1); ``` paulson@3718 ` 207` ```by (Clarify_tac 1); ``` clasohm@925 ` 208` ```by (REPEAT (ares_tac (prems@[UN_equiv_class_type, ``` clasohm@1465 ` 209` ``` congruent2_implies_congruent_UN, ``` clasohm@1465 ` 210` ``` congruent2_implies_congruent, quotientI]) 1)); ``` clasohm@925 ` 211` ```qed "UN_equiv_class_type2"; ``` clasohm@925 ` 212` clasohm@925 ` 213` clasohm@925 ` 214` ```(*Suggested by John Harrison -- the two subproofs may be MUCH simpler ``` clasohm@925 ` 215` ``` than the direct proof*) ``` clasohm@925 ` 216` ```val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def] ``` clasohm@1465 ` 217` ``` "[| equiv A r; \ ``` clasohm@972 ` 218` ```\ !! y z w. [| w: A; (y,z) : r |] ==> b y w = b z w; \ ``` clasohm@972 ` 219` ```\ !! y z w. [| w: A; (y,z) : r |] ==> b w y = b w z \ ``` clasohm@925 ` 220` ```\ |] ==> congruent2 r b"; ``` clasohm@925 ` 221` ```by (cut_facts_tac prems 1); ``` paulson@3718 ` 222` ```by (Clarify_tac 1); ``` wenzelm@4089 ` 223` ```by (blast_tac (claset() addIs (trans::prems)) 1); ``` clasohm@925 ` 224` ```qed "congruent2I"; ``` clasohm@925 ` 225` clasohm@925 ` 226` ```val [equivA,commute,congt] = goal Equiv.thy ``` clasohm@1465 ` 227` ``` "[| equiv A r; \ ``` clasohm@925 ` 228` ```\ !! y z. [| y: A; z: A |] ==> b y z = b z y; \ ``` clasohm@1465 ` 229` ```\ !! y z w. [| w: A; (y,z): r |] ==> b w y = b w z \ ``` clasohm@925 ` 230` ```\ |] ==> congruent2 r b"; ``` clasohm@925 ` 231` ```by (resolve_tac [equivA RS congruent2I] 1); ``` clasohm@925 ` 232` ```by (rtac (commute RS trans) 1); ``` clasohm@925 ` 233` ```by (rtac (commute RS trans RS sym) 3); ``` clasohm@925 ` 234` ```by (rtac sym 5); ``` clasohm@925 ` 235` ```by (REPEAT (ares_tac [congt] 1 ``` clasohm@925 ` 236` ``` ORELSE etac (equivA RS equiv_type RS subsetD RS SigmaE2) 1)); ``` clasohm@925 ` 237` ```qed "congruent2_commuteI"; ``` clasohm@925 ` 238` paulson@3374 ` 239` wenzelm@4195 ` 240` ```(*** Cardinality results suggested by Florian Kammueller ***) ``` paulson@3374 ` 241` paulson@3374 ` 242` ```(*Recall that equiv A r implies r <= A Times A (equiv_type) *) ``` paulson@5143 ` 243` ```Goal "[| finite A; r <= A Times A |] ==> finite (A/r)"; ``` paulson@3374 ` 244` ```by (rtac finite_subset 1); ``` paulson@3374 ` 245` ```by (etac (finite_Pow_iff RS iffD2) 2); ``` paulson@3457 ` 246` ```by (rewtac quotient_def); ``` paulson@3374 ` 247` ```by (Blast_tac 1); ``` paulson@3374 ` 248` ```qed "finite_quotient"; ``` paulson@3374 ` 249` wenzelm@5069 ` 250` ```Goalw [quotient_def] ``` paulson@5148 ` 251` ``` "[| finite A; r <= A Times A; X : A/r |] ==> finite X"; ``` paulson@3374 ` 252` ```by (rtac finite_subset 1); ``` paulson@3457 ` 253` ```by (assume_tac 2); ``` paulson@3374 ` 254` ```by (Blast_tac 1); ``` paulson@3374 ` 255` ```qed "finite_equiv_class"; ``` paulson@3374 ` 256` paulson@5143 ` 257` ```Goal "[| finite A; equiv A r; ! X : A/r. k dvd card(X) |] \ ``` paulson@3374 ` 258` ```\ ==> k dvd card(A)"; ``` paulson@3374 ` 259` ```by (rtac (Union_quotient RS subst) 1); ``` paulson@3374 ` 260` ```by (assume_tac 1); ``` paulson@3374 ` 261` ```by (rtac dvd_partition 1); ``` wenzelm@4089 ` 262` ```by (blast_tac (claset() delrules [equalityI] addEs [quotient_disj RS disjE]) 4); ``` paulson@3374 ` 263` ```by (ALLGOALS ``` wenzelm@4089 ` 264` ``` (asm_simp_tac (simpset() addsimps [Union_quotient, equiv_type, ``` paulson@3374 ` 265` ``` finite_quotient]))); ``` paulson@3374 ` 266` ```qed "equiv_imp_dvd_card"; ```