1.1 --- a/src/HOL/List.thy	Fri Feb 15 16:53:39 2013 +0100
     1.2 +++ b/src/HOL/List.thy	Sat Feb 16 15:27:10 2013 +0100
     1.3 @@ -3077,15 +3077,13 @@
     1.4  
     1.5  subsubsection {* @{text upto}: interval-list on @{typ int} *}
     1.6  
     1.7 -(* FIXME make upto tail recursive? *)
     1.8 -
     1.9  function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where
    1.10 -"upto i j = (if i \<le> j then i # [i+1..j] else [])"
    1.11 +  "upto i j = (if i \<le> j then i # [i+1..j] else [])"
    1.12  by auto
    1.13  termination
    1.14  by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
    1.15  
    1.16 -declare upto.simps[code, simp del]
    1.17 +declare upto.simps[simp del]
    1.18  
    1.19  lemmas upto_rec_numeral [simp] =
    1.20    upto.simps[of "numeral m" "numeral n"]
    1.21 @@ -3096,6 +3094,18 @@
    1.22  lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
    1.23  by(simp add: upto.simps)
    1.24  
    1.25 +lemma upto_rec1: "i \<le> j \<Longrightarrow> [i..j] = i#[i+1..j]"
    1.26 +by(simp add: upto.simps)
    1.27 +
    1.28 +lemma upto_rec2: "i \<le> j \<Longrightarrow> [i..j] = [i..j - 1]@[j]"
    1.29 +proof(induct "nat(j-i)" arbitrary: i j)
    1.30 +  case 0 thus ?case by(simp add: upto.simps)
    1.31 +next
    1.32 +  case (Suc n)
    1.33 +  hence "n = nat (j - (i + 1))" "i < j" by linarith+
    1.34 +  from this(2) Suc.hyps(1)[OF this(1)] Suc(2,3) upto_rec1 show ?case by simp
    1.35 +qed
    1.36 +
    1.37  lemma set_upto[simp]: "set[i..j] = {i..j}"
    1.38  proof(induct i j rule:upto.induct)
    1.39    case (1 i j)
    1.40 @@ -3103,6 +3113,29 @@
    1.41      unfolding upto.simps[of i j] simp_from_to[of i j] by auto
    1.42  qed
    1.43  
    1.44 +text{* Tail recursive version for code generation: *}
    1.45 +
    1.46 +function upto_aux :: "int \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
    1.47 +  "upto_aux i j js = (if j<i then js else upto_aux i (j - 1) (j#js))"
    1.48 +by auto
    1.49 +termination by(relation "measure(%(i::int,j,js). nat(j - i + 1))") auto
    1.50 +
    1.51 +lemma upto_aux_upto: "upto_aux i j js = [i..j] @ js"
    1.52 +proof cases
    1.53 +  assume "j < i" thus ?thesis by(simp)
    1.54 +next
    1.55 +  assume "\<not> j < i"
    1.56 +  thus ?thesis
    1.57 +  proof(induct i j js rule: upto_aux.induct)
    1.58 +     case 1 thus ?case using upto_rec2 by simp
    1.59 +  qed
    1.60 +qed
    1.61 +
    1.62 +declare upto_aux.simps[simp del]
    1.63 +
    1.64 +lemma upto_code[code]: "[i..j] = upto_aux i j []"
    1.65 +by(simp add: upto_aux_upto)
    1.66 +
    1.67  
    1.68  subsubsection {* @{const distinct} and @{const remdups} *}
    1.69