Re: [isabelle-dev] Syntax for lattice operations?

[Tobias Nipkow]

On 12/06/2016 18:22, Florian Haftmann wrote:

Thus I would like to understand why we cannot reuse Sup etc in HOLCF
like we do for all the other variants of lattices we have. We would
probably need a suitable type class because at the moment lub is
unrestricted.


For each type class, per type constructor there is at most *one*
instance.

If we use the standard HOL class hierarchy for HOLCF, we
would e.g. enforce the order on pairs to be component-wise due to the
required / given instance of cpo in HOLCF and hence rule out e.g.
lexicographic ordering on pairs.  Hence the use of a separate
type class hierarchy makes sense for that specific application.


You are saying that the problem is the ordering which would be shared, which is 
why we use "⊑" in HOLCF rather than "<=".


But that argument applies to any instantiation of the order on products. That 
is, any application that instantiates the product order should therefore not use 
the generic "<="? Probably not if it is a development that is supposed to be the 
basis for many others, like HOLCF?


So maybe the deeper reason is indeed the usual problem with type classes, in 
which case I would support the plain ASCII "LUB".


Tobias


Cheers,
Florian





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Syntax for lattice operations?

[Florian Haftmann]

> Thus I would like to understand why we cannot reuse Sup etc in HOLCF
> like we do for all the other variants of lattices we have. We would
> probably need a suitable type class because at the moment lub is
> unrestricted.

For each type class, per type constructor there is at most *one*
instance.

If we use the standard HOL class hierarchy for HOLCF, we
would e.g. enforce the order on pairs to be component-wise due to the
required / given instance of cpo in HOLCF and hence rule out e.g.
lexicographic ordering on pairs.  Hence the use of a separate
type class hierarchy makes sense for that specific application.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.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] Syntax for lattice operations?

[Tobias Nipkow]

On 11/06/2016 21:26, Florian Haftmann wrote:

For the moment I think bold syntax in the first choice.  In the middle
run I would suggest to have a closer look at HOLCF/Porder.thy to see
whether something can be done to integrate it more with the standard
type classes;  a least it formalizes a lot about upper / lower bounds
which is not HOLCF-specific in any way, so it could go to HOL/Library
for example.


After a closer look I came to conclusion that the use of Sup syntax in
HOLCF/Porder.thy is very application-specific.  And it is a deliberate
separate type class hierarchy since these type classes are tailored
towards continuous function space.

So maybe the best option here is to stay with plain ASCII syntax: ‹LUB
x∈A. f x›. – to emphasize its somewhat specific application.


The lub operation in is a lattice-theoretic supremum. So in principle we should 
be able to use operator names and syntax for that; otherwise there is something 
wrong (or maybe our type classes are inadequate).


Thus I would like to understand why we cannot reuse Sup etc in HOLCF like we do 
for all the other variants of lattices we have. We would probably need a 
suitable type class because at the moment lub is unrestricted.


Tobias


Cheers,
Florian



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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Syntax for lattice operations?

[Florian Haftmann]

Hi Makarius,

Am 11.06.2016 um 00:13 schrieb Makarius:
> On 10/03/16 11:19, Makarius wrote:
>> On Thu, 10 Mar 2016, Johannes Hölzl wrote:
>>
>>> Alternatively: Would a lattice_syntax locale work nowadays? I remember
>>> I tried it once and for some reason it didn't work. Either notations
>>> aren't supported in locales or they are exported after the context
>>> -block.
>>
>> The concept of 'bundle' was introduced for that, e.g. to allow "includes
>> lattice_syntax" for local contexts.
>>
>> Unfortunately, it is not quite finished: notation within bundles is not
>> yet supported. It might be relatively easy to do that, but I am
>> presently working in other corners of the system.
> 
> This thread is still pending, while the bundle concept has been enhanced
> in Isabelle/a59801b7f125.

first, thanks for implementing this;  we can now really move forward
wrt. more flexible syntax.

> This shows changes are only needed in relatively isolated places – so
> far there was not even any attempt to use the more flexible type class
> operations of main HOL instead of independent operations with
> alternative (bold) syntax.
> 
> How shall we proceed? Make Lattice_Syntax standard and cleanup
> conflicting applications?

I had a quick look at the changesets; as far as I can glimpse, most
occurences are due to LUB from HOLCF/Porder.thy.

For the moment I think bold syntax in the first choice.  In the middle
run I would suggest to have a closer look at HOLCF/Porder.thy to see
whether something can be done to integrate it more with the standard
type classes;  a least it formalizes a lot about upper / lower bounds
which is not HOLCF-specific in any way, so it could go to HOL/Library
for example.

There are various occurences of no_notation etc. in the HOL and AFP
theories which I will inspect to see what can be done there.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.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] Syntax for lattice operations?

[Makarius]

On 10/03/16 11:19, Makarius wrote:
> On Thu, 10 Mar 2016, Johannes Hölzl wrote:
> 
>> Alternatively: Would a lattice_syntax locale work nowadays? I remember
>> I tried it once and for some reason it didn't work. Either notations
>> aren't supported in locales or they are exported after the context
>> -block.
> 
> The concept of 'bundle' was introduced for that, e.g. to allow "includes
> lattice_syntax" for local contexts.
> 
> Unfortunately, it is not quite finished: notation within bundles is not
> yet supported. It might be relatively easy to do that, but I am
> presently working in other corners of the system.

This thread is still pending, while the bundle concept has been enhanced
in Isabelle/a59801b7f125.

One extra complication for Lattice_Syntax.thy (in contrast to
FinFun.thy) is the use of raw 'syntax' declarations, which are not
localized and thus cannot be put into bundles. (There might be other
ways to do that.)


I have also started an experiment to keep INF and SUP symbol syntax in
main HOL and eliminate clashes in the applications. In the middle of
that I kept all of Lattice_Syntax.thy and eliminated clashes of "inf"
and "sup" syntax as well. The resulting changesets are included.

This shows changes are only needed in relatively isolated places – so
far there was not even any attempt to use the more flexible type class
operations of main HOL instead of independent operations with
alternative (bold) syntax.


How shall we proceed? Make Lattice_Syntax standard and cleanup
conflicting applications?


Makarius



ch-lattice_syntax1.gz
Description: application/gzip


ch-lattice_syntax2.gz
Description: application/gzip
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Syntax for lattice operations?

[Tobias Nipkow]

On 10/03/2016 11:00, Florian Haftmann wrote:

Hi all,

traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been
kept in a separate library theory, to allow use of that quite generic
notation for unforeseen applications.

Meanwhile however all those operations to which that syntax is attached
to are members of syntactic type classes.  It could be worth to attempt
to make that syntax standard, using funny subscripts or similar for the
more exotic cases.


Florian, what are the more exotic cases?

Tobias


Cheers,
Florian



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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Syntax for lattice operations?

[Makarius]

On Thu, 10 Mar 2016, Johannes Hölzl wrote:

Alternatively: Would a lattice_syntax locale work nowadays? I remember I 
tried it once and for some reason it didn't work. Either notations 
aren't supported in locales or they are exported after the context 
-block.


The concept of 'bundle' was introduced for that, e.g. to allow "includes 
lattice_syntax" for local contexts.


Unfortunately, it is not quite finished: notation within bundles is not 
yet supported. It might be relatively easy to do that, but I am presently 
working in other corners of the system.



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

Re: [isabelle-dev] Syntax for lattice operations?

[Florian Haftmann]

> What would be the objective of this change?

Mainly to get rid of those brittle (no_)notation declarations scattered
over various theories.  Organizing syntax through library theories does
not quite work out.

Florian

> 
>> On 10 Mar 2016, at 10:00, Florian Haftmann 
>>  wrote:
>>
>> Hi all,
>>  
>> traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been
>> kept in a separate library theory, to allow use of that quite generic
>> notation for unforeseen applications.
>>
>> Meanwhile however all those operations to which that syntax is attached
>> to are members of syntactic type classes.  It could be worth to attempt
>> to make that syntax standard, using funny subscripts or similar for the
>> more exotic cases.
>>
>> Cheers,
>>  Florian
>>
>> -- 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.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] Syntax for lattice operations?

[Lawrence Paulson]

What would be the objective of this change?
Larry

> On 10 Mar 2016, at 10:00, Florian Haftmann 
>  wrote:
> 
> Hi all,
>   
> traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been
> kept in a separate library theory, to allow use of that quite generic
> notation for unforeseen applications.
> 
> Meanwhile however all those operations to which that syntax is attached
> to are members of syntactic type classes.  It could be worth to attempt
> to make that syntax standard, using funny subscripts or similar for the
> more exotic cases.
> 
> Cheers,
>   Florian
> 
> -- 

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

Re: [isabelle-dev] Syntax for lattice operations?

[Johannes Hölzl]

Am Donnerstag, den 10.03.2016, 11:00 +0100 schrieb Florian Haftmann:
> Hi all,
>   

> 
> traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been
> kept in a separate library theory, to allow use of that quite generic
> notation for unforeseen applications.
> 
> Meanwhile however all those operations to which that syntax is attached
> to are members of syntactic type classes.  It could be worth to attempt
> to make that syntax standard, using funny subscripts or similar for the
> more exotic cases.
> 
> Cheers,
>   > Florian

Yes absolutely. I recently added by accident Lattice_Syntax somewhere
in the Library and a lot of AFP theories (and HOLCF) broke down at
unexpected places.

Alternatively: Would a lattice_syntax locale work nowadays? I remember
I tried it once and for some reason it didn't work. Either notations
aren't supported in locales or they are exported after the context
-block.

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