Re: [isabelle] baffled by fun error message



Dear Thomas,

I have run into this problem before. The issue is that the function package does not seem to properly respect the fixed variables in unnamed contexts. If you change the variable name in the context from R to something else, then the function definition should work. Internally, fun uses the name "R" for the termination relation in the termination proof.

Best,
Andreas

On 22/09/15 14:47, Thomas Sternagel wrote:
Hello mailing-list!

When I try the following minimal example in Isabelle2015



theory Test
imports Main
begin

datatype (funs : 'f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"

type_synonym ('f, 'v) trs = "(('f, 'v) term à ('f, 'v) term) set"

context
   fixes F and R :: "('f, 'v) trs"
   assumes "R â F"
begin

fun star :: "('f, 'v) term â ('f, 'v) term"
where
   "star (Fun f ts) = Fun f (map star ts)"

end

end



I get the error message:

exception THM 0 raised (line 744 of "thm.ML"):
   forall_intr: variable "R" free in assumptions
   wf R â
   (âf ts x. x â set ts â (x, Fun f ts) â R) â
   âx. Wellfounded.accp star_rel x
     [star_rel â ??.Test.star_rel]

Which leaves me quite puzzled. I do neither understand the error
message nor why there is an error at all. Can somebody explain what
happens here, please?

Cheers, Thomas





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.