[isabelle] baffled by fun error message



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.