*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] how to proof termination in "function" command?*From*: 游珍 <yucy0405 at 163.com>*Date*: Wed, 15 Oct 2008 15:41:20 +0800 (CST)

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**

**Follow-Ups**:**Re: [isabelle] how to proof termination in "function" command?***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] Coinduction and induction
- Next by Date: Re: [isabelle] how to proof termination in "function" command?
- Previous by Thread: Re: [isabelle] Coinduction and induction
- Next by Thread: Re: [isabelle] how to proof termination in "function" command?
- Cl-isabelle-users October 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list