Replaced fast_tac by Fast_tac (which uses default claset)
New rules are now also added to default claset.
--- a/src/HOL/Fun.ML Tue May 21 10:52:26 1996 +0200
+++ b/src/HOL/Fun.ML Tue May 21 13:39:31 1996 +0200
@@ -51,19 +51,19 @@
goalw Fun.thy [o_def] "(f o g)``r = f``(g``r)";
by (rtac set_ext 1);
-by (fast_tac (HOL_cs addIs [imageI] addSEs [imageE]) 1);
+by (fast_tac (!claset addIs [imageI] addSEs [imageE]) 1);
qed "image_compose";
goal Fun.thy "f``(A Un B) = f``A Un f``B";
by (rtac set_ext 1);
-by (fast_tac (HOL_cs addIs [imageI,UnCI] addSEs [imageE,UnE]) 1);
+by (fast_tac (!claset addIs [imageI,UnCI] addSEs [imageE,UnE]) 1);
qed "image_Un";
(*** inj(f): f is a one-to-one function ***)
val prems = goalw Fun.thy [inj_def]
"[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
-by (fast_tac (HOL_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
qed "injI";
val [major] = goal Fun.thy "(!!x. g(f(x)) = x) ==> inj(f)";
@@ -109,7 +109,7 @@
val prems = goalw Fun.thy [inj_onto_def]
"(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_onto f A";
-by (fast_tac (HOL_cs addIs prems addSIs [ballI]) 1);
+by (fast_tac (!claset addIs prems addSIs [ballI]) 1);
qed "inj_ontoI";
val [major] = goal Fun.thy
@@ -126,7 +126,7 @@
qed "inj_ontoD";
goal Fun.thy "!!x y.[| inj_onto f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)";
-by (fast_tac (HOL_cs addSEs [inj_ontoD]) 1);
+by (fast_tac (!claset addSEs [inj_ontoD]) 1);
qed "inj_onto_iff";
val major::prems = goal Fun.thy
@@ -142,12 +142,12 @@
val prems = goalw Fun.thy [o_def]
"[| inj(f); inj_onto g (range f) |] ==> inj(g o f)";
by (cut_facts_tac prems 1);
-by (fast_tac (HOL_cs addIs [injI,rangeI]
+by (fast_tac (!claset addIs [injI,rangeI]
addEs [injD,inj_ontoD]) 1);
qed "comp_inj";
val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A";
-by (fast_tac (HOL_cs addIs [prem RS injD, inj_ontoI]) 1);
+by (fast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1);
qed "inj_imp";
val [prem] = goalw Fun.thy [Inv_def] "y : range(f) ==> f(Inv f y) = y";
@@ -163,19 +163,28 @@
val prems = goal Fun.thy
"[| inj(f); A<=range(f) |] ==> inj_onto (Inv f) A";
by (cut_facts_tac prems 1);
-by (fast_tac (HOL_cs addIs [inj_ontoI]
+by (fast_tac (!claset addIs [inj_ontoI]
addEs [Inv_injective,injD,subsetD]) 1);
qed "inj_onto_Inv";
(*** Set reasoning tools ***)
+AddSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI,
+ ComplI, IntI, DiffI, UnCI, insertCI];
+AddIs [bexI, UnionI, UN_I, UN1_I, imageI, rangeI];
+AddSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
+ make_elim singleton_inject,
+ CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE];
+AddEs [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
+ subsetD, subsetCE];
+
val set_cs = HOL_cs
addSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI,
ComplI, IntI, DiffI, UnCI, insertCI]
addIs [bexI, UnionI, UN_I, UN1_I, imageI, rangeI]
addSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
- make_elim singleton_inject,
+ make_elim singleton_inject,
CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE]
addEs [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
subsetD, subsetCE];
--- a/src/HOL/Prod.ML Tue May 21 10:52:26 1996 +0200
+++ b/src/HOL/Prod.ML Tue May 21 13:39:31 1996 +0200
@@ -31,15 +31,15 @@
qed "Pair_inject";
goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')";
-by (fast_tac (set_cs addIs [Pair_inject]) 1);
+by (fast_tac (!claset addIs [Pair_inject]) 1);
qed "Pair_eq";
goalw Prod.thy [fst_def] "fst((a,b)) = a";
-by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1);
+by (fast_tac (!claset addIs [select_equality] addSEs [Pair_inject]) 1);
qed "fst_conv";
goalw Prod.thy [snd_def] "snd((a,b)) = b";
-by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1);
+by (fast_tac (!claset addIs [select_equality] addSEs [Pair_inject]) 1);
qed "snd_conv";
goalw Prod.thy [Pair_def] "? x y. p = (x,y)";
@@ -78,7 +78,7 @@
end;
goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
-by (fast_tac (HOL_cs addbefore split_all_tac 1) 1);
+by (fast_tac (!claset addbefore split_all_tac 1) 1);
qed "split_paired_All";
goalw Prod.thy [split_def] "split c (a,b) = c a b";
@@ -117,7 +117,7 @@
goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))";
by (stac surjective_pairing 1);
by (stac split 1);
-by (fast_tac (HOL_cs addSEs [Pair_inject]) 1);
+by (fast_tac (!claset addSEs [Pair_inject]) 1);
qed "expand_split";
(** split used as a logical connective or set former **)
@@ -188,8 +188,8 @@
by (rtac (major RS imageE) 1);
by (res_inst_tac [("p","x")] PairE 1);
by (resolve_tac prems 1);
-by (fast_tac HOL_cs 2);
-by (fast_tac (HOL_cs addIs [prod_fun]) 1);
+by (Fast_tac 2);
+by (fast_tac (!claset addIs [prod_fun]) 1);
qed "prod_fun_imageE";
(*** Disjoint union of a family of sets - Sigma ***)
@@ -230,21 +230,21 @@
val prems = goal Prod.thy
"[| A<=C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
by (cut_facts_tac prems 1);
-by (fast_tac (set_cs addIs (prems RL [subsetD])
+by (fast_tac (!claset addIs (prems RL [subsetD])
addSIs [SigmaI]
addSEs [SigmaE]) 1);
qed "Sigma_mono";
qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
- (fn _ => [ (fast_tac (eq_cs addSEs [SigmaE]) 1) ]);
+ (fn _ => [ (fast_tac (!claset addSEs [SigmaE]) 1) ]);
qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}"
- (fn _ => [ (fast_tac (eq_cs addSEs [SigmaE]) 1) ]);
+ (fn _ => [ (fast_tac (!claset addSEs [SigmaE]) 1) ]);
Addsimps [Sigma_empty1,Sigma_empty2];
goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))";
-by (fast_tac (eq_cs addSIs [SigmaI] addSEs [SigmaE, Pair_inject]) 1);
+by (fast_tac (!claset addSIs [SigmaI] addSEs [SigmaE, Pair_inject]) 1);
qed "mem_Sigma_iff";
Addsimps [mem_Sigma_iff];
@@ -292,6 +292,12 @@
by (stac (rewrite_rule [Unit_def] Rep_Unit RS CollectD RS sym) 1);
by (rtac (Rep_Unit_inverse RS sym) 1);
qed "unit_eq";
+
+AddSIs [SigmaI, splitI, splitI2, mem_splitI, mem_splitI2];
+AddIs [fst_imageI, snd_imageI, prod_fun_imageI];
+AddSEs [SigmaE2, SigmaE, splitE, mem_splitE,
+ fst_imageE, snd_imageE, prod_fun_imageE,
+ Pair_inject];
val prod_cs = set_cs addSIs [SigmaI, splitI, splitI2, mem_splitI, mem_splitI2]
addIs [fst_imageI, snd_imageI, prod_fun_imageI]
--- a/src/HOL/Relation.ML Tue May 21 10:52:26 1996 +0200
+++ b/src/HOL/Relation.ML Tue May 21 13:39:31 1996 +0200
@@ -27,7 +27,7 @@
qed "idE";
goalw Relation.thy [id_def] "(a,b):id = (a=b)";
-by (fast_tac prod_cs 1);
+by (Fast_tac 1);
qed "pair_in_id_conv";
Addsimps [pair_in_id_conv];
@@ -36,7 +36,7 @@
val prems = goalw Relation.thy [comp_def]
"[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
-by (fast_tac (prod_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
qed "compI";
(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
@@ -56,16 +56,19 @@
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
qed "compEpair";
+AddIs [compI, idI];
+AddSEs [compE, idE];
+
val comp_cs = prod_cs addIs [compI, idI] addSEs [compE, idE];
goal Relation.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
-by (fast_tac comp_cs 1);
+by (Fast_tac 1);
qed "comp_mono";
goal Relation.thy
"!!r s. [| s <= A Times B; r <= B Times C |] ==> \
\ (r O s) <= A Times C";
-by (fast_tac comp_cs 1);
+by (Fast_tac 1);
qed "comp_subset_Sigma";
(** Natural deduction for trans(r) **)
@@ -78,7 +81,7 @@
val major::prems = goalw Relation.thy [trans_def]
"[| trans(r); (a,b):r; (b,c):r |] ==> (a,c):r";
by (cut_facts_tac [major] 1);
-by (fast_tac (HOL_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
qed "transD";
(** Natural deduction for converse(r) **)
@@ -88,7 +91,7 @@
qed "converseI";
goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r";
-by (fast_tac comp_cs 1);
+by (Fast_tac 1);
qed "converseD";
qed_goalw "converseE" Relation.thy [converse_def]
@@ -100,18 +103,21 @@
(REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
(assume_tac 1) ]);
-val converse_cs = comp_cs addSIs [converseI]
+AddSIs [converseI];
+AddSEs [converseD,converseE];
+
+val converse_cs = comp_cs addSIs [converseI]
addSEs [converseD,converseE];
goalw Relation.thy [converse_def] "converse(converse R) = R";
-by(fast_tac (prod_cs addSIs [equalityI]) 1);
+by(fast_tac (!claset addSIs [equalityI]) 1);
qed "converse_converse";
(** Domain **)
qed_goalw "Domain_iff" Relation.thy [Domain_def]
"a: Domain(r) = (EX y. (a,y): r)"
- (fn _=> [ (fast_tac comp_cs 1) ]);
+ (fn _=> [ (Fast_tac 1) ]);
qed_goal "DomainI" Relation.thy "!!a b r. (a,b): r ==> a: Domain(r)"
(fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
@@ -138,19 +144,19 @@
qed_goalw "Image_iff" Relation.thy [Image_def]
"b : r^^A = (? x:A. (x,b):r)"
- (fn _ => [ fast_tac (comp_cs addIs [RangeI]) 1 ]);
+ (fn _ => [ fast_tac (!claset addIs [RangeI]) 1 ]);
qed_goal "Image_singleton_iff" Relation.thy
"(b : r^^{a}) = ((a,b):r)"
(fn _ => [ rtac (Image_iff RS trans) 1,
- fast_tac comp_cs 1 ]);
+ Fast_tac 1 ]);
qed_goalw "ImageI" Relation.thy [Image_def]
"!!a b r. [| (a,b): r; a:A |] ==> b : r^^A"
(fn _ => [ (REPEAT (ares_tac [CollectI,RangeI,bexI] 1)),
(resolve_tac [conjI ] 1),
(rtac RangeI 1),
- (REPEAT (fast_tac set_cs 1))]);
+ (REPEAT (Fast_tac 1))]);
qed_goalw "ImageE" Relation.thy [Image_def]
"[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P"
@@ -167,18 +173,24 @@
[ (rtac subsetI 1),
(REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
+AddSIs [converseI];
+AddIs [ImageI, DomainI, RangeI];
+AddSEs [ImageE, DomainE, RangeE];
+
val rel_cs = converse_cs addSIs [converseI]
addIs [ImageI, DomainI, RangeI]
addSEs [ImageE, DomainE, RangeE];
+AddSIs [equalityI];
+
val rel_eq_cs = rel_cs addSIs [equalityI];
goal Relation.thy "R O id = R";
-by(fast_tac (rel_cs addIs [set_ext] addbefore (split_all_tac 1)) 1);
+by(fast_tac (!claset addIs [set_ext] addbefore (split_all_tac 1)) 1);
qed "R_O_id";
goal Relation.thy "id O R = R";
-by(fast_tac (rel_cs addIs [set_ext] addbefore (split_all_tac 1)) 1);
+by(fast_tac (!claset addIs [set_ext] addbefore (split_all_tac 1)) 1);
qed "id_O_R";
Addsimps [R_O_id,id_O_R];
--- a/src/HOL/equalities.ML Tue May 21 10:52:26 1996 +0200
+++ b/src/HOL/equalities.ML Tue May 21 13:39:31 1996 +0200
@@ -8,29 +8,31 @@
writeln"File HOL/equalities";
+AddSIs [equalityI];
+
val eq_cs = set_cs addSIs [equalityI];
section "{}";
goal Set.thy "{x.False} = {}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Collect_False_empty";
Addsimps [Collect_False_empty];
goal Set.thy "(A <= {}) = (A = {})";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "subset_empty";
Addsimps [subset_empty];
section ":";
goal Set.thy "x ~: {}";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "in_empty";
Addsimps[in_empty];
goal Set.thy "x : insert y A = (x=y | x:A)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "in_insert";
Addsimps[in_insert];
@@ -38,11 +40,11 @@
(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
goal Set.thy "insert a A = {a} Un A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "insert_is_Un";
goal Set.thy "insert a A ~= {}";
-by (fast_tac (set_cs addEs [equalityCE]) 1);
+by (fast_tac (!claset addEs [equalityCE]) 1);
qed"insert_not_empty";
Addsimps[insert_not_empty];
@@ -50,45 +52,45 @@
Addsimps[empty_not_insert];
goal Set.thy "!!a. a:A ==> insert a A = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "insert_absorb";
goal Set.thy "insert x (insert x A) = insert x A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "insert_absorb2";
Addsimps [insert_absorb2];
goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "insert_subset";
Addsimps[insert_subset];
(* use new B rather than (A-{a}) to avoid infinite unfolding *)
goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
by (res_inst_tac [("x","A-{a}")] exI 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "mk_disjoint_insert";
section "``";
goal Set.thy "f``{} = {}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "image_empty";
Addsimps[image_empty];
goal Set.thy "f``insert a B = insert (f a) (f``B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "image_insert";
Addsimps[image_insert];
qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
- (fn _ => [fast_tac set_cs 1]);
+ (fn _ => [Fast_tac 1]);
goalw Set.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);
-by(fast_tac eq_cs 1);
+by(Fast_tac 1);
qed "if_image_distrib";
Addsimps[if_image_distrib];
@@ -96,215 +98,215 @@
section "range";
qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"
- (fn _ => [fast_tac set_cs 1]);
+ (fn _ => [Fast_tac 1]);
qed_goalw "image_range" Set.thy [image_def, range_def]
"f``range g = range (%x. f (g x))" (fn _ => [
rtac Collect_cong 1,
- fast_tac set_cs 1]);
+ Fast_tac 1]);
section "Int";
goal Set.thy "A Int A = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_absorb";
Addsimps[Int_absorb];
goal Set.thy "A Int B = B Int A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_commute";
goal Set.thy "(A Int B) Int C = A Int (B Int C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_assoc";
goal Set.thy "{} Int B = {}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_empty_left";
Addsimps[Int_empty_left];
goal Set.thy "A Int {} = {}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_empty_right";
Addsimps[Int_empty_right];
goal Set.thy "UNIV Int B = B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_UNIV_left";
Addsimps[Int_UNIV_left];
goal Set.thy "A Int UNIV = A";
-by (fast_tac eq_cs 1);
+by (Fast_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)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_Un_distrib";
goal Set.thy "(B Un C) Int A = (B Int A) Un (C Int A)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_Un_distrib2";
goal Set.thy "(A<=B) = (A Int B = A)";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
qed "subset_Int_eq";
goal Set.thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
-by (fast_tac (eq_cs addEs [equalityCE]) 1);
+by (fast_tac (!claset addEs [equalityCE]) 1);
qed "Int_UNIV";
Addsimps[Int_UNIV];
section "Un";
goal Set.thy "A Un A = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_absorb";
Addsimps[Un_absorb];
goal Set.thy "A Un B = B Un A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_commute";
goal Set.thy "(A Un B) Un C = A Un (B Un C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_assoc";
goal Set.thy "{} Un B = B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_empty_left";
Addsimps[Un_empty_left];
goal Set.thy "A Un {} = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_empty_right";
Addsimps[Un_empty_right];
goal Set.thy "UNIV Un B = UNIV";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_UNIV_left";
Addsimps[Un_UNIV_left];
goal Set.thy "A Un UNIV = UNIV";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_UNIV_right";
Addsimps[Un_UNIV_right];
goal Set.thy "insert a B Un C = insert a (B Un C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_insert_left";
goal Set.thy "(A Int B) Un C = (A Un C) Int (B Un C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_Int_distrib";
goal Set.thy
"(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_Int_crazy";
goal Set.thy "(A<=B) = (A Un B = B)";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
qed "subset_Un_eq";
goal Set.thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "subset_insert_iff";
goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
-by (fast_tac (eq_cs addEs [equalityCE]) 1);
+by (fast_tac (!claset addEs [equalityCE]) 1);
qed "Un_empty";
Addsimps[Un_empty];
section "Compl";
goal Set.thy "A Int Compl(A) = {}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Compl_disjoint";
Addsimps[Compl_disjoint];
goal Set.thy "A Un Compl(A) = UNIV";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Compl_partition";
goal Set.thy "Compl(Compl(A)) = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "double_complement";
Addsimps[double_complement];
goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Compl_Un";
goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Compl_Int";
goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Compl_UN";
goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
-by (fast_tac eq_cs 1);
+by (Fast_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)";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
qed "Un_Int_assoc_eq";
section "Union";
goal Set.thy "Union({}) = {}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Union_empty";
Addsimps[Union_empty];
goal Set.thy "Union(UNIV) = UNIV";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Union_UNIV";
Addsimps[Union_UNIV];
goal Set.thy "Union(insert a B) = a Un Union(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Union_insert";
Addsimps[Union_insert];
goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Union_Un_distrib";
Addsimps[Union_Un_distrib];
goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "Union_Int_subset";
val prems = goal Set.thy
"(Union(C) Int A = {}) = (! B:C. B Int A = {})";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
qed "Union_disjoint";
section "Inter";
goal Set.thy "Inter({}) = UNIV";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Inter_empty";
Addsimps[Inter_empty];
goal Set.thy "Inter(UNIV) = {}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Inter_UNIV";
Addsimps[Inter_UNIV];
goal Set.thy "Inter(insert a B) = a Int Inter(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Inter_insert";
Addsimps[Inter_insert];
goal Set.thy "Inter(A) Un Inter(B) <= Inter(A Int B)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "Inter_Un_subset";
goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
@@ -316,97 +318,97 @@
(*Basic identities*)
goal Set.thy "(UN x:{}. B x) = {}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "UN_empty";
Addsimps[UN_empty];
goal Set.thy "(UN x:UNIV. B x) = (UN x. B x)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "UN_UNIV";
Addsimps[UN_UNIV];
goal Set.thy "(INT x:{}. B x) = UNIV";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "INT_empty";
Addsimps[INT_empty];
goal Set.thy "(INT x:UNIV. B x) = (INT x. B x)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "INT_UNIV";
Addsimps[INT_UNIV];
goal Set.thy "(UN x:insert a A. B x) = B a Un UNION A B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "UN_insert";
Addsimps[UN_insert];
goal Set.thy "(INT x:insert a A. B x) = B a Int INTER A B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "INT_insert";
Addsimps[INT_insert];
goal Set.thy "Union(range(f)) = (UN x.f(x))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Union_range_eq";
goal Set.thy "Inter(range(f)) = (INT x.f(x))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Inter_range_eq";
goal Set.thy "Union(B``A) = (UN x:A. B(x))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Union_image_eq";
goal Set.thy "Inter(B``A) = (INT x:A. B(x))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Inter_image_eq";
goal Set.thy "!!A. a: A ==> (UN y:A. c) = c";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "UN_constant";
goal Set.thy "!!A. a: A ==> (INT y:A. c) = c";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "INT_constant";
goal Set.thy "(UN x.B) = B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "UN1_constant";
Addsimps[UN1_constant];
goal Set.thy "(INT x.B) = B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "INT1_constant";
Addsimps[INT1_constant];
goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
-by (fast_tac eq_cs 1);
+by (Fast_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)})";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "INT_eq";
(*Distributive laws...*)
goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_Union";
(* Devlin, Fundamentals 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)";
-by (fast_tac eq_cs 1);
+by (Fast_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))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "UN_Un_distrib";
goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_Inter";
goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
@@ -415,98 +417,98 @@
(*Equivalent version*)
goal Set.thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
-by (fast_tac eq_cs 1);
+by (Fast_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))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_UN_distrib";
goal Set.thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_INT_distrib";
goal Set.thy
"(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Int_UN_distrib2";
goal Set.thy
"(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Un_INT_distrib2";
section "-";
goal Set.thy "A-A = {}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_cancel";
Addsimps[Diff_cancel];
goal Set.thy "{}-A = {}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "empty_Diff";
Addsimps[empty_Diff];
goal Set.thy "A-{} = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_empty";
Addsimps[Diff_empty];
goal Set.thy "A-UNIV = {}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_UNIV";
Addsimps[Diff_UNIV];
goal Set.thy "!!x. x~:A ==> A - insert x B = A-B";
-by (fast_tac eq_cs 1);
+by (Fast_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}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_insert";
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
goal Set.thy "A - insert a B = A - {a} - B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_insert2";
goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "insert_Diff_if";
goal Set.thy "!!x. x:B ==> insert x A - B = A-B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "insert_Diff1";
Addsimps [insert_Diff1];
val prems = goal Set.thy "a:A ==> insert a (A-{a}) = A";
-by (fast_tac (eq_cs addSIs prems) 1);
+by (fast_tac (!claset addSIs prems) 1);
qed "insert_Diff";
goal Set.thy "A Int (B-A) = {}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_disjoint";
Addsimps[Diff_disjoint];
goal Set.thy "!!A. A<=B ==> A Un (B-A) = B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_partition";
goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "double_diff";
goal Set.thy "A - (B Un C) = (A-B) Int (A-C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_Un";
goal Set.thy "A - (B Int C) = (A-B) Un (A-C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "Diff_Int";
Addsimps[subset_UNIV, empty_subsetI, subset_refl];