Re: [isabelle] Type parameters in a locale? Datatypes in a locale?

Dear Randy,

you might want to try the following locale declaration:

locale label = lattice less_eq less inf sup
  for less_eq :: "'a => 'a => bool" (infix "\<le>" 50)
  and less :: "'a => 'a => bool" (infix "<" 50)
  and inf :: "'a => 'a => 'a"
  and sup :: "'a => 'a => 'a"
  fixes noperator :: "'a => 'b"

lemma "x \<le> a \<Longrightarrow> x \<le> (sup a b)"

Mentioning all parameters of lattice in the for clause ensures that label keeps the same order of parameters as lattice does.

Note that 'a no longer carries the sort constraint lattice. This is intentional as the type variables in the context of a type class never carry the sort constraint of the lattice, because the assumptions of the type class are part of the locale assumption. Conversely, from within the type class context, you can only use lemmas that are proved in the type class context, but not with the type constraints.

This also solves the issue with abiguous input: Since 'a is not of sort ord (which defines the syntax for less_eq and less), the syntax for type classes is not applicable.

Hope this helps,

Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
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.