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



hello,
   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 
begin

fun sum :: "nat \<Rightarrow> nat  \<Rightarrow> nat list \<Rightarrow> nat"
where
"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"
where
"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
termination 
apply (relation "measure (\<lambda>(i,j). j + 1 - i)")  ??????????

 

end

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

 
                                      yucy

Attachment: testletter.thy
Description: Binary data



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