simplified construction of upto_aux
authorhaftmann
Sun Feb 17 11:34:40 2013 +0100 (2013-02-17)
changeset 51170b3cdcba073d5
parent 51169 bf18bf4922ea
child 51171 e8b2d90da499
simplified construction of upto_aux
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Sun Feb 17 11:06:10 2013 +0100
     1.2 +++ b/src/HOL/List.thy	Sun Feb 17 11:34:40 2013 +0100
     1.3 @@ -3115,26 +3115,15 @@
     1.4  
     1.5  text{* Tail recursive version for code generation: *}
     1.6  
     1.7 -function upto_aux :: "int \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
     1.8 +definition upto_aux :: "int \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
     1.9 +  "upto_aux i j js = [i..j] @ js"
    1.10 +
    1.11 +lemma upto_aux_rec [code]:
    1.12    "upto_aux i j js = (if j<i then js else upto_aux i (j - 1) (j#js))"
    1.13 -by auto
    1.14 -termination by(relation "measure(%(i::int,j,js). nat(j - i + 1))") auto
    1.15 -
    1.16 -lemma upto_aux_upto: "upto_aux i j js = [i..j] @ js"
    1.17 -proof cases
    1.18 -  assume "j < i" thus ?thesis by(simp)
    1.19 -next
    1.20 -  assume "\<not> j < i"
    1.21 -  thus ?thesis
    1.22 -  proof(induct i j js rule: upto_aux.induct)
    1.23 -     case 1 thus ?case using upto_rec2 by simp
    1.24 -  qed
    1.25 -qed
    1.26 -
    1.27 -declare upto_aux.simps[simp del]
    1.28 +  by (simp add: upto_aux_def upto_rec2)
    1.29  
    1.30  lemma upto_code[code]: "[i..j] = upto_aux i j []"
    1.31 -by(simp add: upto_aux_upto)
    1.32 +by(simp add: upto_aux_def)
    1.33  
    1.34  
    1.35  subsubsection {* @{const distinct} and @{const remdups} *}