*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Type classes and parameters*From*: Esseger <esseger at free.fr>*Date*: Thu, 3 Mar 2016 23:34:52 +0100*In-reply-to*: <1456995934.3724.8.camel@in.tum.de>*References*: <nanmc1$vi1$1@ger.gmane.org> <nb7m2f$ld9$1@ger.gmane.org> <1456995934.3724.8.camel@in.tum.de>*User-agent*: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:38.0) Gecko/20100101 Thunderbird/38.6.0

Sup {p. f \in L^p} ? Or do an induction on (integer) integrability exponents? Esseger 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 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

**Follow-Ups**:**Re: [isabelle] Type classes and parameters***From:*Johannes Hölzl

**References**:**Re: [isabelle] Type classes and parameters***From:*Esseger

**Re: [isabelle] Type classes and parameters***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] Type classes and parameters
- Next by Date: Re: [isabelle] partial functions: is f_rel too weak too?
- Previous by Thread: Re: [isabelle] Type classes and parameters
- Next by Thread: Re: [isabelle] Type classes and parameters
- Cl-isabelle-users March 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list