Re: [isabelle] finite order allows maxima



> (a side issue: I do not understand why I cannot get alternative
> lemma (in order) "⟦ finite S; S ≠ {} ⟧ ⟹ ∃m∈S. ¬(∃x∈S. x < m)"
> )

Welcome to the wonderfully frustrating world of Isabelle typeclasses!
Unfortunately, arg_min etc. are defined with an "ord" sort constraint.
However, inside the context of the "ord" typeclass itself, you do not
yet have this sort "ord" attached to the type variable. Therefore, this
gives you a type error due to the missing sort.

In this particular case, this issue could be fixed by defining the
constants inside the typeclass:

> definition (in ord) is_arg_min :: "('b ⇒ 'a) ⇒ ('b ⇒ bool) ⇒ 'b ⇒
> bool" where
> "is_arg_min f P x = (P x ∧ ¬(∃y. P y ∧ f y < f x))"
>
> definition (in ord) arg_min :: "('b ⇒ 'a) ⇒ ('b ⇒ bool) ⇒ 'b" where
> "arg_min f P = (SOME x. is_arg_min f P x)"

Indeed I would suggest we do it that way.

There are, however, cases where this does not work: for instance, any
definition of theorem involving two different types of that type class.

This is a very annoying technical limitation of Isabelle's type classes.
Usually, there is no big downside to just defining/proving stuff outside
the typeclass using explicit sort constraints, but one situation where
it gets really annoying is when want to use constants defined outside
the typeclass in the assumptions of a new subclass (e.g. something
builting on top of euclidean_space that makes some assumptions about the
limit of some function. Limits are not defined in the type class.)

Manuel






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