Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-09-26 Thread Florian Haftmann
Hi again, the current state of affairs concerning 'a set can be followed there: https://isabelle.in.tum.de/isanotes/index.php/Having_%27a_set_back Although I'd appreciate to see progress there, I do not ask to distract any attention from tasks for the upcoming release. Two remarks concerning

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-09-08 Thread Makarius
On Fri, 26 Aug 2011, Lawrence Paulson wrote: I took a look at some of these. HOL-Library fails in your own Cset.thy, where presumably you know what you are doing (particularly as this theory involves execution I should stay away from it). Similarly I'm not sure I'm the right person to fix

[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-09-07 Thread Florian Haftmann
Hi all, again a report about the current affairs: a) state of discussion IMHO I view the discussion at the point that we want 'a set back after the next release. As a consequence, developers are cordially invited to figure out remaining problems involving their contributions to the system, or

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-09-03 Thread Florian Haftmann
Hi again, thanks Alex for the summary. So, it seems that we can conclude that instead of the nice unified development that we hoped for in 2008, we got quite a bit of confusion (points 1.1 and 1.2), in addition to the drawbacks that were already known (1.3, 1.5-1.6). If we had to choose

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-09-03 Thread Christian Urban
Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de: I will now examine HOL-Nominal more closer, and after that come up with a next report about the distribution. There should be no problems in principle. Early versions of Nominal (1) worked perfectly with an explicit

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Lawrence Paulson
indeed yes I'm the person who decided that this primitive should introduce a type as a copy of an existing non-empty set. I have always preferred sets to predicates and the examples I have looked at lately have only strengthened my view. Not to mention numerous occasions when people have

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Lawrence Paulson
I shall take a look at this one. If anybody else is working on it, please let me know as soon as possible. Larry On 25 Aug 2011, at 21:45, Florian Haftmann wrote: HOL-Probability FAILED ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Andreas Schropp
On 08/26/2011 01:08 PM, Makarius wrote: On Thu, 25 Aug 2011, Andreas Schropp wrote: Of course I am probably the only one that will ever care about these things, so whatever. I have always cared about that, starting about 1994 in my first investigations what HOL actually is -- there are still

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Lawrence Paulson
I took a look at some of these. HOL-Library fails in your own Cset.thy, where presumably you know what you are doing (particularly as this theory involves execution I should stay away from it). Similarly I'm not sure I'm the right person to fix HOL-Nominal or HOL-MicroJava. PG is very fragile

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Andreas Schropp
On 08/26/2011 06:33 PM, Brian Huffman wrote: This approach would let us avoid having to axiomatize the 'a set type. Thanks for trying to help me, but as I said: axiomatized set is just a slight inconvenience for me, so if you go for sets as a seperate type don't bother introducing a new

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Tobias Nipkow
I agree. Since predicates are primitive, starting from them is appropriate. Tobias Am 26/08/2011 18:33, schrieb Brian Huffman: Here's one possible approach to the set-axiomatization/typedef issue: As a new primitive, we could have something like a pred_typedef operation that uses

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Andreas Schropp
On 08/26/2011 06:50 PM, Tobias Nipkow wrote: I agree. Since predicates are primitive, starting from them is appropriate. Tobias Did I get this right: the idea is to implement our advanced typedef via a HOL4-style predicate typedef? That doesn't work because HOL4-style typedefs don't

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Brian Huffman
On Fri, Aug 26, 2011 at 9:36 AM, Andreas Schropp schr...@in.tum.de wrote: On 08/26/2011 06:50 PM, Tobias Nipkow wrote: I agree. Since predicates are primitive, starting from them is appropriate. Tobias Did I get this right:  the idea is to implement our advanced typedef via a HOL4-style

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Andreas Schropp
On 08/26/2011 07:08 PM, Brian Huffman wrote: What exactly are our extensions to typedef? I enumerated them in the other thread: local typedefs, sort constraints on type parameters, overloaded constants in representation sets. Hopefully I am not missing others. My understanding of the

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Andreas Schropp
On 08/26/2011 07:08 PM, Brian Huffman wrote: As far as I understand, the typedef package merely issues global axioms of the form type_definition Rep Abs S, as long as it is provided with a proof of EX x. x : S. The global axiom is EX x. x : A == type_definition Rep Abs A allowing local

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Brian Huffman
On Thu, Aug 25, 2011 at 1:45 PM, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: HOL-Hoare_Parallel FAILED Also Hoare_Parallel is non-terminating. I have a patch for this one: http://isabelle.in.tum.de/repos/isabelle/rev/5e681762d538 Once this changeset gets merged into

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Makarius
On Fri, 26 Aug 2011, Brian Huffman wrote: Here's one possible approach to the set-axiomatization/typedef issue: As a new primitive, we could have something like a pred_typedef operation that uses predicates. This would work just like the new_type_definition facility of HOL4, etc. The type

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Andreas Schropp
On 08/26/2011 10:38 PM, Makarius wrote: What is gained from that apart from having two versions of typedef? I am with you here. We don't need two primitive versions of typedefs. The only thing that might be sensible from my POV is using predicates instead of sets in the primitive version

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Brian Huffman
On Fri, Aug 26, 2011 at 1:38 PM, Makarius makar...@sketis.net wrote: On Fri, 26 Aug 2011, Brian Huffman wrote: Here's one possible approach to the set-axiomatization/typedef issue: As a new primitive, we could have something like a pred_typedef operation that uses predicates. This would work

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Alexander Krauss
The global axiom is EX x. x : A == type_definition Rep Abs A allowing local typedefs whenever non-emptiness of A is derivable, even using assumptions in the context. This is an interesting discussion, but totally off-topic in this thread (whose main content is already growing very large.)

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Brian Huffman
On Fri, Aug 26, 2011 at 1:23 PM, Andreas Schropp schr...@in.tum.de wrote: On 08/26/2011 10:38 PM, Makarius wrote: What is gained from that apart from having two versions of typedef? I am with you here. We don't need two primitive versions of typedefs. This is incorrect: Only the

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Makarius
On Fri, 26 Aug 2011, Brian Huffman wrote: What is gained from that apart from having two versions of typedef? In the current version of Isabelle, not much (although I personally think that a predicate-based variant of typedef would have value). But assuming we go ahead and reintroduce 'a

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Cezary Kaliszyk
On Fri, Aug 26, 2011 at 5:45 AM, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: [...] According to my knowledge, the following session produce problems: [...] HOL-Quotient_Examples FAILED Please propagare the isabelle changeset:

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-25 Thread Alexander Krauss
On 08/24/2011 03:36 PM, Lawrence Paulson wrote: I've just been trying to get the proofs working, not to simplify them or even to understand them. Incidentally, let there be no illusions about people accidentally stumbling into a mixture of sets and predicates. Some of these theories were clearly

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-25 Thread Makarius
On Wed, 24 Aug 2011, Florian Haftmann wrote: I was driven crazy some months ago when I attempted in vain to enable push access. I don't even know what the problem was (authentication, web server configuration, encrpytion) – maybe I wasn't even able to figure out. If someone of the TUM guys

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-25 Thread Florian Haftmann
Should we ask a wider audience (isabelle-users) if anybody else has good reasons against/for a change? The thought deserves attention, but I think the discussion is too early for that. Indeed, this is where, as I deem, we current are: * Some agreement that mixing sets and predicate syntax in

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-25 Thread Florian Haftmann
Hi all, thanks to many efforts (thanks particularly to Alex, Brian, Cezary, Larry) we already have gained some insights whether and how it would be technically possible to introduce a set type constructor. As I see the whole story, we have to think carefully how we would proceed in order to

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-25 Thread Florian Haftmann
Hi Jasmin, HOL-Metis_Examples FAILED HOL-Nitpick_Examples FAILED I can look into those things if and when it is decided to move to sets. in case, thanks for the offer. Please ignore any further announcements of these sessions in intermediate reports ;-). Florian -- Home:

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-25 Thread Andreas Schropp
On 08/25/2011 10:45 PM, Florian Haftmann wrote: Hi all, thanks to many efforts (thanks particularly to Alex, Brian, Cezary, Larry) we already have gained some insights whether and how it would be technically possible to introduce a set type constructor. Let me ask something stupid: why

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-25 Thread Andreas Schropp
On 08/25/2011 11:26 PM, Florian Haftmann wrote: Hi Andreas, Let me ask something stupid: why exactly do you guys axiomatize 'a set? Sure it's admissable and all, but why not do this definitionally via the obvious typedef? the answer is rather technical: »typedef« in its current

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-25 Thread Michael Norrish
On 26/08/11 7:26 AM, Florian Haftmann wrote: Hi Andreas, Let me ask something stupid: why exactly do you guys axiomatize 'a set? Sure it's admissable and all, but why not do this definitionally via the obvious typedef? the answer is rather technical: »typedef« in its current

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-24 Thread Lawrence Paulson
I've just been trying to get the proofs working, not to simplify them or even to understand them. Incidentally, let there be no illusions about people accidentally stumbling into a mixture of sets and predicates. Some of these theories were clearly designed from the ground upwards on the

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-24 Thread Florian Haftmann
maybe also declare them [no_atp], to avoid sledgehammer-generated proofs that we know are going to break one release later...? Maybe better now, as long as there are real sledgehammer-generated proofs depending on it. Florian -- Home: http://www.in.tum.de/~haftmann PGP available:

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-24 Thread Florian Haftmann
A proof works only if I insert before it the following: instance set :: (type) complete_boolean_algebra proof qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def Inf_bool_def Sup_bool_def) this is strange because this exact text already appears in the file Complete_Lattice.thy

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-24 Thread Florian Haftmann
Hi all, Shouldn't one remove quite a bit of duplication first? The classes distributive_complete_lattice and complete_boolean_algebra are now part of HOL (the former as complete_distrib_lattice) (see the FIXME). The set instances for those should be in/go into Florian's HOL repository as

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-23 Thread Alexander Krauss
On 08/23/2011 01:51 PM, Lawrence Paulson wrote: I'm starting to have doubts about this entire procedure. I thought the plan was to get these theories (particularly in the AFP) into a state where they no longer dependent on confusing sets with predicates so that they would work with either

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-22 Thread Lawrence Paulson
I've come across something strange in the file isabelle/afp/devel/thys/DataRefinementIBP/Diagram.thy and was wondering if anybody could think of an explanation. A proof works only if I insert before it the following: instance set :: (type) complete_boolean_algebra proof qed (auto simp add:

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-22 Thread Brian Huffman
On Mon, Aug 22, 2011 at 8:01 AM, Lawrence Paulson l...@cam.ac.uk wrote: I've come across something strange in the file isabelle/afp/devel/thys/DataRefinementIBP/Diagram.thy and was wondering if anybody could think of an explanation. A proof works only if I insert before it the following:

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-20 Thread Alexander Krauss
On 08/20/2011 01:18 AM, Florian Haftmann wrote: A typical example for what I was alluding to can be found at: http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/6e3e9c6c5062#l1.37 Observe the following proof: lemma part_equivpI: (\existsx. R x x) \Longrightarrow symp R

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-19 Thread Lawrence Paulson
I am currently working on AFP/Coinductive, which is full of the sort of thing. Larry On 19 Aug 2011, at 00:31, Gerwin Klein wrote: Can't really quantify it, but I'm seeing this all the time from not-so-novice users over here. Mixing sets and predicates (e.g. using intersection on

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-19 Thread Dmitriy Traytel
Hi all, On 19.08.2011 01:38, Gerwin Klein wrote: Should we ask a wider audience (isabelle-users) if anybody else has good reasons against/for a change? Another small advantage of set as an own datatype arises in the context of subtyping. We use map functions to lift coercions between base

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-19 Thread Lukas Bulwahn
Stefan Berghofer wrote: Alexander Krauss wrote: In particular, Stefan discovered that replacing inductive set definitions by predicates was by no means as easy as everybody had expected. One good example is the small-step relation from Jinja and its various cousins. It had type ((expr * state)

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-19 Thread Lukas Bulwahn
On 08/19/2011 07:39 AM, Tobias Nipkow wrote: Am 19/08/2011 00:00, schrieb Stefan Berghofer: Alexander Krauss wrote: I want to emphasize that the limitation of the code generator mentioned here not only applies to sets-as-predicates but also to maps-as-functions and other abstract types that

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-19 Thread Alexander Krauss
On 08/19/2011 01:31 AM, Gerwin Klein wrote: On 19/08/2011, at 5:56 AM, Alexander Krauss wrote: * Similarly, there is a vast proof search space for automated tools which is not worth exploring since it leads to the »wrong world«, making vain proof attempts lasting longer instead just failing.

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-19 Thread Florian Haftmann
Hi again, Indeed, I think a general point can be made here, and not just about code generation. In the last couple of years, we've run into situations in Quickcheck, Nitpick, the code generator, and perhaps more, where we felt the need for sets as different from functions. However, there

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study

2011-08-18 Thread Jasmin Christian Blanchette
Hi Florian, Am 18.08.2011 um 09:18 schrieb Florian Haftmann: @list: btw. what is the status of »refute« in general? Is it supposed to be superseded by nitpick entirely? Pretty much so, yes, but there are a few reasons why I would rather that we keep it around: 1. Refute participates at

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-18 Thread Cezary Kaliszyk
On Thu, Aug 18, 2011 at 3:49 AM, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: [...] So, the best way now is to continue eliminating set-pred mixture (also in the AFP of course!) and discover problems in packages – I'm a little concerned about quotient since this has

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-18 Thread Jasmin Christian Blanchette
Hi all, Let me describe the implications of reintroducing 'a set for Sledgehammer's and Nitpick's performance. Am 12.08.2011 um 11:27 schrieb Alexander Krauss: What are, actually, the losses when going back? This has not yet been touched by this thread at all (except the

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-18 Thread Makarius
On Thu, 18 Aug 2011, Florian Haftmann wrote: envisaged working plan -- a) general b) elimination of set/pred mixture c) consolidation d) RELEASE This looks quite reasonable to me: the parts a, b, c should be easy to consolidate for the release towards the end of the

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-18 Thread Alexander Krauss
On 08/18/2011 02:16 PM, Florian Haftmann wrote: * (maybe) hide_fact (open) Set.mem_def Set.Collect_def to indicate that something is going on with these maybe also declare them [no_atp], to avoid sledgehammer-generated proofs that we know are going to break one release later...?

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study

2011-08-18 Thread Tjark Weber
On Thu, 2011-08-18 at 09:34 +0200, Jasmin Christian Blanchette wrote: The maintenance load is extremely low. When it comes to the REFUTE exception, I can look at it if and when we decide to move back to sets. I suspect that Jasmin will have no trouble fixing this, but otherwise I'd be happy to

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-18 Thread Alexander Krauss
Hi all, Here are some critical questions/comments towards two of Florian's initial arguments pro 'a set. [...] * Similarly, there is a vast proof search space for automated tools which is not worth exploring since it leads to the »wrong world«, making vain proof attempts lasting longer

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-18 Thread Stefan Berghofer
Alexander Krauss wrote: In particular, Stefan discovered that replacing inductive set definitions by predicates was by no means as easy as everybody had expected. One good example is the small-step relation from Jinja and its various cousins. It had type ((expr * state) * (expr * state)) set,

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-18 Thread Stefan Berghofer
Alexander Krauss wrote: I want to emphasize that the limitation of the code generator mentioned here not only applies to sets-as-predicates but also to maps-as-functions and other abstract types that are often specified in terms of functions (finite maps, almost constant maps, etc.). Thus,

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-18 Thread Stefan Berghofer
Tobias Nipkow wrote: Am 12/08/2011 11:27, schrieb Alexander Krauss: On 08/12/2011 07:51 AM, Tobias Nipkow wrote: The benefits of getting rid of set were smaller than expected but quite a bit of pain was and is inflicted. Do you know of any more pain, apart from what Florian already mentioned?

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-18 Thread Jasmin Christian Blanchette
Am 19.08.2011 um 00:00 schrieb Stefan Berghofer: thanks for your excellent report, I fully agree with this view. There is often a tradeoff between executability and conciseness / abstractness of specifications, so I don't think it is a good idea to tweak the logic in such a way that it is

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-18 Thread Stefan Berghofer
Florian Haftmann wrote: just do something like (unfold mem_def) and your proof will be a mess since you have switched to the wrong world. Like any definition of a primitive operator, mem_def is not really intended to be unfolded by the user, so don't be surprised if your proof is a mess after

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-18 Thread Gerwin Klein
On 19/08/2011, at 5:56 AM, Alexander Krauss wrote: Here are some critical questions/comments towards two of Florian's initial arguments pro 'a set. [...] * Similarly, there is a vast proof search space for automated tools which is not worth exploring since it leads to the »wrong world«,

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-18 Thread Gerwin Klein
On 19/08/2011, at 8:10 AM, Stefan Berghofer wrote: Tobias Nipkow wrote: Am 12/08/2011 11:27, schrieb Alexander Krauss: On 08/12/2011 07:51 AM, Tobias Nipkow wrote: The benefits of getting rid of set were smaller than expected but quite a bit of pain was and is inflicted. Do you know of any

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-18 Thread Tobias Nipkow
Am 19/08/2011 00:10, schrieb Stefan Berghofer: Tobias Nipkow wrote: Am 12/08/2011 11:27, schrieb Alexander Krauss: On 08/12/2011 07:51 AM, Tobias Nipkow wrote: The benefits of getting rid of set were smaller than expected but quite a bit of pain was and is inflicted. Do you know of any more

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-18 Thread Tobias Nipkow
Am 19/08/2011 00:00, schrieb Stefan Berghofer: Alexander Krauss wrote: I want to emphasize that the limitation of the code generator mentioned here not only applies to sets-as-predicates but also to maps-as-functions and other abstract types that are often specified in terms of functions

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-17 Thread Florian Haftmann
Hi again, inquit Brian: Overall, I must say that I am completely in favor of making set a separate type again. But I also believe that the sets=predicates experiment was not a waste of time, since it forced us to improve Isabelle's infrastructure for defining and reasoning about predicates:

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study

2011-08-17 Thread Florian Haftmann
Hi again, thanks to all contributors who already started to sort out some of the set-pred mixture issues. I have merged recent changes back into http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/ -- this is meant as a mere basis for figuring out problems experimentally, not as a

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study

2011-08-13 Thread Gerwin Klein
On 11/08/2011, at 2:44 PM, Florian Haftmann wrote: Then the following sessions fail: HOL-Algebra HOL-Auth HOLCF HOL-ex HOL-Hahn_Banach HOL-Hoare_Parallel HOL-IMP HOL-Imperative_HOL HOL-Induct HOL-Library HOL-Matrix HOL-Metis_Examples HOL-MicroJava

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-12 Thread Amine Chaieb
I am also in favor of the set type-constructor. The issue of compatibility with other HOL provers could very probably be solved by the transfer mechanism. If not immediately from the generic setup, the surely from a tailored one dedicated to this issue, if enough people are concerned. Amine.

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-12 Thread Alexander Krauss
On 08/12/2011 07:51 AM, Tobias Nipkow wrote: The benefits of getting rid of set were smaller than expected but quite a bit of pain was and is inflicted. Do you know of any more pain, apart from what Florian already mentioned? Sticking with something merely to avoid change is not a strong

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-12 Thread Tobias Nipkow
Am 12/08/2011 11:27, schrieb Alexander Krauss: On 08/12/2011 07:51 AM, Tobias Nipkow wrote: The benefits of getting rid of set were smaller than expected but quite a bit of pain was and is inflicted. Do you know of any more pain, apart from what Florian already mentioned? I think he omitted

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-12 Thread Lawrence Paulson
It's clear that for inductive definitions, relations are frequently more natural than sets. But I wonder whether a less drastic solution could have been found than abandoning sets altogether. (I'm trying to imagine some sort of magic operator to ease the transition between sets with various

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-12 Thread Alexander Krauss
On 08/12/2011 01:01 PM, Lawrence Paulson wrote: (I'm trying to imagine some sort of magic operator to ease the transition between sets with various forms of tupling and relations.) These tools exist to some extent, as the attributes [to_set] and [to_pred]. It is used a few times in the

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-12 Thread Tobias Nipkow
Surely we want to maintain both inductive and inductive_set? Tobias Am 12/08/2011 13:01, schrieb Lawrence Paulson: It's clear that for inductive definitions, relations are frequently more natural than sets. But I wonder whether a less drastic solution could have been found than abandoning

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-12 Thread Alexander Krauss
On 08/12/2011 02:16 PM, Tobias Nipkow wrote: Surely we want to maintain both inductive and inductive_set? This is what Florian's experiment does. It basically reverts the 2008 transition, but not the 2007 one. Alex ___ isabelle-dev mailing list

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-12 Thread Brian Huffman
On Fri, Aug 12, 2011 at 2:27 AM, Alexander Krauss kra...@in.tum.de wrote: What are, actually, the losses when going back? This has not yet been touched by this thread at all (except the compatibility/import issue mentioned by Brian), and at least myself I wouldn't feel comfortable answering

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-12 Thread Makarius
On Fri, 12 Aug 2011, Alexander Krauss wrote: Instead of stating an opinion, let me recall the parts of the story so far that I know, to avoid that history repeats itself. I am sure that Stefan will add some interesting details, too. (He wrote to me that it may take him a few days to comment

[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-11 Thread Florian Haftmann
Hello together, recently in some personal discussions the matter has arisen whether there would be good reason to re-introduce the ancient set type constructor. To open the discussion I have carried together some arguments. I'm pretty sure there are further ones either pro or contra, for which

[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study

2011-08-11 Thread Florian Haftmann
Hi again, as feasibility study I re-introduced the good old set type constructor at a recent revision in the history. The result can be inspected at http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329 This is by no means meant as a thorough treatment of the whole

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-11 Thread Brian Huffman
On Thu, Aug 11, 2011 at 5:43 AM, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: Hello together, recently in some personal discussions the matter has arisen whether there would be good reason to re-introduce the ancient set type constructor. To open the discussion I have

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-11 Thread Alexander Krauss
Florian: Is your modified Isabelle repo available for cloning, so we can play with it? If so, I might be able to find an answer to my own question... You can clone directly from the http:// location: hg clone http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set or, faster, clone

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-11 Thread Thomas Sewell
] Sent: Thursday, August 11, 2011 11:09 PM To: Florian Haftmann Cc: DEV Isabelle Mailinglist Subject: Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation I hope that my position on this question is obvious. And if we decide to revert to the former setup

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-11 Thread Tobias Nipkow
The benefits of getting rid of set were smaller than expected but quite a bit of pain was and is inflicted. Sticking with something merely to avoid change is not a strong argument. This time we know what we go back to and the real benefits (and the few losses). Hence I would be in favour. Tobias