# HG changeset patch
# User Andreas Lochbihler
# Date 1349875004 -7200
# Node ID 418991ce7567f4f59113888d5c93a477f5e1542d
# Parent  9a0843995fd3b3e463c502baa624e9da7aa4603d
tail-recursive implementation for length

diff -r 9a0843995fd3 -r 418991ce7567 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Oct 10 15:05:07 2012 +0200
+++ b/src/HOL/List.thy	Wed Oct 10 15:16:44 2012 +0200
@@ -5514,8 +5514,22 @@
   "list_ex P [i..j] \<longleftrightarrow> \<not> (all_interval_int (Not \<circ> P) i j)"
   by (simp add: list_ex_iff all_interval_int_def)
 
-hide_const (open) member null maps map_filter all_interval_nat all_interval_int
-
+text {* optimized code (tail-recursive) for @{term length} *}
+
+definition gen_length :: "nat \<Rightarrow> 'a list \<Rightarrow> nat"
+where "gen_length n xs = n + length xs"
+
+lemma gen_length_code [code]:
+  "gen_length n [] = n"
+  "gen_length n (x # xs) = gen_length (Suc n) xs"
+by(simp_all add: gen_length_def)
+
+declare list.size(3-4)[code del]
+
+lemma length_code [code]: "length = gen_length 0"
+by(simp add: gen_length_def fun_eq_iff)
+
+hide_const (open) member null maps map_filter all_interval_nat all_interval_int gen_length
 
 subsubsection {* Pretty lists *}