Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] sublocales?

view this post on Zulip Email Gateway (Aug 18 2022 at 13:53):

From: Randy Pollack <rpollack@inf.ed.ac.uk>
Where can I find documentation about sublocales? The Isabelle/Isar
Reference Manual (2009) apparently does not contain the string
"sublocale". The Tutorial to Locales and Locale Interpretation (2009)
does not include the syntax that Andreas suggested to me:

sublocale HEv0 < F0HE : HE "%X. if ... then v0 else F X"
unfolding F0_def[symmetric]

Thanks,
Randy
--
Andreas Lochbihler writes:

Hi Randy,

Is there a locale expression (?) that when interpreted with with FF
and vv, gives the context of HE interpreted with
(%X. if ... then vv else FF X)? (Maybe using a "where" clause?)
If I understand you correctly, you want to have an interpretation of HE
for F0 (with the F0's definition unfolded) whenever you interpret HEv0.
You can do this by making HEv0 a sublocale of HE with F instantiated to F0:

sublocale HEv0 < F0HE : HE "%X. if ... then v0 else F X"
unfolding F0_def[symmetric]
by(unfold_locales)(rule HEF0)

where HEF0 refers to your lemma that shows "fixF.HE F0".

Now, whenever you interpret HEv0, this also interprets HE with F0
unfolded. The constants and lemmas generated by this process are
prefixed by F0HE to distinguish them from those that obtained directly
from HE. Also, already inside the HEv0 locale, you can access the HE
context for F0.

Is that what you wanted?

Regards,
Andreas

Randy Pollack schrieb:

I'm reasoning about a properties of a fixed hypothetical function. I
want to say "if F has some specified properties then some given
variant, F0 of F, has the same properties".

First, "F has property HE":

locale fixF = fixes F :: sometype
begin
abbreviation HE :: "bool" where "HE == ...
...
end
locale HE = fixF + assumes HE[rule_format]: HE

If some F has property HE then some variant, F0, of F depending on an
arbitrary constant, v0, also has that property. I can say:

locale HEv0 = HE + fixes v0 :: sometype =
definition F0 :: Ftyp where "F0 X = (if ... then v0 else F X)"
lemma shows "fixF.HE F0"
proof (... using HE ...) qed

If we interpret locale HEv0 with some actual FF and vv, we get a
context where F is interpreted by FF, v is interpreted by vv, and

"fixF.HE (%X. if ... then vv else FF X)"

is a theorem. This is as expected. But we have proved that given FF
(with property HE) and vv then (%X. if ... then vv else FF X)
is a good interpretation of locale HE.

Is there a locale expression (?) that when interpreted with with FF
and vv, gives the context of HE interpreted with
(%X. if ... then vv else FF X)? (Maybe using a "where" clause?)

Thanks,
Randy

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

view this post on Zulip Email Gateway (Aug 18 2022 at 13:54):

From: Clemens Ballarin <ballarin@in.tum.de>
Quoting Randy Pollack <rpollack@inf.ed.ac.uk>:

Where can I find documentation about sublocales? The Isabelle/Isar
Reference Manual (2009) apparently does not contain the string
"sublocale". The Tutorial to Locales and Locale Interpretation (2009)
does not include the syntax that Andreas suggested to me:

sublocale HEv0 < F0HE : HE "%X. if ... then v0 else F X"
unfolding F0_def[symmetric]

The tutorial is currently the only documentation for this feature.

F0HE : HE "%X. if ... then v0 else F X"

is a correct expression according to the grammar given in the tutorial
on page 16. It consists of a single instance with qualifier F0HE,
qualified name HE and term "%X. if ... then v0 else F X". The effect
of the command is an interpretation of the specified instance of HE
relative to HEv0. Note that the scope of the parameters of HEv0
extends over the expression.

Clemens

--
Andreas Lochbihler writes:

Hi Randy,

Is there a locale expression (?) that when interpreted with with FF
and vv, gives the context of HE interpreted with
(%X. if ... then vv else FF X)? (Maybe using a "where" clause?)
If I understand you correctly, you want to have an interpretation of HE
for F0 (with the F0's definition unfolded) whenever you interpret HEv0.
You can do this by making HEv0 a sublocale of HE with F
instantiated to F0:

sublocale HEv0 < F0HE : HE "%X. if ... then v0 else F X"
unfolding F0_def[symmetric]
by(unfold_locales)(rule HEF0)

where HEF0 refers to your lemma that shows "fixF.HE F0".

Now, whenever you interpret HEv0, this also interprets HE with F0
unfolded. The constants and lemmas generated by this process are
prefixed by F0HE to distinguish them from those that obtained directly
from HE. Also, already inside the HEv0 locale, you can access the HE
context for F0.

Is that what you wanted?

Regards,
Andreas

Randy Pollack schrieb:

I'm reasoning about a properties of a fixed hypothetical function. I
want to say "if F has some specified properties then some given
variant, F0 of F, has the same properties".

First, "F has property HE":

locale fixF = fixes F :: sometype
begin
abbreviation HE :: "bool" where "HE == ...
...
end
locale HE = fixF + assumes HE[rule_format]: HE

If some F has property HE then some variant, F0, of F depending on an
arbitrary constant, v0, also has that property. I can say:

locale HEv0 = HE + fixes v0 :: sometype =
definition F0 :: Ftyp where "F0 X = (if ... then v0 else F X)"
lemma shows "fixF.HE F0"
proof (... using HE ...) qed

If we interpret locale HEv0 with some actual FF and vv, we get a
context where F is interpreted by FF, v is interpreted by vv, and

"fixF.HE (%X. if ... then vv else FF X)"

is a theorem. This is as expected. But we have proved that given FF
(with property HE) and vv then (%X. if ... then vv else FF X)
is a good interpretation of locale HE.

Is there a locale expression (?) that when interpreted with with FF
and vv, gives the context of HE interpreted with
(%X. if ... then vv else FF X)? (Maybe using a "where" clause?)

Thanks,
Randy

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Last updated: May 03 2024 at 04:19 UTC