# HG changeset patch
# User paulson
# Date 878385546 -3600
# Node ID 59c1422c9da5fd037446231af25de4fe37df0eb7
# Parent  18fea4aa9625013b34dd677a23577254fb367b1c
New Blast_tac (and minor tidying...)

diff -r 18fea4aa9625 -r 59c1422c9da5 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Sat Nov 01 12:58:08 1997 +0100
+++ b/src/HOL/Divides.ML	Sat Nov 01 12:59:06 1997 +0100
@@ -294,7 +294,7 @@
 (************************************************)
 
 goalw thy [dvd_def] "m dvd 0";
-by (fast_tac (!claset addIs [mult_0_right RS sym]) 1);
+by (blast_tac (!claset addIs [mult_0_right RS sym]) 1);
 qed "dvd_0_right";
 Addsimps [dvd_0_right];
 
@@ -308,12 +308,12 @@
 AddIffs [dvd_1_left];
 
 goalw thy [dvd_def] "m dvd m";
-by (fast_tac (!claset addIs [mult_1_right RS sym]) 1);
+by (blast_tac (!claset addIs [mult_1_right RS sym]) 1);
 qed "dvd_refl";
 Addsimps [dvd_refl];
 
 goalw thy [dvd_def] "!!m n p. [| m dvd n; n dvd p |] ==> m dvd p";
-by (fast_tac (!claset addIs [mult_assoc] ) 1);
+by (blast_tac (!claset addIs [mult_assoc] ) 1);
 qed "dvd_trans";
 
 goalw thy [dvd_def] "!!m n. [| m dvd n; n dvd m |] ==> m=n";
diff -r 18fea4aa9625 -r 59c1422c9da5 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Sat Nov 01 12:58:08 1997 +0100
+++ b/src/HOL/Finite.ML	Sat Nov 01 12:59:06 1997 +0100
@@ -128,20 +128,21 @@
 qed "finite_Diff_singleton";
 AddIffs [finite_Diff_singleton];
 
+(*Lemma for proving finite_imageD*)
 goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_onto f A --> finite A";
 by (etac finite_induct 1);
  by (ALLGOALS Asm_simp_tac);
 by (Clarify_tac 1);
 by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
  by (Clarify_tac 1);
- by (rewtac inj_onto_def);
+ by (full_simp_tac (!simpset addsimps [inj_onto_def]) 1);
  by (Blast_tac 1);
 by (thin_tac "ALL A. ?PP(A)" 1);
 by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
 by (Clarify_tac 1);
 by (res_inst_tac [("x","xa")] bexI 1);
-by (ALLGOALS Asm_simp_tac);
-by (blast_tac (!claset addEs [equalityE]) 1);
+by (ALLGOALS 
+    (asm_full_simp_tac (!simpset addsimps [inj_onto_image_set_diff])));
 val lemma = result();
 
 goal Finite.thy "!!A. [| finite(f``A);  inj_onto f A |] ==> finite A";
diff -r 18fea4aa9625 -r 59c1422c9da5 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Sat Nov 01 12:58:08 1997 +0100
+++ b/src/HOL/Fun.ML	Sat Nov 01 12:59:06 1997 +0100
@@ -128,5 +128,23 @@
                       addEs [inv_injective,injD]) 1);
 qed "inj_onto_inv";
 
+goalw thy [inj_onto_def]
+   "!!f. [| inj_onto f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
+by (Blast_tac 1);
+qed "inj_onto_image_Int";
+
+goalw thy [inj_onto_def]
+   "!!f. [| inj_onto f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
+by (Blast_tac 1);
+qed "inj_onto_image_set_diff";
+
+goalw thy [inj_def] "!!f. inj f ==> f``(A Int B) = f``A Int f``B";
+by (Blast_tac 1);
+qed "image_Int";
+
+goalw thy [inj_def] "!!f. inj f ==> f``(A-B) = f``A - f``B";
+by (Blast_tac 1);
+qed "image_set_diff";
+
 
 val set_cs = !claset delrules [equalityI];
diff -r 18fea4aa9625 -r 59c1422c9da5 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sat Nov 01 12:58:08 1997 +0100
+++ b/src/HOL/Fun.thy	Sat Nov 01 12:59:06 1997 +0100
@@ -8,6 +8,8 @@
 
 Fun = Set +
 
+instance set :: (term) order
+                       (subset_refl,subset_trans,subset_antisym,psubset_eq)
 consts
 
   inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
diff -r 18fea4aa9625 -r 59c1422c9da5 src/HOL/RelPow.ML
--- a/src/HOL/RelPow.ML	Sat Nov 01 12:58:08 1997 +0100
+++ b/src/HOL/RelPow.ML	Sat Nov 01 12:59:06 1997 +0100
@@ -102,7 +102,7 @@
 qed "rel_pow_imp_rtrancl";
 
 goal RelPow.thy "R^* = (UN n. R^n)";
-by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1);
+by (blast_tac (!claset addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1);
 qed "rtrancl_is_UN_rel_pow";
 
 
diff -r 18fea4aa9625 -r 59c1422c9da5 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Sat Nov 01 12:58:08 1997 +0100
+++ b/src/HOL/Set.ML	Sat Nov 01 12:59:06 1997 +0100
@@ -117,7 +117,15 @@
 by (REPEAT (ares_tac (prems @ [ballI]) 1));
 qed "subsetI";
 
-Blast.declConsts (["op <="], [subsetI]);	(*overloading of <=*)
+Blast.overload ("op <=", domain_type); (*The <= relation is overloaded*)
+
+(*While (:) is not, its type must be kept
+  for overloading of = to work.*)
+Blast.overload ("op :", domain_type);
+seq (fn a => Blast.overload (a, HOLogic.dest_setT o domain_type))
+    ["Ball", "Bex"];
+(*need UNION, INTER also?*)
+
 
 (*Rule in Modus Ponens style*)
 val major::prems = goalw Set.thy [subset_def] "[| A <= B;  c:A |] ==> c:B";
@@ -152,7 +160,7 @@
 AddEs  [subsetD, subsetCE];
 
 qed_goal "subset_refl" Set.thy "A <= (A::'a set)"
- (fn _=> [Blast_tac 1]);
+ (fn _=> [Fast_tac 1]);		(*Blast_tac would try order_refl and fail*)
 
 val prems = goal Set.thy "!!B. [| A<=B;  B<=C |] ==> A<=(C::'a set)";
 by (Blast_tac 1);
@@ -168,7 +176,6 @@
 qed "subset_antisym";
 val equalityI = subset_antisym;
 
-Blast.declConsts (["op ="], [equalityI]);	(*overloading of equality*)
 AddSIs [equalityI];
 
 (* Equality rules from ZF set theory -- are they appropriate here? *)
@@ -642,9 +649,6 @@
 by (etac minor 1);
 qed "rangeE";
 
-AddIs  [rangeI]; 
-AddSEs [rangeE]; 
-
 
 (*** Set reasoning tools ***)
 
@@ -694,3 +698,5 @@
     "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
 by (Auto_tac());
 qed "psubset_insertD";
+
+bind_thm ("psubset_eq", psubset_def RS meta_eq_to_obj_eq);
diff -r 18fea4aa9625 -r 59c1422c9da5 src/HOL/Sexp.ML
--- a/src/HOL/Sexp.ML	Sat Nov 01 12:58:08 1997 +0100
+++ b/src/HOL/Sexp.ML	Sat Nov 01 12:59:06 1997 +0100
@@ -90,7 +90,7 @@
 goal Sexp.thy "wf(pred_sexp)";
 by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
 by (etac sexp.induct 1);
-by (ALLGOALS (fast_tac (!claset addSEs [mp, pred_sexpE])));
+by (ALLGOALS (blast_tac (!claset addSEs [allE, pred_sexpE])));
 qed "wf_pred_sexp";
 
 
diff -r 18fea4aa9625 -r 59c1422c9da5 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Sat Nov 01 12:58:08 1997 +0100
+++ b/src/HOL/WF.ML	Sat Nov 01 12:59:06 1997 +0100
@@ -121,9 +121,10 @@
  by (Blast_tac 2);
 by (case_tac "y:Q" 1);
  by (Blast_tac 2);
-by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1);
+by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")] allE 1);
  by (assume_tac 1);
-by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
+by (thin_tac "! Q. (? x. x : Q) --> ?P Q" 1);	(*essential for speed*)
+by (blast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
 qed "wf_insert";
 AddIffs [wf_insert];
 
diff -r 18fea4aa9625 -r 59c1422c9da5 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Sat Nov 01 12:58:08 1997 +0100
+++ b/src/HOL/cladata.ML	Sat Nov 01 12:59:06 1997 +0100
@@ -93,7 +93,7 @@
   end;
 
 structure Blast = BlastFun(Blast_Data);
-Blast.declConsts (["op ="], [iffI]);	(*overloading of equality as iff*)
+Blast.overload ("op =", domain_type);	(*overloading of equality as iff*)
 
 val Blast_tac = Blast.Blast_tac
 and blast_tac = Blast.blast_tac;
diff -r 18fea4aa9625 -r 59c1422c9da5 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Sat Nov 01 12:58:08 1997 +0100
+++ b/src/HOL/equalities.ML	Sat Nov 01 12:59:06 1997 +0100
@@ -12,12 +12,12 @@
 
 section "{}";
 
-goal Set.thy "{x. False} = {}";
+goal thy "{x. False} = {}";
 by (Blast_tac 1);
 qed "Collect_False_empty";
 Addsimps [Collect_False_empty];
 
-goal Set.thy "(A <= {}) = (A = {})";
+goal thy "(A <= {}) = (A = {})";
 by (Blast_tac 1);
 qed "subset_empty";
 Addsimps [subset_empty];
@@ -30,11 +30,11 @@
 section "insert";
 
 (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
-goal Set.thy "insert a A = {a} Un A";
+goal thy "insert a A = {a} Un A";
 by (Blast_tac 1);
 qed "insert_is_Un";
 
-goal Set.thy "insert a A ~= {}";
+goal thy "insert a A ~= {}";
 by (blast_tac (!claset addEs [equalityCE]) 1);
 qed"insert_not_empty";
 Addsimps[insert_not_empty];
@@ -42,78 +42,81 @@
 bind_thm("empty_not_insert",insert_not_empty RS not_sym);
 Addsimps[empty_not_insert];
 
-goal Set.thy "!!a. a:A ==> insert a A = A";
+goal thy "!!a. a:A ==> insert a A = A";
 by (Blast_tac 1);
 qed "insert_absorb";
 
-goal Set.thy "insert x (insert x A) = insert x A";
+goal thy "insert x (insert x A) = insert x A";
 by (Blast_tac 1);
 qed "insert_absorb2";
 Addsimps [insert_absorb2];
 
-goal Set.thy "insert x (insert y A) = insert y (insert x A)";
+goal thy "insert x (insert y A) = insert y (insert x A)";
 by (Blast_tac 1);
 qed "insert_commute";
 
-goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
+goal thy "(insert x A <= B) = (x:B & A <= B)";
 by (Blast_tac 1);
 qed "insert_subset";
 Addsimps[insert_subset];
 
-goal Set.thy "!!a. insert a A ~= insert a B ==> A ~= B";
+goal thy "!!a. insert a A ~= insert a B ==> A ~= B";
 by (Blast_tac 1);
 qed "insert_lim";
 
 (* use new B rather than (A-{a}) to avoid infinite unfolding *)
-goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
+goal thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
 by (res_inst_tac [("x","A-{a}")] exI 1);
 by (Blast_tac 1);
 qed "mk_disjoint_insert";
 
-goal Set.thy
+goal thy
     "!!A. A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
 by (Blast_tac 1);
 qed "UN_insert_distrib";
 
-goal Set.thy "(UN x. insert a (B x)) = insert a (UN x. B x)";
+goal thy "(UN x. insert a (B x)) = insert a (UN x. B x)";
 by (Blast_tac 1);
 qed "UN1_insert_distrib";
 
 section "``";
 
-goal Set.thy "f``{} = {}";
+goal thy "f``{} = {}";
 by (Blast_tac 1);
 qed "image_empty";
 Addsimps[image_empty];
 
-goal Set.thy "f``insert a B = insert (f a) (f``B)";
+goal thy "f``insert a B = insert (f a) (f``B)";
 by (Blast_tac 1);
 qed "image_insert";
 Addsimps[image_insert];
 
-goal Set.thy  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
+goal thy  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
 by (Blast_tac 1);
 qed "image_UNION";
 
-goal Set.thy "(%x. x) `` Y = Y";
+goal thy "(%x. x) `` Y = Y";
 by (Blast_tac 1);
 qed "image_id";
 
-goal Set.thy "f``(range g) = range (%x. f (g x))";
+goal thy "f``(g``A) = (%x. f (g x)) `` A";
 by (Blast_tac 1);
-qed "image_range";
+qed "image_image";
 
-goal Set.thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
+qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
+ (fn _ => [Blast_tac 1]);
+
+goal thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
 by (Blast_tac 1);
 qed "insert_image";
 Addsimps [insert_image];
 
-goal Set.thy "(f``A = {}) = (A = {})";
+goal thy "(f``A = {}) = (A = {})";
 by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "image_is_empty";
 AddIffs [image_is_empty];
 
-goalw Set.thy [image_def]
+goalw thy [image_def]
 "(%x. if P x then f x else g x) `` S                    \
 \ = (f `` ({x. x:S & P x})) Un (g `` ({x. x:S & ~(P x)}))";
 by (split_tac [expand_if] 1);
@@ -122,252 +125,246 @@
 Addsimps[if_image_distrib];
 
 
-section "range";
-
-qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"
- (fn _ => [Blast_tac 1]);
-
-
 section "Int";
 
-goal Set.thy "A Int A = A";
+goal thy "A Int A = A";
 by (Blast_tac 1);
 qed "Int_absorb";
 Addsimps[Int_absorb];
 
-goal Set.thy "A Int B  =  B Int A";
+goal thy "A Int B  =  B Int A";
 by (Blast_tac 1);
 qed "Int_commute";
 
-goal Set.thy "(A Int B) Int C  =  A Int (B Int C)";
+goal thy "(A Int B) Int C  =  A Int (B Int C)";
 by (Blast_tac 1);
 qed "Int_assoc";
 
-goal Set.thy "{} Int B = {}";
+goal thy "{} Int B = {}";
 by (Blast_tac 1);
 qed "Int_empty_left";
 Addsimps[Int_empty_left];
 
-goal Set.thy "A Int {} = {}";
+goal thy "A Int {} = {}";
 by (Blast_tac 1);
 qed "Int_empty_right";
 Addsimps[Int_empty_right];
 
-goal Set.thy "(A Int B = {}) = (A <= Compl B)";
+goal thy "(A Int B = {}) = (A <= Compl B)";
 by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "disjoint_eq_subset_Compl";
 
-goal Set.thy "UNIV Int B = B";
+goal thy "UNIV Int B = B";
 by (Blast_tac 1);
 qed "Int_UNIV_left";
 Addsimps[Int_UNIV_left];
 
-goal Set.thy "A Int UNIV = A";
+goal thy "A Int UNIV = A";
 by (Blast_tac 1);
 qed "Int_UNIV_right";
 Addsimps[Int_UNIV_right];
 
-goal Set.thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
+goal thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
 by (Blast_tac 1);
 qed "Int_Un_distrib";
 
-goal Set.thy "(B Un C) Int A =  (B Int A) Un (C Int A)";
+goal thy "(B Un C) Int A =  (B Int A) Un (C Int A)";
 by (Blast_tac 1);
 qed "Int_Un_distrib2";
 
-goal Set.thy "(A<=B) = (A Int B = A)";
+goal thy "(A<=B) = (A Int B = A)";
 by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "subset_Int_eq";
 
-goal Set.thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
+goal thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
 by (blast_tac (!claset addEs [equalityCE]) 1);
 qed "Int_UNIV";
 Addsimps[Int_UNIV];
 
 section "Un";
 
-goal Set.thy "A Un A = A";
+goal thy "A Un A = A";
 by (Blast_tac 1);
 qed "Un_absorb";
 Addsimps[Un_absorb];
 
-goal Set.thy " A Un (A Un B) = A Un B";
+goal thy " A Un (A Un B) = A Un B";
 by (Blast_tac 1);
 qed "Un_left_absorb";
 
-goal Set.thy "A Un B  =  B Un A";
+goal thy "A Un B  =  B Un A";
 by (Blast_tac 1);
 qed "Un_commute";
 
-goal Set.thy " A Un (B Un C) = B Un (A Un C)";
+goal thy " A Un (B Un C) = B Un (A Un C)";
 by (Blast_tac 1);
 qed "Un_left_commute";
 
-goal Set.thy "(A Un B) Un C  =  A Un (B Un C)";
+goal thy "(A Un B) Un C  =  A Un (B Un C)";
 by (Blast_tac 1);
 qed "Un_assoc";
 
-goal Set.thy "{} Un B = B";
+goal thy "{} Un B = B";
 by (Blast_tac 1);
 qed "Un_empty_left";
 Addsimps[Un_empty_left];
 
-goal Set.thy "A Un {} = A";
+goal thy "A Un {} = A";
 by (Blast_tac 1);
 qed "Un_empty_right";
 Addsimps[Un_empty_right];
 
-goal Set.thy "UNIV Un B = UNIV";
+goal thy "UNIV Un B = UNIV";
 by (Blast_tac 1);
 qed "Un_UNIV_left";
 Addsimps[Un_UNIV_left];
 
-goal Set.thy "A Un UNIV = UNIV";
+goal thy "A Un UNIV = UNIV";
 by (Blast_tac 1);
 qed "Un_UNIV_right";
 Addsimps[Un_UNIV_right];
 
-goal Set.thy "(insert a B) Un C = insert a (B Un C)";
+goal thy "(insert a B) Un C = insert a (B Un C)";
 by (Blast_tac 1);
 qed "Un_insert_left";
 Addsimps[Un_insert_left];
 
-goal Set.thy "A Un (insert a B) = insert a (A Un B)";
+goal thy "A Un (insert a B) = insert a (A Un B)";
 by (Blast_tac 1);
 qed "Un_insert_right";
 Addsimps[Un_insert_right];
 
-goal Set.thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
+goal thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
 \                                          else        B Int C)";
 by (simp_tac (!simpset addsplits [expand_if]) 1);
 by (Blast_tac 1);
 qed "Int_insert_left";
 
-goal Set.thy "A Int (insert a B) = (if a:A then insert a (A Int B) \
+goal thy "A Int (insert a B) = (if a:A then insert a (A Int B) \
 \                                          else        A Int B)";
 by (simp_tac (!simpset addsplits [expand_if]) 1);
 by (Blast_tac 1);
 qed "Int_insert_right";
 
-goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
+goal thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
 by (Blast_tac 1);
 qed "Un_Int_distrib";
 
-goal Set.thy
+goal thy
  "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
 by (Blast_tac 1);
 qed "Un_Int_crazy";
 
-goal Set.thy "(A<=B) = (A Un B = B)";
+goal thy "(A<=B) = (A Un B = B)";
 by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "subset_Un_eq";
 
-goal Set.thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
+goal thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
 by (Blast_tac 1);
 qed "subset_insert_iff";
 
-goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
+goal thy "(A Un B = {}) = (A = {} & B = {})";
 by (blast_tac (!claset addEs [equalityCE]) 1);
 qed "Un_empty";
 Addsimps[Un_empty];
 
 section "Compl";
 
-goal Set.thy "A Int Compl(A) = {}";
+goal thy "A Int Compl(A) = {}";
 by (Blast_tac 1);
 qed "Compl_disjoint";
 Addsimps[Compl_disjoint];
 
-goal Set.thy "A Un Compl(A) = UNIV";
+goal thy "A Un Compl(A) = UNIV";
 by (Blast_tac 1);
 qed "Compl_partition";
 
-goal Set.thy "Compl(Compl(A)) = A";
+goal thy "Compl(Compl(A)) = A";
 by (Blast_tac 1);
 qed "double_complement";
 Addsimps[double_complement];
 
-goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
+goal thy "Compl(A Un B) = Compl(A) Int Compl(B)";
 by (Blast_tac 1);
 qed "Compl_Un";
 
-goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
+goal thy "Compl(A Int B) = Compl(A) Un Compl(B)";
 by (Blast_tac 1);
 qed "Compl_Int";
 
-goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
+goal thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
 by (Blast_tac 1);
 qed "Compl_UN";
 
-goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
+goal thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
 by (Blast_tac 1);
 qed "Compl_INT";
 
 (*Halmos, Naive Set Theory, page 16.*)
 
-goal Set.thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
+goal thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
 by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "Un_Int_assoc_eq";
 
 
 section "Union";
 
-goal Set.thy "Union({}) = {}";
+goal thy "Union({}) = {}";
 by (Blast_tac 1);
 qed "Union_empty";
 Addsimps[Union_empty];
 
-goal Set.thy "Union(UNIV) = UNIV";
+goal thy "Union(UNIV) = UNIV";
 by (Blast_tac 1);
 qed "Union_UNIV";
 Addsimps[Union_UNIV];
 
-goal Set.thy "Union(insert a B) = a Un Union(B)";
+goal thy "Union(insert a B) = a Un Union(B)";
 by (Blast_tac 1);
 qed "Union_insert";
 Addsimps[Union_insert];
 
-goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
+goal thy "Union(A Un B) = Union(A) Un Union(B)";
 by (Blast_tac 1);
 qed "Union_Un_distrib";
 Addsimps[Union_Un_distrib];
 
-goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)";
+goal thy "Union(A Int B) <= Union(A) Int Union(B)";
 by (Blast_tac 1);
 qed "Union_Int_subset";
 
-goal Set.thy "(Union M = {}) = (! A : M. A = {})"; 
+goal thy "(Union M = {}) = (! A : M. A = {})"; 
 by (blast_tac (!claset addEs [equalityE]) 1);
 qed"Union_empty_conv"; 
 AddIffs [Union_empty_conv];
 
-val prems = goal Set.thy
+val prems = goal thy
    "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
 by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "Union_disjoint";
 
 section "Inter";
 
-goal Set.thy "Inter({}) = UNIV";
+goal thy "Inter({}) = UNIV";
 by (Blast_tac 1);
 qed "Inter_empty";
 Addsimps[Inter_empty];
 
-goal Set.thy "Inter(UNIV) = {}";
+goal thy "Inter(UNIV) = {}";
 by (Blast_tac 1);
 qed "Inter_UNIV";
 Addsimps[Inter_UNIV];
 
-goal Set.thy "Inter(insert a B) = a Int Inter(B)";
+goal thy "Inter(insert a B) = a Int Inter(B)";
 by (Blast_tac 1);
 qed "Inter_insert";
 Addsimps[Inter_insert];
 
-goal Set.thy "Inter(A) Un Inter(B) <= Inter(A Int B)";
+goal thy "Inter(A) Un Inter(B) <= Inter(A Int B)";
 by (Blast_tac 1);
 qed "Inter_Un_subset";
 
-goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
+goal thy "Inter(A Un B) = Inter(A) Int Inter(B)";
 by (Blast_tac 1);
 qed "Inter_Un_distrib";
 
@@ -375,147 +372,139 @@
 
 (*Basic identities*)
 
-goal Set.thy "(UN x:{}. B x) = {}";
+goal thy "(UN x:{}. B x) = {}";
 by (Blast_tac 1);
 qed "UN_empty";
 Addsimps[UN_empty];
 
-goal Set.thy "(UN x:A. {}) = {}";
+goal thy "(UN x:A. {}) = {}";
 by (Blast_tac 1);
 qed "UN_empty2";
 Addsimps[UN_empty2];
 
-goal Set.thy "(UN x:UNIV. B x) = (UN x. B x)";
+goal thy "(UN x:UNIV. B x) = (UN x. B x)";
 by (Blast_tac 1);
 qed "UN_UNIV";
 Addsimps[UN_UNIV];
 
-goal Set.thy "(INT x:{}. B x) = UNIV";
+goal thy "(INT x:{}. B x) = UNIV";
 by (Blast_tac 1);
 qed "INT_empty";
 Addsimps[INT_empty];
 
-goal Set.thy "(INT x:UNIV. B x) = (INT x. B x)";
+goal thy "(INT x:UNIV. B x) = (INT x. B x)";
 by (Blast_tac 1);
 qed "INT_UNIV";
 Addsimps[INT_UNIV];
 
-goal Set.thy "(UN x:insert a A. B x) = B a Un UNION A B";
+goal thy "(UN x:insert a A. B x) = B a Un UNION A B";
 by (Blast_tac 1);
 qed "UN_insert";
 Addsimps[UN_insert];
 
-goal Set.thy "(UN i: A Un B. M i) = ((UN i: A. M i) Un (UN i:B. M i))";
+goal thy "(UN i: A Un B. M i) = ((UN i: A. M i) Un (UN i:B. M i))";
 by (Blast_tac 1);
 qed "UN_Un";
 
-goal Set.thy "(INT x:insert a A. B x) = B a Int INTER A B";
+goal thy "(INT x:insert a A. B x) = B a Int INTER A B";
 by (Blast_tac 1);
 qed "INT_insert";
 Addsimps[INT_insert];
 
-goal Set.thy
+goal thy
     "!!A. A~={} ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
 by (Blast_tac 1);
 qed "INT_insert_distrib";
 
-goal Set.thy "(INT x. insert a (B x)) = insert a (INT x. B x)";
+goal thy "(INT x. insert a (B x)) = insert a (INT x. B x)";
 by (Blast_tac 1);
 qed "INT1_insert_distrib";
 
-goal Set.thy "Union(range(f)) = (UN x. f(x))";
-by (Blast_tac 1);
-qed "Union_range_eq";
-
-goal Set.thy "Inter(range(f)) = (INT x. f(x))";
-by (Blast_tac 1);
-qed "Inter_range_eq";
-
-goal Set.thy "Union(B``A) = (UN x:A. B(x))";
+goal thy "Union(B``A) = (UN x:A. B(x))";
 by (Blast_tac 1);
 qed "Union_image_eq";
 
-goal Set.thy "Inter(B``A) = (INT x:A. B(x))";
+goal thy "Inter(B``A) = (INT x:A. B(x))";
 by (Blast_tac 1);
 qed "Inter_image_eq";
 
-goal Set.thy "!!A. a: A ==> (UN y:A. c) = c";
+goal thy "!!A. a: A ==> (UN y:A. c) = c";
 by (Blast_tac 1);
 qed "UN_constant";
 
-goal Set.thy "!!A. a: A ==> (INT y:A. c) = c";
+goal thy "!!A. a: A ==> (INT y:A. c) = c";
 by (Blast_tac 1);
 qed "INT_constant";
 
-goal Set.thy "(UN x. B) = B";
+goal thy "(UN x. B) = B";
 by (Blast_tac 1);
 qed "UN1_constant";
 Addsimps[UN1_constant];
 
-goal Set.thy "(INT x. B) = B";
+goal thy "(INT x. B) = B";
 by (Blast_tac 1);
 qed "INT1_constant";
 Addsimps[INT1_constant];
 
-goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
+goal thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
 by (Blast_tac 1);
 qed "UN_eq";
 
 (*Look: it has an EXISTENTIAL quantifier*)
-goal Set.thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
+goal thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
 by (Blast_tac 1);
 qed "INT_eq";
 
-goalw Set.thy [o_def] "UNION A (g o f) = UNION (f``A) g";
+goalw thy [o_def] "UNION A (g o f) = UNION (f``A) g";
 by (Blast_tac 1);
 qed "UNION_o";
 
 
 (*Distributive laws...*)
 
-goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
+goal thy "A Int Union(B) = (UN C:B. A Int C)";
 by (Blast_tac 1);
 qed "Int_Union";
 
 (* Devlin, Setdamentals of Contemporary Set Theory, page 12, exercise 5: 
    Union of a family of unions **)
-goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
+goal thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
 by (Blast_tac 1);
 qed "Un_Union_image";
 
 (*Equivalent version*)
-goal Set.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
+goal thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
 by (Blast_tac 1);
 qed "UN_Un_distrib";
 
-goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
+goal thy "A Un Inter(B) = (INT C:B. A Un C)";
 by (Blast_tac 1);
 qed "Un_Inter";
 
-goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
+goal thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
 by (Blast_tac 1);
 qed "Int_Inter_image";
 
 (*Equivalent version*)
-goal Set.thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
+goal thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
 by (Blast_tac 1);
 qed "INT_Int_distrib";
 
 (*Halmos, Naive Set Theory, page 35.*)
-goal Set.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
+goal thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
 by (Blast_tac 1);
 qed "Int_UN_distrib";
 
-goal Set.thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
+goal thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
 by (Blast_tac 1);
 qed "Un_INT_distrib";
 
-goal Set.thy
+goal thy
     "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
 by (Blast_tac 1);
 qed "Int_UN_distrib2";
 
-goal Set.thy
+goal thy
     "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
 by (Blast_tac 1);
 qed "Un_INT_distrib2";
@@ -526,103 +515,103 @@
 (** The following are not added to the default simpset because
     (a) they duplicate the body and (b) there are no similar rules for Int. **)
 
-goal Set.thy "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))";
+goal thy "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))";
 by (Blast_tac 1);
 qed "ball_Un";
 
-goal Set.thy "(EX x:A Un B. P x) = ((EX x:A. P x) | (EX x:B. P x))";
+goal thy "(EX x:A Un B. P x) = ((EX x:A. P x) | (EX x:B. P x))";
 by (Blast_tac 1);
 qed "bex_Un";
 
 
 section "-";
 
-goal Set.thy "A-A = {}";
+goal thy "A-A = {}";
 by (Blast_tac 1);
 qed "Diff_cancel";
 Addsimps[Diff_cancel];
 
-goal Set.thy "{}-A = {}";
+goal thy "{}-A = {}";
 by (Blast_tac 1);
 qed "empty_Diff";
 Addsimps[empty_Diff];
 
-goal Set.thy "A-{} = A";
+goal thy "A-{} = A";
 by (Blast_tac 1);
 qed "Diff_empty";
 Addsimps[Diff_empty];
 
-goal Set.thy "A-UNIV = {}";
+goal thy "A-UNIV = {}";
 by (Blast_tac 1);
 qed "Diff_UNIV";
 Addsimps[Diff_UNIV];
 
-goal Set.thy "!!x. x~:A ==> A - insert x B = A-B";
+goal thy "!!x. x~:A ==> A - insert x B = A-B";
 by (Blast_tac 1);
 qed "Diff_insert0";
 Addsimps [Diff_insert0];
 
 (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
-goal Set.thy "A - insert a B = A - B - {a}";
+goal thy "A - insert a B = A - B - {a}";
 by (Blast_tac 1);
 qed "Diff_insert";
 
 (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
-goal Set.thy "A - insert a B = A - {a} - B";
+goal thy "A - insert a B = A - {a} - B";
 by (Blast_tac 1);
 qed "Diff_insert2";
 
-goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
+goal thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
 by (simp_tac (!simpset addsplits [expand_if]) 1);
 by (Blast_tac 1);
 qed "insert_Diff_if";
 
-goal Set.thy "!!x. x:B ==> insert x A - B = A-B";
+goal thy "!!x. x:B ==> insert x A - B = A-B";
 by (Blast_tac 1);
 qed "insert_Diff1";
 Addsimps [insert_Diff1];
 
-goal Set.thy "!!a. a:A ==> insert a (A-{a}) = A";
+goal thy "!!a. a:A ==> insert a (A-{a}) = A";
 by (Blast_tac 1);
 qed "insert_Diff";
 
-goal Set.thy "A Int (B-A) = {}";
+goal thy "A Int (B-A) = {}";
 by (Blast_tac 1);
 qed "Diff_disjoint";
 Addsimps[Diff_disjoint];
 
-goal Set.thy "!!A. A<=B ==> A Un (B-A) = B";
+goal thy "!!A. A<=B ==> A Un (B-A) = B";
 by (Blast_tac 1);
 qed "Diff_partition";
 
-goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
+goal thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
 by (Blast_tac 1);
 qed "double_diff";
 
-goal Set.thy "A - (B Un C) = (A-B) Int (A-C)";
+goal thy "A - (B Un C) = (A-B) Int (A-C)";
 by (Blast_tac 1);
 qed "Diff_Un";
 
-goal Set.thy "A - (B Int C) = (A-B) Un (A-C)";
+goal thy "A - (B Int C) = (A-B) Un (A-C)";
 by (Blast_tac 1);
 qed "Diff_Int";
 
-goal Set.thy "(A Un B) - C = (A - C) Un (B - C)";
+goal thy "(A Un B) - C = (A - C) Un (B - C)";
 by (Blast_tac 1);
 qed "Un_Diff";
 
-goal Set.thy "(A Int B) - C = (A - C) Int (B - C)";
+goal thy "(A Int B) - C = (A - C) Int (B - C)";
 by (Blast_tac 1);
 qed "Int_Diff";
 
 
 section "Miscellany";
 
-goal Set.thy "(A = B) = ((A <= (B::'a set)) & (B<=A))";
+goal thy "(A = B) = ((A <= (B::'a set)) & (B<=A))";
 by (Blast_tac 1);
 qed "set_eq_subset";
 
-goal Set.thy "A <= B =  (! t. t:A --> t:B)";
+goal thy "A <= B =  (! t. t:A --> t:B)";
 by (Blast_tac 1);
 qed "subset_iff";
 
@@ -630,17 +619,17 @@
 by (Blast_tac 1);
 qed "subset_iff_psubset_eq";
 
-goal Set.thy "(!x. x ~: A) = (A={})";
+goal thy "(!x. x ~: A) = (A={})";
 by(Blast_tac 1);
 qed "all_not_in_conv";
 AddIffs [all_not_in_conv];
 
-goalw Set.thy [Pow_def] "Pow {} = {{}}";
+goalw thy [Pow_def] "Pow {} = {{}}";
 by (Auto_tac());
 qed "Pow_empty";
 Addsimps [Pow_empty];
 
-goal Set.thy "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
+goal thy "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
 by Safe_tac;
 by (etac swap 1);
 by (res_inst_tac [("x", "x-{a}")] image_eqI 1);
@@ -650,7 +639,7 @@
 
 (** Miniscoping: pushing in big Unions and Intersections **)
 local
-  fun prover s = prove_goal Set.thy s (fn _ => [Blast_tac 1])
+  fun prover s = prove_goal thy s (fn _ => [Blast_tac 1])
 in
 val UN1_simps = map prover 
                 ["(UN x. insert a (B x)) = insert a (UN x. B x)",