added length_Suc_conv, finite_set
authoroheimb
Wed Aug 12 15:29:34 1998 +0200 (1998-08-12)
changeset 5296bdef7d349d27
parent 5295 25fb5156e0d9
child 5297 410417e0fd04
added length_Suc_conv, finite_set
src/HOL/List.ML
     1.1 --- a/src/HOL/List.ML	Wed Aug 12 15:22:14 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Wed Aug 12 15:29:34 1998 +0200
     1.3 @@ -111,6 +111,12 @@
     1.4  qed "length_greater_0_conv";
     1.5  AddIffs [length_greater_0_conv];
     1.6  
     1.7 +Goal "(length xs = Suc n) = (? y ys. xs = y#ys & length ys = n)";
     1.8 +by (induct_tac "xs" 1);
     1.9 +by (Auto_tac);
    1.10 +qed "length_Suc_conv";
    1.11 +AddIffs [length_Suc_conv];
    1.12 +
    1.13  (** @ - append **)
    1.14  
    1.15  section "@ - append";
    1.16 @@ -160,8 +166,9 @@
    1.17                        addEs [less_not_refl2 RSN (2,rev_notE)]) 1);
    1.18  by (rtac allI 1);
    1.19  by (exhaust_tac "ys" 1);
    1.20 - by (fast_tac (claset() addIs [less_add_Suc2] addss simpset()
    1.21 -                      addEs [(less_not_refl2 RS not_sym) RSN (2,rev_notE)]) 1);
    1.22 +by (fast_tac (claset() addIs [less_add_Suc2] 
    1.23 +		       addss (simpset() delsimps [length_Suc_conv])
    1.24 +                       addEs [(less_not_refl2 RS not_sym) RSN (2,rev_notE)]) 1);
    1.25  by (Asm_simp_tac 1);
    1.26  qed_spec_mp "append_eq_append_conv";
    1.27  Addsimps [append_eq_append_conv];
    1.28 @@ -359,6 +366,11 @@
    1.29  
    1.30  section "set";
    1.31  
    1.32 +qed_goal "finite_set" thy "finite (set xs)" 
    1.33 +	(K [induct_tac "xs" 1, Auto_tac]);
    1.34 +Addsimps[finite_set];
    1.35 +AddSIs[finite_set];
    1.36 +
    1.37  Goal "set (xs@ys) = (set xs Un set ys)";
    1.38  by (induct_tac "xs" 1);
    1.39  by (Auto_tac);
    1.40 @@ -885,14 +897,15 @@
    1.41  by(induct_tac "n" 1);
    1.42   by(Simp_tac 1);
    1.43   by(Blast_tac 1);
    1.44 -by(asm_full_simp_tac (simpset() addsimps [lex_prod_def]) 1);
    1.45 -by(Auto_tac);
    1.46 +by(asm_full_simp_tac (simpset() delsimps [length_Suc_conv] 
    1.47 +				addsimps [lex_prod_def]) 1);
    1.48 +by(auto_tac (claset(), simpset() delsimps [length_Suc_conv]));
    1.49    by(Blast_tac 1);
    1.50   by(rename_tac "a xys x xs' y ys'" 1);
    1.51   by(res_inst_tac [("x","a#xys")] exI 1);
    1.52   by(Simp_tac 1);
    1.53  by(exhaust_tac "xys" 1);
    1.54 - by(ALLGOALS Asm_full_simp_tac);
    1.55 + by(ALLGOALS (asm_full_simp_tac (simpset() delsimps [length_Suc_conv])));
    1.56  by(Blast_tac 1);
    1.57  qed "lexn_conv";
    1.58  
    1.59 @@ -900,7 +913,7 @@
    1.60   "lex r = \
    1.61  \ {(xs,ys). length xs = length ys & \
    1.62  \           (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
    1.63 -by(force_tac (claset(), simpset() addsimps [lexn_conv]) 1);
    1.64 +by(force_tac (claset(), simpset() delsimps [length_Suc_conv] addsimps [lexn_conv]) 1);
    1.65  qed "lex_conv";
    1.66  
    1.67  Goalw [lexico_def] "wf r ==> wf(lexico r)";