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.