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
	wqo.axioms
	wqo.intro

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
beginning.

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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