[isabelle] Type classes and parameters


I am looking for a good way to express some basic mathematical objects in the current Isabelle/HOL framework.

Here is a representative example of my question. Let 'a be a compact metric space. Then a function f from 'a to real numbers is c-HÃlder continuous (where c>0 is some given positive real number) if it is continuous and
(*_c) : sup_{x \neq y} |f(x)-f(y)|/ d(x,y)^c
is finite. It is easy to check that the set of c-HÃlder continuous functions is a Banach space, for the norm equal to the sup norm plus *_c.

In a mathematical paper, I would write this as:
Thm: Let X be a compact metric space, let c>0. Then the set of c-HÃlder continuous functions on X (with the above norm) is a Banach space.

My question is how to express this theorem in Isabelle/HOL in the best way using locales/type classes (given that Banach spaces are type classes). And then write conveniently statements such as: the inclusion of c-HÃlder continuous functions in d-HÃlder continuous functions is a continuous injection when d<c.

Any hint?


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