[isabelle] class instantiation via class.pred



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.