New Blast_tac (and minor tidying...)
authorpaulson
Sat Nov 01 12:59:06 1997 +0100 (1997-11-01)
changeset 405959c1422c9da5
parent 4058 18fea4aa9625
child 4060 600f266eac45
New Blast_tac (and minor tidying...)
src/HOL/Divides.ML
src/HOL/Finite.ML
src/HOL/Fun.ML
src/HOL/Fun.thy
src/HOL/RelPow.ML
src/HOL/Set.ML
src/HOL/Sexp.ML
src/HOL/WF.ML
src/HOL/cladata.ML
src/HOL/equalities.ML
     1.1 --- a/src/HOL/Divides.ML	Sat Nov 01 12:58:08 1997 +0100
     1.2 +++ b/src/HOL/Divides.ML	Sat Nov 01 12:59:06 1997 +0100
     1.3 @@ -294,7 +294,7 @@
     1.4  (************************************************)
     1.5  
     1.6  goalw thy [dvd_def] "m dvd 0";
     1.7 -by (fast_tac (!claset addIs [mult_0_right RS sym]) 1);
     1.8 +by (blast_tac (!claset addIs [mult_0_right RS sym]) 1);
     1.9  qed "dvd_0_right";
    1.10  Addsimps [dvd_0_right];
    1.11  
    1.12 @@ -308,12 +308,12 @@
    1.13  AddIffs [dvd_1_left];
    1.14  
    1.15  goalw thy [dvd_def] "m dvd m";
    1.16 -by (fast_tac (!claset addIs [mult_1_right RS sym]) 1);
    1.17 +by (blast_tac (!claset addIs [mult_1_right RS sym]) 1);
    1.18  qed "dvd_refl";
    1.19  Addsimps [dvd_refl];
    1.20  
    1.21  goalw thy [dvd_def] "!!m n p. [| m dvd n; n dvd p |] ==> m dvd p";
    1.22 -by (fast_tac (!claset addIs [mult_assoc] ) 1);
    1.23 +by (blast_tac (!claset addIs [mult_assoc] ) 1);
    1.24  qed "dvd_trans";
    1.25  
    1.26  goalw thy [dvd_def] "!!m n. [| m dvd n; n dvd m |] ==> m=n";
     2.1 --- a/src/HOL/Finite.ML	Sat Nov 01 12:58:08 1997 +0100
     2.2 +++ b/src/HOL/Finite.ML	Sat Nov 01 12:59:06 1997 +0100
     2.3 @@ -128,20 +128,21 @@
     2.4  qed "finite_Diff_singleton";
     2.5  AddIffs [finite_Diff_singleton];
     2.6  
     2.7 +(*Lemma for proving finite_imageD*)
     2.8  goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_onto f A --> finite A";
     2.9  by (etac finite_induct 1);
    2.10   by (ALLGOALS Asm_simp_tac);
    2.11  by (Clarify_tac 1);
    2.12  by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
    2.13   by (Clarify_tac 1);
    2.14 - by (rewtac inj_onto_def);
    2.15 + by (full_simp_tac (!simpset addsimps [inj_onto_def]) 1);
    2.16   by (Blast_tac 1);
    2.17  by (thin_tac "ALL A. ?PP(A)" 1);
    2.18  by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
    2.19  by (Clarify_tac 1);
    2.20  by (res_inst_tac [("x","xa")] bexI 1);
    2.21 -by (ALLGOALS Asm_simp_tac);
    2.22 -by (blast_tac (!claset addEs [equalityE]) 1);
    2.23 +by (ALLGOALS 
    2.24 +    (asm_full_simp_tac (!simpset addsimps [inj_onto_image_set_diff])));
    2.25  val lemma = result();
    2.26  
    2.27  goal Finite.thy "!!A. [| finite(f``A);  inj_onto f A |] ==> finite A";
     3.1 --- a/src/HOL/Fun.ML	Sat Nov 01 12:58:08 1997 +0100
     3.2 +++ b/src/HOL/Fun.ML	Sat Nov 01 12:59:06 1997 +0100
     3.3 @@ -128,5 +128,23 @@
     3.4                        addEs [inv_injective,injD]) 1);
     3.5  qed "inj_onto_inv";
     3.6  
     3.7 +goalw thy [inj_onto_def]
     3.8 +   "!!f. [| inj_onto f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
     3.9 +by (Blast_tac 1);
    3.10 +qed "inj_onto_image_Int";
    3.11 +
    3.12 +goalw thy [inj_onto_def]
    3.13 +   "!!f. [| inj_onto f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
    3.14 +by (Blast_tac 1);
    3.15 +qed "inj_onto_image_set_diff";
    3.16 +
    3.17 +goalw thy [inj_def] "!!f. inj f ==> f``(A Int B) = f``A Int f``B";
    3.18 +by (Blast_tac 1);
    3.19 +qed "image_Int";
    3.20 +
    3.21 +goalw thy [inj_def] "!!f. inj f ==> f``(A-B) = f``A - f``B";
    3.22 +by (Blast_tac 1);
    3.23 +qed "image_set_diff";
    3.24 +
    3.25  
    3.26  val set_cs = !claset delrules [equalityI];
     4.1 --- a/src/HOL/Fun.thy	Sat Nov 01 12:58:08 1997 +0100
     4.2 +++ b/src/HOL/Fun.thy	Sat Nov 01 12:59:06 1997 +0100
     4.3 @@ -8,6 +8,8 @@
     4.4  
     4.5  Fun = Set +
     4.6  
     4.7 +instance set :: (term) order
     4.8 +                       (subset_refl,subset_trans,subset_antisym,psubset_eq)
     4.9  consts
    4.10  
    4.11    inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
     5.1 --- a/src/HOL/RelPow.ML	Sat Nov 01 12:58:08 1997 +0100
     5.2 +++ b/src/HOL/RelPow.ML	Sat Nov 01 12:59:06 1997 +0100
     5.3 @@ -102,7 +102,7 @@
     5.4  qed "rel_pow_imp_rtrancl";
     5.5  
     5.6  goal RelPow.thy "R^* = (UN n. R^n)";
     5.7 -by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1);
     5.8 +by (blast_tac (!claset addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1);
     5.9  qed "rtrancl_is_UN_rel_pow";
    5.10  
    5.11  
     6.1 --- a/src/HOL/Set.ML	Sat Nov 01 12:58:08 1997 +0100
     6.2 +++ b/src/HOL/Set.ML	Sat Nov 01 12:59:06 1997 +0100
     6.3 @@ -117,7 +117,15 @@
     6.4  by (REPEAT (ares_tac (prems @ [ballI]) 1));
     6.5  qed "subsetI";
     6.6  
     6.7 -Blast.declConsts (["op <="], [subsetI]);	(*overloading of <=*)
     6.8 +Blast.overload ("op <=", domain_type); (*The <= relation is overloaded*)
     6.9 +
    6.10 +(*While (:) is not, its type must be kept
    6.11 +  for overloading of = to work.*)
    6.12 +Blast.overload ("op :", domain_type);
    6.13 +seq (fn a => Blast.overload (a, HOLogic.dest_setT o domain_type))
    6.14 +    ["Ball", "Bex"];
    6.15 +(*need UNION, INTER also?*)
    6.16 +
    6.17  
    6.18  (*Rule in Modus Ponens style*)
    6.19  val major::prems = goalw Set.thy [subset_def] "[| A <= B;  c:A |] ==> c:B";
    6.20 @@ -152,7 +160,7 @@
    6.21  AddEs  [subsetD, subsetCE];
    6.22  
    6.23  qed_goal "subset_refl" Set.thy "A <= (A::'a set)"
    6.24 - (fn _=> [Blast_tac 1]);
    6.25 + (fn _=> [Fast_tac 1]);		(*Blast_tac would try order_refl and fail*)
    6.26  
    6.27  val prems = goal Set.thy "!!B. [| A<=B;  B<=C |] ==> A<=(C::'a set)";
    6.28  by (Blast_tac 1);
    6.29 @@ -168,7 +176,6 @@
    6.30  qed "subset_antisym";
    6.31  val equalityI = subset_antisym;
    6.32  
    6.33 -Blast.declConsts (["op ="], [equalityI]);	(*overloading of equality*)
    6.34  AddSIs [equalityI];
    6.35  
    6.36  (* Equality rules from ZF set theory -- are they appropriate here? *)
    6.37 @@ -642,9 +649,6 @@
    6.38  by (etac minor 1);
    6.39  qed "rangeE";
    6.40  
    6.41 -AddIs  [rangeI]; 
    6.42 -AddSEs [rangeE]; 
    6.43 -
    6.44  
    6.45  (*** Set reasoning tools ***)
    6.46  
    6.47 @@ -694,3 +698,5 @@
    6.48      "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
    6.49  by (Auto_tac());
    6.50  qed "psubset_insertD";
    6.51 +
    6.52 +bind_thm ("psubset_eq", psubset_def RS meta_eq_to_obj_eq);
     7.1 --- a/src/HOL/Sexp.ML	Sat Nov 01 12:58:08 1997 +0100
     7.2 +++ b/src/HOL/Sexp.ML	Sat Nov 01 12:59:06 1997 +0100
     7.3 @@ -90,7 +90,7 @@
     7.4  goal Sexp.thy "wf(pred_sexp)";
     7.5  by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
     7.6  by (etac sexp.induct 1);
     7.7 -by (ALLGOALS (fast_tac (!claset addSEs [mp, pred_sexpE])));
     7.8 +by (ALLGOALS (blast_tac (!claset addSEs [allE, pred_sexpE])));
     7.9  qed "wf_pred_sexp";
    7.10  
    7.11  
     8.1 --- a/src/HOL/WF.ML	Sat Nov 01 12:58:08 1997 +0100
     8.2 +++ b/src/HOL/WF.ML	Sat Nov 01 12:59:06 1997 +0100
     8.3 @@ -121,9 +121,10 @@
     8.4   by (Blast_tac 2);
     8.5  by (case_tac "y:Q" 1);
     8.6   by (Blast_tac 2);
     8.7 -by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1);
     8.8 +by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")] allE 1);
     8.9   by (assume_tac 1);
    8.10 -by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
    8.11 +by (thin_tac "! Q. (? x. x : Q) --> ?P Q" 1);	(*essential for speed*)
    8.12 +by (blast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
    8.13  qed "wf_insert";
    8.14  AddIffs [wf_insert];
    8.15  
     9.1 --- a/src/HOL/cladata.ML	Sat Nov 01 12:58:08 1997 +0100
     9.2 +++ b/src/HOL/cladata.ML	Sat Nov 01 12:59:06 1997 +0100
     9.3 @@ -93,7 +93,7 @@
     9.4    end;
     9.5  
     9.6  structure Blast = BlastFun(Blast_Data);
     9.7 -Blast.declConsts (["op ="], [iffI]);	(*overloading of equality as iff*)
     9.8 +Blast.overload ("op =", domain_type);	(*overloading of equality as iff*)
     9.9  
    9.10  val Blast_tac = Blast.Blast_tac
    9.11  and blast_tac = Blast.blast_tac;
    10.1 --- a/src/HOL/equalities.ML	Sat Nov 01 12:58:08 1997 +0100
    10.2 +++ b/src/HOL/equalities.ML	Sat Nov 01 12:59:06 1997 +0100
    10.3 @@ -12,12 +12,12 @@
    10.4  
    10.5  section "{}";
    10.6  
    10.7 -goal Set.thy "{x. False} = {}";
    10.8 +goal thy "{x. False} = {}";
    10.9  by (Blast_tac 1);
   10.10  qed "Collect_False_empty";
   10.11  Addsimps [Collect_False_empty];
   10.12  
   10.13 -goal Set.thy "(A <= {}) = (A = {})";
   10.14 +goal thy "(A <= {}) = (A = {})";
   10.15  by (Blast_tac 1);
   10.16  qed "subset_empty";
   10.17  Addsimps [subset_empty];
   10.18 @@ -30,11 +30,11 @@
   10.19  section "insert";
   10.20  
   10.21  (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
   10.22 -goal Set.thy "insert a A = {a} Un A";
   10.23 +goal thy "insert a A = {a} Un A";
   10.24  by (Blast_tac 1);
   10.25  qed "insert_is_Un";
   10.26  
   10.27 -goal Set.thy "insert a A ~= {}";
   10.28 +goal thy "insert a A ~= {}";
   10.29  by (blast_tac (!claset addEs [equalityCE]) 1);
   10.30  qed"insert_not_empty";
   10.31  Addsimps[insert_not_empty];
   10.32 @@ -42,78 +42,81 @@
   10.33  bind_thm("empty_not_insert",insert_not_empty RS not_sym);
   10.34  Addsimps[empty_not_insert];
   10.35  
   10.36 -goal Set.thy "!!a. a:A ==> insert a A = A";
   10.37 +goal thy "!!a. a:A ==> insert a A = A";
   10.38  by (Blast_tac 1);
   10.39  qed "insert_absorb";
   10.40  
   10.41 -goal Set.thy "insert x (insert x A) = insert x A";
   10.42 +goal thy "insert x (insert x A) = insert x A";
   10.43  by (Blast_tac 1);
   10.44  qed "insert_absorb2";
   10.45  Addsimps [insert_absorb2];
   10.46  
   10.47 -goal Set.thy "insert x (insert y A) = insert y (insert x A)";
   10.48 +goal thy "insert x (insert y A) = insert y (insert x A)";
   10.49  by (Blast_tac 1);
   10.50  qed "insert_commute";
   10.51  
   10.52 -goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
   10.53 +goal thy "(insert x A <= B) = (x:B & A <= B)";
   10.54  by (Blast_tac 1);
   10.55  qed "insert_subset";
   10.56  Addsimps[insert_subset];
   10.57  
   10.58 -goal Set.thy "!!a. insert a A ~= insert a B ==> A ~= B";
   10.59 +goal thy "!!a. insert a A ~= insert a B ==> A ~= B";
   10.60  by (Blast_tac 1);
   10.61  qed "insert_lim";
   10.62  
   10.63  (* use new B rather than (A-{a}) to avoid infinite unfolding *)
   10.64 -goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
   10.65 +goal thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
   10.66  by (res_inst_tac [("x","A-{a}")] exI 1);
   10.67  by (Blast_tac 1);
   10.68  qed "mk_disjoint_insert";
   10.69  
   10.70 -goal Set.thy
   10.71 +goal thy
   10.72      "!!A. A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
   10.73  by (Blast_tac 1);
   10.74  qed "UN_insert_distrib";
   10.75  
   10.76 -goal Set.thy "(UN x. insert a (B x)) = insert a (UN x. B x)";
   10.77 +goal thy "(UN x. insert a (B x)) = insert a (UN x. B x)";
   10.78  by (Blast_tac 1);
   10.79  qed "UN1_insert_distrib";
   10.80  
   10.81  section "``";
   10.82  
   10.83 -goal Set.thy "f``{} = {}";
   10.84 +goal thy "f``{} = {}";
   10.85  by (Blast_tac 1);
   10.86  qed "image_empty";
   10.87  Addsimps[image_empty];
   10.88  
   10.89 -goal Set.thy "f``insert a B = insert (f a) (f``B)";
   10.90 +goal thy "f``insert a B = insert (f a) (f``B)";
   10.91  by (Blast_tac 1);
   10.92  qed "image_insert";
   10.93  Addsimps[image_insert];
   10.94  
   10.95 -goal Set.thy  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
   10.96 +goal thy  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
   10.97  by (Blast_tac 1);
   10.98  qed "image_UNION";
   10.99  
  10.100 -goal Set.thy "(%x. x) `` Y = Y";
  10.101 +goal thy "(%x. x) `` Y = Y";
  10.102  by (Blast_tac 1);
  10.103  qed "image_id";
  10.104  
  10.105 -goal Set.thy "f``(range g) = range (%x. f (g x))";
  10.106 +goal thy "f``(g``A) = (%x. f (g x)) `` A";
  10.107  by (Blast_tac 1);
  10.108 -qed "image_range";
  10.109 +qed "image_image";
  10.110  
  10.111 -goal Set.thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
  10.112 +qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
  10.113 + (fn _ => [Blast_tac 1]);
  10.114 +
  10.115 +goal thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
  10.116  by (Blast_tac 1);
  10.117  qed "insert_image";
  10.118  Addsimps [insert_image];
  10.119  
  10.120 -goal Set.thy "(f``A = {}) = (A = {})";
  10.121 +goal thy "(f``A = {}) = (A = {})";
  10.122  by (blast_tac (!claset addSEs [equalityE]) 1);
  10.123  qed "image_is_empty";
  10.124  AddIffs [image_is_empty];
  10.125  
  10.126 -goalw Set.thy [image_def]
  10.127 +goalw thy [image_def]
  10.128  "(%x. if P x then f x else g x) `` S                    \
  10.129  \ = (f `` ({x. x:S & P x})) Un (g `` ({x. x:S & ~(P x)}))";
  10.130  by (split_tac [expand_if] 1);
  10.131 @@ -122,252 +125,246 @@
  10.132  Addsimps[if_image_distrib];
  10.133  
  10.134  
  10.135 -section "range";
  10.136 -
  10.137 -qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"
  10.138 - (fn _ => [Blast_tac 1]);
  10.139 -
  10.140 -
  10.141  section "Int";
  10.142  
  10.143 -goal Set.thy "A Int A = A";
  10.144 +goal thy "A Int A = A";
  10.145  by (Blast_tac 1);
  10.146  qed "Int_absorb";
  10.147  Addsimps[Int_absorb];
  10.148  
  10.149 -goal Set.thy "A Int B  =  B Int A";
  10.150 +goal thy "A Int B  =  B Int A";
  10.151  by (Blast_tac 1);
  10.152  qed "Int_commute";
  10.153  
  10.154 -goal Set.thy "(A Int B) Int C  =  A Int (B Int C)";
  10.155 +goal thy "(A Int B) Int C  =  A Int (B Int C)";
  10.156  by (Blast_tac 1);
  10.157  qed "Int_assoc";
  10.158  
  10.159 -goal Set.thy "{} Int B = {}";
  10.160 +goal thy "{} Int B = {}";
  10.161  by (Blast_tac 1);
  10.162  qed "Int_empty_left";
  10.163  Addsimps[Int_empty_left];
  10.164  
  10.165 -goal Set.thy "A Int {} = {}";
  10.166 +goal thy "A Int {} = {}";
  10.167  by (Blast_tac 1);
  10.168  qed "Int_empty_right";
  10.169  Addsimps[Int_empty_right];
  10.170  
  10.171 -goal Set.thy "(A Int B = {}) = (A <= Compl B)";
  10.172 +goal thy "(A Int B = {}) = (A <= Compl B)";
  10.173  by (blast_tac (!claset addSEs [equalityE]) 1);
  10.174  qed "disjoint_eq_subset_Compl";
  10.175  
  10.176 -goal Set.thy "UNIV Int B = B";
  10.177 +goal thy "UNIV Int B = B";
  10.178  by (Blast_tac 1);
  10.179  qed "Int_UNIV_left";
  10.180  Addsimps[Int_UNIV_left];
  10.181  
  10.182 -goal Set.thy "A Int UNIV = A";
  10.183 +goal thy "A Int UNIV = A";
  10.184  by (Blast_tac 1);
  10.185  qed "Int_UNIV_right";
  10.186  Addsimps[Int_UNIV_right];
  10.187  
  10.188 -goal Set.thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
  10.189 +goal thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
  10.190  by (Blast_tac 1);
  10.191  qed "Int_Un_distrib";
  10.192  
  10.193 -goal Set.thy "(B Un C) Int A =  (B Int A) Un (C Int A)";
  10.194 +goal thy "(B Un C) Int A =  (B Int A) Un (C Int A)";
  10.195  by (Blast_tac 1);
  10.196  qed "Int_Un_distrib2";
  10.197  
  10.198 -goal Set.thy "(A<=B) = (A Int B = A)";
  10.199 +goal thy "(A<=B) = (A Int B = A)";
  10.200  by (blast_tac (!claset addSEs [equalityE]) 1);
  10.201  qed "subset_Int_eq";
  10.202  
  10.203 -goal Set.thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
  10.204 +goal thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
  10.205  by (blast_tac (!claset addEs [equalityCE]) 1);
  10.206  qed "Int_UNIV";
  10.207  Addsimps[Int_UNIV];
  10.208  
  10.209  section "Un";
  10.210  
  10.211 -goal Set.thy "A Un A = A";
  10.212 +goal thy "A Un A = A";
  10.213  by (Blast_tac 1);
  10.214  qed "Un_absorb";
  10.215  Addsimps[Un_absorb];
  10.216  
  10.217 -goal Set.thy " A Un (A Un B) = A Un B";
  10.218 +goal thy " A Un (A Un B) = A Un B";
  10.219  by (Blast_tac 1);
  10.220  qed "Un_left_absorb";
  10.221  
  10.222 -goal Set.thy "A Un B  =  B Un A";
  10.223 +goal thy "A Un B  =  B Un A";
  10.224  by (Blast_tac 1);
  10.225  qed "Un_commute";
  10.226  
  10.227 -goal Set.thy " A Un (B Un C) = B Un (A Un C)";
  10.228 +goal thy " A Un (B Un C) = B Un (A Un C)";
  10.229  by (Blast_tac 1);
  10.230  qed "Un_left_commute";
  10.231  
  10.232 -goal Set.thy "(A Un B) Un C  =  A Un (B Un C)";
  10.233 +goal thy "(A Un B) Un C  =  A Un (B Un C)";
  10.234  by (Blast_tac 1);
  10.235  qed "Un_assoc";
  10.236  
  10.237 -goal Set.thy "{} Un B = B";
  10.238 +goal thy "{} Un B = B";
  10.239  by (Blast_tac 1);
  10.240  qed "Un_empty_left";
  10.241  Addsimps[Un_empty_left];
  10.242  
  10.243 -goal Set.thy "A Un {} = A";
  10.244 +goal thy "A Un {} = A";
  10.245  by (Blast_tac 1);
  10.246  qed "Un_empty_right";
  10.247  Addsimps[Un_empty_right];
  10.248  
  10.249 -goal Set.thy "UNIV Un B = UNIV";
  10.250 +goal thy "UNIV Un B = UNIV";
  10.251  by (Blast_tac 1);
  10.252  qed "Un_UNIV_left";
  10.253  Addsimps[Un_UNIV_left];
  10.254  
  10.255 -goal Set.thy "A Un UNIV = UNIV";
  10.256 +goal thy "A Un UNIV = UNIV";
  10.257  by (Blast_tac 1);
  10.258  qed "Un_UNIV_right";
  10.259  Addsimps[Un_UNIV_right];
  10.260  
  10.261 -goal Set.thy "(insert a B) Un C = insert a (B Un C)";
  10.262 +goal thy "(insert a B) Un C = insert a (B Un C)";
  10.263  by (Blast_tac 1);
  10.264  qed "Un_insert_left";
  10.265  Addsimps[Un_insert_left];
  10.266  
  10.267 -goal Set.thy "A Un (insert a B) = insert a (A Un B)";
  10.268 +goal thy "A Un (insert a B) = insert a (A Un B)";
  10.269  by (Blast_tac 1);
  10.270  qed "Un_insert_right";
  10.271  Addsimps[Un_insert_right];
  10.272  
  10.273 -goal Set.thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
  10.274 +goal thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
  10.275  \                                          else        B Int C)";
  10.276  by (simp_tac (!simpset addsplits [expand_if]) 1);
  10.277  by (Blast_tac 1);
  10.278  qed "Int_insert_left";
  10.279  
  10.280 -goal Set.thy "A Int (insert a B) = (if a:A then insert a (A Int B) \
  10.281 +goal thy "A Int (insert a B) = (if a:A then insert a (A Int B) \
  10.282  \                                          else        A Int B)";
  10.283  by (simp_tac (!simpset addsplits [expand_if]) 1);
  10.284  by (Blast_tac 1);
  10.285  qed "Int_insert_right";
  10.286  
  10.287 -goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
  10.288 +goal thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
  10.289  by (Blast_tac 1);
  10.290  qed "Un_Int_distrib";
  10.291  
  10.292 -goal Set.thy
  10.293 +goal thy
  10.294   "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
  10.295  by (Blast_tac 1);
  10.296  qed "Un_Int_crazy";
  10.297  
  10.298 -goal Set.thy "(A<=B) = (A Un B = B)";
  10.299 +goal thy "(A<=B) = (A Un B = B)";
  10.300  by (blast_tac (!claset addSEs [equalityE]) 1);
  10.301  qed "subset_Un_eq";
  10.302  
  10.303 -goal Set.thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
  10.304 +goal thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
  10.305  by (Blast_tac 1);
  10.306  qed "subset_insert_iff";
  10.307  
  10.308 -goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
  10.309 +goal thy "(A Un B = {}) = (A = {} & B = {})";
  10.310  by (blast_tac (!claset addEs [equalityCE]) 1);
  10.311  qed "Un_empty";
  10.312  Addsimps[Un_empty];
  10.313  
  10.314  section "Compl";
  10.315  
  10.316 -goal Set.thy "A Int Compl(A) = {}";
  10.317 +goal thy "A Int Compl(A) = {}";
  10.318  by (Blast_tac 1);
  10.319  qed "Compl_disjoint";
  10.320  Addsimps[Compl_disjoint];
  10.321  
  10.322 -goal Set.thy "A Un Compl(A) = UNIV";
  10.323 +goal thy "A Un Compl(A) = UNIV";
  10.324  by (Blast_tac 1);
  10.325  qed "Compl_partition";
  10.326  
  10.327 -goal Set.thy "Compl(Compl(A)) = A";
  10.328 +goal thy "Compl(Compl(A)) = A";
  10.329  by (Blast_tac 1);
  10.330  qed "double_complement";
  10.331  Addsimps[double_complement];
  10.332  
  10.333 -goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
  10.334 +goal thy "Compl(A Un B) = Compl(A) Int Compl(B)";
  10.335  by (Blast_tac 1);
  10.336  qed "Compl_Un";
  10.337  
  10.338 -goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
  10.339 +goal thy "Compl(A Int B) = Compl(A) Un Compl(B)";
  10.340  by (Blast_tac 1);
  10.341  qed "Compl_Int";
  10.342  
  10.343 -goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
  10.344 +goal thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
  10.345  by (Blast_tac 1);
  10.346  qed "Compl_UN";
  10.347  
  10.348 -goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
  10.349 +goal thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
  10.350  by (Blast_tac 1);
  10.351  qed "Compl_INT";
  10.352  
  10.353  (*Halmos, Naive Set Theory, page 16.*)
  10.354  
  10.355 -goal Set.thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
  10.356 +goal thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
  10.357  by (blast_tac (!claset addSEs [equalityE]) 1);
  10.358  qed "Un_Int_assoc_eq";
  10.359  
  10.360  
  10.361  section "Union";
  10.362  
  10.363 -goal Set.thy "Union({}) = {}";
  10.364 +goal thy "Union({}) = {}";
  10.365  by (Blast_tac 1);
  10.366  qed "Union_empty";
  10.367  Addsimps[Union_empty];
  10.368  
  10.369 -goal Set.thy "Union(UNIV) = UNIV";
  10.370 +goal thy "Union(UNIV) = UNIV";
  10.371  by (Blast_tac 1);
  10.372  qed "Union_UNIV";
  10.373  Addsimps[Union_UNIV];
  10.374  
  10.375 -goal Set.thy "Union(insert a B) = a Un Union(B)";
  10.376 +goal thy "Union(insert a B) = a Un Union(B)";
  10.377  by (Blast_tac 1);
  10.378  qed "Union_insert";
  10.379  Addsimps[Union_insert];
  10.380  
  10.381 -goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
  10.382 +goal thy "Union(A Un B) = Union(A) Un Union(B)";
  10.383  by (Blast_tac 1);
  10.384  qed "Union_Un_distrib";
  10.385  Addsimps[Union_Un_distrib];
  10.386  
  10.387 -goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)";
  10.388 +goal thy "Union(A Int B) <= Union(A) Int Union(B)";
  10.389  by (Blast_tac 1);
  10.390  qed "Union_Int_subset";
  10.391  
  10.392 -goal Set.thy "(Union M = {}) = (! A : M. A = {})"; 
  10.393 +goal thy "(Union M = {}) = (! A : M. A = {})"; 
  10.394  by (blast_tac (!claset addEs [equalityE]) 1);
  10.395  qed"Union_empty_conv"; 
  10.396  AddIffs [Union_empty_conv];
  10.397  
  10.398 -val prems = goal Set.thy
  10.399 +val prems = goal thy
  10.400     "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
  10.401  by (blast_tac (!claset addSEs [equalityE]) 1);
  10.402  qed "Union_disjoint";
  10.403  
  10.404  section "Inter";
  10.405  
  10.406 -goal Set.thy "Inter({}) = UNIV";
  10.407 +goal thy "Inter({}) = UNIV";
  10.408  by (Blast_tac 1);
  10.409  qed "Inter_empty";
  10.410  Addsimps[Inter_empty];
  10.411  
  10.412 -goal Set.thy "Inter(UNIV) = {}";
  10.413 +goal thy "Inter(UNIV) = {}";
  10.414  by (Blast_tac 1);
  10.415  qed "Inter_UNIV";
  10.416  Addsimps[Inter_UNIV];
  10.417  
  10.418 -goal Set.thy "Inter(insert a B) = a Int Inter(B)";
  10.419 +goal thy "Inter(insert a B) = a Int Inter(B)";
  10.420  by (Blast_tac 1);
  10.421  qed "Inter_insert";
  10.422  Addsimps[Inter_insert];
  10.423  
  10.424 -goal Set.thy "Inter(A) Un Inter(B) <= Inter(A Int B)";
  10.425 +goal thy "Inter(A) Un Inter(B) <= Inter(A Int B)";
  10.426  by (Blast_tac 1);
  10.427  qed "Inter_Un_subset";
  10.428  
  10.429 -goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
  10.430 +goal thy "Inter(A Un B) = Inter(A) Int Inter(B)";
  10.431  by (Blast_tac 1);
  10.432  qed "Inter_Un_distrib";
  10.433  
  10.434 @@ -375,147 +372,139 @@
  10.435  
  10.436  (*Basic identities*)
  10.437  
  10.438 -goal Set.thy "(UN x:{}. B x) = {}";
  10.439 +goal thy "(UN x:{}. B x) = {}";
  10.440  by (Blast_tac 1);
  10.441  qed "UN_empty";
  10.442  Addsimps[UN_empty];
  10.443  
  10.444 -goal Set.thy "(UN x:A. {}) = {}";
  10.445 +goal thy "(UN x:A. {}) = {}";
  10.446  by (Blast_tac 1);
  10.447  qed "UN_empty2";
  10.448  Addsimps[UN_empty2];
  10.449  
  10.450 -goal Set.thy "(UN x:UNIV. B x) = (UN x. B x)";
  10.451 +goal thy "(UN x:UNIV. B x) = (UN x. B x)";
  10.452  by (Blast_tac 1);
  10.453  qed "UN_UNIV";
  10.454  Addsimps[UN_UNIV];
  10.455  
  10.456 -goal Set.thy "(INT x:{}. B x) = UNIV";
  10.457 +goal thy "(INT x:{}. B x) = UNIV";
  10.458  by (Blast_tac 1);
  10.459  qed "INT_empty";
  10.460  Addsimps[INT_empty];
  10.461  
  10.462 -goal Set.thy "(INT x:UNIV. B x) = (INT x. B x)";
  10.463 +goal thy "(INT x:UNIV. B x) = (INT x. B x)";
  10.464  by (Blast_tac 1);
  10.465  qed "INT_UNIV";
  10.466  Addsimps[INT_UNIV];
  10.467  
  10.468 -goal Set.thy "(UN x:insert a A. B x) = B a Un UNION A B";
  10.469 +goal thy "(UN x:insert a A. B x) = B a Un UNION A B";
  10.470  by (Blast_tac 1);
  10.471  qed "UN_insert";
  10.472  Addsimps[UN_insert];
  10.473  
  10.474 -goal Set.thy "(UN i: A Un B. M i) = ((UN i: A. M i) Un (UN i:B. M i))";
  10.475 +goal thy "(UN i: A Un B. M i) = ((UN i: A. M i) Un (UN i:B. M i))";
  10.476  by (Blast_tac 1);
  10.477  qed "UN_Un";
  10.478  
  10.479 -goal Set.thy "(INT x:insert a A. B x) = B a Int INTER A B";
  10.480 +goal thy "(INT x:insert a A. B x) = B a Int INTER A B";
  10.481  by (Blast_tac 1);
  10.482  qed "INT_insert";
  10.483  Addsimps[INT_insert];
  10.484  
  10.485 -goal Set.thy
  10.486 +goal thy
  10.487      "!!A. A~={} ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
  10.488  by (Blast_tac 1);
  10.489  qed "INT_insert_distrib";
  10.490  
  10.491 -goal Set.thy "(INT x. insert a (B x)) = insert a (INT x. B x)";
  10.492 +goal thy "(INT x. insert a (B x)) = insert a (INT x. B x)";
  10.493  by (Blast_tac 1);
  10.494  qed "INT1_insert_distrib";
  10.495  
  10.496 -goal Set.thy "Union(range(f)) = (UN x. f(x))";
  10.497 -by (Blast_tac 1);
  10.498 -qed "Union_range_eq";
  10.499 -
  10.500 -goal Set.thy "Inter(range(f)) = (INT x. f(x))";
  10.501 -by (Blast_tac 1);
  10.502 -qed "Inter_range_eq";
  10.503 -
  10.504 -goal Set.thy "Union(B``A) = (UN x:A. B(x))";
  10.505 +goal thy "Union(B``A) = (UN x:A. B(x))";
  10.506  by (Blast_tac 1);
  10.507  qed "Union_image_eq";
  10.508  
  10.509 -goal Set.thy "Inter(B``A) = (INT x:A. B(x))";
  10.510 +goal thy "Inter(B``A) = (INT x:A. B(x))";
  10.511  by (Blast_tac 1);
  10.512  qed "Inter_image_eq";
  10.513  
  10.514 -goal Set.thy "!!A. a: A ==> (UN y:A. c) = c";
  10.515 +goal thy "!!A. a: A ==> (UN y:A. c) = c";
  10.516  by (Blast_tac 1);
  10.517  qed "UN_constant";
  10.518  
  10.519 -goal Set.thy "!!A. a: A ==> (INT y:A. c) = c";
  10.520 +goal thy "!!A. a: A ==> (INT y:A. c) = c";
  10.521  by (Blast_tac 1);
  10.522  qed "INT_constant";
  10.523  
  10.524 -goal Set.thy "(UN x. B) = B";
  10.525 +goal thy "(UN x. B) = B";
  10.526  by (Blast_tac 1);
  10.527  qed "UN1_constant";
  10.528  Addsimps[UN1_constant];
  10.529  
  10.530 -goal Set.thy "(INT x. B) = B";
  10.531 +goal thy "(INT x. B) = B";
  10.532  by (Blast_tac 1);
  10.533  qed "INT1_constant";
  10.534  Addsimps[INT1_constant];
  10.535  
  10.536 -goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
  10.537 +goal thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
  10.538  by (Blast_tac 1);
  10.539  qed "UN_eq";
  10.540  
  10.541  (*Look: it has an EXISTENTIAL quantifier*)
  10.542 -goal Set.thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
  10.543 +goal thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
  10.544  by (Blast_tac 1);
  10.545  qed "INT_eq";
  10.546  
  10.547 -goalw Set.thy [o_def] "UNION A (g o f) = UNION (f``A) g";
  10.548 +goalw thy [o_def] "UNION A (g o f) = UNION (f``A) g";
  10.549  by (Blast_tac 1);
  10.550  qed "UNION_o";
  10.551  
  10.552  
  10.553  (*Distributive laws...*)
  10.554  
  10.555 -goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
  10.556 +goal thy "A Int Union(B) = (UN C:B. A Int C)";
  10.557  by (Blast_tac 1);
  10.558  qed "Int_Union";
  10.559  
  10.560  (* Devlin, Setdamentals of Contemporary Set Theory, page 12, exercise 5: 
  10.561     Union of a family of unions **)
  10.562 -goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
  10.563 +goal thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
  10.564  by (Blast_tac 1);
  10.565  qed "Un_Union_image";
  10.566  
  10.567  (*Equivalent version*)
  10.568 -goal Set.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
  10.569 +goal thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
  10.570  by (Blast_tac 1);
  10.571  qed "UN_Un_distrib";
  10.572  
  10.573 -goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
  10.574 +goal thy "A Un Inter(B) = (INT C:B. A Un C)";
  10.575  by (Blast_tac 1);
  10.576  qed "Un_Inter";
  10.577  
  10.578 -goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
  10.579 +goal thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
  10.580  by (Blast_tac 1);
  10.581  qed "Int_Inter_image";
  10.582  
  10.583  (*Equivalent version*)
  10.584 -goal Set.thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
  10.585 +goal thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
  10.586  by (Blast_tac 1);
  10.587  qed "INT_Int_distrib";
  10.588  
  10.589  (*Halmos, Naive Set Theory, page 35.*)
  10.590 -goal Set.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
  10.591 +goal thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
  10.592  by (Blast_tac 1);
  10.593  qed "Int_UN_distrib";
  10.594  
  10.595 -goal Set.thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
  10.596 +goal thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
  10.597  by (Blast_tac 1);
  10.598  qed "Un_INT_distrib";
  10.599  
  10.600 -goal Set.thy
  10.601 +goal thy
  10.602      "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
  10.603  by (Blast_tac 1);
  10.604  qed "Int_UN_distrib2";
  10.605  
  10.606 -goal Set.thy
  10.607 +goal thy
  10.608      "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
  10.609  by (Blast_tac 1);
  10.610  qed "Un_INT_distrib2";
  10.611 @@ -526,103 +515,103 @@
  10.612  (** The following are not added to the default simpset because
  10.613      (a) they duplicate the body and (b) there are no similar rules for Int. **)
  10.614  
  10.615 -goal Set.thy "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))";
  10.616 +goal thy "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))";
  10.617  by (Blast_tac 1);
  10.618  qed "ball_Un";
  10.619  
  10.620 -goal Set.thy "(EX x:A Un B. P x) = ((EX x:A. P x) | (EX x:B. P x))";
  10.621 +goal thy "(EX x:A Un B. P x) = ((EX x:A. P x) | (EX x:B. P x))";
  10.622  by (Blast_tac 1);
  10.623  qed "bex_Un";
  10.624  
  10.625  
  10.626  section "-";
  10.627  
  10.628 -goal Set.thy "A-A = {}";
  10.629 +goal thy "A-A = {}";
  10.630  by (Blast_tac 1);
  10.631  qed "Diff_cancel";
  10.632  Addsimps[Diff_cancel];
  10.633  
  10.634 -goal Set.thy "{}-A = {}";
  10.635 +goal thy "{}-A = {}";
  10.636  by (Blast_tac 1);
  10.637  qed "empty_Diff";
  10.638  Addsimps[empty_Diff];
  10.639  
  10.640 -goal Set.thy "A-{} = A";
  10.641 +goal thy "A-{} = A";
  10.642  by (Blast_tac 1);
  10.643  qed "Diff_empty";
  10.644  Addsimps[Diff_empty];
  10.645  
  10.646 -goal Set.thy "A-UNIV = {}";
  10.647 +goal thy "A-UNIV = {}";
  10.648  by (Blast_tac 1);
  10.649  qed "Diff_UNIV";
  10.650  Addsimps[Diff_UNIV];
  10.651  
  10.652 -goal Set.thy "!!x. x~:A ==> A - insert x B = A-B";
  10.653 +goal thy "!!x. x~:A ==> A - insert x B = A-B";
  10.654  by (Blast_tac 1);
  10.655  qed "Diff_insert0";
  10.656  Addsimps [Diff_insert0];
  10.657  
  10.658  (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
  10.659 -goal Set.thy "A - insert a B = A - B - {a}";
  10.660 +goal thy "A - insert a B = A - B - {a}";
  10.661  by (Blast_tac 1);
  10.662  qed "Diff_insert";
  10.663  
  10.664  (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
  10.665 -goal Set.thy "A - insert a B = A - {a} - B";
  10.666 +goal thy "A - insert a B = A - {a} - B";
  10.667  by (Blast_tac 1);
  10.668  qed "Diff_insert2";
  10.669  
  10.670 -goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
  10.671 +goal thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
  10.672  by (simp_tac (!simpset addsplits [expand_if]) 1);
  10.673  by (Blast_tac 1);
  10.674  qed "insert_Diff_if";
  10.675  
  10.676 -goal Set.thy "!!x. x:B ==> insert x A - B = A-B";
  10.677 +goal thy "!!x. x:B ==> insert x A - B = A-B";
  10.678  by (Blast_tac 1);
  10.679  qed "insert_Diff1";
  10.680  Addsimps [insert_Diff1];
  10.681  
  10.682 -goal Set.thy "!!a. a:A ==> insert a (A-{a}) = A";
  10.683 +goal thy "!!a. a:A ==> insert a (A-{a}) = A";
  10.684  by (Blast_tac 1);
  10.685  qed "insert_Diff";
  10.686  
  10.687 -goal Set.thy "A Int (B-A) = {}";
  10.688 +goal thy "A Int (B-A) = {}";
  10.689  by (Blast_tac 1);
  10.690  qed "Diff_disjoint";
  10.691  Addsimps[Diff_disjoint];
  10.692  
  10.693 -goal Set.thy "!!A. A<=B ==> A Un (B-A) = B";
  10.694 +goal thy "!!A. A<=B ==> A Un (B-A) = B";
  10.695  by (Blast_tac 1);
  10.696  qed "Diff_partition";
  10.697  
  10.698 -goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
  10.699 +goal thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
  10.700  by (Blast_tac 1);
  10.701  qed "double_diff";
  10.702  
  10.703 -goal Set.thy "A - (B Un C) = (A-B) Int (A-C)";
  10.704 +goal thy "A - (B Un C) = (A-B) Int (A-C)";
  10.705  by (Blast_tac 1);
  10.706  qed "Diff_Un";
  10.707  
  10.708 -goal Set.thy "A - (B Int C) = (A-B) Un (A-C)";
  10.709 +goal thy "A - (B Int C) = (A-B) Un (A-C)";
  10.710  by (Blast_tac 1);
  10.711  qed "Diff_Int";
  10.712  
  10.713 -goal Set.thy "(A Un B) - C = (A - C) Un (B - C)";
  10.714 +goal thy "(A Un B) - C = (A - C) Un (B - C)";
  10.715  by (Blast_tac 1);
  10.716  qed "Un_Diff";
  10.717  
  10.718 -goal Set.thy "(A Int B) - C = (A - C) Int (B - C)";
  10.719 +goal thy "(A Int B) - C = (A - C) Int (B - C)";
  10.720  by (Blast_tac 1);
  10.721  qed "Int_Diff";
  10.722  
  10.723  
  10.724  section "Miscellany";
  10.725  
  10.726 -goal Set.thy "(A = B) = ((A <= (B::'a set)) & (B<=A))";
  10.727 +goal thy "(A = B) = ((A <= (B::'a set)) & (B<=A))";
  10.728  by (Blast_tac 1);
  10.729  qed "set_eq_subset";
  10.730  
  10.731 -goal Set.thy "A <= B =  (! t. t:A --> t:B)";
  10.732 +goal thy "A <= B =  (! t. t:A --> t:B)";
  10.733  by (Blast_tac 1);
  10.734  qed "subset_iff";
  10.735  
  10.736 @@ -630,17 +619,17 @@
  10.737  by (Blast_tac 1);
  10.738  qed "subset_iff_psubset_eq";
  10.739  
  10.740 -goal Set.thy "(!x. x ~: A) = (A={})";
  10.741 +goal thy "(!x. x ~: A) = (A={})";
  10.742  by(Blast_tac 1);
  10.743  qed "all_not_in_conv";
  10.744  AddIffs [all_not_in_conv];
  10.745  
  10.746 -goalw Set.thy [Pow_def] "Pow {} = {{}}";
  10.747 +goalw thy [Pow_def] "Pow {} = {{}}";
  10.748  by (Auto_tac());
  10.749  qed "Pow_empty";
  10.750  Addsimps [Pow_empty];
  10.751  
  10.752 -goal Set.thy "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
  10.753 +goal thy "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
  10.754  by Safe_tac;
  10.755  by (etac swap 1);
  10.756  by (res_inst_tac [("x", "x-{a}")] image_eqI 1);
  10.757 @@ -650,7 +639,7 @@
  10.758  
  10.759  (** Miniscoping: pushing in big Unions and Intersections **)
  10.760  local
  10.761 -  fun prover s = prove_goal Set.thy s (fn _ => [Blast_tac 1])
  10.762 +  fun prover s = prove_goal thy s (fn _ => [Blast_tac 1])
  10.763  in
  10.764  val UN1_simps = map prover 
  10.765                  ["(UN x. insert a (B x)) = insert a (UN x. B x)",