Re: [isabelle] Gcd and algebraic structures

On 02/09/14 13:07, Jose Divasón wrote:
> By the way, in your formalization I have seen you fix the euclidean
> size in the euclidean_semiring class. However, a Euclidean domain will
> admit many different euclidean size functions (in
> is suggested that a
> particular Euclidean function fis notpart of the structure of a
> Euclidean domain).
I am aware of that, but I saw no reason why a single sufficiently nice
(i.e. fulfilling the “b ≠ 0 ⟹ f (a mod b) < f a” and "b ≠ 0 ⟹ f a ≤ f
(a*b)” conditions) should not suffice. I cannot think of a circumstance
in which you might require several different euclidean size functions.

> Would it be possible to define that class this way? Could there be any
> potential drawbacks?
> class euclidean_semiring = … +
> assumes exists_euclidean_size: "∃f::'a => nat. ∀a b. b≠0 ⟶ (∃q r. a =
> b*q + r ∧ (r=0 ∨ f r < f b))"
You can do that and then define euclidean_size with Hilbert choice and
get all the properties you need with exists_euclidean_size. I see no
drawbacks, but, as stated before, I also don't see any real advantages
that would justify it – apart from the fact that you can drop the
monotonicity assumption, because if any euclidean size function exists,
then a monotonic one exists. (which you'd have to prove, of course)

> But if one uses this way of defining the euclidean_semiring class,
> then it would not be possible to get direct executability (because the
> euclidean_size would not be instantiated). Anyway, with your
> definition it would be possible to work with different euclidean sizes
> of the same structure if the instantiations are done in independent
> files. I don’t know which option is more suitable.
I do not think that this is an issue. If I recall correctly, I never use
euclidean_size in any code equations – it is only required for the
termination proof of the Euclidean algorithm, and termination measures
do not have to be executable.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.