Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
Current state of affairs: https://isabelle.in.tum.de/isanotes/index.php/Having_%27a_set_back In case somebody has some time to spend on the AFP, sessions HOL-FinFun HRB-Slicing LinearQuantifierElim HOLCF-Shivers-CFA HOL-Flyspeck-Tame are good candidates too continue with. Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 the Isabelle distribution itself: * In HOL-Nominal-Examples, equivariance in theory Fsub fails. My knowledge about equivariance is too restricted to decide whether this is a mistake in the (adjustion of the) implementation or maybe needs additional declarations etc. I'm happy about any hints concerning this. * The remaining issues mainly are concerned with particular tools at which the corresponding maintainers should have a closer look at (if not done already). Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
>> 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 >> just now, which makes working very tiresome. > > In the past few days I have managed to overcome some serious performance > bottle necks in Isabelle/jEdit (cf. changes leading up to 03a5ba7213cf from > Tuesday this week). This looks very nice btw! Exactly what I need to do demos in the lecture with my old 2 core/2GB MacBook Air. I'm happy to look at MicroJava in a while. The last time I checked it failed because of something in HOL/Library (CSet? not sure any more). Almost all of it was written before the set/predicate unification, so there shouldn't be anything fundamental. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 HOL-Nominal or HOL-MicroJava. PG is very fragile just now, which makes working very tiresome. In the past few days I have managed to overcome some serious performance bottle necks in Isabelle/jEdit (cf. changes leading up to 03a5ba7213cf from Tuesday this week). This means one can now load full sessions like MicroJava into the Prover IDE, even on a two-core machine (say with 4 GB, but it also works with 2 GB to some extent). Minor omission: I still need to make the crude "Prover Session / Theory Status" overview panel more comprehensive. So maintainance of old theory collections could become eanjoyable again, after unlearning some Escape-Meta-Alt-Control-Shift key sequences. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
Quoting Florian Haftmann : 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 set-type. They had an instance for sets and permutation types, and that is basically the only Nominal specific change that is needed now. Best wishes, Christian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 between the two versions now > (with no status quo to consider), the case would be pretty clear. So > the question is whether our users out there will tolerate that they > have to fix quite a number of theories. following the discussions it appears that we have settled to reintroduce 'a set – after the next release. I will now examine HOL-Nominal more closer, and after that come up with a next report about the distribution. The intermediate state can always be inspected at http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set Concerning AFP, the discussion with Viorel (partially of-list) has reminded me that we should trust our users more and not try to convert AFP entries silently without contacting them previously. Already the feedback has a value on its own: Nevertheless, here a repository clone where single adaptions might go at a later time, although I would be lucky not to need it: http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/afp_set Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Thu, Aug 25, 2011 at 1:45 PM, Florian Haftmann wrote: > HOL-Probability FAILED This is now fixed in the main repo; the following changeset should be merged back into isabelle_set: http://isabelle.in.tum.de/repos/isabelle/rev/c10485a6a7af ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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: http://isabelle.in.tum.de/repos/isabelle/rev/5e0f9e0e32fb to Isabelle-set. With it, Quotient_Examples succeeds. Cheers, Cezary ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 set" as a separate type again, this plan for typedef would reduce the number of primitive concepts and axioms required to bootstrap HOL. Of course, axioms like mem_Collect_eq and Collect_mem_eq are rather uncontroversial, as axioms go. But if there is an easy way to avoid declaring these as axioms, then keeping them as axioms seems a bit gratuitous, in my opinion. We have had exactly that discussion in 1994. Nothing is gained foundationally by adding or substracting these the mem/Collect axioms. It is a matter of what is more useful for the user, without duplicating packages at will. Back then we decided to go with 'a set for typedef, as had been the original scheme by Larry from long before. Whetever becomes of the 'a => bool vs. 'a set plan, the typedef package should follow the main line without becoming more complicated by additional variants. Concerning axiomatizations in general, it is good practice to be "conservative" in a common sense, sticking to well-understood axiomatizations instead of reducing them by mere number. Anyway the typedef package is right now in a relatively clean state, and almost fully "localized". Any spare time is better invested in other packages, such as the HOLCF versions of it, not to speak of our running gags of record and datatype. Nothing to be started before the release, though. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On 08/26/2011 10:50 PM, Brian Huffman wrote: On Fri, Aug 26, 2011 at 1:23 PM, Andreas Schropp 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 predicate-based typedef need be primitive. The set-based typedef can be implemented definitionally as a thin layer on top of the predicate-based one. That is exactly what I said below the quoted line. ;> I guess this discussion only came about because you said HOL4-style typedefs, which cannot be used as the primitive. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Fri, Aug 26, 2011 at 1:23 PM, Andreas Schropp 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 predicate-based typedef need be primitive. The set-based typedef can be implemented definitionally as a thin layer on top of the predicate-based one. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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.) Please start a separate thread, if you want to continue... Thanks, Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Fri, Aug 26, 2011 at 1:38 PM, Makarius 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 just like the >> new_type_definition facility of HOL4, etc. >> >> The type "'a set" could be introduced definitionally using "pred_typedef". >> >> After type "'a set" has been defined, we can implement the "typedef" >> command, preserving its current behavior, as a thin wrapper on top of >> "pred_typedef". >> >> This approach would let us avoid having to axiomatize the 'a set type. >> Also, for those of us who like predicates, "pred_typedef" might be rather >> useful as a user-level command. > > 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 set" as a separate type again, this plan for typedef would reduce the number of primitive concepts and axioms required to bootstrap HOL. Of course, axioms like mem_Collect_eq and Collect_mem_eq are rather uncontroversial, as axioms go. But if there is an easy way to avoid declaring these as axioms, then keeping them as axioms seems a bit gratuitous, in my opinion. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 (feat all your extensions) und simulating the one using axiomatized sets via composing Abs,Rep with the set-predicate-bijection. But as I said: I can deal with axiomatized set with only minor complications, so no indication here. Cheers, Andy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 "'a set" could be introduced definitionally using "pred_typedef". After type "'a set" has been defined, we can implement the "typedef" command, preserving its current behavior, as a thin wrapper on top of "pred_typedef". This approach would let us avoid having to axiomatize the 'a set type. Also, for those of us who like predicates, "pred_typedef" might be rather useful as a user-level command. What is gained from that apart from having two versions of typedef? We have had that very discussion around 1994, when Tobias thought that typedef could be a definitional primitive of Pure, but it turned out to be non-conservative outside of its special HOL-ish semantic fitting. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Thu, Aug 25, 2011 at 1:45 PM, Florian Haftmann 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 the isabelle_set repo, Hoare_Parallel should start working. Here's what happened: After a "clarify" step in a proof script, Isabelle yields a variable called "xb" (renamed from "x" to avoid clashes with pre-existing "x" and "xa"), while Isabelle_set calls the same variable "i". It turns out that the Isabelle_set is actually doing the right thing here. There is a goal of the form "x : (INT i:A. B i))", and clarify applies the rule INT_I. In Isabelle_set, the new variable name is inherited from the bound variable "i" in the goal. But in the current version, the subgoal ends up in the eta-expanded form "x : (%a. (INT i:A. B i) a)" and the name "i" doesn't get used. To summarize: eta-expansion is a problem. Eta-expansion seems to happen with induction (either from "induct" or "rule"), although the "eta-contract" pretty-printing option tries to prevent people from noticing (why does this option exist?!?) Switching to a separate set type greatly reduces the number of opportunities for unwanted eta-expansion. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 typedefs whenever non-emptiness of A is derivable, even using assumptions in the context. This is not really a problem, but complicates my conservativity argument. Before local typedefs the proof of (EX x. x : A) was global. Actually Makarius' attitude on this was that those non-emptiness proofs "should be global most of the time", but he didn't want to introduce a check. Cheers, Andy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On 08/26/2011 07:02 PM, Brian Huffman wrote: With ordinary "typedef", I have to do this: typedef (open) bar = "{x. is_bar x}" But then it generates rules of the wrong form: x : {x. is_bar x} ==> Rep_bar (Abs_bar x) = x Rep_bar x : {x. is_bar x} And I have to do an extra step to get the rules I want: lemmas Rep_bar' = Rep_bar [unfolded mem_Collect_eq] lemmas Abs_bar_inverse' = Abs_bar_inverse [unfolded mem_Collect_eq] Even with a transfer tool, the extra step would still be necessary. Predicate application corresponds to set-membership, so in apart from technicalities (which might be hard, no idea) I still don't see the problem. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 localized typedef is that it works by declaring a global typedef behind the scenes (much like a local definition of a polymorphic constant works by declaring a global polymorphic definition behind the scenes). Last time I looked local typedefs were primitive. Makarius? Actually I suggested exactly this treatment of local typedefs back in the day, so thanks for bringing this up. What am I missing here? Most importantly you are missing (indirectly) overloaded constants in representing sets of typedefs. E.g. typedef 'a matrix = {f . finite (nonzero_positions f) } depends on nonzero_positions, which depends on the overloaded constant zero['a]. If we try to transform this to HOL4-style typedef without (indirectly) overloaded constants, we have to abstract out a dictionary for zero['a], which would give rise to dependent typedefs. A solution is to eliminate such typedefs completely, replacing them by their representing sets, regarded as soft-types. This is an extremely non-trivial global theory-transformation. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Fri, Aug 26, 2011 at 9:43 AM, Andreas Schropp wrote: > On 08/26/2011 07:02 PM, Brian Huffman wrote: >> >> I didn't suggest the idea merely for your benefit. I think this >> approach would give Isabelle a nicer, simpler logical foundation. >> >> > > What is this logical foundation of Isabelle that you have in mind? > AFAIK I am the only trying to provide a semantics of any kind, > so please don't think me rude. I just think that having fewer primitive concepts and fewer axioms is generally preferable, that is all. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Fri, Aug 26, 2011 at 9:36 AM, Andreas Schropp 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 predicate > typedef? > That doesn't work because HOL4-style typedefs don't feature our extensions > to typedef and they are only conservative via a global theory > transformation. What exactly are our extensions to typedef? 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". My understanding of the localized typedef is that it works by declaring a global typedef behind the scenes (much like a local definition of a polymorphic constant works by declaring a global polymorphic definition behind the scenes). What am I missing here? - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On 08/26/2011 07:02 PM, Brian Huffman wrote: I didn't suggest the idea merely for your benefit. I think this approach would give Isabelle a nicer, simpler logical foundation. What is this logical foundation of Isabelle that you have in mind? AFAIK I am the only trying to provide a semantics of any kind, so please don't think me rude. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Fri, Aug 26, 2011 at 9:20 AM, Andreas Schropp wrote: > 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 primitive. I didn't suggest the idea merely for your benefit. I think this approach would give Isabelle a nicer, simpler logical foundation. >> Also, for those of us who like predicates, "pred_typedef" might be >> rather useful as a user-level command. >> > > Sets and predicates are isomorphic, so if my isomorphic transfer tool works > out I don't see why this is needed. I've often had situations where I wished I had a user-level "pred_typedef" command. Here's an example: datatype foo = ... definition is_bar :: "foo => bool" where ... Now I want to define a type "bar" such that: Rep_bar :: bar => foo Abs_bar :: foo => bar Abs_bar (Rep_bar x) = x is_bar x ==> Rep_bar (Abs_bar x) = x is_bar (Rep_bar x) With ordinary "typedef", I have to do this: typedef (open) bar = "{x. is_bar x}" But then it generates rules of the wrong form: x : {x. is_bar x} ==> Rep_bar (Abs_bar x) = x Rep_bar x : {x. is_bar x} And I have to do an extra step to get the rules I want: lemmas Rep_bar' = Rep_bar [unfolded mem_Collect_eq] lemmas Abs_bar_inverse' = Abs_bar_inverse [unfolded mem_Collect_eq] Even with a transfer tool, the extra step would still be necessary. On the other hand, a "pred_typedef" command could generate exactly the rules I want. The same "pred_typedef" command could also generate the same rules that "typedef" currently generates, simply by using a predicate of the form "%x. x : S". (This is how I expect the "typedef" wrapper could work.) - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 feature our extensions to typedef and they are only conservative via a global theory transformation. Or do you rather suggest having a predicate-based typedef with all our extensions? Cheers, Andy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 predicates. This would work just like the > new_type_definition facility of HOL4, etc. > > The type "'a set" could be introduced definitionally using "pred_typedef". > > After type "'a set" has been defined, we can implement the "typedef" > command, preserving its current behavior, as a thin wrapper on top of > "pred_typedef". > > This approach would let us avoid having to axiomatize the 'a set type. > Also, for those of us who like predicates, "pred_typedef" might be > rather useful as a user-level command. > > - Brian > > On Fri, Aug 26, 2011 at 12:06 AM, Lawrence Paulson wrote: >> 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-invented the >> notion of an image. >> Larry >> >> On 25 Aug 2011, at 23:24, Michael Norrish wrote: >> >>> 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 implementation needs set syntax / set type as prerequisite. Of course you could change »typedef« to be based on predicates, but there is some kind of unspoken agreement not to set one's hand on that ancient and time-honoured Gordon HOL primitive. >>> >>> HOL88, hol90, hol98 and HOL4 all have new_type_definition. This >>> principle takes a theorem of the form >>> >>> ?x. P x >>> >>> HOL Light takes a theorem of the form P x (removing the dependency on >>> the existential quantifier). >>> >>> To the best of my knowledge, none of these systems ever used sets in >>> this role. >>> >>> Michael >>> >>> >>> ___ >>> 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 >> > ___ > 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
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 primitive. Also, for those of us who like predicates, "pred_typedef" might be rather useful as a user-level command. Sets and predicates are isomorphic, so if my isomorphic transfer tool works out I don't see why this is needed. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 "'a set" could be introduced definitionally using "pred_typedef". After type "'a set" has been defined, we can implement the "typedef" command, preserving its current behavior, as a thin wrapper on top of "pred_typedef". This approach would let us avoid having to axiomatize the 'a set type. Also, for those of us who like predicates, "pred_typedef" might be rather useful as a user-level command. - Brian On Fri, Aug 26, 2011 at 12:06 AM, Lawrence Paulson wrote: > 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-invented the > notion of an image. > Larry > > On 25 Aug 2011, at 23:24, Michael Norrish wrote: > >> 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 implementation >>> needs set syntax / set type as prerequisite. Of course you could change >>> »typedef« to be based on predicates, but there is some kind of unspoken >>> agreement not to set one's hand on that ancient and time-honoured Gordon >>> HOL primitive. >> >> HOL88, hol90, hol98 and HOL4 all have new_type_definition. This >> principle takes a theorem of the form >> >> ?x. P x >> >> HOL Light takes a theorem of the form P x (removing the dependency on >> the existential quantifier). >> >> To the best of my knowledge, none of these systems ever used sets in >> this role. >> >> Michael >> >> >> ___ >> 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 > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 just now, which makes working very tiresome. > In ex/Set_Theory.thy, there is a non-terminating »force« proof, which is > a little bit worrying since I guess that one worked in Isabelle2007. > Maybe someone can inspect the history on that? If my memory is correct, this one worked in a reasonable amount of time on hardware of the late 1990s. But it isn't that surprising that later changes could interfere with its functioning when we restore the set type. I see that it does work with auto, but it's slow, thirty seconds or more. Larry On 25 Aug 2011, at 21:45, Florian Haftmann wrote: > I think it is best to leave the AFP aside for the moment and figure out > still existing problems in the distribution. According to my knowledge, > the following session produce problems: > > HOL-ex FAILED > HOL-Hoare_Parallel FAILED > HOL-Nominal FAILED > HOL-Library FAILED > HOL-Metis_Examples FAILED > HOL-MicroJava FAILED > HOL-Nitpick_Examples FAILED > HOL-Quotient_Examples FAILED > HOL-Predicate_Compile_Examples FAILED > HOL-Word-SMT_Examples FAILED > HOL-TPTP FAILED > HOL-Probability FAILED ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 various misunderstandings in printed texts. And of course there is still no fully formal theory of all the aspects that have been emphasized in the variety of HOL implementations. No offense: the last time we discussed these things you were introducing local typedefs directly instead of expressing them via global typedefs, which I told you is not exactly hard. It looks like you are more concerned with an easy implementation, leaving any matters of conservativity to me. I am not saying this is bad, but every time my transformation gets harder, I am not exactly feeling that "Makarius always cares about conservativity". ;D Maybe you want to start a realistic formalization yourself? This conservativity result that I am animating is a global theory transformation featuring replacement of certain typedefs by their representing sets, regarding them as soft types. If someone is interested I would indeed write this up, but given the complexity (I guess 3-4 pages of rule systems, without text) I don't think we can hope for a realistic formalization. BTW: Steven should get credit for seriously trying conservativity of overloading at least. This helped to expose the misconception, though he did not notice the problem. Also my write-up of the Isabelle-Kernel is 8 pages (of rule systems, without text!) and still incomplete, so I don't think we will ever manage to prove something important about Isabelle. I am even being generous here, excluding e.g. unification which is part of the trusted code (for speed I guess) but generates proof terms. In my eyes, the only reason we can claim to satisfy the deBruijn criterion is that proof-checking is much easier in ZF. From an LCF POV we are not really in game, because unification et al are trusted code. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Thu, 25 Aug 2011, Andreas Schropp wrote: Haha, very funny! We are a long distance from the "ancient HOL primitive" already: local typedefs, sort constraints on type parameters, overloaded constants in representation sets. Perhaps you remember there was quite a suprise regarding those "meta-safety" "proofs" that were once regarded as justification of Isabelle/HOL's extensions to HOL. These days it seems my translation is the only account of the generalized conservativity result that still holds. There are indeed many formal jokes concerning "typedef", which is in fact an axiomatization scheme that happens to with a certain semantic interpretation of HOL that was designed specifically to make it work. 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 various misunderstandings in printed texts. And of course there is still no fully formal theory of all the aspects that have been emphasized in the variety of HOL implementations. Maybe you want to start a realistic formalization yourself? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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-invented the notion of an image. Larry On 25 Aug 2011, at 23:24, Michael Norrish wrote: > 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 implementation >> needs set syntax / set type as prerequisite. Of course you could change >> »typedef« to be based on predicates, but there is some kind of unspoken >> agreement not to set one's hand on that ancient and time-honoured Gordon >> HOL primitive. > > HOL88, hol90, hol98 and HOL4 all have new_type_definition. This > principle takes a theorem of the form > > ?x. P x > > HOL Light takes a theorem of the form P x (removing the dependency on > the existential quantifier). > > To the best of my knowledge, none of these systems ever used sets in > this role. > > Michael > > > ___ > 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
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 implementation > needs set syntax / set type as prerequisite. Of course you could change > »typedef« to be based on predicates, but there is some kind of unspoken > agreement not to set one's hand on that ancient and time-honoured Gordon > HOL primitive. HOL88, hol90, hol98 and HOL4 all have new_type_definition. This principle takes a theorem of the form ?x. P x HOL Light takes a theorem of the form P x (removing the dependency on the existential quantifier). To the best of my knowledge, none of these systems ever used sets in this role. Michael signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 implementation needs set syntax / set type as prerequisite. If 'a set is introduced definitionally (as it were) this is fine for me, but if you axiomatize 'a set my setup in HOL->ZF gets slightly more complicated. So now I am slightly against this. ;D Of course you could change »typedef« to be based on predicates, but there is some kind of unspoken agreement not to set one's hand on that ancient and time-honoured Gordon HOL primitive. Haha, very funny! We are a long distance from the "ancient HOL primitive" already: local typedefs, sort constraints on type parameters, overloaded constants in representation sets. Perhaps you remember there was quite a suprise regarding those "meta-safety" "proofs" that were once regarded as justification of Isabelle/HOL's extensions to HOL. These days it seems my translation is the only account of the generalized conservativity result that still holds. Of course I am probably the only one that will ever care about these things, so whatever. ;D Rgds., Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 implementation needs set syntax / set type as prerequisite. Of course you could change »typedef« to be based on predicates, but there is some kind of unspoken agreement not to set one's hand on that ancient and time-honoured Gordon HOL primitive. Rgds., Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 exactly do you guys axiomatize 'a set? Sure it's admissable and all, but why not do this definitionally via the obvious typedef? BTW: I am pretty ambivalent about this endeavour, but 'a set might be beneficial when postprocessing results of the HOL->ZF translation. So good luck! Cheers, Andy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
Am 25.08.2011 um 22:45 schrieb Florian Haftmann: > HOL-Metis_Examples FAILED > HOL-Nitpick_Examples FAILED Adapting the Metis and Nitpick examples for a set constructor wouldn't be very difficult -- for Metis, it's mostly a matter of rerunning Sledgehammer to discover slightly different proofs if needed (or, worst case, comment out the offending examples), and for Nitpick it is just a technicality. I can look into those things if and when it is decided to move to sets. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 manage such a transition smoothly. Currently, we are (re-)separating predicates and sets syntactically, for three reasons: a) figure out whether and how it can be done b) how invasive this is c) improve quality and robustness of proofs where necessary. So, for the moment, the purpose of http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set is to provide a HOL image with a set type constructor as basis for further exploration. It is not meant as any kind of fork, which would weaken our resources. To prevent this, we must try hard to re-propagate proof improvements, duplication elimination etc. to the main repositories. If any substantial is missing (e.g. type class instances for set type constructor), it must be added to isabelle_set in a suitable manner, as is done already here: http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/893a53a63ba2#l10.42 http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/893a53a63ba2#l1.7 The remaining changes should be as little as possible; to be able to observe them, I organize isabelle_set that way that the last changeset is a merge of a genuine main isabelle revision with all the changes necessary to get HOL (and as many subsessions as possible) through. It is a challenge, with a limited time budget, to follow what is going on, and there is high chance I miss some question or similar. So, don't hesitate to ring the bell twice if you think your point got lost or you are stuck. In particular, I am currently not aware how much of the work on AFP theories has found its way back to the main repository or is still in the queue, and how big the discrepancies to a set-specific version still are. I think it is best to leave the AFP aside for the moment and figure out still existing problems in the distribution. According to my knowledge, the following session produce problems: HOL-ex FAILED HOL-Hoare_Parallel FAILED HOL-Nominal FAILED HOL-Library FAILED HOL-Metis_Examples FAILED HOL-MicroJava FAILED HOL-Nitpick_Examples FAILED HOL-Quotient_Examples FAILED HOL-Predicate_Compile_Examples FAILED HOL-Word-SMT_Examples FAILED HOL-TPTP FAILED HOL-Probability FAILED In ex/Set_Theory.thy, there is a non-terminating »force« proof, which is a little bit worrying since I guess that one worked in Isabelle2007. Maybe someone can inspect the history on that? Also Hoare_Parallel is non-terminating. Concerning the *_Examples session, assistance by the corresponding tool maintainers is necessary and appreciated. I guess HOL-Nominal, HOL-MicroJava, HOL-Probability are easily accessible sessions to tackle next. OK, so much to say on that topic by now. Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
> 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 specifications has drawbacks. * We try where we get if we reduce this. Whether this will ultimately result in a separte set type constructor is still an open question. All the best, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 knows better, tell me. It is probably easier to avoid TUM server infrastructure altogether, and use some existing hosting platform like https://bitbucket.org/ or even Google Code. Anyway, I am not sure what is gained from the extra efforts to produce some kind of set/pred fork of the whole system right now, as if there would be a hurry to prevent rethinking the whole effort further. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 designed from the ground upwards on the premise that sets and predicates were the same thing. I removed most of the duplication now in the main afp repos, which compiles again. I'll have a more closer look at these theories in the next days. Here are Larry's changesets, for reference: https://www4.in.tum.de/~krauss/hg/afp-set-GraphMarking-paulson/ Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 > well... > > (but maybe you already did this???) concerning Complete_Lattice, of course: http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/893a53a63ba2#l1.7 > Can you send me a bundle of your changes, so that I can put them on the > web for people to look at? > > - hg ci # commit your changes locally > - hg bundle SOME_FILENAME http://afp.hg.sourceforge.net/hgweb/afp/afp/ > - send me the file SOME_FILENAME, created in the previous step > > The second command will produce a file which contains all your > changesets that are not in the central afp repos (i.e., your new changes). I confess our infrastructure at the moment is not that good. When there is time, I will allocate an afp_set repository beside the isabelle_set one. 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 knows better, tell me. So the tool of choice would be that each involved in that story to set up his own repositories and publish them by HTTP. Then we can pull each other's changesets. Are there any obstacles? Cheers, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
> 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 (I refer to Florian's version of HOL), which is imported > by Main, which is indirectly imported by Diagram. And just in case I was > mistaken on this last point, I modified Diagram to import Main explicitly, > just to be sure. This instance declaration is still necessary. print_classes should give sufficient data to find out what is going here. The duplication is the same I was referring to a few days ago: > Complete_Lattices.thy > and > http://afp.hg.sourceforge.net/hgweb/afp/afp/file/dce6fbc4d6c0/thys/DataRefinementIBP/Preliminaries.thy > (btw. it took me considerable time to figure out how the class hierarchy > for complete lattices should look like, just to see now that somebody > else got to the same conclusion independently already). Indeed the classes in DataRefinement are duplication of work now in Complete_Lattice.thy and have already been marked by Brian as such. Logically they are equivalent and can be removed. Hope this helps, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
> 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: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 premise that sets and predicates were the same thing. Larry On 23 Aug 2011, at 22:24, Alexander Krauss wrote: > 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 well... > > (but maybe you already did this???) ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 version of Isabelle. Only where this is possible. The purpose of all this work is to see where it is not possible and find out why. After all, these issues may point to difficulties that users will later experience with the change as well. I'm not sure that's possible. I got DataRefinementIBP working with the set-version, but now it doesn't work with the standard version. For one thing, it needs a class declaration for type set, which obviously cannot work with the standard version, 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 well... (but maybe you already did this???) but other proofs also fail to work with the standard version. I'd like to (and others probably too) look at those proofs. Is there anything fundamental hidden there??? Can you send me a bundle of your changes, so that I can put them on the web for people to look at? - hg ci # commit your changes locally - hg bundle SOME_FILENAME http://afp.hg.sourceforge.net/hgweb/afp/afp/ - send me the file SOME_FILENAME, created in the previous step The second command will produce a file which contains all your changesets that are not in the central afp repos (i.e., your new changes). I'll put it up somewhere where people can look at it... Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Mon, Aug 22, 2011 at 8:01 AM, Lawrence Paulson 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: > > 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 (I refer to Florian's version of HOL), which is imported > by Main, which is indirectly imported by Diagram. And just in case I was > mistaken on this last point, I modified Diagram to import Main explicitly, > just to be sure. This instance declaration is still necessary. > > I just don't get this. I thought that an instance declaration lasted for ever. DataRefinementIBP/Preliminaries.thy contains the following line: class complete_boolean_algebra = distributive_complete_lattice + boolean_algebra So your instance proof above is for class Preliminaries.complete_boolean_algebra, while the instance in Complete_Lattice.thy is for the separate Complete_Lattice.complete_boolean_algebra class. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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: 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 (I refer to Florian's version of HOL), which is imported by Main, which is indirectly imported by Diagram. And just in case I was mistaken on this last point, I modified Diagram to import Main explicitly, just to be sure. This instance declaration is still necessary. I just don't get this. I thought that an instance declaration lasted for ever. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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: "(\x. R x x) \ symp R \ transp R \ part_equivp R" apply (simp add: part_equivp_def) -- {* (I) "sane" proof state *} apply auto -- {* (II) "insane" proof state *} apply (auto elim: sympE transpE) -- {* (III) does not even terminate; adding "simp add: mem_def" succeeds! *} The second »auto« imposes a »\« on predicates, although mem_def, Collect_def or similar do not appear in the proof text (push to the »wrong world«). Worse, the final auto does not even terminate, this is what I had in mind when referring to an enlarged search space. Here, the way the system is build forces me to use »simp add: mem_def«. Thanks for clarifying. This is a very good example. In essence, it boils down to this: lemma "(A :: 'a => bool) = B" apply (rule) (* subset_antisym, introduces set connectives *) I have predicates in mind (and in the context, A and B may be used as predicates), but this is not visible from the goal state, which contains only equality. Then, the system will apply subset_antisym, which is incorrect. subset_antisym is declared [intro!], so this happens with auto, too. Then the user has no choice but unfold mem_def, to get back into a sane state. So I would say this is not so much about search space but about the fact that automated tools actually need the proper type information to behave correctly! * The logical identification of sets and predicates prevents some reasonable simp rules on predicates: e.g. you cannot have (A |inf| B) x = A x& B x because then expressions like "set xs |inter| set ys" behave strangely if the are eta-expanded (e.g. due to induction). This sounds more like a problem with the underlying infrastructure that should be fixed, rather than working around the problem by introducing new type constructors. Can you give an example of a proof by induction, where eager eta expansion leads to an unnecessarily complicated proof? theory Scratch imports Main "~~/src/HOL/Library/Lattice_Syntax" begin declare List.set_append [simp del] thm sup_apply declare sup_apply [simp] lemma set_append: "set (xs @ ys) = (set xs \ set ys)" apply (induct xs) apply simp_all apply auto -- {* non-termination! *} Nice example again. Actually, there's a fundamental inconsistency in the current setup in that some operations (like Un) are identified with the lattice operations, where as other operations like membership or comprehension are syntactically distinct. So whenever only connectives of the first kind occur in the goal, the automation can apply rules of both types, which possibly "specializes" the type to one of the two variants. Looks pretty much that one cannot really do without the type information... I wonder if similar effects can occur in other HOLs... The current implementation of subtyping allows to declare only one map function for a type constructor. Thus, we can have either the contravariant or the covariant map for the function type, but not both at the same time. The introduction of set as an own datatype would resolve this issue. This is an interesting oberservation which also applies to the instantiation of sets for type classes: in 'a => bool, you have to think about 'a in a contravariant fashion, whereas in 'a set it is covariant. The situation in monotonicity checking (as part of Nitpick) is exactly this covariant vs. contravariant issue. We resolved it by re-inferring the whole thing. So, from subtyping point of view, sets and predicates are really two different beasts... Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 is no guarantee > that all the people who talked about "sets vs. functions" meant, or needed, > the same thing! > 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, having good old 'a set back is does > not fully solve this problem as a whole, just one (important) instance of it. > My view on this whole topic is outlined in the report I recently sent around > (http://www4.in.tum.de/~krauss/papers/refinement.pdf, not updated since last > time). In the long run, I would prefer to see flexible transport machinery to > move stuff between isomorphic types. It is important to note that the motivation to have set back again as a type constructor is not code generation itself, but fundamental flaws in the current situation. Indeed I fully agree that the driving force behind the development should always be specification and proof, with derived application at a secondary level. Also in our case, code generation is a side effect, although many technical points of this discussion here are related to code generation, I guess mainly since a couple of people involved in this story actually want to see progress here. What is a different – and in itself valuable – thing is the matter of »transport« mentioned by Alex, something which also I am eager to see one day. But now back to sets. In answer to some statements made, I have collected evidence why the current situation indeed is problematic: > 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 unfolding this definition. You wouldn't unfold the definitions of > logical operators like "conj" or "disj" either, except for proving > introduction- or elimination rules for these operators. > Can this claim be made more concrete (or even quantitative)? Or is it merely > a conjecture? > From what Jasmin wrote, this does not seem to hold for sledgehammer, and > simp/auto/blast should not run into the "wrong world" when configured > properly. > I understand that this is true for naive users... but automated tools??? > So your point is actually a different one from Florian's: Users unfold > mem_def in order to gain automation, which may work in that moment, but is > usually a bad idea later on. I understand this point. > (Aside: It would be interesting to explore why users actually do this. Is > there something missing in the automation for sets that works better for > predicates?) > My understanding of Florian's point above was that sets-as-predicates > actually hinder automation by enlarging the search space. But it seems to me > that this is only a theoretical consideration, and that we do not actually > observe this effect in practice. 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: "(\x. R x x) \ symp R \ transp R \ part_equivp R" apply (simp add: part_equivp_def) -- {* (I) "sane" proof state *} apply auto -- {* (II) "insane" proof state *} apply (auto elim: sympE transpE) -- {* (III) does not even terminate; adding "simp add: mem_def" succeeds! *} The second »auto« imposes a »\« on predicates, although mem_def, Collect_def or similar do not appear in the proof text (push to the »wrong world«). Worse, the final auto does not even terminate, this is what I had in mind when referring to an enlarged search space. Here, the way the system is build forces me to use »simp add: mem_def«. (Well, joking you could also argue that there are three thing which LISP, Java and Isabelle have in common: strange syntax, not writable without special tool support, choking as soon as higher-order things come in.) >> * The logical identification of sets and predicates prevents some >> > reasonable simp rules on predicates: e.g. you cannot have (A |inf| B) x >> > = A x & B x >> > because then expressions like "set xs |inter| set ys" behave strangely >> > if the are eta-expanded (e.g. due to induction). > This sounds more like a problem with the underlying infrastructure that should > be fixed, rather than working around the problem by introducing new type > constructors. > Can you give an example of a proof by induction, where eager eta expansion > leads > to an unnecessarily complicated proof? theory Scratch imports Main "~~/src/HOL/Library/Lattice_Syntax" begin declare List.
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On 08/19/2011 07:06 AM, Tobias Nipkow wrote: I think he omitted to mention type classes. It comes up again and again on the mailing list. Really? Yes. You yourself discovered right away that you cannot just treat a set like a predicate in this respect: set_plus: "A + B == {c. EX a:A. EX b:B. c = a + b}" func_plus: "f + g == (%x. f x + g x)" See the emails that Alex sent around recently. We gave up on set_plus. Ok, this (and set_times, which is similar) is the only instance that I knew about, from the old thread. At the time, we concluded that this one wasn't really so important, and I think I would still come to the same conclusion today: The difference between the current version and the old version (http://isabelle.in.tum.de/repos/isabelle/file/878c37886eed/src/HOL/Library/SetsAndFunctions.thy) is mostly notational (we still get the monoid lemmas by a locale interpretation), and even the type class version is not fully satisfactory compared with mathematical practice, where one would also ad-hoc-overload + to write x + A, which has to be x +o A in Isabelle. Later, people wanted to do just that more than once. Here is one instance: http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/1689/focus=1697 There are others. I wonder if there are also *different* instances, where we actually want "set" to be an instance of some type class, which cannot be achieved using "fun" and "bool". It seems that in 2008, no other instances had to be given up, but maybe new opportunities for use of classes arised after that? HOLCF? Multivariate_Analysis? My gut feeling is that there must be such cases, but I'd be much more confident if somebody actually showed me a few. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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. Can this claim be made more concrete (or even quantitative)? Or is it merely a conjecture? From what Jasmin wrote, this does not seem to hold for sledgehammer, and simp/auto/blast should not run into the "wrong world" when configured properly. I understand that this is true for naive users... but automated tools??? 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 predicates) works often enough that people like it and overuse it. Sooner or later you will see unfolding of mem_def. As opposed to unfolding conjunction, unfolding mem_def proves things that otherwise simp/auto/etc fail on. So your point is actually a different one from Florian's: Users unfold mem_def in order to gain automation, which may work in that moment, but is usually a bad idea later on. I understand this point. (Aside: It would be interesting to explore why users actually do this. Is there something missing in the automation for sets that works better for predicates?) My understanding of Florian's point above was that sets-as-predicates actually hinder automation by enlarging the search space. But it seems to me that this is only a theoretical consideration, and that we do not actually observe this effect in practice. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 are often specified in terms of functions (finite maps, almost constant maps, etc.). Thus, having good old 'a set back is does not fully solve this problem as a whole, just one (important) instance of it. My view on this whole topic is outlined in the report I recently sent around (http://www4.in.tum.de/~krauss/papers/refinement.pdf, not updated since last time). In the long run, I would prefer to see flexible transport machinery to move stuff between isomorphic types. Hi Alex, 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 more suitable for code generation. Having a separate type set is more not less abstract. Just like LISP is not more abstract than ML. It allows us to regain a few important things we lost. Sets as predicates are indeed more concise (you don't need {x. P x} and %x. x : S), but this is just a matter of degree, not a complete loss of some feature. If we could freely mix sets and predicates as we had hoped, it would be different. But proof support is lacking. Not just in Isabelle/HOL, but Michael Norrish tells me that in HOL4 it is also better not to mix sets and predicates if you want proof automation. For example, HOL/MicroJava/DFA/Kildall.thy uses the SOME operator to select an element from the worklist, which is highly non-executable but more abstract, since one does not have to commit to a particular strategy for selecting the element. This is a misunderstanding. The SOME operator *does* commit to a particular strategy, but we do not know which one. Which means that we can never prove it equivalent to any strategy. SOME is both abstract and concrete in a way that defeats implementation. Andreas Lochbihler and I elaborate on this topic in our recent paper for the ITP, cf. http://pp.info.uni-karlsruhe.de/publication.php?id=lochbihler11itp (page 14) We present some solutions for code generation when using underspecification. Put simply, the message is: Do not use Hilbert's choice if you want to obtain an executable specification. Of course, handling underspecification is an orthogonal issue to the subject of this thread. Lukas Tobias Greetings, Stefan ___ 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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) * (expr * state)) set", and turning it into a 4-ary predicate (expr => state => expr => state => bool) would cause problems with either version of the transitive closure operator. [Btw, the newer HOL/IMP/Small_Step.thy uses a binary predicate over pairs, which requires massaging the induction rule using [split_format (complete)]]. Hi all, let me take the opportunity to advertise a useful feature of the induct method that avoids such manual "massaging" of induction rules. For example, the command proof(induct rule: small_step_induct) in HOL/IMP/Types.thy can be replaced by proof(induct "(c,s)" "(c',s')" arbitrary: c s c' s' rule: small_step.induct) which allows the standard induction rule small_step.induct to be used instead of the small_step_induct rule produced using split_format, which is a bit of a hack anyway. The above is a shorthand for proof(induct x=="(c,s)" y=="(c',s')" arbitrary: c s c' s' rule: small_step.induct) Since revision b0aaec87751c (Jan 2010), the equational constraints arising from such invocations of induct are solved automatically using injectivity / distinctness rules for datatypes, so the rest of the proof script works as if the custom-made induction rule had been applied. Hi Stefan, In most cases, the advertised feature of the induct method does the job to avoid manual massaging of the induction rule, as you outlined in your mail. But in certain cases, the features of the induct method do not supersede the massaging, e.g. with split_format. Consider the following example: inductive R :: "('a * 'b) => ('a * 'b) => bool" where "R x y ==> R y z ==> R x z" lemma "R (a, b) (c, d) ==> True" proof (induct "(a, b)" "(c, d)" rule: R.induct) oops lemmas R_induct = R.induct[split_format (complete)] lemma "R (a, b) (c, d) ==> True" proof (induct rule: R_induct) oops In the first case, you obtain a free variable y of pair type, and usually it requires to obtain y's components within the proof step, there is no possibility to get this splitting with the induct method right now. Using split_format enables this splitting, as you can see in the second example. This drawback actually stopped us integrating the method for doing "more automatic" rule inductions, which we discussed offline last Christmas. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 types to coercions between type constructors. E.g. "nat list" is subtype of "int list" with the coercion "map int", provided that "int" is declared as a coercion and "map" as map function for "'a list". This is a typical example of a covariant map function (i.e. the lifting does not invert the direction of the subtype relation). On the other hand, the generic map function for "'a => 'b" ("% f g h x. g (h (f x)) :: ('a => 'b) => ('c => 'd) => ('b => 'c) => ('a => 'd)") is contravariant in the first argument. Concretely that means that "int => bool" is a subtype of "nat => bool", provided the above map function and the coercion "int". In contrast, the corresponding map function for sets as predicates ("image :: ('a => 'b) => ('a => bool) => ('b => bool)") is, as one would expect, covariant in the first argument. The current implementation of subtyping allows to declare only one map function for a type constructor. Thus, we can have either the contravariant or the covariant map for the function type, but not both at the same time. The introduction of set as an own datatype would resolve this issue. Cheers, Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 > predicates) works often enough that people like it and overuse it. Sooner or > later you will see unfolding of mem_def. As opposed to unfolding conjunction, > unfolding mem_def proves things that otherwise simp/auto/etc fail on. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 (finite maps, almost constant maps, etc.). Thus, >> having good old 'a set back is does not fully solve this problem as a >> whole, just one (important) instance of it. >> >> My view on this whole topic is outlined in the report I recently sent >> around (http://www4.in.tum.de/~krauss/papers/refinement.pdf, not updated >> since last time). In the long run, I would prefer to see flexible >> transport machinery to move stuff between isomorphic types. > > Hi Alex, > > 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 more suitable for code generation. Having a separate type set is more not less abstract. Just like LISP is not more abstract than ML. It allows us to regain a few important things we lost. Sets as predicates are indeed more concise (you don't need {x. P x} and %x. x : S), but this is just a matter of degree, not a complete loss of some feature. If we could freely mix sets and predicates as we had hoped, it would be different. But proof support is lacking. Not just in Isabelle/HOL, but Michael Norrish tells me that in HOL4 it is also better not to mix sets and predicates if you want proof automation. > For example, > HOL/MicroJava/DFA/Kildall.thy uses the SOME operator to select an element > from the worklist, which is highly non-executable but more abstract, since > one does not have to commit to a particular strategy for selecting the > element. This is a misunderstanding. The SOME operator *does* commit to a particular strategy, but we do not know which one. Which means that we can never prove it equivalent to any strategy. SOME is both abstract and concrete in a way that defeats implementation. Tobias > Greetings, > Stefan > ___ > 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
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 pain, apart from what Florian already mentioned? >> >> I think he omitted to mention type classes. It comes up again and again >> on the mailing list. > > Really? Yes. You yourself discovered right away that you cannot just treat a set like a predicate in this respect: set_plus: "A + B == {c. EX a:A. EX b:B. c = a + b}" func_plus: "f + g == (%x. f x + g x)" See the emails that Alex sent around recently. We gave up on set_plus. Later, people wanted to do just that more than once. Here is one instance: http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/1689/focus=1697 There are others. Tobias > > http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/260/ > > cited by Brian and Alex, Brendan was worried about the fact that one could > no longer declare arities for sets. In my reply to his mail, I pointed > out that arities for sets could usually be rephrased as arities for functions > and booleans. I also asked him to give a concrete example for an arity where > this was not possible, but I never got a reply, so I assume that this is not > so much of a problem. > > Greetings, > Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 more pain, apart from what Florian already mentioned? >> >> I think he omitted to mention type classes. It comes up again and again >> on the mailing list. > > Really? In the thread > > http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/260/ > > cited by Brian and Alex, Brendan was worried about the fact that one could > no longer declare arities for sets. In my reply to his mail, I pointed > out that arities for sets could usually be rephrased as arities for functions > and booleans. I also asked him to give a concrete example for an arity where > this was not possible, but I never got a reply, so I assume that this is not > so much of a problem. Given his employer Brendan not giving an example is no real indication either way ;-) I'm not convinced that any class that works for sets can be expressed nicely as a class on the function type and booleans. Splitting up the declaration over two types at least makes it hard to think about. You're right, though, that it may be less of a problem than we currently have the feeling it is. It hasn't prevented anything yet that we wanted to do at NICTA. Should we ask a wider audience (isabelle-users) if anybody else has good reasons against/for a change? Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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«, making >> vain proof attempts lasting longer instead just failing. > > Can this claim be made more concrete (or even quantitative)? Or is it merely > a conjecture? > > From what Jasmin wrote, this does not seem to hold for sledgehammer, and > simp/auto/blast should not run into the "wrong world" when configured > properly. > > I understand that this is true for naive users... but automated tools??? 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 predicates) works often enough that people like it and overuse it. Sooner or later you will see unfolding of mem_def. As opposed to unfolding conjunction, unfolding mem_def proves things that otherwise simp/auto/etc fail on. Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 unfolding this definition. You wouldn't unfold the definitions of logical operators like "conj" or "disj" either, except for proving introduction- or elimination rules for these operators. > * The logical identification of sets and predicates prevents some > reasonable simp rules on predicates: e.g. you cannot have (A |inf| B) x > = A x & B x > because then expressions like "set xs |inter| set ys" behave strangely > if the are eta-expanded (e.g. due to induction). This sounds more like a problem with the underlying infrastructure that should be fixed, rather than working around the problem by introducing new type constructors. Can you give an example of a proof by induction, where eager eta expansion leads to an unnecessarily complicated proof? Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 more suitable for code generation. 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 is no guarantee that all the people who talked about "sets vs. functions" meant, or needed, the same thing! For Nitpick (and code generation I guess), it helps to know whether a predicate is a finite set or not. However, we can't expect the entire world to understand "'a set" as a finite set built from {} by adding elements one by one -- and what's the type constructor for the complement of such a set anyway? For Nitpick, Alex and I solved the problem generally by inferring "finite sets" as well as "complements of finite sets" in addition to plain functions [1, sect. 6]. Needless to say, we're in better shape with our robust inference than by just crossing our fingers, hoping that the user distinguishes between "'a set" and "'a => bool" the way we intend to. Jasmin [1] http://www4.in.tum.de/~blanchet/jar2011-mono.pdf ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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? > > I think he omitted to mention type classes. It comes up again and again > on the mailing list. Really? In the thread http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/260/ cited by Brian and Alex, Brendan was worried about the fact that one could no longer declare arities for sets. In my reply to his mail, I pointed out that arities for sets could usually be rephrased as arities for functions and booleans. I also asked him to give a concrete example for an arity where this was not possible, but I never got a reply, so I assume that this is not so much of a problem. Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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, > having good old 'a set back is does not fully solve this problem as a > whole, just one (important) instance of it. > > My view on this whole topic is outlined in the report I recently sent > around (http://www4.in.tum.de/~krauss/papers/refinement.pdf, not updated > since last time). In the long run, I would prefer to see flexible > transport machinery to move stuff between isomorphic types. Hi Alex, 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 more suitable for code generation. For example, HOL/MicroJava/DFA/Kildall.thy uses the SOME operator to select an element from the worklist, which is highly non-executable but more abstract, since one does not have to commit to a particular strategy for selecting the element. Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
Am 18.08.2011 um 21:40 schrieb 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...? Sounds like a good idea, but make sure also to remove the following lines in "sledgehammer_filter.ML": (* Set constants tend to pull in too many irrelevant facts. We limit the damage by treating them more or less as if they were built-in but add their definition at the end. *) val set_consts = [(@{const_name Collect}, @{thms Collect_def}), (@{const_name Set.member}, @{thms mem_def})] And (effectively) replace "set_consts" with the empty list, ideally simplifying the code as you go. This will degrade the quality of the relevance filtering slightly, but would have to be done anyway when "'a set" is reintroduced. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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", and turning it into a 4-ary predicate (expr => state => expr => > state => bool) would cause problems with either version of the > transitive closure operator. [Btw, the newer HOL/IMP/Small_Step.thy > uses a binary predicate over pairs, which requires massaging the > induction rule using [split_format (complete)]]. Hi all, let me take the opportunity to advertise a useful feature of the induct method that avoids such manual "massaging" of induction rules. For example, the command proof(induct rule: small_step_induct) in HOL/IMP/Types.thy can be replaced by proof(induct "(c,s)" "(c',s')" arbitrary: c s c' s' rule: small_step.induct) which allows the standard induction rule small_step.induct to be used instead of the small_step_induct rule produced using split_format, which is a bit of a hack anyway. The above is a shorthand for proof(induct x=="(c,s)" y=="(c',s')" arbitrary: c s c' s' rule: small_step.induct) Since revision b0aaec87751c (Jan 2010), the equational constraints arising from such invocations of induct are solved automatically using injectivity / distinctness rules for datatypes, so the rest of the proof script works as if the custom-made induction rule had been applied. Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 instead just failing. Can this claim be made more concrete (or even quantitative)? Or is it merely a conjecture? From what Jasmin wrote, this does not seem to hold for sledgehammer, and simp/auto/blast should not run into the "wrong world" when configured properly. I understand that this is true for naive users... but automated tools??? * The logical identification of sets and predicates prevents some reasonable simp rules on predicates: e.g. you cannot have (A |inf| B) x = A x& B x because then expressions like »set xs |inter| set ys« behave strangely if the are eta-expanded (e.g. due to induction). * The missing abstraction for sets prevents straightforward code generation for them (for the moment, the most pressing, but not the only issue). 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, having good old 'a set back is does not fully solve this problem as a whole, just one (important) instance of it. My view on this whole topic is outlined in the report I recently sent around (http://www4.in.tum.de/~krauss/papers/refinement.pdf, not updated since last time). In the long run, I would prefer to see flexible transport machinery to move stuff between isomorphic types. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study
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 look into it as well. Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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...? Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 summer. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
envisaged working plan -- a) general * continue discussion about having set or not, end with a summary (for the mailing list archive) * provide repository http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/ with newest changesets from Isabelle main repository, keep HOL image building (Florian) * figure out with type class instances for set to add (maybe as a provisory in a separate theory) > grep -rIPn '(instantatiation|instance).*(bool|"fun").*::' src/HOL * examine changesets e8cc166ba123 to ec46381f149d for changes done to packages etc., from there distill/assert necessary back-changes to inductive_set etc. b) elimination of set/pred mixture * backport admissible changes from isabelle_set to isabelle (Florian) * eliminate occurences of mem_set and Collect_def in distribution and AFP theories AFAP, propagate back to main repository * figure out problem with »force« in ex/Set_Theory.thy * figure out problem with »refute« in ex/Refute_Examples.thy with "distinct [a, b]" (examine changes done to refute since 2008) c) consolidation * get isabelle_set running * (maybe) > hide_fact (open) Set.mem_def Set.Collect_def to indicate that something is going on with these d) RELEASE e) introduce set type constructor * backport necessary changes (as little invasive as possible) from isabelle_set * distribute type class instances for set over theories appropriately * add naive code generator setup for sets in Set.thy * drop theory Executable_Set * drop optional special type alias treatment in Pure/Isar/code.ML (Florian) * drop theory CSet (naive version, maybe not quotient version) * mark _apply rules for pointwise operations on functions as [simp] * provide theories Dlist_Set, RBT_Set (or maybe Mapping_Set), etc. Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 compatibility/import issue mentioned by > Brian), and at least myself I wouldn't feel comfortable answering this > question just now... For Sledgehammer, reverting would be a (fairly) small loss. At the ATP level, types are erased (or encoded), and it doesn't really matter if something is a "'a set" or a "'a => bool". Higher-order functions and predicates are translated as simple values of the universe, and when they are applied this is done using an explicit operator called "hAPP". Apart from the order of the arguments, there is no difference between "hAPP" and "Set.member". Hence, the main difference to the ATPs is whether we have "mem_def"/"Collect_def" to bridge the two worlds or the weaker "mem_Collect_def". "mem_def" and "Collect_def" seem more flexible in that respect, and it's no coincidence that several "metis" calls with one or the other were found when reintroducing "'a set". (On the other hand, one could argue that "mem_def"/"Collect_def" are more useful to prove things today in the current state of mismatch, cf. "Multivariate_Analysis", than they would have been a few years ago right after the elimination of "'a set".) Sledgehammer and Metis also have a flag that preprocesses away all "member" and "Collect" before doing the proof search. For Sledgehammer, the success rate for a single prover went up by about .5% -- which is good but not fantastic. This option is still off by default because it needs a more thorough evaluation and it broke at least one Metis proof (for no deep reason, except what I'd call "a failure to perform"). For Nitpick, reintroducing sets wouldn't make any difference in terms of performance one way or the other, since "'a set" and "'a => bool" are isomorphic and hence as many bits are required to code one or the other. I would need to spend some time to make Nitpick (and Refute) work smoothly, though, and there are many more urgent things on my plate, so don't hold your breath. My personal gut feeling is that if we are to have "Collect" and "member" at all, then it might be just as well that we keep them separated from the rest using type discipline, to catch various stylistic horrors. But beyond from this I'm not leaning one way or another. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 been introduced after 2008, but maybe Cezary can > comment on this. Hi Florian, I already made the changes to the core of the quotient package as of: http://isabelle.in.tum.de/repos/isabelle/rev/3cdc4176638c With the above the quotient package works both as is and with the explicit set type. It seems you included only a part of the above changeset in the isabelle_set repository, in particular the change in the src/HOL/Equiv_Relations.thy is necessary but seems it did not go in. With this change the quotient package works and only changes to the particular examples may be needed, but many work without any changes: New Nominal: Works. Quotient_Message: Works. Quotient_Int: Works. FSet: Requires removing one 'simp add: mem_def', then works. DList: I pushed a change 5 min ago; with it it works. CSet and List_Cset depend on Library/More_Set which doesn't load, so I can't say if there are any quotient issues... AFP/Coinductive needs updating, long before quotients it does: enat_set :: "enat => bool" so I can't say without going further in the code. Regards, Cezary. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study
Am 18.08.2011 um 09:18 schrieb Florian Haftmann: > Strange. I guess refute was not modified in 2008 (at least according to > hg diff -r e8cc166ba123 -r ec46381f149d | grep -i refute). Maybe this > crept in silently over the last years? It was not modified in 2008, but it was modified in 2009. It wasn't using antiquotation, so its support for "set"s was just hanging around dead. If you look more closely at the history, you'll see what needs to be reverted. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study
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 CASC, where it performs very well. Without Refute, we'd have only two systems (including Satallax) in the higher-order model finding division and there would be no competition. 2. On several occasions Refute has founds models that escaped Nitpick, usually pointing at bugs in Nitpick. 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. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study
Hi Brian, thanks for the excellent work you are doing. >> HOL-ex FAILED > I looked into this, and as far as I can tell, there are two theories > left that have problems. > > First, ex/Refute_Examples.thy raises exception REFUTE on line 113: > lemma "distinct [a,b]" refute Strange. I guess refute was not modified in 2008 (at least according to hg diff -r e8cc166ba123 -r ec46381f149d | grep -i refute). Maybe this crept in silently over the last years? @list: btw. what is the status of »refute« in general? Is it supposed to be superseded by nitpick entirely? > Second, ex/set.thy freezes on the "force" methods from lines 180 and 197: > lemma "a < b & b < (c::int) ==> EX A. a ~: A & b : A & c ~: A" by force > lemma "(ALL u v. u < (0::int) --> u ~= abs v) > --> (EX A::int set. (ALL y. abs y ~: A) & -2 : A)" by (simp add: > abs_if, force) Similar strange. The history http://isabelle.in.tum.de/repos/isabelle/log/355d5438f5fb/src/HOL/ex/set.thy does not exhibit any clues that something went utterly wrong. >> Possible showstoppers: >> src/HOL/Library/Cset.thy > This one requires a design decision: What should the type of the > "member" function be? It could be either "'a Cset.set => 'a set" or > "'a Cset.set => 'a => bool". Similarly, "Set" could be either "'a set > => 'a Cset.set" or "('a => bool) => 'a Cset.set". member :: 'a Cset.set => 'a => bool Set :: ('a => bool) => 'a Cset.set Eventually Cset.thy should disappear of course. >> src/HOL/Nominal/Nominal.thy > I have done some playing around with this, but the required changes > include class instances for the "set" type, and so they cannot be > merged back into the main distribution. >> A glimpse at the AFP: > >> thys/Shivers-CFA/ExCFSV.thy >> thys/Shivers-CFA/HOLCFUtils.thy > Updating this one will require class instances for the "set" type; the > changes are not backward compatible. Maybe, as intermediate solution, these instances can be provided in a separate theory in the isabelle_set repository? Which one to add should be obvious from the 2008 changesets, or maybe we can even inspect instances for _ => _ and bool and derive the possible set instances from there. Cheers, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study
On Wed, Aug 17, 2011 at 11:51 AM, Florian Haftmann wrote: > HOLCF-Library FAILED Fixed: http://isabelle.in.tum.de/repos/isabelle/rev/c478cd500dc4 > HOL-Bali FAILED > HOL-Decision_Procs FAILED > HOL-Induct FAILED > HOL-Subst FAILED > HOL-NanoJava FAILED Fixed: http://isabelle.in.tum.de/repos/isabelle/rev/b922e91dd1d9 > HOL-Multivariate_Analysis FAILED Fixed: http://isabelle.in.tum.de/repos/isabelle/rev/7784fa3232ce > HOL-IMP FAILED Fixed: http://isabelle.in.tum.de/repos/isabelle/rev/e44f465c00a1 > HOL-ex FAILED I looked into this, and as far as I can tell, there are two theories left that have problems. First, ex/Refute_Examples.thy raises exception REFUTE on line 113: lemma "distinct [a,b]" refute Second, ex/set.thy freezes on the "force" methods from lines 180 and 197: lemma "a < b & b < (c::int) ==> EX A. a ~: A & b : A & c ~: A" by force lemma "(ALL u v. u < (0::int) --> u ~= abs v) --> (EX A::int set. (ALL y. abs y ~: A) & -2 : A)" by (simp add: abs_if, force) > Possible showstoppers: > src/HOL/Library/Cset.thy This one requires a design decision: What should the type of the "member" function be? It could be either "'a Cset.set => 'a set" or "'a Cset.set => 'a => bool". Similarly, "Set" could be either "'a set => 'a Cset.set" or "('a => bool) => 'a Cset.set". > src/HOL/Nominal/Nominal.thy I have done some playing around with this, but the required changes include class instances for the "set" type, and so they cannot be merged back into the main distribution. > A glimpse at the AFP: > thys/Shivers-CFA/ExCFSV.thy > thys/Shivers-CFA/HOLCFUtils.thy Updating this one will require class instances for the "set" type; the changes are not backward compatible. > thys/Presburger-Automata/Presburger_Automata.thy > thys/Presburger-Automata/DFS.thy Fixed: http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/b8be79162da4 > thys/SIFPL/VS.thy > thys/SIFPL/VS_OBJ.thy > thys/SIFPL/HuntSands.thy Fixed: http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/8d44eafb4517 - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
[forgot to answer in particular] > inquit Brian: >> As long as we put off reintroducing 'a set as a separate type, we will >> continue to accumulate more theories (like Multivariate_Analysis) that >> confuse sets and predicates. The job of introducing 'a set will only >> get more difficult the longer we wait. I would certainly like to see >> the job completed before the next release, although it might require >> more time than we have. I feel sympathetic with that concern, but I do not view that so critical: according to what is currently going on in the repository, now many contributors are aware to avoid set/pred mixture, and even so have a personal interest to have the set type constructor back. For the black matter outside there, the introduction of the set type constructor is invasive anyway. Cheers, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study
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 proper history to be taken over finally! Currently makeall says: HOL-ex FAILED HOL-Decision_Procs FAILED HOL-Nominal FAILED HOL-Bali FAILED HOL-Hoare_Parallel FAILED HOLCF-Library FAILED HOL-Induct FAILED HOL-Library FAILED HOL-Metis_Examples FAILED HOL-MicroJava FAILED HOL-NanoJava FAILED HOL-Nitpick_Examples FAILED HOL-Quotient_Examples FAILED HOL-Predicate_Compile_Examples FAILED HOL-Word-SMT_Examples FAILED HOL-Subst FAILED HOL-TPTP FAILED HOL-Multivariate_Analysis FAILED HOL-IMP FAILED Possible showstoppers: haftmann@macbroy20:~/data/isabelle/with_set$ grep -rIPl 'Collect_def|mem_def' src/HOL/*/ src/HOL/Library/Predicate_Compile_Alternative_Defs.thy src/HOL/Library/Executable_Set.thy src/HOL/Library/Cset.thy src/HOL/Library/More_Set.thy src/HOL/Library/List_Cset.thy src/HOL/Quotient_Examples/FSet.thy src/HOL/Quotient_Examples/List_Cset.thy src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy src/HOL/Nitpick_Examples/Core_Nits.thy src/HOL/Nominal/Examples/Standardization.thy src/HOL/Nominal/Nominal.thy src/HOL/TPTP/CASC_Setup.thy src/HOL/SMT_Examples/SMT_Tests.thy src/HOL/MicroJava/J/TypeRel.thy src/HOL/MicroJava/BV/BVExample.thy src/HOL/Metis_Examples/Message.thy src/HOL/Metis_Examples/Tarski.thy src/HOL/Metis_Examples/Trans_Closure.thy src/HOL/Metis_Examples/Sets.thy src/HOL/Metis_Examples/Proxies.thy src/HOL/Metis_Examples/Abstraction.thy A glimpse at the AFP: haftmann@macbroy20:~/data/isabelle/afp/blank$ grep -rIPl 'Collect_def|mem_def' thys/ thys/HRB-Slicing/JinjaVM_Inter/JVMInterpretation.thy thys/Group-Ring-Module/Algebra1.thy thys/FinFun/FinFunSet.thy thys/FinFun/FinFun.thy thys/Slicing/JinjaVM/SemanticsWF.thy.orig thys/LinearQuantifierElim/Thys/QE.thy thys/DataRefinementIBP/Diagram.thy thys/DataRefinementIBP/DataRefinement.thy thys/DataRefinementIBP/Preliminaries.thy thys/Tree-Automata/Ta_impl.thy thys/Lower_Semicontinuous/Lower_Semicontinuous.thy thys/Flyspeck-Tame/LowerBound.thy thys/Flyspeck-Tame/ScoreProps.thy thys/JinjaThreads/BV/BCVExec.thy thys/JinjaThreads/MM/Orders.thy thys/JinjaThreads/MM/JMM_Spec.thy thys/JinjaThreads/Execute/ExternalCall_Execute.thy thys/JinjaThreads/Execute/JVMExec_Execute.thy thys/JinjaThreads/Execute/JVM_Execute2.thy thys/JinjaThreads/Execute/TypeRelRefine.thy thys/JinjaThreads/Common/SemiType.thy thys/JinjaThreads/Common/Cset_Monad.thy thys/JinjaThreads/Common/Aux.thy thys/JinjaThreads/Compiler/PCompiler.thy thys/JinjaThreads/Compiler/JVMJ1.thy thys/JinjaThreads/Compiler/Execs.thy thys/JinjaThreads/Framework/LTS.thy thys/JinjaThreads/Framework/FWLTS.thy thys/JinjaThreads/Framework/FWDeadlock.thy thys/JinjaThreads/Framework/FWBisimDeadlock.thy thys/JinjaThreads/Framework/FWBisimulation.thy thys/JinjaThreads/Framework/Bisimulation.thy thys/Coinductive/Coinductive_Nat.thy thys/Coinductive/TLList.thy thys/Coinductive/Coinductive_List_Lib.thy thys/Binomial-Heaps/SkewBinomialHeap.thy thys/Perfect-Number-Thm/Sigma.thy thys/GraphMarkingIBP/DSWMark.thy thys/GraphMarkingIBP/Preliminaries.thy thys/GraphMarkingIBP/LinkMark.thy thys/GraphMarkingIBP/StackMark.thy thys/POPLmark-deBruijn/Execute.thy thys/Shivers-CFA/ExCFSV.thy thys/Shivers-CFA/HOLCFUtils.thy thys/Abstract-Rewriting/Abstract_Rewriting.thy thys/Presburger-Automata/Presburger_Automata.thy thys/Presburger-Automata/DFS.thy thys/Collections/ListSetImpl.thy thys/Collections/common/FTGAAdd.thy thys/Collections/AnnotatedListGAPrioUniqueImpl.thy thys/NormByEval/NBE.thy thys/Free-Groups/Isomorphisms.thy thys/KBPs/DFS.thy thys/SIFPL/VS.thy thys/SIFPL/VS_OBJ.thy thys/SIFPL/HuntSands.thy thys/ArrowImpossibilityGS/Thys/Arrow_Order.thy A vast area for volunteers. Cheers, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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: > Consider the new inductive package, complete_lattice type classes, > etc. Important point. Similarly, the generaliziation of class instances from set to fun has been a noteworthy contribution on its own. inquit Makarius: > I am more concerned about the general process of such upheavals, and hope > that more time is taken this time to consider the moves. In particular we > are already a bit late in the release schedule, and things are supposed to > converge soon. So anything that cannot be finished within very few weeks > needs to be postponed. (People who have participated in the 2006/2007 release > desaster know what I mean.) inquit Brian: > As long as we put off reintroducing 'a set as a separate type, we will > continue to accumulate more theories (like Multivariate_Analysis) that > confuse sets and predicates. The job of introducing 'a set will only > get more difficult the longer we wait. I would certainly like to see > the job completed before the next release, although it might require > more time than we have. Putting aside that the discussion itself seems not yet finished (although most voices speak in favor for set, I would not want to continue without considering Stefan's concerns), from my point of view it is not realistic to reintroduce the set type constructor before the next release because it opens too many uncertainties. Let me briefly sum up where we are standing now: we have figured out that it is possible in principle, and have found out how we can get there rather smoothly: eliminate all set-pred mixture from theories and make proofs robust to persist in both worlds. Ultimately, this will enable us to introduce set with a rather minimal-invasive changeset. But before, there is still a lot of work to do, and (solvable but) unexpected problems may lurk beyond the corner. 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 been introduced after 2008, but maybe Cezary can comment on this. These tasks can proceed side-by-side with release preparation since they only affect single theories or are independent of the main repository. When this is finished (and this will take some time, I guess beyond the release – I will mail another report on this), we hopefully have learnt enough to introduce 'a set again and then we have time to consider 2008's changesets thoroughly, discover and iron out remaining deficiencies and make use of the benefits accordingly, which still will take some time, but after release time should be available. Cheers, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study
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 > HOL-Multivariate_Analysis > HOL-Nitpick_Examples > HOL-Nominal > HOL-NSA > HOL-Old_Number_Theory > HOL-Predicate_Compile_Examples > HOL-Quotient_Examples > HOL-TPTP > HOL-UNITY > HOL-Word-SMT_Examples Some more data from HOL-IMP and HOL-MicroJava: the former was trivial to fix (patch in main repository already). MJ after removing an unused lemma only seems to require a working Library/More_Set.thy to get through (haven't done anything about that one). At least for applications in that style, I don't think we need to expect much pain for going back to a separate set type. Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 on this thread.) 2007 2008 Thanks for digging up the history, it sheds some further light on it. I abstain from voicing an oponion on the matter itself, because I am not an expert of the increasingly complex Isabelle/HOL library. In 2008 I've lost some nice Isar proofs due to change of the HO unification behaviour, but that was only a minor disadvantage, and predicates are nicer in many situations, which does not mean there could not be a separate set type, even though Coq and HOLs prefer predicates. I am more concerned about the general process of such upheavals, and hope that more time is taken this time to consider the moves. In particular we are already a bit late in the release schedule, and things are supposed to converge soon. So anything that cannot be finished within very few weeks needs to be postponed. (People who have participated in the 2006/2007 release desaster know what I mean.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study
On Thu, Aug 11, 2011 at 5:44 AM, Florian Haftmann wrote: > 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 > 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 > HOL-Multivariate_Analysis > HOL-Nitpick_Examples > HOL-Nominal > HOL-NSA > HOL-Old_Number_Theory > HOL-Predicate_Compile_Examples > HOL-Quotient_Examples > HOL-TPTP > HOL-UNITY > HOL-Word-SMT_Examples Working from a copy of Florian's repo, I have got HOLCF and HOL-Multivariate_Analysis working again. I transferred the changes back to the main repo as well: http://isabelle.in.tum.de/repos/isabelle/rev/bdcc11b2fdc8 http://isabelle.in.tum.de/repos/isabelle/rev/510ac30f44c0 > I estimate that half of these failures are marginal and are just due to > use of mem_def or Collect_def in proofs. Indeed, many of the changes are simply removing mem_def and Collect_def (possibly adding mem_Collect_eq) from calls to metis. HOLCF required one such change in Library/Infinite_Set.thy, removing Collect_def in a metis call. The other HOLCF changes were in ML code in packages: Specifically, when building terms, I was sometimes using "T --> boolT" instead of "mk_setT T". Overall, HOLCF was very good about respecting the distinction between sets and predicates, probably because most of it was written before 2008, back when 'a set and 'a => bool were actually distinct types. > Other failures > are caused by some constructs which somehow exploit the set-predicate > identification (Library/Cset.thy "set = member", > HOL-Multivariate_Analysis "mono (S :: 'a set ==> _"), but this can be > changed with comparably little effort. There was a lot more of this kind of thing in the Multivariate_Analysis libraries. This was to be expected, since much of it was written in 2009 or later, after 'a set became an abbreviation. In the case of "mono" used at type "'a set => bool", I ended up defining a separate constant called "mono_set". This seems to work just fine, although it is a user-visible change. In other cases, an single operation was defined in the library, and then used sometimes as a set, and other times as a predicate. In these situations, I had to decide on a specific type signature for each constant, and restate some lemmas accordingly. Making these decisions is not trivial, and requires a bit of understanding of the library involved, and how the constants defined in them are usually used. > What can be drawn for that? If there is an agreement that > re-introducing set is a good idea, this requires some effort, but it is > not unrealistic. A working plan could look like the following: > > Step A > * eliminate predicate / set »misfits« > * eliminate proofs with mem_def / Collect_def > * repair proofs which fail in this ad-hoc adjustment setup > The advantage is that these quality improvements can be committed to > Isabelle as it is by now and do not demand a reintroduction of set > immediately, but eliminate obstacles later on. I have already started on this, and I will continue to do more. > Step B > * solve problems which existing packages (quotient) > * re-construct from relevant changesets what still has to be done to > keep the system consistent > * re-introduce 'a set > > Step C > * cleaning up the situation: type class instantiations for sets, > appropriate simp rules for predicates, … > * code generation setup for sets > > It should be self-evident that nothing beyond Step A can be undertaken > before the next release. As long as we put off reintroducing 'a set as a separate type, we will continue to accumulate more theories (like Multivariate_Analysis) that confuse sets and predicates. The job of introducing 'a set will only get more difficult the longer we wait. I would certainly like to see the job completed before the next release, although it might require more time than we have. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Fri, Aug 12, 2011 at 2:27 AM, Alexander Krauss 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 this question just now... I think the simplest solution to the import issue is just to use predicates for everything, and don't try to map anything onto the Isabelle set type. For example, set union and intersection in HOL-Light can translate to "sup" and "inf" on predicates in Isabelle. Since Isabelle has pretty good support for predicates now, I think this would work well enough. 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: Consider the new inductive package, complete_lattice type classes, etc. Perhaps this is mostly just a personal preference, but I am also in favor of having the standard Isabelle libraries emphasize (curried) predicates more than sets. We have been moving in this direction for the past few years, and I think that is a good thing. (For example, I think a transitive closure operator on type 'a => 'a => bool is more valuable than on ('a * 'a) set.) I think that library support for predicates is the main thing that would allow importing from other HOLs to work well, regardless of whether 'a set is a separate type or not. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 sets altogether. (I'm trying to imagine > some sort of magic operator to ease the transition between sets with > various forms of tupling and relations.) I certainly find the new world > confusing. And of course every set has a function type, which has > implications for all the theorem proving tools. > Larry > > On 12 Aug 2011, at 10:26, Alexander Krauss wrote: > >> In 2007, Stefan reengineered the inductive package, which could only >> define inductive sets at the time. For many applications, inductive >> predicates were more natural, in particular since one could directly >> attach mixfix notation to them, without having to introduce another >> abbreviation. This was a big improvement. > > > > ___ > 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
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 development of HOL, but otherwise not very well-known: krauss@lapbroy38:~/wd/isabelle/src/HOL$ egrep -r '\[to_(pred|set)\]' . ./List.thy:lemmas lists_IntI = listsp_infI [to_set] ./List.thy:lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set] ./List.thy:lemmas in_lists_conv_set = in_listsp_conv_set [to_set] ./List.thy:lemmas in_listsD [dest!,no_atp] = in_listspD [to_set] ./List.thy:lemmas in_listsI [intro!,no_atp] = in_listspI [to_set] ./Transitive_Closure.thy:lemmas rtrancl_mono = rtranclp_mono [to_set] ./Transitive_Closure.thy:lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set] ./Transitive_Closure.thy:lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set] ./Transitive_Closure.thy:lemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set] ./Transitive_Closure.thy:lemmas rtrancl_subset = rtranclp_subset [to_set] ./Transitive_Closure.thy:lemmas rtrancl_Un_rtrancl = rtranclp_sup_rtranclp [to_set] ./Transitive_Closure.thy:lemmas rtrancl_reflcl [simp] = rtranclp_reflcl [to_set] ./Transitive_Closure.thy:lemmas rtrancl_converseD = rtranclp_converseD [to_set] ./Transitive_Closure.thy:lemmas rtrancl_converseI = rtranclp_converseI [to_set] ./Transitive_Closure.thy:lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set] ./Transitive_Closure.thy:lemmas converse_rtranclE = converse_rtranclpE [to_set] ./Transitive_Closure.thy:lemmas trancl_into_rtrancl = tranclp_into_rtranclp [to_set] ./Transitive_Closure.thy:lemmas rtrancl_into_trancl1 = rtranclp_into_tranclp1 [to_set] ./Transitive_Closure.thy:lemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set] ./Transitive_Closure.thy:lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set] ./Transitive_Closure.thy:lemmas trancl_trans_induct = tranclp_trans_induct [to_set] ./Transitive_Closure.thy:lemmas rtrancl_trancl_trancl = rtranclp_tranclp_tranclp [to_set] ./Transitive_Closure.thy:lemmas trancl_into_trancl2 = tranclp_into_tranclp2 [to_set] ./Transitive_Closure.thy:lemmas trancl_converseI = tranclp_converseI [to_set] ./Transitive_Closure.thy:lemmas trancl_converseD = tranclp_converseD [to_set] ./Transitive_Closure.thy:lemmas trancl_converse = tranclp_converse [to_set] ./Transitive_Closure.thy:lemmas converse_trancl_induct = converse_tranclp_induct [to_set] ./Transitive_Closure.thy:lemmas tranclD = tranclpD [to_set] ./Transitive_Closure.thy:lemmas converse_tranclE = converse_tranclpE [to_set] ./Transitive_Closure.thy:lemmas reflcl_trancl [simp] = reflcl_tranclp [to_set] ./Transitive_Closure.thy:lemmas rtranclD = rtranclpD [to_set] ./Transitive_Closure.thy:lemmas trancl_rtrancl_trancl = tranclp_rtranclp_tranclp [to_set] ./Wellfounded.thy:lemmas wfPUNIVI = wfUNIVI [to_pred] ./Wellfounded.thy:lemmas wfP_induct = wf_induct [to_pred] ./Wellfounded.thy:lemmas wfP_eq_minimal = wf_eq_minimal [to_pred] ./Wellfounded.thy:lemmas wfP_trancl = wf_trancl [to_pred] ./Wellfounded.thy:lemmas wfP_subset = wf_subset [to_pred] ./Wellfounded.thy:lemmas wfP_acyclicP = wf_acyclic [to_pred] ./Wellfounded.thy:lemmas acyclicP_converse [iff] = acyclic_converse [to_pred] ./Wellfounded.thy:lemmas acc_induct = accp_induct [to_set] ./Wellfounded.thy:lemmas acc_downward = accp_downward [to_set] ./Wellfounded.thy:lemmas not_acc_down = not_accp_down [to_set] ./Wellfounded.thy:lemmas acc_downwards_aux = accp_downwards_aux [to_set] ./Wellfounded.thy:lemmas acc_downwards = accp_downwards [to_set] ./Wellfounded.thy:lemmas acc_wfI = accp_wfPI [to_set] ./Wellfounded.thy:lemmas acc_wfD = accp_wfPD [to_set] ./Wellfounded.thy:lemmas wf_acc_iff = wfP_accp_iff [to_set] krauss@lapbroy38:~/wd/isabelle/src/HOL$ krauss@lapbroy38:~/wd/afp/thys$ egrep -r '\[to_(pred|set)\]' . ./Simpl/AlternativeSmallStep.thy:by (rule renumber [to_pred]) ./Simpl/AlternativeSmallStep.thy:by (rule renumber [to_pred]) ./Simpl/SmallStep.thy:by (rule renumber [to_pred]) ./Simpl/SmallStep.thy:by (rule renumber [to_pred]) krauss@lapbroy38:~/wd/afp/thys$ Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 forms of tupling and relations.) I certainly find the new world confusing. And of course every set has a function type, which has implications for all the theorem proving tools. Larry On 12 Aug 2011, at 10:26, Alexander Krauss wrote: > In 2007, Stefan reengineered the inductive package, which could only > define inductive sets at the time. For many applications, inductive > predicates were more natural, in particular since one could directly > attach mixfix notation to them, without having to introduce another > abbreviation. This was a big improvement. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 to mention type classes. It comes up again and again on the mailing list. >> 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). > > Do we really know? > > 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 this question just now... The only gain I remember when we made the switch was that in some places I could include precidates in set-theoretic terms, eg "even -> even". Before I had to write something like "{x. even x} -> {x. even x}". How the proofs changed in those places I do not remember. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 argument. This time we know what we go back to and the real benefits (and the few losses). Do we really know? 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 this question just now... I am not arguing against 'a set, but please bring the facts to light! That we have to discuss this now is mainly since the last switch was made without fully evaluating the consequences (even though they were known already at the time). Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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. Am 11/08/2011 14:43, schrieb 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 this mailing list seems a good place to collect them. Why (I think) the current state concerning sets is a bad idea: * There are two worlds (sets and predicates) which are logically the same but syntactically different. Although the logic construction suggests that you can switch easily between both, in practice you can't – just do something like (unfold mem_def) and your proof will be a mess since you have switched to the »wrong world«. * 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. * The logical identification of sets and predicates prevents some reasonable simp rules on predicates: e.g. you cannot have (A |inf| B) x = A x& B x because then expressions like »set xs |inter| set ys« behave strangely if the are eta-expanded (e.g. due to induction). * The missing abstraction for sets prevents straightforward code generation for them (for the moment, the most pressing, but not the only issue). What is your opinion? In a further e-mail I give some estimations I gained through some experiments to figure out how feasible a re-introduction would be in practice. Btw. the history of the set-elimination can be found here: http://isabelle.in.tum.de/repos/isabelle/shortlog/26839 Cheers, Florian ___ 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 Am 11/08/2011 14:43, schrieb 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 this mailing list seems a good place to collect > them. > > Why (I think) the current state concerning sets is a bad idea: * > There are two worlds (sets and predicates) which are logically the > same but syntactically different. Although the logic construction > suggests that you can switch easily between both, in practice you > can't – just do something like (unfold mem_def) and your proof will > be a mess since you have switched to the »wrong world«. * 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. * The logical > identification of sets and predicates prevents some reasonable simp > rules on predicates: e.g. you cannot have (A |inf| B) x = A x & B x > because then expressions like »set xs |inter| set ys« behave > strangely if the are eta-expanded (e.g. due to induction). * The > missing abstraction for sets prevents straightforward code generation > for them (for the moment, the most pressing, but not the only > issue). > > What is your opinion? > > In a further e-mail I give some estimations I gained through some > experiments to figure out how feasible a re-introduction would be in > practice. > > Btw. the history of the set-elimination can be found here: > http://isabelle.in.tum.de/repos/isabelle/shortlog/26839 > > Cheers, Florian > > > > > ___ 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
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
I'm strongly in favour of an explicit set type. I've been asked for advice by a number of novice Isabelle users and given the same recommendation: go make the development type-check under the old rules. Then the simplifier will start helping you rather than fighting you. I suppose there might be an alternative strategy involving adapting the simpset or similar to try to standardise blended terms on set operations or function operations. But I don't think this is possible the way Isabelle works - if it were not the default noone then it would not help, and if it were then it would generate years of work in compatibility with the existing proof library. Yours, Thomas. From: isabelle-dev-boun...@mailbroy.informatik.tu-muenchen.de [isabelle-dev-boun...@mailbroy.informatik.tu-muenchen.de] On Behalf Of Lawrence Paulson [l...@cam.ac.uk] 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, I would be happy to help track down and fix some problems in theories. Larry On 11 Aug 2011, at 13:43, Florian Haftmann wrote: > Why (I think) the current state concerning sets is a bad idea: > * There are two worlds (sets and predicates) which are logically the > same but syntactically different. Although the logic construction > suggests that you can switch easily between both, in practice you can't ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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 isabelle locally and pull the extra revision. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Thu, Aug 11, 2011 at 5:43 AM, Florian Haftmann 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 carried together some > arguments. I'm pretty sure there are further ones either pro or contra, > for which this mailing list seems a good place to collect them. One of the arguments in favor of identifying "'a set" and "'a => bool" was for "compatibility with other HOLs". https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-December/msg00043.html If we make them into separate types again, how will tools that import proofs from other HOLs be affected? I am interested in this question because I have written such a tool myself (I hacked up an importer for Joe Hurd's OpenTheory format a while back). 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... - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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, I would be happy to help track down and fix some problems in theories. Larry On 11 Aug 2011, at 13:43, Florian Haftmann wrote: > Why (I think) the current state concerning sets is a bad idea: > * There are two worlds (sets and predicates) which are logically the > same but syntactically different. Although the logic construction > suggests that you can switch easily between both, in practice you can't ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev