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.