Re: [isabelle] baffled by fun error message
A related question: Who is the maintainer of the function package these
If my suspicion is correct this (slightly) confusing error could be
avoided by using the existing Isabelle/ML machinery for inventing fresh
names at the right point in the function package (wherever this is ;)).
On 09/22/2015 05:00 PM, Andreas Lochbihler wrote:
> 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
> 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