# Re: [isabelle] Generalize CPO definition

```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!
>
>

```

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