*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Generalize CPO definition*From*: Jonathan Woodgate via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Date*: Wed, 17 Feb 2016 17:16:23 +0000 (UTC)*References*: <303940385.9201173.1455729383658.JavaMail.yahoo.ref@mail.yahoo.com>*Reply-to*: Jonathan Woodgate <jonathan_woodgate_90210 at yahoo.com>

Hello, I have a simple question: Let f :: N => Nf k = {n:N. predicate(k) } typedef T1 = "f 1" typedef T2 = "f 2" ... instance T1::cpo Â //assume the predicate is such that they are indeed cpo'sinstance T2::cpo ... So for 100 type definitions i have to prove the instantiation 100 times by hand. My question is, how can I automatize this, by defining a lemma as follows: lemma " âT. OFCLASS(f T, pcpo_class) " PS: I know that this is syntactically wrong, since f T is a set and it should instead be a type. Thank You!

**Follow-Ups**:**Re: [isabelle] Generalize CPO definition***From:*Jonathan Woodgate via Cl-isabelle-users

- Previous by Date: [isabelle] folding and linking in jEdit; curry/split
- Next by Date: Re: [isabelle] Generalize CPO definition
- Previous by Thread: Re: [isabelle] folding and linking in jEdit; curry/split
- Next by Thread: Re: [isabelle] Generalize CPO definition
- Cl-isabelle-users February 2016 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