Added a few thms to nat_ss and list_ss
authornipkow
Fri Mar 17 15:49:37 1995 +0100 (1995-03-17)
changeset 962136308504cd9
parent 961 932784dfa671
child 963 7a78fda77104
Added a few thms to nat_ss and list_ss
src/HOL/List.ML
src/HOL/Nat.ML
     1.1 --- a/src/HOL/List.ML	Fri Mar 17 15:35:09 1995 +0100
     1.2 +++ b/src/HOL/List.ML	Fri Mar 17 15:49:37 1995 +0100
     1.3 @@ -36,7 +36,8 @@
     1.4     map_Nil, map_Cons,
     1.5     flat_Nil, flat_Cons,
     1.6     list_all_Nil, list_all_Cons,
     1.7 -   filter_Nil, filter_Cons];
     1.8 +   filter_Nil, filter_Cons,
     1.9 +   length_Nil, length_Cons];
    1.10  
    1.11  
    1.12  (** @ - append **)
    1.13 @@ -117,6 +118,13 @@
    1.14  by(ALLGOALS(asm_simp_tac (list_ss addsimps [append_assoc])));
    1.15  qed"flat_append";
    1.16  
    1.17 +(** length **)
    1.18 +
    1.19 +goal List.thy "length(xs@ys) = length(xs)+length(ys)";
    1.20 +by (list.induct_tac "xs" 1);
    1.21 +by(ALLGOALS(asm_simp_tac list_ss));
    1.22 +qed"length_append";
    1.23 +
    1.24  (** nth **)
    1.25  
    1.26  val [nth_0,nth_Suc] = nat_recs nth_def; 
    1.27 @@ -144,5 +152,5 @@
    1.28    [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq,
    1.29     mem_append, mem_filter,
    1.30     map_ident, map_append, map_compose,
    1.31 -   flat_append, list_all_True, list_all_conj, nth_0, nth_Suc];
    1.32 +   flat_append, length_append, list_all_True, list_all_conj, nth_0, nth_Suc];
    1.33  
     2.1 --- a/src/HOL/Nat.ML	Fri Mar 17 15:35:09 1995 +0100
     2.2 +++ b/src/HOL/Nat.ML	Fri Mar 17 15:49:37 1995 +0100
     2.3 @@ -433,4 +433,4 @@
     2.4  by (simp_tac (nat_ss0 addsimps [le_eq_less_or_eq]) 1);
     2.5  qed "Suc_le_mono";
     2.6  
     2.7 -val nat_ss = nat_ss0 addsimps [le_refl];
     2.8 +val nat_ss = nat_ss0 addsimps [le_refl,Suc_le_mono];