*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Type classes and parameters*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Fri, 04 Mar 2016 11:59:50 +0100*In-reply-to*: <nbae6e$ck4$1@ger.gmane.org>*Organization*: TU München*References*: <nanmc1$vi1$1@ger.gmane.org> <nb7m2f$ld9$1@ger.gmane.org> <1456995934.3724.8.camel@in.tum.de> <nbae6e$ck4$1@ger.gmane.org>

Hm, I think defining the integrability exponent of a function is not possible in a nice way. But in this specific case you can unfold the definition itself: Sup {p. |f^p| has_integral} I'm not sure about induction on (integer) integrability exponents... - Johannes Am Donnerstag, den 03.03.2016, 23:34 +0100 schrieb Esseger: > 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? > > 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 > > > > > > > > > > > > > > > >

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

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

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

- Previous by Date: [isabelle] Splitting if-then-else in assumptions?
- Next by Date: [isabelle] Documentation?
- Previous by Thread: Re: [isabelle] Type classes and parameters
- Next by Thread: Re: [isabelle] partial functions: is f_rel too weak too?
- 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