Re: [isabelle-dev] typedef (open) legacy
On 10/09/2012 11:20 AM, Makarius wrote:
On Mon, 8 Oct 2012, Brian Huffman wrote:
I have a changeset that removes the set-definition features from the
{cpo,pcpo,domain}def commands in HOLCF, and it checks successfully on
testboard.
http://isabelle.in.tum.de/testboard/Isabelle/rev/a093798fa71b
Should I go ahead and push this changeset to the current tip?
I cannot connect to testboard at the moment, it seems to be in bad
shape again.
The testboard should now be in a running state again.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] typedef (open) legacy
On Fri, Oct 5, 2012 at 10:37 AM, Makarius makar...@sketis.net wrote:
On Thu, 4 Oct 2012, Brian Huffman wrote:
I was reluctant to support closed type definitions at all in HOLCF's
cpodef and friends, preferring to make (open) the default behavior; but in
the end I decided it was more important to make the input syntax consistent
with typedef. I would be more than happy to remove this feature from the
HOLCF packages if typedef will be changed to match.
Do you want to make the first move to remove the (open) option from the
HOLCF cpodef packages? I will later follow trimming down HOL typedef --
there are a few more fine points on my list to iron out there once the set
defs are gone. Alternatively, I can take do it for 'typdef' packages
simultaneously.
Hi Makarius,
I have a changeset that removes the set-definition features from the
{cpo,pcpo,domain}def commands in HOLCF, and it checks successfully on
testboard.
http://isabelle.in.tum.de/testboard/Isabelle/rev/a093798fa71b
Should I go ahead and push this changeset to the current tip?
- Brian
Before doing anything on the packages, we should make another round through
the visible universe of theories to eliminate the last uses of the legacy
mode.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] typedef (open) legacy
On Thu, 4 Oct 2012, Florian Haftmann wrote: I think either option 3 or 4 would make sense, although I'd say 4 is preferable for a couple of reasons: First, it makes the implementation of typedef simpler. Second, it actually gives users more flexibility because if they want a set constant, they can use any definition package, not just definition. The extra verbosity in some cases is a small price to pay. I would support (4). In the long run, typedef should be the bare foundational minimum for introducing HOL types I also remember it like that -- most package authors were already in favour of (4) open only without option some years ago, but we never made the move. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] typedef (open) legacy
Hi, Closed type definitions with typedef new_type = some set are considered legacy. The warning message suggests to use typedef (open) new_type = some set but as far as I can see, this does not introduce a definition for the set underlying the type. For example the theorem new_type_def is not generated with open. I have a number of lemmas that are of the form f \in new_type == something which require new_type_def. What is the received wisdom to update those proofs? I see that FinFun.thy goes around the problem above by giving an explicit definition for the set as in definition new_type_set = something typedef (open) new_type = new_type_set Is this how it should be done nowadays? Looks to me more verbose than an improvement. Any comments? Best wishes, Christian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] typedef (open) legacy
On Thu, Oct 4, 2012 at 2:17 PM, Makarius makar...@sketis.net wrote:
On Thu, 4 Oct 2012, Christian Urban wrote:
Closed type definitions with
typedef new_type = some set
are considered legacy. The warning message suggests
to use
typedef (open) new_type = some set
but as far as I can see, this does not introduce a definition for the set
underlying the type. For example the theorem
new_type_def
is not generated with open.
Defining a set constant does not make sense for all typedefs. For
example, type 'a word in HOL-Word is defined something like this:
typedef (open) 'a word = {(0::int) .. 2^card (UNIV :: 'a set)}
It is not possible to define a single constant word :: int set that
is equal to the given right-hand side for any 'a.
Similar typedefs are also found in the HOLCF libraries.
Here are the options we have for the typedef implementation:
1) typedef fails with an internal error on such definitions in its
default (closed) mode
2) typedef includes special code to generate set definitions with
extra type parameters, e.g. word :: 'a itself = int set
3) typedef uses (open) as the default mode, with closed definitions as an option
4) typedef supports only open set definitions
Option 1 is how typedef worked until a few years ago; obviously the
error message was undesirable. Option 2 is how it works now, but the
special code complicates the package and the special behavior is a bit
surprising when it happens.
I think either option 3 or 4 would make sense, although I'd say 4 is
preferable for a couple of reasons: First, it makes the implementation
of typedef simpler. Second, it actually gives users more flexibility
because if they want a set constant, they can use any definition
package, not just definition. The extra verbosity in some cases is a
small price to pay.
[...]
So today, the form with the extra definition is mostly irrelevant, but we
were a bit slow to remove the last remains of it from the typedef packages
(and some add-ons of it in HOLCF). It might be time now to do the purge
before the next release ...
I was reluctant to support closed type definitions at all in HOLCF's
cpodef and friends, preferring to make (open) the default behavior;
but in the end I decided it was more important to make the input
syntax consistent with typedef. I would be more than happy to remove
this feature from the HOLCF packages if typedef will be changed to
match.
- Brian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] typedef (open) legacy
Thanks a lot for all replies! Christian On Thursday, October 4, 2012 at 14:17:48 (+0200), Makarius wrote: On Thu, 4 Oct 2012, Christian Urban wrote: Closed type definitions with typedef new_type = some set are considered legacy. The warning message suggests to use typedef (open) new_type = some set but as far as I can see, this does not introduce a definition for the set underlying the type. For example the theorem new_type_def is not generated with open. I have a number of lemmas that are of the form f \in new_type == something which require new_type_def. What is the received wisdom to update those proofs? I see that FinFun.thy goes around the problem above by giving an explicit definition for the set as in definition new_type_set = something typedef (open) new_type = new_type_set Is this how it should be done nowadays? Looks to me more verbose than an improvement. The latter verbose version is the canonical way to upgrade old theories, without changing their structure. If a bit more work is invested, in most cases the very need for the new_type_set definition can be eliminated in the concrete application, and then everything becomes simpler than before. Historically, Larry introduced a certain Gordon HOL typedef imitation scheme for Isabelle/HOL, which I imitated faithfully in the first version of the typedef package, to generate exactly the same axiomatization with the auxiliary new_type_set. Several years later, Brian Huffman pointed out first that this is redundant in many situations. Some more years later, I joined Brian in this observation --- after looking critically through the existing library of theories and packages. So today, the form with the extra definition is mostly irrelevant, but we were a bit slow to remove the last remains of it from the typedef packages (and some add-ons of it in HOLCF). It might be time now to do the purge before the next release ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
