src/HOL/Set.ML
 author clasohm Fri Mar 03 12:02:25 1995 +0100 (1995-03-03) changeset 923 ff1574a81019 child 1465 5d7a7e439cec permissions -rw-r--r--
new version of HOL with curried function application
 clasohm@923 ` 1` ```(* Title: HOL/set ``` clasohm@923 ` 2` ``` ID: \$Id\$ ``` clasohm@923 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@923 ` 4` ``` Copyright 1991 University of Cambridge ``` clasohm@923 ` 5` clasohm@923 ` 6` ```For set.thy. Set theory for higher-order logic. A set is simply a predicate. ``` clasohm@923 ` 7` ```*) ``` clasohm@923 ` 8` clasohm@923 ` 9` ```open Set; ``` clasohm@923 ` 10` clasohm@923 ` 11` ```val [prem] = goal Set.thy "[| P(a) |] ==> a : {x.P(x)}"; ``` clasohm@923 ` 12` ```by (rtac (mem_Collect_eq RS ssubst) 1); ``` clasohm@923 ` 13` ```by (rtac prem 1); ``` clasohm@923 ` 14` ```qed "CollectI"; ``` clasohm@923 ` 15` clasohm@923 ` 16` ```val prems = goal Set.thy "[| a : {x.P(x)} |] ==> P(a)"; ``` clasohm@923 ` 17` ```by (resolve_tac (prems RL [mem_Collect_eq RS subst]) 1); ``` clasohm@923 ` 18` ```qed "CollectD"; ``` clasohm@923 ` 19` clasohm@923 ` 20` ```val [prem] = goal Set.thy "[| !!x. (x:A) = (x:B) |] ==> A = B"; ``` clasohm@923 ` 21` ```by (rtac (prem RS ext RS arg_cong RS box_equals) 1); ``` clasohm@923 ` 22` ```by (rtac Collect_mem_eq 1); ``` clasohm@923 ` 23` ```by (rtac Collect_mem_eq 1); ``` clasohm@923 ` 24` ```qed "set_ext"; ``` clasohm@923 ` 25` clasohm@923 ` 26` ```val [prem] = goal Set.thy "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}"; ``` clasohm@923 ` 27` ```by (rtac (prem RS ext RS arg_cong) 1); ``` clasohm@923 ` 28` ```qed "Collect_cong"; ``` clasohm@923 ` 29` clasohm@923 ` 30` ```val CollectE = make_elim CollectD; ``` clasohm@923 ` 31` clasohm@923 ` 32` ```(*** Bounded quantifiers ***) ``` clasohm@923 ` 33` clasohm@923 ` 34` ```val prems = goalw Set.thy [Ball_def] ``` clasohm@923 ` 35` ``` "[| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)"; ``` clasohm@923 ` 36` ```by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); ``` clasohm@923 ` 37` ```qed "ballI"; ``` clasohm@923 ` 38` clasohm@923 ` 39` ```val [major,minor] = goalw Set.thy [Ball_def] ``` clasohm@923 ` 40` ``` "[| ! x:A. P(x); x:A |] ==> P(x)"; ``` clasohm@923 ` 41` ```by (rtac (minor RS (major RS spec RS mp)) 1); ``` clasohm@923 ` 42` ```qed "bspec"; ``` clasohm@923 ` 43` clasohm@923 ` 44` ```val major::prems = goalw Set.thy [Ball_def] ``` clasohm@923 ` 45` ``` "[| ! x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q"; ``` clasohm@923 ` 46` ```by (rtac (major RS spec RS impCE) 1); ``` clasohm@923 ` 47` ```by (REPEAT (eresolve_tac prems 1)); ``` clasohm@923 ` 48` ```qed "ballE"; ``` clasohm@923 ` 49` clasohm@923 ` 50` ```(*Takes assumptions ! x:A.P(x) and a:A; creates assumption P(a)*) ``` clasohm@923 ` 51` ```fun ball_tac i = etac ballE i THEN contr_tac (i+1); ``` clasohm@923 ` 52` clasohm@923 ` 53` ```val prems = goalw Set.thy [Bex_def] ``` clasohm@923 ` 54` ``` "[| P(x); x:A |] ==> ? x:A. P(x)"; ``` clasohm@923 ` 55` ```by (REPEAT (ares_tac (prems @ [exI,conjI]) 1)); ``` clasohm@923 ` 56` ```qed "bexI"; ``` clasohm@923 ` 57` clasohm@923 ` 58` ```qed_goal "bexCI" Set.thy ``` clasohm@923 ` 59` ``` "[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A.P(x)" ``` clasohm@923 ` 60` ``` (fn prems=> ``` clasohm@923 ` 61` ``` [ (rtac classical 1), ``` clasohm@923 ` 62` ``` (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); ``` clasohm@923 ` 63` clasohm@923 ` 64` ```val major::prems = goalw Set.thy [Bex_def] ``` clasohm@923 ` 65` ``` "[| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q"; ``` clasohm@923 ` 66` ```by (rtac (major RS exE) 1); ``` clasohm@923 ` 67` ```by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)); ``` clasohm@923 ` 68` ```qed "bexE"; ``` clasohm@923 ` 69` clasohm@923 ` 70` ```(*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) ``` clasohm@923 ` 71` ```val prems = goal Set.thy ``` clasohm@923 ` 72` ``` "(! x:A. True) = True"; ``` clasohm@923 ` 73` ```by (REPEAT (ares_tac [TrueI,ballI,iffI] 1)); ``` clasohm@923 ` 74` ```qed "ball_rew"; ``` clasohm@923 ` 75` clasohm@923 ` 76` ```(** Congruence rules **) ``` clasohm@923 ` 77` clasohm@923 ` 78` ```val prems = goal Set.thy ``` clasohm@923 ` 79` ``` "[| A=B; !!x. x:B ==> P(x) = Q(x) |] ==> \ ``` clasohm@923 ` 80` ```\ (! x:A. P(x)) = (! x:B. Q(x))"; ``` clasohm@923 ` 81` ```by (resolve_tac (prems RL [ssubst]) 1); ``` clasohm@923 ` 82` ```by (REPEAT (ares_tac [ballI,iffI] 1 ``` clasohm@923 ` 83` ``` ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1)); ``` clasohm@923 ` 84` ```qed "ball_cong"; ``` clasohm@923 ` 85` clasohm@923 ` 86` ```val prems = goal Set.thy ``` clasohm@923 ` 87` ``` "[| A=B; !!x. x:B ==> P(x) = Q(x) |] ==> \ ``` clasohm@923 ` 88` ```\ (? x:A. P(x)) = (? x:B. Q(x))"; ``` clasohm@923 ` 89` ```by (resolve_tac (prems RL [ssubst]) 1); ``` clasohm@923 ` 90` ```by (REPEAT (etac bexE 1 ``` clasohm@923 ` 91` ``` ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1)); ``` clasohm@923 ` 92` ```qed "bex_cong"; ``` clasohm@923 ` 93` clasohm@923 ` 94` ```(*** Subsets ***) ``` clasohm@923 ` 95` clasohm@923 ` 96` ```val prems = goalw Set.thy [subset_def] "(!!x.x:A ==> x:B) ==> A <= B"; ``` clasohm@923 ` 97` ```by (REPEAT (ares_tac (prems @ [ballI]) 1)); ``` clasohm@923 ` 98` ```qed "subsetI"; ``` clasohm@923 ` 99` clasohm@923 ` 100` ```(*Rule in Modus Ponens style*) ``` clasohm@923 ` 101` ```val major::prems = goalw Set.thy [subset_def] "[| A <= B; c:A |] ==> c:B"; ``` clasohm@923 ` 102` ```by (rtac (major RS bspec) 1); ``` clasohm@923 ` 103` ```by (resolve_tac prems 1); ``` clasohm@923 ` 104` ```qed "subsetD"; ``` clasohm@923 ` 105` clasohm@923 ` 106` ```(*The same, with reversed premises for use with etac -- cf rev_mp*) ``` clasohm@923 ` 107` ```qed_goal "rev_subsetD" Set.thy "[| c:A; A <= B |] ==> c:B" ``` clasohm@923 ` 108` ``` (fn prems=> [ (REPEAT (resolve_tac (prems@[subsetD]) 1)) ]); ``` clasohm@923 ` 109` clasohm@923 ` 110` ```(*Classical elimination rule*) ``` clasohm@923 ` 111` ```val major::prems = goalw Set.thy [subset_def] ``` clasohm@923 ` 112` ``` "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P"; ``` clasohm@923 ` 113` ```by (rtac (major RS ballE) 1); ``` clasohm@923 ` 114` ```by (REPEAT (eresolve_tac prems 1)); ``` clasohm@923 ` 115` ```qed "subsetCE"; ``` clasohm@923 ` 116` clasohm@923 ` 117` ```(*Takes assumptions A<=B; c:A and creates the assumption c:B *) ``` clasohm@923 ` 118` ```fun set_mp_tac i = etac subsetCE i THEN mp_tac i; ``` clasohm@923 ` 119` clasohm@923 ` 120` ```qed_goal "subset_refl" Set.thy "A <= (A::'a set)" ``` clasohm@923 ` 121` ``` (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]); ``` clasohm@923 ` 122` clasohm@923 ` 123` ```val prems = goal Set.thy "[| A<=B; B<=C |] ==> A<=(C::'a set)"; ``` clasohm@923 ` 124` ```by (cut_facts_tac prems 1); ``` clasohm@923 ` 125` ```by (REPEAT (ares_tac [subsetI] 1 ORELSE set_mp_tac 1)); ``` clasohm@923 ` 126` ```qed "subset_trans"; ``` clasohm@923 ` 127` clasohm@923 ` 128` clasohm@923 ` 129` ```(*** Equality ***) ``` clasohm@923 ` 130` clasohm@923 ` 131` ```(*Anti-symmetry of the subset relation*) ``` clasohm@923 ` 132` ```val prems = goal Set.thy "[| A <= B; B <= A |] ==> A = (B::'a set)"; ``` clasohm@923 ` 133` ```by (rtac (iffI RS set_ext) 1); ``` clasohm@923 ` 134` ```by (REPEAT (ares_tac (prems RL [subsetD]) 1)); ``` clasohm@923 ` 135` ```qed "subset_antisym"; ``` clasohm@923 ` 136` ```val equalityI = subset_antisym; ``` clasohm@923 ` 137` clasohm@923 ` 138` ```(* Equality rules from ZF set theory -- are they appropriate here? *) ``` clasohm@923 ` 139` ```val prems = goal Set.thy "A = B ==> A<=(B::'a set)"; ``` clasohm@923 ` 140` ```by (resolve_tac (prems RL [subst]) 1); ``` clasohm@923 ` 141` ```by (rtac subset_refl 1); ``` clasohm@923 ` 142` ```qed "equalityD1"; ``` clasohm@923 ` 143` clasohm@923 ` 144` ```val prems = goal Set.thy "A = B ==> B<=(A::'a set)"; ``` clasohm@923 ` 145` ```by (resolve_tac (prems RL [subst]) 1); ``` clasohm@923 ` 146` ```by (rtac subset_refl 1); ``` clasohm@923 ` 147` ```qed "equalityD2"; ``` clasohm@923 ` 148` clasohm@923 ` 149` ```val prems = goal Set.thy ``` clasohm@923 ` 150` ``` "[| A = B; [| A<=B; B<=(A::'a set) |] ==> P |] ==> P"; ``` clasohm@923 ` 151` ```by (resolve_tac prems 1); ``` clasohm@923 ` 152` ```by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1)); ``` clasohm@923 ` 153` ```qed "equalityE"; ``` clasohm@923 ` 154` clasohm@923 ` 155` ```val major::prems = goal Set.thy ``` clasohm@923 ` 156` ``` "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P"; ``` clasohm@923 ` 157` ```by (rtac (major RS equalityE) 1); ``` clasohm@923 ` 158` ```by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)); ``` clasohm@923 ` 159` ```qed "equalityCE"; ``` clasohm@923 ` 160` clasohm@923 ` 161` ```(*Lemma for creating induction formulae -- for "pattern matching" on p ``` clasohm@923 ` 162` ``` To make the induction hypotheses usable, apply "spec" or "bspec" to ``` clasohm@923 ` 163` ``` put universal quantifiers over the free variables in p. *) ``` clasohm@923 ` 164` ```val prems = goal Set.thy ``` clasohm@923 ` 165` ``` "[| p:A; !!z. z:A ==> p=z --> R |] ==> R"; ``` clasohm@923 ` 166` ```by (rtac mp 1); ``` clasohm@923 ` 167` ```by (REPEAT (resolve_tac (refl::prems) 1)); ``` clasohm@923 ` 168` ```qed "setup_induction"; ``` clasohm@923 ` 169` clasohm@923 ` 170` clasohm@923 ` 171` ```(*** Set complement -- Compl ***) ``` clasohm@923 ` 172` clasohm@923 ` 173` ```val prems = goalw Set.thy [Compl_def] ``` clasohm@923 ` 174` ``` "[| c:A ==> False |] ==> c : Compl(A)"; ``` clasohm@923 ` 175` ```by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1)); ``` clasohm@923 ` 176` ```qed "ComplI"; ``` clasohm@923 ` 177` clasohm@923 ` 178` ```(*This form, with negated conclusion, works well with the Classical prover. ``` clasohm@923 ` 179` ``` Negated assumptions behave like formulae on the right side of the notional ``` clasohm@923 ` 180` ``` turnstile...*) ``` clasohm@923 ` 181` ```val major::prems = goalw Set.thy [Compl_def] ``` clasohm@923 ` 182` ``` "[| c : Compl(A) |] ==> c~:A"; ``` clasohm@923 ` 183` ```by (rtac (major RS CollectD) 1); ``` clasohm@923 ` 184` ```qed "ComplD"; ``` clasohm@923 ` 185` clasohm@923 ` 186` ```val ComplE = make_elim ComplD; ``` clasohm@923 ` 187` clasohm@923 ` 188` clasohm@923 ` 189` ```(*** Binary union -- Un ***) ``` clasohm@923 ` 190` clasohm@923 ` 191` ```val prems = goalw Set.thy [Un_def] "c:A ==> c : A Un B"; ``` clasohm@923 ` 192` ```by (REPEAT (resolve_tac (prems @ [CollectI,disjI1]) 1)); ``` clasohm@923 ` 193` ```qed "UnI1"; ``` clasohm@923 ` 194` clasohm@923 ` 195` ```val prems = goalw Set.thy [Un_def] "c:B ==> c : A Un B"; ``` clasohm@923 ` 196` ```by (REPEAT (resolve_tac (prems @ [CollectI,disjI2]) 1)); ``` clasohm@923 ` 197` ```qed "UnI2"; ``` clasohm@923 ` 198` clasohm@923 ` 199` ```(*Classical introduction rule: no commitment to A vs B*) ``` clasohm@923 ` 200` ```qed_goal "UnCI" Set.thy "(c~:B ==> c:A) ==> c : A Un B" ``` clasohm@923 ` 201` ``` (fn prems=> ``` clasohm@923 ` 202` ``` [ (rtac classical 1), ``` clasohm@923 ` 203` ``` (REPEAT (ares_tac (prems@[UnI1,notI]) 1)), ``` clasohm@923 ` 204` ``` (REPEAT (ares_tac (prems@[UnI2,notE]) 1)) ]); ``` clasohm@923 ` 205` clasohm@923 ` 206` ```val major::prems = goalw Set.thy [Un_def] ``` clasohm@923 ` 207` ``` "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"; ``` clasohm@923 ` 208` ```by (rtac (major RS CollectD RS disjE) 1); ``` clasohm@923 ` 209` ```by (REPEAT (eresolve_tac prems 1)); ``` clasohm@923 ` 210` ```qed "UnE"; ``` clasohm@923 ` 211` clasohm@923 ` 212` clasohm@923 ` 213` ```(*** Binary intersection -- Int ***) ``` clasohm@923 ` 214` clasohm@923 ` 215` ```val prems = goalw Set.thy [Int_def] ``` clasohm@923 ` 216` ``` "[| c:A; c:B |] ==> c : A Int B"; ``` clasohm@923 ` 217` ```by (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1)); ``` clasohm@923 ` 218` ```qed "IntI"; ``` clasohm@923 ` 219` clasohm@923 ` 220` ```val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:A"; ``` clasohm@923 ` 221` ```by (rtac (major RS CollectD RS conjunct1) 1); ``` clasohm@923 ` 222` ```qed "IntD1"; ``` clasohm@923 ` 223` clasohm@923 ` 224` ```val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:B"; ``` clasohm@923 ` 225` ```by (rtac (major RS CollectD RS conjunct2) 1); ``` clasohm@923 ` 226` ```qed "IntD2"; ``` clasohm@923 ` 227` clasohm@923 ` 228` ```val [major,minor] = goal Set.thy ``` clasohm@923 ` 229` ``` "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"; ``` clasohm@923 ` 230` ```by (rtac minor 1); ``` clasohm@923 ` 231` ```by (rtac (major RS IntD1) 1); ``` clasohm@923 ` 232` ```by (rtac (major RS IntD2) 1); ``` clasohm@923 ` 233` ```qed "IntE"; ``` clasohm@923 ` 234` clasohm@923 ` 235` clasohm@923 ` 236` ```(*** Set difference ***) ``` clasohm@923 ` 237` clasohm@923 ` 238` ```qed_goalw "DiffI" Set.thy [set_diff_def] ``` clasohm@923 ` 239` ``` "[| c : A; c ~: B |] ==> c : A - B" ``` clasohm@923 ` 240` ``` (fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1)) ]); ``` clasohm@923 ` 241` clasohm@923 ` 242` ```qed_goalw "DiffD1" Set.thy [set_diff_def] ``` clasohm@923 ` 243` ``` "c : A - B ==> c : A" ``` clasohm@923 ` 244` ``` (fn [major]=> [ (rtac (major RS CollectD RS conjunct1) 1) ]); ``` clasohm@923 ` 245` clasohm@923 ` 246` ```qed_goalw "DiffD2" Set.thy [set_diff_def] ``` clasohm@923 ` 247` ``` "[| c : A - B; c : B |] ==> P" ``` clasohm@923 ` 248` ``` (fn [major,minor]=> ``` clasohm@923 ` 249` ``` [rtac (minor RS (major RS CollectD RS conjunct2 RS notE)) 1]); ``` clasohm@923 ` 250` clasohm@923 ` 251` ```qed_goal "DiffE" Set.thy ``` clasohm@923 ` 252` ``` "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P" ``` clasohm@923 ` 253` ``` (fn prems=> ``` clasohm@923 ` 254` ``` [ (resolve_tac prems 1), ``` clasohm@923 ` 255` ``` (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]); ``` clasohm@923 ` 256` clasohm@923 ` 257` ```qed_goal "Diff_iff" Set.thy "(c : A-B) = (c:A & c~:B)" ``` clasohm@923 ` 258` ``` (fn _ => [ (fast_tac (HOL_cs addSIs [DiffI] addSEs [DiffE]) 1) ]); ``` clasohm@923 ` 259` clasohm@923 ` 260` clasohm@923 ` 261` ```(*** The empty set -- {} ***) ``` clasohm@923 ` 262` clasohm@923 ` 263` ```qed_goalw "emptyE" Set.thy [empty_def] "a:{} ==> P" ``` clasohm@923 ` 264` ``` (fn [prem] => [rtac (prem RS CollectD RS FalseE) 1]); ``` clasohm@923 ` 265` clasohm@923 ` 266` ```qed_goal "empty_subsetI" Set.thy "{} <= A" ``` clasohm@923 ` 267` ``` (fn _ => [ (REPEAT (ares_tac [equalityI,subsetI,emptyE] 1)) ]); ``` clasohm@923 ` 268` clasohm@923 ` 269` ```qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}" ``` clasohm@923 ` 270` ``` (fn prems=> ``` clasohm@923 ` 271` ``` [ (REPEAT (ares_tac (prems@[empty_subsetI,subsetI,equalityI]) 1 ``` clasohm@923 ` 272` ``` ORELSE eresolve_tac (prems RL [FalseE]) 1)) ]); ``` clasohm@923 ` 273` clasohm@923 ` 274` ```qed_goal "equals0D" Set.thy "[| A={}; a:A |] ==> P" ``` clasohm@923 ` 275` ``` (fn [major,minor]=> ``` clasohm@923 ` 276` ``` [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]); ``` clasohm@923 ` 277` clasohm@923 ` 278` clasohm@923 ` 279` ```(*** Augmenting a set -- insert ***) ``` clasohm@923 ` 280` clasohm@923 ` 281` ```qed_goalw "insertI1" Set.thy [insert_def] "a : insert a B" ``` clasohm@923 ` 282` ``` (fn _ => [rtac (CollectI RS UnI1) 1, rtac refl 1]); ``` clasohm@923 ` 283` clasohm@923 ` 284` ```qed_goalw "insertI2" Set.thy [insert_def] "a : B ==> a : insert b B" ``` clasohm@923 ` 285` ``` (fn [prem]=> [ (rtac (prem RS UnI2) 1) ]); ``` clasohm@923 ` 286` clasohm@923 ` 287` ```qed_goalw "insertE" Set.thy [insert_def] ``` clasohm@923 ` 288` ``` "[| a : insert b A; a=b ==> P; a:A ==> P |] ==> P" ``` clasohm@923 ` 289` ``` (fn major::prems=> ``` clasohm@923 ` 290` ``` [ (rtac (major RS UnE) 1), ``` clasohm@923 ` 291` ``` (REPEAT (eresolve_tac (prems @ [CollectE]) 1)) ]); ``` clasohm@923 ` 292` clasohm@923 ` 293` ```qed_goal "insert_iff" Set.thy "a : insert b A = (a=b | a:A)" ``` clasohm@923 ` 294` ``` (fn _ => [fast_tac (HOL_cs addIs [insertI1,insertI2] addSEs [insertE]) 1]); ``` clasohm@923 ` 295` clasohm@923 ` 296` ```(*Classical introduction rule*) ``` clasohm@923 ` 297` ```qed_goal "insertCI" Set.thy "(a~:B ==> a=b) ==> a: insert b B" ``` clasohm@923 ` 298` ``` (fn [prem]=> ``` clasohm@923 ` 299` ``` [ (rtac (disjCI RS (insert_iff RS iffD2)) 1), ``` clasohm@923 ` 300` ``` (etac prem 1) ]); ``` clasohm@923 ` 301` clasohm@923 ` 302` ```(*** Singletons, using insert ***) ``` clasohm@923 ` 303` clasohm@923 ` 304` ```qed_goal "singletonI" Set.thy "a : {a}" ``` clasohm@923 ` 305` ``` (fn _=> [ (rtac insertI1 1) ]); ``` clasohm@923 ` 306` clasohm@923 ` 307` ```qed_goal "singletonE" Set.thy "[| a: {b}; a=b ==> P |] ==> P" ``` clasohm@923 ` 308` ``` (fn major::prems=> ``` clasohm@923 ` 309` ``` [ (rtac (major RS insertE) 1), ``` clasohm@923 ` 310` ``` (REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]); ``` clasohm@923 ` 311` clasohm@923 ` 312` ```goalw Set.thy [insert_def] "!!a. b : {a} ==> b=a"; ``` clasohm@923 ` 313` ```by(fast_tac (HOL_cs addSEs [emptyE,CollectE,UnE]) 1); ``` clasohm@923 ` 314` ```qed "singletonD"; ``` clasohm@923 ` 315` clasohm@923 ` 316` ```val singletonE = make_elim singletonD; ``` clasohm@923 ` 317` clasohm@923 ` 318` ```val [major] = goal Set.thy "{a}={b} ==> a=b"; ``` clasohm@923 ` 319` ```by (rtac (major RS equalityD1 RS subsetD RS singletonD) 1); ``` clasohm@923 ` 320` ```by (rtac singletonI 1); ``` clasohm@923 ` 321` ```qed "singleton_inject"; ``` clasohm@923 ` 322` clasohm@923 ` 323` ```(*** Unions of families -- UNION x:A. B(x) is Union(B``A) ***) ``` clasohm@923 ` 324` clasohm@923 ` 325` ```(*The order of the premises presupposes that A is rigid; b may be flexible*) ``` clasohm@923 ` 326` ```val prems = goalw Set.thy [UNION_def] ``` clasohm@923 ` 327` ``` "[| a:A; b: B(a) |] ==> b: (UN x:A. B(x))"; ``` clasohm@923 ` 328` ```by (REPEAT (resolve_tac (prems @ [bexI,CollectI]) 1)); ``` clasohm@923 ` 329` ```qed "UN_I"; ``` clasohm@923 ` 330` clasohm@923 ` 331` ```val major::prems = goalw Set.thy [UNION_def] ``` clasohm@923 ` 332` ``` "[| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R"; ``` clasohm@923 ` 333` ```by (rtac (major RS CollectD RS bexE) 1); ``` clasohm@923 ` 334` ```by (REPEAT (ares_tac prems 1)); ``` clasohm@923 ` 335` ```qed "UN_E"; ``` clasohm@923 ` 336` clasohm@923 ` 337` ```val prems = goal Set.thy ``` clasohm@923 ` 338` ``` "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \ ``` clasohm@923 ` 339` ```\ (UN x:A. C(x)) = (UN x:B. D(x))"; ``` clasohm@923 ` 340` ```by (REPEAT (etac UN_E 1 ``` clasohm@923 ` 341` ``` ORELSE ares_tac ([UN_I,equalityI,subsetI] @ ``` clasohm@923 ` 342` ``` (prems RL [equalityD1,equalityD2] RL [subsetD])) 1)); ``` clasohm@923 ` 343` ```qed "UN_cong"; ``` clasohm@923 ` 344` clasohm@923 ` 345` clasohm@923 ` 346` ```(*** Intersections of families -- INTER x:A. B(x) is Inter(B``A) *) ``` clasohm@923 ` 347` clasohm@923 ` 348` ```val prems = goalw Set.thy [INTER_def] ``` clasohm@923 ` 349` ``` "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"; ``` clasohm@923 ` 350` ```by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1)); ``` clasohm@923 ` 351` ```qed "INT_I"; ``` clasohm@923 ` 352` clasohm@923 ` 353` ```val major::prems = goalw Set.thy [INTER_def] ``` clasohm@923 ` 354` ``` "[| b : (INT x:A. B(x)); a:A |] ==> b: B(a)"; ``` clasohm@923 ` 355` ```by (rtac (major RS CollectD RS bspec) 1); ``` clasohm@923 ` 356` ```by (resolve_tac prems 1); ``` clasohm@923 ` 357` ```qed "INT_D"; ``` clasohm@923 ` 358` clasohm@923 ` 359` ```(*"Classical" elimination -- by the Excluded Middle on a:A *) ``` clasohm@923 ` 360` ```val major::prems = goalw Set.thy [INTER_def] ``` clasohm@923 ` 361` ``` "[| b : (INT x:A. B(x)); b: B(a) ==> R; a~:A ==> R |] ==> R"; ``` clasohm@923 ` 362` ```by (rtac (major RS CollectD RS ballE) 1); ``` clasohm@923 ` 363` ```by (REPEAT (eresolve_tac prems 1)); ``` clasohm@923 ` 364` ```qed "INT_E"; ``` clasohm@923 ` 365` clasohm@923 ` 366` ```val prems = goal Set.thy ``` clasohm@923 ` 367` ``` "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \ ``` clasohm@923 ` 368` ```\ (INT x:A. C(x)) = (INT x:B. D(x))"; ``` clasohm@923 ` 369` ```by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI])); ``` clasohm@923 ` 370` ```by (REPEAT (dtac INT_D 1 ``` clasohm@923 ` 371` ``` ORELSE ares_tac (prems RL [equalityD1,equalityD2] RL [subsetD]) 1)); ``` clasohm@923 ` 372` ```qed "INT_cong"; ``` clasohm@923 ` 373` clasohm@923 ` 374` clasohm@923 ` 375` ```(*** Unions over a type; UNION1(B) = Union(range(B)) ***) ``` clasohm@923 ` 376` clasohm@923 ` 377` ```(*The order of the premises presupposes that A is rigid; b may be flexible*) ``` clasohm@923 ` 378` ```val prems = goalw Set.thy [UNION1_def] ``` clasohm@923 ` 379` ``` "b: B(x) ==> b: (UN x. B(x))"; ``` clasohm@923 ` 380` ```by (REPEAT (resolve_tac (prems @ [TrueI, CollectI RS UN_I]) 1)); ``` clasohm@923 ` 381` ```qed "UN1_I"; ``` clasohm@923 ` 382` clasohm@923 ` 383` ```val major::prems = goalw Set.thy [UNION1_def] ``` clasohm@923 ` 384` ``` "[| b : (UN x. B(x)); !!x. b: B(x) ==> R |] ==> R"; ``` clasohm@923 ` 385` ```by (rtac (major RS UN_E) 1); ``` clasohm@923 ` 386` ```by (REPEAT (ares_tac prems 1)); ``` clasohm@923 ` 387` ```qed "UN1_E"; ``` clasohm@923 ` 388` clasohm@923 ` 389` clasohm@923 ` 390` ```(*** Intersections over a type; INTER1(B) = Inter(range(B)) *) ``` clasohm@923 ` 391` clasohm@923 ` 392` ```val prems = goalw Set.thy [INTER1_def] ``` clasohm@923 ` 393` ``` "(!!x. b: B(x)) ==> b : (INT x. B(x))"; ``` clasohm@923 ` 394` ```by (REPEAT (ares_tac (INT_I::prems) 1)); ``` clasohm@923 ` 395` ```qed "INT1_I"; ``` clasohm@923 ` 396` clasohm@923 ` 397` ```val [major] = goalw Set.thy [INTER1_def] ``` clasohm@923 ` 398` ``` "b : (INT x. B(x)) ==> b: B(a)"; ``` clasohm@923 ` 399` ```by (rtac (TrueI RS (CollectI RS (major RS INT_D))) 1); ``` clasohm@923 ` 400` ```qed "INT1_D"; ``` clasohm@923 ` 401` clasohm@923 ` 402` ```(*** Unions ***) ``` clasohm@923 ` 403` clasohm@923 ` 404` ```(*The order of the premises presupposes that C is rigid; A may be flexible*) ``` clasohm@923 ` 405` ```val prems = goalw Set.thy [Union_def] ``` clasohm@923 ` 406` ``` "[| X:C; A:X |] ==> A : Union(C)"; ``` clasohm@923 ` 407` ```by (REPEAT (resolve_tac (prems @ [UN_I]) 1)); ``` clasohm@923 ` 408` ```qed "UnionI"; ``` clasohm@923 ` 409` clasohm@923 ` 410` ```val major::prems = goalw Set.thy [Union_def] ``` clasohm@923 ` 411` ``` "[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R"; ``` clasohm@923 ` 412` ```by (rtac (major RS UN_E) 1); ``` clasohm@923 ` 413` ```by (REPEAT (ares_tac prems 1)); ``` clasohm@923 ` 414` ```qed "UnionE"; ``` clasohm@923 ` 415` clasohm@923 ` 416` ```(*** Inter ***) ``` clasohm@923 ` 417` clasohm@923 ` 418` ```val prems = goalw Set.thy [Inter_def] ``` clasohm@923 ` 419` ``` "[| !!X. X:C ==> A:X |] ==> A : Inter(C)"; ``` clasohm@923 ` 420` ```by (REPEAT (ares_tac ([INT_I] @ prems) 1)); ``` clasohm@923 ` 421` ```qed "InterI"; ``` clasohm@923 ` 422` clasohm@923 ` 423` ```(*A "destruct" rule -- every X in C contains A as an element, but ``` clasohm@923 ` 424` ``` A:X can hold when X:C does not! This rule is analogous to "spec". *) ``` clasohm@923 ` 425` ```val major::prems = goalw Set.thy [Inter_def] ``` clasohm@923 ` 426` ``` "[| A : Inter(C); X:C |] ==> A:X"; ``` clasohm@923 ` 427` ```by (rtac (major RS INT_D) 1); ``` clasohm@923 ` 428` ```by (resolve_tac prems 1); ``` clasohm@923 ` 429` ```qed "InterD"; ``` clasohm@923 ` 430` clasohm@923 ` 431` ```(*"Classical" elimination rule -- does not require proving X:C *) ``` clasohm@923 ` 432` ```val major::prems = goalw Set.thy [Inter_def] ``` clasohm@923 ` 433` ``` "[| A : Inter(C); A:X ==> R; X~:C ==> R |] ==> R"; ``` clasohm@923 ` 434` ```by (rtac (major RS INT_E) 1); ``` clasohm@923 ` 435` ```by (REPEAT (eresolve_tac prems 1)); ``` clasohm@923 ` 436` ```qed "InterE"; ``` clasohm@923 ` 437` clasohm@923 ` 438` ```(*** Powerset ***) ``` clasohm@923 ` 439` clasohm@923 ` 440` ```qed_goalw "PowI" Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)" ``` clasohm@923 ` 441` ``` (fn _ => [ (etac CollectI 1) ]); ``` clasohm@923 ` 442` clasohm@923 ` 443` ```qed_goalw "PowD" Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B" ``` clasohm@923 ` 444` ``` (fn _=> [ (etac CollectD 1) ]); ``` clasohm@923 ` 445` clasohm@923 ` 446` ```val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *) ``` clasohm@923 ` 447` ```val Pow_top = subset_refl RS PowI; (* A : Pow(A) *) ```