maybe someone can help me with a termination proof in Isabelle. I am trying to construct from the list A a new sub-list B. For constructing B, I read again and again of the whole A. Take out elements and use the result for the search for the next element. I designed a simple example to illustrate that:
given is a list of random real numbers. And we say that a number P is on the list, if an item from the list is greater than P.
definition pointOnList :: "real list ⇒ real ⇒ bool" where
"pointOnList L P ≡ ∃ i. i < length L ∧ P < L!i"
I create a function that always take the next larger element.
fun nextPoint :: "real list ⇒ real ⇒ real" where
"nextPoint (X#Ls) P = (if (X > P)
then (X)
else (nextPoint Ls P))"
And now I'm trying to create a new sorted part-list by take out the next larger element than P but less than Q with nextPoint and continuing with this.
function listBetween :: "real list ⇒ real ⇒ real ⇒ real list" where
"pointOnList L P ⟹ pointOnList L Q ⟹ listBetween L P Q = (if(P ≤ Q)
then(P # (listBetween L (nextPoint L P) Q))
else([]))"
I have already demonstrated nextPoint always returns a growing number:
lemma foo: "pointOnList P A ⟹ A < (nextPoint P A)"
the termination proof with relation "measure (size o fst o snd)“ not working for real numbers…and now I don’t know how to continue.
To show termination in Isabelle, you have to show that the recursive calls follow a wellfounded relation. The easiest way to do that is to give a termination measure returning natural number that becomes smaller with every call. That does not work with real numbers because they are not wellfounded – you could have something like 1 → 1/2 → 1/4 → 1/8 → …
The termination measure to use in your case would be the number of list elements that fulfil the condition, i.e. length (filter (λx. P ≤ x ∧ x ≤ Q)) l. However, note that your definition fails to work if Q is larger than all numbers in the list.
Your definition is somewhat laborious and complicated. I recommend the following definition:
listBetween L P Q = sort (filter (λx. P ≤ x ∧ x ≤ Q) L)
or, equivalently,
listBetween L P Q = sort [x ← L. x ∈ {P..Q}]
Note, however, that this definition does not throw away multiple occurrences of the same number, i.e. listBetween L 0 10 [2,1,2] = [1,2,2]. If you want to throw them away, you can use remdups.
Also note that something like pointOnList L P ≡ ∃ i. i < length L ∧ P < L!i is pretty much never what you want – there is no need to work with explicit list indices here. Just do ∃x∈set L. P < x.