Re: [isabelle] Type classes and parameters

Thanks a lot for your answer, indeed it helps! Although as far as I understand I have the impression that some useful constructions would not be expressible in this formalism. For instance, would it be possible in this way to define the integrability exponent of a function, i.e.,

Sup {p. f \in L^p} ?

Or do an induction on (integer) integrability exponents?


Le 03/03/2016 10:05, Johannes HÃlzl a Ãcrit :
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

     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.


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