*To*: Jasmin Christian Blanchette <jasmin.blanchette at gmail.com>*Subject*: Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion*From*: Lars Hupel <hupel at in.tum.de>*Date*: Tue, 10 Jun 2014 19:59:51 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <E6631791-5109-4420-A1E8-CDD83D77D17A@in.tum.de>*References*: <754300cfd012d184c95def922fbb4a43-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1UENGV1gNQV53A0tUVFYwQEECXV5YSVhVXQ==-webmailer2@server02.webmailer.hosteurope.de> <E6631791-5109-4420-A1E8-CDD83D77D17A@in.tum.de>*User-agent*: Host Europe Webmailer/2.0

Hi Jasmin,

instantiation rose :: (foo) foo begin primrec count_rose where "count (Fork a as) = count a + count (map count as)" instance .. end

class evaluate =

assumes ... Instantiations typically look like this: instantiation list :: (evaluate) evaluate begin primrec eval_list where "eval_list rs t [] ⟷ rs ⊢ t ⟶* Const ''List.list.Nil''" |

... end

You might want to take a look at the BNF-based size extension. Try thm list.size thm rose.size to see what it has to offer. I suspect that you could base "count" on"size_xxx" (e.g. "size_list"). If not, the idiom used to derive"size"systematically for all BNF-based datatypes might still serve as an inspiration.

The author of this entry is all in favor of porting it to the new package, and it is, from what I understand, only a matter of time until he gets to it. ;)

Cheers Lars

**Follow-Ups**:

**References**:**[isabelle] Modular definition of type class constants for datatypes with nested recursion***From:*Lars Hupel

**Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion***From:*Jasmin Christian Blanchette

- Previous by Date: Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion
- Next by Date: Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion
- Previous by Thread: Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion
- Next by Thread: Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion
- Cl-isabelle-users June 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