# HG changeset patch
# User haftmann
# Date 1361097280 -3600
# Node ID b3cdcba073d58141490cf1f14178f81992092dcd
# Parent  bf18bf4922ead40a1345d1a950f1f0cf35829dbb
simplified construction of upto_aux

diff -r bf18bf4922ea -r b3cdcba073d5 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Feb 17 11:06:10 2013 +0100
+++ b/src/HOL/List.thy	Sun Feb 17 11:34:40 2013 +0100
@@ -3115,26 +3115,15 @@
 
 text{* Tail recursive version for code generation: *}
 
-function upto_aux :: "int \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
+definition upto_aux :: "int \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
+  "upto_aux i j js = [i..j] @ js"
+
+lemma upto_aux_rec [code]:
   "upto_aux i j js = (if j<i then js else upto_aux i (j - 1) (j#js))"
-by auto
-termination by(relation "measure(%(i::int,j,js). nat(j - i + 1))") auto
-
-lemma upto_aux_upto: "upto_aux i j js = [i..j] @ js"
-proof cases
-  assume "j < i" thus ?thesis by(simp)
-next
-  assume "\<not> 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]
+  by (simp add: upto_aux_def upto_rec2)
 
 lemma upto_code[code]: "[i..j] = upto_aux i j []"
-by(simp add: upto_aux_upto)
+by(simp add: upto_aux_def)
 
 
 subsubsection {* @{const distinct} and @{const remdups} *}