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

On Thu, Aug 25, 2011 at 1:45 PM, Florian Haftmann
 wrote:
> HOL-Probability FAILED

This is now fixed in the main repo; the following changeset should be
merged back into isabelle_set:

http://isabelle.in.tum.de/repos/isabelle/rev/c10485a6a7af
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-08-26 Thread Cezary Kaliszyk

On Fri, Aug 26, 2011 at 5:45 AM, Florian Haftmann <
florian.haftm...@informatik.tu-muenchen.de> wrote:
>
> [...] According to my knowledge, the following session produce
> problems: [...]
> HOL-Quotient_Examples FAILED
>

Please propagare the isabelle changeset:
http://isabelle.in.tum.de/repos/isabelle/rev/5e0f9e0e32fb
to Isabelle-set. With it, Quotient_Examples succeeds.

Cheers,

Cezary
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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


On 08/26/2011 10:50 PM, Brian Huffman wrote:

On Fri, Aug 26, 2011 at 1:23 PM, Andreas Schropp  wrote:
   

On 08/26/2011 10:38 PM, Makarius wrote:
 

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

I am with you here.
We don't need two primitive versions of typedefs.
 

This is incorrect: Only the predicate-based typedef need be primitive.
The set-based typedef can be implemented definitionally as a thin
layer on top of the predicate-based one.
   


That is exactly what I said below the quoted line. ;>
I guess this discussion only came about because you said HOL4-style
typedefs, which cannot be used as the primitive.


- Brian
   


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

On Fri, Aug 26, 2011 at 1:23 PM, Andreas Schropp  wrote:
> On 08/26/2011 10:38 PM, Makarius wrote:
>>
>> What is gained from that apart from having two versions of typedef?
>
> I am with you here.
> We don't need two primitive versions of typedefs.

This is incorrect: Only the predicate-based typedef need be primitive.
The set-based typedef can be implemented definitionally as a thin
layer on top of the predicate-based one.

- Brian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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:38 PM, Makarius  wrote:
> On Fri, 26 Aug 2011, Brian Huffman wrote:
>
>> Here's one possible approach to the set-axiomatization/typedef issue:
>>
>> As a new primitive, we could have something like a "pred_typedef"
>> operation that uses predicates. This would work just like the
>> new_type_definition facility of HOL4, etc.
>>
>> The type "'a set" could be introduced definitionally using "pred_typedef".
>>
>> After type "'a set" has been defined, we can implement the "typedef"
>> command, preserving its current behavior, as a thin wrapper on top of
>> "pred_typedef".
>>
>> This approach would let us avoid having to axiomatize the 'a set type.
>> Also, for those of us who like predicates, "pred_typedef" might be rather
>> useful as a user-level command.
>
> What is gained from that apart from having two versions of typedef?

In the current version of Isabelle, not much (although I personally
think that a predicate-based variant of typedef would have value). But
assuming we go ahead and reintroduce "'a set" as a separate type
again, this plan for typedef would reduce the number of primitive
concepts and axioms required to bootstrap HOL.

Of course, axioms like mem_Collect_eq and Collect_mem_eq are rather
uncontroversial, as axioms go. But if there is an easy way to avoid
declaring these as axioms, then keeping them as axioms seems a bit
gratuitous, in my opinion.

- Brian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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


On 08/26/2011 10:38 PM, Makarius wrote:

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


I am with you here.
We don't need two primitive versions of typedefs.

The only thing that might be sensible from my POV is using predicates 
instead of
sets in the primitive version (feat all your extensions) und simulating 
the one using

axiomatized sets via composing Abs,Rep with the set-predicate-bijection.
But as I said: I can deal with axiomatized set with only minor 
complications, so no

indication here.

Cheers,
  Andy


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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 Thu, Aug 25, 2011 at 1:45 PM, Florian Haftmann
 wrote:
> HOL-Hoare_Parallel FAILED

> Also Hoare_Parallel is non-terminating.

I have a patch for this one:

http://isabelle.in.tum.de/repos/isabelle/rev/5e681762d538

Once this changeset gets merged into the isabelle_set repo,
Hoare_Parallel should start working.

Here's what happened: After a "clarify" step in a proof script,
Isabelle yields a variable called "xb" (renamed from "x" to avoid
clashes with pre-existing "x" and "xa"), while Isabelle_set calls the
same variable "i". It turns out that the Isabelle_set is actually
doing the right thing here. There is a goal of the form "x : (INT i:A.
B i))", and clarify applies the rule INT_I. In Isabelle_set, the new
variable name is inherited from the bound variable "i" in the goal.
But in the current version, the subgoal ends up in the eta-expanded
form "x : (%a. (INT i:A. B i) a)" and the name "i" doesn't get used.

To summarize: eta-expansion is a problem. Eta-expansion seems to
happen with induction (either from "induct" or "rule"), although the
"eta-contract" pretty-printing option tries to prevent people from
noticing (why does this option exist?!?) Switching to a separate set
type greatly reduces the number of opportunities for unwanted
eta-expansion.

- Brian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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


On 08/26/2011 07:08 PM, Brian Huffman wrote:

As far as I understand, the typedef package merely issues global
axioms of the form "type_definition Rep Abs S", as long as it is
provided with a proof of "EX x. x : S".
   


The global axiom is

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

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

This is not really a problem, but complicates my conservativity
argument. Before local typedefs the proof of (EX x. x : A) was
global. Actually Makarius' attitude on this was that those non-emptiness
proofs "should be global most of the time", but he didn't want to
introduce a check.

Cheers,
  Andy

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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


On 08/26/2011 07:02 PM, Brian Huffman wrote:

With ordinary "typedef", I have to do this:

typedef (open) bar = "{x. is_bar x}"

But then it generates rules of the wrong form:
x : {x. is_bar x} ==>  Rep_bar (Abs_bar x) = x
Rep_bar x : {x. is_bar x}

And I have to do an extra step to get the rules I want:
lemmas Rep_bar' = Rep_bar [unfolded mem_Collect_eq]
lemmas Abs_bar_inverse' = Abs_bar_inverse [unfolded mem_Collect_eq]

Even with a transfer tool, the extra step would still be necessary.
   


Predicate application corresponds to set-membership, so
in apart from technicalities (which might be hard, no idea)
I still don't see the problem.



- Brian
   


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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


On 08/26/2011 07:08 PM, Brian Huffman wrote:

What exactly are our extensions to typedef?
   


I enumerated them in the other thread:
  local typedefs, sort constraints on type parameters,
overloaded constants in representation sets.
Hopefully I am not missing others.


My understanding of the localized typedef is that it works by
declaring a global typedef behind the scenes (much like a local
definition of a polymorphic constant works by declaring a global
polymorphic definition behind the scenes).
   


Last time I looked local typedefs were primitive. Makarius?
Actually I suggested exactly this treatment of local typedefs
back in the day, so thanks for bringing this up.


What am I missing here?
   


Most importantly you are missing (indirectly) overloaded constants in
representing sets of typedefs. E.g.
  typedef 'a matrix = {f . finite (nonzero_positions f) }
depends on nonzero_positions, which depends on the
overloaded constant zero['a].
If we try to transform this to HOL4-style typedef without (indirectly) 
overloaded
constants, we have to abstract out a dictionary for zero['a], which 
would give rise to

dependent typedefs. A solution is to eliminate such typedefs completely,
replacing them by their representing sets, regarded as soft-types.
This is an extremely non-trivial global theory-transformation.


- Brian
   


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

On Fri, Aug 26, 2011 at 9:43 AM, Andreas Schropp  wrote:
> On 08/26/2011 07:02 PM, Brian Huffman wrote:
>>
>> I didn't suggest the idea merely for your benefit. I think this
>> approach would give Isabelle a nicer, simpler logical foundation.
>>
>>
>
> What is this logical foundation of Isabelle that you have in mind?
> AFAIK I am the only trying to provide a semantics of any kind,
> so please don't think me rude.

I just think that having fewer primitive concepts and fewer axioms is
generally preferable, that is all.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

On Fri, Aug 26, 2011 at 9:36 AM, Andreas Schropp  wrote:
> On 08/26/2011 06:50 PM, Tobias Nipkow wrote:
>>
>> I agree. Since predicates are primitive, starting from them is
>> appropriate.
>>
>> Tobias
>
> Did I get this right:
>  the idea is to implement our advanced typedef via a HOL4-style predicate
> typedef?
> That doesn't work because HOL4-style typedefs don't feature our extensions
> to typedef and they are only conservative via a global theory
> transformation.

What exactly are our extensions to typedef?

As far as I understand, the typedef package merely issues global
axioms of the form "type_definition Rep Abs S", as long as it is
provided with a proof of "EX x. x : S".

My understanding of the localized typedef is that it works by
declaring a global typedef behind the scenes (much like a local
definition of a polymorphic constant works by declaring a global
polymorphic definition behind the scenes).

What am I missing here?

- Brian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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


On 08/26/2011 07:02 PM, Brian Huffman wrote:

I didn't suggest the idea merely for your benefit. I think this
approach would give Isabelle a nicer, simpler logical foundation.

   


What is this logical foundation of Isabelle that you have in mind?
AFAIK I am the only trying to provide a semantics of any kind,
so please don't think me rude.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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

I didn't suggest the idea merely for your benefit. I think this
approach would give Isabelle a nicer, simpler logical foundation.

>> Also, for those of us who like predicates, "pred_typedef" might be
>> rather useful as a user-level command.
>>
>
> Sets and predicates are isomorphic, so if my isomorphic transfer tool works
> out I don't see why this is needed.

I've often had situations where I wished I had a user-level
"pred_typedef" command. Here's an example:

datatype foo = ...
definition is_bar :: "foo => bool" where ...

Now I want to define a type "bar" such that:
Rep_bar :: bar => foo
Abs_bar :: foo => bar
Abs_bar (Rep_bar x) = x
is_bar x ==> Rep_bar (Abs_bar x) = x
is_bar (Rep_bar x)

With ordinary "typedef", I have to do this:

typedef (open) bar = "{x. is_bar x}"

But then it generates rules of the wrong form:
x : {x. is_bar x} ==> Rep_bar (Abs_bar x) = x
Rep_bar x : {x. is_bar x}

And I have to do an extra step to get the rules I want:
lemmas Rep_bar' = Rep_bar [unfolded mem_Collect_eq]
lemmas Abs_bar_inverse' = Abs_bar_inverse [unfolded mem_Collect_eq]

Even with a transfer tool, the extra step would still be necessary.

On the other hand, a "pred_typedef" command could generate exactly the
rules I want. The same "pred_typedef" command could also generate the
same rules that "typedef" currently generates, simply by using a
predicate of the form "%x. x : S". (This is how I expect the "typedef"
wrapper could work.)

- Brian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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


On 08/26/2011 06:50 PM, Tobias Nipkow wrote:

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

Tobias


Did I get this right:
  the idea is to implement our advanced typedef via a HOL4-style 
predicate typedef?

That doesn't work because HOL4-style typedefs don't feature our extensions
to typedef and they are only conservative via a global theory 
transformation.


Or do you rather suggest having a predicate-based typedef with all our 
extensions?


Cheers,
  Andy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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  wrote:
>> indeed yes I'm the person who decided that this primitive should introduce a 
>> type as a copy of an existing non-empty set. I have always preferred sets to 
>> predicates and the examples I have looked at lately have only strengthened 
>> my view. Not to mention numerous occasions when people have re-invented the 
>> notion of an image.
>> Larry
>>
>> On 25 Aug 2011, at 23:24, Michael Norrish wrote:
>>
>>> On 26/08/11 7:26 AM, Florian Haftmann wrote:
 Hi Andreas,

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

 the answer is rather technical: »typedef« in its current implementation
 needs set syntax / set type as prerequisite.  Of course you could change
 »typedef« to be based on predicates, but there is some kind of unspoken
 agreement not to set one's hand on that ancient and time-honoured Gordon
 HOL primitive.
>>>
>>> HOL88, hol90, hol98 and HOL4 all have new_type_definition.  This
>>> principle takes a theorem of the form
>>>
>>>  ?x. P x
>>>
>>> HOL Light takes a theorem of the form  P x (removing the dependency on
>>> the existential quantifier).
>>>
>>> To the best of my knowledge, none of these systems ever used sets in
>>> this role.
>>>
>>> Michael
>>>
>>>
>>> ___
>>> isabelle-dev mailing list
>>> isabelle-...@in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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


On 08/26/2011 06:33 PM, Brian Huffman wrote:

This approach would let us avoid having to axiomatize the 'a set type.
   


Thanks for trying to help me, but as I said:
  axiomatized set is just a slight inconvenience for me, so if you go for
sets as a seperate type don't bother introducing a new primitive.


Also, for those of us who like predicates, "pred_typedef" might be
rather useful as a user-level command.
   


Sets and predicates are isomorphic, so if my isomorphic transfer tool works
out I don't see why this is needed.


- Brian
   


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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

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

The type "'a set" could be introduced definitionally using "pred_typedef".

After type "'a set" has been defined, we can implement the "typedef"
command, preserving its current behavior, as a thin wrapper on top of
"pred_typedef".

This approach would let us avoid having to axiomatize the 'a set type.
Also, for those of us who like predicates, "pred_typedef" might be
rather useful as a user-level command.

- Brian

On Fri, Aug 26, 2011 at 12:06 AM, Lawrence Paulson  wrote:
> indeed yes I'm the person who decided that this primitive should introduce a 
> type as a copy of an existing non-empty set. I have always preferred sets to 
> predicates and the examples I have looked at lately have only strengthened my 
> view. Not to mention numerous occasions when people have re-invented the 
> notion of an image.
> Larry
>
> On 25 Aug 2011, at 23:24, Michael Norrish wrote:
>
>> On 26/08/11 7:26 AM, Florian Haftmann wrote:
>>> Hi Andreas,
>>>
 Let me ask something stupid:
  why exactly do you guys axiomatize 'a set?
 Sure it's admissable and all, but why not do this definitionally
 via the obvious typedef?
>>>
>>> the answer is rather technical: »typedef« in its current implementation
>>> needs set syntax / set type as prerequisite.  Of course you could change
>>> »typedef« to be based on predicates, but there is some kind of unspoken
>>> agreement not to set one's hand on that ancient and time-honoured Gordon
>>> HOL primitive.
>>
>> HOL88, hol90, hol98 and HOL4 all have new_type_definition.  This
>> principle takes a theorem of the form
>>
>>  ?x. P x
>>
>> HOL Light takes a theorem of the form  P x (removing the dependency on
>> the existential quantifier).
>>
>> To the best of my knowledge, none of these systems ever used sets in
>> this role.
>>
>> Michael
>>
>>
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-08-26 Thread Lawrence Paulson

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

> In ex/Set_Theory.thy, there is a non-terminating »force« proof, which is
> a little bit worrying since I guess that one worked in Isabelle2007.
> Maybe someone can inspect the history on that?

If my memory is correct, this one worked in a reasonable amount of time on 
hardware of the late 1990s. But it isn't that surprising that later changes 
could interfere with its functioning when we restore the set type. I see that 
it does work with auto, but it's slow, thirty seconds or more.

Larry

On 25 Aug 2011, at 21:45, Florian Haftmann wrote:

> I think it is best to leave the AFP aside for the moment and figure out
> still existing problems in the distribution.  According to my knowledge,
> the following session produce problems:
> 
> HOL-ex FAILED
> HOL-Hoare_Parallel FAILED
> HOL-Nominal FAILED
> HOL-Library FAILED
> HOL-Metis_Examples FAILED
> HOL-MicroJava FAILED
> HOL-Nitpick_Examples FAILED
> HOL-Quotient_Examples FAILED
> HOL-Predicate_Compile_Examples FAILED
> HOL-Word-SMT_Examples FAILED
> HOL-TPTP FAILED
> HOL-Probability FAILED

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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


On 08/26/2011 01:08 PM, Makarius wrote:

On Thu, 25 Aug 2011, Andreas Schropp wrote:
Of course I am probably the only one that will ever care about these 
things, so whatever.


I have always cared about that, starting about 1994 in my first 
investigations what HOL actually is -- there are still various 
misunderstandings in printed texts.  And of course there is still no 
fully formal theory of all the aspects that have been emphasized in 
the variety of HOL implementations.


No offense: the last time we discussed these things
you were introducing local typedefs directly instead of expressing them
via global typedefs, which I told you is not exactly hard.
It looks like you are more concerned with an easy implementation,
leaving any matters of conservativity to me. I am not saying this is
bad, but every time my transformation gets harder, I am not
exactly feeling that "Makarius always cares about conservativity". ;D



Maybe you want to start a realistic formalization yourself?



This conservativity result that I am animating is a global theory
transformation featuring replacement of certain typedefs by
their representing sets, regarding them as soft types.
If someone is interested I would indeed write this up, but
given the complexity (I guess 3-4 pages of rule systems, without text)
I don't think we can hope for a realistic formalization.

BTW: Steven should get credit for seriously trying
conservativity of overloading at least. This helped to expose
the misconception, though he did not notice the problem.

Also my write-up of the Isabelle-Kernel is 8 pages (of rule systems, 
without text!)
and still incomplete, so I don't think we will ever manage to prove 
something
important about Isabelle. I am even being generous here, excluding e.g. 
unification
which is part of the trusted code (for speed I guess) but generates 
proof terms.
In my eyes, the only reason we can claim to satisfy the deBruijn 
criterion is

that proof-checking is much easier in ZF. From an LCF POV we are not really
in game, because unification et al are trusted code.



Makarius


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-08-26 Thread Lawrence Paulson

I shall take a look at this one. If anybody else is working on it, please let 
me know as soon as possible.
Larry

On 25 Aug 2011, at 21:45, Florian Haftmann wrote:

> HOL-Probability FAILED

___
isabelle-dev mailing list
isabelle-...@in.tum.de
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 Thu, 25 Aug 2011, Andreas Schropp wrote:

Haha, very funny! We are a long distance from the "ancient HOL 
primitive" already: local typedefs, sort constraints on type parameters, 
overloaded constants in representation sets. Perhaps you remember there 
was quite a suprise regarding those "meta-safety" "proofs" that were 
once regarded as justification of Isabelle/HOL's extensions to HOL. 
These days it seems my translation is the only account of the 
generalized conservativity result that still holds.


There are indeed many formal jokes concerning "typedef", which is in fact 
an axiomatization scheme that happens to with a certain semantic 
interpretation of HOL that was designed specifically to make it work.


Of course I am probably the only one that will ever care about these 
things, so whatever.


I have always cared about that, starting about 1994 in my first 
investigations what HOL actually is -- there are still various 
misunderstandings in printed texts.  And of course there is still no fully 
formal theory of all the aspects that have been emphasized in the variety 
of HOL implementations.


Maybe you want to start a realistic formalization yourself?


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-08-26 Thread Lawrence Paulson

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

On 25 Aug 2011, at 23:24, Michael Norrish wrote:

> On 26/08/11 7:26 AM, Florian Haftmann wrote:
>> Hi Andreas,
>> 
>>> Let me ask something stupid:
>>>  why exactly do you guys axiomatize 'a set?
>>> Sure it's admissable and all, but why not do this definitionally
>>> via the obvious typedef?
>> 
>> the answer is rather technical: »typedef« in its current implementation
>> needs set syntax / set type as prerequisite.  Of course you could change
>> »typedef« to be based on predicates, but there is some kind of unspoken
>> agreement not to set one's hand on that ancient and time-honoured Gordon
>> HOL primitive.
> 
> HOL88, hol90, hol98 and HOL4 all have new_type_definition.  This
> principle takes a theorem of the form
> 
>  ?x. P x
> 
> HOL Light takes a theorem of the form  P x (removing the dependency on
> the existential quantifier).
> 
> To the best of my knowledge, none of these systems ever used sets in
> this role.
> 
> Michael
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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

Hi Andreas,

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

the answer is rather technical: »typedef« in its current implementation
needs set syntax / set type as prerequisite.  Of course you could change
»typedef« to be based on predicates, but there is some kind of unspoken
agreement not to set one's hand on that ancient and time-honoured Gordon
HOL primitive.

Rgds.,
Florian

-- 

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

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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

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 Jasmin Christian Blanchette

Am 25.08.2011 um 22:45 schrieb Florian Haftmann:

> HOL-Metis_Examples FAILED
> HOL-Nitpick_Examples FAILED

Adapting the Metis and Nitpick examples for a set constructor wouldn't be very 
difficult -- for Metis, it's mostly a matter of rerunning Sledgehammer to 
discover slightly different proofs if needed (or, worst case, comment out the 
offending examples), and for Nitpick it is just a technicality.

I can look into those things if and when it is decided to move to sets.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

Hi all,

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

As I see the whole story, we have to think carefully how we would
proceed in order to manage such a transition smoothly.

Currently, we are (re-)separating predicates and sets syntactically, for
three reasons:
a) figure out whether and how it can be done
b) how invasive this is
c) improve quality and robustness of proofs where necessary.

So, for the moment, the purpose of
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set is to
provide a HOL image with a set type constructor as basis for further
exploration. It is not meant as any kind of fork, which would weaken
our resources. To prevent this, we must try hard to re-propagate proof
improvements, duplication elimination etc. to the main repositories. If
any substantial is missing (e.g. type class instances for set type
constructor), it must be added to isabelle_set in a suitable manner, as
is done already here:

http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/893a53a63ba2#l10.42

http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/893a53a63ba2#l1.7
The remaining changes should be as little as possible; to be able to
observe them, I organize isabelle_set that way that the last changeset
is a merge of a genuine main isabelle revision with all the changes
necessary to get HOL (and as many subsessions as possible) through.

It is a challenge, with a limited time budget, to follow what is going
on, and there is high chance I miss some question or similar. So, don't
hesitate to ring the bell twice if you think your point got lost or you
are stuck. In particular, I am currently not aware how much of the work
on AFP theories has found its way back to the main repository or is
still in the queue, and how big the discrepancies to a set-specific
version still are.

I think it is best to leave the AFP aside for the moment and figure out
still existing problems in the distribution. According to my knowledge,
the following session produce problems:

HOL-ex FAILED
HOL-Hoare_Parallel FAILED
HOL-Nominal FAILED
HOL-Library FAILED
HOL-Metis_Examples FAILED
HOL-MicroJava FAILED
HOL-Nitpick_Examples FAILED
HOL-Quotient_Examples FAILED
HOL-Predicate_Compile_Examples FAILED
HOL-Word-SMT_Examples FAILED
HOL-TPTP FAILED
HOL-Probability FAILED

In ex/Set_Theory.thy, there is a non-terminating »force« proof, which is
a little bit worrying since I guess that one worked in Isabelle2007.
Maybe someone can inspect the history on that?

Also Hoare_Parallel is non-terminating.

Concerning the *_Examples session, assistance by the corresponding tool
maintainers is necessary and appreciated. I guess HOL-Nominal,
HOL-MicroJava, HOL-Probability are easily accessible sessions to tackle
next.

OK, so much to say on that topic by now.

Florian

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

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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

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

Indeed, this is where, as I deem, we current are:
* Some agreement that mixing sets and predicate syntax in specifications
has drawbacks.
* We try where we get if we reduce this.

Whether this will ultimately result in a separte set type constructor is
still an open question.

All the best,
Florian

-- 

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

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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

> 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 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-23 Thread Alexander Krauss


On 08/23/2011 01:51 PM, Lawrence Paulson wrote:

I'm starting to have doubts about this entire procedure.

I thought the plan was to get these theories (particularly in the
AFP) into a state where they no longer dependent on confusing sets
with predicates so that they would work with either version of
Isabelle.


Only where this is possible. The purpose of all this work is to see 
where it is not possible and find out why. After all, these issues may 
point to difficulties that users will later experience with the change 
as well.



I'm not sure that's possible. I got DataRefinementIBP
working with the set-version, but now it doesn't work with the
standard version. For one thing, it needs a class declaration for
type set, which obviously cannot work with the standard version,


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


(but maybe you already did this???)


but
other proofs also fail to work with the standard version.


I'd like to (and others probably too) look at those proofs. Is there 
anything fundamental hidden there???


Can you send me a bundle of your changes, so that I can put them on the 
web for people to look at?


- hg ci  # commit your changes locally
- hg bundle SOME_FILENAME http://afp.hg.sourceforge.net/hgweb/afp/afp/
- send me the file SOME_FILENAME, created in the previous step

The second command will produce a file which contains all your 
changesets that are not in the central afp repos (i.e., your new changes).


I'll put it up somewhere where people can look at it...

Alex
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-08-22 Thread Brian Huffman

On Mon, Aug 22, 2011 at 8:01 AM, Lawrence Paulson  wrote:
> I've come across something strange in the file 
> isabelle/afp/devel/thys/DataRefinementIBP/Diagram.thy and was wondering if 
> anybody could think of an explanation.
>
> A proof works only if I insert before it the following:
>
> instance "set" :: (type) complete_boolean_algebra
> proof
> qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def Inf_bool_def 
> Sup_bool_def)
>
> this is strange because this exact text already appears in the file 
> Complete_Lattice.thy (I refer to Florian's version of HOL), which is imported 
> by Main, which is indirectly imported by Diagram. And just in case I was 
> mistaken on this last point, I modified Diagram to import Main explicitly, 
> just to be sure. This instance declaration is still necessary.
>
> I just don't get this. I thought that an instance declaration lasted for ever.

DataRefinementIBP/Preliminaries.thy contains the following line:

class complete_boolean_algebra = distributive_complete_lattice + boolean_algebra

So your instance proof above is for class
Preliminaries.complete_boolean_algebra, while the instance in
Complete_Lattice.thy is for the separate
Complete_Lattice.complete_boolean_algebra class.

- Brian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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-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: "(\x. R x x) \  symp R
\  transp R \  part_equivp R" apply
(simp add: part_equivp_def) -- {* (I) "sane" proof state *} apply
auto -- {* (II) "insane" proof state *} apply (auto elim: sympE
transpE) -- {* (III) does not even terminate; adding "simp add:
mem_def" succeeds! *}

The second »auto« imposes a »\« on predicates, although mem_def,
Collect_def or similar do not appear in the proof text (push to the
»wrong world«).  Worse, the final auto does not even terminate, this
is what I had in mind when referring to an enlarged search space.
Here, the way the system is build forces me to use »simp add:
mem_def«.


Thanks for clarifying. This is a very good example. In essence, it boils
down to this:

lemma "(A :: 'a => bool) = B"
apply (rule) (* subset_antisym, introduces set connectives *)

I have predicates in mind (and in the context, A and B may be used as
predicates), but this is not visible from the goal state, which contains
only equality. Then, the system will apply subset_antisym, which is
incorrect. subset_antisym is declared [intro!], so this happens with
auto, too. Then the user has no choice but unfold mem_def, to get back
into a sane state.

So I would say this is not so much about search space but about the fact
that automated tools actually need the proper type information to behave
correctly!


* The logical identification of sets and predicates prevents
some

reasonable simp rules on predicates: e.g. you cannot have (A
|inf| B) x = A x&  B x because then expressions like "set xs
|inter| set ys" behave strangely if the are eta-expanded (e.g.
due to induction).

This sounds more like a problem with the underlying infrastructure
that should be fixed, rather than working around the problem by
introducing new type constructors. Can you give an example of a
proof by induction, where eager eta expansion leads to an
unnecessarily complicated proof?


theory Scratch imports Main "~~/src/HOL/Library/Lattice_Syntax"
begin

declare List.set_append [simp del]

thm sup_apply declare sup_apply [simp]

lemma set_append: "set (xs @ ys) = (set xs \  set ys)" apply
(induct xs) apply simp_all apply auto -- {* non-termination! *}



Nice example again.

Actually, there's a fundamental inconsistency in the current setup in
that some operations (like Un) are identified with the lattice
operations, where as other operations like membership or comprehension
are syntactically distinct. So whenever only connectives of the first
kind occur in the goal, the automation can apply rules of both types,
which possibly "specializes" the type to one of the two variants.

Looks pretty much that one cannot really do without the type
information... I wonder if similar effects can occur in other HOLs...


The current
implementation of subtyping allows to declare only one map function
for a type constructor. Thus, we can have either the contravariant
or the covariant map for the function type, but not both at the
same time. The introduction of set as an own datatype would resolve
this issue.



This is an interesting oberservation which also applies to the
instantiation of sets for type classes: in 'a =>  bool, you have to
think about 'a in a contravariant fashion, whereas in 'a set it is
covariant.


The situation in monotonicity checking (as part of Nitpick) is exactly 
this covariant vs. contravariant issue. We resolved it by re-inferring 
the whole thing.


So, from subtyping point of view, sets and predicates are really two 
different beasts...


Alex
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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:
  "(\x. R x x) \ symp R \ transp
R \ part_equivp R"
  apply (simp add: part_equivp_def)
  -- {* (I) "sane" proof state *}
  apply auto
  -- {* (II) "insane" proof state *}
  apply (auto elim: sympE transpE)
  -- {* (III) does not even terminate; adding "simp add: mem_def"
succeeds! *}

The second »auto« imposes a »\« on predicates, although mem_def,
Collect_def or similar do not appear in the proof text (push to the
»wrong world«).  Worse, the final auto does not even terminate, this is
what I had in mind when referring to an enlarged search space.  Here,
the way the system is build forces me to use »simp add: mem_def«.

(Well, joking you could also argue that there are three thing which
LISP, Java and Isabelle have in common: strange syntax, not writable
without special tool support, choking as soon as higher-order things
come in.)

>> * The logical identification of sets and predicates prevents some
>> > reasonable simp rules on predicates: e.g. you cannot have (A |inf| B) x
>> > = A x & B x
>> > because then expressions like "set xs |inter| set ys" behave strangely
>> > if the are eta-expanded (e.g. due to induction).
> This sounds more like a problem with the underlying infrastructure that should
> be fixed, rather than working around the problem by introducing new type 
> constructors.
> Can you give an example of a proof by induction, where eager eta expansion 
> leads
> to an unnecessarily complicated proof?

theory Scratch
imports Main "~~/src/HOL/Library/Lattice_Syntax"
begin

declare List.

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

2011-08-19 Thread Alexander Krauss

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

I think he omitted to mention type classes. It comes up again and again
on the mailing list.

Really?

Yes. You yourself discovered right away that you cannot just treat a set
like a predicate in this respect:

set_plus: "A + B == {c. EX a:A. EX b:B. c = a + b}"
func_plus: "f + g == (%x. f x + g x)"

See the emails that Alex sent around recently. We gave up on set_plus.

Ok, this (and set_times, which is similar) is the only instance that I
knew about, from the old thread.

At the time, we concluded that this one wasn't really so important, and
I think I would still come to the same conclusion today: The difference
between the current version and the old version
(http://isabelle.in.tum.de/repos/isabelle/file/878c37886eed/src/HOL/Library/SetsAndFunctions.thy)
is mostly notational (we still get the monoid lemmas by a locale
interpretation), and even the type class version is not fully
satisfactory compared with mathematical practice, where one would also
ad-hoc-overload + to write x + A, which has to be x +o A in Isabelle.

Later, people wanted to do just that more than once. Here is one instance:

http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/1689/focus=1697

There are others.

I wonder if there are also *different* instances, where we actually want
"set" to be an instance of some type class, which cannot be achieved
using "fun" and "bool". It seems that in 2008, no other instances had to
be given up, but maybe new opportunities for use of classes arised after
that? HOLCF? Multivariate_Analysis? My gut feeling is that there must be
such cases, but I'd be much more confident if somebody actually showed
me a few.

Alex
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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 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 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 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 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-18 Thread Tobias Nipkow

Am 19/08/2011 00:00, schrieb Stefan Berghofer:
> Alexander Krauss wrote:
>> I want to emphasize that the limitation of the code generator mentioned
>> here not only applies to sets-as-predicates but also to
>> maps-as-functions and other abstract types that are often specified in
>> terms of functions (finite maps, almost constant maps, etc.). Thus,
>> having good old 'a set back is does not fully solve this problem as a
>> whole, just one (important) instance of it.
>>
>> My view on this whole topic is outlined in the report I recently sent
>> around (http://www4.in.tum.de/~krauss/papers/refinement.pdf, not updated
>> since last time). In the long run, I would prefer to see flexible
>> transport machinery to move stuff between isomorphic types.
> 
> Hi Alex,
> 
> thanks for your excellent report, I fully agree with this view. There is
> often a tradeoff between executability and conciseness / abstractness of
> specifications, so I don't think it is a good idea to tweak the logic in
> such a way that it is more suitable for code generation.

Having a separate type set is more not less abstract. Just like LISP is
not more abstract than ML. It allows us to regain a few important things
we lost. Sets as predicates are indeed more concise (you don't need {x.
P x} and %x. x : S), but this is just a matter of degree, not a complete
loss of some feature.

If we could freely mix sets and predicates as we had hoped, it would be
different. But proof support is lacking. Not just in Isabelle/HOL, but
Michael Norrish tells me that in HOL4 it is also better not to mix sets
and predicates if you want proof automation.

> For example,
> HOL/MicroJava/DFA/Kildall.thy uses the SOME operator to select an element
> from the worklist, which is highly non-executable but more abstract, since
> one does not have to commit to a particular strategy for selecting the 
> element.

This is a misunderstanding. The SOME operator *does* commit to a
particular strategy, but we do not know which one. Which means that we
can never prove it equivalent to any strategy. SOME is both abstract and
concrete in a way that defeats implementation.

Tobias

> Greetings,
> Stefan
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-08-18 Thread Tobias Nipkow

Am 19/08/2011 00:10, schrieb Stefan Berghofer:
> Tobias Nipkow wrote:
>> Am 12/08/2011 11:27, schrieb Alexander Krauss:
>>> On 08/12/2011 07:51 AM, Tobias Nipkow wrote:
 The benefits of getting rid of set were smaller than expected but quite
 a bit of pain was and is inflicted.
>>> Do you know of any more pain, apart from what Florian already mentioned?
>>
>> I think he omitted to mention type classes. It comes up again and again
>> on the mailing list.
> 
> Really?

Yes. You yourself discovered right away that you cannot just treat a set
like a predicate in this respect:

  set_plus: "A + B == {c. EX a:A. EX b:B. c = a + b}"
  func_plus: "f + g == (%x. f x + g x)"

See the emails that Alex sent around recently. We gave up on set_plus.

Later, people wanted to do just that more than once. Here is one instance:

http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/1689/focus=1697

There are others.

Tobias

> 
>   http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/260/
> 
> cited by Brian and Alex, Brendan was worried about the fact that one could
> no longer declare arities for sets. In my reply to his mail, I pointed
> out that arities for sets could usually be rephrased as arities for functions
> and booleans. I also asked him to give a concrete example for an arity where
> this was not possible, but I never got a reply, so I assume that this is not
> so much of a problem.
> 
> Greetings,
> Stefan
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-08-18 Thread Gerwin Klein

On 19/08/2011, at 8:10 AM, Stefan Berghofer wrote:

> Tobias Nipkow wrote:
>> Am 12/08/2011 11:27, schrieb Alexander Krauss:
>>> On 08/12/2011 07:51 AM, Tobias Nipkow wrote:
 The benefits of getting rid of set were smaller than expected but quite
 a bit of pain was and is inflicted.
>>> Do you know of any more pain, apart from what Florian already mentioned?
>> 
>> I think he omitted to mention type classes. It comes up again and again
>> on the mailing list.
> 
> Really? In the thread
> 
>  http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/260/
> 
> cited by Brian and Alex, Brendan was worried about the fact that one could
> no longer declare arities for sets. In my reply to his mail, I pointed
> out that arities for sets could usually be rephrased as arities for functions
> and booleans. I also asked him to give a concrete example for an arity where
> this was not possible, but I never got a reply, so I assume that this is not
> so much of a problem.

Given his employer Brendan not giving an example is no real indication either 
way ;-)

I'm not convinced that any class that works for sets can be expressed nicely as 
a class on the function type and booleans. Splitting up the declaration over 
two types at least makes it hard to think about. You're right, though, that it 
may be less of a problem than we currently have the feeling it is. It hasn't 
prevented anything yet that we wanted to do at NICTA.

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

Cheers,
Gerwin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-08-18 Thread Gerwin Klein

On 19/08/2011, at 5:56 AM, Alexander Krauss wrote:
> Here are some critical questions/comments towards two of Florian's initial 
> arguments pro 'a set.
> 
> [...]
> 
>> * Similarly, there is a vast proof search space for automated tools
>> which is not worth exploring since it leads to the »wrong world«, making
>> vain proof attempts lasting longer instead just failing.
> 
> Can this claim be made more concrete (or even quantitative)? Or is it merely 
> a conjecture?
> 
> From what Jasmin wrote, this does not seem to hold for sledgehammer, and 
> simp/auto/blast should not run into the "wrong world" when configured 
> properly.
> 
> I understand that this is true for naive users... but automated tools???

Can't really quantify it, but I'm seeing this all the time from not-so-novice 
users over here. Mixing sets and predicates (e.g. using intersection on 
predicates) works often enough that people like it and overuse it. Sooner or 
later you will see unfolding of mem_def. As opposed to unfolding conjunction, 
unfolding mem_def proves things that otherwise simp/auto/etc fail on.

Gerwin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

Florian Haftmann wrote:
> just do something like (unfold mem_def) and your proof will be a mess
> since you have switched to the "wrong world".

Like any definition of a primitive operator, mem_def is not really intended
to be unfolded by the user, so don't be surprised if your proof is a mess
after unfolding this definition. You wouldn't unfold the definitions of
logical operators like "conj" or "disj" either, except for proving
introduction- or elimination rules for these operators.

> * The logical identification of sets and predicates prevents some
> reasonable simp rules on predicates: e.g. you cannot have (A |inf| B) x
> = A x & B x
> because then expressions like "set xs |inter| set ys" behave strangely
> if the are eta-expanded (e.g. due to induction).

This sounds more like a problem with the underlying infrastructure that should
be fixed, rather than working around the problem by introducing new type 
constructors.
Can you give an example of a proof by induction, where eager eta expansion leads
to an unnecessarily complicated proof?

Greetings,
Stefan
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

Am 19.08.2011 um 00:00 schrieb Stefan Berghofer:

> thanks for your excellent report, I fully agree with this view. There is
> often a tradeoff between executability and conciseness / abstractness of
> specifications, so I don't think it is a good idea to tweak the logic in
> such a way that it is more suitable for code generation.

Indeed, I think a general point can be made here, and not just about code 
generation. In the last couple of years, we've run into situations in 
Quickcheck, Nitpick, the code generator, and perhaps more, where we felt the 
need for sets as different from functions. However, there is no guarantee that 
all the people who talked about "sets vs. functions" meant, or needed, the same 
thing!

For Nitpick (and code generation I guess), it helps to know whether a predicate 
is a finite set or not. However, we can't expect the entire world to understand 
"'a set" as a finite set built from {} by adding elements one by one -- and 
what's the type constructor for the complement of such a set anyway? For 
Nitpick, Alex and I solved the problem generally by inferring "finite sets" as 
well as "complements of finite sets" in addition to plain functions [1, sect. 
6]. Needless to say, we're in better shape with our robust inference than by 
just crossing our fingers, hoping that the user distinguishes between "'a set" 
and "'a => bool" the way we intend to.

Jasmin

[1] http://www4.in.tum.de/~blanchet/jar2011-mono.pdf
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

Tobias Nipkow wrote:
> Am 12/08/2011 11:27, schrieb Alexander Krauss:
>> On 08/12/2011 07:51 AM, Tobias Nipkow wrote:
>>> The benefits of getting rid of set were smaller than expected but quite
>>> a bit of pain was and is inflicted.
>> Do you know of any more pain, apart from what Florian already mentioned?
> 
> I think he omitted to mention type classes. It comes up again and again
> on the mailing list.

Really? In the thread

  http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/260/

cited by Brian and Alex, Brendan was worried about the fact that one could
no longer declare arities for sets. In my reply to his mail, I pointed
out that arities for sets could usually be rephrased as arities for functions
and booleans. I also asked him to give a concrete example for an arity where
this was not possible, but I never got a reply, so I assume that this is not
so much of a problem.

Greetings,
Stefan
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

Alexander Krauss wrote:
> I want to emphasize that the limitation of the code generator mentioned
> here not only applies to sets-as-predicates but also to
> maps-as-functions and other abstract types that are often specified in
> terms of functions (finite maps, almost constant maps, etc.). Thus,
> having good old 'a set back is does not fully solve this problem as a
> whole, just one (important) instance of it.
> 
> My view on this whole topic is outlined in the report I recently sent
> around (http://www4.in.tum.de/~krauss/papers/refinement.pdf, not updated
> since last time). In the long run, I would prefer to see flexible
> transport machinery to move stuff between isomorphic types.

Hi Alex,

thanks for your excellent report, I fully agree with this view. There is
often a tradeoff between executability and conciseness / abstractness of
specifications, so I don't think it is a good idea to tweak the logic in
such a way that it is more suitable for code generation. For example,
HOL/MicroJava/DFA/Kildall.thy uses the SOME operator to select an element
from the worklist, which is highly non-executable but more abstract, since
one does not have to commit to a particular strategy for selecting the element.

Greetings,
Stefan
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

Am 18.08.2011 um 21:40 schrieb Alexander Krauss:

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

Sounds like a good idea, but make sure also to remove the following lines in 
"sledgehammer_filter.ML":

(* Set constants tend to pull in too many irrelevant facts. We limit the damage
   by treating them more or less as if they were built-in but add their
   definition at the end. *)
val set_consts =
  [(@{const_name Collect}, @{thms Collect_def}),
   (@{const_name Set.member}, @{thms mem_def})]

And (effectively) replace "set_consts" with the empty list, ideally simplifying 
the code as you go. This will degrade the quality of the relevance filtering 
slightly, but would have to be done anyway when "'a set" is reintroduced.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

Alexander Krauss wrote:
> In particular, Stefan discovered that replacing inductive set
> definitions by predicates was by no means as easy as everybody had
> expected. One good example is the small-step relation from Jinja and
> its various cousins. It had type "((expr * state) * (expr * state))
> set", and turning it into a 4-ary predicate (expr => state => expr =>
> state => bool) would cause problems with either version of the
> transitive closure operator. [Btw, the newer HOL/IMP/Small_Step.thy
> uses a binary predicate over pairs, which requires massaging the
> induction rule using [split_format (complete)]].

Hi all,

let me take the opportunity to advertise a useful feature of the induct
method that avoids such manual "massaging" of induction rules. For example,
the command

  proof(induct rule: small_step_induct)

in HOL/IMP/Types.thy can be replaced by

  proof(induct "(c,s)" "(c',s')" arbitrary: c s c' s' rule: small_step.induct)

which allows the standard induction rule small_step.induct to be used instead
of the small_step_induct rule produced using split_format, which is a bit of
a hack anyway. The above is a shorthand for

  proof(induct x=="(c,s)" y=="(c',s')" arbitrary: c s c' s' rule: 
small_step.induct)

Since revision b0aaec87751c (Jan 2010), the equational constraints arising from
such invocations of induct are solved automatically using injectivity / 
distinctness
rules for datatypes, so the rest of the proof script works as if the custom-made
induction rule had been applied.

Greetings,
Stefan
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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


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

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 Florian Haftmann

envisaged working plan
--

a) general
* continue discussion about having set or not, end with a summary (for
the mailing list archive)
* provide repository
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/ with
newest changesets from Isabelle main repository, keep HOL image building
(Florian)
* figure out with type class instances for set to add (maybe as a
provisory in a separate theory)
  > grep -rIPn '(instantatiation|instance).*(bool|"fun").*::' src/HOL
* examine changesets e8cc166ba123 to ec46381f149d for changes done to
packages etc., from there distill/assert necessary back-changes to
inductive_set etc.

b) elimination of set/pred mixture
* backport admissible changes from isabelle_set to isabelle (Florian)
* eliminate occurences of mem_set and Collect_def in distribution and
AFP theories AFAP, propagate back to main repository
* figure out problem with »force« in ex/Set_Theory.thy
* figure out problem with »refute« in ex/Refute_Examples.thy with
"distinct [a, b]" (examine changes done to refute since 2008)

c) consolidation
* get isabelle_set running
* (maybe)
  > hide_fact (open) Set.mem_def Set.Collect_def
  to indicate that something is going on with these

d) RELEASE

e) introduce set type constructor
* backport necessary changes (as little invasive as possible) from
isabelle_set
* distribute type class instances for set over theories appropriately
* add naive code generator setup for sets in Set.thy
* drop theory Executable_Set
* drop optional special type alias treatment in Pure/Isar/code.ML (Florian)
* drop theory CSet (naive version, maybe not quotient version)
* mark _apply rules for pointwise operations on functions as [simp]
* provide theories Dlist_Set, RBT_Set (or maybe Mapping_Set), etc.

Florian

-- 

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

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

Hi all,

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

Am 12.08.2011 um 11:27 schrieb Alexander Krauss:

> What are, actually, the losses when going back? This has not yet been touched 
> by this thread at all (except the compatibility/import issue mentioned by 
> Brian), and at least myself I wouldn't feel comfortable answering this 
> question just now...

For Sledgehammer, reverting would be a (fairly) small loss. At the ATP level, 
types are erased (or encoded), and it doesn't really matter if something is a 
"'a set" or a "'a => bool". Higher-order functions and predicates are 
translated as simple values of the universe, and when they are applied this is 
done using an explicit operator called "hAPP". Apart from the order of the 
arguments, there is no difference between "hAPP" and "Set.member".

Hence, the main difference to the ATPs is whether we have 
"mem_def"/"Collect_def" to bridge the two worlds or the weaker 
"mem_Collect_def". "mem_def" and "Collect_def" seem more flexible in that 
respect, and it's no coincidence that several "metis" calls with one or the 
other were found when reintroducing "'a set". (On the other hand, one could 
argue that "mem_def"/"Collect_def" are more useful to prove things today in the 
current state of mismatch, cf. "Multivariate_Analysis", than they would have 
been a few years ago right after the elimination of "'a set".)

Sledgehammer and Metis also have a flag that preprocesses away all "member" and 
"Collect" before doing the proof search. For Sledgehammer, the success rate for 
a single prover went up by about .5% -- which is good but not fantastic. This 
option is still off by default because it needs a more thorough evaluation and 
it broke at least one Metis proof (for no deep reason, except what I'd call "a 
failure to perform").

For Nitpick, reintroducing sets wouldn't make any difference in terms of 
performance one way or the other, since "'a set" and "'a => bool" are 
isomorphic and hence as many bits are required to code one or the other. I 
would need to spend some time to make Nitpick (and Refute) work smoothly, 
though, and there are many more urgent things on my plate, so don't hold your 
breath.

My personal gut feeling is that if we are to have "Collect" and "member" at 
all, then it might be just as well that we keep them separated from the rest 
using type discipline, to catch various stylistic horrors. But beyond from this 
I'm not leaning one way or another.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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 – feasibility study

Am 18.08.2011 um 09:18 schrieb Florian Haftmann:

> Strange.  I guess refute was not modified in 2008 (at least according to
> hg diff -r e8cc166ba123 -r ec46381f149d | grep -i refute).  Maybe this
> crept in silently over the last years?

It was not modified in 2008, but it was modified in 2009. It wasn't using 
antiquotation, so its support for "set"s was just hanging around dead. If you 
look more closely at the history, you'll see what needs to be reverted.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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