converted theory "Set";
authorwenzelm
Sun Oct 28 22:59:12 2001 +0100 (2001-10-28)
changeset 119790a3dace545c5
parent 11978 a394d3e9c8bb
child 11980 98a1bb0bfd3a
converted theory "Set";
src/HOL/Set.ML
src/HOL/Set.thy
src/HOL/Typedef.thy
src/HOL/subset.ML
     1.1 --- a/src/HOL/Set.ML	Sun Oct 28 22:58:39 2001 +0100
     1.2 +++ b/src/HOL/Set.ML	Sun Oct 28 22:59:12 2001 +0100
     1.3 @@ -1,845 +1,26 @@
     1.4 -(*  Title:      HOL/Set.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1991  University of Cambridge
     1.8  
     1.9 -Set theory for higher-order logic.  A set is simply a predicate.
    1.10 -*)
    1.11 -
    1.12 -section "Relating predicates and sets";
    1.13 -
    1.14 -Addsimps [Collect_mem_eq];
    1.15 -AddIffs  [mem_Collect_eq];
    1.16 -
    1.17 -Goal "P(a) ==> a : {x. P(x)}";
    1.18 -by (Asm_simp_tac 1);
    1.19 -qed "CollectI";
    1.20 -
    1.21 -Goal "a : {x. P(x)} ==> P(a)";
    1.22 -by (Asm_full_simp_tac 1);
    1.23 -qed "CollectD";
    1.24 -
    1.25 -val [prem] = Goal "(!!x. (x:A) = (x:B)) ==> A = B";
    1.26 -by (rtac (prem RS ext RS arg_cong RS box_equals) 1);
    1.27 -by (rtac Collect_mem_eq 1);
    1.28 -by (rtac Collect_mem_eq 1);
    1.29 -qed "set_ext";
    1.30 -
    1.31 -val [prem] = Goal "(!!x. P(x)=Q(x)) ==> {x. P(x)} = {x. Q(x)}";
    1.32 -by (rtac (prem RS ext RS arg_cong) 1);
    1.33 -qed "Collect_cong";
    1.34 -
    1.35 -bind_thm ("CollectE", make_elim CollectD);
    1.36 -
    1.37 -AddSIs [CollectI];
    1.38 -AddSEs [CollectE];
    1.39 -
    1.40 -
    1.41 -section "Bounded quantifiers";
    1.42 -
    1.43 -val prems = Goalw [Ball_def]
    1.44 -    "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)";
    1.45 -by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
    1.46 -qed "ballI";
    1.47 -
    1.48 -bind_thms ("strip", [impI, allI, ballI]);
    1.49 -
    1.50 -Goalw [Ball_def] "[| ALL x:A. P(x);  x:A |] ==> P(x)";
    1.51 -by (Blast_tac 1);
    1.52 -qed "bspec";
    1.53 -
    1.54 -val major::prems = Goalw [Ball_def]
    1.55 -    "[| ALL x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q";
    1.56 -by (rtac (major RS spec RS impCE) 1);
    1.57 -by (REPEAT (eresolve_tac prems 1));
    1.58 -qed "ballE";
    1.59 -
    1.60 -(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
    1.61 -fun ball_tac i = etac ballE i THEN contr_tac (i+1);
    1.62 -
    1.63 -AddSIs [ballI];
    1.64 -AddEs  [ballE];
    1.65 -AddXDs [bspec];
    1.66 -(* gives better instantiation for bound: *)
    1.67 -claset_ref() := claset() addbefore ("bspec", datac bspec 1);
    1.68 -
    1.69 -(*Normally the best argument order: P(x) constrains the choice of x:A*)
    1.70 -Goalw [Bex_def] "[| P(x);  x:A |] ==> EX x:A. P(x)";
    1.71 -by (Blast_tac 1);
    1.72 -qed "bexI";
    1.73 -
    1.74 -(*The best argument order when there is only one x:A*)
    1.75 -Goalw [Bex_def] "[| x:A;  P(x) |] ==> EX x:A. P(x)";
    1.76 -by (Blast_tac 1);
    1.77 -qed "rev_bexI";
    1.78 -
    1.79 -val prems = Goal 
    1.80 -   "[| ALL x:A. ~P(x) ==> P(a);  a:A |] ==> EX x:A. P(x)";
    1.81 -by (rtac classical 1);
    1.82 -by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1))  ;
    1.83 -qed "bexCI";
    1.84 -
    1.85 -val major::prems = Goalw [Bex_def]
    1.86 -    "[| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q";
    1.87 -by (rtac (major RS exE) 1);
    1.88 -by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1));
    1.89 -qed "bexE";
    1.90 -
    1.91 -AddIs  [bexI];
    1.92 -AddSEs [bexE];
    1.93 -
    1.94 -(*Trival rewrite rule*)
    1.95 -Goal "(ALL x:A. P) = ((EX x. x:A) --> P)";
    1.96 -by (simp_tac (simpset() addsimps [Ball_def]) 1);
    1.97 -qed "ball_triv";
    1.98 -
    1.99 -(*Dual form for existentials*)
   1.100 -Goal "(EX x:A. P) = ((EX x. x:A) & P)";
   1.101 -by (simp_tac (simpset() addsimps [Bex_def]) 1);
   1.102 -qed "bex_triv";
   1.103 -
   1.104 -Addsimps [ball_triv, bex_triv];
   1.105 -
   1.106 -Goal "(EX x:A. x=a) = (a:A)";
   1.107 -by(Blast_tac 1);
   1.108 -qed "bex_triv_one_point1";
   1.109 -
   1.110 -Goal "(EX x:A. a=x) = (a:A)";
   1.111 -by(Blast_tac 1);
   1.112 -qed "bex_triv_one_point2";
   1.113 -
   1.114 -Goal "(EX x:A. x=a & P x) = (a:A & P a)";
   1.115 -by(Blast_tac 1);
   1.116 -qed "bex_one_point1";
   1.117 -
   1.118 -Goal "(EX x:A. a=x & P x) = (a:A & P a)";
   1.119 -by(Blast_tac 1);
   1.120 -qed "bex_one_point2";
   1.121 -
   1.122 -Goal "(ALL x:A. x=a --> P x) = (a:A --> P a)";
   1.123 -by(Blast_tac 1);
   1.124 -qed "ball_one_point1";
   1.125 -
   1.126 -Goal "(ALL x:A. a=x --> P x) = (a:A --> P a)";
   1.127 -by(Blast_tac 1);
   1.128 -qed "ball_one_point2";
   1.129 -
   1.130 -Addsimps [bex_triv_one_point1,bex_triv_one_point2,
   1.131 -          bex_one_point1,bex_one_point2,
   1.132 -          ball_one_point1,ball_one_point2];
   1.133 -
   1.134 -let
   1.135 -val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
   1.136 -    ("EX x:A. P(x) & Q(x)",HOLogic.boolT)
   1.137 -
   1.138 -val prove_bex_tac = rewrite_goals_tac [Bex_def] THEN
   1.139 -                    Quantifier1.prove_one_point_ex_tac;
   1.140 -
   1.141 -val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
   1.142 -
   1.143 -val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
   1.144 -    ("ALL x:A. P(x) --> Q(x)",HOLogic.boolT)
   1.145 -
   1.146 -val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN
   1.147 -                     Quantifier1.prove_one_point_all_tac;
   1.148 -
   1.149 -val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
   1.150 -
   1.151 -val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex;
   1.152 -val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball;
   1.153 -in
   1.154 -
   1.155 -Addsimprocs [defBALL_regroup,defBEX_regroup]
   1.156 -
   1.157 -end;
   1.158 -
   1.159 -(** Congruence rules **)
   1.160 -
   1.161 -val prems = Goalw [Ball_def]
   1.162 -    "[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
   1.163 -\    (ALL x:A. P(x)) = (ALL x:B. Q(x))";
   1.164 -by (asm_simp_tac (simpset() addsimps prems) 1);
   1.165 -qed "ball_cong";
   1.166 -
   1.167 -val prems = Goalw [Bex_def]
   1.168 -    "[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
   1.169 -\    (EX x:A. P(x)) = (EX x:B. Q(x))";
   1.170 -by (asm_simp_tac (simpset() addcongs [conj_cong] addsimps prems) 1);
   1.171 -qed "bex_cong";
   1.172 -
   1.173 -Addcongs [ball_cong,bex_cong];
   1.174 -
   1.175 -section "Subsets";
   1.176 -
   1.177 -val prems = Goalw [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
   1.178 -by (REPEAT (ares_tac (prems @ [ballI]) 1));
   1.179 -qed "subsetI";
   1.180 -
   1.181 -(*Map the type ('a set => anything) to just 'a.
   1.182 -  For overloading constants whose first argument has type "'a set" *)
   1.183 -fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type);
   1.184 -
   1.185 -(*While (:) is not, its type must be kept
   1.186 -  for overloading of = to work.*)
   1.187 -Blast.overloaded ("op :", domain_type);
   1.188 -
   1.189 -overload_1st_set "Ball";		(*need UNION, INTER also?*)
   1.190 -overload_1st_set "Bex";
   1.191 -
   1.192 -(*Image: retain the type of the set being expressed*)
   1.193 -Blast.overloaded ("image", domain_type);
   1.194 -
   1.195 -(*Rule in Modus Ponens style*)
   1.196 -Goalw [subset_def] "[| A <= B;  c:A |] ==> c:B";
   1.197 -by (Blast_tac 1);
   1.198 -qed "subsetD";
   1.199 -AddXIs [subsetD];
   1.200 -
   1.201 -(*The same, with reversed premises for use with etac -- cf rev_mp*)
   1.202 -Goal "[| c:A;  A <= B |] ==> c:B";
   1.203 -by (REPEAT (ares_tac [subsetD] 1)) ;
   1.204 -qed "rev_subsetD";
   1.205 -AddXIs [rev_subsetD];
   1.206 -
   1.207 -(*Converts A<=B to x:A ==> x:B*)
   1.208 -fun impOfSubs th = th RSN (2, rev_subsetD);
   1.209 -
   1.210 -(*Classical elimination rule*)
   1.211 -val major::prems = Goalw [subset_def] 
   1.212 -    "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P";
   1.213 -by (rtac (major RS ballE) 1);
   1.214 -by (REPEAT (eresolve_tac prems 1));
   1.215 -qed "subsetCE";
   1.216 -
   1.217 -(*Takes assumptions A<=B; c:A and creates the assumption c:B *)
   1.218 -fun set_mp_tac i = etac subsetCE i  THEN  mp_tac i;
   1.219 -
   1.220 -AddSIs [subsetI];
   1.221 -AddEs  [subsetD, subsetCE];
   1.222 -
   1.223 -Goal "[| A <= B; c ~: B |] ==> c ~: A";
   1.224 -by (Blast_tac 1);
   1.225 -qed "contra_subsetD";
   1.226 -
   1.227 -Goal "A <= (A::'a set)";
   1.228 -by (Fast_tac 1);
   1.229 -qed "subset_refl";
   1.230 -
   1.231 -Goal "[| A<=B;  B<=C |] ==> A<=(C::'a set)";
   1.232 -by (Blast_tac 1);
   1.233 -qed "subset_trans";
   1.234 -
   1.235 -
   1.236 -section "Equality";
   1.237 -
   1.238 -(*Anti-symmetry of the subset relation*)
   1.239 -Goal "[| A <= B;  B <= A |] ==> A = (B::'a set)";
   1.240 -by (rtac set_ext 1);
   1.241 -by (blast_tac (claset() addIs [subsetD]) 1);
   1.242 -qed "subset_antisym";
   1.243 -bind_thm ("equalityI", subset_antisym);
   1.244 -
   1.245 -AddSIs [equalityI];
   1.246 -
   1.247 -(* Equality rules from ZF set theory -- are they appropriate here? *)
   1.248 -Goal "A = B ==> A<=(B::'a set)";
   1.249 -by (etac ssubst 1);
   1.250 -by (rtac subset_refl 1);
   1.251 -qed "equalityD1";
   1.252 -
   1.253 -Goal "A = B ==> B<=(A::'a set)";
   1.254 -by (etac ssubst 1);
   1.255 -by (rtac subset_refl 1);
   1.256 -qed "equalityD2";
   1.257 -
   1.258 -(*Be careful when adding this to the claset as subset_empty is in the simpset:
   1.259 -  A={} goes to {}<=A and A<={} and then back to A={} !*)
   1.260 -val prems = Goal
   1.261 -    "[| A = B;  [| A<=B; B<=(A::'a set) |] ==> P |]  ==>  P";
   1.262 -by (resolve_tac prems 1);
   1.263 -by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
   1.264 -qed "equalityE";
   1.265 -
   1.266 -val major::prems = Goal
   1.267 -    "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P";
   1.268 -by (rtac (major RS equalityE) 1);
   1.269 -by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
   1.270 -qed "equalityCE";
   1.271 -
   1.272 -AddEs [equalityCE];
   1.273 -
   1.274 -(*Lemma for creating induction formulae -- for "pattern matching" on p
   1.275 -  To make the induction hypotheses usable, apply "spec" or "bspec" to
   1.276 -  put universal quantifiers over the free variables in p. *)
   1.277 -val prems = Goal 
   1.278 -    "[| p:A;  !!z. z:A ==> p=z --> R |] ==> R";
   1.279 -by (rtac mp 1);
   1.280 -by (REPEAT (resolve_tac (refl::prems) 1));
   1.281 -qed "setup_induction";
   1.282 -
   1.283 -Goal "A = B ==> (x : A) = (x : B)";
   1.284 -by (Asm_simp_tac 1);
   1.285 -qed "eqset_imp_iff";
   1.286 -
   1.287 -
   1.288 -section "The universal set -- UNIV";
   1.289 -
   1.290 -Goalw [UNIV_def] "x : UNIV";
   1.291 -by (rtac CollectI 1);
   1.292 -by (rtac TrueI 1);
   1.293 -qed "UNIV_I";
   1.294 -
   1.295 -Addsimps [UNIV_I];
   1.296 -AddIs    [UNIV_I];  (*unsafe makes it less likely to cause problems*)
   1.297 -
   1.298 -Goal "EX x. x : UNIV";
   1.299 -by (Simp_tac 1);
   1.300 -qed "UNIV_witness";
   1.301 -AddXIs [UNIV_witness];
   1.302 -
   1.303 -Goal "A <= UNIV";
   1.304 -by (rtac subsetI 1);
   1.305 -by (rtac UNIV_I 1);
   1.306 -qed "subset_UNIV";
   1.307 -
   1.308 -(** Eta-contracting these two rules (to remove P) causes them to be ignored
   1.309 -    because of their interaction with congruence rules. **)
   1.310 -
   1.311 -Goalw [Ball_def] "Ball UNIV P = All P";
   1.312 -by (Simp_tac 1);
   1.313 -qed "ball_UNIV";
   1.314 -
   1.315 -Goalw [Bex_def] "Bex UNIV P = Ex P";
   1.316 -by (Simp_tac 1);
   1.317 -qed "bex_UNIV";
   1.318 -Addsimps [ball_UNIV, bex_UNIV];
   1.319 -
   1.320 -
   1.321 -section "The empty set -- {}";
   1.322 -
   1.323 -Goalw [empty_def] "(c : {}) = False";
   1.324 -by (Blast_tac 1) ;
   1.325 -qed "empty_iff";
   1.326 -
   1.327 -Addsimps [empty_iff];
   1.328 -
   1.329 -Goal "a:{} ==> P";
   1.330 -by (Full_simp_tac 1);
   1.331 -qed "emptyE";
   1.332 -
   1.333 -AddSEs [emptyE];
   1.334 -
   1.335 -Goal "{} <= A";
   1.336 -by (Blast_tac 1) ;
   1.337 -qed "empty_subsetI";
   1.338 -
   1.339 -(*One effect is to delete the ASSUMPTION {} <= A*)
   1.340 -AddIffs [empty_subsetI];
   1.341 -
   1.342 -val [prem]= Goal "[| !!y. y:A ==> False |] ==> A={}";
   1.343 -by (blast_tac (claset() addIs [prem RS FalseE]) 1) ;
   1.344 -qed "equals0I";
   1.345 -
   1.346 -(*Use for reasoning about disjointness: A Int B = {} *)
   1.347 -Goal "A={} ==> a ~: A";
   1.348 -by (Blast_tac 1) ;
   1.349 -qed "equals0D";
   1.350 -
   1.351 -Goalw [Ball_def] "Ball {} P = True";
   1.352 -by (Simp_tac 1);
   1.353 -qed "ball_empty";
   1.354 -
   1.355 -Goalw [Bex_def] "Bex {} P = False";
   1.356 -by (Simp_tac 1);
   1.357 -qed "bex_empty";
   1.358 -Addsimps [ball_empty, bex_empty];
   1.359 -
   1.360 -Goal "UNIV ~= {}";
   1.361 -by (blast_tac (claset() addEs [equalityE]) 1);
   1.362 -qed "UNIV_not_empty";
   1.363 -AddIffs [UNIV_not_empty];
   1.364 -
   1.365 -
   1.366 -
   1.367 -section "The Powerset operator -- Pow";
   1.368 -
   1.369 -Goalw [Pow_def] "(A : Pow(B)) = (A <= B)";
   1.370 -by (Asm_simp_tac 1);
   1.371 -qed "Pow_iff";
   1.372 -
   1.373 -AddIffs [Pow_iff]; 
   1.374 -
   1.375 -Goalw [Pow_def] "A <= B ==> A : Pow(B)";
   1.376 -by (etac CollectI 1);
   1.377 -qed "PowI";
   1.378 -
   1.379 -Goalw [Pow_def] "A : Pow(B)  ==>  A<=B";
   1.380 -by (etac CollectD 1);
   1.381 -qed "PowD";
   1.382 -
   1.383 -
   1.384 -bind_thm ("Pow_bottom", empty_subsetI RS PowI);        (* {}: Pow(B) *)
   1.385 -bind_thm ("Pow_top", subset_refl RS PowI);             (* A : Pow(A) *)
   1.386 -
   1.387 -
   1.388 -section "Set complement";
   1.389 -
   1.390 -Goalw [Compl_def] "(c : -A) = (c~:A)";
   1.391 -by (Blast_tac 1);
   1.392 -qed "Compl_iff";
   1.393 -
   1.394 -Addsimps [Compl_iff];
   1.395 -
   1.396 -val prems = Goalw [Compl_def] "[| c:A ==> False |] ==> c : -A";
   1.397 -by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1));
   1.398 -qed "ComplI";
   1.399 -
   1.400 -(*This form, with negated conclusion, works well with the Classical prover.
   1.401 -  Negated assumptions behave like formulae on the right side of the notional
   1.402 -  turnstile...*)
   1.403 -Goalw [Compl_def] "c : -A ==> c~:A";
   1.404 -by (etac CollectD 1);
   1.405 -qed "ComplD";
   1.406 -
   1.407 -bind_thm ("ComplE", make_elim ComplD);
   1.408 -
   1.409 -AddSIs [ComplI];
   1.410 -AddSEs [ComplE];
   1.411 -
   1.412 -
   1.413 -section "Binary union -- Un";
   1.414 -
   1.415 -Goalw [Un_def] "(c : A Un B) = (c:A | c:B)";
   1.416 -by (Blast_tac 1);
   1.417 -qed "Un_iff";
   1.418 -Addsimps [Un_iff];
   1.419 -
   1.420 -Goal "c:A ==> c : A Un B";
   1.421 -by (Asm_simp_tac 1);
   1.422 -qed "UnI1";
   1.423 +(* legacy ML bindings *)
   1.424  
   1.425 -Goal "c:B ==> c : A Un B";
   1.426 -by (Asm_simp_tac 1);
   1.427 -qed "UnI2";
   1.428 -
   1.429 -AddXEs [UnI1, UnI2];
   1.430 -
   1.431 -
   1.432 -(*Classical introduction rule: no commitment to A vs B*)
   1.433 -
   1.434 -val prems = Goal "(c~:B ==> c:A) ==> c : A Un B";
   1.435 -by (Simp_tac 1);
   1.436 -by (REPEAT (ares_tac (prems@[disjCI]) 1)) ;
   1.437 -qed "UnCI";
   1.438 -
   1.439 -val major::prems = Goalw [Un_def]
   1.440 -    "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P";
   1.441 -by (rtac (major RS CollectD RS disjE) 1);
   1.442 -by (REPEAT (eresolve_tac prems 1));
   1.443 -qed "UnE";
   1.444 -
   1.445 -AddSIs [UnCI];
   1.446 -AddSEs [UnE];
   1.447 -
   1.448 -
   1.449 -section "Binary intersection -- Int";
   1.450 -
   1.451 -Goalw [Int_def] "(c : A Int B) = (c:A & c:B)";
   1.452 -by (Blast_tac 1);
   1.453 -qed "Int_iff";
   1.454 -Addsimps [Int_iff];
   1.455 -
   1.456 -Goal "[| c:A;  c:B |] ==> c : A Int B";
   1.457 -by (Asm_simp_tac 1);
   1.458 -qed "IntI";
   1.459 -
   1.460 -Goal "c : A Int B ==> c:A";
   1.461 -by (Asm_full_simp_tac 1);
   1.462 -qed "IntD1";
   1.463 -
   1.464 -Goal "c : A Int B ==> c:B";
   1.465 -by (Asm_full_simp_tac 1);
   1.466 -qed "IntD2";
   1.467 -
   1.468 -val [major,minor] = Goal
   1.469 -    "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P";
   1.470 -by (rtac minor 1);
   1.471 -by (rtac (major RS IntD1) 1);
   1.472 -by (rtac (major RS IntD2) 1);
   1.473 -qed "IntE";
   1.474 -
   1.475 -AddSIs [IntI];
   1.476 -AddSEs [IntE];
   1.477 -
   1.478 -section "Set difference";
   1.479 -
   1.480 -Goalw [set_diff_def] "(c : A-B) = (c:A & c~:B)";
   1.481 -by (Blast_tac 1);
   1.482 -qed "Diff_iff";
   1.483 -Addsimps [Diff_iff];
   1.484 -
   1.485 -Goal "[| c : A;  c ~: B |] ==> c : A - B";
   1.486 -by (Asm_simp_tac 1) ;
   1.487 -qed "DiffI";
   1.488 -
   1.489 -Goal "c : A - B ==> c : A";
   1.490 -by (Asm_full_simp_tac 1) ;
   1.491 -qed "DiffD1";
   1.492 -
   1.493 -Goal "[| c : A - B;  c : B |] ==> P";
   1.494 -by (Asm_full_simp_tac 1) ;
   1.495 -qed "DiffD2";
   1.496 -
   1.497 -val prems = Goal "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P";
   1.498 -by (resolve_tac prems 1);
   1.499 -by (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ;
   1.500 -qed "DiffE";
   1.501 -
   1.502 -AddSIs [DiffI];
   1.503 -AddSEs [DiffE];
   1.504 -
   1.505 -
   1.506 -section "Augmenting a set -- insert";
   1.507 -
   1.508 -Goalw [insert_def] "(a : insert b A) = (a=b | a:A)";
   1.509 -by (Blast_tac 1);
   1.510 -qed "insert_iff";
   1.511 -Addsimps [insert_iff];
   1.512 -
   1.513 -Goal "a : insert a B";
   1.514 -by (Simp_tac 1);
   1.515 -qed "insertI1";
   1.516 -
   1.517 -Goal "!!a. a : B ==> a : insert b B";
   1.518 -by (Asm_simp_tac 1);
   1.519 -qed "insertI2";
   1.520 -
   1.521 -val major::prems = Goalw [insert_def]
   1.522 -    "[| a : insert b A;  a=b ==> P;  a:A ==> P |] ==> P";
   1.523 -by (rtac (major RS UnE) 1);
   1.524 -by (REPEAT (eresolve_tac (prems @ [CollectE]) 1));
   1.525 -qed "insertE";
   1.526 -
   1.527 -(*Classical introduction rule*)
   1.528 -val prems = Goal "(a~:B ==> a=b) ==> a: insert b B";
   1.529 -by (Simp_tac 1);
   1.530 -by (REPEAT (ares_tac (prems@[disjCI]) 1)) ;
   1.531 -qed "insertCI";
   1.532 -
   1.533 -AddSIs [insertCI]; 
   1.534 -AddSEs [insertE];
   1.535 -
   1.536 -Goal "(A <= insert x B) = (if x:A then A-{x} <= B else A<=B)";
   1.537 -by Auto_tac; 
   1.538 -qed "subset_insert_iff";
   1.539 -
   1.540 -section "Singletons, using insert";
   1.541 -
   1.542 -Goal "a : {a}";
   1.543 -by (rtac insertI1 1) ;
   1.544 -qed "singletonI";
   1.545 -
   1.546 -Goal "b : {a} ==> b=a";
   1.547 -by (Blast_tac 1);
   1.548 -qed "singletonD";
   1.549 -
   1.550 -bind_thm ("singletonE", make_elim singletonD);
   1.551 -
   1.552 -Goal "(b : {a}) = (b=a)";
   1.553 -by (Blast_tac 1);
   1.554 -qed "singleton_iff";
   1.555 -
   1.556 -Goal "{a}={b} ==> a=b";
   1.557 -by (blast_tac (claset() addEs [equalityE]) 1);
   1.558 -qed "singleton_inject";
   1.559 -
   1.560 -(*Redundant? But unlike insertCI, it proves the subgoal immediately!*)
   1.561 -AddSIs [singletonI];   
   1.562 -AddSDs [singleton_inject];
   1.563 -AddSEs [singletonE];
   1.564 -
   1.565 -Goal "({b} = insert a A) = (a = b & A <= {b})";
   1.566 -by (blast_tac (claset() addSEs [equalityE]) 1);
   1.567 -qed "singleton_insert_inj_eq";
   1.568 -
   1.569 -Goal "(insert a A = {b}) = (a = b & A <= {b})";
   1.570 -by (blast_tac (claset() addSEs [equalityE]) 1);
   1.571 -qed "singleton_insert_inj_eq'";
   1.572 -
   1.573 -AddIffs [singleton_insert_inj_eq, singleton_insert_inj_eq'];
   1.574 -
   1.575 -Goal "A <= {x} ==> A={} | A = {x}";
   1.576 -by (Fast_tac 1);
   1.577 -qed "subset_singletonD";
   1.578 -
   1.579 -Goal "{x. x=a} = {a}";
   1.580 -by (Blast_tac 1);
   1.581 -qed "singleton_conv";
   1.582 -Addsimps [singleton_conv];
   1.583 -
   1.584 -Goal "{x. a=x} = {a}";
   1.585 -by (Blast_tac 1);
   1.586 -qed "singleton_conv2";
   1.587 -Addsimps [singleton_conv2];
   1.588 -
   1.589 -Goal "[| A - {x} <= B; x : A |] ==> A <= insert x B"; 
   1.590 -by(Blast_tac 1);
   1.591 -qed "diff_single_insert";
   1.592 -
   1.593 -
   1.594 -section "Unions of families -- UNION x:A. B(x) is Union(B`A)";
   1.595 -
   1.596 -Goalw [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))";
   1.597 -by (Blast_tac 1);
   1.598 -qed "UN_iff";
   1.599 -
   1.600 -Addsimps [UN_iff];
   1.601 -
   1.602 -(*The order of the premises presupposes that A is rigid; b may be flexible*)
   1.603 -Goal "[| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))";
   1.604 -by Auto_tac;
   1.605 -qed "UN_I";
   1.606 -
   1.607 -val major::prems = Goalw [UNION_def]
   1.608 -    "[| b : (UN x:A. B(x));  !!x.[| x:A;  b: B(x) |] ==> R |] ==> R";
   1.609 -by (rtac (major RS CollectD RS bexE) 1);
   1.610 -by (REPEAT (ares_tac prems 1));
   1.611 -qed "UN_E";
   1.612 -
   1.613 -AddIs  [UN_I];
   1.614 -AddSEs [UN_E];
   1.615 -
   1.616 -val prems = Goalw [UNION_def]
   1.617 -    "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
   1.618 -\    (UN x:A. C(x)) = (UN x:B. D(x))";
   1.619 -by (asm_simp_tac (simpset() addsimps prems) 1);
   1.620 -qed "UN_cong";
   1.621 -Addcongs [UN_cong];
   1.622 -
   1.623 -
   1.624 -section "Intersections of families -- INTER x:A. B(x) is Inter(B`A)";
   1.625 -
   1.626 -Goalw [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))";
   1.627 -by Auto_tac;
   1.628 -qed "INT_iff";
   1.629 -
   1.630 -Addsimps [INT_iff];
   1.631 -
   1.632 -val prems = Goalw [INTER_def]
   1.633 -    "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))";
   1.634 -by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
   1.635 -qed "INT_I";
   1.636 -
   1.637 -Goal "[| b : (INT x:A. B(x));  a:A |] ==> b: B(a)";
   1.638 -by Auto_tac;
   1.639 -qed "INT_D";
   1.640 -
   1.641 -(*"Classical" elimination -- by the Excluded Middle on a:A *)
   1.642 -val major::prems = Goalw [INTER_def]
   1.643 -    "[| b : (INT x:A. B(x));  b: B(a) ==> R;  a~:A ==> R |] ==> R";
   1.644 -by (rtac (major RS CollectD RS ballE) 1);
   1.645 -by (REPEAT (eresolve_tac prems 1));
   1.646 -qed "INT_E";
   1.647 -
   1.648 -AddSIs [INT_I];
   1.649 -AddEs  [INT_D, INT_E];
   1.650 -
   1.651 -val prems = Goalw [INTER_def]
   1.652 -    "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
   1.653 -\    (INT x:A. C(x)) = (INT x:B. D(x))";
   1.654 -by (asm_simp_tac (simpset() addsimps prems) 1);
   1.655 -qed "INT_cong";
   1.656 -Addcongs [INT_cong];
   1.657 -
   1.658 -
   1.659 -section "Union";
   1.660 -
   1.661 -Goalw [Union_def] "(A : Union(C)) = (EX X:C. A:X)";
   1.662 -by (Blast_tac 1);
   1.663 -qed "Union_iff";
   1.664 -
   1.665 -Addsimps [Union_iff];
   1.666 -
   1.667 -(*The order of the premises presupposes that C is rigid; A may be flexible*)
   1.668 -Goal "[| X:C;  A:X |] ==> A : Union(C)";
   1.669 -by Auto_tac;
   1.670 -qed "UnionI";
   1.671 -
   1.672 -val major::prems = Goalw [Union_def]
   1.673 -    "[| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R";
   1.674 -by (rtac (major RS UN_E) 1);
   1.675 -by (REPEAT (ares_tac prems 1));
   1.676 -qed "UnionE";
   1.677 -
   1.678 -AddIs  [UnionI];
   1.679 -AddSEs [UnionE];
   1.680 -
   1.681 -
   1.682 -section "Inter";
   1.683 -
   1.684 -Goalw [Inter_def] "(A : Inter(C)) = (ALL X:C. A:X)";
   1.685 -by (Blast_tac 1);
   1.686 -qed "Inter_iff";
   1.687 -
   1.688 -Addsimps [Inter_iff];
   1.689 -
   1.690 -val prems = Goalw [Inter_def]
   1.691 -    "[| !!X. X:C ==> A:X |] ==> A : Inter(C)";
   1.692 -by (REPEAT (ares_tac ([INT_I] @ prems) 1));
   1.693 -qed "InterI";
   1.694 -
   1.695 -(*A "destruct" rule -- every X in C contains A as an element, but
   1.696 -  A:X can hold when X:C does not!  This rule is analogous to "spec". *)
   1.697 -Goal "[| A : Inter(C);  X:C |] ==> A:X";
   1.698 -by Auto_tac;
   1.699 -qed "InterD";
   1.700 -
   1.701 -(*"Classical" elimination rule -- does not require proving X:C *)
   1.702 -val major::prems = Goalw [Inter_def]
   1.703 -    "[| A : Inter(C);  X~:C ==> R;  A:X ==> R |] ==> R";
   1.704 -by (rtac (major RS INT_E) 1);
   1.705 -by (REPEAT (eresolve_tac prems 1));
   1.706 -qed "InterE";
   1.707 -
   1.708 -AddSIs [InterI];
   1.709 -AddEs  [InterD, InterE];
   1.710 -
   1.711 -
   1.712 -(*** Image of a set under a function ***)
   1.713 -
   1.714 -(*Frequently b does not have the syntactic form of f(x).*)
   1.715 -Goalw [image_def] "[| b=f(x);  x:A |] ==> b : f`A";
   1.716 -by (Blast_tac 1);
   1.717 -qed "image_eqI";
   1.718 -Addsimps [image_eqI];
   1.719 -
   1.720 -bind_thm ("imageI", refl RS image_eqI);
   1.721 -
   1.722 -(*This version's more effective when we already have the required x*)
   1.723 -Goalw [image_def] "[| x:A;  b=f(x) |] ==> b : f`A";
   1.724 -by (Blast_tac 1);
   1.725 -qed "rev_image_eqI";
   1.726 -
   1.727 -(*The eta-expansion gives variable-name preservation.*)
   1.728 -val major::prems = Goalw [image_def]
   1.729 -    "[| b : (%x. f(x))`A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
   1.730 -by (rtac (major RS CollectD RS bexE) 1);
   1.731 -by (REPEAT (ares_tac prems 1));
   1.732 -qed "imageE";
   1.733 -
   1.734 -AddIs  [image_eqI];
   1.735 -AddSEs [imageE]; 
   1.736 -
   1.737 -Goal "f`(A Un B) = f`A Un f`B";
   1.738 -by (Blast_tac 1);
   1.739 -qed "image_Un";
   1.740 -
   1.741 -Goal "(z : f`A) = (EX x:A. z = f x)";
   1.742 -by (Blast_tac 1);
   1.743 -qed "image_iff";
   1.744 -
   1.745 -(*This rewrite rule would confuse users if made default.*)
   1.746 -Goal "(f`A <= B) = (ALL x:A. f(x): B)";
   1.747 -by (Blast_tac 1);
   1.748 -qed "image_subset_iff";
   1.749 -
   1.750 -Goal "(B <= f ` A) = (? AA. AA <= A & B = f ` AA)";
   1.751 -by Safe_tac;
   1.752 -by  (Fast_tac 2);
   1.753 -by (res_inst_tac [("x","{a. a : A & f a : B}")] exI 1);
   1.754 -by (Fast_tac 1);
   1.755 -qed "subset_image_iff";
   1.756 -
   1.757 -(*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too
   1.758 -  many existing proofs.*)
   1.759 -val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f`A <= B";
   1.760 -by (blast_tac (claset() addIs prems) 1);
   1.761 -qed "image_subsetI";
   1.762 -
   1.763 -(*** Range of a function -- just a translation for image! ***)
   1.764 -
   1.765 -Goal "b=f(x) ==> b : range(f)";
   1.766 -by (EVERY1 [etac image_eqI, rtac UNIV_I]);
   1.767 -bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI));
   1.768 -
   1.769 -bind_thm ("rangeI", UNIV_I RS imageI);
   1.770 -
   1.771 -val [major,minor] = Goal 
   1.772 -    "[| b : range(%x. f(x));  !!x. b=f(x) ==> P |] ==> P"; 
   1.773 -by (rtac (major RS imageE) 1);
   1.774 -by (etac minor 1);
   1.775 -qed "rangeE";
   1.776 -AddXEs [rangeE];
   1.777 -
   1.778 -
   1.779 -(*** Set reasoning tools ***)
   1.780 -
   1.781 -
   1.782 -(** Rewrite rules for boolean case-splitting: faster than 
   1.783 -	addsplits[split_if]
   1.784 -**)
   1.785 -
   1.786 -bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if);
   1.787 -bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if);
   1.788 -
   1.789 -(*Split ifs on either side of the membership relation.
   1.790 -	Not for Addsimps -- can cause goals to blow up!*)
   1.791 -bind_thm ("split_if_mem1", inst "P" "%x. x : ?b" split_if);
   1.792 -bind_thm ("split_if_mem2", inst "P" "%x. ?a : x" split_if);
   1.793 -
   1.794 -bind_thms ("split_ifs", [if_bool_eq_conj, split_if_eq1, split_if_eq2,
   1.795 -			 split_if_mem1, split_if_mem2]);
   1.796 -
   1.797 -
   1.798 -(*Each of these has ALREADY been added to simpset() above.*)
   1.799 -bind_thms ("mem_simps", [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
   1.800 -                 mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff]);
   1.801 -
   1.802 -(*Would like to add these, but the existing code only searches for the 
   1.803 -  outer-level constant, which in this case is just "op :"; we instead need
   1.804 -  to use term-nets to associate patterns with rules.  Also, if a rule fails to
   1.805 -  apply, then the formula should be kept.
   1.806 -  [("uminus", Compl_iff RS iffD1), ("op -", [Diff_iff RS iffD1]), 
   1.807 -   ("op Int", [IntD1,IntD2]),
   1.808 -   ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
   1.809 - *)
   1.810 -val mksimps_pairs =
   1.811 -  [("Ball",[bspec])] @ mksimps_pairs;
   1.812 -
   1.813 -simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs);
   1.814 -
   1.815 -Addsimps[subset_UNIV, subset_refl];
   1.816 -
   1.817 -
   1.818 -(*** The 'proper subset' relation (<) ***)
   1.819 -
   1.820 -Goalw [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B";
   1.821 -by (Blast_tac 1);
   1.822 -qed "psubsetI";
   1.823 -AddSIs [psubsetI];
   1.824 -
   1.825 -Goalw [psubset_def]
   1.826 -  "(A < insert x B) = (if x:B then A<B else if x:A then A-{x} < B else A<=B)";
   1.827 -by (asm_simp_tac (simpset() addsimps [subset_insert_iff]) 1);
   1.828 -by (Blast_tac 1); 
   1.829 -qed "psubset_insert_iff";
   1.830 -
   1.831 -bind_thm ("psubset_eq", psubset_def RS meta_eq_to_obj_eq);
   1.832 -
   1.833 -bind_thm ("psubset_imp_subset", psubset_eq RS iffD1 RS conjunct1);
   1.834 -
   1.835 -Goal"[| (A::'a set) < B; B <= C |] ==> A < C";
   1.836 -by (auto_tac (claset(), simpset() addsimps [psubset_eq]));
   1.837 -qed "psubset_subset_trans";
   1.838 -
   1.839 -Goal"[| (A::'a set) <= B; B < C|] ==> A < C";
   1.840 -by (auto_tac (claset(), simpset() addsimps [psubset_eq]));
   1.841 -qed "subset_psubset_trans";
   1.842 -
   1.843 -Goalw [psubset_def] "A < B ==> EX b. b : (B - A)";
   1.844 -by (Blast_tac 1);
   1.845 -qed "psubset_imp_ex_mem";
   1.846 -
   1.847 -Goal "(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)";
   1.848 -by (simp_tac (simpset () addsimps [Ball_def, thm "atomize_all", thm "atomize_imp"]) 1);
   1.849 -qed "atomize_ball";
   1.850 +structure Set =
   1.851 +struct
   1.852 +  val thy = the_context ();
   1.853 +  val Ball_def = Ball_def;
   1.854 +  val Bex_def = Bex_def;
   1.855 +  val Collect_mem_eq = Collect_mem_eq;
   1.856 +  val Compl_def = Compl_def;
   1.857 +  val INTER_def = INTER_def;
   1.858 +  val Int_def = Int_def;
   1.859 +  val Inter_def = Inter_def;
   1.860 +  val Pow_def = Pow_def;
   1.861 +  val UNION_def = UNION_def;
   1.862 +  val UNIV_def = UNIV_def;
   1.863 +  val Un_def = Un_def;
   1.864 +  val Union_def = Union_def;
   1.865 +  val empty_def = empty_def;
   1.866 +  val image_def = image_def;
   1.867 +  val insert_def = insert_def;
   1.868 +  val mem_Collect_eq = mem_Collect_eq;
   1.869 +  val psubset_def = psubset_def;
   1.870 +  val set_diff_def = set_diff_def;
   1.871 +  val subset_def = subset_def;
   1.872 +end;
     2.1 --- a/src/HOL/Set.thy	Sun Oct 28 22:58:39 2001 +0100
     2.2 +++ b/src/HOL/Set.thy	Sun Oct 28 22:59:12 2001 +0100
     2.3 @@ -4,70 +4,71 @@
     2.4      Copyright   1993  University of Cambridge
     2.5  *)
     2.6  
     2.7 -Set = HOL +
     2.8 +header {* Set theory for higher-order logic *}
     2.9 +
    2.10 +theory Set = HOL
    2.11 +files ("subset.ML") ("equalities.ML") ("mono.ML"):
    2.12 +
    2.13 +text {* A set in HOL is simply a predicate. *}
    2.14  
    2.15  
    2.16 -(** Core syntax **)
    2.17 +subsection {* Basic syntax *}
    2.18  
    2.19  global
    2.20  
    2.21 -types
    2.22 -  'a set
    2.23 -
    2.24 -arities
    2.25 -  set :: (term) term
    2.26 -
    2.27 -instance
    2.28 -  set :: (term) {ord, minus}
    2.29 -
    2.30 -syntax
    2.31 -  "op :"        :: ['a, 'a set] => bool             ("op :")
    2.32 +typedecl 'a set
    2.33 +arities set :: ("term") "term"
    2.34  
    2.35  consts
    2.36 -  "{}"          :: 'a set                           ("{}")
    2.37 -  UNIV          :: 'a set
    2.38 -  insert        :: ['a, 'a set] => 'a set
    2.39 -  Collect       :: ('a => bool) => 'a set               (*comprehension*)
    2.40 -  Int           :: ['a set, 'a set] => 'a set       (infixl 70)
    2.41 -  Un            :: ['a set, 'a set] => 'a set       (infixl 65)
    2.42 -  UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
    2.43 -  Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
    2.44 -  Pow           :: 'a set => 'a set set                 (*powerset*)
    2.45 -  Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
    2.46 -  "image"       :: ['a => 'b, 'a set] => ('b set)   (infixr "`" 90)
    2.47 -  (*membership*)
    2.48 -  "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
    2.49 +  "{}"          :: "'a set"                             ("{}")
    2.50 +  UNIV          :: "'a set"
    2.51 +  insert        :: "'a => 'a set => 'a set"
    2.52 +  Collect       :: "('a => bool) => 'a set"              -- "comprehension"
    2.53 +  Int           :: "'a set => 'a set => 'a set"          (infixl 70)
    2.54 +  Un            :: "'a set => 'a set => 'a set"          (infixl 65)
    2.55 +  UNION         :: "'a set => ('a => 'b set) => 'b set"  -- "general union"
    2.56 +  INTER         :: "'a set => ('a => 'b set) => 'b set"  -- "general intersection"
    2.57 +  Union         :: "'a set set => 'a set"                -- "union of a set"
    2.58 +  Inter         :: "'a set set => 'a set"                -- "intersection of a set"
    2.59 +  Pow           :: "'a set => 'a set set"                -- "powerset"
    2.60 +  Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
    2.61 +  Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
    2.62 +  image         :: "('a => 'b) => 'a set => 'b set"      (infixr "`" 90)
    2.63 +
    2.64 +syntax
    2.65 +  "op :"        :: "'a => 'a set => bool"                ("op :")
    2.66 +consts
    2.67 +  "op :"        :: "'a => 'a set => bool"                ("(_/ : _)" [50, 51] 50)  -- "membership"
    2.68 +
    2.69 +local
    2.70 +
    2.71 +instance set :: ("term") ord ..
    2.72 +instance set :: ("term") minus ..
    2.73  
    2.74  
    2.75 -(** Additional concrete syntax **)
    2.76 +subsection {* Additional concrete syntax *}
    2.77  
    2.78  syntax
    2.79 -  range         :: ('a => 'b) => 'b set                 (*of function*)
    2.80 -
    2.81 -  (* Infix syntax for non-membership *)
    2.82 +  range         :: "('a => 'b) => 'b set"             -- "of function"
    2.83  
    2.84 -  "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
    2.85 -  "op ~:"       :: ['a, 'a set] => bool               ("(_/ ~: _)" [50, 51] 50)
    2.86 -
    2.87 +  "op ~:"       :: "'a => 'a set => bool"                 ("op ~:")  -- "non-membership"
    2.88 +  "op ~:"       :: "'a => 'a set => bool"                 ("(_/ ~: _)" [50, 51] 50)
    2.89  
    2.90 -  "@Finset"     :: args => 'a set                     ("{(_)}")
    2.91 -  "@Coll"       :: [pttrn, bool] => 'a set            ("(1{_./ _})")
    2.92 -  "@SetCompr"   :: ['a, idts, bool] => 'a set         ("(1{_ |/_./ _})")
    2.93 -
    2.94 -  (* Big Intersection / Union *)
    2.95 +  "@Finset"     :: "args => 'a set"                       ("{(_)}")
    2.96 +  "@Coll"       :: "pttrn => bool => 'a set"              ("(1{_./ _})")
    2.97 +  "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
    2.98  
    2.99 -  "@INTER1"     :: [pttrns, 'b set] => 'b set         ("(3INT _./ _)" 10)
   2.100 -  "@UNION1"     :: [pttrns, 'b set] => 'b set         ("(3UN _./ _)" 10)
   2.101 -  "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3INT _:_./ _)" 10)
   2.102 -  "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3UN _:_./ _)" 10)
   2.103 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" 10)
   2.104 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" 10)
   2.105 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" 10)
   2.106 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" 10)
   2.107  
   2.108 -  (* Bounded Quantifiers *)
   2.109 -  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
   2.110 -  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
   2.111 +  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
   2.112 +  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
   2.113  
   2.114  syntax (HOL)
   2.115 -  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" [0, 0, 10] 10)
   2.116 -  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
   2.117 +  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3! _:_./ _)" [0, 0, 10] 10)
   2.118 +  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
   2.119  
   2.120  translations
   2.121    "range f"     == "f`UNIV"
   2.122 @@ -85,120 +86,811 @@
   2.123    "EX x:A. P"   == "Bex A (%x. P)"
   2.124  
   2.125  syntax ("" output)
   2.126 -  "_setle"      :: ['a set, 'a set] => bool           ("op <=")
   2.127 -  "_setle"      :: ['a set, 'a set] => bool           ("(_/ <= _)" [50, 51] 50)
   2.128 -  "_setless"    :: ['a set, 'a set] => bool           ("op <")
   2.129 -  "_setless"    :: ['a set, 'a set] => bool           ("(_/ < _)" [50, 51] 50)
   2.130 +  "_setle"      :: "'a set => 'a set => bool"             ("op <=")
   2.131 +  "_setle"      :: "'a set => 'a set => bool"             ("(_/ <= _)" [50, 51] 50)
   2.132 +  "_setless"    :: "'a set => 'a set => bool"             ("op <")
   2.133 +  "_setless"    :: "'a set => 'a set => bool"             ("(_/ < _)" [50, 51] 50)
   2.134  
   2.135  syntax (symbols)
   2.136 -  "_setle"      :: ['a set, 'a set] => bool           ("op \\<subseteq>")
   2.137 -  "_setle"      :: ['a set, 'a set] => bool           ("(_/ \\<subseteq> _)" [50, 51] 50)
   2.138 -  "_setless"    :: ['a set, 'a set] => bool           ("op \\<subset>")
   2.139 -  "_setless"    :: ['a set, 'a set] => bool           ("(_/ \\<subset> _)" [50, 51] 50)
   2.140 -  "op Int"      :: ['a set, 'a set] => 'a set         (infixl "\\<inter>" 70)
   2.141 -  "op Un"       :: ['a set, 'a set] => 'a set         (infixl "\\<union>" 65)
   2.142 -  "op :"        :: ['a, 'a set] => bool               ("op \\<in>")
   2.143 -  "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
   2.144 -  "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
   2.145 -  "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
   2.146 -  "@UNION1"     :: [pttrns, 'b set] => 'b set         ("(3\\<Union>_./ _)" 10)
   2.147 -  "@INTER1"     :: [pttrns, 'b set] => 'b set         ("(3\\<Inter>_./ _)" 10)
   2.148 -  "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union>_\\<in>_./ _)" 10)
   2.149 -  "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter>_\\<in>_./ _)" 10)
   2.150 -  Union         :: (('a set) set) => 'a set           ("\\<Union>_" [90] 90)
   2.151 -  Inter         :: (('a set) set) => 'a set           ("\\<Inter>_" [90] 90)
   2.152 -  "_Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall>_\\<in>_./ _)" [0, 0, 10] 10)
   2.153 -  "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists>_\\<in>_./ _)" [0, 0, 10] 10)
   2.154 +  "_setle"      :: "'a set => 'a set => bool"             ("op \<subseteq>")
   2.155 +  "_setle"      :: "'a set => 'a set => bool"             ("(_/ \<subseteq> _)" [50, 51] 50)
   2.156 +  "_setless"    :: "'a set => 'a set => bool"             ("op \<subset>")
   2.157 +  "_setless"    :: "'a set => 'a set => bool"             ("(_/ \<subset> _)" [50, 51] 50)
   2.158 +  "op Int"      :: "'a set => 'a set => 'a set"           (infixl "\<inter>" 70)
   2.159 +  "op Un"       :: "'a set => 'a set => 'a set"           (infixl "\<union>" 65)
   2.160 +  "op :"        :: "'a => 'a set => bool"                 ("op \<in>")
   2.161 +  "op :"        :: "'a => 'a set => bool"                 ("(_/ \<in> _)" [50, 51] 50)
   2.162 +  "op ~:"       :: "'a => 'a set => bool"                 ("op \<notin>")
   2.163 +  "op ~:"       :: "'a => 'a set => bool"                 ("(_/ \<notin> _)" [50, 51] 50)
   2.164 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" 10)
   2.165 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" 10)
   2.166 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" 10)
   2.167 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" 10)
   2.168 +  Union         :: "'a set set => 'a set"                 ("\<Union>_" [90] 90)
   2.169 +  Inter         :: "'a set set => 'a set"                 ("\<Inter>_" [90] 90)
   2.170 +  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
   2.171 +  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
   2.172  
   2.173  translations
   2.174 -  "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool"
   2.175 -  "op \\<subset>" => "op <  :: [_ set, _ set] => bool"
   2.176 -
   2.177 +  "op \<subseteq>" => "op <= :: _ set => _ set => bool"
   2.178 +  "op \<subset>" => "op <  :: _ set => _ set => bool"
   2.179  
   2.180  
   2.181 -(** Rules and definitions **)
   2.182 +typed_print_translation {*
   2.183 +  let
   2.184 +    fun le_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
   2.185 +          list_comb (Syntax.const "_setle", ts)
   2.186 +      | le_tr' _ _ _ = raise Match;
   2.187 +
   2.188 +    fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
   2.189 +          list_comb (Syntax.const "_setless", ts)
   2.190 +      | less_tr' _ _ _ = raise Match;
   2.191 +  in [("op <=", le_tr'), ("op <", less_tr')] end
   2.192 +*}
   2.193  
   2.194 -local
   2.195 +text {*
   2.196 +  \medskip Translate between @{text "{e | x1...xn. P}"} and @{text
   2.197 +  "{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is
   2.198 +  only translated if @{text "[0..n] subset bvs(e)"}.
   2.199 +*}
   2.200 +
   2.201 +parse_translation {*
   2.202 +  let
   2.203 +    val ex_tr = snd (mk_binder_tr ("EX ", "Ex"));
   2.204  
   2.205 -rules
   2.206 +    fun nvars (Const ("_idts", _) $ _ $ idts) = nvars idts + 1
   2.207 +      | nvars _ = 1;
   2.208 +
   2.209 +    fun setcompr_tr [e, idts, b] =
   2.210 +      let
   2.211 +        val eq = Syntax.const "op =" $ Bound (nvars idts) $ e;
   2.212 +        val P = Syntax.const "op &" $ eq $ b;
   2.213 +        val exP = ex_tr [idts, P];
   2.214 +      in Syntax.const "Collect" $ Abs ("", dummyT, exP) end;
   2.215 +
   2.216 +  in [("@SetCompr", setcompr_tr)] end;
   2.217 +*}
   2.218  
   2.219 -  (* Isomorphisms between Predicates and Sets *)
   2.220 +print_translation {*
   2.221 +  let
   2.222 +    val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY"));
   2.223 +
   2.224 +    fun setcompr_tr' [Abs (_, _, P)] =
   2.225 +      let
   2.226 +        fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
   2.227 +          | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
   2.228 +              if n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
   2.229 +                ((0 upto (n - 1)) subset add_loose_bnos (e, 0, [])) then ()
   2.230 +              else raise Match;
   2.231  
   2.232 -  mem_Collect_eq    "(a : {x. P(x)}) = P(a)"
   2.233 -  Collect_mem_eq    "{x. x:A} = A"
   2.234 +        fun tr' (_ $ abs) =
   2.235 +          let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]
   2.236 +          in Syntax.const "@SetCompr" $ e $ idts $ Q end;
   2.237 +      in check (P, 0); tr' P end;
   2.238 +  in [("Collect", setcompr_tr')] end;
   2.239 +*}
   2.240 +
   2.241 +
   2.242 +subsection {* Rules and definitions *}
   2.243 +
   2.244 +text {* Isomorphisms between predicates and sets. *}
   2.245  
   2.246 +axioms
   2.247 +  mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
   2.248 +  Collect_mem_eq [simp]: "{x. x:A} = A"
   2.249 +
   2.250 +defs
   2.251 +  Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
   2.252 +  Bex_def:      "Bex A P        == EX x. x:A & P(x)"
   2.253 +
   2.254 +defs (overloaded)
   2.255 +  subset_def:   "A <= B         == ALL x:A. x:B"
   2.256 +  psubset_def:  "A < B          == (A::'a set) <= B & ~ A=B"
   2.257 +  Compl_def:    "- A            == {x. ~x:A}"
   2.258  
   2.259  defs
   2.260 -  Ball_def      "Ball A P       == ! x. x:A --> P(x)"
   2.261 -  Bex_def       "Bex A P        == ? x. x:A & P(x)"
   2.262 -  subset_def    "A <= B         == ! x:A. x:B"
   2.263 -  psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
   2.264 -  Compl_def     "- A            == {x. ~x:A}"
   2.265 -  Un_def        "A Un B         == {x. x:A | x:B}"
   2.266 -  Int_def       "A Int B        == {x. x:A & x:B}"
   2.267 -  set_diff_def  "A - B          == {x. x:A & ~x:B}"
   2.268 -  INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
   2.269 -  UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
   2.270 -  Inter_def     "Inter S        == (INT x:S. x)"
   2.271 -  Union_def     "Union S        == (UN x:S. x)"
   2.272 -  Pow_def       "Pow A          == {B. B <= A}"
   2.273 -  empty_def     "{}             == {x. False}"
   2.274 -  UNIV_def      "UNIV           == {x. True}"
   2.275 -  insert_def    "insert a B     == {x. x=a} Un B"
   2.276 -  image_def     "f`A           == {y. ? x:A. y=f(x)}"
   2.277 +  Un_def:       "A Un B         == {x. x:A | x:B}"
   2.278 +  Int_def:      "A Int B        == {x. x:A & x:B}"
   2.279 +  set_diff_def: "A - B          == {x. x:A & ~x:B}"
   2.280 +  INTER_def:    "INTER A B      == {y. ALL x:A. y: B(x)}"
   2.281 +  UNION_def:    "UNION A B      == {y. EX x:A. y: B(x)}"
   2.282 +  Inter_def:    "Inter S        == (INT x:S. x)"
   2.283 +  Union_def:    "Union S        == (UN x:S. x)"
   2.284 +  Pow_def:      "Pow A          == {B. B <= A}"
   2.285 +  empty_def:    "{}             == {x. False}"
   2.286 +  UNIV_def:     "UNIV           == {x. True}"
   2.287 +  insert_def:   "insert a B     == {x. x=a} Un B"
   2.288 +  image_def:    "f`A            == {y. EX x:A. y = f(x)}"
   2.289 +
   2.290 +
   2.291 +subsection {* Lemmas and proof tool setup *}
   2.292 +
   2.293 +subsubsection {* Relating predicates and sets *}
   2.294 +
   2.295 +lemma CollectI [intro!]: "P(a) ==> a : {x. P(x)}"
   2.296 +  by simp
   2.297 +
   2.298 +lemma CollectD: "a : {x. P(x)} ==> P(a)"
   2.299 +  by simp
   2.300 +
   2.301 +lemma set_ext: "(!!x. (x:A) = (x:B)) ==> A = B"
   2.302 +proof -
   2.303 +  case rule_context
   2.304 +  show ?thesis
   2.305 +    apply (rule prems [THEN ext, THEN arg_cong, THEN box_equals])
   2.306 +     apply (rule Collect_mem_eq)
   2.307 +    apply (rule Collect_mem_eq)
   2.308 +    done
   2.309 +qed
   2.310 +
   2.311 +lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
   2.312 +  by simp
   2.313 +
   2.314 +lemmas CollectE [elim!] = CollectD [elim_format]
   2.315 +
   2.316 +
   2.317 +subsubsection {* Bounded quantifiers *}
   2.318 +
   2.319 +lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
   2.320 +  by (simp add: Ball_def)
   2.321 +
   2.322 +lemmas strip = impI allI ballI
   2.323 +
   2.324 +lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x"
   2.325 +  by (simp add: Ball_def)
   2.326 +
   2.327 +lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
   2.328 +  by (unfold Ball_def) blast
   2.329 +
   2.330 +text {*
   2.331 +  \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and
   2.332 +  @{prop "a:A"}; creates assumption @{prop "P a"}.
   2.333 +*}
   2.334 +
   2.335 +ML {*
   2.336 +  local val ballE = thm "ballE"
   2.337 +  in fun ball_tac i = etac ballE i THEN contr_tac (i + 1) end;
   2.338 +*}
   2.339 +
   2.340 +text {*
   2.341 +  Gives better instantiation for bound:
   2.342 +*}
   2.343 +
   2.344 +ML_setup {*
   2.345 +  claset_ref() := claset() addbefore ("bspec", datac (thm "bspec") 1);
   2.346 +*}
   2.347 +
   2.348 +lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
   2.349 +  -- {* Normally the best argument order: @{prop "P x"} constrains the
   2.350 +    choice of @{prop "x:A"}. *}
   2.351 +  by (unfold Bex_def) blast
   2.352 +
   2.353 +lemma rev_bexI: "x:A ==> P x ==> EX x:A. P x"
   2.354 +  -- {* The best argument order when there is only one @{prop "x:A"}. *}
   2.355 +  by (unfold Bex_def) blast
   2.356 +
   2.357 +lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x"
   2.358 +  by (unfold Bex_def) blast
   2.359 +
   2.360 +lemma bexE [elim!]: "EX x:A. P x ==> (!!x. x:A ==> P x ==> Q) ==> Q"
   2.361 +  by (unfold Bex_def) blast
   2.362 +
   2.363 +lemma ball_triv [simp]: "(ALL x:A. P) = ((EX x. x:A) --> P)"
   2.364 +  -- {* Trival rewrite rule. *}
   2.365 +  by (simp add: Ball_def)
   2.366 +
   2.367 +lemma bex_triv [simp]: "(EX x:A. P) = ((EX x. x:A) & P)"
   2.368 +  -- {* Dual form for existentials. *}
   2.369 +  by (simp add: Bex_def)
   2.370 +
   2.371 +lemma bex_triv_one_point1 [simp]: "(EX x:A. x = a) = (a:A)"
   2.372 +  by blast
   2.373 +
   2.374 +lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)"
   2.375 +  by blast
   2.376 +
   2.377 +lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)"
   2.378 +  by blast
   2.379 +
   2.380 +lemma bex_one_point2 [simp]: "(EX x:A. a = x & P x) = (a:A & P a)"
   2.381 +  by blast
   2.382 +
   2.383 +lemma ball_one_point1 [simp]: "(ALL x:A. x = a --> P x) = (a:A --> P a)"
   2.384 +  by blast
   2.385 +
   2.386 +lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
   2.387 +  by blast
   2.388 +
   2.389 +ML_setup {*
   2.390 +  let
   2.391 +    val Ball_def = thm "Ball_def";
   2.392 +    val Bex_def = thm "Bex_def";
   2.393 +
   2.394 +    val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
   2.395 +      ("EX x:A. P x & Q x", HOLogic.boolT);
   2.396 +
   2.397 +    val prove_bex_tac =
   2.398 +      rewrite_goals_tac [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;
   2.399 +    val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
   2.400 +
   2.401 +    val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
   2.402 +      ("ALL x:A. P x --> Q x", HOLogic.boolT);
   2.403 +
   2.404 +    val prove_ball_tac =
   2.405 +      rewrite_goals_tac [Ball_def] THEN Quantifier1.prove_one_point_all_tac;
   2.406 +    val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
   2.407 +
   2.408 +    val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex;
   2.409 +    val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball;
   2.410 +  in
   2.411 +    Addsimprocs [defBALL_regroup, defBEX_regroup]
   2.412 +  end;
   2.413 +*}
   2.414 +
   2.415 +
   2.416 +subsubsection {* Congruence rules *}
   2.417 +
   2.418 +lemma ball_cong [cong]:
   2.419 +  "A = B ==> (!!x. x:B ==> P x = Q x) ==>
   2.420 +    (ALL x:A. P x) = (ALL x:B. Q x)"
   2.421 +  by (simp add: Ball_def)
   2.422 +
   2.423 +lemma bex_cong [cong]:
   2.424 +  "A = B ==> (!!x. x:B ==> P x = Q x) ==>
   2.425 +    (EX x:A. P x) = (EX x:B. Q x)"
   2.426 +  by (simp add: Bex_def cong: conj_cong)
   2.427  
   2.428  
   2.429 -end
   2.430 +subsubsection {* Subsets *}
   2.431 +
   2.432 +lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A <= B"
   2.433 +  by (simp add: subset_def)
   2.434 +
   2.435 +text {*
   2.436 +  \medskip Map the type @{text "'a set => anything"} to just @{typ
   2.437 +  'a}; for overloading constants whose first argument has type @{typ
   2.438 +  "'a set"}.
   2.439 +*}
   2.440 +
   2.441 +ML {*
   2.442 +  fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type);
   2.443 +*}
   2.444 +
   2.445 +ML "
   2.446 +  (* While (:) is not, its type must be kept
   2.447 +    for overloading of = to work. *)
   2.448 +  Blast.overloaded (\"op :\", domain_type);
   2.449 +
   2.450 +  overload_1st_set \"Ball\";            (*need UNION, INTER also?*)
   2.451 +  overload_1st_set \"Bex\";
   2.452 +
   2.453 +  (*Image: retain the type of the set being expressed*)
   2.454 +  Blast.overloaded (\"image\", domain_type);
   2.455 +"
   2.456 +
   2.457 +lemma subsetD [elim]: "A <= B ==> c:A ==> c:B"
   2.458 +  -- {* Rule in Modus Ponens style. *}
   2.459 +  by (unfold subset_def) blast
   2.460 +
   2.461 +declare subsetD [intro?] -- FIXME
   2.462 +
   2.463 +lemma rev_subsetD: "c:A ==> A <= B ==> c:B"
   2.464 +  -- {* The same, with reversed premises for use with @{text erule} --
   2.465 +      cf @{text rev_mp}. *}
   2.466 +  by (rule subsetD)
   2.467 +
   2.468 +declare rev_subsetD [intro?] -- FIXME
   2.469 +
   2.470 +text {*
   2.471 +  \medskip Converts @{prop "A <= B"} to @{prop "x:A ==> x:B"}.
   2.472 +*}
   2.473 +
   2.474 +ML {*
   2.475 +  local val rev_subsetD = thm "rev_subsetD"
   2.476 +  in fun impOfSubs th = th RSN (2, rev_subsetD) end;
   2.477 +*}
   2.478 +
   2.479 +lemma subsetCE [elim]: "A <= B ==> (c~:A ==> P) ==> (c:B ==> P) ==> P"
   2.480 +  -- {* Classical elimination rule. *}
   2.481 +  by (unfold subset_def) blast
   2.482 +
   2.483 +text {*
   2.484 +  \medskip Takes assumptions @{prop "A <= B"}; @{prop "c:A"} and
   2.485 +  creates the assumption @{prop "c:B"}.
   2.486 +*}
   2.487 +
   2.488 +ML {*
   2.489 +  local val subsetCE = thm "subsetCE"
   2.490 +  in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end;
   2.491 +*}
   2.492 +
   2.493 +lemma contra_subsetD: "A <= B ==> c ~: B ==> c ~: A"
   2.494 +  by blast
   2.495 +
   2.496 +lemma subset_refl: "A <= (A::'a set)"
   2.497 +  by fast
   2.498 +
   2.499 +lemma subset_trans: "A <= B ==> B <= C ==> A <= (C::'a set)"
   2.500 +  by blast
   2.501  
   2.502  
   2.503 -ML
   2.504 +subsubsection {* Equality *}
   2.505 +
   2.506 +lemma subset_antisym [intro!]: "A <= B ==> B <= A ==> A = (B::'a set)"
   2.507 +  -- {* Anti-symmetry of the subset relation. *}
   2.508 +  by (rule set_ext) (blast intro: subsetD)
   2.509 +
   2.510 +lemmas equalityI = subset_antisym
   2.511 +
   2.512 +text {*
   2.513 +  \medskip Equality rules from ZF set theory -- are they appropriate
   2.514 +  here?
   2.515 +*}
   2.516 +
   2.517 +lemma equalityD1: "A = B ==> A <= (B::'a set)"
   2.518 +  by (simp add: subset_refl)
   2.519 +
   2.520 +lemma equalityD2: "A = B ==> B <= (A::'a set)"
   2.521 +  by (simp add: subset_refl)
   2.522 +
   2.523 +text {*
   2.524 +  \medskip Be careful when adding this to the claset as @{text
   2.525 +  subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{}
   2.526 +  <= A"} and @{prop "A <= {}"} and then back to @{prop "A = {}"}!
   2.527 +*}
   2.528 +
   2.529 +lemma equalityE: "A = B ==> (A <= B ==> B <= (A::'a set) ==> P) ==> P"
   2.530 +  by (simp add: subset_refl)
   2.531  
   2.532 -local
   2.533 +lemma equalityCE [elim]:
   2.534 +    "A = B ==> (c:A ==> c:B ==> P) ==> (c~:A ==> c~:B ==> P) ==> P"
   2.535 +  by blast
   2.536 +
   2.537 +text {*
   2.538 +  \medskip Lemma for creating induction formulae -- for "pattern
   2.539 +  matching" on @{text p}.  To make the induction hypotheses usable,
   2.540 +  apply @{text spec} or @{text bspec} to put universal quantifiers over the free
   2.541 +  variables in @{text p}.
   2.542 +*}
   2.543 +
   2.544 +lemma setup_induction: "p:A ==> (!!z. z:A ==> p = z --> R) ==> R"
   2.545 +  by simp
   2.546  
   2.547 -(* Set inclusion *)
   2.548 +lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)"
   2.549 +  by simp
   2.550 +
   2.551 +
   2.552 +subsubsection {* The universal set -- UNIV *}
   2.553 +
   2.554 +lemma UNIV_I [simp]: "x : UNIV"
   2.555 +  by (simp add: UNIV_def)
   2.556 +
   2.557 +declare UNIV_I [intro]  -- {* unsafe makes it less likely to cause problems *}
   2.558 +
   2.559 +lemma UNIV_witness [intro?]: "EX x. x : UNIV"
   2.560 +  by simp
   2.561 +
   2.562 +lemma subset_UNIV: "A <= UNIV"
   2.563 +  by (rule subsetI) (rule UNIV_I)
   2.564  
   2.565 -fun le_tr' _ (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts =
   2.566 -      list_comb (Syntax.const "_setle", ts)
   2.567 -  | le_tr' _ (*op <=*) _ _ = raise Match;
   2.568 +text {*
   2.569 +  \medskip Eta-contracting these two rules (to remove @{text P})
   2.570 +  causes them to be ignored because of their interaction with
   2.571 +  congruence rules.
   2.572 +*}
   2.573 +
   2.574 +lemma ball_UNIV [simp]: "Ball UNIV P = All P"
   2.575 +  by (simp add: Ball_def)
   2.576 +
   2.577 +lemma bex_UNIV [simp]: "Bex UNIV P = Ex P"
   2.578 +  by (simp add: Bex_def)
   2.579 +
   2.580 +
   2.581 +subsubsection {* The empty set *}
   2.582 +
   2.583 +lemma empty_iff [simp]: "(c : {}) = False"
   2.584 +  by (simp add: empty_def)
   2.585 +
   2.586 +lemma emptyE [elim!]: "a : {} ==> P"
   2.587 +  by simp
   2.588 +
   2.589 +lemma empty_subsetI [iff]: "{} <= A"
   2.590 +    -- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
   2.591 +  by blast
   2.592 +
   2.593 +lemma equals0I: "(!!y. y:A ==> False) ==> A = {}"
   2.594 +  by blast
   2.595  
   2.596 -fun less_tr' _ (*op <*) (Type ("fun", (Type ("set", _) :: _))) ts =
   2.597 -      list_comb (Syntax.const "_setless", ts)
   2.598 -  | less_tr' _ (*op <*) _ _ = raise Match;
   2.599 +lemma equals0D: "A={} ==> a ~: A"
   2.600 +    -- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *}
   2.601 +  by blast
   2.602 +
   2.603 +lemma ball_empty [simp]: "Ball {} P = True"
   2.604 +  by (simp add: Ball_def)
   2.605 +
   2.606 +lemma bex_empty [simp]: "Bex {} P = False"
   2.607 +  by (simp add: Bex_def)
   2.608 +
   2.609 +lemma UNIV_not_empty [iff]: "UNIV ~= {}"
   2.610 +  by (blast elim: equalityE)
   2.611 +
   2.612 +
   2.613 +section {* The Powerset operator -- Pow *}
   2.614 +
   2.615 +lemma Pow_iff [iff]: "(A : Pow B) = (A <= B)"
   2.616 +  by (simp add: Pow_def)
   2.617 +
   2.618 +lemma PowI: "A <= B ==> A : Pow B"
   2.619 +  by (simp add: Pow_def)
   2.620 +
   2.621 +lemma PowD: "A : Pow B ==> A <= B"
   2.622 +  by (simp add: Pow_def)
   2.623 +
   2.624 +lemma Pow_bottom: "{}: Pow B"
   2.625 +  by simp
   2.626 +
   2.627 +lemma Pow_top: "A : Pow A"
   2.628 +  by (simp add: subset_refl)
   2.629  
   2.630  
   2.631 -(* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)
   2.632 -(* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
   2.633 +subsubsection {* Set complement *}
   2.634 +
   2.635 +lemma Compl_iff [simp]: "(c : -A) = (c~:A)"
   2.636 +  by (unfold Compl_def) blast
   2.637 +
   2.638 +lemma ComplI [intro!]: "(c:A ==> False) ==> c : -A"
   2.639 +  by (unfold Compl_def) blast
   2.640 +
   2.641 +text {*
   2.642 +  \medskip This form, with negated conclusion, works well with the
   2.643 +  Classical prover.  Negated assumptions behave like formulae on the
   2.644 +  right side of the notional turnstile ... *}
   2.645 +
   2.646 +lemma ComplD: "c : -A ==> c~:A"
   2.647 +  by (unfold Compl_def) blast
   2.648 +
   2.649 +lemmas ComplE [elim!] = ComplD [elim_format]
   2.650 +
   2.651 +
   2.652 +subsubsection {* Binary union -- Un *}
   2.653  
   2.654 -val ex_tr = snd(mk_binder_tr("EX ","Ex"));
   2.655 +lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
   2.656 +  by (unfold Un_def) blast
   2.657 +
   2.658 +lemma UnI1 [elim?]: "c:A ==> c : A Un B"
   2.659 +  by simp
   2.660 +
   2.661 +lemma UnI2 [elim?]: "c:B ==> c : A Un B"
   2.662 +  by simp
   2.663  
   2.664 -fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
   2.665 -  | nvars(_) = 1;
   2.666 +text {*
   2.667 +  \medskip Classical introduction rule: no commitment to @{prop A} vs
   2.668 +  @{prop B}.
   2.669 +*}
   2.670 +
   2.671 +lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B"
   2.672 +  by auto
   2.673 +
   2.674 +lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"
   2.675 +  by (unfold Un_def) blast
   2.676 +
   2.677 +
   2.678 +section {* Binary intersection -- Int *}
   2.679  
   2.680 -fun setcompr_tr[e,idts,b] =
   2.681 -  let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e
   2.682 -      val P = Syntax.const("op &") $ eq $ b
   2.683 -      val exP = ex_tr [idts,P]
   2.684 -  in Syntax.const("Collect") $ Abs("",dummyT,exP) end;
   2.685 +lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   2.686 +  by (unfold Int_def) blast
   2.687 +
   2.688 +lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B"
   2.689 +  by simp
   2.690 +
   2.691 +lemma IntD1: "c : A Int B ==> c:A"
   2.692 +  by simp
   2.693 +
   2.694 +lemma IntD2: "c : A Int B ==> c:B"
   2.695 +  by simp
   2.696 +
   2.697 +lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P"
   2.698 +  by simp
   2.699 +
   2.700 +
   2.701 +section {* Set difference *}
   2.702 +
   2.703 +lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
   2.704 +  by (unfold set_diff_def) blast
   2.705  
   2.706 -val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
   2.707 +lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A - B"
   2.708 +  by simp
   2.709 +
   2.710 +lemma DiffD1: "c : A - B ==> c : A"
   2.711 +  by simp
   2.712 +
   2.713 +lemma DiffD2: "c : A - B ==> c : B ==> P"
   2.714 +  by simp
   2.715 +
   2.716 +lemma DiffE [elim!]: "c : A - B ==> (c:A ==> c~:B ==> P) ==> P"
   2.717 +  by simp
   2.718 +
   2.719 +
   2.720 +subsubsection {* Augmenting a set -- insert *}
   2.721 +
   2.722 +lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"
   2.723 +  by (unfold insert_def) blast
   2.724 +
   2.725 +lemma insertI1: "a : insert a B"
   2.726 +  by simp
   2.727 +
   2.728 +lemma insertI2: "a : B ==> a : insert b B"
   2.729 +  by simp
   2.730  
   2.731 -fun setcompr_tr'[Abs(_,_,P)] =
   2.732 -  let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1)
   2.733 -        | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ P, n) =
   2.734 -            if n>0 andalso m=n andalso not(loose_bvar1(P,n)) andalso
   2.735 -               ((0 upto (n-1)) subset add_loose_bnos(e,0,[]))
   2.736 -            then () else raise Match
   2.737 +lemma insertE [elim!]: "a : insert b A ==> (a = b ==> P) ==> (a:A ==> P) ==> P"
   2.738 +  by (unfold insert_def) blast
   2.739 +
   2.740 +lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B"
   2.741 +  -- {* Classical introduction rule. *}
   2.742 +  by auto
   2.743 +
   2.744 +lemma subset_insert_iff: "(A <= insert x B) = (if x:A then A - {x} <= B else A <= B)"
   2.745 +  by auto
   2.746 +
   2.747 +
   2.748 +subsubsection {* Singletons, using insert *}
   2.749 +
   2.750 +lemma singletonI [intro!]: "a : {a}"
   2.751 +    -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
   2.752 +  by (rule insertI1)
   2.753 +
   2.754 +lemma singletonD: "b : {a} ==> b = a"
   2.755 +  by blast
   2.756 +
   2.757 +lemmas singletonE [elim!] = singletonD [elim_format]
   2.758 +
   2.759 +lemma singleton_iff: "(b : {a}) = (b = a)"
   2.760 +  by blast
   2.761 +
   2.762 +lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
   2.763 +  by blast
   2.764 +
   2.765 +lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A <= {b})"
   2.766 +  by blast
   2.767 +
   2.768 +lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A <= {b})"
   2.769 +  by blast
   2.770 +
   2.771 +lemma subset_singletonD: "A <= {x} ==> A={} | A = {x}"
   2.772 +  by fast
   2.773 +
   2.774 +lemma singleton_conv [simp]: "{x. x = a} = {a}"
   2.775 +  by blast
   2.776 +
   2.777 +lemma singleton_conv2 [simp]: "{x. a = x} = {a}"
   2.778 +  by blast
   2.779  
   2.780 -      fun tr'(_ $ abs) =
   2.781 -        let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]
   2.782 -        in Syntax.const("@SetCompr") $ e $ idts $ Q end
   2.783 -  in ok(P,0); tr'(P) end;
   2.784 +lemma diff_single_insert: "A - {x} <= B ==> x : A ==> A <= insert x B"
   2.785 +  by blast
   2.786 +
   2.787 +
   2.788 +subsubsection {* Unions of families *}
   2.789 +
   2.790 +text {*
   2.791 +  @{term [source] "UN x:A. B x"} is @{term "Union (B`A)"}.
   2.792 +*}
   2.793 +
   2.794 +lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
   2.795 +  by (unfold UNION_def) blast
   2.796 +
   2.797 +lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)"
   2.798 +  -- {* The order of the premises presupposes that @{term A} is rigid;
   2.799 +    @{term b} may be flexible. *}
   2.800 +  by auto
   2.801 +
   2.802 +lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R"
   2.803 +  by (unfold UNION_def) blast
   2.804  
   2.805 -in
   2.806 +lemma UN_cong [cong]:
   2.807 +    "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"
   2.808 +  by (simp add: UNION_def)
   2.809 +
   2.810 +
   2.811 +subsubsection {* Intersections of families *}
   2.812 +
   2.813 +text {* @{term [source] "INT x:A. B x"} is @{term "Inter (B`A)"}. *}
   2.814 +
   2.815 +lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
   2.816 +  by (unfold INTER_def) blast
   2.817  
   2.818 -val parse_translation = [("@SetCompr", setcompr_tr)];
   2.819 -val print_translation = [("Collect", setcompr_tr')];
   2.820 -val typed_print_translation = [("op <=", le_tr'), ("op <", less_tr')];
   2.821 +lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)"
   2.822 +  by (unfold INTER_def) blast
   2.823 +
   2.824 +lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a"
   2.825 +  by auto
   2.826 +
   2.827 +lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R"
   2.828 +  -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a:A"}. *}
   2.829 +  by (unfold INTER_def) blast
   2.830 +
   2.831 +lemma INT_cong [cong]:
   2.832 +    "A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)"
   2.833 +  by (simp add: INTER_def)
   2.834  
   2.835  
   2.836 -end;
   2.837 +subsubsection {* Union *}
   2.838 +
   2.839 +lemma Union_iff [simp]: "(A : Union C) = (EX X:C. A:X)"
   2.840 +  by (unfold Union_def) blast
   2.841 +
   2.842 +lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C"
   2.843 +  -- {* The order of the premises presupposes that @{term C} is rigid;
   2.844 +    @{term A} may be flexible. *}
   2.845 +  by auto
   2.846 +
   2.847 +lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R"
   2.848 +  by (unfold Union_def) blast
   2.849 +
   2.850 +
   2.851 +subsubsection {* Inter *}
   2.852 +
   2.853 +lemma Inter_iff [simp]: "(A : Inter C) = (ALL X:C. A:X)"
   2.854 +  by (unfold Inter_def) blast
   2.855 +
   2.856 +lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
   2.857 +  by (simp add: Inter_def)
   2.858 +
   2.859 +text {*
   2.860 +  \medskip A ``destruct'' rule -- every @{term X} in @{term C}
   2.861 +  contains @{term A} as an element, but @{prop "A:X"} can hold when
   2.862 +  @{prop "X:C"} does not!  This rule is analogous to @{text spec}.
   2.863 +*}
   2.864 +
   2.865 +lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
   2.866 +  by auto
   2.867 +
   2.868 +lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
   2.869 +  -- {* ``Classical'' elimination rule -- does not require proving
   2.870 +    @{prop "X:C"}. *}
   2.871 +  by (unfold Inter_def) blast
   2.872 +
   2.873 +text {*
   2.874 +  \medskip Image of a set under a function.  Frequently @{term b} does
   2.875 +  not have the syntactic form of @{term "f x"}.
   2.876 +*}
   2.877 +
   2.878 +lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A"
   2.879 +  by (unfold image_def) blast
   2.880 +
   2.881 +lemma imageI: "x : A ==> f x : f ` A"
   2.882 +  by (rule image_eqI) (rule refl)
   2.883 +
   2.884 +lemma rev_image_eqI: "x:A ==> b = f x ==> b : f`A"
   2.885 +  -- {* This version's more effective when we already have the
   2.886 +    required @{term x}. *}
   2.887 +  by (unfold image_def) blast
   2.888 +
   2.889 +lemma imageE [elim!]:
   2.890 +  "b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P"
   2.891 +  -- {* The eta-expansion gives variable-name preservation. *}
   2.892 +  by (unfold image_def) blast
   2.893 +
   2.894 +lemma image_Un: "f`(A Un B) = f`A Un f`B"
   2.895 +  by blast
   2.896 +
   2.897 +lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
   2.898 +  by blast
   2.899 +
   2.900 +lemma image_subset_iff: "(f`A <= B) = (ALL x:A. f x: B)"
   2.901 +  -- {* This rewrite rule would confuse users if made default. *}
   2.902 +  by blast
   2.903 +
   2.904 +lemma subset_image_iff: "(B <= f ` A) = (EX AA. AA <= A & B = f ` AA)"
   2.905 +  apply safe
   2.906 +   prefer 2 apply fast
   2.907 +  apply (rule_tac x = "{a. a : A & f a : B}" in exI)
   2.908 +  apply fast
   2.909 +  done
   2.910 +
   2.911 +lemma image_subsetI: "(!!x. x:A ==> f x : B) ==> f`A <= B"
   2.912 +  -- {* Replaces the three steps @{text subsetI}, @{text imageE},
   2.913 +    @{text hypsubst}, but breaks too many existing proofs. *}
   2.914 +  by blast
   2.915 +
   2.916 +text {*
   2.917 +  \medskip Range of a function -- just a translation for image!
   2.918 +*}
   2.919 +
   2.920 +lemma range_eqI: "b = f x ==> b : range f"
   2.921 +  by simp
   2.922 +
   2.923 +lemma rangeI: "f x : range f"
   2.924 +  by simp
   2.925 +
   2.926 +lemma rangeE [elim?]: "b : range (%x. f x) ==> (!!x. b = f x ==> P) ==> P"
   2.927 +  by blast
   2.928 +
   2.929 +
   2.930 +subsubsection {* Set reasoning tools *}
   2.931 +
   2.932 +text {*
   2.933 +  Rewrite rules for boolean case-splitting: faster than @{text
   2.934 +  "split_if [split]"}.
   2.935 +*}
   2.936 +
   2.937 +lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"
   2.938 +  by (rule split_if)
   2.939 +
   2.940 +lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))"
   2.941 +  by (rule split_if)
   2.942 +
   2.943 +text {*
   2.944 +  Split ifs on either side of the membership relation.  Not for @{text
   2.945 +  "[simp]"} -- can cause goals to blow up!
   2.946 +*}
   2.947 +
   2.948 +lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"
   2.949 +  by (rule split_if)
   2.950 +
   2.951 +lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))"
   2.952 +  by (rule split_if)
   2.953 +
   2.954 +lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
   2.955 +
   2.956 +lemmas mem_simps =
   2.957 +  insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
   2.958 +  mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
   2.959 +  -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
   2.960 +
   2.961 +(*Would like to add these, but the existing code only searches for the
   2.962 +  outer-level constant, which in this case is just "op :"; we instead need
   2.963 +  to use term-nets to associate patterns with rules.  Also, if a rule fails to
   2.964 +  apply, then the formula should be kept.
   2.965 +  [("uminus", Compl_iff RS iffD1), ("op -", [Diff_iff RS iffD1]),
   2.966 +   ("op Int", [IntD1,IntD2]),
   2.967 +   ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
   2.968 + *)
   2.969 +
   2.970 +ML_setup {*
   2.971 +  val mksimps_pairs = [("Ball", [thm "bspec"])] @ mksimps_pairs;
   2.972 +  simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs);
   2.973 +*}
   2.974 +
   2.975 +declare subset_UNIV [simp] subset_refl [simp]
   2.976 +
   2.977 +
   2.978 +subsubsection {* The ``proper subset'' relation *}
   2.979 +
   2.980 +lemma psubsetI [intro!]: "(A::'a set) <= B ==> A ~= B ==> A < B"
   2.981 +  by (unfold psubset_def) blast
   2.982 +
   2.983 +lemma psubset_insert_iff:
   2.984 +  "(A < insert x B) = (if x:B then A < B else if x:A then A - {x} < B else A <= B)"
   2.985 +  apply (simp add: psubset_def subset_insert_iff)
   2.986 +  apply blast
   2.987 +  done
   2.988 +
   2.989 +lemma psubset_eq: "((A::'a set) < B) = (A <= B & A ~= B)"
   2.990 +  by (simp only: psubset_def)
   2.991 +
   2.992 +lemma psubset_imp_subset: "(A::'a set) < B ==> A <= B"
   2.993 +  by (simp add: psubset_eq)
   2.994 +
   2.995 +lemma psubset_subset_trans: "(A::'a set) < B ==> B <= C ==> A < C"
   2.996 +  by (auto simp add: psubset_eq)
   2.997 +
   2.998 +lemma subset_psubset_trans: "(A::'a set) <= B ==> B < C ==> A < C"
   2.999 +  by (auto simp add: psubset_eq)
  2.1000 +
  2.1001 +lemma psubset_imp_ex_mem: "A < B ==> EX b. b : (B - A)"
  2.1002 +  by (unfold psubset_def) blast
  2.1003 +
  2.1004 +lemma atomize_ball:
  2.1005 +    "(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)"
  2.1006 +  by (simp only: Ball_def atomize_all atomize_imp)
  2.1007 +
  2.1008 +declare atomize_ball [symmetric, rulify]
  2.1009 +
  2.1010 +
  2.1011 +subsection {* Further set-theory lemmas *}
  2.1012 +
  2.1013 +use "subset.ML"
  2.1014 +use "equalities.ML"
  2.1015 +use "mono.ML"
  2.1016 +
  2.1017 +end
     3.1 --- a/src/HOL/Typedef.thy	Sun Oct 28 22:58:39 2001 +0100
     3.2 +++ b/src/HOL/Typedef.thy	Sun Oct 28 22:59:12 2001 +0100
     3.3 @@ -3,18 +3,15 @@
     3.4      Author:     Markus Wenzel, TU Munich
     3.5  *)
     3.6  
     3.7 -header {* Set-theory lemmas and HOL type definitions *}
     3.8 +header {* HOL type definitions *}
     3.9  
    3.10  theory Typedef = Set
    3.11 -files "subset.ML" "equalities.ML" "mono.ML" ("Tools/typedef_package.ML"):
    3.12 +files ("Tools/typedef_package.ML"):
    3.13  
    3.14 -(*belongs to theory Set*)
    3.15 -declare atomize_ball [symmetric, rulify]
    3.16 -
    3.17 -(* Courtesy of Stephan Merz *)
    3.18  lemma Least_mono: 
    3.19    "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
    3.20      ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
    3.21 +    -- {* Courtesy of Stephan Merz *}
    3.22    apply clarify
    3.23    apply (erule_tac P = "%x. x : S" in LeastI2)
    3.24     apply fast
     4.1 --- a/src/HOL/subset.ML	Sun Oct 28 22:58:39 2001 +0100
     4.2 +++ b/src/HOL/subset.ML	Sun Oct 28 22:59:12 2001 +0100
     4.3 @@ -7,6 +7,163 @@
     4.4  operations.
     4.5  *)
     4.6  
     4.7 +(* legacy ML bindings *)
     4.8 +
     4.9 +val Ball_def = thm "Ball_def";
    4.10 +val Bex_def = thm "Bex_def";
    4.11 +val Collect_mem_eq = thm "Collect_mem_eq";
    4.12 +val Compl_def = thm "Compl_def";
    4.13 +val INTER_def = thm "INTER_def";
    4.14 +val Int_def = thm "Int_def";
    4.15 +val Inter_def = thm "Inter_def";
    4.16 +val Pow_def = thm "Pow_def";
    4.17 +val UNION_def = thm "UNION_def";
    4.18 +val UNIV_def = thm "UNIV_def";
    4.19 +val Un_def = thm "Un_def";
    4.20 +val Union_def = thm "Union_def";
    4.21 +val empty_def = thm "empty_def";
    4.22 +val image_def = thm "image_def";
    4.23 +val insert_def = thm "insert_def";
    4.24 +val mem_Collect_eq = thm "mem_Collect_eq";
    4.25 +val psubset_def = thm "psubset_def";
    4.26 +val set_diff_def = thm "set_diff_def";
    4.27 +val subset_def = thm "subset_def";
    4.28 +val CollectI = thm "CollectI";
    4.29 +val CollectD = thm "CollectD";
    4.30 +val set_ext = thm "set_ext";
    4.31 +val Collect_cong = thm "Collect_cong";
    4.32 +val CollectE = thm "CollectE";
    4.33 +val ballI = thm "ballI";
    4.34 +val strip = thms "strip";
    4.35 +val bspec = thm "bspec";
    4.36 +val ballE = thm "ballE";
    4.37 +val bexI = thm "bexI";
    4.38 +val rev_bexI = thm "rev_bexI";
    4.39 +val bexCI = thm "bexCI";
    4.40 +val bexE = thm "bexE";
    4.41 +val ball_triv = thm "ball_triv";
    4.42 +val bex_triv = thm "bex_triv";
    4.43 +val bex_triv_one_point1 = thm "bex_triv_one_point1";
    4.44 +val bex_triv_one_point2 = thm "bex_triv_one_point2";
    4.45 +val bex_one_point1 = thm "bex_one_point1";
    4.46 +val bex_one_point2 = thm "bex_one_point2";
    4.47 +val ball_one_point1 = thm "ball_one_point1";
    4.48 +val ball_one_point2 = thm "ball_one_point2";
    4.49 +val ball_cong = thm "ball_cong";
    4.50 +val bex_cong = thm "bex_cong";
    4.51 +val subsetI = thm "subsetI";
    4.52 +val subsetD = thm "subsetD";
    4.53 +val rev_subsetD = thm "rev_subsetD";
    4.54 +val subsetCE = thm "subsetCE";
    4.55 +val contra_subsetD = thm "contra_subsetD";
    4.56 +val subset_refl = thm "subset_refl";
    4.57 +val subset_trans = thm "subset_trans";
    4.58 +val subset_antisym = thm "subset_antisym";
    4.59 +val equalityI = thm "equalityI";
    4.60 +val equalityD1 = thm "equalityD1";
    4.61 +val equalityD2 = thm "equalityD2";
    4.62 +val equalityE = thm "equalityE";
    4.63 +val equalityCE = thm "equalityCE";
    4.64 +val setup_induction = thm "setup_induction";
    4.65 +val eqset_imp_iff = thm "eqset_imp_iff";
    4.66 +val UNIV_I = thm "UNIV_I";
    4.67 +val UNIV_witness = thm "UNIV_witness";
    4.68 +val subset_UNIV = thm "subset_UNIV";
    4.69 +val ball_UNIV = thm "ball_UNIV";
    4.70 +val bex_UNIV = thm "bex_UNIV";
    4.71 +val empty_iff = thm "empty_iff";
    4.72 +val emptyE = thm "emptyE";
    4.73 +val empty_subsetI = thm "empty_subsetI";
    4.74 +val equals0I = thm "equals0I";
    4.75 +val equals0D = thm "equals0D";
    4.76 +val ball_empty = thm "ball_empty";
    4.77 +val bex_empty = thm "bex_empty";
    4.78 +val UNIV_not_empty = thm "UNIV_not_empty";
    4.79 +val Pow_iff = thm "Pow_iff";
    4.80 +val PowI = thm "PowI";
    4.81 +val PowD = thm "PowD";
    4.82 +val Pow_bottom = thm "Pow_bottom";
    4.83 +val Pow_top = thm "Pow_top";
    4.84 +val Compl_iff = thm "Compl_iff";
    4.85 +val ComplI = thm "ComplI";
    4.86 +val ComplD = thm "ComplD";
    4.87 +val ComplE = thm "ComplE";
    4.88 +val Un_iff = thm "Un_iff";
    4.89 +val UnI1 = thm "UnI1";
    4.90 +val UnI2 = thm "UnI2";
    4.91 +val UnCI = thm "UnCI";
    4.92 +val UnE = thm "UnE";
    4.93 +val Int_iff = thm "Int_iff";
    4.94 +val IntI = thm "IntI";
    4.95 +val IntD1 = thm "IntD1";
    4.96 +val IntD2 = thm "IntD2";
    4.97 +val IntE = thm "IntE";
    4.98 +val Diff_iff = thm "Diff_iff";
    4.99 +val DiffI = thm "DiffI";
   4.100 +val DiffD1 = thm "DiffD1";
   4.101 +val DiffD2 = thm "DiffD2";
   4.102 +val DiffE = thm "DiffE";
   4.103 +val insert_iff = thm "insert_iff";
   4.104 +val insertI1 = thm "insertI1";
   4.105 +val insertI2 = thm "insertI2";
   4.106 +val insertE = thm "insertE";
   4.107 +val insertCI = thm "insertCI";
   4.108 +val subset_insert_iff = thm "subset_insert_iff";
   4.109 +val singletonI = thm "singletonI";
   4.110 +val singletonD = thm "singletonD";
   4.111 +val singletonE = thm "singletonE";
   4.112 +val singleton_iff = thm "singleton_iff";
   4.113 +val singleton_inject = thm "singleton_inject";
   4.114 +val singleton_insert_inj_eq = thm "singleton_insert_inj_eq";
   4.115 +val singleton_insert_inj_eq' = thm "singleton_insert_inj_eq'";
   4.116 +val subset_singletonD = thm "subset_singletonD";
   4.117 +val singleton_conv = thm "singleton_conv";
   4.118 +val singleton_conv2 = thm "singleton_conv2";
   4.119 +val diff_single_insert = thm "diff_single_insert";
   4.120 +val UN_iff = thm "UN_iff";
   4.121 +val UN_I = thm "UN_I";
   4.122 +val UN_E = thm "UN_E";
   4.123 +val UN_cong = thm "UN_cong";
   4.124 +val INT_iff = thm "INT_iff";
   4.125 +val INT_I = thm "INT_I";
   4.126 +val INT_D = thm "INT_D";
   4.127 +val INT_E = thm "INT_E";
   4.128 +val INT_cong = thm "INT_cong";
   4.129 +val Union_iff = thm "Union_iff";
   4.130 +val UnionI = thm "UnionI";
   4.131 +val UnionE = thm "UnionE";
   4.132 +val Inter_iff = thm "Inter_iff";
   4.133 +val InterI = thm "InterI";
   4.134 +val InterD = thm "InterD";
   4.135 +val InterE = thm "InterE";
   4.136 +val image_eqI = thm "image_eqI";
   4.137 +val imageI = thm "imageI";
   4.138 +val rev_image_eqI = thm "rev_image_eqI";
   4.139 +val imageE = thm "imageE";
   4.140 +val image_Un = thm "image_Un";
   4.141 +val image_iff = thm "image_iff";
   4.142 +val image_subset_iff = thm "image_subset_iff";
   4.143 +val subset_image_iff = thm "subset_image_iff";
   4.144 +val image_subsetI = thm "image_subsetI";
   4.145 +val range_eqI = thm "range_eqI";
   4.146 +val rangeI = thm "rangeI";
   4.147 +val rangeE = thm "rangeE";
   4.148 +val split_if_eq1 = thm "split_if_eq1";
   4.149 +val split_if_eq2 = thm "split_if_eq2";
   4.150 +val split_if_mem1 = thm "split_if_mem1";
   4.151 +val split_if_mem2 = thm "split_if_mem2";
   4.152 +val split_ifs = thms "split_ifs";
   4.153 +val mem_simps = thms "mem_simps";
   4.154 +val psubsetI = thm "psubsetI";
   4.155 +val psubset_insert_iff = thm "psubset_insert_iff";
   4.156 +val psubset_eq = thm "psubset_eq";
   4.157 +val psubset_imp_subset = thm "psubset_imp_subset";
   4.158 +val psubset_subset_trans = thm "psubset_subset_trans";
   4.159 +val subset_psubset_trans = thm "subset_psubset_trans";
   4.160 +val psubset_imp_ex_mem = thm "psubset_imp_ex_mem";
   4.161 +val atomize_ball = thm "atomize_ball";
   4.162 +
   4.163 +
   4.164  (*** insert ***)
   4.165  
   4.166  Goal "B <= insert a B";