# [isabelle] class instantiation via class.pred

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] class instantiation via class.pred
*From*: Christian Sternagel <c-sterna at jaist.ac.jp>
*Date*: Mon, 26 Mar 2012 16:30:54 +0900
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120316 Thunderbird/11.0

Hi all,

`I defined a typeclass "wqo" (on top of Isabelle/HOL's preorder) for
``well-quasi-orders (but the specific application is not really important
``for my question). Additionally I have a predicate "wqo_on P A" (for
``predicates P that form a well-quasi-order on elements of the set A)
``which is defined independently. Furthermore I have the connecting lemma
`
wqo_on P UNIV <-> class.wqo P (%x y. P x y & ~ P y x) (1)
For wqo_on, I proved:
wqo_on P1 A1 ==> wqo_on P2 A2 ==>
wqo_on (%(p1,p2) (q1,q2). P1 p1 q1 & P2 p2 q2) (A1 <*> A2) (2)
Now I want to use (2) where A1 and A2 is instantiated to UNIV
in combination with (1) in order to proof
instantiation prod :: (wqo, wqo) wqo

`But I fail to obtain appropriate facts for discharging the assumptions
``of the instantiated (2) (which should be possible since the components
``are assumed to be wqo and hence by (1) it should be possible to obtain
``the necessary assumptions). How is it possible to refer inside a
``recursive instance proof to the class predicates (sorry I don't know
``whether this is the correct terminology, I mean class.wqo here) of
``subparts? Moreover, how is it possible to obtain a class instance by
``proving that the class predicate holds? (By intro_classes I only obtain
``OFCLASS(...) and fail to see the connection to class.wqo.)
`
cheers
chris

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