src/HOL/List.ML
changeset 962 136308504cd9
parent 923 ff1574a81019
child 974 68d58134fad6
equal deleted inserted replaced
961:932784dfa671 962:136308504cd9
    34    mem_Nil, mem_Cons,
    34    mem_Nil, mem_Cons,
    35    append_Nil, append_Cons,
    35    append_Nil, append_Cons,
    36    map_Nil, map_Cons,
    36    map_Nil, map_Cons,
    37    flat_Nil, flat_Cons,
    37    flat_Nil, flat_Cons,
    38    list_all_Nil, list_all_Cons,
    38    list_all_Nil, list_all_Cons,
    39    filter_Nil, filter_Cons];
    39    filter_Nil, filter_Cons,
       
    40    length_Nil, length_Cons];
    40 
    41 
    41 
    42 
    42 (** @ - append **)
    43 (** @ - append **)
    43 
    44 
    44 goal List.thy "(xs@ys)@zs = xs@(ys@zs)";
    45 goal List.thy "(xs@ys)@zs = xs@(ys@zs)";
   115 goal List.thy  "flat(xs@ys) = flat(xs)@flat(ys)";
   116 goal List.thy  "flat(xs@ys) = flat(xs)@flat(ys)";
   116 by (list.induct_tac "xs" 1);
   117 by (list.induct_tac "xs" 1);
   117 by(ALLGOALS(asm_simp_tac (list_ss addsimps [append_assoc])));
   118 by(ALLGOALS(asm_simp_tac (list_ss addsimps [append_assoc])));
   118 qed"flat_append";
   119 qed"flat_append";
   119 
   120 
       
   121 (** length **)
       
   122 
       
   123 goal List.thy "length(xs@ys) = length(xs)+length(ys)";
       
   124 by (list.induct_tac "xs" 1);
       
   125 by(ALLGOALS(asm_simp_tac list_ss));
       
   126 qed"length_append";
       
   127 
   120 (** nth **)
   128 (** nth **)
   121 
   129 
   122 val [nth_0,nth_Suc] = nat_recs nth_def; 
   130 val [nth_0,nth_Suc] = nat_recs nth_def; 
   123 store_thm("nth_0",nth_0);
   131 store_thm("nth_0",nth_0);
   124 store_thm("nth_Suc",nth_Suc);
   132 store_thm("nth_Suc",nth_Suc);
   142 
   150 
   143 val list_ss = list_ss addsimps
   151 val list_ss = list_ss addsimps
   144   [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq,
   152   [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq,
   145    mem_append, mem_filter,
   153    mem_append, mem_filter,
   146    map_ident, map_append, map_compose,
   154    map_ident, map_append, map_compose,
   147    flat_append, list_all_True, list_all_conj, nth_0, nth_Suc];
   155    flat_append, length_append, list_all_True, list_all_conj, nth_0, nth_Suc];
   148 
   156