Re: [isabelle] locales?



Hi Randy,

I want to use the locale "preorder" from HOL Main.
preorder is primarily a type class. Every type class has an associated locale, for which the naming conventions differ a bit: Some names need to be prefixed with "class.".

    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:

1. As preorder is a type class, the corresponding predicate from the locale assumptions is "class.preorder", not preorder. In the above form, preorder in p2leAx is a free variable that is quantified over. Although the locale itself is called preorder without prefix!

2. When you replace "preorder" with "class.preorder" in p2leAx, Isabelle now generates a type error, which guides you to the second issue: The quantifier over n is vacuous because n does not appear inside the quantifier. Hence, type inference computes a type 'b for n, which does not occur among the parameters. Hence, the warning about additional type variables.

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

Note that you can drop the quantifier on n, because locale declarations implicitly quantify universally over all free variables in the assumptions.

> 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
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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