# Re: [isabelle] Type classes and parameters

Hi Esseger,

one option you would have is to somehow encode the parameter in a type.
For example you could use Numeral_Types to represent natural numbers at
the type level, as it is done in Multivariate_Analysis.

Another hack is to introduce a type class real_value:

class real_value =
fixes real_value :: 'a itself => real

which assign to an arbitrary type a real value. Then you could express
c-HÃlder continuous functions as a type. And also your inclusion
statement:

lemma
fixes C :: "'c :: real_value"  and D :: "'c :: real_value"
assumes "real_value ITSELF('c) > real_value ITSELF('d)"
shows "EX i :: ('a, 'c) hÃlder => ('a, 'd) hÃlder. ..."
...

Problem is: it is currently not possible to construct a
"'a::real_value" in a proof! OndÅej KunÄar and Andrei Popescu work on a
solution but it is not there yet.

I hope this helps!

- Johannes

Am Mittwoch, den 02.03.2016, 22:30 +0100 schrieb Esseger:
> Maybe I wasn't clear enough that the only problem I have is that the
> Banach spaces depend on a parameter. A similar question would arise when
> defining for instance the L^p spaces, for p in [1, \infty) (maybe the
> most prominent missing block in Multivariate_Analysis).
>
> Does the absence of answer mean that there is no nice way to do this in
> current Isabelle, and that tools with dependent type theory such as CoQ
> would be better suited for the task? That would be very sad in my
> opinion, as Isar is by far more mathematician-friendly, and the analysis
> libraries are also by far superior in Isabelle/HOL.
>
> Best,
> Esseger
>
>
>



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