Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] fun raises THM in context with non-function ty...

Email Gateway (Aug 19 2022 at 14:15):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Isabelle developers,

I just want to report that the function package fails with an exception THM whenever I use
it in a context that fixes a variable of non-function type which is used in the function
definition.

Here's a minimal example:

theory Scratch imports "~~/src/HOL/Main" begin
context fixes y :: "'a" begin
fun foo :: "unit => 'a" where "foo _ = y"
end

*** exception THM 0 raised (line 726 of "thm.ML"):
*** forall_intr: variable "y" free in assumptions
*** [|foo x1 = y; accp foo_rel x1;
*** !!uu_. [|x1 = uu_; y = id y; accp foo_rel uu_|] ==> P|]
*** ==> P
*** [foo == Scratch.foo y, foo_sumC == Scratch.foo_sumC y,
*** foo_graph == Scratch.foo_graph y]
*** At command "fun"

Interestingly, there's no error if I change y's type to "unit => 'a":

context fixes y :: "unit => 'a" begin
fun foo :: "unit => 'a" where "foo _ = y ()"
end

The same error also occurs when I change replace the unnamed context with a locale.

By the way, this is with Isabelle2013-2.

Best,
Andreas

Last updated: Apr 16 2024 at 20:15 UTC