*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Generalize CPO definition*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Wed, 17 Feb 2016 20:29:49 +0100*In-reply-to*: <1867786960.9288110.1455730348487.JavaMail.yahoo@mail.yahoo.com>*Organization*: TU München*References*: <303940385.9201173.1455729383658.JavaMail.yahoo@mail.yahoo.com> <1867786960.9288110.1455730348487.JavaMail.yahoo@mail.yahoo.com>

You can use the usual trick to use the cardinality of a type parameter: typedef 'a T = "f (card (UNIV :: 'a set))" Then you can use the Numeral_Type library to write: 1 T, 2 T, ... - Johannes Am Mittwoch, den 17.02.2016, 17:32 +0000 schrieb Jonathan Woodgate via Cl-isabelle-users: > Hello, > small correction: > f :: nat => nat set where > f 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, cpo_class) " > Thank you very much! Jonathan Woodgate via Cl-isabelle-users < > cl-isabelle-users at lists.cam.ac.uk> schrieb am 18:16 Mittwoch, > 17.Februar 2016: > > > > > 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! > >

**References**:**[isabelle] Generalize CPO definition***From:*Jonathan Woodgate via Cl-isabelle-users

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

- Previous by Date: Re: [isabelle] Generalize CPO definition
- Next by Date: Re: [isabelle] [Isabelle2016-RC4] sledgehammer blocks metis proofs
- Previous by Thread: Re: [isabelle] Generalize CPO definition
- Next by Thread: [isabelle] Announcing Isabelle2016
- 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