Re: [isabelle-dev] Factorial ring

[Manuel Eberl]

"multiplicity" is definitely interesting; we could then probably define 
the "order" of a root of a polynomial in terms of "multiplicity", which 
simplifies things a bit.


I don't see why is_prime should require an algebraic_semidom; the 
definition of prime elements makes sense in any commutative semiring.


Factorial rings (also known as unique factorisation domains) usually 
demand that any non-zero element can be written as a (finite) product of 
prime factors and a unit. This representation is necessarily unique 
modulo associativity/commutativity.


Intuitively, I would think that in a normalization_semidom, this implies 
that every non-zero element only has finitely many normalised divisors, 
but I am not completely sure about this. However, this would imply that 
your current definition is, in fact, equivalent to the standard 
mathematical one, at least in the context of the (somewhat non-standard) 
normalization_semidom.



Cheers,

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

[isabelle-dev] Factorial ring

[Florian Haftmann]

Hi all,

since 4a5b81ff5992 in src/HOL/Number_Theory/Factorial_Ring.thy, there is
an abstract formalization of an factorial ring with a constructive
factorization operation:

factorization a :: 'a => 'a multiset option

Maybe other algebraists can comment on this.  I would appreciate if we
can use this is a base to push abstract algebra forward.

Two remarks have to be made:
a) The development has no auxiliary operations; maybe borrowing ideas
like multiplicity and prime_factors from UniqueFactorization can turn
proofs more compact.
b) In private discussion there was the idea to define is_prime
generically in class algebraic_semidom, rather than to provide it is a
class parameter.  Class factorial_semiring would then just assume
finite_divisors (or maybe there is a more appropriate criterion?).

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?

[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

Re: [isabelle-dev] Preferred syntax for big GCD?

[Lawrence Paulson]

I’m sympathetic to this view. On the other hand, GCD is the only one of these 
uppercase formulations that’s actually in widespread use.
Larry

> On 10 Mar 2016, at 09:46, Florian Haftmann 
>  wrote:
> 
> Since there is no generally accepted symbolic syntax for gcd, it might
> be better to let the (slightly more readable) form (a) stand.
> 
> I have no strong opinion on this.  Any suggestions?

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

Re: [isabelle-dev] Preferred syntax for big GCD?

[Tobias Nipkow]

THE, LEAST, GCD.

Tobias

On 10/03/2016 10:46, Florian Haftmann wrote:

Hi all,

in 66a381d3f88f, the usual syntax for big operators has been added for
GCD (and LCM):

   (a) Gcd x \ A. f x

An alternative could be

   (b) GCD x \ A. f x

The form (b) follows the tradition to have binders all-capitalized (SUP,
INF, UNION, INTER, THE, LEAST, SUM, PROD).

On the other hand nearly all those binders have pretty symbolic syntax,
such that the all-capitalized variants rarely show up in theory text.
Since there is no generally accepted symbolic syntax for gcd, it might
be better to let the (slightly more readable) form (a) stand.

I have no strong opinion on this.  Any suggestions?

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

[isabelle-dev] Syntax for lattice operations?

[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

-- 

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

[isabelle-dev] Explicit representation of multisets

[Florian Haftmann]

Hi all,

in recent private discussion the question was raised whether the
explicit representation of multisets should follow that of sets.

For sets, we have:
{a, b, c} = insert a (insert b (insert c empty))

For multisets, we currently have:
{#a, b, c#} = single a + single b + single c

But the following would also be possible:
{#a, b, c#} = insert# a (insert# b (insert# c empty#))

Is there any evidence that we should not attempt this?

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

[isabelle-dev] Preferred syntax for big GCD?

[Florian Haftmann]

Hi all,

in 66a381d3f88f, the usual syntax for big operators has been added for
GCD (and LCM):

  (a) Gcd x \ A. f x

An alternative could be

  (b) GCD x \ A. f x

The form (b) follows the tradition to have binders all-capitalized (SUP,
INF, UNION, INTER, THE, LEAST, SUM, PROD).

On the other hand nearly all those binders have pretty symbolic syntax,
such that the all-capitalized variants rarely show up in theory text.
Since there is no generally accepted symbolic syntax for gcd, it might
be better to let the (slightly more readable) form (a) stand.

I have no strong opinion on this.  Any suggestions?

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