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.