src/HOL/List.ML
changeset 10709 7a29b71d6352
parent 10385 22836e4c5f4e
child 10832 e33b47e4246d
     1.1 --- a/src/HOL/List.ML	Wed Dec 20 11:54:58 2000 +0100
     1.2 +++ b/src/HOL/List.ML	Wed Dec 20 12:13:59 2000 +0100
     1.3 @@ -89,12 +89,6 @@
     1.4  qed "length_0_conv";
     1.5  AddIffs [length_0_conv];
     1.6  
     1.7 -Goal "(0 = length xs) = (xs = [])";
     1.8 -by (induct_tac "xs" 1);
     1.9 -by Auto_tac;
    1.10 -qed "zero_length_conv";
    1.11 -AddIffs [zero_length_conv];
    1.12 -
    1.13  Goal "(0 < length xs) = (xs ~= [])";
    1.14  by (induct_tac "xs" 1);
    1.15  by Auto_tac;
    1.16 @@ -1100,7 +1094,8 @@
    1.17  by (rtac iffI 1);
    1.18   by (res_inst_tac [("x","take (length xs) zs")] exI 1);
    1.19   by (res_inst_tac [("x","drop (length xs) zs")] exI 1);
    1.20 - by (asm_full_simp_tac (simpset() addsimps [min_def,eq_sym_conv]) 1);
    1.21 + by (force_tac (claset(),
    1.22 +		simpset() addsplits [nat_diff_split] addsimps [min_def]) 1);
    1.23  by (Clarify_tac 1);
    1.24  by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
    1.25  qed "list_all2_append1";
    1.26 @@ -1113,7 +1108,8 @@
    1.27  by (rtac iffI 1);
    1.28   by (res_inst_tac [("x","take (length ys) xs")] exI 1);
    1.29   by (res_inst_tac [("x","drop (length ys) xs")] exI 1);
    1.30 - by (asm_full_simp_tac (simpset() addsimps [min_def,eq_sym_conv]) 1);
    1.31 + by (force_tac (claset(),
    1.32 +		simpset() addsplits [nat_diff_split] addsimps [min_def]) 1);
    1.33  by (Clarify_tac 1);
    1.34  by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
    1.35  qed "list_all2_append2";
    1.36 @@ -1409,8 +1405,7 @@
    1.37  qed "wf_lexico";
    1.38  AddSIs [wf_lexico];
    1.39  
    1.40 -Goalw
    1.41 - [lexico_def,diag_def,lex_prod_def,measure_def,inv_image_def]
    1.42 +Goalw [lexico_def,diag_def,lex_prod_def,measure_def,inv_image_def]
    1.43  "lexico r = {(xs,ys). length xs < length ys | \
    1.44  \                     length xs = length ys & (xs,ys) : lex r}";
    1.45  by (Simp_tac 1);
    1.46 @@ -1431,7 +1426,7 @@
    1.47  by (simp_tac (simpset() addsimps [lex_conv]) 1);
    1.48  by (rtac iffI 1);
    1.49   by (blast_tac (claset() addIs [Cons_eq_appendI]) 2);
    1.50 -by (REPEAT(eresolve_tac [conjE, exE] 1));
    1.51 +by (Clarify_tac 1);
    1.52  by (case_tac "xys" 1);
    1.53  by (Asm_full_simp_tac 1);
    1.54  by (Asm_full_simp_tac 1);
    1.55 @@ -1492,8 +1487,7 @@
    1.56  (*** Versions of some theorems above using binary numerals ***)
    1.57  
    1.58  AddIffs (map rename_numerals
    1.59 -	  [length_0_conv, zero_length_conv, length_greater_0_conv,
    1.60 -	   sum_eq_0_conv]);
    1.61 +	  [length_0_conv, length_greater_0_conv, sum_eq_0_conv]);
    1.62  
    1.63  Goal "take n (x#xs) = (if n = #0 then [] else x # take (n-#1) xs)";
    1.64  by (case_tac "n" 1);