Defining a generic real function in Isabelle 2015

Question

In Isabelle2014 I was able to define a generic function which takes a natural number and a real number and outputs a real number in the following way:

definition example :: "nat ⇒ real ⇒ real"
where "example i = real"

However, I am unable to this in Isabelle2015. I get the following error:

Bad head of lhs: "λx. example i (real x)"
The error(s) above occurred in definition:
"λx. example i (real x) ≡ real"

Has the method of defining a generic real function changed in the newer version of Isabelle? How can I define a generic function as I used to?

I've looked through the newer Isabelle documentation however I have been unable to find anything which relates to the following case.

Do you want to define a function ignoring its first argument, or a function converting the first argument from nat to real, ignoring the second argument? In both cases, the example you will not do what you want, neither in 2014 or 2015. — Lars Noschinski
@LarsNoschinski I want to define a function which ignores the first argument and outputs a real number using the second argument. The output will be of type real, however I want to avoid using a specific functional form. How would I be able to achieve this? — A K
@JoachimBreitner Apologies for the confusion; by generic I mean I want to avoid explicitly defining a function and instead just work with a real output — A K

Unknown Unknown · Accepted Answer · 2015-07-19T21:20:19

Myself, I always have on declare[[show_sorts=true]] and declare[[show_consts=true]], so I see things about type classes and types that I otherwise wouldn't see and think about.

In Isabelle2015, you have

term "real :: 'a∷real_of => real".

But in Isabelle2014, it's

term "real :: 'a::type => real".

Apparently, the type class real_of is new in Isabelle2015.

I use the command print_classes in both Isabelle2015 and Isabelle2014, and search on the results in the output panel.

Nothing shows up for real_of in Isabelle2014, but in Isabelle2015 I get

class real_of:
  supersort: type
  parameters:
    real :: 'a => real
  instances:
    int :: real_of
    nat :: real_of

This shows that only int and nat have been instantiated for real_of. You can change your example to this:

definition example :: "nat => 'a::real_of => real" where 
  "example i = real"

Defining a generic real function in Isabelle 2015

2 Answers