src/HOL/List.thy
 changeset 51166 a019e013b7e4 parent 51160 599ff65b85e2 child 51170 b3cdcba073d5
```     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
```