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

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

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

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

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

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

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

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

[isabelle-dev] Preferred syntax for big GCD?

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

[isabelle-dev] Explicit representation of multisets

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 +

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

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

[isabelle-dev] Syntax for lattice operations?

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

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

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

[isabelle-dev] Factorial ring

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

Re: [isabelle-dev] Factorial ring

"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