# HG changeset patch # User haftmann # Date 1361095570 -3600 # Node ID bf18bf4922ead40a1345d1a950f1f0cf35829dbb # Parent 55644f8caeb3c9aa3fba802e2afd6481ea9af299# Parent 35d00ce5862615242458e895758f93ccf13d23db merged diff -r 35d00ce58626 -r bf18bf4922ea CONTRIBUTORS --- a/CONTRIBUTORS Sat Feb 16 08:21:08 2013 +0100 +++ b/CONTRIBUTORS Sun Feb 17 11:06:10 2013 +0100 @@ -6,6 +6,11 @@ Contributions to this Isabelle version -------------------------------------- +* 2013: Florian Haftmann, TUM + Reworking and consolidation of code generation for target + language numerals. + + Contributions to Isabelle2013 ----------------------------- diff -r 35d00ce58626 -r bf18bf4922ea src/HOL/List.thy --- a/src/HOL/List.thy Sat Feb 16 08:21:08 2013 +0100 +++ b/src/HOL/List.thy Sun Feb 17 11:06:10 2013 +0100 @@ -3077,15 +3077,13 @@ subsubsection {* @{text upto}: interval-list on @{typ int} *} -(* FIXME make upto tail recursive? *) - function upto :: "int \ int \ int list" ("(1[_../_])") where -"upto i j = (if i \ j then i # [i+1..j] else [])" + "upto i j = (if i \ j then i # [i+1..j] else [])" by auto termination by(relation "measure(%(i::int,j). nat(j - i + 1))") auto -declare upto.simps[code, simp del] +declare upto.simps[simp del] lemmas upto_rec_numeral [simp] = upto.simps[of "numeral m" "numeral n"] @@ -3096,6 +3094,18 @@ lemma upto_empty[simp]: "j < i \ [i..j] = []" by(simp add: upto.simps) +lemma upto_rec1: "i \ j \ [i..j] = i#[i+1..j]" +by(simp add: upto.simps) + +lemma upto_rec2: "i \ j \ [i..j] = [i..j - 1]@[j]" +proof(induct "nat(j-i)" arbitrary: i j) + case 0 thus ?case by(simp add: upto.simps) +next + case (Suc n) + hence "n = nat (j - (i + 1))" "i < j" by linarith+ + from this(2) Suc.hyps(1)[OF this(1)] Suc(2,3) upto_rec1 show ?case by simp +qed + lemma set_upto[simp]: "set[i..j] = {i..j}" proof(induct i j rule:upto.induct) case (1 i j) @@ -3103,6 +3113,29 @@ unfolding upto.simps[of i j] simp_from_to[of i j] by auto qed +text{* Tail recursive version for code generation: *} + +function upto_aux :: "int \ int \ int list \ int list" where + "upto_aux i j js = (if j j < i" + thus ?thesis + proof(induct i j js rule: upto_aux.induct) + case 1 thus ?case using upto_rec2 by simp + qed +qed + +declare upto_aux.simps[simp del] + +lemma upto_code[code]: "[i..j] = upto_aux i j []" +by(simp add: upto_aux_upto) + subsubsection {* @{const distinct} and @{const remdups} *}