Email Gateway (Aug 18 2022 at 19:21): Email Gateway (Aug 18 2022 at 19:21):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Hi all,
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
But I fail to obtain appropriate facts for discharging the assumptions
of the instantiated (2) (which should be possible since the components
are assumed to be wqo and hence by (1) it should be possible to obtain
the necessary assumptions). How is it possible to refer inside a
recursive instance proof to the class predicates (sorry I don't know
whether this is the correct terminology, I mean class.wqo here) of
subparts? Moreover, how is it possible to obtain a class instance by
proving that the class predicate holds? (By intro_classes I only obtain
OFCLASS(...) and fail to see the connection to class.wqo.)
cheers
chris
Email Gateway (Aug 18 2022 at 19:23):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,
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
signature.asc
Email Gateway (Aug 18 2022 at 19:23):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
Last updated: Apr 26 2024 at 04:17 UTC