*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] class instantiation via class.pred*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Thu, 29 Mar 2012 12:45:06 +0900*In-reply-to*: <4F736559.6060103@informatik.tu-muenchen.de>*References*: <4F701B2E.4060805@jaist.ac.jp> <4F736559.6060103@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120316 Thunderbird/11.0

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

cheers chris

**References**:**[isabelle] class instantiation via class.pred***From:*Christian Sternagel

**Re: [isabelle] class instantiation via class.pred***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] class instantiation via class.pred
- Next by Date: Re: [isabelle] Is Simpl code executable?
- Previous by Thread: Re: [isabelle] class instantiation via class.pred
- Next by Thread: [isabelle] Is Simpl code executable?
- Cl-isabelle-users March 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list