# HG changeset patch # User paulson # Date 977310839 -3600 # Node ID 7a29b71d635265983c556615500da48738428f44 # Parent 1a6348a114895589e494aa50058b159891dacbcc tidying, removing obsolete lemmas about 0=... diff -r 1a6348a11489 -r 7a29b71d6352 src/HOL/List.ML --- a/src/HOL/List.ML Wed Dec 20 11:54:58 2000 +0100 +++ b/src/HOL/List.ML Wed Dec 20 12:13:59 2000 +0100 @@ -89,12 +89,6 @@ qed "length_0_conv"; AddIffs [length_0_conv]; -Goal "(0 = length xs) = (xs = [])"; -by (induct_tac "xs" 1); -by Auto_tac; -qed "zero_length_conv"; -AddIffs [zero_length_conv]; - Goal "(0 < length xs) = (xs ~= [])"; by (induct_tac "xs" 1); by Auto_tac; @@ -1100,7 +1094,8 @@ by (rtac iffI 1); by (res_inst_tac [("x","take (length xs) zs")] exI 1); by (res_inst_tac [("x","drop (length xs) zs")] exI 1); - by (asm_full_simp_tac (simpset() addsimps [min_def,eq_sym_conv]) 1); + by (force_tac (claset(), + simpset() addsplits [nat_diff_split] addsimps [min_def]) 1); by (Clarify_tac 1); by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1); qed "list_all2_append1"; @@ -1113,7 +1108,8 @@ by (rtac iffI 1); by (res_inst_tac [("x","take (length ys) xs")] exI 1); by (res_inst_tac [("x","drop (length ys) xs")] exI 1); - by (asm_full_simp_tac (simpset() addsimps [min_def,eq_sym_conv]) 1); + by (force_tac (claset(), + simpset() addsplits [nat_diff_split] addsimps [min_def]) 1); by (Clarify_tac 1); by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1); qed "list_all2_append2"; @@ -1409,8 +1405,7 @@ qed "wf_lexico"; AddSIs [wf_lexico]; -Goalw - [lexico_def,diag_def,lex_prod_def,measure_def,inv_image_def] +Goalw [lexico_def,diag_def,lex_prod_def,measure_def,inv_image_def] "lexico r = {(xs,ys). length xs < length ys | \ \ length xs = length ys & (xs,ys) : lex r}"; by (Simp_tac 1); @@ -1431,7 +1426,7 @@ by (simp_tac (simpset() addsimps [lex_conv]) 1); by (rtac iffI 1); by (blast_tac (claset() addIs [Cons_eq_appendI]) 2); -by (REPEAT(eresolve_tac [conjE, exE] 1)); +by (Clarify_tac 1); by (case_tac "xys" 1); by (Asm_full_simp_tac 1); by (Asm_full_simp_tac 1); @@ -1492,8 +1487,7 @@ (*** Versions of some theorems above using binary numerals ***) AddIffs (map rename_numerals - [length_0_conv, zero_length_conv, length_greater_0_conv, - sum_eq_0_conv]); + [length_0_conv, length_greater_0_conv, sum_eq_0_conv]); Goal "take n (x#xs) = (if n = #0 then [] else x # take (n-#1) xs)"; by (case_tac "n" 1);