[isabelle] Generalize CPO definition



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.