Re: [isabelle] baffled by fun error message



A related question: Who is the maintainer of the function package these
days?

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 ;)).

cheers

chris

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
> 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.