*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Is it bad to instantiate "list" with custom classes to be used with "bool list"?*From*: Gottfried Barrow <igbi at gmx.com>*Date*: Mon, 08 Sep 2014 07:43:11 -0500*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <540D4DCB.2000509@inf.ethz.ch>*References*: <540D4613.6080603@gmx.com> <540D4DCB.2000509@inf.ethz.ch>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 14-09-08 01:33, Andreas Lochbihler wrote:

This will not work the way you expect. To make the list type aninstance of binc, you have to do this for lists of arbitrary elementsof the assumed sort ("{complete_boolean_algebra, linorder}" in thisexample), not for a specific type bool. As it is now, you define afunction binc_list which is completely unrelated to binc. You willrealise this at the latest when you introcude some assumptions aboutbinc and are unable to prove them for your attempted instantiation.Note that if you replace False by bot and True by top, then yourdefinition should generalise to 'a :: {complete_boolean_algebra,linorder}.

Andreas,

instantiation list :: ("{bot,top}") binc begin primrec binc_list :: "'a list ⇒ 'a list" where "binc_list [] = bot # []" |"binc_list (b # bl) = (if b = bot then top # bl else bot # (binc_list bl))" instance .. end

Is instantiating "list" like this a bad thing in general?If you define your own type classes and instantiate them for list,that is all right. However, you should be very careful when youinstantiate list for type classes of HOL/Main or other people, becausethis may restrict the interoperability with the formalisations ofothers, as type classes may only be instantiated once for each type inone session.

Thanks, GB

**References**:**[isabelle] Is it bad to instantiate "list" with custom classes to be used with "bool list"?***From:*Gottfried Barrow

**Re: [isabelle] Is it bad to instantiate "list" with custom classes to be used with "bool list"?***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Quickcheck in locale with defines directive
- Next by Date: Re: [isabelle] Gcd and algebraic structures
- Previous by Thread: Re: [isabelle] Is it bad to instantiate "list" with custom classes to be used with "bool list"?
- Next by Thread: [isabelle] Counting the proof time
- Cl-isabelle-users September 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list