Email Gateway (Aug 18 2022 at 17:50): Email Gateway (Aug 18 2022 at 17:50):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Consider the following in HOL
locale label = bounded_lattice +
fixes lblRem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
and canElim :: "'b \<Rightarrow> 'a \<Rightarrow> bool"
begin
First question: which type variable of the locale "label" ('a or 'b,
or neither) is understood to be the single type variable of
"bounded_lattice"? I want 'a to be the lattice. How can I say that?
In the locale context I want to define a datatype
datatype ('a,'b) expr = ...
where 'a and 'b are the type variables of the locale, and 'a is the
lattice. It seems that datatype definitions are not accepted in a
locale context, so I defined ('a,'b) expr before the locale and tried
to instantiate it with 'a and 'b inside the locale.
type_synonym exp = "('a,'b) expr"
This fails: '*** Extra variables on rhs: "'b", "'a"'. In my mind, the
type variables 'a and 'b are somehow fixed in the locale context, so
are not extra variables on rhs. That is, in any (concrete?) instance
of the locale 'a and 'b will be fixed, so I should be able to give
them symbolic names and use them as if they were declared (say with
typedecl) inside the locale context.
I try something else:
type_synonym ('a,'b) exp = "('a,'b) expr"
This fails too: '*** Locally fixed type arguments "'a", "'b" in type
declaration "exp"' So Isabelle also thinks 'a and 'b are fixed in the
locale context.
Now I'm stuck. Can I do what I'm trying to do.? If not, is there a
logical reason why not?
Thanks,
Randy
Email Gateway (Aug 18 2022 at 17:50):From: Makarius <makarius@sketis.net>
On Fri, 24 Jun 2011, Randy Pollack wrote:
In the locale context I want to define a datatype
datatype ('a,'b) expr = ...
where 'a and 'b are the type variables of the locale, and 'a is the
lattice. It seems that datatype definitions are not accepted in a
locale context, so I defined ('a,'b) expr before the locale and tried
to instantiate it with 'a and 'b inside the locale.type_synonym exp = "('a,'b) expr"
This fails: '*** Extra variables on rhs: "'b", "'a"'. In my mind, the
type variables 'a and 'b are somehow fixed in the locale context, so
are not extra variables on rhs.
I try something else:
type_synonym ('a,'b) exp = "('a,'b) expr"
This fails too: '*** Locally fixed type arguments "'a", "'b" in type
declaration "exp"' So Isabelle also thinks 'a and 'b are fixed in the
locale context.
Conceptually, the "locality" of type specifications is limited: it may not
depend on the context parameters. Its own parameters are considered fresh
abstractions, so an accidental clash with outer ones is an error.
type_synonym, typedecl, typedef already work in that sense, but datatype
is still not "localized". (It is on the agenda with high priority for
quite a few years already, although it is become some kind of running
gag in the meantime).
That is, in any (concrete?) instance of the locale 'a and 'b will be
fixed, so I should be able to give them symbolic names and use them as
if they were declared (say with typedecl) inside the locale context.
Local type parameters are fixed, outside the context they become
arbitrary, and may thus get instantiated.
Now I'm stuck. Can I do what I'm trying to do.? If not, is there a
logical reason why not?
You can define the datatype globally and use it locally. This means its
parameters will be always mentioned (again) in the local situation.
Makarius
Email Gateway (Aug 18 2022 at 17:50):From: Clemens Ballarin <ballarin@in.tum.de>
Quoting Randy Pollack <rpollack@inf.ed.ac.uk>:
Consider the following in HOL
locale label = bounded_lattice +
fixes lblRem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
and canElim :: "'b \<Rightarrow> 'a \<Rightarrow> bool"
beginFirst question: which type variable of the locale "label" ('a or 'b,
or neither) is understood to be the single type variable of
"bounded_lattice"?
This is not specified. Use print_locale to find out what happened
(you may need to set show_types).
I want 'a to be the lattice. How can I say that?
You need to mention the type variable in the imported expression.
This can be done like this:
locale label = bounded_lattice x for x :: "... 'a ..." + ...
In the locale context I want to define a datatype
datatype ('a,'b) expr = ...
where 'a and 'b are the type variables of the locale, and 'a is the
lattice. It seems that datatype definitions are not accepted in a
locale context, so I defined ('a,'b) expr before the locale and tried
to instantiate it with 'a and 'b inside the locale.[...]
Now I'm stuck. Can I do what I'm trying to do.? If not, is there a
logical reason why not?
As Makarius already said, use ('a, 'b) expr in your locale.
Clemens
Email Gateway (Aug 18 2022 at 17:50):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Thanks Clemens and Makarius, but now I have a new problem with notation.
Consider this
context lattice begin
thm le_supI1 a theorem from the typeclass lattice )
This prints out
?x \<le> ?a \<Longrightarrow> ?x \<le> sup ?a ?b
So the typeclass "lattice" from Main supplies notation for less_eq,
(and less) but not for sup (or inf). I don't understand why, but I
know how to fix it: put
notation sup (infixl "\<squnion>" 70)
in the context.
Now consider my locale
locale label = lattice less_eq ( as Clemens suggested )
for less_eq::"'a::lattice \<Rightarrow> 'a \<Rightarrow> bool" +
fixes oprn :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
begin
thm le_supI1
This prints out
less_eq ?x ?a \<Longrightarrow> less_eq ?x (sup ?a ?b)
So my "for" clause for less_eq has removed (or shadowed?) the notation
\<le> from the typeclass lattice.
I tried
locale label2 = lattice less_eq less inf sup
for less_eq::"'a::bounded_lattice \<Rightarrow> 'a \<Rightarrow> bool" +
fixes oprn :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
begin
notation
less_eq (infix "\<le>" 50) and
less (infix "<" 50) and
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 70)
thm le_supI1
This prints out
?x \<le> ?a \<Longrightarrow> ?x \<le> ?a \<squnion> ?b
So it looks good. But I try
lemma "x \<le> a \<Longrightarrow> x \<le> a \<squnion> b"
This gives
*** Ambiguous input, 4 terms are type correct:
*** ((x \<le> a) \<Longrightarrow> (x \<le> (a \<squnion> b)))
*** ((x \<le> a) \<Longrightarrow> (x \<le> (a \<squnion> b)))
*** ((x \<le> a) \<Longrightarrow> (x \<le> (a \<squnion> b)))
*** ((x \<le> a) \<Longrightarrow> (x \<le> (a \<squnion> b)))
I guess some mixup between \<squnion> of lattice and \<squnion> of label1
What is the problem? How can I fix it?
Thanks for any help,
Randy
Email Gateway (Aug 18 2022 at 17:50):From: Clemens Ballarin <ballarin@in.tum.de>
There's two issues here:
locale label = lattice less_eq ( as Clemens suggested )
for less_eq::"'a::lattice \<Rightarrow> 'a \<Rightarrow> bool" +
removes the syntax from the parameter. It can either be declared with
a syntax annotation in the for clause or via the notation command.
So, what you did I would have expected to work.
What happens in you case is that syntax from an imported class does
not arrive at the locale.
class my_class =
fixes operation :: "'a => 'a => 'a" (infixl "++" 60)
begin
term operation (* prints op ++ *)
end
locale my_locale = my_class
begin
term operation (* prints operation, concrete syntax lost *)
end
(If you make my_class a locale, the syntax arrives in the second
locale.) I suspect this is either explained by the class package or
perhaps local theories (Florian, Makarius?). Class syntax is declared
both at the theory level and in the class context. This likely causes
the syntax conflict you observe.
Clemens
Quoting Randy Pollack <rpollack@inf.ed.ac.uk>:
Email Gateway (Aug 18 2022 at 17:51):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
Class syntax is declared
both at the theory level and in the class context.
Not exactly. Class syntax is only declared at the theory level, but
inside the class context occurences of the global class operations on
the type parameter 'a of the class are improved to their local
counterparts. This allows to use syntax uniformly (c.f. class tutorial,
§3.6).
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 17:51):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Thanks, but I'm still stumped. Let's go through a simplified example.
I'm using
Isabelle2011.
theory testing imports Main begin ( nothing up my sleeve )
thm le_supI1 (* some theorem from semilattice_sup *)
Prints out
(?x\<Colon>?'a\<Colon>semilattice_sup) \<le>
(?a\<Colon>?'a\<Colon>semilattice_sup) \<Longrightarrow>
?x \<le> sup ?a (?b\<Colon>?'a\<Colon>semilattice_sup)
Why? The notation
\<le> (from class order) is preserved, but the notation "\<squnion>"
for sup (from
class semilattice_sup is gone.
I want to create a new locale, extending lattice with a new operator. The new
operator may mention several type variables, one specific one of which
should be the
same as the lattice type. This was my original question.
I first tried this:
locale label = lattice +
fixes noperator :: "'a::lattice \<Rightarrow> 'b"
begin
This doesn't seem to work:
locale label =
fixes less_eq :: "'c\<Colon>type \<Rightarrow> 'c\<Colon>type
\<Rightarrow> bool"
and less :: "'c\<Colon>type \<Rightarrow> 'c\<Colon>type
\<Rightarrow> bool"
and inf :: "'c\<Colon>type \<Rightarrow> 'c\<Colon>type
\<Rightarrow> 'c\<Colon>type"
and sup :: "'c\<Colon>type \<Rightarrow> 'c\<Colon>type
\<Rightarrow> 'c\<Colon>type"
and nopr :: "'b\<Colon>type \<Rightarrow> 'a\<Colon>lattice"
"noperator" is not constrained to have type 'c, which seems to be the
lattice type here.
And why does 'c have sort "type" instead of sort "lattice"?
So following Clemens' suggestion, I write:
locale label = lattice less_eq
for less_eq::"'a::lattice \<Rightarrow> 'a \<Rightarrow> bool"
(infix "\<le>" 50) +
fixes noperator :: "'a \<Rightarrow> 'b"
begin
locale label =
fixes less :: "'a\<Colon>lattice \<Rightarrow> 'a\<Colon>lattice
\<Rightarrow> bool"
and inf :: "'a\<Colon>lattice \<Rightarrow> 'a\<Colon>lattice
\<Rightarrow> 'a\<Colon>lattice"
and sup :: "'a\<Colon>lattice \<Rightarrow> 'a\<Colon>lattice
\<Rightarrow> 'a\<Colon>lattice"
and less_eq :: "'a\<Colon>lattice \<Rightarrow> 'a\<Colon>lattice
\<Rightarrow> bool"
and noperator :: "'a\<Colon>lattice \<Rightarrow> 'b\<Colon>type"
That looks better, and printing "le_supI1" as above gives:
(?x\<Colon>'a\<Colon>lattice) \<le> (?a\<Colon>'a\<Colon>lattice)
\<Longrightarrow>
?x \<le> (sup\<Colon>'a\<Colon>lattice \<Rightarrow> 'a\<Colon>lattice
\<Rightarrow> 'a\<Colon>lattice) ?a (?b\<Colon>'a\<Colon>lattice)
But when I try to state this myself:
lemma "x \<le> a \<Longrightarrow> x \<le> (sup a b)"
*** Ambiguous input, 4 terms are type correct:
*** ((x \<le> a) \<Longrightarrow> (x \<le> (sup a b)))
*** ((x \<le> a) \<Longrightarrow> (x \<le> (sup a b)))
*** ((x \<le> a) \<Longrightarrow> (x \<le> (sup a b)))
*** ((x \<le> a) \<Longrightarrow> (x \<le> (sup a b)))
What do you suggest?
Thanks,
Randy
Email Gateway (Aug 18 2022 at 17:51):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
I guess the source for the misunderstanding is that the lattice syntax
for sup etc. is deleted in theory Lattices; to obtain it again, import
theory Lattice_Syntax.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 17:51):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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"
begin
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,
Andreas
Last updated: Apr 25 2024 at 20:15 UTC