# Re: [isabelle] Trivial lemma requires syntactic fiddling

*To*: Nemouchi Yakoub <y.nemouchi at gmail.com>
*Subject*: Re: [isabelle] Trivial lemma requires syntactic fiddling
*From*: Lawrence Paulson <lp15 at cam.ac.uk>
*Date*: Fri, 1 Mar 2019 15:18:46 +0000
*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
*In-reply-to*: <CAH9vN+fEorvhSYqY4UK41YDZnzmNKq7YZ6=1XNjHauprA=6cOw@mail.gmail.com>
*References*: <CAH9vN+fEorvhSYqY4UK41YDZnzmNKq7YZ6=1XNjHauprA=6cOw@mail.gmail.com>

In logic there are always many ways of writing the same thing. But as regards Isabelle’s automation, as a general rule, you should prefer to minimise the use of bound variables. In this case, {na::nat. na ≤n} looks much more complicated to Isabelle than {0..n::nat}. More generally, consider replacing {x. P x & Q x} by the obvious intersection, et cetera.
Larry Paulson
> On 1 Mar 2019, at 15:13, Nemouchi Yakoub <y.nemouchi at gmail.com> wrote:
>
> Dear list,
>
> It is a bit awkward to see that to prove a trivial lemma on natural numbers
> requires syntactic fiddling on the notation of sets. It looks like the
> whole reasoning machinery behind assumes a certain syntactic notation for
> sets.
>
> For example the lemma in the sequel requires me to apply (**) twice as
> substitution just to get in a syntactic form where I can apply the
> reasoning machinery provided by the library. Namely, it is awkward to see
> that the notation {0..n::nat} is better than {na::nat. na ≤n} when proving
> stuff on ∑ .
> My question is why not just having the same syntactic sugar for both
> notations? Any limitations to have an abbreviation of the form {na::nat. na
> ≤n} == {0..n::nat}? Or just because ∑ is too general? Is there an existing
> AFP entry or an Isabelle theory that introduces these kind of abbreviations
> when sets are specialized for natural numbers?

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