Re: [isabelle] Function Definitions Within Locales

On Mon, 13 Sep 2010, Matej Urbas wrote:

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:

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:

  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>")
  "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)"


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.