src/HOL/Finite.ML
changeset 1660 8cb42cd97579
parent 1618 372880456b5b
child 1760 6f41a494f3b1
     1.1 --- a/src/HOL/Finite.ML	Wed Apr 17 11:46:10 1996 +0200
     1.2 +++ b/src/HOL/Finite.ML	Wed Apr 17 17:59:58 1996 +0200
     1.3 @@ -73,7 +73,8 @@
     1.4  by (rtac (major RS Fin_induct) 1);
     1.5  by (Simp_tac 1);
     1.6  by (asm_simp_tac
     1.7 -    (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
     1.8 +    (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]
     1.9 +	      delsimps [insert_Fin]) 1);
    1.10  qed "Fin_imageI";
    1.11  
    1.12  val major::prems = goal Finite.thy 
    1.13 @@ -181,7 +182,7 @@
    1.14  by (hyp_subst_tac 1);
    1.15  by (res_inst_tac [("x","Suc n")] exI 1);
    1.16  by (res_inst_tac [("x","%i. if i<n then f i else x")] exI 1);
    1.17 -by (asm_simp_tac (!simpset addsimps [Collect_conv_insert]
    1.18 +by (asm_simp_tac (!simpset addsimps [Collect_conv_insert, less_Suc_eq]
    1.19                            addcongs [rev_conj_cong]) 1);
    1.20  qed "finite_has_card";
    1.21  
    1.22 @@ -198,14 +199,14 @@
    1.23   by (Simp_tac 2);
    1.24   by (fast_tac eq_cs 2);
    1.25  by (etac exE 1);
    1.26 -by (Simp_tac 1);
    1.27 +by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    1.28  by (rtac exI 1);
    1.29  by (rtac conjI 1);
    1.30   br disjI2 1;
    1.31   br refl 1;
    1.32  by (etac equalityE 1);
    1.33  by (asm_full_simp_tac
    1.34 -     (!simpset addsimps [subset_insert,Collect_conv_insert]) 1);
    1.35 +     (!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
    1.36  by (SELECT_GOAL(safe_tac eq_cs)1);
    1.37    by (Asm_full_simp_tac 1);
    1.38    by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    1.39 @@ -259,7 +260,8 @@
    1.40   by (res_inst_tac
    1.41     [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
    1.42   by (simp_tac
    1.43 -    (!simpset addsimps [Collect_conv_insert] addcongs [rev_conj_cong]) 1);
    1.44 +    (!simpset addsimps [Collect_conv_insert, less_Suc_eq] 
    1.45 +	      addcongs [rev_conj_cong]) 1);
    1.46   be subst 1;
    1.47   br refl 1;
    1.48  by (rtac notI 1);
    1.49 @@ -270,7 +272,7 @@
    1.50  by (etac conjE 1);
    1.51  by (dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
    1.52  by (dtac le_less_trans 1 THEN atac 1);
    1.53 -by (Asm_full_simp_tac 1);
    1.54 +by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    1.55  by (etac disjE 1);
    1.56  by (etac less_asym 1 THEN atac 1);
    1.57  by (hyp_subst_tac 1);