Email Gateway (Aug 18 2022 at 12:31): Email Gateway (Aug 18 2022 at 12:31):From: 游珍 <yucy0405@163.com>
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
testletter.thy
Email Gateway (Aug 18 2022 at 12:31):From: Alexander Krauss <krauss@in.tum.de>
Dear Yucy,
apply (relation "measure (\<lambda>(i,j). j + 1 - i)")
Your function has three arguments, so your measure function must be on
triples. Then it works:
termination
by (relation "measure (\<lambda>(i,j,_). j + 1 - i)") auto
Alex
Last updated: May 03 2024 at 04:19 UTC