src/HOL/Finite.ML
changeset 4089 96fba19bcbe2
parent 4059 59c1422c9da5
child 4153 e534c4c32d54
     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);