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

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

cheers

chris





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