Re: [isabelle] class instantiation via class.pred

Hi Christian,

> 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

I think the reason for your confusion is that there are not two, but
three layers:

a) your user-space predicate wqo_on
b) the module system predicate class.wqo (where »class« refers to the a
locale combined with a type class rather than a mere type class)
c) the proper type class wqo

You can jumb between b) and c) by means of theorems

So in your case, this would roughly meen something like:

a) From sort hypothesis, obtain class.wqo ['a] … and class.wqo ['b] … by
means of wqo.axioms
b) Obtain wqo_on ['a] … and wqo_on ['b] … by means of (1)
c) Obtain wqo_on ['a * 'b] … by means of (2)
d) Obtain class.wqo ['a * 'b] … by means of (1)
e) Conclude using wqo.intro – which could also be an intro step in the

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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