Email Gateway (Aug 18 2022 at 18:45): Email Gateway (Aug 18 2022 at 18:45):From: Randy Pollack <rpollack@inf.ed.ac.uk>
I want to have a locale combining two different lattices, and using
the infix syntax. This goes back to help I got from this list several
months ago. Here is a script that worked in Isabelle2011 (and I've
developed significant work in this locale) and fails in
Isabelle2011-1:
theory localeTypeUnif imports Main begin
locale labelAuth =
label: lattice lblle lbllt lblinf lblsup
+
auth: lattice authle authlt authinf authsup
for lblle::"'a \<Rightarrow> 'a \<Rightarrow> bool" (infix
"\<sqsubseteq>" 50)
and lbllt::"'a \<Rightarrow> 'a \<Rightarrow> bool" (infix
"\<sqsubset>" 50)
and lblinf::"'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl
"\<sqinter>" 70)
and lblsup::"'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl
"\<squnion>" 65)
and authle:: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix
"\<sqsubseteq>" 50)
and authlt:: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix
"\<sqsubset>" 50)
and authinf::"'b \<Rightarrow> 'b \<Rightarrow> 'b" (infixl
"\<sqinter>" 70)
and authsup::"'b \<Rightarrow> 'b \<Rightarrow> 'b" (infixl
"\<squnion>" 65)
*** Type unification failed
*** Failed to meet type constraint:
*** Term: op \<sqsubseteq> :: 'a \<Rightarrow> 'a \<Rightarrow> bool
*** Type: 'a \<Rightarrow> 'a \<Rightarrow> 'a
*** At command "locale" (line 3 of
"/home/rpollack/work/seas/crash/ubreeze/isabelle/experiments/localeTypeUnif.thy")
What is the problem? Thanks for any help.
Randy
Email Gateway (Aug 18 2022 at 18:45):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Randy,
I dimly remember that there have been changes in the type class import
hierarchy which changed the order of arguments for locale predicates,
but I can't recall exactly which. Maybe somebody else can comment?
Cheers,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 18:45):From: Alexander Krauss <krauss@in.tum.de>
Hi Randy,
The change was 5e51075cbd97, and here is the NEWS entry:
Your definition works again, when lblinf/authinf are moved to the front.
The dependence of the predicate arguments on the specifics of the
hierarchy is a bit unfortunate...
Alex
Email Gateway (Aug 18 2022 at 18:45):From: Clemens Ballarin <ballarin@in.tum.de>
If this resolves the problem, then not only the order of the arguments
of the locale predicate but also the order of the locale parameters
has changed. The latter is, of course, not internal if a class is
used as a locale.
Randy can make the locale expression invariant to such changes by
using named instantiation syntax like this:
labelAuth =
label: lattice
where le = lblle and lt = lbllt and inf = lblinf and sup = lblsup +
auth: lattice
...
Clemens
Quoting Alexander Krauss <krauss@in.tum.de>:
Email Gateway (Aug 18 2022 at 18:45):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Hi Clemens,
I like your suggestion. However I guess I didn't understand it.
locale labelAuth =
label: lattice where
le = lblle and lt = lbllt and inf = lblinf and sup = lblsup
+
auth: lattice where
le = authle and lt = authlt and inf = authinf and sup = authsup
returns error message
*** "le" not a parameter of instantiated expression
*** At command "locale" (line 3 of
"/home/rpollack/work/seas/crash/ubreeze/isabelle/experiments/localeTypeUnif.thy")
I tried a few other syntaxes without success, e.g.
locale labelAuth =
label: lattice where label.le = lblle
*** Outer syntax error (line 4 of
"/home/rpollack/work/seas/crash/ubreeze/isabelle/experiments/localeTypeUnif.thy"):
command expected,
*** but keyword where (line 4 of
"/home/rpollack/work/seas/crash/ubreeze/isabelle/experiments/localeTypeUnif.thy")
was found
I'm completely floundering. I found no explanation I could understand
in the Tutorial on Locales.
Best,
Randy
Email Gateway (Aug 18 2022 at 18:45):From: Clemens Ballarin <ballarin@in.tum.de>
Oops. Sorry, I did not look up the parameter names of lattice when I
wrote this. They are less_eq, less, inf and sup.
locale labelAuth =
label: lattice where
less_eq = lblle and less = lbllt and inf = lblinf and sup = lblsup
for lblle and lbllt and lblinf and lblsup
will work. An instantiation 'name = term' means that the parameter
'name' of lattice is instantiated with 'term', which is an expression
over the parameters of the declared locale. You still need the for
clause, and in your case of importing two instances you will need the
parameter type declarations as well in order share the type parameters.
The Isabelle/Isar reference manual documents named instantiation, but
there are indeed no examples.
Sorry again for the confusion.
Clemens
Randy Pollack <rpollack@inf.ed.ac.uk>:
Last updated: Nov 21 2024 at 12:39 UTC