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

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: at

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.


Attachment: OpenPGP_signature
Description: OpenPGP digital signature

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