Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Type variables, locale import and notation

Email Gateway (Aug 22 2022 at 13:12):

From: Ferdinand Vesely <csfvesely@swansea.ac.uk>
Dear List,

I have a problem with using (infix) notation inside a locale in
combination with type variables. In summary, I'm trying to introduce a
binary abbreviation of a ternary predicate, where the type of the
omitted parameter is a type variable (restricted by a sort). On the
top-level, such a binary abbreviation is generalised to three
parameters again by introducing a "type parameter" (e.g., "'a itself").
I've figured out that by using locales I can fix the (abstract) type
locally and use the binary predicate inside the locale as I've
intended. However, this does not play well when I also want to use
infix notation for the abbreviation in a specialised locale (= import
with instantiated parameter). Here is a contrived example of my
problem. First the basic definitions:

class a = fixes pred :: "'a ⇒ bool"

locale s =
fixes foo :: "'a ⇒ ('b :: a) ⇒ 'a ⇒ bool"
begin
definition bar :: "'a ⇒ 'a ⇒ bool" (infix "→" 50) where
"x → y = (∃(l :: 'b). foo x l y ∧ pred l)"
end

class b = a +
assumes b_pred: "∃l. pred l"

definition ex :: "nat ⇒ ('b :: b) ⇒ nat ⇒ bool" where
"ex x l y = (y = x + 1 ∧ pred l)"

Now if I create a new locale where I only import locale s above, the
types are as expected:

locale s1 = s
begin
term bar (* "op →" :: "'a ⇒ 'a ⇒ bool" *)
term "op →" (* "op →" :: "'a ⇒ 'a ⇒ bool" *)
end

But if I want to specialise the locale with the above definition of 'ex,
the type parameter is re-introduced even inside the locale and the infix
notation does not work anymore (Isabelle does not warn about this). I'm
not sure why the parameter is introduced inside the locale. Why is this
the case? Shouldn't the types of the corresponding parameters of 'foo'
and 'ex' be unified?

locale s2 = s where foo = ex
begin
term bar (* "λtype. spec.bar ex" :: "'a itself ⇒ nat ⇒ nat ⇒ bool", where "'a :: b" *)
term "op →" (* Inner lexical error. Failed to parse term *)
end

Anyway, I've found out that if I add a new locale parameter with the
same sort constraint on the type as in the type of 'ex', the additional
"itself parameter" is not introduced. However, the infix notation still
does not work.

locale s3 = s where foo = "ex :: nat ⇒ ('b :: b) ⇒ nat ⇒ bool" +
fixes t :: "('b :: b) itself"
begin
term bar (* "s.bar ex" :: "nat ⇒ nat ⇒ bool" *)
term "op →" (* Inner lexical error. Failed to parse term *)

lemma "1 → 2" (* Inner lexical error. Failed to parse term *)

lemma "bar 1 2" (* OK *)
by (simp add: bar_def ex_def b_pred)

lemma "¬bar 2 1" (* OK *)
by (simp add: bar_def ex_def)
end

Why is the infix notation for bar silently dropped in locale s3? Is
there any way around this, i.e., using the infix notation introduced
in locale s?

My other question is if there is a better way to introduce such an
abbreviation without implicitly adding the extra "type parameter" and
to keep the infix notation.

Kind regards,
Ferdinand

Email Gateway (Aug 22 2022 at 13:12):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Ferdinand,

Any notation is dropped when you instantiate the parameters of a locale beyond renaming.
The reason is that in general the number of arguments changes, so the notation does not
make much sense any more. You can always reintroduce the notations using the command
notation as follows:

context s3 begin
notation bar (infix "→" 50)

The reason for the type token 'b itself for bar is as follows: In HOL, all type variables
in the definition of a constant must appear in the type of the constant. Otherwise,
inconsistencies could be introduced. In Isabelle, abbreviations must also obey this rule.
Now, the locale constant bar gets translated to a foundational constant s.bar with the
locale parameters as additional ones. This can be seen when pretty-printing bar in s3: you
get "s.bar ex". Now, s.bar ex contains the type variable 'b, which does not show up in the
fixed parameters of the locale (in fact s2 does not fix any parameters at all). Therefore,
Isabelle introduces the type token for s2.bar.

Best,
Andreas

Last updated: Apr 19 2024 at 01:05 UTC