# Re: [isabelle] Generalize CPO definition

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.*