1.1 --- a/src/HOL/Finite.ML Mon Nov 03 12:12:10 1997 +0100
1.2 +++ b/src/HOL/Finite.ML Mon Nov 03 12:13:18 1997 +0100
1.3 @@ -17,7 +17,7 @@
1.4 qed "Fin_mono";
1.5
1.6 goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
1.7 -by (blast_tac (!claset addSIs [lfp_lowerbound]) 1);
1.8 +by (blast_tac (claset() addSIs [lfp_lowerbound]) 1);
1.9 qed "Fin_subset_Pow";
1.10
1.11 (* A : Fin(B) ==> A <= B *)
1.12 @@ -41,7 +41,7 @@
1.13 \ !!F a. [| finite F; a:A; a ~: F; P(F) |] ==> P(insert a F) \
1.14 \ |] ==> F <= A --> P(F)";
1.15 by (rtac (major RS finite_induct) 1);
1.16 -by (ALLGOALS (blast_tac (!claset addIs prems)));
1.17 +by (ALLGOALS (blast_tac (claset() addIs prems)));
1.18 val lemma = result();
1.19
1.20 val prems = goal Finite.thy
1.21 @@ -59,7 +59,7 @@
1.22 val major::prems = goal Finite.thy
1.23 "[| finite F; finite G |] ==> finite(F Un G)";
1.24 by (rtac (major RS finite_induct) 1);
1.25 -by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
1.26 +by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
1.27 qed "finite_UnI";
1.28
1.29 (*Every subset of a finite set is finite*)
1.30 @@ -68,14 +68,14 @@
1.31 rtac mp, etac spec,
1.32 rtac subs]);
1.33 by (rtac (fin RS finite_induct) 1);
1.34 -by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
1.35 -by (safe_tac (!claset addSDs [subset_insert_iff RS iffD1]));
1.36 +by (simp_tac (simpset() addsimps [subset_Un_eq]) 1);
1.37 +by (safe_tac (claset() addSDs [subset_insert_iff RS iffD1]));
1.38 by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
1.39 by (ALLGOALS Asm_simp_tac);
1.40 qed "finite_subset";
1.41
1.42 goal Finite.thy "finite(F Un G) = (finite F & finite G)";
1.43 -by (blast_tac (!claset addIs [finite_UnI] addDs
1.44 +by (blast_tac (claset() addIs [finite_UnI] addDs
1.45 [Un_upper1 RS finite_subset, Un_upper2 RS finite_subset]) 1);
1.46 qed "finite_Un";
1.47 AddIffs[finite_Un];
1.48 @@ -102,7 +102,7 @@
1.49 by (rtac (major RS finite_induct) 1);
1.50 by (stac Diff_insert 2);
1.51 by (ALLGOALS (asm_simp_tac
1.52 - (!simpset addsimps (prems@[Diff_subset RS finite_subset]))));
1.53 + (simpset() addsimps (prems@[Diff_subset RS finite_subset]))));
1.54 val lemma = result();
1.55
1.56 val prems = goal Finite.thy
1.57 @@ -135,14 +135,14 @@
1.58 by (Clarify_tac 1);
1.59 by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
1.60 by (Clarify_tac 1);
1.61 - by (full_simp_tac (!simpset addsimps [inj_onto_def]) 1);
1.62 + by (full_simp_tac (simpset() addsimps [inj_onto_def]) 1);
1.63 by (Blast_tac 1);
1.64 by (thin_tac "ALL A. ?PP(A)" 1);
1.65 by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
1.66 by (Clarify_tac 1);
1.67 by (res_inst_tac [("x","xa")] bexI 1);
1.68 by (ALLGOALS
1.69 - (asm_full_simp_tac (!simpset addsimps [inj_onto_image_set_diff])));
1.70 + (asm_full_simp_tac (simpset() addsimps [inj_onto_image_set_diff])));
1.71 val lemma = result();
1.72
1.73 goal Finite.thy "!!A. [| finite(f``A); inj_onto f A |] ==> finite A";
1.74 @@ -163,7 +163,7 @@
1.75
1.76 goalw Finite.thy [Sigma_def]
1.77 "!!A. [| finite A; !a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)";
1.78 -by(blast_tac (!claset addSIs [finite_UnionI]) 1);
1.79 +by(blast_tac (claset() addSIs [finite_UnionI]) 1);
1.80 bind_thm("finite_SigmaI", ballI RSN (2,result()));
1.81 Addsimps [finite_SigmaI];
1.82
1.83 @@ -174,7 +174,7 @@
1.84 by (rtac finite_subset 2);
1.85 by (assume_tac 3);
1.86 by (ALLGOALS
1.87 - (fast_tac (!claset addSDs [rewrite_rule [inj_onto_def] finite_imageD])));
1.88 + (fast_tac (claset() addSDs [rewrite_rule [inj_onto_def] finite_imageD])));
1.89 val lemma = result();
1.90
1.91 goal Finite.thy "finite(Pow A) = finite A";
1.92 @@ -184,7 +184,7 @@
1.93 by (etac finite_induct 1);
1.94 by (ALLGOALS
1.95 (asm_simp_tac
1.96 - (!simpset addsimps [finite_UnI, finite_imageI, Pow_insert])));
1.97 + (simpset() addsimps [finite_UnI, finite_imageI, Pow_insert])));
1.98 qed "finite_Pow_iff";
1.99 AddIffs [finite_Pow_iff];
1.100
1.101 @@ -193,9 +193,9 @@
1.102 by (Asm_simp_tac 1);
1.103 by (rtac iffI 1);
1.104 by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
1.105 - by (simp_tac (!simpset addsplits [expand_split]) 1);
1.106 + by (simp_tac (simpset() addsplits [expand_split]) 1);
1.107 by (etac finite_imageI 1);
1.108 -by (simp_tac (!simpset addsimps [inverse_def,image_def]) 1);
1.109 +by (simp_tac (simpset() addsimps [inverse_def,image_def]) 1);
1.110 by (Auto_tac());
1.111 by (rtac bexI 1);
1.112 by (assume_tac 2);
1.113 @@ -227,7 +227,7 @@
1.114 by (hyp_subst_tac 1);
1.115 by (res_inst_tac [("x","Suc n")] exI 1);
1.116 by (res_inst_tac [("x","%i. if i<n then f i else x")] exI 1);
1.117 -by (asm_simp_tac (!simpset addsimps [Collect_conv_insert, less_Suc_eq]
1.118 +by (asm_simp_tac (simpset() addsimps [Collect_conv_insert, less_Suc_eq]
1.119 addcongs [rev_conj_cong]) 1);
1.120 qed "finite_has_card";
1.121
1.122 @@ -244,41 +244,41 @@
1.123 by (Simp_tac 2);
1.124 by (Blast_tac 2);
1.125 by (etac exE 1);
1.126 -by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
1.127 +by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
1.128 by (rtac exI 1);
1.129 by (rtac (refl RS disjI2 RS conjI) 1);
1.130 by (etac equalityE 1);
1.131 by (asm_full_simp_tac
1.132 - (!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
1.133 -by (safe_tac (!claset));
1.134 + (simpset() addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
1.135 +by (safe_tac (claset()));
1.136 by (Asm_full_simp_tac 1);
1.137 by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
1.138 - by (SELECT_GOAL(safe_tac (!claset))1);
1.139 + by (SELECT_GOAL(safe_tac (claset()))1);
1.140 by (subgoal_tac "x ~= f m" 1);
1.141 by (Blast_tac 2);
1.142 by (subgoal_tac "? k. f k = x & k<m" 1);
1.143 by (Blast_tac 2);
1.144 - by (SELECT_GOAL(safe_tac (!claset))1);
1.145 + by (SELECT_GOAL(safe_tac (claset()))1);
1.146 by (res_inst_tac [("x","k")] exI 1);
1.147 by (Asm_simp_tac 1);
1.148 - by (simp_tac (!simpset addsplits [expand_if]) 1);
1.149 + by (simp_tac (simpset() addsplits [expand_if]) 1);
1.150 by (Blast_tac 1);
1.151 by (dtac sym 1);
1.152 by (rotate_tac ~1 1);
1.153 by (Asm_full_simp_tac 1);
1.154 by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
1.155 - by (SELECT_GOAL(safe_tac (!claset))1);
1.156 + by (SELECT_GOAL(safe_tac (claset()))1);
1.157 by (subgoal_tac "x ~= f m" 1);
1.158 by (Blast_tac 2);
1.159 by (subgoal_tac "? k. f k = x & k<m" 1);
1.160 by (Blast_tac 2);
1.161 - by (SELECT_GOAL(safe_tac (!claset))1);
1.162 + by (SELECT_GOAL(safe_tac (claset()))1);
1.163 by (res_inst_tac [("x","k")] exI 1);
1.164 by (Asm_simp_tac 1);
1.165 - by (simp_tac (!simpset addsplits [expand_if]) 1);
1.166 + by (simp_tac (simpset() addsplits [expand_if]) 1);
1.167 by (Blast_tac 1);
1.168 by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
1.169 -by (SELECT_GOAL(safe_tac (!claset))1);
1.170 +by (SELECT_GOAL(safe_tac (claset()))1);
1.171 by (subgoal_tac "x ~= f i" 1);
1.172 by (Blast_tac 2);
1.173 by (case_tac "x = f m" 1);
1.174 @@ -286,10 +286,10 @@
1.175 by (Asm_simp_tac 1);
1.176 by (subgoal_tac "? k. f k = x & k<m" 1);
1.177 by (Blast_tac 2);
1.178 - by (SELECT_GOAL(safe_tac (!claset))1);
1.179 + by (SELECT_GOAL(safe_tac (claset()))1);
1.180 by (res_inst_tac [("x","k")] exI 1);
1.181 by (Asm_simp_tac 1);
1.182 -by (simp_tac (!simpset addsplits [expand_if]) 1);
1.183 +by (simp_tac (simpset() addsplits [expand_if]) 1);
1.184 by (Blast_tac 1);
1.185 val lemma = result();
1.186
1.187 @@ -303,7 +303,7 @@
1.188 by (res_inst_tac
1.189 [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
1.190 by (simp_tac
1.191 - (!simpset addsimps [Collect_conv_insert, less_Suc_eq]
1.192 + (simpset() addsimps [Collect_conv_insert, less_Suc_eq]
1.193 addcongs [rev_conj_cong]) 1);
1.194 by (etac subst 1);
1.195 by (rtac refl 1);
1.196 @@ -315,7 +315,7 @@
1.197 by (etac conjE 1);
1.198 by (dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
1.199 by (dtac le_less_trans 1 THEN atac 1);
1.200 -by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
1.201 +by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
1.202 by (etac disjE 1);
1.203 by (etac less_asym 1 THEN atac 1);
1.204 by (hyp_subst_tac 1);
1.205 @@ -335,18 +335,18 @@
1.206 by (Clarify_tac 1);
1.207 by (case_tac "x:B" 1);
1.208 by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
1.209 - by (SELECT_GOAL(safe_tac (!claset))1);
1.210 + by (SELECT_GOAL(safe_tac (claset()))1);
1.211 by (rotate_tac ~1 1);
1.212 - by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
1.213 + by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
1.214 by (rotate_tac ~1 1);
1.215 -by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
1.216 +by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
1.217 qed_spec_mp "card_mono";
1.218
1.219 goal Finite.thy "!!A B. [| finite A; finite B |]\
1.220 \ ==> A Int B = {} --> card(A Un B) = card A + card B";
1.221 by (etac finite_induct 1);
1.222 by (ALLGOALS
1.223 - (asm_simp_tac (!simpset addsimps [Int_insert_left]
1.224 + (asm_simp_tac (simpset() addsimps [Int_insert_left]
1.225 addsplits [expand_if])));
1.226 qed_spec_mp "card_Un_disjoint";
1.227
1.228 @@ -359,7 +359,7 @@
1.229 by (Blast_tac 3);
1.230 by (ALLGOALS
1.231 (asm_simp_tac
1.232 - (!simpset addsimps [add_commute, not_less_iff_le,
1.233 + (simpset() addsimps [add_commute, not_less_iff_le,
1.234 add_diff_inverse, card_mono, finite_subset])));
1.235 qed "card_Diff_subset";
1.236
1.237 @@ -371,7 +371,7 @@
1.238
1.239 goal Finite.thy "!!A. [| finite A; x: A |] ==> card(A-{x}) < card A";
1.240 by (rtac Suc_less_SucD 1);
1.241 -by (asm_simp_tac (!simpset addsimps [card_Suc_Diff]) 1);
1.242 +by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
1.243 qed "card_Diff";
1.244
1.245
1.246 @@ -380,7 +380,7 @@
1.247 val [major] = goal Finite.thy
1.248 "finite A ==> card(insert x A) = Suc(card(A-{x}))";
1.249 by (case_tac "x:A" 1);
1.250 -by (asm_simp_tac (!simpset addsimps [insert_absorb]) 1);
1.251 +by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
1.252 by (dtac mk_disjoint_insert 1);
1.253 by (etac exE 1);
1.254 by (Asm_simp_tac 1);
1.255 @@ -388,7 +388,7 @@
1.256 by (rtac (major RSN (2,finite_subset)) 1);
1.257 by (Blast_tac 1);
1.258 by (Blast_tac 1);
1.259 -by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
1.260 +by (asm_simp_tac (simpset() addsimps [major RS card_insert_disjoint]) 1);
1.261 qed "card_insert";
1.262 Addsimps [card_insert];
1.263
1.264 @@ -406,13 +406,13 @@
1.265
1.266 goal thy "!!A. finite A ==> card (Pow A) = 2 ^ card A";
1.267 by (etac finite_induct 1);
1.268 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [Pow_insert])));
1.269 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert])));
1.270 by (stac card_Un_disjoint 1);
1.271 -by (EVERY (map (blast_tac (!claset addIs [finite_imageI])) [3,2,1]));
1.272 +by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1]));
1.273 by (subgoal_tac "inj_onto (insert x) (Pow F)" 1);
1.274 -by (asm_simp_tac (!simpset addsimps [card_image, Pow_insert]) 1);
1.275 +by (asm_simp_tac (simpset() addsimps [card_image, Pow_insert]) 1);
1.276 by (rewtac inj_onto_def);
1.277 -by (blast_tac (!claset addSEs [equalityE]) 1);
1.278 +by (blast_tac (claset() addSEs [equalityE]) 1);
1.279 qed "card_Pow";
1.280 Addsimps [card_Pow];
1.281
1.282 @@ -430,12 +430,12 @@
1.283 by (etac conjE 1);
1.284 by (hyp_subst_tac 1);
1.285 by (rotate_tac ~1 1);
1.286 -by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
1.287 +by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
1.288 by (Blast_tac 1);
1.289 (*2*)
1.290 by (rotate_tac ~1 1);
1.291 by (eres_inst_tac [("P","?a<?b")] notE 1);
1.292 -by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
1.293 +by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
1.294 by (case_tac "A=F" 1);
1.295 by (ALLGOALS Asm_simp_tac);
1.296 qed_spec_mp "psubset_card" ;
1.297 @@ -452,7 +452,7 @@
1.298 by (Clarify_tac 1);
1.299 by (stac card_Un_disjoint 1);
1.300 by (ALLGOALS
1.301 - (asm_full_simp_tac (!simpset
1.302 + (asm_full_simp_tac (simpset()
1.303 addsimps [dvd_add, disjoint_eq_subset_Compl])));
1.304 by (thin_tac "!c:F. ?PP(c)" 1);
1.305 by (thin_tac "!c:F. ?PP(c) & ?QQ(c)" 1);