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.


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

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"

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

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



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.