Re: [isabelle] class instantiation via class.pred

On 03/29/2012 04:24 AM, Florian Haftmann wrote:
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,

Thanks that worked! Just for the record: Type classes have a "_class" suffix, i.e., it is wqo_class.intro and wqo_class.axioms.



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