*To*: Randy Pollack <rpollack at inf.ed.ac.uk>*Subject*: Re: [isabelle] locales?*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Wed, 06 Jun 2012 09:03:09 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CANofLeL3o+gLVY8Y3fMfm9xewGXepJehqF4msh2fx5hyh8bbeQ@mail.gmail.com>*References*: <CANofLeL3o+gLVY8Y3fMfm9xewGXepJehqF4msh2fx5hyh8bbeQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.27) Gecko/20120216 Thunderbird/3.1.19

Hi Randy,

I want to use the locale "preorder" from HOL Main.

thm preorder_def (*** Unknown fact "preorder_def" (line 3 of ...

thm class.preorder_def is what you want.

Next, I define a locale: locale funny = p1: preorder where less_eq = p1le and less = p1lt for p1le::"'a => 'a => bool" and p1lt::"'a => 'a => bool" + fixes p2le:: "nat => 'a => 'a" and p2lt:: "nat => 'a => 'a" assumes p2leAx: "\forall n. preorder p2le p2lt"

The declaration has 3 flaws:

3. The type for p2le and p2lt are wrong, they should be "nat => 'a => 'a => bool" Here's the declaration you want: locale funny = p1: preorder where less_eq = p1le and less = p1lt for p1le::"'a => 'a => bool" and p1lt::"'a => 'a => bool" + fixes p2le:: "nat => 'a => 'a => bool" and p2lt:: "nat => 'a => 'a => bool" assumes p2leAx: "class.preorder (p2le n) (p2lt n)"

> Is there a better way to construct this structure? No, this is the canonical way, see also this thread: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2010-March/msg00005.html

Finally, the context "preorder" contains some definitions and lemmas outside the original locale definition of "preorder". (E.g. in the context preorder I define the symmetric closure of less_eq, and prove that is an equivalence.) Can I access those definitions and lemmas for the preorder "p2le" in my example?

You first have to make funny a sublocale of preorder as follows: sublocale funny < p2!: preorder "p2le n" "p2lt n" for n by(rule p2leAx) The "p2!" determines the prefix to be used. For example: context funny begin thm p2.less_asym Andreas -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Am Fasanengarten 5, Geb. 50.34, Raum 025 76131 Karlsruhe Telefon: +49 721 608-47399 Fax: +49 721 608-48457 E-Mail: andreas.lochbihler at kit.edu http://pp.info.uni-karlsruhe.de

**References**:**[isabelle] locales?***From:*Randy Pollack

- Previous by Date: [isabelle] locales?
- Next by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Previous by Thread: [isabelle] locales?
- Next by Thread: [isabelle] Assumptions of auxiliary context in other contexts
- Cl-isabelle-users June 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