Re: [isabelle] baffled by fun error message
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:
When I try the following minimal example in Isabelle2015
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and