src/HOL/Set.ML
 author oheimb Tue Nov 04 20:50:35 1997 +0100 (1997-11-04) changeset 4135 4830f1f5f6ea parent 4089 96fba19bcbe2 child 4159 4aff9b7e5597 permissions -rw-r--r--
removed redundant ball_empty and bex_empty (see equalities.ML)
 clasohm@1465 ` 1` ```(* Title: HOL/set ``` clasohm@923 ` 2` ``` ID: \$Id\$ ``` clasohm@1465 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@923 ` 4` ``` Copyright 1991 University of Cambridge ``` clasohm@923 ` 5` paulson@1985 ` 6` ```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` nipkow@1548 ` 11` ```section "Relating predicates and sets"; ``` nipkow@1548 ` 12` paulson@3469 ` 13` ```Addsimps [Collect_mem_eq]; ``` paulson@3469 ` 14` ```AddIffs [mem_Collect_eq]; ``` paulson@2499 ` 15` wenzelm@3842 ` 16` ```goal Set.thy "!!a. P(a) ==> a : {x. P(x)}"; ``` paulson@2499 ` 17` ```by (Asm_simp_tac 1); ``` clasohm@923 ` 18` ```qed "CollectI"; ``` clasohm@923 ` 19` wenzelm@3842 ` 20` ```val prems = goal Set.thy "!!a. a : {x. P(x)} ==> P(a)"; ``` paulson@2499 ` 21` ```by (Asm_full_simp_tac 1); ``` clasohm@923 ` 22` ```qed "CollectD"; ``` clasohm@923 ` 23` clasohm@923 ` 24` ```val [prem] = goal Set.thy "[| !!x. (x:A) = (x:B) |] ==> A = B"; ``` clasohm@923 ` 25` ```by (rtac (prem RS ext RS arg_cong RS box_equals) 1); ``` clasohm@923 ` 26` ```by (rtac Collect_mem_eq 1); ``` clasohm@923 ` 27` ```by (rtac Collect_mem_eq 1); ``` clasohm@923 ` 28` ```qed "set_ext"; ``` clasohm@923 ` 29` clasohm@923 ` 30` ```val [prem] = goal Set.thy "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}"; ``` clasohm@923 ` 31` ```by (rtac (prem RS ext RS arg_cong) 1); ``` clasohm@923 ` 32` ```qed "Collect_cong"; ``` clasohm@923 ` 33` clasohm@923 ` 34` ```val CollectE = make_elim CollectD; ``` clasohm@923 ` 35` paulson@2499 ` 36` ```AddSIs [CollectI]; ``` paulson@2499 ` 37` ```AddSEs [CollectE]; ``` paulson@2499 ` 38` paulson@2499 ` 39` nipkow@1548 ` 40` ```section "Bounded quantifiers"; ``` clasohm@923 ` 41` clasohm@923 ` 42` ```val prems = goalw Set.thy [Ball_def] ``` clasohm@923 ` 43` ``` "[| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)"; ``` clasohm@923 ` 44` ```by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); ``` clasohm@923 ` 45` ```qed "ballI"; ``` clasohm@923 ` 46` clasohm@923 ` 47` ```val [major,minor] = goalw Set.thy [Ball_def] ``` clasohm@923 ` 48` ``` "[| ! x:A. P(x); x:A |] ==> P(x)"; ``` clasohm@923 ` 49` ```by (rtac (minor RS (major RS spec RS mp)) 1); ``` clasohm@923 ` 50` ```qed "bspec"; ``` clasohm@923 ` 51` clasohm@923 ` 52` ```val major::prems = goalw Set.thy [Ball_def] ``` clasohm@923 ` 53` ``` "[| ! x:A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q"; ``` clasohm@923 ` 54` ```by (rtac (major RS spec RS impCE) 1); ``` clasohm@923 ` 55` ```by (REPEAT (eresolve_tac prems 1)); ``` clasohm@923 ` 56` ```qed "ballE"; ``` clasohm@923 ` 57` clasohm@923 ` 58` ```(*Takes assumptions ! x:A.P(x) and a:A; creates assumption P(a)*) ``` clasohm@923 ` 59` ```fun ball_tac i = etac ballE i THEN contr_tac (i+1); ``` clasohm@923 ` 60` paulson@2499 ` 61` ```AddSIs [ballI]; ``` paulson@2499 ` 62` ```AddEs [ballE]; ``` paulson@2499 ` 63` clasohm@923 ` 64` ```val prems = goalw Set.thy [Bex_def] ``` clasohm@923 ` 65` ``` "[| P(x); x:A |] ==> ? x:A. P(x)"; ``` clasohm@923 ` 66` ```by (REPEAT (ares_tac (prems @ [exI,conjI]) 1)); ``` clasohm@923 ` 67` ```qed "bexI"; ``` clasohm@923 ` 68` clasohm@923 ` 69` ```qed_goal "bexCI" Set.thy ``` wenzelm@3842 ` 70` ``` "[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A. P(x)" ``` clasohm@923 ` 71` ``` (fn prems=> ``` clasohm@923 ` 72` ``` [ (rtac classical 1), ``` clasohm@923 ` 73` ``` (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); ``` clasohm@923 ` 74` clasohm@923 ` 75` ```val major::prems = goalw Set.thy [Bex_def] ``` clasohm@923 ` 76` ``` "[| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q"; ``` clasohm@923 ` 77` ```by (rtac (major RS exE) 1); ``` clasohm@923 ` 78` ```by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)); ``` clasohm@923 ` 79` ```qed "bexE"; ``` clasohm@923 ` 80` paulson@2499 ` 81` ```AddIs [bexI]; ``` paulson@2499 ` 82` ```AddSEs [bexE]; ``` paulson@2499 ` 83` paulson@3420 ` 84` ```(*Trival rewrite rule*) ``` wenzelm@3842 ` 85` ```goal Set.thy "(! x:A. P) = ((? x. x:A) --> P)"; ``` wenzelm@4089 ` 86` ```by (simp_tac (simpset() addsimps [Ball_def]) 1); ``` paulson@3420 ` 87` ```qed "ball_triv"; ``` paulson@1816 ` 88` paulson@1882 ` 89` ```(*Dual form for existentials*) ``` wenzelm@3842 ` 90` ```goal Set.thy "(? x:A. P) = ((? x. x:A) & P)"; ``` wenzelm@4089 ` 91` ```by (simp_tac (simpset() addsimps [Bex_def]) 1); ``` paulson@3420 ` 92` ```qed "bex_triv"; ``` paulson@1882 ` 93` paulson@3420 ` 94` ```Addsimps [ball_triv, bex_triv]; ``` clasohm@923 ` 95` clasohm@923 ` 96` ```(** Congruence rules **) ``` clasohm@923 ` 97` clasohm@923 ` 98` ```val prems = goal Set.thy ``` clasohm@923 ` 99` ``` "[| A=B; !!x. x:B ==> P(x) = Q(x) |] ==> \ ``` clasohm@923 ` 100` ```\ (! x:A. P(x)) = (! x:B. Q(x))"; ``` clasohm@923 ` 101` ```by (resolve_tac (prems RL [ssubst]) 1); ``` clasohm@923 ` 102` ```by (REPEAT (ares_tac [ballI,iffI] 1 ``` clasohm@923 ` 103` ``` ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1)); ``` clasohm@923 ` 104` ```qed "ball_cong"; ``` clasohm@923 ` 105` clasohm@923 ` 106` ```val prems = goal Set.thy ``` clasohm@923 ` 107` ``` "[| A=B; !!x. x:B ==> P(x) = Q(x) |] ==> \ ``` clasohm@923 ` 108` ```\ (? x:A. P(x)) = (? x:B. Q(x))"; ``` clasohm@923 ` 109` ```by (resolve_tac (prems RL [ssubst]) 1); ``` clasohm@923 ` 110` ```by (REPEAT (etac bexE 1 ``` clasohm@923 ` 111` ``` ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1)); ``` clasohm@923 ` 112` ```qed "bex_cong"; ``` clasohm@923 ` 113` nipkow@1548 ` 114` ```section "Subsets"; ``` clasohm@923 ` 115` wenzelm@3842 ` 116` ```val prems = goalw Set.thy [subset_def] "(!!x. x:A ==> x:B) ==> A <= B"; ``` clasohm@923 ` 117` ```by (REPEAT (ares_tac (prems @ [ballI]) 1)); ``` clasohm@923 ` 118` ```qed "subsetI"; ``` clasohm@923 ` 119` paulson@4059 ` 120` ```Blast.overload ("op <=", domain_type); (*The <= relation is overloaded*) ``` paulson@4059 ` 121` paulson@4059 ` 122` ```(*While (:) is not, its type must be kept ``` paulson@4059 ` 123` ``` for overloading of = to work.*) ``` paulson@4059 ` 124` ```Blast.overload ("op :", domain_type); ``` paulson@4059 ` 125` ```seq (fn a => Blast.overload (a, HOLogic.dest_setT o domain_type)) ``` paulson@4059 ` 126` ``` ["Ball", "Bex"]; ``` paulson@4059 ` 127` ```(*need UNION, INTER also?*) ``` paulson@4059 ` 128` paulson@2881 ` 129` clasohm@923 ` 130` ```(*Rule in Modus Ponens style*) ``` clasohm@923 ` 131` ```val major::prems = goalw Set.thy [subset_def] "[| A <= B; c:A |] ==> c:B"; ``` clasohm@923 ` 132` ```by (rtac (major RS bspec) 1); ``` clasohm@923 ` 133` ```by (resolve_tac prems 1); ``` clasohm@923 ` 134` ```qed "subsetD"; ``` clasohm@923 ` 135` clasohm@923 ` 136` ```(*The same, with reversed premises for use with etac -- cf rev_mp*) ``` clasohm@923 ` 137` ```qed_goal "rev_subsetD" Set.thy "[| c:A; A <= B |] ==> c:B" ``` clasohm@923 ` 138` ``` (fn prems=> [ (REPEAT (resolve_tac (prems@[subsetD]) 1)) ]); ``` clasohm@923 ` 139` paulson@1920 ` 140` ```(*Converts A<=B to x:A ==> x:B*) ``` paulson@1920 ` 141` ```fun impOfSubs th = th RSN (2, rev_subsetD); ``` paulson@1920 ` 142` paulson@1841 ` 143` ```qed_goal "contra_subsetD" Set.thy "!!c. [| A <= B; c ~: B |] ==> c ~: A" ``` paulson@1841 ` 144` ``` (fn prems=> [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]); ``` paulson@1841 ` 145` paulson@1841 ` 146` ```qed_goal "rev_contra_subsetD" Set.thy "!!c. [| c ~: B; A <= B |] ==> c ~: A" ``` paulson@1841 ` 147` ``` (fn prems=> [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]); ``` paulson@1841 ` 148` clasohm@923 ` 149` ```(*Classical elimination rule*) ``` clasohm@923 ` 150` ```val major::prems = goalw Set.thy [subset_def] ``` clasohm@923 ` 151` ``` "[| A <= B; c~:A ==> P; c:B ==> P |] ==> P"; ``` clasohm@923 ` 152` ```by (rtac (major RS ballE) 1); ``` clasohm@923 ` 153` ```by (REPEAT (eresolve_tac prems 1)); ``` clasohm@923 ` 154` ```qed "subsetCE"; ``` clasohm@923 ` 155` clasohm@923 ` 156` ```(*Takes assumptions A<=B; c:A and creates the assumption c:B *) ``` clasohm@923 ` 157` ```fun set_mp_tac i = etac subsetCE i THEN mp_tac i; ``` clasohm@923 ` 158` paulson@2499 ` 159` ```AddSIs [subsetI]; ``` paulson@2499 ` 160` ```AddEs [subsetD, subsetCE]; ``` clasohm@923 ` 161` paulson@2499 ` 162` ```qed_goal "subset_refl" Set.thy "A <= (A::'a set)" ``` paulson@4059 ` 163` ``` (fn _=> [Fast_tac 1]); (*Blast_tac would try order_refl and fail*) ``` paulson@2499 ` 164` paulson@2499 ` 165` ```val prems = goal Set.thy "!!B. [| A<=B; B<=C |] ==> A<=(C::'a set)"; ``` paulson@2891 ` 166` ```by (Blast_tac 1); ``` clasohm@923 ` 167` ```qed "subset_trans"; ``` clasohm@923 ` 168` clasohm@923 ` 169` nipkow@1548 ` 170` ```section "Equality"; ``` clasohm@923 ` 171` clasohm@923 ` 172` ```(*Anti-symmetry of the subset relation*) ``` clasohm@923 ` 173` ```val prems = goal Set.thy "[| A <= B; B <= A |] ==> A = (B::'a set)"; ``` clasohm@923 ` 174` ```by (rtac (iffI RS set_ext) 1); ``` clasohm@923 ` 175` ```by (REPEAT (ares_tac (prems RL [subsetD]) 1)); ``` clasohm@923 ` 176` ```qed "subset_antisym"; ``` clasohm@923 ` 177` ```val equalityI = subset_antisym; ``` clasohm@923 ` 178` berghofe@1762 ` 179` ```AddSIs [equalityI]; ``` berghofe@1762 ` 180` clasohm@923 ` 181` ```(* Equality rules from ZF set theory -- are they appropriate here? *) ``` clasohm@923 ` 182` ```val prems = goal Set.thy "A = B ==> A<=(B::'a set)"; ``` clasohm@923 ` 183` ```by (resolve_tac (prems RL [subst]) 1); ``` clasohm@923 ` 184` ```by (rtac subset_refl 1); ``` clasohm@923 ` 185` ```qed "equalityD1"; ``` clasohm@923 ` 186` clasohm@923 ` 187` ```val prems = goal Set.thy "A = B ==> B<=(A::'a set)"; ``` clasohm@923 ` 188` ```by (resolve_tac (prems RL [subst]) 1); ``` clasohm@923 ` 189` ```by (rtac subset_refl 1); ``` clasohm@923 ` 190` ```qed "equalityD2"; ``` clasohm@923 ` 191` clasohm@923 ` 192` ```val prems = goal Set.thy ``` clasohm@923 ` 193` ``` "[| A = B; [| A<=B; B<=(A::'a set) |] ==> P |] ==> P"; ``` clasohm@923 ` 194` ```by (resolve_tac prems 1); ``` clasohm@923 ` 195` ```by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1)); ``` clasohm@923 ` 196` ```qed "equalityE"; ``` clasohm@923 ` 197` clasohm@923 ` 198` ```val major::prems = goal Set.thy ``` clasohm@923 ` 199` ``` "[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P"; ``` clasohm@923 ` 200` ```by (rtac (major RS equalityE) 1); ``` clasohm@923 ` 201` ```by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)); ``` clasohm@923 ` 202` ```qed "equalityCE"; ``` clasohm@923 ` 203` clasohm@923 ` 204` ```(*Lemma for creating induction formulae -- for "pattern matching" on p ``` clasohm@923 ` 205` ``` To make the induction hypotheses usable, apply "spec" or "bspec" to ``` clasohm@923 ` 206` ``` put universal quantifiers over the free variables in p. *) ``` clasohm@923 ` 207` ```val prems = goal Set.thy ``` clasohm@923 ` 208` ``` "[| p:A; !!z. z:A ==> p=z --> R |] ==> R"; ``` clasohm@923 ` 209` ```by (rtac mp 1); ``` clasohm@923 ` 210` ```by (REPEAT (resolve_tac (refl::prems) 1)); ``` clasohm@923 ` 211` ```qed "setup_induction"; ``` clasohm@923 ` 212` clasohm@923 ` 213` paulson@2858 ` 214` ```section "The empty set -- {}"; ``` paulson@2858 ` 215` paulson@2858 ` 216` ```qed_goalw "empty_iff" Set.thy [empty_def] "(c : {}) = False" ``` paulson@2891 ` 217` ``` (fn _ => [ (Blast_tac 1) ]); ``` paulson@2858 ` 218` paulson@2858 ` 219` ```Addsimps [empty_iff]; ``` paulson@2858 ` 220` paulson@2858 ` 221` ```qed_goal "emptyE" Set.thy "!!a. a:{} ==> P" ``` paulson@2858 ` 222` ``` (fn _ => [Full_simp_tac 1]); ``` paulson@2858 ` 223` paulson@2858 ` 224` ```AddSEs [emptyE]; ``` paulson@2858 ` 225` paulson@2858 ` 226` ```qed_goal "empty_subsetI" Set.thy "{} <= A" ``` paulson@2891 ` 227` ``` (fn _ => [ (Blast_tac 1) ]); ``` paulson@2858 ` 228` paulson@2858 ` 229` ```qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}" ``` paulson@2858 ` 230` ``` (fn [prem]=> ``` wenzelm@4089 ` 231` ``` [ (blast_tac (claset() addIs [prem RS FalseE]) 1) ]); ``` paulson@2858 ` 232` paulson@2858 ` 233` ```qed_goal "equals0D" Set.thy "!!a. [| A={}; a:A |] ==> P" ``` paulson@2891 ` 234` ``` (fn _ => [ (Blast_tac 1) ]); ``` paulson@2858 ` 235` paulson@2858 ` 236` paulson@2858 ` 237` ```section "The Powerset operator -- Pow"; ``` paulson@2858 ` 238` paulson@2858 ` 239` ```qed_goalw "Pow_iff" Set.thy [Pow_def] "(A : Pow(B)) = (A <= B)" ``` paulson@2858 ` 240` ``` (fn _ => [ (Asm_simp_tac 1) ]); ``` paulson@2858 ` 241` paulson@2858 ` 242` ```AddIffs [Pow_iff]; ``` paulson@2858 ` 243` paulson@2858 ` 244` ```qed_goalw "PowI" Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)" ``` paulson@2858 ` 245` ``` (fn _ => [ (etac CollectI 1) ]); ``` paulson@2858 ` 246` paulson@2858 ` 247` ```qed_goalw "PowD" Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B" ``` paulson@2858 ` 248` ``` (fn _=> [ (etac CollectD 1) ]); ``` paulson@2858 ` 249` paulson@2858 ` 250` ```val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *) ``` paulson@2858 ` 251` ```val Pow_top = subset_refl RS PowI; (* A : Pow(A) *) ``` paulson@2858 ` 252` paulson@2858 ` 253` nipkow@1548 ` 254` ```section "Set complement -- Compl"; ``` clasohm@923 ` 255` paulson@2499 ` 256` ```qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : Compl(A)) = (c~:A)" ``` paulson@2891 ` 257` ``` (fn _ => [ (Blast_tac 1) ]); ``` paulson@2499 ` 258` paulson@2499 ` 259` ```Addsimps [Compl_iff]; ``` paulson@2499 ` 260` clasohm@923 ` 261` ```val prems = goalw Set.thy [Compl_def] ``` clasohm@923 ` 262` ``` "[| c:A ==> False |] ==> c : Compl(A)"; ``` clasohm@923 ` 263` ```by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1)); ``` clasohm@923 ` 264` ```qed "ComplI"; ``` clasohm@923 ` 265` clasohm@923 ` 266` ```(*This form, with negated conclusion, works well with the Classical prover. ``` clasohm@923 ` 267` ``` Negated assumptions behave like formulae on the right side of the notional ``` clasohm@923 ` 268` ``` turnstile...*) ``` clasohm@923 ` 269` ```val major::prems = goalw Set.thy [Compl_def] ``` paulson@2499 ` 270` ``` "c : Compl(A) ==> c~:A"; ``` clasohm@923 ` 271` ```by (rtac (major RS CollectD) 1); ``` clasohm@923 ` 272` ```qed "ComplD"; ``` clasohm@923 ` 273` clasohm@923 ` 274` ```val ComplE = make_elim ComplD; ``` clasohm@923 ` 275` paulson@2499 ` 276` ```AddSIs [ComplI]; ``` paulson@2499 ` 277` ```AddSEs [ComplE]; ``` paulson@1640 ` 278` clasohm@923 ` 279` nipkow@1548 ` 280` ```section "Binary union -- Un"; ``` clasohm@923 ` 281` paulson@2499 ` 282` ```qed_goalw "Un_iff" Set.thy [Un_def] "(c : A Un B) = (c:A | c:B)" ``` paulson@2891 ` 283` ``` (fn _ => [ Blast_tac 1 ]); ``` paulson@2499 ` 284` paulson@2499 ` 285` ```Addsimps [Un_iff]; ``` paulson@2499 ` 286` paulson@2499 ` 287` ```goal Set.thy "!!c. c:A ==> c : A Un B"; ``` paulson@2499 ` 288` ```by (Asm_simp_tac 1); ``` clasohm@923 ` 289` ```qed "UnI1"; ``` clasohm@923 ` 290` paulson@2499 ` 291` ```goal Set.thy "!!c. c:B ==> c : A Un B"; ``` paulson@2499 ` 292` ```by (Asm_simp_tac 1); ``` clasohm@923 ` 293` ```qed "UnI2"; ``` clasohm@923 ` 294` clasohm@923 ` 295` ```(*Classical introduction rule: no commitment to A vs B*) ``` clasohm@923 ` 296` ```qed_goal "UnCI" Set.thy "(c~:B ==> c:A) ==> c : A Un B" ``` clasohm@923 ` 297` ``` (fn prems=> ``` paulson@2499 ` 298` ``` [ (Simp_tac 1), ``` paulson@2499 ` 299` ``` (REPEAT (ares_tac (prems@[disjCI]) 1)) ]); ``` clasohm@923 ` 300` clasohm@923 ` 301` ```val major::prems = goalw Set.thy [Un_def] ``` clasohm@923 ` 302` ``` "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"; ``` clasohm@923 ` 303` ```by (rtac (major RS CollectD RS disjE) 1); ``` clasohm@923 ` 304` ```by (REPEAT (eresolve_tac prems 1)); ``` clasohm@923 ` 305` ```qed "UnE"; ``` clasohm@923 ` 306` paulson@2499 ` 307` ```AddSIs [UnCI]; ``` paulson@2499 ` 308` ```AddSEs [UnE]; ``` paulson@1640 ` 309` clasohm@923 ` 310` nipkow@1548 ` 311` ```section "Binary intersection -- Int"; ``` clasohm@923 ` 312` paulson@2499 ` 313` ```qed_goalw "Int_iff" Set.thy [Int_def] "(c : A Int B) = (c:A & c:B)" ``` paulson@2891 ` 314` ``` (fn _ => [ (Blast_tac 1) ]); ``` paulson@2499 ` 315` paulson@2499 ` 316` ```Addsimps [Int_iff]; ``` paulson@2499 ` 317` paulson@2499 ` 318` ```goal Set.thy "!!c. [| c:A; c:B |] ==> c : A Int B"; ``` paulson@2499 ` 319` ```by (Asm_simp_tac 1); ``` clasohm@923 ` 320` ```qed "IntI"; ``` clasohm@923 ` 321` paulson@2499 ` 322` ```goal Set.thy "!!c. c : A Int B ==> c:A"; ``` paulson@2499 ` 323` ```by (Asm_full_simp_tac 1); ``` clasohm@923 ` 324` ```qed "IntD1"; ``` clasohm@923 ` 325` paulson@2499 ` 326` ```goal Set.thy "!!c. c : A Int B ==> c:B"; ``` paulson@2499 ` 327` ```by (Asm_full_simp_tac 1); ``` clasohm@923 ` 328` ```qed "IntD2"; ``` clasohm@923 ` 329` clasohm@923 ` 330` ```val [major,minor] = goal Set.thy ``` clasohm@923 ` 331` ``` "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"; ``` clasohm@923 ` 332` ```by (rtac minor 1); ``` clasohm@923 ` 333` ```by (rtac (major RS IntD1) 1); ``` clasohm@923 ` 334` ```by (rtac (major RS IntD2) 1); ``` clasohm@923 ` 335` ```qed "IntE"; ``` clasohm@923 ` 336` paulson@2499 ` 337` ```AddSIs [IntI]; ``` paulson@2499 ` 338` ```AddSEs [IntE]; ``` clasohm@923 ` 339` nipkow@1548 ` 340` ```section "Set difference"; ``` clasohm@923 ` 341` paulson@2499 ` 342` ```qed_goalw "Diff_iff" Set.thy [set_diff_def] "(c : A-B) = (c:A & c~:B)" ``` paulson@2891 ` 343` ``` (fn _ => [ (Blast_tac 1) ]); ``` clasohm@923 ` 344` paulson@2499 ` 345` ```Addsimps [Diff_iff]; ``` paulson@2499 ` 346` paulson@2499 ` 347` ```qed_goal "DiffI" Set.thy "!!c. [| c : A; c ~: B |] ==> c : A - B" ``` paulson@2499 ` 348` ``` (fn _=> [ Asm_simp_tac 1 ]); ``` clasohm@923 ` 349` paulson@2499 ` 350` ```qed_goal "DiffD1" Set.thy "!!c. c : A - B ==> c : A" ``` paulson@2499 ` 351` ``` (fn _=> [ (Asm_full_simp_tac 1) ]); ``` clasohm@923 ` 352` paulson@2499 ` 353` ```qed_goal "DiffD2" Set.thy "!!c. [| c : A - B; c : B |] ==> P" ``` paulson@2499 ` 354` ``` (fn _=> [ (Asm_full_simp_tac 1) ]); ``` paulson@2499 ` 355` paulson@2499 ` 356` ```qed_goal "DiffE" Set.thy "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P" ``` clasohm@923 ` 357` ``` (fn prems=> ``` clasohm@923 ` 358` ``` [ (resolve_tac prems 1), ``` clasohm@923 ` 359` ``` (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]); ``` clasohm@923 ` 360` paulson@2499 ` 361` ```AddSIs [DiffI]; ``` paulson@2499 ` 362` ```AddSEs [DiffE]; ``` clasohm@923 ` 363` clasohm@923 ` 364` nipkow@1548 ` 365` ```section "Augmenting a set -- insert"; ``` clasohm@923 ` 366` paulson@2499 ` 367` ```qed_goalw "insert_iff" Set.thy [insert_def] "a : insert b A = (a=b | a:A)" ``` paulson@2891 ` 368` ``` (fn _ => [Blast_tac 1]); ``` paulson@2499 ` 369` paulson@2499 ` 370` ```Addsimps [insert_iff]; ``` clasohm@923 ` 371` paulson@2499 ` 372` ```qed_goal "insertI1" Set.thy "a : insert a B" ``` paulson@2499 ` 373` ``` (fn _ => [Simp_tac 1]); ``` paulson@2499 ` 374` paulson@2499 ` 375` ```qed_goal "insertI2" Set.thy "!!a. a : B ==> a : insert b B" ``` paulson@2499 ` 376` ``` (fn _=> [Asm_simp_tac 1]); ``` clasohm@923 ` 377` clasohm@923 ` 378` ```qed_goalw "insertE" Set.thy [insert_def] ``` clasohm@923 ` 379` ``` "[| a : insert b A; a=b ==> P; a:A ==> P |] ==> P" ``` clasohm@923 ` 380` ``` (fn major::prems=> ``` clasohm@923 ` 381` ``` [ (rtac (major RS UnE) 1), ``` clasohm@923 ` 382` ``` (REPEAT (eresolve_tac (prems @ [CollectE]) 1)) ]); ``` clasohm@923 ` 383` clasohm@923 ` 384` ```(*Classical introduction rule*) ``` clasohm@923 ` 385` ```qed_goal "insertCI" Set.thy "(a~:B ==> a=b) ==> a: insert b B" ``` paulson@2499 ` 386` ``` (fn prems=> ``` paulson@2499 ` 387` ``` [ (Simp_tac 1), ``` paulson@2499 ` 388` ``` (REPEAT (ares_tac (prems@[disjCI]) 1)) ]); ``` paulson@2499 ` 389` paulson@2499 ` 390` ```AddSIs [insertCI]; ``` paulson@2499 ` 391` ```AddSEs [insertE]; ``` clasohm@923 ` 392` nipkow@1548 ` 393` ```section "Singletons, using insert"; ``` clasohm@923 ` 394` clasohm@923 ` 395` ```qed_goal "singletonI" Set.thy "a : {a}" ``` clasohm@923 ` 396` ``` (fn _=> [ (rtac insertI1 1) ]); ``` clasohm@923 ` 397` paulson@2499 ` 398` ```goal Set.thy "!!a. b : {a} ==> b=a"; ``` paulson@2891 ` 399` ```by (Blast_tac 1); ``` clasohm@923 ` 400` ```qed "singletonD"; ``` clasohm@923 ` 401` oheimb@1776 ` 402` ```bind_thm ("singletonE", make_elim singletonD); ``` oheimb@1776 ` 403` paulson@2499 ` 404` ```qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" ``` paulson@2891 ` 405` ```(fn _ => [Blast_tac 1]); ``` clasohm@923 ` 406` paulson@2499 ` 407` ```goal Set.thy "!!a b. {a}={b} ==> a=b"; ``` wenzelm@4089 ` 408` ```by (blast_tac (claset() addEs [equalityE]) 1); ``` clasohm@923 ` 409` ```qed "singleton_inject"; ``` clasohm@923 ` 410` paulson@2858 ` 411` ```(*Redundant? But unlike insertCI, it proves the subgoal immediately!*) ``` paulson@2858 ` 412` ```AddSIs [singletonI]; ``` paulson@2499 ` 413` ```AddSDs [singleton_inject]; ``` paulson@3718 ` 414` ```AddSEs [singletonE]; ``` paulson@2499 ` 415` wenzelm@3842 ` 416` ```goal Set.thy "{x. x=a} = {a}"; ``` nipkow@3582 ` 417` ```by(Blast_tac 1); ``` nipkow@3582 ` 418` ```qed "singleton_conv"; ``` nipkow@3582 ` 419` ```Addsimps [singleton_conv]; ``` nipkow@1531 ` 420` nipkow@1548 ` 421` ```section "The universal set -- UNIV"; ``` nipkow@1531 ` 422` paulson@1882 ` 423` ```qed_goal "UNIV_I" Set.thy "x : UNIV" ``` paulson@1882 ` 424` ``` (fn _ => [rtac ComplI 1, etac emptyE 1]); ``` paulson@1882 ` 425` nipkow@1531 ` 426` ```qed_goal "subset_UNIV" Set.thy "A <= UNIV" ``` paulson@1882 ` 427` ``` (fn _ => [rtac subsetI 1, rtac UNIV_I 1]); ``` nipkow@1531 ` 428` nipkow@1531 ` 429` nipkow@1548 ` 430` ```section "Unions of families -- UNION x:A. B(x) is Union(B``A)"; ``` clasohm@923 ` 431` paulson@2499 ` 432` ```goalw Set.thy [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))"; ``` paulson@2891 ` 433` ```by (Blast_tac 1); ``` paulson@2499 ` 434` ```qed "UN_iff"; ``` paulson@2499 ` 435` paulson@2499 ` 436` ```Addsimps [UN_iff]; ``` paulson@2499 ` 437` clasohm@923 ` 438` ```(*The order of the premises presupposes that A is rigid; b may be flexible*) ``` paulson@2499 ` 439` ```goal Set.thy "!!b. [| a:A; b: B(a) |] ==> b: (UN x:A. B(x))"; ``` paulson@2499 ` 440` ```by (Auto_tac()); ``` clasohm@923 ` 441` ```qed "UN_I"; ``` clasohm@923 ` 442` clasohm@923 ` 443` ```val major::prems = goalw Set.thy [UNION_def] ``` clasohm@923 ` 444` ``` "[| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R"; ``` clasohm@923 ` 445` ```by (rtac (major RS CollectD RS bexE) 1); ``` clasohm@923 ` 446` ```by (REPEAT (ares_tac prems 1)); ``` clasohm@923 ` 447` ```qed "UN_E"; ``` clasohm@923 ` 448` paulson@2499 ` 449` ```AddIs [UN_I]; ``` paulson@2499 ` 450` ```AddSEs [UN_E]; ``` paulson@2499 ` 451` clasohm@923 ` 452` ```val prems = goal Set.thy ``` clasohm@923 ` 453` ``` "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \ ``` clasohm@923 ` 454` ```\ (UN x:A. C(x)) = (UN x:B. D(x))"; ``` clasohm@923 ` 455` ```by (REPEAT (etac UN_E 1 ``` clasohm@923 ` 456` ``` ORELSE ares_tac ([UN_I,equalityI,subsetI] @ ``` clasohm@1465 ` 457` ``` (prems RL [equalityD1,equalityD2] RL [subsetD])) 1)); ``` clasohm@923 ` 458` ```qed "UN_cong"; ``` clasohm@923 ` 459` clasohm@923 ` 460` nipkow@1548 ` 461` ```section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)"; ``` clasohm@923 ` 462` paulson@2499 ` 463` ```goalw Set.thy [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))"; ``` paulson@2499 ` 464` ```by (Auto_tac()); ``` paulson@2499 ` 465` ```qed "INT_iff"; ``` paulson@2499 ` 466` paulson@2499 ` 467` ```Addsimps [INT_iff]; ``` paulson@2499 ` 468` clasohm@923 ` 469` ```val prems = goalw Set.thy [INTER_def] ``` clasohm@923 ` 470` ``` "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"; ``` clasohm@923 ` 471` ```by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1)); ``` clasohm@923 ` 472` ```qed "INT_I"; ``` clasohm@923 ` 473` paulson@2499 ` 474` ```goal Set.thy "!!b. [| b : (INT x:A. B(x)); a:A |] ==> b: B(a)"; ``` paulson@2499 ` 475` ```by (Auto_tac()); ``` clasohm@923 ` 476` ```qed "INT_D"; ``` clasohm@923 ` 477` clasohm@923 ` 478` ```(*"Classical" elimination -- by the Excluded Middle on a:A *) ``` clasohm@923 ` 479` ```val major::prems = goalw Set.thy [INTER_def] ``` clasohm@923 ` 480` ``` "[| b : (INT x:A. B(x)); b: B(a) ==> R; a~:A ==> R |] ==> R"; ``` clasohm@923 ` 481` ```by (rtac (major RS CollectD RS ballE) 1); ``` clasohm@923 ` 482` ```by (REPEAT (eresolve_tac prems 1)); ``` clasohm@923 ` 483` ```qed "INT_E"; ``` clasohm@923 ` 484` paulson@2499 ` 485` ```AddSIs [INT_I]; ``` paulson@2499 ` 486` ```AddEs [INT_D, INT_E]; ``` paulson@2499 ` 487` clasohm@923 ` 488` ```val prems = goal Set.thy ``` clasohm@923 ` 489` ``` "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \ ``` clasohm@923 ` 490` ```\ (INT x:A. C(x)) = (INT x:B. D(x))"; ``` clasohm@923 ` 491` ```by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI])); ``` clasohm@923 ` 492` ```by (REPEAT (dtac INT_D 1 ``` clasohm@923 ` 493` ``` ORELSE ares_tac (prems RL [equalityD1,equalityD2] RL [subsetD]) 1)); ``` clasohm@923 ` 494` ```qed "INT_cong"; ``` clasohm@923 ` 495` clasohm@923 ` 496` nipkow@1548 ` 497` ```section "Unions over a type; UNION1(B) = Union(range(B))"; ``` clasohm@923 ` 498` paulson@2499 ` 499` ```goalw Set.thy [UNION1_def] "(b: (UN x. B(x))) = (EX x. b: B(x))"; ``` paulson@2499 ` 500` ```by (Simp_tac 1); ``` paulson@2891 ` 501` ```by (Blast_tac 1); ``` paulson@2499 ` 502` ```qed "UN1_iff"; ``` paulson@2499 ` 503` paulson@2499 ` 504` ```Addsimps [UN1_iff]; ``` paulson@2499 ` 505` clasohm@923 ` 506` ```(*The order of the premises presupposes that A is rigid; b may be flexible*) ``` paulson@2499 ` 507` ```goal Set.thy "!!b. b: B(x) ==> b: (UN x. B(x))"; ``` paulson@2499 ` 508` ```by (Auto_tac()); ``` clasohm@923 ` 509` ```qed "UN1_I"; ``` clasohm@923 ` 510` clasohm@923 ` 511` ```val major::prems = goalw Set.thy [UNION1_def] ``` clasohm@923 ` 512` ``` "[| b : (UN x. B(x)); !!x. b: B(x) ==> R |] ==> R"; ``` clasohm@923 ` 513` ```by (rtac (major RS UN_E) 1); ``` clasohm@923 ` 514` ```by (REPEAT (ares_tac prems 1)); ``` clasohm@923 ` 515` ```qed "UN1_E"; ``` clasohm@923 ` 516` paulson@2499 ` 517` ```AddIs [UN1_I]; ``` paulson@2499 ` 518` ```AddSEs [UN1_E]; ``` paulson@2499 ` 519` clasohm@923 ` 520` nipkow@1548 ` 521` ```section "Intersections over a type; INTER1(B) = Inter(range(B))"; ``` clasohm@923 ` 522` paulson@2499 ` 523` ```goalw Set.thy [INTER1_def] "(b: (INT x. B(x))) = (ALL x. b: B(x))"; ``` paulson@2499 ` 524` ```by (Simp_tac 1); ``` paulson@2891 ` 525` ```by (Blast_tac 1); ``` paulson@2499 ` 526` ```qed "INT1_iff"; ``` paulson@2499 ` 527` paulson@2499 ` 528` ```Addsimps [INT1_iff]; ``` paulson@2499 ` 529` clasohm@923 ` 530` ```val prems = goalw Set.thy [INTER1_def] ``` clasohm@923 ` 531` ``` "(!!x. b: B(x)) ==> b : (INT x. B(x))"; ``` clasohm@923 ` 532` ```by (REPEAT (ares_tac (INT_I::prems) 1)); ``` clasohm@923 ` 533` ```qed "INT1_I"; ``` clasohm@923 ` 534` paulson@2499 ` 535` ```goal Set.thy "!!b. b : (INT x. B(x)) ==> b: B(a)"; ``` paulson@2499 ` 536` ```by (Asm_full_simp_tac 1); ``` clasohm@923 ` 537` ```qed "INT1_D"; ``` clasohm@923 ` 538` paulson@2499 ` 539` ```AddSIs [INT1_I]; ``` paulson@2499 ` 540` ```AddDs [INT1_D]; ``` paulson@2499 ` 541` paulson@2499 ` 542` nipkow@1548 ` 543` ```section "Union"; ``` clasohm@923 ` 544` paulson@2499 ` 545` ```goalw Set.thy [Union_def] "(A : Union(C)) = (EX X:C. A:X)"; ``` paulson@2891 ` 546` ```by (Blast_tac 1); ``` paulson@2499 ` 547` ```qed "Union_iff"; ``` paulson@2499 ` 548` paulson@2499 ` 549` ```Addsimps [Union_iff]; ``` paulson@2499 ` 550` clasohm@923 ` 551` ```(*The order of the premises presupposes that C is rigid; A may be flexible*) ``` paulson@2499 ` 552` ```goal Set.thy "!!X. [| X:C; A:X |] ==> A : Union(C)"; ``` paulson@2499 ` 553` ```by (Auto_tac()); ``` clasohm@923 ` 554` ```qed "UnionI"; ``` clasohm@923 ` 555` clasohm@923 ` 556` ```val major::prems = goalw Set.thy [Union_def] ``` clasohm@923 ` 557` ``` "[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R"; ``` clasohm@923 ` 558` ```by (rtac (major RS UN_E) 1); ``` clasohm@923 ` 559` ```by (REPEAT (ares_tac prems 1)); ``` clasohm@923 ` 560` ```qed "UnionE"; ``` clasohm@923 ` 561` paulson@2499 ` 562` ```AddIs [UnionI]; ``` paulson@2499 ` 563` ```AddSEs [UnionE]; ``` paulson@2499 ` 564` paulson@2499 ` 565` nipkow@1548 ` 566` ```section "Inter"; ``` clasohm@923 ` 567` paulson@2499 ` 568` ```goalw Set.thy [Inter_def] "(A : Inter(C)) = (ALL X:C. A:X)"; ``` paulson@2891 ` 569` ```by (Blast_tac 1); ``` paulson@2499 ` 570` ```qed "Inter_iff"; ``` paulson@2499 ` 571` paulson@2499 ` 572` ```Addsimps [Inter_iff]; ``` paulson@2499 ` 573` clasohm@923 ` 574` ```val prems = goalw Set.thy [Inter_def] ``` clasohm@923 ` 575` ``` "[| !!X. X:C ==> A:X |] ==> A : Inter(C)"; ``` clasohm@923 ` 576` ```by (REPEAT (ares_tac ([INT_I] @ prems) 1)); ``` clasohm@923 ` 577` ```qed "InterI"; ``` clasohm@923 ` 578` clasohm@923 ` 579` ```(*A "destruct" rule -- every X in C contains A as an element, but ``` clasohm@923 ` 580` ``` A:X can hold when X:C does not! This rule is analogous to "spec". *) ``` paulson@2499 ` 581` ```goal Set.thy "!!X. [| A : Inter(C); X:C |] ==> A:X"; ``` paulson@2499 ` 582` ```by (Auto_tac()); ``` clasohm@923 ` 583` ```qed "InterD"; ``` clasohm@923 ` 584` clasohm@923 ` 585` ```(*"Classical" elimination rule -- does not require proving X:C *) ``` clasohm@923 ` 586` ```val major::prems = goalw Set.thy [Inter_def] ``` paulson@2721 ` 587` ``` "[| A : Inter(C); X~:C ==> R; A:X ==> R |] ==> R"; ``` clasohm@923 ` 588` ```by (rtac (major RS INT_E) 1); ``` clasohm@923 ` 589` ```by (REPEAT (eresolve_tac prems 1)); ``` clasohm@923 ` 590` ```qed "InterE"; ``` clasohm@923 ` 591` paulson@2499 ` 592` ```AddSIs [InterI]; ``` paulson@2499 ` 593` ```AddEs [InterD, InterE]; ``` paulson@2499 ` 594` paulson@2499 ` 595` nipkow@2912 ` 596` ```(*** Image of a set under a function ***) ``` nipkow@2912 ` 597` nipkow@2912 ` 598` ```(*Frequently b does not have the syntactic form of f(x).*) ``` nipkow@2912 ` 599` ```val prems = goalw thy [image_def] "[| b=f(x); x:A |] ==> b : f``A"; ``` nipkow@2912 ` 600` ```by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1)); ``` nipkow@2912 ` 601` ```qed "image_eqI"; ``` nipkow@3909 ` 602` ```Addsimps [image_eqI]; ``` nipkow@2912 ` 603` nipkow@2912 ` 604` ```bind_thm ("imageI", refl RS image_eqI); ``` nipkow@2912 ` 605` nipkow@2912 ` 606` ```(*The eta-expansion gives variable-name preservation.*) ``` nipkow@2912 ` 607` ```val major::prems = goalw thy [image_def] ``` wenzelm@3842 ` 608` ``` "[| b : (%x. f(x))``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P"; ``` nipkow@2912 ` 609` ```by (rtac (major RS CollectD RS bexE) 1); ``` nipkow@2912 ` 610` ```by (REPEAT (ares_tac prems 1)); ``` nipkow@2912 ` 611` ```qed "imageE"; ``` nipkow@2912 ` 612` nipkow@2912 ` 613` ```AddIs [image_eqI]; ``` nipkow@2912 ` 614` ```AddSEs [imageE]; ``` nipkow@2912 ` 615` nipkow@2912 ` 616` ```goalw thy [o_def] "(f o g)``r = f``(g``r)"; ``` paulson@2935 ` 617` ```by (Blast_tac 1); ``` nipkow@2912 ` 618` ```qed "image_compose"; ``` nipkow@2912 ` 619` nipkow@2912 ` 620` ```goal thy "f``(A Un B) = f``A Un f``B"; ``` paulson@2935 ` 621` ```by (Blast_tac 1); ``` nipkow@2912 ` 622` ```qed "image_Un"; ``` nipkow@2912 ` 623` paulson@3960 ` 624` ```goal Set.thy "(z : f``A) = (EX x:A. z = f x)"; ``` paulson@3960 ` 625` ```by (Blast_tac 1); ``` paulson@3960 ` 626` ```qed "image_iff"; ``` paulson@3960 ` 627` nipkow@2912 ` 628` nipkow@2912 ` 629` ```(*** Range of a function -- just a translation for image! ***) ``` nipkow@2912 ` 630` nipkow@2912 ` 631` ```goal thy "!!b. b=f(x) ==> b : range(f)"; ``` nipkow@2912 ` 632` ```by (EVERY1 [etac image_eqI, rtac UNIV_I]); ``` nipkow@2912 ` 633` ```bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI)); ``` nipkow@2912 ` 634` nipkow@2912 ` 635` ```bind_thm ("rangeI", UNIV_I RS imageI); ``` nipkow@2912 ` 636` nipkow@2912 ` 637` ```val [major,minor] = goal thy ``` wenzelm@3842 ` 638` ``` "[| b : range(%x. f(x)); !!x. b=f(x) ==> P |] ==> P"; ``` nipkow@2912 ` 639` ```by (rtac (major RS imageE) 1); ``` nipkow@2912 ` 640` ```by (etac minor 1); ``` nipkow@2912 ` 641` ```qed "rangeE"; ``` nipkow@2912 ` 642` oheimb@1776 ` 643` oheimb@1776 ` 644` ```(*** Set reasoning tools ***) ``` oheimb@1776 ` 645` oheimb@1776 ` 646` paulson@3912 ` 647` ```(** Rewrite rules for boolean case-splitting: faster than ``` nipkow@3919 ` 648` ``` addsplits[expand_if] ``` paulson@3912 ` 649` ```**) ``` paulson@3912 ` 650` paulson@3912 ` 651` ```bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if); ``` paulson@3912 ` 652` ```bind_thm ("expand_if_eq2", read_instantiate [("P", "%x. ?a = x")] expand_if); ``` paulson@3912 ` 653` paulson@3912 ` 654` ```bind_thm ("expand_if_mem1", ``` paulson@3912 ` 655` ``` read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] expand_if); ``` paulson@3912 ` 656` ```bind_thm ("expand_if_mem2", ``` paulson@3912 ` 657` ``` read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] expand_if); ``` paulson@3912 ` 658` paulson@3912 ` 659` ```val expand_ifs = [if_bool_eq, expand_if_eq1, expand_if_eq2, ``` paulson@3912 ` 660` ``` expand_if_mem1, expand_if_mem2]; ``` paulson@3912 ` 661` paulson@3912 ` 662` wenzelm@4089 ` 663` ```(*Each of these has ALREADY been added to simpset() above.*) ``` paulson@2024 ` 664` ```val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, ``` paulson@2499 ` 665` ``` mem_Collect_eq, ``` paulson@2499 ` 666` ``` UN_iff, UN1_iff, Union_iff, ``` paulson@2499 ` 667` ``` INT_iff, INT1_iff, Inter_iff]; ``` oheimb@1776 ` 668` paulson@1937 ` 669` ```(*Not for Addsimps -- it can cause goals to blow up!*) ``` paulson@1937 ` 670` ```goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))"; ``` wenzelm@4089 ` 671` ```by (simp_tac (simpset() addsplits [expand_if]) 1); ``` paulson@1937 ` 672` ```qed "mem_if"; ``` paulson@1937 ` 673` oheimb@1776 ` 674` ```val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs; ``` oheimb@1776 ` 675` wenzelm@4089 ` 676` ```simpset_ref() := simpset() addcongs [ball_cong,bex_cong] ``` oheimb@1776 ` 677` ``` setmksimps (mksimps mksimps_pairs); ``` nipkow@3222 ` 678` nipkow@3222 ` 679` ```Addsimps[subset_UNIV, empty_subsetI, subset_refl]; ``` nipkow@3222 ` 680` nipkow@3222 ` 681` nipkow@3222 ` 682` ```(*** < ***) ``` nipkow@3222 ` 683` nipkow@3222 ` 684` ```goalw Set.thy [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A (x ~: A) & A<=B | x:A & A-{x}