tail-recursive implementation for length
authorAndreas Lochbihler
Wed Oct 10 15:16:44 2012 +0200 (2012-10-10)
changeset 49808418991ce7567
parent 49807 9a0843995fd3
child 49809 39db47ed6d54
tail-recursive implementation for length
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Wed Oct 10 15:05:07 2012 +0200
     1.2 +++ b/src/HOL/List.thy	Wed Oct 10 15:16:44 2012 +0200
     1.3 @@ -5514,8 +5514,22 @@
     1.4    "list_ex P [i..j] \<longleftrightarrow> \<not> (all_interval_int (Not \<circ> P) i j)"
     1.5    by (simp add: list_ex_iff all_interval_int_def)
     1.6  
     1.7 -hide_const (open) member null maps map_filter all_interval_nat all_interval_int
     1.8 -
     1.9 +text {* optimized code (tail-recursive) for @{term length} *}
    1.10 +
    1.11 +definition gen_length :: "nat \<Rightarrow> 'a list \<Rightarrow> nat"
    1.12 +where "gen_length n xs = n + length xs"
    1.13 +
    1.14 +lemma gen_length_code [code]:
    1.15 +  "gen_length n [] = n"
    1.16 +  "gen_length n (x # xs) = gen_length (Suc n) xs"
    1.17 +by(simp_all add: gen_length_def)
    1.18 +
    1.19 +declare list.size(3-4)[code del]
    1.20 +
    1.21 +lemma length_code [code]: "length = gen_length 0"
    1.22 +by(simp add: gen_length_def fun_eq_iff)
    1.23 +
    1.24 +hide_const (open) member null maps map_filter all_interval_nat all_interval_int gen_length
    1.25  
    1.26  subsubsection {* Pretty lists *}
    1.27