Re: [isabelle] Turning intervals into lists: upt and upto



Yes, "[i..<j] = (if i < j then i # [Suc i..<j] else [])" does not terminate (hence my "something like") and two conditional rules are probably the best option. But updating the proofs could be daunting...

Tobias

On 17/07/2021 10:57, Florian Haftmann wrote:
Hi all,

I always like to balance ease of notation and proof automation.

I would have no objection against generalising [_.._] to some type class.

5 years ago I posted sth. on the mailing list:
https://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg06715.html

I think it is still a valid starting point for further discussion.

If you really want to improve the situation, you could iron out a
different problem. This is a defining equation and simp rule:

"[i..<(Suc j)] = (if i ≤ j then [i..<j] @ [j] else [])"

Unfortunately it leads to lists where elements are appended at the end,
but many functions consume lists from the front. Thus this simp rule is
frequently removed. Something like the following one should work better
(I hope):

"[i..<j] = (if i < j then i # [Suc i..<j] else [])"

I agree with the observation that the default simp rule above obstructs
proofs that would require unfolding from the lower bound rather than the
upper bound.  But the alternative formulation has no syntactic circuit
breaker like Suc and would hence unfold infinitely.  Maybe a conditional
formulation would help:

‹i < j ==> [i..<j] = i # [Suc i..<j]›

But this all would require further thinking.

Cheers,
	Florian


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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