Email Gateway (Aug 19 2022 at 17:01): Email Gateway (Aug 19 2022 at 17:01):From: Ghassen HELALI <helali@encs.concordia.ca>
Dear Fellows
I was trying t load the Lazy list theory of L. Paulson in the 2014
Isabelle/HOL version but I found some errors occurring.
As for example in the definition of:
definition
lmap :: "('a=>'b) => 'a llist => 'b llist" where
"lmap f l = llist_corec l (%z. case z of LNil => None
| LCons y z => Some(f(y), z))"
I got the error saying that LNil is not a constructor. I recall that it is
previously defined as an abstract constructor from NIL.
Any ideas how to solve this issue?
Regards
--gh
Email Gateway (Aug 19 2022 at 17:01):From: Johannes Hölzl <hoelzl@in.tum.de>
Huh, which theory are you using? The lazy list theory in AFP 2014 is
using the new codatatype package, which defines lmap internally.
Maybe you are trying to load a old theory with a new Isabelle version?
Email Gateway (Aug 19 2022 at 17:01):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Ghassen,
Where did you get Larry's theory from and what Isabelle version was that for? AFAIK this
theory has not been distributed with Isabelle for a few releases. IIRC this theory
emulates case syntax with syntax translations. This predates Dmitriy's new implementation,
which supports proper nesting. This is why you get the error message. In Isabelle2014, you
have to explicitly register the constructors using a case_translation declaration. In the
AFP entry Coinductive, there is still a working example (of a different type) which
derives the constructors from Larry's universe of datatypes:
http://afp.sourceforge.net/browser_info/current/AFP/Coinductive/Resumption.html
There, you find the declaration
declare [[case_translation case_resumption Terminal Linear Branch]]
In the lazy list case, you have to replace the syntax translations for the case combinator
with something like
declare [[case_translation case_llist LNil LCons]]
provided that your case operator is called "case_llist". You can also dig in the version
history of the Resumption file in the AFP to figure out what exactly has to be changed.
There is also a new command free_constructors in Isabelle2014, which can do most of the
case combinator definition and declarations for you. See the datatype tutorial for more
information on that.
Hope this helps,
Andreas
Last updated: Apr 24 2024 at 01:07 UTC