[isabelle] polymorphic enough friend

[Thomas Sternagel]

Dear list,

another question on corecursion and friends in Isabelle/HOL development
version 6703434c96d6:
In theory 'Foo' below I am able to show that function "some" which
depends on an inductive set "A" is friendly but when I try to do the
same for function "some'" defined similarly but depending on the
inductive set "C X" instead, I get the error message:

"Eps" not polymorphic enough to be applied like this and no friend

I'm not quite sure why the former works whereas the latter fails.
Maybe someone besides Jasmin is able to answer this one?

theory Foo
imports
"~~/src/HOL/Library/Stream"
"~~/src/HOL/Library/BNF_Corec"
begin

inductive_set A :: "'a stream set" where "s ∈ A"

primcorec some :: "'a ⇒ 'a stream ⇒ 'a stream" where
"some a s = (let t = SOME v. v ∈ A in SCons a (stl t))"

friend_of_corec some :: "'a ⇒ 'a stream ⇒ 'a stream" where
"some a s = (let t = SOME v. v ∈ A in SCons a (stl t))"
by (auto simp add: stream.expand)

inductive_set C :: "'a set ⇒ 'a stream set" for X :: "'a set" where
"shd s ∈ X ⟹ s ∈ C X"

primcorec some' :: "'a set ⇒ 'a ⇒ 'a stream ⇒ 'a stream" where
"some' X a s = (let t = SOME v. v ∈ C X in SCons a (stl t))"

friend_of_corec some' :: "'a set ⇒ 'a ⇒ 'a stream ⇒ 'a stream" where
"some' X a s = (let t = SOME v. v ∈ C X in SCons a (stl t))"

end

Cheers,
Tom