Re: [isabelle] Linear Ordering for nat list



On 02/05/2012, at 9:48 AM, Aaron W. Hsu wrote:

> On Wed, 02 May 2012 00:03:07 +0100, John Wickerson wrote:
> 
>> I reckon this is a job for isabelle's "type classes". You should make an
>> instantiation of the "linorder" class (defined in
>> http://isabelle.in.tum.de/library/HOL/Orderings.html) for nat lists.
> 
> Thank you!  I have not used type classes before, but after reading about 
> them, I think I can make it work. 

Before you do, have a poke around the Isabelle sources. There are a few theories about list orders already in there (e.g. "Length Lexicographic Ordering" in src/HOL/List.thy and probably a prefix order somewhere).

cheers
peter

-- 
http://peteg.org/






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.