[isabelle] how to proof termination in "function" command?

   I try to define a funciton:

     Premise xs:: nat list  

     lists(i,j,xs) =  [ ]                               (if j≥size xs)

     ists(i,j,xs) =   [ ]                         (if j<size xs and i>j)

     lists(i,j,xs) =  (∑k:i≤k≤j xs[i])#lists(i+1.j,xs)

                                                     (if j<size xs and i≤j)

   Firstly, i use "fun" command, but it fails.
   so ,i try to define this function using "function" command. 
   In order to proof the completeness and compatibilitiy ,i use the method  "pat_completeness" and method "auto". 
   However, in the process of proofing termination,  method "lexicographic_order" can't work, because the variable i get greater in every step. hence, i choose the method 

apply (relation "measure (\<lambda>(i,j). j + 1 - i)"), because j+1-i get smaller in every step.  it still fails, and i don't know where is the promble. the following are my theory file: 



theory minsum
imports Main 

fun sum :: "nat \<Rightarrow> nat  \<Rightarrow> nat list \<Rightarrow> nat"
"sum i j xs = (if j\<ge>size xs then 0 else (if i>j then 0 else (\<Sum>k\<in>{i..<Suc j}. (xs !k))))"

function lists::  "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat list"
"lists i j xs =(if j\<ge>size xs then [] else ( if i>j then [] else (sum i j xs)#(lists (Suc i) j xs) ))"
by pat_completeness auto
apply (relation "measure (\<lambda>(i,j). j + 1 - i)")  ??????????



 need help!
 Thank you in advance for any help on this.


Attachment: testletter.thy
Description: Binary data

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.