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