Email Gateway (Aug 18 2022 at 16:04): Email Gateway (Aug 18 2022 at 16:04):From: Matej Urbas <mu232@cam.ac.uk>
Hello all,
I hope you don't mind a question about locales:
Is it possible to provide function definitions within locales (before
the 'assumes' block)?
Some of my locale's assumptions refer to functions which need not be
locale parameters. I want to provide full definitions for such functions
within the locale (after the parameters and before the assumptions). See
example below:
========== A silly example ==========
types
zone = "nat"
myregion = "zone set"
myfoo = "nat"
record 'e foo_rec =
zone_map :: "zone ⇒ 'e set" ("zmapı _" [80] 70)
foo_map :: "myfoo ⇒ 'e" ("fmapı _" [80] 70)
foo_habitat :: "myfoo ⇒ myregion" ("fhabı _" [80] 70)
locale foo =
fixes d :: "('e, 'a) foo_rec_scheme" (structure)
(* Problem here: I want to say that a mapped 'foo' is an element
of its habitat, but the 'rmap' function is not defined yet. *)
assumes mapped_foo_in_region: "(fmap f) ∈ rmap (fhab f)"
begin
(* I would like this function to be just above 'assumes' -- to make
it accessible within 'mapped_foo_in_region.' *)
fun myregion_map :: "myregion ⇒ 'e set" ("rmap _" [80] 70)
where
"myregion_map r = (⋃z ∈ r. zmap z)"
end
=====================================
Apologies if this has been answered before.
Cheers,
Matej
signature.asc
Email Gateway (Aug 18 2022 at 16:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Matej,
This in the strictest sense is not possible. You can circumvent this in
one of the following ways.
a) Introduce intermediate locale where you just define the function
formally and then import this locale into the main locale with
assumptions about the function
b) Turn the function itself into a parameter of the locale and assume
its desired properties explicitly.
It depends on what you want to model which option makes more sense.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 16:04):From: Matej Urbas <mu232@cam.ac.uk>
Mhm, I see. I was already eyeing the intermediate locale approach. It is
actually quite a natural 'workaround.'
Thank you very much indeed.
Cheers,
Matej
signature.asc
Email Gateway (Aug 18 2022 at 16:05):From: Makarius <makarius@sketis.net>
Here is an alternative version: since you have started with "indexed
syntax" already (a relatively old feature predating proper definitions
within locales) it can be done like this:
types
zone = "nat"
myregion = "zone set"
myfoo = "nat"
record 'e foo_rec =
zone_map :: "zone \<Rightarrow> 'e set" ("zmap\<index>")
foo_map :: "myfoo \<Rightarrow> 'e" ("fmap\<index>")
foo_habitat :: "myfoo \<Rightarrow> myregion" ("fhab\<index>")
fun myregion_map :: "('e, 'a) foo_rec_scheme => myregion \<Rightarrow> 'e
set" ("rmap\<index>")
where
"rmap\<^bsub>d\<^esub> r = (\<Union>z \<in> r. zmap\<^bsub>d\<^esub> z)"
locale foo =
fixes d :: "('e, 'a) foo_rec_scheme" (structure)
assumes mapped_foo_in_region: "(fmap f) \<in> rmap (fhab f)"
Makarius
Email Gateway (Aug 18 2022 at 16:06):From: Matej Urbas <mu232@cam.ac.uk>
I see. Thank you very much indeed. This definitely fits my purpose.
Cheers,
Matej
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC