Email Gateway (Aug 22 2022 at 09:37): Email Gateway (Aug 22 2022 at 09:37):From: "W. Douglas Maurer" <maurer@gwu.edu>
I am trying to formalize the usual rule about checking whether a list
is sorted by checking only adjacent elements of the list. So if t is
an int list with no duplicate elements, then in order to show that t
! i < t ! j for all i < j in range, it is enough to show that t ! i <
t ! (i+1) for all i in range (other than the end of t, where t !
(i+1) is not defined). I wanted to formalize this with fixes,
assumes, and shows, and so I started out by writing lemma fixes "t ::
int list"; and I got an error message reading Legacy feature! Bad
name binding: "t :: int list". Well, if I understand the term "legacy
feature," this is something that used to work, in older versions of
Isabelle, so I must have learned it while using an older version. By
experimentation I was able to get this to work by taking the "t :: "
outside the double quotes, like this: lemma fixes t :: "int list" .
But this raises a larger question: When features are taken out of
Isabelle n in producing Isabelle n+1, is there a list of such
features, somewhere, together with what they are replaced by? I don't
want to teach my students something that no longer works, even if it
used to work. I'm particularly interested in seeing such a list for
Isabelle2015, when that comes out. -WDMaurer
Last updated: Nov 21 2024 at 12:39 UTC