[isabelle] pairs and friends

[Thomas Sternagel]

Dear mailing list,

In Isabelle/HOL development version 6703434c96d6 I have the following
problem: I want to have a friendly function 'foo' (which I reduced so
much, that it does not do anything useful anymore for sake of a minimal
example). If I use the type "a list ⇒ 'a stream ⇒ 'a stream" everything
works out as expected, but if I switch to streams of pairs, like shown
below I get the following error message:

Cannot have type variable "'a" in the argument types when it does not
occur in the result type

Now "'a" clearly appears in the result type, so I don't see what is
going wrong.

theory Foo
imports
"~~/src/HOL/Library/Stream"
"~~/src/HOL/Library/BNF_Corec"
begin
primcorec foo :: "'a list ⇒
('a × 'a) stream ⇒ ('a × 'a) stream" where
"foo us T = (case us of
[] ⇒ SCons (shd T) (stl T)
| u # us ⇒ SCons (shd T) (stl T))"

friend_of_corec foo :: "'a list ⇒
('a × 'a) stream ⇒ ('a × 'a) stream" where
"foo us T = (case us of
[] ⇒ SCons (shd T) (stl T)
| u # us ⇒ SCons (shd T) (stl T))"

end

Cheers,
Tom

[Jasmin Blanchette]

Dear Thomas,

> In Isabelle/HOL development version 6703434c96d6 I have the following
> problem: I want to have a friendly function 'foo' (which I reduced so
> much, that it does not do anything useful anymore for sake of a minimal
> example). If I use the type "a list ⇒ 'a stream ⇒ 'a stream" everything
> works out as expected, but if I switch to streams of pairs, like shown
> below I get the following error message:
>
> Cannot have type variable "'a" in the argument types when it does not
> occur in the result type

I'm on vacation for two weeks starting today and won't be able to look into this until then. I hope we can support your function. In any case, the error message is wrong. Hopefully, you can either wait until then or find a workaround.

Cheers,

Jasmin

[Thomas Sternagel]

I see. Have a nice vacation. I will try to figure something out.
Thanks,
Tom

[Dmitriy Traytel]

Hi Tom,

an admittedly ugly temporary workaround is to use a separate codatatype for streams of pairs:

codatatype 'a pairstream = SCons (shd: "'a × 'a") (stl: "'a pairstream”)

corecursive (friend) foo :: "'a list ⇒ 'a pairstream ⇒ 'a pairstream" where

"foo us T = (case us of
[] ⇒ SCons (shd T) (stl T)
| u # us ⇒ SCons (shd T) (stl T))"

unfolding relator_eq[symmetric] by transfer_prover

Cheers,
Dmitriy

[Thomas Sternagel]

Thanks for the tip, Dmitriy. I will try it.

Cheers,
Tom