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
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
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
Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:
I will now examine HOL-Nominal more closer, and after that come up with
a next report about the distribution.
There should be no problems in principle.
Early versions of Nominal (1) worked perfectly
with an explicit
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
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
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
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
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
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
On Fri, Aug 26, 2011 at 9:36 AM, Andreas Schropp schr...@in.tum.de wrote:
On 08/26/2011 06:50 PM, Tobias Nipkow wrote:
I agree. Since predicates are primitive, starting from them is
appropriate.
Tobias
Did I get this right:
the idea is to implement our advanced typedef via a HOL4-style
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
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
On Thu, Aug 25, 2011 at 1:45 PM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
HOL-Hoare_Parallel FAILED
Also Hoare_Parallel is non-terminating.
I have a patch for this one:
http://isabelle.in.tum.de/repos/isabelle/rev/5e681762d538
Once this changeset gets merged into
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
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
On Fri, Aug 26, 2011 at 1:38 PM, Makarius makar...@sketis.net wrote:
On Fri, 26 Aug 2011, Brian Huffman wrote:
Here's one possible approach to the set-axiomatization/typedef issue:
As a new primitive, we could have something like a pred_typedef
operation that uses predicates. This would work
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.)
On Fri, Aug 26, 2011 at 1:23 PM, Andreas Schropp schr...@in.tum.de wrote:
On 08/26/2011 10:38 PM, Makarius wrote:
What is gained from that apart from having two versions of typedef?
I am with you here.
We don't need two primitive versions of typedefs.
This is incorrect: Only the
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
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
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
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
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
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:
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
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
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
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
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:
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
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
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:
On Mon, Aug 22, 2011 at 8:01 AM, Lawrence Paulson l...@cam.ac.uk wrote:
I've come across something strange in the file
isabelle/afp/devel/thys/DataRefinementIBP/Diagram.thy and was wondering if
anybody could think of an explanation.
A proof works only if I insert before it the following:
On 08/20/2011 01:18 AM, Florian Haftmann wrote:
A typical example for what I was alluding to can be found at:
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/6e3e9c6c5062#l1.37
Observe the following proof:
lemma part_equivpI: (\existsx. R x x) \Longrightarrow symp R
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
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
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)
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
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.
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
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
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
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
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
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...?
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
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
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,
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,
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?
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
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
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«,
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
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
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
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:
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
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
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.
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
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
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
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
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
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
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
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
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
Hi again,
as feasibility study I re-introduced the good old set type constructor
at a recent revision in the history. The result can be inspected at
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329
This is by no means meant as a thorough treatment of the whole
On Thu, Aug 11, 2011 at 5:43 AM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
Hello together,
recently in some personal discussions the matter has arisen whether
there would be good reason to re-introduce the ancient set type
constructor. To open the discussion I have
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
]
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
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
75 matches
Mail list logo
