subject:"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


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

2011-08-26 Thread Tobias Nipkow

I agree. Since predicates are primitive, starting from them is appropriate.

Tobias

Am 26/08/2011 18:33, schrieb Brian Huffman:
 Here's one possible approach to the set-axiomatization/typedef issue:
 
 As a new primitive, we could have something like a pred_typedef
 operation that uses 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 l...@cam.ac.uk 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: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

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 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: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 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 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 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

2011-08-26 Thread Makarius


On Fri, 26 Aug 2011, Brian Huffman wrote:


Here's one possible approach to the set-axiomatization/typedef issue:

As a new primitive, we could have something like a pred_typedef 
operation that uses predicates. This would work just like the 
new_type_definition facility of HOL4, etc.


The type '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 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, 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 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

2011-08-26 Thread Alexander Krauss


The global axiom is

EX x. x : A == type_definition Rep Abs A

allowing local typedefs whenever non-emptiness of A is
derivable, even using assumptions in the context.


This is an interesting discussion, but totally off-topic in this thread 
(whose main content is already growing very large.)


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: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 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

2011-08-26 Thread Makarius


On Fri, 26 Aug 2011, Brian Huffman wrote:


What is gained from that apart from having two versions of typedef?


In the current version of Isabelle, not much (although I personally 
think that a predicate-based variant of typedef would have value). But 
assuming we go ahead and reintroduce 'a 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

2011-08-25 Thread Alexander Krauss


On 08/24/2011 03:36 PM, Lawrence Paulson wrote:

I've just been trying to get the proofs working, not to simplify them
or even to understand them. Incidentally, let there be no illusions
about people accidentally stumbling into a mixture of sets and
predicates. Some of these theories were clearly 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

2011-08-25 Thread Makarius


On Wed, 24 Aug 2011, Florian Haftmann wrote:

I was driven crazy some months ago when I attempted in vain to enable 
push access.  I don't even know what the problem was (authentication, 
web server configuration, encrpytion) – maybe I wasn't even able to 
figure out.  If someone of the TUM guys 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

2011-08-25 Thread Florian Haftmann

 Should we ask a wider audience (isabelle-users) if anybody else has good 
 reasons against/for a change?

The thought deserves attention, but I think the discussion is too early
for that.

Indeed, this is where, as I deem, we current are:
* Some agreement that mixing sets and predicate syntax in 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

2011-08-25 Thread Florian Haftmann

Hi all,

thanks to many efforts (thanks particularly to Alex, Brian, Cezary,
Larry) we already have gained some insights whether and how it would be
technically possible to introduce a set type constructor.

As I see the whole story, we have to think carefully how we would
proceed in order to 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

2011-08-25 Thread Florian Haftmann

Hi Jasmin,

 HOL-Metis_Examples FAILED
 HOL-Nitpick_Examples FAILED
 
 I can look into those things if and when it is decided to move to sets.

in case, thanks for the offer.  Please ignore any further announcements
of these sessions in intermediate reports ;-).

Florian

-- 

Home:
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

2011-08-25 Thread Andreas Schropp


On 08/25/2011 10:45 PM, Florian Haftmann wrote:

Hi all,

thanks to many efforts (thanks particularly to Alex, Brian, Cezary,
Larry) we already have gained some insights whether and how it would be
technically possible to introduce a set type constructor.
   


Let me ask something stupid:
  why 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

2011-08-25 Thread Andreas Schropp


On 08/25/2011 11:26 PM, Florian Haftmann wrote:

Hi Andreas,

   

Let me ask something stupid:
   why exactly do you guys axiomatize 'a set?
Sure it's admissable and all, but why not do this definitionally
via the obvious typedef?
 

the answer is rather technical: »typedef« in its current 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

2011-08-25 Thread Michael Norrish

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

2011-08-24 Thread Lawrence Paulson

I've just been trying to get the proofs working, not to simplify them or even 
to understand them. Incidentally, let there be no illusions about people 
accidentally stumbling into a mixture of sets and predicates. Some of these 
theories were clearly designed from the ground upwards on the 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

2011-08-24 Thread Florian Haftmann

 maybe also declare them [no_atp], to avoid sledgehammer-generated proofs
 that we know are going to break one release later...?

Maybe better now, as long as there are real sledgehammer-generated
proofs depending on it.

Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
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

2011-08-24 Thread Florian Haftmann

 A proof works only if I insert before it the following:
 
 instance set :: (type) complete_boolean_algebra
 proof
 qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def Inf_bool_def 
 Sup_bool_def)
 
 this is strange because this exact text already appears in the file 
 Complete_Lattice.thy (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

2011-08-24 Thread Florian Haftmann

Hi all,

Shouldn't one remove quite a bit of duplication first? The classes
distributive_complete_lattice and complete_boolean_algebra are now part
of HOL (the former as complete_distrib_lattice) (see the FIXME). The set
instances for those should be in/go into Florian's HOL repository as
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

2011-08-22 Thread Lawrence Paulson

I've come across something strange in the file 
isabelle/afp/devel/thys/DataRefinementIBP/Diagram.thy and was wondering if 
anybody could think of an explanation.

A proof works only if I insert before it the following:

instance set :: (type) complete_boolean_algebra
proof
qed (auto simp add: 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

2011-08-22 Thread Brian Huffman

On Mon, Aug 22, 2011 at 8:01 AM, Lawrence Paulson l...@cam.ac.uk wrote:
 I've come across something strange in the file 
 isabelle/afp/devel/thys/DataRefinementIBP/Diagram.thy and was wondering if 
 anybody could think of an explanation.

 A proof works only if I insert before it the following:

 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

2011-08-20 Thread Alexander Krauss


On 08/20/2011 01:18 AM, Florian Haftmann wrote:


A typical example for what I was alluding to can be found at:

http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/6e3e9c6c5062#l1.37

 Observe the following proof:

lemma part_equivpI: (\existsx. R x x) \Longrightarrow  symp R
\Longrightarrow  transp R \Longrightarrow  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 »\in« 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 \union  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

2011-08-19 Thread Lawrence Paulson

I am currently working on AFP/Coinductive, which is full of the sort of thing.
Larry

On 19 Aug 2011, at 00:31, Gerwin Klein wrote:

 Can't really quantify it, but I'm seeing this all the time from not-so-novice 
 users over here. Mixing sets and predicates (e.g. using intersection on 
 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

2011-08-19 Thread Dmitriy Traytel


Hi all,

On 19.08.2011 01:38, Gerwin Klein wrote:
Should we ask a wider audience (isabelle-users) if anybody else has 
good reasons against/for a change?
Another small advantage of set as an own datatype arises in the context 
of subtyping.


We use map functions to lift coercions between base 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

2011-08-19 Thread Lukas Bulwahn


Stefan Berghofer wrote:

Alexander Krauss wrote:

In particular, Stefan discovered that replacing inductive set
definitions by predicates was by no means as easy as everybody had
expected. One good example is the small-step relation from Jinja and
its various cousins. It had type ((expr * state) * (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

2011-08-19 Thread Lukas Bulwahn


On 08/19/2011 07:39 AM, Tobias Nipkow wrote:

Am 19/08/2011 00:00, schrieb Stefan Berghofer:

Alexander Krauss wrote:

I want to emphasize that the limitation of the code generator mentioned
here not only applies to sets-as-predicates but also to
maps-as-functions and other abstract types that 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

2011-08-19 Thread Alexander Krauss


On 08/19/2011 01:31 AM, Gerwin Klein wrote:

On 19/08/2011, at 5:56 AM, Alexander Krauss wrote:



* Similarly, there is a vast proof search space for automated
tools which is not worth exploring since it leads to the »wrong
world«, making vain proof attempts lasting longer instead just
failing.


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

2011-08-19 Thread Florian Haftmann

Hi again,

 Indeed, I think a general point can be made here, and not just about code 
 generation. In the last couple of years, we've run into situations in 
 Quickcheck, Nitpick, the code generator, and perhaps more, where we felt the 
 need for sets as different from functions. However, there 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:
  (\existsx. R x x) \Longrightarrow symp R \Longrightarrow transp
R \Longrightarrow 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 »\in« 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.set_append [simp del]

thm

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

2011-08-18 Thread Jasmin Christian Blanchette

Hi Florian,

Am 18.08.2011 um 09:18 schrieb Florian Haftmann:

 @list: btw. what is the status of »refute« in general?  Is it supposed
 to be superseded by nitpick entirely?

Pretty much so, yes, but there are a few reasons why I would rather that we 
keep it around:

1. Refute participates at 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

2011-08-18 Thread Cezary Kaliszyk

On Thu, Aug 18, 2011 at 3:49 AM, Florian Haftmann 
florian.haftm...@informatik.tu-muenchen.de wrote:

 [...] So, the best way now is
 to continue eliminating set-pred mixture (also in the AFP of course!)
 and discover problems in packages – I'm a little concerned about
 quotient since this has 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

2011-08-18 Thread Jasmin Christian Blanchette

Hi all,

Let me describe the implications of reintroducing 'a set for Sledgehammer's 
and Nitpick's performance.

Am 12.08.2011 um 11:27 schrieb Alexander Krauss:

 What are, actually, the losses when going back? This has not yet been touched 
 by this thread at all (except the 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

2011-08-18 Thread Makarius


On Thu, 18 Aug 2011, Florian Haftmann wrote:


envisaged working plan
--

a) general
b) elimination of set/pred mixture
c) consolidation
d) RELEASE


This looks quite reasonable to me: the parts a, b, c should be easy to 
consolidate for the release towards the end of the 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

2011-08-18 Thread Alexander Krauss


On 08/18/2011 02:16 PM, Florian Haftmann wrote:

* (maybe)
 hide_fact (open) Set.mem_def Set.Collect_def
   to indicate that something is going on with these


maybe also declare them [no_atp], to avoid sledgehammer-generated proofs 
that we know are going to break one release later...?


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

2011-08-18 Thread Tjark Weber

On Thu, 2011-08-18 at 09:34 +0200, Jasmin Christian Blanchette wrote:
 The maintenance load is extremely low. When it comes to the REFUTE
 exception, I can look at it if and when we decide to move back to
 sets.

I suspect that Jasmin will have no trouble fixing this, but otherwise
I'd be happy to 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

2011-08-18 Thread Alexander Krauss


Hi all,

Here are some critical questions/comments towards two of Florian's 
initial arguments pro 'a set.


[...]


* Similarly, there is a vast proof search space for automated tools
which is not worth exploring since it leads to the »wrong world«, making
vain proof attempts lasting longer 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

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

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

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

2011-08-18 Thread Jasmin Christian Blanchette

Am 19.08.2011 um 00:00 schrieb Stefan Berghofer:

 thanks for your excellent report, I fully agree with this view. There is
 often a tradeoff between executability and conciseness / abstractness of
 specifications, so I don't think it is a good idea to tweak the logic in
 such a way that it is 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