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
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
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
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
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
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 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
On Fri, Aug 12, 2011 at 2:27 AM, Alexander Krauss kra...@in.tum.de wrote:
What are, actually, the losses when going back? This has not yet been
touched by this thread at all (except the compatibility/import issue
mentioned by Brian), and at least myself I wouldn't feel comfortable
answering 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 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] performance regression for simp_all
On Fri, Aug 12, 2011 at 4:07 PM, Makarius makar...@sketis.net wrote: http://isabelle.in.tum.de/repos/isabelle/rev/13e297dc improves startup time of the worker thread farm significantly, and I've got real times in the range of 0.003s -- 0.005s on my old machine from 2 years ago with Proof General. Thanks for the quick response; with this new patch everything looks much better. Proving True and True with simp_all in Proof General now takes only 0.002s on my machine. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
