Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Additional type variable(s) in specification

Email Gateway (Aug 19 2022 at 12:36):

From: Joachim Breitner <breitner@kit.edu>
Hi,

I’m having a problem with function definitions in a locale with type
parameters. I reduced it to the following non-sensical code:

locale semantic_domain =
fixes tick :: "'Value ⇒ 'Value"
begin

function
myfun :: "unit ⇒ 'Value ⇒ 'Value"
where
"myfun () = (λ x. tick (myfun () x))"
oops

Gives me
Additional type variable(s) in specification of "myfun_rel": 'Value
Additional type variable(s) in specification of "myfun_dom": 'Value

It does not happen with the parameter on the LHS:

function
myfun :: "unit ⇒ 'Value ⇒ 'Value"
where
"myfun () x = tick (myfun () x)"

nor with out the locale parameter:

function
myfun :: "unit ⇒ 'Value ⇒ 'Value"
where
"myfun () = (λ x. (myfun () x))"
oops

Unfortunately, this does not help me in my real use-case (I’m using
nominal_primrec, not function, and the "λ x" is indeed a "Λ x" from
HOLCF, so I cannot put the argument on the left).

Is there another way to prevent that problem?

Greetings,
Joachim
signature.asc

Email Gateway (Aug 19 2022 at 12:37):

From: Joachim Breitner <breitner@kit.edu>
Hi,

let me add that, although I originally thought that this was a cause for
my proofs to fail, it turned out that that is not the case. So the
warnings are there, but are not causing any problems.

If there is a way to avoid them I’d still like to know, but it is in no
way critical.

Thanks,
Joachim
signature.asc

Last updated: Apr 23 2024 at 08:19 UTC